diff --git a/specs/opcode/15ISZERO.md b/specs/opcode/15ISZERO.md new file mode 100644 index 000000000..0d3547313 --- /dev/null +++ b/specs/opcode/15ISZERO.md @@ -0,0 +1,34 @@ +# ISZERO opcodes + +## Procedure + +### EVM behavior + +Pop an EVM word `value` from the stack. If it is zero, push `1` back to the stask. Otherwise push `0` to stack. + +### Circuit behavior + +The IsZeroGadget takes an argument `value: [u8;32]`. + +If `value` is zero, we annotate stack as \[1, ...\]. Otherwise annotate stack as \[0, ...\]. + +## 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/opcode/iszero.py` diff --git a/src/zkevm_specs/evm/execution/__init__.py b/src/zkevm_specs/evm/execution/__init__.py index 0ecb05b2f..88d9780ae 100644 --- a/src/zkevm_specs/evm/execution/__init__.py +++ b/src/zkevm_specs/evm/execution/__init__.py @@ -18,6 +18,7 @@ from .calldatacopy import * from .calldataload import * from .gas import * +from .iszero import * from .jump import * from .jumpi import * from .origin import * @@ -55,4 +56,5 @@ ExecutionState.SELFBALANCE: selfbalance, ExecutionState.GASPRICE: gasprice, ExecutionState.EXTCODEHASH: extcodehash, + ExecutionState.ISZERO: iszero, } diff --git a/src/zkevm_specs/evm/execution/iszero.py b/src/zkevm_specs/evm/execution/iszero.py new file mode 100644 index 000000000..04013250a --- /dev/null +++ b/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.delta(0), + ) diff --git a/tests/evm/test_iszero.py b/tests/evm/test_iszero.py new file mode 100644 index 000000000..0b0f0f300 --- /dev/null +++ b/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, + ), + ], + )