In zkWasm, the arrangement of each instruction's related states occupies 4 rows within the circuit table, defined as instruction_rows. Constraints are established within these four rows and between successive instruction_rows. See the code here.

While zkWasm employs Halo2's API, it defines a custom circuit layouter with three main differences from Halo2:

• Column Type Bounds: Each column is bound by a range constraint. This includes BitColumn, CommonRangeColumn (ranging from 0 to 1 << zkwasm_k() - 1), U16Column, U32Column, U64Column, JTableLookup, MTableLookup, etc. For ease of reference later, we collectively refer to all these columns as TypeColumn.

• Gate Constraint Building: Constructing gate constraints involves querying related cells and creating gates. To query a cell, an alloc function is utilized to obtain an unused cell of a TypeColumn within the current instruction_rows (akin to a conceptual region in Halo2). Moreover, after allocating one cell, the subsequent cell of the same type will be assigned to the next cell in that column. If allocation extends beyond the fourth row, allocation restarts from the first row of the subsequent column of the same type (See code). The code utilizes a BTreeMap named free_cells to record the allocation of each type of cell up to which column's first row. When creating gates for an instruction, a constraint builder is encapsulated (e.g., integer addition here) and then finalized to call Halo2's create gate API.

• Lookup: During a lookup, zkWasm encodes cells to be looked up into an auxiliary cell and constrains the encoding equation. Then, it looks up the auxiliary cell in another table's encoded cell. An example is the op_br instruction's encode_memory_table_entry.

For instance, let's consider etable. A log_cell macro has been integrated into the etable code to log the location of cells by their col and row.

After running the following simple test case, the cell's Column and Rotation will be printed.

cargo test test_uniform_verifier -- --show-output

The i32.Add instruction in WebAssembly is a typical binary operation binop(wasm spec). zkWasm's implementation of Call is here. Its execution involves several steps:

1. Pop the value lhs from the stack.
2. Pop the value rhs from the stack.
3. Compute the result res = lhs + rhs.
4. Push the value res onto the stack.

The constraints associated with this operation are defined by mathematical equations and rules to ensure correct execution within the WebAssembly framework. These constraints can be summarized as follows:

1. Mathematical Equation Constraint: lhs + rhs − res + isoverflow * 1<<32 = 0 This equation ensures that the arithmetic operation is correct even when overflow happens. The add gate circuit is defined here.

2. Instruction Address Constraint: iaddr.curr + 1 − iaddr.next = 0.

   • This constraint manages the flow of instructions within the WebAssembly execution and maintain the order of operations.
   • The circuits pertaining to the stack pointer (sp) and instruction addresses (iaddr) in zkwasm are situated within the same context as other instructions.
   • The iaddr tuple comprises the modular ID (moid), memory block instance ID (mmid), function ID (fid), and instruction offset within a specific function (iid). Given that moid and mmid remain constant, only fid and iid are constrained within zkwasm to ensure the proper execution flow and adherence to WebAssembly's specifications.

3. Stack Pointer Constraint: sp.curr + 1 - sp.next = 0 As the WebAssembly stack grows downwards, these constraints handle the stack pointer adjustments after popping or pushing values onto the stack.

4. Memory Table Constraints:

   Plookup(MemoryTable, (StackType, read, sp.curr + 1, rhs)) = 0
   Plookup(MemoryTable, (StackType, read, sp.curr + 2, lhs)) = 0
   Plookup(MemoryTable, (StackType, write, sp.curr + 2, res)) = 0
   

   • These constraints ensure proper memory table lookups and operations related to the stack values involved in the i32.Add instruction.
   • Note that the stack pointer for the resulting value res is determined as sp.curr + 2. This adjustment is due to the nature of WebAssembly's stack, which grows downwards. Consequently, when an item is popped from the stack, the stack pointer effectively decreases by 1.
   • This behavior is reflected in the implementation of the WebAssembly interpreter. Circuit for 3 Plookups's encoded cells for lookup are defined here

These configurations and constraints collectively ensure the correct handling of binary operations, including i32.Add, within the zkwasm framework, aligning with WebAssembly's stack behavior and execution requirements.

Wasm's Call instruction spec is simple, zkWasm's implementation of Call is here. It involves 3 constraints:

1. Instruction Address Constraint: iaddr.curr − iaddr.next = 0 This makes sure that the next instruction addr is call instruction's target jump addr. This constrain involves next_fid and next_iid function, fid change gate and iid change gate.

2. Stack Pointer Constraint: sp.curr - sp.next = 0 This ensures there is no stack change. This constrain is implemented along with other instructions.

3. Call Frame Constraint: eid.curr - frame_id.next = 0 This ensures the following instruction's previous call frame is the current call frame. This constrain involves next_frame_id function and frame_id change gate.

4. Frame Table Constraints:

   Plookup(FrameTable, (
       eid: currentFrame, 
       frame_id_cell: prevFrame, 
       index_cell: iaddr.next.fid, 
       fid_cell: iaddr.curr.fid, 
       iid_cell: iaddr.curr.iid + 1)
   )
   

   This helps us to find out the next iaddr of Return instruction, which should be offset by 1 compared to that of current Call instruction. Also, it constrains that Call instruction's next instruction should be in the same call frame with the corresponding Return instruction. And, the corresponding lookup constraint is here.

Wasm's Return instruction spec is a bit more complicated compared to Call. Especially, wasm current doesn't support multiple returns. Follow zkWasm interpreter's Return implementation, self.value_stack.drop_keep(drop_keep) is the most important part. So, according to the implementation, Return involves the following constraints:

| prev call frame  |
| curr call frame  |  <-- write 1 kept value to next call frame (sp + drop + 1)
|  - arg 1         |        |
|  - arg 2         |        |
+------------------+        |
| callee locals    |        | <-- the number of dropped values is `drop`
|  - var 1         |        |
|  - var 2         |        |
+------------------+        |
| operands         |        |
|  - op 1          |        |
|  top value       |  <-- kept value (sp + 1)
|  return          |  <-- current stack pointer (sp)
+------------------+

1. MemoryTable Read Constraint: Plookup(MemoryTable, (StackType, sp.curr + 1, return_value)) keep = 0. The above constrain is enabled when keep = 1, which means the top value will be kept before "discarding" the current stack frame. The circuit of encoded cell for lookup is defined here.

2. MemoryTable Write Constraint: Plookup(MemoryTable, (StackType, sp.curr + 1, return_value)) keep = 0. The above constrain is enabled when keep = 1. This ensures the kept value written to top of the next stack frame. The circuit of encoded cell for lookup is defined here.

3. FrameTable Constraint: This ensures Return instruction finds the correct next instruction. It's the same as the corresponding Call instruction. The circuit of encoded cell for lookup is defined here

Wasm's heap load instruction specification can be found here. However, due to zkWasm's utilization of a 64-bit word size to adhere to the specification, the 64-bit word-length rw_table introduces not one, but two memory-word-length constraints when performing cross-block reads and writes (refer to related implementation in zkwasm's interpreter). Consequently, the load instruction for the heap primarily encounters the following constraints:

1. MemoryTable Read Constraints: Plookup(MemoryTable, (HeapType, load_block)) = 0 Plookup(MemoryTable, (HeapType, load_block + 1)) = 0 This ensures memory are loaded from specific offset(load_block and the next block) in heap. The circuit of encoded cell for lookup is defined here.

2. MemoryTable Write Constraint: Plookup(MemoryTable, (Stack, load_block)) = 0 This ensures the heap/stack/global loaded value are written to the value stack. The circuit of encoded cell for lookup is defined here.

3. Other constraints such as the length, offset, loaded value size check, etc.

In zkWasm, the ImageTable consists of a column memory_addr_sel to store memory addresses (which increase row by row), and a column col to store the corresponding values of these memory addresses.

In the Continuation, the memory at the start of the program execution is referred to as pre_image_table, and the memory after program execution is referred to as post_image_table. Both are configured using the ImageTable.

Constraints for post_image_table are as follows:

• post image table: update gate: If a memory address has not been written to (update selector = 0), it should be the same as the col in the same row of pre_image_table.

• post image table: memory_finalized_lookup_encode gate: If a memory address has been written (updateselector = 1), it should be the same as the last written value for that address. Additionally, through the lookup gate, it ensures that the value of memory_finalized_lookup_encode is indeed the last written value for that address. lookuped value of memory_finalized_lookup_encode lies in MemoryTableConfig's post_init_encode_cell, corresponding to post init memory entry gate.

  • To dive a little bit into this gate, as the rows in MemoryTableConfig are sorted by address and eid, the constraint to determine the last written value for a certain address is: it is not an initialized value and it is the last row for that memory address. Then, the corresponding value is written into post_init_encode_cell for the purpose of lookup.