start, memory, stack and storage, rw table synchronization

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`.

specs/state-proof.md

@@ -41,9 +41,44 @@ 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. 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`

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`.

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

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")
 
 

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,
 )

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
@@ -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
 
 
@@ -215,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
 
 
@@ -247,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
 
 
@@ -256,16 +259,14 @@ 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.
-    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)
+    # 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(
             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,
@@ -299,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 = 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
@@ -317,8 +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(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,
@@ -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 = 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):

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
 

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()