# Sin7Y Tech Review (24): The Stark Proof System of Miden V1 ![](https://i.imgur.com/TCOmp2o.png) 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. ![](https://i.imgur.com/u2Jia8b.png) 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. ![](https://i.imgur.com/VJuvShE.png) 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. ![](https://i.imgur.com/J29QJ5P.png) 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. ```asm 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: ```asm 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. ![](https://i.imgur.com/MFTy3QP.png) 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: ```Makefile 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: ```Makefile 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 ```
Last changed by  
 
Sin7Y
Exploring #Layer 2, #Crosschain, #ZK, and #Privacy Computing.
767

Read more

無標題

Traditional STARK systems require cyclic groups within the field with a smooth order for efficient processing. FFT (Fast Fourier Transform) is leveraged for efficient calculation of polynomial interpolation points, taking advantage of unit roots with smooth orders in fields. Such fields must have the property of being a power of n to be considered efficient for these operations. However, the efficiency is compromised for fields without this property. Consequently, performing FFT on such fields becomes less efficient. To address this issue, Eli Ben-Sasson and others introduced a fast algorithm for polynomial computations over large finite fields, known as ECFFT (Elliptic Curve Fast Fourier Transform). This algorithm, inspired by Lenstra's methods, extends the applicability of FFT to all prime fields, dramatically enhancing computational capabilities.

4/11/2024
Balancing Privacy between Decentralization and Regulation: Insights from DevConnect Istanbul

During DevConnect Istanbul, I had the privilege of engaging with various project teams and researchers dedicated to privacy-oriented initiatives. We discussed a range of privacy-related topics. To my surprise, I found that the concept of ‘privacy’ is interpreted quite differently by different people, generally falling into two distinct categories:

11/29/2023
Programmable Privacy Could Be More Compliance-Friendly

At Ola, we strongly agree with a16z’s statement in their article “Achieving Crypto Privacy and Regulatory Compliance” about web3:

11/29/2023
Sin7y Tech Review (35) Hybrid Rollup - The Next-Generation Infrastructure

A comparative study of Aztec, Miden, and Ola In this article, we delve into the concept of "Hybrid Rollup," examining how projects Aztec, Miden, and Ola approach this technology. We investigate their unique smart contract languages, explore state tree designs, and consider the trade-offs in privacy designs. Our objective is to provide a comprehensive overview of Hybrid Rollup technologies, helping you understand their key components and envision their future trajectory. What is Hybrid Rollup? We are delighted to see that our recent initiatives have been garnering an increasing amount of attention in the market. "Hybrid Rollup" is the most accurate summary of what we at Ola have been working on: Rollup: a. It operates at Layer 2, but it also has the flexibility to function at Layer 3, depending on the platform utilized for the verification contract deployment.b. It's a scalability solution.c. It has programmability - "Rollup" doesn't specifically indicate this feature; "Programmable Rollup" is more accurate. Hybrid: a. It supports public, private, and hybrid contract types.b. Developers can freely choose the contract type based on their needs.c. Users can freely choose the transaction type in hybrid contracts.

6/13/2023
Read more from Sin7Y
Published on HackMD