GitLab

简介

Fixed circuit是在电路初始化阶段预先向fixed_table填入一些cell数据，在后续电路运行过程中进行lookup查表操作；

当前fixed_table填入了几种类型的数据：1. evm opcode的信息，2. 8bit范围内数据的与、或操作结果，3. 10bit、16bit可表示的全量的数据，用于数据的范围证明。注意，10bit数据我们的数据是1-1024，不是0-1023。16bit数据是0-65535。

Witness、Column设计

在Witness中为不同场景预先生成一行行（Row）数据，将它们填入Fixed Table中作为lookup查询的去向，优化在电路运算过程常见的计算场景（如：8bit范围的与、或运算）；且在零知识证明中，实现范围比较功能有点困难，因为无法直接进行大小比较。为了在零知识证明中实现范围比较，通常需要使用额外的技巧和方法，如进行查表，预先将一段范围的数据填入表中，范围比较时将数据查表，如果在表中，则表示数据在指定范围。

在 Fixed Circuit 中，Row 结构用于定义在 fixed_table 中填入的每一行数据，包含以下字段：

pub struct Row {    
    pub tag: Tag,    
    pub value_0: Option<U256>,    
    pub value_1: Option<U256>,
    pub value_2: Option<U256>,
}

#[derive(Clone, Copy, Debug, Default, Serialize)]
pub enum Tag {
    #[default]
    U16,
    And,
    Or,
    Bytecode,
}

Row的设计如下

1. 数据标识：

• 对于逻辑运算（LogicAnd、LogicOr ）、Bytecode 等类型，使用下列定义：

  • Tag::And
  • Tag::Or
  • Tag::Bytecode

• 对于 10bit 和 16bit 范围的数据，Tag 列未使用，填入 Tag::U16 作为默认值。

2. value_0字段：

• 在 And 和 Or 操作中，value_0 标识左边的操作数。
• 在 Bytecode 类型中，value_0 标识 EVM 操作码。
• 在 16bit 范围的数据查找表中，value_0 标识一个 [0..1<<16-1] 范围的数据。

3. value_1字段：

• 在 And 和 Or 操作中，value_1 标识右边的操作数。
• 在 Bytecode 类型中，对于 Push 类型的操作码，value_1 标识 push 到栈上的字节数，其他类型的操作码数值为 0。
• 在 10bit 范围的数据查找表中，value_1 赋值为固定的 U10_TAG。

4. value_2字段：

• 在 And 和 Or 操作的计算结果。
• 在 Bytecode 类型中，如果 Push 到栈上的数据大于 15，则该值为 1，其他情况为 0，即为 Push 的 is_high。
• 在 10bit 范围的数据查找表中，value_2 标识一个 [1..1<<10] 范围的数据。

Fixed电路为不同的场景生成多行Row数据，将它填入Fixed_table表后示例如下：

使用

在 Fixed Circuit 中预先定义的值被填入 Fixed Table 后，可以在其他电路的后续查表操作中使用。例如，用来实现一些数值的范围证明（如证明数值在 u10, u16 范围内），或一些逻辑运算操作（如 And, Or）。以下是一个范围约束的示例：

State Circuit 记录了栈上和内存操作的动态，当约束栈上元素时需要校验元素指向栈的指针。因为 EVM 中栈上的元素最多可以有 1024 个，指向栈的索引范围必须在 u10；EVM 的内存状态中操作是以 byte 为单位的，因此约束内存元素时所指向的值在 u8 范围。

fn new( meta: &mut ConstraintSystem<F>,
        Self::ConfigArgs {
            q_enable, state_table, fixed_table,
        }: Self::ConfigArgs,
    )  -> Self{

	.....
  	meta.lookup_any("STATE_lookup_stack_pointer", |meta| {
        let mut constraints = vec![];
        // 1<= pointer_lo <=1024 in stack
        let entry = LookupEntry::U10(meta.query_advice(config.pointer_lo, Rotation::cur()));
        let stack_condition = config.tag.value_equals(state::Tag::Stack, Rotation::cur())(meta);
        if let LookupEntry::Conditional(expr, entry) = entry.conditional(stack_condition) {
            let lookup_vec = config.fixed_table.get_lookup_vector(meta, *entry);
            constraints = lookup_vec
                .into_iter()
                .map(|(left, right)| {
                    let q_enable = meta.query_selector(config.q_enable);
                    (q_enable * left * expr.clone(), right)
                })
                .collect();
        }
        constraints
     });
        
     ....
       
}        

1. 构造基于栈指针 config.pointer_lo 的 LookupEntry 对象：
   • 创建一个基于栈指针的 LookupEntry 对象来表示查找表中的项。
2. 设置约束启用条件为栈上的对象 stack_condition：
   • 使用 config.tag.value_equals 方法设置约束启用条件，确保只有在特定条件下（如栈上的对象）才会进行查表操作。
3. 使用 Halo2 提供的 lookup_any 方法将栈指针在预先填写好的 Fixed Table 表上进行查表校验：
   • 使用 lookup_any 方法在 fixed_table 中查找栈指针，如果查找失败则表示栈指针超出范围，查表校验失败。