From c0f69d8b6ef0407682684d9bf72e3f269be422e6 Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Wed, 23 Mar 2022 16:08:05 +0800 Subject: [PATCH 01/15] Implement opcode `ISZERO`. --- src/zkevm_specs/evm/execution/__init__.py | 2 + src/zkevm_specs/evm/execution/iszero.py | 20 +++++++ tests/evm/test_iszero.py | 72 +++++++++++++++++++++++ 3 files changed, 94 insertions(+) create mode 100644 src/zkevm_specs/evm/execution/iszero.py create mode 100644 tests/evm/test_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..b9c034b01 --- /dev/null +++ b/tests/evm/test_iszero.py @@ -0,0 +1,72 @@ +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 = ( + (Opcode.ISZERO, 0x0, 0x1), + (Opcode.ISZERO, 0x060504, 0x0), +) + + +@pytest.mark.parametrize("opcode, value, is_zero", TESTING_DATA) +def test_iszero(opcode: Opcode, value: int, is_zero: int): + randomness = rand_fq() + + value = RLC(value, randomness) + is_zero = RLC(is_zero, randomness) + + bytecode = Bytecode().iszero(value) + 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, 1022, value) + .stack_write(1, 1023, is_zero) + .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=66, + stack_pointer=1022, + gas_left=3, + ), + StepState( + execution_state=ExecutionState.STOP, + rw_counter=12, + call_id=1, + is_root=True, + is_create=False, + code_source=bytecode_hash, + program_counter=67, + stack_pointer=1023, + gas_left=0, + ), + ], + ) From da3a5bf1d3f01c80545bb54a1be2b80ff43c9d13 Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Wed, 23 Mar 2022 16:22:32 +0800 Subject: [PATCH 02/15] Fix wrong delta for pointers. --- tests/evm/test_iszero.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/evm/test_iszero.py b/tests/evm/test_iszero.py index b9c034b01..e9f6c95f9 100644 --- a/tests/evm/test_iszero.py +++ b/tests/evm/test_iszero.py @@ -59,13 +59,13 @@ def test_iszero(opcode: Opcode, value: int, is_zero: int): ), StepState( execution_state=ExecutionState.STOP, - rw_counter=12, + rw_counter=11, call_id=1, is_root=True, is_create=False, code_source=bytecode_hash, program_counter=67, - stack_pointer=1023, + stack_pointer=1022, gas_left=0, ), ], From eff6770ed5b9926cf45c8cd879b16f156a7ef5c7 Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Wed, 23 Mar 2022 16:35:39 +0800 Subject: [PATCH 03/15] Fix the wrong stack pointer. --- tests/evm/test_iszero.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/evm/test_iszero.py b/tests/evm/test_iszero.py index e9f6c95f9..586510454 100644 --- a/tests/evm/test_iszero.py +++ b/tests/evm/test_iszero.py @@ -36,7 +36,7 @@ def test_iszero(opcode: Opcode, value: int, is_zero: int): bytecode_table=set(bytecode.table_assignments(randomness)), rw_table=set( RWDictionary(9) - .stack_read(1, 1022, value) + .stack_read(1, 1023, value) .stack_write(1, 1023, is_zero) .rws ), @@ -54,7 +54,7 @@ def test_iszero(opcode: Opcode, value: int, is_zero: int): is_create=False, code_source=bytecode_hash, program_counter=66, - stack_pointer=1022, + stack_pointer=1023, gas_left=3, ), StepState( @@ -65,7 +65,7 @@ def test_iszero(opcode: Opcode, value: int, is_zero: int): is_create=False, code_source=bytecode_hash, program_counter=67, - stack_pointer=1022, + stack_pointer=1023, gas_left=0, ), ], From 3997634717ec9fc76da23b656296e053d89dfedf Mon Sep 17 00:00:00 2001 From: HAOYUatHZ Date: Wed, 23 Mar 2022 16:59:55 +0800 Subject: [PATCH 04/15] refactor --- tests/evm/test_iszero.py | 21 +++++++++------------ 1 file changed, 9 insertions(+), 12 deletions(-) diff --git a/tests/evm/test_iszero.py b/tests/evm/test_iszero.py index 586510454..88358c5be 100644 --- a/tests/evm/test_iszero.py +++ b/tests/evm/test_iszero.py @@ -15,31 +15,28 @@ TESTING_DATA = ( - (Opcode.ISZERO, 0x0, 0x1), - (Opcode.ISZERO, 0x060504, 0x0), + (0x0), + (0x060504), ) -@pytest.mark.parametrize("opcode, value, is_zero", TESTING_DATA) -def test_iszero(opcode: Opcode, value: int, is_zero: int): +@pytest.mark.parametrize("value", TESTING_DATA) +def test_iszero(value: int): randomness = rand_fq() + result = 0x1 if value == 0x0 else 0x0 + value = RLC(value, randomness) - is_zero = RLC(is_zero, randomness) + result = RLC(result, randomness) - bytecode = Bytecode().iszero(value) + bytecode = Bytecode().iszero(value).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, is_zero) - .rws - ), + rw_table=set(RWDictionary(9).stack_read(1, 1023, value).stack_write(1, 1023, result).rws), ) verify_steps( From c05af4bb1d5827da7c7172c4fc4c47855eb9f85f Mon Sep 17 00:00:00 2001 From: HAOYUatHZ Date: Wed, 23 Mar 2022 17:11:48 +0800 Subject: [PATCH 05/15] fix --- tests/evm/test_iszero.py | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/tests/evm/test_iszero.py b/tests/evm/test_iszero.py index 88358c5be..0b0f0f300 100644 --- a/tests/evm/test_iszero.py +++ b/tests/evm/test_iszero.py @@ -15,21 +15,21 @@ TESTING_DATA = ( - (0x0), - (0x060504), + bytes([0]), + bytes([7]), ) -@pytest.mark.parametrize("value", TESTING_DATA) -def test_iszero(value: int): +@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().iszero(value).stop() + bytecode = Bytecode().push1(value_be_bytes).iszero().stop() bytecode_hash = RLC(bytecode.hash(), randomness) tables = Tables( @@ -50,7 +50,7 @@ def test_iszero(value: int): is_root=True, is_create=False, code_source=bytecode_hash, - program_counter=66, + program_counter=2, stack_pointer=1023, gas_left=3, ), @@ -61,7 +61,7 @@ def test_iszero(value: int): is_root=True, is_create=False, code_source=bytecode_hash, - program_counter=67, + program_counter=3, stack_pointer=1023, gas_left=0, ), From eda049b425456e15f4f6776c540242f4cc0e0e6b Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Wed, 23 Mar 2022 17:51:50 +0800 Subject: [PATCH 06/15] Add markdown. --- specs/opcode/15ISZERO.md | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 specs/opcode/15ISZERO.md diff --git a/specs/opcode/15ISZERO.md b/specs/opcode/15ISZERO.md new file mode 100644 index 000000000..d53859451 --- /dev/null +++ b/specs/opcode/15ISZERO.md @@ -0,0 +1,36 @@ +# 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 argument of `value: [u8;32]` and `result: [u8;32]`. + +If `value` is zero, it validates `result === 1`. Otherwise it validates `result === 0`. + +We annotate stack as \[value, ...\] and \[result, ...\]. + +## Constraints + +1. opId = OpcodeId(0x15) +2. state transition: + - gc + 2 (1 stack read + 1 stack write) + - stack_pointer + 0 (one pop and one push) + - pc + 1 + - gas + 3 +3. 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: `1023 <= stack_pointer <= 1023` +2. out of gas: remaining gas is not enough + +## Code + +See `src/zkevm_specs/opcode/iszero.py` From cc182a39d073b9c2abfacf806d299278cacb41f8 Mon Sep 17 00:00:00 2001 From: Steven Date: Wed, 23 Mar 2022 19:40:55 +0800 Subject: [PATCH 07/15] Fix `stack underflow`. Co-authored-by: HAOYUatHZ <37070449+HAOYUatHZ@users.noreply.github.com> --- specs/opcode/15ISZERO.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/specs/opcode/15ISZERO.md b/specs/opcode/15ISZERO.md index d53859451..3fba71f9e 100644 --- a/specs/opcode/15ISZERO.md +++ b/specs/opcode/15ISZERO.md @@ -28,7 +28,8 @@ We annotate stack as \[value, ...\] and \[result, ...\]. ## Exceptions -1. stack underflow: `1023 <= stack_pointer <= 1023` +1. stack underflow: + - the stack is empty: `1024 == stack_pointer` 2. out of gas: remaining gas is not enough ## Code From bd8efc9132ea2a71eaf7c7ceddb9de0b3be499b3 Mon Sep 17 00:00:00 2001 From: Steven Date: Wed, 23 Mar 2022 19:41:41 +0800 Subject: [PATCH 08/15] Update specs/opcode/15ISZERO.md Co-authored-by: HAOYUatHZ <37070449+HAOYUatHZ@users.noreply.github.com> --- specs/opcode/15ISZERO.md | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/specs/opcode/15ISZERO.md b/specs/opcode/15ISZERO.md index 3fba71f9e..105666fc6 100644 --- a/specs/opcode/15ISZERO.md +++ b/specs/opcode/15ISZERO.md @@ -8,11 +8,9 @@ Pop an EVM word `value` from the stack. If it is zero, push `1` back to the stas ### Circuit behavior -The IsZeroGadget takes argument of `value: [u8;32]` and `result: [u8;32]`. +The IsZeroGadget takes an argument `value: [u8;32]`. -If `value` is zero, it validates `result === 1`. Otherwise it validates `result === 0`. - -We annotate stack as \[value, ...\] and \[result, ...\]. +If `value` is zero, we annotate stack as \[1, ...\]. Otherwise annotate stack as \[0, ...\]. ## Constraints From d1b99a821521741c6f8da4c49ae76b95e923d26e Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Wed, 23 Mar 2022 19:45:36 +0800 Subject: [PATCH 09/15] Remove opcode check in markdown. --- specs/opcode/15ISZERO.md | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/specs/opcode/15ISZERO.md b/specs/opcode/15ISZERO.md index 105666fc6..0d3547313 100644 --- a/specs/opcode/15ISZERO.md +++ b/specs/opcode/15ISZERO.md @@ -14,13 +14,12 @@ If `value` is zero, we annotate stack as \[1, ...\]. Otherwise annotate stack as ## Constraints -1. opId = OpcodeId(0x15) -2. state transition: +1. state transition: - gc + 2 (1 stack read + 1 stack write) - stack_pointer + 0 (one pop and one push) - pc + 1 - gas + 3 -3. Lookups: 2 busmapping lookups +2. Lookups: 2 busmapping lookups - `value` is at the top of the stack - `result`, is at the new top of the stack From 98fb255f14c6e63c5df45835c7a4e3c45732469e Mon Sep 17 00:00:00 2001 From: HAOYUatHZ Date: Thu, 24 Mar 2022 10:31:26 +0800 Subject: [PATCH 10/15] simplify fix typos --- specs/opcode/15ISZERO.md | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/specs/opcode/15ISZERO.md b/specs/opcode/15ISZERO.md index 0d3547313..002689b93 100644 --- a/specs/opcode/15ISZERO.md +++ b/specs/opcode/15ISZERO.md @@ -2,15 +2,7 @@ ## 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, ...\]. +Pop an EVM word `value` from the stack. If it is zero, push `1` back to the stack. Otherwise push `0` to stack. ## Constraints From b0a815f3df5068b8b0121281cc95833321d9291b Mon Sep 17 00:00:00 2001 From: HAOYUatHZ <37070449+HAOYUatHZ@users.noreply.github.com> Date: Mon, 28 Mar 2022 15:15:28 +0800 Subject: [PATCH 11/15] Update src/zkevm_specs/evm/execution/iszero.py Co-authored-by: DreamWuGit --- src/zkevm_specs/evm/execution/iszero.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/zkevm_specs/evm/execution/iszero.py b/src/zkevm_specs/evm/execution/iszero.py index 04013250a..9dd614d0e 100644 --- a/src/zkevm_specs/evm/execution/iszero.py +++ b/src/zkevm_specs/evm/execution/iszero.py @@ -16,5 +16,5 @@ def iszero(instruction: Instruction): opcode, rw_counter=Transition.delta(2), program_counter=Transition.delta(1), - stack_pointer=Transition.delta(0), + stack_pointer=Transition.same(), ) From 0bae65b37d352ddc3ebb05ee5f3eadd28148c978 Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Tue, 29 Mar 2022 10:49:55 +0800 Subject: [PATCH 12/15] Fix to sum all limbs of a RLC then assert zero. --- src/zkevm_specs/evm/execution/iszero.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/zkevm_specs/evm/execution/iszero.py b/src/zkevm_specs/evm/execution/iszero.py index 9dd614d0e..ecf8e227f 100644 --- a/src/zkevm_specs/evm/execution/iszero.py +++ b/src/zkevm_specs/evm/execution/iszero.py @@ -1,5 +1,6 @@ from ..instruction import Instruction, Transition from ..opcode import Opcode +from ...util import FQ def iszero(instruction: Instruction): @@ -8,7 +9,7 @@ def iszero(instruction: Instruction): value = instruction.stack_pop() instruction.constrain_equal( - instruction.is_zero(value), + instruction.is_zero(FQ(sum(value.le_bytes))), instruction.stack_push(), ) From e9ed21112e8175303663713207005234600e26e0 Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Wed, 30 Mar 2022 08:16:21 +0800 Subject: [PATCH 13/15] Revert the code of sum all limbs of a RLC. --- src/zkevm_specs/evm/execution/iszero.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/zkevm_specs/evm/execution/iszero.py b/src/zkevm_specs/evm/execution/iszero.py index ecf8e227f..9dd614d0e 100644 --- a/src/zkevm_specs/evm/execution/iszero.py +++ b/src/zkevm_specs/evm/execution/iszero.py @@ -1,6 +1,5 @@ from ..instruction import Instruction, Transition from ..opcode import Opcode -from ...util import FQ def iszero(instruction: Instruction): @@ -9,7 +8,7 @@ def iszero(instruction: Instruction): value = instruction.stack_pop() instruction.constrain_equal( - instruction.is_zero(FQ(sum(value.le_bytes))), + instruction.is_zero(value), instruction.stack_push(), ) From 1de59c5496c102e5d1860f1a8e89556b37b670d0 Mon Sep 17 00:00:00 2001 From: Steven Date: Thu, 31 Mar 2022 14:06:50 +0800 Subject: [PATCH 14/15] Update specs/opcode/15ISZERO.md Co-authored-by: Haichen Shen --- specs/opcode/15ISZERO.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/specs/opcode/15ISZERO.md b/specs/opcode/15ISZERO.md index 002689b93..5a9997068 100644 --- a/specs/opcode/15ISZERO.md +++ b/specs/opcode/15ISZERO.md @@ -1,4 +1,4 @@ -# ISZERO opcodes +# ISZERO opcode ## Procedure From efa714021825c8ed6a463c21c0cecd6df2f61103 Mon Sep 17 00:00:00 2001 From: Steven Date: Thu, 31 Mar 2022 14:06:58 +0800 Subject: [PATCH 15/15] Update specs/opcode/15ISZERO.md Co-authored-by: Haichen Shen --- specs/opcode/15ISZERO.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/specs/opcode/15ISZERO.md b/specs/opcode/15ISZERO.md index 5a9997068..5bc6178b7 100644 --- a/specs/opcode/15ISZERO.md +++ b/specs/opcode/15ISZERO.md @@ -23,4 +23,4 @@ Pop an EVM word `value` from the stack. If it is zero, push `1` back to the stac ## Code -See `src/zkevm_specs/opcode/iszero.py` +See `src/zkevm_specs/evm/execution/iszero.py`