add sload & sstore specs

specs/opcode/54SLOAD_55SSTORE.md

@@ -0,0 +1,104 @@
+# 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`: +8
+       - 4 call_context read
+       - 2 stack operations
+       - 1 storage reads
+       - 1 access_list write
+     - `SSTORE`: +9
+       - 4 call_context read
+       - 2 stack operations
+       - 1 storage reads/writes
+       - 1 access_list write
+       - 1 gas_refund writes
+   - stack_pointer
+     - `SLOAD`: remains the same
+     - `SSTORE`: -2
+   - pc + 1
+   - state_write_counter
+     - `SLOAD`: +1 (access_list)
+     - `SSTORE`: +3 (for storage, access_list & gas_refund respectively)
+   - gas:
+     - `SLOAD`:
+       - the accessed `key` is warm: gas + WARM_STORAGE_READ_COST
+       - the accessed `key` is cold: gas + COLD_SLOAD_COST
+     - `SSTORE`:
+       - the accessed `key` 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 `key` 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`: 8 busmapping lookups
+     - call_context:
+       - `tx_id`: Read the `tx_id` for this tx.
+       - `rw_counter_end_of_reversion`: Read the `rw_counter_end` if this tx get reverted.
+       - `is_persistent`: Read if this tx will be reverted.
+       - `callee_address`: Read the `callee_address` of this call.
+     - stack:
+       - `key` 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 `key`
+     - access_list: Write as `true` for `key`
+   - `SSTORE`: 9 busmapping lookups
+     - call_context:
+       - `tx_id`: Read the `tx_id` for this tx.
+       - `rw_counter_end_of_reversion`: Read the `rw_counter_end` if this tx get reverted.
+       - `is_persistent`: Read if this tx will be reverted.
+       - `callee_address`: Read the `callee_address` of this call.
+     - stack:
+       - `key` is popped off the top of the stack
+       - `value` is popped off the top of the stack
+     - storage:
+       - The 32 bytes of new `value` are written to storage at `key`, with the previous `value` and `committed_value`
+     - access_list: Write as `true` for `key`
+     - gas_refund:
+       - 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

@@ -16,11 +16,13 @@
 from .callvalue import *
 from .calldatacopy import *
 from .gas import *
-from .gasprice import *
 from .jump import *
 from .jumpi import *
 from .push import *
 from .slt_sgt import *
+from .gas import *
+from .gasprice import *
+from .storage import *
 from .selfbalance import *
 
 
@@ -41,6 +43,8 @@
     ExecutionState.PUSH: push,
     ExecutionState.SCMP: scmp,
     ExecutionState.GAS: gas,
+    ExecutionState.SLOAD: sload,
+    ExecutionState.SSTORE: sstore,
     ExecutionState.SELFBALANCE: selfbalance,
     ExecutionState.GASPRICE: gasprice,
 }

src/zkevm_specs/evm/execution/storage.py

@@ -0,0 +1,111 @@
+from ..instruction import Instruction, Transition
+from ..opcode import Opcode
+from ..table import CallContextFieldTag, TxContextFieldTag
+from ...util.param 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.call_context_lookup(CallContextFieldTag.CalleeAddress)
+
+    storage_key = instruction.stack_pop()
+
+    instruction.constrain_equal(
+        instruction.account_storage_read(callee_address, storage_key, tx_id),
+        instruction.stack_push(),
+    )
+
+    is_warm_new, is_warm = instruction.add_account_storage_to_access_list_with_reversion(
+        tx_id, callee_address, storage_key, is_persistent, rw_counter_end_of_reversion
+    )
+
+    dynamic_gas_cost = WARM_STORAGE_READ_COST if is_warm == 1 else COLD_SLOAD_COST
+
+    instruction.step_state_transition_in_same_context(
+        opcode,
+        rw_counter=Transition.delta(8),
+        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.call_context_lookup(CallContextFieldTag.CalleeAddress)
+
+    storage_key = instruction.stack_pop()
+    storage_value = instruction.stack_pop()
+    value, value_prev, original_value = instruction.account_storage_write_with_reversion(
+        callee_address, storage_key, tx_id, is_persistent, rw_counter_end_of_reversion
+    )
+    instruction.constrain_equal(storage_value, value)
+
+    is_warm_new, is_warm = instruction.add_account_storage_to_access_list_with_reversion(
+        tx_id, callee_address, storage_key, is_persistent, rw_counter_end_of_reversion
+    )
+
+    gas_refund, gas_refund_prev = instruction.tx_refund_write_with_reversion(
+        tx_id, is_persistent, rw_counter_end_of_reversion
+    )
+    gas_refund_new = gas_refund_prev
+    if value_prev != value:
+        if original_value == value_prev:
+            if original_value != 0 and value == 0:
+                gas_refund_new = gas_refund_new + SSTORE_CLEARS_SCHEDULE
+        else:
+            if original_value != 0:
+                if value_prev == 0:
+                    gas_refund_new = gas_refund_new - SSTORE_CLEARS_SCHEDULE
+                if value == 0:
+                    gas_refund_new = gas_refund_new + SSTORE_CLEARS_SCHEDULE
+            if original_value == value:
+                if original_value == 0:
+                    gas_refund_new = gas_refund_new + SSTORE_SET_GAS - SLOAD_GAS
+                else:
+                    gas_refund_new = gas_refund_new + SSTORE_RESET_GAS - SLOAD_GAS
+    instruction.constrain_equal(gas_refund, gas_refund_new)
+
+    if value_prev == value:
+        dynamic_gas_cost = SLOAD_GAS
+    else:
+        if original_value == value_prev:
+            if original_value == 0:
+                dynamic_gas_cost = SSTORE_SET_GAS
+            else:
+                dynamic_gas_cost = SSTORE_RESET_GAS
+        else:
+            dynamic_gas_cost = SLOAD_GAS
+    if is_warm == 0:
+        dynamic_gas_cost = dynamic_gas_cost + COLD_SLOAD_COST
+
+    instruction.step_state_transition_in_same_context(
+        opcode,
+        rw_counter=Transition.delta(9),
+        program_counter=Transition.delta(1),
+        stack_pointer=Transition.delta(2),
+        state_write_counter=Transition.delta(3),
+        dynamic_gas_cost=dynamic_gas_cost,
+    )

src/zkevm_specs/evm/instruction.py

@@ -410,7 +410,7 @@ def state_write_with_reversion(
 
     def call_context_lookup(
         self, field_tag: CallContextFieldTag, rw: RW = RW.Read, call_id: Optional[int] = None
-    ) -> Union[FQ, RLC]:
+    ) -> FQ:
         if call_id is None:
             call_id = self.curr.call_id
         return self.rw_lookup(rw, RWTableTag.CallContext, [call_id, field_tag])[-4]
@@ -440,6 +440,22 @@ def tx_refund_read(self, tx_id) -> FQ:
         row = self.rw_lookup(RW.Read, RWTableTag.TxRefund, [tx_id])
         return row[-4]
 
+    def tx_refund_write_with_reversion(
+        self,
+        tx_id: int,
+        is_persistent: bool,
+        rw_counter_end_of_reversion: int,
+        state_write_counter: Optional[int] = None,
+    ) -> Tuple[FQ, FQ]:
+        row = self.state_write_with_reversion(
+            RWTableTag.TxRefund,
+            [tx_id],
+            is_persistent,
+            rw_counter_end_of_reversion,
+            state_write_counter,
+        )
+        return row[-4], row[-3]
+
     def account_read(self, account_address: int, account_field_tag: AccountFieldTag) -> FQ:
         row = self.rw_lookup(RW.Read, RWTableTag.Account, [account_address, account_field_tag])
         return row[-4]
@@ -527,6 +543,32 @@ def sub_balance_with_reversion(
         self.constrain_zero(carry)
         return balance, balance_prev
 
+    def account_storage_read(self, account_address: int, storage_key: int, tx_id: int) -> FQ:
+        row = self.rw_lookup(
+            RW.Read,
+            RWTableTag.AccountStorage,
+            [account_address, storage_key, 0, Tables._, Tables._, tx_id],
+        )
+        return row[-4]
+
+    def account_storage_write_with_reversion(
+        self,
+        account_address: int,
+        storage_key: int,
+        tx_id: int,
+        is_persistent: bool,
+        rw_counter_end_of_reversion: int,
+        state_write_counter: Optional[int] = None,
+    ) -> Tuple[FQ, FQ, FQ]:
+        row = self.state_write_with_reversion(
+            RWTableTag.AccountStorage,
+            [account_address, storage_key, 0, Tables._, Tables._, tx_id],
+            is_persistent,
+            rw_counter_end_of_reversion,
+            state_write_counter,
+        )
+        return row[-4], row[-3], row[-1]
+
     def add_account_to_access_list(
         self,
         tx_id: int,
@@ -561,13 +603,13 @@ def add_account_storage_to_access_list(
         tx_id: int,
         account_address: int,
         storage_key: int,
-    ) -> bool:
+    ) -> Tuple[FQ, FQ]:
         row = self.rw_lookup(
             RW.Write,
             RWTableTag.TxAccessListAccountStorage,
             [tx_id, account_address, storage_key, 1],
         )
-        return row[-4] - row[-3]
+        return row[-4], row[-3]
 
     def add_account_storage_to_access_list_with_reversion(
         self,
@@ -577,15 +619,15 @@ def add_account_storage_to_access_list_with_reversion(
         is_persistent: bool,
         rw_counter_end_of_reversion: int,
         state_write_counter: Optional[int] = None,
-    ) -> bool:
+    ) -> Tuple[FQ, FQ]:
         row = self.state_write_with_reversion(
             RWTableTag.TxAccessListAccountStorage,
             [tx_id, account_address, storage_key, 1],
             is_persistent,
             rw_counter_end_of_reversion,
             state_write_counter,
         )
-        return row[-4] - row[-3]
+        return row[-4], row[-3]
 
     def transfer_with_gas_fee(
         self,
@@ -618,7 +660,7 @@ def transfer(
         is_persistent: bool,
         rw_counter_end_of_reversion: int,
         state_write_counter: Optional[int] = None,
-    ) -> Tuple[Tuple[int, int], Tuple[int, int]]:
+    ) -> Tuple[Tuple[FQ, FQ], Tuple[FQ, FQ]]:
         sender_balance_pair = self.sub_balance_with_reversion(
             sender_address,
             [value],

src/zkevm_specs/util/param.py

@@ -68,3 +68,11 @@
 MEMORY_EXPANSION_QUAD_DENOMINATOR = 512
 # Coefficient of linear part of memory expansion gas cost
 MEMORY_EXPANSION_LINEAR_COEFF = 3
+
+
+COLD_SLOAD_COST = 2100
+WARM_STORAGE_READ_COST = 100
+SLOAD_GAS = 100
+SSTORE_SET_GAS = 20000
+SSTORE_RESET_GAS = 2900
+SSTORE_CLEARS_SCHEDULE = 15000