first level title

Miden proof system architecture

miden is a zkvm implementation based on strark technology. Its bottom layer is based on the zkp library of winterfell to generate stark proofs and verify the proofs. The dotted line in Figure 1 below is the main function implemented by Miden. It can be seen that there are mainly three components.

1. A set of lexical grammar compiler, lexical analyzer and syntax parser in Figure 1 below. They can program the assembly instructions defined by miden into opcode and op value contained in codeblock and block.

3. A set of AIR (Algebraic Intermediate Representation) that meets the stark proof requirements, the AIR in Figure 1 below. It is used to constrain the execution process of miden's virtual machine.

first level title

AIR structure design

The constraints of AIR are divided into two parts: stack and decoder:

Figure 3 shows the constraints of the decoder. Among them, op_counter, op_sponge, cf_op_bits, ld_op_bits, hd_op_bits are fixed column lengths. Among them, op_sponge is used to constrain the order and correctness of executing instructions. cf_op_bits constrains 3bit flow_ops. ld_op_bits, hd_op_bits constrain the low 5bits and high 2bits of user_ops respectively. The combination of ld_op_bits and hd_op_bits constitutes an executed user_op, and is also used as a selector for each step state constraint of the stack.

first level title

Miden VM execution process instance

This section will show a simple miden logic to illustrate the execution process of vm and the generation of stark's execution trace.

Code segment 1 below is the code segment to be executed:

The logic it executes is to push 3 and 5 onto the stack. Then read the flag from the tape. Determine whether the flag is 1 or 0. If it is 1, run the if.true branch to take out the two numbers 3 and 5 that were pushed on the stack, add them together to get 8 and push it back on the stack. If it is 0, run the else branch to take out the two numbers 3 and 5 that were pushed on the stack and multiply them to get 15, and then push 15 back into the stack.

The final instruction code after the code segment is parsed by miden's lexical and grammatical analyzer is as follows Code segment 2:

Figure 4 below shows the process of vm running code segment 2. In the middle is the flowchart of executor executing opcode. The dotted line on the left points to the decoder trace generated by code execution, and the dotted line on the right points to the stack trace generated by code execution.

Among them, the executor is executed one by one according to the code block. In this example, a span block is executed first. Then execute the if-else-end structure at step 32 to enter the swtich block, and push the sponge hash generated by the last step of the previous span block into ctx_stack, and after the swtich block is executed, at step 49 Pop into the sponge.

Note: This document describes the latest version of the main branch for the miden project. At present, the next branch of miden has redesigned a lot of instructions, and AIR only implements a small part of the constraints.

stack constraints

conditional instruction

Choose

Constrain:

text

text

add

Constrain:

mul

Constrain:

inv

Constrain:

neg

Constrain:

boolean directive

not

Constrain:

and

Constrain:

or

Constrain:

hash command

RESCR

text

Occupies 6 registers

Constrain:

comparison instruction

eq

Constrain:

cmp

text

A: [0,1,0,1]

B: [0,0,1,1]

Need to compare 4 times

Constrain:

text

dup.n

Constrain:

swap

Constrain:

ROLL4

Constrain:

first level title

Decoder constraints

user code execution

op_bits

text

Constraints for cf_op_bits, ld_op_bits, 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 be 0 at the same time.

Constraint 3: When cf_op_bits is hacc. The op_counter status will be incremented by 1.

Constraint 4: BEGIN, LOOP, BREAK, and WRAP instructions require 16 alignment

Constraint 6: PUSH instruction requires 8 alignment

hacc

hacc is used as flowOps, each execution of this instruction will cause the state of the sponge to change, which needs to be constrained

conditional judgment

t_end

text

The constraint that is the end of the true branch of if is divided into two parts:

Constraint 1: The constraint of the sponge state, the value at the top of the pop-up stack is equal to new_sponge_0. The sponge after the execution of the last step of the true branch of if is equal to new_sponge_1. new_sponge_3 is equal to 0.

Constraint 3: Constraints of loop_stack. The state of loop_stack does not change.

f_end

text

As the constraint at the end of the false branch of if, it is divided into two parts:

Constraint 1: The constraint of the sponge state, the value at the top of the pop-up stack is equal to new_sponge_0. The sponge after the execution of the last step of the true branch of if is equal to new_sponge_2. new_sponge_3 is equal to 0.

Sin7y was established in 2021 and is composed of top blockchain developers. We are both a project incubator and a blockchain technology research team, exploring the most important and cutting-edge technologies such as EVM, Layer2, cross-chain, privacy computing, and autonomous payment solutions.

about Us

Sin7y was established in 2021 and is composed of top blockchain developers. We are both a project incubator and a blockchain technology research team, exploring the most important and cutting-edge technologies such as EVM, Layer2, cross-chain, privacy computing, and autonomous payment solutions.

WeChat public account: Sin7Y

GitHub | Twitter | Telegram | Medium| Mirror | HackMD | HackerNoon