Miden is a stark technology-based ZKVM implementation solution. In its basic layer, the stark proof is generated based on the ZKP library and the proof will be verified. The dotted part in the following Figure 1 is the main function implemented by Miden. It mainly consists of three components.
Figure 1. Miden project components
AIR's constraints divide into stack and decoder:
Figure 2 shows the stack's constraints, distributed with a stack with a top depth of 8 at initialization. The max_depth is incremented as needed if the initial distribution may be exceeded during the execution, depending on program needs, but it must not exceed the maximum depth of 16, otherwise, an error is reported.
Figure 2: Column of stack constraint
As can be seen below, Figure 3 shows the constraints of the decoder. Among these constraints, op_counter, op_SPONGE, CF_OP_bits, LD_OP_BITS, and hd_OP_bits are fixed column lengths. The op_sponge is used to constrain the order and correctness of instructions. The cf_op_bits constrains the 3-bit flow_ops. The ld_op_bits and hd_op_bits constrain the low 5 bits and high 2 bits of user_ops, respectively. The ld_op_bits and hd_op_bits combine to form an executable user_op that is also used as a selector for each step of the stack's state constraints.
Figure 3: Column of decoder constraint
This section shows simple Miden logic to illustrate the execution of the virtual machine and the generation of stark's execution trace.
The following code segment 1 is the segment to execute:
Its execution logic is to push 3 and 5 on the stack. Then read the flag from the tape. Check whether the flag is 1 or 0. If it is 1, run the "if.true logic" to take the two numbers 3 and 5 which are pushed on the stack, add them together, resulting in 8, and push 8 on the stack. If it's 0, run the "else logic" to take the numbers 3 and 5 and multiply them together resulting in 15, and then push 15 on the stack.
Code segment 1
The final instruction code parsed by Miden's lexical analyzer and syntax parser is shown in the following code segment 2:
Code segment 2
Figure 4 shows the process of the virtual machine executing code segment 2. The middle part is the flowchart of the executor executing opcodes. The left dotted lines refer to the decoder trace generated in the code execution. The right dot-dash lines refer to the stack trace generated in the code execution.
In the figure, the executor conducts executions block by block according to the code block. In this example, a span block is executed first. Then the if-else-end structure at step 32 is performed to enter the switch block and press the sponge hash generated by the last execution of the previous span block into the ctx_stack. After the switch block is executed, pop it into the sponge at step 49.
Figure 4: the state change figure of the VM executing opcode
Note: This document describes the latest version of the main branch for Miden projects as of 2022-05-27. So far Miden's next branch has done a lot of redesigning of instructions, and AIR has implemented only a few constraints.
In this section, we will show the constraint conditions of the main User operation instructions, among which, old_stack_x refers to the value stored at the x position of the stack before the instruction execution, new_stack_x refers to the value stored at the x position of the stack after the instruction execution, "–>" refers to the copy of the value from the left side of the stack to the right, and "==" refers to the equation constraint. The constraints of the stack are relatively simple, and no explanation is required.
Constraint:
If the condition is 1, x is at the top of the stack. If the condition is 0, y is at the top of the stack.
Constraint:
Constraint:
Constraint:
Constraint:
Constraint:
Constraint:
Constraint:
Limit function hash satisfying hash function protocol
Occupying 6 registers
Constraint:
Constraint:
Compare according to the bit length cycle of the two numbers to be compared, such as:
A: [0,1,0,1]
B: [0,0,1,1]
The compare instructions need to be executed four times.
Constraint:
Constraint:
Constraint:
Constraint:
In this section, we will show the constraint conditions of the main Flow operation instruction.
For the constraints of cf_op_bits, ld_op_bits and hd_op_bits
Constraint 1: each bit can only be 0 or 1.
Constraint 2: when op_counter is not 0, ld_ops and hd_ops cannot both be 0.
Constraint 3: when cf_op_bits is hacc, the op_counter state will increase by 1.
Constraint 4: BEGIN, LOOP, BREAK, and WRAP instructions need to be aligned according to 16.
Constraint 5: TEND and FEND instructions need to be aligned according to 16.
Constraint 6: PUSH instruction needs to be aligned according to 8.
Constraint:
Hacc, as the flowOps, will always cause the state change of sponge when conducting this instruction, and therefore it is needed to perform the constraints.
Constraint:
As the constraint of the true branch end of if, it is divided into two parts:
Constraint 1: is the constraint of the sponge state. The value at the top of the stack is equal to new_sponge_0. The sponge after the last execution of the true branch of if is equal to new_sponge_1. New_sponge_3 is equal to 0.
Constraint 2: is the constraint of ctx_stack. The value at the top of the stack is equal to new_sponge_0. Any other element in the stack will move by one position to the top of the stack.
Constraint 3: is the constraint of loop_stack. The state of loop_stack is changeless.
Constraint:
As the constraint of the false branch end of if, it is divided into two parts:
Constraint 1: is the constraint of the sponge state. The value at the top of the stack is equal to new_sponge_0. The sponge after the last execution of the true branch of if is equal to new_sponge_2. new_sponge_3 is equal to 0.
Constraint 2: is the constraint of ctx_stack. The value at the top of the stack is equal to new_sponge_0. Any other element in the stack will move by one position to the top of the stack.
Constraint 3: is the constraint of loop_stack. The state of loop_stack is unchanged.
Constraint: