From e64407b97b6665a0f09e37cf15a88ca26064c078 Mon Sep 17 00:00:00 2001 From: Rohit Narurkar Date: Tue, 11 Jan 2022 17:34:55 +0800 Subject: [PATCH 1/7] feat: add specs and tests for SLT and SGT opcodes --- specs/opcode/12SLT_13SGT.md | 38 ++++++++++++++++ src/zkevm_specs/evm/execution/__init__.py | 1 + src/zkevm_specs/evm/execution/slt_sgt.py | 49 ++++++++++++++++++++ src/zkevm_specs/opcode/__init__.py | 1 + src/zkevm_specs/opcode/slt_sgt.py | 55 +++++++++++++++++++++++ tests/common.py | 2 + tests/test_slt_sgt.py | 39 ++++++++++++++++ 7 files changed, 185 insertions(+) create mode 100644 specs/opcode/12SLT_13SGT.md create mode 100644 src/zkevm_specs/evm/execution/slt_sgt.py create mode 100644 src/zkevm_specs/opcode/slt_sgt.py create mode 100644 tests/test_slt_sgt.py diff --git a/specs/opcode/12SLT_13SGT.md b/specs/opcode/12SLT_13SGT.md new file mode 100644 index 000000000..a69ce6f27 --- /dev/null +++ b/specs/opcode/12SLT_13SGT.md @@ -0,0 +1,38 @@ +# SLT & SGT opcode + +## Procedure + +The `SLT` and `SGT` opcodes compare the top two values on the stack, and push the result (0 or 1) back to the stack. + +The stack inputs `a` and `b` are 256-bits signed integers with the most significant bit being the sign (1 for negative and 0 for positive). The 256-bits are in the two's complement form of representing signed integers. + +#### Circuit Behaviour + +The `SignedComparatorGadget` takes arguments `a: [u8; 32]`, `b: [u8; 32]` and `is_sgt: bool`. + +It returns the result of `a < b` where: +- `Stack = [b, a]` if `is_sgt == false` +- `Stack = [a, b]` if `is_sgt == true` + +## Constraints +- `OpcodeId` check: + - opId === OpcodeId(0x12) for `SLT` + - opId === OpcodeId(0x13) for `SGT` +- State Transition: + - gc -> gc + 3 + - stack pointer -> stack pointer + 1 + - pc -> pc + 1 + - gas -> gas + 3 +- Lookups: + - `a` is at the top of the stack + - `b` is at the second position of the stack + - `result` is the new top of the stack + +## Exceptions + +1. Stack underflow: `1023 <= stack pointer <= 1024` +2. Out of gas: gas left < 3 + +## Code + +See [`src/zkevm_specs/opcode/slt_sgt.py`](../../src/zkevm_specs/evm/execution/slt_sgt.py) diff --git a/src/zkevm_specs/evm/execution/__init__.py b/src/zkevm_specs/evm/execution/__init__.py index 429364adc..abe0dd407 100644 --- a/src/zkevm_specs/evm/execution/__init__.py +++ b/src/zkevm_specs/evm/execution/__init__.py @@ -13,6 +13,7 @@ from .push import * from .block_coinbase import * from .caller import * +from .slt_sgt import * EXECUTION_STATE_IMPL: Dict[ExecutionState, Callable] = { diff --git a/src/zkevm_specs/evm/execution/slt_sgt.py b/src/zkevm_specs/evm/execution/slt_sgt.py new file mode 100644 index 000000000..cd373f045 --- /dev/null +++ b/src/zkevm_specs/evm/execution/slt_sgt.py @@ -0,0 +1,49 @@ +from ..instruction import Instruction, Transition +from ..opcode import Opcode + +from zkevm_specs.encoding import U256, u256_to_u8s + +def scmp(instruction: Instruction): + opcode = instruction.opcode_lookup(True) + + is_sgt, _ = instruction.pair_select(opcode, Opcode.SGT, Opcode.LGT) + + a = instruction.stack_pop() + b = instruction.stack_pop() + c = instruction.stack_push() + + a8s = u256_to_u8s(U256(a)) + b8s = u256_to_u8s(U256(b)) + c8s = u256_to_u8s(U256(c)) + + # if both a and b are unsigned + if a8s[0] < 128 and b8s[0] < 128: + instruction.constrain_equal( + instruction.select(is_sgt, b < a, a < b), + c, + ) + # only a is unsigned + elif a8s[0] < 128: + instruction.constrain_equal( + instruction.select(is_sgt, 1, 0), + c, + ) + # only b is unsigned + elif b8s[0] < 128: + instruction.constrain_equal( + instruction.select(is_sgt, 0, 1), + c, + ) + # both a and b are signed + else: + instruction.constrain_equal( + instruction.select(is_sgt, a < b, b < a), + c, + ) + + instruction.constrain_same_context_state_transition( + opcode, + rw_counter=Transition.delta(3), + program_counter=Transition.delta(1), + stack_pointer=Transition.delta(1), + ) diff --git a/src/zkevm_specs/opcode/__init__.py b/src/zkevm_specs/opcode/__init__.py index cff0a7ce0..1343e96ba 100644 --- a/src/zkevm_specs/opcode/__init__.py +++ b/src/zkevm_specs/opcode/__init__.py @@ -3,6 +3,7 @@ from .byte import * from .comparator import * from .lt_gt import * +from .slt_sgt import * from .stack import * from .mload_mstore import * from .msize import * diff --git a/src/zkevm_specs/opcode/slt_sgt.py b/src/zkevm_specs/opcode/slt_sgt.py new file mode 100644 index 000000000..4d8de63dd --- /dev/null +++ b/src/zkevm_specs/opcode/slt_sgt.py @@ -0,0 +1,55 @@ +from typing import Sequence + +from ..encoding import is_circuit_code, U8, U256, u8s_to_u256 + +def slt_circuit( + a8s: Sequence[U8], + b8s: Sequence[U8], + result8s: Sequence[U8], +): + """ + Check if `a8s < b8s` and set `result8s = 1` if that is the case, else set `result8s = 0`. + """ + assert len(a8s) == len(b8s) == len(result8s) == 32 + + # result is binary + assert result8s[0] in [0, 1] + for i in range(1, 32): + assert result8s[i] == 0 + + # encode a8s and b8s to U256 + aa = u8s_to_u256(a8s) + bb = u8s_to_u256(b8s) + + # if a and b (two's complement form) both are unsigned + if a8s[0] < 128 and b8s[0] < 128: + assert result8s[0] == (aa < bb) + # only a is unsigned + elif a8s[0] < 128: + assert result8s[0] == 1 + # only b is unsigned + elif b8s[0] < 128: + assert result8s[0] == 0 + # both a and b are signed, reverse our check + else: + assert result8s[0] == (bb < aa) + +@is_circuit_code +def check_slt( + a8s: Sequence[U8], + b8s: Sequence[U8], + result8s: Sequence[U8], + is_sgt: bool, +): + assert not is_sgt + slt_circuit(a8s, b8s, result8s) + +@is_circuit_code +def check_sgt( + a8s: Sequence[U8], + b8s: Sequence[U8], + result8s: Sequence[U8], + is_sgt: bool, +): + assert is_sgt + slt_circuit(b8s, a8s, result8s) diff --git a/tests/common.py b/tests/common.py index 6e700b676..5fad7994c 100644 --- a/tests/common.py +++ b/tests/common.py @@ -18,4 +18,6 @@ (65536, 65536), ((1 << 256) - 1, (1 << 256) - 2), ((1 << 256) - 2, (1 << 256) - 1), + ((1 << 256) - 1, 0), + (0, (1 << 256) - 1), ) diff --git a/tests/test_slt_sgt.py b/tests/test_slt_sgt.py new file mode 100644 index 000000000..477392f15 --- /dev/null +++ b/tests/test_slt_sgt.py @@ -0,0 +1,39 @@ +import pytest + +from zkevm_specs.encoding import u256_to_u8s, U256 +from zkevm_specs.opcode import check_slt, check_sgt +from zkevm_specs.opcode.stack import Stack +from common import NASTY_AB_VALUES + +def gen_slt_sgt_witness(a: U256, b: U256, is_sgt: bool): + a8s = u256_to_u8s(a) + b8s = u256_to_u8s(b) + result8s = [0] * 32 + + (aa, aa8s) = (b, b8s) if is_sgt else (a, a8s) + (bb, bb8s) = (a, a8s) if is_sgt else (b, b8s) + + # both a and b are unsigned + if aa8s[0] < 128 and bb8s[0] < 128: + result8s[0] = int(aa < bb) + # only a is unsigned + elif aa8s[0] < 128: + result8s[0] = 1 + # only b is unsigned + elif bb8s[0] < 128: + result8s[0] = 0 + # both are signed + else: + result8s[0] = int(bb < aa) + + return a8s, b8s, result8s + +@pytest.mark.parametrize("a,b", NASTY_AB_VALUES) +def test_slt(a, b): + a8s, b8s, result8s = gen_slt_sgt_witness(a, b, False) + check_slt(a8s, b8s, result8s, False) + +@pytest.mark.parametrize("a,b", NASTY_AB_VALUES) +def test_sgt(a, b): + a8s, b8s, result8s = gen_slt_sgt_witness(a, b, True) + check_sgt(a8s, b8s, result8s, True) From 3e51cc2358065b715dc9ef39cb11ae0aaca532c0 Mon Sep 17 00:00:00 2001 From: Rohit Narurkar Date: Thu, 13 Jan 2022 11:34:45 +0800 Subject: [PATCH 2/7] fix: comments and refactoring --- specs/opcode/12SLT_13SGT.md | 21 ++++++++- src/zkevm_specs/evm/execution/slt_sgt.py | 38 ++++++++-------- src/zkevm_specs/opcode/__init__.py | 1 - src/zkevm_specs/opcode/slt_sgt.py | 55 ------------------------ tests/test_slt_sgt.py | 16 +++---- 5 files changed, 44 insertions(+), 87 deletions(-) delete mode 100644 src/zkevm_specs/opcode/slt_sgt.py diff --git a/specs/opcode/12SLT_13SGT.md b/specs/opcode/12SLT_13SGT.md index a69ce6f27..d0c64bafb 100644 --- a/specs/opcode/12SLT_13SGT.md +++ b/specs/opcode/12SLT_13SGT.md @@ -14,6 +14,25 @@ It returns the result of `a < b` where: - `Stack = [b, a]` if `is_sgt == false` - `Stack = [a, b]` if `is_sgt == true` +The gadget is constructed with the following logic: +``` +if a_0 >= 128 and b_0 < 128: + result = 1 +elif b_0 >= 128 and a_0 < 128: + result = 0 +else: + if a_hi < b_hi: + result = 1 + elif a_hi == b_hi and a_lo < b_lo: + result = 1 + else: + result = 0 +``` +where: +- `a_0` and `b_0` represent the most significant bytes of `a` and `b` respectively. +- `a_0 >= 128` (same for `b`) signifies that `a` (same for `b`) is a negative number. +- `a_hi = a[0..16]` and `a_lo = a[16..32]` (same for `b`) with `a` (same for `b`) being represented in the big-endian form. + ## Constraints - `OpcodeId` check: - opId === OpcodeId(0x12) for `SLT` @@ -35,4 +54,4 @@ It returns the result of `a < b` where: ## Code -See [`src/zkevm_specs/opcode/slt_sgt.py`](../../src/zkevm_specs/evm/execution/slt_sgt.py) +See [`slt_sgt.py`](../../src/zkevm_specs/evm/execution/slt_sgt.py) diff --git a/src/zkevm_specs/evm/execution/slt_sgt.py b/src/zkevm_specs/evm/execution/slt_sgt.py index cd373f045..ff9477bd1 100644 --- a/src/zkevm_specs/evm/execution/slt_sgt.py +++ b/src/zkevm_specs/evm/execution/slt_sgt.py @@ -1,8 +1,6 @@ from ..instruction import Instruction, Transition from ..opcode import Opcode -from zkevm_specs.encoding import U256, u256_to_u8s - def scmp(instruction: Instruction): opcode = instruction.opcode_lookup(True) @@ -12,33 +10,33 @@ def scmp(instruction: Instruction): b = instruction.stack_pop() c = instruction.stack_push() - a8s = u256_to_u8s(U256(a)) - b8s = u256_to_u8s(U256(b)) - c8s = u256_to_u8s(U256(c)) + # decode RLC to bytes for a and b + a8s = instruction.rlc_to_bytes(a, 32) + b8s = instruction.rlc_to_bytes(b, 32) + aa = instruction.bytes_to_int(a8s) + bb = instruction.bytes_to_int(b8s) + cc = instruction.bytes_to_int(instruction.rlc_to_bytes(c, 32)) - # if both a and b are unsigned - if a8s[0] < 128 and b8s[0] < 128: - instruction.constrain_equal( - instruction.select(is_sgt, b < a, a < b), - c, - ) - # only a is unsigned - elif a8s[0] < 128: + # c is the result and hence should be binary + instruction.constrain_bool(cc) + + # a is positive and b is negative + if a8s[0] < 128 and b8s[0] >= 128: instruction.constrain_equal( instruction.select(is_sgt, 1, 0), - c, + cc, ) - # only b is unsigned - elif b8s[0] < 128: + # b is negative and a is positive + elif b8s[0] < 128 and a8s[0] >= 128: instruction.constrain_equal( instruction.select(is_sgt, 0, 1), - c, + cc, ) - # both a and b are signed + # both a and b are of the same sign (positive/negative) else: instruction.constrain_equal( - instruction.select(is_sgt, a < b, b < a), - c, + instruction.select(is_sgt, int(bb < aa), int(aa < bb)), + cc, ) instruction.constrain_same_context_state_transition( diff --git a/src/zkevm_specs/opcode/__init__.py b/src/zkevm_specs/opcode/__init__.py index 1343e96ba..cff0a7ce0 100644 --- a/src/zkevm_specs/opcode/__init__.py +++ b/src/zkevm_specs/opcode/__init__.py @@ -3,7 +3,6 @@ from .byte import * from .comparator import * from .lt_gt import * -from .slt_sgt import * from .stack import * from .mload_mstore import * from .msize import * diff --git a/src/zkevm_specs/opcode/slt_sgt.py b/src/zkevm_specs/opcode/slt_sgt.py deleted file mode 100644 index 4d8de63dd..000000000 --- a/src/zkevm_specs/opcode/slt_sgt.py +++ /dev/null @@ -1,55 +0,0 @@ -from typing import Sequence - -from ..encoding import is_circuit_code, U8, U256, u8s_to_u256 - -def slt_circuit( - a8s: Sequence[U8], - b8s: Sequence[U8], - result8s: Sequence[U8], -): - """ - Check if `a8s < b8s` and set `result8s = 1` if that is the case, else set `result8s = 0`. - """ - assert len(a8s) == len(b8s) == len(result8s) == 32 - - # result is binary - assert result8s[0] in [0, 1] - for i in range(1, 32): - assert result8s[i] == 0 - - # encode a8s and b8s to U256 - aa = u8s_to_u256(a8s) - bb = u8s_to_u256(b8s) - - # if a and b (two's complement form) both are unsigned - if a8s[0] < 128 and b8s[0] < 128: - assert result8s[0] == (aa < bb) - # only a is unsigned - elif a8s[0] < 128: - assert result8s[0] == 1 - # only b is unsigned - elif b8s[0] < 128: - assert result8s[0] == 0 - # both a and b are signed, reverse our check - else: - assert result8s[0] == (bb < aa) - -@is_circuit_code -def check_slt( - a8s: Sequence[U8], - b8s: Sequence[U8], - result8s: Sequence[U8], - is_sgt: bool, -): - assert not is_sgt - slt_circuit(a8s, b8s, result8s) - -@is_circuit_code -def check_sgt( - a8s: Sequence[U8], - b8s: Sequence[U8], - result8s: Sequence[U8], - is_sgt: bool, -): - assert is_sgt - slt_circuit(b8s, a8s, result8s) diff --git a/tests/test_slt_sgt.py b/tests/test_slt_sgt.py index 477392f15..fd754596a 100644 --- a/tests/test_slt_sgt.py +++ b/tests/test_slt_sgt.py @@ -2,7 +2,6 @@ from zkevm_specs.encoding import u256_to_u8s, U256 from zkevm_specs.opcode import check_slt, check_sgt -from zkevm_specs.opcode.stack import Stack from common import NASTY_AB_VALUES def gen_slt_sgt_witness(a: U256, b: U256, is_sgt: bool): @@ -13,18 +12,15 @@ def gen_slt_sgt_witness(a: U256, b: U256, is_sgt: bool): (aa, aa8s) = (b, b8s) if is_sgt else (a, a8s) (bb, bb8s) = (a, a8s) if is_sgt else (b, b8s) - # both a and b are unsigned - if aa8s[0] < 128 and bb8s[0] < 128: - result8s[0] = int(aa < bb) - # only a is unsigned - elif aa8s[0] < 128: + # a < 0 and b >= 0 + if aa8s[0] >= 128 and bb8s[0] < 128: result8s[0] = 1 - # only b is unsigned - elif bb8s[0] < 128: + # b < 0 and a >= 0 + elif bb8s[0] >= 128 and aa8s[0] < 128: result8s[0] = 0 - # both are signed + # (a >= 0 and b >= 0) or (a < 0 and b < 0) else: - result8s[0] = int(bb < aa) + result8s[0] = int(aa < bb) return a8s, b8s, result8s From 97c822ee1faf4f1be3d8e76235e371f9f8abbf27 Mon Sep 17 00:00:00 2001 From: Rohit Narurkar Date: Thu, 13 Jan 2022 16:07:43 +0800 Subject: [PATCH 3/7] feat: tests for SGT/SLT (refactored) --- specs/opcode/12SLT_13SGT.md | 42 +++-- src/zkevm_specs/evm/execution/__init__.py | 1 + src/zkevm_specs/evm/execution/slt_sgt.py | 60 +++--- tests/evm/test_slt_sgt.py | 213 ++++++++++++++++++++++ tests/test_slt_sgt.py | 35 ---- 5 files changed, 272 insertions(+), 79 deletions(-) create mode 100644 tests/evm/test_slt_sgt.py delete mode 100644 tests/test_slt_sgt.py diff --git a/specs/opcode/12SLT_13SGT.md b/specs/opcode/12SLT_13SGT.md index d0c64bafb..72be95629 100644 --- a/specs/opcode/12SLT_13SGT.md +++ b/specs/opcode/12SLT_13SGT.md @@ -11,15 +11,22 @@ The stack inputs `a` and `b` are 256-bits signed integers with the most signific The `SignedComparatorGadget` takes arguments `a: [u8; 32]`, `b: [u8; 32]` and `is_sgt: bool`. It returns the result of `a < b` where: + - `Stack = [b, a]` if `is_sgt == false` - `Stack = [a, b]` if `is_sgt == true` +We basically swap the stack inputs if `is_sgt == true`, so that we only need to compare `a < b` in our gadget. + The gadget is constructed with the following logic: -``` -if a_0 >= 128 and b_0 < 128: + +```python +# a < 0 and b >= 0 +if a[31] >= 128 and b[31] < 128: result = 1 -elif b_0 >= 128 and a_0 < 128: +# b < 0 and a >= 0 +elif b[31] >= 128 and a[31] < 128: result = 0 +# (a < 0 and b < 0) or (a >= 0 and b >= 0) else: if a_hi < b_hi: result = 1 @@ -28,29 +35,32 @@ else: else: result = 0 ``` + where: -- `a_0` and `b_0` represent the most significant bytes of `a` and `b` respectively. -- `a_0 >= 128` (same for `b`) signifies that `a` (same for `b`) is a negative number. -- `a_hi = a[0..16]` and `a_lo = a[16..32]` (same for `b`) with `a` (same for `b`) being represented in the big-endian form. + +- `a[31]` and `b[31]` represent the most significant bytes of `a` and `b` respectively. +- `a[31] >= 128` (same for `b`) signifies that `a` (same for `b`) is a negative number. +- `a_hi = a[16..32]` and `a_lo = a[0..16]` (same for `b`) with `a` (same for `b`) being represented in the little-endian form. ## Constraints + - `OpcodeId` check: - - opId === OpcodeId(0x12) for `SLT` - - opId === OpcodeId(0x13) for `SGT` + - opId === OpcodeId(0x12) for `SLT` + - opId === OpcodeId(0x13) for `SGT` - State Transition: - - gc -> gc + 3 - - stack pointer -> stack pointer + 1 - - pc -> pc + 1 - - gas -> gas + 3 + - gc -> gc + 3 + - stack pointer -> stack pointer + 1 + - pc -> pc + 1 + - gas -> gas + 3 - Lookups: - - `a` is at the top of the stack - - `b` is at the second position of the stack - - `result` is the new top of the stack + - `a` is at the top of the stack + - `b` is at the second position of the stack + - `result` is the new top of the stack ## Exceptions 1. Stack underflow: `1023 <= stack pointer <= 1024` -2. Out of gas: gas left < 3 +2. Out of gas: gas left \< 3 ## Code diff --git a/src/zkevm_specs/evm/execution/__init__.py b/src/zkevm_specs/evm/execution/__init__.py index abe0dd407..5163c12c2 100644 --- a/src/zkevm_specs/evm/execution/__init__.py +++ b/src/zkevm_specs/evm/execution/__init__.py @@ -26,4 +26,5 @@ ExecutionState.JUMP: jump, ExecutionState.JUMPI: jumpi, ExecutionState.PUSH: push, + ExecutionState.SCMP: scmp, } diff --git a/src/zkevm_specs/evm/execution/slt_sgt.py b/src/zkevm_specs/evm/execution/slt_sgt.py index ff9477bd1..58f28badc 100644 --- a/src/zkevm_specs/evm/execution/slt_sgt.py +++ b/src/zkevm_specs/evm/execution/slt_sgt.py @@ -1,45 +1,49 @@ +from typing import Sequence, Tuple + from ..instruction import Instruction, Transition from ..opcode import Opcode + def scmp(instruction: Instruction): opcode = instruction.opcode_lookup(True) - is_sgt, _ = instruction.pair_select(opcode, Opcode.SGT, Opcode.LGT) + is_sgt, _ = instruction.pair_select(opcode, Opcode.SGT, Opcode.SLT) a = instruction.stack_pop() b = instruction.stack_pop() c = instruction.stack_push() + # swap a and b if the opcode is SGT + aa = b if is_sgt else a + bb = a if is_sgt else b + # decode RLC to bytes for a and b - a8s = instruction.rlc_to_bytes(a, 32) - b8s = instruction.rlc_to_bytes(b, 32) - aa = instruction.bytes_to_int(a8s) - bb = instruction.bytes_to_int(b8s) - cc = instruction.bytes_to_int(instruction.rlc_to_bytes(c, 32)) - - # c is the result and hence should be binary - instruction.constrain_bool(cc) - - # a is positive and b is negative - if a8s[0] < 128 and b8s[0] >= 128: - instruction.constrain_equal( - instruction.select(is_sgt, 1, 0), - cc, - ) - # b is negative and a is positive - elif b8s[0] < 128 and a8s[0] >= 128: - instruction.constrain_equal( - instruction.select(is_sgt, 0, 1), - cc, - ) - # both a and b are of the same sign (positive/negative) + a8s = instruction.rlc_to_le_bytes(aa) + b8s = instruction.rlc_to_le_bytes(bb) + c8s = instruction.rlc_to_le_bytes(c) + + a_lo = int.from_bytes(a8s[:16], "little") + a_hi = int.from_bytes(a8s[16:], "little") + b_lo = int.from_bytes(b8s[:16], "little") + b_hi = int.from_bytes(b8s[16:], "little") + cc = int.from_bytes(c8s, "little") + + a_lt_b_lo, a_eq_b_lo = instruction.compare(a_lo, b_lo, 16) + a_lt_b_hi, a_eq_b_hi = instruction.compare(a_hi, b_hi, 16) + + a_lt_b = instruction.select(a_lt_b_hi, 1, instruction.select(a_eq_b_hi * a_lt_b_lo, 1, 0)) + + # a < 0 and b >= 0 => a < b == true + if a8s[31] >= 128 and b8s[31] < 128: + instruction.constrain_equal(cc, 1) + # b < 0 and a >= 0 => a < b == false + elif b8s[31] >= 128 and a8s[31] < 128: + instruction.constrain_equal(cc, 0) + # (a < 0 and b < 0) or (a >= 0 and b >= 0) else: - instruction.constrain_equal( - instruction.select(is_sgt, int(bb < aa), int(aa < bb)), - cc, - ) + instruction.constrain_equal(cc, a_lt_b) - instruction.constrain_same_context_state_transition( + instruction.step_state_transition_in_same_context( opcode, rw_counter=Transition.delta(3), program_counter=Transition.delta(1), diff --git a/tests/evm/test_slt_sgt.py b/tests/evm/test_slt_sgt.py new file mode 100644 index 000000000..d664381f2 --- /dev/null +++ b/tests/evm/test_slt_sgt.py @@ -0,0 +1,213 @@ +import pytest + +from zkevm_specs.evm import ( + ExecutionState, + StepState, + Opcode, + verify_steps, + Tables, + RWTableTag, + RW, + Block, + Bytecode, +) +from zkevm_specs.util import rand_fp, rand_word, RLC + +RAND_1 = rand_word() + +RAND_2 = rand_word() + +TESTING_DATA = ( + # a >= 0 and b >= 0 + ( + Opcode.SLT, + 0x00, + 0x01, + 0x01, + ), + ( + Opcode.SGT, + 0x00, + 0x01, + 0x00, + ), + ( + Opcode.SLT, + 0x01, + 0x00, + 0x00, + ), + ( + Opcode.SGT, + 0x01, + 0x00, + 0x01, + ), + # a < 0 and b >= 0 + ( + Opcode.SLT, + 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF, + 0x00, + 0x01, + ), + ( + Opcode.SGT, + 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF, + 0x00, + 0x00, + ), + ( + Opcode.SLT, + 0x00, + 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF, + 0x00, + ), + ( + Opcode.SGT, + 0x00, + 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF, + 0x01, + ), + # a < 0 and b < 0 + ( + Opcode.SLT, + 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFE, + 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF, + 0x01, + ), + ( + Opcode.SGT, + 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFE, + 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF, + 0x00, + ), + ( + Opcode.SLT, + 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF, + 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFE, + 0x00, + ), + ( + Opcode.SGT, + 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF, + 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFE, + 0x01, + ), + # a_hi == b_hi and a_lo < b_lo and a < 0 and b < 0 + ( + Opcode.SLT, + 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF11111111111111111111111111111111, + 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF22222222222222222222222222222222, + 0x01, + ), + ( + Opcode.SGT, + 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF11111111111111111111111111111111, + 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF22222222222222222222222222222222, + 0x00, + ), + ( + Opcode.SLT, + 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF22222222222222222222222222222222, + 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF11111111111111111111111111111111, + 0x00, + ), + ( + Opcode.SGT, + 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF22222222222222222222222222222222, + 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF11111111111111111111111111111111, + 0x01, + ), + # a_hi == b_hi and a_lo < b_lo and a >= 0 and b >= 0 + ( + Opcode.SLT, + 0x1111111111111111111111111111111144444444444444444444444444444443, + 0x1111111111111111111111111111111144444444444444444444444444444444, + 0x01, + ), + ( + Opcode.SGT, + 0x1111111111111111111111111111111144444444444444444444444444444443, + 0x1111111111111111111111111111111144444444444444444444444444444444, + 0x00, + ), + ( + Opcode.SLT, + 0x1111111111111111111111111111111144444444444444444444444444444444, + 0x1111111111111111111111111111111144444444444444444444444444444443, + 0x00, + ), + ( + Opcode.SGT, + 0x1111111111111111111111111111111144444444444444444444444444444444, + 0x1111111111111111111111111111111144444444444444444444444444444443, + 0x01, + ), + # both equal + ( + Opcode.SLT, + RAND_1, + RAND_1, + 0x00, + ), + ( + Opcode.SGT, + RAND_2, + RAND_2, + 0x00, + ), +) + + +@pytest.mark.parametrize("opcode, a, b, res", TESTING_DATA) +def test_slt_sgt(opcode: Opcode, a: int, b: int, res: int): + randomness = rand_fp() + + a = RLC(a, randomness) + b = RLC(b, randomness) + res = RLC(res, randomness) + + bytecode = Bytecode().slt(a, b) if opcode == Opcode.SLT else Bytecode().sgt(a, b) + 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( + [ + (9, RW.Read, RWTableTag.Stack, 1, 1022, a, 0, 0), + (10, RW.Read, RWTableTag.Stack, 1, 1023, b, 0, 0), + (11, RW.Write, RWTableTag.Stack, 1, 1023, res, 0, 0), + ] + ), + ) + + verify_steps( + randomness=randomness, + tables=tables, + steps=[ + StepState( + execution_state=ExecutionState.SCMP, + 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, + ), + ], + ) diff --git a/tests/test_slt_sgt.py b/tests/test_slt_sgt.py deleted file mode 100644 index fd754596a..000000000 --- a/tests/test_slt_sgt.py +++ /dev/null @@ -1,35 +0,0 @@ -import pytest - -from zkevm_specs.encoding import u256_to_u8s, U256 -from zkevm_specs.opcode import check_slt, check_sgt -from common import NASTY_AB_VALUES - -def gen_slt_sgt_witness(a: U256, b: U256, is_sgt: bool): - a8s = u256_to_u8s(a) - b8s = u256_to_u8s(b) - result8s = [0] * 32 - - (aa, aa8s) = (b, b8s) if is_sgt else (a, a8s) - (bb, bb8s) = (a, a8s) if is_sgt else (b, b8s) - - # a < 0 and b >= 0 - if aa8s[0] >= 128 and bb8s[0] < 128: - result8s[0] = 1 - # b < 0 and a >= 0 - elif bb8s[0] >= 128 and aa8s[0] < 128: - result8s[0] = 0 - # (a >= 0 and b >= 0) or (a < 0 and b < 0) - else: - result8s[0] = int(aa < bb) - - return a8s, b8s, result8s - -@pytest.mark.parametrize("a,b", NASTY_AB_VALUES) -def test_slt(a, b): - a8s, b8s, result8s = gen_slt_sgt_witness(a, b, False) - check_slt(a8s, b8s, result8s, False) - -@pytest.mark.parametrize("a,b", NASTY_AB_VALUES) -def test_sgt(a, b): - a8s, b8s, result8s = gen_slt_sgt_witness(a, b, True) - check_sgt(a8s, b8s, result8s, True) From d2dd1e87280bdcc22393e2c99a406473ae4a6bd5 Mon Sep 17 00:00:00 2001 From: Rohit Narurkar Date: Fri, 14 Jan 2022 16:54:30 +0800 Subject: [PATCH 4/7] fix: follow little endianness for decoded inputs a and b (same as circuits) --- specs/opcode/12SLT_13SGT.md | 2 +- tests/evm/test_slt_sgt.py | 26 ++++++++++++++++++++++++++ 2 files changed, 27 insertions(+), 1 deletion(-) diff --git a/specs/opcode/12SLT_13SGT.md b/specs/opcode/12SLT_13SGT.md index 72be95629..1521d678e 100644 --- a/specs/opcode/12SLT_13SGT.md +++ b/specs/opcode/12SLT_13SGT.md @@ -64,4 +64,4 @@ where: ## Code -See [`slt_sgt.py`](../../src/zkevm_specs/evm/execution/slt_sgt.py) +See [`slt_sgt.py`](src/zkevm_specs/evm/execution/slt_sgt.py) diff --git a/tests/evm/test_slt_sgt.py b/tests/evm/test_slt_sgt.py index d664381f2..3597caded 100644 --- a/tests/evm/test_slt_sgt.py +++ b/tests/evm/test_slt_sgt.py @@ -156,6 +156,32 @@ RAND_2, 0x00, ), + + # more cases where contiguous bytes are different + ( + Opcode.SLT, + hex_to_word("1234567812345678123456781234567812345678123456781234567812345678"), + hex_to_word("2345678123456781234567812345678123456781234567812345678123456781"), + hex_to_word("01"), + ), + ( + Opcode.SGT, + hex_to_word("1234567812345678123456781234567812345678123456781234567812345678"), + hex_to_word("2345678123456781234567812345678123456781234567812345678123456781"), + hex_to_word("00"), + ), + ( + Opcode.SLT, + hex_to_word("2345678123456781234567812345678123456781234567812345678123456781"), + hex_to_word("1234567812345678123456781234567812345678123456781234567812345678"), + hex_to_word("00"), + ), + ( + Opcode.SGT, + hex_to_word("2345678123456781234567812345678123456781234567812345678123456781"), + hex_to_word("1234567812345678123456781234567812345678123456781234567812345678"), + hex_to_word("01"), + ), ) From 882d3b0840c523c821b700959690a04becc81d96 Mon Sep 17 00:00:00 2001 From: Rohit Narurkar Date: Fri, 14 Jan 2022 17:43:27 +0800 Subject: [PATCH 5/7] fix: linting --- tests/evm/test_slt_sgt.py | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/evm/test_slt_sgt.py b/tests/evm/test_slt_sgt.py index 3597caded..2a0379683 100644 --- a/tests/evm/test_slt_sgt.py +++ b/tests/evm/test_slt_sgt.py @@ -156,7 +156,6 @@ RAND_2, 0x00, ), - # more cases where contiguous bytes are different ( Opcode.SLT, From bf236b9d3dd14c784176254ed02c1bbd2e3acd34 Mon Sep 17 00:00:00 2001 From: Rohit Narurkar Date: Fri, 14 Jan 2022 17:54:52 +0800 Subject: [PATCH 6/7] fix: lint specs | check only /specs --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index a450b648d..d90c6de50 100644 --- a/Makefile +++ b/Makefile @@ -12,7 +12,7 @@ fmt: ## Format the code lint: ## Check whether the code is formated correctly black . --check - mdformat . --number --check + mdformat specs/ --number --check test: ## Run tests pytest From e166308918765c149ac82919b8b6bcf7e9ade921 Mon Sep 17 00:00:00 2001 From: Rohit Narurkar Date: Thu, 20 Jan 2022 11:03:04 +0800 Subject: [PATCH 7/7] fix: use instruction compare, match specs and circuit --- tests/evm/test_slt_sgt.py | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/tests/evm/test_slt_sgt.py b/tests/evm/test_slt_sgt.py index 2a0379683..7d26ccb5c 100644 --- a/tests/evm/test_slt_sgt.py +++ b/tests/evm/test_slt_sgt.py @@ -159,27 +159,27 @@ # more cases where contiguous bytes are different ( Opcode.SLT, - hex_to_word("1234567812345678123456781234567812345678123456781234567812345678"), - hex_to_word("2345678123456781234567812345678123456781234567812345678123456781"), - hex_to_word("01"), + 0x1234567812345678123456781234567812345678123456781234567812345678, + 0x2345678123456781234567812345678123456781234567812345678123456781, + 0x01, ), ( Opcode.SGT, - hex_to_word("1234567812345678123456781234567812345678123456781234567812345678"), - hex_to_word("2345678123456781234567812345678123456781234567812345678123456781"), - hex_to_word("00"), + 0x1234567812345678123456781234567812345678123456781234567812345678, + 0x2345678123456781234567812345678123456781234567812345678123456781, + 0x00, ), ( Opcode.SLT, - hex_to_word("2345678123456781234567812345678123456781234567812345678123456781"), - hex_to_word("1234567812345678123456781234567812345678123456781234567812345678"), - hex_to_word("00"), + 0x2345678123456781234567812345678123456781234567812345678123456781, + 0x1234567812345678123456781234567812345678123456781234567812345678, + 0x00, ), ( Opcode.SGT, - hex_to_word("2345678123456781234567812345678123456781234567812345678123456781"), - hex_to_word("1234567812345678123456781234567812345678123456781234567812345678"), - hex_to_word("01"), + 0x2345678123456781234567812345678123456781234567812345678123456781, + 0x1234567812345678123456781234567812345678123456781234567812345678, + 0x01, ), )