zkevm-docs/8-arithmetic.markdown

+# 布局
+
+arithmetic 子电路的设计包含如下几列。我们重点关注 operand*与 u16*列，
+
+```rust
+pub struct ArithmeticCircuitConfig<F> {
+    // TODO use table to let core lookup
+    q_enable: Selector,
+    // arithmetic table for lookup starts
+    tag: BinaryNumberConfig<Tag, 3>, //todo not use 3
+    cnt: Column<Advice>,
+    operand0_hi: Column<Advice>,
+    operand0_lo: Column<Advice>,
+    operand1_hi: Column<Advice>,
+    operand1_lo: Column<Advice>,
+    operand2_hi: Column<Advice>,
+    operand2_lo: Column<Advice>,
+    operand3_hi: Column<Advice>,
+    operand3_lo: Column<Advice>,
+    // arithmetic table for lookup ends
+    u16_0: Column<Advice>,
+    u16_1: Column<Advice>,
+    u16_2: Column<Advice>,
+    u16_3: Column<Advice>,
+    u16_4: Column<Advice>,
+    u16_5: Column<Advice>,
+    u16_6: Column<Advice>,
+    u16_7: Column<Advice>,
+    cnt_is_zero: IsZeroWithRotationConfig<F>,
+}
+
+pub enum Tag {
+    #[default]
+    Nil,
+    Add,
+    Addmod,
+    Mul,
+    Mulmod,
+    Lt,
+    Gt,
+    Slt,
+    Sgt,
+    Sub,
+    DivMod,
+}
+```
+
+在这里 tag 我们使用了一个电路小工具“BinaryNumberConfig/BinaryNumberChip”。关于 BinaryNumberChip，详见[here](../code-notes/binary_number_with_real_selector.rs的内容和用法.markdown)。
+
+## 列的含义
+
+operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b,c,overflow。u16*用来 lookup 算术中的输出如 c_hi,c_lo 属于 u128 范围。这里我们只需要保证输出值的 lookup 就好。cnt 记录某个具体算术指令的行计数器，从正数开始递减到 0。
+
+# 约束
+
+在 arithmetic 子电路中约束可以分为两类。
+通用约束
+
+- 约束 cnt 除零行外,当前行与下一行差值为 1
+
+不同 Tag 对应的约束不同
+
+- Add（在表中使用两行）
+
+  - 如果是 0 行，则 cnt_prev=1,cnt_prev_prev=0
+  - c_lo = u16 sum(rotation cur)
+  - c_hi = u16 sum(rotation prev)
+  - carry hi is bool
+  - carry lo is bool
+  - c lo + carry lo \* 2^128 = a lo + b lo
+  - c hi + carry hi \* 2^128 = a hi + b hi + carry lo
+
+- Sub_Lt_Gt (a+b=c+overflow\*2^256) (可以使用 select struct)
+  - 如果是 0 行，则 cnt_prev=1,cnt_prev_prev=0
+  - carry hi is bool
+  - carry lo is bool
+  - c lo + carry lo \* 2^128 = a lo + b lo
+  - c hi + carry hi \* 2^128 = a hi + b hi + carry lo
+  - if tag is sub 有 c_lo = u16 sum(rotation cur),c_hi = u16 sum(rotation prev) and carry_hi iszero
+  - if tag is lt 则有 carry_hi iszero
+  - if tag is gt 则有 carry_hi 1
+- Div_Mod
+- Mul
+- Slt_Sgt
+- Sdiv_Smod
+- Addmod
+- Mulmod
+
+# 实现 arithmetic 子电路中 Add 例子
+
+如果我们希望为某一个 tag 实现它的约束，我们需要实现 OperationGadget，然后在 config 方法中实现 tag 对应的约束就好。
+
+```rust
+pub(crate) trait OperationGadget<F: Field> {
+    const NAME: &'static str;
+    const TAG: Tag;
+    const NUM_ROW: usize;
+
+    fn constraints(
+        config: &OperationConfig<F>,
+        meta: &mut VirtualCells<F>,
+    ) -> Vec<(&'static str, Expression<F>)>;
+}
+
+impl<F: Field> OperationGadget<F> for AddGadget<F> {
+    const NAME: &'static str = "Arithmetic Circuit Add";
+    const TAG: Tag = Tag::Add;
+    const NUM_ROW: usize = 2;
+
+    fn constraints(
+        config: &OperationConfig<F>,
+        meta: &mut VirtualCells<F>,
+    ) -> Vec<(&'static str, Expression<F>)> {
+        let mut constraints = vec![];
+        let a_hi = meta.query_advice(config.operand0_hi, Rotation::cur());
+        ...
+        let carry_lo = meta.query_advice(config.operand3_lo, Rotation::cur());
+        let u16_0_for_c_lo = meta.query_advice(config.u16_0, Rotation::cur());
+        ...
+        let u16_7_for_c_lo = meta.query_advice(config.u16_7, Rotation::cur());
+        let u16_sum_for_c_lo = expr_from_u16s(&[
+            u16_0_for_c_lo,
+            ...
+            u16_7_for_c_lo,
+        ]);
+        let u16_0_for_c_hi = meta.query_advice(config.u16_0, Rotation::prev());
+        ...
+        let u16_7_for_c_hi = meta.query_advice(config.u16_7, Rotation::prev());
+        let u16_sum_for_c_hi = expr_from_u16s(&[
+            u16_0_for_c_hi,
+            ...
+            u16_7_for_c_hi,
+        ]);
+        constraints.push(("c lo = u16 sum", c_lo.clone() - u16_sum_for_c_lo));
+        constraints.push(("c hi = u16 sum", c_hi.clone() - u16_sum_for_c_hi));
+        constraints.push((
+            "carry hi is bool",
+            carry_hi.clone() * (1.expr() - carry_hi.clone()),
+        ));
+        constraints.push((
+            "carry lo is bool",
+            carry_lo.clone() * (1.expr() - carry_lo.clone()),
+        ));
+        constraints.push((
+            "c lo + carry lo * 2^128 = a lo + b lo",
+            c_lo + carry_lo.clone() * pow_of_two::<F>(128) - a_lo - b_lo,
+        ));
+        constraints.push((
+            "c hi + carry hi * 2^128 = a hi + b hi + carry lo",
+            c_hi + carry_hi * pow_of_two::<F>(128) - a_hi - b_hi - carry_lo,
+        ));
+        constraints
+    }
+}
+```