From b5b9c30fcd52bcffd296c03ab0f5030515afceb0 Mon Sep 17 00:00:00 2001 From: Adam Mohammed A Latif Date: Thu, 6 Aug 2026 12:32:58 +0000 Subject: [PATCH 01/22] research: add 84f Gate 0 measurement seam --- crates/lean_vm/src/lib.rs | 32 +- crates/pcs/src/stack_open.rs | 25 +- crates/pcs/src/whir.rs | 249 +++++-- crates/rec_aggregation/src/lib.rs | 7 +- crates/rec_aggregation/src/recursion.rs | 902 ++++++++++++++++++++++++ src/main.rs | 105 ++- 6 files changed, 1250 insertions(+), 70 deletions(-) diff --git a/crates/lean_vm/src/lib.rs b/crates/lean_vm/src/lib.rs index 748c2869..0ca4233c 100644 --- a/crates/lean_vm/src/lib.rs +++ b/crates/lean_vm/src/lib.rs @@ -75,13 +75,41 @@ pub const SECURITY_BITS: u32 = 128; /// overhead is not worth it for small inputs. Shared by [`constraints`], [`gkr`], [`leaf`]. pub(crate) const PAR_THRESHOLD: usize = 1 << 11; +fn gate0_trace_enabled() -> bool { + static ENABLED: std::sync::OnceLock = std::sync::OnceLock::new(); + *ENABLED.get_or_init(|| std::env::var_os("LEANVM_GATE0_TRACE").as_deref() == Some(std::ffi::OsStr::new("1"))) +} + +fn gate0_trace_event(kind: &str, id: u64, name: &str) { + static ORIGIN: std::sync::OnceLock = std::sync::OnceLock::new(); + let process_ns = ORIGIN.get_or_init(std::time::Instant::now).elapsed().as_nanos(); + let unix_ns = std::time::SystemTime::now() + .duration_since(std::time::UNIX_EPOCH) + .expect("system clock is after the Unix epoch") + .as_nanos(); + eprintln!( + "LEANVM_GATE0_EVENT schema=1 source=lean_vm kind={kind} id={id} name={name:?} unix_ns={unix_ns} process_ns={process_ns} pid={}", + std::process::id() + ); +} + /// Run one prover stage inside its `tracing` span and, under `LEANVM_PROFILE`, -/// report its wall time. Called through [`stage!`], which spells the stage's name -/// once for both. +/// report its wall time. `LEANVM_GATE0_TRACE=1` adds stable start and end +/// lifecycle records without changing the proof transcript. Called through +/// [`stage!`], which spells the stage's name once for both. pub(crate) fn stage_impl(name: &str, span: tracing::Span, f: impl FnOnce() -> T) -> T { static PROFILE: std::sync::OnceLock = std::sync::OnceLock::new(); + static NEXT_ID: std::sync::atomic::AtomicU64 = std::sync::atomic::AtomicU64::new(1); + let trace = gate0_trace_enabled(); + let id = NEXT_ID.fetch_add(1, std::sync::atomic::Ordering::Relaxed); + if trace { + gate0_trace_event("start", id, name); + } let t = std::time::Instant::now(); let out = span.in_scope(f); + if trace { + gate0_trace_event("end", id, name); + } if *PROFILE.get_or_init(|| std::env::var_os("LEANVM_PROFILE").is_some()) { eprintln!("[profile] {name:<20}: {:>8.2} ms", t.elapsed().as_secs_f64() * 1e3); } diff --git a/crates/pcs/src/stack_open.rs b/crates/pcs/src/stack_open.rs index 6fd80f13..9ffae3e7 100644 --- a/crates/pcs/src/stack_open.rs +++ b/crates/pcs/src/stack_open.rs @@ -332,6 +332,7 @@ pub fn open_batch_mixed_whir_stacked( // 1. Ring-switch reduction: observe every claim's s_hat_v, sample one // shared linear map, then finish each claim against that map. + let gate0_ring_switch = super::whir::Gate0Span::new("stack_open_ring_switch"); let qflock = &stack[ring.offset..ring.offset + qflock_len]; let mut rs_proofs = Vec::with_capacity(ring.claims.len()); let mut rs_states = Vec::with_capacity(ring.claims.len()); @@ -362,6 +363,7 @@ pub fn open_batch_mixed_whir_stacked( .zip(gammas_rs) .map(|(state, gamma)| ring_switch::prove_finish_deferred(state, &coordinate_weights, gamma)) .collect(); + drop(gate0_ring_switch); mark("ring-switch proves", &mut t); // 2. Observe point-claim values + sample their gammas (Schwartz-Zippel @@ -385,6 +387,7 @@ pub fn open_batch_mixed_whir_stacked( // // SAFETY: every slot is written before it is read: the fill covers everything // outside the q_flock block, and `combine_deferred_into` writes the block. + let gate0_basis = super::whir::Gate0Span::new("stack_open_build_basis"); let mut b_stack = unsafe { zk_alloc::ArenaVec::::uninitialized(stack.len()) }; { const ZERO_CHUNK: usize = 1 << 16; @@ -398,19 +401,23 @@ pub fn open_batch_mixed_whir_stacked( mark("rs_eq_ind scatter", &mut t); } fold_stacked_point_claims(&mut b_stack, &mut target, point_claims, &gammas_pd); + drop(gate0_basis); mark("point-claim folds", &mut t); // 4. One WHIR over the full stack against the combined claim (the // stack is borrowed by the prover; no copy). - let whir = recursive_prover_with_basis( - config, - stack, - b_stack, - target, - &prover_data.codeword, - &prover_data.merkle_tree, - sponge, - ); + let whir = { + let _gate0 = super::whir::Gate0Span::new("stack_open_whir"); + recursive_prover_with_basis( + config, + stack, + b_stack, + target, + &prover_data.codeword, + &prover_data.merkle_tree, + sponge, + ) + }; BatchOpeningProof { ring_switches: rs_proofs, whir, diff --git a/crates/pcs/src/whir.rs b/crates/pcs/src/whir.rs index d83f97a5..540c6a63 100644 --- a/crates/pcs/src/whir.rs +++ b/crates/pcs/src/whir.rs @@ -56,6 +56,54 @@ pub use super::whir_config::{default_config, default_verifier_config, udr_querie pub use crate::whir_induce::*; use crate::whir_ntt_ext::*; +fn gate0_trace_enabled() -> bool { + static ENABLED: std::sync::OnceLock = std::sync::OnceLock::new(); + *ENABLED.get_or_init(|| std::env::var_os("LEANVM_GATE0_TRACE").as_deref() == Some(std::ffi::OsStr::new("1"))) +} + +fn gate0_trace_event(kind: &str, id: u64, name: &str) { + static ORIGIN: std::sync::OnceLock = std::sync::OnceLock::new(); + let process_ns = ORIGIN.get_or_init(std::time::Instant::now).elapsed().as_nanos(); + let unix_ns = std::time::SystemTime::now() + .duration_since(std::time::UNIX_EPOCH) + .expect("system clock is after the Unix epoch") + .as_nanos(); + eprintln!( + "LEANVM_GATE0_EVENT schema=1 source=pcs kind={kind} id={id} name={name:?} unix_ns={unix_ns} process_ns={process_ns} pid={}", + std::process::id() + ); +} + +pub(crate) struct Gate0Span { + enabled: bool, + id: u64, + name: &'static str, +} + +impl Gate0Span { + pub(crate) fn new(name: &'static str) -> Self { + static NEXT_ID: std::sync::atomic::AtomicU64 = std::sync::atomic::AtomicU64::new(2_000_000); + let enabled = gate0_trace_enabled(); + let id = if enabled { + NEXT_ID.fetch_add(1, std::sync::atomic::Ordering::Relaxed) + } else { + 0 + }; + if enabled { + gate0_trace_event("start", id, name); + } + Self { enabled, id, name } + } +} + +impl Drop for Gate0Span { + fn drop(&mut self) { + if self.enabled { + gate0_trace_event("end", self.id, self.name); + } + } +} + /// Bind a Merkle root into the transcript as two `F192` scalars rather than /// as a byte string. Binds the root before any challenge exactly as `absorb_bytes` /// would; keeping the scalar form matches the recursion guest's replay. @@ -359,10 +407,13 @@ pub fn commit(message: &[F64], log_batch_size: usize, log_inv_rate: usize) -> (C // work when unset. let trace = std::env::var_os("WHIR_TRACE").is_some(); let t_ntt = std::time::Instant::now(); - tracing::info_span!("NTT", kind = "base encode", log_domain = k_code, lanes = num_ntts).in_scope(|| { - let ntt = AdditiveNttF64::standard(k_code); - ntt.encode_interleaved(&mut codeword, message, num_ntts, log_inv_rate); - }); + { + let _gate0 = Gate0Span::new("whir_commit_l0_ntt"); + tracing::info_span!("NTT", kind = "base encode", log_domain = k_code, lanes = num_ntts).in_scope(|| { + let ntt = AdditiveNttF64::standard(k_code); + ntt.encode_interleaved(&mut codeword, message, num_ntts, log_inv_rate); + }); + } let ntt_elapsed = t_ntt.elapsed(); let t_merkle = std::time::Instant::now(); @@ -377,7 +428,10 @@ pub fn commit(message: &[F64], log_batch_size: usize, log_inv_rate: usize) -> (C codeword.len() * core::mem::size_of::(), ) }; - let merkle_tree = merkle::merkle_tree(codeword_bytes, n_positions); + let merkle_tree = { + let _gate0 = Gate0Span::new("whir_commit_l0_merkle"); + merkle::merkle_tree(codeword_bytes, n_positions) + }; let root = *merkle_tree.last().expect("merkle tree non-empty"); if trace { let k_code = pretty_integer(k_code); @@ -448,13 +502,16 @@ pub(crate) fn ligero_commit_ext( // commit level, no work when unset. let trace = std::env::var_os("WHIR_TRACE").is_some(); let t_ntt = std::time::Instant::now(); - tracing::info_span!( - "NTT", - kind = "extension encode", - log_domain = log_block_len, - lanes = num_interleaved - ) - .in_scope(|| forward_transform_interleaved_ext_from_layer(ntt, &mut mat, num_interleaved, log_inv_rate)); + { + let _gate0 = Gate0Span::new("whir_recursive_commit_ntt"); + tracing::info_span!( + "NTT", + kind = "extension encode", + log_domain = log_block_len, + lanes = num_interleaved + ) + .in_scope(|| forward_transform_interleaved_ext_from_layer(ntt, &mut mat, num_interleaved, log_inv_rate)); + } let ntt_elapsed = t_ntt.elapsed(); let t_merkle = std::time::Instant::now(); @@ -467,7 +524,10 @@ pub(crate) fn ligero_commit_ext( let data_bytes: &[u8] = unsafe { core::slice::from_raw_parts(mat.as_ptr() as *const u8, mat.len() * core::mem::size_of::()) }; debug_assert_eq!(data_bytes.len(), block_len * leaf_size_bytes); - let tree = merkle::merkle_tree(data_bytes, block_len); + let tree = { + let _gate0 = Gate0Span::new("whir_recursive_commit_merkle"); + merkle::merkle_tree(data_bytes, block_len) + }; if trace { let log_block_len = pretty_integer(log_block_len); let num_interleaved = pretty_integer(num_interleaved); @@ -1057,6 +1117,33 @@ pub fn recursive_prover_with_basis( let log_n = witness.len().trailing_zeros() as usize; let r = config.level_steps; let initial_k = config.initial_k; + const FOLD_LEVEL_NAMES: [&str; 5] = [ + "whir_fold_l1", + "whir_fold_l2", + "whir_fold_l3", + "whir_fold_l4", + "whir_fold_l5", + ]; + const COMMIT_LEVEL_NAMES: [&str; 4] = [ + "whir_recursive_commit_l2", + "whir_recursive_commit_l3", + "whir_recursive_commit_l4", + "whir_recursive_commit_l5", + ]; + const OPEN_LEVEL_NAMES: [&str; 5] = [ + "whir_open_l1", + "whir_open_l2", + "whir_open_l3", + "whir_open_l4", + "whir_open_l5", + ]; + const INDUCE_LEVEL_NAMES: [&str; 5] = [ + "whir_induce_l1", + "whir_induce_l2", + "whir_induce_l3", + "whir_induce_l4", + "whir_induce_l5", + ]; assert_eq!(witness.len(), 1usize << log_n); assert_eq!(b_initial.len(), 1usize << log_n); @@ -1104,6 +1191,7 @@ pub fn recursive_prover_with_basis( let ood_count = |lvl: usize| -> usize { config.ood_samples.get(lvl).copied().unwrap_or(0) }; let _t = std::time::Instant::now(); + let gate0_initial_sumcheck = Gate0Span::new("whir_initial_sumcheck"); let sumcheck_span = tracing::info_span!("Sumcheck"); let (mut sc_prover, start_msg) = sumcheck_span.in_scope(|| SumcheckProver::new(witness, b_initial, target)); sponge.observe(start_msg.u_0); @@ -1125,6 +1213,7 @@ pub fn recursive_prover_with_basis( r_lane_fold.push(r_j); } drop(sumcheck_span); + drop(gate0_initial_sumcheck); if trace { t_init_sumcheck += _t.elapsed(); } @@ -1135,10 +1224,26 @@ pub fn recursive_prover_with_basis( assert!(n1 >= log_num_interleaved_1); let log_msg_cols_1 = n1 - log_num_interleaved_1; let log_inv_rate_1 = config.log_inv_rates[1]; + if gate0_trace_enabled() { + eprintln!( + "LEANVM_GATE0_PCS_CONFIG schema=1 log_n={log_n} initial_k={initial_k} level_ks={:?} log_inv_rates={:?} queries={:?} ood_samples={:?} grinding_bits={:?} fold_grinding_bits={:?} l0_induce_ntt={} workers={}", + config.level_ks, + config.log_inv_rates, + config.queries, + config.ood_samples, + config.grinding_bits, + config.fold_grinding_bits, + induce_use_ntt_heuristic(n1, log_inv_rate_0, config.queries[0]), + parallel::num_threads(), + ); + } let _t = std::time::Instant::now(); let ntt_1 = AdditiveNttF64::standard(log_msg_cols_1 + log_inv_rate_1); let f1 = sc_prover.f_ext().to_vec(); - let wtns_1 = ligero_commit_ext(&f1, log_msg_cols_1, log_num_interleaved_1, log_inv_rate_1, &ntt_1); + let wtns_1 = { + let _gate0 = Gate0Span::new("whir_recursive_commit_l1"); + ligero_commit_ext(&f1, log_msg_cols_1, log_num_interleaved_1, log_inv_rate_1, &ntt_1) + }; if trace { t_commits += _t.elapsed(); } @@ -1159,10 +1264,14 @@ pub fn recursive_prover_with_basis( let alpha_0 = sponge.sample_vec(log2_ceil_usize(num_queries_0)); let _t = std::time::Instant::now(); // Ordered (dup-possible) rows for the local induce math ... - let opened_rows_0: Vec> = queries_0.iter().map(|&q| l0_row(q).to_vec()).collect(); - // ... but the stored proof carries the sorted-unique rows + one octopus over - // the sorted-unique positions (the verifier re-fans them to ordered). - let (stored_rows_0, merkle_proof_0) = stored_opening(&queries_0, |q| l0_row(q).to_vec(), l0_tree, block_len_0); + let (opened_rows_0, stored_rows_0, merkle_proof_0) = { + let _gate0 = Gate0Span::new("whir_open_l0"); + let opened_rows: Vec> = queries_0.iter().map(|&q| l0_row(q).to_vec()).collect(); + // ... but the stored proof carries the sorted-unique rows + one octopus over + // the sorted-unique positions (the verifier re-fans them to ordered). + let (stored_rows, merkle_proof) = stored_opening(&queries_0, |q| l0_row(q).to_vec(), l0_tree, block_len_0); + (opened_rows, stored_rows, merkle_proof) + }; if trace { t_opens += _t.elapsed(); } @@ -1176,15 +1285,18 @@ pub fn recursive_prover_with_basis( // it (deeper levels stay dense), mirroring the original. let sks_vks_n1 = eval_sk_at_vks(n1); let _t = std::time::Instant::now(); - let (basis_0_induced, enforced_sum_0) = induce_sumcheck_poly_auto_base( - n1, - log_inv_rate_0, - &sks_vks_n1, - &opened_rows_0, - &r_lane_fold, - &queries_0, - &alpha_0, - ); + let (basis_0_induced, enforced_sum_0) = { + let _gate0 = Gate0Span::new("whir_induce_l0"); + induce_sumcheck_poly_auto_base( + n1, + log_inv_rate_0, + &sks_vks_n1, + &opened_rows_0, + &r_lane_fold, + &queries_0, + &alpha_0, + ) + }; if trace { t_induce += _t.elapsed(); } @@ -1209,6 +1321,7 @@ pub fn recursive_prover_with_basis( let k_i = config.level_ks[i]; let mut level_rs = Vec::with_capacity(k_i); let _t = std::time::Instant::now(); + let gate0_fold = Gate0Span::new(FOLD_LEVEL_NAMES.get(i).copied().unwrap_or("whir_fold_level")); let sumcheck_span = tracing::info_span!("Sumcheck"); for j in 0..k_i { // These folds fold level i+1's commitment; tapered grinding as in @@ -1224,6 +1337,7 @@ pub fn recursive_prover_with_basis( level_rs.push(ri); } drop(sumcheck_span); + drop(gate0_fold); if trace { t_sumcheck_folds += _t.elapsed(); } @@ -1244,17 +1358,22 @@ pub fn recursive_prover_with_basis( let _t = std::time::Instant::now(); // Final level: stored (sorted-unique) only, no local induce; the // verifier fans these to ordered for its last-level induce. - let (opened_rows_last, merkle_proof_last) = stored_opening( - &queries_last, - |q| wtns_prev.row(q).to_vec(), - &wtns_prev.tree, - wtns_prev.block_len, - ); + let (opened_rows_last, merkle_proof_last, rows_last) = { + let _gate0 = Gate0Span::new(OPEN_LEVEL_NAMES.get(i).copied().unwrap_or("whir_open_level")); + let (opened_rows, merkle_proof) = stored_opening( + &queries_last, + |q| wtns_prev.row(q).to_vec(), + &wtns_prev.tree, + wtns_prev.block_len, + ); + let rows: Vec> = queries_last.iter().map(|&q| wtns_prev.row(q).to_vec()).collect(); + (opened_rows, merkle_proof, rows) + }; // Tie the last commitment into the running claim through the same // intro/glue step as every other level, then finish the remaining // sumcheck rounds. This closes on one weight evaluation instead of // a sweep over the residual cube. - let rows_last: Vec> = queries_last.iter().map(|&q| wtns_prev.row(q).to_vec()).collect(); + let gate0_induce = Gate0Span::new(INDUCE_LEVEL_NAMES.get(i).copied().unwrap_or("whir_induce_level")); let enforced_sum_last = induce_sumcheck_enforced_sum(&rows_last, &level_rs, &queries_last, &alpha_last); let n_res = sc_prover.f_ext().len().trailing_zeros() as usize; let basis_last = induce_sumcheck_evaluate_at_residual( @@ -1265,16 +1384,20 @@ pub fn recursive_prover_with_basis( &[], n_res, ); + drop(gate0_induce); let intro_msg_last = sc_prover.introduce_new(basis_last, enforced_sum_last); sponge.observe(intro_msg_last.u_0); sponge.observe(intro_msg_last.u_2); sc_prover.glue(sponge.sample()); - for j in 0..n_res { - let ri = sponge.sample(); - let msg = sc_prover.fold(ri); - if j + 1 < n_res { - sponge.observe(msg.u_0); - sponge.observe(msg.u_2); + { + let _gate0 = Gate0Span::new("whir_fold_residual"); + for j in 0..n_res { + let ri = sponge.sample(); + let msg = sc_prover.fold(ri); + if j + 1 < n_res { + sponge.observe(msg.u_0); + sponge.observe(msg.u_2); + } } } let transmitted_sumcheck_len = sc_prover.transcript().len() - usize::from(n_res > 0); @@ -1331,13 +1454,21 @@ pub fn recursive_prover_with_basis( let _t = std::time::Instant::now(); let ntt_next = AdditiveNttF64::standard(log_msg_cols_next + log_inv_rate_next); let f_evals = sc_prover.f_ext().to_vec(); - let wtns_next = ligero_commit_ext( - &f_evals, - log_msg_cols_next, - log_num_interleaved_next, - log_inv_rate_next, - &ntt_next, - ); + let wtns_next = { + let _gate0 = Gate0Span::new( + COMMIT_LEVEL_NAMES + .get(i) + .copied() + .unwrap_or("whir_recursive_commit_level"), + ); + ligero_commit_ext( + &f_evals, + log_msg_cols_next, + log_num_interleaved_next, + log_inv_rate_next, + &ntt_next, + ) + }; if trace { t_commits += _t.elapsed(); } @@ -1355,13 +1486,17 @@ pub fn recursive_prover_with_basis( let alpha_i = sponge.sample_vec(log2_ceil_usize(num_queries_i)); let _t = std::time::Instant::now(); // Ordered rows for the local induce; sorted-unique rows + octopus stored. - let opened_rows_i: Vec> = queries_i.iter().map(|&q| wtns_prev.row(q).to_vec()).collect(); - let (stored_rows_i, merkle_proof_i) = stored_opening( - &queries_i, - |q| wtns_prev.row(q).to_vec(), - &wtns_prev.tree, - wtns_prev.block_len, - ); + let (opened_rows_i, stored_rows_i, merkle_proof_i) = { + let _gate0 = Gate0Span::new(OPEN_LEVEL_NAMES.get(i).copied().unwrap_or("whir_open_level")); + let opened_rows: Vec> = queries_i.iter().map(|&q| wtns_prev.row(q).to_vec()).collect(); + let (stored_rows, merkle_proof) = stored_opening( + &queries_i, + |q| wtns_prev.row(q).to_vec(), + &wtns_prev.tree, + wtns_prev.block_len, + ); + (opened_rows, stored_rows, merkle_proof) + }; if trace { t_opens += _t.elapsed(); } @@ -1372,8 +1507,10 @@ pub fn recursive_prover_with_basis( let sks_vks_i = eval_sk_at_vks(n_next); let _t = std::time::Instant::now(); - let (basis_i_induced, enforced_sum_i) = - induce_sumcheck_poly(n_next, &sks_vks_i, &opened_rows_i, &level_rs, &queries_i, &alpha_i); + let (basis_i_induced, enforced_sum_i) = { + let _gate0 = Gate0Span::new(INDUCE_LEVEL_NAMES.get(i).copied().unwrap_or("whir_induce_level")); + induce_sumcheck_poly(n_next, &sks_vks_i, &opened_rows_i, &level_rs, &queries_i, &alpha_i) + }; if trace { t_induce += _t.elapsed(); } diff --git a/crates/rec_aggregation/src/lib.rs b/crates/rec_aggregation/src/lib.rs index bbb0596c..ccf6164d 100644 --- a/crates/rec_aggregation/src/lib.rs +++ b/crates/rec_aggregation/src/lib.rs @@ -9,7 +9,12 @@ pub mod signers_cache; pub mod xmss_aggregation; pub use fibonacci::run_fibonacci; -pub use recursion::{RecursiveProof, RecursiveVerifyError, run_recursion}; +pub use recursion::{ + RecursionBoundaryReport, RecursionFixtureInspectionReport, RecursionFixturePreparationReport, RecursiveProof, + RecursiveProofInspectionReport, RecursiveVerifyError, inspect_recursion_fixture, inspect_recursive_proof_artifact, + prepare_recursion_fixture, read_recursive_proof_artifact, run_recursion, run_recursion_fixture_aggregation, + run_recursion_with_artifact, +}; pub use xmss_aggregation::run_xmss_aggregation; /// The pieces every workload's benchmark report ends with. diff --git a/crates/rec_aggregation/src/recursion.rs b/crates/rec_aggregation/src/recursion.rs index 9964a959..c48b32ff 100644 --- a/crates/rec_aggregation/src/recursion.rs +++ b/crates/rec_aggregation/src/recursion.rs @@ -13,7 +13,13 @@ //! the outer VM proof and evaluates every deferred fixed polynomial. use std::collections::BTreeMap; +use std::ffi::OsString; +use std::fs::{File, OpenOptions}; +use std::io::{self, Read, Write}; +use std::path::{Path, PathBuf}; +use std::time::{Duration, Instant}; +use bincode::Options; use lean_compiler::{compile, parse, parse_with_replacements}; use lean_vm::cpu::{Program, prove, verify}; use lean_vm::leaf::{Block, Coord}; @@ -32,6 +38,217 @@ use primitives::{ const VALCOL_FRAMEWORK: &str = "a framework block must not reference a virtual value column"; const RECURSION_AGG_LABEL: &[u8] = b"leanvm-b/recursion-aggregation/v1"; const RECURSION_STATEMENT_LABEL: &[u8] = b"leanvm-b/recursive-statement/v1"; +const RECURSION_FIXTURE_MAGIC: [u8; 8] = *b"LVRFX002"; +const RECURSION_FIXTURE_VERSION: u32 = 2; +const RECURSIVE_PROOF_ARTIFACT_MAGIC: [u8; 8] = *b"LVRPF002"; +const RECURSIVE_PROOF_ARTIFACT_VERSION: u32 = 2; +const RECURSIVE_PROOF_ARTIFACT_HEADER_LEN: usize = 8 + 4 + 8 + 32; + +fn gate0_trace_enabled() -> bool { + static ENABLED: std::sync::OnceLock = std::sync::OnceLock::new(); + *ENABLED.get_or_init(|| std::env::var_os("LEANVM_GATE0_TRACE").as_deref() == Some(std::ffi::OsStr::new("1"))) +} + +fn gate0_boundary_event(kind: &str, id: u64, name: &str) { + static ORIGIN: std::sync::OnceLock = std::sync::OnceLock::new(); + let process_ns = ORIGIN.get_or_init(Instant::now).elapsed().as_nanos(); + let unix_ns = std::time::SystemTime::now() + .duration_since(std::time::UNIX_EPOCH) + .expect("system clock is after the Unix epoch") + .as_nanos(); + eprintln!( + "LEANVM_GATE0_EVENT schema=1 source=rec_aggregation kind={kind} id={id} name={name:?} unix_ns={unix_ns} process_ns={process_ns} pid={}", + std::process::id() + ); +} + +fn measure_boundary(name: &str, f: impl FnOnce() -> T) -> (T, Duration) { + static NEXT_ID: std::sync::atomic::AtomicU64 = std::sync::atomic::AtomicU64::new(1_000_000); + let trace = gate0_trace_enabled(); + let id = NEXT_ID.fetch_add(1, std::sync::atomic::Ordering::Relaxed); + if trace { + gate0_boundary_event("start", id, name); + } + let started = Instant::now(); + let output = f(); + let elapsed = started.elapsed(); + if trace { + gate0_boundary_event("end", id, name); + } + (output, elapsed) +} + +#[derive(Clone, Debug, serde::Serialize, serde::Deserialize)] +struct RecursionChildV1 { + hashes: u64, + iters: u64, + log_inv_rate: u64, + public_input: [F192; 2], + proof: lean_vm::cpu::Proof, + cycles: u64, + committed: u64, +} + +#[derive(Clone, Debug, serde::Serialize, serde::Deserialize)] +struct RecursionFixtureV1 { + magic: [u8; 8], + version: u32, + inner_environment: [F192; 2], + children: Vec, +} + +#[derive(Clone, Debug)] +pub struct RecursionFixturePreparationReport { + pub child_count: usize, + pub child_proving: Duration, + pub child_verification: Duration, + pub total: Duration, + pub fixture_bytes: usize, + pub fixture_blake3: String, +} + +#[derive(Clone, Debug)] +pub struct RecursionFixtureInspectionReport { + pub child_count: usize, + pub total: Duration, + pub fixture_bytes: usize, + pub fixture_blake3: String, +} + +#[derive(Clone, Debug)] +pub struct RecursiveProofInspectionReport { + pub child_count: usize, + pub total: Duration, + pub artifact_bytes: usize, + pub artifact_blake3: String, +} + +#[derive(Clone, Debug)] +pub struct RecursionBoundaryReport { + pub child_count: usize, + pub fixture_open_and_read: Duration, + pub fixture_decode_and_validate: Duration, + pub child_verify_and_hint_reconstruction: Duration, + pub outer_guest_compile: Duration, + pub outer_prove: Duration, + pub in_memory_verify: Duration, + pub durable_output: Duration, + pub boundary_total: Duration, + pub fixture_bytes: usize, + pub recursive_proof_bytes: usize, + pub artifact_bytes: usize, + pub fixture_blake3: String, + pub artifact_blake3: String, + pub outer_cycles: usize, + pub outer_counts: [usize; lean_vm::tables::N_TABLES], + pub outer_base_counts: [usize; lean_vm::tables::N_TABLES], + pub outer_log_mem: usize, + pub outer_mem_used: usize, + pub outer_committed: usize, + pub outer_stack_log: usize, +} + +impl RecursionFixturePreparationReport { + pub fn print(&self) { + println!("recursion fixture preparation"); + println!(" child proofs : {}", pretty_integer(self.child_count)); + println!( + " child proving : {:.6} s", + self.child_proving.as_secs_f64() + ); + println!( + " child verification : {:.6} s", + self.child_verification.as_secs_f64() + ); + println!(" total : {:.6} s", self.total.as_secs_f64()); + println!(" fixture bytes : {}", pretty_integer(self.fixture_bytes)); + println!(" fixture BLAKE3 : {}", self.fixture_blake3); + } +} + +impl RecursionFixtureInspectionReport { + pub fn print(&self) { + println!("recursion fixture read-only inspection"); + println!(" child proofs : {}", pretty_integer(self.child_count)); + println!(" total : {:.6} s", self.total.as_secs_f64()); + println!(" fixture bytes : {}", pretty_integer(self.fixture_bytes)); + println!(" fixture BLAKE3 : {}", self.fixture_blake3); + } +} + +impl RecursiveProofInspectionReport { + pub fn print(&self) { + println!("recursive proof read-only inspection"); + println!(" child statements : {}", pretty_integer(self.child_count)); + println!(" total : {:.6} s", self.total.as_secs_f64()); + println!( + " artifact bytes : {}", + pretty_integer(self.artifact_bytes) + ); + println!(" artifact BLAKE3 : {}", self.artifact_blake3); + } +} + +impl RecursionBoundaryReport { + pub fn print(&self) { + println!("recursion input-ready to durable-output gate"); + println!(" child proofs : {}", pretty_integer(self.child_count)); + println!( + " fixture open and read : {:.6} s", + self.fixture_open_and_read.as_secs_f64() + ); + println!( + " fixture decode and validate : {:.6} s", + self.fixture_decode_and_validate.as_secs_f64() + ); + println!( + " child verify and hint build : {:.6} s", + self.child_verify_and_hint_reconstruction.as_secs_f64() + ); + println!( + " outer guest compile : {:.6} s", + self.outer_guest_compile.as_secs_f64() + ); + println!( + " outer proving : {:.6} s", + self.outer_prove.as_secs_f64() + ); + println!( + " in-memory verify : {:.6} s", + self.in_memory_verify.as_secs_f64() + ); + println!( + " durable output : {:.6} s", + self.durable_output.as_secs_f64() + ); + println!( + " boundary total : {:.6} s", + self.boundary_total.as_secs_f64() + ); + println!(" fixture bytes : {}", pretty_integer(self.fixture_bytes)); + println!( + " recursive proof bytes : {}", + pretty_integer(self.recursive_proof_bytes) + ); + println!( + " artifact bytes : {}", + pretty_integer(self.artifact_bytes) + ); + println!(" fixture BLAKE3 : {}", self.fixture_blake3); + println!(" artifact BLAKE3 : {}", self.artifact_blake3); + println!( + "LEANVM_GATE0_GEOMETRY schema=2 children={} cycles={} counts={:?} base_counts={:?} log_mem={} mem_used={} committed={} stack_log={}", + self.child_count, + self.outer_cycles, + self.outer_counts, + self.outer_base_counts, + self.outer_log_mem, + self.outer_mem_used, + self.outer_committed, + self.outer_stack_log + ); + } +} /// Aggregation arity bound: the guest hints the count and range-checks its /// exponent against this (`NSUB_BOUND`), which is what makes its per-sub walks @@ -273,6 +490,323 @@ pub enum RecursiveVerifyError { MatrixBClaim, } +fn invalid_data(message: impl Into) -> io::Error { + io::Error::new(io::ErrorKind::InvalidData, message.into()) +} + +fn child_public_input(index: usize) -> io::Result<[F192; 2]> { + let k = u64::try_from(index) + .map_err(|_| io::Error::new(io::ErrorKind::InvalidInput, "child index does not fit in u64"))?; + let c0 = 0x1111_2222u64 + .checked_add(k) + .ok_or_else(|| io::Error::new(io::ErrorKind::InvalidInput, "too many child statements"))?; + let c1 = 0x7777_8888u64 + .checked_add(k) + .ok_or_else(|| io::Error::new(io::ErrorKind::InvalidInput, "too many child statements"))?; + Ok([F192::new(c0, 0x3333_4444, 0), F192::new(0x5555_6666, c1, 0)]) +} + +fn validate_fixture(fixture: &RecursionFixtureV1) -> io::Result<()> { + if fixture.magic != RECURSION_FIXTURE_MAGIC { + return Err(invalid_data("recursion fixture magic mismatch")); + } + if fixture.version != RECURSION_FIXTURE_VERSION { + return Err(invalid_data(format!( + "unsupported recursion fixture version {}", + fixture.version + ))); + } + if fixture.children.is_empty() { + return Err(invalid_data("recursion fixture contains no child proofs")); + } + if fixture.children.len() >= NSUB_BOUND { + return Err(invalid_data(format!( + "recursion fixture has {} children, but the guest bound is strictly below {NSUB_BOUND}", + fixture.children.len() + ))); + } + for (index, child) in fixture.children.iter().enumerate() { + if child.hashes == 0 || child.iters == 0 || child.cycles == 0 || child.committed == 0 { + return Err(invalid_data(format!("child {index} contains zero metadata"))); + } + if !(1..=4).contains(&child.log_inv_rate) { + return Err(invalid_data(format!("child {index} has an invalid PCS rate"))); + } + if child.public_input != child_public_input(index)? { + return Err(invalid_data(format!("child {index} public input is not canonical"))); + } + } + Ok(()) +} + +fn encode_fixture(fixture: &RecursionFixtureV1) -> io::Result> { + bincode::DefaultOptions::new() + .with_little_endian() + .with_fixint_encoding() + .serialize(fixture) + .map_err(|error| invalid_data(format!("recursion fixture encode: {error}"))) +} + +fn decode_fixture(bytes: &[u8]) -> io::Result { + bincode::DefaultOptions::new() + .with_little_endian() + .with_fixint_encoding() + .with_limit(bytes.len() as u64) + .reject_trailing_bytes() + .deserialize(bytes) + .map_err(|error| invalid_data(format!("recursion fixture decode: {error}"))) +} + +fn encode_recursive_proof(proof: &RecursiveProof) -> io::Result> { + bincode::DefaultOptions::new() + .with_little_endian() + .with_fixint_encoding() + .serialize(proof) + .map_err(|error| invalid_data(format!("recursive proof encode: {error}"))) +} + +fn decode_recursive_proof(bytes: &[u8]) -> io::Result { + bincode::DefaultOptions::new() + .with_little_endian() + .with_fixint_encoding() + .with_limit(bytes.len() as u64) + .reject_trailing_bytes() + .deserialize(bytes) + .map_err(|error| invalid_data(format!("recursive proof decode: {error}"))) +} + +fn encode_recursive_proof_artifact(proof: &RecursiveProof) -> io::Result> { + let payload = encode_recursive_proof(proof)?; + let payload_len = + u64::try_from(payload.len()).map_err(|_| invalid_data("recursive proof payload length does not fit in u64"))?; + let digest = blake3::hash(&payload); + let mut artifact = Vec::with_capacity(RECURSIVE_PROOF_ARTIFACT_HEADER_LEN + payload.len()); + artifact.extend_from_slice(&RECURSIVE_PROOF_ARTIFACT_MAGIC); + artifact.extend_from_slice(&RECURSIVE_PROOF_ARTIFACT_VERSION.to_le_bytes()); + artifact.extend_from_slice(&payload_len.to_le_bytes()); + artifact.extend_from_slice(digest.as_bytes()); + artifact.extend_from_slice(&payload); + Ok(artifact) +} + +fn decode_recursive_proof_artifact(bytes: &[u8]) -> io::Result { + if bytes.len() < RECURSIVE_PROOF_ARTIFACT_HEADER_LEN { + return Err(invalid_data("recursive proof artifact header is truncated")); + } + if bytes[..8] != RECURSIVE_PROOF_ARTIFACT_MAGIC { + return Err(invalid_data("recursive proof artifact magic mismatch")); + } + let version = u32::from_le_bytes(bytes[8..12].try_into().expect("fixed version slice")); + if version != RECURSIVE_PROOF_ARTIFACT_VERSION { + return Err(invalid_data(format!( + "unsupported recursive proof artifact version {version}" + ))); + } + let payload_len = usize::try_from(u64::from_le_bytes( + bytes[12..20].try_into().expect("fixed length slice"), + )) + .map_err(|_| invalid_data("recursive proof payload length does not fit in usize"))?; + let expected_len = RECURSIVE_PROOF_ARTIFACT_HEADER_LEN + .checked_add(payload_len) + .ok_or_else(|| invalid_data("recursive proof artifact length overflow"))?; + if bytes.len() != expected_len { + return Err(invalid_data(format!( + "recursive proof artifact length mismatch: expected {expected_len}, got {}", + bytes.len() + ))); + } + let payload = &bytes[RECURSIVE_PROOF_ARTIFACT_HEADER_LEN..]; + if blake3::hash(payload).as_bytes() != &bytes[20..RECURSIVE_PROOF_ARTIFACT_HEADER_LEN] { + return Err(invalid_data("recursive proof artifact payload digest mismatch")); + } + decode_recursive_proof(payload) +} + +fn read_all(path: &Path) -> io::Result> { + let mut file = File::open(path)?; + let mut bytes = Vec::new(); + file.read_to_end(&mut bytes)?; + Ok(bytes) +} + +fn output_parent(output: &Path) -> &Path { + output + .parent() + .filter(|parent| !parent.as_os_str().is_empty()) + .unwrap_or_else(|| Path::new(".")) +} + +fn ensure_create_new_target(output: &Path) -> io::Result<()> { + if output.file_name().is_none() { + return Err(io::Error::new( + io::ErrorKind::InvalidInput, + format!("output path has no file name: {}", output.display()), + )); + } + if !std::fs::metadata(output_parent(output))?.is_dir() { + return Err(io::Error::new( + io::ErrorKind::InvalidInput, + format!("output parent is not a directory: {}", output_parent(output).display()), + )); + } + match std::fs::symlink_metadata(output) { + Ok(_) => Err(io::Error::new( + io::ErrorKind::AlreadyExists, + format!("refusing to overwrite existing output: {}", output.display()), + )), + Err(error) if error.kind() == io::ErrorKind::NotFound => Ok(()), + Err(error) => Err(error), + } +} + +struct PendingOutput { + path: PathBuf, + target: PathBuf, + file: Option, + published: bool, +} + +impl PendingOutput { + fn create(output: &Path) -> io::Result { + ensure_create_new_target(output)?; + let parent = output_parent(output); + let file_name = output.file_name().expect("output file name was checked"); + for attempt in 0..128u32 { + let mut temp_name = OsString::from("."); + temp_name.push(file_name); + temp_name.push(format!(".tmp.{}.{attempt}", std::process::id())); + let path = parent.join(temp_name); + match OpenOptions::new().write(true).create_new(true).open(&path) { + Ok(file) => { + return Ok(Self { + path, + target: output.to_path_buf(), + file: Some(file), + published: false, + }); + } + Err(error) if error.kind() == io::ErrorKind::AlreadyExists => continue, + Err(error) => return Err(error), + } + } + Err(io::Error::new( + io::ErrorKind::AlreadyExists, + format!("could not allocate a temporary file beside {}", output.display()), + )) + } + + fn write_and_sync(&mut self, bytes: &[u8]) -> io::Result<()> { + let file = self.file.as_mut().expect("pending output remains open"); + file.write_all(bytes)?; + file.sync_all()?; + self.file.take(); + Ok(()) + } + + fn readback(&self) -> io::Result> { + read_all(&self.path) + } + + fn publish(mut self) -> io::Result<()> { + if self.file.is_some() { + return Err(io::Error::other("pending output must be synced before publication")); + } + let parent = output_parent(&self.target); + let sync_parent = || File::open(parent).and_then(|directory| directory.sync_all()); + std::fs::hard_link(&self.path, &self.target)?; + if let Err(error) = sync_parent() { + let _ = std::fs::remove_file(&self.target); + let _ = sync_parent(); + return Err(error); + } + if let Err(error) = std::fs::remove_file(&self.path) { + let _ = std::fs::remove_file(&self.target); + let _ = sync_parent(); + return Err(error); + } + if let Err(error) = sync_parent() { + let _ = std::fs::remove_file(&self.target); + let _ = sync_parent(); + return Err(error); + } + self.published = true; + Ok(()) + } +} + +impl Drop for PendingOutput { + fn drop(&mut self) { + if !self.published { + let _ = std::fs::remove_file(&self.path); + } + } +} + +struct RecursiveProofArtifactInfo { + artifact_bytes: usize, + proof_bytes: usize, + blake3: String, +} + +fn persist_recursive_proof_artifact( + output: &Path, + proof: &RecursiveProof, + inner_program: &Program, +) -> io::Result { + let proof_bytes = encode_recursive_proof(proof)?.len(); + let encoded = encode_recursive_proof_artifact(proof)?; + let digest = blake3::hash(&encoded).to_hex().to_string(); + let mut pending = PendingOutput::create(output)?; + pending.write_and_sync(&encoded)?; + let readback = pending.readback()?; + if readback != encoded { + return Err(invalid_data( + "recursive proof artifact readback differs from serialized bytes", + )); + } + decode_recursive_proof_artifact(&readback)? + .verify(inner_program) + .map_err(|error| invalid_data(format!("persisted recursive proof did not verify: {error:?}")))?; + pending.publish()?; + Ok(RecursiveProofArtifactInfo { + artifact_bytes: encoded.len(), + proof_bytes, + blake3: digest, + }) +} + +pub fn read_recursive_proof_artifact>(path: P) -> io::Result { + decode_recursive_proof_artifact(&read_all(path.as_ref())?) +} + +pub fn inspect_recursive_proof_artifact>( + artifact_path: P, +) -> io::Result { + let started = Instant::now(); + let first_bytes = read_all(artifact_path.as_ref())?; + let first_proof = decode_recursive_proof_artifact(&first_bytes)?; + let child_count = first_proof.statement.sub_statements.len(); + first_proof + .verify(&inner_program()) + .map_err(|error| invalid_data(format!("recursive proof verification failed: {error:?}")))?; + + let reopened_bytes = read_all(artifact_path.as_ref())?; + if reopened_bytes != first_bytes { + return Err(invalid_data("recursive proof artifact changed across reopen")); + } + let reopened_proof = decode_recursive_proof_artifact(&reopened_bytes)?; + reopened_proof + .verify(&inner_program()) + .map_err(|error| invalid_data(format!("reopened recursive proof verification failed: {error:?}")))?; + + Ok(RecursiveProofInspectionReport { + child_count, + total: started.elapsed(), + artifact_bytes: first_bytes.len(), + artifact_blake3: blake3::hash(&first_bytes).to_hex().to_string(), + }) +} + fn fold_lsb(t: &mut Vec, r: F192) { let half = t.len() / 2; for i in 0..half { @@ -1328,6 +1862,78 @@ fn build_batch(inner: &[(usize, usize)], log_inv_rates: &[usize], outer_log_inv_ } } +fn build_batch_from_fixture( + program0: Program, + fixture: &RecursionFixtureV1, + outer_log_inv_rate: usize, +) -> io::Result { + let mut merged: Vec<(String, Vec>)> = Vec::new(); + let mut subs = Vec::with_capacity(fixture.children.len()); + let mut inner_stats = Vec::with_capacity(fixture.children.len()); + + for (index, child) in fixture.children.iter().enumerate() { + trace_start(); + let summary_result = verify(&program0, &child.public_input, &child.proof); + let ops = trace_take(); + let summary = summary_result + .map_err(|error| invalid_data(format!("child {index} proof verification failed: {error:?}")))?; + let declared_log_inv_rate = usize::try_from(child.log_inv_rate) + .map_err(|_| invalid_data(format!("child {index} PCS rate does not fit in usize")))?; + if summary.log_inv_rate != declared_log_inv_rate { + return Err(invalid_data(format!( + "child {index} proof uses PCS rate {}, but its fixture metadata declares {declared_log_inv_rate}", + summary.log_inv_rate + ))); + } + let (hints, deferred) = gen_verify(&program0, child.public_input, &child.proof, &summary, &ops); + + if merged.is_empty() { + merged = hints.into_iter().map(|(name, values)| (name, vec![values])).collect(); + } else { + if merged.len() != hints.len() { + return Err(invalid_data(format!( + "child {index} reconstructed a different hint stream count" + ))); + } + for ((name, entries), (next_name, values)) in merged.iter_mut().zip(hints) { + if *name != next_name { + return Err(invalid_data(format!( + "child {index} reconstructed hint stream {next_name:?}, expected {name:?}" + ))); + } + entries.push(values); + } + } + subs.push(deferred); + inner_stats.push(( + usize::try_from(child.cycles) + .map_err(|_| invalid_data("fixture child cycle count does not fit in usize"))?, + usize::try_from(child.committed) + .map_err(|_| invalid_data("fixture child committed size does not fit in usize"))?, + )); + } + + let (aggregate_hints, guest_public_input, reduced) = aggregate_deferred_claims(&program0, &subs); + merged.extend(aggregate_hints.into_iter().map(|(name, values)| (name, vec![values]))); + let statement = RecursiveStatement { + sub_statements: subs.iter().map(|deferred| deferred.public_input).collect(), + reduced, + }; + if statement.public_input(lean_vm::cpu::fs_seed(&program0)) != guest_public_input { + return Err(invalid_data( + "native recursive statement reconstruction diverged from the guest", + )); + } + + Ok(Batch { + merged, + program0, + statement, + inner_stats, + outer_log_inv_rate, + }) +} + struct OpeningShape { n_levels: usize, yr_level: usize, @@ -2022,6 +2628,211 @@ fn recursion_guest(inner_program: &Program) -> Program { (*recursion_guest_arc(inner_program)).clone() } +pub fn prepare_recursion_fixture>( + inner: &[(usize, usize)], + log_inv_rate: usize, + output: P, +) -> io::Result { + let output = output.as_ref(); + let total_started = Instant::now(); + ensure_create_new_target(output)?; + if inner.is_empty() { + return Err(io::Error::new( + io::ErrorKind::InvalidInput, + "a recursion fixture cannot be empty", + )); + } + if inner.len() >= NSUB_BOUND { + return Err(io::Error::new( + io::ErrorKind::InvalidInput, + format!( + "recursion fixture has {} children, but the guest bound is strictly below {NSUB_BOUND}", + inner.len() + ), + )); + } + + let canonical_program = inner_program(); + let inner_environment = lean_vm::cpu::fs_seed(&canonical_program); + let mut children = Vec::with_capacity(inner.len()); + let mut child_proving = Duration::ZERO; + let mut child_verification = Duration::ZERO; + for (index, &(hashes, iters)) in inner.iter().enumerate() { + if hashes == 0 || iters == 0 { + return Err(io::Error::new( + io::ErrorKind::InvalidInput, + format!("child {index} has a zero loop bound"), + )); + } + let public_input = child_public_input(index)?; + let ((program, proof, cycles, committed), elapsed) = measure_boundary("fixture_child_prove", || { + prove_inner(public_input, hashes, iters, log_inv_rate) + }); + child_proving += elapsed; + if lean_vm::cpu::fs_seed(&program) != inner_environment { + return Err(invalid_data(format!( + "child {index} was proved against a non-canonical inner environment" + ))); + } + let (verification, elapsed) = + measure_boundary("fixture_child_verify", || verify(&program, &public_input, &proof)); + verification.map_err(|error| invalid_data(format!("child {index} proof did not verify: {error:?}")))?; + child_verification += elapsed; + children.push(RecursionChildV1 { + hashes: u64::try_from(hashes) + .map_err(|_| io::Error::new(io::ErrorKind::InvalidInput, "hash count does not fit in u64"))?, + iters: u64::try_from(iters) + .map_err(|_| io::Error::new(io::ErrorKind::InvalidInput, "iteration count does not fit in u64"))?, + log_inv_rate: u64::try_from(log_inv_rate) + .map_err(|_| io::Error::new(io::ErrorKind::InvalidInput, "PCS rate does not fit in u64"))?, + public_input, + proof, + cycles: u64::try_from(cycles).map_err(|_| invalid_data("child cycle count does not fit in u64"))?, + committed: u64::try_from(committed) + .map_err(|_| invalid_data("child committed size does not fit in u64"))?, + }); + } + + let fixture = RecursionFixtureV1 { + magic: RECURSION_FIXTURE_MAGIC, + version: RECURSION_FIXTURE_VERSION, + inner_environment, + children, + }; + validate_fixture(&fixture)?; + let encoded = encode_fixture(&fixture)?; + let fixture_blake3 = blake3::hash(&encoded).to_hex().to_string(); + let mut pending = PendingOutput::create(output)?; + pending.write_and_sync(&encoded)?; + let readback = pending.readback()?; + if readback != encoded { + return Err(invalid_data("recursion fixture readback differs from serialized bytes")); + } + let persisted = decode_fixture(&readback)?; + validate_fixture(&persisted)?; + if persisted.inner_environment != inner_environment { + return Err(invalid_data("persisted fixture inner environment mismatch")); + } + for (index, child) in persisted.children.iter().enumerate() { + verify(&canonical_program, &child.public_input, &child.proof) + .map_err(|error| invalid_data(format!("persisted child {index} proof did not verify: {error:?}")))?; + } + pending.publish()?; + + Ok(RecursionFixturePreparationReport { + child_count: fixture.children.len(), + child_proving, + child_verification, + total: total_started.elapsed(), + fixture_bytes: encoded.len(), + fixture_blake3, + }) +} + +pub fn inspect_recursion_fixture>(fixture_path: P) -> io::Result { + let started = Instant::now(); + let first_bytes = read_all(fixture_path.as_ref())?; + let first_fixture = decode_fixture(&first_bytes)?; + validate_fixture(&first_fixture)?; + let program = inner_program(); + if lean_vm::cpu::fs_seed(&program) != first_fixture.inner_environment { + return Err(invalid_data("fixture inner program environment mismatch")); + } + for (index, child) in first_fixture.children.iter().enumerate() { + verify(&program, &child.public_input, &child.proof) + .map_err(|error| invalid_data(format!("child {index} proof verification failed: {error:?}")))?; + } + let reopened_bytes = read_all(fixture_path.as_ref())?; + if reopened_bytes != first_bytes { + return Err(invalid_data("recursion fixture changed across reopen")); + } + let reopened_fixture = decode_fixture(&reopened_bytes)?; + validate_fixture(&reopened_fixture)?; + for (index, child) in reopened_fixture.children.iter().enumerate() { + verify(&program, &child.public_input, &child.proof) + .map_err(|error| invalid_data(format!("reopened child {index} proof verification failed: {error:?}")))?; + } + Ok(RecursionFixtureInspectionReport { + child_count: first_fixture.children.len(), + total: started.elapsed(), + fixture_bytes: first_bytes.len(), + fixture_blake3: blake3::hash(&first_bytes).to_hex().to_string(), + }) +} + +pub fn run_recursion_fixture_aggregation, Q: AsRef>( + fixture_path: P, + output: Q, + outer_log_inv_rate: usize, + enable_tracing: bool, +) -> io::Result { + let output = output.as_ref(); + ensure_create_new_target(output)?; + let boundary_started = Instant::now(); + + let (fixture_bytes_result, fixture_open_and_read) = + measure_boundary("fixture_open_and_read", || read_all(fixture_path.as_ref())); + let fixture_bytes = fixture_bytes_result?; + let fixture_blake3 = blake3::hash(&fixture_bytes).to_hex().to_string(); + + let (fixture_result, fixture_decode_and_validate) = measure_boundary("fixture_decode_and_validate", || { + let fixture = decode_fixture(&fixture_bytes)?; + validate_fixture(&fixture)?; + Ok::<_, io::Error>(fixture) + }); + let fixture = fixture_result?; + + let program = inner_program(); + if lean_vm::cpu::fs_seed(&program) != fixture.inner_environment { + return Err(invalid_data("fixture inner program environment mismatch")); + } + let (batch_result, child_verify_and_hint_reconstruction) = + measure_boundary("child_verify_and_hint_reconstruction", || { + build_batch_from_fixture(program, &fixture, outer_log_inv_rate) + }); + let batch = batch_result?; + let child_count = batch.inner_stats.len(); + + let (mut guest, outer_guest_compile) = measure_boundary("outer_guest_compile", || recursion_guest(&batch.program0)); + if enable_tracing { + primitives::init_tracing(); + } + let ((recursive_proof, stats), outer_prove) = measure_boundary("outer_prove", || batch.prove(&mut guest)); + let (verification, in_memory_verify) = + measure_boundary("in_memory_verify", || recursive_proof.verify(&batch.program0)); + verification.map_err(|error| invalid_data(format!("in-memory recursive proof verification failed: {error:?}")))?; + + let (artifact_result, durable_output) = measure_boundary("durable_output", || { + persist_recursive_proof_artifact(output, &recursive_proof, &batch.program0) + }); + let artifact = artifact_result?; + let outer_stack_log = log2_ceil_usize(stats.committed).max(lean_vm::pcs::MIN_MU); + + Ok(RecursionBoundaryReport { + child_count, + fixture_open_and_read, + fixture_decode_and_validate, + child_verify_and_hint_reconstruction, + outer_guest_compile, + outer_prove, + in_memory_verify, + durable_output, + boundary_total: boundary_started.elapsed(), + fixture_bytes: fixture_bytes.len(), + recursive_proof_bytes: artifact.proof_bytes, + artifact_bytes: artifact.artifact_bytes, + fixture_blake3, + artifact_blake3: artifact.blake3, + outer_cycles: stats.cycles, + outer_counts: stats.counts, + outer_base_counts: stats.base_counts, + outer_log_mem: stats.log_mem, + outer_mem_used: stats.mem_used, + outer_committed: stats.committed, + outer_stack_log, + }) +} + /// Run an `inner.len()`→1 recursive aggregation and verify the outer proof; /// each entry `(hashes, iters)` shapes one inner proof of the fixed inner /// program. Prints the benchmark report. The flow: @@ -2043,6 +2854,97 @@ pub fn run_recursion( run_recursion_with_rates(inner, &rates, log_inv_rate, enable_tracing, plan) } +/// Run the unchanged native recursion path and publish its returned proof in +/// the same deterministic artifact format used by the input-ready seam. +pub fn run_recursion_with_artifact>( + inner: &[(usize, usize)], + log_inv_rate: usize, + enable_tracing: bool, + output: P, + plan: Plan, +) -> io::Result { + let output = output.as_ref(); + ensure_create_new_target(output)?; + let proof = run_recursion(inner, log_inv_rate, enable_tracing, plan); + let program = inner_program(); + let artifact = persist_recursive_proof_artifact(output, &proof, &program)?; + println!( + "[recursive-proof-artifact-v2] path={} artifact_bytes={} proof_bytes={} blake3={}", + output.display(), + artifact.artifact_bytes, + artifact.proof_bytes, + artifact.blake3 + ); + Ok(proof) +} + +/// Compare the unchanged native recursion path with the input-ready seam using +/// real proofs. This stays ignored because it launches several proving passes. +#[test] +#[ignore] +fn gate0_fixture_matches_native_proof_bytes() { + lean_vm::init_prover(); + let nonce = std::time::SystemTime::now() + .duration_since(std::time::UNIX_EPOCH) + .expect("system clock is after the Unix epoch") + .as_nanos(); + let directory = std::env::temp_dir().join(format!("leanvm-gate0-exactness-{}-{nonce}", std::process::id())); + std::fs::create_dir(&directory).expect("create exactness directory"); + let fixture_path = directory.join("children.bin"); + let native_path = directory.join("native.bin"); + let seam_path = directory.join("seam.bin"); + let inner = [(1usize, 1usize << 9)]; + + prepare_recursion_fixture(&inner, lean_vm::pcs::LOG_INV_RATE, &fixture_path).expect("prepare fixture"); + inspect_recursion_fixture(&fixture_path).expect("inspect fixture"); + run_recursion_with_artifact(&inner, lean_vm::pcs::LOG_INV_RATE, false, &native_path, Plan::default()) + .expect("run native path"); + run_recursion_fixture_aggregation(&fixture_path, &seam_path, lean_vm::pcs::LOG_INV_RATE, false) + .expect("run input-ready seam"); + + let native = std::fs::read(&native_path).expect("read native artifact"); + let seam = std::fs::read(&seam_path).expect("read seam artifact"); + assert_eq!( + native, seam, + "native and input-ready proof artifacts must be byte-identical" + ); + read_recursive_proof_artifact(&native_path) + .expect("decode native artifact") + .verify(&inner_program()) + .expect("native artifact verifies"); + read_recursive_proof_artifact(&seam_path) + .expect("decode seam artifact") + .verify(&inner_program()) + .expect("input-ready artifact verifies"); + + std::fs::remove_dir_all(&directory).expect("remove exactness directory"); +} + +#[test] +fn gate0_pending_output_is_create_new_and_reopen_exact() { + let nonce = std::time::SystemTime::now() + .duration_since(std::time::UNIX_EPOCH) + .expect("system clock is after the Unix epoch") + .as_nanos(); + let directory = std::env::temp_dir().join(format!("leanvm-gate0-output-{}-{nonce}", std::process::id())); + std::fs::create_dir(&directory).expect("create output test directory"); + let output = directory.join("artifact.bin"); + let payload = b"gate0-durable-output-v1"; + + let mut pending = PendingOutput::create(&output).expect("create pending output"); + pending.write_and_sync(payload).expect("write and sync pending output"); + assert_eq!(pending.readback().expect("read pending output"), payload); + pending.publish().expect("publish pending output"); + assert_eq!(std::fs::read(&output).expect("reopen published output"), payload); + + match PendingOutput::create(&output) { + Err(error) => assert_eq!(error.kind(), io::ErrorKind::AlreadyExists), + Ok(_) => panic!("create-new output must reject an existing target"), + } + std::fs::remove_file(&output).expect("remove output test artifact"); + std::fs::remove_dir(&directory).expect("remove output test directory"); +} + /// Run recursion with one transcript-bound PCS rate per inner proof. The guest /// bytecode is independent of these values and supports mixed-rate batches. fn run_recursion_with_rates( diff --git a/src/main.rs b/src/main.rs index d12de05e..06f6bd32 100644 --- a/src/main.rs +++ b/src/main.rs @@ -5,6 +5,10 @@ //! cargo run --release -- xmss --n-signatures 820 --log-inv-rate 2 //! cargo run --release -- xmss --n-signatures 820 --repeat 5 //! cargo run --release -- recursion --n 2 +//! cargo run --release -- recursion-prepare --output children.bin --n 2 +//! cargo run --release -- recursion-inspect --fixture children.bin +//! cargo run --release -- recursion-aggregate --fixture children.bin --output proof.bin +//! cargo run --release -- recursion-proof-inspect --artifact proof.bin //! cargo run --release -- fibonacci --n 2000000 //! cargo run --release -- --tracing fibonacci --n 2000000 //! ``` @@ -15,6 +19,8 @@ //! the mean. `--cooldown` (seconds, default 2) idles before each pass so a //! thermally limited laptop does not report its power budget as proving cost. +use std::path::PathBuf; + use clap::{Parser, Subcommand}; #[derive(Parser)] @@ -71,6 +77,50 @@ enum Command { /// range check gives out just above 66000, so this is near the ceiling. #[arg(long, default_value = "64000")] iters: usize, + /// Create a deterministic, create-new artifact from the proof returned + /// by the unchanged native recursion path. + #[arg(long, value_name = "PATH")] + proof_artifact_v2: Option, + }, + /// Prove canonical children once and publish an input-ready fixture. + #[command(name = "recursion-prepare")] + RecursionPrepare { + /// Create-new output path for the child-proof fixture. + #[arg(long)] + output: PathBuf, + /// Number of child proofs. + #[arg(long, default_value = "2")] + n: usize, + /// BLAKE3 compressions per child proof. + #[arg(long, default_value = "8")] + hashes: usize, + /// MUL iterations per child proof. + #[arg(long, default_value = "64000")] + iters: usize, + }, + /// Reopen, exactly decode, and verify every proof in a child fixture. + #[command(name = "recursion-inspect")] + RecursionInspect { + /// Existing child-proof fixture. + #[arg(long)] + fixture: PathBuf, + }, + /// Aggregate an input-ready fixture and publish a verified proof artifact. + #[command(name = "recursion-aggregate")] + RecursionAggregate { + /// Existing child-proof fixture. + #[arg(long)] + fixture: PathBuf, + /// Create-new output path for the recursive proof artifact. + #[arg(long)] + output: PathBuf, + }, + /// Reopen, exactly decode, and verify a recursive proof artifact twice. + #[command(name = "recursion-proof-inspect")] + RecursionProofInspect { + /// Existing recursive proof artifact. + #[arg(long)] + artifact: PathBuf, }, /// Prove and verify Fibonacci in the exponent (demo). Fibonacci { @@ -110,9 +160,60 @@ fn main() { } // `run_recursion` initializes tracing itself, after the guest compile it // does not want traced. - Command::Recursion { n, hashes, iters } => { + Command::Recursion { + n, + hashes, + iters, + proof_artifact_v2, + } => { + let inner: Vec<(usize, usize)> = (0..*n).map(|_| (*hashes, *iters)).collect(); + if let Some(output) = proof_artifact_v2 { + rec_aggregation::run_recursion_with_artifact(&inner, cli.log_inv_rate, cli.tracing, output, plan) + .unwrap_or_else(|error| { + eprintln!("recursive proof artifact failed: {error}"); + std::process::exit(1); + }); + } else { + rec_aggregation::run_recursion(&inner, cli.log_inv_rate, cli.tracing, plan); + } + } + Command::RecursionPrepare { + output, + n, + hashes, + iters, + } => { let inner: Vec<(usize, usize)> = (0..*n).map(|_| (*hashes, *iters)).collect(); - rec_aggregation::run_recursion(&inner, cli.log_inv_rate, cli.tracing, plan); + rec_aggregation::prepare_recursion_fixture(&inner, cli.log_inv_rate, output) + .unwrap_or_else(|error| { + eprintln!("recursion fixture preparation failed: {error}"); + std::process::exit(1); + }) + .print(); + } + Command::RecursionInspect { fixture } => { + rec_aggregation::inspect_recursion_fixture(fixture) + .unwrap_or_else(|error| { + eprintln!("recursion fixture inspection failed: {error}"); + std::process::exit(1); + }) + .print(); + } + Command::RecursionAggregate { fixture, output } => { + rec_aggregation::run_recursion_fixture_aggregation(fixture, output, cli.log_inv_rate, cli.tracing) + .unwrap_or_else(|error| { + eprintln!("recursion fixture aggregation failed: {error}"); + std::process::exit(1); + }) + .print(); + } + Command::RecursionProofInspect { artifact } => { + rec_aggregation::inspect_recursive_proof_artifact(artifact) + .unwrap_or_else(|error| { + eprintln!("recursive proof inspection failed: {error}"); + std::process::exit(1); + }) + .print(); } Command::Fibonacci { n } => { if cli.tracing { From 4892eeeb7eb7be6ff006d60276ffaeba42d54cd1 Mon Sep 17 00:00:00 2001 From: Adam Mohammed A Latif Date: Wed, 5 Aug 2026 14:12:53 +0000 Subject: [PATCH 02/22] experiment: rederive direct fold6 on c091b044 --- crates/pcs/src/ring_switch.rs | 221 +++++++++++++++- crates/pcs/src/stack_open.rs | 481 +++++++++++++++++++++++++++++++++- crates/pcs/src/whir.rs | 224 +++++++++++++++- 3 files changed, 905 insertions(+), 21 deletions(-) diff --git a/crates/pcs/src/ring_switch.rs b/crates/pcs/src/ring_switch.rs index b78022da..1dcc9e20 100644 --- a/crates/pcs/src/ring_switch.rs +++ b/crates/pcs/src/ring_switch.rs @@ -73,7 +73,7 @@ use fiat_shamir::sponge::Sponge; use primitives::bits::transpose_8x8_bits; -use primitives::field::{F64, F192}; +use primitives::field::{F64, F192, F192BaseUnreduced}; use serde::{Deserialize, Serialize}; use super::pack::PACKING_WIDTH; @@ -136,16 +136,20 @@ pub const COMPOSITION_SHIFTS: [usize; 6] = [32, 16, 8, 4, 2, 1]; /// nonzero error lies in the kernel for EVERY coefficient choice and passes /// with probability one. pub fn build_coordinate_weights(challenges: &[F192; COMPOSITION_SHIFTS.len()]) -> Vec { - // b_w has only bit w set: bits 0..64 are K's power basis, and bits 64/128 - // shift it by Y / Y^2. - let basis = |w: usize| match w / PACKING_WIDTH { + (0..DEGREE_E) + .map(|w| apply_composed_map(extension_coordinate_basis(w), challenges)) + .collect() +} + +/// The `w`-th coordinate basis element of E over F_2. +#[inline] +fn extension_coordinate_basis(w: usize) -> F192 { + // Bits 0..64 are K's power basis, and bits 64/128 shift it by Y / Y^2. + match w / PACKING_WIDTH { 0 => F192::new(1u64 << (w % PACKING_WIDTH), 0, 0), 1 => F192::new(0, 1u64 << (w % PACKING_WIDTH), 0), _ => F192::new(0, 0, 1u64 << (w % PACKING_WIDTH)), - }; - (0..DEGREE_E) - .map(|w| apply_composed_map(basis(w), challenges)) - .collect() + } } /// Applies the composed map `Phi` of [`build_coordinate_weights`] to one value. @@ -248,6 +252,65 @@ pub fn s_hat_v_from_z_vec(z_vec: &[F192], inner_rest_tail: &[F192]) -> Vec ) } +/// Number of packed-polynomial coordinates retained by the direct fold-6 +/// statistic. +pub const FOLD6_RETAINED_VARS: usize = 6; + +/// Number of endpoints retained across the six deferred coordinates. +pub const FOLD6_ENDPOINT_BANKS: usize = 1 << FOLD6_RETAINED_VARS; + +/// Number of values in the endpoint-major bit-slice representation. +pub const FOLD6_ENDPOINT_VALUES: usize = FOLD6_ENDPOINT_BANKS * PACKING_WIDTH; + +/// Number of entries in the 64 by 64 endpoint-product matrix. +pub const FOLD6_ENDPOINT_MATRIX_VALUES: usize = FOLD6_ENDPOINT_BANKS * FOLD6_ENDPOINT_BANKS; + +/// Retain the six least-significant packed indices while evaluating the tail +/// of a ring-switch suffix point. The output is endpoint-major, with 64 bit +/// slices per endpoint. +pub fn s_hat_v_fold6_from_q_flock(q_flock: &[F64], suffix_point: &[F192]) -> Vec { + assert!(suffix_point.len() >= FOLD6_RETAINED_VARS); + assert_eq!(q_flock.len(), 1usize << suffix_point.len()); + + let high_eq = build_eq_table_ext(&suffix_point[FOLD6_RETAINED_VARS..]); + parallel::fold_reduce( + high_eq.len(), + || vec![F192::ZERO; FOLD6_ENDPOINT_VALUES], + |out, high| { + let weight = high_eq[high]; + let block = &q_flock[high * FOLD6_ENDPOINT_BANKS..(high + 1) * FOLD6_ENDPOINT_BANKS]; + for (endpoint, word) in block.iter().enumerate() { + let mut bits = word.0; + while bits != 0 { + let bit = bits.trailing_zeros() as usize; + out[endpoint * PACKING_WIDTH + bit] += weight; + bits &= bits - 1; + } + } + }, + |mut out, part| { + for (slot, value) in out.iter_mut().zip(part) { + *slot += value; + } + out + }, + ) +} + +/// Collapse a fold-6 endpoint statistic to the canonical 64-entry wire. +pub fn collapse_s_hat_v_fold6(endpoint_banks: &[F192], low_point: &[F192]) -> Vec { + assert_eq!(endpoint_banks.len(), FOLD6_ENDPOINT_VALUES); + assert_eq!(low_point.len(), FOLD6_RETAINED_VARS); + let low_eq = build_eq_table_ext(low_point); + let mut out = vec![F192::ZERO; PACKING_WIDTH]; + for (endpoint, &weight) in low_eq.iter().enumerate() { + for bit in 0..PACKING_WIDTH { + out[bit] += weight * endpoint_banks[endpoint * PACKING_WIDTH + bit]; + } + } + out +} + /// XOR-reduce two per-worker partial accumulators of the bit-slice folds /// (E addition is XOR, so the reduction order does not matter). fn xor_accs(mut a: Vec, b: Vec) -> Vec { @@ -455,6 +518,139 @@ pub(crate) fn prove_finish_deferred( } } +/// Compact ring-switch plan for deferring the first six WHIR folds. +#[derive(Clone, Debug)] +pub struct DirectFold6RingPlan { + batched_sumcheck_claim: F192, + low_eq: [F192; FOLD6_ENDPOINT_BANKS], + tail_eq_lo: Vec, + tail_eq_hi: Vec, + scaled_coordinate_weights: Vec, + endpoint_products: Vec, +} + +impl DirectFold6RingPlan { + pub fn batched_sumcheck_claim(&self) -> F192 { + self.batched_sumcheck_claim + } + + pub fn add_endpoint_products_into(&self, mixed: &mut [F192]) { + assert_eq!(mixed.len(), FOLD6_ENDPOINT_MATRIX_VALUES); + for (out, &value) in mixed.iter_mut().zip(&self.endpoint_products) { + *out += value; + } + } + + /// Materialize only the ring-switch basis remaining after six LSB-first + /// folds. The batching scalar is already included in the plan. + pub fn materialize_basis_after_fold6(&self, fold_challenges: &[F192; FOLD6_RETAINED_VARS]) -> Vec { + let fold_weights = build_eq_table_ext(fold_challenges); + let base_table = build_fold_byte_table_ext(&self.scaled_coordinate_weights); + let mut folded_coordinate_weights = vec![F192::ZERO; DEGREE_E]; + for (coordinate, out) in folded_coordinate_weights.iter_mut().enumerate() { + let basis = extension_coordinate_basis(coordinate); + for (endpoint, &fold_weight) in fold_weights.iter().enumerate() { + *out += fold_weight * fold_one_slot_ext(self.low_eq[endpoint] * basis, &base_table); + } + } + drop(base_table); + let direct_table = build_fold_byte_table_ext(&folded_coordinate_weights); + + let block_len = self.tail_eq_lo.len(); + debug_assert!(block_len.is_power_of_two()); + let mask = block_len - 1; + let shift = block_len.trailing_zeros(); + parallel::map_collect(block_len * self.tail_eq_hi.len(), |high| { + fold_one_slot_ext( + self.tail_eq_lo[high & mask] * self.tail_eq_hi[high >> shift], + &direct_table, + ) + }) + } +} + +#[inline] +fn inner_product_base_ext_deferred(witness: &[F64], weights: &[F192]) -> F192 { + assert_eq!(witness.len(), weights.len()); + witness + .iter() + .zip(weights) + .fold(F192BaseUnreduced::ZERO, |acc, (&base, &weight)| { + acc ^ weight.mul_base_unreduced(base) + }) + .reduce() +} + +/// Finalize a ring-switch claim using a caller-supplied fold-6 endpoint +/// statistic. The observed 64-entry wire is checked against the statistic +/// before the compact plan is returned. +pub fn prove_finish_direct_fold6( + state: RingSwitchProveState, + endpoint_banks: &[F192], + coordinate_weights: &[F192], + gamma: F192, +) -> DirectFold6RingPlan { + assert_eq!(coordinate_weights.len(), DEGREE_E); + assert_eq!(endpoint_banks.len(), FOLD6_ENDPOINT_VALUES); + assert!(state.suffix_point.len() >= FOLD6_RETAINED_VARS); + + let low_eq: [F192; FOLD6_ENDPOINT_BANKS] = build_eq_table_ext(&state.suffix_point[..FOLD6_RETAINED_VARS]) + .try_into() + .expect("six suffix coordinates have sixty-four equality weights"); + assert_eq!( + collapse_s_hat_v_fold6(endpoint_banks, &state.suffix_point[..FOLD6_RETAINED_VARS]), + state.s_hat_v, + "direct fold-6 banks do not refine the observed s_hat_v" + ); + + let s_hat_u = transpose_s_hat(&state.s_hat_v); + let sumcheck_claim = inner_product_base_ext(&s_hat_u, coordinate_weights); + let scaled_coordinate_weights: Vec = coordinate_weights.iter().map(|&weight| gamma * weight).collect(); + let scaled_table = build_fold_byte_table_ext(&scaled_coordinate_weights); + + let changed_weights: Vec = parallel::map_collect(FOLD6_ENDPOINT_BANKS * DEGREE_E, |cell| { + let basis_endpoint = cell / DEGREE_E; + let coordinate = cell % DEGREE_E; + fold_one_slot_ext( + low_eq[basis_endpoint] * extension_coordinate_basis(coordinate), + &scaled_table, + ) + }); + let transposed_banks: Vec> = parallel::map_collect(FOLD6_ENDPOINT_BANKS, |endpoint| { + let start = endpoint * PACKING_WIDTH; + transpose_s_hat(&endpoint_banks[start..start + PACKING_WIDTH]) + }); + let endpoint_products = parallel::map_collect(FOLD6_ENDPOINT_MATRIX_VALUES, |cell| { + let witness_endpoint = cell / FOLD6_ENDPOINT_BANKS; + let basis_endpoint = cell % FOLD6_ENDPOINT_BANKS; + inner_product_base_ext_deferred( + &transposed_banks[witness_endpoint], + &changed_weights[basis_endpoint * DEGREE_E..(basis_endpoint + 1) * DEGREE_E], + ) + }); + + let (tail_eq_lo, tail_eq_hi) = build_eq_split_ext(&state.suffix_point[FOLD6_RETAINED_VARS..]); + DirectFold6RingPlan { + batched_sumcheck_claim: gamma * sumcheck_claim, + low_eq, + tail_eq_lo, + tail_eq_hi, + scaled_coordinate_weights, + endpoint_products, + } +} + +/// Portable fold-6 path for callers without producer-native endpoint banks. +pub fn prove_finish_direct_fold6_from_q_flock( + state: RingSwitchProveState, + q_flock: &[F64], + coordinate_weights: &[F192], + gamma: F192, +) -> DirectFold6RingPlan { + let endpoint_banks = s_hat_v_fold6_from_q_flock(q_flock, &state.suffix_point); + prove_finish_direct_fold6(state, &endpoint_banks, coordinate_weights, gamma) +} + /// Fold several deferred claims directly into their final combined dense basis. /// No per-claim dense vector is allocated or read back, and the first claim /// **writes** rather than accumulates, so the caller need not pre-zero `out`. @@ -620,6 +816,7 @@ pub struct RingSwitchProveState { s_hat_v: Vec, eq_lo: Vec, eq_hi: Vec, + suffix_point: Vec, } /// Phase 1 of the ring-switch prover: compute + observe `s_hat_v` (NO domain @@ -662,7 +859,12 @@ pub fn prove_observe( RingSwitchProof { s_hat_v: s_hat_v.clone(), }, - RingSwitchProveState { s_hat_v, eq_lo, eq_hi }, + RingSwitchProveState { + s_hat_v, + eq_lo, + eq_hi, + suffix_point: suffix_point.to_vec(), + }, ) } @@ -854,6 +1056,7 @@ mod tests { s_hat_v: rng.ext_vec(PACKING_WIDTH), eq_lo, eq_hi, + suffix_point: point.clone(), } }) .collect::>(); diff --git a/crates/pcs/src/stack_open.rs b/crates/pcs/src/stack_open.rs index 9ffae3e7..1c927bad 100644 --- a/crates/pcs/src/stack_open.rs +++ b/crates/pcs/src/stack_open.rs @@ -51,7 +51,7 @@ use crate::merkle::Hash; use fiat_shamir::sponge::Sponge; -use primitives::field::{F64, F192, powers}; +use primitives::field::{F64, F192, F192BaseUnreduced, F192Unreduced, powers}; use primitives::multilinear::eq_eval; use serde::{Deserialize, Serialize}; @@ -59,7 +59,7 @@ use super::pack::PACKING_WIDTH; use super::ring_switch::{self, RingSwitchProof}; use super::whir::{ProverConfig, VerifierConfig}; use super::whir::{ - ProverData, WhirProof, build_eq_table_ext, recursive_prover_with_basis, + ProverData, WhirProof, build_eq_table_ext, recursive_prover_with_basis, recursive_prover_with_basis_direct_fold6, recursive_verifier_with_basis_succinct_with_squeezes, }; @@ -286,6 +286,307 @@ fn stack_claim_eq_at(claim: &StackClaim, x: &[F192]) -> F192 { } } +// --------------------------------------------------------------------------- +// Compact point and strided plans for the first six direct folds +// --------------------------------------------------------------------------- + +/// Equality support after the six low coordinates have been split off. +/// Boolean selector coordinates remain fixed instead of expanding a +/// stack-sized equality table. +struct DirectEqSupport { + fixed_ones: usize, + live_positions: Vec, + live_eq: Vec, +} + +impl DirectEqSupport { + fn new(coords: &[F192]) -> Self { + assert!(coords.len() < usize::BITS as usize); + let mut fixed_ones = 0usize; + let mut live_positions = Vec::new(); + let mut live_coords = Vec::new(); + for (position, &coord) in coords.iter().enumerate() { + if coord == F192::ZERO { + continue; + } + if coord == F192::ONE { + fixed_ones |= 1usize << position; + continue; + } + live_positions.push(position); + live_coords.push(coord); + } + Self { + fixed_ones, + live_positions, + live_eq: build_eq_table_ext(&live_coords), + } + } + + #[inline] + fn full_index(&self, compact_index: usize) -> usize { + let mut full = self.fixed_ones; + for (compact_bit, &full_bit) in self.live_positions.iter().enumerate() { + if (compact_index >> compact_bit) & 1 == 1 { + full |= 1usize << full_bit; + } + } + full + } + + fn weighted_stack_sums(&self, stack: &[F64]) -> [F192; 64] { + let accumulate = |sums: &mut [F192BaseUnreduced; 64], compact_index: usize| { + let weight = self.live_eq[compact_index]; + let base = 64 * self.full_index(compact_index); + for endpoint in 0..64 { + sums[endpoint] ^= weight.mul_base_unreduced(stack[base + endpoint]); + } + }; + let xor = |mut lhs: [F192BaseUnreduced; 64], rhs: [F192BaseUnreduced; 64]| { + for endpoint in 0..64 { + lhs[endpoint] ^= rhs[endpoint]; + } + lhs + }; + let sums = if self.live_eq.len() < 1 << 10 { + let mut sums = [F192BaseUnreduced::ZERO; 64]; + for compact_index in 0..self.live_eq.len() { + accumulate(&mut sums, compact_index); + } + sums + } else { + parallel::fold_reduce(self.live_eq.len(), || [F192BaseUnreduced::ZERO; 64], accumulate, xor) + }; + sums.map(F192BaseUnreduced::reduce) + } + + fn scatter_scaled(&self, dst: &mut [F192], scale: F192) { + if scale == F192::ZERO { + return; + } + for (compact_index, &weight) in self.live_eq.iter().enumerate() { + dst[self.full_index(compact_index)] += scale * weight; + } + } +} + +struct DirectPointGroup { + support: DirectEqSupport, + low_weights: [F192; 64], +} + +struct PendingDirectPointGroup { + tail: Vec, + low_weights: [F192; 64], +} + +fn stack_claim_full_point(claim: &StackClaim, log_stack: usize) -> Vec { + let (mut full, selector, block_vars) = match claim { + StackClaim::Point { offset, low_point, .. } => { + let block_vars = low_point.len(); + let block_len = 1usize << block_vars; + assert!(offset.is_multiple_of(block_len)); + assert!(*offset + block_len <= 1usize << log_stack); + (low_point.clone(), *offset >> block_vars, block_vars) + } + StackClaim::Strided { + offset, + slot, + stride_log, + point, + .. + } => { + let stride = 1usize << stride_log; + let block_vars = stride_log + point.len(); + let block_len = 1usize << block_vars; + assert!(*slot < stride); + assert!(offset.is_multiple_of(block_len)); + assert!(*offset + block_len <= 1usize << log_stack); + let mut low = Vec::with_capacity(block_vars); + for bit in 0..*stride_log { + low.push(if (slot >> bit) & 1 == 1 { F192::ONE } else { F192::ZERO }); + } + low.extend_from_slice(point); + (low, *offset >> block_vars, block_vars) + } + }; + assert!(block_vars <= log_stack); + for bit in 0..log_stack - block_vars { + full.push(if (selector >> bit) & 1 == 1 { + F192::ONE + } else { + F192::ZERO + }); + } + full +} + +fn direct_point_groups(claims: &[StackClaim], gammas: &[F192], log_stack: usize) -> Vec { + assert!(log_stack >= 6); + assert_eq!(claims.len(), gammas.len()); + let mut pending: Vec = Vec::new(); + for (claim, &gamma) in claims.iter().zip(gammas) { + let full = stack_claim_full_point(claim, log_stack); + let low = build_eq_table_ext(&full[..6]); + let tail = &full[6..]; + let group = if let Some(index) = pending.iter().position(|group| group.tail == tail) { + &mut pending[index] + } else { + pending.push(PendingDirectPointGroup { + tail: tail.to_vec(), + low_weights: [F192::ZERO; 64], + }); + pending.last_mut().expect("inserted direct point group") + }; + for endpoint in 0..64 { + group.low_weights[endpoint] += gamma * low[endpoint]; + } + } + pending + .into_iter() + .map(|group| DirectPointGroup { + support: DirectEqSupport::new(&group.tail), + low_weights: group.low_weights, + }) + .collect() +} + +fn add_direct_point_products(products: &mut [F192], stack: &[F64], groups: &[DirectPointGroup]) { + assert_eq!(products.len(), 64 * 64); + for group in groups { + let witness_sums = group.support.weighted_stack_sums(stack); + for witness_endpoint in 0..64 { + for basis_endpoint in 0..64 { + products[64 * witness_endpoint + basis_endpoint] += + witness_sums[witness_endpoint] * group.low_weights[basis_endpoint]; + } + } + } +} + +fn materialize_direct_point_basis_fold6( + folded_len: usize, + groups: Vec, + challenges: [F192; 6], +) -> zk_alloc::ArenaVec { + let fold_weights = build_eq_table_ext(&challenges); + // SAFETY: all-zero bits are the canonical F192 zero. + let mut b_folded = unsafe { zk_alloc::ArenaVec::zeroed(folded_len) }; + for group in groups { + let scale = group + .low_weights + .iter() + .zip(&fold_weights) + .fold(F192::ZERO, |acc, (&low, &fold)| acc + low * fold); + group.support.scatter_scaled(&mut b_folded, scale); + } + b_folded +} + +#[inline] +fn dot_base64(values: &[F64], weights: &[F192]) -> F192 { + assert_eq!(values.len(), 64); + assert_eq!(weights.len(), 64); + values + .iter() + .zip(weights) + .fold(F192BaseUnreduced::ZERO, |acc, (&value, &weight)| { + acc ^ weight.mul_base_unreduced(value) + }) + .reduce() +} + +/// Fold the base witness by six coordinates and compute message M6 in the +/// same pass over the compact basis. +fn fold6_witness_fused_m6( + witness: &[F64], + basis: &[F192], + challenges: &[F192; 6], +) -> (zk_alloc::ArenaVec, super::whir::SumcheckMessage) { + let weights = build_eq_table_ext(challenges); + let out_len = witness.len() / 64; + assert!(out_len >= 2 && out_len.is_power_of_two()); + assert_eq!(basis.len(), out_len); + const CHUNK: usize = 2048; + // SAFETY: each parallel chunk initializes one disjoint output window. + let mut folded = unsafe { zk_alloc::ArenaVec::::uninitialized(out_len) }; + let out = parallel::SendPtr(folded.as_mut_ptr()); + let (u_0, u_2) = parallel::map_reduce( + out_len.div_ceil(CHUNK), + || (F192Unreduced::ZERO, F192Unreduced::ZERO), + |chunk_index| { + let base = chunk_index * CHUNK; + let len = CHUNK.min(out_len - base); + assert!(base.is_multiple_of(2) && len.is_multiple_of(2)); + // SAFETY: chunk indices own disjoint output windows. + let chunk = unsafe { out.slice(base, len) }; + for (local, value) in chunk.iter_mut().enumerate() { + let high = base + local; + *value = dot_base64(&witness[64 * high..64 * (high + 1)], &weights); + } + let mut local_u_0 = F192Unreduced::ZERO; + let mut local_u_2 = F192Unreduced::ZERO; + for local in (0..len).step_by(2) { + let f0 = chunk[local]; + let f1 = chunk[local + 1]; + let b0 = basis[base + local]; + let b1 = basis[base + local + 1]; + local_u_0 ^= f0.mul_unreduced(b0); + local_u_2 ^= (f0 + f1).mul_unreduced(b0 + b1); + } + (local_u_0, local_u_2) + }, + |(a0, a2), (b0, b2)| (a0 ^ b0, a2 ^ b2), + ); + ( + folded, + super::whir::SumcheckMessage { + u_0: u_0.reduce(), + u_2: u_2.reduce(), + }, + ) +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +enum DirectFoldMode { + Dense, + Fold6, +} + +impl DirectFoldMode { + fn trace_label(self) -> &'static str { + match self { + Self::Dense => "dense", + Self::Fold6 => "direct-fold6", + } + } +} + +/// Fail-closed selector for the exact current six-round geometry. +fn direct_fold_mode( + requested: Option<&str>, + stack: &[F64], + config: &ProverConfig, + ring: &RingSwitchOpen, +) -> DirectFoldMode { + let qflock_len = 1usize.checked_shl(ring.qflock_vars as u32); + let eligible = config.initial_k == 6 + && config.ood_samples.first().copied().unwrap_or(0) == 0 + && stack.len().is_power_of_two() + && stack.len() >= 128 + && ring.qflock_vars >= 6 + && qflock_len.is_some_and(|len| { + len.is_multiple_of(64) + && ring.offset.is_multiple_of(64) + && ring.offset.checked_add(len).is_some_and(|end| end <= stack.len()) + }); + if requested == Some("1") && eligible { + DirectFoldMode::Fold6 + } else { + DirectFoldMode::Dense + } +} + // --------------------------------------------------------------------------- // Prover // --------------------------------------------------------------------------- @@ -305,6 +606,20 @@ pub fn open_batch_mixed_whir_stacked( config: &ProverConfig, point_claims: &[StackClaim], ring: &RingSwitchOpen, +) -> BatchOpeningProof { + let requested = std::env::var("LEANVM_PCS_DIRECT_FOLD6").ok(); + let mode = direct_fold_mode(requested.as_deref(), stack, config, ring); + open_batch_mixed_whir_stacked_impl(sponge, stack, prover_data, config, point_claims, ring, mode) +} + +fn open_batch_mixed_whir_stacked_impl( + sponge: &mut Sponge, + stack: &[F64], + prover_data: &ProverData, + config: &ProverConfig, + point_claims: &[StackClaim], + ring: &RingSwitchOpen, + mode: DirectFoldMode, ) -> BatchOpeningProof { let qflock_len = 1usize << ring.qflock_vars; assert!( @@ -322,6 +637,19 @@ pub fn open_batch_mixed_whir_stacked( // Optional phase timing, answering to the same env var as the WHIR // prover/commit tracing (one env lookup per open, no work when unset). let trace = std::env::var_os("WHIR_TRACE").is_some(); + if trace { + eprintln!( + "STACK_OPEN_DIRECT_FOLD schema=2 selected={} literal={} initial_k={} stack_log={} qflock_vars={} ring_offset={} point_claims={} ring_claims={}", + mode.trace_label(), + std::env::var("LEANVM_PCS_DIRECT_FOLD6").as_deref() == Ok("1"), + config.initial_k, + stack.len().trailing_zeros(), + ring.qflock_vars, + ring.offset, + point_claims.len(), + ring.claims.len(), + ); + } let mut t = std::time::Instant::now(); let mark = |label: &str, t: &mut std::time::Instant| { if trace { @@ -358,11 +686,30 @@ pub fn open_batch_mixed_whir_stacked( // Per-claim batching gammas, sampled AFTER all ring-switch messages are // bound. let gammas_rs = powers(sponge.sample(), ring.claims.len()); - let rs_outputs: Vec<_> = rs_states - .into_iter() - .zip(gammas_rs) - .map(|(state, gamma)| ring_switch::prove_finish_deferred(state, &coordinate_weights, gamma)) - .collect(); + let (rs_outputs, direct_ring_plans) = match mode { + DirectFoldMode::Dense => ( + Some( + rs_states + .into_iter() + .zip(gammas_rs) + .map(|(state, gamma)| ring_switch::prove_finish_deferred(state, &coordinate_weights, gamma)) + .collect::>(), + ), + None, + ), + DirectFoldMode::Fold6 => ( + None, + Some( + rs_states + .into_iter() + .zip(gammas_rs) + .map(|(state, gamma)| { + ring_switch::prove_finish_direct_fold6_from_q_flock(state, qflock, &coordinate_weights, gamma) + }) + .collect::>(), + ), + ), + }; drop(gate0_ring_switch); mark("ring-switch proves", &mut t); @@ -373,6 +720,65 @@ pub fn open_batch_mixed_whir_stacked( } let gammas_pd = powers(sponge.sample(), point_claims.len()); + if let Some(direct_ring_plans) = direct_ring_plans { + let mut target = direct_ring_plans + .iter() + .fold(F192::ZERO, |acc, plan| acc + plan.batched_sumcheck_claim()); + target = point_claims + .iter() + .zip(&gammas_pd) + .fold(target, |acc, (claim, &gamma)| acc + gamma * claim.value()); + + let point_groups = direct_point_groups(point_claims, &gammas_pd, stack.len().trailing_zeros() as usize); + let mut products = vec![F192::ZERO; ring_switch::FOLD6_ENDPOINT_MATRIX_VALUES]; + add_direct_point_products(&mut products, stack, &point_groups); + for plan in &direct_ring_plans { + plan.add_endpoint_products_into(&mut products); + } + mark("direct fold-6 plans", &mut t); + + let ring_start = ring.offset / ring_switch::FOLD6_ENDPOINT_BANKS; + let ring_folded_len = qflock_len / ring_switch::FOLD6_ENDPOINT_BANKS; + let materialize = move |witness: &[F64], challenges: [F192; 6]| { + let folded_len = witness.len() / ring_switch::FOLD6_ENDPOINT_BANKS; + let mut b_folded = materialize_direct_point_basis_fold6(folded_len, point_groups, challenges); + let ring_end = ring_start + ring_folded_len; + assert!(ring_end <= b_folded.len()); + let ring_dst = &mut b_folded[ring_start..ring_end]; + for plan in direct_ring_plans { + let contribution = plan.materialize_basis_after_fold6(&challenges); + assert_eq!(contribution.len(), ring_folded_len); + let chunk = parallel::recommended_chunk_size(ring_dst.len()); + parallel::chunks_mut_zip(ring_dst, &contribution, chunk, |_, dst, src| { + for (dst, &value) in dst.iter_mut().zip(src) { + *dst += value; + } + }); + } + let (f_folded, next_msg) = fold6_witness_fused_m6(witness, &b_folded, &challenges); + (f_folded, b_folded, next_msg) + }; + let whir = { + let _gate0 = super::whir::Gate0Span::new("stack_open_whir"); + recursive_prover_with_basis_direct_fold6( + config, + stack, + target, + &prover_data.codeword, + &prover_data.merkle_tree, + products, + materialize, + sponge, + ) + }; + return BatchOpeningProof { + ring_switches: rs_proofs, + whir, + }; + } + + let rs_outputs = rs_outputs.expect("dense mode has deferred ring-switch outputs"); + // 3. Combined target and lifted stack weight b_stack: the gamma-weighted // rs_eq_ind sum scattered at the q_flock slice, plus the point-claim // eq tensors scattered at their offsets. @@ -577,6 +983,10 @@ mod tests { /// nonempty E-valued selector prefix from ris); the crossing regime is /// exercised by `stacked_open_residual_crosses_qflock`. fn build_instance(seed: u64) -> Instance { + build_instance_with_mode(seed, None, DirectFoldMode::Dense) + } + + fn build_instance_with_mode(seed: u64, initial_k: Option, mode: DirectFoldMode) -> Instance { let log_n = 14usize; let col_vars = 12usize; let col_len = 1usize << col_vars; @@ -647,7 +1057,14 @@ mod tests { }], }; - let (pc, vc) = test_configs_for(log_n); + let (pc, vc) = if let Some(initial_k) = initial_k { + ( + default_config(log_n, initial_k, 1).unwrap(), + default_verifier_config(log_n, initial_k, 1).unwrap(), + ) + } else { + test_configs_for(log_n) + }; // Pin the intended residual regime: the residual cube must sit // entirely above the q_flock coords, with at least one selector coord // covered by ris (the E-valued sel prefix) and the rest by y bits. @@ -658,7 +1075,7 @@ mod tests { ); let (cm, pd) = commit(&stack, pc.initial_k, pc.log_inv_rates[0]); let mut ch = Sponge::new(DOMAIN, &[]); - let proof = open_batch_mixed_whir_stacked(&mut ch, &stack, &pd, &pc, &point_claims, &ring); + let proof = open_batch_mixed_whir_stacked_impl(&mut ch, &stack, &pd, &pc, &point_claims, &ring, mode); Instance { vc, @@ -768,6 +1185,52 @@ mod tests { assert_eq!(bytes_a, bytes_b, "proof bytes must be deterministic"); } + #[test] + fn direct_fold6_proof_bytes_and_verifier_match_dense() { + let dense = build_instance_with_mode(0xd1ec_7f06, Some(6), DirectFoldMode::Dense); + let direct = build_instance_with_mode(0xd1ec_7f06, Some(6), DirectFoldMode::Fold6); + assert_eq!(dense.root, direct.root); + assert_eq!(dense.point_claims, direct.point_claims); + assert_eq!(dense.ring.claims, direct.ring.claims); + assert_eq!( + dense.proof, direct.proof, + "direct fold-6 proof object differs from dense" + ); + let dense_bytes = bincode::serialize(&dense.proof).unwrap(); + let direct_bytes = bincode::serialize(&direct.proof).unwrap(); + assert_eq!(dense_bytes, direct_bytes, "direct fold-6 proof bytes differ from dense"); + assert!(verify_instance( + &direct, + &direct.point_claims, + &direct.ring.claims, + &direct.proof, + )); + } + + #[test] + fn direct_fold6_selector_is_literal_and_fail_closed() { + let stack = vec![F64::ZERO; 1 << 14]; + let pc = default_config(14, 6, 1).unwrap(); + let ring = RingSwitchOpen { + offset: 3 << 12, + qflock_vars: 8, + claims: Vec::new(), + }; + assert_eq!(direct_fold_mode(None, &stack, &pc, &ring), DirectFoldMode::Dense); + assert_eq!( + direct_fold_mode(Some("true"), &stack, &pc, &ring), + DirectFoldMode::Dense + ); + assert_eq!(direct_fold_mode(Some("1"), &stack, &pc, &ring), DirectFoldMode::Fold6); + + let mut ineligible = ring; + ineligible.qflock_vars = 5; + assert_eq!( + direct_fold_mode(Some("1"), &stack, &pc, &ineligible), + DirectFoldMode::Dense, + ); + } + /// Residual cube crossing INTO the q_flock slice (case split = n_ris in the /// verifier closure): q_flock occupies half a 2^14 stack (qflock_vars = 13), /// and the fallback config's residual cube (yr_log_n = 3) is wider than diff --git a/crates/pcs/src/whir.rs b/crates/pcs/src/whir.rs index 540c6a63..94d7d07b 100644 --- a/crates/pcs/src/whir.rs +++ b/crates/pcs/src/whir.rs @@ -565,6 +565,63 @@ pub struct SumcheckMessage { pub u_2: F192, } +/// Adaptive endpoint-product state for the first six LSB-first sumcheck +/// messages. The row-major 64 by 64 matrix represents all products after the +/// high coordinates have already been summed out. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct DirectFold6Messages { + products: Vec, + width: usize, +} + +impl DirectFold6Messages { + pub fn new(products: Vec) -> Self { + assert_eq!(products.len(), 64 * 64); + Self { products, width: 64 } + } + + pub fn current_message(&self) -> SumcheckMessage { + assert!(self.width >= 2 && self.width.is_power_of_two()); + let mut u_0 = F192::ZERO; + let mut u_2 = F192::ZERO; + for pair in 0..self.width / 2 { + let even = 2 * pair; + let odd = even + 1; + u_0 += self.products[even * self.width + even]; + u_2 += self.products[even * self.width + even] + + self.products[even * self.width + odd] + + self.products[odd * self.width + even] + + self.products[odd * self.width + odd]; + } + SumcheckMessage { u_0, u_2 } + } + + pub fn fold_and_message(&mut self, challenge: F192) -> SumcheckMessage { + assert!(self.width >= 4); + let old_width = self.width; + let new_width = old_width / 2; + let mut rows_folded = vec![F192::ZERO; new_width * old_width]; + for row in 0..new_width { + for column in 0..old_width { + let p0 = self.products[(2 * row) * old_width + column]; + let p1 = self.products[(2 * row + 1) * old_width + column]; + rows_folded[row * old_width + column] = p0 + challenge * (p0 + p1); + } + } + let mut next = vec![F192::ZERO; new_width * new_width]; + for row in 0..new_width { + for column in 0..new_width { + let p0 = rows_folded[row * old_width + 2 * column]; + let p1 = rows_folded[row * old_width + 2 * column + 1]; + next[row * new_width + column] = p0 + challenge * (p0 + p1); + } + } + self.products = next; + self.width = new_width; + self.current_message() + } +} + /// Round-quadratic in coefficient form `c + b X + a X^2` (verifier side). #[derive(Clone, Copy, Debug)] struct RoundQuad { @@ -877,6 +934,36 @@ impl<'a> SumcheckProver<'a> { (inst, msg) } + /// Resume after six deferred folds using compact, already-folded vectors + /// and the seventh message computed in the same pass as materialization. + fn new_ext_after_prefix_with_message( + f: ArenaVec, + b1: ArenaVec, + h1: F192, + mut prefix: Vec, + challenges: &[F192], + msg: SumcheckMessage, + ) -> (Self, SumcheckMessage) { + assert_eq!(f.len(), b1.len()); + assert_eq!(prefix.len(), challenges.len()); + let mut t_r = h1; + for (&prefix_msg, &challenge) in prefix.iter().zip(challenges) { + t_r = RoundQuad::from_msg(prefix_msg, t_r).eval(challenge); + } + prefix.push(msg); + ( + Self { + f: Witness::Ext(f), + combined_basis: b1, + t_r, + transcript: prefix, + round: challenges.len(), + pending_glue: None, + }, + msg, + ) + } + fn fold(&mut self, r: F192) -> SumcheckMessage { self.round += 1; let log_size = match &self.f { @@ -1094,6 +1181,14 @@ fn stored_opening( (rows, multi_proof) } +type DirectFold6Materializer<'a> = + Box (ArenaVec, ArenaVec, SumcheckMessage) + 'a>; + +struct DirectFold6Init<'a> { + messages: DirectFold6Messages, + materialize: DirectFold6Materializer<'a>, +} + /// Prove `Σ_x witness(x) · b_initial(x) = target` against the L0 commitment /// produced by [`commit`] (with `log_batch_size = config.initial_k` and /// `log_inv_rate = config.log_inv_rates[0]`). @@ -1113,6 +1208,68 @@ pub fn recursive_prover_with_basis( l0_codeword: &[F64], l0_tree: &[Hash], sponge: &mut Sponge, +) -> WhirProof { + recursive_prover_with_basis_impl( + config, + witness, + Some(b_initial), + target, + l0_codeword, + l0_tree, + None, + sponge, + ) +} + +/// Run the ordinary WHIR prover after deferring exactly the first six folds to +/// a 64 by 64 endpoint-product matrix and a compact materializer. +#[allow(clippy::too_many_arguments)] +pub(crate) fn recursive_prover_with_basis_direct_fold6<'a, M>( + config: &ProverConfig, + witness: &'a [F64], + target: F192, + l0_codeword: &[F64], + l0_tree: &[Hash], + products: Vec, + materialize: M, + sponge: &mut Sponge, +) -> WhirProof +where + M: FnOnce(&[F64], [F192; 6]) -> (ArenaVec, ArenaVec, SumcheckMessage) + 'a, +{ + assert_eq!(config.initial_k, 6, "direct fold-6 requires initial_k = 6"); + assert!( + witness.len() >= 128, + "direct fold-6 requires a nontrivial folded witness" + ); + assert_eq!(products.len(), 64 * 64); + let diagonal = (0..64).fold(F192::ZERO, |acc, endpoint| acc + products[64 * endpoint + endpoint]); + assert_eq!(diagonal, target, "direct fold-6 endpoint matrix must encode the target"); + recursive_prover_with_basis_impl( + config, + witness, + None, + target, + l0_codeword, + l0_tree, + Some(DirectFold6Init { + messages: DirectFold6Messages::new(products), + materialize: Box::new(materialize), + }), + sponge, + ) +} + +#[allow(clippy::too_many_arguments)] +fn recursive_prover_with_basis_impl<'a>( + config: &ProverConfig, + witness: &'a [F64], + mut b_initial: Option>, + target: F192, + l0_codeword: &[F64], + l0_tree: &[Hash], + mut direct: Option>, + sponge: &mut Sponge, ) -> WhirProof { let log_n = witness.len().trailing_zeros() as usize; let r = config.level_steps; @@ -1146,7 +1303,13 @@ pub fn recursive_prover_with_basis( ]; assert_eq!(witness.len(), 1usize << log_n); - assert_eq!(b_initial.len(), 1usize << log_n); + if let Some(b_initial) = &b_initial { + assert!(direct.is_none()); + assert_eq!(b_initial.len(), 1usize << log_n); + } else { + assert!(direct.is_some(), "missing initial sumcheck basis"); + assert_eq!(initial_k, 6); + } assert_eq!(config.level_ks.len(), r); assert_eq!(config.log_inv_rates.len(), r + 1); assert!(r >= 1); @@ -1193,7 +1356,27 @@ pub fn recursive_prover_with_basis( let _t = std::time::Instant::now(); let gate0_initial_sumcheck = Gate0Span::new("whir_initial_sumcheck"); let sumcheck_span = tracing::info_span!("Sumcheck"); - let (mut sc_prover, start_msg) = sumcheck_span.in_scope(|| SumcheckProver::new(witness, b_initial, target)); + let (mut sc_prover, start_msg) = sumcheck_span.in_scope(|| { + if let Some(direct) = &direct { + (None, direct.messages.current_message()) + } else { + let (prover, msg) = SumcheckProver::new( + witness, + b_initial.take().expect("dense initialization requires a basis"), + target, + ); + (Some(prover), msg) + } + }); + let mut direct_prefix = if direct.is_some() { vec![start_msg] } else { Vec::new() }; + if trace { + eprintln!( + "WHIR_DIRECT_FOLD6 schema=1 selected={} initial_k={} log_n={}", + direct.is_some(), + initial_k, + log_n, + ); + } sponge.observe(start_msg.u_0); sponge.observe(start_msg.u_2); @@ -1207,7 +1390,41 @@ pub fn recursive_prover_with_basis( fold_grinding_nonces.push(sponge.grind_pow(bits)); } let r_j = sponge.sample(); - let msg = sumcheck_span.in_scope(|| sc_prover.fold(r_j)); + let msg = sumcheck_span.in_scope(|| { + if direct.is_some() { + if j + 1 < 6 { + let msg = direct + .as_mut() + .expect("direct fold-6 prefix state") + .messages + .fold_and_message(r_j); + direct_prefix.push(msg); + msg + } else { + assert_eq!(j + 1, 6, "direct fold-6 must hand off after six challenges"); + let mut challenge_vec = r_lane_fold.clone(); + challenge_vec.push(r_j); + let challenges: [F192; 6] = challenge_vec.try_into().expect("six direct fold challenges"); + let init = direct.take().expect("direct fold-6 handoff state"); + let (f_folded, b_folded, next_msg) = (init.materialize)(witness, challenges); + let expected_len = 1usize << (log_n - 6); + assert_eq!(f_folded.len(), expected_len); + assert_eq!(b_folded.len(), expected_len); + let (prover, msg) = SumcheckProver::new_ext_after_prefix_with_message( + f_folded, + b_folded, + target, + std::mem::take(&mut direct_prefix), + &challenges, + next_msg, + ); + sc_prover = Some(prover); + msg + } + } else { + sc_prover.as_mut().expect("sumcheck prover materialized").fold(r_j) + } + }); sponge.observe(msg.u_0); sponge.observe(msg.u_2); r_lane_fold.push(r_j); @@ -1217,6 +1434,7 @@ pub fn recursive_prover_with_basis( if trace { t_init_sumcheck += _t.elapsed(); } + let mut sc_prover = sc_prover.expect("initial sumcheck must materialize a prover"); // Commit f^1 = folded (now E-valued) witness as wtns_1. let n1 = log_n - initial_k; From cd11645df29d93120c8f193740938540100ce39b Mon Sep 17 00:00:00 2001 From: Adam Mohammed A Latif Date: Thu, 6 Aug 2026 14:13:43 +0000 Subject: [PATCH 03/22] research: add opt-in GKR phase attribution --- crates/lean_vm/src/gkr.rs | 41 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) diff --git a/crates/lean_vm/src/gkr.rs b/crates/lean_vm/src/gkr.rs index 4239f198..a40975cb 100644 --- a/crates/lean_vm/src/gkr.rs +++ b/crates/lean_vm/src/gkr.rs @@ -316,6 +316,9 @@ pub struct ProductTriple { /// Prove three identity-padded grand products as one RLC-batched radix-four GKR. pub fn prove_product_triple(leaves: [LeafVector; 3], ps: &mut ProverState) -> ProductTriple { + let detail_trace = std::env::var("LEANVM_GKR_DETAIL_TRACE").as_deref() == Ok("1"); + let total_started = detail_trace.then(std::time::Instant::now); + let leaf_lengths: [usize; 3] = std::array::from_fn(|lane| leaves[lane].leaves.len()); let mu = crate::log2_ceil_usize(leaves[0].leaves.len()); assert!( leaves @@ -323,7 +326,15 @@ pub fn prove_product_triple(leaves: [LeafVector; 3], ps: &mut ProverState) -> Pr .all(|lane| !lane.leaves.is_empty() && lane.leaves.len() <= 1 << mu), "batched trees must be nonempty prefixes of the first tree's logical tree" ); + let build_started = detail_trace.then(std::time::Instant::now); let mut layers = leaves.map(|lane| build_layers(lane, mu)); + let build_ns = build_started.map_or(0, |started| started.elapsed().as_nanos()); + let retained_layer_values: [usize; 3] = + std::array::from_fn(|tree| layers[tree].iter().map(|layer| layer.values.len()).sum()); + let retained_layer_bytes = retained_layer_values + .iter() + .sum::() + .saturating_mul(std::mem::size_of::()); let roots = [ layers[0][mu].values[0], layers[1][mu].values[0], @@ -337,6 +348,11 @@ pub fn prove_product_triple(leaves: [LeafVector; 3], ps: &mut ProverState) -> Pr let mut values = roots; let mut layer = mu; + let mut message_ns = 0u128; + let mut fold_ns = 0u128; + let mut equality_ns = 0u128; + let mut message_rounds = 0usize; + let mut equality_peak_entries = 0usize; while layer > 0 { let round_count = mu - layer; if layer % 2 == 1 { @@ -367,23 +383,41 @@ pub fn prove_product_triple(leaves: [LeafVector; 3], ps: &mut ProverState) -> Pr let Layer { values } = std::mem::take(&mut layers[tree][layer - 2]); QuaternaryLayerState::new(values, width) }); + let equality_started = detail_trace.then(std::time::Instant::now); let mut equality = if round_count > 0 { eq_table(&point[1..]) } else { Vec::new() }; + equality_peak_entries = equality_peak_entries.max(equality.len()); + if let Some(started) = equality_started { + equality_ns += started.elapsed().as_nanos(); + } let mut round_point = Vec::with_capacity(round_count); for _ in 0..round_count { + let message_started = detail_trace.then(std::time::Instant::now); let messages = [0, 1, 2].map(|tree| trees[tree].round_message(&equality)); + if let Some(started) = message_started { + message_ns += started.elapsed().as_nanos(); + } + message_rounds += 1; ps.add_scalars(&[0, 1, 2, 3].map(|coefficient| { messages[0][coefficient] + lambda * (messages[1][coefficient] + lambda * messages[2][coefficient]) })); let challenge = ps.sample(); round_point.push(challenge); + let fold_started = detail_trace.then(std::time::Instant::now); for tree in &mut trees { tree.fold(challenge); } + if let Some(started) = fold_started { + fold_ns += started.elapsed().as_nanos(); + } + let equality_started = detail_trace.then(std::time::Instant::now); shrink_eq_low(&mut equality); + if let Some(started) = equality_started { + equality_ns += started.elapsed().as_nanos(); + } } for tree in &trees { @@ -405,6 +439,13 @@ pub fn prove_product_triple(leaves: [LeafVector; 3], ps: &mut ProverState) -> Pr layer -= 2; } + if let Some(started) = total_started { + eprintln!( + "LEANVM_GKR_DETAIL schema=1 mu={mu} leaf_lengths={leaf_lengths:?} retained_layer_values={retained_layer_values:?} retained_layer_bytes={retained_layer_bytes} build_ns={build_ns} message_ns={message_ns} fold_ns={fold_ns} equality_ns={equality_ns} message_rounds={message_rounds} equality_peak_entries={equality_peak_entries} total_ns={}", + started.elapsed().as_nanos(), + ); + } + ProductTriple { roots, point, values } } From 12dce362633e88aab4e8fbe31f6867be825e631d Mon Sep 17 00:00:00 2001 From: Adam Mohammed A Latif Date: Thu, 6 Aug 2026 14:25:51 +0000 Subject: [PATCH 04/22] experiment: skip redundant GKR fold zero fill --- crates/lean_vm/src/gkr.rs | 52 ++++++++++++++++++++++++++++++++++++--- 1 file changed, 49 insertions(+), 3 deletions(-) diff --git a/crates/lean_vm/src/gkr.rs b/crates/lean_vm/src/gkr.rs index a40975cb..2d0ea525 100644 --- a/crates/lean_vm/src/gkr.rs +++ b/crates/lean_vm/src/gkr.rs @@ -255,11 +255,28 @@ impl QuaternaryLayerState { message.map(F192Unreduced::reduce) } - fn fold(&mut self, challenge: F192) { + fn fold(&mut self, challenge: F192, uninitialized_output: bool) { let stored_rows = self.values.len() / 4; let full_rows = stored_rows / 2; let rows = stored_rows.div_ceil(2); - self.next.resize(4 * rows, F192::ZERO); + let next_len = 4 * rows; + if uninitialized_output { + if self.next.capacity() == 0 { + // SAFETY: the full-row path writes `4 * full_rows` slots and the + // odd-row path writes the remaining four slots, when present. + // Since `rows = ceil(stored_rows / 2)`, together they initialize + // exactly `next_len` slots before the buffer is read or swapped. + self.next = unsafe { ArenaVec::uninitialized(next_len) }; + } else { + // After the first fold the two buffers alternate. The previous + // input is always at least as long as this geometrically shrinking + // output, so retaining its initialized prefix needs no fill. + debug_assert!(self.next.len() >= next_len); + self.next.truncate(next_len); + } + } else { + self.next.resize(next_len, F192::ZERO); + } let (values, next) = (&self.values, &mut self.next); let fold_row = |row: usize, destination: &mut [F192]| { let lo = 8 * row; @@ -317,6 +334,10 @@ pub struct ProductTriple { /// Prove three identity-padded grand products as one RLC-batched radix-four GKR. pub fn prove_product_triple(leaves: [LeafVector; 3], ps: &mut ProverState) -> ProductTriple { let detail_trace = std::env::var("LEANVM_GKR_DETAIL_TRACE").as_deref() == Ok("1"); + let uninitialized_fold_output = std::env::var("LEANVM_GKR_UNINIT_FOLD").as_deref() == Ok("1"); + if std::env::var_os("LEANVM_GKR_UNINIT_FOLD").is_some() { + eprintln!("LEANVM_GKR_FOLD_OUTPUT schema=1 uninitialized={uninitialized_fold_output}"); + } let total_started = detail_trace.then(std::time::Instant::now); let leaf_lengths: [usize; 3] = std::array::from_fn(|lane| leaves[lane].leaves.len()); let mu = crate::log2_ceil_usize(leaves[0].leaves.len()); @@ -408,7 +429,7 @@ pub fn prove_product_triple(leaves: [LeafVector; 3], ps: &mut ProverState) -> Pr round_point.push(challenge); let fold_started = detail_trace.then(std::time::Instant::now); for tree in &mut trees { - tree.fold(challenge); + tree.fold(challenge, uninitialized_fold_output); } if let Some(started) = fold_started { fold_ns += started.elapsed().as_nanos(); @@ -648,4 +669,29 @@ mod tests { vs.finish().expect("proof stream is consumed"); } } + + #[test] + fn uninitialized_fold_output_matches_zero_filled_path() { + for stored_rows in [2usize, 3, 4, 5, 8, 17, 32, 65] { + let values = (0..4 * stored_rows) + .map(|i| F192::new((13 * i + 1) as u64, (7 * i + 3) as u64, (5 * i + 9) as u64)) + .collect::>(); + let width = stored_rows.next_power_of_two(); + let mut zero_filled = QuaternaryLayerState::new(ArenaVec::from_slice(&values), width); + let mut uninitialized = QuaternaryLayerState::new(ArenaVec::from_slice(&values), width); + let mut round = 0usize; + while zero_filled.values.len() > 4 { + let challenge = F192::new( + (17 * round + 2) as u64, + (19 * round + 5) as u64, + (23 * round + 7) as u64, + ); + zero_filled.fold(challenge, false); + uninitialized.fold(challenge, true); + assert_eq!(uninitialized.values, zero_filled.values); + assert_eq!(uninitialized.logical_rows, zero_filled.logical_rows); + round += 1; + } + } + } } From 974740f6042f5f8b883ebe920255fd3dcb6b5811 Mon Sep 17 00:00:00 2001 From: Adam Mohammed A Latif Date: Thu, 6 Aug 2026 14:44:53 +0000 Subject: [PATCH 05/22] experiment: skip redundant Bus leaf initialization --- crates/lean_vm/src/leaf.rs | 99 +++++++++++++++++++++++++++++++++++--- 1 file changed, 91 insertions(+), 8 deletions(-) diff --git a/crates/lean_vm/src/leaf.rs b/crates/lean_vm/src/leaf.rs index 58915df2..094e17bb 100644 --- a/crates/lean_vm/src/leaf.rs +++ b/crates/lean_vm/src/leaf.rs @@ -158,11 +158,16 @@ fn push_terms<'a>(c: &'a Coord, w: F192, terms: &mut Vec>, constant: &m } } -/// Build one side's leaf vector: block `b` row `z` holds `γ − Σ_i α^i c_i(z)`, -/// followed implicitly by the identity `1` up to `2^μ`. The row-invariant -/// `α`-power chain and constant coordinates are folded once per block into -/// `const_part`. -pub fn build_leaves(blocks: &[Block], lay: &Layout, cols: &[&[F64]], alpha: F192, gamma: F192) -> gkr::LeafVector { +/// Build one side's explicit leaf values. Block `b` row `z` holds +/// `γ − Σ_i α^i c_i(z)`; the identity suffix up to `2^μ` remains implicit. +fn build_leaf_values( + blocks: &[Block], + lay: &Layout, + cols: &[&[F64]], + alpha: F192, + gamma: F192, + uninitialized_output: bool, +) -> ArenaVec { let explicit = blocks .iter() .enumerate() @@ -170,7 +175,26 @@ pub fn build_leaves(blocks: &[Block], lay: &Layout, cols: &[&[F64]], alpha: F192 .max() .unwrap_or(1); debug_assert!(explicit <= 1usize << lay.mu); - let mut leaves = ArenaVec::filled(F192::ONE, explicit); + let covered: usize = blocks.iter().map(|block| 1usize << block.kappa).sum(); + debug_assert!(blocks.is_empty() || covered == explicit); + let mut leaves = if uninitialized_output && !blocks.is_empty() { + let canonical = layout(blocks); + assert_eq!( + lay.offsets, canonical.offsets, + "uninitialized leaf output requires canonical offsets" + ); + assert_eq!( + lay.mu, canonical.mu, + "uninitialized leaf output requires the canonical depth" + ); + assert_eq!(covered, explicit, "canonical leaf blocks must tile the explicit prefix"); + // SAFETY: `stack_offsets` packs the power-of-two blocks contiguously + // from zero. Their disjoint destination windows therefore cover all + // `explicit == covered` slots, and each fill joins before return. + unsafe { ArenaVec::uninitialized(explicit) } + } else { + ArenaVec::filled(F192::ONE, explicit) + }; let maxk = blocks.iter().map(|b| b.kappa).max().unwrap_or(0); let gpow = primitives::field::g_powers(1usize << maxk); for (b, blk) in blocks.iter().enumerate() { @@ -210,7 +234,22 @@ pub fn build_leaves(blocks: &[Block], lay: &Layout, cols: &[&[F64]], alpha: F192 } } } - gkr::LeafVector::new(leaves) + leaves +} + +/// Build one side's leaf vector. The row-invariant `α`-power chain and constant +/// coordinates are folded once per block into `const_part`. +pub fn build_leaves(blocks: &[Block], lay: &Layout, cols: &[&[F64]], alpha: F192, gamma: F192) -> gkr::LeafVector { + let uninitialized_output = std::env::var("LEANVM_BUS_UNINIT_LEAVES").as_deref() == Ok("1"); + let values = build_leaf_values(blocks, lay, cols, alpha, gamma, uninitialized_output); + if std::env::var_os("LEANVM_BUS_UNINIT_LEAVES").is_some() { + let covered: usize = blocks.iter().map(|block| 1usize << block.kappa).sum(); + eprintln!( + "LEANVM_BUS_LEAF_OUTPUT schema=1 uninitialized={uninitialized_output} explicit={} covered={covered}", + values.len(), + ); + } + gkr::LeafVector::new(values) } /// One table's bus contribution on one side, as a form over that table's committed @@ -846,7 +885,7 @@ pub fn verify_balance( #[cfg(test)] mod tests { - use super::soundness_bits; + use super::*; /// The bound is `tuple_width · 2^mu` plus the GKR terms, so a wider tuple or a /// deeper bus costs bits. One factor of two more than before this test was @@ -859,4 +898,48 @@ mod tests { assert!(soundness_bits(61, 12) < crate::SECURITY_BITS); assert!(soundness_bits(58, 16) < soundness_bits(58, 1)); } + + #[test] + fn uninitialized_leaf_output_matches_one_filled_path() { + let columns = [ + (0..32).map(|i| F64((3 * i + 1) as u64)).collect::>(), + (0..32).map(|i| F64((5 * i + 7) as u64)).collect::>(), + ]; + let column_slices = columns.each_ref().map(Vec::as_slice); + let blocks = vec![ + Block { + kappa: 3, + coords: vec![Coord::Col(0), Coord::GCol(1, 2), Coord::Const(F64(11))], + }, + Block { + kappa: 5, + coords: vec![Coord::Prod(0, 1, 1), Coord::Index], + }, + Block { + kappa: 2, + coords: vec![Coord::Sum(vec![Coord::Col(0), Coord::Const(F64(13))])], + }, + ]; + let lay = layout(&blocks); + let alpha = F192::new(17, 19, 23); + let gamma = F192::new(29, 31, 37); + let one_filled = build_leaf_values(&blocks, &lay, &column_slices, alpha, gamma, false); + let uninitialized = build_leaf_values(&blocks, &lay, &column_slices, alpha, gamma, true); + assert_eq!(uninitialized, one_filled); + assert_eq!(uninitialized.len(), 44); + } + + #[test] + #[should_panic(expected = "uninitialized leaf output requires canonical offsets")] + fn uninitialized_leaf_output_rejects_noncanonical_layout() { + let blocks = vec![Block { + kappa: 1, + coords: vec![Coord::Const(F64::ONE)], + }]; + let bad_layout = Layout { + mu: 2, + offsets: vec![1], + }; + let _ = build_leaf_values(&blocks, &bad_layout, &[], F192::ONE, F192::ONE, true); + } } From ee2449d21bbd988411b4236df2deabb435446d43 Mon Sep 17 00:00:00 2001 From: Adam Mohammed A Latif Date: Thu, 6 Aug 2026 15:03:47 +0000 Subject: [PATCH 06/22] experiment: reserve quaternary Bus leaf padding --- crates/lean_vm/src/leaf.rs | 58 +++++++++++++++++++++++++++++++------- 1 file changed, 48 insertions(+), 10 deletions(-) diff --git a/crates/lean_vm/src/leaf.rs b/crates/lean_vm/src/leaf.rs index 094e17bb..8fac3d56 100644 --- a/crates/lean_vm/src/leaf.rs +++ b/crates/lean_vm/src/leaf.rs @@ -167,6 +167,7 @@ fn build_leaf_values( alpha: F192, gamma: F192, uninitialized_output: bool, + quaternary_capacity: bool, ) -> ArenaVec { let explicit = blocks .iter() @@ -177,6 +178,11 @@ fn build_leaf_values( debug_assert!(explicit <= 1usize << lay.mu); let covered: usize = blocks.iter().map(|block| 1usize << block.kappa).sum(); debug_assert!(blocks.is_empty() || covered == explicit); + let capacity = if quaternary_capacity { + explicit.next_multiple_of(4) + } else { + explicit + }; let mut leaves = if uninitialized_output && !blocks.is_empty() { let canonical = layout(blocks); assert_eq!( @@ -188,12 +194,17 @@ fn build_leaf_values( "uninitialized leaf output requires the canonical depth" ); assert_eq!(covered, explicit, "canonical leaf blocks must tile the explicit prefix"); + let mut values = ArenaVec::with_capacity(capacity); // SAFETY: `stack_offsets` packs the power-of-two blocks contiguously // from zero. Their disjoint destination windows therefore cover all - // `explicit == covered` slots, and each fill joins before return. - unsafe { ArenaVec::uninitialized(explicit) } + // `explicit == covered` live slots, and each fill joins before return. + // Any quaternary-capacity tail remains outside `len` until GKR writes it. + unsafe { values.set_len(explicit) }; + values } else { - ArenaVec::filled(F192::ONE, explicit) + let mut values = ArenaVec::with_capacity(capacity); + values.resize(explicit, F192::ONE); + values }; let maxk = blocks.iter().map(|b| b.kappa).max().unwrap_or(0); let gpow = primitives::field::g_powers(1usize << maxk); @@ -241,12 +252,24 @@ fn build_leaf_values( /// coordinates are folded once per block into `const_part`. pub fn build_leaves(blocks: &[Block], lay: &Layout, cols: &[&[F64]], alpha: F192, gamma: F192) -> gkr::LeafVector { let uninitialized_output = std::env::var("LEANVM_BUS_UNINIT_LEAVES").as_deref() == Ok("1"); - let values = build_leaf_values(blocks, lay, cols, alpha, gamma, uninitialized_output); - if std::env::var_os("LEANVM_BUS_UNINIT_LEAVES").is_some() { + let quaternary_capacity = std::env::var("LEANVM_BUS_LEAF_QUAD_CAPACITY").as_deref() == Ok("1"); + let values = build_leaf_values( + blocks, + lay, + cols, + alpha, + gamma, + uninitialized_output, + quaternary_capacity, + ); + if std::env::var_os("LEANVM_BUS_UNINIT_LEAVES").is_some() + || std::env::var_os("LEANVM_BUS_LEAF_QUAD_CAPACITY").is_some() + { let covered: usize = blocks.iter().map(|block| 1usize << block.kappa).sum(); eprintln!( - "LEANVM_BUS_LEAF_OUTPUT schema=1 uninitialized={uninitialized_output} explicit={} covered={covered}", + "LEANVM_BUS_LEAF_OUTPUT schema=2 uninitialized={uninitialized_output} quad_capacity={quaternary_capacity} explicit={} capacity={} covered={covered}", values.len(), + values.capacity(), ); } gkr::LeafVector::new(values) @@ -919,14 +942,29 @@ mod tests { kappa: 2, coords: vec![Coord::Sum(vec![Coord::Col(0), Coord::Const(F64(13))])], }, + Block { + kappa: 0, + coords: vec![Coord::Const(F64(17))], + }, ]; let lay = layout(&blocks); let alpha = F192::new(17, 19, 23); let gamma = F192::new(29, 31, 37); - let one_filled = build_leaf_values(&blocks, &lay, &column_slices, alpha, gamma, false); - let uninitialized = build_leaf_values(&blocks, &lay, &column_slices, alpha, gamma, true); + let one_filled = build_leaf_values(&blocks, &lay, &column_slices, alpha, gamma, false, false); + let uninitialized = build_leaf_values(&blocks, &lay, &column_slices, alpha, gamma, true, false); + let mut with_headroom = build_leaf_values(&blocks, &lay, &column_slices, alpha, gamma, true, true); assert_eq!(uninitialized, one_filled); - assert_eq!(uninitialized.len(), 44); + assert_eq!(with_headroom, one_filled); + assert_eq!(uninitialized.len(), 45); + assert_eq!(uninitialized.capacity(), 45); + assert_eq!(with_headroom.capacity(), 48); + let pointer = with_headroom.as_ptr(); + with_headroom.resize(48, F192::ONE); + assert_eq!( + with_headroom.as_ptr(), + pointer, + "quaternary padding must not reallocate" + ); } #[test] @@ -940,6 +978,6 @@ mod tests { mu: 2, offsets: vec![1], }; - let _ = build_leaf_values(&blocks, &bad_layout, &[], F192::ONE, F192::ONE, true); + let _ = build_leaf_values(&blocks, &bad_layout, &[], F192::ONE, F192::ONE, true, true); } } From efefb23d5d5bf0af306a1673e88b2d2007391c01 Mon Sep 17 00:00:00 2001 From: Adam Mohammed A Latif Date: Thu, 6 Aug 2026 15:20:06 +0000 Subject: [PATCH 07/22] experiment: preallocate GKR layer tails --- crates/lean_vm/src/gkr.rs | 60 ++++++++++++++++++++++++++++++++++++--- 1 file changed, 56 insertions(+), 4 deletions(-) diff --git a/crates/lean_vm/src/gkr.rs b/crates/lean_vm/src/gkr.rs index 2d0ea525..74e536a7 100644 --- a/crates/lean_vm/src/gkr.rs +++ b/crates/lean_vm/src/gkr.rs @@ -123,7 +123,7 @@ struct Layer { /// Build only the levels consumed by radix four: `0,2,4,…`, plus a final /// binary root when the logical depth is odd. -fn build_layers(leaves: LeafVector, mu: usize) -> Vec { +fn build_layers(leaves: LeafVector, mu: usize, preallocate_tail: bool) -> Vec { assert!(!leaves.leaves.is_empty()); assert!(leaves.leaves.len() <= 1usize << mu); let mut layers: Vec = (0..=mu).map(|_| Layer::default()).collect(); @@ -132,6 +132,8 @@ fn build_layers(leaves: LeafVector, mu: usize) -> Vec { while level + 2 <= mu { let Layer { values: current } = &layers[level]; let full_rows = current.len() / 4; + let has_tail = current.len() % 4 != 0 && current.len() > 2; + let output_rows = full_rows + usize::from(has_tail); let product = |row: usize| { let [left, right] = mul_pair( [current[4 * row], current[4 * row + 2]], @@ -144,11 +146,28 @@ fn build_layers(leaves: LeafVector, mu: usize) -> Vec { } else if current.len() == 2 { ArenaVec::from_iter([current[0] * current[1]]) } else if full_rows >= PAR_THRESHOLD { - ArenaVec::par_collect(full_rows, product) + if preallocate_tail && has_tail { + // `par_collect` deliberately allocates exactly `full_rows`. + // Appending the identity-padded tail would therefore double the + // buffer and copy every complete row. Reserve the known final + // shape while keeping the live prefix limited to initialized rows. + let mut output = ArenaVec::with_capacity(output_rows); + // SAFETY: the parallel fill below writes every slot in + // `0..full_rows` exactly once and joins before `output` escapes. + unsafe { output.set_len(full_rows) }; + parallel::fill(&mut output, product); + output + } else { + ArenaVec::par_collect(full_rows, product) + } + } else if preallocate_tail && has_tail { + let mut output = ArenaVec::with_capacity(output_rows); + output.extend((0..full_rows).map(product)); + output } else { (0..full_rows).map(product).collect() }; - if current.len() % 4 != 0 && current.len() > 2 { + if has_tail { let row = full_rows; let child = |index| current.get(4 * row + index).copied().unwrap_or(F192::ONE); let [left, right] = mul_pair([child(0), child(2)], [child(1), child(3)]); @@ -335,6 +354,7 @@ pub struct ProductTriple { pub fn prove_product_triple(leaves: [LeafVector; 3], ps: &mut ProverState) -> ProductTriple { let detail_trace = std::env::var("LEANVM_GKR_DETAIL_TRACE").as_deref() == Ok("1"); let uninitialized_fold_output = std::env::var("LEANVM_GKR_UNINIT_FOLD").as_deref() == Ok("1"); + let preallocate_layer_tail = std::env::var("LEANVM_GKR_PREALLOCATE_LAYER_TAIL").as_deref() == Ok("1"); if std::env::var_os("LEANVM_GKR_UNINIT_FOLD").is_some() { eprintln!("LEANVM_GKR_FOLD_OUTPUT schema=1 uninitialized={uninitialized_fold_output}"); } @@ -348,7 +368,7 @@ pub fn prove_product_triple(leaves: [LeafVector; 3], ps: &mut ProverState) -> Pr "batched trees must be nonempty prefixes of the first tree's logical tree" ); let build_started = detail_trace.then(std::time::Instant::now); - let mut layers = leaves.map(|lane| build_layers(lane, mu)); + let mut layers = leaves.map(|lane| build_layers(lane, mu, preallocate_layer_tail)); let build_ns = build_started.map_or(0, |started| started.elapsed().as_nanos()); let retained_layer_values: [usize; 3] = std::array::from_fn(|tree| layers[tree].iter().map(|layer| layer.values.len()).sum()); @@ -356,6 +376,15 @@ pub fn prove_product_triple(leaves: [LeafVector; 3], ps: &mut ProverState) -> Pr .iter() .sum::() .saturating_mul(std::mem::size_of::()); + if std::env::var_os("LEANVM_GKR_PREALLOCATE_LAYER_TAIL").is_some() { + let retained_layer_capacities: [usize; 3] = + std::array::from_fn(|tree| layers[tree].iter().map(|layer| layer.values.capacity()).sum()); + eprintln!( + "LEANVM_GKR_LAYER_CAPACITY schema=1 preallocate_tail={preallocate_layer_tail} \ + retained_values={retained_layer_values:?} \ + retained_capacities={retained_layer_capacities:?}" + ); + } let roots = [ layers[0][mu].values[0], layers[1][mu].values[0], @@ -670,6 +699,29 @@ mod tests { } } + #[test] + fn preallocated_layer_tail_matches_exact_capacity_path() { + for mu in 3..=12 { + for len in [3usize, 5, 6, 7, (1usize << (mu - 1)) + 1, (1usize << mu) - 3] { + let len = len.min(1usize << mu); + let values = (0..len) + .map(|row| F192::new((11 * row + 1) as u64, (7 * row + 3) as u64, row as u64)) + .collect::>(); + let exact = build_layers(LeafVector::new(ArenaVec::from_slice(&values)), mu, false); + let preallocated = build_layers(LeafVector::new(ArenaVec::from_slice(&values)), mu, true); + assert_eq!(exact.len(), preallocated.len()); + for (exact_layer, preallocated_layer) in exact.iter().zip(&preallocated) { + assert_eq!(exact_layer.values, preallocated_layer.values); + assert_eq!( + preallocated_layer.values.capacity(), + preallocated_layer.values.len(), + "the preallocated path retains no spare layer capacity" + ); + } + } + } + } + #[test] fn uninitialized_fold_output_matches_zero_filled_path() { for stored_rows in [2usize, 3, 4, 5, 8, 17, 32, 65] { From ae541223e108db043e23a20822a48832ebd78103 Mon Sep 17 00:00:00 2001 From: Adam Mohammed A Latif Date: Thu, 6 Aug 2026 15:30:57 +0000 Subject: [PATCH 08/22] experiment: preserve quaternary GKR layer headroom --- crates/lean_vm/src/gkr.rs | 53 +++++++++++++++++++++++---------------- 1 file changed, 31 insertions(+), 22 deletions(-) diff --git a/crates/lean_vm/src/gkr.rs b/crates/lean_vm/src/gkr.rs index 74e536a7..ed0e49c9 100644 --- a/crates/lean_vm/src/gkr.rs +++ b/crates/lean_vm/src/gkr.rs @@ -123,7 +123,7 @@ struct Layer { /// Build only the levels consumed by radix four: `0,2,4,…`, plus a final /// binary root when the logical depth is odd. -fn build_layers(leaves: LeafVector, mu: usize, preallocate_tail: bool) -> Vec { +fn build_layers(leaves: LeafVector, mu: usize, quaternary_capacity: bool) -> Vec { assert!(!leaves.leaves.is_empty()); assert!(leaves.leaves.len() <= 1usize << mu); let mut layers: Vec = (0..=mu).map(|_| Layer::default()).collect(); @@ -134,6 +134,7 @@ fn build_layers(leaves: LeafVector, mu: usize, preallocate_tail: bool) -> Vec 2; let output_rows = full_rows + usize::from(has_tail); + let output_capacity = output_rows.next_multiple_of(4); let product = |row: usize| { let [left, right] = mul_pair( [current[4 * row], current[4 * row + 2]], @@ -146,12 +147,13 @@ fn build_layers(leaves: LeafVector, mu: usize, preallocate_tail: bool) -> Vec= PAR_THRESHOLD { - if preallocate_tail && has_tail { + if quaternary_capacity { // `par_collect` deliberately allocates exactly `full_rows`. - // Appending the identity-padded tail would therefore double the - // buffer and copy every complete row. Reserve the known final - // shape while keeping the live prefix limited to initialized rows. - let mut output = ArenaVec::with_capacity(output_rows); + // Appending the identity-padded tail, or padding this output for + // the next quaternary sumcheck, would therefore double and copy + // the buffer. Reserve both known shapes while keeping the live + // prefix limited to initialized rows. + let mut output = ArenaVec::with_capacity(output_capacity); // SAFETY: the parallel fill below writes every slot in // `0..full_rows` exactly once and joins before `output` escapes. unsafe { output.set_len(full_rows) }; @@ -160,8 +162,8 @@ fn build_layers(leaves: LeafVector, mu: usize, preallocate_tail: bool) -> Vec ProductTriple { let detail_trace = std::env::var("LEANVM_GKR_DETAIL_TRACE").as_deref() == Ok("1"); let uninitialized_fold_output = std::env::var("LEANVM_GKR_UNINIT_FOLD").as_deref() == Ok("1"); - let preallocate_layer_tail = std::env::var("LEANVM_GKR_PREALLOCATE_LAYER_TAIL").as_deref() == Ok("1"); + let quaternary_layer_capacity = std::env::var("LEANVM_GKR_QUATERNARY_LAYER_CAPACITY").as_deref() == Ok("1"); if std::env::var_os("LEANVM_GKR_UNINIT_FOLD").is_some() { eprintln!("LEANVM_GKR_FOLD_OUTPUT schema=1 uninitialized={uninitialized_fold_output}"); } @@ -368,7 +370,7 @@ pub fn prove_product_triple(leaves: [LeafVector; 3], ps: &mut ProverState) -> Pr "batched trees must be nonempty prefixes of the first tree's logical tree" ); let build_started = detail_trace.then(std::time::Instant::now); - let mut layers = leaves.map(|lane| build_layers(lane, mu, preallocate_layer_tail)); + let mut layers = leaves.map(|lane| build_layers(lane, mu, quaternary_layer_capacity)); let build_ns = build_started.map_or(0, |started| started.elapsed().as_nanos()); let retained_layer_values: [usize; 3] = std::array::from_fn(|tree| layers[tree].iter().map(|layer| layer.values.len()).sum()); @@ -376,11 +378,11 @@ pub fn prove_product_triple(leaves: [LeafVector; 3], ps: &mut ProverState) -> Pr .iter() .sum::() .saturating_mul(std::mem::size_of::()); - if std::env::var_os("LEANVM_GKR_PREALLOCATE_LAYER_TAIL").is_some() { + if std::env::var_os("LEANVM_GKR_QUATERNARY_LAYER_CAPACITY").is_some() { let retained_layer_capacities: [usize; 3] = std::array::from_fn(|tree| layers[tree].iter().map(|layer| layer.values.capacity()).sum()); eprintln!( - "LEANVM_GKR_LAYER_CAPACITY schema=1 preallocate_tail={preallocate_layer_tail} \ + "LEANVM_GKR_LAYER_CAPACITY schema=2 quaternary_capacity={quaternary_layer_capacity} \ retained_values={retained_layer_values:?} \ retained_capacities={retained_layer_capacities:?}" ); @@ -700,7 +702,7 @@ mod tests { } #[test] - fn preallocated_layer_tail_matches_exact_capacity_path() { + fn quaternary_layer_capacity_matches_exact_capacity_path() { for mu in 3..=12 { for len in [3usize, 5, 6, 7, (1usize << (mu - 1)) + 1, (1usize << mu) - 3] { let len = len.min(1usize << mu); @@ -708,15 +710,22 @@ mod tests { .map(|row| F192::new((11 * row + 1) as u64, (7 * row + 3) as u64, row as u64)) .collect::>(); let exact = build_layers(LeafVector::new(ArenaVec::from_slice(&values)), mu, false); - let preallocated = build_layers(LeafVector::new(ArenaVec::from_slice(&values)), mu, true); - assert_eq!(exact.len(), preallocated.len()); - for (exact_layer, preallocated_layer) in exact.iter().zip(&preallocated) { - assert_eq!(exact_layer.values, preallocated_layer.values); - assert_eq!( - preallocated_layer.values.capacity(), - preallocated_layer.values.len(), - "the preallocated path retains no spare layer capacity" - ); + let quaternary = build_layers(LeafVector::new(ArenaVec::from_slice(&values)), mu, true); + assert_eq!(exact.len(), quaternary.len()); + for (exact_layer, quaternary_layer) in exact.iter().zip(&quaternary) { + assert_eq!(exact_layer.values, quaternary_layer.values); + } + let mut level = 2; + while level <= mu { + let parent_len = quaternary[level - 2].values.len(); + let layer = &quaternary[level].values; + let expected_capacity = if parent_len > 2 { + layer.len().next_multiple_of(4) + } else { + layer.len() + }; + assert_eq!(layer.capacity(), expected_capacity); + level += 2; } } } From eb6f460beb11b57e52cdc8675fdecc72e0c43d24 Mon Sep 17 00:00:00 2001 From: Adam Mohammed A Latif Date: Thu, 6 Aug 2026 15:49:36 +0000 Subject: [PATCH 09/22] experiment: screen AVX-512 MLE fold lanes --- crates/primitives/src/multilinear.rs | 118 +++++++++++++++++++++++++++ 1 file changed, 118 insertions(+) diff --git a/crates/primitives/src/multilinear.rs b/crates/primitives/src/multilinear.rs index 1bbeec5c..457c2a70 100644 --- a/crates/primitives/src/multilinear.rs +++ b/crates/primitives/src/multilinear.rs @@ -256,6 +256,16 @@ pub fn mle_eval(table: &[F64], point: &[F192]) -> F192 { fold_ladder(fold_low_k(table, point[0]), &point[1..]) } +/// [`mle_eval`] with four independent pure-extension folds packed together on +/// x86 AVX-512. The first mixed base/extension fold remains unchanged. +pub fn mle_eval_vec4(table: &[F64], point: &[F192]) -> F192 { + debug_assert_eq!(table.len(), 1 << point.len()); + if point.is_empty() { + return F192::from(table[0]); + } + fold_ladder_vec4(fold_low_k(table, point[0]), &point[1..]) +} + /// The MLE of the pointwise product `a·b` at an `E`-point, i.e. `Σ_z eq(point, /// z)·a(z)·b(z)`. This is NOT `â(point)·b̂(point)`: a product of multilinears is /// not multilinear, so it has to be summed over the cube. The first fold takes the @@ -273,6 +283,21 @@ pub fn mle_eval_prod(a: &[F64], b: &[F64], point: &[F192]) -> F192 { fold_ladder(cur, &point[1..]) } +/// [`mle_eval_prod`] with the same four-output pure-extension fold as +/// [`mle_eval_vec4`]. +pub fn mle_eval_prod_vec4(a: &[F64], b: &[F64], point: &[F192]) -> F192 { + debug_assert_eq!(a.len(), b.len()); + debug_assert_eq!(a.len(), 1 << point.len()); + if point.is_empty() { + return F192::from(a[0] * b[0]); + } + let rho = point[0]; + let cur = (0..a.len() / 2) + .map(|i| interp_k(a[2 * i] * b[2 * i], a[2 * i + 1] * b[2 * i + 1], rho)) + .collect(); + fold_ladder_vec4(cur, &point[1..]) +} + /// Bind the remaining variables of a half-folded `E`-table, LSB-first. fn fold_ladder(mut cur: Vec, point: &[F192]) -> F192 { let mut len = cur.len(); @@ -288,6 +313,41 @@ fn fold_ladder(mut cur: Vec, point: &[F192]) -> F192 { cur[0] } +#[inline] +fn interp_vec4(lo: [F192; 4], hi: [F192; 4], point: F192) -> [F192; 4] { + #[cfg(all(target_arch = "x86_64", target_feature = "vpclmulqdq", target_feature = "avx512f"))] + { + let difference = std::array::from_fn(|lane| lo[lane] + hi[lane]); + // SAFETY: both target features are enabled for the whole crate. + let product = unsafe { crate::field::gf2_64x3::x86_64::mul_vec4([point; 4], difference) }; + std::array::from_fn(|lane| lo[lane] + product[lane]) + } + #[cfg(not(all(target_arch = "x86_64", target_feature = "vpclmulqdq", target_feature = "avx512f")))] + { + std::array::from_fn(|lane| interp(lo[lane], hi[lane], point)) + } +} + +fn fold_ladder_vec4(mut cur: Vec, point: &[F192]) -> F192 { + let mut live = cur.len(); + for &p in point { + let next = live / 2; + let groups = next / 4; + for group in 0..groups { + let first = 4 * group; + let lo = std::array::from_fn(|lane| cur[2 * (first + lane)]); + let hi = std::array::from_fn(|lane| cur[2 * (first + lane) + 1]); + let output = interp_vec4(lo, hi, p); + cur[first..first + 4].copy_from_slice(&output); + } + for i in 4 * groups..next { + cur[i] = interp(cur[2 * i], cur[2 * i + 1], p); + } + live = next; + } + cur[0] +} + /// Barycentric weights over the first `2^k_skip` nodes of the GF(2^8) subfield. /// O(2^{2·k_skip}) field multiplies, a one-time cost. pub fn lagrange_weights_naive(k_skip: usize, z: F192) -> Vec { @@ -296,3 +356,61 @@ pub fn lagrange_weights_naive(k_skip: usize, z: F192) -> Vec { assert!(ell <= 256, "k_skip > 8 would exceed PHI_8_TABLE"); lagrange_weights(&PHI_8_TABLE[..ell], z) } + +#[cfg(test)] +mod vec4_tests { + use super::*; + + fn next_u64(state: &mut u64) -> u64 { + *state = state + .wrapping_mul(0x9e37_79b9_7f4a_7c15) + .wrapping_add(0xda94_2042_e4dd_58b5); + *state + } + + #[test] + fn vec4_mle_paths_match_scalar_exactly() { + let mut state = 0x243f_6a88_85a3_08d3; + for log_n in 1..=14 { + let a: Vec = (0..1usize << log_n).map(|_| F64(next_u64(&mut state))).collect(); + let b: Vec = (0..1usize << log_n).map(|_| F64(next_u64(&mut state))).collect(); + let point: Vec = (0..log_n) + .map(|_| F192::new(next_u64(&mut state), next_u64(&mut state), next_u64(&mut state))) + .collect(); + assert_eq!(mle_eval_vec4(&a, &point), mle_eval(&a, &point)); + assert_eq!(mle_eval_prod_vec4(&a, &b, &point), mle_eval_prod(&a, &b, &point)); + } + } + + #[test] + #[ignore = "production-sized x86 AVX-512 MLE kernel screening probe"] + fn vec4_mle_screen() { + use std::hint::black_box; + use std::time::Instant; + + let log_n = 20usize; + let mut state = 0x1319_8a2e_0370_7344; + let table: Vec = (0..1usize << log_n).map(|_| F64(next_u64(&mut state))).collect(); + let point: Vec = (0..log_n) + .map(|_| F192::new(next_u64(&mut state), next_u64(&mut state), next_u64(&mut state))) + .collect(); + assert_eq!(mle_eval_vec4(&table, &point), mle_eval(&table, &point)); + for repetition in 0..16 { + let candidate_first = repetition & 1 == 1; + for candidate in [candidate_first, !candidate_first] { + let started = Instant::now(); + let value = if candidate { + mle_eval_vec4(&table, &point) + } else { + mle_eval(&table, &point) + }; + let elapsed_ns = started.elapsed().as_nanos(); + black_box(value); + eprintln!( + "MLE_VEC4_PROBE schema=1 repetition={repetition} arm={} elapsed_ns={elapsed_ns}", + if candidate { "candidate" } else { "baseline" } + ); + } + } + } +} From 14f5b606732ca8c56c5ca2119121d8da15ec5de9 Mon Sep 17 00:00:00 2001 From: Adam Mohammed A Latif Date: Thu, 6 Aug 2026 15:42:24 +0000 Subject: [PATCH 10/22] experiment: trace Bus post-GKR phases --- crates/lean_vm/src/leaf.rs | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/crates/lean_vm/src/leaf.rs b/crates/lean_vm/src/leaf.rs index 8fac3d56..754439be 100644 --- a/crates/lean_vm/src/leaf.rs +++ b/crates/lean_vm/src/leaf.rs @@ -694,6 +694,7 @@ pub fn prove_balance( tables: &[(usize, usize)], ps: &mut ProverState, ) -> BusProof { + let detail_trace = std::env::var("LEANVM_BUS_DETAIL_TRACE").as_deref() == Ok("1"); let push_lay = layout(push); let pull_lay = layout(pull); let mut count_lay = layout(count); @@ -720,22 +721,31 @@ pub fn prove_balance( let bus_gkr = crate::stage!("Bus GKR", || { gkr::prove_product_triple([push_leaves, pull_leaves, count_leaves], ps) }); + let post_gkr_started = detail_trace.then(std::time::Instant::now); // Framework blocks keep their per-column claims (deduped: push/pull share ζ); // every table block becomes a form for the zerocheck instead. let mut claims: Vec = Vec::new(); let sides = sides([push, pull, count], [&push_lay, &pull_lay, &count_lay], alpha, gamma); + let setup_ns = post_gkr_started.map_or(0, |started| started.elapsed().as_nanos()); // Each table's columns at ζ[..τ], computed once and shared by the three sides // (a form's linear part factors through them). Nothing here travels, neither the // evaluations nor any total: the verifier derives each side's table share as `Ṽ₀(ζ)` less the // framework decomposition ([`verify_balance`]) and the batch settles it. A // transmitted total would appear in exactly one check, which it could always be // solved to satisfy, and would settle nothing. + let table_evals_started = detail_trace.then(std::time::Instant::now); let table_evals = tables_at(cols, tables, &bus_gkr.point); + let table_evals_ns = table_evals_started.map_or(0, |started| started.elapsed().as_nanos()); + let forms_started = detail_trace.then(std::time::Instant::now); let mut forms = std::array::from_fn(|_| tables.iter().map(|&(_, n)| BusForm::new(n)).collect::>()); + let forms_setup_ns = forms_started.map_or(0, |started| started.elapsed().as_nanos()); let mut frameworks = [F192::ZERO; 3]; + let mut decompose_side_ns = [0u128; 3]; + let decompose_started = detail_trace.then(std::time::Instant::now); crate::stage!("Bus decompose", || { for (s, &(blocks, lay, a, g)) in sides.iter().enumerate() { + let side_started = detail_trace.then(std::time::Instant::now); frameworks[s] = decompose_prove( blocks, lay, @@ -748,9 +758,16 @@ pub fn prove_balance( &mut claims, ps, ); + if let Some(started) = side_started { + decompose_side_ns[s] = started.elapsed().as_nanos(); + } } }); + let decompose_ns = decompose_started.map_or(0, |started| started.elapsed().as_nanos()); + let prod_sums_started = detail_trace.then(std::time::Instant::now); let prod_sums = prod_sums_at(cols, tables, &forms, &bus_gkr.point); + let prod_sums_ns = prod_sums_started.map_or(0, |started| started.elapsed().as_nanos()); + let sigmas_started = detail_trace.then(std::time::Instant::now); let sigmas: [Vec; 3] = std::array::from_fn(|s| { let sigmas: Vec = forms[s] .iter() @@ -767,8 +784,21 @@ pub fn prove_balance( ); sigmas }); + let sigmas_ns = sigmas_started.map_or(0, |started| started.elapsed().as_nanos()); + let bytecode_started = detail_trace.then(std::time::Instant::now); let bytecode_claims = vec![bytecode_claim(push, &bus_gkr.point, ps)]; + let bytecode_ns = bytecode_started.map_or(0, |started| started.elapsed().as_nanos()); + if let Some(started) = post_gkr_started { + eprintln!( + "LEANVM_BUS_DETAIL schema=1 setup_ns={setup_ns} table_evals_ns={table_evals_ns} \ + forms_setup_ns={forms_setup_ns} decompose_ns={decompose_ns} \ + decompose_side_ns={decompose_side_ns:?} prod_sums_ns={prod_sums_ns} \ + sigmas_ns={sigmas_ns} bytecode_ns={bytecode_ns} \ + total_post_gkr_ns={}", + started.elapsed().as_nanos() + ); + } BusProof { claims, bytecode_claims, From b61a0ee64a9e5f41c368f937c56cdbb74fd3908b Mon Sep 17 00:00:00 2001 From: Adam Mohammed A Latif Date: Thu, 6 Aug 2026 15:52:41 +0000 Subject: [PATCH 11/22] experiment: gate AVX-512 Bus MLE folds --- crates/lean_vm/src/leaf.rs | 70 +++++++++++++++++++++++++++++++------- 1 file changed, 58 insertions(+), 12 deletions(-) diff --git a/crates/lean_vm/src/leaf.rs b/crates/lean_vm/src/leaf.rs index 754439be..a5c93cc7 100644 --- a/crates/lean_vm/src/leaf.rs +++ b/crates/lean_vm/src/leaf.rs @@ -12,7 +12,7 @@ use crate::colval::ColVal; use crate::gkr; use crate::transcript::{ProverState, VerifierState}; use primitives::field::{F64, F192, F192BaseUnreduced, g_pow, index_mle}; -use primitives::multilinear::{eq_eval, mle_eval, mle_eval_prod}; +use primitives::multilinear::{eq_eval, mle_eval, mle_eval_prod, mle_eval_prod_vec4, mle_eval_vec4}; use zk_alloc::ArenaVec; /// One tuple coordinate as a function of the block's row `z`. @@ -442,6 +442,24 @@ fn known_claim(claims: &[ColumnClaim], col: usize, point: &[F192]) -> Option F192 { + if vec4 { + mle_eval_vec4(table, point) + } else { + mle_eval(table, point) + } +} + +#[inline] +fn eval_mle_prod(a: &[F64], b: &[F64], point: &[F192], vec4: bool) -> F192 { + if vec4 { + mle_eval_prod_vec4(a, b, point) + } else { + mle_eval_prod(a, b, point) + } +} + /// Prover-side decomposition: reads the real columns, writing each FRESH /// committed value onto the stream and recording the matching claim /// (block/coord order); duplicates reuse the recorded value. @@ -464,6 +482,7 @@ fn decompose_prove( forms: &mut [BusForm], claims: &mut Vec, ps: &mut ProverState, + mle_vec4: bool, ) -> F192 { // Pass 1: enumerate the FRESH committed coords exactly as `decompose_formula` // visits them (blocks in order, coords in order, Col/GCol only, first @@ -485,7 +504,7 @@ fn decompose_prove( } let vals: Vec = parallel::map_collect(jobs.len(), |i| { let (col, kappa) = jobs[i]; - mle_eval(cols[col], &zeta[..kappa]) + eval_mle(cols[col], &zeta[..kappa], mle_vec4) }); // Pass 2: replay in the original order; duplicates reuse the recorded claim. @@ -552,13 +571,17 @@ pub struct BytecodeClaim { /// The public (bytecode) coordinate evaluations of a side at its GKR point, /// block/coord order, with the bytecode block's `κ`. pub fn public_evals(blocks: &[Block], zeta: &[F192]) -> (usize, Vec) { + public_evals_with_mode(blocks, zeta, false) +} + +fn public_evals_with_mode(blocks: &[Block], zeta: &[F192], mle_vec4: bool) -> (usize, Vec) { let mut kappa = 0; let mut out = Vec::new(); for blk in blocks { for c in &blk.coords { if let Coord::Public(vals) = c { kappa = blk.kappa; - out.push(mle_eval(vals, &zeta[..blk.kappa])); + out.push(eval_mle(vals, &zeta[..blk.kappa], mle_vec4)); } } } @@ -653,8 +676,8 @@ impl Absorb for VerifierState<'_> { /// columns are opened ONCE: bind the evaluations, sample the four selector /// challenges, emit the single reduced claim. Both sides run exactly this /// sequence, in this order. -fn bytecode_claim(blocks: &[Block], point: &[F192], t: &mut impl Absorb) -> BytecodeClaim { - let (kbc, pv) = public_evals(blocks, point); +fn bytecode_claim(blocks: &[Block], point: &[F192], t: &mut impl Absorb, mle_vec4: bool) -> BytecodeClaim { + let (kbc, pv) = public_evals_with_mode(blocks, point, mle_vec4); for &v in &pv { t.observe(v); } @@ -695,6 +718,23 @@ pub fn prove_balance( ps: &mut ProverState, ) -> BusProof { let detail_trace = std::env::var("LEANVM_BUS_DETAIL_TRACE").as_deref() == Ok("1"); + let mle_vec4_requested = std::env::var("LEANVM_BUS_MLE_VEC4").as_deref() == Ok("1"); + let mle_vec4_eligible = cfg!(all( + target_arch = "x86_64", + target_feature = "vpclmulqdq", + target_feature = "avx512f" + )); + assert!( + !mle_vec4_requested || mle_vec4_eligible, + "LEANVM_BUS_MLE_VEC4=1 requires an x86-64 VPCLMULQDQ/AVX-512F build" + ); + let mle_vec4 = mle_vec4_requested && mle_vec4_eligible; + if std::env::var_os("LEANVM_BUS_MLE_VEC4").is_some() { + eprintln!( + "LEANVM_BUS_MLE schema=1 requested={mle_vec4_requested} \ + eligible={mle_vec4_eligible} selected={mle_vec4}" + ); + } let push_lay = layout(push); let pull_lay = layout(pull); let mut count_lay = layout(count); @@ -735,7 +775,7 @@ pub fn prove_balance( // transmitted total would appear in exactly one check, which it could always be // solved to satisfy, and would settle nothing. let table_evals_started = detail_trace.then(std::time::Instant::now); - let table_evals = tables_at(cols, tables, &bus_gkr.point); + let table_evals = tables_at(cols, tables, &bus_gkr.point, mle_vec4); let table_evals_ns = table_evals_started.map_or(0, |started| started.elapsed().as_nanos()); let forms_started = detail_trace.then(std::time::Instant::now); let mut forms = std::array::from_fn(|_| tables.iter().map(|&(_, n)| BusForm::new(n)).collect::>()); @@ -757,6 +797,7 @@ pub fn prove_balance( &mut forms[s], &mut claims, ps, + mle_vec4, ); if let Some(started) = side_started { decompose_side_ns[s] = started.elapsed().as_nanos(); @@ -765,7 +806,7 @@ pub fn prove_balance( }); let decompose_ns = decompose_started.map_or(0, |started| started.elapsed().as_nanos()); let prod_sums_started = detail_trace.then(std::time::Instant::now); - let prod_sums = prod_sums_at(cols, tables, &forms, &bus_gkr.point); + let prod_sums = prod_sums_at(cols, tables, &forms, &bus_gkr.point, mle_vec4); let prod_sums_ns = prod_sums_started.map_or(0, |started| started.elapsed().as_nanos()); let sigmas_started = detail_trace.then(std::time::Instant::now); let sigmas: [Vec; 3] = std::array::from_fn(|s| { @@ -787,7 +828,7 @@ pub fn prove_balance( let sigmas_ns = sigmas_started.map_or(0, |started| started.elapsed().as_nanos()); let bytecode_started = detail_trace.then(std::time::Instant::now); - let bytecode_claims = vec![bytecode_claim(push, &bus_gkr.point, ps)]; + let bytecode_claims = vec![bytecode_claim(push, &bus_gkr.point, ps, mle_vec4)]; let bytecode_ns = bytecode_started.map_or(0, |started| started.elapsed().as_nanos()); if let Some(started) = post_gkr_started { eprintln!( @@ -810,12 +851,12 @@ pub fn prove_balance( /// Every table's committed columns at `ζ[..τ_t]`: one `eq` table per table, then an /// inner product per column. `tables[t] = (base, n_cols)` in the global schema. -fn tables_at(cols: &[&[F64]], tables: &[(usize, usize)], zeta: &[F192]) -> Vec> { +fn tables_at(cols: &[&[F64]], tables: &[(usize, usize)], zeta: &[F192], mle_vec4: bool) -> Vec> { tables .iter() .map(|&(base, n_cols)| { let tau = crate::log2_strict_usize(cols[base].len()); - parallel::map_collect(n_cols, |c| mle_eval(cols[base + c], &zeta[..tau])) + parallel::map_collect(n_cols, |c| eval_mle(cols[base + c], &zeta[..tau], mle_vec4)) }) .collect() } @@ -830,6 +871,7 @@ fn prod_sums_at( tables: &[(usize, usize)], forms: &[Vec; 3], zeta: &[F192], + mle_vec4: bool, ) -> Vec> { tables .iter() @@ -844,7 +886,11 @@ fn prod_sums_at( pairs.dedup(); parallel::map_collect(pairs.len(), |i| { let (a, b) = pairs[i]; - (a, b, mle_eval_prod(cols[base + a], cols[base + b], &zeta[..tau])) + ( + a, + b, + eval_mle_prod(cols[base + a], cols[base + b], &zeta[..tau], mle_vec4), + ) }) }) .collect() @@ -925,7 +971,7 @@ pub fn verify_balance( totals[s] = framework + bus_gkr.values[s]; } - let bytecode_claims = vec![bytecode_claim(push, &bus_gkr.point, vs)]; + let bytecode_claims = vec![bytecode_claim(push, &bus_gkr.point, vs, false)]; Ok(BusVerify { claims, bytecode_claims, From 256928f9127c812749e40b08b4cf9744185c6b61 Mon Sep 17 00:00:00 2001 From: Adam Mohammed A Latif Date: Thu, 6 Aug 2026 17:28:26 +0000 Subject: [PATCH 12/22] experiment: gate L0 induce NTT selection --- crates/pcs/src/whir_induce.rs | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/crates/pcs/src/whir_induce.rs b/crates/pcs/src/whir_induce.rs index 9bfc6940..468bb8a8 100644 --- a/crates/pcs/src/whir_induce.rs +++ b/crates/pcs/src/whir_induce.rs @@ -498,7 +498,21 @@ pub(crate) fn induce_sumcheck_poly_auto_base( queries: &[usize], alpha: &[F192], ) -> (ArenaVec, F192) { - if induce_use_ntt_heuristic(log_msg_cols, log_inv_rate, queries.len()) { + let heuristic = induce_use_ntt_heuristic(log_msg_cols, log_inv_rate, queries.len()); + let requested = std::env::var("LEANVM_PCS_L0_INDUCE_NTT").ok(); + let selected = match requested.as_deref() { + Some("1") => true, + Some("0") => false, + _ => heuristic, + }; + if requested.is_some() { + eprintln!( + "LEANVM_PCS_L0_INDUCE schema=1 requested={} heuristic={heuristic} selected={selected} log_msg_cols={log_msg_cols} log_inv_rate={log_inv_rate} queries={}", + requested.as_deref() == Some("1"), + queries.len() + ); + } + if selected { induce_sumcheck_poly_via_ntt_base(log_msg_cols, log_inv_rate, opened_rows, v_challenges, queries, alpha) } else { induce_sumcheck_poly(log_msg_cols, sks_vks, opened_rows, v_challenges, queries, alpha) From 7be45deb92135c615dee0aaa4b294390b2de6902 Mon Sep 17 00:00:00 2001 From: Adam Mohammed A Latif Date: Thu, 6 Aug 2026 19:13:25 +0000 Subject: [PATCH 13/22] perf: select L0 induce NTT for measured shapes --- crates/pcs/src/whir.rs | 33 +++++++++++++++++++-- crates/pcs/src/whir_induce.rs | 56 ++++++++++++++++++++++++++--------- 2 files changed, 73 insertions(+), 16 deletions(-) diff --git a/crates/pcs/src/whir.rs b/crates/pcs/src/whir.rs index 94d7d07b..1d3f2162 100644 --- a/crates/pcs/src/whir.rs +++ b/crates/pcs/src/whir.rs @@ -26,8 +26,9 @@ //! //! Basis induction mirrors the original's two strategies: the dense //! per-query LCH expansion and the sparse transposed-NTT fast path -//! (`induce_sumcheck_poly_via_ntt_base`), with the SAME auto-dispatch size -//! heuristic at L0 (deeper levels stay dense, exactly like the original). +//! (`induce_sumcheck_poly_via_ntt_base`). L0 keeps the original size heuristic +//! and also selects the fast path for the independently measured production +//! family; deeper levels stay dense, exactly like the original. //! //! Soundness note: [`WhirSecurityConfig`] analyzes the actual challenge //! field size `q = 2^192`; the committed alphabet remains `K = GF(2^64)`. @@ -2940,6 +2941,34 @@ mod tests { assert!(configs_for(12).is_err()); } + #[test] + fn l0_induce_policy_and_override_are_narrow_and_fail_closed() { + for log_msg_cols in 19..=21 { + assert!(induce_ntt_validated_shape(log_msg_cols, 2, 113)); + assert!(!induce_use_ntt_heuristic(log_msg_cols, 2, 113)); + assert!(induce_use_ntt_policy(log_msg_cols, 2, 113)); + assert_eq!( + parse_induce_ntt_override(Some(std::ffi::OsStr::new("1")), true), + Ok(Some(true)) + ); + } + assert!(!induce_ntt_validated_shape(18, 2, 113)); + assert_eq!(induce_use_ntt_policy(18, 2, 113), induce_use_ntt_heuristic(18, 2, 113)); + assert_eq!(parse_induce_ntt_override(None, false), Ok(None)); + assert_eq!( + parse_induce_ntt_override(Some(std::ffi::OsStr::new("0")), false), + Ok(Some(false)) + ); + assert!(parse_induce_ntt_override(Some(std::ffi::OsStr::new("1")), false).is_err()); + assert!(parse_induce_ntt_override(Some(std::ffi::OsStr::new("true")), true).is_err()); + #[cfg(unix)] + { + use std::os::unix::ffi::OsStringExt; + let invalid = std::ffi::OsString::from_vec(vec![0xff]); + assert!(parse_induce_ntt_override(Some(&invalid), true).is_err()); + } + } + /// The parallel eq builder must be byte-identical to the serial one, and /// the seeded variant must equal the gamma-scaled table, at sizes on both /// sides of the internal parallel level floor (2^12 halves, so n = 15 diff --git a/crates/pcs/src/whir_induce.rs b/crates/pcs/src/whir_induce.rs index 468bb8a8..386271b9 100644 --- a/crates/pcs/src/whir_induce.rs +++ b/crates/pcs/src/whir_induce.rs @@ -483,12 +483,40 @@ pub(crate) fn induce_use_ntt_heuristic(log_msg_cols: usize, log_inv_rate: usize, log_msg_cols >= 12 && n_queries > 4 * (1usize << log_inv_rate) * log_block.max(1) } +#[inline] +pub(crate) fn induce_ntt_validated_shape(log_msg_cols: usize, log_inv_rate: usize, n_queries: usize) -> bool { + log_inv_rate == 2 && n_queries == 113 && (19..=21).contains(&log_msg_cols) +} + +/// Preserve the inherited heuristic everywhere, then add only the production +/// family measured on both x86-64 and AArch64. +#[inline] +pub(crate) fn induce_use_ntt_policy(log_msg_cols: usize, log_inv_rate: usize, n_queries: usize) -> bool { + induce_ntt_validated_shape(log_msg_cols, log_inv_rate, n_queries) + || induce_use_ntt_heuristic(log_msg_cols, log_inv_rate, n_queries) +} + +pub(crate) fn parse_induce_ntt_override( + value: Option<&std::ffi::OsStr>, + force_ntt_eligible: bool, +) -> Result, &'static str> { + match value { + None => Ok(None), + Some(value) if value == std::ffi::OsStr::new("0") => Ok(Some(false)), + Some(value) if value == std::ffi::OsStr::new("1") && force_ntt_eligible => Ok(Some(true)), + Some(value) if value == std::ffi::OsStr::new("1") => { + Err("forcing NTT is restricted to the validated shape family") + } + Some(_) => Err("expected the literal value 0 or 1"), + } +} + /// Dispatch between the dense [`induce_sumcheck_poly`] and the sparse /// [`induce_sumcheck_poly_via_ntt_base`] for L0 (base-field rows). Mirror of -/// `whir::induce_sumcheck_poly_auto`: in the recursive PCS this fires -/// only at the top level (large message domain, many queries); deeper levels -/// stay dense. Both paths produce identical output, so a mis-dispatch only -/// costs time. +/// `whir::induce_sumcheck_poly_auto`: in the recursive PCS this fires only at +/// the top level (large message domain, many queries); deeper levels stay +/// dense. Both paths produce identical output. The environment variable is a +/// fail-closed experiment replay hook, not the production policy. pub(crate) fn induce_sumcheck_poly_auto_base( log_msg_cols: usize, log_inv_rate: usize, @@ -498,18 +526,18 @@ pub(crate) fn induce_sumcheck_poly_auto_base( queries: &[usize], alpha: &[F192], ) -> (ArenaVec, F192) { - let heuristic = induce_use_ntt_heuristic(log_msg_cols, log_inv_rate, queries.len()); - let requested = std::env::var("LEANVM_PCS_L0_INDUCE_NTT").ok(); - let selected = match requested.as_deref() { - Some("1") => true, - Some("0") => false, - _ => heuristic, - }; + let n_queries = queries.len(); + let heuristic = induce_use_ntt_heuristic(log_msg_cols, log_inv_rate, n_queries); + let validated_shape = induce_ntt_validated_shape(log_msg_cols, log_inv_rate, n_queries); + let policy = induce_use_ntt_policy(log_msg_cols, log_inv_rate, n_queries); + let requested = std::env::var_os("LEANVM_PCS_L0_INDUCE_NTT"); + let override_value = parse_induce_ntt_override(requested.as_deref(), validated_shape) + .unwrap_or_else(|reason| panic!("invalid LEANVM_PCS_L0_INDUCE_NTT override: {reason}")); + let selected = override_value.unwrap_or(policy); if requested.is_some() { eprintln!( - "LEANVM_PCS_L0_INDUCE schema=1 requested={} heuristic={heuristic} selected={selected} log_msg_cols={log_msg_cols} log_inv_rate={log_inv_rate} queries={}", - requested.as_deref() == Some("1"), - queries.len() + "LEANVM_PCS_L0_INDUCE schema=2 override={} validated_shape={validated_shape} heuristic={heuristic} policy={policy} selected={selected} log_msg_cols={log_msg_cols} log_inv_rate={log_inv_rate} queries={n_queries}", + if override_value == Some(true) { "ntt" } else { "dense" }, ); } if selected { From a2c10248d2b38c4e1381687b7e193eca081f612c Mon Sep 17 00:00:00 2001 From: Adam Mohammed A Latif Date: Thu, 6 Aug 2026 20:24:03 +0000 Subject: [PATCH 14/22] test: cover L0 induce policy boundaries --- crates/pcs/src/whir.rs | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/crates/pcs/src/whir.rs b/crates/pcs/src/whir.rs index 1d3f2162..4a2741a9 100644 --- a/crates/pcs/src/whir.rs +++ b/crates/pcs/src/whir.rs @@ -2952,8 +2952,21 @@ mod tests { Ok(Some(true)) ); } - assert!(!induce_ntt_validated_shape(18, 2, 113)); - assert_eq!(induce_use_ntt_policy(18, 2, 113), induce_use_ntt_heuristic(18, 2, 113)); + // Every edge of the measured family is explicit: below/above the + // column range, a different inverse-rate, and a different query count. + for (log_msg_cols, log_inv_rate, n_queries) in [(18, 2, 113), (22, 2, 113), (19, 1, 113), (19, 2, 112)] { + assert!(!induce_ntt_validated_shape(log_msg_cols, log_inv_rate, n_queries)); + assert_eq!( + induce_use_ntt_policy(log_msg_cols, log_inv_rate, n_queries), + induce_use_ntt_heuristic(log_msg_cols, log_inv_rate, n_queries) + ); + } + + // Outside the measured family, the inherited heuristic still selects + // NTT when its crossover condition is met. + assert!(!induce_ntt_validated_shape(18, 2, 1_000)); + assert!(induce_use_ntt_heuristic(18, 2, 1_000)); + assert!(induce_use_ntt_policy(18, 2, 1_000)); assert_eq!(parse_induce_ntt_override(None, false), Ok(None)); assert_eq!( parse_induce_ntt_override(Some(std::ffi::OsStr::new("0")), false), From 3b1597076e603470ee95c04355b879df2c4da99f Mon Sep 17 00:00:00 2001 From: Adam Mohammed A Latif Date: Fri, 7 Aug 2026 05:44:20 +0000 Subject: [PATCH 15/22] docs: add aggregation research handoff --- RESEARCH_HANDOFF.md | 70 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 70 insertions(+) create mode 100644 RESEARCH_HANDOFF.md diff --git a/RESEARCH_HANDOFF.md b/RESEARCH_HANDOFF.md new file mode 100644 index 00000000..be5efa03 --- /dev/null +++ b/RESEARCH_HANDOFF.md @@ -0,0 +1,70 @@ +# Aggregation performance research handoff + +Date: 2026-08-07 + +## Purpose + +This branch preserves the exact measured seven-component research lineage and integrates upstream `main` at `e9cd16d49ef33909d9732778451ec73fbbedfd4a`. It is intended for technical review and current-source reproduction. It is not proposed as a merge-ready production patch. + +## Source identities + +| Role | Commit | +|---|---| +| Measured upstream freeze | `84fbd3ef49573537950f83c7ff66fd489476ca5d` | +| Six-component measured candidate | `b61a0ee64a9e5f41c368f937c56cdbb74fd3908b` | +| Seven-component measured candidate | `256928f9127c812749e40b08b4cf9744185c6b61` | +| Hardened L0 policy | `7be45deb92135c615dee0aaa4b294390b2de6902` | +| L0 boundary tests | `a2c10248d2b38c4e1381687b7e193eca081f612c` | +| Upstream integrated for this handoff | `e9cd16d49ef33909d9732778451ec73fbbedfd4a` | +| Integration merge | `ae08017b89fdc03bfa0af31d31b08bf3c11eaa9d` | + +The statistical performance campaigns bind to `256928f`, not to the integration merge. The integration merge establishes source compatibility and test acceptance only. It has not received a fresh full-system performance campaign. + +## Accepted stack + +1. Direct fold-6 for stacked opening. +2. Uninitialized GKR fold output with complete-write tests. +3. Uninitialized Bus leaf output with canonical-layout checks. +4. Quaternary Bus leaf capacity. +5. Quaternary retained GKR-layer capacity. +6. AVX-512 Bus MLE pure-extension folds on eligible x86-64 builds. +7. Narrow L0 induction dispatch to the existing exact transposed-NTT path for inverse-rate log 2, 113 queries and columns 19 through 21. + +The first six mechanisms retain literal replay selectors because the retained campaigns compared enabled and disabled modes in the same binary. The L0 policy is default-on only for its measured family, preserves the inherited heuristic elsewhere and retains a fail-closed force-dense replay hook. The branch also retains the measurement seam used to produce fixtures, durable proof artifacts and phase events. + +## Measured result + +The retained full-system campaigns ran on an AMD EPYC 9354 Zen 4 host with 15 workers, 85.4 GiB available memory, zero swap and `pclmulqdq`, AVX2, VPCLMULQDQ, AVX-512F and AVX-512VL. The canonical child workload was 8 hashes and 64,000 iterations per child, with outer inverse-rate log 2. + +| Comparison | Topology | Outer prove | Process wall | Peak physical memory | +|---|---:|---:|---:|---:| +| Six components versus all off | N2 | -30.91% | -20.72% | -22.98% | +| Six components versus all off | N8 | -31.87% | -26.85% | -32.44% | +| L0 NTT versus dense on the six-component stack | N2 | -7.07% | -3.51% | -2.48% | +| L0 NTT versus dense on the six-component stack | N8 | -6.51% | -4.46% | -3.27% | + +The incremental L0 induction span fell 78.02% at N2 and 74.10% at N8. After all seven components, the N2 median phase cluster was Bus 0.687050 s, PCS opening 0.527055 s, constraints 0.518037 s and Flock reduction 0.336672 s. At N8, Bus led six of eight runs and PCS led two. The result moves the previously dominant PCS bottleneck; it does not establish that the complete aggregation system meets an agreed production budget. + +All 142 retained proofs were byte-identical within topology and passed the unchanged inspection path. The canonical artifacts were 229,588 bytes for N2, 240,292 bytes for N4 and 258,204 bytes for N8. + +## Current-source validation + +On the integration merge, the following passed on an Apple M4 Pro: + +- `cargo testall`: 293 passed, 0 failed and 9 ignored, including doctests. +- `cargo test --release --workspace --all-features`: 293 passed, 0 failed and 9 ignored, including doctests. +- `cargo clippyall`. +- `cargo fmt --all -- --check`. +- `cargo docall`. + +The AVX-512 component is not selected on this Apple host. Its system measurements and x86 exactness coverage belong to the sealed Zen 4 campaign. + +## Evidence boundary + +The evidence pack contains raw run order, command and environment records, 25 ms process-memory samples, host samples, phase events, serialized proofs, inspection logs, fixtures, source bundles and campaign checksum manifests. Its root manifest names 2,137 files and has SHA-256 `b6ae60e665294629bfc9dc599ed44472cf38fef4b487553f9aba5464b13dcd71`. The pack is retained outside this source branch and can be transferred separately. + +Before drawing a current-main performance conclusion, rerun the canonical N2 campaign on this integration branch or a later descendant. Upstream commits after the measured freeze changed the recursion guest, native recursion code and Python verifier, so the old medians must not be relabeled as measurements of the integrated head. + +## Fast-upstream procedure + +Fetch `origin/main` immediately before review. If `git rev-list --count HEAD..origin/main` is nonzero, inspect the changed files first, merge the exact new head into this branch and rerun the validation commands. Do not rewrite commits `256928f`, `7be45de` or `a2c1024`, because the retained evidence and source bundles identify those exact objects. From 0e36615968ab3b7efeebe8ec2b6996dfa44f5219 Mon Sep 17 00:00:00 2001 From: Adam Mohammed A Latif Date: Fri, 7 Aug 2026 06:14:38 +0000 Subject: [PATCH 16/22] experiment: derive one constraints sumcheck node --- crates/lean_vm/src/constraints.rs | 203 ++++++++++++++++++++++++++++-- 1 file changed, 191 insertions(+), 12 deletions(-) diff --git a/crates/lean_vm/src/constraints.rs b/crates/lean_vm/src/constraints.rs index 64880778..20eee25a 100644 --- a/crates/lean_vm/src/constraints.rs +++ b/crates/lean_vm/src/constraints.rs @@ -92,7 +92,7 @@ pub fn eta_offsets(n_constraints: impl Iterator) -> Vec { /// time. Nothing is lifted into `E`, so a `K` round evaluates the identity and the /// bus forms in 64-bit arithmetic, and its scratch is a third the size. #[inline(always)] -fn table_message + Sync>( +fn table_message_all_nodes + Sync>( cols: &[C], eval: &(dyn Fn(&[F192], &[T]) -> F192 + Sync), pows: &[F192], @@ -133,6 +133,66 @@ fn table_message + Sync>( [acc[0].reduce(), acc[1].reduce(), acc[2].reduce()] } +/// Evaluate one Boolean node and `g`. The other Boolean node is recovered from +/// the running sumcheck claim, so this removes one full pass over every active +/// table while preserving the four transmitted round values exactly. +#[inline(always)] +fn table_message_with_derived_boolean + Sync>( + cols: &[C], + eval: &(dyn Fn(&[F192], &[T]) -> F192 + Sync), + pows: &[F192], + half: usize, + eqr: &[F192], + derive_zero: bool, +) -> [F192; 2] { + let ncols = cols.len(); + let summand = |i: usize, scratch: &mut [T]| -> [F192Unreduced; 2] { + let e = eqr[i]; + let (vb, vg) = scratch.split_at_mut(ncols); + for (ci, c) in cols.iter().enumerate() { + let (lo, hi) = (c[i], c[i + half]); + vb[ci] = if derive_zero { hi } else { lo }; + vg[ci] = T::at_g(lo, hi); + } + [e.mul_unreduced(eval(pows, vb)), e.mul_unreduced(eval(pows, vg))] + }; + let acc = if half >= PAR_THRESHOLD { + parallel::map_reduce_with_state( + half, + || vec![T::ZERO; 2 * ncols], + || [F192Unreduced::ZERO; 2], + |scratch, acc, i| { + let value = summand(i, scratch); + acc[0] ^= value[0]; + acc[1] ^= value[1]; + }, + |mut left, right| { + left[0] ^= right[0]; + left[1] ^= right[1]; + left + }, + ) + } else { + let mut scratch = vec![T::ZERO; 2 * ncols]; + (0..half).fold([F192Unreduced::ZERO; 2], |mut acc, i| { + let value = summand(i, &mut scratch); + acc[0] ^= value[0]; + acc[1] ^= value[1]; + acc + }) + }; + [acc[0].reduce(), acc[1].reduce()] +} + +fn node_skip_mode(value: Option<&std::ffi::OsStr>) -> Result { + match value { + None => Ok(false), + Some(value) if value == std::ffi::OsStr::new("0") => Ok(false), + Some(value) if value == std::ffi::OsStr::new("1") => Ok(true), + Some(_) => Err("expected the literal value 0 or 1"), + } +} + /// Prove that every table's batched constraint vanishes on all of its rows, as ONE /// sumcheck over `max τ_t` variables. `cols[t]` holds table `t`'s involved columns /// (`2^{τ_t}` values each, folded in place). Returns the per-table claims, in input @@ -144,6 +204,24 @@ pub fn prove( zeta: &[F192], sigma: &[F192], ps: &mut ProverState, +) -> Vec { + let requested = std::env::var_os("LEANVM_CONSTRAINT_NODE_SKIP"); + let enabled = node_skip_mode(requested.as_deref()) + .unwrap_or_else(|reason| panic!("invalid LEANVM_CONSTRAINT_NODE_SKIP override: {reason}")); + if requested.is_some() { + eprintln!("LEANVM_CONSTRAINT_NODE_SKIP schema=1 enabled={enabled}"); + } + prove_with_node_skip(airs, cols, eta, zeta, sigma, ps, enabled) +} + +fn prove_with_node_skip( + airs: &[Air<'_>], + cols: &[Vec<&[F64]>], + eta: F192, + zeta: &[F192], + sigma: &[F192], + ps: &mut ProverState, + node_skip: bool, ) -> Vec { let n = airs.iter().map(|a| a.tau).max().unwrap_or(0); debug_assert!(zeta.len() >= n, "the eq point must cover the tallest table"); @@ -162,6 +240,7 @@ pub fn prove( let mut folded: Vec>>> = (0..airs.len()).map(|_| None).collect(); // `k`, the challenges drawn so far, common to every air that is still waiting. let mut k = F192::ONE; + let mut claim = sigma.iter().copied().fold(F192::ZERO, |acc, value| acc + value); for j in 0..n { let m = n - 1 - j; // the variable this round binds // The waiting airs contribute the line `Y·k·Σσ`, whose slope `u` is all there @@ -173,18 +252,51 @@ pub fn prove( .filter(|(a, _)| a.tau <= m) .fold(F192::ZERO, |acc, (_, &s)| acc + s); let u = k * waiting; - let mut msg = [F192::ZERO; 3]; - for (t, air) in airs.iter().enumerate() { - if air.tau > m { - let w = &pows[offsets[t]..offsets[t] + air.n_constraints]; - let p = if let Some(table) = &folded[t] { - table_message(table, &*air.eval, w, 1 << m, &eqr) - } else { - table_message(&cols[t], &*air.eval_k, w, 1 << m, &eqr) - }; - msg = add3(msg, p.map(|x| weights[t] * x)); + let msg = if node_skip { + // Normally recover p(0). If ζ_m = 1, its eq coefficient at zero + // vanishes, so recover p(1) instead. One Boolean endpoint and g are + // therefore sufficient for every field value without a fallback pass. + let derive_zero = zeta[m] != F192::ONE; + let mut sent = [F192::ZERO; 2]; + for (t, air) in airs.iter().enumerate() { + if air.tau > m { + let w = &pows[offsets[t]..offsets[t] + air.n_constraints]; + let p = if let Some(table) = &folded[t] { + table_message_with_derived_boolean(table, &*air.eval, w, 1 << m, &eqr, derive_zero) + } else { + table_message_with_derived_boolean(&cols[t], &*air.eval_k, w, 1 << m, &eqr, derive_zero) + }; + sent[0] += weights[t] * p[0]; + sent[1] += weights[t] * p[1]; + } } - } + if derive_zero { + let p1 = sent[0]; + let h1 = zeta[m] * p1 + u; + let p0 = (claim + h1) * (F192::ONE + zeta[m]).inv(); + [p0, p1, sent[1]] + } else { + debug_assert_eq!(zeta[m], F192::ONE); + let p0 = sent[0]; + let h0 = (F192::ONE + zeta[m]) * p0; + let p1 = claim + h0 + u; + [p0, p1, sent[1]] + } + } else { + let mut msg = [F192::ZERO; 3]; + for (t, air) in airs.iter().enumerate() { + if air.tau > m { + let w = &pows[offsets[t]..offsets[t] + air.n_constraints]; + let p = if let Some(table) = &folded[t] { + table_message_all_nodes(table, &*air.eval, w, 1 << m, &eqr) + } else { + table_message_all_nodes(&cols[t], &*air.eval_k, w, 1 << m, &eqr) + }; + msg = add3(msg, p.map(|x| weights[t] * x)); + } + } + msg + }; shrink_eq_high(&mut eqr); // Assemble `h` and send it whole. The cofactor `p` is degree 2, so its value // at the fourth node is an interpolation of three scalars, NOT another pass @@ -194,9 +306,11 @@ pub fn prove( debug_assert_eq!(q[..3], nd[..], "the cubic's first three nodes are the cofactor's"); let p4 = [msg[0], msg[1], msg[2], lagrange_eval(&nd, &msg, q[3])]; let h: [F192; 4] = std::array::from_fn(|i| (F192::ONE + zeta[m] + q[i]) * p4[i] + q[i] * u); + debug_assert_eq!(h[0] + h[1], claim); // A separate pass: the challenge only exists once the message is bound. ps.add_scalars(&h); let rk = ps.sample(); + claim = lagrange_eval(&q, &h, rk); rho[m] = rk; k *= rk; let eq_k = F192::ONE + zeta[m] + rk; @@ -434,6 +548,71 @@ mod tests { } } + fn attached_proof_with_mode( + taus: &[usize], + cols: &[Vec>], + eta: F192, + zeta: &[F192], + node_skip: bool, + ) -> (Proof, Vec, Vec) { + let airs = airs_for(taus, true); + let pows = powers(eta, 3 * taus.len()); + let sigmas: Vec = taus + .iter() + .enumerate() + .map(|(t, &tau)| pows[3 * t + 2] * primitives::multilinear::mle_eval(&cols[t][1], &zeta[..tau])) + .collect(); + let views: Vec> = cols + .iter() + .map(|table| table.iter().map(|col| &col[..]).collect()) + .collect(); + let mut ps = ProverState::new(b"zc-node-skip-exactness", &SEED); + let claims = prove_with_node_skip(&airs, &views, eta, zeta, &sigmas, &mut ps, node_skip); + (ps.into_proof(), claims, sigmas) + } + + #[test] + fn claim_derived_node_skip_preserves_the_transcript() { + let taus = [5usize, 3, 5, 0, 1]; + let cols: Vec>> = taus + .iter() + .enumerate() + .map(|(i, &tau)| good_table(tau, i as u64)) + .collect(); + let (eta, ordinary_zeta) = eta_zeta(&taus); + let mut exceptional_zeta = ordinary_zeta.clone(); + exceptional_zeta[0] = F192::ONE; + exceptional_zeta[3] = F192::ONE; + + for zeta in [&ordinary_zeta, &exceptional_zeta] { + let (all_nodes, all_claims, sigmas) = attached_proof_with_mode(&taus, &cols, eta, zeta, false); + let (node_skip, skip_claims, skip_sigmas) = attached_proof_with_mode(&taus, &cols, eta, zeta, true); + + assert_eq!(sigmas, skip_sigmas); + assert_eq!(all_nodes.stream, node_skip.stream); + assert!(all_nodes.openings.is_empty()); + assert!(node_skip.openings.is_empty()); + assert_eq!(all_claims, skip_claims); + + let airs = airs_for(&taus, true); + let target = sigmas.iter().copied().fold(F192::ZERO, |acc, value| acc + value); + let mut vs = VerifierState::new(b"zc-node-skip-exactness", &node_skip, &SEED); + assert_eq!(verify(&airs, eta, zeta, target, &mut vs), Ok(skip_claims)); + } + } + + #[test] + fn node_skip_override_parser_fails_closed() { + use std::ffi::OsStr; + + assert_eq!(node_skip_mode(None), Ok(false)); + assert_eq!(node_skip_mode(Some(OsStr::new("0"))), Ok(false)); + assert_eq!(node_skip_mode(Some(OsStr::new("1"))), Ok(true)); + assert!(node_skip_mode(Some(OsStr::new("true"))).is_err()); + assert!(node_skip_mode(Some(OsStr::new("2"))).is_err()); + assert!(node_skip_mode(Some(OsStr::new(""))).is_err()); + } + /// Tampering any transmitted word breaks the chain: the batch is one sumcheck, /// so there is no per-table slack. #[test] From 79c9523747b70b5e87c41337d585e21f767f9aae Mon Sep 17 00:00:00 2001 From: Adam Mohammed A Latif Date: Fri, 7 Aug 2026 06:14:38 +0000 Subject: [PATCH 17/22] experiment: parallelize packed Flock serialization --- crates/flock/src/blake3.rs | 241 ++++++++++++++++++++++++++++++++++++- 1 file changed, 237 insertions(+), 4 deletions(-) diff --git a/crates/flock/src/blake3.rs b/crates/flock/src/blake3.rs index ed647daf..0e4efe2c 100644 --- a/crates/flock/src/blake3.rs +++ b/crates/flock/src/blake3.rs @@ -1239,6 +1239,60 @@ fn packed_128_bytes(words: &[F192]) -> Vec { out } +#[inline(always)] +fn write_packed_128(out: &mut [std::mem::MaybeUninit], word: F192) { + debug_assert_eq!(out.len(), 16); + debug_assert_eq!(word.c2, 0, "packed Flock witness escaped 128-bit subspace"); + for (slot, byte) in out[..8].iter_mut().zip(word.c0.to_le_bytes()) { + slot.write(byte); + } + for (slot, byte) in out[8..].iter_mut().zip(word.c1.to_le_bytes()) { + slot.write(byte); + } +} + +/// Serialize the three live packed witnesses in one parallel dispatch. Each +/// task owns one 16-byte output chunk in every destination, so no task can race +/// another and all bytes are initialized before the boxes are exposed as `u8`. +fn packed_128_bytes3_parallel(a: &[F192], b: &[F192], c: &[F192]) -> (Vec, Vec, Vec) { + assert_eq!(a.len(), b.len(), "packed A and B lengths differ"); + assert_eq!(a.len(), c.len(), "packed A and C lengths differ"); + let byte_len = a.len().checked_mul(16).expect("packed byte length overflow"); + let mut a_out = Box::<[u8]>::new_uninit_slice(byte_len); + let mut b_out = Box::<[u8]>::new_uninit_slice(byte_len); + let mut c_out = Box::<[u8]>::new_uninit_slice(byte_len); + let a_chunks = parallel::Chunks::new(&mut a_out, 16); + let b_chunks = parallel::Chunks::new(&mut b_out, 16); + let c_chunks = parallel::Chunks::new(&mut c_out, 16); + parallel::for_each(a.len(), |i| { + // SAFETY: `for_each` calls this body exactly once per `i`; equal-width + // chunks are disjoint and remain live until the blocking dispatch ends. + unsafe { + write_packed_128(a_chunks.get(i), a[i]); + write_packed_128(b_chunks.get(i), b[i]); + write_packed_128(c_chunks.get(i), c[i]); + } + }); + // SAFETY: the dispatch above initialized all 16 bytes of every chunk in all + // three boxes and returned only after every task completed. + unsafe { + ( + a_out.assume_init().into_vec(), + b_out.assume_init().into_vec(), + c_out.assume_init().into_vec(), + ) + } +} + +fn packed_128_parallel_mode(value: Option<&std::ffi::OsStr>) -> Result { + match value { + None => Ok(false), + Some(value) if value == std::ffi::OsStr::new("0") => Ok(false), + Some(value) if value == std::ffi::OsStr::new("1") => Ok(true), + Some(_) => Err("expected the literal value 0 or 1"), + } +} + // --------------------------------------------------------------------------- // Convenience API: Blake3Setup // --------------------------------------------------------------------------- @@ -1469,6 +1523,150 @@ mod tests { } } + #[test] + fn parallel_packed_128_copy_is_byte_exact() { + for &len in &[0usize, 1, 2, 7, 8, 31, 257, 4096] { + let words = |salt: u64| { + (0..len) + .map(|i| { + let i = i as u64; + F192::new( + i.wrapping_mul(0x9e37_79b9_7f4a_7c15).wrapping_add(salt), + i.rotate_left(17) ^ salt.wrapping_mul(0xd6e8_feb8_6659_fd93), + 0, + ) + }) + .collect::>() + }; + let (a, b, c) = (words(1), words(2), words(3)); + let expected = (packed_128_bytes(&a), packed_128_bytes(&b), packed_128_bytes(&c)); + assert_eq!(packed_128_bytes3_parallel(&a, &b, &c), expected, "length {len}"); + } + } + + #[test] + fn packed_128_parallel_override_parser_fails_closed() { + use std::ffi::OsStr; + + assert_eq!(packed_128_parallel_mode(None), Ok(false)); + assert_eq!(packed_128_parallel_mode(Some(OsStr::new("0"))), Ok(false)); + assert_eq!(packed_128_parallel_mode(Some(OsStr::new("1"))), Ok(true)); + assert!(packed_128_parallel_mode(Some(OsStr::new("true"))).is_err()); + assert!(packed_128_parallel_mode(Some(OsStr::new("2"))).is_err()); + assert!(packed_128_parallel_mode(Some(OsStr::new(""))).is_err()); + } + + #[test] + fn parallel_packed_128_copy_preserves_the_reduction_transcript() { + let setup = Blake3Setup::new(1); + let block = pinned_compression(std::array::from_fn(|i| 0x9e37_79b9u32.wrapping_mul(i as u32 + 1))); + let (z, a, b, z_lincheck) = generate_witness_with_ab_packed_and_lincheck(&[block], setup.n_blocks_log()); + + let prove = |use_parallel| { + let mut ps = fiat_shamir::transcript::ProverState::<()>::new(b"packed-128-copy-exactness", &[]); + setup.prove_reduction_precomputed_with_parallel(&z, &a, &b, &z_lincheck, &mut ps, use_parallel); + ps.into_proof() + }; + let serial = prove(false); + let parallel = prove(true); + assert_eq!(serial.stream, parallel.stream); + assert!(serial.openings.is_empty()); + assert!(parallel.openings.is_empty()); + + let mut vs = fiat_shamir::transcript::VerifierState::<()>::new(b"packed-128-copy-exactness", ¶llel, &[]); + setup + .verify_reduction(&mut vs) + .expect("parallel-copy reduction verifies"); + vs.finish().expect("parallel-copy proof is fully consumed"); + } + + #[test] + #[ignore = "manual production-shaped component benchmark"] + fn packed_128_copy_component_benchmark() { + parallel::init(); + let log_words: usize = std::env::var("FLOCK_PACKED_128_BENCH_LOG_WORDS") + .ok() + .map(|value| { + value + .parse() + .expect("FLOCK_PACKED_128_BENCH_LOG_WORDS must be an integer") + }) + .unwrap_or(22); + assert!((10..=25).contains(&log_words), "benchmark log-words must be in 10..=25"); + let len = 1usize << log_words; + let words = |salt: u64| { + (0..len) + .map(|i| { + let i = i as u64; + F192::new( + i.wrapping_mul(0x9e37_79b9_7f4a_7c15).wrapping_add(salt), + i.rotate_left(17) ^ salt.wrapping_mul(0xd6e8_feb8_6659_fd93), + 0, + ) + }) + .collect::>() + }; + let (a, b, c) = (words(1), words(2), words(3)); + let run = |use_parallel: bool| { + let start = std::time::Instant::now(); + let out = if use_parallel { + packed_128_bytes3_parallel(&a, &b, &c) + } else { + (packed_128_bytes(&a), packed_128_bytes(&b), packed_128_bytes(&c)) + }; + let elapsed_ms = start.elapsed().as_secs_f64() * 1e3; + let fingerprint = out.0[0] + ^ out.0[out.0.len() - 1] + ^ out.1[0] + ^ out.1[out.1.len() - 1] + ^ out.2[0] + ^ out.2[out.2.len() - 1]; + std::hint::black_box((out, fingerprint)); + (elapsed_ms, fingerprint) + }; + + let serial_warm = run(false); + let parallel_warm = run(true); + assert_eq!(serial_warm.1, parallel_warm.1); + println!( + "packed-copy warmup log_words={log_words} serial_ms={:.3} parallel_ms={:.3}", + serial_warm.0, parallel_warm.0 + ); + + let mut serial = Vec::new(); + let mut parallel = Vec::new(); + for block in 0..12 { + let modes = if block % 2 == 0 { + [false, true, true, false] + } else { + [true, false, false, true] + }; + for (position, use_parallel) in modes.into_iter().enumerate() { + let (elapsed_ms, fingerprint) = run(use_parallel); + assert_eq!(fingerprint, serial_warm.1); + if use_parallel { + parallel.push(elapsed_ms); + } else { + serial.push(elapsed_ms); + } + println!( + "packed-copy observation block={block} position={position} mode={} elapsed_ms={elapsed_ms:.3} fingerprint={fingerprint}", + if use_parallel { "parallel" } else { "serial" } + ); + } + } + serial.sort_by(f64::total_cmp); + parallel.sort_by(f64::total_cmp); + let median = |values: &[f64]| (values[values.len() / 2 - 1] + values[values.len() / 2]) / 2.0; + let serial_median = median(&serial); + let parallel_median = median(¶llel); + println!( + "packed-copy result observations_per_mode={} serial_median_ms={serial_median:.3} parallel_median_ms={parallel_median:.3} speedup={:.3}", + serial.len(), + serial_median / parallel_median + ); + } + #[test] fn setup_sizes_correctly() { for &(n_blocks, expected_n_log) in &[(1usize, 3), (8, 3), (9, 4), (16, 4), (17, 5), (1000, 10)] { @@ -1637,6 +1835,31 @@ impl Blake3Setup { b_packed_words: &[F192], z_packed_lincheck: &[u8], ps: &mut fiat_shamir::transcript::ProverState, + ) -> PackedWitnessClaims { + let requested = std::env::var_os("FLOCK_PACKED_128_PARALLEL"); + let use_parallel = packed_128_parallel_mode(requested.as_deref()) + .unwrap_or_else(|reason| panic!("invalid FLOCK_PACKED_128_PARALLEL override: {reason}")); + if requested.is_some() { + eprintln!("FLOCK_PACKED_128_PARALLEL schema=1 enabled={use_parallel}"); + } + self.prove_reduction_precomputed_with_parallel( + z_packed, + a_packed_words, + b_packed_words, + z_packed_lincheck, + ps, + use_parallel, + ) + } + + fn prove_reduction_precomputed_with_parallel( + &self, + z_packed: &[F192], + a_packed_words: &[F192], + b_packed_words: &[F192], + z_packed_lincheck: &[u8], + ps: &mut fiat_shamir::transcript::ProverState, + use_parallel: bool, ) -> PackedWitnessClaims { let trace = std::env::var_os("FLOCK_PROVE_TRACE").is_some(); let t_reduction = std::time::Instant::now(); @@ -1659,10 +1882,19 @@ impl Blake3Setup { useful_bits_per_block: self.r1cs.useful_bits, }; let t_zerocheck = std::time::Instant::now(); + let packed_copy_time; let (zc_claim, s_hat_v_c) = { - let a_packed = packed_128_bytes(a_packed_words); - let b_packed = packed_128_bytes(b_packed_words); - let c_packed = packed_128_bytes(z_packed); + let t_packed_copy = std::time::Instant::now(); + let (a_packed, b_packed, c_packed) = if use_parallel { + packed_128_bytes3_parallel(a_packed_words, b_packed_words, z_packed) + } else { + ( + packed_128_bytes(a_packed_words), + packed_128_bytes(b_packed_words), + packed_128_bytes(z_packed), + ) + }; + packed_copy_time = t_packed_copy.elapsed(); crate::zerocheck::prove_packed_padded_capture_s_hat_v_c( &a_packed, &b_packed, @@ -1729,9 +1961,10 @@ impl Blake3Setup { let reduction_time = t_reduction.elapsed(); let glue_time = reduction_time.saturating_sub(zerocheck_time + lincheck_time); eprintln!( - "[flock prove] reduction: {:.2} ms (zerocheck: {:.2} ms, lincheck: {:.2} ms, glue: {:.2} ms)", + "[flock prove] reduction: {:.2} ms (zerocheck: {:.2} ms, packed copy: {:.2} ms, lincheck: {:.2} ms, glue: {:.2} ms)", reduction_time.as_secs_f64() * 1e3, zerocheck_time.as_secs_f64() * 1e3, + packed_copy_time.as_secs_f64() * 1e3, lincheck_time.as_secs_f64() * 1e3, glue_time.as_secs_f64() * 1e3, ); From a5477b369ee44ef7aea91b0799f7b920b349632f Mon Sep 17 00:00:00 2001 From: Adam Mohammed A Latif Date: Fri, 7 Aug 2026 06:40:25 +0000 Subject: [PATCH 18/22] experiment: separate packed copy timing --- crates/flock/src/blake3.rs | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/crates/flock/src/blake3.rs b/crates/flock/src/blake3.rs index 0e4efe2c..cedab435 100644 --- a/crates/flock/src/blake3.rs +++ b/crates/flock/src/blake3.rs @@ -1881,8 +1881,8 @@ impl Blake3Setup { k_log: self.r1cs.k_log, useful_bits_per_block: self.r1cs.useful_bits, }; - let t_zerocheck = std::time::Instant::now(); let packed_copy_time; + let zerocheck_time; let (zc_claim, s_hat_v_c) = { let t_packed_copy = std::time::Instant::now(); let (a_packed, b_packed, c_packed) = if use_parallel { @@ -1895,16 +1895,18 @@ impl Blake3Setup { ) }; packed_copy_time = t_packed_copy.elapsed(); - crate::zerocheck::prove_packed_padded_capture_s_hat_v_c( + let t_zerocheck = std::time::Instant::now(); + let claim = crate::zerocheck::prove_packed_padded_capture_s_hat_v_c( &a_packed, &b_packed, &c_packed, self.r1cs.m, &padding, ps, - ) + ); + zerocheck_time = t_zerocheck.elapsed(); + claim }; - let zerocheck_time = t_zerocheck.elapsed(); let inner_rest_len = self.r1cs.k_log - self.r1cs.k_skip; let x_ab = crate::lincheck::QuirkyPoint { @@ -1959,7 +1961,8 @@ impl Blake3Setup { }; if trace { let reduction_time = t_reduction.elapsed(); - let glue_time = reduction_time.saturating_sub(zerocheck_time + lincheck_time); + let accounted_time = packed_copy_time + zerocheck_time + lincheck_time; + let glue_time = reduction_time.saturating_sub(accounted_time); eprintln!( "[flock prove] reduction: {:.2} ms (zerocheck: {:.2} ms, packed copy: {:.2} ms, lincheck: {:.2} ms, glue: {:.2} ms)", reduction_time.as_secs_f64() * 1e3, From 067268f76dc06dcd9317ee7243eedd1a5f4cc26d Mon Sep 17 00:00:00 2001 From: Adam Mohammed A Latif Date: Fri, 7 Aug 2026 07:31:37 +0000 Subject: [PATCH 19/22] docs: record current-source kernel pair result --- RESEARCH_HANDOFF.md | 33 +++++++++++++++++++++++++++++++-- 1 file changed, 31 insertions(+), 2 deletions(-) diff --git a/RESEARCH_HANDOFF.md b/RESEARCH_HANDOFF.md index be5efa03..4346ce6d 100644 --- a/RESEARCH_HANDOFF.md +++ b/RESEARCH_HANDOFF.md @@ -17,8 +17,9 @@ This branch preserves the exact measured seven-component research lineage and in | L0 boundary tests | `a2c10248d2b38c4e1381687b7e193eca081f612c` | | Upstream integrated for this handoff | `e9cd16d49ef33909d9732778451ec73fbbedfd4a` | | Integration merge | `ae08017b89fdc03bfa0af31d31b08bf3c11eaa9d` | +| Current-source two-kernel measured candidate | `a5477b369ee44ef7aea91b0799f7b920b349632f` | -The statistical performance campaigns bind to `256928f`, not to the integration merge. The integration merge establishes source compatibility and test acceptance only. It has not received a fresh full-system performance campaign. +The earlier seven-component statistical campaigns bind to `256928f`, not to the integration merge. The integration merge initially established source compatibility and test acceptance only. The separate current-source campaign described below binds to descendant `a5477b3` and measures only the two additional kernels. ## Accepted stack @@ -63,7 +64,35 @@ The AVX-512 component is not selected on this Apple host. Its system measurement The evidence pack contains raw run order, command and environment records, 25 ms process-memory samples, host samples, phase events, serialized proofs, inspection logs, fixtures, source bundles and campaign checksum manifests. Its root manifest names 2,137 files and has SHA-256 `b6ae60e665294629bfc9dc599ed44472cf38fef4b487553f9aba5464b13dcd71`. The pack is retained outside this source branch and can be transferred separately. -Before drawing a current-main performance conclusion, rerun the canonical N2 campaign on this integration branch or a later descendant. Upstream commits after the measured freeze changed the recursion guest, native recursion code and Python verifier, so the old medians must not be relabeled as measurements of the integrated head. +Before relabeling the earlier seven-component medians as a current-main result, rerun that complete comparison on this integration branch or a later descendant. Upstream commits after the old measured freeze changed the recursion guest, native recursion code and Python verifier. The two-kernel campaign below does not retroactively transfer the old seven-component percentages to the integrated head. + +## Current-source two-kernel result + +Commit `a5477b369ee44ef7aea91b0799f7b920b349632f` adds two replayable, default-off experiments on top of the integrated stack: + +1. `LEANVM_CONSTRAINT_NODE_SKIP=1` evaluates one Boolean endpoint and the third interpolation node for each constraints sumcheck message. It derives the omitted endpoint from the running claim, with a separate exact branch for `zeta == 1` where the usual denominator vanishes. +2. `FLOCK_PACKED_128_PARALLEL=1` serializes the three live packed Flock witnesses in one parallel dispatch over disjoint, completely initialized output chunks. The legacy serial route remains the default. + +Both overrides accept only literal `0` or `1` and fail closed otherwise. Unit tests establish byte-identical transcript streams, unchanged claims and acceptance by the unchanged verifier. The packed-copy tests cover empty, boundary and non-power-of-two lengths as well as the complete reduction transcript. + +The canonical N2 campaign used one AMD EPYC 9354 NUMA domain, CPUs 8 through 15, and the same binary for a repeated Williams-square 2-by-2 factorial design. It retained four pilots and 32 measured fresh processes. All 36 proofs were 230,804 bytes, had SHA-256 `c05561327b52c3a11466511dc4ccde942d89086f4541b13eb9d27ae1cf0d3e79`, and passed the unchanged proof-inspection command. + +| Factorial effect | Paired-block median | Favorable blocks | +|---|---:|---:| +| Node skip on `Prove constraints` | -62.897 ms | 8 / 8 | +| Parallel serialization on packed copy | -118.250 ms | 8 / 8 | +| Parallel serialization on Flock reduction | -124.799 ms | 8 / 8 | +| Combined versus control on outer prove | -189.041 ms | 8 / 8 | +| Combined versus control on process wall | -175.106 ms | 8 / 8 | +| Combined versus control on peak physical memory | -3.781 MB | 5 / 8 | + +Relative to the control-arm medians, the paired combined effect is approximately -6.31% of outer-prove time and -3.02% of process wall time. The median peak footprint is effectively unchanged. Cgroup CPU throttling, swap, memory fail counts and full-memory PSI did not increase during the campaign. + +The preregistered mechanism gates passed, but a deliberately stronger system-materiality rule required an outer-prove delta of at least -350 ms. The observed -189 ms therefore establishes a repeatable system improvement on this host without satisfying that larger-win target. It does not establish that aggregation as a whole meets a production budget. + +A separate 24-observation-per-arm component sweep on the same eight cores found that the packed path crosses over between 2^12 and 2^14 words: it is slower at 2^10 and 2^12, 1.226 times faster at 2^14, and 2.073 to 3.351 times faster from 2^16 through 2^22. Any automatic production policy should therefore retain a size threshold rather than enabling the parallel dispatch for every shape. + +The complete single-NUMA campaign checksum manifest has SHA-256 `d7f9bedf61556cd6b0d17f052d70d4e791dfb77047bca45e054ac47228d3f03a`. An independent validator rehashed all 548 entries and reconstructed every metric and factorial effect from raw run records. On the same exact commit, Linux release validation passed 293 tests with 0 failures and 10 ignored tests, plus Clippy, formatting and documentation. ## Fast-upstream procedure From c02f3012ce4eb9f8cbc585ae3a5084e374ded739 Mon Sep 17 00:00:00 2001 From: Adam Mohammed A Latif Date: Fri, 7 Aug 2026 07:34:37 +0000 Subject: [PATCH 20/22] docs: clarify node skip mechanism --- crates/lean_vm/src/constraints.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/crates/lean_vm/src/constraints.rs b/crates/lean_vm/src/constraints.rs index 20eee25a..8a3a9c45 100644 --- a/crates/lean_vm/src/constraints.rs +++ b/crates/lean_vm/src/constraints.rs @@ -134,8 +134,8 @@ fn table_message_all_nodes + Sync>( } /// Evaluate one Boolean node and `g`. The other Boolean node is recovered from -/// the running sumcheck claim, so this removes one full pass over every active -/// table while preserving the four transmitted round values exactly. +/// the running sumcheck claim, so this removes one constraint evaluation at +/// every active row while preserving the four transmitted round values exactly. #[inline(always)] fn table_message_with_derived_boolean + Sync>( cols: &[C], From c4b8348fdd473d7896942373d212879608e5e989 Mon Sep 17 00:00:00 2001 From: Adam Mohammed A Latif Date: Fri, 7 Aug 2026 08:22:06 +0000 Subject: [PATCH 21/22] test: harden two-kernel exactness boundaries --- crates/flock/src/blake3.rs | 21 ++++++++++++++++----- crates/lean_vm/src/constraints.rs | 6 +++++- 2 files changed, 21 insertions(+), 6 deletions(-) diff --git a/crates/flock/src/blake3.rs b/crates/flock/src/blake3.rs index cedab435..a8c62852 100644 --- a/crates/flock/src/blake3.rs +++ b/crates/flock/src/blake3.rs @@ -1240,8 +1240,7 @@ fn packed_128_bytes(words: &[F192]) -> Vec { } #[inline(always)] -fn write_packed_128(out: &mut [std::mem::MaybeUninit], word: F192) { - debug_assert_eq!(out.len(), 16); +fn write_packed_128(out: &mut [std::mem::MaybeUninit; 16], word: F192) { debug_assert_eq!(word.c2, 0, "packed Flock witness escaped 128-bit subspace"); for (slot, byte) in out[..8].iter_mut().zip(word.c0.to_le_bytes()) { slot.write(byte); @@ -1268,9 +1267,21 @@ fn packed_128_bytes3_parallel(a: &[F192], b: &[F192], c: &[F192]) -> (Vec, V // SAFETY: `for_each` calls this body exactly once per `i`; equal-width // chunks are disjoint and remain live until the blocking dispatch ends. unsafe { - write_packed_128(a_chunks.get(i), a[i]); - write_packed_128(b_chunks.get(i), b[i]); - write_packed_128(c_chunks.get(i), c[i]); + let a_chunk: &mut [std::mem::MaybeUninit; 16] = a_chunks + .get(i) + .try_into() + .expect("parallel packed A chunk must contain exactly 16 bytes"); + let b_chunk: &mut [std::mem::MaybeUninit; 16] = b_chunks + .get(i) + .try_into() + .expect("parallel packed B chunk must contain exactly 16 bytes"); + let c_chunk: &mut [std::mem::MaybeUninit; 16] = c_chunks + .get(i) + .try_into() + .expect("parallel packed C chunk must contain exactly 16 bytes"); + write_packed_128(a_chunk, a[i]); + write_packed_128(b_chunk, b[i]); + write_packed_128(c_chunk, c[i]); } }); // SAFETY: the dispatch above initialized all 16 bytes of every chunk in all diff --git a/crates/lean_vm/src/constraints.rs b/crates/lean_vm/src/constraints.rs index 8a3a9c45..d8d041e3 100644 --- a/crates/lean_vm/src/constraints.rs +++ b/crates/lean_vm/src/constraints.rs @@ -573,7 +573,10 @@ mod tests { #[test] fn claim_derived_node_skip_preserves_the_transcript() { - let taus = [5usize, 3, 5, 0, 1]; + // `tau = 12` makes the first round's half-table exactly + // `PAR_THRESHOLD`, exercising the two-node reducer's parallel branch. + let taus = [12usize, 3, 5, 0, 1]; + assert!((1usize << (taus[0] - 1)) >= PAR_THRESHOLD); let cols: Vec>> = taus .iter() .enumerate() @@ -583,6 +586,7 @@ mod tests { let mut exceptional_zeta = ordinary_zeta.clone(); exceptional_zeta[0] = F192::ONE; exceptional_zeta[3] = F192::ONE; + exceptional_zeta[11] = F192::ONE; for zeta in [&ordinary_zeta, &exceptional_zeta] { let (all_nodes, all_claims, sigmas) = attached_proof_with_mode(&taus, &cols, eta, zeta, false); From e8e873f47f4f03743f1e1bbc95e26026063016e8 Mon Sep 17 00:00:00 2001 From: Adam Mohammed A Latif Date: Fri, 7 Aug 2026 08:22:07 +0000 Subject: [PATCH 22/22] docs: correct two-kernel evidence boundary --- RESEARCH_HANDOFF.md | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/RESEARCH_HANDOFF.md b/RESEARCH_HANDOFF.md index 4346ce6d..2ad1fd0d 100644 --- a/RESEARCH_HANDOFF.md +++ b/RESEARCH_HANDOFF.md @@ -19,7 +19,7 @@ This branch preserves the exact measured seven-component research lineage and in | Integration merge | `ae08017b89fdc03bfa0af31d31b08bf3c11eaa9d` | | Current-source two-kernel measured candidate | `a5477b369ee44ef7aea91b0799f7b920b349632f` | -The earlier seven-component statistical campaigns bind to `256928f`, not to the integration merge. The integration merge initially established source compatibility and test acceptance only. The separate current-source campaign described below binds to descendant `a5477b3` and measures only the two additional kernels. +The earlier six-component all-off/on campaign binds to `b61a0ee`; the incremental L0/seven-component campaign binds to `256928f`. Neither binds to the integration merge. The integration merge initially established source compatibility and test acceptance only. The separate current-source campaign described below binds to descendant `a5477b3` and measures only the two additional kernels. ## Accepted stack @@ -50,7 +50,7 @@ All 142 retained proofs were byte-identical within topology and passed the uncha ## Current-source validation -On the integration merge, the following passed on an Apple M4 Pro: +The following passed locally on an Apple M4 Pro, but those local logs are not part of the sealed evidence pack: - `cargo testall`: 293 passed, 0 failed and 9 ignored, including doctests. - `cargo test --release --workspace --all-features`: 293 passed, 0 failed and 9 ignored, including doctests. @@ -58,7 +58,7 @@ On the integration merge, the following passed on an Apple M4 Pro: - `cargo fmt --all -- --check`. - `cargo docall`. -The AVX-512 component is not selected on this Apple host. Its system measurements and x86 exactness coverage belong to the sealed Zen 4 campaign. +The AVX-512 component is not selected on this Apple host. The sealed regression receipt is the Linux run on exact measured commit `a5477b3`: `cargo testall` passed 293 tests with 0 failures and 10 ignored tests, including doctests; Clippy, formatting and documentation also passed. GitHub reported no CI checks for PR #5 when this disclosure was prepared. ## Evidence boundary @@ -73,7 +73,7 @@ Commit `a5477b369ee44ef7aea91b0799f7b920b349632f` adds two replayable, default-o 1. `LEANVM_CONSTRAINT_NODE_SKIP=1` evaluates one Boolean endpoint and the third interpolation node for each constraints sumcheck message. It derives the omitted endpoint from the running claim, with a separate exact branch for `zeta == 1` where the usual denominator vanishes. 2. `FLOCK_PACKED_128_PARALLEL=1` serializes the three live packed Flock witnesses in one parallel dispatch over disjoint, completely initialized output chunks. The legacy serial route remains the default. -Both overrides accept only literal `0` or `1` and fail closed otherwise. Unit tests establish byte-identical transcript streams, unchanged claims and acceptance by the unchanged verifier. The packed-copy tests cover empty, boundary and non-power-of-two lengths as well as the complete reduction transcript. +Both overrides accept only literal `0` or `1` and fail closed otherwise. Unit tests establish byte-identical transcript streams, unchanged claims and acceptance by the unchanged verifier. The constraints test covers the parallel two-node reducer at `tau = 12`, including the exceptional `zeta == 1` recovery branch. The packed-copy tests cover empty, boundary and non-power-of-two lengths as well as the complete reduction transcript, and the helper's complete-write contract is enforced by a `[MaybeUninit; 16]` parameter rather than a debug-only length assertion. The canonical N2 campaign used one AMD EPYC 9354 NUMA domain, CPUs 8 through 15, and the same binary for a repeated Williams-square 2-by-2 factorial design. It retained four pilots and 32 measured fresh processes. All 36 proofs were 230,804 bytes, had SHA-256 `c05561327b52c3a11466511dc4ccde942d89086f4541b13eb9d27ae1cf0d3e79`, and passed the unchanged proof-inspection command. @@ -88,7 +88,13 @@ The canonical N2 campaign used one AMD EPYC 9354 NUMA domain, CPUs 8 through 15, Relative to the control-arm medians, the paired combined effect is approximately -6.31% of outer-prove time and -3.02% of process wall time. The median peak footprint is effectively unchanged. Cgroup CPU throttling, swap, memory fail counts and full-memory PSI did not increase during the campaign. -The preregistered mechanism gates passed, but a deliberately stronger system-materiality rule required an outer-prove delta of at least -350 ms. The observed -189 ms therefore establishes a repeatable system improvement on this host without satisfying that larger-win target. It does not establish that aggregation as a whole meets a production budget. +The decision rules were not prospectively preregistered. They were authored at 07:25:04 UTC after 16 measured processes had completed and the seventeenth was active, then copied to the host at 07:25:19 after 18 of 32 measured processes had completed. The exposed console observation contained admission lines rather than outcomes, but non-observation of already-written result files is not independently provable. Treat the record as a timestamped mid-campaign analysis decision, not a prospective preregistration. + +Under that record, the mechanism and direction gates passed, while the deliberately stronger system-materiality rule required an outer-prove delta of at least -350 ms and failed at -189.041 ms. The direct mechanism measurements are exact and repeatedly favorable. The -189 ms outer and -175 ms wall effects are descriptive paired system measurements, not a confirmatory end-to-end acceptance claim, and they do not establish that aggregation meets a production budget. + +Selection of the single-NUMA campaign was also data-driven after the valid split-NUMA `_02` campaign. In `_02`, packed copy and Flock were favorable in 8/8 blocks, constraints in 6/8, and combined outer and wall effects in only 4/8. Effective CPU service was 2.136–2.885 cores and pooled wall/service correlation was -0.773. The single-NUMA `_04` repeat narrowed service to 3.280–3.442 cores; its pooled correlation was still -0.593, while within-arm correlations were much weaker (-0.278, +0.193, -0.348 and +0.253). Campaigns `_01` and `_03` failed before retaining a proof because of, respectively, a non-native binary and a non-login `PATH` without `rustc`. + +The node skip removed one of three per-row constraint evaluations and reduced the constraints phase by 13.59%. If the three evaluations have approximately equal cost, that implies about 40.8% of the phase is evaluation arithmetic and about 59.2% is traversal/materialization. This is a calibration inference rather than direct instrumentation; it points the next constraints work toward traversal fusion rather than more node algebra. A separate 24-observation-per-arm component sweep on the same eight cores found that the packed path crosses over between 2^12 and 2^14 words: it is slower at 2^10 and 2^12, 1.226 times faster at 2^14, and 2.073 to 3.351 times faster from 2^16 through 2^22. Any automatic production policy should therefore retain a size threshold rather than enabling the parallel dispatch for every shape.