add TxReceipt constraint in begin&end tx

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

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

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

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:

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)

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,
             ),
         ],