Use legacy transaction format and defer support of dynamic gas price

src/zkevm_specs/evm/execution/add.py

@@ -12,7 +12,7 @@ def add(instruction: Instruction):
     c = instruction.stack_push()
 
     instruction.constrain_equal(
-        instruction.add_word(instruction.select(is_sub, c, a), b)[0],
+        instruction.add_words([instruction.select(is_sub, c, a), b])[0],
         instruction.select(is_sub, a, c),
     )
 

src/zkevm_specs/evm/execution/begin_tx.py

@@ -26,23 +26,24 @@ def begin_tx(instruction: Instruction, is_first_step: bool = False):
     instruction.constrain_equal(tx_nonce, nonce_prev)
     instruction.constrain_equal(nonce, nonce_prev + 1)
 
-    # TODO: Implement EIP 1559 (currently this assumes gas_fee_cap <= basefee + gas_tip_cap)
+    # TODO: Implement EIP 1559 (currently it supports legacy transaction format)
     # Calculate gas fee
     tx_gas = instruction.tx_lookup(tx_id, TxContextFieldTag.Gas)
-    tx_gas_fee_cap = instruction.tx_lookup(tx_id, TxContextFieldTag.GasFeeCap)
-    gas_fee, carry = instruction.mul_word_by_u64(tx_gas_fee_cap, tx_gas)
+    tx_gas_price = instruction.tx_lookup(tx_id, TxContextFieldTag.GasPrice)
+    gas_fee, carry = instruction.mul_word_by_u64(tx_gas_price, tx_gas)
     instruction.constrain_zero(carry)
 
-    # TODO: Use intrinsic gas (EIP 2028, 2930)
-    gas_left = tx_gas - (53000 if tx_is_create else 21000)
-    instruction.int_to_bytes(gas_left, 8)
+    # TODO: Handle gas cost of tx level access list (EIP 2930)
+    tx_call_data_gas_cost = instruction.tx_lookup(tx_id, TxContextFieldTag.CallDataGasCost)
+    gas_left = tx_gas - (53000 if tx_is_create else 21000) - tx_call_data_gas_cost
+    instruction.constrain_gas_left_not_underflow(gas_left)
 
     # Prepare access list of caller and callee
     instruction.constrain_equal(instruction.add_account_to_access_list(tx_id, tx_caller_address), 1)
     instruction.constrain_equal(instruction.add_account_to_access_list(tx_id, tx_callee_address), 1)
 
     # Verify transfer
-    instruction.constrain_transfer(
+    instruction.transfer_with_gas_fee(
         tx_caller_address,
         tx_callee_address,
         tx_value,

src/zkevm_specs/evm/instruction.py

@@ -2,7 +2,7 @@
 from enum import IntEnum, auto
 from typing import Optional, Sequence, Tuple, Union
 
-from ..util import Array4, Array8, linear_combine, RLCStore, MAX_N_BYTES
+from ..util import Array4, Array8, linear_combine, RLCStore, MAX_N_BYTES, N_BYTES_GAS
 from .opcode import Opcode
 from .step import StepState
 from .table import (
@@ -74,32 +74,8 @@ def constrain_equal(self, lhs: int, rhs: int):
     def constrain_bool(self, value: int):
         assert value in [0, 1]
 
-    def constrain_transfer(
-        self,
-        sender_address: int,
-        receiver_address: int,
-        value: int,
-        gas_fee: int = 0,
-        is_persistent: bool = True,
-        rw_counter_end_of_reversion: int = 0,
-    ):
-        sender_balance, sender_balance_prev = self.account_write_with_reversion(
-            sender_address, AccountFieldTag.Balance, is_persistent, rw_counter_end_of_reversion
-        )
-        receiver_balance, receiver_balance_prev = self.account_write_with_reversion(
-            receiver_address, AccountFieldTag.Balance, is_persistent, rw_counter_end_of_reversion
-        )
-
-        value_with_gas_fee, overflow = self.add_word(value, gas_fee)
-        self.constrain_zero(overflow)
-
-        result, carry = self.add_word(value_with_gas_fee, sender_balance)
-        self.constrain_equal(sender_balance_prev, result)
-        self.constrain_zero(carry)
-
-        result, carry = self.add_word(value, receiver_balance_prev)
-        self.constrain_equal(receiver_balance, result)
-        self.constrain_zero(carry)
+    def constrain_gas_left_not_underflow(self, gas_left: int):
+        self.int_to_bytes(gas_left, N_BYTES_GAS)
 
     def constrain_state_transition(self, **kwargs: Transition):
         for key in [
@@ -172,8 +148,7 @@ def constrain_same_context_state_transition(
     ):
         gas_cost = Opcode(opcode).constant_gas_cost() + dynamic_gas_cost
 
-        self.int_to_bytes(self.curr.gas_left - gas_cost, 8)
-
+        self.constrain_gas_left_not_underflow(self.curr.gas_left - gas_cost)
         self.constrain_state_transition(
             rw_counter=rw_counter,
             program_counter=program_counter,
@@ -197,20 +172,30 @@ def select(self, condition: bool, when_true: int, when_false: int) -> int:
     def pair_select(self, value: int, lhs: int, rhs: int) -> Tuple[bool, bool]:
         return value == lhs, value == rhs
 
-    def add_word(self, a: int, b: int) -> Tuple[int, bool]:
-        a_bytes = self.rlc_to_bytes(a, 32)
-        b_bytes = self.rlc_to_bytes(b, 32)
+    def add_words(self, addends: Sequence[int]) -> Tuple[int, int]:
+        def rlc_to_lo_hi(rlc: int) -> Tuple[Sequence[int], Sequence[int]]:
+            bytes = self.rlc_to_bytes(rlc, 32)
+            return self.bytes_to_int(bytes[:16]), self.bytes_to_int(bytes[16:])
+
+        addends_lo, addends_hi = list(zip(*map(rlc_to_lo_hi, addends)))
+        carry_lo, sum_lo = divmod(sum(addends_lo), 1 << 128)
+        carry_hi, sum_hi = divmod(sum(addends_hi) + carry_lo, 1 << 128)
 
-        a_lo = self.bytes_to_int(a_bytes[:16])
-        a_hi = self.bytes_to_int(a_bytes[16:])
-        b_lo = self.bytes_to_int(b_bytes[:16])
-        b_hi = self.bytes_to_int(b_bytes[16:])
-        carry_lo, c_lo = divmod(a_lo + b_lo, 1 << 128)
-        carry_hi, c_hi = divmod(a_hi + b_hi + carry_lo, 1 << 128)
+        sum_bytes = sum_lo.to_bytes(16, "little") + sum_hi.to_bytes(16, "little")
 
-        c_bytes = c_lo.to_bytes(16, "little") + c_hi.to_bytes(16, "little")
+        return self.rlc_store.to_rlc(sum_bytes), carry_hi
 
-        return self.rlc_store.to_rlc(c_bytes), carry_hi
+    def sub_word(self, minuend: int, subtrahend: int) -> Tuple[int, bool]:
+        minuend_lo, minuend_hi = self.rlc_to_lo_hi(minuend)
+        subtrahend_lo, subtrahend_hi = self.rlc_to_lo_hi(subtrahend)
+        borrow_lo = minuend_lo < subtrahend_lo
+        diff_lo = minuend_lo - subtrahend_lo + (1 << 128 if borrow_lo else 0)
+        borrow_hi = minuend_hi < subtrahend_hi + borrow_lo
+        diff_hi = minuend_hi - subtrahend_hi - borrow_lo + (1 << 128 if borrow_hi else 0)
+
+        diff_bytes = diff_lo.to_bytes(16, "little") + diff_hi.to_bytes(16, "little")
+
+        return self.rlc_store.to_rlc(diff_bytes), borrow_hi
 
     def mul_word_by_u64(self, multiplicand: int, multiplier: int) -> Tuple[int, int]:
         multiplicand_bytes = self.rlc_to_bytes(multiplicand, 32)
@@ -260,6 +245,20 @@ def tx_lookup(self, tx_id: int, tag: TxContextFieldTag, index: int = 0) -> int:
     def bytecode_lookup(self, bytecode_hash: int, index: int, is_code: int) -> int:
         return self.tables.bytecode_lookup([bytecode_hash, index, Tables._, is_code])[2]
 
+    def opcode_lookup(self, is_code: bool) -> int:
+        index = self.curr.program_counter + self.program_counter_offset
+        self.program_counter_offset += 1
+
+        return self.opcode_lookup_at(index, is_code)
+
+    def opcode_lookup_at(self, index: int, is_code: bool) -> int:
+        if self.curr.is_root and self.curr.is_create:
+            raise NotImplementedError(
+                "The opcode source when is_root and is_create (root creation call) is not determined yet"
+            )
+        else:
+            return self.bytecode_lookup(self.curr.opcode_source, index, is_code)
+
     def rw_lookup(self, rw: RW, tag: RWTableTag, inputs: Sequence[int], rw_counter: Optional[int] = None) -> Array8:
         if rw_counter is None:
             rw_counter = self.curr.rw_counter + self.rw_counter_offset
@@ -271,7 +270,7 @@ def state_write_only_persistent(
         self,
         tag: RWTableTag,
         inputs: Sequence[int],
-        is_persistent: bool = True,
+        is_persistent: bool,
     ) -> Array8:
         assert tag.write_only_persistent()
 
@@ -284,8 +283,8 @@ def state_write_with_reversion(
         self,
         tag: RWTableTag,
         inputs: Sequence[int],
-        is_persistent: bool = True,
-        rw_counter_end_of_reversion: int = 0,
+        is_persistent: bool,
+        rw_counter_end_of_reversion: int,
     ) -> Array8:
         assert tag.write_with_reversion()
 
@@ -309,20 +308,6 @@ def state_write_with_reversion(
 
         return row
 
-    def opcode_lookup(self, is_code: bool) -> int:
-        index = self.curr.program_counter + self.program_counter_offset
-        self.program_counter_offset += 1
-
-        return self.opcode_lookup_at(index, is_code)
-
-    def opcode_lookup_at(self, index: int, is_code: bool) -> int:
-        if self.curr.is_root and self.curr.is_create:
-            raise NotImplementedError(
-                "The opcode source when is_root and is_create (root creation call) is not determined yet"
-            )
-        else:
-            return self.bytecode_lookup(self.curr.opcode_source, index, is_code)
-
     def call_context_lookup(self, tag: CallContextFieldTag, rw: RW = RW.Read, call_id: Union[int, None] = None) -> int:
         if call_id is None:
             call_id = self.curr.call_id
@@ -358,8 +343,8 @@ def account_write_with_reversion(
         self,
         account_address: int,
         account_field_tag: AccountFieldTag,
-        is_persistent: bool = True,
-        rw_counter_end_of_reversion: int = 0,
+        is_persistent: bool,
+        rw_counter_end_of_reversion: int,
     ) -> Tuple[int, int]:
         row = self.state_write_with_reversion(
             RWTableTag.Account,
@@ -369,6 +354,46 @@ def account_write_with_reversion(
         )
         return row[5], row[6]
 
+    def add_balance(self, account_address: int, values: Sequence[int]):
+        balance, balance_prev = self.account_write(account_address, AccountFieldTag.Balance)
+        result, carry = self.add_words([balance_prev, *values])
+        self.constrain_equal(balance, result)
+        self.constrain_zero(carry)
+
+    def add_balance_with_reversion(
+        self,
+        account_address: int,
+        values: Sequence[int],
+        is_persistent: bool,
+        rw_counter_end_of_reversion: int,
+    ):
+        balance, balance_prev = self.account_write_with_reversion(
+            account_address, AccountFieldTag.Balance, is_persistent, rw_counter_end_of_reversion
+        )
+        result, carry = self.add_words([balance_prev, *values])
+        self.constrain_equal(balance, result)
+        self.constrain_zero(carry)
+
+    def sub_balance(self, account_address: int, values: Sequence[int]):
+        balance, balance_prev = self.account_write(account_address, AccountFieldTag.Balance)
+        result, carry = self.add_words([balance, *values])
+        self.constrain_equal(balance_prev, result)
+        self.constrain_zero(carry)
+
+    def sub_balance_with_reversion(
+        self,
+        account_address: int,
+        values: Sequence[int],
+        is_persistent: bool,
+        rw_counter_end_of_reversion: int,
+    ):
+        balance, balance_prev = self.account_write_with_reversion(
+            account_address, AccountFieldTag.Balance, is_persistent, rw_counter_end_of_reversion
+        )
+        result, carry = self.add_words([balance, *values])
+        self.constrain_equal(balance_prev, result)
+        self.constrain_zero(carry)
+
     def account_read(self, account_address: int, account_field_tag: AccountFieldTag) -> Tuple[int, int]:
         row = self.rw_lookup(RW.Read, RWTableTag.Account, [account_address, account_field_tag])
         return row[5], row[6]
@@ -389,8 +414,8 @@ def add_account_to_access_list_with_reversion(
         self,
         tx_id: int,
         account_address: int,
-        is_persistent: bool = True,
-        rw_counter_end_of_reversion: int = 0,
+        is_persistent: bool,
+        rw_counter_end_of_reversion: int,
     ) -> bool:
         row = self.state_write_with_reversion(
             RWTableTag.TxAccessListAccount,
@@ -417,8 +442,8 @@ def add_storage_slot_to_access_list_with_reversion(
         tx_id: int,
         account_address: int,
         storage_slot: int,
-        is_persistent: bool = True,
-        rw_counter_end_of_reversion: int = 0,
+        is_persistent: bool,
+        rw_counter_end_of_reversion: int,
     ) -> bool:
         row = self.state_write_with_reversion(
             RWTableTag.TxAccessListAccount,
@@ -427,3 +452,25 @@ def add_storage_slot_to_access_list_with_reversion(
             rw_counter_end_of_reversion,
         )
         return row[6] - row[7]
+
+    def transfer_with_gas_fee(
+        self,
+        sender_address: int,
+        receiver_address: int,
+        value: int,
+        gas_fee: int,
+        is_persistent: bool,
+        rw_counter_end_of_reversion: int,
+    ):
+        self.sub_balance_with_reversion(
+            sender_address,
+            [value, gas_fee],
+            is_persistent,
+            rw_counter_end_of_reversion,
+        )
+        self.add_balance_with_reversion(
+            receiver_address,
+            [value],
+            is_persistent,
+            rw_counter_end_of_reversion,
+        )

src/zkevm_specs/evm/step.py

@@ -15,13 +15,14 @@ class StepState:
     rw_counter: int
     call_id: int
 
-    # The following 3 fields decide the source of opcode. There are 3 possible
+    # The following 3 fields decide the opcode source. There are 2 possible
     # cases:
-    # 1. Tx contract deployment (is_root and is_create)
-    #   We set opcode_source to tx_id and lookup call_data in tx_table.
-    # 2. CREATE and CREATE2 (not is_root and is_create)
-    #   We set opcode_source to caller_id and lookup memory in rw_table.
-    # 3. Contract execution (not is_create)
+    # 1. Root creation call (is_root and is_create)
+    #   It was planned to set the opcode_source to tx_id, then lookup tx_table's
+    #   CallData field directly, but is still yet to be determined.
+    #   See the issue https://github.com/appliedzkp/zkevm-specs/issues/73 for
+    #   further discussion.
+    # 2. Deployed contract interaction or internal creation call
     #   We set opcode_source to bytecode_hash and lookup bytecode_table.
     is_root: bool
     is_create: bool

src/zkevm_specs/evm/table.py

@@ -60,17 +60,19 @@ class TxContextFieldTag(IntEnum):
     """
     Tag for TxTable lookup, where the TxTable is an instance-column table where
     part of it will be built by verifier.
+    Note that the field here is targeting legacy transaction format, supporting
+    of EIP1559 is deferred to future work.
     """
 
     Nonce = auto()
     Gas = auto()
-    GasTipCap = auto()
-    GasFeeCap = auto()
+    GasPrice = auto()
     CallerAddress = auto()
     CalleeAddress = auto()
     IsCreate = auto()
     Value = auto()
     CallDataLength = auto()
+    CallDataGasCost = auto()
     CallData = auto()