Single whir commitment

Cargo.toml

@@ -8,10 +8,7 @@ version = "0.1.0"
 edition = "2024"
 
 [workspace]
-members = [
-    "crates/*",
-    "crates/lean_prover/witness_generation",
-]
+members = ["crates/*"]
 
 [workspace.lints]
 rust.missing_debug_implementations = "warn"
@@ -51,7 +48,6 @@ sub_protocols = { path = "crates/sub_protocols" }
 lean_compiler = { path = "crates/lean_compiler" }
 lean_prover = { path = "crates/lean_prover" }
 rec_aggregation = { path = "crates/rec_aggregation" }
-witness_generation = { path = "crates/lean_prover/witness_generation" }
 
 # External
 thiserror = "2.0"

README.md

@@ -11,25 +11,25 @@ Documentation: [PDF](minimal_zkVM.pdf)
 ## Proving System
 
 
-- multilinear with [WHIR](https://eprint.iacr.org/2024/1586.pdf)
+- multilinear with [WHIR](https://eprint.iacr.org/2024/1586.pdf), allowing polynomial stacking (reducing proof size)
 - [SuperSpartan](https://eprint.iacr.org/2023/552.pdf), with [AIR-specific optimizations](https://solvable.group/posts/super-air/#fnref:1)
-- [Logup](https://eprint.iacr.org/2023/1284.pdf) / [Logup*](https://eprint.iacr.org/2025/946.pdf)
+- [Logup](https://eprint.iacr.org/2023/1284.pdf), with a system of buses similar to [OpenVM](https://openvm.dev/whitepaper.pdf)
 
 The VM design is inspired by the famous [Cairo paper](https://eprint.iacr.org/2021/1063.pdf).
 
 
 ## Security
 
-123 bits of security. Johnson bound + degree 5 extension of koala-bear -> **no proximity gaps conjecture**. (TODO 128 bits, which requires hash digests bigger than 8 koala-bears).
+123 bits of security. Johnson bound + degree 5 extension of koala-bear -> **no proximity gaps conjecture**. (TODO 128 bits? this would require hash digests bigger than 8 koala-bears).
 
-## Benchmarks
+## Benchmarks (Slightly outdated, new benchmarks incoming)
 
 Machine: M4 Max 48GB (CPU only)
 
 | Benchmark                  | Current              | Target          |
 | -------------------------- | -------------------- | --------------- |
 | Poseidon2 (16 koala-bears) | `560K Poseidon2 / s` | n/a             |
-| 2 -> 1 Recursion           | `1.35 s`             | `0.25 s `       |
+| 2 -> 1 Recursion           | `1.15 s`             | `0.25 s `       |
 | XMSS aggregation           | `554 XMSS / s`       | `1000 XMSS / s` |
 
 *Expect incoming perf improvements.*
@@ -39,11 +39,11 @@ To reproduce:
 - `cargo run --release -- recursion --n 2`
 - `cargo run --release -- xmss --n-signatures 1350`
 
-(Small detail remaining in recursion: final (multilinear) evaluation of the guest program bytecode, there are multiple ways of handling it... TBD soon)
-
 ## Proof size
 
-WHIR intial rate = 1/4. Proof size ≈ 325 KiB. TODO: WHIR batch opening + [2024/108](https://eprint.iacr.org/2024/108.pdf) section 3.1  -> close to 256 KiB. (To go below 256 KiB -> rate 1/8 or 1/16 in the final recursion).
+WHIR intial rate = 1/4 -> proof size ≈ 225 KiB. (150 KiB with rate 1/16, and < 100 KiB is possible with poximity gaps conjecture + rate 1/16).
+
+(TODO: remaining optimization = [2024/108](https://eprint.iacr.org/2024/108.pdf) section 3.1)
 
 ## Credits
 

TODO.md

@@ -5,7 +5,7 @@
 - 128 bits security
 - Merkle pruning
 - the interpreter of leanISA (+ witness generation) can be partially parallelized when there are some independent loops
-- Make everything "padding aware" (including WHIR, logup*, AIR, etc)
+- Make everything "padding aware" (including WHIR, logup, AIR, etc)
 - Opti WHIR: in sumcheck we know more than f(0) + f(1), we know f(0) and f(1)
 - Opti WHIR https://github.com/tcoratger/whir-p3/issues/303 and https://github.com/tcoratger/whir-p3/issues/306 ?
 - Avoid the embedding overhead in logup, when denominators = "c - index"
@@ -37,6 +37,7 @@ But we can get the bost of both worlds (suggested by Lev, TODO implement):
 - Fiat Shamir: add a claim tracing feature, to ensure all the claims are indeed checked (Lev)
 - Double Check AIR constraints, logup overflows etc
 - Formal Verification
+- Padd with noop cycles to always ensure memory size >= bytecode size (liveness), and ensure this condition is checked by the verifier (soundness)
 
 # Ideas
 

crates/air/src/prove.rs

@@ -37,15 +37,7 @@ where
         "TODO handle the case UNIVARIATE_SKIPS >= log_length"
     );
 
-    // crate::check_air_validity(
-    //     air,
-    //     &extra_data,
-    //     &columns_f,
-    //     &columns_ef,
-    //     last_row_shifted_f,
-    //     last_row_shifted_ef,
-    // )
-    // .unwrap();
+    // crate::check_air_validity(air, &extra_data, &columns_f, &columns_ef).unwrap();
 
     assert!(extra_data.alpha_powers().len() >= air.n_constraints() + virtual_column_statement.is_some() as usize);
 

crates/air/src/validity_check.rs

@@ -8,8 +8,6 @@ pub fn check_air_validity<A: Air, EF: ExtensionField<PF<EF>>>(
     extra_data: &A::ExtraData,
     columns_f: &[&[PF<EF>]],
     columns_ef: &[&[EF]],
-    last_row_f: &[PF<EF>],
-    last_row_ef: &[EF],
 ) -> Result<(), String> {
     let n_rows = columns_f[0].len();
     assert!(columns_f.iter().all(|col| col.len() == n_rows));
@@ -67,13 +65,19 @@ pub fn check_air_validity<A: Air, EF: ExtensionField<PF<EF>>>(
     let up_ef = (0..air.n_columns_ef_air())
         .map(|j| columns_ef[j][n_rows - 1])
         .collect::<Vec<_>>();
-    assert_eq!(last_row_f.len(), air.n_down_columns_f());
-    assert_eq!(last_row_ef.len(), air.n_down_columns_ef());
     let mut constraints_checker = ConstraintChecker {
         up_f,
         up_ef,
-        down_f: last_row_f.to_vec(),
-        down_ef: last_row_ef.to_vec(),
+        down_f: air
+            .down_column_indexes_f()
+            .iter()
+            .map(|j| columns_f[*j][n_rows - 1])
+            .collect::<Vec<_>>(),
+        down_ef: air
+            .down_column_indexes_ef()
+            .iter()
+            .map(|j| columns_ef[*j][n_rows - 1])
+            .collect::<Vec<_>>(),
         constraint_index: 0,
         errors: Vec::new(),
     };

crates/lean_compiler/snark_lib.py

@@ -79,6 +79,10 @@ def hint_decompose_bits(value, bits, n_bits, endian):
     _ = value, bits, n_bits, endian
 
 
+def hint_less_than(a, b, result_ptr):
+    _ = a, b, result_ptr
+
+
 def log2_ceil(x: int) -> int:
     assert x > 0
     return math.ceil(math.log2(x))

crates/lean_compiler/src/a_simplify_lang.rs

@@ -409,7 +409,10 @@ fn compile_time_transform_in_program(
             return Err("Inlined functions with mutable arguments are not supported yet".to_string());
         }
         if func.has_const_arguments() {
-            return Err("Inlined functions with constant arguments are not supported yet".to_string());
+            return Err(format!(
+                "Inlined function should not have \"Const\" arguments (function \"{}\")",
+                func.name
+            ));
         }
     }
 

crates/lean_compiler/src/c_compile_final.rs

@@ -1,4 +1,4 @@
-use crate::{F, ir::*, lang::*};
+use crate::{F, instruction_encoder::field_representation, ir::*, lang::*};
 use lean_vm::*;
 use multilinear_toolkit::prelude::*;
 use std::collections::BTreeMap;
@@ -144,6 +144,15 @@ pub fn compile_to_low_level_bytecode(
             &mut hints,
         );
     }
+    let instructions_encoded = instructions.par_iter().map(field_representation).collect::<Vec<_>>();
+
+    let mut instructions_multilinear = vec![];
+    for instr in &instructions_encoded {
+        instructions_multilinear.extend_from_slice(instr);
+        let padding = N_INSTRUCTION_COLUMNS.next_power_of_two() - N_INSTRUCTION_COLUMNS;
+        instructions_multilinear.extend(vec![F::ZERO; padding]);
+    }
+    instructions_multilinear.resize(instructions_multilinear.len().next_power_of_two(), F::ZERO);
 
     // Build pc_to_location mapping from LocationReport hints
     let mut pc_to_location = Vec::with_capacity(instructions.len());
@@ -164,6 +173,7 @@ pub fn compile_to_low_level_bytecode(
 
     Ok(Bytecode {
         instructions,
+        instructions_multilinear,
         hints,
         starting_frame_memory,
         function_locations,

crates/lean_prover/witness_generation/src/instruction_encoder.rs → crates/lean_compiler/src/instruction_encoder.rs

@@ -1,6 +1,5 @@
 use lean_vm::*;
 use multilinear_toolkit::prelude::*;
-use utils::padd_with_zero_to_next_power_of_two;
 
 pub fn field_representation(instr: &Instruction) -> [F; N_INSTRUCTION_COLUMNS] {
     let mut fields = [F::ZERO; N_INSTRUCTION_COLUMNS];
@@ -32,17 +31,17 @@ pub fn field_representation(instr: &Instruction) -> [F; N_INSTRUCTION_COLUMNS] {
             fields[instr_idx(COL_OPERAND_C)] = F::from_usize(*shift_1);
             match res {
                 MemOrFpOrConstant::Constant(cst) => {
-                    fields[instr_idx(COL_AUX_1)] = F::ONE;
+                    fields[instr_idx(COL_AUX)] = F::ONE;
                     fields[instr_idx(COL_FLAG_B)] = F::ONE;
                     fields[instr_idx(COL_OPERAND_B)] = *cst;
                 }
                 MemOrFpOrConstant::MemoryAfterFp { offset } => {
-                    fields[instr_idx(COL_AUX_1)] = F::ONE;
+                    fields[instr_idx(COL_AUX)] = F::ONE;
                     fields[instr_idx(COL_FLAG_B)] = F::ZERO;
                     fields[instr_idx(COL_OPERAND_B)] = F::from_usize(*offset);
                 }
                 MemOrFpOrConstant::Fp => {
-                    fields[instr_idx(COL_AUX_1)] = F::ZERO;
+                    fields[instr_idx(COL_AUX)] = F::ZERO;
                     fields[instr_idx(COL_FLAG_B)] = F::ONE;
                 }
             }
@@ -70,8 +69,8 @@ pub fn field_representation(instr: &Instruction) -> [F; N_INSTRUCTION_COLUMNS] {
             set_nu_a(&mut fields, arg_a);
             set_nu_b(&mut fields, arg_b);
             set_nu_c(&mut fields, arg_c);
-            fields[instr_idx(COL_AUX_1)] = F::from_usize(*aux_1);
-            fields[instr_idx(COL_AUX_2)] = F::from_usize(*aux_2);
+            assert!(*aux_2 == 0 || *aux_2 == 1);
+            fields[instr_idx(COL_AUX)] = F::from_usize(2 * *aux_1 + *aux_2);
         }
     }
     fields
@@ -114,11 +113,3 @@ fn set_nu_c(fields: &mut [F; N_INSTRUCTION_COLUMNS], c: &MemOrFp) {
         }
     }
 }
-
-pub fn bytecode_to_multilinear_polynomial(instructions: &[Instruction]) -> Vec<F> {
-    let res = instructions
-        .par_iter()
-        .flat_map(|instr| padd_with_zero_to_next_power_of_two(&field_representation(instr)))
-        .collect::<Vec<F>>();
-    padd_with_zero_to_next_power_of_two(&res)
-}

crates/lean_compiler/src/lib.rs

@@ -11,6 +11,7 @@ use crate::{
 mod a_simplify_lang;
 mod b_compile_intermediate;
 mod c_compile_final;
+mod instruction_encoder;
 pub mod ir;
 mod lang;
 mod parser;

crates/lean_compiler/src/parser/parsers/literal.rs

@@ -1,6 +1,4 @@
-use lean_vm::{
-    NONRESERVED_PROGRAM_INPUT_START, ONE_VEC_PTR, PRIVATE_INPUT_START_PTR, SAMPLING_DOMAIN_SEPARATOR_PTR, ZERO_VEC_PTR,
-};
+use lean_vm::{NONRESERVED_PROGRAM_INPUT_START, ONE_VEC_PTR, SAMPLING_DOMAIN_SEPARATOR_PTR, ZERO_VEC_PTR};
 use multilinear_toolkit::prelude::*;
 
 use super::expression::ExpressionParser;
@@ -133,7 +131,6 @@ impl VarOrConstantParser {
             "NONRESERVED_PROGRAM_INPUT_START" => Ok(SimpleExpr::Constant(ConstExpression::from(
                 NONRESERVED_PROGRAM_INPUT_START,
             ))),
-            "PRIVATE_INPUT_START_PTR" => Ok(SimpleExpr::Constant(ConstExpression::from(PRIVATE_INPUT_START_PTR))),
             "ZERO_VEC_PTR" => Ok(SimpleExpr::Constant(ConstExpression::from(ZERO_VEC_PTR))),
             "ONE_VEC_PTR" => Ok(SimpleExpr::Constant(ConstExpression::from(ONE_VEC_PTR))),
             "SAMPLING_DOMAIN_SEPARATOR_PTR" => Ok(SimpleExpr::Constant(ConstExpression::from(

crates/lean_prover/Cargo.toml

@@ -21,7 +21,6 @@ air.workspace = true
 sub_protocols.workspace = true
 lean_vm.workspace = true
 lean_compiler.workspace = true
-witness_generation.workspace = true
 multilinear-toolkit.workspace = true
 itertools.workspace = true
 

crates/lean_prover/src/lib.rs

@@ -4,56 +4,32 @@ use lean_vm::{EF, F};
 use multilinear_toolkit::prelude::*;
 use utils::*;
 
-use lean_vm::execute_bytecode;
-use witness_generation::*;
+mod trace_gen;
 
-mod common;
 pub mod prove_execution;
+pub mod verify_execution;
+
 #[cfg(test)]
 mod test_zkvm;
-pub mod verify_execution;
 
-pub use witness_generation::bytecode_to_multilinear_polynomial;
+use trace_gen::*;
 
 // Right now, hash digests = 8 koala-bear (p = 2^31 - 2^24 + 1, i.e. ≈ 30.98 bits per field element)
 // so ≈ 123.92 bits of security against collisions
-pub const SECURITY_BITS: usize = 123; // TODO 128 bits security (with Poseidon over 20 field elements)
+pub const SECURITY_BITS: usize = 123; // TODO 128 bits security? (with Poseidon over 20 field elements or with a more subtle soundness analysis (cf. https://eprint.iacr.org/2021/188.pdf))
 
 // Provable security (no proximity gaps conjectures)
 pub const SECURITY_REGIME: SecurityAssumption = SecurityAssumption::JohnsonBound;
 
-pub const GRINDING_BITS: usize = 16;
-
-pub const STARTING_LOG_INV_RATE_BASE: usize = 2;
-
-pub const STARTING_LOG_INV_RATE_EXTENSION: usize = 3;
-
-#[derive(Debug)]
-pub struct SnarkParams {
-    pub first_whir: WhirConfigBuilder,
-    pub second_whir: WhirConfigBuilder,
-}
-
-impl Default for SnarkParams {
-    fn default() -> Self {
-        Self {
-            first_whir: whir_config_builder(STARTING_LOG_INV_RATE_BASE, 7, 5),
-            second_whir: whir_config_builder(STARTING_LOG_INV_RATE_EXTENSION, 4, 1),
-        }
-    }
-}
+pub const GRINDING_BITS: usize = 18;
 
-pub fn whir_config_builder(
-    starting_log_inv_rate: usize,
-    first_folding_factor: usize,
-    rs_domain_initial_reduction_factor: usize,
-) -> WhirConfigBuilder {
+pub fn default_whir_config(starting_log_inv_rate: usize) -> WhirConfigBuilder {
     WhirConfigBuilder {
-        folding_factor: FoldingFactor::new(first_folding_factor, 4),
+        folding_factor: FoldingFactor::new(7, 5),
         soundness_type: SECURITY_REGIME,
         pow_bits: GRINDING_BITS,
-        max_num_variables_to_send_coeffs: 6,
-        rs_domain_initial_reduction_factor,
+        max_num_variables_to_send_coeffs: 9,
+        rs_domain_initial_reduction_factor: 5,
         security_level: SECURITY_BITS,
         starting_log_inv_rate,
     }