# Ceno EVM Add Breakdown

## Overview

The add opcode constraints can be divided into three parts: **main constraints**, **selection constraint**, and **product constraint**.

### Main constraints

These constraints include computing uint addition and generating records. We use the notation `Uint<M, C>` to denote the total bit width is `M`, the bit width for each cell is `C`.
- The program counter is denoted by `Uint<64, 32>`.
- The stack value is denoted by `Uint<256, 16>`.
- The timestamp is denoted by `Uint<48, 48>`

#### Witnesses

// state updates
- pc: 2 cells
- ts: 1 cell
- top: 1 cell
- pc carry: 1 cell

// stack operations
- addend_0: 16 cells
- addend_1: 16 cells
- stack_ts_lt0: 3 cells
- stack_ts_lt1: 3 cells

// uint add
- carry: 16 cells

#### State updates

From `(pc, ts, top)` to `(pc + 1, ts + 1, top - 1)`

$$
\begin{align}
record_{lk0} &= \mathsf{RANGE} + r_0 \cdot 2^{15} \cdot carry_{pc} + r_1 \\
record_{r0} &= \mathsf{STATE} + r_0 \cdot pc[0] + r_0^2 \cdot pc[1] + r_0^3 \cdot ts + r_0^4 \cdot top + r_1 \\
record_{w0} &= \mathsf{STATE} + r_0 \cdot (pc[0] + 1 - 2^{32} \cdot carry_{pc}) + r_0^2 \cdot (pc[1] + carry_{pc}) \\
&+ r_0^3 \cdot (ts + 1) + r_0^4 \cdot (top - 1) + r_1
\end{align}
$$

#### Bytecode check

Check `(pc, ADD)` in the program.

$$
\begin{align}
record_{lk1} &= \mathsf{BYTECODE} + r_0 \cdot pc[0] + r_0^2 \cdot pc[1] + r_0^3 \cdot \mathsf{ADD} + r_1
\end{align}
$$

#### Stack operations
Check `0 <= top - 2 < 1024`.

Suppose the previous timestamp is `old_stack_ts0` and `old_stack_ts1`, then `stack_ts_lt0 = ts - old_stack_ts0`, `stack_ts_lt1 = ts - old_stack_ts1`. Check `stack_ts_lt0` and `stack_ts_lt1` are within $[0..2^{48})$.

Read `(top - 1, addend_0, ts - stack_ts_lt0)` and `(top - 2, addend_1, ts - stack_ts_lt1)` from the stack and push `(top - 2, addend_0 + addend_1, ts)` into the stack.

$$
\begin{align}
record_{lk2} &= \mathsf{RANGE} + r_0 \cdot 2^{6} \cdot (top - 2) + r_1 \\
record_{lk3} &= \mathsf{RANGE} + r_0 \cdot stack\_ts\_lt0[0] + r_1 \\
record_{lk4} &= \mathsf{RANGE} + r_0 \cdot stack\_ts\_lt0[1] + r_1 \\
record_{lk5} &= \mathsf{RANGE} + r_0 \cdot stack\_ts\_lt0[2] + r_1 \\
record_{lk6} &= \mathsf{RANGE} + r_0 \cdot stack\_ts\_lt1[0] + r_1 \\
record_{lk7} &= \mathsf{RANGE} + r_0 \cdot stack\_ts\_lt1[1] + r_1 \\
record_{lk8} &= \mathsf{RANGE} + r_0 \cdot stack\_ts\_lt1[2] + r_1 \\
record_{r1} &= \mathsf{STACK} + r_0 \cdot (top - 1) + r_0^2 \cdot addend_0[0] + \cdot + r_0^{17} \cdot addend_0[15] + r_0^{18} \cdot (ts - 2^{32} \cdot stack\_ts\_lt0[2] - 2^{16} \cdot stack\_ts\_lt0[1] - stack\_ts\_lt0[0]) + r_1 \\
record_{r2} &= \mathsf{STACK} + r_0 \cdot (top - 2) + r_0^2 \cdot addend_1[0] + \cdot + r_0^{17} \cdot addend_1[15] + r_0^{18} \cdot (ts - 2^{32} \cdot stack\_ts\_lt1[2] - 2^{16} \cdot stack\_ts\_lt1[1] - stack\_ts\_lt1[0]) + r_1 \\
record_{w1} &= \mathsf{STACK} + r_0 \cdot (top - 2) + r_0^2 \cdot (addend_0[0] + addend_1[0] - 2^{16} \cdot carry[0]) + \cdot + r_0^{17} \cdot (addend_0[15] + addend_1[15] - 2^{16} \cdot carry[15] + carry[14]) + r_0^{18} \cdot ts + r_1
\end{align}
$$

#### Uint
Check `(addend_0 + addend_1)[0..16]` are in $[0..2^{16})$.
Check `carry[0..16]` are bits.

$$
\begin{align}
record_{lk9} &= \mathsf{RANGE} + r_0 \cdot (addend_0[0] + addend_1[0] - 2^{16} \cdot carry[0]) + r_1 \\
\vdots & \\
record_{lk24} &= \mathsf{RANGE} + r_0 \cdot (addend_0[15] + addend_1[15] - 2^{16} \cdot carry[15] + carry[14]) + r_1 \\
record_{lk25} &= \mathsf{RANGE} + r_0 \cdot 2^{15} \cdot carry[0] + r_1 \\
\vdots & \\
record_{lk40} &= \mathsf{RANGE} + r_0 \cdot 2^{15} \cdot carry[15] + r_1
\end{align}
$$

### Proving protocol (Suppose `inst_num_vars = 20`)

#### Layer 0..21: Split and read / write / lookup

$$
\begin{align}
out_{lk\_d}(rt) &+ \\
\alpha_i out_{lk\_n}(rt) &+ \\
\alpha_i^2 out_r(rt) &+ \\
\alpha_i^3 out_w(rt)
&= \sum_{b_s}eq(rt, b_s) \Big(in^{(0)}_{lk\_d}(b_s) \cdot in^{(1)}_{lk\_d}(b_s) \\
&+ \alpha_i \left(in^{(0)}_{lk\_d}(b_s) * in^{(1)}_{lk\_n}(b_s) + in^{(0)}_{lk\_n}(b_s) \cdot in^{(1)}_{lk\_d}(b_s)\right) \\
&+ \alpha_i^2 in^{(0)}_r(b_s) \cdot in^{(1)}_r(b_s) \\
&+ \alpha_i^3 in^{(0)}_w(b_s) \cdot in^{(1)}_w(b_s) \Big)
\end{align}
$$
Receive a randomness $r$ from the verifier. Let $rt' = [r] \| rs$, then
$$
\begin{align}
out'_{lk\_d}(rt') &= in^{(0)}_{lk\_d}(rs) + r \cdot (in^{(1)}_{lk\_d}(rs) - in^{(0)}_{lk\_d}(rs)) \\
out'_{lk\_n}(rt') &= in^{(0)}_{lk\_n}(rs) + r \cdot (in^{(1)}_{lk\_n}(rs) - in^{(0)}_{lk\_n}(rs)) \\
out'_r(rt') &= in^{(0)}_{r}(rs) + r \cdot (in^{(1)}_{r}(rs) - in^{(0)}_{r}(rs)) \\
out'_w(rt') &= in^{(0)}_{w}(rs) + r \cdot (in^{(1)}_{w}(rs) - in^{(0)}_{w}(rs))
\end{align}
$$

Let $rt_w$ be the last `rt'`.

#### Layer 21..22: Split and read / lookup

$$
\begin{align}
out_{lk\_d}(rt) &+ \\
\alpha_i out_{lk\_n}(rt) &+ \\
\alpha_i^2 out_r(rt)
&= \sum_{b_s}eq(rt, b_s) \Big(in^{(0)}_{lk\_d}(b_s) \cdot in^{(1)}_{lk\_d}(b_s) \\
&+ \alpha_i in^{(0)}_{lk\_d}(b_s) * in^{(1)}_{lk\_n}(b_s) + in^{(0)}_{lk\_n}(b_s) \cdot in^{(1)}_{lk\_d}(b_s) \\
&+ \alpha_i^2 in^{(0)}_r(b_s) \cdot in^{(1)}_r(b_s) \Big)
\end{align}
$$
Receive a randomness $r_i$ from the verifier. Let $rt' = [r] || rs$, then
$$
\begin{align}
out'_{lk\_d}(rt') &= in^{(0)}_{lk\_d}(rs) + r \cdot (in^{(1)}_{lk\_d}(rs) - in^{(0)}_{lk\_d}(rs)) \\
out'_{lk\_n}(rt') &= in^{(0)}_{lk\_n}(rs) + r \cdot (in^{(1)}_{lk\_n}(rs) - in^{(0)}_{lk\_n}(rs)) \\
out'_r(rt') &= in^{(0)}_{r}(rs) + r \cdot (in^{(1)}_{r}(rs) - in^{(0)}_{r}(rs))
\end{align}
$$

Let $rt_r$ be the last `rt'`.

#### Layer 22..26: Split and lookup

$$
\begin{align}
out_{lk\_d}(rt) + \alpha_i out_{lk\_n}(rt) &= \sum_{b_s}eq(rt, b_s) \Big(in^{(0)}_{lk\_d}(b_s) \cdot in^{(1)}_{lk\_d}(b_s) \\
&+ \alpha_i in^{(0)}_{lk\_d}(b_s) * in^{(1)}_{lk\_n}(b_s) + in^{(0)}_{lk\_n}(b_s) \cdot in^{(1)}_{lk\_d}(b_s) \Big)
\end{align}
$$
Receive a randomness $r_i$ from the verifier. Let $rt' = [r] || rs$, then
$$
\begin{align}
out'_{lk\_d}(rt') &= in^{(0)}_{lk\_d}(rs) + r \cdot (in^{(1)}_{lk\_d}(rs) - in^{(0)}_{lk\_d}(rs)) \\
out'_{lk\_n}(rt') &= in^{(0)}_{lk\_n}(rs) + r \cdot (in^{(1)}_{lk\_n}(rs) - in^{(0)}_{lk\_n}(rs))
\end{align}
$$

Let $rt_{lk}$ be the last `rt'`.

#### Layer 26: Select layer

$$
\begin{align}
&out'_{lk\_d}(rt_{lk}) + \alpha_{26} \cdot out'_{lk\_n}(rt_{lk}) + \alpha_{26}^2 \cdot out'_r(rt_r) + \alpha_{26}^3 \cdot out'_w(rt_w) \\
&= \sum_{b_s} sel(rt_{lk}[6..], b_s) \Big(\sum_{i = 0}^{40} eq(rt_{lk}[..6], i) \cdot \big(record_{lki}(b_s) + \alpha_{26} \cdot 1 \big) + \sum_{i = 41}^{63} eq(rt_{lk}[..6], i) \cdot \big(1 + \alpha_{26} \cdot 0 \big) \Big) \\
&+ \sum_{b_s} \Big(eq(rt_{lk}[6..], b_s) - sel(rt_{lk}[6..], b_s)\Big) \cdot \Big(1 + \alpha_{26} \cdot 0 \Big) \\
&+ \alpha_{26}^2 \cdot \sum_{b_s}sel(rt_r[2..], b_s) \cdot \Big(\sum_{i = 0}^2 eq(rt_r[..2], i) record_{ri}(b_s) + \sum_{i = 3}^3 eq(rt_r[..2], i)\Big) \\
&+ \alpha_{26}^2 \cdot \sum_{b_s}\Big(eq(rt_r[2..],b_s) - sel(rt_r[2..], b_s)\Big) \cdot 1 \\
&+ \alpha_{26}^3 \cdot \sum_{b_s}sel(rt_w[1..], b_s) \cdot \Big(\sum_{i = 0}^1 eq(rt_w[..1], i) record_{wi}(b_s)\Big) \\
&+ \alpha_{26}^3 \cdot \sum_{b_s}\Big(eq(rt_w[1..],b_s) - sel(rt_w[1..], b_s)\Big) \cdot 1
\end{align}
$$

After reorganizing the equation:

$$
\begin{align}
&out'_{lk\_d}(rt_{lk}) + \alpha_{26} \cdot out'_{lk\_n}(rt_{lk}) + \alpha_{26}^2 \cdot out'_r(rt_r) + \alpha_{26}^3 \cdot out'_w(rt_w) - (1 + \alpha_{26}^2 + \alpha_{26}^3) \\
&= \sum_{b_s} sel(rt_{lk}[6..], b_s) \Big(\sum_{i = 0}^{40} eq(rt_{lk}[..6], i) record_{lki}(b_s) + \sum_{i = 41}^{63} eq(rt_{lk}[..6], i) + \alpha_{26} \cdot \sum_{i = 0}^{40} eq(rt_{lk}[..6], i) - 1 \Big) \\
&+ \alpha_{26}^2 \cdot \sum_{b_s}sel(rt_r[2..], b_s) \cdot \Big(\sum_{i = 0}^2 eq(rt_r[..2], i) record_{ri}(b_s) + \sum_{i = 3}^3 eq(rt_r[..2], i) - 1\Big) \\
&+ \alpha_{26}^3 \cdot \sum_{b_s}sel(rt_w[1..], b_s) \cdot \Big(\sum_{i = 0}^1 eq(rt_w[..1], i) record_{wi}(b_s) - 1\Big)
\end{align}
$$

#### Final layer: Main body

$$
\begin{align}
&\sum_{i = 0}^{40}\alpha_{27}^i \cdot record_{lki}(rt) + \sum_{i = 0}^{2}\alpha_{27}^{i + 41} \cdot record_{ri}(rt) + \sum_{i = 0}^{1}\alpha_{27}^{i + 44} \cdot record_{wi}(rt) \\
&= \mathsf{RANGE} + r_0 \cdot 2^{15} \cdot carry_{pc}(rt) + r_1 \\
&+ \alpha_{27} \cdot (\mathsf{BYTECODE} + r_0 \cdot pc[0](rt) + r_0^2 \cdot pc[1](rt) + r_0^3 \cdot \mathsf{ADD} + r_1) \\
&+ \alpha_{27}^2 \cdot (\mathsf{RANGE} + r_0 \cdot 2^{6} \cdot (top(rt) - 2) + r_1) \\
&+ \alpha_{27}^3 \cdot(\mathsf{RANGE} + r_0 \cdot stack\_ts\_lt0[0](rt) + r_1) \\
&+ \alpha_{27}^3 \cdot(\mathsf{RANGE} + r_0 \cdot stack\_ts\_lt0[1](rt) + r_1) \\
&+ \alpha_{27}^5 \cdot(\mathsf{RANGE} + r_0 \cdot stack\_ts\_lt0[2](rt) + r_1) \\
&+ \alpha_{27}^6 \cdot(\mathsf{RANGE} + r_0 \cdot stack\_ts\_lt1[0](rt) + r_1) \\
&+ \alpha_{27}^7 \cdot(\mathsf{RANGE} + r_0 \cdot stack\_ts\_lt1[1](rt) + r_1) \\
&+ \alpha_{27}^8 \cdot (\mathsf{RANGE} + r_0 \cdot stack\_ts\_lt1[2](rt) + r_1) \\
&+ \sum_{i = 9}^{24} \alpha_{27}^i \cdot (\mathsf{RANGE} + r_0 \cdot (addend_0[i - 9](rt) + addend_1[i - 9](rt) - 2^{16} \cdot carry[i - 9](rt)) + r_1) + \sum_{i = 10}^{24} \alpha_{27}^i r_0 carry[i - 10](rt)\\
&+ \sum_{i = 25}^{40} \alpha_{27}^i \cdot (\mathsf{RANGE} + r_0 \cdot 2^{15} \cdot carry[i - 25](rt) + r_1) \\
&+ \alpha_{27}^{41} \cdot (\mathsf{STATE} + r_0 \cdot pc[0](rt) + r_0^2 \cdot pc[1](rt) + r_0^3 \cdot ts(rt) + r_0^4 \cdot top(rt) + r_1) \\
&+ \alpha_{27}^{42} \cdot (\mathsf{STACK} + r_0 \cdot (top(rt) - 1) + r_0^2 \cdot addend_0[0](rt) + \cdot + r_0^{17} \cdot addend_0[15](rt) + r_0^{18} \cdot (ts(rt) - 2^{32} \cdot stack\_ts\_lt0[2](rt) - 2^{16} \cdot stack\_ts\_lt0[1](rt) - stack\_ts\_lt0[0](rt)) + r_1) \\
&+ \alpha_{27}^{43} \cdot (\mathsf{STACK} + r_0 \cdot (top(rt) - 2) + r_0^2 \cdot addend_1[0](rt) + \cdot + r_0^{17} \cdot addend_1[15](rt) + r_0^{18} \cdot (ts(rt) - 2^{32} \cdot stack\_ts\_lt1[2](rt) - 2^{16} \cdot stack\_ts\_lt1[1](rt) - stack\_ts\_lt1[0](rt)) + r_1) \\
&+ \alpha_{27}^{44} \cdot (\mathsf{STATE} + r_0 \cdot (pc[0](rt) + 1 - 2^{32} \cdot carry_{pc}(rt)) + r_0^2 \cdot (pc[1](rt) + carry_{pc}(rt)) + r_0^3 \cdot (ts(rt) + 1) + r_0^4 \cdot (top(rt) - 1) + r_1) \\
&+ \alpha_{27}^{45} \cdot (\mathsf{STACK} + r_0 \cdot (top(rt) - 2) + r_0^2 \cdot (addend_0[0](rt) + addend_1[0](rt) - 2^{16} \cdot carry[0]) + \cdot + r_0^{17} \cdot (addend_0[15](rt) + addend_1[15](rt) - 2^{16} \cdot carry[15](rt) + carry[14](rt)) + r_0^{18} \cdot ts(rt) + r_1)
\end{align}
$$

After reorganizing the equation:

$$
\begin{align}
&\sum_{i = 0}^{40}\alpha_{27}^i \cdot record_{lki}(rt) + \sum_{i = 0}^{2}\alpha_{27}^{i + 41} \cdot record_{ri}(rt) + \sum_{i = 0}^{1}\alpha_{27}^{i + 44} \cdot record_{wi}(rt) \\
&- \mathsf{BYTECODE} - r_0^3\mathsf{ADD} - (\sum_{i = 1}^{40}\alpha_{27}^i) \mathsf{RANGE} - (\alpha_{27}^{41} + \alpha_{27}^{44}) \mathsf{STATE} - (\alpha_{27}^{42} + \alpha_{27}^{43} + \alpha_{27}^{45})\mathsf{STACK} - (\sum_{i = 0}^{45}\alpha_{27}^i)r_1 + r_0(2^{7}\alpha_{27}^2 + \alpha_{27}^{42} + 2\alpha_{27}^{43} + 2\alpha_{27}^{45} - \alpha_{27}^{44}) + r_0^4\alpha_{27}^{44} \\
&= r_0(1 + \alpha_{27}^{41} + \alpha_{27}^{44}) \cdot pc[0](rt) \\
&+ r_0^2(1 + \alpha_{27}^{41} + \alpha_{27}^{44}) \cdot pc[1](rt)\\
&+ (r_0^3(\alpha_{27}^{41}+ \alpha_{27}^{44}) + r_0^{18}(\alpha_{27}^{42} + \alpha_{27}^{43} + \alpha_{27}^{45})) \cdot ts(rt) \\
&+ (r_0(2^6 \alpha_{27}^{2} + \alpha_{27}^{42} + \alpha_{27}^{43} + \alpha_{27}^{45}) + r_0^4(\alpha_{27}^{41} + \alpha_{27}^{44})) \cdot top(rs) \\
&+ (r_0 (2^{15} \alpha_{27} - 2^{32} \alpha_{27}^{44}) + r_0^2(\alpha_{27}^{44})) \cdot carry_{pc}(rt) \\
&+ \sum_{i = 0}^{15}(r_0\alpha_{27}^{9 + i} + r_0^{2 + i}(\alpha_{27}^{42} + \alpha_{27}^{45})) \cdot addend_0[i](rt) \\
&+ \sum_{i = 0}^{15}(r_0\alpha_{27}^{9 + i} + r_0^{2 + i}(\alpha_{27}^{43} + \alpha_{27}^{45})) \cdot addend_0[i](rt) \\
&+ \sum_{i=0}^{14}(r_0(\alpha_{27}^{10 + i} - 2^{16}\alpha_{27}^{9 + i} + 2^{15}\alpha_{27}^{25 + i}) - r_0^{2 + i}2^{16} \alpha_{27}^{45} + r_0^{3 + i}\alpha_{27}^{45}) carry[i](rt) \\
&+ (r_0(- 2^{16}\alpha_{27}^{9 + i} + 2^{15}\alpha_{27}^{25 + i}) - r_0^{2 + i}2^{16} \alpha_{27}^{45}) carry[15](rt) \\
\end{align}
$$

## Time consuming (outdated)

### Binary tree

| num_vars | prover time | setup (time before sumcheck) |
|-------------------------|--------------|------------------------------|
| **prove split and product** | | |
| 0 | 1.821ms | 23.200µs |
| 1 | 342.451µs | 56.780µs |
| 2 | 424.292µs | 40.410µs |
| 3 | 508.262µs | 45.700µs |
| 4 | 566.923µs | 55.400µs |
| 5 | 668.973µs | 45.280µs |
| 6 | 868.954µs | 58.760µs |
| 7 | 834.033µs | 66.300µs |
| 8 | 1.094ms | 82.361µs |
| 9 | 1.561ms | 169.661µs |
| 10 | 2.086ms | 248.871µs |
| 11 | 2.537ms | 409.291µs |
| 12 | 1.712ms | 358.852µs |
| 13 | 2.835ms | 493.372µs |
| 14 | 3.032ms | 646.133µs |
| 15 | 4.011ms | 1.130ms |
| 16 | 5.030ms | 1.563ms |
| 17 | 8.301ms | 2.993ms |
| 18 | 13.419ms | 5.224ms |
| 19 | 23.927ms | 10.524ms |
| 20 | 43.387ms | 20.724ms |
| 21 | 86.262ms | 43.771ms |
| 22 | 155.693ms | 76.566ms |
| 23 | 288.990ms | 140.764ms |
| 24 | 534.614ms | 263.226ms |
| 25 | 1.038s | 523.181ms |
| **prove select** | | |
| 20 | 1.523s | 1.507s |
| **total** | **4.309640456s** | |

### 4-ary tree

| num_vars | prover time | setup (time before sumcheck) |
|-------------------------|--------------|------------------------------|
| **prove split and product** | | |
| 0 | 1.745ms | 20.710µs |
| 2 | 755.783µs | 46.320µs |
| 4 | 945.794µs | 51.760µs |
| 6 | 1.161ms | 59.290µs |
| 8 | 1.787ms | 88.181µs |
| 10 | 2.250ms | 253.031µs |
| 12 | 2.708ms | 341.651µs |
| 14 | 5.322ms | 1.217ms |
| 16 | 7.650ms | 1.754ms |
| 18 | 19.357ms | 5.608ms |
| 20 | 64.324ms | 21.960ms |
| 22 | 226.425ms | 78.134ms |
| 24 | 786.492ms | 262.881m |
| **prove select** | | |
| 20 | 1.483s | 1.467s |
| total | 3.044195178s | |