don't harcode LOG_INV_RATE in recursion program

Author: TomWambsgans

crates/lean_prover/src/prove_execution.rs

@@ -51,7 +51,7 @@ pub fn prove_execution(
     let mut prover_state = build_prover_state();
     prover_state.add_base_scalars(
         &[
-            vec![log2_strict_usize(memory.len())],
+            vec![whir_config.starting_log_inv_rate, log2_strict_usize(memory.len())],
             traces.values().map(|t| t.log_n_rows).collect::<Vec<_>>(),
         ]
         .concat()

crates/lean_prover/src/test_zkvm.rs

@@ -162,7 +162,7 @@ fn test_zk_vm_helper(program_str: &str, (public_input, private_input): (&[F], &[
         &bytecode,
         public_input,
         proof.proof.clone(),
-        &default_whir_config(starting_log_inv_rate, false),
+        default_whir_config(starting_log_inv_rate, false),
     )
     .unwrap();
     println!("{}", proof.exec_summary);
@@ -183,7 +183,7 @@ fn test_zk_vm_helper(program_str: &str, (public_input, private_input): (&[F], &[
                 &bytecode,
                 public_input,
                 fuzzed_proof,
-                &default_whir_config(starting_log_inv_rate, false),
+                default_whir_config(starting_log_inv_rate, false),
             );
             assert!(verify_result.is_err(), "Fuzzing failed at index {}", i);
         }

crates/lean_prover/src/verify_execution.rs

@@ -20,17 +20,22 @@ pub fn verify_execution(
     bytecode: &Bytecode,
     public_input: &[F],
     proof: Vec<F>,
-    whir_config: &WhirConfigBuilder,
+    mut whir_config: WhirConfigBuilder,
 ) -> Result<ProofVerificationDetails, ProofError> {
     let mut verifier_state = VerifierState::<EF, _>::new(proof, get_poseidon16().clone());
 
     let dims = verifier_state
-        .next_base_scalars_vec(1 + N_TABLES)?
+        .next_base_scalars_vec(2 + N_TABLES)?
         .into_iter()
         .map(|x| x.to_usize())
         .collect::<Vec<_>>();
-    let log_memory = dims[0];
-    let table_n_vars: BTreeMap<Table, VarCount> = (0..N_TABLES).map(|i| (ALL_TABLES[i], dims[i + 1])).collect();
+    let log_inv_rate = dims[0];
+    let log_memory = dims[1];
+    let table_n_vars: BTreeMap<Table, VarCount> = (0..N_TABLES).map(|i| (ALL_TABLES[i], dims[i + 2])).collect();
+    if !(MIN_WHIR_LOG_INV_RATE..=MAX_WHIR_LOG_INV_RATE).contains(&log_inv_rate) {
+        return Err(ProofError::InvalidProof);
+    }
+    whir_config.starting_log_inv_rate = log_inv_rate;
     for (table, &n_vars) in &table_n_vars {
         if n_vars < MIN_LOG_N_ROWS_PER_TABLE {
             return Err(ProofError::InvalidProof);
@@ -57,7 +62,7 @@ pub fn verify_execution(
     }
 
     let parsed_commitment = stacked_pcs_parse_commitment(
-        whir_config,
+        &whir_config,
         &mut verifier_state,
         log_memory,
         bytecode.log_size(),
@@ -145,7 +150,7 @@ pub fn verify_execution(
         &committed_statements,
     );
     let total_whir_statements = global_statements_base.iter().map(|s| s.values.len()).sum();
-    WhirConfig::new(whir_config, parsed_commitment.num_variables).verify(
+    WhirConfig::new(&whir_config, parsed_commitment.num_variables).verify(
         &mut verifier_state,
         &parsed_commitment,
         global_statements_base,

crates/lean_vm/src/core/constants.rs

@@ -5,6 +5,9 @@ pub const DIMENSION: usize = 5;
 
 pub const DIGEST_LEN: usize = 8;
 
+pub const MIN_WHIR_LOG_INV_RATE: usize = 1;
+pub const MAX_WHIR_LOG_INV_RATE: usize = 4;
+
 /// Minimum and maximum memory size (as powers of two)
 pub const MIN_LOG_MEMORY_SIZE: usize = 16;
 pub const MAX_LOG_MEMORY_SIZE: usize = 26;

crates/lean_vm/src/execution/memory.rs

@@ -50,7 +50,7 @@ impl Memory {
             if index >= 1 << MAX_LOG_MEMORY_SIZE {
                 return Err(RunnerError::OutOfMemory);
             }
-            self.0.resize((index + 1).next_power_of_two(), None);
+            self.0.resize(index + 1, None);
         }
         if let Some(existing) = &mut self.0[index] {
             if *existing != value {

crates/rec_aggregation/recursion.py

@@ -2,6 +2,9 @@
 from whir import *
 
 N_TABLES = N_TABLES_PLACEHOLDER
+
+MIN_WHIR_LOG_INV_RATE = MIN_WHIR_LOG_INV_RATE_PLACEHOLDER
+MAX_WHIR_LOG_INV_RATE = MAX_WHIR_LOG_INV_RATE_PLACEHOLDER
 MIN_LOG_N_ROWS_PER_TABLE = MIN_LOG_N_ROWS_PER_TABLE_PLACEHOLDER
 MAX_LOG_N_ROWS_PER_TABLE = MAX_LOG_N_ROWS_PER_TABLE_PLACEHOLDER
 MIN_LOG_MEMORY_SIZE = MIN_LOG_MEMORY_SIZE_PLACEHOLDER
@@ -61,12 +64,16 @@ def recursion(inner_public_memory_log_size, inner_public_memory, proof_transcrip
 
     # table dims
     debug_assert(N_TABLES + 1 < DIGEST_LEN)
-    fs, mem_and_table_dims = fs_receive_chunks(fs, 1)
-    for i in unroll(N_TABLES + 1, 8):
-        assert mem_and_table_dims[i] == 0
-    log_memory = mem_and_table_dims[0]
+    fs, dims = fs_receive_chunks(fs, 1)
+    for i in unroll(N_TABLES + 2, 8):
+        assert dims[i] == 0
+    whir_log_inv_rate = dims[0]
+    log_memory = dims[1]
+    table_log_heights = dims + 2
+
+    assert MIN_WHIR_LOG_INV_RATE <= whir_log_inv_rate
+    assert whir_log_inv_rate <= MAX_WHIR_LOG_INV_RATE
 
-    table_log_heights = mem_and_table_dims + 1
     log_n_cycles = table_log_heights[EXECUTION_TABLE_INDEX]
     assert log_n_cycles <= log_memory
 
@@ -85,6 +92,7 @@ def recursion(inner_public_memory_log_size, inner_public_memory, proof_transcrip
     assert log_memory <= GUEST_BYTECODE_LEN
 
     stacked_n_vars = compute_stacked_n_vars(log_memory, log_bytecode_padded, table_heights)
+    assert stacked_n_vars <= TWO_ADICITY + WHIR_FOLDING_FACTORS[0] - whir_log_inv_rate
 
     fs, whir_base_root, whir_base_ood_points, whir_base_ood_evals = parse_whir_commitment_const(fs, WHIR_NUM_OOD_COMMIT)
 
@@ -486,6 +494,7 @@ def recursion(inner_public_memory_log_size, inner_public_memory, proof_transcrip
     fs, folding_randomness_global, s, final_value, end_sum = whir_open(
         fs,
         stacked_n_vars,
+        whir_log_inv_rate,
         whir_base_root,
         whir_base_ood_points,
         combination_randomness_powers,

crates/rec_aggregation/src/recursion.rs

@@ -65,20 +65,12 @@ def main():
         &bytecode_to_prove,
         &inner_public_input,
         proof_to_prove.proof.clone(),
-        &inner_whir_config,
+        inner_whir_config.clone(),
     )
     .unwrap();
 
     let outer_whir_config = WhirConfig::<EF>::new(&inner_whir_config, proof_to_prove.whir_n_vars);
 
-    // let guest_program_commitment = {
-    //     let mut prover_state = build_prover_state();
-    //     let polynomial = MleOwned::Base(bytecode_to_multilinear_polynomial(&bytecode_to_prove.instructions));
-    //     let witness = ext_whir.commit(&mut prover_state, &polynomial);
-    //     let commitment_transcript = prover_state.proof().to_vec();
-    //     assert_eq!(commitment_transcript.len(), ext_whir.committment_ood_samples * DIMENSION + VECTOR_LEN);
-    // };
-
     let mut replacements = whir_recursion_placeholder_replacements(&outer_whir_config);
 
     assert!(
@@ -106,6 +98,14 @@ def main():
     max_log_n_rows_per_table.sort_by_key(|(table, _)| table.index());
     max_log_n_rows_per_table.dedup();
     assert_eq!(max_log_n_rows_per_table.len(), N_TABLES);
+    replacements.insert(
+        "MIN_WHIR_LOG_INV_RATE_PLACEHOLDER".to_string(),
+        MIN_WHIR_LOG_INV_RATE.to_string(),
+    );
+    replacements.insert(
+        "MAX_WHIR_LOG_INV_RATE_PLACEHOLDER".to_string(),
+        MAX_WHIR_LOG_INV_RATE.to_string(),
+    );
     replacements.insert(
         "MAX_LOG_N_ROWS_PER_TABLE_PLACEHOLDER".to_string(),
         format!(
@@ -335,7 +335,7 @@ def main():
         &recursion_bytecode,
         &outer_public_input,
         recursion_proof.proof,
-        &default_whir_config(log_inv_rate, prox_gaps_conjecture),
+        default_whir_config(log_inv_rate, prox_gaps_conjecture),
     )
     .unwrap();
     println!(
@@ -396,10 +396,6 @@ pub(crate) fn whir_recursion_placeholder_replacements(whir_config: &WhirConfig<E
         format!("WHIR_FOLDING_FACTORS{}", end),
         format!("[{}]", folding_factors.join(", ")),
     );
-    replacements.insert(
-        format!("WHIR_LOG_INV_RATE{}", end),
-        whir_config.starting_log_inv_rate.to_string(),
-    );
     replacements.insert(
         format!("WHIR_FINAL_VARS{}", end),
         whir_config.n_vars_of_final_polynomial().to_string(),

crates/rec_aggregation/src/xmss_aggregate.rs

@@ -223,7 +223,7 @@ pub fn xmss_verify_aggregated_signatures(
         program,
         &public_input,
         proof,
-        &default_whir_config(log_inv_rate, prox_gaps_conjecture),
+        default_whir_config(log_inv_rate, prox_gaps_conjecture),
     )
     .map(|_| ())
 }

crates/rec_aggregation/whir.py

@@ -1,7 +1,6 @@
 from snark_lib import *
 from fiat_shamir import *
 
-WHIR_LOG_INV_RATE = WHIR_LOG_INV_RATE_PLACEHOLDER
 WHIR_FOLDING_FACTORS = WHIR_FOLDING_FACTORS_PLACEHOLDER
 WHIR_FINAL_VARS = WHIR_FINAL_VARS_PLACEHOLDER
 WHIR_FIRST_RS_REDUCTION_FACTOR = WHIR_FIRST_RS_REDUCTION_FACTOR_PLACEHOLDER
@@ -13,6 +12,7 @@
 def whir_open(
     fs: Mut,
     n_vars,
+    initial_log_inv_rate,
     root: Mut,
     ood_points_commit,
     combination_randomness_powers_0,
@@ -23,7 +23,7 @@ def whir_open(
     all_circle_values = Array(WHIR_N_ROUNDS + 1)
     all_combination_randomness_powers = Array(WHIR_N_ROUNDS)
 
-    domain_sz: Mut = n_vars + WHIR_LOG_INV_RATE
+    domain_sz: Mut = n_vars + initial_log_inv_rate
     for r in unroll(0, WHIR_N_ROUNDS):
         is_first_round: Imu
         if r == 0:

crates/sub_protocols/src/stacked_pcs.rs

@@ -167,6 +167,11 @@ pub fn stacked_pcs_parse_commitment(
     }
 
     let stacked_n_vars = compute_stacked_n_vars(log_memory, log_bytecode, tables_heights);
+    if stacked_n_vars
+        > F::TWO_ADICITY + whir_config_builder.folding_factor.at_round(0) - whir_config_builder.starting_log_inv_rate
+    {
+        return Err(ProofError::InvalidProof);
+    }
     WhirConfig::new(whir_config_builder, stacked_n_vars).parse_commitment(verifier_state)
 }