Spec for ErrorInvalidOpcode state

specs/error_state/error_invalid_jump.md → specs/error_state/ErrorInvalidJump.md

@@ -1,4 +1,4 @@
-# ErrorOutOfGasConstant state
+# ErrorInvalidJump state
 
 ## Procedure
 this type of error only occurs when executing op code is `JUMP` or `JUMPI`.

specs/error_state/ErrorInvalidOpcode.md

@@ -0,0 +1,21 @@
+# ErrorInvalidOpcode state
+
+## Procedure
+
+`ErrorInvalidOpcode` may occur when an invalid opcode is encountered in any step during the execution.
+
+### EVM behavior
+
+1. If it's a root call, it ends the execution.
+2. Otherwise, it restores caller's context and switch to it.
+
+### Constraints
+
+1. Do a fixed lookup for `FixedTableTag.ResponsibleOpcode`.
+2. Current call must be failed. Do a call context lookup for `CallContextFieldTag.IsSuccess`.
+3. If it's a root call, it transits to `EndTx`.
+4. if it is not root call, it restores caller's context by reading to `rw_table`, then does step state transition to it.
+
+## Code
+
+Please refer to `src/zkevm_specs/evm/execution/error_invalid_opcode.py`.

src/zkevm_specs/evm/execution/__init__.py

@@ -55,7 +55,8 @@
 from .oog_constant import *
 from .oog_call import *
 from .error_stack import *
-from .error_Invalid_jump import *
+from .error_invalid_jump import *
+from .error_invalid_opcode import *
 
 
 EXECUTION_STATE_IMPL: Dict[ExecutionState, Callable] = {
@@ -106,9 +107,10 @@
     ExecutionState.SHL_SHR: shl_shr,
     ExecutionState.STOP: stop,
     ExecutionState.RETURN: return_revert,
-    ExecutionState.ErrorOutOfGasConstant: oog_constant,
     ExecutionState.ErrorInvalidJump: invalid_jump,
+    ExecutionState.ErrorInvalidOpcode: invalid_opcode,
     ExecutionState.ErrorOutOfGasCALL: oog_call,
+    ExecutionState.ErrorOutOfGasConstant: oog_constant,
     ExecutionState.ErrorStack: stack_error,
     # ExecutionState.ECRECOVER: ,
     # ExecutionState.SHA256: ,

src/zkevm_specs/evm/execution/error_Invalid_jump.py → src/zkevm_specs/evm/execution/error_invalid_jump.py

@@ -1,7 +1,5 @@
 from ...util import FQ
-from ..instruction import Instruction, Transition
-from ..table import CallContextFieldTag
-from ..execution_state import ExecutionState
+from ..instruction import Instruction
 from ..opcode import Opcode
 from ...util import N_BYTES_PROGRAM_COUNTER
 
@@ -30,26 +28,6 @@ def invalid_jump(instruction: Instruction):
         is_jump_dest = value == Opcode.JUMPDEST
         instruction.constrain_zero(is_code * FQ(is_jump_dest))
 
-    # current call must be failed.
-    is_success = instruction.call_context_lookup(CallContextFieldTag.IsSuccess)
-    instruction.constrain_equal(is_success, FQ(0))
-
-    # 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:
-        # Do step state transition
-        instruction.constrain_step_state_transition(
-            rw_counter=Transition.delta(2 + is_jumpi.n + instruction.curr.reversible_write_counter),
-            call_id=Transition.same(),
-        )
-    else:
-        # when it is internal call, 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=2 + is_jumpi.n + instruction.curr.reversible_write_counter.n,
-            return_data_offset=FQ(0),
-            return_data_length=FQ(0),
-            gas_left=instruction.curr.gas_left,
+        instruction.constrain_error_state(
+            2 + is_jumpi.n + instruction.curr.reversible_write_counter.n
         )

src/zkevm_specs/evm/execution/error_invalid_opcode.py

@@ -0,0 +1,10 @@
+from ..instruction import Instruction
+
+
+# Gadget for invalid opcodes. It verifies by a fixed lookup for ResponsibleOpcode.
+def invalid_opcode(instruction: Instruction):
+    # Fixed lookup for invalid opcode.
+    opcode = instruction.opcode_lookup(True)
+    instruction.responsible_opcode_lookup(opcode)
+
+    instruction.constrain_error_state(1 + instruction.curr.reversible_write_counter.n)

src/zkevm_specs/evm/execution/error_stack.py

@@ -1,7 +1,5 @@
 from ...util import FQ
-from ..instruction import Instruction, Transition, FixedTableTag
-from ..table import CallContextFieldTag
-from ..execution_state import ExecutionState
+from ..instruction import Instruction, FixedTableTag
 from ..opcode import Opcode
 from ...util import N_BYTES_STACK
 
@@ -30,26 +28,4 @@ def stack_error(instruction: Instruction):
     # constrain one of [is_underflow, is_overflow] must be true when stack error happens
     instruction.constrain_equal(is_underflow + is_overflow, FQ(1))
 
-    # current call must be failed.
-    is_success = instruction.call_context_lookup(CallContextFieldTag.IsSuccess)
-    instruction.constrain_equal(is_success, FQ(0))
-
-    # 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:
-        # Do step state transition
-        instruction.constrain_step_state_transition(
-            rw_counter=Transition.delta(1 + instruction.curr.reversible_write_counter),
-            call_id=Transition.same(),
-        )
-    else:
-        # when it is internal call, 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 + instruction.curr.reversible_write_counter.n,
-            return_data_offset=FQ(0),
-            return_data_length=FQ(0),
-            gas_left=instruction.curr.gas_left,
-        )
+    instruction.constrain_error_state(1 + instruction.curr.reversible_write_counter.n)

src/zkevm_specs/evm/execution/oog_call.py

@@ -1,8 +1,7 @@
 from zkevm_specs.evm.util.call_gadget import CallGadget
 from ...util import FQ
-from ..instruction import Instruction, Transition
+from ..instruction import Instruction
 from ..table import CallContextFieldTag
-from ..execution_state import ExecutionState
 from ...util import N_BYTES_GAS
 from ..opcode import Opcode
 
@@ -30,28 +29,4 @@ def oog_call(instruction: Instruction):
     gas_not_enough, _ = instruction.compare(instruction.curr.gas_left, gas_cost, N_BYTES_GAS)
     instruction.constrain_equal(gas_not_enough, FQ(1))
 
-    # current call must be failed.
-    instruction.constrain_equal(
-        instruction.call_context_lookup(CallContextFieldTag.IsSuccess), FQ(0)
-    )
-
-    # 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)
-
-    # state transition.
-    if instruction.curr.is_root:
-        # Do step state transition
-        instruction.constrain_step_state_transition(
-            rw_counter=Transition.delta(12),
-            call_id=Transition.same(),
-        )
-    else:
-        # when it is internal call, 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=12,
-            return_data_offset=FQ(0),
-            return_data_length=FQ(0),
-            gas_left=instruction.curr.gas_left,
-        )
+    instruction.constrain_error_state(12 + instruction.curr.reversible_write_counter.n)

src/zkevm_specs/evm/execution/oog_constant.py

@@ -1,7 +1,5 @@
 from ...util import FQ
-from ..instruction import Instruction, Transition, FixedTableTag
-from ..table import CallContextFieldTag
-from ..execution_state import ExecutionState
+from ..instruction import Instruction, FixedTableTag
 from ..opcode import Opcode
 from ...util import N_BYTES_GAS
 
@@ -19,26 +17,4 @@ def oog_constant(instruction: Instruction):
     )
     instruction.constrain_equal(gas_not_enough, FQ(1))
 
-    # current call must be failed.
-    is_success = instruction.call_context_lookup(CallContextFieldTag.IsSuccess)
-    instruction.constrain_equal(is_success, FQ(0))
-
-    # 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:
-        # Do step state transition
-        instruction.constrain_step_state_transition(
-            rw_counter=Transition.delta(1 + instruction.curr.reversible_write_counter),
-            call_id=Transition.same(),
-        )
-    else:
-        # when it is internal call, 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 + instruction.curr.reversible_write_counter.n,
-            return_data_offset=FQ(0),
-            return_data_length=FQ(0),
-            gas_left=instruction.curr.gas_left,
-        )
+    instruction.constrain_error_state(1 + instruction.curr.reversible_write_counter.n)

src/zkevm_specs/evm/instruction.py

@@ -285,10 +285,6 @@ def step_state_transition_to_restored_context(
                 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
@@ -1129,3 +1125,30 @@ def exp_lookup(
     ) -> Tuple[FQ, FQ]:
         exp_table_row = self.tables.exp_lookup(identifier, is_last, base_limbs, exponent_lo_hi)
         return exp_table_row.exponentiation_lo, exp_table_row.exponentiation_hi
+
+    def constrain_error_state(self, rw_counter_delta: int):
+        # Current call must fail.
+        is_success = self.call_context_lookup(CallContextFieldTag.IsSuccess)
+        self.constrain_equal(is_success, FQ(0))
+
+        # Go to EndTx only when is_root.
+        is_to_end_tx = self.is_equal(self.next.execution_state, ExecutionState.EndTx)
+        self.constrain_equal(FQ(self.curr.is_root), is_to_end_tx)
+
+        # When it's a root call.
+        if self.curr.is_root:
+            # Do step state transition.
+            self.constrain_step_state_transition(
+                rw_counter=Transition.delta(rw_counter_delta),
+                call_id=Transition.same(),
+            )
+        else:
+            # When it is internal call, need to restore caller's state as finishing this call.
+            # Restore caller state to next StepState.
+            self.step_state_transition_to_restored_context(
+                rw_counter_delta=rw_counter_delta,
+                return_data_offset=FQ(0),
+                return_data_length=FQ(0),
+                # Consume all gas_left if it's an exception step.
+                gas_left=FQ(0),
+            )

tests/evm/test_error_stack.py

@@ -97,7 +97,7 @@ def test_overflow_not_root(caller_ctx: CallContext, callee_bytecode: Bytecode):
     caller_bytecode_hash = RLC(caller_bytecode.hash(), randomness)
     callee_bytecode_hash = RLC(callee_bytecode.hash(), randomness)
     # gas is insufficient
-    callee_reversible_write_counter = 0
+    callee_reversible_write_counter = 2
 
     tables = Tables(
         block_table=set(Block().table_assignments(randomness)),
@@ -147,7 +147,7 @@ def test_overflow_not_root(caller_ctx: CallContext, callee_bytecode: Bytecode):
             ),
             StepState(
                 execution_state=ExecutionState.STOP,
-                rw_counter=82,
+                rw_counter=82 + callee_reversible_write_counter,
                 call_id=1,
                 is_root=caller_ctx.is_root,
                 is_create=caller_ctx.is_create,
@@ -156,8 +156,7 @@ def test_overflow_not_root(caller_ctx: CallContext, callee_bytecode: Bytecode):
                 stack_pointer=caller_ctx.stack_pointer,
                 gas_left=caller_ctx.gas_left,
                 memory_size=caller_ctx.memory_size,
-                reversible_write_counter=caller_ctx.reversible_write_counter
-                + callee_reversible_write_counter,
+                reversible_write_counter=caller_ctx.reversible_write_counter,
             ),
         ],
     )

tests/evm/test_invalid_jump.py

@@ -100,7 +100,7 @@ def test_invalid_jump_not_root(caller_ctx: CallContext, dest_bytes: bytes):
     caller_bytecode_hash = RLC(caller_bytecode.hash(), randomness)
     callee_bytecode = Bytecode().push1(0x80).push1(0x40).push1(dest_bytes).jump().jumpdest().stop()
     callee_bytecode_hash = RLC(callee_bytecode.hash(), randomness)
-    callee_reversible_write_counter = 0
+    callee_reversible_write_counter = 2
 
     tables = Tables(
         block_table=set(Block().table_assignments(randomness)),
@@ -151,7 +151,7 @@ def test_invalid_jump_not_root(caller_ctx: CallContext, dest_bytes: bytes):
             ),
             StepState(
                 execution_state=ExecutionState.STOP,
-                rw_counter=83,
+                rw_counter=83 + callee_reversible_write_counter,
                 call_id=1,
                 is_root=caller_ctx.is_root,
                 is_create=caller_ctx.is_create,
@@ -160,8 +160,7 @@ def test_invalid_jump_not_root(caller_ctx: CallContext, dest_bytes: bytes):
                 stack_pointer=caller_ctx.stack_pointer,
                 gas_left=caller_ctx.gas_left,
                 memory_size=caller_ctx.memory_size,
-                reversible_write_counter=caller_ctx.reversible_write_counter
-                + callee_reversible_write_counter,
+                reversible_write_counter=caller_ctx.reversible_write_counter,
             ),
         ],
     )