basic sll working, overflow faling

overflow sll working

finish work

ceno_zkvm/src/chip_handler/general.rs

@@ -314,6 +314,15 @@ impl<'a, E: ExtensionField> CircuitBuilder<'a, E> {
         self.logic_u8(ROMType::Ltu, a, b, c)
     }
 
+    pub fn lookup_pow(
+        &mut self,
+        a: Expression<E>,
+        b: Expression<E>,
+        c: Expression<E>,
+    ) -> Result<(), ZKVMError> {
+        self.logic_u8(ROMType::Pow, a, b, c)
+    }
+
     /// less_than
     pub(crate) fn less_than<N, NR>(
         &mut self,

ceno_zkvm/src/instructions/riscv.rs

@@ -8,6 +8,7 @@ pub mod constants;
 pub mod divu;
 mod i_insn;
 pub mod logic;
+pub mod sll;
 pub mod sltu;
 
 mod b_insn;

ceno_zkvm/src/instructions/riscv/sll.rs

@@ -0,0 +1,214 @@
+use std::{marker::PhantomData, mem::MaybeUninit};
+
+use ceno_emul::InsnKind;
+use ff_ext::ExtensionField;
+
+use crate::{
+    expression::{ToExpr, WitIn},
+    instructions::Instruction,
+    set_val, Value,
+};
+
+use super::{constants::UInt, r_insn::RInstructionConfig, RIVInstruction};
+
+pub struct ShiftLeftConfig<E: ExtensionField> {
+    r_insn: RInstructionConfig<E>,
+
+    rs1_read: UInt<E>,
+    rs2_read: UInt<E>,
+    rd_written: UInt<E>,
+
+    quotient: UInt<E>,
+    rs2_low5: WitIn,
+    multiplier: UInt<E>,
+}
+
+pub struct ShiftLeftLogicalInstruction<E>(PhantomData<E>);
+
+impl<E> RIVInstruction for ShiftLeftLogicalInstruction<E> {
+    const INST_KIND: InsnKind = InsnKind::SLL;
+}
+
+impl<E: ExtensionField> Instruction<E> for ShiftLeftLogicalInstruction<E> {
+    type InstructionConfig = ShiftLeftConfig<E>;
+
+    fn name() -> String {
+        format!("{:?}", Self::INST_KIND)
+    }
+
+    fn construct_circuit(
+        circuit_builder: &mut crate::circuit_builder::CircuitBuilder<E>,
+    ) -> Result<Self::InstructionConfig, crate::error::ZKVMError> {
+        // rs1_read * rs2_read = rd_written
+        let mut rs1_read = UInt::new_unchecked(|| "rs1_read", circuit_builder)?;
+        let rs2_read = UInt::new_unchecked(|| "rs2_read", circuit_builder)?;
+
+        let rs2_low5 = circuit_builder.create_witin(|| "rs2_low5")?;
+        let quotient = UInt::new(|| "quotient", circuit_builder)?;
+        let mut multiplier = UInt::new_unchecked(|| "multiplier", circuit_builder)?;
+
+        let rd_written = rs1_read.mul(|| "rd_written", circuit_builder, &mut multiplier, true)?;
+
+        let r_insn = RInstructionConfig::<E>::construct_circuit(
+            circuit_builder,
+            Self::INST_KIND,
+            rs1_read.register_expr(),
+            rs2_read.register_expr(),
+            rd_written.register_expr(),
+        )?;
+
+        circuit_builder.lookup_pow(2.into(), rs2_low5.expr(), multiplier.value())?;
+        circuit_builder.assert_ux::<_, _, 5>(|| "rs2_low5 in u5", rs2_low5.expr())?;
+        circuit_builder.require_equal(
+            || "rs2 == quotient * 2^5 + rs2_low5",
+            rs2_read.value(),
+            quotient.value() * (1 << 5).into() + rs2_low5.expr(),
+        )?;
+
+        Ok(ShiftLeftConfig {
+            r_insn,
+            rs1_read,
+            rs2_read,
+            rd_written,
+            quotient,
+            rs2_low5,
+            multiplier,
+        })
+    }
+
+    fn assign_instance(
+        config: &Self::InstructionConfig,
+        instance: &mut [std::mem::MaybeUninit<<E as ExtensionField>::BaseField>],
+        lk_multiplicity: &mut crate::witness::LkMultiplicity,
+        step: &ceno_emul::StepRecord,
+    ) -> Result<(), crate::error::ZKVMError> {
+        let rs1_read = Value::new_unchecked(step.rs1().unwrap().value);
+        let rs2_read = Value::new_unchecked(step.rs2().unwrap().value);
+
+        let rs2_low5 = rs2_read.as_u64() & 0b11111;
+        let quotient = Value::new_unchecked(((rs2_read.as_u64() - rs2_low5) >> 5) as u32);
+        let multiplier = Value::new_unchecked((1 << rs2_low5) as u32);
+
+        let rd_written = rs1_read.mul(&multiplier, lk_multiplicity, true);
+
+        config
+            .r_insn
+            .assign_instance(instance, lk_multiplicity, step)?;
+
+        config.rs1_read.assign_value(instance, rs1_read);
+        config.rs2_read.assign_value(instance, rs2_read);
+
+        set_val!(instance, config.rs2_low5, rs2_low5);
+        config.quotient.assign_value(instance, quotient);
+        config.multiplier.assign_value(instance, multiplier);
+        config.rd_written.assign_limb_with_carry_auxiliary(
+            instance,
+            lk_multiplicity,
+            &rd_written,
+        )?;
+
+        Ok(())
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use ceno_emul::{Change, StepRecord};
+    use goldilocks::GoldilocksExt2;
+    use itertools::Itertools;
+    use multilinear_extensions::mle::IntoMLEs;
+
+    use crate::{
+        circuit_builder::{CircuitBuilder, ConstraintSystem},
+        instructions::Instruction,
+        scheme::mock_prover::{MockProver, MOCK_PC_SLL, MOCK_PROGRAM},
+    };
+
+    use super::ShiftLeftLogicalInstruction;
+
+    #[test]
+    fn test_opcode_sll_1() {
+        let mut cs = ConstraintSystem::<GoldilocksExt2>::new(|| "riscv");
+        let mut cb = CircuitBuilder::new(&mut cs);
+        let config = cb
+            .namespace(
+                || "sll",
+                |cb| {
+                    let config =
+                        ShiftLeftLogicalInstruction::<GoldilocksExt2>::construct_circuit(cb);
+                    Ok(config)
+                },
+            )
+            .unwrap()
+            .unwrap();
+
+        let (raw_witin, _) = ShiftLeftLogicalInstruction::<GoldilocksExt2>::assign_instances(
+            &config,
+            cb.cs.num_witin as usize,
+            vec![StepRecord::new_r_instruction(
+                3,
+                MOCK_PC_SLL,
+                MOCK_PROGRAM[18],
+                32,
+                3,
+                Change::new(0, 32 << 3),
+                0,
+            )],
+        )
+        .unwrap();
+
+        MockProver::assert_satisfied(
+            &cb,
+            &raw_witin
+                .de_interleaving()
+                .into_mles()
+                .into_iter()
+                .map(|v| v.into())
+                .collect_vec(),
+            None,
+        );
+    }
+
+    #[test]
+    fn test_opcode_sll_2_overflow() {
+        let mut cs = ConstraintSystem::<GoldilocksExt2>::new(|| "riscv");
+        let mut cb = CircuitBuilder::new(&mut cs);
+        let config = cb
+            .namespace(
+                || "sll",
+                |cb| {
+                    let config =
+                        ShiftLeftLogicalInstruction::<GoldilocksExt2>::construct_circuit(cb);
+                    Ok(config)
+                },
+            )
+            .unwrap()
+            .unwrap();
+
+        let (raw_witin, _) = ShiftLeftLogicalInstruction::<GoldilocksExt2>::assign_instances(
+            &config,
+            cb.cs.num_witin as usize,
+            vec![StepRecord::new_r_instruction(
+                3,
+                MOCK_PC_SLL,
+                MOCK_PROGRAM[18],
+                32,
+                33,
+                Change::new(0, 32 << 3),
+                0,
+            )],
+        )
+        .unwrap();
+
+        MockProver::assert_satisfied(
+            &cb,
+            &raw_witin
+                .de_interleaving()
+                .into_mles()
+                .into_iter()
+                .map(|v| v.into())
+                .collect_vec(),
+            None,
+        );
+    }
+}

ceno_zkvm/src/scheme/mock_prover.rs

@@ -4,8 +4,8 @@ use crate::{
     expression::{fmt, Expression},
     scheme::utils::eval_by_expr_with_fixed,
     tables::{
-        AndTable, LtuTable, OpsTable, OrTable, ProgramTableCircuit, RangeTable, TableCircuit,
-        U16Table, U5Table, U8Table, XorTable,
+        AndTable, LtuTable, OpsTable, OrTable, PowTable, ProgramTableCircuit, RangeTable,
+        TableCircuit, U16Table, U5Table, U8Table, XorTable,
     },
 };
 use ark_std::test_rng;
@@ -68,14 +68,16 @@ pub const MOCK_PROGRAM: &[u32] = &[
     0x00 << 25 | MOCK_RS2 << 20 | MOCK_RS1 << 15 | 0b011 << 12 | MOCK_RD << 7 | 0x33,
     // addi x4, x2, 3
     0x00 << 25 | MOCK_IMM_3 << 20 | MOCK_RS1 << 15 | 0x00 << 12 | MOCK_RD << 7 | 0x13,
-    // addi x4, x2, -3, correc this below
+    // addi x4, x2, -3
     0b_1_111111 << 25 | MOCK_IMM_NEG3 << 20 | MOCK_RS1 << 15 | 0x00 << 12 | MOCK_RD << 7 | 0x13,
     // bltu x2, x3, -8
     0b_1_111111 << 25 | MOCK_RS2 << 20 | MOCK_RS1 << 15 | 0b_110 << 12 | 0b_1100_1 << 7 | 0x63,
     // bgeu x2, x3, -8
     0b_1_111111 << 25 | MOCK_RS2 << 20 | MOCK_RS1 << 15 | 0b_111 << 12 | 0b_1100_1 << 7 | 0x63,
     // bge x2, x3, -8
     0b_1_111111 << 25 | MOCK_RS2 << 20 | MOCK_RS1 << 15 | 0b_101 << 12 | 0b_1100_1 << 7 | 0x63,
+    // sll x4, x2, x3
+    0x00 << 25 | MOCK_RS2 << 20 | MOCK_RS1 << 15 | 0b001 << 12 | MOCK_RD << 7 | 0x33,
 ];
 // Addresses of particular instructions in the mock program.
 pub const MOCK_PC_ADD: ByteAddr = ByteAddr(CENO_PLATFORM.pc_start());
@@ -96,6 +98,7 @@ pub const MOCK_PC_ADDI_SUB: ByteAddr = ByteAddr(CENO_PLATFORM.pc_start() + 56);
 pub const MOCK_PC_BLTU: ByteAddr = ByteAddr(CENO_PLATFORM.pc_start() + 60);
 pub const MOCK_PC_BGEU: ByteAddr = ByteAddr(CENO_PLATFORM.pc_start() + 64);
 pub const MOCK_PC_BGE: ByteAddr = ByteAddr(CENO_PLATFORM.pc_start() + 68);
+pub const MOCK_PC_SLL: ByteAddr = ByteAddr(CENO_PLATFORM.pc_start() + 72);
 
 #[allow(clippy::enum_variant_names)]
 #[derive(Debug, PartialEq, Clone)]
@@ -253,6 +256,7 @@ fn load_tables<E: ExtensionField>(cb: &CircuitBuilder<E>, challenge: [E; 2]) ->
     load_op_table::<OrTable, _>(&mut table_vec, cb, challenge);
     load_op_table::<XorTable, _>(&mut table_vec, cb, challenge);
     load_op_table::<LtuTable, _>(&mut table_vec, cb, challenge);
+    load_op_table::<PowTable, _>(&mut table_vec, cb, challenge);
     load_program_table(&mut table_vec, cb, challenge);
     HashSet::from_iter(table_vec)
 }

ceno_zkvm/src/structs.rs

@@ -49,6 +49,7 @@ pub enum ROMType {
     Or,          // a | b where a, b are bytes
     Xor,         // a ^ b where a, b are bytes
     Ltu,         // a <(usign) b where a, b are bytes and the result is 0/1.
+    Pow,         // a ** b where a is a 5-bit number
     Instruction, // Decoded instruction from the fixed program.
 }
 

ceno_zkvm/src/tables/ops.rs

@@ -78,3 +78,18 @@ impl OpsTable for LtuTable {
     }
 }
 pub type LtuTableCircuit<E> = OpsTableCircuit<E, LtuTable>;
+
+pub struct PowTable;
+impl OpsTable for PowTable {
+    const ROM_TYPE: ROMType = ROMType::Pow;
+    fn len() -> usize {
+        (1 << 5) + 1
+    }
+
+    fn content() -> Vec<[u64; 3]> {
+        (0..Self::len() as u64)
+            .map(|b| [2, b, 1 << b])
+            .chain(std::iter::once([0, 0, 0]))
+            .collect()
+    }
+}

ceno_zkvm/src/uint.rs

@@ -173,6 +173,16 @@ impl<const M: usize, const C: usize, E: ExtensionField> UIntLimbs<M, C, E> {
         self.assign_carries(instance, carries);
     }
 
+    pub fn assign_limb_with_carry_auxiliary(
+        &self,
+        instance: &mut [MaybeUninit<E::BaseField>],
+        lkm: &mut LkMultiplicity,
+        (limbs, carries, max_carry): &(Vec<u16>, Vec<u64>, u64),
+    ) -> Result<(), ZKVMError> {
+        self.assign_limbs(instance, limbs);
+        self.assign_carries_auxiliary(instance, lkm, carries, *max_carry)
+    }
+
     pub fn assign_limbs(&self, instance: &mut [MaybeUninit<E::BaseField>], limbs_values: &[u16]) {
         assert!(
             limbs_values.len() <= Self::NUM_CELLS,