The execution environment of OlaVM can be viewed as a state machine, where the execution of each instruction causes the state of the state machine to flow. The circuits of OlaVM is used to constrain:

  • The state of the OlaVM before the program is executed is correct.

  • The correct program is loaded for execution.

  • The correct state of the OlaVM is streamed with each instruction executed.

World State Tree

We use a Sparse Merkle Tree(SMT) to store all the data, and the data stored under each contract is mapped to this tree.

In this way, the state of OlaVM Storage can be represented by the root of the Word State Tree. The World State Tree receives commands from the cpu to query or update the state, and the values of reads and writes are stored in the MemoryTable. At the same time, the construction of the world state tree requires hash operations, and the correctness of the hash is taken care of by the PoseidonTable. The above tables are associated with StorageAccessTable through cross table lookup.

Correctness of Program

The process of deploying a contract in OlaOS, for the state of the world, is essentially a hash operation on the bytecode of a smart contract and saving the result into a slot in the state of the world state tree. When the contract is invoked externally, the address of the invoked contract is specified, and OlaOS is responsible for loading the contract source code into OlaVM. The information we have now:

  • Contract source bytecode and deployment address.

  • All executed instructions. The constraints we need to perform are:

  • The executed instructions are contained in the contract source bytecode.

  • The hash value of the contract bytecode is stored in the deployment address of the world state tree. We introduce two new tables: ProgramTable and ProgChunkTable:

The CpuTable contains all executed instructions, and the ProgChunkTable contains the source code of the contract. ProgramTable is guaranteed to contain all executed instructions by lookup with the CpuTable, and the ProgramTable is guaranteed to contain the source bytecode by lookup with the ProgChunkTable. The ProgramTable constrains all executed instructions to be included in the contract's source code. ProgChunkTable constrains the correctness of contract source bytecode hash calculation by cross-table lookup with PosedionTable, and at the same time, cross-table lookup with StorageAccessTable ensures that the value stored in the contract deployment address in the world state tree is indeed the hash of the source code. Through the above process, we can ensure that the program we execute is correct.

Correctness of Instructions Execution

In the previous sections, we have constrained the correctness of the executed statements, now we continue to constrain the correctness of the execution logic. The instruction is disassembled into opcode selectors, operand selectors, and OP1_IMM, a flag bit that indicates whether or not op1 is an immediate number, according to the encoding rules. The result of this disassembly is constrained to be correct by a linear combination of the encoding rules. In the same way, we disassemble the opcode into opcode selectors, and the correct operand selector in combination with OP1_IMM can be used to constrain DST, OP0, OP1 to be the correct register or immediate number. The correct opcode selector then constrains the relationship between DST, OP0, OP1.

In addition to arithmetic commands, memory operations, storage operations and other commands need to be combined with other tables for cross-table-lookup constraints, we do not do too much to expand, but only a brief description of the main logic of the constraints here.

Last updated