Recursive aggregation

README.md

@@ -30,7 +30,7 @@ Machine: M4 Max 48GB (CPU only)
 
 ### XMSS aggregation
 
-```
+```bash
 cargo run --release -- xmss --n-signatures 1350
 ```
 
@@ -43,7 +43,7 @@ cargo run --release -- xmss --n-signatures 1350
 
 ### Recursion
 
-```
+```bash
 cargo run --release -- recursion --n 2
 ```
 
@@ -53,6 +53,17 @@ cargo run --release -- recursion --n 2
 | --------------- | --------------- |
 | 1.10s - 223 KiB | 1.05s - 134 KiB |
 
+
+### Bonus: unbounded recursive aggregation
+
+```bash
+cargo run --release -- fancy-aggregation
+```
+
+![Recursive aggregation](./misc/images/rec-agg.png)
+
+(Proven regime)
+
 ## Credits
 
 - [Plonky3](https://github.com/Plonky3/Plonky3) for its various performant crates

crates/lean_compiler/src/lib.rs

@@ -153,7 +153,8 @@ pub fn try_compile_and_run(
 ) -> Result<String, Error> {
     let bytecode = try_compile_program(input)?;
     let result = try_execute_bytecode(&bytecode, (public_input, private_input), profiler, &vec![])?;
-    Ok(result.summary)
+    println!("{}", result.metadata.display());
+    Ok(result.metadata.display())
 }
 
 pub fn compile_and_run(input: &ProgramSource, (public_input, private_input): (&[F], &[F]), profiler: bool) {

crates/lean_prover/src/prove_execution.rs

@@ -14,8 +14,7 @@ use xmss::Poseidon16History;
 pub struct ExecutionProof {
     pub proof: Vec<F>,
     pub proof_size_fe: usize,
-    pub exec_summary: String,
-    pub whir_n_vars: usize,
+    pub metadata: ExecutionMetadata,
 }
 
 pub fn prove_execution(
@@ -25,22 +24,21 @@ pub fn prove_execution(
     whir_config: &WhirConfigBuilder,
     vm_profiler: bool,
 ) -> ExecutionProof {
-    let mut exec_summary = String::new();
     let ExecutionTrace {
         traces,
         public_memory_size,
         non_zero_memory_size: _, // TODO use the information of the ending zeros for speedup
         mut memory,              // padded with zeros to next power of two
+        metadata,
     } = info_span!("Witness generation").in_scope(|| {
-        let mut execution_result = info_span!("Executing bytecode").in_scope(|| {
+        let execution_result = info_span!("Executing bytecode").in_scope(|| {
             execute_bytecode(
                 bytecode,
                 (public_input, private_input),
                 vm_profiler,
                 poseidons_16_precomputed,
             )
         });
-        exec_summary = std::mem::take(&mut execution_result.summary);
         info_span!("Building execution trace").in_scope(|| get_execution_trace(bytecode, execution_result))
     });
 
@@ -50,7 +48,6 @@ pub fn prove_execution(
     if memory.len() < min_memory_size {
         memory.resize(min_memory_size, F::ZERO);
     }
-
     let mut prover_state = build_prover_state();
     prover_state.add_base_scalars(
         &[
@@ -113,7 +110,6 @@ pub fn prove_execution(
         &bytecode_acc,
         &traces,
     );
-    let whir_n_vars = stacked_pcs_witness.global_polynomial.by_ref().n_vars();
 
     // logup (GKR)
     let logup_c = prover_state.sample();
@@ -212,8 +208,7 @@ pub fn prove_execution(
     ExecutionProof {
         proof: prover_state.raw_proof(),
         proof_size_fe,
-        exec_summary,
-        whir_n_vars,
+        metadata,
     }
 }
 

crates/lean_prover/src/test_zkvm.rs

@@ -158,14 +158,8 @@ fn test_zk_vm_helper(program_str: &str, (public_input, private_input): (&[F], &[
         false,
     );
     let proof_time = time.elapsed();
-    verify_execution(
-        &bytecode,
-        public_input,
-        proof.proof.clone(),
-        default_whir_config(starting_log_inv_rate, false),
-    )
-    .unwrap();
-    println!("{}", proof.exec_summary);
+    verify_execution(&bytecode, public_input, proof.proof.clone(), false).unwrap();
+    println!("{}", proof.metadata.display());
     println!("Proof time: {:.3} s", proof_time.as_secs_f32());
 
     if fuzzing {
@@ -179,12 +173,7 @@ fn test_zk_vm_helper(program_str: &str, (public_input, private_input): (&[F], &[
             }
             let mut fuzzed_proof = proof.proof.clone();
             fuzzed_proof[i] += F::ONE;
-            let verify_result = verify_execution(
-                &bytecode,
-                public_input,
-                fuzzed_proof,
-                default_whir_config(starting_log_inv_rate, false),
-            );
+            let verify_result = verify_execution(&bytecode, public_input, fuzzed_proof, false);
             assert!(verify_result.is_err(), "Fuzzing failed at index {}", i);
         }
     }

crates/lean_prover/src/trace_gen.rs

@@ -9,6 +9,7 @@ pub struct ExecutionTrace {
     pub public_memory_size: usize,
     pub non_zero_memory_size: usize,
     pub memory: Vec<F>, // of length a multiple of public_memory_size
+    pub metadata: ExecutionMetadata,
 }
 
 pub fn get_execution_trace(bytecode: &Bytecode, execution_result: ExecutionResult) -> ExecutionTrace {
@@ -37,13 +38,13 @@ pub fn get_execution_trace(bytecode: &Bytecode, execution_result: ExecutionResul
                 // flag_a == 0
                 addr_a = F::from_usize(fp) + field_repr[instr_idx(COL_OPERAND_A)]; // fp + operand_a
             }
-            let value_a = memory.0[addr_a.to_usize()].unwrap_or_default();
+            let value_a = memory.0.get(addr_a.to_usize()).copied().flatten().unwrap_or_default();
             let mut addr_b = F::ZERO;
             if field_repr[instr_idx(COL_FLAG_B)].is_zero() {
                 // flag_b == 0
                 addr_b = F::from_usize(fp) + field_repr[instr_idx(COL_OPERAND_B)]; // fp + operand_b
             }
-            let value_b = memory.0[addr_b.to_usize()].unwrap_or_default();
+            let value_b = memory.0.get(addr_b.to_usize()).copied().flatten().unwrap_or_default();
 
             let mut addr_c = F::ZERO;
             if field_repr[instr_idx(COL_FLAG_C)].is_zero() {
@@ -54,7 +55,7 @@ pub fn get_execution_trace(bytecode: &Bytecode, execution_result: ExecutionResul
                 assert_eq!(field_repr[instr_idx(COL_OPERAND_C)], operand_c); // debug purpose
                 addr_c = value_a + operand_c;
             }
-            let value_c = memory.0[addr_c.to_usize()].unwrap_or_default();
+            let value_c = memory.0.get(addr_c.to_usize()).copied().flatten().unwrap_or_default();
 
             for (j, field) in field_repr.iter().enumerate() {
                 *trace_row[j + N_RUNTIME_COLUMNS] = *field;
@@ -114,6 +115,7 @@ pub fn get_execution_trace(bytecode: &Bytecode, execution_result: ExecutionResul
         public_memory_size: execution_result.public_memory_size,
         non_zero_memory_size: memory.0.len(),
         memory: memory_padded,
+        metadata: execution_result.metadata,
     }
 }
 

crates/lean_prover/src/verify_execution.rs

@@ -9,17 +9,14 @@ use utils::ToUsize;
 
 #[derive(Debug, Clone)]
 pub struct ProofVerificationDetails {
-    pub log_memory: usize,
-    pub table_n_vars: BTreeMap<Table, VarCount>,
-    pub first_quotient_gkr_n_vars: usize,
     pub bytecode_evaluation: Evaluation<EF>,
 }
 
 pub fn verify_execution(
     bytecode: &Bytecode,
     public_input: &[F],
     proof: Vec<F>,
-    mut whir_config: WhirConfigBuilder,
+    prox_gaps_conjecture: bool,
 ) -> Result<ProofVerificationDetails, ProofError> {
     let mut verifier_state = VerifierState::<EF, _>::new(proof, get_poseidon16().clone());
 
@@ -34,7 +31,7 @@ pub fn verify_execution(
     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;
+    let whir_config = default_whir_config(log_inv_rate, prox_gaps_conjecture);
     for (table, &n_vars) in &table_n_vars {
         if n_vars < MIN_LOG_N_ROWS_PER_TABLE {
             return Err(ProofError::InvalidProof);
@@ -161,9 +158,6 @@ pub fn verify_execution(
     )?;
 
     Ok(ProofVerificationDetails {
-        log_memory,
-        table_n_vars,
-        first_quotient_gkr_n_vars: logup_statements.total_gkr_n_vars,
         bytecode_evaluation: logup_statements.bytecode_evaluation.unwrap(),
     })
 }

crates/lean_vm/src/diagnostics/exec_result.rs

@@ -5,6 +5,80 @@ use crate::diagnostics::profiler::MemoryProfile;
 use crate::execution::Memory;
 use crate::{N_TABLES, Table, TableTrace};
 use thiserror::Error;
+use utils::pretty_integer;
+
+#[derive(Debug, Default)]
+pub struct ExecutionMetadata {
+    pub cycles: usize,
+    pub memory: usize,
+    pub n_poseidons: usize,
+    pub n_dot_products: usize,
+    pub bytecode_size: usize,
+    pub public_input_size: usize,
+    pub private_input_size: usize,
+    pub runtime_memory: usize,
+    pub memory_usage_percent: f64,
+    pub n_poseidon_precomputed_used: usize,
+    pub n_poseidons_precomputed_total: usize,
+    pub stdout: String,
+    pub profiling_report: Option<String>,
+}
+
+impl ExecutionMetadata {
+    pub fn display(&self) -> String {
+        let mut out = String::new();
+
+        if let Some(ref report) = self.profiling_report {
+            out.push_str(report);
+        }
+
+        if !self.stdout.is_empty() {
+            out.push_str("╔═════════════════════════════════════════════════════════════════════════╗\n");
+            out.push_str("║                                STD-OUT                                  ║\n");
+            out.push_str("╚═════════════════════════════════════════════════════════════════════════╝\n");
+            out.push_str(&format!("\n{}", self.stdout));
+            out.push_str("──────────────────────────────────────────────────────────────────────────\n\n");
+        }
+
+        out.push_str("╔═════════════════════════════════════════════════════════════════════════╗\n");
+        out.push_str("║                                 STATS                                   ║\n");
+        out.push_str("╚═════════════════════════════════════════════════════════════════════════╝\n\n");
+
+        out.push_str(&format!("CYCLES: {}\n", pretty_integer(self.cycles)));
+        out.push_str(&format!("MEMORY: {}\n", pretty_integer(self.memory)));
+        out.push('\n');
+        out.push_str(&format!("Bytecode size: {}\n", pretty_integer(self.bytecode_size)));
+        out.push_str(&format!(
+            "Public input size: {}\n",
+            pretty_integer(self.public_input_size)
+        ));
+        out.push_str(&format!(
+            "Private input size: {}\n",
+            pretty_integer(self.private_input_size)
+        ));
+        out.push_str(&format!("Runtime memory: {}\n", pretty_integer(self.runtime_memory)));
+        out.push_str(&format!("Memory usage: {:.1}%\n", self.memory_usage_percent));
+        out.push_str(&format!(
+            "Poseidon2_16 precomputed used: {}/{}\n",
+            pretty_integer(self.n_poseidon_precomputed_used),
+            pretty_integer(self.n_poseidons_precomputed_total)
+        ));
+        out.push('\n');
+        if self.n_poseidons > 0 {
+            out.push_str(&format!(
+                "Poseidon2_16 calls: {} (1 poseidon per {} instructions)\n",
+                pretty_integer(self.n_poseidons),
+                self.cycles / self.n_poseidons
+            ));
+        }
+        if self.n_dot_products > 0 {
+            out.push_str(&format!("DotProduct calls: {}\n", pretty_integer(self.n_dot_products)));
+        }
+        out.push_str("──────────────────────────────────────────────────────────────────────────\n");
+
+        out
+    }
+}
 
 #[derive(Debug)]
 pub struct ExecutionResult {
@@ -14,6 +88,5 @@ pub struct ExecutionResult {
     pub pcs: Vec<usize>,
     pub fps: Vec<usize>,
     pub traces: BTreeMap<Table, TableTrace>,
-    pub summary: String,
-    pub memory_profile: Option<MemoryProfile>,
+    pub metadata: ExecutionMetadata,
 }

crates/lean_vm/src/diagnostics/profiler.rs

@@ -10,6 +10,7 @@ use crate::{ExecutionHistory, NONRESERVED_PROGRAM_INPUT_START};
 pub(crate) fn profiling_report(
     instructions: &ExecutionHistory,
     function_locations: &BTreeMap<SourceLocation, String>,
+    mem_profile: &MemoryProfile,
 ) -> String {
     #[derive(Default, Clone)]
     struct FunctionStats {
@@ -56,6 +57,9 @@ pub(crate) fn profiling_report(
 
     let mut report = String::new();
 
+    // memory profiling report
+    report += &memory_profiling_report(mem_profile);
+
     report.push_str("\n╔═════════════════════════════════════════════════════════════════════════╗\n");
     report.push_str("║                              PROFILING REPORT                           ║\n");
     report.push_str("╚═════════════════════════════════════════════════════════════════════════╝\n\n");