|
|
|
## 简介
|
|
|
|
|
|
|
|
Fixed circuit是在电路初始化阶段预先向fixed_table填入一些cell数据,在后续电路运行过程中进行lookup查表操作;
|
|
|
|
|
|
|
|
当前fixed_table填入了几种类型的数据:1. evm opcode的信息,2. 8bit范围内数据的与、或、异或操作结果,3. 10bit、16bit可表示的全量的数据,用于数据的范围证明。
|
|
|
|
|
|
|
|
|
|
|
|
## Witness、Column设计
|
|
|
|
|
|
|
|
在Witness中为不同场景预先生成一行行(Row)数据,将它们填入Fixed Table中作为lookup查询的去向,优化在电路运算过程常见的计算场景(如:8bit范围的与、或、异或运算);且在零知识证明中,实现范围比较功能有点困难,因为无法直接进行大小比较。为了在零知识证明中实现范围比较,通常需要使用额外的技巧和方法,如进行查表,预先将一段范围的数据填入表中,范围比较时将数据查表如果不存在,则表示数据不在指定范围。
|
|
|
|
|
|
|
|
```Rust
|
|
|
|
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]
|
|
|
|
And,
|
|
|
|
Or,
|
|
|
|
Xor,
|
|
|
|
U16,
|
|
|
|
Bytecode,
|
|
|
|
}
|
|
|
|
|
|
|
|
```
|
|
|
|
|
|
|
|
#### Row的设计如下
|
|
|
|
|
|
|
|
**tag**字段的不同场景
|
|
|
|
1. 数据标识,对LogicAnd、LogicOr、LogicXor、Bytecode等类型,使用下列定义Tag::And、Or、Xor、Bytecode
|
|
|
|
2. 对于10bit、16bit的范围的数据,Tag列未使用<br/>
|
|
|
|
**value_0**字段
|
|
|
|
1. And, Or, Xor操作中需要两个操作数,标识左边的操作数
|
|
|
|
2. Bytecode类型中标识 evm opcode
|
|
|
|
3. 16bit范围的数据查找表,标识一个[0..1<<16]范围的数据<br/>
|
|
|
|
**value_1**字段
|
|
|
|
1. And, Or, Xor操作中需要两个操作数,标识右边的操作数
|
|
|
|
2. Bytecode类型中对于Push类型的操作码,标识push到栈上的字节数,其它类型的操作码数值为0
|
|
|
|
3. 10bit范围的数据查找表,该字段赋值为固定的`U10_TAG` <br/>
|
|
|
|
**value_2**字段
|
|
|
|
1. And, Or, Xor操作的计算结果
|
|
|
|
2. Bytecode类型中如果Push到栈上的数据大于15则改值为1,其它情况为0
|
|
|
|
3. 10bit范围的数据查找表,标识一个[0..1<<10]范围的数据
|
|
|
|
|
|
|
|
###### Fixed电路为不同的场景生成多行Row数据,将它填入Fixed_table表后示例如下:
|
|
|
|
|
|
|
|
| tag | value_0 | value_1 | value_2 |
|
|
|
|
----|----|----|-----|
|
|
|
|
| And | 0 | 0 | 0 |
|
|
|
|
| And | 0 | 1 | 0 |
|
|
|
|
| And | ...| ...| ...|
|
|
|
|
| And | 255 | 0 | 0 |
|
|
|
|
| And | 255 | 1 | 255 |
|
|
|
|
| Or | 0 | 0 | 0 |
|
|
|
|
| Or | 0 | 1 | 1 |
|
|
|
|
| Or | ...| ...| ...|
|
|
|
|
| Or | 255 | 0 | 255 |
|
|
|
|
| Or | 255 | 1 | 255 |
|
|
|
|
| Xor | ...| ...| ...|
|
|
|
|
| Bytecode | MLOAD | 0 | 0 |
|
|
|
|
| Bytecode | PUSH1 | 1 | 0|
|
|
|
|
| Bytecode | PUSH30 | 30 | 1|
|
|
|
|
| Bytecode | ...| ...| ...|
|
|
|
|
| | | U10_TAG | 0|
|
|
|
|
| | | U10_TAG| ... |
|
|
|
|
| | | U10_TAG| 1023|
|
|
|
|
| | 1| | |
|
|
|
|
| | ...| | |
|
|
|
|
| | 65535| | |
|
|
|
|
|
|
|
|
## 使用
|
|
|
|
|
|
|
|
Fixed Circuit电路填写预定义的值到Fixed Table后,可以使用在其它电路的后续lookup查表操作中,例如:用来实现一些数值的范围证明(证明数值在u10, u16范围),或一些逻辑运算操作(And, Or, Xor);下面给出范围约束的示例:
|
|
|
|
|
|
|
|
State Circuit记录了栈上、内存操作的动态,当约束栈上元素时需要校验元素指向栈的指针,因为EVM中栈上的元素最多可以有1024个,指向栈的索引范围必须在u16;EVM的内存状态中操作是以byte为单位的,因此约束内存元素时所指向的值在u8范围。
|
|
|
|
|
|
|
|
```Rust
|
|
|
|
// 约束栈上的元素在u16范围
|
|
|
|
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对象
|
|
|
|
2. 设置约束启用条件为栈上的对象 stack_condition
|
|
|
|
3. 使用halo2提供的lookup_any方法将栈指针在预先填写好的fixed table表上进行lookup校验,如果不在u16范围则lookup校验失败。
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
\ No newline at end of file |