Spec ExecutionState::STOP

specs/opcode/00STOP.md

@@ -0,0 +1,21 @@
+# STOP opcode
+
+## Procedure
+
+### EVM behavior
+
+The `STOP` opcode terminates the call, then:
+
+1. If it's an root call, it ends the execution.
+2. Otherwise, it restores caller's context and switch to it.
+
+### Circuit behavior
+
+The circuit first checks the `result` in call context is indeed success. Then:
+
+1. If it's an root call, it transits to `EndTx`.
+2. Otherwise, it restore caller's context by reading to `rw_table`, then does step state transition to it.
+
+## Code
+
+Please refer to `src/zkevm_specs/evm/execution/stop.py`.

src/zkevm_specs/evm/execution/__init__.py

@@ -39,6 +39,7 @@
 from .shr import shr
 from .bitwise import not_opcode
 from .sdiv_smod import sdiv_smod
+from .stop import stop
 
 
 EXECUTION_STATE_IMPL: Dict[ExecutionState, Callable] = {
@@ -77,4 +78,5 @@
     ExecutionState.ISZERO: iszero,
     ExecutionState.SHR: shr,
     ExecutionState.SDIV_SMOD: sdiv_smod,
+    ExecutionState.STOP: stop,
 }

src/zkevm_specs/evm/execution/calldatacopy.py

@@ -37,7 +37,6 @@ def calldatacopy(instruction: Instruction):
 
     # When length != 0, constrain the state in the next execution state CopyToMemory
     if instruction.is_zero(length) == FQ(0):
-        assert instruction.next is not None
         instruction.constrain_equal(instruction.next.execution_state, ExecutionState.CopyToMemory)
         next_aux = instruction.next.aux_data
         instruction.constrain_equal(next_aux.src_addr, data_offset + call_data_offset)

src/zkevm_specs/evm/execution/codecopy.py

@@ -25,7 +25,6 @@ def codecopy(instruction: Instruction):
     gas_cost = instruction.memory_copier_gas_cost(size, memory_expansion_gas_cost)
 
     if instruction.is_zero(size) == FQ(0):
-        assert instruction.next is not None
         instruction.constrain_equal(
             instruction.next.execution_state, ExecutionState.CopyCodeToMemory
         )

src/zkevm_specs/evm/execution/copy_code_to_memory.py

@@ -37,7 +37,6 @@ def copy_code_to_memory(instruction: Instruction):
     instruction.constrain_zero((1 - lt) * (1 - finished))
 
     if finished == 0:
-        assert instruction.next is not None
         instruction.constrain_equal(
             instruction.next.execution_state, ExecutionState.CopyCodeToMemory
         )

src/zkevm_specs/evm/execution/copy_to_log.py

@@ -39,7 +39,6 @@ def copy_to_log(instruction: Instruction):
     instruction.constrain_zero((1 - lt) * (1 - finished))
 
     if finished == 0:
-        assert instruction.next is not None
         instruction.constrain_equal(instruction.next.execution_state, ExecutionState.CopyToLog)
         next_aux = instruction.next.aux_data
         assert isinstance(next_aux, CopyToLogAuxData)

src/zkevm_specs/evm/execution/log.py

@@ -65,7 +65,6 @@ def log(instruction: Instruction):
     # check memory copy, should do in next step here
     # When length != 0, constrain the state in the next execution state CopyToLog
     if not instruction.is_zero(msize):
-        assert instruction.next is not None
         instruction.constrain_equal(instruction.next.execution_state, ExecutionState.CopyToLog)
         next_aux = instruction.next.aux_data
         instruction.constrain_equal(next_aux.src_addr, mstart)

src/zkevm_specs/evm/execution/stop.py

@@ -0,0 +1,51 @@
+from ...util import FQ
+from ..instruction import Instruction, Transition
+from ..table import CallContextFieldTag
+from ..execution_state import ExecutionState
+
+
+def stop(instruction: Instruction):
+    # Note when transition to STOP, program_counter can only be increased by 1,
+    # (JUMP* will always transit to JUMPDEST, then to STOP if any) so when opcode
+    # fetching is out of range, the program_counter must be equal to code_length.
+    code_length = instruction.bytecode_length(instruction.curr.code_hash)
+    is_out_of_range = instruction.is_equal(code_length, instruction.curr.program_counter)
+    if is_out_of_range == FQ(0):
+        instruction.responsible_opcode_lookup(instruction.opcode_lookup(True))
+
+    # When a call ends with STOP, this call must be successful, but it's not
+    # necessary persistent depends on if it's a sub-call of a failed call or not.
+    is_success = instruction.call_context_lookup(CallContextFieldTag.IsSuccess)
+    instruction.constrain_equal(is_success, FQ(1))
+
+    # Go to EndTx only when is_root
+    is_to_end_tx = instruction.is_equal(instruction.next.execution_state, ExecutionState.EndTx)
+    instruction.constrain_equal(FQ(instruction.curr.is_root), is_to_end_tx)
+
+    if instruction.curr.is_root:
+        # When a transaction ends with STOP, this call must be persistent
+        is_persistent = instruction.call_context_lookup(CallContextFieldTag.IsPersistent)
+        instruction.constrain_equal(is_persistent, FQ(1))
+
+        # Do step state transition
+        instruction.constrain_step_state_transition(
+            rw_counter=Transition.delta(2),
+            call_id=Transition.same(),
+        )
+    else:
+        # There are 2 possible branch for internal call:
+        # 1. is_create:
+        #   STOP returns empty bytes as deployment code, but when it's an internal creation call,
+        #   the code_hash of callee must already be random linear combination of EMPTY_CODE_HASH,
+        #   which doesn't need any update here.
+        # 2. not is_create:
+        #   STOP returns empty bytes as return_data, which doesn't affect caller's memory at all.
+        # So we only need to restore caller's state as finishing this call.
+
+        # Restore caller state to next StepState
+        instruction.step_state_transition_to_restored_context(
+            rw_counter_delta=1,
+            return_data_offset=FQ(0),
+            return_data_length=FQ(0),
+            gas_left=instruction.curr.gas_left,
+        )

src/zkevm_specs/evm/instruction.py

@@ -50,9 +50,9 @@ class TransitionKind(IntEnum):
 
 class Transition:
     kind: TransitionKind
-    value: Union[int, FQ, RLC]
+    value: Union[int, Expression]
 
-    def __init__(self, kind: TransitionKind, value: Union[int, FQ, RLC] = 0) -> None:
+    def __init__(self, kind: TransitionKind, value: Union[int, Expression] = 0) -> None:
         self.kind = kind
         self.value = value
 
@@ -61,11 +61,11 @@ def same() -> Transition:
         return Transition(TransitionKind.Same)
 
     @staticmethod
-    def delta(delta: Union[int, FQ, RLC]):
+    def delta(delta: Union[int, Expression]):
         return Transition(TransitionKind.Delta, delta)
 
     @staticmethod
-    def to(to: Union[int, FQ, RLC]):
+    def to(to: Union[int, Expression]):
         return Transition(TransitionKind.To, to)
 
 
@@ -229,6 +229,79 @@ def step_state_transition_to_new_context(
             memory_size=Transition.to(0),
         )
 
+    def step_state_transition_to_restored_context(
+        self,
+        rw_counter_delta: int,
+        return_data_offset: Expression,
+        return_data_length: Expression,
+        gas_left: Expression,
+    ):
+        # Read caller's context for restore
+        caller_id = self.call_context_lookup(CallContextFieldTag.CallerId)
+        [
+            caller_is_root,
+            caller_is_create,
+            caller_code_hash,
+            caller_program_counter,
+            caller_stack_pointer,
+            caller_gas_left,
+            caller_memory_size,
+            caller_reversible_write_counter,
+        ] = [
+            self.call_context_lookup(field_tag, call_id=caller_id)
+            for field_tag in [
+                CallContextFieldTag.IsRoot,
+                CallContextFieldTag.IsCreate,
+                CallContextFieldTag.CodeHash,
+                CallContextFieldTag.ProgramCounter,
+                CallContextFieldTag.StackPointer,
+                CallContextFieldTag.GasLeft,
+                CallContextFieldTag.MemorySize,
+                CallContextFieldTag.ReversibleWriteCounter,
+            ]
+        ]
+
+        # Update caller's last callee information
+        for (field_tag, expected_value) in [
+            (CallContextFieldTag.LastCalleeId, self.curr.call_id),
+            (CallContextFieldTag.LastCalleeReturnDataOffset, return_data_offset),
+            (CallContextFieldTag.LastCalleeReturnDataLength, return_data_length),
+        ]:
+            self.constrain_equal(
+                self.call_context_lookup(field_tag, RW.Write, call_id=caller_id),
+                expected_value,
+            )
+
+        # Consume all gas_left if call halts in exception
+        if self.curr.execution_state.halts_in_exception():
+            gas_left = FQ(0)
+
+        # Accumulate reversible_write_counter in case this call stack reverts
+        # in the future even it itself succeeds.
+        # Note that when sub-call halts in failure, we don't need to
+        # accumulate reversible_write_counter because what happened in the
+        # sub-call has been reverted.
+        reversible_write_counter = FQ(0)
+        if self.curr.execution_state.halts_in_success():
+            reversible_write_counter = self.curr.reversible_write_counter
+
+        self.constrain_step_state_transition(
+            rw_counter=Transition.delta(rw_counter_delta + 12),
+            call_id=Transition.to(caller_id),
+            is_root=Transition.to(caller_is_root),
+            is_create=Transition.to(caller_is_create),
+            code_hash=Transition.to(caller_code_hash),
+            program_counter=Transition.to(caller_program_counter),
+            stack_pointer=Transition.to(caller_stack_pointer),
+            # Pays back gas_left to caller
+            gas_left=Transition.to(caller_gas_left.expr() + gas_left.expr()),
+            memory_size=Transition.to(caller_memory_size),
+            # Accumulate reversible_write_counter to caller
+            reversible_write_counter=Transition.to(
+                caller_reversible_write_counter.expr() + reversible_write_counter.expr()
+            ),
+        )
+
     def step_state_transition_in_same_context(
         self,
         opcode: Expression,