diff --git a/specs/opcode/00STOP.md b/specs/opcode/00STOP.md new file mode 100644 index 000000000..311f4a8c9 --- /dev/null +++ b/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`. diff --git a/src/zkevm_specs/evm/execution/__init__.py b/src/zkevm_specs/evm/execution/__init__.py index d1ecc5bb2..6e236cbfe 100644 --- a/src/zkevm_specs/evm/execution/__init__.py +++ b/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, } diff --git a/src/zkevm_specs/evm/execution/calldatacopy.py b/src/zkevm_specs/evm/execution/calldatacopy.py index eb3152345..186271bc9 100644 --- a/src/zkevm_specs/evm/execution/calldatacopy.py +++ b/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) diff --git a/src/zkevm_specs/evm/execution/codecopy.py b/src/zkevm_specs/evm/execution/codecopy.py index 3ddc5e1f5..6790c5d1a 100644 --- a/src/zkevm_specs/evm/execution/codecopy.py +++ b/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 ) diff --git a/src/zkevm_specs/evm/execution/copy_code_to_memory.py b/src/zkevm_specs/evm/execution/copy_code_to_memory.py index 52949b002..d39da5ef9 100644 --- a/src/zkevm_specs/evm/execution/copy_code_to_memory.py +++ b/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 ) diff --git a/src/zkevm_specs/evm/execution/copy_to_log.py b/src/zkevm_specs/evm/execution/copy_to_log.py index 04961ba2d..b4aab4d3c 100644 --- a/src/zkevm_specs/evm/execution/copy_to_log.py +++ b/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) diff --git a/src/zkevm_specs/evm/execution/log.py b/src/zkevm_specs/evm/execution/log.py index b3c8f9ffc..c68e47dbc 100644 --- a/src/zkevm_specs/evm/execution/log.py +++ b/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) diff --git a/src/zkevm_specs/evm/execution/stop.py b/src/zkevm_specs/evm/execution/stop.py new file mode 100644 index 000000000..32bf13095 --- /dev/null +++ b/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, + ) diff --git a/src/zkevm_specs/evm/instruction.py b/src/zkevm_specs/evm/instruction.py index 341790e03..fb251747f 100644 --- a/src/zkevm_specs/evm/instruction.py +++ b/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, diff --git a/tests/evm/test_stop.py b/tests/evm/test_stop.py new file mode 100644 index 000000000..50a04e32c --- /dev/null +++ b/tests/evm/test_stop.py @@ -0,0 +1,168 @@ +import pytest +from collections import namedtuple +from itertools import chain + +from zkevm_specs.evm import ( + ExecutionState, + StepState, + verify_steps, + Tables, + CallContextFieldTag, + Block, + Transaction, + Bytecode, + RWDictionary, +) +from zkevm_specs.util import rand_fq, RLC + +BYTECODE_END_WITHOUT_STOP = Bytecode().push(0, n_bytes=1) +BYTECODE_END_WITH_STOP = Bytecode().push(0, n_bytes=1).stop() + +TESTING_DATA_IS_ROOT = ( + (Transaction(), BYTECODE_END_WITHOUT_STOP), + (Transaction(), BYTECODE_END_WITH_STOP), +) + + +@pytest.mark.parametrize("tx, bytecode", TESTING_DATA_IS_ROOT) +def test_stop_is_root(tx: Transaction, bytecode: Bytecode): + randomness = rand_fq() + + block = Block() + + bytecode_hash = RLC(bytecode.hash(), randomness) + + tables = Tables( + block_table=set(block.table_assignments(randomness)), + tx_table=set( + chain( + tx.table_assignments(randomness), + Transaction(id=tx.id + 1).table_assignments(randomness), + ) + ), + bytecode_table=set(bytecode.table_assignments(randomness)), + rw_table=set( + RWDictionary(24) + .call_context_read(1, CallContextFieldTag.IsSuccess, 1) + .call_context_read(1, CallContextFieldTag.IsPersistent, 1) + .rws + ), + ) + + verify_steps( + randomness=randomness, + tables=tables, + steps=[ + StepState( + execution_state=ExecutionState.STOP, + rw_counter=24, + call_id=1, + is_root=True, + is_create=False, + code_hash=bytecode_hash, + program_counter=2, + stack_pointer=1023, + gas_left=0, + reversible_write_counter=2, + ), + StepState( + execution_state=ExecutionState.EndTx, + rw_counter=26, + call_id=1, + ), + ], + ) + + +CallContext = namedtuple( + "CallContext", + [ + "is_root", + "is_create", + "program_counter", + "stack_pointer", + "gas_left", + "memory_size", + "reversible_write_counter", + ], + defaults=[True, False, 232, 1023, 0, 0, 0], +) + +TESTING_DATA_NOT_ROOT = ( + (CallContext(), BYTECODE_END_WITHOUT_STOP), + (CallContext(), BYTECODE_END_WITH_STOP), +) + + +@pytest.mark.parametrize("caller_ctx, callee_bytecode", TESTING_DATA_NOT_ROOT) +def test_stop_not_root(caller_ctx: CallContext, callee_bytecode: Bytecode): + randomness = rand_fq() + + caller_bytecode = Bytecode().call(0, 0xFF, 0, 0, 0, 0, 0).stop() + caller_bytecode_hash = RLC(caller_bytecode.hash(), randomness) + callee_bytecode_hash = RLC(callee_bytecode.hash(), randomness) + callee_gas_left = 400 + callee_reversible_write_counter = 2 + + tables = Tables( + block_table=set(Block().table_assignments(randomness)), + tx_table=set(), + bytecode_table=set( + chain( + caller_bytecode.table_assignments(randomness), + callee_bytecode.table_assignments(randomness), + ) + ), + rw_table=set( + # fmt: off + RWDictionary(69) + .call_context_read(24, CallContextFieldTag.IsSuccess, 1) + .call_context_read(24, CallContextFieldTag.CallerId, 1) + .call_context_read(1, CallContextFieldTag.IsRoot, caller_ctx.is_root) + .call_context_read(1, CallContextFieldTag.IsCreate, caller_ctx.is_create) + .call_context_read(1, CallContextFieldTag.CodeHash, caller_bytecode_hash) + .call_context_read(1, CallContextFieldTag.ProgramCounter, caller_ctx.program_counter) + .call_context_read(1, CallContextFieldTag.StackPointer, caller_ctx.stack_pointer) + .call_context_read(1, CallContextFieldTag.GasLeft, caller_ctx.gas_left) + .call_context_read(1, CallContextFieldTag.MemorySize, caller_ctx.memory_size) + .call_context_read(1, CallContextFieldTag.ReversibleWriteCounter, caller_ctx.reversible_write_counter) + .call_context_write(1, CallContextFieldTag.LastCalleeId, 24) + .call_context_write(1, CallContextFieldTag.LastCalleeReturnDataOffset, 0) + .call_context_write(1, CallContextFieldTag.LastCalleeReturnDataLength, 0) + .rws + # fmt: on + ), + ) + + verify_steps( + randomness=randomness, + tables=tables, + steps=[ + StepState( + execution_state=ExecutionState.STOP, + rw_counter=69, + call_id=24, + is_root=False, + is_create=False, + code_hash=callee_bytecode_hash, + program_counter=2, + stack_pointer=1023, + gas_left=callee_gas_left, + reversible_write_counter=callee_reversible_write_counter, + ), + StepState( + execution_state=ExecutionState.STOP, + rw_counter=82, + call_id=1, + is_root=caller_ctx.is_root, + is_create=caller_ctx.is_create, + code_hash=caller_bytecode_hash, + program_counter=caller_ctx.program_counter, + stack_pointer=caller_ctx.stack_pointer, + gas_left=caller_ctx.gas_left + callee_gas_left, + memory_size=caller_ctx.memory_size, + reversible_write_counter=caller_ctx.reversible_write_counter + + callee_reversible_write_counter, + ), + ], + )