Overview:
Setup input:
wasm code
Runtime input:
input of wasm function and the top level function must be main.
Proving target
simulation of wasm execution of target wasm bytecode with particular inputs are correct.
Static Data:
Instruction Table
Instruction Table[ITable] is a [FIXED] map reprensents the wasm code image.
ITable: address
Initial Memory Table
Initial Memory Table[MTable] is [FIXED] and represents the heap memory of wasm.
IMTable: heap memory index
Execution Trace Table:
Exexution Trace Table [ETable] is used to verifying that the execution sequence enforces the semantics of each instruction's bytecode.
ETable: eid execution
Jump table
(eid, return address, last jump eid)
Memory Trace Table
((eid+empty, stack + heap) -> memory access log empty for heap memory initialization (verifies data access)
Extra
public inputs for top level functions
(index
Prerequisite
Memory Access Log
Memory access log is used to describe how memory is used.
- MemoryAccessLog = ((Init + Write + Read), (i32/64+f32/64), data)
Sujective map
Suppose that A, B are tables, A = (
Polynomial lookup can prove
- find l' from
${b_i}$ to${a_i}$ . - compare row numbers of
$A$ and$B$ and make sure${a_i}$ are unique and$f(a_i) \neq f(a_j)$ when$a_i \neq a_j$ .
Circuits
Static Table:
ITable + IMTable
Dynamic Table:
ETable, MTable, JTable
Instruction Table (ITable)
Instruction encodes the static predefined wasm image and is abstracted as a table of pair (InstructionAddress, Instruction).
- InstructionAddress = (ModuleId, FunctionId, InstructionId)
- Opcode = (OpcodeClass + InnerParameters)
- MemoryAddress = (Stack + Heap, ModuleId, offset)
- for stack memory, its ModuleId always equals 0.
- for heap memory, its Module Id start from 1.
- offset: start from 0.
Init memory table (IMTable)
Init memory table describes the initial data of heap before execution and is abstracted as a table of pair IMTable = (HeapMemoryIndex, data)
Execution table (ETable):
Execution table represents the execution sequence and it needs to match the semantic of each opcode in the sequence.
ETable [$T_e$] = (EId, Instruction, SP,restMops, lastJumpEId, RestJops)
-
$eid$ starts from 1 and inc one after each instruction in the ETable. -
$\forall e \in \mathbb{T_e}$ there exists$e'\in \mathbb{T_i}$ such that$e.instruction = e'.instruction$ . This constraint proves that each executed bytecode exists in the instruction table. -
$\forall e_k, e_{k+1} \in T_e$ $e_k.eid + 1= e_{k+1}.eid$ -
$e1.next(e1.address) = e2.address$ .
-
lookup(EID, Instruction, SP) --> mtable
- (
$eid$ ,$i$ ,$sp$ ) is unique - map from etable to mtable is identical mapping
- It remains to show two table has same number of memory rw rows:
- Suppose that
$e$ is the last element of$\mathbb{T_e}$ , then$e.restMops = 0$ .
- Suppose that
- (
-
sp -> stack memory log [emid] 存在于 mtable
- mtable log = init + execution
-
Example
EID OP accessType Address value eid op write address data ... .. .... ..... ... eid op read address data
Memory Access Table (MTable)
MTable [$T_m$] = ( eid, emid, address, accessType, type, data)
- Suppose that
$r_k$ and$r_{k+1}$ in MTable and$r_{k}.accessType = write$ and$r_{k+1}$ .accessType = Read$ Then$r_{k+1}.data = r_k.data$ - Suppose that
$r_k$ and$r_{k+1}$ in Mtable, addressCode(r_k) <= addressCode(r_{k+1}) where addressCode(r_k) = address << 2 + emid
Operations Spec [WIP]
We uses z3 (https://github.com/Z3Prover/z3) to check that all operation are compiled to zkp circuits correctly.
[This is a WIP project, only sample code are provided here. Please contact xgao@zoyoe.com for state circuit customization and application integration.