Bitwise opcode spec (AND, OR, XOR)

specs/opcode/16AND_17OR_18XOR.md

@@ -0,0 +1,39 @@
+# AND, OR, XOR op code
+
+## Procedure
+
+Pop two EVM words `a` and `b` from the stack, and the output `c` is pushed to
+the stack.
+
+`a`, `b`, and `c` are all EVM words. We break three EVM words into 32 bytes and
+apply the lookup to the 32 chunks of `a`, `b`, and `c` to see if
+`a[i] OP b[i] == c[i]` holds for `i = 0..32`, where `OP` belongs to
+`[AND, OR, XOR]`.
+
+## Constraints
+
+1. opcodeId checks
+    - opId == OpcodeId(0x16) for `AND`
+    - opId == OpcodeId(0x17) for `OR`
+    - opId == OpcodeId(0x18) for `XOR`
+2. state transition:
+    - gc + 3
+    - stack_pointer + 1
+    - pc + 1
+    - gas + 3
+3. Lookups: 35 busmapping lookups
+    - `a` is at the top of the stack
+    - `b` is at the second position of the stack
+    - `c`, the result, is at the new top of the stack
+    - Apply the lookup to 32 tuples of `a, b, c` chunks,
+        `(a[i], b[i], c[i]), i = 0..32`, with opcode corresponding table
+        (`BitwiseAnd`, `BitwiseOr`, and `BitwiseXor`).
+
+## Exceptions
+
+1. stack underflow: `1023 <= stack_pointer <= 1024`
+2. out of gas: remaining gas is not enough
+
+## Code
+
+See `src/zkevm_specs/opcode/bitwise.py`

src/zkevm_specs/opcode/__init__.py

@@ -1,4 +1,5 @@
 from .add_sub import *
+from .bitwise import *
 from .byte import *
 from .comparator import *
 from .lt_gt import *

src/zkevm_specs/opcode/bitwise.py

@@ -0,0 +1,35 @@
+from typing import Sequence
+from ..encoding import U8, is_circuit_code
+
+@is_circuit_code
+def check_and(
+    a8s: Sequence[U8],
+    b8s: Sequence[U8],
+    c8s: Sequence[U8],
+):
+    assert len(a8s) == len(b8s) == len(c8s) == 32
+    for i in range(32):
+        assert a8s[i] & b8s[i] == c8s[i]
+
+
+@is_circuit_code
+def check_or(
+    a8s: Sequence[U8],
+    b8s: Sequence[U8],
+    c8s: Sequence[U8],
+):
+    assert len(a8s) == len(b8s) == len(c8s) == 32
+    for i in range(32):
+        assert a8s[i] | b8s[i] == c8s[i]
+
+
+
+@is_circuit_code
+def check_xor(
+    a8s: Sequence[U8],
+    b8s: Sequence[U8],
+    c8s: Sequence[U8],
+):
+    assert len(a8s) == len(b8s) == len(c8s) == 32
+    for i in range(32):
+        assert a8s[i] ^ b8s[i] == c8s[i]

tests/test_bitwise.py

@@ -0,0 +1,38 @@
+import random
+import pytest
+
+from zkevm_specs.encoding import u256_to_u8s, u8s_to_u256
+from zkevm_specs.opcode import check_and, check_or, check_xor
+
+
+def test_and():
+    for _ in range(5):
+        a = random.randint(0, 2**256)
+        b = random.randint(0, 2**256)
+        c = a & b
+        a8s = u256_to_u8s(a)
+        b8s = u256_to_u8s(b)
+        c8s = u256_to_u8s(c)
+        check_and(a8s, b8s, c8s)
+
+
+def test_check_or():
+    for _ in range(5):
+        a = random.randint(0, 2**256)
+        b = random.randint(0, 2**256)
+        c = a | b
+        a8s = u256_to_u8s(a)
+        b8s = u256_to_u8s(b)
+        c8s = u256_to_u8s(c)
+        check_or(a8s, b8s, c8s)
+
+def test_check_xor():
+    for i in range(5):
+        print(i)
+        a = random.randint(0, 2**256)
+        b = random.randint(0, 2**256)
+        c = a ^ b
+        a8s = u256_to_u8s(a)
+        b8s = u256_to_u8s(b)
+        c8s = u256_to_u8s(c)
+        check_xor(a8s, b8s, c8s)