Opcode SHL

zkevm-circuits/src/evm_circuit/execution.rs

@@ -68,7 +68,7 @@ mod r#return;
 mod sdiv_smod;
 mod selfbalance;
 mod sha3;
-mod shr;
+mod shl_shr;
 mod signed_comparator;
 mod signextend;
 mod sload;
@@ -120,7 +120,7 @@ use push::PushGadget;
 use r#return::ReturnGadget;
 use sdiv_smod::SignedDivModGadget;
 use selfbalance::SelfbalanceGadget;
-use shr::ShrGadget;
+use shl_shr::ShlShrGadget;
 use signed_comparator::SignedComparatorGadget;
 use signextend::SignextendGadget;
 use sload::SloadGadget;
@@ -200,10 +200,9 @@ pub(crate) struct ExecutionConfig<F> {
     sdiv_smod_gadget: SignedDivModGadget<F>,
     selfbalance_gadget: SelfbalanceGadget<F>,
     sha3_gadget: Sha3Gadget<F>,
-    shr_gadget: ShrGadget<F>,
+    shl_shr_gadget: ShlShrGadget<F>,
     balance_gadget: DummyGadget<F, 1, 1, { ExecutionState::BALANCE }>,
     exp_gadget: DummyGadget<F, 2, 1, { ExecutionState::EXP }>,
-    shl_gadget: DummyGadget<F, 2, 1, { ExecutionState::SHL }>,
     sar_gadget: DummyGadget<F, 2, 1, { ExecutionState::SAR }>,
     extcodesize_gadget: DummyGadget<F, 1, 1, { ExecutionState::EXTCODESIZE }>,
     extcodecopy_gadget: DummyGadget<F, 4, 0, { ExecutionState::EXTCODECOPY }>,
@@ -446,7 +445,6 @@ impl<F: Field> ExecutionConfig<F> {
             balance_gadget: configure_gadget!(),
             blockhash_gadget: configure_gadget!(),
             exp_gadget: configure_gadget!(),
-            shl_gadget: configure_gadget!(),
             sar_gadget: configure_gadget!(),
             extcodesize_gadget: configure_gadget!(),
             extcodecopy_gadget: configure_gadget!(),
@@ -458,7 +456,7 @@ impl<F: Field> ExecutionConfig<F> {
             create2_gadget: configure_gadget!(),
             staticcall_gadget: configure_gadget!(),
             selfdestruct_gadget: configure_gadget!(),
-            shr_gadget: configure_gadget!(),
+            shl_shr_gadget: configure_gadget!(),
             signed_comparator_gadget: configure_gadget!(),
             signextend_gadget: configure_gadget!(),
             sload_gadget: configure_gadget!(),
@@ -960,7 +958,6 @@ impl<F: Field> ExecutionConfig<F> {
             // dummy gadgets
             ExecutionState::BALANCE => assign_exec_step!(self.balance_gadget),
             ExecutionState::EXP => assign_exec_step!(self.exp_gadget),
-            ExecutionState::SHL => assign_exec_step!(self.shl_gadget),
             ExecutionState::SAR => assign_exec_step!(self.sar_gadget),
             ExecutionState::EXTCODESIZE => assign_exec_step!(self.extcodesize_gadget),
             ExecutionState::EXTCODECOPY => assign_exec_step!(self.extcodecopy_gadget),
@@ -974,7 +971,7 @@ impl<F: Field> ExecutionConfig<F> {
             ExecutionState::SELFDESTRUCT => assign_exec_step!(self.selfdestruct_gadget),
             // end of dummy gadgets
             ExecutionState::SHA3 => assign_exec_step!(self.sha3_gadget),
-            ExecutionState::SHR => assign_exec_step!(self.shr_gadget),
+            ExecutionState::SHL_SHR => assign_exec_step!(self.shl_shr_gadget),
             ExecutionState::SIGNEXTEND => assign_exec_step!(self.signextend_gadget),
             ExecutionState::SLOAD => assign_exec_step!(self.sload_gadget),
             ExecutionState::SSTORE => assign_exec_step!(self.sstore_gadget),

zkevm-circuits/src/evm_circuit/execution/shl_shr.rs

@@ -0,0 +1,242 @@
+use crate::{
+    evm_circuit::{
+        execution::ExecutionGadget,
+        step::ExecutionState,
+        table::{FixedTableTag, Lookup},
+        util::{
+            self,
+            common_gadget::SameContextGadget,
+            constraint_builder::{ConstraintBuilder, StepStateTransition, Transition::Delta},
+            from_bytes,
+            math_gadget::{IsZeroGadget, LtWordGadget, MulAddWordsGadget},
+            sum, CachedRegion, Cell,
+        },
+        witness::{Block, Call, ExecStep, Transaction},
+    },
+    util::Expr,
+};
+use bus_mapping::evm::OpcodeId;
+use eth_types::{Field, ToLittleEndian, U256};
+use halo2_proofs::plonk::Error;
+
+/// ShlShrGadget verifies opcode SHL and SHR.
+/// For SHL, verify pop1 * (2^pop2) % 2^256 == push;
+/// For SHR, verify pop1 / (2^pop2) % 2^256 == push;
+/// when pop1, pop2, push are 256-bit words.
+#[derive(Clone, Debug)]
+pub(crate) struct ShlShrGadget<F> {
+    same_context: SameContextGadget<F>,
+    quotient: util::Word<F>,
+    divisor: util::Word<F>,
+    remainder: util::Word<F>,
+    dividend: util::Word<F>,
+    /// Shift word
+    shift: util::Word<F>,
+    /// First byte of shift word
+    shf0: Cell<F>,
+    /// Gadget that verifies quotient * divisor + remainder = dividend
+    mul_add_words: MulAddWordsGadget<F>,
+    /// Check if divisor is zero
+    divisor_is_zero: IsZeroGadget<F>,
+    /// Check if remainder is zero
+    remainder_is_zero: IsZeroGadget<F>,
+    /// Check if remainder < divisor when divisor != 0
+    remainder_lt_divisor: LtWordGadget<F>,
+}
+
+impl<F: Field> ExecutionGadget<F> for ShlShrGadget<F> {
+    const NAME: &'static str = "SHL_SHR";
+
+    const EXECUTION_STATE: ExecutionState = ExecutionState::SHL_SHR;
+
+    fn configure(cb: &mut ConstraintBuilder<F>) -> Self {
+        let opcode = cb.query_cell();
+        let is_shl = OpcodeId::SHR.expr() - opcode.expr();
+        let is_shr = 1.expr() - is_shl.expr();
+
+        let quotient = cb.query_word();
+        let divisor = cb.query_word();
+        let remainder = cb.query_word();
+        let dividend = cb.query_word();
+        let shift = cb.query_word();
+        let shf0 = cb.query_cell();
+
+        let mul_add_words =
+            MulAddWordsGadget::construct(cb, [&quotient, &divisor, &remainder, &dividend]);
+        let divisor_is_zero = IsZeroGadget::construct(cb, sum::expr(&divisor.cells));
+        let remainder_is_zero = IsZeroGadget::construct(cb, sum::expr(&remainder.cells));
+        let remainder_lt_divisor = LtWordGadget::construct(cb, &remainder, &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.
+        cb.stack_pop(shift.expr());
+        cb.stack_pop(is_shl.expr() * quotient.expr() + is_shr.expr() * dividend.expr());
+        cb.stack_push(
+            (is_shl.expr() * dividend.expr() + is_shr.expr() * quotient.expr())
+                * (1.expr() - divisor_is_zero.expr()),
+        );
+
+        cb.require_zero(
+            "shift == shift.cells[0] when divisor != 0",
+            (1.expr() - divisor_is_zero.expr()) * (shift.expr() - shift.cells[0].expr()),
+        );
+
+        cb.require_zero(
+            "remainder < divisor when divisor != 0",
+            (1.expr() - divisor_is_zero.expr()) * (1.expr() - remainder_lt_divisor.expr()),
+        );
+
+        cb.require_zero(
+            "remainder == 0 for opcode SHL",
+            is_shl * (1.expr() - remainder_is_zero.expr()),
+        );
+
+        cb.require_zero(
+            "overflow == 0 for opcode SHR",
+            is_shr * mul_add_words.overflow(),
+        );
+
+        // Constrain divisor_lo == 2^shf0 when shf0 < 128, and
+        // divisor_hi == 2^(128 - shf0) otherwise.
+        let divisor_lo = from_bytes::expr(&divisor.cells[..16]);
+        let divisor_hi = from_bytes::expr(&divisor.cells[16..]);
+        cb.condition(1.expr() - divisor_is_zero.expr(), |cb| {
+            cb.add_lookup(
+                "Pow2 lookup of shf0, divisor_lo and divisor_hi",
+                Lookup::Fixed {
+                    tag: FixedTableTag::Pow2.expr(),
+                    values: [shf0.expr(), divisor_lo.expr(), divisor_hi.expr()],
+                },
+            );
+        });
+
+        let step_state_transition = StepStateTransition {
+            rw_counter: Delta(3.expr()),
+            program_counter: Delta(1.expr()),
+            stack_pointer: Delta(1.expr()),
+            gas_left: Delta(-OpcodeId::SHL.constant_gas_cost().expr()),
+            ..Default::default()
+        };
+
+        let same_context = SameContextGadget::construct(cb, opcode, step_state_transition);
+
+        Self {
+            same_context,
+            quotient,
+            divisor,
+            remainder,
+            dividend,
+            shift,
+            shf0,
+            mul_add_words,
+            divisor_is_zero,
+            remainder_is_zero,
+            remainder_lt_divisor,
+        }
+    }
+
+    fn assign_exec_step(
+        &self,
+        region: &mut CachedRegion<'_, '_, F>,
+        offset: usize,
+        block: &Block<F>,
+        _: &Transaction,
+        _: &Call,
+        step: &ExecStep,
+    ) -> Result<(), Error> {
+        self.same_context.assign_exec_step(region, offset, step)?;
+        let indices = [step.rw_indices[0], step.rw_indices[1], step.rw_indices[2]];
+        let [pop1, pop2, push] = indices.map(|idx| block.rws[idx].stack_value());
+        let shf0 = pop1.to_le_bytes()[0];
+        let divisor = if U256::from(shf0) == pop1 {
+            U256::from(1) << shf0
+        } else {
+            U256::from(0)
+        };
+
+        let (quotient, remainder, dividend) = match step.opcode.unwrap() {
+            OpcodeId::SHL => (pop2, U256::from(0), push),
+            OpcodeId::SHR => (push, pop2 - push * divisor, pop2),
+            _ => unreachable!(),
+        };
+        self.quotient
+            .assign(region, offset, Some(quotient.to_le_bytes()))?;
+        self.divisor
+            .assign(region, offset, Some(divisor.to_le_bytes()))?;
+        self.remainder
+            .assign(region, offset, Some(remainder.to_le_bytes()))?;
+        self.dividend
+            .assign(region, offset, Some(dividend.to_le_bytes()))?;
+        self.shift
+            .assign(region, offset, Some(pop1.to_le_bytes()))?;
+        self.shf0
+            .assign(region, offset, Some(u64::from(shf0).into()))?;
+        self.mul_add_words
+            .assign(region, offset, [quotient, divisor, remainder, dividend])?;
+        let divisor_sum = (0..32).fold(0, |acc, idx| acc + divisor.byte(idx) as u64);
+        self.divisor_is_zero
+            .assign(region, offset, F::from(divisor_sum))?;
+        let remainder_sum = (0..32).fold(0, |acc, idx| acc + remainder.byte(idx) as u64);
+        self.remainder_is_zero
+            .assign(region, offset, F::from(remainder_sum))?;
+        self.remainder_lt_divisor
+            .assign(region, offset, remainder, divisor)
+    }
+}
+
+#[cfg(test)]
+mod test {
+    use crate::{evm_circuit::test::rand_word, test_util::run_test_circuits};
+    use eth_types::evm_types::OpcodeId;
+    use eth_types::{bytecode, Word};
+    use mock::TestContext;
+
+    fn test_ok(opcode: OpcodeId, pop1: Word, pop2: Word) {
+        let bytecode = bytecode! {
+            PUSH32(pop1)
+            PUSH32(pop2)
+            #[start]
+            .write_op(opcode)
+            STOP
+        };
+
+        assert_eq!(
+            run_test_circuits(
+                TestContext::<2, 1>::simple_ctx_with_bytecode(bytecode).unwrap(),
+                None
+            ),
+            Ok(())
+        );
+    }
+
+    #[test]
+    fn shl_gadget_tests() {
+        test_ok(OpcodeId::SHL, Word::from(0xABCD) << 240, Word::from(8));
+        test_ok(OpcodeId::SHL, Word::from(0x1234) << 240, Word::from(7));
+        test_ok(OpcodeId::SHL, Word::from(0x8765) << 240, Word::from(17));
+        test_ok(OpcodeId::SHL, Word::from(0x4321) << 240, Word::from(0));
+        test_ok(OpcodeId::SHL, Word::from(0xFFFF), Word::from(256));
+        test_ok(OpcodeId::SHL, Word::from(0x12345), Word::from(256 + 8 + 1));
+        let max_word = Word::from_big_endian(&[255_u8; 32]);
+        test_ok(OpcodeId::SHL, max_word, Word::from(63));
+        test_ok(OpcodeId::SHL, max_word, Word::from(128));
+        test_ok(OpcodeId::SHL, max_word, Word::from(129));
+        test_ok(OpcodeId::SHL, rand_word(), rand_word());
+    }
+
+    #[test]
+    fn shr_gadget_tests() {
+        test_ok(OpcodeId::SHR, Word::from(0xABCD), Word::from(8));
+        test_ok(OpcodeId::SHR, Word::from(0x1234), Word::from(7));
+        test_ok(OpcodeId::SHR, Word::from(0x8765), Word::from(17));
+        test_ok(OpcodeId::SHR, Word::from(0x4321), Word::from(0));
+        test_ok(OpcodeId::SHR, Word::from(0xFFFF), Word::from(256));
+        test_ok(OpcodeId::SHR, Word::from(0x12345), Word::from(256 + 8 + 1));
+        let max_word = Word::from_big_endian(&[255_u8; 32]);
+        test_ok(OpcodeId::SHR, max_word, Word::from(63));
+        test_ok(OpcodeId::SHR, max_word, Word::from(128));
+        test_ok(OpcodeId::SHR, max_word, Word::from(129));
+        test_ok(OpcodeId::SHR, rand_word(), rand_word());
+    }
+}