Merge remote-tracking branch 'origin/master' into feat/state_circuit

ceno_emul/Cargo.toml

@@ -6,6 +6,8 @@ license.workspace = true
 
 [dependencies]
 anyhow = { version = "1.0", default-features = false }
+strum = "0.25.0"
+strum_macros = "0.25.3"
 tracing = { version = "0.1", default-features = false, features = [
     "attributes",
 ] }

ceno_emul/src/addr.rs

@@ -67,6 +67,12 @@ impl From<WordAddr> for u32 {
     }
 }
 
+impl From<WordAddr> for u64 {
+    fn from(addr: WordAddr) -> Self {
+        addr.baddr().0 as u64
+    }
+}
+
 impl ByteAddr {
     pub const fn waddr(self) -> WordAddr {
         WordAddr(self.0 / WORD_SIZE as u32)

ceno_emul/src/lib.rs

@@ -11,7 +11,7 @@ mod vm_state;
 pub use vm_state::VMState;
 
 mod rv32im;
-pub use rv32im::{DecodedInstruction, EmuContext, InsnCategory, InsnKind};
+pub use rv32im::{DecodedInstruction, EmuContext, InsnCodes, InsnCategory, InsnKind};
 
 mod elf;
 pub use elf::Program;

ceno_emul/src/rv32im.rs

@@ -16,6 +16,7 @@
 
 use anyhow::{anyhow, Result};
 use std::sync::OnceLock;
+use strum_macros::EnumIter;
 
 use super::addr::{ByteAddr, RegIdx, Word, WordAddr, WORD_SIZE};
 
@@ -121,7 +122,7 @@ pub enum InsnCategory {
     Invalid,
 }
 
-#[derive(Clone, Copy, Debug, PartialEq)]
+#[derive(Clone, Copy, Debug, PartialEq, EnumIter)]
 #[allow(clippy::upper_case_acronyms)]
 pub enum InsnKind {
     INVALID,
@@ -174,8 +175,14 @@ pub enum InsnKind {
     MRET,
 }
 
+impl InsnKind {
+    pub const fn codes(self) -> InsnCodes {
+        RV32IM_ISA[self as usize]
+    }
+}
+
 #[derive(Clone, Copy, Debug)]
-struct FastDecodeEntry {
+pub struct InsnCodes {
     pub kind: InsnKind,
     category: InsnCategory,
     pub opcode: u32,
@@ -197,6 +204,28 @@ impl DecodedInstruction {
         }
     }
 
+    #[allow(dead_code)]
+    pub fn from_raw(kind: InsnKind, rs1: u32, rs2: u32, rd: u32) -> Self {
+        // limit the range of inputs
+        let rs2 = rs2 & 0x1f; // 5bits mask
+        let rs1 = rs1 & 0x1f;
+        let rd = rd & 0x1f;
+        let func7 = kind.codes().func7;
+        let func3 = kind.codes().func3;
+        let opcode = kind.codes().opcode;
+        let insn = func7 << 25 | rs2 << 20 | rs1 << 15 | func3 << 12 | rd << 7 | opcode;
+        Self {
+            insn,
+            top_bit: func7 | 0x80,
+            func7,
+            rs2,
+            rs1,
+            func3,
+            rd,
+            opcode,
+        }
+    }
+
     pub fn encoded(&self) -> u32 {
         self.insn
     }
@@ -269,8 +298,8 @@ const fn insn(
     opcode: u32,
     func3: i32,
     func7: i32,
-) -> FastDecodeEntry {
-    FastDecodeEntry {
+) -> InsnCodes {
+    InsnCodes {
         kind,
         category,
         opcode,
@@ -279,7 +308,7 @@ const fn insn(
     }
 }
 
-type InstructionTable = [FastDecodeEntry; 48];
+type InstructionTable = [InsnCodes; 48];
 type FastInstructionTable = [u8; 1 << 10];
 
 const RV32IM_ISA: InstructionTable = [
@@ -333,6 +362,15 @@ const RV32IM_ISA: InstructionTable = [
     insn(InsnKind::MRET, InsnCategory::System, 0x73, 0x0, 0x18),
 ];
 
+#[cfg(test)]
+#[test]
+fn test_isa_table() {
+    use strum::IntoEnumIterator;
+    for kind in InsnKind::iter() {
+        assert_eq!(kind.codes().kind, kind);
+    }
+}
+
 // RISC-V instruction are determined by 3 parts:
 // - Opcode: 7 bits
 // - Func3: 3 bits
@@ -373,7 +411,7 @@ impl FastDecodeTable {
         ((op_high << 5) | (func72bits << 3) | func3) as usize
     }
 
-    fn add_insn(table: &mut FastInstructionTable, insn: &FastDecodeEntry, isa_idx: usize) {
+    fn add_insn(table: &mut FastInstructionTable, insn: &InsnCodes, isa_idx: usize) {
         let op_high = insn.opcode >> 2;
         if (insn.func3 as i32) < 0 {
             for f3 in 0..8 {
@@ -392,7 +430,7 @@ impl FastDecodeTable {
         }
     }
 
-    fn lookup(&self, decoded: &DecodedInstruction) -> FastDecodeEntry {
+    fn lookup(&self, decoded: &DecodedInstruction) -> InsnCodes {
         let isa_idx = self.table[Self::map10(decoded.opcode, decoded.func3, decoded.func7)];
         RV32IM_ISA[isa_idx as usize]
     }

ceno_emul/src/tracer.rs

@@ -60,6 +60,7 @@ impl StepRecord {
         rs1_read: Word,
         rs2_read: Word,
         rd: Change<Word>,
+        previous_cycle: Cycle,
     ) -> StepRecord {
         let insn = DecodedInstruction::new(insn_code);
         StepRecord {
@@ -69,17 +70,17 @@ impl StepRecord {
             rs1: Some(ReadOp {
                 addr: CENO_PLATFORM.register_vma(insn.rs1() as RegIdx).into(),
                 value: rs1_read,
-                previous_cycle: 0,
+                previous_cycle,
             }),
             rs2: Some(ReadOp {
                 addr: CENO_PLATFORM.register_vma(insn.rs2() as RegIdx).into(),
                 value: rs2_read,
-                previous_cycle: 0,
+                previous_cycle,
             }),
             rd: Some(WriteOp {
                 addr: CENO_PLATFORM.register_vma(insn.rd() as RegIdx).into(),
                 value: rd,
-                previous_cycle: 0,
+                previous_cycle,
             }),
             memory_op: None,
         }

ceno_zkvm/examples/riscv_add.rs

@@ -12,7 +12,7 @@ use ceno_emul::{ByteAddr, InsnKind::ADD, StepRecord, VMState, CENO_PLATFORM};
 use ceno_zkvm::{
     scheme::verifier::ZKVMVerifier,
     structs::{ZKVMConstraintSystem, ZKVMFixedTraces, ZKVMWitnesses},
-    tables::RangeTableCircuit,
+    tables::U16TableCircuit,
 };
 use ff_ext::ff::Field;
 use goldilocks::GoldilocksExt2;
@@ -92,12 +92,12 @@ fn main() {
     // keygen
     let mut zkvm_cs = ZKVMConstraintSystem::default();
     let add_config = zkvm_cs.register_opcode_circuit::<AddInstruction<E>>();
-    let range_config = zkvm_cs.register_table_circuit::<RangeTableCircuit<E>>();
+    let range_config = zkvm_cs.register_table_circuit::<U16TableCircuit<E>>();
     let prog_config = zkvm_cs.register_table_circuit::<ProgramTableCircuit<E>>();
 
     let mut zkvm_fixed_traces = ZKVMFixedTraces::default();
     zkvm_fixed_traces.register_opcode_circuit::<AddInstruction<E>>(&zkvm_cs);
-    zkvm_fixed_traces.register_table_circuit::<RangeTableCircuit<E>>(
+    zkvm_fixed_traces.register_table_circuit::<U16TableCircuit<E>>(
         &zkvm_cs,
         range_config.clone(),
         &(),
@@ -148,7 +148,7 @@ fn main() {
         zkvm_witness.finalize_lk_multiplicities();
         // assign table circuits
         zkvm_witness
-            .assign_table_circuit::<RangeTableCircuit<E>>(&zkvm_cs, &range_config, &())
+            .assign_table_circuit::<U16TableCircuit<E>>(&zkvm_cs, &range_config, &())
             .unwrap();
         zkvm_witness
             .assign_table_circuit::<ProgramTableCircuit<E>>(

ceno_zkvm/src/chip_handler.rs

@@ -18,23 +18,23 @@ pub trait GlobalStateRegisterMachineChipOperations<E: ExtensionField> {
 }
 
 pub trait RegisterChipOperations<E: ExtensionField, NR: Into<String>, N: FnOnce() -> NR> {
-    fn register_read<V: ToExpr<E, Output = Vec<Expression<E>>>>(
+    fn register_read(
         &mut self,
         name_fn: N,
         register_id: &WitIn,
         prev_ts: Expression<E>,
         ts: Expression<E>,
-        values: &V,
+        values: &impl ToExpr<E, Output = Vec<Expression<E>>>,
     ) -> Result<(Expression<E>, ExprLtConfig), ZKVMError>;
 
     #[allow(clippy::too_many_arguments)]
-    fn register_write<V: ToExpr<E, Output = Vec<Expression<E>>>>(
+    fn register_write(
         &mut self,
         name_fn: N,
         register_id: &WitIn,
         prev_ts: Expression<E>,
         ts: Expression<E>,
-        prev_values: &V,
-        values: &V,
+        prev_values: &impl ToExpr<E, Output = Vec<Expression<E>>>,
+        values: &impl ToExpr<E, Output = Vec<Expression<E>>>,
     ) -> Result<(Expression<E>, ExprLtConfig), ZKVMError>;
 }

ceno_zkvm/src/chip_handler/general.rs

@@ -216,7 +216,10 @@ impl<'a, E: ExtensionField> CircuitBuilder<'a, E> {
         NR: Into<String>,
         N: FnOnce() -> NR,
     {
-        self.assert_u16(name_fn, expr * Expression::from(1 << 8))
+        let items: Vec<Expression<E>> = vec![(ROMType::U8 as usize).into(), expr];
+        let rlc_record = self.rlc_chip_record(items);
+        self.lk_record(name_fn, rlc_record)?;
+        Ok(())
     }
 
     pub(crate) fn assert_bit<NR, N>(
@@ -228,6 +231,7 @@ impl<'a, E: ExtensionField> CircuitBuilder<'a, E> {
         NR: Into<String>,
         N: FnOnce() -> NR,
     {
+        // TODO: Replace with `x * (1 - x)` or a multi-bit lookup similar to assert_u8_pair.
         self.assert_u16(name_fn, expr * Expression::from(1 << 15))
     }
 

ceno_zkvm/src/chip_handler/register.rs

@@ -13,13 +13,13 @@ use super::RegisterChipOperations;
 impl<'a, E: ExtensionField, NR: Into<String>, N: FnOnce() -> NR> RegisterChipOperations<E, NR, N>
     for CircuitBuilder<'a, E>
 {
-    fn register_read<V: ToExpr<E, Output = Vec<Expression<E>>>>(
+    fn register_read(
         &mut self,
         name_fn: N,
         register_id: &WitIn,
         prev_ts: Expression<E>,
         ts: Expression<E>,
-        values: &V,
+        values: &impl ToExpr<E, Output = Vec<Expression<E>>>,
     ) -> Result<(Expression<E>, ExprLtConfig), ZKVMError> {
         self.namespace(name_fn, |cb| {
             // READ (a, v, t)
@@ -58,14 +58,14 @@ impl<'a, E: ExtensionField, NR: Into<String>, N: FnOnce() -> NR> RegisterChipOpe
         })
     }
 
-    fn register_write<V: ToExpr<E, Output = Vec<Expression<E>>>>(
+    fn register_write(
         &mut self,
         name_fn: N,
         register_id: &WitIn,
         prev_ts: Expression<E>,
         ts: Expression<E>,
-        prev_values: &V,
-        values: &V,
+        prev_values: &impl ToExpr<E, Output = Vec<Expression<E>>>,
+        values: &impl ToExpr<E, Output = Vec<Expression<E>>>,
     ) -> Result<(Expression<E>, ExprLtConfig), ZKVMError> {
         self.namespace(name_fn, |cb| {
             // READ (a, v, t)

ceno_zkvm/src/expression.rs

@@ -1,5 +1,6 @@
 use std::{
     cmp::max,
+    mem::MaybeUninit,
     ops::{Add, Deref, Mul, Neg, Sub},
 };
 
@@ -426,6 +427,14 @@ impl WitIn {
             },
         )
     }
+
+    pub fn assign<E: ExtensionField>(
+        &self,
+        instance: &mut [MaybeUninit<E::BaseField>],
+        value: E::BaseField,
+    ) {
+        instance[self.id as usize] = MaybeUninit::new(value);
+    }
 }
 
 #[macro_export]

ceno_zkvm/src/instructions/riscv.rs

@@ -1,16 +1,16 @@
-use constants::OpcodeType;
-use ff_ext::ExtensionField;
-
-use super::Instruction;
+use ceno_emul::InsnKind;
 
 pub mod addsub;
 pub mod blt;
 pub mod config;
 pub mod constants;
+pub mod mul;
+
+mod r_insn;
 
 #[cfg(test)]
 mod test;
 
-pub trait RIVInstruction<E: ExtensionField>: Instruction<E> {
-    const OPCODE_TYPE: OpcodeType;
+pub trait RIVInstruction {
+    const INST_KIND: InsnKind;
 }