From adcef4d2053f27dee373bb2f7c12edc7b226dbf8 Mon Sep 17 00:00:00 2001 From: ashWhiteHat Date: Fri, 10 Feb 2023 16:39:11 +0900 Subject: [PATCH 1/9] rename to circuit --- src/zkevm_specs/__init__.py | 5 ++--- src/zkevm_specs/{bytecode.py => bytecode_circuit.py} | 0 src/zkevm_specs/public_inputs.py | 2 +- src/zkevm_specs/{tx.py => tx_circuit.py} | 0 tests/test_bytecode_circuit.py | 2 +- tests/test_tx_circuit.py | 2 +- 6 files changed, 5 insertions(+), 6 deletions(-) rename src/zkevm_specs/{bytecode.py => bytecode_circuit.py} (100%) rename src/zkevm_specs/{tx.py => tx_circuit.py} (100%) diff --git a/src/zkevm_specs/__init__.py b/src/zkevm_specs/__init__.py index e53b97b48..b2979e553 100644 --- a/src/zkevm_specs/__init__.py +++ b/src/zkevm_specs/__init__.py @@ -1,10 +1,9 @@ -from . import bytecode +from . import bytecode_circuit from . import copy_circuit from . import encoding from . import evm from . import exp_circuit from . import opcode from . import state_circuit -from . import tx +from . import tx_circuit from . import util -from . import tx diff --git a/src/zkevm_specs/bytecode.py b/src/zkevm_specs/bytecode_circuit.py similarity index 100% rename from src/zkevm_specs/bytecode.py rename to src/zkevm_specs/bytecode_circuit.py diff --git a/src/zkevm_specs/public_inputs.py b/src/zkevm_specs/public_inputs.py index e7332c818..7b6303f53 100644 --- a/src/zkevm_specs/public_inputs.py +++ b/src/zkevm_specs/public_inputs.py @@ -15,7 +15,7 @@ Expression, ) from .encoding import is_circuit_code -from .tx import Tag as TxTag +from .tx_circuit import Tag as TxTag from .evm import ( BlockContextFieldTag as BlockTag, ) diff --git a/src/zkevm_specs/tx.py b/src/zkevm_specs/tx_circuit.py similarity index 100% rename from src/zkevm_specs/tx.py rename to src/zkevm_specs/tx_circuit.py diff --git a/tests/test_bytecode_circuit.py b/tests/test_bytecode_circuit.py index af58e611c..24583286d 100644 --- a/tests/test_bytecode_circuit.py +++ b/tests/test_bytecode_circuit.py @@ -1,7 +1,7 @@ import traceback from copy import deepcopy -from zkevm_specs.bytecode import * +from zkevm_specs.bytecode_circuit import * from zkevm_specs.evm import Opcode, Bytecode, BytecodeFieldTag, BytecodeTableRow, is_push from zkevm_specs.util import RLC, rand_fq, U256 diff --git a/tests/test_tx_circuit.py b/tests/test_tx_circuit.py index c81a08619..ba1d1c275 100644 --- a/tests/test_tx_circuit.py +++ b/tests/test_tx_circuit.py @@ -2,7 +2,7 @@ from eth_keys import keys from eth_utils import keccak import rlp -from zkevm_specs.tx import * +from zkevm_specs.tx_circuit import * from zkevm_specs.util import rand_fq, FQ, U64 randomness = rand_fq() From 8278c354fe5dae0d761b50071e75c053fc8d47e6 Mon Sep 17 00:00:00 2001 From: ashWhiteHat Date: Fri, 10 Feb 2023 16:54:43 +0900 Subject: [PATCH 2/9] synchronize start contraints --- specs/state_circuits/01Start.md | 13 +++++++++++++ src/zkevm_specs/state_circuit.py | 17 +++++++---------- 2 files changed, 20 insertions(+), 10 deletions(-) create mode 100644 specs/state_circuits/01Start.md diff --git a/specs/state_circuits/01Start.md b/specs/state_circuits/01Start.md new file mode 100644 index 000000000..05a5d3b7d --- /dev/null +++ b/specs/state_circuits/01Start.md @@ -0,0 +1,13 @@ +# Start + +## Procedure + +The `Start` checks the value to refund to the transaction sender. + +### Circuit behavior + +0. `field_tag`, `address` and `id`, `storage_key` are 0 +1. `rw counter` is increased if it's not first row +2. `value` is 0 +3. `initial value` is 0 +4. `state root` is not changed if it's not first row diff --git a/src/zkevm_specs/state_circuit.py b/src/zkevm_specs/state_circuit.py index 9df63ce5f..34e4b0c7d 100644 --- a/src/zkevm_specs/state_circuit.py +++ b/src/zkevm_specs/state_circuit.py @@ -171,25 +171,22 @@ def assert_in_range(x: FQ, min_val: int, max_val: int) -> None: @is_circuit_code def check_start(row: Row, row_prev: Row): - # 1.0. field_tag is 0 for Start + # 1.0. Unused keys are 0 assert row.field_tag() == 0 - - # 1.1. address is 0 for Start assert row.address() == 0 - - # 1.2. id is 0 for Start assert row.id() == 0 - - # 1.3. storage_key is 0 for Start assert row.storage_key() == 0 - # 1.4. rw_counter increases by 1 for every non-first row + # 1.1. rw_counter increases by 1 for every non-first row assert row.lexicographic_ordering_selector * (row.rw_counter - row_prev.rw_counter - 1) == 0 - # 1.5. Start value is 0 + # 1.2. Start value is 0 assert row.value == 0 - # 1.6. state_root is unchanged for Start + # 1.3. Start initial value is 0 + assert row.initial_value == 0 + + # 1.4. state_root is unchanged for every non-first row assert row.lexicographic_ordering_selector * (row.root - row_prev.root) == 0 From 15de1f584e99a0899e7b43bee3b6f90e7bc15b5f Mon Sep 17 00:00:00 2001 From: ashWhiteHat Date: Fri, 10 Feb 2023 17:27:15 +0900 Subject: [PATCH 3/9] describe memory, stack and storage --- specs/state-proof.md | 42 +++++++++++++++++++++++++++--- specs/state_circuits/01Start.md | 13 --------- specs/state_circuits/07TxRefund.md | 12 --------- src/zkevm_specs/state_circuit.py | 16 ++++++++---- 4 files changed, 50 insertions(+), 33 deletions(-) delete mode 100644 specs/state_circuits/01Start.md delete mode 100644 specs/state_circuits/07TxRefund.md diff --git a/specs/state-proof.md b/specs/state-proof.md index 617b3b4f1..28ee9894a 100644 --- a/specs/state-proof.md +++ b/specs/state-proof.md @@ -41,9 +41,45 @@ found in the table, and a reverse ordering will make the difference to wrap around to a very high value (due to the field arithmetic), causing the result to not be in the table. -The exact list of constraints is documented in detail as comments in the python -code implementation. +### Start + +1.0. `field_tag`, `address` and `id`, `storage_key` are 0 +1.1. `rw counter` is increased if it's not first row +1.2. `value` is 0 +1.3. `initial value` is 0 +1.4. `state root` is not changed if it's not first row + +### Memory + +2.0. `field_tag` and `storage_key` are 0 +2.1. `value` is 0 if first access and READ +2.2. Memory address is in 32 bits range +2.3. `value` is byte +2.4. `initial value` is 0 +2.5. `state root` is not changed + +### Stack + +3.0. `field_tag` and `storage_key` are 0 +3.1. First access is WRITE +3.2. Stack address is in 10 bits range +3.3. Stack address is increated only 0 or 1 +3.4. `initial value` is 0 +3.5. `state root` is not changed + +### Storage + +4.0. `storage_key` is 0 +4.1. non-existing proof if value is 0 +4.2. mpt_update exists in mpt circuit for AccountStorage last access + +### Tx Refund + +7.0. `address`, `field_tag` and `storage_key` are 0 +7.1. `state root` is not changed +7.2. `initial value` is 0 +7.3. First access for a set of all keys are 0 if READ ## Code -Please refer to `src/zkevm-specs/state.py` +Please refer to `src/zkevm-specs/state_circuit.py` diff --git a/specs/state_circuits/01Start.md b/specs/state_circuits/01Start.md deleted file mode 100644 index 05a5d3b7d..000000000 --- a/specs/state_circuits/01Start.md +++ /dev/null @@ -1,13 +0,0 @@ -# Start - -## Procedure - -The `Start` checks the value to refund to the transaction sender. - -### Circuit behavior - -0. `field_tag`, `address` and `id`, `storage_key` are 0 -1. `rw counter` is increased if it's not first row -2. `value` is 0 -3. `initial value` is 0 -4. `state root` is not changed if it's not first row diff --git a/specs/state_circuits/07TxRefund.md b/specs/state_circuits/07TxRefund.md deleted file mode 100644 index b18842378..000000000 --- a/specs/state_circuits/07TxRefund.md +++ /dev/null @@ -1,12 +0,0 @@ -# Tx Refund - -## Procedure - -The `Tx Refund` checks the value to refund to the transaction sender. - -### Circuit behavior - -0. `address`, `field_tag` and `storage_key` are 0 -1. `state root` is not changed -2. `initial value` is 0 -3. First access for a set of all keys are 0 if READ diff --git a/src/zkevm_specs/state_circuit.py b/src/zkevm_specs/state_circuit.py index 34e4b0c7d..731d51264 100644 --- a/src/zkevm_specs/state_circuit.py +++ b/src/zkevm_specs/state_circuit.py @@ -212,7 +212,10 @@ def check_memory(row: Row, row_prev: Row): # 2.3. value is a byte assert_in_range(row.value, 0, 2**8 - 1) - # 2.4 state root does not change + # 2.4. Start initial value is 0 + assert row.initial_value == 0 + + # 2.5. state root does not change assert row.root == row_prev.root @@ -244,7 +247,10 @@ def check_stack(row: Row, row_prev: Row): stack_ptr_diff = get_stack_ptr(row) - get_stack_ptr(row_prev) assert_in_range(stack_ptr_diff, 0, 1) - # 3.4 state root does not change + # 3.4. Stack initial value is 0 + assert row.initial_value == 0 + + # 3.5 state root does not change assert row.root == row_prev.root @@ -253,11 +259,11 @@ def check_storage(row: Row, row_prev: Row, row_next: Row, tables: Tables): # 4.0. Unused keys are 0 assert row.field_tag() == 0 - # value = 0 means the leaf doesn't exist. 0->0 transition requires a - # non-existing proof. + # 4.1. value = 0 means the leaf doesn't exist. 0->0 + # transition requires a non-existing proof. is_non_exist = FQ(row.value.expr() == FQ(0)) * FQ(row.initial_value.expr() == FQ(0)) - # 4.1. MPT lookup for last access to (address, storage_key) + # 4.2. MPT lookup for last access to (address, storage_key) if not all_keys_eq(row, row_next): tables.mpt_lookup( row.address(), From 1ad58d3c6a0d01de6a87e85ef4dbfaedc8ff0724 Mon Sep 17 00:00:00 2001 From: ashWhiteHat Date: Sat, 11 Feb 2023 13:00:38 +0900 Subject: [PATCH 4/9] update rw table column --- specs/bytecode-proof.md | 2 +- specs/tables.md | 116 ++++++++++++++++++------------------ specs/transactions-proof.md | 2 +- 3 files changed, 60 insertions(+), 60 deletions(-) diff --git a/specs/bytecode-proof.md b/specs/bytecode-proof.md index 95d681644..0cc6f3173 100644 --- a/specs/bytecode-proof.md +++ b/specs/bytecode-proof.md @@ -169,4 +169,4 @@ As well as (mentioned above) `cur.tag == Header`. ## Code -Please refer to `src/zkevm-specs/bytecode.py`. +Please refer to `src/zkevm-specs/bytecode_circuit.py`. diff --git a/specs/tables.md b/specs/tables.md index 47c39497d..7a9c41759 100644 --- a/specs/tables.md +++ b/specs/tables.md @@ -68,64 +68,64 @@ Details: NOTE: `kN` means `keyN` -| 0 *Rwc* | 1 *IsWrite* | 2 *Tag* (k0) | 3 *Id* (k1) | 4 *Address* (k2) | 5 *FieldTag* (k3) | 6 *StorageKey* (k4) | 7 *Value* | 8 *InitialValue* | 9 *Root* | -| -------- | ----------- | -------------------------- | -------- | -------- | -------------------------- | ----------- | --------- | ---------------- | -------- | -| | | *RwTableTag* | | | | | | | | -| $counter | true | TxAccessListAccount | $txID | $address | | | $value | 0 | $root | -| $counter | true | TxAccessListAccountStorage | $txID | $address | | $storageKey | $value | 0 | $root | -| $counter | $isWrite | TxRefund | $txID | | | | $value | 0 | $root | -| | | | | | | | | | | -| | | | | | *AccountFieldTag* | | | | | -| $counter | $isWrite | Account | | $address | Nonce | | $value | $committedValue | $root | -| $counter | $isWrite | Account | | $address | Balance | | $value | $committedValue | $root | -| $counter | $isWrite | Account | | $address | CodeHash | | $value | $committedValue | $root | -| | | | | | | | | | | -| | | *CallContext constant* | | | *CallContextFieldTag* (ro) | | | | | -| $counter | false | CallContext | $callID | | RwCounterEndOfReversion | | $value | 0 | $root | -| $counter | false | CallContext | $callID | | CallerId | | $value | 0 | $root | -| $counter | false | CallContext | $callID | | TxId | | $value | 0 | $root | -| $counter | false | CallContext | $callID | | Depth | | $value | 0 | $root | -| $counter | false | CallContext | $callID | | CallerAddress | | $value | 0 | $root | -| $counter | false | CallContext | $callID | | CalleeAddress | | $value | 0 | $root | -| $counter | false | CallContext | $callID | | CallDataOffset | | $value | 0 | $root | -| $counter | false | CallContext | $callID | | CallDataLength | | $value | 0 | $root | -| $counter | false | CallContext | $callID | | ReturnDataOffset | | $value | 0 | $root | -| $counter | false | CallContext | $callID | | ReturnDataLength | | $value | 0 | $root | -| $counter | false | CallContext | $callID | | Value | | $value | 0 | $root | -| $counter | false | CallContext | $callID | | IsSuccess | | $value | 0 | $root | -| $counter | false | CallContext | $callID | | IsPersistent | | $value | 0 | $root | -| $counter | false | CallContext | $callID | | IsStatic | | $value | 0 | $root | -| | | | | | | | | | | -| | | *CallContext last callee* | | | *CallContextFieldTag* (rw) | | | | | -| $counter | $isWrite | CallContext | $callID | | LastCalleeId | | $value | 0 | $root | -| $counter | $isWrite | CallContext | $callID | | LastCalleeReturnDataOffset | | $value | 0 | $root | -| $counter | $isWrite | CallContext | $callID | | LastCalleeReturnDataLength | | $value | 0 | $root | -| | | | | | | | | | | -| | | *CallContext state* | | | *CallContextFieldTag* (rw) | | | | | -| $counter | $isWrite | CallContext | $callID | | IsRoot | | $value | 0 | $root | -| $counter | $isWrite | CallContext | $callID | | IsCreate | | $value | 0 | $root | -| $counter | $isWrite | CallContext | $callID | | CodeHash | | $value | 0 | $root | -| $counter | $isWrite | CallContext | $callID | | ProgramCounter | | $value | 0 | $root | -| $counter | $isWrite | CallContext | $callID | | StackPointer | | $value | 0 | $root | -| $counter | $isWrite | CallContext | $callID | | GasLeft | | $value | 0 | $root | -| $counter | $isWrite | CallContext | $callID | | MemorySize | | $value | 0 | $root | -| $counter | $isWrite | CallContext | $callID | | ReversibleWriteCounter | | $value | 0 | $root | -| | | | | | | | | | | -| $counter | $isWrite | Stack | $callID | $stackPointer | | | $value | 0 | $root | -| $counter | $isWrite | Memory | $callID | $memoryAddress | | | $value | 0 | $root | -| $counter | $isWrite | AccountStorage | $txID | $address | | $storageKey | $value | $committedValue | -| | | | | | | | | | | -| | | | | | *TxLogTag* | | | | | -| $counter | true | TxLog | $txID | $logID,0 | Address | 0 | $value | 0 | $root | -| $counter | true | TxLog | $txID | $logID,$topicIndex | Topic | 0 | $value | 0 | $root | -| $counter | true | TxLog | $txID | $logID,$byteIndex | Data | 0 | $value | 0 | $root | -| $counter | true | TxLog | $txID | $logID,0 | TopicLength | 0 | $value | 0 | $root | -| $counter | true | TxLog | $txID | $logID,0 | DataLength | 0 | $value | 0 | $root | -| | | | | | | | | | | -| | | | | | *TxReceiptTag* | | | | | -| $counter | false | TxReceipt | $txID | 0 | PostStateOrStatus | 0 | $value | 0 | $root | -| $counter | false | TxReceipt | $txID | 0 | CumulativeGasUsed | 0 | $value | 0 | $root | -| $counter | false | TxReceipt | $txID | 0 | LogLength | 0 | $value | 0 | $root | +| 0 *Rwc* | 1 *IsWrite* | 2 *Tag* (k0) | 3 *Id* (k1) | 4 *Address* (k2) | 5 *FieldTag* (k3) | 6 *StorageKey* (k4) | 7 *Value* | 8 *ValuePrev* | 9 *Aux1* | 10 *Aux2* | +| -------- | ----------- | -------------------------- | -------- | -------- | -------------------------- | ----------- | --------- | ---------------- | -------- | -------- | +| | | *RwTableTag* | | | | | | | | | +| $counter | true | TxAccessListAccount | $txID | $address | | | $value | 0 | $aux1 | $aux2 | +| $counter | true | TxAccessListAccountStorage | $txID | $address | | $storageKey | $value | 0 | $aux1 | $aux2 | +| $counter | $isWrite | TxRefund | $txID | | | | $value | 0 | $aux1 | $aux2 | +| | | | | | | | | | | | +| | | | | | *AccountFieldTag* | | | | | | +| $counter | $isWrite | Account | | $address | Nonce | | $value | $valuePrev | $aux1 | $aux2 | +| $counter | $isWrite | Account | | $address | Balance | | $value | $valuePrev | $aux1 | $aux2 | +| $counter | $isWrite | Account | | $address | CodeHash | | $value | $valuePrev | $aux1 | $aux2 | +| | | | | | | | | | | | +| | | *CallContext constant* | | | *CallContextFieldTag* (ro) | | | | | | +| $counter | false | CallContext | $callID | | RwCounterEndOfReversion | | $value | 0 | $aux1 | $aux2 | +| $counter | false | CallContext | $callID | | CallerId | | $value | 0 | $aux1 | $aux2 | +| $counter | false | CallContext | $callID | | TxId | | $value | 0 | $aux1 | $aux2 | +| $counter | false | CallContext | $callID | | Depth | | $value | 0 | $aux1 | $aux2 | +| $counter | false | CallContext | $callID | | CallerAddress | | $value | 0 | $aux1 | $aux2 | +| $counter | false | CallContext | $callID | | CalleeAddress | | $value | 0 | $aux1 | $aux2 | +| $counter | false | CallContext | $callID | | CallDataOffset | | $value | 0 | $aux1 | $aux2 | +| $counter | false | CallContext | $callID | | CallDataLength | | $value | 0 | $aux1 | $aux2 | +| $counter | false | CallContext | $callID | | ReturnDataOffset | | $value | 0 | $aux1 | $aux2 | +| $counter | false | CallContext | $callID | | ReturnDataLength | | $value | 0 | $aux1 | $aux2 | +| $counter | false | CallContext | $callID | | Value | | $value | 0 | $aux1 | $aux2 | +| $counter | false | CallContext | $callID | | IsSuccess | | $value | 0 | $aux1 | $aux2 | +| $counter | false | CallContext | $callID | | IsPersistent | | $value | 0 | $aux1 | $aux2 | +| $counter | false | CallContext | $callID | | IsStatic | | $value | 0 | $aux1 | $aux2 | +| | | | | | | | | | | | +| | | *CallContext last callee* | | | *CallContextFieldTag* (rw) | | | | | | +| $counter | $isWrite | CallContext | $callID | | LastCalleeId | | $value | 0 | $aux1 | $aux2 | +| $counter | $isWrite | CallContext | $callID | | LastCalleeReturnDataOffset | | $value | 0 | $aux1 | $aux2 | +| $counter | $isWrite | CallContext | $callID | | LastCalleeReturnDataLength | | $value | 0 | $aux1 | $aux2 | +| | | | | | | | | | | | +| | | *CallContext state* | | | *CallContextFieldTag* (rw) | | | | | | +| $counter | $isWrite | CallContext | $callID | | IsRoot | | $value | 0 | $aux1 | $aux2 | +| $counter | $isWrite | CallContext | $callID | | IsCreate | | $value | 0 | $aux1 | $aux2 | +| $counter | $isWrite | CallContext | $callID | | CodeHash | | $value | 0 | $aux1 | $aux2 | +| $counter | $isWrite | CallContext | $callID | | ProgramCounter | | $value | 0 | $aux1 | $aux2 | +| $counter | $isWrite | CallContext | $callID | | StackPointer | | $value | 0 | $aux1 | $aux2 | +| $counter | $isWrite | CallContext | $callID | | GasLeft | | $value | 0 | $aux1 | $aux2 | +| $counter | $isWrite | CallContext | $callID | | MemorySize | | $value | 0 | $aux1 | $aux2 | +| $counter | $isWrite | CallContext | $callID | | ReversibleWriteCounter | | $value | 0 | $aux1 | $aux2 | +| | | | | | | | | | | | +| $counter | $isWrite | Stack | $callID | $stackPointer | | | $value | 0 | $aux1 | $aux2 | +| $counter | $isWrite | Memory | $callID | $memoryAddress | | | $value | 0 | $aux1 | $aux2 | +| $counter | $isWrite | AccountStorage | $txID | $address | | $storageKey | $value | $valuePrev | +| | | | | | | | | | | | +| | | | | | *TxLogTag* | | | | | | +| $counter | true | TxLog | $txID | $logID,0 | Address | 0 | $value | 0 | $aux1 | $aux2 | +| $counter | true | TxLog | $txID | $logID,$topicIndex | Topic | 0 | $value | 0 | $aux1 | $aux2 | +| $counter | true | TxLog | $txID | $logID,$byteIndex | Data | 0 | $value | 0 | $aux1 | $aux2 | +| $counter | true | TxLog | $txID | $logID,0 | TopicLength | 0 | $value | 0 | $aux1 | $aux2 | +| $counter | true | TxLog | $txID | $logID,0 | DataLength | 0 | $value | 0 | $aux1 | $aux2 | +| | | | | | | | | | | | +| | | | | | *TxReceiptTag* | | | | | | +| $counter | false | TxReceipt | $txID | 0 | PostStateOrStatus | 0 | $value | 0 | $aux1 | $aux2 | +| $counter | false | TxReceipt | $txID | 0 | CumulativeGasUsed | 0 | $value | 0 | $aux1 | $aux2 | +| $counter | false | TxReceipt | $txID | 0 | LogLength | 0 | $value | 0 | $aux1 | $aux2 | ## `bytecode_table` diff --git a/specs/transactions-proof.md b/specs/transactions-proof.md index 01071454c..97f3456f8 100644 --- a/specs/transactions-proof.md +++ b/specs/transactions-proof.md @@ -243,4 +243,4 @@ The extended random linear combination gate requires one extra column in second ## Code -Please refer to `src/zkevm-specs/tx.py`. +Please refer to `src/zkevm-specs/tx_circuit.py`. From 2db6d0b5cc1fd1ee50dfcc846aec197aa2876e79 Mon Sep 17 00:00:00 2001 From: ashWhiteHat Date: Sat, 11 Feb 2023 13:19:01 +0900 Subject: [PATCH 5/9] update mpt proof --- specs/tables.md | 14 +++++++------- src/zkevm_specs/evm/table.py | 26 +++++++++++++------------- src/zkevm_specs/state_circuit.py | 17 +++++++++-------- 3 files changed, 29 insertions(+), 28 deletions(-) diff --git a/specs/tables.md b/specs/tables.md index 7a9c41759..205c477f2 100644 --- a/specs/tables.md +++ b/specs/tables.md @@ -211,13 +211,13 @@ The circuit can prove that updates to account nonces, balances, or storage slots | Address | ProofType | Key | ValuePrev | Value | RootPrev | Root | | ------- | ----------------------- | ---- | ------------- | ------------ | --------- | ----- | -| $addr | NonceMod | 0 | $noncePrev | $nonceCur | $rootPrev | $root | -| $addr | BalanceMod | 0 | $balancePrev | $balanceCur | $rootPrev | $root | -| $addr | CodeHashMod | 0 | $codeHashPrev | $codeHashCur | $rootPrev | $root | -| $addr | NonExistingAccountProof | 0 | 0 | 0 | $root | $root | -| $addr | AccountDeleteMod | 0 | 0 | 0 | $rootPrev | $root | -| $addr | StorageMod | $key | $valuePrev | $value | $rootPrev | $root | -| $addr | NonExistingStorageProof | $key | 0 | 0 | $root | $root | +| $addr | NonceChanged | 0 | $noncePrev | $nonceCur | $rootPrev | $root | +| $addr | BalanceChanged | 0 | $balancePrev | $balanceCur | $rootPrev | $root | +| $addr | CodeHashExists | 0 | $codeHashPrev | $codeHashCur | $rootPrev | $root | +| $addr | AccountDoesNotExist | 0 | 0 | 0 | $root | $root | +| $addr | AccountDestructed | 0 | 0 | 0 | $rootPrev | $root | +| $addr | StorageChanged | $key | $valuePrev | $value | $rootPrev | $root | +| $addr | StorageDoesNotExist | $key | 0 | 0 | $root | $root | ## `Keccak Table` diff --git a/src/zkevm_specs/evm/table.py b/src/zkevm_specs/evm/table.py index 58ffbafc1..b207c25de 100644 --- a/src/zkevm_specs/evm/table.py +++ b/src/zkevm_specs/evm/table.py @@ -317,29 +317,29 @@ class CopyDataTypeTag(IntEnum): RlcAcc = auto() -class MPTProofType(IntEnum): +class ProofType(IntEnum): """ Tag for MPT lookup. """ - NonceMod = 1 - BalanceMod = 2 - CodeHashMod = 3 - NonExistingAccountProof = 4 - AccountDeleteMod = 5 - StorageMod = 6 - NonExistingStorageProof = 7 + NonceChanged = 1 + BalanceChanged = 2 + CodeHashExists = 3 + AccountDoesNotExist = 4 + AccountDestructed = 5 + StorageChanged = 6 + StorageDoesNotExist = 7 @staticmethod - def from_account_field_tag(field_tag: AccountFieldTag) -> MPTProofType: + def from_account_field_tag(field_tag: AccountFieldTag) -> ProofType: if field_tag == AccountFieldTag.Nonce: - return MPTProofType.NonceMod + return ProofType.NonceChanged if field_tag == AccountFieldTag.Balance: - return MPTProofType.BalanceMod + return ProofType.BalanceChanged elif field_tag == AccountFieldTag.CodeHash: - return MPTProofType.CodeHashMod + return ProofType.CodeHashExists elif field_tag == AccountFieldTag.NonExisting: - return MPTProofType.NonExistingAccountProof + return ProofType.AccountDoesNotExist raise Exception("Unexpected AccountFieldTag value") diff --git a/src/zkevm_specs/state_circuit.py b/src/zkevm_specs/state_circuit.py index 731d51264..82008d0b7 100644 --- a/src/zkevm_specs/state_circuit.py +++ b/src/zkevm_specs/state_circuit.py @@ -2,7 +2,7 @@ from enum import IntEnum from math import log, ceil -from zkevm_specs.evm.table import MPTProofType +from zkevm_specs.evm.table import ProofType from .util import FQ, RLC, U160, U256, Expression, linear_combine_bytes from .encoding import U8, is_circuit_code @@ -261,14 +261,16 @@ def check_storage(row: Row, row_prev: Row, row_next: Row, tables: Tables): # 4.1. value = 0 means the leaf doesn't exist. 0->0 # transition requires a non-existing proof. + mpt_proof_type = ProofType.StorageDoesNotExist is_non_exist = FQ(row.value.expr() == FQ(0)) * FQ(row.initial_value.expr() == FQ(0)) + mpt_proof_type == is_non_exist * ProofType.StorageDoesNotExist # 4.2. MPT lookup for last access to (address, storage_key) if not all_keys_eq(row, row_next): tables.mpt_lookup( row.address(), - is_non_exist * FQ(MPTProofType.NonExistingStorageProof) - + (1 - is_non_exist) * FQ(MPTProofType.StorageMod), + is_non_exist * FQ(ProofType.AccountDoesNotExist) + + (1 - is_non_exist) * FQ(ProofType.StorageChanged), row.storage_key(), row.value, row.initial_value, @@ -302,7 +304,7 @@ def check_account(row: Row, row_prev: Row, row_next: Row, tables: Tables): get_addr = lambda row: row.address() field_tag = row.field_tag() - proof_type = MPTProofType.from_account_field_tag(field_tag) + proof_type = ProofType.from_account_field_tag(field_tag) # 6.0. Unused keys are 0 assert row.id() == 0 @@ -320,8 +322,7 @@ def check_account(row: Row, row_prev: Row, row_next: Row, tables: Tables): if not all_keys_eq(row, row_next): tables.mpt_lookup( get_addr(row), - is_non_exist * FQ(MPTProofType.NonExistingAccountProof) - + (1 - is_non_exist) * FQ(proof_type), + is_non_exist * FQ(ProofType.AccountDoesNotExist) + (1 - is_non_exist) * FQ(proof_type), row.storage_key(), row.value, row.initial_value, @@ -852,9 +853,9 @@ def _mock_mpt_updates(ops: List[Operation], randomness: FQ) -> Dict[Tuple[FQ, FQ continue field_tag = op.field_tag - proof_type = MPTProofType.StorageMod # type warning if None + proof_type = ProofType.StorageChanged # type warning if None if isinstance(field_tag, AccountFieldTag): - proof_type = MPTProofType.from_account_field_tag(field_tag) + proof_type = ProofType.from_account_field_tag(field_tag) new_root = root + 5 if isinstance(op, StartOp): From 07d3abbacb6e6aef8f9c82208dd55d17bad53db6 Mon Sep 17 00:00:00 2001 From: ashWhiteHat Date: Mon, 20 Feb 2023 17:28:51 +0900 Subject: [PATCH 6/9] update constraint description --- specs/state-proof.md | 3 +-- src/zkevm_specs/state_circuit.py | 8 ++------ 2 files changed, 3 insertions(+), 8 deletions(-) diff --git a/specs/state-proof.md b/specs/state-proof.md index 28ee9894a..ff60d7f39 100644 --- a/specs/state-proof.md +++ b/specs/state-proof.md @@ -70,8 +70,7 @@ to not be in the table. ### Storage 4.0. `storage_key` is 0 -4.1. non-existing proof if value is 0 -4.2. mpt_update exists in mpt circuit for AccountStorage last access +4.1. mpt_update exists in mpt circuit for AccountStorage last access ### Tx Refund diff --git a/src/zkevm_specs/state_circuit.py b/src/zkevm_specs/state_circuit.py index 82008d0b7..96ac7a401 100644 --- a/src/zkevm_specs/state_circuit.py +++ b/src/zkevm_specs/state_circuit.py @@ -259,13 +259,9 @@ def check_storage(row: Row, row_prev: Row, row_next: Row, tables: Tables): # 4.0. Unused keys are 0 assert row.field_tag() == 0 - # 4.1. value = 0 means the leaf doesn't exist. 0->0 - # transition requires a non-existing proof. - mpt_proof_type = ProofType.StorageDoesNotExist + # 4.1. MPT lookup for last access to (address, storage_key) + # value = 0 means the leaf doesn't exist and this needs for non-existing proof is_non_exist = FQ(row.value.expr() == FQ(0)) * FQ(row.initial_value.expr() == FQ(0)) - mpt_proof_type == is_non_exist * ProofType.StorageDoesNotExist - - # 4.2. MPT lookup for last access to (address, storage_key) if not all_keys_eq(row, row_next): tables.mpt_lookup( row.address(), From 68e8e0e228eaf99c1c9cac04526c04fa6323e713 Mon Sep 17 00:00:00 2001 From: ashWhiteHat Date: Sat, 25 Feb 2023 10:49:07 +0900 Subject: [PATCH 7/9] Update src/zkevm_specs/state_circuit.py MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Carlos Pérez <37264926+CPerezz@users.noreply.github.com> --- src/zkevm_specs/state_circuit.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/zkevm_specs/state_circuit.py b/src/zkevm_specs/state_circuit.py index 96ac7a401..a9d5a108c 100644 --- a/src/zkevm_specs/state_circuit.py +++ b/src/zkevm_specs/state_circuit.py @@ -260,7 +260,7 @@ def check_storage(row: Row, row_prev: Row, row_next: Row, tables: Tables): assert row.field_tag() == 0 # 4.1. MPT lookup for last access to (address, storage_key) - # value = 0 means the leaf doesn't exist and this needs for non-existing proof + # value = 0 means that the leaf doesn't exist. And this is needed by the non-existing proof. is_non_exist = FQ(row.value.expr() == FQ(0)) * FQ(row.initial_value.expr() == FQ(0)) if not all_keys_eq(row, row_next): tables.mpt_lookup( From c97428c4f1cec031fb31c1d476b46e68bcaba893 Mon Sep 17 00:00:00 2001 From: ashWhiteHat Date: Tue, 28 Feb 2023 19:41:49 +0900 Subject: [PATCH 8/9] Apply suggestions from @ed255's code review --- specs/tables.md | 16 ++++++++-------- src/zkevm_specs/evm/table.py | 26 +++++++++++++------------- src/zkevm_specs/state_circuit.py | 14 +++++++------- 3 files changed, 28 insertions(+), 28 deletions(-) diff --git a/specs/tables.md b/specs/tables.md index 205c477f2..a54cce52d 100644 --- a/specs/tables.md +++ b/specs/tables.md @@ -209,15 +209,15 @@ From this table, the following columns contain values using the RLC encoding: The circuit can prove that updates to account nonces, balances, or storage slots are correct, or that an account's code hash is some particular value. Note that it is not possible to change the code hash for an account without deleting it and then recreating it. -| Address | ProofType | Key | ValuePrev | Value | RootPrev | Root | +| Address | MPTProofType | Key | ValuePrev | Value | RootPrev | Root | | ------- | ----------------------- | ---- | ------------- | ------------ | --------- | ----- | -| $addr | NonceChanged | 0 | $noncePrev | $nonceCur | $rootPrev | $root | -| $addr | BalanceChanged | 0 | $balancePrev | $balanceCur | $rootPrev | $root | -| $addr | CodeHashExists | 0 | $codeHashPrev | $codeHashCur | $rootPrev | $root | -| $addr | AccountDoesNotExist | 0 | 0 | 0 | $root | $root | -| $addr | AccountDestructed | 0 | 0 | 0 | $rootPrev | $root | -| $addr | StorageChanged | $key | $valuePrev | $value | $rootPrev | $root | -| $addr | StorageDoesNotExist | $key | 0 | 0 | $root | $root | +| $addr | NonceMod | 0 | $noncePrev | $nonceCur | $rootPrev | $root | +| $addr | BalanceMod | 0 | $balancePrev | $balanceCur | $rootPrev | $root | +| $addr | CodeHashMod | 0 | $codeHashPrev | $codeHashCur | $rootPrev | $root | +| $addr | NonExistingAccountProof | 0 | 0 | 0 | $root | $root | +| $addr | AccountDeleteMod | 0 | 0 | 0 | $rootPrev | $root | +| $addr | StorageMod | $key | $valuePrev | $value | $rootPrev | $root | +| $addr | NonExistingStorageProof | $key | 0 | 0 | $root | $root | ## `Keccak Table` diff --git a/src/zkevm_specs/evm/table.py b/src/zkevm_specs/evm/table.py index b207c25de..58ffbafc1 100644 --- a/src/zkevm_specs/evm/table.py +++ b/src/zkevm_specs/evm/table.py @@ -317,29 +317,29 @@ class CopyDataTypeTag(IntEnum): RlcAcc = auto() -class ProofType(IntEnum): +class MPTProofType(IntEnum): """ Tag for MPT lookup. """ - NonceChanged = 1 - BalanceChanged = 2 - CodeHashExists = 3 - AccountDoesNotExist = 4 - AccountDestructed = 5 - StorageChanged = 6 - StorageDoesNotExist = 7 + NonceMod = 1 + BalanceMod = 2 + CodeHashMod = 3 + NonExistingAccountProof = 4 + AccountDeleteMod = 5 + StorageMod = 6 + NonExistingStorageProof = 7 @staticmethod - def from_account_field_tag(field_tag: AccountFieldTag) -> ProofType: + def from_account_field_tag(field_tag: AccountFieldTag) -> MPTProofType: if field_tag == AccountFieldTag.Nonce: - return ProofType.NonceChanged + return MPTProofType.NonceMod if field_tag == AccountFieldTag.Balance: - return ProofType.BalanceChanged + return MPTProofType.BalanceMod elif field_tag == AccountFieldTag.CodeHash: - return ProofType.CodeHashExists + return MPTProofType.CodeHashMod elif field_tag == AccountFieldTag.NonExisting: - return ProofType.AccountDoesNotExist + return MPTProofType.NonExistingAccountProof raise Exception("Unexpected AccountFieldTag value") diff --git a/src/zkevm_specs/state_circuit.py b/src/zkevm_specs/state_circuit.py index 96ac7a401..8ceaa4bb5 100644 --- a/src/zkevm_specs/state_circuit.py +++ b/src/zkevm_specs/state_circuit.py @@ -2,7 +2,7 @@ from enum import IntEnum from math import log, ceil -from zkevm_specs.evm.table import ProofType +from zkevm_specs.evm.table import MPTProofType from .util import FQ, RLC, U160, U256, Expression, linear_combine_bytes from .encoding import U8, is_circuit_code @@ -265,8 +265,8 @@ def check_storage(row: Row, row_prev: Row, row_next: Row, tables: Tables): if not all_keys_eq(row, row_next): tables.mpt_lookup( row.address(), - is_non_exist * FQ(ProofType.AccountDoesNotExist) - + (1 - is_non_exist) * FQ(ProofType.StorageChanged), + is_non_exist * FQ(MPTProofType.NonExistingAccountProof) + + (1 - is_non_exist) * FQ(MPTProofType.StorageMod), row.storage_key(), row.value, row.initial_value, @@ -300,7 +300,7 @@ def check_account(row: Row, row_prev: Row, row_next: Row, tables: Tables): get_addr = lambda row: row.address() field_tag = row.field_tag() - proof_type = ProofType.from_account_field_tag(field_tag) + proof_type = MPTProofType.from_account_field_tag(field_tag) # 6.0. Unused keys are 0 assert row.id() == 0 @@ -318,7 +318,7 @@ def check_account(row: Row, row_prev: Row, row_next: Row, tables: Tables): if not all_keys_eq(row, row_next): tables.mpt_lookup( get_addr(row), - is_non_exist * FQ(ProofType.AccountDoesNotExist) + (1 - is_non_exist) * FQ(proof_type), + is_non_exist * FQ(MPTProofType.NonExistingAccountProof) + (1 - is_non_exist) * FQ(proof_type), row.storage_key(), row.value, row.initial_value, @@ -849,9 +849,9 @@ def _mock_mpt_updates(ops: List[Operation], randomness: FQ) -> Dict[Tuple[FQ, FQ continue field_tag = op.field_tag - proof_type = ProofType.StorageChanged # type warning if None + proof_type = MPTProofType.StorageMod # type warning if None if isinstance(field_tag, AccountFieldTag): - proof_type = ProofType.from_account_field_tag(field_tag) + proof_type = MPTProofType.from_account_field_tag(field_tag) new_root = root + 5 if isinstance(op, StartOp): From 7b28695214f78118b837764dd6d272ca6a08bfc6 Mon Sep 17 00:00:00 2001 From: ashWhiteHat Date: Tue, 28 Feb 2023 19:44:05 +0900 Subject: [PATCH 9/9] fix lint --- src/zkevm_specs/state_circuit.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/zkevm_specs/state_circuit.py b/src/zkevm_specs/state_circuit.py index 67f211f55..99c8a335b 100644 --- a/src/zkevm_specs/state_circuit.py +++ b/src/zkevm_specs/state_circuit.py @@ -318,7 +318,8 @@ def check_account(row: Row, row_prev: Row, row_next: Row, tables: Tables): if not all_keys_eq(row, row_next): tables.mpt_lookup( get_addr(row), - is_non_exist * FQ(MPTProofType.NonExistingAccountProof) + (1 - is_non_exist) * FQ(proof_type), + is_non_exist * FQ(MPTProofType.NonExistingAccountProof) + + (1 - is_non_exist) * FQ(proof_type), row.storage_key(), row.value, row.initial_value,