WIP: no-op MIPS

o1vm/src/cli/cannon.rs

@@ -105,6 +105,8 @@ impl From<MipsVmConfigurationArgs> for VmConfiguration {
 pub struct RunArgs {
     #[arg(long = "preimage-db-dir", value_name = "PREIMAGE_DB_DIR")]
     pub preimage_db_dir: Option<String>,
+    #[arg(long = "srs-cache", value_name = "SRS_CACHE")]
+    pub srs_cache: Option<String>,
     // it's important that vm_cfg is last in order to properly parse the host field
     #[command(flatten)]
     pub vm_cfg: MipsVmConfigurationArgs,

o1vm/src/interpreters/mips/column.rs

@@ -44,8 +44,9 @@ pub const SCRATCH_SIZE_INVERSE: usize = 12;
 pub const N_MIPS_REL_COLS: usize = SCRATCH_SIZE + SCRATCH_SIZE_INVERSE + 2;
 
 /// The number of witness columns used to store the instruction selectors.
+/// NOTE: The +1 is coming from the NoOp instruction.
 pub const N_MIPS_SEL_COLS: usize =
-    RTypeInstruction::COUNT + JTypeInstruction::COUNT + ITypeInstruction::COUNT;
+    RTypeInstruction::COUNT + JTypeInstruction::COUNT + ITypeInstruction::COUNT + 1;
 
 /// All the witness columns used in MIPS
 pub const N_MIPS_COLS: usize = N_MIPS_REL_COLS + N_MIPS_SEL_COLS;
@@ -94,6 +95,12 @@ impl From<Instruction> for usize {
             IType(itype) => {
                 N_MIPS_REL_COLS + RTypeInstruction::COUNT + JTypeInstruction::COUNT + itype as usize
             }
+            Instruction::NoOp => {
+                N_MIPS_REL_COLS
+                    + RTypeInstruction::COUNT
+                    + JTypeInstruction::COUNT
+                    + ITypeInstruction::COUNT
+            }
         }
     }
 }

o1vm/src/interpreters/mips/interpreter.rs

@@ -31,6 +31,7 @@ pub enum Instruction {
     RType(RTypeInstruction),
     JType(JTypeInstruction),
     IType(ITypeInstruction),
+    NoOp,
 }
 
 #[derive(
@@ -153,6 +154,7 @@ impl IntoIterator for Instruction {
                 }
                 iter_contents.into_iter()
             }
+            Instruction::NoOp => vec![Instruction::NoOp].into_iter(),
         }
     }
 }
@@ -970,9 +972,33 @@ pub fn interpret_instruction<Env: InterpreterEnv>(env: &mut Env, instr: Instruct
         Instruction::RType(instr) => interpret_rtype(env, instr),
         Instruction::JType(instr) => interpret_jtype(env, instr),
         Instruction::IType(instr) => interpret_itype(env, instr),
+        Instruction::NoOp => interpret_noop(env),
     }
 }
 
+pub fn interpret_noop<Env: InterpreterEnv>(env: &mut Env) {
+    let instruction_pointer = env.get_instruction_pointer();
+    let instruction = {
+        let v0 = env.read_memory(&instruction_pointer);
+        let v1 = env.read_memory(&(instruction_pointer.clone() + Env::constant(1)));
+        let v2 = env.read_memory(&(instruction_pointer.clone() + Env::constant(2)));
+        let v3 = env.read_memory(&(instruction_pointer.clone() + Env::constant(3)));
+        (v0 * Env::constant(1 << 24))
+            + (v1 * Env::constant(1 << 16))
+            + (v2 * Env::constant(1 << 8))
+            + v3
+    };
+    let opcode = {
+        let pos = env.alloc_scratch();
+        unsafe { env.bitmask(&instruction, 32, 26, pos) }
+    };
+
+    env.range_check8(&opcode, 6);
+    env.assert_is_zero(opcode);
+    let next_instruction_pointer = env.get_next_instruction_pointer();
+    env.set_instruction_pointer(next_instruction_pointer);
+}
+
 pub fn interpret_rtype<Env: InterpreterEnv>(env: &mut Env, instr: RTypeInstruction) {
     let instruction_pointer = env.get_instruction_pointer();
     let next_instruction_pointer = env.get_next_instruction_pointer();

o1vm/src/interpreters/mips/witness.rs

@@ -989,7 +989,13 @@ impl<Fp: Field, PreImageOracle: PreImageOracleT> Env<Fp, PreImageOracle> {
         let opcode = {
             match instruction >> 26 {
                 0x00 => match instruction & 0x3F {
-                    0x00 => Instruction::RType(RTypeInstruction::ShiftLeftLogical),
+                    0x00 => {
+                        if instruction == 0 {
+                            Instruction::NoOp
+                        } else {
+                            Instruction::RType(RTypeInstruction::ShiftLeftLogical)
+                        }
+                    }
                     0x02 => Instruction::RType(RTypeInstruction::ShiftRightLogical),
                     0x03 => Instruction::RType(RTypeInstruction::ShiftRightArithmetic),
                     0x04 => Instruction::RType(RTypeInstruction::ShiftLeftLogicalVariable),

o1vm/src/pickles/main.rs

@@ -1,14 +1,15 @@
-use ark_ff::UniformRand;
+use ark_ff::{UniformRand, Zero};
 use clap::Parser;
-use kimchi::circuits::domains::EvaluationDomains;
+use kimchi::{circuits::domains::EvaluationDomains, precomputed_srs::TestSRS};
+use kimchi_msm::expr::E;
 use log::debug;
 use mina_curves::pasta::{Fp, Vesta, VestaParameters};
 use mina_poseidon::{
     constants::PlonkSpongeConstantsKimchi,
     sponge::{DefaultFqSponge, DefaultFrSponge},
 };
 use o1vm::{
-    cannon::{self, Start, State},
+    cannon::{self, Meta, Start, State},
     cli, elf_loader,
     interpreters::mips::{
         column::N_MIPS_REL_COLS,
@@ -21,6 +22,7 @@ use o1vm::{
     test_preimage_read,
 };
 use poly_commitment::{ipa::SRS, SRS as _};
+use rand::rngs::ThreadRng;
 use std::{fs::File, io::BufReader, path::Path, process::ExitCode, time::Instant};
 
 pub const DOMAIN_SIZE: usize = 1 << 15;
@@ -48,10 +50,37 @@ pub fn cannon_main(args: cli::cannon::RunArgs) {
     let start = Start::create(state.step as usize);
 
     let domain_fp = EvaluationDomains::<Fp>::create(DOMAIN_SIZE).unwrap();
-    let srs: SRS<Vesta> = {
-        let srs = SRS::create(DOMAIN_SIZE);
-        srs.get_lagrange_basis(domain_fp.d1);
-        srs
+    let srs: SRS<Vesta> = match &args.srs_cache {
+        Some(cache) => {
+            debug!("Loading SRS from cache {}", cache);
+            let file_path = Path::new(cache);
+            let file = File::open(file_path).expect("Error opening SRS cache file");
+            let srs: SRS<Vesta> = {
+                // By convention, proof systems serializes a TestSRS with filename 'test_<CURVE_NAME>.srs'.
+                // The benefit of using this is you don't waste time verifying the SRS.
+                if file_path
+                    .file_name()
+                    .unwrap()
+                    .to_str()
+                    .unwrap()
+                    .starts_with("test_")
+                {
+                    let test_srs: TestSRS<Vesta> = rmp_serde::from_read(&file).unwrap();
+                    From::from(test_srs)
+                } else {
+                    rmp_serde::from_read(&file).unwrap()
+                }
+            };
+            debug!("SRS loaded successfully from cache");
+            srs
+        }
+        None => {
+            debug!("No SRS cache provided. Creating SRS from scratch");
+            let srs = SRS::create(DOMAIN_SIZE);
+            srs.get_lagrange_basis(domain_fp.d1);
+            debug!("SRS created successfully");
+            srs
+        }
     };
 
     // Initialize the environments
@@ -79,67 +108,137 @@ pub fn cannon_main(args: cli::cannon::RunArgs) {
     let constraints = mips_constraints::get_all_constraints::<Fp>();
 
     let mut curr_proof_inputs: ProofInputs<Vesta> = ProofInputs::new(DOMAIN_SIZE);
+
     while !mips_wit_env.halt {
-        let _instr: Instruction = mips_wit_env.step(&configuration, meta, &start);
-        for (scratch, scratch_chunk) in mips_wit_env
-            .scratch_state
-            .iter()
-            .zip(curr_proof_inputs.evaluations.scratch.iter_mut())
-        {
-            scratch_chunk.push(*scratch);
-        }
-        for (scratch, scratch_chunk) in mips_wit_env
-            .scratch_state_inverse
-            .iter()
-            .zip(curr_proof_inputs.evaluations.scratch_inverse.iter_mut())
-        {
-            scratch_chunk.push(*scratch);
-        }
-        curr_proof_inputs
-            .evaluations
-            .instruction_counter
-            .push(Fp::from(mips_wit_env.instruction_counter));
-        // FIXME: Might be another value
-        curr_proof_inputs.evaluations.error.push(Fp::rand(&mut rng));
-
-        curr_proof_inputs
-            .evaluations
-            .selector
-            .push(Fp::from((mips_wit_env.selector - N_MIPS_REL_COLS) as u64));
+        step_prover(
+            &mut mips_wit_env,
+            &configuration,
+            meta,
+            &start,
+            &mut curr_proof_inputs,
+            &mut rng,
+        );
 
         if curr_proof_inputs.evaluations.instruction_counter.len() == DOMAIN_SIZE {
-            let start_iteration = Instant::now();
             debug!("Limit of {DOMAIN_SIZE} reached. We make a proof, verify it (for testing) and start with a new chunk");
-            let proof = prover::prove::<
-                Vesta,
-                DefaultFqSponge<VestaParameters, PlonkSpongeConstantsKimchi>,
-                DefaultFrSponge<Fp, PlonkSpongeConstantsKimchi>,
-                _,
-            >(domain_fp, &srs, curr_proof_inputs, &constraints, &mut rng)
-            .unwrap();
-            // Check that the proof is correct. This is for testing purposes.
-            // Leaving like this for now.
-            debug!(
-                "Proof generated in {elapsed} μs",
-                elapsed = start_iteration.elapsed().as_micros()
-            );
-            {
-                let start_iteration = Instant::now();
-                let verif = verifier::verify::<
-                    Vesta,
-                    DefaultFqSponge<VestaParameters, PlonkSpongeConstantsKimchi>,
-                    DefaultFrSponge<Fp, PlonkSpongeConstantsKimchi>,
-                >(domain_fp, &srs, &constraints, &proof);
-                debug!(
-                    "Verification done in {elapsed} μs",
-                    elapsed = start_iteration.elapsed().as_micros()
-                );
-                assert!(verif);
-            }
+            prove_and_verify(domain_fp, &srs, &constraints, curr_proof_inputs, &mut rng);
 
             curr_proof_inputs = ProofInputs::new(DOMAIN_SIZE);
         }
     }
+
+    if curr_proof_inputs.evaluations.instruction_counter.len() < DOMAIN_SIZE {
+        debug!(
+            "Evaluation ended with {} elements. Pad it to prove and verify",
+            curr_proof_inputs.evaluations.instruction_counter.len()
+        );
+        pad(&mips_wit_env, &mut curr_proof_inputs, &mut rng);
+        prove_and_verify(domain_fp, &srs, &constraints, curr_proof_inputs, &mut rng);
+    }
+}
+
+fn step_prover(
+    mips_wit_env: &mut mips_witness::Env<Fp, Box<dyn PreImageOracleT>>,
+    configuration: &cannon::VmConfiguration,
+    meta: &Option<Meta>,
+    start: &Start,
+    curr_proof_inputs: &mut ProofInputs<Vesta>,
+    rng: &mut ThreadRng,
+) {
+    let _instr: Instruction = mips_wit_env.step(configuration, meta, start);
+    for (scratch, scratch_chunk) in mips_wit_env
+        .scratch_state
+        .iter()
+        .zip(curr_proof_inputs.evaluations.scratch.iter_mut())
+    {
+        scratch_chunk.push(*scratch);
+    }
+    for (scratch, scratch_chunk) in mips_wit_env
+        .scratch_state_inverse
+        .iter()
+        .zip(curr_proof_inputs.evaluations.scratch_inverse.iter_mut())
+    {
+        scratch_chunk.push(*scratch);
+    }
+    curr_proof_inputs
+        .evaluations
+        .instruction_counter
+        .push(Fp::from(mips_wit_env.instruction_counter));
+    // FIXME: Might be another value
+    curr_proof_inputs.evaluations.error.push(Fp::rand(rng));
+
+    curr_proof_inputs
+        .evaluations
+        .selector
+        .push(Fp::from((mips_wit_env.selector - N_MIPS_REL_COLS) as u64));
+}
+
+fn pad(
+    witness_env: &mips_witness::Env<Fp, Box<dyn PreImageOracleT>>,
+    curr_proof_inputs: &mut ProofInputs<Vesta>,
+    rng: &mut ThreadRng,
+) {
+    let zero = Fp::zero();
+    let noop_selector: Fp = {
+        let noop: usize = Instruction::NoOp.into();
+        Fp::from((noop - N_MIPS_REL_COLS) as u64)
+    };
+    curr_proof_inputs
+        .evaluations
+        .scratch
+        .iter_mut()
+        .for_each(|x| x.resize(x.capacity(), zero));
+    curr_proof_inputs
+        .evaluations
+        .scratch_inverse
+        .iter_mut()
+        .for_each(|x| x.resize(x.capacity(), zero));
+    curr_proof_inputs.evaluations.instruction_counter.resize(
+        curr_proof_inputs.evaluations.instruction_counter.capacity(),
+        Fp::from(witness_env.instruction_counter),
+    );
+    curr_proof_inputs
+        .evaluations
+        .error
+        .resize_with(curr_proof_inputs.evaluations.error.capacity(), || {
+            Fp::rand(rng)
+        });
+    curr_proof_inputs.evaluations.selector.resize(
+        curr_proof_inputs.evaluations.selector.capacity(),
+        noop_selector,
+    );
+}
+
+fn prove_and_verify(
+    domain_fp: EvaluationDomains<Fp>,
+    srs: &SRS<Vesta>,
+    constraints: &[E<Fp>],
+    curr_proof_inputs: ProofInputs<Vesta>,
+    rng: &mut ThreadRng,
+) {
+    let start_iteration = Instant::now();
+    let proof = prover::prove::<
+        Vesta,
+        DefaultFqSponge<VestaParameters, PlonkSpongeConstantsKimchi>,
+        DefaultFrSponge<Fp, PlonkSpongeConstantsKimchi>,
+        _,
+    >(domain_fp, srs, curr_proof_inputs, constraints, rng)
+    .unwrap();
+    debug!(
+        "Proof generated in {elapsed} μs",
+        elapsed = start_iteration.elapsed().as_micros()
+    );
+    let start_iteration = Instant::now();
+    let verif = verifier::verify::<
+        Vesta,
+        DefaultFqSponge<VestaParameters, PlonkSpongeConstantsKimchi>,
+        DefaultFrSponge<Fp, PlonkSpongeConstantsKimchi>,
+    >(domain_fp, srs, constraints, &proof);
+    debug!(
+        "Verification done in {elapsed} μs",
+        elapsed = start_iteration.elapsed().as_micros()
+    );
+    assert!(verif);
 }
 
 fn gen_state_json(arg: cli::cannon::GenStateJsonArgs) -> Result<(), String> {

o1vm/src/pickles/verifier.rs

@@ -1,5 +1,6 @@
 use ark_ec::AffineRepr;
 use ark_ff::{Field, One, PrimeField, Zero};
+use log::debug;
 use rand::thread_rng;
 
 use kimchi::{
@@ -262,6 +263,12 @@ where
             (res, zeta_i_n)
         },
     );
-    (quotient_zeta == numerator_zeta / (zeta.pow([domain.d1.size]) - G::ScalarField::one()))
-        && OpeningProof::verify(srs, &group_map, &mut [batch], &mut thread_rng())
+    let c1 = quotient_zeta == numerator_zeta / (zeta.pow([domain.d1.size]) - G::ScalarField::one());
+    debug!(
+        "Verification condition 1 (numerator_zeta vanishes on domain): {}",
+        c1
+    );
+    let c2 = OpeningProof::verify(srs, &group_map, &mut [batch], &mut thread_rng());
+    debug!("Verification condition 2 (verify opening proof): {}", c2);
+    c1 && c2
 }