Make recursion program independent from the number of cycles / poseidons / dot products of the inner program

crates/lean_compiler/src/a_simplify_lang.rs

@@ -476,7 +476,8 @@ fn compile_time_transform_in_lines(
             value,
             location,
         } = line
-            && let Some(expanded) = try_expand_match_range(value, targets, *location)?
+            && let Some(expanded) =
+                try_expand_match_range(value, targets, *location, const_arrays, &vector_len_tracker)?
         {
             lines.splice(i..=i, expanded);
             continue;
@@ -642,10 +643,13 @@ fn compile_time_transform_in_lines(
                 end,
                 body,
                 unroll: true,
-                ..
+                location,
             } => {
                 let (Some(start), Some(end)) = (start.as_scalar(), end.as_scalar()) else {
-                    return Err("Cannot unroll loop with non-constant bounds".to_string());
+                    return Err(format!(
+                        "line {}: Cannot unroll loop with non-constant bounds",
+                        location
+                    ));
                 };
                 let unroll_index = unroll_counter.get_next();
                 let (internal_vars, _) = find_variable_usage(body, const_arrays);
@@ -686,6 +690,8 @@ fn try_expand_match_range(
     value: &Expression,
     targets: &[AssignmentTarget],
     location: SourceLocation,
+    const_arrays: &BTreeMap<String, ConstArrayValue>,
+    vector_len: &VectorLenTracker,
 ) -> Result<Option<Vec<Line>>, String> {
     let Expression::FunctionCall {
         function_name, args, ..
@@ -746,12 +752,12 @@ fn try_expand_match_range(
             return Err("match_range: expected range(start, end)".into());
         }
         let start = ra[0]
-            .as_scalar()
-            .ok_or("match_range: range start must be constant")?
+            .compile_time_eval(const_arrays, vector_len)
+            .ok_or(format!("match_range: range start must be constant (at {location})"))?
             .to_usize();
         let end = ra[1]
-            .as_scalar()
-            .ok_or("match_range: range end must be constant")?
+            .compile_time_eval(const_arrays, vector_len)
+            .ok_or(format!("match_range: range end must be constant (at {location})"))?
             .to_usize();
 
         // Parse lambda

crates/lean_prover/src/lib.rs

@@ -19,17 +19,20 @@ use trace_gen::*;
 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))
 
 pub const GRINDING_BITS: usize = 18;
+pub const MAX_NUM_VARIABLES_TO_SEND_COEFFS: usize = 8;
+pub const WHIR_INITIAL_FOLDING_FACTOR: usize = 7;
+pub const WHIR_SUBSEQUENT_FOLDING_FACTOR: usize = 5;
 
 pub fn default_whir_config(starting_log_inv_rate: usize, prox_gaps_conjecture: bool) -> WhirConfigBuilder {
     WhirConfigBuilder {
-        folding_factor: FoldingFactor::new(7, 5),
+        folding_factor: FoldingFactor::new(WHIR_INITIAL_FOLDING_FACTOR, WHIR_SUBSEQUENT_FOLDING_FACTOR),
         soundness_type: if prox_gaps_conjecture {
             SecurityAssumption::CapacityBound // TODO update formula with State of the Art Conjecture
         } else {
             SecurityAssumption::JohnsonBound
         },
         pow_bits: GRINDING_BITS,
-        max_num_variables_to_send_coeffs: 9,
+        max_num_variables_to_send_coeffs: MAX_NUM_VARIABLES_TO_SEND_COEFFS,
         rs_domain_initial_reduction_factor: 5,
         security_level: SECURITY_BITS,
         starting_log_inv_rate,

crates/lean_prover/src/prove_execution.rs

@@ -142,7 +142,11 @@ pub fn prove_execution(
     let air_alpha = prover_state.sample();
     let air_alpha_powers: Vec<EF> = air_alpha.powers().collect_n(max_air_constraints() + 1);
 
-    for (table, trace) in traces.iter() {
+    let tables_log_heights: BTreeMap<Table, VarCount> =
+        traces.iter().map(|(table, trace)| (*table, trace.log_n_rows)).collect();
+    let tables_sorted = sort_tables_by_height(&tables_log_heights);
+    for (table, _) in &tables_sorted {
+        let trace = &traces[table];
         let this_air_claims = prove_bus_and_air(
             &mut prover_state,
             table,
@@ -185,7 +189,6 @@ pub fn prove_execution(
         ),
     ];
 
-    let tables_log_heights = traces.iter().map(|(table, trace)| (*table, trace.log_n_rows)).collect();
     let global_statements_base = stacked_pcs_global_statements(
         stacked_pcs_witness.stacked_n_vars,
         log2_strict_usize(memory.len()),

crates/lean_prover/src/verify_execution.rs

@@ -97,7 +97,8 @@ pub fn verify_execution(
     let air_alpha = verifier_state.sample();
     let air_alpha_powers: Vec<EF> = air_alpha.powers().collect_n(max_air_constraints() + 1);
 
-    for (table, log_n_rows) in &table_n_vars {
+    let tables_sorted = sort_tables_by_height(&table_n_vars);
+    for (table, log_n_rows) in &tables_sorted {
         let this_air_claims = verify_bus_and_air(
             &mut verifier_state,
             table,

crates/rec_aggregation/fiat_shamir.py

@@ -95,12 +95,25 @@ def fs_receive_chunks(fs, n_chunks: Const):
 
 
 @inline
-def fs_receive_ef(fs, n):
+def fs_receive_ef_inlined(fs, n):
     new_fs, ef_ptr = fs_receive_chunks(fs, div_ceil(n * DIM, 8))
     for i in unroll(n * DIM, next_multiple_of(n * DIM, 8)):
         assert ef_ptr[i] == 0
     return new_fs, ef_ptr
 
+def fs_receive_ef_by_log_dynamic(fs, log_n, min_value: Const, max_value: Const):
+    debug_assert(log_n < max_value)
+    debug_assert(min_value <= log_n)
+    new_fs: Imu
+    ef_ptr: Imu
+    new_fs, ef_ptr = match_range(log_n, range(min_value, max_value), lambda ln: fs_receive_ef(fs, 2**ln))
+    return new_fs, ef_ptr
+
+def fs_receive_ef(fs, n: Const):
+    new_fs, ef_ptr = fs_receive_chunks(fs, div_ceil(n * DIM, 8))
+    for i in unroll(n * DIM, next_multiple_of(n * DIM, 8)):
+        assert ef_ptr[i] == 0
+    return new_fs, ef_ptr
 
 def fs_print_state(fs_state):
     for i in unroll(0, 9):