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/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

@@ -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,15 +259,13 @@ 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)
+            is_non_exist * FQ(MPTProofType.NonExistingAccountProof)
             + (1 - is_non_exist) * FQ(MPTProofType.StorageMod),
             row.storage_key(),
             row.value,

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