| ... | @@ -2,12 +2,12 @@ |
... | @@ -2,12 +2,12 @@ |
|
|
|
|
|
|
|
Fixed circuit是在电路初始化阶段预先向fixed_table填入一些cell数据，在后续电路运行过程中进行lookup查表操作；
|
|
Fixed circuit是在电路初始化阶段预先向fixed_table填入一些cell数据，在后续电路运行过程中进行lookup查表操作；
|
|
|
|
|
|
|
|
当前fixed_table填入了几种类型的数据：1. evm opcode的信息，2. 8bit范围内数据的与、或、异或操作结果，3. 10bit、16bit可表示的全量的数据，用于数据的范围证明。
|
|
当前fixed_table填入了几种类型的数据：1. evm opcode的信息，2. 8bit范围内数据的与、或、异或操作结果，3. 10bit、16bit可表示的全量的数据，用于数据的范围证明。注意，10bit数据我们的数据是1-1024，不是0-1023。16bit数据是0-65535。
|
|
|
|
|
|
|
|
|
|
|
|
|
## Witness、Column设计
|
|
## Witness、Column设计
|
|
|
|
|
|
|
|
在Witness中为不同场景预先生成一行行（Row）数据，将它们填入Fixed Table中作为lookup查询的去向，优化在电路运算过程常见的计算场景（如：8bit范围的与、或、异或运算）；且在零知识证明中，实现范围比较功能有点困难，因为无法直接进行大小比较。为了在零知识证明中实现范围比较，通常需要使用额外的技巧和方法，如进行查表，预先将一段范围的数据填入表中，范围比较时将数据查表如果不存在，则表示数据不在指定范围。
|
|
在Witness中为不同场景预先生成一行行（Row）数据，将它们填入Fixed Table中作为lookup查询的去向，优化在电路运算过程常见的计算场景（如：8bit范围的与、或、异或运算）；且在零知识证明中，实现范围比较功能有点困难，因为无法直接进行大小比较。为了在零知识证明中实现范围比较，通常需要使用额外的技巧和方法，如进行查表，预先将一段范围的数据填入表中，范围比较时将数据查表，如果在表中，则表示数据在指定范围。
|
|
|
|
|
|
|
|
```Rust
|
|
```Rust
|
|
|
pub struct Row {
|
|
pub struct Row {
|
| ... | @@ -37,15 +37,15 @@ pub enum Tag { |
... | @@ -37,15 +37,15 @@ pub enum Tag { |
|
|
**value_0**字段
|
|
**value_0**字段
|
|
|
1. And, Or, Xor操作中需要两个操作数，标识左边的操作数
|
|
1. And, Or, Xor操作中需要两个操作数，标识左边的操作数
|
|
|
2. Bytecode类型中标识 evm opcode
|
|
2. Bytecode类型中标识 evm opcode
|
|
|
3. 16bit范围的数据查找表，标识一个[0..1<<16]范围的数据<br/>
|
|
3. 16bit范围的数据查找表，标识一个[0..1<<16-1]范围的数据<br/>
|
|
|
**value_1**字段
|
|
**value_1**字段
|
|
|
1. And, Or, Xor操作中需要两个操作数，标识右边的操作数
|
|
1. And, Or, Xor操作中需要两个操作数，标识右边的操作数
|
|
|
2. Bytecode类型中对于Push类型的操作码，标识push到栈上的字节数，其它类型的操作码数值为0
|
|
2. Bytecode类型中对于Push类型的操作码，标识push到栈上的字节数，其它类型的操作码数值为0
|
|
|
3. 10bit范围的数据查找表，该字段赋值为固定的`U10_TAG` <br/>
|
|
3. 10bit范围的数据查找表，该字段赋值为固定的`U10_TAG` <br/>
|
|
|
**value_2**字段
|
|
**value_2**字段
|
|
|
1. And, Or, Xor操作的计算结果
|
|
1. And, Or, Xor操作的计算结果
|
|
|
2. Bytecode类型中如果Push到栈上的数据大于15则改值为1，其它情况为0
|
|
2. Bytecode类型中如果Push到栈上的数据大于15则改值为1，其它情况为0。即为Push的is_high。
|
|
|
3. 10bit范围的数据查找表，标识一个[0..1<<10]范围的数据
|
|
3. 10bit范围的数据查找表，标识一个[1..1<<10]范围的数据
|
|
|
|
|
|
|
|
###### Fixed电路为不同的场景生成多行Row数据，将它填入Fixed_table表后示例如下：
|
|
###### Fixed电路为不同的场景生成多行Row数据，将它填入Fixed_table表后示例如下：
|
|
|
|
|
|
| ... | @@ -66,21 +66,17 @@ pub enum Tag { |
... | @@ -66,21 +66,17 @@ pub enum Tag { |
|
|
| Bytecode | PUSH1 | 1 | 0|
|
|
| Bytecode | PUSH1 | 1 | 0|
|
|
|
| Bytecode | PUSH30 | 30 | 1|
|
|
| Bytecode | PUSH30 | 30 | 1|
|
|
|
| Bytecode | ...| ...| ...|
|
|
| Bytecode | ...| ...| ...|
|
|
|
| | | U10_TAG | 0|
|
|
| | 256 (不必从0开始) | U10_TAG | 1|
|
|
|
| | | U10_TAG| ... |
|
|
| | ... | U10_TAG| ... |
|
|
|
| | | U10_TAG| 1023|
|
|
| | 65535 | U10_TAG| 1024|
|
|
|
| | 1| | |
|
|
|
|
|
| | ...| | |
|
|
|
|
|
| | 65535| | |
|
|
|
|
|
|
|
|
|
|
## 使用
|
|
## 使用
|
|
|
|
|
|
|
|
Fixed Circuit电路填写预定义的值到Fixed Table后，可以使用在其它电路的后续lookup查表操作中，例如：用来实现一些数值的范围证明（证明数值在u10, u16范围），或一些逻辑运算操作（And, Or, Xor）；下面给出范围约束的示例：
|
|
Fixed Circuit电路填写预定义的值到Fixed Table后，可以使用在其它电路的后续lookup查表操作中，例如：用来实现一些数值的范围证明（证明数值在u10, u16范围），或一些逻辑运算操作（And, Or, Xor）；下面给出范围约束的示例：
|
|
|
|
|
|
|
|
State Circuit记录了栈上、内存操作的动态，当约束栈上元素时需要校验元素指向栈的指针，因为EVM中栈上的元素最多可以有1024个，指向栈的索引范围必须在u16；EVM的内存状态中操作是以byte为单位的，因此约束内存元素时所指向的值在u8范围。
|
|
State Circuit记录了栈上、内存操作的动态，当约束栈上元素时需要校验元素指向栈的指针，因为EVM中栈上的元素最多可以有1024个，指向栈的索引范围必须在u10；EVM的内存状态中操作是以byte为单位的，因此约束内存元素时所指向的值在u8范围。
|
|
|
|
|
|
|
|
```Rust
|
|
```Rust
|
|
|
// 约束栈上的元素在u16范围
|
|
|
|
|
fn new( meta: &mut ConstraintSystem<F>,
|
|
fn new( meta: &mut ConstraintSystem<F>,
|
|
|
Self::ConfigArgs {
|
|
Self::ConfigArgs {
|
|
|
q_enable, state_table, fixed_table,
|
|
q_enable, state_table, fixed_table,
|
| ... | | ... | |
