Spec for opcode SHL

specs/opcode/1bSHL_1cSHR.md

@@ -0,0 +1,57 @@
+# SHL and SHR opcodes
+
+## Procedure
+
+### EVM behavior
+
+Pop two EVM words `shift` and `a` from the stack, and push `b` to the stack, where `b` is computed as
+
+- for opcode SHL, `shift` is a number of bits to shift to the left, compute `b = (a * 2^shift) % 2^256` when `shift < 256` otherwise `b = 0`
+- for opcode SHR, `shift` is a number of bits to shift to the right, compute `b = a // 2^shift` when `shift < 256` otherwise `b = 0`
+
+### Circuit behavior
+
+To prove the SHL and SHR opcodes, we first construct a `MulAddWordsGadget` that proves `quotient * divisor + remainder = dividend (% 2^256)` where quotient, divisor, remainder and dividend are all 256-bit words. Reference `02MUL_04DIV_06MOD.md` for details about `MulAddWordsGadget`.
+
+Based on different opcode cases, we constrain the stack pops and pushes as follows
+
+- for opcode SHL, two stack pops are shift and quotient, when `divisor = 2^shift` if `shift < 256` and 0 otherwise. The stack push is dividend if `shift < 256` and 0 otherwise.
+- for opcode SHR, two stack pops are shift and dividend, when `divisor = 2^shift` if `shift < 256` and 0 otherwise. The stack push is quotient if `shift < 256` and 0 otherwise.
+
+The opcode circuit also adds some extra constraints:
+
+- contrain `shift == shift.cells[0]` when `divisor != 0`.
+- use a `LtWordGadget` to constrain `remainder < divisor` when `divisor != 0`.
+- if the opcode is SHL, constrain `remainder == 0`.
+- if the opcode is SHR, constrain `overflow == 0` in `MulAddWordsGadget`.
+
+## Constraints
+
+1. opcodeId checks
+   - opId === OpcodeId(0x1b) for SHL
+   - opId === OpcodeId(0x1c) for SHR
+2. state transition:
+   - gc + 3
+   - stack_pointer + 1
+   - pc + 1
+   - gas + 3
+3. Lookups: 1 pow2 lookup + 3 busmapping lookups
+   - divisor lookup in pow2 table (where 0≤shf0<256)  
+      - when `shf0 < 128`, constrain `divisor_lo == 2^shf0`.
+      - when `shf0 >= 128`, constrain `divisor_hi == 2^(shf0 - 128)`.
+   - top of the stack
+      - when opcode is SHL, quotient is at the top of the stack.
+      - when opcode is SHR, dividend is at the top of the stack.
+   - shift is at the second position of the stack when `divisor = 2^shift`.
+   - new top of the stack
+      - when opcode is SHL, dividend is at the new top of the stack.
+      - when opcode is SHR, quotient is at the new top of the stack if `divisor != 0` otherwise 0.
+
+## Exceptions
+
+1. stack underflow: `1023 <= stack_pointer <= 1024`
+2. out of gas: remaining gas is not enough
+
+## Code
+
+See `src/zkevm_specs/evm/execution/shl_shr.py`

src/zkevm_specs/evm/execution/__init__.py

@@ -33,10 +33,10 @@
 from .selfbalance import *
 from .extcodehash import *
 from .log import *
-from .sha3 import sha3
-from .shr import shr
 from .bitwise import not_opcode
 from .sdiv_smod import sdiv_smod
+from .sha3 import sha3
+from .shl_shr import shl_shr
 from .stop import stop
 from .return_ import *
 
@@ -73,8 +73,8 @@
     ExecutionState.LOG: log,
     ExecutionState.CALL: call,
     ExecutionState.ISZERO: iszero,
-    ExecutionState.SHR: shr,
     ExecutionState.SDIV_SMOD: sdiv_smod,
+    ExecutionState.SHL_SHR: shl_shr,
     ExecutionState.STOP: stop,
     ExecutionState.RETURN: return_,
 }

src/zkevm_specs/evm/execution/shl_shr.py

@@ -0,0 +1,119 @@
+from ...util import FQ, RLC
+from ..instruction import Instruction, Transition
+from ..opcode import Opcode
+
+
+def shl_shr(instruction: Instruction):
+    opcode = instruction.opcode_lookup(True)
+
+    pop1 = instruction.stack_pop()
+    pop2 = instruction.stack_pop()
+    push = instruction.stack_push()
+
+    (
+        is_shl,
+        shf0,
+        shift,
+        dividend,
+        divisor,
+        quotient,
+        remainder,
+    ) = gen_witness(opcode, pop1, pop2, push)
+    check_witness(
+        instruction,
+        is_shl,
+        shf0,
+        shift,
+        dividend,
+        divisor,
+        quotient,
+        remainder,
+        pop1,
+        pop2,
+        push,
+    )
+
+    instruction.step_state_transition_in_same_context(
+        opcode,
+        rw_counter=Transition.delta(3),
+        program_counter=Transition.delta(1),
+        stack_pointer=Transition.delta(1),
+    )
+
+
+def check_witness(
+    instruction: Instruction,
+    is_shl: FQ,
+    shf0: FQ,
+    shift: RLC,
+    dividend: RLC,
+    divisor: RLC,
+    quotient: RLC,
+    remainder: RLC,
+    pop1: RLC,
+    pop2: RLC,
+    push: RLC,
+):
+    is_shr = 1 - is_shl
+    divisor_is_zero = instruction.word_is_zero(divisor)
+
+    # Constrain stack pops and pushes as:
+    # - for SHL, two pops are shift and quotient, and push is dividend.
+    # - for SHR, two pops are shift and dividend, and push is quotient.
+    instruction.constrain_equal(pop1.expr(), shift.expr())
+    instruction.constrain_equal(
+        pop2.expr(),
+        is_shl * quotient.expr() + is_shr * dividend.expr(),
+    )
+    instruction.constrain_equal(
+        push.expr(), (is_shl * dividend.expr() + is_shr * quotient.expr()) * (1 - divisor_is_zero)
+    )
+
+    # Constrain shift == shift.cells[0] when divisor != 0.
+    instruction.constrain_zero(
+        (1 - divisor_is_zero) * (shift.expr() - shift.le_bytes[0]),
+    )
+
+    # Constrain remainder < divisor when divisor != 0.
+    remainder_lt_divisor, _ = instruction.compare_word(remainder, divisor)
+    instruction.constrain_zero((1 - divisor_is_zero) * (1 - remainder_lt_divisor))
+
+    # Constrain remainder == 0 for SHL.
+    remainder_is_zero = instruction.word_is_zero(remainder)
+    instruction.constrain_zero(is_shl * (1 - remainder_is_zero))
+
+    # Constrain overflow == 0 for SHR.
+    overflow = instruction.mul_add_words(quotient, divisor, remainder, dividend)
+    instruction.constrain_zero(is_shr * overflow)
+
+    # Constrain divisor_lo == 2^shf0 when shf0 < 128, and
+    # divisor_hi == 2^(128 - shf0) otherwise.
+    divisor_lo = instruction.bytes_to_fq(divisor.le_bytes[:16])
+    divisor_hi = instruction.bytes_to_fq(divisor.le_bytes[16:])
+    if (1 - divisor_is_zero) == 1:
+        instruction.pow2_lookup(shf0, divisor_lo, divisor_hi)
+
+
+def gen_witness(opcode: FQ, pop1: RLC, pop2: RLC, push: RLC):
+    is_shl = Opcode.SHR - opcode
+    shift = pop1
+    shf0 = shift.le_bytes[0]
+    divisor = RLC(1 << shf0) if shf0 == shift.int_value else RLC(0)
+    if is_shl.n == 1:
+        dividend = push
+        quotient = pop2
+        remainder = RLC(0)
+    else:  # SHR
+        dividend = pop2
+        quotient = push
+        remainder = RLC(dividend.int_value - quotient.int_value * divisor.int_value)
+
+    return (
+        is_shl,
+        shf0,
+        shift,
+        dividend,
+        divisor,
+        quotient,
+        remainder,
+    )