diff --git a/src/zkevm_specs/evm/execution/begin_tx.py b/src/zkevm_specs/evm/execution/begin_tx.py index e852c6c0c..f12887ba6 100644 --- a/src/zkevm_specs/evm/execution/begin_tx.py +++ b/src/zkevm_specs/evm/execution/begin_tx.py @@ -113,4 +113,5 @@ def begin_tx(instruction: Instruction): code_source=Transition.to(code_hash), gas_left=Transition.to(gas_left), reversible_write_counter=Transition.to(2), + log_id=Transition.to(0), ) diff --git a/src/zkevm_specs/evm/execution/call.py b/src/zkevm_specs/evm/execution/call.py index a5a4eeb04..1327e410f 100644 --- a/src/zkevm_specs/evm/execution/call.py +++ b/src/zkevm_specs/evm/execution/call.py @@ -199,4 +199,5 @@ def call(instruction: Instruction): code_source=Transition.to(callee_code_hash), gas_left=Transition.to(callee_gas_left), reversible_write_counter=Transition.to(2), + log_id=Transition.same(), ) diff --git a/src/zkevm_specs/evm/execution/end_tx.py b/src/zkevm_specs/evm/execution/end_tx.py index 3d2b86628..823996403 100644 --- a/src/zkevm_specs/evm/execution/end_tx.py +++ b/src/zkevm_specs/evm/execution/end_tx.py @@ -1,11 +1,12 @@ from ...util import N_BYTES_GAS, MAX_REFUND_QUOTIENT_OF_GAS_USED, FQ, RLC, cast_expr from ..execution_state import ExecutionState from ..instruction import Instruction, Transition -from ..table import BlockContextFieldTag, CallContextFieldTag, TxContextFieldTag +from ..table import BlockContextFieldTag, CallContextFieldTag, TxContextFieldTag, TxReceiptFieldTag def end_tx(instruction: Instruction): tx_id = instruction.call_context_lookup(CallContextFieldTag.TxId) + is_persistent = instruction.call_context_lookup(CallContextFieldTag.IsPersistent) # Handle gas refund (refund is capped to gas_used // MAX_REFUND_QUOTIENT_OF_GAS_USED in EIP 3529) tx_gas = instruction.tx_context_lookup(tx_id, TxContextFieldTag.Gas) @@ -33,6 +34,29 @@ def end_tx(instruction: Instruction): coinbase = instruction.block_context_lookup(BlockContextFieldTag.Coinbase) instruction.add_balance(coinbase, [reward]) + # constrain tx status matches with `PostStateOrStatus` of TxReceipt tag in RW + instruction.constrain_equal( + is_persistent, instruction.tx_receipt_lookup(tx_id, TxReceiptFieldTag.PostStateOrStatus) + ) + + # constrain log id matches with `LogLength` of TxReceipt tag in RW + log_id = instruction.tx_receipt_lookup(tx_id, TxReceiptFieldTag.LogLength) + instruction.constrain_equal(log_id, instruction.curr.log_id) + + # constrain `CumulativeGasUsed` of TxReceipt tag in RW + is_first_tx = tx_id == 1 + if is_first_tx: # check if it is the first tx + current_cumulative_gas_used = FQ(0) + else: + current_cumulative_gas_used = instruction.tx_receipt_lookup( + tx_id - FQ(1), TxReceiptFieldTag.CumulativeGasUsed + ).expr() + + instruction.constrain_equal( + current_cumulative_gas_used + gas_used, + instruction.tx_receipt_lookup(tx_id, TxReceiptFieldTag.CumulativeGasUsed), + ) + # When to next transaction if instruction.next.execution_state == ExecutionState.BeginTx: # Check next tx_id is increased by 1 @@ -43,11 +67,11 @@ def end_tx(instruction: Instruction): tx_id.expr() + 1, ) # Do step state transition for rw_counter - instruction.constrain_step_state_transition(rw_counter=Transition.delta(5)) + instruction.constrain_step_state_transition(rw_counter=Transition.delta(10 - is_first_tx)) # When to end of block if instruction.next.execution_state == ExecutionState.EndBlock: # Do step state transition for rw_counter and call_id instruction.constrain_step_state_transition( - rw_counter=Transition.delta(4), call_id=Transition.same() + rw_counter=Transition.delta(9 - is_first_tx), call_id=Transition.same() ) diff --git a/src/zkevm_specs/evm/instruction.py b/src/zkevm_specs/evm/instruction.py index b822ed352..9ae39bea8 100644 --- a/src/zkevm_specs/evm/instruction.py +++ b/src/zkevm_specs/evm/instruction.py @@ -33,6 +33,7 @@ RW, RWTableTag, TxLogFieldTag, + TxReceiptFieldTag, ) @@ -211,6 +212,7 @@ def step_state_transition_to_new_context( code_source: Transition, gas_left: Transition, reversible_write_counter: Transition, + log_id: Transition, ): self.constrain_step_state_transition( rw_counter=rw_counter, @@ -220,6 +222,7 @@ def step_state_transition_to_new_context( code_source=code_source, gas_left=gas_left, reversible_write_counter=reversible_write_counter, + log_id=log_id, # Initailization unconditionally program_counter=Transition.to(0), stack_pointer=Transition.to(1024), @@ -461,6 +464,22 @@ def tx_log_lookup( ).value return value + # look up TxReceipt fields (PostStateOrStatus, CumulativeGasUsed, LogLength) + def tx_receipt_lookup( + self, + tx_id: Expression, + field_tag: TxReceiptFieldTag, + ) -> Expression: + value = self.rw_lookup( + RW.Read, + RWTableTag.TxReceipt, + key1=tx_id, + key2=FQ(0), + key3=FQ(field_tag), + key4=FQ(0), + ).value + return value + def bytecode_lookup( self, bytecode_hash: Expression, index: Expression, is_code: Expression = None ) -> Expression: diff --git a/src/zkevm_specs/evm/typing.py b/src/zkevm_specs/evm/typing.py index 1f2a0c114..f09373525 100644 --- a/src/zkevm_specs/evm/typing.py +++ b/src/zkevm_specs/evm/typing.py @@ -28,6 +28,7 @@ RWTableTag, TxContextFieldTag, TxLogFieldTag, + TxReceiptFieldTag, TxTableRow, ) from .opcode import get_push_size, Opcode @@ -390,6 +391,24 @@ def tx_log_write( value=value, ) + def tx_receipt_read( + self, + tx_id: IntOrFQ, + field_tag: TxReceiptFieldTag, + value: Union[int, FQ, RLC], + ) -> RWDictionary: + if isinstance(value, int): + value = FQ(value) + return self._append( + RW.Read, + RWTableTag.TxReceipt, + key1=FQ(tx_id), + key2=FQ(0), + key3=FQ(field_tag), + key4=FQ(0), + value=value, + ) + def tx_refund_read(self, tx_id: IntOrFQ, refund: IntOrFQ) -> RWDictionary: return self._append( RW.Read, RWTableTag.TxRefund, key1=FQ(tx_id), value=FQ(refund), value_prev=FQ(refund) diff --git a/tests/evm/test_end_tx.py b/tests/evm/test_end_tx.py index 03f0e3643..df718390e 100644 --- a/tests/evm/test_end_tx.py +++ b/tests/evm/test_end_tx.py @@ -7,6 +7,7 @@ Tables, AccountFieldTag, CallContextFieldTag, + TxReceiptFieldTag, Block, Transaction, RWDictionary, @@ -19,35 +20,42 @@ # Tx with non-capped refund ( Transaction( - caller_address=0xFE, callee_address=CALLEE_ADDRESS, gas=27000, gas_price=int(2e9) + id=1, caller_address=0xFE, callee_address=CALLEE_ADDRESS, gas=27000, gas_price=int(2e9) ), 994, 4800, False, + 0, ), # Tx with capped refund ( Transaction( - caller_address=0xFE, callee_address=CALLEE_ADDRESS, gas=65000, gas_price=int(2e9) + id=2, caller_address=0xFE, callee_address=CALLEE_ADDRESS, gas=65000, gas_price=int(2e9) ), 3952, 38400, False, + 100, ), # Last tx ( Transaction( - caller_address=0xFE, callee_address=CALLEE_ADDRESS, gas=21000, gas_price=int(2e9) + id=3, caller_address=0xFE, callee_address=CALLEE_ADDRESS, gas=21000, gas_price=int(2e9) ), 0, 0, True, + 20000, ), ) -@pytest.mark.parametrize("tx, gas_left, refund, is_last_tx", TESTING_DATA) -def test_end_tx(tx: Transaction, gas_left: int, refund: int, is_last_tx: bool): +@pytest.mark.parametrize( + "tx, gas_left, refund, is_last_tx, current_cumulative_gas_used", TESTING_DATA +) +def test_end_tx( + tx: Transaction, gas_left: int, refund: int, is_last_tx: bool, current_cumulative_gas_used: int +): randomness = rand_fq() block = Block() @@ -61,13 +69,32 @@ def test_end_tx(tx: Transaction, gas_left: int, refund: int, is_last_tx: bool): # fmt: off RWDictionary(17) .call_context_read(1, CallContextFieldTag.TxId, tx.id) + .call_context_read(1, CallContextFieldTag.IsPersistent, 1) .tx_refund_read(tx.id, refund) .account_write(tx.caller_address, AccountFieldTag.Balance, RLC(caller_balance, randomness), RLC(caller_balance_prev, randomness)) .account_write(block.coinbase, AccountFieldTag.Balance, RLC(coinbase_balance, randomness), RLC(coinbase_balance_prev, randomness)) + .tx_receipt_read(tx.id, TxReceiptFieldTag.PostStateOrStatus, 1) + .tx_receipt_read(tx.id, TxReceiptFieldTag.LogLength, 0) # fmt: on ) + + # check it is first tx + is_first_tx = tx.id == 1 + if is_first_tx: + assert current_cumulative_gas_used == 0 + rw_dictionary.tx_receipt_read(tx.id, TxReceiptFieldTag.CumulativeGasUsed, tx.gas - gas_left) + else: + rw_dictionary.tx_receipt_read( + tx.id - 1, TxReceiptFieldTag.CumulativeGasUsed, current_cumulative_gas_used + ) + rw_dictionary.tx_receipt_read( + tx.id, + TxReceiptFieldTag.CumulativeGasUsed, + tx.gas - gas_left + current_cumulative_gas_used, + ) + if not is_last_tx: - rw_dictionary.call_context_read(22, CallContextFieldTag.TxId, tx.id + 1) + rw_dictionary.call_context_read(27 - is_first_tx, CallContextFieldTag.TxId, tx.id + 1) tables = Tables( block_table=set(block.table_assignments(randomness)), @@ -94,7 +121,7 @@ def test_end_tx(tx: Transaction, gas_left: int, refund: int, is_last_tx: bool): ), StepState( execution_state=ExecutionState.EndBlock if is_last_tx else ExecutionState.BeginTx, - rw_counter=22 - is_last_tx, + rw_counter=27 - is_first_tx - is_last_tx, call_id=1 if is_last_tx else 0, ), ],