【zkMIPS系列】ZKM Prover—Memory & Logic Stark

ZKM
发布于 4天前
阅读 329

MemoryStark确保内存访问操作是按时间和地址顺序进行的，并且读取的值与之前写入的值一致。LogicSNARK确保逻辑运算的正确性。

# 1. Memory Stark
 
 `MemoryStark` 证明过程主要包括 **数据收集（Trace Generation）**、**约束检查（Constraints Evaluation）** 和 **零知识证明电路生成（ZK Circuit Evaluation）** 三个部分。整个过程的核心目标是 **确保内存访问操作是按时间和地址顺序进行的，并且读取的值与之前写入的值一致。**
 具体如下：
 1. **追踪数据生成**
 - 收集 `MemoryOp`，转换为 `Trace` 行 (`into_row`)
 - 排序 (`generate_trace_row_major`)
 - 生成 `First Change Flags` 和 `RANGE_CHECK` (`generate_first_change_flags_and_rc`)
 - 处理数据格式 (`generate_trace_col_major`)
 2. **约束检查**
 - 约束 `FILTER` 只能是 `0` 或 `1`
 - 确保地址变化满足规则
 - 确保时间戳递增
 - 确保读取数据与上次写入一致
 3. **电路约束**
 - 在 `eval_ext_circuit` 进行相同的检查
 - 约束所有变量为布尔值
 - 确保 `range_check` 计算正确
 4. **查找约束**
 - 通过 `Lookup Argument` 处理 `RANGE_CHECK` 的取值范围
 
 ## 1.1 追踪数据生成（Trace Generation）
 
 内存操作 `MemoryOp` 记录所有的读写操作，包括：
 
 - 访问地址 `(context, segment, virtual address)`
 - 访问时间戳 `timestamp`
 - 访问数据 `value`
 - 访问类型 `Read/Write`
 - 是否为有效操作 `filter`
 
 ### 1.1.1 处理 `MemoryOp` 转换为追踪行
 
 ```rust
 fn into_row<F: Field>(self) -> [F; NUM_COLUMNS]
 
 ```
 
 每个 `MemoryOp` 代表一个内存访问，转换为 `NUM_COLUMNS` 长度的数组，其中：
 
 - `FILTER` 指示是否是有效行
 - `ADDR_CONTEXT`, `ADDR_SEGMENT`, `ADDR_VIRTUAL` 记录访问地址
 - `TIMESTAMP` 记录操作发生的时间
 - `IS_READ` 指示是读 (`1`) 还是写 (`0`)
 - `VALUE` 记录访问的数据
 
 ### 1.1.2 处理并排序 `MemoryOp`
 
 ```rust
 fn generate_trace_row_major(&self, mut memory_ops: Vec<MemoryOp>) -> Vec<[F; NUM_COLUMNS]>
 
 ```
 
 - 对 `MemoryOp` 按 `(context, segment, virtual address, timestamp)` 进行排序
 - 调用 `fill_gaps` 确保时间戳和地址的变化不超过 `range_check` 允许的范围
 - 调用 `generate_first_change_flags_and_rc` 生成 `First Change Flags` 和 `RANGE_CHECK` 约束
 
 ### 1.1.3 生成 `First Change Flags`
 
 ```rust
 pub fn generate_first_change_flags_and_rc<F: RichField>(trace_rows: &mut [[F; NUM_COLUMNS]])
 
 ```
 
 - `CONTEXT_FIRST_CHANGE`：当前行的 `context` 是否改变？
 - `SEGMENT_FIRST_CHANGE`：当前行的 `segment` 是否改变？
 - `VIRTUAL_FIRST_CHANGE`：当前行的 `virtual address` 是否改变？
 - `RANGE_CHECK`：确保相邻行的变化量不超过最大限制
 
 ### 1.1.4 处理数据格式
 
 ```rust
 fn generate_trace_col_major(trace_col_vecs: &mut [Vec<F>])
 
 ```
 
 - 生成 `COUNTER` 计数器，用于范围检查
 - 计算 `FREQUENCIES`，存储 `RANGE_CHECK` 值出现的次数
 
 ## 1.2 约束检查（Constraint Evaluation）
 
 在 STARK 证明中，我们需要确保：
 
 - 访问时间戳 **递增**
 - 访问地址 **按顺序变化**
 - **读取的值必须和上次写入的值匹配**
 - `FILTER` 只能是 `0` 或 `1`
 
 ### 1.2.1 约束检查
 
 ```rust
 fn eval_packed_generic<FE, P, const D2: usize>(
 
 ```
 
 **约束逻辑**
 
 ```rust
 // 确保 filter 只为 0 或 1
 let filter = local_values[FILTER];
 yield_constr.constraint(filter * (filter - P::ONES));
 
 ```
 
 ```rust
 // 确保 first_change 只能发生一次
 yield_constr.constraint(context_first_change * not_context_first_change);
 yield_constr.constraint(segment_first_change * not_segment_first_change);
 yield_constr.constraint(virtual_first_change * not_virtual_first_change);
 yield_constr.constraint(address_unchanged * not_address_unchanged);
 
 ```
 
 ```rust
 // 确保 range_check 计算正确
 let computed_range_check = context_first_change * (next_addr_context - addr_context - one)
 + segment_first_change * (next_addr_segment - addr_segment - one)
 + virtual_first_change * (next_addr_virtual - addr_virtual - one)
 + address_unchanged * (next_timestamp - timestamp);
 yield_constr.constraint_transition(range_check - computed_range_check);
 
 ```
 
 ```rust
 // 确保读出的数据和之前写入的数据一致
 for i in 0..VALUE_LIMBS {
 yield_constr.constraint_transition(
 next_is_read * address_unchanged * (next_values_limbs[i] - value_limbs[i]),
 );
 }
 
 ```
 
 ## 1.3 零知识证明电路（ZK Circuit Evaluation）
 
 在 STARK 证明中，我们不仅需要常规约束，还需要在 **电路级别** 进行相同的检查，以适用于 zk-SNARK。
 
 ### 1.3.1 约束布尔变量
 
 ```rust
 fn eval_ext_circuit(
 
 ```
 
 ```rust
 // 确保 first_change 变量是布尔值
 let context_first_change_bool =
 builder.mul_extension(context_first_change, not_context_first_change);
 yield_constr.constraint(builder, context_first_change_bool);
 
 ```
 
 ```rust
 // 确保地址变化的正确性
 let segment_first_change_check =
 builder.mul_extension(segment_first_change, addr_context_diff);
 yield_constr.constraint_transition(builder, segment_first_change_check);
 
 ```
 
 ```rust
 // 确保 range_check 正确
 let range_check_diff = builder.sub_extension(range_check, computed_range_check);
 yield_constr.constraint_transition(builder, range_check_diff);
 
 ```
 
 ## 1.4 查找约束（Lookups）
 
 为了高效处理 `RANGE_CHECK`，使用了 **查找约束 (Lookup Argument)**。
 
 ```rust
 fn lookups(&self) -> Vec<Lookup<F>> {
 vec![Lookup {
 columns: vec![Column::single(RANGE_CHECK)],
 table_column: Column::single(COUNTER),
 frequencies_column: Column::single(FREQUENCIES),
 filter_columns: vec![None],
 }]
 }
 
 ```
 
 - 确保 `RANGE_CHECK` 的值在 `COUNTER` 表中（确保变化量在合理范围）。
 
 # 2 Logic Stark
 
 LogicSNARK是针对 **基本逻辑运算** 的证明系统。整个过程包括 **迹生成、约束构造、STARK 证明生成、递归电路验证**，最终用于高效证明这些逻辑运算的正确性。
 
 STARK 证明系统的流程通常包含以下几个阶段：
 
 1. **迹（Trace）生成**
 - 计算所有的运算，并存储计算路径。
 - 生成适合 STARK 证明的多项式表示。
 2. **约束（Constraints）构造**
 - 确保逻辑运算的正确性，并定义约束条件。
 - 约束用于确保 `输入 → 运算 → 结果` 的正确性。
 3. **多项式承诺（PCS）和 FRI 证明**
 - 将迹数据转换为多项式，使用 FRI（Fast Reed-Solomon Interactive Oracle Proofs of Proximity）方法进行验证。
 4. **递归证明**（可选）
 - 通过 SNARK 递归检查，减少证明大小，提高验证效率。
 
 ## 2.1 迹（Trace）生成
 
 在 STARK 证明系统中，**迹** 是计算过程的核心。它记录了输入、计算过程及输出，最终用于生成多项式表示。
 
 ### 2.1.1 逻辑运算定义
 
 代码首先定义了支持的四种逻辑运算：
 
 ```rust
 #[derive(Copy, Clone, Debug, Eq, PartialEq)]
 pub(crate) enum Op {
 And,
 Or,
 Xor,
 Nor,
 }
 
 impl Op {
 pub(crate) fn result(&self, a: u32, b: u32) -> u32 {
 match self {
 Op::And => a & b,
 Op::Or => a | b,
 Op::Xor => a ^ b,
 Op::Nor => !(a | b),
 }
 }
 }
 
 ```
 
 - `Op` 枚举定义了 **AND、OR、XOR、NOR** 操作。
 - `result()` 方法计算两个 `u32` 数的逻辑运算结果。
 
 ### 2.1.2 计算迹
 
 `Operation` 结构体存储一条逻辑运算：
 
 ```rust
 #[derive(Debug, Clone)]
 pub(crate) struct Operation {
 operator: Op,
 input0: u32,
 input1: u32,
 pub(crate) result: u32,
 }
 
 impl Operation {
 pub(crate) fn new(operator: Op, input0: u32, input1: u32) -> Self {
 let result = operator.result(input0, input1);
 Operation { operator, input0, input1, result }
 }
 }
 
 ```
 
 - `Operation::new` 创建一个新的逻辑运算，并计算 `result`。
 - 该结构体存储 `input0`、`input1` 及其计算的 `result`，用于后续的 STARK 证明。
 
 ### 2.1.3 迹行生成
 
 迹是一个二维数组，每一行表示一个逻辑运算：
 
 ```rust
 fn generate_trace_rows(
 &self,
 operations: Vec<Operation>,
 min_rows: usize,
 ) -> Vec<[F; NUM_COLUMNS]> {
 let len = operations.len();
 let padded_len = len.max(min_rows).next_power_of_two();
 
 let mut rows = Vec::with_capacity(padded_len);
 for op in operations {
 rows.push(op.into_row());
 }
 
 // 填充到 2 的幂次方
 for _ in len..padded_len {
 rows.push([F::ZERO; NUM_COLUMNS]);
 }
 
 rows
 }
 
 ```
 
 - 迹行按 **输入、计算过程、结果** 组织，每一行都是 `NUM_COLUMNS` 个字段。
 - 迹大小填充为 **2 的幂次方**，便于使用 FFT 进行 STARK 证明。
 
 ## 2.2 约束（Constraints）构造
 
 **约束（Constraints）** 是 STARK 证明的核心，确保逻辑运算在计算过程中始终满足数学规则。
 
 ### 2.2.1 定义列索引
 
 ```rust
 pub const IS_AND: usize = 0;
 pub const IS_OR: usize = IS_AND + 1;
 pub const IS_XOR: usize = IS_OR + 1;
 pub const IS_NOR: usize = IS_XOR + 1;
 
 ```
 
 - `IS_AND`, `IS_OR`, `IS_XOR`, `IS_NOR` 代表某一行是否执行该运算。
 
 ```rust
 pub const INPUT0: Range<usize> = (IS_NOR + 1)..(IS_NOR + 1) + VAL_BITS;
 pub const INPUT1: Range<usize> = INPUT0.end..INPUT0.end + VAL_BITS;
 pub const RESULT: Range<usize> = INPUT1.end..INPUT1.end + PACKED_LEN;
 
 ```
 
 - `INPUT0` 和 `INPUT1` 存储 **输入值的位分解**。
 - `RESULT` 存储 **最终结果**。
 
 ### 2.2.2 逻辑运算的约束
 
 **在 STARK 评估过程中，每个逻辑运算都必须满足：**
 
 \text{result} = \text{sum_coeff} \cdot (\text{input0} + \text{input1}) + \text{and_coeff} \cdot (\text{input0} \& \text{input1}) + \text{not_coeff} \cdot \text{MASK}
 
 其中：
 
 - `sum_coeff`、`and_coeff` 和 `not_coeff` 由 `IS_AND`、`IS_OR` 等列的值决定。
 
 约束实现：
 
 ```rust
 fn eval_packed_generic<FE, P, const D2: usize>(
 &self,
 vars: &Self::EvaluationFrame<FE, P, D2>,
 yield_constr: &mut ConstraintConsumer<P>,
 ) {
 let lv = vars.get_local_values();
 
 let sum_coeff = lv[columns::IS_OR] + lv[columns::IS_XOR] - lv[columns::IS_NOR];
 let and_coeff = lv[columns::IS_AND] - lv[columns::IS_OR] - lv[columns::IS_XOR] * FE::TWO + lv[columns::IS_NOR];
 let not_coeff = lv[columns::IS_NOR];
 
 for (result_col, x_bits_cols, y_bits_cols) in izip!(
 columns::RESULT,
 columns::limb_bit_cols_for_input(columns::INPUT0),
 columns::limb_bit_cols_for_input(columns::INPUT1),
 ) {
 let x: P = limb_from_bits_le(x_bits_cols.clone().map(|col| lv[col]));
 let y: P = limb_from_bits_le(y_bits_cols.clone().map(|col| lv[col]));
 
 let x_op_y = sum_coeff * (x + y) + and_coeff * (x & y) + not_coeff * FE::from_canonical_u32(u32::MAX);
 yield_constr.constraint(lv[result_col] - x_op_y);
 }
 }
 
 ```
 
 - 计算 `sum_coeff`, `and_coeff`, `not_coeff`。
 - `x_op_y` 计算逻辑运算的理论结果，并约束 `lv[result_col]`。
 
 ## 2.3 多项式承诺（PCS）和 FRI 证明
 
 该部分参考本系列之前的文档。
 
 
 ## 2.4 递归证明
 
 递归电路用于 **高效验证 STARK 证明**：
 
 ```rust
 fn eval_ext_circuit(
 &self,
 builder: &mut CircuitBuilder<F, D>,
 vars: &Self::EvaluationFrameTarget,
 yield_constr: &mut RecursiveConstraintConsumer<F, D>,
 )
 
 ```
 
 - `CircuitBuilder` 负责 SNARK 递归约束。
 - 计算 `x_op_y`，确保 `result` 计算正确。

1. Memory Stark

MemoryStark 证明过程主要包括 数据收集（Trace Generation）、约束检查（Constraints Evaluation） 和 零知识证明电路生成（ZK Circuit Evaluation） 三个部分。整个过程的核心目标是 确保内存访问操作是按时间和地址顺序进行的，并且读取的值与之前写入的值一致。 具体如下：

追踪数据生成
- 收集 MemoryOp，转换为 Trace 行 (into_row)
- 排序 (generate_trace_row_major)
- 生成 First Change Flags 和 RANGE_CHECK (generate_first_change_flags_and_rc)
- 处理数据格式 (generate_trace_col_major)
约束检查
- 约束 FILTER 只能是 0 或 1
- 确保地址变化满足规则
- 确保时间戳递增
- 确保读取数据与上次写入一致
电路约束
- 在 eval_ext_circuit 进行相同的检查
- 约束所有变量为布尔值
- 确保 range_check 计算正确

查找约束

通过 Lookup Argument 处理 RANGE_CHECK 的取值范围

1.1 追踪数据生成（Trace Generation）

内存操作 MemoryOp 记录所有的读写操作，包括：

访问地址 (context, segment, virtual address)
访问时间戳 timestamp
访问数据 value
访问类型 Read/Write
是否为有效操作 filter

1.1.1 处理 `MemoryOp` 转换为追踪行

fn into_row&lt;F: Field>(self) -> [F; NUM_COLUMNS]

每个 MemoryOp 代表一个内存访问，转换为 NUM_COLUMNS 长度的数组，其中：

FILTER 指示是否是有效行
ADDR_CONTEXT, ADDR_SEGMENT, ADDR_VIRTUAL 记录访问地址
TIMESTAMP 记录操作发生的时间
IS_READ 指示是读 (1) 还是写 (0)
VALUE 记录访问的数据

1.1.2 处理并排序 `MemoryOp`

fn generate_trace_row_major(&self, mut memory_ops: Vec&lt;MemoryOp>) -> Vec&lt;[F; NUM_COLUMNS]>

对 MemoryOp 按 (context, segment, virtual address, timestamp) 进行排序
调用 fill_gaps 确保时间戳和地址的变化不超过 range_check 允许的范围
调用 generate_first_change_flags_and_rc 生成 First Change Flags 和 RANGE_CHECK 约束

1.1.3 生成 `First Change Flags`

pub fn generate_first_change_flags_and_rc&lt;F: RichField>(trace_rows: &mut [[F; NUM_COLUMNS]])

CONTEXT_FIRST_CHANGE：当前行的 context 是否改变？
SEGMENT_FIRST_CHANGE：当前行的 segment 是否改变？
VIRTUAL_FIRST_CHANGE：当前行的 virtual address 是否改变？
RANGE_CHECK：确保相邻行的变化量不超过最大限制

1.1.4 处理数据格式

fn generate_trace_col_major(trace_col_vecs: &mut [Vec&lt;F>])

生成 COUNTER 计数器，用于范围检查
计算 FREQUENCIES，存储 RANGE_CHECK 值出现的次数

1.2 约束检查（Constraint Evaluation）

在 STARK 证明中，我们需要确保：

访问时间戳递增
访问地址 按顺序变化
读取的值必须和上次写入的值匹配
FILTER 只能是 0 或 1

1.2.1 约束检查

fn eval_packed_generic&lt;FE, P, const D2: usize>(

约束逻辑

// 确保 filter 只为 0 或 1
let filter = local_values[FILTER];
yield_constr.constraint(filter * (filter - P::ONES));

// 确保 first_change 只能发生一次
yield_constr.constraint(context_first_change * not_context_first_change);
yield_constr.constraint(segment_first_change * not_segment_first_change);
yield_constr.constraint(virtual_first_change * not_virtual_first_change);
yield_constr.constraint(address_unchanged * not_address_unchanged);

// 确保 range_check 计算正确
let computed_range_check = context_first_change * (next_addr_context - addr_context - one)
+ segment_first_change * (next_addr_segment - addr_segment - one)
+ virtual_first_change * (next_addr_virtual - addr_virtual - one)
+ address_unchanged * (next_timestamp - timestamp);
yield_constr.constraint_transition(range_check - computed_range_check);

// 确保读出的数据和之前写入的数据一致
for i in 0..VALUE_LIMBS {
yield_constr.constraint_transition(
next_is_read * address_unchanged * (next_values_limbs[i] - value_limbs[i]),
);
}

1.3 零知识证明电路（ZK Circuit Evaluation）

在 STARK 证明中，我们不仅需要常规约束，还需要在 电路级别 进行相同的检查，以适用于 zk-SNARK。

1.3.1 约束布尔变量

fn eval_ext_circuit(

// 确保 first_change 变量是布尔值
let context_first_change_bool =
builder.mul_extension(context_first_change, not_context_first_change);
yield_constr.constraint(builder, context_first_change_bool);

// 确保地址变化的正确性
let segment_first_change_check =
builder.mul_extension(segment_first_change, addr_context_diff);
yield_constr.constraint_transition(builder, segment_first_change_check);

// 确保 range_check 正确
let range_check_diff = builder.sub_extension(range_check, computed_range_check);
yield_constr.constraint_transition(builder, range_check_diff);

1.4 查找约束（Lookups）

为了高效处理 RANGE_CHECK，使用了 查找约束 (Lookup Argument)。

fn lookups(&self) -> Vec&lt;Lookup&lt;F>> {
vec![Lookup {
columns: vec![Column::single(RANGE_CHECK)],
table_column: Column::single(COUNTER),
frequencies_column: Column::single(FREQUENCIES),
filter_columns: vec![None],
}]
}

确保 RANGE_CHECK 的值在 COUNTER 表中（确保变化量在合理范围）。

2 Logic Stark

LogicSNARK是针对 基本逻辑运算 的证明系统。整个过程包括 迹生成、约束构造、STARK 证明生成、递归电路验证，最终用于高效证明这些逻辑运算的正确性。

STARK 证明系统的流程通常包含以下几个阶段：

迹（Trace）生成
- 计算所有的运算，并存储计算路径。
- 生成适合 STARK 证明的多项式表示。
约束（Constraints）构造
- 确保逻辑运算的正确性，并定义约束条件。
- 约束用于确保 输入 → 运算 → 结果 的正确性。
多项式承诺（PCS）和 FRI 证明
- 将迹数据转换为多项式，使用 FRI（Fast Reed-Solomon Interactive Oracle Proofs of Proximity）方法进行验证。

递归证明（可选）

通过 SNARK 递归检查，减少证明大小，提高验证效率。

2.1 迹（Trace）生成

在 STARK 证明系统中，迹是计算过程的核心。它记录了输入、计算过程及输出，最终用于生成多项式表示。

2.1.1 逻辑运算定义

代码首先定义了支持的四种逻辑运算：

#[derive(Copy, Clone, Debug, Eq, PartialEq)]
pub(crate) enum Op {
And,
Or,
Xor,
Nor,
}

impl Op {
pub(crate) fn result(&self, a: u32, b: u32) -> u32 {
match self {
Op::And => a & b,
Op::Or => a | b,
Op::Xor => a ^ b,
Op::Nor => !(a | b),
}
}
}

Op 枚举定义了 AND、OR、XOR、NOR 操作。
result() 方法计算两个 u32 数的逻辑运算结果。

2.1.2 计算迹

Operation 结构体存储一条逻辑运算：

#[derive(Debug, Clone)]
pub(crate) struct Operation {
operator: Op,
input0: u32,
input1: u32,
pub(crate) result: u32,
}

impl Operation {
pub(crate) fn new(operator: Op, input0: u32, input1: u32) -> Self {
let result = operator.result(input0, input1);
Operation { operator, input0, input1, result }
}
}

Operation::new 创建一个新的逻辑运算，并计算 result。
该结构体存储 input0、input1 及其计算的 result，用于后续的 STARK 证明。

2.1.3 迹行生成

迹是一个二维数组，每一行表示一个逻辑运算：

fn generate_trace_rows(
&self,
operations: Vec&lt;Operation>,
min_rows: usize,
) -> Vec&lt;[F; NUM_COLUMNS]> {
let len = operations.len();
let padded_len = len.max(min_rows).next_power_of_two();

let mut rows = Vec::with_capacity(padded_len);
for op in operations {
rows.push(op.into_row());
}

// 填充到 2 的幂次方
for _ in len..padded_len {
rows.push([F::ZERO; NUM_COLUMNS]);
}

rows
}

迹行按 输入、计算过程、结果 组织，每一行都是 NUM_COLUMNS 个字段。
迹大小填充为 2 的幂次方，便于使用 FFT 进行 STARK 证明。

2.2 约束（Constraints）构造

约束（Constraints） 是 STARK 证明的核心，确保逻辑运算在计算过程中始终满足数学规则。

2.2.1 定义列索引

pub const IS_AND: usize = 0;
pub const IS_OR: usize = IS_AND + 1;
pub const IS_XOR: usize = IS_OR + 1;
pub const IS_NOR: usize = IS_XOR + 1;

IS_AND, IS_OR, IS_XOR, IS_NOR 代表某一行是否执行该运算。

pub const INPUT0: Range&lt;usize> = (IS_NOR + 1)..(IS_NOR + 1) + VAL_BITS;
pub const INPUT1: Range&lt;usize> = INPUT0.end..INPUT0.end + VAL_BITS;
pub const RESULT: Range&lt;usize> = INPUT1.end..INPUT1.end + PACKED_LEN;

INPUT0 和 INPUT1 存储 输入值的位分解。
RESULT 存储 最终结果。

2.2.2 逻辑运算的约束

在 STARK 评估过程中，每个逻辑运算都必须满足：

\text{result} = \text{sum_coeff} \cdot (\text{input0} + \text{input1}) + \text{and_coeff} \cdot (\text{input0} \& \text{input1}) + \text{not_coeff} \cdot \text{MASK}

其中：

sum_coeff、and_coeff 和 not_coeff 由 IS_AND、IS_OR 等列的值决定。

约束实现：

fn eval_packed_generic&lt;FE, P, const D2: usize>(
&self,
vars: &Self::EvaluationFrame&lt;FE, P, D2>,
yield_constr: &mut ConstraintConsumer&lt;P>,
) {
let lv = vars.get_local_values();

let sum_coeff = lv[columns::IS_OR] + lv[columns::IS_XOR] - lv[columns::IS_NOR];
let and_coeff = lv[columns::IS_AND] - lv[columns::IS_OR] - lv[columns::IS_XOR] * FE::TWO + lv[columns::IS_NOR];
let not_coeff = lv[columns::IS_NOR];

for (result_col, x_bits_cols, y_bits_cols) in izip!(
columns::RESULT,
columns::limb_bit_cols_for_input(columns::INPUT0),
columns::limb_bit_cols_for_input(columns::INPUT1),
) {
let x: P = limb_from_bits_le(x_bits_cols.clone().map(|col| lv[col]));
let y: P = limb_from_bits_le(y_bits_cols.clone().map(|col| lv[col]));

let x_op_y = sum_coeff * (x + y) + and_coeff * (x & y) + not_coeff * FE::from_canonical_u32(u32::MAX);
yield_constr.constraint(lv[result_col] - x_op_y);
}
}

计算 sum_coeff, and_coeff, not_coeff。
x_op_y 计算逻辑运算的理论结果，并约束 lv[result_col]。

2.3 多项式承诺（PCS）和 FRI 证明

该部分参考本系列之前的文档。

2.4 递归证明

递归电路用于 高效验证 STARK 证明：

fn eval_ext_circuit(
&self,
builder: &mut CircuitBuilder&lt;F, D>,
vars: &Self::EvaluationFrameTarget,
yield_constr: &mut RecursiveConstraintConsumer&lt;F, D>,
)

CircuitBuilder 负责 SNARK 递归约束。
计算 x_op_y，确保 result 计算正确。

原创
学分: 0
分类: Layer2
标签: zkVM zkMIPS

本文参与登链社区写作激励计划，好文好收益，欢迎正在阅读的你也加入。

【zkMIPS系列】ZKM Prover—Memory & Logic Stark

1. Memory Stark

1.1 追踪数据生成（Trace Generation）

1.1.1 处理 `MemoryOp` 转换为追踪行

1.1.2 处理并排序 `MemoryOp`

1.1.3 生成 `First Change Flags`

1.1.4 处理数据格式

1.2 约束检查（Constraint Evaluation）

1.2.1 约束检查

1.3 零知识证明电路（ZK Circuit Evaluation）

1.3.1 约束布尔变量

1.4 查找约束（Lookups）

2 Logic Stark

2.1 迹（Trace）生成

2.1.1 逻辑运算定义

2.1.2 计算迹

2.1.3 迹行生成

2.2 约束（Constraints）构造

2.2.1 定义列索引

2.2.2 逻辑运算的约束

2.3 多项式承诺（PCS）和 FRI 证明

2.4 递归证明

0 条评论

专栏: zkMIPS解读

文章目录

【zkMIPS系列】ZKM Prover—Memory & Logic Stark

1. Memory Stark

1.1 追踪数据生成（Trace Generation）

1.1.1 处理 MemoryOp 转换为追踪行

1.1.2 处理并排序 MemoryOp

1.1.3 生成 First Change Flags

1.1.4 处理数据格式

1.2 约束检查（Constraint Evaluation）

1.2.1 约束检查

1.3 零知识证明电路（ZK Circuit Evaluation）

1.3.1 约束布尔变量

1.4 查找约束（Lookups）

2 Logic Stark

2.1 迹（Trace）生成

2.1.1 逻辑运算定义

2.1.2 计算迹

2.1.3 迹行生成

2.2 约束（Constraints）构造

2.2.1 定义列索引

2.2.2 逻辑运算的约束

2.3 多项式承诺（PCS）和 FRI 证明

2.4 递归证明

0 条评论

专栏: zkMIPS解读

文章目录

1.1.1 处理 `MemoryOp` 转换为追踪行

1.1.2 处理并排序 `MemoryOp`

1.1.3 生成 `First Change Flags`