Miden的stark证明系统

Miden证明系统概述：Miden是基于STARK技术的zkVM实现方案，底层依赖Winterfell库生成和验证STARK证明，核心功能包括词法语法编译器、指令执行器和符合STARK要求的AIR（代数中间表示）。
核心组件
- 词法语法编译器：将Miden汇编指令编译为包含操作码和操作值的代码块（codeblock）。
- 指令执行器：执行代码块生成执行轨迹（execution trace），供证明生成使用。
- AIR约束：分为堆栈（stack）和解码器（decoder）两部分，分别约束虚拟机执行过程中的堆栈操作和指令流逻辑。
AIR设计细节
- Stack约束：初始化堆栈深度为8，可动态扩展至最大16，超出则报错。
- Decoder约束：通过固定列（如op_counter、op_sponge）和位字段（cf_op_bits等）确保指令顺序与正确性，并作为堆栈状态选择器。
执行实例演示
- 示例代码通过条件分支（if-else）实现加法或乘法操作，展示从汇编解析到生成执行轨迹的全流程，包括span block和switch block的执行逻辑及上下文切换。
指令约束条件
- 算术/逻辑指令：如add、mul、not等，约束执行前后堆栈值的关系。
- 控制流指令：如hacc（哈希累加）、t_end/f_end（条件分支结束），约束sponge状态和上下文栈的同步。
- 堆栈操作：如dup.n、swap，限制值复制或交换的规则。
备注：当前文档基于Miden的main分支，next分支正进行指令重构，AIR约束尚未完全实现。
团队信息：开发方Sin7Y为区块链技术研究团队，专注EVM、Layer2、隐私计算等领域。

miden 证明系统架构

miden是一个基于strark技术的zkvm实现方案。它的底层是基于winterfell这个zkp库来生成stark证明和对证明进行验证。下图1中虚线部分是Miden实现的主要功能。可以看出，主要有三个组件构成。

1. 一套词法语法编译器,下图1中的lexical analyzer和syntax parser。它们可以将miden定义的汇编指令编程成codeblock和block中包含的opcode和op value。

2. 一套指令的执行器，下图1中的executor。它负责按照定义的规则执行codeblock和block中包含的opcode及op value。执行结果为用于生成证明的execution trace。

3. 一套符合stark证明要求的AIR(代数中间表示)，下图1中的AIR。用来对miden的虚拟机执行过程进行约束。

AIR结构设计图

AIR的约束分为stack和decoder两部分：

图2为stack的约束，初始化时分配了最上边深度为8的stack。在执行时根据程序需要，可能会超出初始化分配的深度，那么max_depth会根据需要递增。但是不能超过最大深度16。否则报错。

图3为decoder的约束。其中的op_counter,op_sponge,cf_op_bits, ld_op_bits,hd_op_bits是固定列长度的。其中的op_sponge用于执行指令的顺序和正确性的约束。cf_op_bits约束3bit的flow_ops。ld_op_bits,hd_op_bits分别约束了user_ops的低5bits和高2bits。ld_op_bits和hd_op_bits组合构成一条执行的user_op,还用来作为stack每step状态约束的selector。

Miden VM执行过程实例

本节将展示一个简单的miden逻辑来说明vm的执行过程和stark的execution trace的生成。

下边代码段1是要执行的代码段：

它执行的逻辑是将3和5压栈。之后从tape读取flag。判断flag是1还是0。如果是1则运行if.true分支将压栈的两个数3和5取出，相加得到8并重新压入栈。如果是0则运行else分支将压栈的两个数3和5取出相乘得到15，再将15重新压入栈。

代码段通过miden的词法和语法分析器解析后的最终指令代码如下代码段2:

下边图4是vm运行代码段2的过程，中间是executor执行opcode的流程图，左边虚线指向的是代码执行产生的decoder trace，右边点划线指向的是代码执行产生的stack trace。

其中executor是按照code block来一块一块执行。在本例子里，首先执行了一个span block。之后在第32步时执行if-else-end结构进入了swtich block块，并将之前的span block的最后一步执行生成的sponge hash压入ctx_stack，并在swtich block块执行完之后，在第49步弹出到sponge里。

Note：本文档描述针对miden工程的main分支最新版本。目前miden的next分支对于指令进行了大量重新设计，AIR也只实现了很少一部分的约束。

stack约束条件

本节将展示主要的User操作指令的约束条件。其中的old_stack_x指的是指令执行前的stack的x位置存储的value。new_stack_x指的是指令执行后的stack的x位置存储的value。-->是将栈左边位置的value拷贝到右边位置。==是等式约束。stack的约束相对比较简单，就不多做解释了。