基于 STARK 的执行证明流程如何在 Miden V1 上工作？

Miden 是一个基于技术的 ZKVM 实施解决方案。

在其基础层，基于 ZKP 库生成明确的证明，并验证证明。下图1中的虚线部分是Miden实现的主要功能。它主要由三个部分组成。

1. 一组词法语法编译器，即图1中的词法分析器和语法分析器。它们可以将Miden定义的汇编指令编入codeblock或block中包含的opcode和op值。

2. 一组指令执行器，即图1中的执行器。它将按照定义的规则执行代码块以及块中包含的操作码和操作值。执行结果将是用于生成证明的执行跟踪。

3. 一组AIR（Abstract Inter-mediate Representation），满足严格证明的要求，即图1中的AIR，对Miden虚拟机的执行过程进行约束。

图 1. Miden 项目组件

AIR结构设计图

AIR 的约束分为堆栈和解码器：图 2 显示了堆栈的约束，在初始化时与顶部深度为 8 的堆栈一起分布。

如果执行过程中可能超出初始分布，max_depth会根据需要递增，具体取决于程序需要，但不能超过最大深度16，否则会报错。

图 2：堆栈约束列

如下所示，图 3 显示了解码器的约束。在这些约束中，op_counter、op_SPONGE、CF_OP_bits、LD_OP_BITS 和 hd_OP_bits 是固定的列长度。

op_sponge 用于约束指令的顺序和正确性。 cf_op_bits 约束 3 位 flow_ops。 ld_op_bits 和 hd_op_bits 分别约束 user_ops 的低 5 位和高 2 位。

ld_op_bits 和 hd_op_bits 组合形成一个可执行的 user_op，它也用作堆栈状态约束的每个步骤的选择器！

图 3：解码器约束列

Miden VM的执行流程示例

本节展示了简单的 Miden 逻辑来说明虚拟机的执行和 stark 执行跟踪的生成。

下面的代码段 1 是要执行的段： 它的执行逻辑是把 3 和 5 压入栈中。然后从磁带中读取标志。

检查 flag 是 1 还是 0，如果是 1，运行“if.true 逻辑”将压入堆栈的两个数字 3 和 5 相加，得到 8，然后将 8 压入堆栈堆。如果为 0，则运行“其他逻辑”以将数字 3 和 5 相乘，得到 15，然后将 15 压入堆栈。

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

代码段 1

Miden的词法分析器和语法分析器解析出的最终指令代码如下代码段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]

代码段 2

图 4 显示了虚拟机执行代码段 2 的过程。

中间部分是执行器执行操作码的流程图。左边的虚线指的是代码执行中生成的解码器跟踪。右侧的点划线指的是代码执行中生成的堆栈跟踪。

图中，执行器根据代码块逐块执行。在此示例中，首先执行 span 块。

然后执行步骤32的if-else-end结构，进入switch块，将上一个span块最后执行产生的海绵哈希压入ctx_stack。执行完 switch 块后，在步骤 49 将其弹出到海绵中。

图4：VM执行opcode的状态变化图

注意：本文档描述了截至 2022-05-27 的 Miden 项目主分支的最新版本。到目前为止，Miden 的下一个分支已经对指令进行了大量的重新设计，而 AIR 只实现了一些约束。

堆栈的约束条件

本节将展示主要用户操作指令的约束条件，其中，old_stack_x 是指指令执行前存储在栈 x 位置的值，new_stack_x 是指存储在栈 x 位置的值。指令执行后入栈，“->”指的是从栈的左边到右边的值的拷贝，“==”指的是方程约束。栈的约束比较简单，不需要解释。

条件说明

选择

约束：

 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

如果条件为 1，则 x 在栈顶。如果条件为 0，则 y 位于栈顶。

算术教学

添加

约束：

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

穆尔

约束：

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

投资

约束：

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

否定

约束：

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

布尔指令

不是

约束：

 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

和

约束：

 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

或者

约束：

 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

哈希指令

恢复

限制函数哈希满足哈希函数协议
占用6个寄存器。

约束：

 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

比较指令

情商

约束：

 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

根据要比较的两个数的位长周期进行比较，如：

答：[0,1,0,1]
B：[0,0,1,1]

比较指令需要执行四次。

约束：

 // 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

堆栈操作说明

dup.n

约束：

 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

交换

约束：

 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

约束：

 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

解码器注释的约束条件

在本节中，我们将展示主要 Flow 操作指令的约束条件。

用户代码执行

操作位

对于 cf_op_bits、ld_op_bits 和 hd_op_bits 的约束
约束 1：每个位只能是 0 或 1。
约束2：当op_counter不为0时，ld_ops和hd_ops不能同时为0。
约束3：当cf_op_bits为hacc时，op_counter状态会加1。
约束4：BEGIN、LOOP、BREAK、WRAP指令需要按照16对齐。
约束5：TEND和FEND指令需要按照16对齐。
约束6：PUSH指令需要按照8对齐。

约束：

 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作为flowOps，在执行该指令时总会引起spond的状态变化，因此需要执行约束。

约束：

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

条件判断

趋向

作为if真分支端的约束，分为两部分：
约束1：是海绵状态的约束。

栈顶的值等于 new_sponge_0。 if的真分支最后一次执行后的sponge等于new_sponge_1。 New_sponge_3 等于 0。

约束2：是ctx_stack的约束。栈顶的值等于 new_sponge_0。堆栈中的任何其他元素都将移动一个位置到堆栈顶部。

约束3：是loop_stack的约束。 loop_stack 的状态是不变的。

约束：

 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

作为if的假分支端的约束，分为两部分：
约束1：是海绵状态的约束。栈顶的值等于 new_sponge_0。

if的真分支最后一次执行后的sponge等于new_sponge_2。 new_sponge_3 等于 0。

约束2：是ctx_stack的约束。栈顶的值等于 new_sponge_0。堆栈中的任何其他元素都将移动一个位置到堆栈顶部。

约束3：是loop_stack的约束。 loop_stack 的状态不变。

约束：

 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