Merge branch 'feat/guest-example' into feat/guest-example-mem-fixes

ceno_zkvm/examples/fibonacci_elf.rs

@@ -3,7 +3,7 @@ use ceno_emul::{
     WORD_SIZE, WordAddr,
 };
 use ceno_zkvm::{
-    instructions::riscv::{DummyExtraConfig, Rv32imConfig},
+    instructions::riscv::{DummyExtraConfig, MmuConfig, Rv32imConfig},
     scheme::{
         PublicValues, constants::MAX_NUM_VARIABLES, mock_prover::MockProver, prover::ZKVMProver,
         verifier::ZKVMVerifier,
@@ -65,6 +65,7 @@ fn main() {
     let mut zkvm_cs = ZKVMConstraintSystem::default();
 
     let config = Rv32imConfig::<E>::construct_circuits(&mut zkvm_cs);
+    let mmu_config = MmuConfig::<E>::construct_circuits(&mut zkvm_cs);
     let dummy_config = DummyExtraConfig::<E>::construct_circuits(&mut zkvm_cs);
     let prog_config = zkvm_cs.register_table_circuit::<ExampleProgramTableCircuit<E>>();
     zkvm_cs.register_global_state::<GlobalState>();
@@ -95,12 +96,8 @@ fn main() {
     };
 
     let reg_init = initial_registers();
-    config.generate_fixed_traces(
-        &zkvm_cs,
-        &mut zkvm_fixed_traces,
-        &reg_init,
-        &program_data_init,
-    );
+    config.generate_fixed_traces(&zkvm_cs, &mut zkvm_fixed_traces, &reg_init);
+    mmu_config.generate_fixed_traces(&zkvm_cs, &mut zkvm_fixed_traces, &program_data_init);
     dummy_config.generate_fixed_traces(&zkvm_cs, &mut zkvm_fixed_traces);
 
     let pk = zkvm_cs
@@ -221,14 +218,10 @@ fn main() {
 
     // assign table circuits
     config
-        .assign_table_circuit(
-            &zkvm_cs,
-            &mut zkvm_witness,
-            &reg_final,
-            &[],
-            &program_data_final,
-            &[],
-        )
+        .assign_table_circuit(&zkvm_cs, &mut zkvm_witness, &reg_final, &[], &[])
+        .unwrap();
+    mmu_config
+        .assign_table_circuit(&zkvm_cs, &mut zkvm_witness, &program_data_final)
         .unwrap();
     // assign program circuit
     zkvm_witness

ceno_zkvm/examples/riscv_opcodes.rs

@@ -6,8 +6,8 @@ use ceno_zkvm::{
     scheme::{mock_prover::MockProver, prover::ZKVMProver},
     state::GlobalState,
     tables::{
-        DynVolatileRamTable, MemFinalRecord, MemTable, ProgramTableCircuit, init_program_data,
-        init_public_io, initial_registers,
+        DynVolatileRamTable, MemFinalRecord, MemTable, ProgramTableCircuit, init_public_io,
+        initial_registers,
     },
 };
 use clap::Parser;
@@ -121,16 +121,8 @@ fn main() {
     );
 
     let reg_init = initial_registers();
-    // Define program constant here
-    let program_data: &[u32] = &[];
-    let program_data_init = init_program_data(program_data);
 
-    config.generate_fixed_traces(
-        &zkvm_cs,
-        &mut zkvm_fixed_traces,
-        &reg_init,
-        &program_data_init,
-    );
+    config.generate_fixed_traces(&zkvm_cs, &mut zkvm_fixed_traces, &reg_init);
 
     let pk = zkvm_cs
         .clone()
@@ -154,7 +146,7 @@ fn main() {
         let mut vm = VMState::new(CENO_PLATFORM, program.clone());
 
         // init mmio
-        for record in program_data_init.iter().chain(public_io_init.iter()) {
+        for record in &public_io_init {
             vm.init_memory(record.addr.into(), record.value);
         }
 
@@ -215,19 +207,6 @@ fn main() {
             })
             .collect_vec();
 
-        // Find the final program_data cycles.
-        let program_data_final = program_data_init
-            .iter()
-            .map(|rec| {
-                let vma: WordAddr = rec.addr.into();
-                MemFinalRecord {
-                    addr: rec.addr,
-                    value: rec.value,
-                    cycle: *final_access.get(&vma).unwrap_or(&0),
-                }
-            })
-            .collect_vec();
-
         // Find the final public io cycles.
         let public_io_final = public_io_init
             .iter()
@@ -264,7 +243,6 @@ fn main() {
                 &mut zkvm_witness,
                 &reg_final,
                 &mem_final,
-                &program_data_final,
                 &public_io_final,
             )
             .unwrap();

ceno_zkvm/src/instructions/riscv.rs

@@ -1,7 +1,7 @@
 use ceno_emul::InsnKind;
 
 mod rv32im;
-pub use rv32im::{DummyExtraConfig, Rv32imConfig};
+pub use rv32im::{DummyExtraConfig, Rv32imConfig, mmu::MmuConfig};
 
 pub mod arith;
 pub mod arith_imm;

ceno_zkvm/src/instructions/riscv/rv32im.rs

@@ -21,9 +21,8 @@ use crate::{
     structs::{ZKVMConstraintSystem, ZKVMFixedTraces, ZKVMWitnesses},
     tables::{
         AndTableCircuit, LtuTableCircuit, MemCircuit, MemFinalRecord, MemInitRecord,
-        OrTableCircuit, PowTableCircuit, ProgramDataCircuit, PubIOCircuit, RegTableCircuit,
-        TableCircuit, U5TableCircuit, U8TableCircuit, U14TableCircuit, U16TableCircuit,
-        XorTableCircuit,
+        OrTableCircuit, PowTableCircuit, PubIOCircuit, RegTableCircuit, TableCircuit,
+        U5TableCircuit, U8TableCircuit, U14TableCircuit, U16TableCircuit, XorTableCircuit,
     },
 };
 use ceno_emul::{CENO_PLATFORM, InsnKind, InsnKind::*, StepRecord};
@@ -46,6 +45,8 @@ use super::{
     memory::LwInstruction,
 };
 
+pub mod mmu;
+
 pub struct Rv32imConfig<E: ExtensionField> {
     // ALU Opcodes.
     pub add_config: <AddInstruction<E> as Instruction<E>>::InstructionConfig,
@@ -115,7 +116,6 @@ pub struct Rv32imConfig<E: ExtensionField> {
     // RW tables.
     pub reg_config: <RegTableCircuit<E> as TableCircuit<E>>::TableConfig,
     //  pub mem_config: <MemCircuit<E> as TableCircuit<E>>::TableConfig,
-    pub program_data_config: <ProgramDataCircuit<E> as TableCircuit<E>>::TableConfig,
     //  pub public_io_config: <PubIOCircuit<E> as TableCircuit<E>>::TableConfig,
 }
 
@@ -192,7 +192,6 @@ impl<E: ExtensionField> Rv32imConfig<E> {
         //  let mem_config = cs.register_table_circuit::<MemCircuit<E>>();
 
         // RO tables
-        let program_data_config = cs.register_table_circuit::<ProgramDataCircuit<E>>();
         //   let public_io_config = cs.register_table_circuit::<PubIOCircuit<E>>();
 
         Self {
@@ -258,7 +257,6 @@ impl<E: ExtensionField> Rv32imConfig<E> {
 
             reg_config,
             //  mem_config,
-            program_data_config,
             //  public_io_config,
         }
     }
@@ -268,7 +266,6 @@ impl<E: ExtensionField> Rv32imConfig<E> {
         cs: &ZKVMConstraintSystem<E>,
         fixed: &mut ZKVMFixedTraces<E>,
         reg_init: &[MemInitRecord],
-        program_data_init: &[MemInitRecord],
     ) {
         // alu
         fixed.register_opcode_circuit::<AddInstruction<E>>(cs);
@@ -331,11 +328,7 @@ impl<E: ExtensionField> Rv32imConfig<E> {
         fixed.register_table_circuit::<PowTableCircuit<E>>(cs, &self.pow_config, &());
 
         fixed.register_table_circuit::<RegTableCircuit<E>>(cs, &self.reg_config, reg_init);
-        fixed.register_table_circuit::<ProgramDataCircuit<E>>(
-            cs,
-            &self.program_data_config,
-            program_data_init,
-        );
+
         //  fixed.register_table_circuit::<PubIOCircuit<E>>(cs, &self.public_io_config, &());
     }
 
@@ -452,7 +445,6 @@ impl<E: ExtensionField> Rv32imConfig<E> {
         witness: &mut ZKVMWitnesses<E>,
         reg_final: &[MemFinalRecord],
         mem_final: &[MemFinalRecord],
-        program_data_final: &[MemFinalRecord],
         public_io_final: &[MemFinalRecord],
     ) -> Result<(), ZKVMError> {
         witness.assign_table_circuit::<U16TableCircuit<E>>(cs, &self.u16_range_config, &())?;
@@ -473,14 +465,6 @@ impl<E: ExtensionField> Rv32imConfig<E> {
         // witness
         //   .assign_table_circuit::<MemCircuit<E>>(cs, &self.mem_config, mem_final)
         // .unwrap();
-        // assign program_data finalization.
-        witness
-            .assign_table_circuit::<ProgramDataCircuit<E>>(
-                cs,
-                &self.program_data_config,
-                program_data_final,
-            )
-            .unwrap();
 
         //   witness
         //      .assign_table_circuit::<PubIOCircuit<E>>(cs, &self.public_io_config, public_io_final)

ceno_zkvm/src/instructions/riscv/rv32im/mmu.rs

@@ -0,0 +1,46 @@
+use ff_ext::ExtensionField;
+
+use crate::{
+    error::ZKVMError,
+    structs::{ZKVMConstraintSystem, ZKVMFixedTraces, ZKVMWitnesses},
+    tables::{MemFinalRecord, MemInitRecord, ProgramDataCircuit, TableCircuit},
+};
+
+pub struct MmuConfig<E: ExtensionField> {
+    pub program_data_config: <ProgramDataCircuit<E> as TableCircuit<E>>::TableConfig,
+}
+
+impl<E: ExtensionField> MmuConfig<E> {
+    pub fn construct_circuits(cs: &mut ZKVMConstraintSystem<E>) -> Self {
+        let program_data_config = cs.register_table_circuit::<ProgramDataCircuit<E>>();
+        Self {
+            program_data_config,
+        }
+    }
+
+    pub fn generate_fixed_traces(
+        &self,
+        cs: &ZKVMConstraintSystem<E>,
+        fixed: &mut ZKVMFixedTraces<E>,
+        program_data_init: &[MemInitRecord],
+    ) {
+        fixed.register_table_circuit::<ProgramDataCircuit<E>>(
+            cs,
+            &self.program_data_config,
+            program_data_init,
+        );
+    }
+
+    pub fn assign_table_circuit(
+        &self,
+        cs: &ZKVMConstraintSystem<E>,
+        witness: &mut ZKVMWitnesses<E>,
+        program_data_final: &[MemFinalRecord],
+    ) -> Result<(), ZKVMError> {
+        witness.assign_table_circuit::<ProgramDataCircuit<E>>(
+            cs,
+            &self.program_data_config,
+            program_data_final,
+        )
+    }
+}