# Sin7Y Tech Review (24): The Stark Proof System of Miden V1


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.
1. One set of lexical syntax compilers, that is the lexical analyzer and syntax parser in Figure 1. They can program the assembly instructions defined by Miden into codeblock or the opcode and op value contained in the block.
2. One set of instruction executors, that is the executor in Figure 1. It will execute the codeblock and the opcode and op value contained in the block according to the defined rules. And the executed results will be the execution trace used for generating the proof.
3. One set of AIR(Abstract Inter-mediate Representation), satisfying the requirements of the stark proof, that is the AIR in Figure 1. It conducts constraints to the execution process of the Miden Virtual Machine.

Figure 1. Miden project components

## AIR Structural Design Drawing
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

## Execution process example of Miden VM

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.

begin 
    push.3 
    push.5 
    read 
    if.true 
        add
    else 
        mul 
    end 
end

Code segment 1

The final instruction code parsed by Miden's lexical analyzer and syntax parser is shown in the following code segment 2:

begin 
noop noop noop noop noop noop noop 
push(3) noop noop noop noop noop noop noop 
push(5) read noop noop noop noop noop noop 
noop noop noop noop noop noop noop,

if 
assert add noop noop noop noop noop noop 
noop noop noop noop noop noop noop 
else 
not assert mul noop noop noop noop noop 
noop noop noop noop noop noop noop 
end]

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.

## Constraint conditions of the stack

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.

### Condition instruction

#### Choose

Constraint:

new_stack_0 == (condition * x) + ((1 - condition) * y)

 old_stack_0 == x
 old_stack_1 == y
 old_stack_2 == condition
  
 old_stack_3  --> new_stack_1
 old_stack_n. --> new_stack_n-2
 
 aux_0 == condition.is_binary == true

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.

### Arithmetic instruction

#### add

Constraint:

old_stack_0 + old_stack_1 == new_stack_0
old_stack_2  --> new_stack_1
old_stack_n. --> new_stack_n-1

#### mul

Constraint:

old_stack_0 * old_stack_1 == new_stack_0
old_stack_2  --> new_stack_1
old_stack_n. --> new_stack_n-1

#### inv

Constraint:

old_stack_0 * new_stack_0 == 1
old_stack_1  --> new_stack_1
old_stack_n. --> new_stack_n

#### neg

Constraint:

old_stack_0 + new_stack_0 == 0
old_stack_1  --> new_stack_1
old_stack_n. --> new_stack_n

### Bool instruction

#### not

Constraint:

aux_0: make sure old_stack_0 is binary

1-old_stack_0 ==  new_stack_0 
old_stack_1  --> new_stack_1
old_stack_n. --> new_stack_n

#### and

Constraint:

aux_0: make sure old_stack_0 is binary
aux_1: make sure old_stack_1 is binary

old_stack_0 * old_stack_1 == new_stack_0
old_stack_2  --> new_stack_1
old_stack_n. --> new_stack_n-1

#### or

Constraint:

aux_0: make sure old_stack_0 is binary
aux_1: make sure old_stack_1 is binary

1- (1-old_stack_0) *(1- old_stack_1) == new_stack_0
old_stack_2  --> new_stack_1
old_stack_n. --> new_stack_n-1

### Hash instruction

#### RESCR

Limit function hash satisfying hash function protocol
Occupying 6 registers

Constraint:

hash(old_stack0，old_stack1， old_stack2， old_stack3， old_stack3， old_stack5) == 
（new_stack0，new_stack1， new_stack2， new_stack3， new_stack3， new_stack5）

old_stack_6  --> new_stack_6
old_stack_n. --> new_stack_n

### Compare instruction

#### eq

Constraint:

aux_0 == new_stack_0 * diff == 0

new_stack_0 == 1- (old_stack_1-old_stack_2)*old_stack_0

old_stack_0 == inv(old_stack_1-old_stack_2)

old_stack_3  --> new_stack_1
old_stack_n. --> new_stack_n-2

#### cmp

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:

// layout of first 8 registers
// [pow, bit_a, bit_b, not_set, gt, lt, acc_b, acc_a]
    
// x and y bits are binary
new_stack_1 == x_big_idx(lg lt flag) （type:binary)
new_stack_2 == y_big_idx(lg lt flag) （type:binary) 


bit_gt = x_big_idx*(1-y_big_idx)
bit_lt = y_big_idx*(1-x_big_idx)

// comparison trackers were updated correctly
new_stack_3 = not_set_idx

new_stack_4(gt) == old_stack_4(gt_idx) + bit_gt * not_set_idx
new_stack_5(lt) == old_stack_5(lt_idx) + bit_lt * not_set_idx 

 // binary representation accumulators were updated correctly
old_stack_0 = POW2_IDX

old_stack_6 = Y_ACC_IDX
old_stack_7 = X_ACC_IDX

new_stack_6 == old_stack_6 + x_big_idx * old_stack_0(power_of_two);
new_stack_7 == old_stack_7 + y_big_idx * old_stack_0(power_of_two);

// when GT or LT register is set to 1, not_set flag is cleared

not_set_check = (1-old_stack_5(lt_idx))*(1-old_stack_4(gt_idx))
not_set_check == new_stack_3(not_set_idx)

// power of 2 register was updated correctly

new_stack[POW2_IDX] * two == old_stack[POW2_IDX]

old_stack_8  --> new_stack_8
old_stack_n  --> new_stack_n

### Stack operation instruction

#### dup.n

Constraint:

new_stack_0 == old_stack_0
...
new_stack_n-1 == old_stack_n-1

old_stack_0  --> new_stack_n
old_stack_k  --> new_stack_n+k

#### swap

Constraint:

new_stack_0 == old_stack_1
new_stack_1 == old_stack_0

old_stack_2  --> new_stack_2
old_stack_n  --> new_stack_n

#### ROLL4

Constraint:

new_stack_0 == old_stack_3
new_stack_1 == old_stack_0
new_stack_2 == old_stack_1
new_stack_3 == old_stack_2

old_stack_4  --> new_stack_4
old_stack_n  --> new_stack_n

## Constraint condition of decoder

In this section, we will show the constraint conditions of the main Flow operation instruction.

### User code execution

#### op_bits

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:

cf_op_bits == binary
ld_op_bits == binary
hd_op_bits == binary

// ld_ops and hd_ops can be all 0s at the first step, but cannot be all 0s at any other step
op_counter * binary_not(ld_bit_prod) * binary_not(hd_bit_prod) == 0


if op_counter != 0
    (1-ld_bit_prod)*(1- hd_bit_prod) == 0

if is_hacc != true
    op_counter = current.op_counter
    

// BEGIN, LOOP, BREAK, and WRAP are allowed only on one less than multiple of 16

// TEND and FEND is allowed only on multiples of 16

// PUSH is allowed only on multiples of 8

#### hacc

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:

mds(sbox(old_sponge) + user_opcode(7bits) + op_value(push_flag=1))  == sbox(inv_mds(new_sponge)) 

### Condition judgment

#### t_end

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:

parent_hash = current.ctx_stack()[0]
block_hash = current.op_sponge()[0]
new_sponge = next.op_sponge()

parent_hash ==  new_sponge[0]
block_hash == new_sponge[1]
new_sponge[3] == 0

// make parent hash was popped from context stack
ctx_stack_start = OP_SPONGE_WIDTH + 1 // 1 is for loop image constraint
ctx_stack_end = ctx_stack_start + ctx_stack_current.len()
ctx_result = &mut result[ctx_stack_start..ctx_stack_end]

ctx_stack_current_0 = ctx_stack_next_1
ctx_stack_current_1 = ctx_stack_next_2
...
ctx_stack_current_n = ctx_stack_next_n+1

// loop_stack copy
copy range: ctx_stack_end  to. ctx_stack_end + loop_stack_current.len()
loop_stack_current_0 = loop_stack_next_0
...
loop_stack_current_n = loop_stack_next_n

#### f_end

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:

parent_hash = current.ctx_stack()[0]
block_hash = current.op_sponge()[0]
new_sponge = next.op_sponge()

parent_hash ==  new_sponge[0]
block_hash == new_sponge[2]
new_sponge[3] == 0

// make parent hash was popped from context stack
ctx_stack_start = OP_SPONGE_WIDTH + 1 // 1 is for loop image constraint
ctx_stack_end = ctx_stack_start + ctx_stack_current.len()
ctx_result = &mut result[ctx_stack_start..ctx_stack_end]

ctx_stack_current_0 = ctx_stack_next_1
ctx_stack_current_1 = ctx_stack_next_2
...
ctx_stack_current_n = ctx_stack_next_n+1

// loop_stack copy
copy range: ctx_stack_end  to. ctx_stack_end + loop_stack_current.len()
loop_stack_current_0 = loop_stack_next_0
...
loop_stack_current_n = loop_stack_next_n