Copy Circuit

specs/copy-proof.md

@@ -0,0 +1,57 @@
+# Copy Proof
+
+The copy proof checks the values in the copy table and applies the lookup arguments to the corresponding tables to check if the value read from and write to data source is correct.
+It also checks the padding behavior that the value read from an out-of-boundary address is 0.
+
+## Circuit Layout
+
+First, copy circuit contains 13 columns from the [copy table](./tables.md#copytable) with the same witness assignment.
+Every two rows in the copy circuit represent a copy step where the first row is a read operation and the second is a write operation.
+A copy event consists of multiple copy steps, which the first row in the copy event has `is_first` assigned to 1 and the last row has `is_last` assigned to 1.
+
+In addition to the columns in the copy table, copy circuit adds a few auxiliary columns to help check the constraints.
+
+- `is_memory`: indicates if `Type` is `Memory` using `IsZero` gadget.
+- `is_bytecode`: indicates if `Type` is `Bytecode` using `IsZero` gadget.
+- `is_tx_calldata`: indicates if `Type` is `TxCalldata` using `IsZero` gadget.
+- `is_tx_log`: indicates if `Type` is `TxLog` using `IsZero` gadget.
+
+## Circuit Constraints
+
+The constraints are divided into three groups.
+
+First, the circuit adds common constraints that applied to every rows in the circuit:
+
+- Boolean check for `is_first`, and `is_last`
+- Check `is_first == 0` when `q_step == 0`
+- Check `is_last == 0` when `q_step == 1`
+- Construct the IsZero gadget and constrain `is_memory`, `is_bytecode`, `is_tx_calldata`, and `is_tx_log`.
+- The transition constraints from a copy step to the next step (with 2-row rotation), applied to all rows except the last two rows (the last step) in a copy event:
+    - `ID`, `Type`, `AddressEnd` should be same between two steps.
+    - `Address` increase by 1 in the next copy step.
+- The transition constraints for `RwCounter` and `RwcIncreaseLeft` column
+    - define `rw_diff` to be 1 if the `Type` is `Memory` or `TxLog` and `Padding` is 0 in the current row; otherwise 0.
+    - when it's not the last row in a copy event (`is_last == 0`), `RwCounter` increases by `rw_diff` and `RwcIncreaseLeft` decrases by `rw_diff`.
+    - when it's the last row in a copy event (`is_last == 1`), `RwcIncreaseLeft` is equal to `rw_diff`.
+
+Second, the circuit adds the constraints for every copy step in the circuit, when `q_step` is 1.
+
+- Look up the copy type pair `(Type, Type[1])` in a fixed table to make sure it's a valid copy step.
+- Constrain the transition for `BytesLeft`
+    - when it's not the last step (`is_last[1] != 1`), decrease by 1 in the next step
+    - otherwise, equals to 1.
+- Constrain the write value equals to read value: `Value[1] == Value`
+- Constrain `Value == 0` when `Padding == 1`.
+- Construct the LT gadget to compare `Address` and `AddressEnd` in the read operation. If `Address >= AddressEnd`, constrain `Padding == 1`
+- Constrain `Padding[1] == 0` as the write operation is never padded.
+
+Third, the circuit adds the lookup arguments to the corresponding tables.
+
+- When `Type` is `Memory` or `is_memory == 1` and `Padding == 0`, look up the `Value` to `rw_table` with `Memory` tag.
+- When `Type` is `TxCalldata` or `is_tx_calldata == 1` and `Padding == 0`, look up the `Value` to `tx_table`.
+- When `Type` is `Bytecode` or `is_bytecode == 1` and `Padding == 0`, look up the `Value` and `IsCode` to `bytecode_table`
+- When `Type` is `TxLog` or `is_tx_log == 1`, look up the `Value` to `rw_table` with `TxLog` tag.
+
+## Code
+
+Please refer to `src/zkevm-specs/copy_circuit.py`

specs/tables.md

@@ -271,3 +271,52 @@ Columns expressions in circuit:
 - Key: `key_rlc_mult`
 - ValuePrev: `is_nonce_mod * sel1 + is_balance_mod * sel2 + is_codehash_mod * sel2 + is_storage_mod * mult_diff`
 - ValueCur: `is_nonce_mod * s_mod_node_hash_rlc + is_balance_mod * c_mod_node_hash_rlc + is_codehash_mod * c_mod_node_hash_rlc + is_storage_mod * acc_c`
+
+## `copy_table`
+
+Proved by the copy circuit.
+
+The copy table consists of 13 columns, described as follows:
+
+- **q_step**: a fixed column for boolean value to indicate a copy step, always alternating between 1 and 0, where 1 indicates a read op and 0 indicates a write op.
+- **is_first**: a boolean value to indicate the first row in a copy event.
+- **is_last**: a boolean value to indicate the last row in a copy event.
+- **ID**: could be `$txID`, `$callID`, `$codeHash` (RLC encoded).
+- **Type**: indicates the type of data source, including `Memory`, `Bytecode`, `TxCalldata`, `TxLog`.
+- **Address**: indicates the address in the source data, could be memory address, byte index in the bytecode, tx call data, and tx log data. When the data type is `TxLog`, the address is the combination of byte index, `TxLogFieldTag.Data` tag, and `LogID`.
+- **AddressEnd**: indicates the address boundary of the source data. Any data read from address greater than or equal to `AddressEnd` should be 0. Note `AddressEnd` is only valid for read operations or `q_step` is 1.
+- **BytesLeft**: indicates the number of bytes left to be copied.
+- **Value**: indicates the value read or write from source or to the destination.
+- **Pad**: indicates if the value read from the source is padded. Only valid for read operations or `q_step` is 1.
+- **IsCode**: a boolean value to indicate if the `Value` is an executable opcode or the data portion of `PUSH*` operations. Only valid when `Type` is `Bytecode`.
+- **RwCounter**: indicates the current RW counter at this row. This value will be used in the lookup to the `rw_table` when `Type` is  `Memory` or `TxLog`.
+- **RwcIncreaseLeft**: indicates how much the RW counter will increase in a copy event.
+
+
+Unlike other lookup tables, the copy table is a virtual table. The lookup entry is not a single row in the table, and not every row corresponds to a lookup entry.
+Instead, a lookup entry is constructed from the first two rows in each copy event as
+`(is_first, ID, Type, ID[1], Type[1], Address, AddressEnd, Address[1], BytesLeft, RwCounter, RwcIncreaseLeft)`, where `is_first` is 1 and `Column[1]` indicates the next row in the corresponding column.
+
+The table below lists all of copy pairs supported in the copy table:
+- Copy from Tx call data to memory (`CALLDATACOPY`).
+- Copy from caller/callee memory to callee/caller memory (`CALLDATACOPY`, `RETURN` (not create), `RETURNDATACOPY`, `REVERT`).
+- Copy from bytecode to memory (`CODECOPY`, `EXTCODECOPY`).
+- Copy from memory to bytecode (`CREATE`, `CREATE2`, `RETURN` (create))
+- Copy from memory to TxLog in the `rw_table` (`LOGX`)
+
+| q_step | q_first | q_last | ID        | Type       | Address        | AddressEnd     | BytesLeft  | Value  | IsCode  | Pad | RwCounter | RwcIncreaseLeft |
+|--------|---------|--------|-----------|------------|----------------|----------------|------------|--------|---------|-----|-----------|-----------------|
+| 1      | 0/1     | 0      | $txID     | TxCalldata | $byteIndex     | $cdLength      | $bytesLeft | $value | -       | 0/1 | -         | $rwcIncLeft     |
+| 0      | 0       | 0/1    | $callID   | Memory     | $memoryAddress | -              | -          | $value | -       | 0   | $counter  | $rwcIncLeft     |
+|        |         |        |           |            |                |                |            |        |         |     |           |                 |
+| 1      | 0/1     | 0      | $callID   | Memory     | $memoryAddress | $memoryAddress | $bytesLeft | $value | -       | 0/1 | $counter  | $rwcIncLeft     |
+| 0      | 0       | 0/1    | $callID   | Memory     | $memoryAddress | -              | -          | $value | -       | 0   | $counter  | $rwcIncLeft     |
+|        |         |        |           |            |                |                |            |        |         |     |           |                 |
+| 1      | 0/1     | 0      | $callID   | Memory     | $memoryAddress | $memoryAddress | $bytesLeft | $value | $isCode | 0/1 | $counter  | $rwcIncLeft     |
+| 0      | 0       | 0/1    | $codeHash | Bytecode   | $byteIndex     | -              | -          | $value | $isCode | 0   | -         | $rwcIncLeft     |
+|        |         |        |           |            |                |                |            |        |         |     |           |                 |
+| 1      | 0/1     | 0      | $codeHash | Bytecode   | $byteIndex     | $codeLength    | $bytesLeft | $value | $isCode | 0/1 | -         | $rwcIncLeft     |
+| 0      | 0       | 0/1    | $callID   | Memory     | $memoryAddress | -              | -          | $value | $isCode | 0   | $counter  | $rwcIncLeft     |
+|        |         |        |           |            |                |                |            |        |         |     |           |                 |
+| 1      | 0/1     | 0      | $callID   | Memory     | $memoryAddress | $memoryAddress | $bytesLeft | $value | -       | 0/1 | $counter  | $rwcIncLeft     |
+| 0      | 0       | 0/1    | $txID     | TxLog      | $byteIndex \|\| TxLogData \|\| $logID | -              | -          | $value | -       | 0   | $counter  | $rwcIncLeft     |

src/zkevm_specs/__init__.py

@@ -1,6 +1,9 @@
 from . import bytecode
+from . import copy_circuit
 from . import encoding
 from . import evm
 from . import opcode
+from . import state
+from . import tx
 from . import util
 from . import tx

src/zkevm_specs/copy_circuit.py

@@ -0,0 +1,111 @@
+from typing import Dict, Iterator, List, NewType, Optional, Sequence, Union, Mapping, Tuple
+
+from .util import FQ, Expression, ConstraintSystem, cast_expr, MAX_N_BYTES, N_BYTES_MEMORY_ADDRESS
+from .evm import (
+    Tables,
+    CopyDataTypeTag,
+    CopyCircuitRow,
+    RW,
+    RWTableTag,
+    FixedTableTag,
+    CopyCircuit,
+    TxContextFieldTag,
+    BytecodeFieldTag,
+    TxLogFieldTag,
+)
+
+
+def lt(lhs: Expression, rhs: Expression, n_bytes: int) -> FQ:
+    assert n_bytes <= MAX_N_BYTES, "Too many bytes to composite an integer in field"
+    assert lhs.expr().n < 256**n_bytes, f"lhs {lhs} exceeds the range of {n_bytes} bytes"
+    assert rhs.expr().n < 256**n_bytes, f"rhs {rhs} exceeds the range of {n_bytes} bytes"
+    return FQ(lhs.expr().n < rhs.expr().n)
+
+
+def verify_row(cs: ConstraintSystem, rows: Sequence[CopyCircuitRow]):
+    cs.constrain_bool(rows[0].is_first)
+    cs.constrain_bool(rows[0].is_last)
+    # is_first == 0 when q_step == 0
+    cs.constrain_zero((1 - rows[0].q_step) * rows[0].is_first)
+    # is_last == 0 when q_step == 1
+    cs.constrain_zero(rows[0].q_step * rows[0].is_last)
+    cs.constrain_equal(rows[0].is_memory, cs.is_zero(rows[0].tag - CopyDataTypeTag.Memory))
+    cs.constrain_equal(rows[0].is_bytecode, cs.is_zero(rows[0].tag - CopyDataTypeTag.Bytecode))
+    cs.constrain_equal(rows[0].is_tx_calldata, cs.is_zero(rows[0].tag - CopyDataTypeTag.TxCalldata))
+    cs.constrain_equal(rows[0].is_tx_log, cs.is_zero(rows[0].tag - CopyDataTypeTag.TxLog))
+
+    # constrain the transition between two copy steps
+    is_last_two_rows = rows[0].is_last + rows[1].is_last
+    with cs.condition(1 - is_last_two_rows) as cs:
+        # not last two rows
+        cs.constrain_equal(rows[0].id, rows[2].id)
+        cs.constrain_equal(rows[0].tag, rows[2].tag)
+        cs.constrain_equal(rows[0].addr + 1, rows[2].addr)
+        cs.constrain_equal(rows[0].src_addr_end, rows[2].src_addr_end)
+
+    # contrain the transition for `rw_counter` and `rwc_inc_left`
+    rw_diff = (1 - rows[0].is_pad) * (rows[0].is_memory + rows[0].is_tx_log)
+    with cs.condition(1 - rows[0].is_last) as cs:
+        # not last row
+        cs.constrain_equal(rows[0].rw_counter + rw_diff, rows[1].rw_counter)
+        cs.constrain_equal(rows[0].rwc_inc_left - rw_diff, rows[1].rwc_inc_left)
+    with cs.condition(rows[0].is_last) as cs:
+        # rwc_inc_left == rw_diff for last row in the copy slot
+        cs.constrain_equal(rows[0].rwc_inc_left, rw_diff)
+
+
+def verify_step(cs: ConstraintSystem, rows: Sequence[CopyCircuitRow]):
+    with cs.condition(rows[0].q_step):
+        # bytes_left == 1 for last step
+        cs.constrain_zero(rows[1].is_last * (1 - rows[0].bytes_left))
+        # bytes_left == bytes_left_next + 1 for non-last step
+        cs.constrain_zero((1 - rows[1].is_last) * (rows[0].bytes_left - rows[2].bytes_left - 1))
+        # write value == read value
+        cs.constrain_equal(rows[0].value, rows[1].value)
+        # value == 0 when is_pad == 1 for read
+        cs.constrain_zero(rows[0].is_pad * rows[0].value)
+        # is_pad == 1 - (src_addr < src_addr_end) for read row
+        cs.constrain_equal(
+            1 - lt(rows[0].addr, rows[0].src_addr_end, N_BYTES_MEMORY_ADDRESS), rows[0].is_pad
+        )
+        # is_pad == 0 for write row
+        cs.constrain_zero(rows[1].is_pad)
+
+
+def verify_copy_table(copy_circuit: CopyCircuit, tables: Tables):
+    cs = ConstraintSystem()
+    copy_table = copy_circuit.table()
+    n = len(copy_table)
+    for i, row in enumerate(copy_table):
+        rows = [
+            row,
+            copy_table[(i + 1) % n],
+            copy_table[(i + 2) % n],
+        ]
+        # constrain on each row and step
+        verify_row(cs, rows)
+        verify_step(cs, rows)
+
+        # lookup into tables
+        if row.is_memory == 1 and row.is_pad == 0:
+            val = tables.rw_lookup(
+                row.rw_counter, 1 - row.q_step, FQ(RWTableTag.Memory), row.id, row.addr
+            ).value
+            cs.constrain_equal(cast_expr(val, FQ), row.value)
+        if row.is_bytecode == 1 and row.is_pad == 0:
+            val = tables.bytecode_lookup(
+                row.id, FQ(BytecodeFieldTag.Byte), row.addr, row.is_code
+            ).value
+            cs.constrain_equal(cast_expr(val, FQ), row.value)
+        if row.is_tx_calldata == 1 and row.is_pad == 0:
+            val = tables.tx_lookup(row.id, FQ(TxContextFieldTag.CallData), row.addr).value
+            cs.constrain_equal(val, row.value)
+        if row.is_tx_log == 1:
+            val = tables.rw_lookup(
+                row.rw_counter,
+                FQ(RW.Write),
+                FQ(RWTableTag.TxLog),
+                row.id,  # tx_id
+                row.addr,
+            ).value
+            cs.constrain_equal(cast_expr(val, FQ), row.value)