diff --git a/ceno_zkvm/src/chip_handler/general.rs b/ceno_zkvm/src/chip_handler/general.rs index bf3116caa..53a165c8c 100644 --- a/ceno_zkvm/src/chip_handler/general.rs +++ b/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, + b: Expression, + c: Expression, + ) -> Result<(), ZKVMError> { + self.logic_u8(ROMType::Pow, a, b, c) + } + /// less_than pub(crate) fn less_than( &mut self, diff --git a/ceno_zkvm/src/instructions/riscv.rs b/ceno_zkvm/src/instructions/riscv.rs index 67fb31cd2..0c3e72dd9 100644 --- a/ceno_zkvm/src/instructions/riscv.rs +++ b/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; diff --git a/ceno_zkvm/src/instructions/riscv/sll.rs b/ceno_zkvm/src/instructions/riscv/sll.rs new file mode 100644 index 000000000..c7aa22a36 --- /dev/null +++ b/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 { + r_insn: RInstructionConfig, + + rs1_read: UInt, + rs2_read: UInt, + rd_written: UInt, + + quotient: UInt, + rs2_low5: WitIn, + multiplier: UInt, +} + +pub struct ShiftLeftLogicalInstruction(PhantomData); + +impl RIVInstruction for ShiftLeftLogicalInstruction { + const INST_KIND: InsnKind = InsnKind::SLL; +} + +impl Instruction for ShiftLeftLogicalInstruction { + type InstructionConfig = ShiftLeftConfig; + + fn name() -> String { + format!("{:?}", Self::INST_KIND) + } + + fn construct_circuit( + circuit_builder: &mut crate::circuit_builder::CircuitBuilder, + ) -> Result { + // 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::::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<::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::::new(|| "riscv"); + let mut cb = CircuitBuilder::new(&mut cs); + let config = cb + .namespace( + || "sll", + |cb| { + let config = + ShiftLeftLogicalInstruction::::construct_circuit(cb); + Ok(config) + }, + ) + .unwrap() + .unwrap(); + + let (raw_witin, _) = ShiftLeftLogicalInstruction::::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::::new(|| "riscv"); + let mut cb = CircuitBuilder::new(&mut cs); + let config = cb + .namespace( + || "sll", + |cb| { + let config = + ShiftLeftLogicalInstruction::::construct_circuit(cb); + Ok(config) + }, + ) + .unwrap() + .unwrap(); + + let (raw_witin, _) = ShiftLeftLogicalInstruction::::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, + ); + } +} diff --git a/ceno_zkvm/src/scheme/mock_prover.rs b/ceno_zkvm/src/scheme/mock_prover.rs index ca088040f..258dc4aa1 100644 --- a/ceno_zkvm/src/scheme/mock_prover.rs +++ b/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,7 +68,7 @@ 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, @@ -76,6 +76,8 @@ pub const MOCK_PROGRAM: &[u32] = &[ 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(cb: &CircuitBuilder, challenge: [E; 2]) -> load_op_table::(&mut table_vec, cb, challenge); load_op_table::(&mut table_vec, cb, challenge); load_op_table::(&mut table_vec, cb, challenge); + load_op_table::(&mut table_vec, cb, challenge); load_program_table(&mut table_vec, cb, challenge); HashSet::from_iter(table_vec) } diff --git a/ceno_zkvm/src/structs.rs b/ceno_zkvm/src/structs.rs index fbafda2c9..0e8d8d122 100644 --- a/ceno_zkvm/src/structs.rs +++ b/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. } diff --git a/ceno_zkvm/src/tables/ops.rs b/ceno_zkvm/src/tables/ops.rs index f624dfb0a..7ae004212 100644 --- a/ceno_zkvm/src/tables/ops.rs +++ b/ceno_zkvm/src/tables/ops.rs @@ -78,3 +78,18 @@ impl OpsTable for LtuTable { } } pub type LtuTableCircuit = OpsTableCircuit; + +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() + } +} diff --git a/ceno_zkvm/src/uint.rs b/ceno_zkvm/src/uint.rs index dbe0b3c8a..694af2019 100644 --- a/ceno_zkvm/src/uint.rs +++ b/ceno_zkvm/src/uint.rs @@ -173,6 +173,16 @@ impl UIntLimbs { self.assign_carries(instance, carries); } + pub fn assign_limb_with_carry_auxiliary( + &self, + instance: &mut [MaybeUninit], + lkm: &mut LkMultiplicity, + (limbs, carries, max_carry): &(Vec, Vec, 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], limbs_values: &[u16]) { assert!( limbs_values.len() <= Self::NUM_CELLS,