add SLOAD & SSTORE spec

specs/opcode/54SLOAD_55SSTORE.md

@@ -0,0 +1,95 @@
+# SLOAD & SSTORE op code
+
+## Variables definition
+
+| Name | Value |
+| - | - |
+| COLD_SLOAD_COST | 2100 |
+| WARM_STORAGE_READ_COST | 100 |
+| SLOAD_GAS | 100 |
+| SSTORE_SET_GAS | 20000 |
+| SSTORE_RESET_GAS | 2900 |
+| SSTORE_CLEARS_SCHEDULE | 15000 |
+
+## Constraints
+
+1. opcodeId checks
+   1. opId === OpcodeId(0x54) for `SLOAD`
+   2. opId === OpcodeId(0x55) for `SSTORE`
+2. state transition:
+   - gc
+     - `SLOAD`: +5 (2 stack operations + 1 storage reads + 2 access_list reads/writes)
+     - `SSTORE`: +9 if persistent, +8 otherwise
+       + 2 stack operations
+       + 1 original value read
+       + 2 storage reads/writes
+       + 2 access_list reads/writes
+       + 2 gas_refund reads/writes if persistent, 1 otherwise
+         * 1 gas_refund read
+         * 1 gas_refund write if persistent 
+   - stack_pointer
+     - `SLOAD`: remains the same
+     - `SSTORE`: -2
+   - pc + 1
+   - state_write_counter
+       - `SLOAD`: +1
+       - `SSTORE`: +2
+   - gas:
+     - `SLOAD`:
+       + the accessed address is warm: gas + WARM_STORAGE_READ_COST
+       + the accessed address is cold: gas + COLD_SLOAD_COST
+     - `SSTORE`:
+       + the accessed address is warm:
+         * `current_value == new_value`: gas + SLOAD_GAS
+         * `current_value != new_value`:
+           - `original_value == current_value`:
+             - `original_value == 0`: gas + SSTORE_SET_GAS
+             - `original_value != 0`: gas + SSTORE_RESET_GAS
+           - `original_value != current_value`: gas + SLOAD_GAS
+       + the accessed address is cold:
+         * `current_value == new_value`: gas + SLOAD_GAS + COLD_SLOAD_COST
+         * `current_value != new_value`:
+           - `original_value == current_value`:
+             - `original_value == 0`: gas + SSTORE_SET_GAS + COLD_SLOAD_COST
+             - `original_value != 0`: gas + SSTORE_RESET_GAS + COLD_SLOAD_COST
+           - `original_value != current_value`: gas + SLOAD_GAS + COLD_SLOAD_COST
+   * gas_refund:
+     - `SSTORE`:
+       + `current_value != new_value`:
+         * `original_value == current_value`:
+           * `original_value != 0` && `new_value == 0`: gas_refund + SSTORE_CLEARS_SCHEDULE
+         * `original_value != current_value`:
+           * `original_value != 0`:
+             - `current_value == 0`: gas_refund - SSTORE_CLEARS_SCHEDULE
+             - `new_value == 0`: gas_refund + SSTORE_CLEARS_SCHEDULE
+           * `original_value == new_value`:
+             - `original_value == 0`: gas_refund + SSTORE_SET_GAS - SLOAD_GAS
+             - `original_value != 0`: gas_refund + SSTORE_RESET_GAS - SLOAD_GAS
+3. lookups:
+   - `SLOAD`: 5 busmapping lookups
+     - stack:
+       - `address` is popped off the top of the stack
+       - `value` is pushed on top of the stack
+     - storage: The 32 bytes of `value` are read from storage at `address`
+     - access_list: Whether the address is warm (accessed before), mark as warm afterward
+   - `SSTORE`: 9 busmapping lookups if persist, 8 otherwise
+     - stack:
+       - `address` is popped off the top of the stack
+       - `value` is popped off the top of the stack
+     - storage:
+       - Read the orignal value at `address`
+       - Read the current value at `address`
+       - The 32 bytes of new `value` are written to storage at `address`
+     - access_list: Whether the address is warm (accessed before), mark as warm afterward
+     - gas_refund:
+       + Read the accumulated gas_refund for this tx
+       + If persist, write the new accumulated gas_refund for this tx
+
+## Exceptions
+
+1. gas out: remaining gas is not enough
+2. stack underflow:
+   - the stack is empty: `1024 == stack_pointer`
+   - only for `SSTORE`: contains a single value: `1023 == stack_pointer`
+3. context error
+   - only for `SSTORE`: the current execution context is from a `STATICCALL` (since Byzantium fork).

src/zkevm_specs/evm/execution/__init__.py

@@ -6,5 +6,7 @@
 from .jump import *
 from .jumpi import *
 from .block_coinbase import *
+from .storage import *
+from .gas import *
 
 # Error cases

src/zkevm_specs/evm/execution/gas.py

@@ -0,0 +1,6 @@
+COLD_SLOAD_COST = 2100
+WARM_STORAGE_READ_COST = 100
+SLOAD_GAS = 100
+SSTORE_SET_GAS = 20000
+SSTORE_RESET_GAS = 2900
+SSTORE_CLEARS_SCHEDULE = 15000

src/zkevm_specs/evm/execution/storage.py

@@ -0,0 +1,105 @@
+from ..instruction import Instruction, Transition
+from ..opcode import Opcode
+from ..table import CallContextFieldTag, TxContextFieldTag
+from .gas import (
+    COLD_SLOAD_COST,
+    WARM_STORAGE_READ_COST,
+    SLOAD_GAS,
+    SSTORE_SET_GAS,
+    SSTORE_RESET_GAS,
+    SSTORE_CLEARS_SCHEDULE,
+)
+
+def sload(instruction: Instruction):
+    opcode = instruction.opcode_lookup(True)
+    instruction.constrain_equal(opcode, Opcode.SLOAD)
+
+    tx_id = instruction.call_context_lookup(CallContextFieldTag.TxId)
+    rw_counter_end_of_reversion = instruction.call_context_lookup(CallContextFieldTag.RWCounterEndOfReversion)
+    is_persistent = instruction.call_context_lookup(CallContextFieldTag.IsPersistent)
+    callee_address = instruction.tx_lookup(tx_id, TxContextFieldTag.CalleeAddress)
+
+    storage_slot = instruction.stack_pop()
+    warm = instruction.access_list_storage_slot_read(tx_id, callee_address, storage_slot)
+
+    # TODO: Use intrinsic gas (EIP 2028, 2930)
+    dynamic_gas_cost = WARM_STORAGE_READ_COST if warm else COLD_SLOAD_COST
+
+    instruction.storage_slot_read(callee_address, storage_slot)
+    instruction.add_storage_slot_to_access_list_with_reversion(
+        tx_id, callee_address, storage_slot, is_persistent, rw_counter_end_of_reversion
+    )
+    instruction.stack_push()
+
+    instruction.constrain_same_context_state_transition(
+        opcode,
+        rw_counter=Transition.delta(5),
+        program_counter=Transition.delta(1),
+        stack_pointer=Transition.delta(0),
+        state_write_counter=Transition.delta(1),
+        dynamic_gas_cost=dynamic_gas_cost,
+    )
+
+
+def sstore(instruction: Instruction):
+    opcode = instruction.opcode_lookup(True)
+    instruction.constrain_equal(opcode, Opcode.SSTORE)
+
+    tx_id = instruction.call_context_lookup(CallContextFieldTag.TxId)
+    rw_counter_end_of_reversion = instruction.call_context_lookup(CallContextFieldTag.RWCounterEndOfReversion)
+    is_persistent = instruction.call_context_lookup(CallContextFieldTag.IsPersistent)
+    callee_address = instruction.tx_lookup(tx_id, TxContextFieldTag.CalleeAddress)
+
+    storage_slot = instruction.stack_pop()
+    new_value = instruction.stack_pop()
+    warm = instruction.access_list_storage_slot_read(tx_id, callee_address, storage_slot)
+    original_value = instruction.storage_slot_original_value_read(tx_id, callee_address, storage_slot)
+    current_value, _ = instruction.storage_slot_read(callee_address, storage_slot)
+
+    # TODO: Use intrinsic gas (EIP 2028, 2930)
+    if current_value == new_value:
+        dynamic_gas_cost = SLOAD_GAS
+    else:
+        if original_value == current_value:
+            if original_value == 0:
+                dynamic_gas_cost = SSTORE_SET_GAS
+            else:
+                dynamic_gas_cost = SSTORE_RESET_GAS
+        else:
+            dynamic_gas_cost = SLOAD_GAS
+    if not warm:
+        dynamic_gas_cost = dynamic_gas_cost + COLD_SLOAD_COST
+
+    gas_refund = instruction.gas_refund_read(tx_id)
+    if current_value != new_value:
+        if original_value == current_value:
+            if original_value != 0 and new_value == 0:
+                gas_refund = gas_refund + SSTORE_CLEARS_SCHEDULE
+        else:
+            if original_value != 0:
+                if current_value == 0:
+                    gas_refund = gas_refund - SSTORE_CLEARS_SCHEDULE
+                if new_value == 0:
+                    gas_refund = gas_refund + SSTORE_CLEARS_SCHEDULE
+            if original_value == new_value:
+                if original_value == 0:
+                    gas_refund = gas_refund + SSTORE_SET_GAS - SLOAD_GAS
+                else:
+                    gas_refund = gas_refund + SSTORE_RESET_GAS - SLOAD_GAS
+
+    instruction.storage_slot_write_with_reversion(
+        callee_address, storage_slot, is_persistent, rw_counter_end_of_reversion
+    )
+    instruction.add_storage_slot_to_access_list_with_reversion(
+        tx_id, callee_address, storage_slot, is_persistent, rw_counter_end_of_reversion
+    )
+    instruction.gas_refund_write_only_persistent(tx_id, is_persistent)
+
+    instruction.constrain_same_context_state_transition(
+        opcode,
+        rw_counter=Transition.delta(9) if is_persistent else Transition.delta(8),
+        program_counter=Transition.delta(1),
+        stack_pointer=Transition.delta(2),
+        state_write_counter=Transition.delta(2),
+        dynamic_gas_cost=dynamic_gas_cost,
+    )

src/zkevm_specs/evm/instruction.py

@@ -145,6 +145,7 @@ def constrain_same_context_state_transition(
         stack_pointer: Transition = Transition.persistent(),
         memory_size: Transition = Transition.persistent(),
         dynamic_gas_cost: int = 0,
+        state_write_counter: Transition = Transition.persistent(),
     ):
         gas_cost = Opcode(opcode).constant_gas_cost() + dynamic_gas_cost
 
@@ -155,6 +156,7 @@ def constrain_same_context_state_transition(
             stack_pointer=stack_pointer,
             memory_size=memory_size,
             gas_left=Transition.delta(-gas_cost),
+            state_write_counter=state_write_counter,
         )
 
     def is_zero(self, value: int) -> bool:
@@ -303,7 +305,7 @@ def state_write_with_reversion(
             elif tag == RWTableTag.Account:
                 inputs[2], inputs[3] = inputs[3], inputs[2]
             elif tag == RWTableTag.AccountStorage:
-                inputs[3], inputs[4] = inputs[4], inputs[3]
+                inputs[2], inputs[3] = inputs[3], inputs[2]
             self.rw_lookup(RW.Write, tag, inputs, rw_counter=rw_counter)
 
         return row
@@ -425,14 +427,66 @@ def add_account_to_access_list_with_reversion(
         )
         return row[5] - row[6]
 
+    def storage_slot_write(
+        self,
+        account_address: int,
+        storage_slot: int,
+    ) -> Tuple[int, int]:
+        row = self.rw_lookup(
+            RW.Write,
+            RWTableTag.AccountStorage,
+            [account_address, storage_slot],
+        )
+        return row[5], row[6]
+
+    def storage_slot_write_with_reversion(
+        self,
+        account_address: int,
+        storage_slot: int,
+        is_persistent: bool = True,
+        rw_counter_end_of_reversion: int = 0,
+    ) -> Tuple[int, int]:
+        row = self.state_write_with_reversion(
+            RWTableTag.AccountStorage,
+            [account_address, storage_slot],
+            is_persistent,
+            rw_counter_end_of_reversion,
+        )
+        return row[5], row[6]
+
+    def storage_slot_read(
+        self,
+        account_address: int,
+        storage_slot: int,
+    ) -> Tuple[int, int]:
+        row = self.rw_lookup(
+            RW.Read,
+            RWTableTag.AccountStorage,
+            [account_address, storage_slot],
+        )
+        return row[5], row[6]
+
+    def storage_slot_original_value_read(
+        self,
+        tx_id: int,
+        account_address: int,
+        storage_slot: int,
+    ) -> int:
+        row = self.rw_lookup(
+            RW.Read,
+            RWTableTag.TxStorageSlotOriginalValue,
+            [tx_id, account_address, storage_slot],
+        )
+        return row[6]
+
     def add_storage_slot_to_access_list(
         self,
         tx_id: int,
         account_address: int,
         storage_slot: int,
     ) -> bool:
         row = self.state_write_with_reversion(
-            RWTableTag.TxAccessListAccount,
+            RWTableTag.TxAccessListStorageSlot,
             [tx_id, account_address, storage_slot, 1],
         )
         return row[6] - row[7]
@@ -446,13 +500,49 @@ def add_storage_slot_to_access_list_with_reversion(
         rw_counter_end_of_reversion: int,
     ) -> bool:
         row = self.state_write_with_reversion(
-            RWTableTag.TxAccessListAccount,
+            RWTableTag.TxAccessListStorageSlot,
             [tx_id, account_address, storage_slot, 1],
             is_persistent,
             rw_counter_end_of_reversion,
         )
         return row[6] - row[7]
 
+    def access_list_storage_slot_read(
+        self,
+        tx_id: int,
+        account_address: int,
+        storage_slot: int,
+    ) -> bool:
+        row = self.rw_lookup(
+            RW.Read,
+            RWTableTag.TxAccessListStorageSlot,
+            [tx_id, account_address, storage_slot],
+        )
+        return row[6]
+
+    def gas_refund_read(
+        self,
+        tx_id: int,
+    ) -> int:
+        row = self.rw_lookup(
+            RW.Read,
+            RWTableTag.TxRefund,
+            [tx_id],
+        )
+        return row[4]
+
+    def gas_refund_write_only_persistent(
+        self,
+        tx_id: int,
+        is_persistent: bool,
+    ) -> int:
+        row = self.state_write_only_persistent(
+            RWTableTag.TxRefund,
+            [tx_id],
+            is_persistent,
+        )
+        return row[4]
+
     def transfer_with_gas_fee(
         self,
         sender_address: int,

src/zkevm_specs/evm/main.py

@@ -8,6 +8,8 @@
     jump,
     jumpi,
     coinbase,
+    sload,
+    sstore
 )
 from .execution_state import ExecutionState
 from .instruction import Instruction
@@ -51,6 +53,10 @@ def verify_step(
         jumpi(instruction)
     elif instruction.curr.execution_state == ExecutionState.COINBASE:
         coinbase(instruction)
+    elif instruction.curr.execution_state == ExecutionState.SLOAD:
+        sload(instruction)
+    elif instruction.curr.execution_state == ExecutionState.SSTORE:
+        sstore(instruction)
     # Error cases
     else:
         raise NotImplementedError

src/zkevm_specs/evm/table.py

@@ -90,6 +90,7 @@ class RWTableTag(IntEnum):
 
     TxAccessListAccount = auto()
     TxAccessListStorageSlot = auto()
+    TxStorageSlotOriginalValue = auto()
     TxRefund = auto()
 
     Account = auto()