Merge branch 'master' into feat/integrate_mpcs

ceno_zkvm/src/chip_handler/general.rs

@@ -235,40 +235,57 @@ impl<'a, E: ExtensionField> CircuitBuilder<'a, E> {
         self.assert_u16(name_fn, expr * Expression::from(1 << 15))
     }
 
-    /// Assert `a & b = res` and that `a, b, res` are all bytes.
-    pub(crate) fn lookup_and_byte(
+    /// Assert `rom_type(a, b) = c` and that `a, b, c` are all bytes.
+    pub fn logic_u8(
         &mut self,
+        rom_type: ROMType,
         a: Expression<E>,
         b: Expression<E>,
-        res: Expression<E>,
+        c: Expression<E>,
     ) -> Result<(), ZKVMError> {
-        let items: Vec<Expression<E>> = vec![
-            Expression::Constant(E::BaseField::from(ROMType::And as u64)),
-            a,
-            b,
-            res,
-        ];
+        let items: Vec<Expression<E>> = vec![(rom_type as usize).into(), a, b, c];
         let rlc_record = self.rlc_chip_record(items);
-        self.lk_record(|| "and lookup record", rlc_record)?;
-        Ok(())
+        self.lk_record(|| format!("lookup_{:?}", rom_type), rlc_record)
     }
 
-    /// Assert that `(a < b) == res as bool`, that `a, b` are unsigned bytes, and that `res` is 0 or 1.
-    pub(crate) fn lookup_ltu_limb8(
+    /// Assert `a & b = c` and that `a, b, c` are all bytes.
+    pub fn lookup_and_byte(
         &mut self,
         a: Expression<E>,
         b: Expression<E>,
-        res: Expression<E>,
+        c: Expression<E>,
     ) -> Result<(), ZKVMError> {
-        let items: Vec<Expression<E>> = vec![
-            Expression::Constant(E::BaseField::from(ROMType::Ltu as u64)),
-            a,
-            b,
-            res,
-        ];
-        let rlc_record = self.rlc_chip_record(items);
-        self.lk_record(|| "ltu lookup record", rlc_record)?;
-        Ok(())
+        self.logic_u8(ROMType::And, a, b, c)
+    }
+
+    /// Assert `a | b = c` and that `a, b, c` are all bytes.
+    pub fn lookup_or_byte(
+        &mut self,
+        a: Expression<E>,
+        b: Expression<E>,
+        c: Expression<E>,
+    ) -> Result<(), ZKVMError> {
+        self.logic_u8(ROMType::Or, a, b, c)
+    }
+
+    /// Assert `a ^ b = c` and that `a, b, c` are all bytes.
+    pub fn lookup_xor_byte(
+        &mut self,
+        a: Expression<E>,
+        b: Expression<E>,
+        c: Expression<E>,
+    ) -> Result<(), ZKVMError> {
+        self.logic_u8(ROMType::Xor, a, b, c)
+    }
+
+    /// Assert that `(a < b) == c as bool`, that `a, b` are unsigned bytes, and that `c` is 0 or 1.
+    pub fn lookup_ltu_byte(
+        &mut self,
+        a: Expression<E>,
+        b: Expression<E>,
+        c: Expression<E>,
+    ) -> Result<(), ZKVMError> {
+        self.logic_u8(ROMType::Ltu, a, b, c)
     }
 
     /// less_than

ceno_zkvm/src/instructions/riscv.rs

@@ -4,6 +4,7 @@ pub mod arith;
 pub mod blt;
 pub mod config;
 pub mod constants;
+pub mod logic;
 
 mod r_insn;
 

ceno_zkvm/src/instructions/riscv/logic.rs

@@ -0,0 +1,29 @@
+mod logic_circuit;
+use logic_circuit::{LogicInstruction, LogicOp};
+
+#[cfg(test)]
+mod test;
+
+use crate::tables::{AndTable, OrTable, XorTable};
+use ceno_emul::InsnKind;
+
+pub struct AndOp;
+impl LogicOp for AndOp {
+    const INST_KIND: InsnKind = InsnKind::AND;
+    type OpsTable = AndTable;
+}
+pub type AndInstruction<E> = LogicInstruction<E, AndOp>;
+
+pub struct OrOp;
+impl LogicOp for OrOp {
+    const INST_KIND: InsnKind = InsnKind::OR;
+    type OpsTable = OrTable;
+}
+pub type OrInstruction<E> = LogicInstruction<E, OrOp>;
+
+pub struct XorOp;
+impl LogicOp for XorOp {
+    const INST_KIND: InsnKind = InsnKind::XOR;
+    type OpsTable = XorTable;
+}
+pub type XorInstruction<E> = LogicInstruction<E, XorOp>;

ceno_zkvm/src/instructions/riscv/logic/logic_circuit.rs

@@ -0,0 +1,131 @@
+//! The circuit implementation of logic instructions.
+
+use core::mem::MaybeUninit;
+use ff_ext::ExtensionField;
+use std::marker::PhantomData;
+
+use crate::{
+    circuit_builder::CircuitBuilder,
+    error::ZKVMError,
+    instructions::{
+        riscv::{constants::UInt8, r_insn::RInstructionConfig},
+        Instruction,
+    },
+    tables::OpsTable,
+    witness::LkMultiplicity,
+};
+use ceno_emul::{InsnKind, StepRecord, Word, WORD_SIZE};
+
+/// This trait defines a logic instruction, connecting an instruction type to a lookup table.
+pub trait LogicOp {
+    const INST_KIND: InsnKind;
+    type OpsTable: OpsTable;
+}
+
+/// The Instruction circuit for a given LogicOp.
+pub struct LogicInstruction<E, I>(PhantomData<(E, I)>);
+
+impl<E: ExtensionField, I: LogicOp> Instruction<E> for LogicInstruction<E, I> {
+    type InstructionConfig = LogicConfig<E>;
+
+    fn name() -> String {
+        format!("{:?}", I::INST_KIND)
+    }
+
+    fn construct_circuit(cb: &mut CircuitBuilder<E>) -> Result<Self::InstructionConfig, ZKVMError> {
+        let config = LogicConfig::construct_circuit(cb, I::INST_KIND)?;
+
+        // Constrain the registers based on the given lookup table.
+        UInt8::logic(
+            cb,
+            I::OpsTable::ROM_TYPE,
+            &config.rs1_read,
+            &config.rs2_read,
+            &config.rd_written,
+        )?;
+
+        Ok(config)
+    }
+
+    fn assign_instance(
+        config: &Self::InstructionConfig,
+        instance: &mut [MaybeUninit<<E as ExtensionField>::BaseField>],
+        lk_multiplicity: &mut LkMultiplicity,
+        step: &StepRecord,
+    ) -> Result<(), ZKVMError> {
+        UInt8::<E>::logic_assign::<I::OpsTable>(
+            lk_multiplicity,
+            step.rs1().unwrap().value as u64,
+            step.rs2().unwrap().value as u64,
+        );
+
+        config.assign_instance(instance, lk_multiplicity, step)
+    }
+}
+
+/// This config implements R-Instructions that represent registers values as 4 * u8.
+/// Non-generic code shared by several circuits.
+#[derive(Debug)]
+pub struct LogicConfig<E: ExtensionField> {
+    r_insn: RInstructionConfig<E>,
+
+    rs1_read: UInt8<E>,
+    rs2_read: UInt8<E>,
+    rd_written: UInt8<E>,
+}
+
+impl<E: ExtensionField> LogicConfig<E> {
+    fn construct_circuit(
+        cb: &mut CircuitBuilder<E>,
+        insn_kind: InsnKind,
+    ) -> Result<Self, ZKVMError> {
+        let rs1_read = UInt8::new_unchecked(|| "rs1_read", cb)?;
+        let rs2_read = UInt8::new_unchecked(|| "rs2_read", cb)?;
+        let rd_written = UInt8::new_unchecked(|| "rd_written", cb)?;
+
+        let r_insn = RInstructionConfig::<E>::construct_circuit(
+            cb,
+            insn_kind,
+            &rs1_read,
+            &rs2_read,
+            &rd_written,
+        )?;
+
+        Ok(Self {
+            r_insn,
+            rs1_read,
+            rs2_read,
+            rd_written,
+        })
+    }
+
+    fn assign_instance(
+        &self,
+        instance: &mut [MaybeUninit<<E as ExtensionField>::BaseField>],
+        lk_multiplicity: &mut LkMultiplicity,
+        step: &StepRecord,
+    ) -> Result<(), ZKVMError> {
+        self.r_insn
+            .assign_instance(instance, lk_multiplicity, step)?;
+
+        let rs1_read = Self::u8_limbs(step.rs1().unwrap().value);
+        self.rs1_read.assign_limbs(instance, rs1_read);
+
+        let rs2_read = Self::u8_limbs(step.rs2().unwrap().value);
+        self.rs2_read.assign_limbs(instance, rs2_read);
+
+        let rd_written = Self::u8_limbs(step.rd().unwrap().value.after);
+        self.rd_written.assign_limbs(instance, rd_written);
+
+        Ok(())
+    }
+
+    /// Decompose a word into byte field elements in little-endian order.
+    fn u8_limbs(v: Word) -> Vec<E::BaseField> {
+        let mut limbs = Vec::with_capacity(WORD_SIZE);
+        for i in 0..WORD_SIZE {
+            limbs.push(E::BaseField::from(((v >> (i * 8)) & 0xff) as u64));
+        }
+        limbs
+    }
+}