<style>
.add-table table tr td:first-child {
background-color: #ecf2ea;
}
.add-table table tr:nth-child(1) td:not(:first-child):not(:last-child), tr:nth-child(2) td:not(:first-child):not(:last-child), tr:nth-child(3) td:not(:first-child):not(:last-child), tr:nth-child(4) td:not(:first-child):not(:last-child), tr:nth-child(5) td:not(:first-child):not(:last-child) {
background-color: #fdf2e6;
}
.add-table table tr:nth-child(6) td:not(:first-child):not(:last-child) {
background-color: #fcf6e5;
}
.add-table table tr:nth-child(7) td:not(:first-child):not(:last-child), tr:nth-child(8) td:not(:first-child):not(:last-child) {
background-color: #edf3fc;
}
.jumpi-table table tr td:first-child {
background-color: #ecf2ea;
}
.jumpi-table table tr:nth-child(1) td:not(:first-child):not(:last-child), tr:nth-child(2) td:not(:first-child):not(:last-child), tr:nth-child(3) td:not(:first-child):not(:last-child) {
background-color: #fdf2e6;
}
.jumpi-table table tr:nth-child(4) td:not(:first-child):not(:last-child) {
background-color: #fcf6e5;
}
.jumpi-table table tr:nth-child(5) td:not(:first-child):not(:last-child), tr:nth-child(6) td:not(:first-child):not(:last-child) {
background-color: #edf3fc;
}
</style>

## Definition

- `slot` - multiple rows to verify a single `op`
- `q` - selector to enable a slot, should be `1` only in the last row in a `slot`.
- `x_diff_inv` - witnessed by prover to be `inv(fixed_x - x)`, where the `fixed_x` is baked into circuit. It's used to switch on op and case custom constraint by `1 - (fixed_x - x) * x_diff_inv` (`is_zero` expression).
- `context`
- `gc` - global counter
- `addr` - address holding opcodes
- `pc` - program counter
- `op` - operator respect to `addr` and `pc`
- `sp` - stack pointer
- `...` - more will be needed, see more details [here](https://hackmd.io/0Z3N9gniRAmOg8X1RN6VAg)
- `v0..v31` - decompressed operating values in word bytes from low to high (`0x42` will be `[0x42, 0, ..., 0]`)
- `inv` - a function returns inverse in field `fq` if exists, returns `0` otherwise.
- `compress` a function to compress variadic inputs into single `fq` using random linear combination.

## Layout

In evm circuit, we need to verify all possible opcodes including their error cases in a single fixed slot, so we need prover to provide some auxiliary values for us to switch on custom constraint. Naively the circuit would need 3 regions:

- operating values
The inputs and outputs of a opcode. For example, a `ADD` takes 2 inputs and returns 1 output. Decompression is needed when the relation between inputs and outputs requires byte to byte check.
- context
The current context evm holds, could have `gc`, `addr`, `pc`, etc...
- op and case switch
The auxiliary values for circuit to know which custom constraint of opcodes and cases to switch on. Naively we could require prover to witness the `{op,case}_diff_inv` for circuit to produce a `is_zero` boolean expression to switch the op ==[Q1](#Q1-Switch)==.
The case here stands for all possiblibility when executing a op, for example, a `ADD` could have 1 success case and 2 error cases `ErrOutOfGas` and `ErrStackUnderflow`.

For visualization, the layout could be like:


## Example - `ADD`

If we don't care about the limit of wire number and we could have such wide circut (`w=32`) to put each word into one row.

Then if now we have `(op, va, vb, vc) = (1, 3, 5, 8)` as example (to verify `8 = 3 + 5`), We decompress the values in bus mapping into 3 `v0..v31` and do custom constraint of `ADD`.

<div class="add-table">

| `q` | `a_1` | `a_2` | `a_3` | `a_4` | `a_5` | `...` | `a_32` | Note |
| ------ | ------------------ | ------------------ | ------------------ | ----- | ----- | ----- | ------ | --------------------------------------- |
| `...` | `...` | `...` | `...` | `...` | `...` | `...` | `...` | Cells storing values |
| `0` | `0` | `0` | `0` | `0` | `0` | `...` | `0` | ↑ (`carry`) |
| `0` | `8` | `0` | `0` | `0` | `0` | `...` | `0` | ↑ (`vc`) |
| `0` | `5` | `0` | `0` | `0` | `0` | `...` | `0` | ↑ (`vb`) |
| `0` | `3` | `0` | `0` | `0` | `0` | `...` | `0` | ↑ (`va`) |
| `0` | `gc` | `addr` | `pc` | `op` | `sp` | `...` | `...` | Context |
| `...` | `...` | `...` | `...` | `...` | `...` | `...` | `...` | Witness inverse of op difference or `0` |
| `1` | `inv(1-1)` (`ADD`) | `inv(2-1)` (`MUL`) | `inv(3-1)` (`SUB`) | `...` | `...` | `...` | `...` | ↑ |

</div>

Then several constraints we will have (`cur()` to the last row):

// switch on custom constraint only when the opcode is ADD
if is_zero(op - 1) {
    if case_success {
        // two source read
        for (gc, sp, v) in [(gc, sp, va), (gc+1, sp+1, vb)] {
            bus_mapping_lookup(
                gc,
                Stack,
                sp,
                compress(v),
                Read
            )
        }

        // one result write
        bus_mapping_lookup(
            gc+2,
            Stack,
            sp+1,
            compress(vc),
            Write
        )

        // result is indeed added by two source
        eight_bit_lookup(va[0])
        eight_bit_lookup(vb[0])
        eight_bit_lookup(vc[0])
        256 * carry[0] + vc[0] === va[0] + vb[0]

        for i in range 1..=31 {
            eight_bit_lookup(va[i])
            eight_bit_lookup(vb[i])
            eight_bit_lookup(vc[i])

            256 * carry[i] + vc[i] === va[i] + vb[i] + carry[i-1]
        }

        // gc in the next slot should increase 3
        gc_next === gc + 3

        // addr should be same
        addr_next === addr

        // pc should increase 1
        pc_next === pc + 1

        // sp should increase 1 (ADD = 2 POP + 1 PUSH)
        sp_next === sp + 1
    }

    if case_err_out_of_gas {
        // TODO:
        // - gas_left > gas_cost
        // - consume all give gas
        // - context switch to parent
        // - ...
    }

    if case_err_stack_underflow {
        // TODO:
        // - sp + 1 === 1023 + surfeit
        // - consume all give gas
        // - context switch to parent
        // - ...
    }
}

Note we don't need 8-bit addition lookup here, because in some op like [comparators](https://github.com/appliedzkp/zkevm-specs/blob/master/src/encoding/comparator.py) are already using 8-bit range lookup to check if values are in 8-bit. So 8-bit range check become free for other ops because we only need to add the switch boolean expression together to enable it.

Once we know all values are in 8-bit, we only need to iteratively check every bytes are added correctly with the carry bit by simple custom constraint.

## Example - `JUMPI`

We have `(op, dest, cond) = (87, 4, cond)` as example (to verify a jump to `pc = 4` when condition is non zero). Here the `cond` is compressed form of actual value, which is used directly by `is_zero` gadget to check if it's zero or not, prover has negligible chance to compress a non zero value into `0`. (`is_zero` gadget needs another cell to allocate inverse of `cond` to produce the expression, so is the `inv(cond)`)

<div class="jumpi-table">

| `q` | `a_1` | `a_2` | `a_3` | `a_4` | `a_5` | `...` | `a_32` | Note |
| ------ | ------------------- | ------------------- | ------------------- | ----- | ----- | ----- | ------ | --------------------------------------- |
| `...` | `...` | `...` | `...` | `...` | `...` | `...` | `...` | Cells storing values |
| `0` | `cond` | `inv(cond)` | `0` | `0` | `0` | `...` | `0` | ↑ (`cond`) |
| `0` | `4` | `0` | `0` | `0` | `0` | `...` | `0` | ↑ (`dest`) |
| `0` | `gc` | `addr` | `pc` | `op` | `sp` | `...` | `...` | Context |
| `...` | `...` | `...` | `...` | `...` | `...` | `...` | `...` | Witness inverse of op difference or `0` |
| `1` | `inv(1-87)` (`ADD`) | `inv(2-87)` (`MUL`) | `inv(3-87)` (`SUB`) | `...` | `...` | `...` | `...` | ↑ |

</div>

> We could further optimize the cells cost if needed, becasue a contract could have `0x6000` opcodes. So `dest` could fit in two cells.

// switch on custom constraint only when the opcode is JUMPI
if is_zero(op - 87) {
    if case_success {
        // one stack read for destination
        bus_mapping_lookup(
            gc,
            Stack,
            sp,
            compress(dest),
            Read
        )

        // one stack read for condition
        bus_mapping_lookup(
            gc+1,
            Stack,
            sp+1,
            cond,
            Read
        )

        // we don't jump when condition is zero
        if is_zero(cond) {
            pc_next === pc + 1 // pc should increase by 1
        } else {
            pc_next === dest // pc should change to dest
            op_next === 91   // destination should be JUMPDEST
        }

        gc_next === gc + 1 // gc should increase by 1
        addr_next === addr // addr remains the same
        sp_next === sp + 2 // sp should increase by 2 (JUMPI = 2 POP)
    }

    if case_err_out_of_gas {
        // TODO:
        // - gas_left > gas_cost
        // - consume all give gas
        // - context switch to parent
        // - ...
    }

    if case_err_stack_underflow {
        // TODO:
        // - sp + 1 === 1023 + surfeit
        // - consume all give gas
        // - context switch to parent
        // - ...
    }}

    if case_err_jump_dest_invalid {
        // TODO:
        // - op_lookup(addr, dest, dest_op) && dest_op !== JUMPDEST
        // - consume all give gas
        // - context switch to parent
        // - ...
    }

    if case_err_jump_dest_out_of_range {
        // TODO:
        // - dest >= len(code)
        // - consume all give gas
        // - context switch to parent
        // - ...
    }
}

## Question & Discussion

### Q1. Switch

Now it costs a cell for `op_diff_inv` per op for circuit to get a `is_zero` boolean expression, which means a slot requires 142 cells just for op switch.

The case switch is in the same situation, the op with the most error cases is `CREATE`, which could has 7 error cases. Then we need 7 cells per slot for case switch.

> Is there other more efficient methods to produce a boolean expression for each opcode?
> [name=han]

### Q2. Multi-Slot op

There are ops `SHA3`, `CALLDATACOPY`, `CODECOPY`, `EXTCODECOPY`, `RETURNDATACOPY`, `LOGX`, `CREATEX` with variadic values we need to operate, so multiple `slot` will be needed because we don't know how much values to process when building the circuit.

We could have `slot_todo` in each `slot` to count how many things we still need to handle.

### Q3. Proof size discussion

How much the proof size will increase for KZG10 if we

- access a new rotation $n$ on $m$ columns
- $[W_{\mathfrak{z\omega^n}}]_1$ element (linear combination commitment)
- $(\bar{c}_{i\omega^n})_{i=1}^m$ scalars (evaluations)
- add an extra column $c_i$
- $[c_i]_1$ element (commitment)
- $\bar{c}_i$ scalar (evaluation)

If we don't want to have too wide circuit (too much column), we have to fold `v0, ..., v31` into different rows, then the rotation will become more complicated and new rotations might be needed. So we need to know how much they cost then we can decide the cheap one for circuit dimension.

> Not sure if this estimation makes sense
> [name=han]