Spec for opcode ISZERO

specs/opcode/15ISZERO.md

@@ -0,0 +1,26 @@
+# ISZERO opcode
+
+## Procedure
+
+Pop an EVM word `value` from the stack. If it is zero, push `1` back to the stack. Otherwise push `0` to stack.
+
+## Constraints
+
+1. state transition:
+   - gc + 2 (1 stack read + 1 stack write)
+   - stack_pointer + 0 (one pop and one push)
+   - pc + 1
+   - gas + 3
+2. Lookups: 2 busmapping lookups
+   - `value` is at the top of the stack
+   - `result`, is at the new top of the stack
+
+## Exceptions
+
+1. stack underflow:
+   - the stack is empty: `1024 == stack_pointer`
+2. out of gas: remaining gas is not enough
+
+## Code
+
+See `src/zkevm_specs/evm/execution/iszero.py`

src/zkevm_specs/evm/execution/__init__.py

@@ -20,6 +20,7 @@
 from .calldatacopy import *
 from .calldataload import *
 from .gas import *
+from .iszero import *
 from .jump import *
 from .jumpi import *
 from .origin import *
@@ -61,4 +62,5 @@
     ExecutionState.CopyToLog: copy_to_log,
     ExecutionState.LOG: log,
     ExecutionState.CALL: call,
+    ExecutionState.ISZERO: iszero,
 }

src/zkevm_specs/evm/execution/iszero.py

@@ -0,0 +1,20 @@
+from ..instruction import Instruction, Transition
+from ..opcode import Opcode
+
+
+def iszero(instruction: Instruction):
+    opcode = instruction.opcode_lookup(True)
+
+    value = instruction.stack_pop()
+
+    instruction.constrain_equal(
+        instruction.is_zero(value),
+        instruction.stack_push(),
+    )
+
+    instruction.step_state_transition_in_same_context(
+        opcode,
+        rw_counter=Transition.delta(2),
+        program_counter=Transition.delta(1),
+        stack_pointer=Transition.same(),
+    )

tests/evm/test_iszero.py

@@ -0,0 +1,69 @@
+import pytest
+
+from typing import Optional
+from zkevm_specs.evm import (
+    ExecutionState,
+    StepState,
+    Opcode,
+    verify_steps,
+    Tables,
+    Block,
+    Bytecode,
+    RWDictionary,
+)
+from zkevm_specs.util import rand_fq, rand_word, RLC
+
+
+TESTING_DATA = (
+    bytes([0]),
+    bytes([7]),
+)
+
+
+@pytest.mark.parametrize("value_be_bytes", TESTING_DATA)
+def test_iszero(value_be_bytes: bytes):
+    randomness = rand_fq()
+
+    value = int.from_bytes(value_be_bytes, "big")
+    result = 0x1 if value == 0x0 else 0x0
+    value = RLC(value, randomness)
+    result = RLC(result, randomness)
+
+    bytecode = Bytecode().push1(value_be_bytes).iszero().stop()
+    bytecode_hash = RLC(bytecode.hash(), randomness)
+
+    tables = Tables(
+        block_table=set(Block().table_assignments(randomness)),
+        tx_table=set(),
+        bytecode_table=set(bytecode.table_assignments(randomness)),
+        rw_table=set(RWDictionary(9).stack_read(1, 1023, value).stack_write(1, 1023, result).rws),
+    )
+
+    verify_steps(
+        randomness=randomness,
+        tables=tables,
+        steps=[
+            StepState(
+                execution_state=ExecutionState.ISZERO,
+                rw_counter=9,
+                call_id=1,
+                is_root=True,
+                is_create=False,
+                code_source=bytecode_hash,
+                program_counter=2,
+                stack_pointer=1023,
+                gas_left=3,
+            ),
+            StepState(
+                execution_state=ExecutionState.STOP,
+                rw_counter=11,
+                call_id=1,
+                is_root=True,
+                is_create=False,
+                code_source=bytecode_hash,
+                program_counter=3,
+                stack_pointer=1023,
+                gas_left=0,
+            ),
+        ],
+    )