From 0623f2ec7a59697bcce3f2f63151ad1c844632ec Mon Sep 17 00:00:00 2001 From: MauroFab Date: Tue, 8 Sep 2026 14:36:51 -0300 Subject: [PATCH 01/17] feat(lfm): publish the block-binding schema from the epoch wrap MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit An aggregation node over epoch wraps sees exactly two things about a child: its `program_id`, an emit-time constant of the parent, and its PUBLISHED WORDS. The per-table wrap published neither the register boundary vectors, nor the epoch label, nor the public-output bytes, nor the L2G re-commit root — so the cross-wrap bindings an aggregator must CHECK (register fini->init across every seam, the label pinned to a chain position, the L2G root equality against the global proof) were not weak, they were unbuildable. In the batched format these four were the CARVED schema, published by the carve rather than by the program. The carve went with the format. Publishing costs no soundness: each value is already bound elsewhere. The register vectors derive the REGISTER preprocessed commitment Phase A absorbs, the label and the output halves are absorbed by `absorb_epoch_statement`, and the L2G root is a Phase A absorb. The L2G bookend's position (the epoch's last sub-proof) is asserted rather than assumed: publishing another sub-proof's root would bind an aggregator's L2G compare to an unrelated table and still look like a passing gate. `schema_words` names the run's width so a reader walks past it by name. `the_assembled_epoch_verifier_runs` uses it: with a literal, that gate would start checking `beta of table 0` against a register slot the next time the schema moves, and would report a pass while doing it. --- prover/src/lfm/epoch_tests.rs | 63 ++++++++++++++++++++++++++++ prover/src/lfm/epoch_verify_tests.rs | 10 ++++- 2 files changed, 72 insertions(+), 1 deletion(-) diff --git a/prover/src/lfm/epoch_tests.rs b/prover/src/lfm/epoch_tests.rs index 678ed51f7..93a684fb9 100644 --- a/prover/src/lfm/epoch_tests.rs +++ b/prover/src/lfm/epoch_tests.rs @@ -1760,6 +1760,51 @@ fn epoch_program_with(e: &RealEpoch, with_legs: bool, split_decode: bool) -> Lfm b.public(id[1]); } + // ---- ★ THE BLOCK-BINDING SCHEMA, published right after the attestation id + // + // An aggregation node over these wraps sees exactly two things about a child: + // its `program_id`, which is an emit-time CONSTANT of the parent, and its + // PUBLISHED WORDS. Everything below is arena data that the epoch statement or + // Phase A already bound, and every one of them is material a node must CHECK + // rather than trust — so without these publishes the cross-wrap bindings are + // not weak, they are unbuildable. + // + // In the batched format these were the CARVED schema, published by the carve + // rather than by the program. The carve went with the format, so the program + // publishes them. + // + // Publishing costs no soundness, because each is already bound: the register + // vectors through the REGISTER preprocessed commitment DERIVED from them + // (`PrepSource::Register`), the label and the output halves through + // `absorb_epoch_statement`, and the L2G root through Phase A's absorb. + // + // ⚠ This order IS [`SchemaLayout`]'s, which the aggregator indexes by. A + // field inserted in the middle silently re-binds every field below it, so + // append here and extend `SchemaLayout` in the same commit. + for cell in reg_init.iter().chain(®_fini) { + b.public(cell.as_cell()); + } + for half in epoch_label { + b.public(half.as_cell()); + } + for half in public_output { + b.public(half.as_cell()); + } + // ★ The L2G bookend is the LAST sub-proof — `EpochSession::pairs` proves the + // VM tables and then pushes `l2g_air`, and the from-proof reconstruction + // rebuilds the AIR list the same way. Asserted rather than assumed: publishing + // some other sub-proof's root would bind the aggregator's L2G compare to a + // table with nothing to do with the global memory argument, and would still + // look like a passing gate. + assert_eq!( + e.tables[n - 1].shape.index, + n - 1, + "the L2G bookend is the epoch's last sub-proof" + ); + for half in main_cells[n - 1].lanes_flat() { + b.public(half.as_cell()); + } + // ---- one fork per table ---- let mut contributions: Vec = Vec::new(); for (i, h) in e.tables.iter().enumerate() { @@ -1892,6 +1937,24 @@ pub(super) fn num_epoch_wide_arenas(e: &RealEpoch) -> usize { 6 + usize::from(!e.page_commitments.is_empty()) } +/// How many words [`epoch_program`] publishes for the BLOCK-BINDING SCHEMA — the +/// run that sits between the attestation id and the first sub-proof's block. +/// +/// Exposed rather than recomputed at each reader for the reason +/// [`num_epoch_wide_arenas`] is: a gate that walks the published words by index +/// starts checking the WRONG field when this changes, and reports a pass. The +/// aggregator's `SchemaLayout` indexes the same run and must agree with this +/// number field for field. +/// +/// The order is the emitter's: register INIT, register FINI, the two epoch-label +/// halves, the public-output halves, then the L2G re-commit root's lanes. +pub(super) fn schema_words(e: &RealEpoch) -> usize { + 2 * crate::tables::register::NUM_REGISTER_ADDRESSES + + 2 + + e.statement.public_output_len.div_ceil(4) + + super::proof_arena::lanes_per_root() +} + /// The arenas [`epoch_program`] declares, in the same order. pub(super) fn epoch_arena_words(e: &RealEpoch, with_legs: bool) -> Vec> { let mut stmt: Vec = Vec::new(); diff --git a/prover/src/lfm/epoch_verify_tests.rs b/prover/src/lfm/epoch_verify_tests.rs index d56326ad2..65542a057 100644 --- a/prover/src/lfm/epoch_verify_tests.rs +++ b/prover/src/lfm/epoch_verify_tests.rs @@ -377,7 +377,15 @@ fn the_assembled_epoch_verifier_runs() { // rests on. Its value is differentialled in the spine test; here it only has to // be skipped, and skipped by NAME rather than by a literal. let program_id_words = 2usize; - let mut cursor = 2 + program_id_words; + // ★ Then the BLOCK-BINDING SCHEMA — the register boundary vectors, the epoch + // label, the public-output halves and the L2G re-commit root. Skipped by NAME + // (`epoch_tests::schema_words`) rather than by a literal, for the same reason + // the id is: a literal here would start checking `beta of table 0` against a + // register slot the moment the schema moves, and would report a pass while + // doing it. Its VALUES are the aggregator's subject and are differentialled + // there; this gate only has to walk past them and still account for every word. + let schema_words = super::epoch_tests::schema_words(&e); + let mut cursor = 2 + program_id_words + schema_words; let mut checked = 2usize; for (i, (h, leg)) in e.tables.iter().zip(&e.legs).enumerate() { // The legs publish first: the recomputed composition, then a terminal From ef8654163ae7e72686afd206733cc3aa6304fe76 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Tue, 8 Sep 2026 14:38:52 -0300 Subject: [PATCH 02/17] feat(lfm): give the epoch wrap a publish profile MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A wrap's published words are the only thing an aggregation node can read about it, and a node pays per word: eight hinted halves, four canonicity guards, four recombinations, thirty-six bytes of statement absorb and one extension-field inverse in the LfmPublic balance — per word, per child. So what a wrap publishes is the size of the layer above it. At the production posture the wrap publishes 10,507 words; the binding set is around eighty. The other ~10,400 have no consumer above: `composition` is already asserted equal to the claimed Horner inside `emit_table_verification`, the DEEP invariants are documented as exposed for tests, and the beta/z/gamma/zeta/iota runs are challenges the machine derives for itself. They are this crate's differential surface against production's replay, not a binding — a node that hinted them would pay to re-read numbers it can recompute. `Publishes::Diagnostic` stays the default and every existing gate keeps exactly the words it had; `Publishes::Aggregation` is chosen per emission by the aggregator. Dropping the differential surface globally would trade the evidence that this machine derives production's challenges for the saving, so the lever is local. The new gate asserts the containment rather than assuming it: the binding head is identical cell for cell, the bus total still ends the list, and what was dropped is counted from the epoch's own shapes — so a diagnostic added later fails here naming the count instead of silently widening what every node above pays for. --- prover/src/lfm/epoch_tests.rs | 84 ++++++++++++++++---- prover/src/lfm/per_table_aggregator_tests.rs | 81 +++++++++++++++++++ 2 files changed, 149 insertions(+), 16 deletions(-) diff --git a/prover/src/lfm/epoch_tests.rs b/prover/src/lfm/epoch_tests.rs index 93a684fb9..e32b4f472 100644 --- a/prover/src/lfm/epoch_tests.rs +++ b/prover/src/lfm/epoch_tests.rs @@ -1492,7 +1492,48 @@ fn epoch_challenge_program(e: &RealEpoch) -> LfmProgram { /// arenas and emits no verification, so the spine test's own arena-word count is /// untouched. pub(super) fn epoch_program(e: &RealEpoch, with_legs: bool) -> LfmProgram { - epoch_program_with(e, with_legs, false) + epoch_program_with(e, with_legs, false, Publishes::Diagnostic) +} + +/// Which words [`epoch_program`] publishes. +/// +/// The wrap's published words are the ONLY thing an aggregation node can read +/// about it, and a node pays for every one of them: eight hinted halves, four +/// canonicity guards, four recombinations, thirty-six bytes of statement absorb +/// and one extension-field inverse in the `LfmPublic` balance — per word, per +/// child. So what a wrap publishes is the size of the layer above it. +/// +/// At the production posture the diagnostic set is 10,507 words, of which the +/// binding set is ≈80. The other ~10,400 have no consumer above: `composition` +/// is already asserted equal to the claimed Horner INSIDE +/// `epoch_verify::emit_table_verification`, the DEEP invariants are documented +/// as exposed for tests, and β/z/γ/ζ/ι are challenges the machine derives for +/// itself. They are an oracle for this crate's differentials, not a binding, and +/// a node that hinted them would be paying to re-read numbers it could recompute. +/// +/// ⚠ [`Publishes::Diagnostic`] is the DEFAULT and every existing gate keeps +/// exactly the words it had. Dropping the differential surface is a choice made +/// per emission by the aggregator, never a global one: the differentials against +/// production's own replay are how this machine is known to derive production's +/// challenges, and a preset that quietly removed them everywhere would trade the +/// evidence for the saving. +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +pub(super) enum Publishes { + /// The shared pair, the attestation id, the block-binding schema, then every + /// per-sub-proof diagnostic, then the bus total. + Diagnostic, + /// The shared pair, the attestation id, the block-binding schema and the bus + /// total — nothing per sub-proof. What a wrap feeding an aggregator emits. + Aggregation, +} + +/// [`epoch_program`] with the publish set named — the aggregation lever. +pub(super) fn epoch_program_publishing( + e: &RealEpoch, + with_legs: bool, + publishes: Publishes, +) -> LfmProgram { + epoch_program_with(e, with_legs, false, publishes) } /// The epoch program, optionally with the DECODE cell SPLIT — a deliberately @@ -1509,7 +1550,12 @@ pub(super) fn epoch_program(e: &RealEpoch, with_legs: bool) -> LfmProgram { /// [`the_assembled_verifier_declares_exactly_the_shape_words`] is what refuses it. /// /// The extra arena is declared LAST so no existing arena index moves. -fn epoch_program_with(e: &RealEpoch, with_legs: bool, split_decode: bool) -> LfmProgram { +fn epoch_program_with( + e: &RealEpoch, + with_legs: bool, + split_decode: bool, + publishes: Publishes, +) -> LfmProgram { use super::statement_replay::{EpochStatementVars, PhaseATable, absorb_epoch_statement}; let mut b = LfmBuilder::new().with_wrap_hash(super::edsl::WrapHash::production()); @@ -1876,20 +1922,26 @@ fn epoch_program_with(e: &RealEpoch, with_legs: bool, split_decode: bool) -> Lfm }, leg_arenas, ); - b.public(out.composition.as_cell()); - for v in &out.fri_terminal { - b.public(v.as_cell()); + if publishes == Publishes::Diagnostic { + b.public(out.composition.as_cell()); + for v in &out.fri_terminal { + b.public(v.as_cell()); + } } } - b.public(ch.beta.as_cell()); - b.public(ch.z.as_cell()); - b.public(ch.gamma.as_cell()); - for zeta in &ch.zetas { - b.public(zeta.as_cell()); - } - for bits in &ch.iota_bits { - let felt = edsl::bits_to_felt(&mut b, bits); - b.public(felt.as_cell()); + if publishes == Publishes::Diagnostic { + b.public(ch.beta.as_cell()); + b.public(ch.z.as_cell()); + b.public(ch.gamma.as_cell()); + for zeta in &ch.zetas { + b.public(zeta.as_cell()); + } + for bits in &ch.iota_bits { + // The recombination is emitted only to be published; under + // `Aggregation` it is dead work, so it goes with the publish. + let felt = edsl::bits_to_felt(&mut b, bits); + b.public(felt.as_cell()); + } } } @@ -2358,7 +2410,7 @@ fn the_assembled_verifier_declares_exactly_the_shape_words() { // Positive control on the guard itself: the split-cell control program DOES // declare a surplus word, and this is the comparison that sees it. - let split = epoch_program_with(&e, false, true); + let split = epoch_program_with(&e, false, true, Publishes::Diagnostic); let split_declared: usize = split.arena_schema.lens.iter().map(|l| *l as usize).sum(); assert_eq!( split_declared, @@ -2408,7 +2460,7 @@ fn a_split_decode_cell_forges_the_attestation() { ); // ---- (a) the SPLIT program: the forgery runs and publishes the forged id. - let split = epoch_program_with(&e, false, true); + let split = epoch_program_with(&e, false, true, Publishes::Diagnostic); let mut split_arenas = honest.clone(); split_arenas.push(super::proof_arena::commitments_to_arena(&[substituted])); let exec = execute(&split, &split_arenas, &crate::hash_pin::BLOCK_HASHER).expect( diff --git a/prover/src/lfm/per_table_aggregator_tests.rs b/prover/src/lfm/per_table_aggregator_tests.rs index b5af6b284..38c8f750e 100644 --- a/prover/src/lfm/per_table_aggregator_tests.rs +++ b/prover/src/lfm/per_table_aggregator_tests.rs @@ -462,3 +462,84 @@ fn the_global_verifier_leg_runs_and_rejects_tampers() { "a flipped L2G re-commit root must make the global leg unprovable" ); } + +/// ★ THE AGGREGATION PUBLISH PROFILE drops diagnostics and NOTHING else. +/// +/// # Why this gate exists +/// +/// A wrap's published words are the only thing an aggregation node can read +/// about it, and a node pays per word: eight hinted halves, four canonicity +/// guards, four recombinations, thirty-six bytes of statement absorb and one +/// extension-field inverse in the `LfmPublic` balance. At the production posture +/// the diagnostic set is 10,507 words against a binding set of ≈80, so the +/// profile is what decides whether a fan-in-2 leaf hints ~21,000 +/// canonicity-guarded words before it has verified anything. +/// +/// A saving of that size is worth exactly as much as the proof that it saves +/// only what has no consumer. So this asserts the containment directly: +/// `Aggregation`'s words are `Diagnostic`'s with the per-sub-proof runs cut out, +/// value for value — the shared pair, the attestation id and the block-binding +/// schema are identical cells, and the bus total still ends the list. +/// +/// The arithmetic is asserted alongside, from the epoch's own shapes, so a +/// diagnostic added to the per-sub-proof block in future fails here naming the +/// count rather than silently widening what every node above pays for. +#[test] +fn the_aggregation_publish_profile_drops_only_diagnostics() { + use super::epoch_tests::{Publishes, epoch_program_publishing, schema_words}; + + let e = super::epoch_tests::real_epoch(); + let arenas = super::epoch_tests::epoch_arena_words(&e, true); + + let run = |publishes| { + let program = epoch_program_publishing(&e, true, publishes); + let exec = execute(&program, &arenas, &crate::hash_pin::BLOCK_HASHER) + .expect("the assembled verifier must execute under either profile"); + (program.instrs.len(), exec.public_words) + }; + let (diag_instrs, diag) = run(Publishes::Diagnostic); + let (agg_instrs, agg) = run(Publishes::Aggregation); + + // ---- the head: the pair, the id and the schema, identical cells. + let head = 2 + 2 + schema_words(&e); + assert_eq!( + diag[..head], + agg[..head], + "the binding head must not move with the profile" + ); + // ---- the tail: the bus total, which both profiles still publish last. + assert_eq!( + diag[diag.len() - 1], + agg[agg.len() - 1], + "the closure's total ends the list under either profile" + ); + assert_eq!(agg.len(), head + 1, "Aggregation is the head and the total"); + + // ---- what was dropped, from the epoch's own shapes rather than from a + // literal: per sub-proof the composition, one terminal per query, the + // (beta, z, gamma) triple, the DEEP zetas and one index per query. + let dropped: usize = e + .tables + .iter() + .zip(&e.legs) + .map(|(h, leg)| { + 1 + leg.verify.num_queries + 3 + h.zetas.len() + h.shape.num_queries + }) + .sum(); + assert_eq!( + diag.len(), + agg.len() + dropped, + "Aggregation must drop exactly the per-sub-proof diagnostics" + ); + + println!( + "★ publish profile over {} sub-proofs: Diagnostic {} words / {diag_instrs} instrs, \\ + Aggregation {} words / {agg_instrs} instrs ({:.1}% of the words, {:.1}% of the \\ + instructions)", + e.tables.len(), + diag.len(), + agg.len(), + 100.0 * agg.len() as f64 / diag.len() as f64, + 100.0 * agg_instrs as f64 / diag_instrs as f64, + ); +} From 390a4e855a73da32e2798ad6843d73e65ef7424d Mon Sep 17 00:00:00 2001 From: MauroFab Date: Tue, 8 Sep 2026 14:39:08 -0300 Subject: [PATCH 03/17] style(lfm): cargo fmt the publish-profile gate --- prover/src/lfm/per_table_aggregator_tests.rs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/prover/src/lfm/per_table_aggregator_tests.rs b/prover/src/lfm/per_table_aggregator_tests.rs index 38c8f750e..5a4cf0534 100644 --- a/prover/src/lfm/per_table_aggregator_tests.rs +++ b/prover/src/lfm/per_table_aggregator_tests.rs @@ -522,9 +522,7 @@ fn the_aggregation_publish_profile_drops_only_diagnostics() { .tables .iter() .zip(&e.legs) - .map(|(h, leg)| { - 1 + leg.verify.num_queries + 3 + h.zetas.len() + h.shape.num_queries - }) + .map(|(h, leg)| 1 + leg.verify.num_queries + 3 + h.zetas.len() + h.shape.num_queries) .sum(); assert_eq!( diag.len(), From a9cf28d40e2ae63288bcb4af989b8d6784307601 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Tue, 8 Sep 2026 14:45:31 -0300 Subject: [PATCH 04/17] feat(lfm): the per-table aggregation leg and its binding legs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The emitted verifier of one child LFM proof, and the cross-child checks a tree of them needs. A leg is the machine twin of `verify_against_chunked`, which is four steps and no more: absorb the LFM statement, fork and replay Phase A for the shared LogUp pair, recompute the LfmPublic balance from the CLAIMED public words, and verify every sub-proof against it. So this reuses the spine the epoch wrap and the global-memory leg already gate — `emit_table_challenges`, `emit_table_verification`, `replay_phase_a`, `emit_bus_closure` — and adds only the LFM-shaped statement, the canonicity-guarded public-word hinting, the balance target and the bindings. There is no new cryptographic arithmetic here. ⚠ ONE TRANSCRIPT PER CHILD. Each child was produced against a transcript seeded by its own statement, so a node runs one replay per child: two Phase A's, two challenge pairs, two closures. A shared spine that re-indexed every sub-proof over the union of both children would be verifying one proof with 2n tables — a different statement, and not one either child ever made. `per_table_census_tests::tenant_node_program` is shaped that way on purpose, as a census instrument, and is not a template. `SchemaLayout` is the reader of the schema the wrap now publishes, and `assert_covers` pins it against the child's actual published count so a layout applied to the wrong level fails at assembly instead of mis-binding fifty asserts later. The L2G compare is a separate entry point rather than part of the chain bindings: in a tree the epoch wrap and the global proof are not generally in the same node, so it is emitted where both sides are in scope and nowhere else. --- prover/src/lfm/mod.rs | 1 + prover/src/lfm/per_table_aggregator.rs | 592 +++++++++++++++++++++++++ 2 files changed, 593 insertions(+) create mode 100644 prover/src/lfm/per_table_aggregator.rs diff --git a/prover/src/lfm/mod.rs b/prover/src/lfm/mod.rs index bf7f1e4ae..f6c5fd26f 100644 --- a/prover/src/lfm/mod.rs +++ b/prover/src/lfm/mod.rs @@ -41,6 +41,7 @@ pub mod keccak_host; pub mod layout; pub mod lde; pub mod logup; +pub mod per_table_aggregator; pub mod poseidon; pub mod programs; pub mod proof; diff --git a/prover/src/lfm/per_table_aggregator.rs b/prover/src/lfm/per_table_aggregator.rs new file mode 100644 index 000000000..5013ae849 --- /dev/null +++ b/prover/src/lfm/per_table_aggregator.rs @@ -0,0 +1,592 @@ +//! The aggregation NODE's building block: a per-table VERIFY LEG — the emitted +//! verifier of one child LFM proof — plus the cross-child binding legs. +//! +//! # What a leg is +//! +//! A leg is the machine twin of [`super::proof::verify_against_chunked`], which +//! is four steps and no more: absorb the LFM statement, fork the statement-bound +//! state and replay Phase A to recover the shared LogUp pair, recompute the +//! `LfmPublic` balance from the CLAIMED public words, and verify every +//! sub-proof against it. [`emit_leg`] emits exactly those four, so the leg and +//! the host verifier are two renderings of one contract rather than two +//! implementations of one idea. +//! +//! Nothing here is new cryptographic arithmetic. The spine is +//! [`super::epoch::emit_table_challenges`], the per-sub-proof verification is +//! [`super::epoch_verify::emit_table_verification`], Phase A is +//! [`super::statement_replay::replay_phase_a`] and the closure is +//! [`super::logup::emit_bus_closure`] — every one already gated by the epoch +//! wrap and by the global-memory leg. This module contributes the LFM-shaped +//! statement, the public-word hinting under a canonicity guard, the balance +//! target, and the binding legs. +//! +//! # Why a node is uniform +//! +//! A child is a plain per-table `MultiProof` whichever level produced it — a +//! wrap of an epoch, or another node. So one emitter serves every level, and a +//! node's statement is its children's published words and roots. What is NOT +//! uniform is the node's IDENTITY: a leg absorbs its child's `program_id` as an +//! emit-time CONSTANT, and `program_id` is derived from the compiled program, so +//! a program that verified its own shape would need its own id inside its own +//! instruction stream. That fixed point is why each level is a distinct program. +//! +//! # What the bindings are for +//! +//! Verifying two children says nothing about their relationship. The chain is a +//! CHECK on published words and never a trust: one shared attestation id across +//! every child, each child's register fini vector equal to the next child's init +//! vector, and each child's epoch label pinned to its chain position as an +//! emit-time constant. Those are [`emit_chain_bindings`], and they are the whole +//! reason a tree of these proves something a bag of them does not. + +use stark::config::Commitment; + +use crate::tables::types::{FE, FEE}; + +use super::builder::{Ext, Felt, LfmBuilder}; +use super::constraints::Analysis; +use super::epoch::{RootCells, TableAbsorbs, TableChallengeShape, fork_table}; +use super::epoch_verify::{TableQueryArenas, TableVerifyShape}; +use super::instr::ArenaId; +use super::statement::{LFM_MACHINE_VERSION, LFM_STATEMENT_TAG}; +use super::statement_replay::{PhaseAPreprocessed, PhaseATable, replay_phase_a}; +use super::transcript_replay::{Candidate, TranscriptReplay, assert_canonical, candidate_to_felt}; + +/// `u32` halves one lane's canonical `u64` occupies — the unit +/// [`super::statement::absorb_lfm_statement`] appends a lane in. +const HALVES_PER_LANE: usize = 2; + +/// Lanes one published word carries. +const LANES_PER_WORD: usize = super::word::WORD_LANES; + +// ======================= the child's shape, at emit time ================== + +/// One sub-proof of a child, as the leg needs it. +/// +/// Every field is program SHAPE — derived from the AIR and the proof options, +/// never read off the proof at verify time. The one exception is the trace +/// length inside `verify`, which the prover chooses and which is program shape +/// here for the reason the arena schema makes it one: the node is emitted for a +/// specific child shape, and a child whose trace length disagreed would not fill +/// the arenas the node declares. +pub struct ChildTable<'a> { + /// What the fork absorbs and what challenges come out of it. + pub challenge: &'a TableChallengeShape, + /// What the verification legs open. + pub verify: &'a TableVerifyShape, + /// The constraint program, captured from the AIR. + pub analysis: &'a Analysis, + /// The preprocessed-columns commitment, when the AIR is preprocessed. + /// + /// An AIR-SET constant at emit time, exactly as production takes it + /// (`air.precomputed_commitment()`, never the proof's copy). Interning it + /// here is what makes production's explicit proof-copy-equals-AIR-copy check + /// the ABSENCE of a second value in this machine rather than a comparison. + pub precomputed_root: Option<&'a Commitment>, +} + +/// One child proof, as the node's emitter needs it. +pub struct ChildShape<'a> { + /// The identity of the program that produced this child — a PROGRAM + /// CONSTANT of the node, which is what pins WHICH program the node accepts a + /// proof of. + pub program_id: &'a Commitment, + /// How many words the child publishes. Publish indices auto-increment from + /// zero (`LfmBuilder::public`), so the count is the whole layout. + pub num_public_words: usize, + /// The child's `ProofOptions::fri_final_poly_log_degree` — the statement's + /// last byte. + pub fri_final_poly_log_degree: u8, + /// The child's sub-proofs, in proof order. + pub tables: Vec>, +} + +// ==================== the emitted statement + publics ==================== + +/// One hinted public word of a child: the emit-time-constant index, the eight +/// hinted halves (absorbed by the statement), and the four lanes reassembled as +/// CANONICITY-GUARDED felts (consumed by the balance and the binding legs). +pub struct HintedPublicWord { + pub index: u32, + pub halves: Vec, + pub lanes: Vec, +} + +/// Hint a child's published words from `arena` (eight halves per word, the +/// serializer's layout) and reassemble each lane under the canonicity guard. +/// +/// The guard is the same `(lo, hi)` predicate the transcript replay's own +/// digest-to-felt path enforces, so a hinted half pair CANNOT alias a second +/// representation of the same felt while absorbing different bytes. Without it a +/// prover could absorb one byte string into the statement and hand the balance +/// and the binding legs a different value for the same word. +/// +/// ⚠ This is the node's per-word bill — eight hints, four guards, four +/// recombinations — and it is paid per word per child. What a child publishes is +/// therefore the size of the layer above it; see +/// `epoch_tests::Publishes`. +pub fn hint_public_words( + b: &mut LfmBuilder, + arena: ArenaId, + count: usize, +) -> Vec { + let mut cursor = 0u32; + (0..count) + .map(|index| { + let mut halves = Vec::with_capacity(LANES_PER_WORD * HALVES_PER_LANE); + let mut lanes = Vec::with_capacity(LANES_PER_WORD); + for _ in 0..LANES_PER_WORD { + let lo = b.hint_felt(arena, cursor); + let hi = b.hint_felt(arena, cursor + 1); + cursor += HALVES_PER_LANE as u32; + let c = Candidate { lo, hi }; + assert_canonical(b, c); + lanes.push(candidate_to_felt(b, c)); + halves.push(lo); + halves.push(hi); + } + HintedPublicWord { + index: index as u32, + halves, + lanes, + } + }) + .collect() +} + +/// Emits [`super::statement::absorb_lfm_statement`] byte for byte: the tag, the +/// child's program id (a PROGRAM CONSTANT), the machine version, the word count, +/// each word's emit-time-constant index and hinted lane halves, and the FRI +/// terminal byte. +pub fn emit_lfm_statement( + t: &mut TranscriptReplay, + program_id: &Commitment, + words: &[HintedPublicWord], + fri_final_poly_log_degree: u8, +) { + t.append_const_bytes(LFM_STATEMENT_TAG); + t.append_const_bytes(program_id); + t.append_const_bytes(&LFM_MACHINE_VERSION.to_le_bytes()); + t.append_const_bytes(&(words.len() as u64).to_le_bytes()); + for word in words { + t.append_const_bytes(&word.index.to_le_bytes()); + // ⚠ ONE CALL PER LANE, not one for the word. `absorb_lfm_statement` + // appends each lane's canonical `u64` separately, so a word is FIVE host + // calls — the index and four lanes — not two. A byte transcript + // concatenates and cannot tell the difference; an ALGEBRAIC one + // length-prefixes every call, so absorbing the eight halves in one go is + // a DIFFERENT transcript, and since the statement is absorbed first that + // means every challenge downstream. See `transcript_replay::Append`. + for lane in word.halves.chunks(HALVES_PER_LANE) { + t.append_halves_misaligned(lane); + } + } + t.append_const_bytes(&[fri_final_poly_log_degree]); +} + +/// The `LfmPublic` balance the leg's LogUp closure must reach — the machine twin +/// of `proof::expected_public_balance`: +/// `Σ_i 1/(z − (LfmPublic + index_i·α + Σ_l lane_l·α^{2+l}))`, with each division +/// by an interned one so a fingerprint collision with `z` is unprovable rather +/// than `0/0 = 1`. +pub fn emit_public_balance( + b: &mut LfmBuilder, + words: &[HintedPublicWord], + z: Ext, + alpha: Ext, +) -> Ext { + let bus = b.ext_const(&FEE::from(crate::tables::types::BusId::LfmPublic as u64)); + let one = b.ext_const(&FEE::one()); + // α¹..α⁵ — the index takes α, lane l takes α^{2+l}. + let mut powers = Vec::with_capacity(1 + LANES_PER_WORD); + powers.push(alpha); + for i in 1..=LANES_PER_WORD { + let next = b.emul(powers[i - 1], alpha); + powers.push(next); + } + let mut acc: Option = None; + for word in words { + let idx = b.felt_const(FE::from(word.index as u64)); + let idx_term = b.emul_base(powers[0], idx); + let mut linear = b.eadd(bus, idx_term); + for (l, lane) in word.lanes.iter().enumerate() { + let term = b.emul_base(powers[1 + l], *lane); + linear = b.eadd(linear, term); + } + let fingerprint = b.esub(z, linear); + let term = b.ediv(one, fingerprint); + acc = Some(match acc { + None => term, + Some(a) => b.eadd(a, term), + }); + } + acc.unwrap_or_else(|| b.ext_const(&FEE::zero())) +} + +// ============================== the verify leg ============================ + +/// The arenas one child's leg reads, in DECLARATION ORDER — which is absorb +/// order. The caller declares one set per child, in child order, before emitting +/// any leg, so the node's declaration order is its absorb order end to end. +pub struct LegArenas { + publics: ArenaId, + main_roots: ArenaId, + per_table: Vec, +} + +struct TableArenas { + aux_root: Option, + contribution: Option, + composition_root: ArenaId, + ood_current: ArenaId, + ood_next: ArenaId, + parts: ArenaId, + fri_roots: ArenaId, + fri_coeffs: ArenaId, + nonce: Option, + legs: TableQueryArenas, +} + +/// Declare one child's arenas. +pub fn declare_leg_arenas(b: &mut LfmBuilder, child: &ChildShape<'_>) -> LegArenas { + let per_root = RootCells::words_per_root(b); + let publics = + b.declare_arena((LANES_PER_WORD * HALVES_PER_LANE * child.num_public_words) as u32); + let main_roots = b.declare_arena(per_root * child.tables.len() as u32); + let per_table = child + .tables + .iter() + .map(|t| { + let c = t.challenge; + TableArenas { + aux_root: c.has_aux_root.then(|| b.declare_arena(per_root)), + contribution: c.has_contribution.then(|| b.declare_arena(1)), + composition_root: b.declare_arena(per_root), + ood_current: b + .declare_arena((c.ood_current_dims.0 * c.ood_current_dims.1) as u32), + ood_next: b.declare_arena((c.ood_next_dims.0 * c.ood_next_dims.1) as u32), + parts: b.declare_arena(c.num_parts as u32), + fri_roots: b.declare_arena(per_root * c.fri.num_committed() as u32), + fri_coeffs: b.declare_arena(c.fri.num_terminal_coeffs() as u32), + nonce: (c.grinding_factor > 0).then(|| b.declare_arena(1)), + legs: super::epoch_verify::declare_table_arenas(b, t.verify), + } + }) + .collect(); + LegArenas { + publics, + main_roots, + per_table, + } +} + +/// What a leg hands the node's binding layer. +pub struct LegCells { + /// The child's published words — index plus canonicity-guarded lanes. This + /// is the binding legs' entire input, and the only thing a node learns about + /// a child beyond "its proof verifies". + pub publics: Vec, + /// The child's own shared LogUp pair, exposed for the differential gates. + pub z_alpha: (Ext, Ext), +} + +/// Emit ONE child's complete verification. +/// +/// ⚠ ONE TRANSCRIPT PER CHILD. Each child proof was produced against a +/// transcript seeded by its OWN statement, so a node verifying two children runs +/// two independent replays: two Phase A's, two `(z, α)` pairs, two closures. A +/// shared spine that re-indexed every sub-proof over the union of both children +/// would be verifying one proof with `2n` tables — a different statement, and +/// not one either child ever made. (`per_table_census_tests::tenant_node_program` +/// is shaped that way ON PURPOSE, as a census instrument; it is not a template.) +pub fn emit_leg(b: &mut LfmBuilder, child: &ChildShape<'_>, a: &LegArenas) -> LegCells { + let n = child.tables.len(); + let per_root = RootCells::words_per_root(b); + + // ---- the statement, over the child's claimed published words ---- + let publics = hint_public_words(b, a.publics, child.num_public_words); + let mut t = TranscriptReplay::new(&[]); + emit_lfm_statement( + &mut t, + child.program_id, + &publics, + child.fri_final_poly_log_degree, + ); + + // ---- Phase A: preprocessed roots as AIR-set constants, main roots hinted. + let main_cells: Vec = (0..n) + .map(|i| RootCells::hint(b, a.main_roots, per_root * i as u32)) + .collect(); + // ⚠ The DIGEST's felts, not the root's bytes. `replay_phase_a` absorbs + // through `absorb_root_felts`, which declares the host's 32 bytes on both + // arms and packs the algebraic arm's four felts into the one digest cell they + // already are, so the root absorb CANCELS rather than paying a byte + // regrouping. `byte_halves` is for `program_id`, which is deliberately + // keccak-over-bytes. + let main_halves: Vec> = main_cells.iter().map(RootCells::lanes_flat).collect(); + let prep_cells: Vec> = child + .tables + .iter() + .map(|t| t.precomputed_root.map(|c| RootCells::constant(b, c))) + .collect(); + let phase_a: Vec = child + .tables + .iter() + .enumerate() + .map(|(i, t)| PhaseATable { + preprocessed_root: t.precomputed_root.map(PhaseAPreprocessed::Constant), + main_root: &main_halves[i][..], + }) + .collect(); + let (z, alpha) = replay_phase_a(&mut t, b, &phase_a); + + // ---- one fork per sub-proof, with the full verification legs ---- + let mut contributions: Vec = Vec::new(); + for (i, table) in child.tables.iter().enumerate() { + let c = table.challenge; + let arenas = &a.per_table[i]; + let aux = arenas.aux_root.map(|id| RootCells::hint(b, id, 0)); + let contribution = arenas.contribution.map(|id| b.hint_word(id, 0).as_ext()); + let composition = RootCells::hint(b, arenas.composition_root, 0); + let ood_current: Vec = (0..(c.ood_current_dims.0 * c.ood_current_dims.1) as u32) + .map(|k| b.hint_word(arenas.ood_current, k).as_ext()) + .collect(); + let ood_next: Vec = (0..(c.ood_next_dims.0 * c.ood_next_dims.1) as u32) + .map(|k| b.hint_word(arenas.ood_next, k).as_ext()) + .collect(); + let parts: Vec = (0..c.num_parts as u32) + .map(|k| b.hint_word(arenas.parts, k).as_ext()) + .collect(); + let fri_roots: Vec = (0..c.fri.num_committed()) + .map(|k| RootCells::hint(b, arenas.fri_roots, per_root * k as u32)) + .collect(); + let fri_coeffs: Vec = (0..c.fri.num_terminal_coeffs() as u32) + .map(|k| b.hint_word(arenas.fri_coeffs, k).as_ext()) + .collect(); + let nonce = arenas.nonce.map(|id| b.hint_felt(id, 0)); + if let Some(l) = contribution { + contributions.push(l); + } + + let mut fork = fork_table(&t, c.index, c.num_tables); + let absorbs = TableAbsorbs { + aux_root: aux.as_ref(), + contribution, + composition_root: &composition, + ood_current: &ood_current, + ood_next: &ood_next, + parts: &parts, + fri_roots: &fri_roots, + fri_coeffs: &fri_coeffs, + nonce, + }; + let ch = super::epoch::emit_table_challenges(b, &mut fork, c, &absorbs); + // ★ THE SEAM: `absorbs` is passed on by REFERENCE rather than rebuilt, + // so there is no second reading of the proof for a leg to disagree with + // the transcript about. + super::epoch_verify::emit_table_verification( + b, + table.verify, + table.analysis, + &ch, + &absorbs, + &super::epoch_verify::TableInputs { + precomputed_root: prep_cells[i].as_ref(), + main_root: &main_cells[i], + rap_challenges: &[z, alpha], + }, + &arenas.legs, + ); + } + + // ---- the closure, against the PUBLIC balance ---- + // + // Every other LFM bus balances to zero internally; `LfmPublic` is the one + // whose target is the claimed words, which is what makes this the binding + // between "the proof verifies" and "it published THESE words". + let target = emit_public_balance(b, &publics, z, alpha); + let shape = super::logup::LogUpShape { + num_contributing_tables: contributions.len(), + num_output_bytes: 0, + }; + super::logup::emit_bus_closure(b, &shape, &contributions, target); + + LegCells { + publics, + z_alpha: (z, alpha), + } +} + +// ============================ the binding legs ============================ + +/// Where each field of the block-binding schema sits in a child's published +/// words. +/// +/// The order is the emitter's, and it is one order: `epoch_tests::epoch_program` +/// publishes the pair, the attestation id, then this schema, and +/// `epoch_tests::schema_words` is the same arithmetic as [`Self::schema_words`]. +/// A node indexes by these accessors, so a field inserted on one side and not +/// the other re-binds every field below it — which is why +/// [`Self::assert_covers`] is called at assembly time rather than trusted. +pub struct SchemaLayout { + pub num_reg: usize, + pub out_halves: usize, + /// Lanes the L2G root occupies — four on an algebraic hash, eight on a byte + /// one. Read from `proof_arena::lanes_per_root` rather than spelled, because + /// a reader that spells `8` walks an algebraic schema at twice the stride and + /// lands on the wrong field instead of out of bounds. + pub root_lanes: usize, +} + +impl SchemaLayout { + /// The words published before the schema: the shared pair and the two + /// attestation-id words. + pub const HEAD: usize = 4; + + pub fn new(out_halves: usize) -> Self { + Self { + num_reg: crate::tables::register::NUM_REGISTER_ADDRESSES, + out_halves, + root_lanes: super::proof_arena::lanes_per_root(), + } + } + + pub fn schema_words(&self) -> usize { + 2 * self.num_reg + 2 + self.out_halves + self.root_lanes + } + + /// Total words a child publishes under `Publishes::Aggregation` — the head, + /// the schema and the closure's bus total. + pub fn total(&self) -> usize { + Self::HEAD + self.schema_words() + 1 + } + + /// Pin the layout against what the child actually publishes. + /// + /// A level confusion — a layout built for one child applied to another — is + /// a loud failure here rather than a silent mis-binding fifty asserts later. + pub fn assert_covers(&self, num_public_words: usize) { + assert_eq!( + self.total(), + num_public_words, + "the layout must cover the child's published words exactly \ + (num_reg={}, out_halves={}, root_lanes={})", + self.num_reg, + self.out_halves, + self.root_lanes, + ); + } + + pub fn id(&self, half: usize) -> usize { + 2 + half + } + pub fn reg_init(&self, r: usize) -> usize { + Self::HEAD + r + } + pub fn reg_fini(&self, r: usize) -> usize { + Self::HEAD + self.num_reg + r + } + pub fn label(&self, half: usize) -> usize { + Self::HEAD + 2 * self.num_reg + half + } + pub fn out_half(&self, i: usize) -> usize { + Self::HEAD + 2 * self.num_reg + 2 + i + } + pub fn l2g_lane(&self, lane: usize) -> usize { + Self::HEAD + 2 * self.num_reg + 2 + self.out_halves + lane + } +} + +/// Assert two hinted public words carry the same value, lane by lane. +pub fn assert_words_equal(b: &mut LfmBuilder, x: &HintedPublicWord, y: &HintedPublicWord) { + for (xl, yl) in x.lanes.iter().zip(&y.lanes) { + let xe = xl.as_ext(); + let ye = yl.as_ext(); + b.assert_eq_ext(xe, ye); + } +} + +/// Assert a hinted public word's base value equals a program constant — lanes +/// `1..4` must be zero, which is what a BASE publish looks like. +pub fn assert_word_is_const(b: &mut LfmBuilder, x: &HintedPublicWord, v: u64) { + let c = b.ext_const(&FEE::from(v)); + let x0 = x.lanes[0].as_ext(); + b.assert_eq_ext(x0, c); + let zero = b.ext_const(&FEE::zero()); + for lane in &x.lanes[1..] { + let le = lane.as_ext(); + b.assert_eq_ext(le, zero); + } +} + +/// The cross-child binding legs: one shared attestation id across every child, +/// each child's register fini vector equal to the next child's init vector, and +/// each child's epoch label pinned to its chain position as an emit-time +/// constant. +/// +/// These are CHECKS on published words, never trusts. Verifying two children +/// says nothing about their relationship; this is what makes a tree of proofs a +/// statement about one execution rather than about several. +pub fn emit_chain_bindings( + b: &mut LfmBuilder, + legs: &[LegCells], + layouts: &[SchemaLayout], + labels: &[u64], +) { + assert_eq!(legs.len(), layouts.len(), "one layout per child"); + assert_eq!(legs.len(), labels.len(), "one chain position per child"); + + // ---- one attestation id answers for every child. + for k in 1..legs.len() { + for half in 0..2 { + assert_words_equal( + b, + &legs[0].publics[layouts[0].id(half)], + &legs[k].publics[layouts[k].id(half)], + ); + } + } + // ---- the register chain, across every seam. + for k in 0..legs.len().saturating_sub(1) { + for r in 0..layouts[k].num_reg { + assert_words_equal( + b, + &legs[k].publics[layouts[k].reg_fini(r)], + &legs[k + 1].publics[layouts[k + 1].reg_init(r)], + ); + } + } + // ---- each label pinned to its position, as a constant of THIS program. + for (k, &label) in labels.iter().enumerate() { + assert_word_is_const( + b, + &legs[k].publics[layouts[k].label(0)], + label & 0xFFFF_FFFF, + ); + assert_word_is_const(b, &legs[k].publics[layouts[k].label(1)], label >> 32); + } +} + +/// Assert child `k`'s published L2G re-commit root equals the root the global +/// proof's verifier published for epoch `k`. +/// +/// The in-VM half of the root-equality binding. In a TREE the two sides are not +/// generally in the same node — the global wrap rides at the ROOT — so this is +/// emitted where both are in scope and nowhere else. +pub fn assert_l2g_roots_equal( + b: &mut LfmBuilder, + epoch: &LegCells, + epoch_layout: &SchemaLayout, + global: &LegCells, + global_first_root_word: usize, + epoch_index: usize, +) { + let lanes = epoch_layout.root_lanes; + for lane in 0..lanes { + assert_words_equal( + b, + &epoch.publics[epoch_layout.l2g_lane(lane)], + &global.publics[global_first_root_word + lanes * epoch_index + lane], + ); + } +} From 8fb3ba8abc4d9d9d73c640a98e2605f2a25a6d80 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Tue, 8 Sep 2026 14:47:42 -0300 Subject: [PATCH 05/17] test(lfm): the aggregation node's cost model, measured MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three emission-only measurements, in the order the per-table format makes correct rather than the order lane C's narrowing implies. C narrowed the fan-in question to the binding legs, and did so under the batched assumption that a child publishes ~285 words. The per-table diagnostic wrap publishes 10,507, and a leg pays LINEARLY per published word — eight hints, four canonicity guards, four recombinations, thirty-six bytes of statement absorb and one extension-field inverse. So the term that actually grew by 37x is the per-word one, and it is measured first. (a) is sampled at seven counts rather than fitted from two: the statement's sponge absorbs in rate-sized blocks, so the hash term is a step function whose average is linear, and a two-point fit would hide the step. The linearity is asserted with a tolerance that admits the step and nothing wider. (b) is the bindings as a with/without delta over the same hinted words, so what is left is the bindings alone. (c) needs no second emission. This leg is `tenant_node_program` plus the statement, the balance and the bindings; the balance is field arithmetic and hashes nothing, so in COMPRESSIONS the only term added to C's F is the statement's — which is (a)'s hash column. ⚠ C's F(1) = 2,886 and F(2) = 5,771 are COMPRESSIONS over a glue delta, not cells. The instrument prints all three units side by side so the two are not compared by accident. --- prover/src/lfm/per_table_aggregator.rs | 3 +- prover/src/lfm/per_table_aggregator_tests.rs | 182 +++++++++++++++++++ 2 files changed, 183 insertions(+), 2 deletions(-) diff --git a/prover/src/lfm/per_table_aggregator.rs b/prover/src/lfm/per_table_aggregator.rs index 5013ae849..3e7f1b2ac 100644 --- a/prover/src/lfm/per_table_aggregator.rs +++ b/prover/src/lfm/per_table_aggregator.rs @@ -262,8 +262,7 @@ pub fn declare_leg_arenas(b: &mut LfmBuilder, child: &ChildShape<'_>) -> LegAren aux_root: c.has_aux_root.then(|| b.declare_arena(per_root)), contribution: c.has_contribution.then(|| b.declare_arena(1)), composition_root: b.declare_arena(per_root), - ood_current: b - .declare_arena((c.ood_current_dims.0 * c.ood_current_dims.1) as u32), + ood_current: b.declare_arena((c.ood_current_dims.0 * c.ood_current_dims.1) as u32), ood_next: b.declare_arena((c.ood_next_dims.0 * c.ood_next_dims.1) as u32), parts: b.declare_arena(c.num_parts as u32), fri_roots: b.declare_arena(per_root * c.fri.num_committed() as u32), diff --git a/prover/src/lfm/per_table_aggregator_tests.rs b/prover/src/lfm/per_table_aggregator_tests.rs index 5a4cf0534..155777fe2 100644 --- a/prover/src/lfm/per_table_aggregator_tests.rs +++ b/prover/src/lfm/per_table_aggregator_tests.rs @@ -541,3 +541,185 @@ fn the_aggregation_publish_profile_drops_only_diagnostics() { 100.0 * agg_instrs as f64 / diag_instrs as f64, ); } + +// ===================== the node's cost instrument ========================= + +/// A root of zeroes, standing in for a child's `program_id` where only the +/// LENGTH of the constant matters — the statement absorbs 32 bytes whatever +/// they are. +const ZERO_ROOT: stark::config::Commitment = [0u8; 32]; + +/// The leg's per-published-word part, and NOTHING else: hint the words under +/// the canonicity guard, absorb them as the statement, squeeze the pair, and +/// recompute the `LfmPublic` balance. +/// +/// Phase A runs over ZERO tables, so the squeeze that forces the statement's +/// segment to pack and hash is present and the per-sub-proof verification is +/// not. Everything that is not a function of `count` is therefore a fixed +/// overhead common to every point below, and cancels in the marginals. +fn publics_only_program(count: usize) -> LfmProgram { + use super::per_table_aggregator::{emit_lfm_statement, emit_public_balance, hint_public_words}; + use super::statement_replay::replay_phase_a; + + let mut b = LfmBuilder::new().with_wrap_hash(super::edsl::WrapHash::production()); + let arena = b.declare_arena(8 * count as u32); + let words = hint_public_words(&mut b, arena, count); + let mut t = TranscriptReplay::new(&[]); + emit_lfm_statement(&mut t, &ZERO_ROOT, &words, 8); + let (z, alpha) = replay_phase_a(&mut t, &mut b, &[]); + let target = emit_public_balance(&mut b, &words, z, alpha); + b.public(target.as_cell()); + compile(b.finish()) +} + +/// The binding legs over `children` children, and nothing else — the words are +/// hinted (the leg would have hinted them anyway) and the delta against the +/// same program without the bindings is the bindings' whole cost. +fn bindings_only_program(children: usize, with_bindings: bool) -> (LfmProgram, usize) { + use super::per_table_aggregator::{ + LegCells, SchemaLayout, emit_chain_bindings, hint_public_words, + }; + use super::statement_replay::replay_phase_a; + + // A block-final epoch's output length; the schema's only variable term. + const OUT_HALVES: usize = 8; + let layout = SchemaLayout::new(OUT_HALVES); + let words = layout.total(); + + let mut b = LfmBuilder::new().with_wrap_hash(super::edsl::WrapHash::production()); + let mut legs = Vec::with_capacity(children); + for _ in 0..children { + let arena = b.declare_arena(8 * words as u32); + let publics = hint_public_words(&mut b, arena, words); + let mut t = TranscriptReplay::new(&[]); + t.append_const_bytes(&ZERO_ROOT[..]); + let (z, alpha) = replay_phase_a(&mut t, &mut b, &[]); + legs.push(LegCells { + publics, + z_alpha: (z, alpha), + }); + } + if with_bindings { + let layouts: Vec = (0..children) + .map(|_| SchemaLayout::new(OUT_HALVES)) + .collect(); + let labels: Vec = (0..children as u64).collect(); + emit_chain_bindings(&mut b, &legs, &layouts, &labels); + } + (compile(b.finish()), words) +} + +/// ★ THE NODE'S COST, in the three units that decide the fan-in. +/// +/// # What this measures and why in this order +/// +/// Lane C narrowed the fan-in question to the binding legs, and did so under the +/// BATCHED assumption that a child publishes ~285 words. Under the per-table +/// format the diagnostic wrap publishes 10,507, and the leg pays LINEARLY per +/// published word — eight hints, four canonicity guards, four recombinations, +/// thirty-six bytes of statement absorb and one extension-field inverse. So the +/// term that actually grew is the per-word one, and it is measured FIRST. +/// +/// The three quantities, all emission-only: +/// +/// (a) the per-published-word marginal, at several counts so LINEARITY is +/// checked rather than assumed — the statement's sponge absorbs in +/// rate-sized blocks, so the hash term is a step function whose average is +/// linear, and a two-point fit would hide that; +/// (b) the binding legs, as the delta between a node with and without them; +/// (c) F(1) and F(2), which follow from (a) rather than needing a second +/// emission: this leg is `per_table_census_tests::tenant_node_program` plus +/// the statement, the balance and the bindings. The balance is pure field +/// arithmetic and hashes NOTHING, so in COMPRESSIONS the only term this leg +/// adds to C's is the statement's — which is exactly (a)'s hash column. +/// +/// ⚠ C's F(1) = 2,886 / F(2) = 5,771 are COMPRESSIONS (`wrap_tests::hash_ops` +/// over a glue delta), not cells. Quoting them against a cell figure would be +/// comparing two different measurements that happen to be numbers. +#[test] +#[ignore = "emission instrument: run explicitly, prints the node cost model"] +fn the_node_cost_model_is_measured() { + use super::per_table_aggregator::SchemaLayout; + + let hash = super::edsl::WrapHash::production(); + let census = |p: &LfmProgram| -> (usize, usize, u64) { + let (main, aux) = + super::airs::lfm_cell_counts_with_hasher(p, crate::hash_pin::BLOCK_HASHER); + ( + p.instrs.len(), + super::wrap_tests::hash_ops(p, hash), + main + 3 * aux, + ) + }; + + // ---- (a) the per-published-word marginal. + const OUT_HALVES: usize = 8; + let aggregation_words = SchemaLayout::new(OUT_HALVES).total(); + // The measured diagnostic count at q=110, plus the schema this branch adds. + let diagnostic_words = 10_507 + SchemaLayout::new(OUT_HALVES).schema_words(); + let points = [0, 64, 128, 256, 512, aggregation_words, diagnostic_words]; + println!( + "\n★ (a) THE PER-PUBLISHED-WORD BILL, at {hash:?}\n \ + {:>8} {:>12} {:>12} {:>14} {:>10}", + "words", "instrs", "hash ops", "cells", "cells/word" + ); + let mut base = (0usize, 0usize, 0u64); + for (i, &count) in points.iter().enumerate() { + let (instrs, ops, cells) = census(&publics_only_program(count)); + if i == 0 { + base = (instrs, ops, cells); + } + let per_word = if count > 0 { + (cells - base.2) as f64 / count as f64 + } else { + 0.0 + }; + println!(" {count:>8} {instrs:>12} {ops:>12} {cells:>14} {per_word:>10.2}"); + } + // Linearity, asserted rather than eyeballed: the marginal between the two + // largest sampled points must agree with the marginal between the two + // smallest to within the sponge's rate-sized step. + let cells_at = |n: usize| census(&publics_only_program(n)).2; + let (c64, c512) = (cells_at(64), cells_at(512)); + let low = (c64 - base.2) as f64 / 64.0; + let high = (c512 - c64) as f64 / (512.0 - 64.0); + let drift = (high - low).abs() / low; + println!( + " marginal 0->64 {low:.2} cells/word, 64->512 {high:.2} cells/word \ + ({:+.1}%)", + 100.0 * (high - low) / low + ); + assert!( + drift < 0.25, + "the per-word bill must be linear to within the sponge's step, got \ + {low:.2} then {high:.2} cells/word" + ); + + // ---- (b) the binding legs. + println!( + "\n★ (b) THE BINDING LEGS (schema = {aggregation_words} words/child)\n \ + {:>8} {:>12} {:>12} {:>14}", + "children", "Δinstrs", "Δhash ops", "Δcells" + ); + for children in [2usize, 3] { + let (with, _) = bindings_only_program(children, true); + let (without, _) = bindings_only_program(children, false); + let (wi, wo_ops, wc) = census(&with); + let (bi, bo_ops, bc) = census(&without); + println!( + " {children:>8} {:>12} {:>12} {:>14}", + wi - bi, + wo_ops as i64 - bo_ops as i64, + wc - bc + ); + } + + // ---- (c) what a leaf node costs, composed. + println!( + "\n★ (c) LEAF NODE = fan-in × (C's F + the statement) + the bindings.\n \ + C measured F(1) = 2,886 and F(2) = 5,771 COMPRESSIONS at production \ + heights; the columns above are what this leg adds on top, per child.\n \ + A child publishing {aggregation_words} words instead of {diagnostic_words} \ + is the whole lever." + ); +} From d19b620517376a7a5fe7935f81fcf19d738996bc Mon Sep 17 00:00:00 2001 From: MauroFab Date: Tue, 8 Sep 2026 15:01:32 -0300 Subject: [PATCH 06/17] feat(lfm): the aggregation node, and the L2G fold that makes it compose MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit One emitter for every level: declare each child's arenas in absorb order, verify each child, bind them, publish the node's own schema. A child is a plain per-table MultiProof whether a wrap or another node produced it, so nothing here is level-specific — the harvest proves it, since `host_table_forked` and `build_table_legs` take (&dyn AIR, StarkProofView) and read a wrap proof exactly as they read a VM epoch's. ★ THE L2G FOLD. The batched aggregator compared each epoch's published L2G root against the global proof's re-commit root for that epoch, and could do it as a local assert because all six legs sat in ONE program. A tree splits them — the epoch wraps are in leaf nodes and the global wrap rides at the root — so the compare must defer to their common ancestor. Re-publishing the subtree's roots as a LIST would grow the node schema with the subtree and make every level's published width a function of the block's epoch count. Folding them with the production hash's two-to-one compression keeps the node schema FIXED SIZE at every level; the root recomputes the same fold over the global wrap's published roots and compares one digest. The fold rule is documented where the root must replicate it. `SchemaLayout` now covers a wrap child and a node child. They differ in their head (a node has FAN_IN Phase A's and no single pair), in their labels (a node covers a RANGE and publishes both ends, which is what gives a parent contiguity across siblings for free) and in their L2G item. That is a constructor apiece rather than a flag, because the differences are real. `digest_from_lanes` is the both-arms inverse of `RootCells::lanes_flat`, written rather than reused: `from_halves` asserts eight halves and is byte-arm-only by construction. FAN_IN is a default, not an assumption — every emitter takes a slice, so the arity is the caller's and the measured host peak still decides it. The gate carries one tamper arm per binding leg, and three rather than one because "both children verified" is exactly what a broken binding looks like: each arm moves one published word in one child's arena and nothing else, so what fails is named by which arm failed. --- prover/src/lfm/per_table_aggregator.rs | 351 +++++++++++++--- prover/src/lfm/per_table_aggregator_tests.rs | 396 ++++++++++++++++++- 2 files changed, 680 insertions(+), 67 deletions(-) diff --git a/prover/src/lfm/per_table_aggregator.rs b/prover/src/lfm/per_table_aggregator.rs index 3e7f1b2ac..d3e3d662a 100644 --- a/prover/src/lfm/per_table_aggregator.rs +++ b/prover/src/lfm/per_table_aggregator.rs @@ -419,80 +419,115 @@ pub fn emit_leg(b: &mut LfmBuilder, child: &ChildShape<'_>, a: &LegArenas) -> Le // ============================ the binding legs ============================ /// Where each field of the block-binding schema sits in a child's published -/// words. +/// words — for a WRAP child and for a NODE child alike. /// -/// The order is the emitter's, and it is one order: `epoch_tests::epoch_program` -/// publishes the pair, the attestation id, then this schema, and -/// `epoch_tests::schema_words` is the same arithmetic as [`Self::schema_words`]. -/// A node indexes by these accessors, so a field inserted on one side and not -/// the other re-binds every field below it — which is why -/// [`Self::assert_covers`] is called at assembly time rather than trusted. +/// The two differ in their head and in two fields, and the difference is real +/// rather than incidental, so it is a constructor apiece rather than a flag: +/// +/// | | wrap child | node child | +/// |---|---|---| +/// | head | `z, α, id₀, id₁` | `id₀, id₁` — a node has FAN_IN Phase A's and no single pair | +/// | labels | one epoch label | the FIRST and LAST label of its subtree | +/// | L2G | the epoch's re-commit root, as lanes | the subtree's FOLDED digest, as cells | +/// | tail | the closure's bus total | nothing | +/// +/// A node has no single `(z, α)` because it replays one transcript per child, +/// and no single epoch label because it covers a RANGE — publishing the range's +/// two ends is what lets a parent pin them to constants and get contiguity +/// across siblings for free. +/// +/// ⚠ `l2g_words` is a WORD count, not a lane count, and the two constructors +/// disagree on purpose: a wrap publishes `RootCells::lanes_flat` (four lanes per +/// root word) while a node publishes the fold's digest CELLS. The codebase has +/// been bitten by lanes-versus-words twice; the field is named for the unit it +/// actually is. pub struct SchemaLayout { + /// Where the two attestation-id words start. + pub id_at: usize, + /// Words published before the schema run. + pub head: usize, pub num_reg: usize, + /// Label words: two for a wrap (one label, lo/hi), four for a node. + pub label_words: usize, pub out_halves: usize, - /// Lanes the L2G root occupies — four on an algebraic hash, eight on a byte - /// one. Read from `proof_arena::lanes_per_root` rather than spelled, because - /// a reader that spells `8` walks an algebraic schema at twice the stride and - /// lands on the wrong field instead of out of bounds. - pub root_lanes: usize, + pub l2g_words: usize, + /// Words published after the schema run. + pub tail: usize, } impl SchemaLayout { - /// The words published before the schema: the shared pair and the two - /// attestation-id words. - pub const HEAD: usize = 4; + /// The layout of an epoch WRAP published under `Publishes::Aggregation`. + pub fn wrap(out_halves: usize) -> Self { + Self { + id_at: 2, + head: 4, + num_reg: crate::tables::register::NUM_REGISTER_ADDRESSES, + label_words: 2, + out_halves, + l2g_words: super::proof_arena::lanes_per_root(), + tail: 1, + } + } - pub fn new(out_halves: usize) -> Self { + /// The layout of an aggregation NODE, at any level. + pub fn node(out_halves: usize) -> Self { Self { + id_at: 0, + head: 2, num_reg: crate::tables::register::NUM_REGISTER_ADDRESSES, + label_words: 4, out_halves, - root_lanes: super::proof_arena::lanes_per_root(), + l2g_words: super::proof_arena::words_per_root(), + tail: 0, } } pub fn schema_words(&self) -> usize { - 2 * self.num_reg + 2 + self.out_halves + self.root_lanes + 2 * self.num_reg + self.label_words + self.out_halves + self.l2g_words } - /// Total words a child publishes under `Publishes::Aggregation` — the head, - /// the schema and the closure's bus total. + /// Every word the child publishes. pub fn total(&self) -> usize { - Self::HEAD + self.schema_words() + 1 + self.head + self.schema_words() + self.tail } /// Pin the layout against what the child actually publishes. /// - /// A level confusion — a layout built for one child applied to another — is - /// a loud failure here rather than a silent mis-binding fifty asserts later. + /// A level confusion — a wrap layout applied to a node, or a layout built + /// for one block applied to another — is a loud failure here rather than a + /// silent mis-binding fifty asserts later. pub fn assert_covers(&self, num_public_words: usize) { assert_eq!( self.total(), num_public_words, "the layout must cover the child's published words exactly \ - (num_reg={}, out_halves={}, root_lanes={})", + (head={}, num_reg={}, label_words={}, out_halves={}, l2g_words={}, tail={})", + self.head, self.num_reg, + self.label_words, self.out_halves, - self.root_lanes, + self.l2g_words, + self.tail, ); } pub fn id(&self, half: usize) -> usize { - 2 + half + self.id_at + half } pub fn reg_init(&self, r: usize) -> usize { - Self::HEAD + r + self.head + r } pub fn reg_fini(&self, r: usize) -> usize { - Self::HEAD + self.num_reg + r + self.head + self.num_reg + r } - pub fn label(&self, half: usize) -> usize { - Self::HEAD + 2 * self.num_reg + half + pub fn label(&self, i: usize) -> usize { + self.head + 2 * self.num_reg + i } pub fn out_half(&self, i: usize) -> usize { - Self::HEAD + 2 * self.num_reg + 2 + i + self.head + 2 * self.num_reg + self.label_words + i } - pub fn l2g_lane(&self, lane: usize) -> usize { - Self::HEAD + 2 * self.num_reg + 2 + self.out_halves + lane + pub fn l2g_word(&self, w: usize) -> usize { + self.head + 2 * self.num_reg + self.label_words + self.out_halves + w } } @@ -530,7 +565,7 @@ pub fn emit_chain_bindings( b: &mut LfmBuilder, legs: &[LegCells], layouts: &[SchemaLayout], - labels: &[u64], + labels: &[&[u64]], ) { assert_eq!(legs.len(), layouts.len(), "one layout per child"); assert_eq!(legs.len(), labels.len(), "one chain position per child"); @@ -556,36 +591,234 @@ pub fn emit_chain_bindings( } } // ---- each label pinned to its position, as a constant of THIS program. - for (k, &label) in labels.iter().enumerate() { - assert_word_is_const( - b, - &legs[k].publics[layouts[k].label(0)], - label & 0xFFFF_FFFF, + // + // A wrap child carries ONE label; a node child carries the first and last of + // its subtree. Pinning every one of them to a constant is what makes + // contiguity across siblings free: the emitter knows the true label + // sequence, so a child covering the wrong range cannot satisfy the pins. + for (k, child_labels) in labels.iter().enumerate() { + assert_eq!( + 2 * child_labels.len(), + layouts[k].label_words, + "child {k} publishes {} label words but {} labels were given", + layouts[k].label_words, + child_labels.len() ); - assert_word_is_const(b, &legs[k].publics[layouts[k].label(1)], label >> 32); + for (i, &label) in child_labels.iter().enumerate() { + assert_word_is_const( + b, + &legs[k].publics[layouts[k].label(2 * i)], + label & 0xFFFF_FFFF, + ); + assert_word_is_const( + b, + &legs[k].publics[layouts[k].label(2 * i + 1)], + label >> 32, + ); + } } } -/// Assert child `k`'s published L2G re-commit root equals the root the global -/// proof's verifier published for epoch `k`. +// ============================ the aggregation node ======================== + +/// Children per node — the tree's arity. +/// +/// A DEFAULT, not an assumption: every emitter below takes a slice, so the +/// arity is whatever the caller passes and nothing here depends on this value. +/// It exists so the tree builder has one place to change. +/// +/// Two is the brief's working default and three is COORD's tie-break, on the +/// grounds that over ten epochs it is 5 distinct programs / 7 proofs / 3 levels +/// against two's 6 / 11 / 4. The measured host peak decides; until it has, the +/// conservative value stands. +pub const FAN_IN: usize = 2; + +/// A digest rebuilt from the lanes a child PUBLISHED for it. +/// +/// The inverse of `RootCells::lanes_flat`, and correct on both arms — four +/// lanes pack into one word, and a root is `words_per_root` of them. +/// +/// ⚠ Deliberately not `RootCells::from_halves`, which asserts EIGHT halves and +/// is byte-arm-only by construction. Handing it an algebraic root's four felts +/// fails the assert; handing a byte root's eight halves to a caller expecting +/// felts would hash four values as if they were eight, silently. +pub fn digest_from_lanes(b: &mut LfmBuilder, lanes: &[Felt]) -> super::edsl::WrapDigest { + let words = super::proof_arena::words_per_root(); + assert_eq!( + lanes.len(), + LANES_PER_WORD * words, + "a published root is four lanes per root word" + ); + let cells: Vec = lanes + .chunks(LANES_PER_WORD) + .map(|c| b.pack_word([c[0], c[1], c[2], c[3]])) + .collect(); + match cells.len() { + 1 => super::edsl::WrapDigest::from_cell(cells[0]), + 2 => super::edsl::WrapDigest::from_pair(cells[0], cells[1]), + n => unreachable!("a root is one or two words, got {n}"), + } +} + +/// Fold a subtree's L2G re-commit roots into ONE digest — a left fold of the +/// production hash's two-to-one compression, identity on a singleton. +/// +/// # Why a fold and not a list +/// +/// The batched aggregator compared each epoch's published L2G root against the +/// global proof's re-commit root for that epoch, and could do it as a local +/// assert because all six legs were in ONE program. A tree splits them: the +/// epoch wraps sit in leaf nodes and the global wrap rides at the ROOT, so the +/// compare must be deferred to their common ancestor. +/// +/// If each node re-published its subtree's roots as a LIST, the node schema +/// would grow with the subtree and every level would have a different published +/// width — which is what makes the parent's leg shape depend on the block's +/// epoch count. Folding them keeps the node schema FIXED SIZE at every level, +/// and the root recomputes the same fold over the global wrap's published roots +/// and compares one digest. /// -/// The in-VM half of the root-equality binding. In a TREE the two sides are not -/// generally in the same node — the global wrap rides at the ROOT — so this is -/// emitted where both are in scope and nowhere else. -pub fn assert_l2g_roots_equal( +/// The rule is stated here because the root must replicate it exactly: left +/// fold, in tree order, `hash_pair(acc, next)`; a single root folds to itself. +pub fn fold_l2g( b: &mut LfmBuilder, - epoch: &LegCells, - epoch_layout: &SchemaLayout, - global: &LegCells, - global_first_root_word: usize, - epoch_index: usize, -) { - let lanes = epoch_layout.root_lanes; - for lane in 0..lanes { - assert_words_equal( - b, - &epoch.publics[epoch_layout.l2g_lane(lane)], - &global.publics[global_first_root_word + lanes * epoch_index + lane], - ); + digests: &[super::edsl::WrapDigest], +) -> super::edsl::WrapDigest { + assert!(!digests.is_empty(), "a subtree covers at least one epoch"); + let hash = b.wrap_hash(); + let mut acc = digests[0]; + for next in &digests[1..] { + acc = hash.hash_pair(b, acc, *next); + } + acc +} + +/// What a node publishes, so that its parent binds it exactly as it binds a +/// wrap. See [`SchemaLayout::node`] for the layout this fills. +pub struct NodePublishes<'a> { + /// The children's legs, in chain order. + pub legs: &'a [LegCells], + /// One layout per child. + pub layouts: &'a [SchemaLayout], + /// The first and last epoch label of the subtree — emit-time constants. + pub label_range: (u64, u64), +} + +/// Emit a node's published words: the shared attestation id, the first child's +/// register INIT vector, the last child's register FINI vector, the subtree's +/// first and last epoch labels, the last child's output halves, and the folded +/// L2G digest. +/// +/// Every value is republished in the SAME form the wrap published it, so a +/// parent's `assert_words_equal` reads a node and a wrap alike: the id as a +/// four-lane digest word, the register / label / output items as base words. +pub fn emit_node_publishes(b: &mut LfmBuilder, p: &NodePublishes<'_>) { + let NodePublishes { + legs, + layouts, + label_range, + } = *p; + assert_eq!(legs.len(), layouts.len(), "one layout per child"); + assert!(!legs.is_empty(), "a node has children"); + let first = &legs[0]; + let last = legs.last().expect("nonempty"); + let l_first = &layouts[0]; + let l_last = layouts.last().expect("nonempty"); + + // ---- the attestation id, as the four-lane word the wrap published. + for half in 0..2 { + let lanes = &first.publics[l_first.id(half)].lanes; + let word = b.pack_word([lanes[0], lanes[1], lanes[2], lanes[3]]); + b.public(word); + } + // ---- the chain's two ends. + for r in 0..l_first.num_reg { + b.public(first.publics[l_first.reg_init(r)].lanes[0].as_cell()); + } + for r in 0..l_last.num_reg { + b.public(last.publics[l_last.reg_fini(r)].lanes[0].as_cell()); + } + // ---- the label RANGE, as constants of this program. Publishing the ends + // rather than the list is what keeps the schema fixed-size; the parent pins + // both to constants and gets contiguity across siblings for free. + for label in [label_range.0, label_range.1] { + let lo = b.felt_const(FE::from(label & 0xFFFF_FFFF)); + b.public(lo.as_cell()); + let hi = b.felt_const(FE::from(label >> 32)); + b.public(hi.as_cell()); + } + // ---- the last child's output halves — the block's output, carried up. + for i in 0..l_last.out_halves { + b.public(last.publics[l_last.out_half(i)].lanes[0].as_cell()); + } + // ---- the folded L2G digest. + let digests: Vec = legs + .iter() + .zip(layouts) + .map(|(leg, layout)| { + let lanes: Vec = (0..layout.l2g_words) + .map(|w| leg.publics[layout.l2g_word(w)].lanes[0]) + .collect(); + digest_from_lanes(b, &lanes) + }) + .collect(); + let folded = fold_l2g(b, &digests); + for cell in folded.cells() { + b.public(*cell); } } + +/// One aggregation node, end to end: verify every child, bind them, publish the +/// node's own schema. +/// +/// The SAME function serves every level — a child is a plain per-table +/// `MultiProof` whether a wrap or another node produced it, and the only thing +/// that changes is the children's shapes and layouts. What does not carry across +/// levels is the node's IDENTITY: the legs absorb their children's `program_id` +/// as emit-time constants, so each level compiles to its own program. +pub struct NodeInputs<'a> { + pub children: &'a [ChildShape<'a>], + pub layouts: &'a [SchemaLayout], + /// Per child, the epoch labels it must carry: one for a wrap child, the two + /// ends of its subtree for a node child. + pub labels: &'a [&'a [u64]], + /// The first and last epoch label this node's subtree covers. + pub label_range: (u64, u64), +} + +/// Declare every arena the node reads, in absorb order, then emit it. +pub fn emit_node(b: &mut LfmBuilder, inputs: &NodeInputs<'_>) { + let NodeInputs { + children, + layouts, + labels, + label_range, + } = *inputs; + assert!(!children.is_empty(), "a node verifies at least one child"); + assert_eq!(children.len(), layouts.len(), "one layout per child"); + assert_eq!(children.len(), labels.len(), "one label list per child"); + for (child, layout) in children.iter().zip(layouts) { + layout.assert_covers(child.num_public_words); + } + + // Declaration order IS absorb order, end to end: every child's arenas are + // declared before any leg is emitted. + let arenas: Vec = children + .iter() + .map(|child| declare_leg_arenas(b, child)) + .collect(); + let legs: Vec = children + .iter() + .zip(&arenas) + .map(|(child, a)| emit_leg(b, child, a)) + .collect(); + emit_chain_bindings(b, &legs, layouts, labels); + emit_node_publishes( + b, + &NodePublishes { + legs: &legs, + layouts, + label_range, + }, + ); +} diff --git a/prover/src/lfm/per_table_aggregator_tests.rs b/prover/src/lfm/per_table_aggregator_tests.rs index 155777fe2..5934221ed 100644 --- a/prover/src/lfm/per_table_aggregator_tests.rs +++ b/prover/src/lfm/per_table_aggregator_tests.rs @@ -145,8 +145,8 @@ pub(super) fn real_global( let lookup: Vec = (0..stark::lookup::LOGUP_NUM_CHALLENGES) .map(|_| transcript.sample_field_element()) .collect(); - let z_alpha = (lookup[0], lookup[1]); + let z_alpha = (lookup[0], lookup[1]); let num_tables = refs.len(); let tables: Vec = refs .iter() @@ -583,7 +583,7 @@ fn bindings_only_program(children: usize, with_bindings: bool) -> (LfmProgram, u // A block-final epoch's output length; the schema's only variable term. const OUT_HALVES: usize = 8; - let layout = SchemaLayout::new(OUT_HALVES); + let layout = SchemaLayout::wrap(OUT_HALVES); let words = layout.total(); let mut b = LfmBuilder::new().with_wrap_hash(super::edsl::WrapHash::production()); @@ -601,10 +601,12 @@ fn bindings_only_program(children: usize, with_bindings: bool) -> (LfmProgram, u } if with_bindings { let layouts: Vec = (0..children) - .map(|_| SchemaLayout::new(OUT_HALVES)) + .map(|_| SchemaLayout::wrap(OUT_HALVES)) .collect(); - let labels: Vec = (0..children as u64).collect(); - emit_chain_bindings(&mut b, &legs, &layouts, &labels); + // One label per WRAP child, matching `SchemaLayout::wrap`'s two label words. + let labels: Vec<[u64; 1]> = (0..children as u64).map(|k| [k]).collect(); + let label_refs: Vec<&[u64]> = labels.iter().map(|l| &l[..]).collect(); + emit_chain_bindings(&mut b, &legs, &layouts, &label_refs); } (compile(b.finish()), words) } @@ -654,9 +656,15 @@ fn the_node_cost_model_is_measured() { // ---- (a) the per-published-word marginal. const OUT_HALVES: usize = 8; - let aggregation_words = SchemaLayout::new(OUT_HALVES).total(); - // The measured diagnostic count at q=110, plus the schema this branch adds. - let diagnostic_words = 10_507 + SchemaLayout::new(OUT_HALVES).schema_words(); + let aggregation_words = SchemaLayout::wrap(OUT_HALVES).total(); + // ⚠ A SAMPLE POINT, not an assumption. 10,507 is the MEASURED diagnostic + // count of the q=110 wrap; the diagnostic set is dominated by per-query terms + // (one FRI terminal and one index per query per sub-proof), so this point + // goes stale the moment the query count moves — and lane P's re-tune may take + // it to 119. Nothing is built against it: what this instrument produces is + // the per-word COEFFICIENT, which is a property of the emitter and holds at + // any count. The point is here only so the table brackets the real range. + let diagnostic_words = 10_507 + SchemaLayout::wrap(OUT_HALVES).schema_words(); let points = [0, 64, 128, 256, 512, aggregation_words, diagnostic_words]; println!( "\n★ (a) THE PER-PUBLISHED-WORD BILL, at {hash:?}\n \ @@ -723,3 +731,375 @@ fn the_node_cost_model_is_measured() { is the whole lever." ); } + +// ======================= the child harvest and the node =================== + +/// One child LFM proof, production-accepted, harvested for emission. +/// +/// The per-table sibling of `epoch_tests::RealEpoch`, over an LFM machine's +/// proof rather than the VM's. ★ Nothing in the harvest is LFM-specific: +/// `host_table_forked` and `build_table_legs` take `(&dyn AIR, +/// StarkProofView)`, so the same two functions read a wrap proof, a node proof +/// and a VM epoch proof alike. That is what makes one node emitter serve every +/// level. +pub(super) struct RealChild { + pub(super) artifacts: super::registry::LfmArtifacts, + pub(super) opts: crate::ProofOptions, + pub(super) public_words: Vec<(u32, LfmWord)>, + pub(super) tables: Vec, + pub(super) legs: Vec, +} + +// ⚠ The harvested `(z, α)` is deliberately NOT kept. It is the right +// differential oracle for a leg — it is what the global leg publishes and +// compares — but a node under `Publishes::Aggregation` publishes no challenges, +// so there is nowhere to compare it against and a kept field would be dead. What +// stands in its place is weaker and worth naming: the node EXECUTING at all +// means the leg derived the child's own challenges, because a leg on different +// challenges cannot authenticate the child's walks. That is implication, not a +// value comparison, and it is a real gap in the evidence until a diagnostic node +// variant exists to publish the pair. + +/// Harvest a child from a proof PRODUCTION ACCEPTS. Panics loudly otherwise — +/// nothing downstream may read a proof the verifier would reject. +pub(super) fn real_child( + artifacts: super::registry::LfmArtifacts, + opts: crate::ProofOptions, + proved: &super::proof::LfmProof, +) -> RealChild { + use crypto::fiat_shamir::is_transcript::IsTranscript; + use stark::proof::view::MultiProofView; + + assert!( + super::proof::verify_against_artifacts( + &artifacts, + &proved.proof, + &proved.public_words, + &opts + ), + "the harness only reads children production accepts" + ); + + let airs = super::airs::LfmAirs::new_chunked( + &artifacts.roots, + &artifacts.blake3_chunk_roots, + &opts, + artifacts.keccak_rnd_chunks, + artifacts.hasher, + artifacts.chip_set, + ); + let refs = airs.air_refs(); + let view = MultiProofView::Owned(&proved.proof); + assert_eq!(refs.len(), view.len(), "one AIR per sub-proof"); + + // The seed IS `verify_against_chunked`'s: the LFM statement over the claimed + // words, and nothing before it. + let seed = || { + let mut t = crate::hash_pin::block_transcript(&[]); + super::statement::absorb_lfm_statement( + &mut t, + &artifacts.program_id, + &proved.public_words, + opts.fri_final_poly_log_degree, + ); + t + }; + + let mut transcript = seed(); + for (idx, air) in refs.iter().enumerate() { + let v = view.get(idx); + if air.is_preprocessed() { + transcript.append_bytes(&air.precomputed_commitment()); + } + transcript.append_bytes(v.lde_trace_main_merkle_root()); + } + let lookup: Vec = (0..stark::lookup::LOGUP_NUM_CHALLENGES) + .map(|_| transcript.sample_field_element()) + .collect(); + + let num_tables = refs.len(); + let tables: Vec = refs + .iter() + .enumerate() + .map(|(idx, air)| { + let v = view.get(idx); + let mut fork = transcript.clone(); + if num_tables > 1 { + fork.append_bytes(&(idx as u64).to_le_bytes()); + } + if let Some(root) = v.lde_trace_aux_merkle_root() { + fork.append_bytes(root); + } + if let Some(c) = v.bus_table_contribution() { + fork.append_field_element(&c); + } + super::epoch_tests::host_table_forked(*air, v, idx, num_tables, &mut fork, &lookup) + }) + .collect(); + let legs = refs + .iter() + .enumerate() + .map(|(idx, air)| super::epoch_verify_tests::build_table_legs(*air, view.get(idx), &lookup)) + .collect(); + + RealChild { + artifacts, + opts, + public_words: proved.public_words.clone(), + tables, + legs, + } +} + +/// The child's shape, as the node's emitter reads it. +pub(super) fn child_shape(c: &RealChild) -> super::per_table_aggregator::ChildShape<'_> { + super::per_table_aggregator::ChildShape { + program_id: &c.artifacts.program_id, + num_public_words: c.public_words.len(), + fri_final_poly_log_degree: c.opts.fri_final_poly_log_degree, + tables: c + .tables + .iter() + .zip(&c.legs) + .map(|(h, leg)| super::per_table_aggregator::ChildTable { + challenge: &h.shape, + verify: &leg.verify, + analysis: &leg.analysis, + precomputed_root: leg.precomputed_commitment.as_ref(), + }) + .collect(), + } +} + +/// The child's arenas, in `declare_leg_arenas`' declaration order. +pub(super) fn child_arena_words(c: &RealChild) -> Vec> { + let mut arenas: Vec> = Vec::new(); + // The published words, eight halves each — the statement's own layout. + let mut publics = Vec::with_capacity(8 * c.public_words.len()); + for (_, word) in &c.public_words { + for lane in word { + let v: u64 = lane.canonical(); + publics.push(base_word(FE::from(v & 0xFFFF_FFFF))); + publics.push(base_word(FE::from(v >> 32))); + } + } + arenas.push(publics); + arenas.push(super::proof_arena::commitments_to_arena( + &c.tables.iter().map(|h| h.main_root).collect::>(), + )); + for (h, leg) in c.tables.iter().zip(&c.legs) { + if let Some(root) = &h.aux_root { + arenas.push(super::proof_arena::commitments_to_arena(&[*root])); + } + if let Some(l) = &h.contribution { + arenas.push(vec![ext_word(l)]); + } + arenas.push(super::proof_arena::commitments_to_arena(&[ + h.composition_root + ])); + arenas.push(h.ood_current.iter().map(ext_word).collect()); + arenas.push(h.ood_next.iter().map(ext_word).collect()); + arenas.push(h.parts.iter().map(ext_word).collect()); + arenas.push(super::proof_arena::commitments_to_arena(&h.fri_roots)); + arenas.push(h.fri_coeffs.iter().map(ext_word).collect()); + if let Some(nonce) = h.nonce { + arenas.push(vec![base_word(FE::from(nonce))]); + } + arenas.push(leg.opening_arena()); + arenas.push(leg.fri_arena()); + } + arenas +} + +/// The aggregation node over `children`, at any level and any arity. +pub(super) fn node_program( + children: &[RealChild], + layouts: &[super::per_table_aggregator::SchemaLayout], + labels: &[&[u64]], + label_range: (u64, u64), +) -> LfmProgram { + let mut b = LfmBuilder::new().with_wrap_hash(super::edsl::WrapHash::production()); + let shapes: Vec<_> = children.iter().map(child_shape).collect(); + super::per_table_aggregator::emit_node( + &mut b, + &super::per_table_aggregator::NodeInputs { + children: &shapes, + layouts, + labels, + label_range, + }, + ); + compile(b.finish()) +} + +/// ★ THE LEAF NODE RUNS — the first aggregation node over real per-table wrap +/// proofs. +/// +/// # What it is +/// +/// `FAN_IN` epochs of a fixture continuation, each wrapped by the assembled +/// per-table epoch verifier under `Publishes::Aggregation`, and ONE emitted +/// program that verifies both wrap proofs and binds them: the shared attestation +/// id, the register fini→init seam, and each epoch's label pinned to its chain +/// position as a constant. The node then publishes the schema its own parent +/// will read. +/// +/// # Why the tamper arms are three and not one +/// +/// Each binding leg can fail on its own and a single arm would not tell them +/// apart. The register seam, the shared id and the label pin are three +/// independent claims about the relationship between two proofs that both +/// verify — and "both children verified" is exactly what a broken binding still +/// looks like. Each arm moves ONE published word in ONE child's arena and +/// nothing else, so what fails is named by which arm failed. +/// +/// # Cost +/// +/// Box tier and `#[ignore]`d: two epoch wraps proved (a wrap proof carries a +/// full LFM chip set), then a node program that verifies both. The suite gates +/// the pieces — `wrap_tests::the_fixture_epoch_wraps` proves one wrap, +/// `the_global_verifier_leg_runs_and_rejects_tampers` runs a per-table leg, and +/// `the_aggregation_publish_profile_drops_only_diagnostics` pins what a wrap +/// publishes — so this is the assembly rather than any of its parts. +#[test] +#[ignore = "box tier: proves FAN_IN epoch wraps and a node over them"] +fn the_leaf_node_verifies_and_binds_two_wraps() { + use super::epoch_tests::Publishes; + use super::per_table_aggregator::{FAN_IN, SchemaLayout}; + use super::proof::lfm_prove; + use super::registry::build_artifacts_with_hasher; + use std::time::Instant; + + let elf_bytes = super::proof_fixture::read_inner_elf(); + let inner = super::proof_fixture::fixture_options(); + let bundle = crate::continuation::prove_continuation( + &elf_bytes, + &[], + super::proof_fixture::FIXTURE_EPOCH_LOG2, + &inner, + ) + .expect("the fixture continuation must prove"); + assert!( + bundle.num_epochs() >= FAN_IN, + "a fan-in-{FAN_IN} leaf needs {FAN_IN} epochs, the fixture has {}", + bundle.num_epochs() + ); + + // ---- the children: one wrap per epoch, at the AGGREGATION publish set. + let t = Instant::now(); + let mut children = Vec::with_capacity(FAN_IN); + let mut layouts = Vec::with_capacity(FAN_IN); + let mut labels = Vec::with_capacity(FAN_IN); + let wrap_opts = super::proof::aggregation_wrap_options(); + for k in 0..FAN_IN { + let e = + super::epoch_tests::real_epoch_from_continuation(&inner, &elf_bytes, &bundle, k, None) + .expect("every epoch must reconstruct from proofs alone"); + let out_halves = e.statement.public_output_len.div_ceil(4); + let program = + super::epoch_tests::epoch_program_publishing(&e, true, Publishes::Aggregation); + let arenas = super::epoch_tests::epoch_arena_words(&e, true); + let artifacts = + build_artifacts_with_hasher(&program, &wrap_opts, crate::hash_pin::BLOCK_HASHER); + let proved = lfm_prove(&program, &artifacts, &arenas, &wrap_opts) + .expect("the epoch wrap must prove at the aggregation preset"); + let layout = SchemaLayout::wrap(out_halves); + layout.assert_covers(proved.public_words.len()); + layouts.push(layout); + // The label is a pure function of the chain position, exactly as the + // global proof's own AIR reconstruction derives it. + labels.push([crate::tables::local_to_global::epoch_label(k as u64)]); + children.push(real_child(artifacts, wrap_opts.clone(), &proved)); + } + let label_refs: Vec<&[u64]> = labels.iter().map(|l| &l[..]).collect(); + let label_range = (labels[0][0], labels[FAN_IN - 1][0]); + println!( + " {FAN_IN} epoch wraps proved in {:.1}s, {} published words each, \ + {} sub-proofs each", + t.elapsed().as_secs_f64(), + children[0].public_words.len(), + children[0].tables.len(), + ); + + // ---- the node. + let t = Instant::now(); + let program = node_program(&children, &layouts, &label_refs, label_range); + let arenas: Vec> = children.iter().flat_map(child_arena_words).collect(); + println!( + " leaf node emitted in {:.1}s: {} instructions", + t.elapsed().as_secs_f64(), + program.instrs.len() + ); + + let t = Instant::now(); + let exec = execute(&program, &arenas, &crate::hash_pin::BLOCK_HASHER) + .expect("★ the leaf node must execute"); + let node_layout = SchemaLayout::node(layouts[FAN_IN - 1].out_halves); + node_layout.assert_covers(exec.public_words.len()); + println!( + " ★ LEAF NODE EXECUTED in {:.1}s: {} published words (schema {} + head {})", + t.elapsed().as_secs_f64(), + exec.public_words.len(), + node_layout.schema_words(), + node_layout.head, + ); + + // ---- the node's own proof, so the level above has something to verify. + let artifacts = + build_artifacts_with_hasher(&program, &wrap_opts, crate::hash_pin::BLOCK_HASHER); + let t = Instant::now(); + let proved = + lfm_prove(&program, &artifacts, &arenas, &wrap_opts).expect("★ THE LEAF NODE MUST PROVE"); + let prove_secs = t.elapsed().as_secs_f64(); + let t = Instant::now(); + assert!( + super::proof::verify_against_artifacts( + &artifacts, + &proved.proof, + &proved.public_words, + &wrap_opts + ), + "the leaf node's proof must verify" + ); + println!( + "\n★ LEAF NODE PROVED AND VERIFIED\n prove {prove_secs:.1}s\n verify {:.2}s\n \ + {} sub-proofs, {} published words\n peak RSS {:?} GiB", + t.elapsed().as_secs_f64(), + proved.proof.proofs.len(), + proved.public_words.len(), + super::wrap_tests::peak_rss_gib(), + ); + + // ---- ONE TAMPER ARM PER BINDING LEG. + // + // Each moves a single published HALF in one child's publics arena — arena 0 + // of that child, eight halves per word — and nothing else. Both children's + // proofs still verify on their own; what breaks is the relationship. + let arena_of = |child: usize| -> usize { + // Each child contributes `child_arena_words(child).len()` arenas, and its + // publics arena is the first of them. Counted rather than assumed, so a + // declaration-order change tampers the right arena or fails loudly. + children[..child] + .iter() + .map(|c| child_arena_words(c).len()) + .sum() + }; + let bump = |arenas: &mut Vec>, arena: usize, word: usize| { + let half = 8 * word; + arenas[arena][half] = + base_word(super::word::word_as_base(&arenas[arena][half]).expect("a half") + FE::one()); + }; + for (name, child, word) in [ + ("the register chain", 0usize, layouts[0].reg_fini(0)), + ("the shared attestation id", 1usize, layouts[1].id(0)), + ("the epoch label pin", 1usize, layouts[1].label(0)), + ] { + let mut tampered = arenas.clone(); + bump(&mut tampered, arena_of(child), word); + assert!( + execute(&program, &tampered, &crate::hash_pin::BLOCK_HASHER).is_err(), + "moving {name} in child {child} must make the node unprovable" + ); + println!(" ✓ tamper arm: {name} rejected"); + } +} From 540c247029a3afa247ae187fbdd5bcfea7bff065 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Tue, 8 Sep 2026 15:04:16 -0300 Subject: [PATCH 07/17] test(lfm): differential the node's legs against their children's own pair MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes the evidence gap named when the node was built. A node under the aggregation publish set publishes no challenges, so the only thing saying its legs derived their CHILDREN's challenges was that the node executes at all — a leg on different challenges cannot authenticate the child's walks, so execution implies agreement. Implication is weaker than what every other emitted verifier in this crate is held to. The epoch wrap and the global leg both publish their pair and compare it against production's own replay; the node was the one that did not, and only because its publish set had no room for it. `NodePublishSet::Diagnostic` publishes each child's pair AFTER the schema, so no schema index moves and `SchemaLayout::node` reads both variants identically. It is a gate shape and never a child — nothing verifies a diagnostic node. The oracle is the pair `verify_against_chunked`'s own Phase A recovers host-side from the same proof, which is why `RealChild` keeps `z_alpha` again: it now has a consumer, where before it would have been a dead field. --- prover/src/lfm/per_table_aggregator.rs | 36 +++++++++ prover/src/lfm/per_table_aggregator_tests.rs | 78 ++++++++++++++++---- 2 files changed, 100 insertions(+), 14 deletions(-) diff --git a/prover/src/lfm/per_table_aggregator.rs b/prover/src/lfm/per_table_aggregator.rs index d3e3d662a..9dbbb62f0 100644 --- a/prover/src/lfm/per_table_aggregator.rs +++ b/prover/src/lfm/per_table_aggregator.rs @@ -784,6 +784,34 @@ pub struct NodeInputs<'a> { pub labels: &'a [&'a [u64]], /// The first and last epoch label this node's subtree covers. pub label_range: (u64, u64), + /// Which words this node publishes. + pub publishes: NodePublishSet, +} + +/// Which words a node publishes — the node-level counterpart of +/// `epoch_tests::Publishes`, and it exists for a different reason. +/// +/// A node under [`NodePublishSet::Aggregation`] publishes no challenges at all, +/// which leaves its legs with no differential surface: the only evidence that a +/// leg derived its CHILD's challenges is that the node executes, since a leg on +/// different challenges cannot authenticate the child's walks. That is +/// implication rather than a value comparison, and it is weaker than what every +/// other emitted verifier in this crate is held to — the epoch wrap and the +/// global leg both publish their pair and differential it against production's +/// own replay. +/// +/// [`NodePublishSet::Diagnostic`] restores that surface by publishing each +/// child's `(z, α)` AFTER the schema, so the schema's own indices do not move +/// and `SchemaLayout::node` reads both variants' heads identically. It is a gate +/// shape, never a child: nothing verifies a diagnostic node. +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +pub enum NodePublishSet { + /// The node schema and nothing else — what a node that will be VERIFIED + /// publishes. + Aggregation, + /// The schema, then each child's `(z, α)` in child order — the differential + /// surface. + Diagnostic, } /// Declare every arena the node reads, in absorb order, then emit it. @@ -793,6 +821,7 @@ pub fn emit_node(b: &mut LfmBuilder, inputs: &NodeInputs<'_>) { layouts, labels, label_range, + publishes, } = *inputs; assert!(!children.is_empty(), "a node verifies at least one child"); assert_eq!(children.len(), layouts.len(), "one layout per child"); @@ -821,4 +850,11 @@ pub fn emit_node(b: &mut LfmBuilder, inputs: &NodeInputs<'_>) { label_range, }, ); + // The differential surface, AFTER the schema so no schema index moves. + if publishes == NodePublishSet::Diagnostic { + for leg in &legs { + b.public(leg.z_alpha.0.as_cell()); + b.public(leg.z_alpha.1.as_cell()); + } + } } diff --git a/prover/src/lfm/per_table_aggregator_tests.rs b/prover/src/lfm/per_table_aggregator_tests.rs index 5934221ed..b3541623a 100644 --- a/prover/src/lfm/per_table_aggregator_tests.rs +++ b/prover/src/lfm/per_table_aggregator_tests.rs @@ -748,18 +748,14 @@ pub(super) struct RealChild { pub(super) public_words: Vec<(u32, LfmWord)>, pub(super) tables: Vec, pub(super) legs: Vec, + /// The child's OWN shared LogUp pair, recovered host-side by + /// `verify_against_chunked`'s own Phase A replay — the oracle the node's leg + /// must reproduce in-machine. Consumed by + /// [`the_leaf_node_verifies_and_binds_two_wraps`] through + /// `NodePublishSet::Diagnostic`. + pub(super) z_alpha: (FEE, FEE), } -// ⚠ The harvested `(z, α)` is deliberately NOT kept. It is the right -// differential oracle for a leg — it is what the global leg publishes and -// compares — but a node under `Publishes::Aggregation` publishes no challenges, -// so there is nowhere to compare it against and a kept field would be dead. What -// stands in its place is weaker and worth naming: the node EXECUTING at all -// means the leg derived the child's own challenges, because a leg on different -// challenges cannot authenticate the child's walks. That is implication, not a -// value comparison, and it is a real gap in the evidence until a diagnostic node -// variant exists to publish the pair. - /// Harvest a child from a proof PRODUCTION ACCEPTS. Panics loudly otherwise — /// nothing downstream may read a proof the verifier would reject. pub(super) fn real_child( @@ -848,6 +844,7 @@ pub(super) fn real_child( public_words: proved.public_words.clone(), tables, legs, + z_alpha: (lookup[0], lookup[1]), } } @@ -917,6 +914,7 @@ pub(super) fn node_program( layouts: &[super::per_table_aggregator::SchemaLayout], labels: &[&[u64]], label_range: (u64, u64), + publishes: super::per_table_aggregator::NodePublishSet, ) -> LfmProgram { let mut b = LfmBuilder::new().with_wrap_hash(super::edsl::WrapHash::production()); let shapes: Vec<_> = children.iter().map(child_shape).collect(); @@ -927,6 +925,7 @@ pub(super) fn node_program( layouts, labels, label_range, + publishes, }, ); compile(b.finish()) @@ -965,7 +964,7 @@ pub(super) fn node_program( #[ignore = "box tier: proves FAN_IN epoch wraps and a node over them"] fn the_leaf_node_verifies_and_binds_two_wraps() { use super::epoch_tests::Publishes; - use super::per_table_aggregator::{FAN_IN, SchemaLayout}; + use super::per_table_aggregator::{FAN_IN, NodePublishSet, SchemaLayout}; use super::proof::lfm_prove; use super::registry::build_artifacts_with_hasher; use std::time::Instant; @@ -1022,9 +1021,61 @@ fn the_leaf_node_verifies_and_binds_two_wraps() { ); // ---- the node. - let t = Instant::now(); - let program = node_program(&children, &layouts, &label_refs, label_range); let arenas: Vec> = children.iter().flat_map(child_arena_words).collect(); + let node_layout = SchemaLayout::node(layouts[FAN_IN - 1].out_halves); + + // ---- ★ THE DIFFERENTIAL, on the same shape with the surface restored. + // + // Without this the only evidence that a leg derived its CHILD's challenges + // is that the node executes — a leg on different challenges cannot + // authenticate the child's walks, so execution implies agreement. That is + // implication, and every other emitted verifier in this crate is held to a + // value comparison against production's own replay. This is that comparison: + // the pair each leg reaches, against the pair `verify_against_chunked`'s own + // Phase A recovered host-side from the same proof. + let t = Instant::now(); + let diagnostic = node_program( + &children, + &layouts, + &label_refs, + label_range, + NodePublishSet::Diagnostic, + ); + let exec_diag = execute(&diagnostic, &arenas, &crate::hash_pin::BLOCK_HASHER) + .expect("the diagnostic node must execute"); + let tail = node_layout.head + node_layout.schema_words(); + assert_eq!( + exec_diag.public_words.len(), + tail + 2 * FAN_IN, + "the diagnostic node publishes the schema then one pair per child" + ); + for (k, child) in children.iter().enumerate() { + let got = |i: usize| { + super::word::word_as_ext(&exec_diag.public_words[i].1).expect("an ext challenge") + }; + assert_eq!(got(tail + 2 * k), child.z_alpha.0, "child {k}: the leg's z"); + assert_eq!( + got(tail + 2 * k + 1), + child.z_alpha.1, + "child {k}: the leg's alpha" + ); + } + println!( + " ✓ differential: every leg reaches its child's OWN (z, alpha) \ + ({:.1}s, {} instructions)", + t.elapsed().as_secs_f64(), + diagnostic.instrs.len() + ); + + // ---- the node a parent would verify. + let t = Instant::now(); + let program = node_program( + &children, + &layouts, + &label_refs, + label_range, + NodePublishSet::Aggregation, + ); println!( " leaf node emitted in {:.1}s: {} instructions", t.elapsed().as_secs_f64(), @@ -1034,7 +1085,6 @@ fn the_leaf_node_verifies_and_binds_two_wraps() { let t = Instant::now(); let exec = execute(&program, &arenas, &crate::hash_pin::BLOCK_HASHER) .expect("★ the leaf node must execute"); - let node_layout = SchemaLayout::node(layouts[FAN_IN - 1].out_halves); node_layout.assert_covers(exec.public_words.len()); println!( " ★ LEAF NODE EXECUTED in {:.1}s: {} published words (schema {} + head {})", From e198f76ca9adf55e5ae0eeba1c9d019d966fea40 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Tue, 8 Sep 2026 15:05:33 -0300 Subject: [PATCH 08/17] docs(lfm): the query count is settled at 110, not provisional The re-tune holds q=110 by moving security_bits 128 -> 120 at blowup 4 rather than by taking the count to 119, so the cost instrument's 10,507 sample point is current rather than a value that may go stale. The coefficient the instrument produces was never a function of it. --- prover/src/lfm/per_table_aggregator_tests.rs | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/prover/src/lfm/per_table_aggregator_tests.rs b/prover/src/lfm/per_table_aggregator_tests.rs index b3541623a..2d4ac272b 100644 --- a/prover/src/lfm/per_table_aggregator_tests.rs +++ b/prover/src/lfm/per_table_aggregator_tests.rs @@ -660,10 +660,15 @@ fn the_node_cost_model_is_measured() { // ⚠ A SAMPLE POINT, not an assumption. 10,507 is the MEASURED diagnostic // count of the q=110 wrap; the diagnostic set is dominated by per-query terms // (one FRI terminal and one index per query per sub-proof), so this point - // goes stale the moment the query count moves — and lane P's re-tune may take - // it to 119. Nothing is built against it: what this instrument produces is - // the per-word COEFFICIENT, which is a property of the emitter and holds at - // any count. The point is here only so the table brackets the real range. + // moves with the query count. + // + // ✓ The posture is settled and q STAYS AT 110 — the security re-tune holds it + // by moving `security_bits` 128 -> 120 at blowup 4 rather than by taking the + // count to 119. So this point is current, not provisional. + // + // Nothing is built against it either way: what this instrument produces is + // the per-word COEFFICIENT, a property of the emitter that holds at any + // count. The point is here so the table brackets the real range. let diagnostic_words = 10_507 + SchemaLayout::wrap(OUT_HALVES).schema_words(); let points = [0, 64, 128, 256, 512, aggregation_words, diagnostic_words]; println!( From e7081d135e9c35fee3b1f314fe131dbf1d5534f4 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Tue, 8 Sep 2026 16:05:33 -0300 Subject: [PATCH 09/17] fix(lfm): the publish-profile gate compared indices it meant to differ MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The assertion read `assert_eq!(diag[last], agg[last])`, and a published word is an `(index, value)` pair. The two indices cannot be equal — making the lists different lengths is the entire point of R2 — so the gate asserted the negation of the property it exists to prove. Box A caught it with the four field elements matching exactly and only the indices differing, 307 against 144: the emitter doing precisely what it should, failed by a test asserting something it never meant. 144 is also the predicted Aggregation size (5 + schema_words), so the profile is doing its job at fixture scale. The replacement checks each profile on its own against production's COMMIT bus balance, which is a stronger oracle than "the other profile agrees with me": the last published word must be the closure's total AND reach the target production computed. Position is asserted separately, as what "ends the list" actually means for an auto-incrementing index. --- prover/src/lfm/per_table_aggregator_tests.rs | 34 ++++++++++++++++---- 1 file changed, 28 insertions(+), 6 deletions(-) diff --git a/prover/src/lfm/per_table_aggregator_tests.rs b/prover/src/lfm/per_table_aggregator_tests.rs index 2d4ac272b..058972eb0 100644 --- a/prover/src/lfm/per_table_aggregator_tests.rs +++ b/prover/src/lfm/per_table_aggregator_tests.rs @@ -507,12 +507,34 @@ fn the_aggregation_publish_profile_drops_only_diagnostics() { agg[..head], "the binding head must not move with the profile" ); - // ---- the tail: the bus total, which both profiles still publish last. - assert_eq!( - diag[diag.len() - 1], - agg[agg.len() - 1], - "the closure's total ends the list under either profile" - ); + // ---- the tail: the closure's total, which both profiles publish LAST. + // + // ⚠ Against PRODUCTION'S OWN TARGET, one profile at a time — never by + // comparing the two lists' last entries to each other. A published word is + // an `(index, value)` pair, and the two indices cannot be equal: making the + // lists different lengths is the entire point of R2. That was this + // assertion's first form, and it failed on box A with the four field + // elements matching exactly and only the indices differing (307 against + // 144) — the emitter doing precisely what it should, caught by a test + // asserting something it never meant. + // + // The oracle here is also stronger than the one it replaces: production's + // COMMIT-bus balance, rather than "the other profile agrees with me". + for (label, words) in [("Diagnostic", &diag), ("Aggregation", &agg)] { + let (index, word) = words.last().expect("a profile publishes words"); + assert_eq!( + *index as usize, + words.len() - 1, + "{label}: publish indices auto-increment, so the last word's index \ + is len-1" + ); + assert_eq!( + super::word::word_as_ext(word).expect("the bus total is ext"), + e.expected_bus_balance, + "{label}: the closure's total must end the list and reach \ + production's own COMMIT-bus target" + ); + } assert_eq!(agg.len(), head + 1, "Aggregation is the head and the total"); // ---- what was dropped, from the epoch's own shapes rather than from a From d48f4e1401779699d787517ece4efba75132acf1 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Tue, 8 Sep 2026 16:16:57 -0300 Subject: [PATCH 10/17] fix(lfm): the spine gate walked past the schema by a literal too MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `the_epoch_challenge_spine_matches_production` failed on box A with "beta of table 0" reading an all-zero challenge. It is not an underived challenge and it is not a leak: `epoch_challenge_program` is `epoch_program(e, false)` — the SAME emitter with the legs off, as its own doc says and says why — so it gained R1's schema like every other caller, and a literal cursor of 4 landed on register INIT slot 0. x0 is hard-wired zero, so the mismatch printed zeroes and read like a derivation failure. This is the exact failure the R1 commit message described, at a second site that commit missed. The audit that missed it read the function's NAME and concluded "different emitter" without opening its two-line body — a claim about what code does, made from a name. The re-audit walked every caller of `epoch_program`/`epoch_challenge_program`/`epoch_program_with` and every positional read of `public_words`: this was the last one. The rest read index 0, 1, 2 or the final word, all of which sit outside the inserted run. Also adds a samplability pre-flight to the leaf gate. `emit_table_challenges` samples each query index with `sample_u64_pow2(index_bits())`, and a one-row trace at blowup 2 makes that zero; the sampler's assert then fires deep inside emission naming neither the table nor which side of the tree it came from, which is how it reached box A as a bare "got 0". The pre-flight names the sub-proof and prints the shallowest shape on both the inner-epoch and the wrap-child side, so the next run attributes it instead of reporting it. It is a diagnostic, not a fix: if it fires the shape is real. --- prover/src/lfm/epoch_tests.rs | 14 ++++- prover/src/lfm/per_table_aggregator_tests.rs | 54 +++++++++++++++++++- 2 files changed, 66 insertions(+), 2 deletions(-) diff --git a/prover/src/lfm/epoch_tests.rs b/prover/src/lfm/epoch_tests.rs index e32b4f472..e9ebd802e 100644 --- a/prover/src/lfm/epoch_tests.rs +++ b/prover/src/lfm/epoch_tests.rs @@ -2154,7 +2154,19 @@ fn the_epoch_challenge_spine_matches_production() { `program_id_from_digest` over the same inputs" ); - let mut cursor = 4usize; + // The pair, the two attestation-id words, then the BLOCK-BINDING SCHEMA — + // skipped by NAME, never by a literal. + // + // ⚠ `epoch_challenge_program` is `epoch_program(e, false)`, the SAME emitter + // with the legs off — the doc on `epoch_program` says so, and says why: a + // second copy of the spine would be a place for the assembled verifier's + // Fiat-Shamir to drift from the one this test checks. So every publish the + // assembled verifier gained, this spine gained too. A literal 4 here read + // register INIT slot 0 as `beta of table 0`, and since x0 is hard-wired zero + // the failure printed an all-zero challenge — which reads like a challenge + // that was never derived rather than like a cursor pointing at the wrong + // field. + let mut cursor = 4 + schema_words(&e); let mut multi_row_ood = 0; for (i, h) in e.tables.iter().enumerate() { assert_eq!(pub_ext(cursor), h.beta, "beta of table {i}"); diff --git a/prover/src/lfm/per_table_aggregator_tests.rs b/prover/src/lfm/per_table_aggregator_tests.rs index 058972eb0..b710e636c 100644 --- a/prover/src/lfm/per_table_aggregator_tests.rs +++ b/prover/src/lfm/per_table_aggregator_tests.rs @@ -958,6 +958,46 @@ pub(super) fn node_program( compile(b.finish()) } +/// Name any sub-proof whose query sampler would be handed a zero bit width, +/// BEFORE emission reaches it. +/// +/// `epoch::emit_table_challenges` samples each query index with +/// `sample_u64_pow2(shape.index_bits())`, and `index_bits()` is +/// `log2_trace_length + log2_blowup - 1`. A one-row trace at blowup 2 makes that +/// ZERO, and the sampler's own assert then fires deep inside emission with no +/// idea which table or which side of the tree it came from — which is exactly +/// how it surfaced on box A: a bare "nbits must be in 1..=32, got 0" with +/// nothing to attach it to. +/// +/// A diagnostic, not a fix. If it fires, the shape is real and the question is +/// whether a one-row sub-proof should exist at all at this preset. +fn assert_samplable(label: &str, shapes: &[&super::epoch::TableChallengeShape]) { + for (i, s) in shapes.iter().enumerate() { + let lde = s.log2_trace_length + s.log2_blowup; + assert!( + lde >= 1, + "{label} sub-proof {i}: log2_trace {} + log2_blowup {} = {lde}, so \ + index_bits() would be {} — the query sampler needs at least one bit", + s.log2_trace_length, + s.log2_blowup, + lde as i64 - 1, + ); + } + let worst = shapes + .iter() + .enumerate() + .min_by_key(|(_, s)| s.log2_trace_length + s.log2_blowup) + .expect("a proof has sub-proofs"); + println!( + " {label}: {} sub-proofs, shallowest is #{} at log2_trace {} + log2_blowup {} = {} index bits", + shapes.len(), + worst.0, + worst.1.log2_trace_length, + worst.1.log2_blowup, + worst.1.index_bits(), + ); +} + /// ★ THE LEAF NODE RUNS — the first aggregation node over real per-table wrap /// proofs. /// @@ -1022,6 +1062,12 @@ fn the_leaf_node_verifies_and_binds_two_wraps() { super::epoch_tests::real_epoch_from_continuation(&inner, &elf_bytes, &bundle, k, None) .expect("every epoch must reconstruct from proofs alone"); let out_halves = e.statement.public_output_len.div_ceil(4); + // Pre-flight: the wrap program emits one query sampler per INNER + // sub-proof, so a shape it cannot sample must be named here rather than + // deep inside `epoch_program_publishing`. + let inner_shapes: Vec<&super::epoch::TableChallengeShape> = + e.tables.iter().map(|h| &h.shape).collect(); + assert_samplable(&format!("inner epoch {k}"), &inner_shapes); let program = super::epoch_tests::epoch_program_publishing(&e, true, Publishes::Aggregation); let arenas = super::epoch_tests::epoch_arena_words(&e, true); @@ -1047,7 +1093,13 @@ fn the_leaf_node_verifies_and_binds_two_wraps() { children[0].tables.len(), ); - // ---- the node. + // ---- the node. Same pre-flight on the CHILD side, so a zero bit width is + // attributed to the wrap's own sub-proofs rather than to the inner epoch's. + for (k, c) in children.iter().enumerate() { + let shapes: Vec<&super::epoch::TableChallengeShape> = + c.tables.iter().map(|h| &h.shape).collect(); + assert_samplable(&format!("child {k} (a wrap proof)"), &shapes); + } let arenas: Vec> = children.iter().flat_map(child_arena_words).collect(); let node_layout = SchemaLayout::node(layouts[FAN_IN - 1].out_halves); From d2d3006cefcd3bf929c8c802e4af4d9f75dc09ce Mon Sep 17 00:00:00 2001 From: MauroFab Date: Tue, 8 Sep 2026 16:30:23 -0300 Subject: [PATCH 11/17] fix(lfm): a one-row table's query draw is legal, and it consumes MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The emitted verifier could not be built over a legal continuation epoch. A one-row trace at blowup 2 has a two-leaf LDE, so production samples `sample_u64(domain_size >> 1)` = `sample_u64(1)` for each of that table's queries, and `sample_u64_pow2` refused the corresponding `nbits = 0` outright. Found by the leaf-node gate at inner epoch 1's sub-proof #10; `emit_table_challenges` and `sample_u64_pow2` are untouched by every other commit on this branch, so this is a latent defect on the tip. The obvious fix would have been the bug. "One index, so skip the sample" is wrong: production does NOT skip it. The byte arm's threshold is `1u64.wrapping_neg() % 1 = 0`, so `next_sample_u64()` runs once and advances `out_pos`; the pinned algebraic arm squeezes a cell and only then masks with `& (upper_bound - 1)`. An emitter that skipped would be one squeeze short for that table and every challenge after it in that fork would diverge. Both emitted arms already consume before reading `nbits` — `squeeze_bits` calls `squeeze_cell` first, the byte arm calls `next_candidate` first — so letting zero through is the whole change. The lower bound was unjustified: the assert message and the doc paragraph both justify only `<= 32`. Every downstream consumer degenerates correctly, checked rather than assumed: `point_factors(1)` is empty and matches the empty bit vector, `pow_bits` over no bits returns the coset offset (which IS the query point for a two-leaf domain), and `merkle_depth + 1 == log2_lde_length` makes the depth zero, so the leaf hash is the root — correct for a one-pair tree. ⚠ The gate is not "the panic is gone". A consumption desync here is invisible to a value differential: every index is 0 whether the draw happened or not, and `iota_bits` is the last thing sampled in that fork, so nothing later disagrees either. The new test samples an extension element AFTER the zero-bit draw on both sides and compares against the HOST's — the only observable that moves if the squeeze is missing. --- prover/src/lfm/per_table_aggregator_tests.rs | 66 ++++++++++++++++++++ prover/src/lfm/transcript_replay.rs | 35 ++++++++++- 2 files changed, 99 insertions(+), 2 deletions(-) diff --git a/prover/src/lfm/per_table_aggregator_tests.rs b/prover/src/lfm/per_table_aggregator_tests.rs index b710e636c..0dcb835cf 100644 --- a/prover/src/lfm/per_table_aggregator_tests.rs +++ b/prover/src/lfm/per_table_aggregator_tests.rs @@ -1232,3 +1232,69 @@ fn the_leaf_node_verifies_and_binds_two_wraps() { println!(" ✓ tamper arm: {name} rejected"); } } + +/// ★ A ZERO-BIT QUERY DRAW CONSUMES WHAT THE HOST CONSUMES. +/// +/// # The defect this holds shut +/// +/// A one-row trace at blowup 2 has a two-leaf LDE, so production's +/// `sample_query_indexes` calls `sample_u64(domain_size >> 1)` = `sample_u64(1)` +/// for every query of that table. Both host transcripts CONSUME before masking — +/// the byte arm draws one `next_sample_u64()`, the pinned algebraic arm squeezes +/// a cell — and return index 0. The emitted sampler refused `nbits = 0` outright, +/// so the epoch verifier could not be built over such an epoch at all; that is +/// what `the_leaf_node_verifies_and_binds_two_wraps` hit on box A, at inner epoch +/// 1's sub-proof #10. +/// +/// # Why the obvious fix would have been the bug +/// +/// "One index, so skip the sample" is wrong: the host does not skip it. An +/// emitter that skipped would be one squeeze short for that table and every +/// challenge after it in that fork would diverge. +/// +/// # Why this test needs the follow-up draw +/// +/// ⚠ A consumption desync here is invisible to a value differential ON the +/// table: every index is 0 whether the draw happened or not, and `iota_bits` is +/// the LAST thing `epoch::emit_table_challenges` samples, so nothing later in +/// that fork disagrees either. A green leaf test therefore proves nothing about +/// consumption — it proves only that no panic fired. +/// +/// So this samples an extension element AFTER the zero-bit draw on both sides. +/// That element is the single observable that differs if the squeeze is missing, +/// and comparing it against the HOST's is what makes this emitter-host agreement +/// rather than emitter self-consistency. +/// +/// ⓘ It lives here because lane A owns `transcript_replay.rs` only for this fix; +/// its natural home is beside the other transcript differentials. +#[test] +fn a_zero_bit_query_draw_consumes_what_the_host_does() { + use crypto::fiat_shamir::is_transcript::IsTranscript; + + const SEED: &[u8] = b"lane-A zero-bit query draw v0"; + + // ---- the HOST, exactly as `sample_query_indexes` drives it at a one-row + // table: one `sample_u64(1)`, then the next thing the transcript would give. + let mut host = crate::hash_pin::block_transcript(SEED); + let index = host.sample_u64(1); + assert_eq!(index, 0, "a two-leaf domain has exactly one query index"); + let host_after: FEE = host.sample_field_element(); + + // ---- the EMITTER, same seed, same sequence. + let mut b = LfmBuilder::new().with_wrap_hash(super::edsl::WrapHash::production()); + let mut t = TranscriptReplay::new(SEED); + let bits = t.sample_u64_pow2(&mut b, 0); + assert!(bits.is_empty(), "a zero-bit draw yields no bits"); + let after = t.sample_ext(&mut b); + b.public(after.as_cell()); + let program = compile(b.finish()); + let exec = execute(&program, &[], &crate::hash_pin::BLOCK_HASHER) + .expect("a zero-bit query draw must emit and execute"); + + assert_eq!( + super::word::word_as_ext(&exec.public_words[0].1).expect("an ext"), + host_after, + "the draw AFTER a zero-bit query index must equal the host's — if the \ + emitter skipped the squeeze, this is the ONLY place it shows" + ); +} diff --git a/prover/src/lfm/transcript_replay.rs b/prover/src/lfm/transcript_replay.rs index eebe77d5b..b77cdde44 100644 --- a/prover/src/lfm/transcript_replay.rs +++ b/prover/src/lfm/transcript_replay.rs @@ -786,10 +786,41 @@ impl TranscriptReplay { /// `nbits ≤ 32` keeps the answer inside the candidate's low half. The bound /// is real rather than defensive: FRI query indices are bounded by the LDE /// domain, which is ≤ 2^25 here. + /// + /// ## `nbits = 0` is legal, and it still CONSUMES + /// + /// A one-row trace at blowup 2 has a two-leaf LDE, so `sample_query_indexes` + /// calls `sample_u64(domain_size >> 1)` = `sample_u64(1)`: one pair, one + /// index, and that index is 0. Production does not skip the draw for it. + /// + /// - `DefaultTranscript::sample_u64` computes + /// `threshold = 1u64.wrapping_neg() % 1 = 0`, so the loop calls + /// `next_sample_u64()` ONCE — advancing `out_pos` by eight — and returns + /// `candidate % 1 = 0`. + /// - `AlgebraicTranscript::sample_u64`, the PINNED path, squeezes a cell and + /// then masks: `squeeze_cell()`, then `canonical(c[0]) & (upper_bound − 1)`. + /// The squeeze happens first and unconditionally; `& 0` is what yields 0. + /// + /// So an emitter that skipped the draw would be one squeeze short of the host + /// for that table, and every challenge after it in that fork would diverge. + /// Both arms below already consume BEFORE reading `nbits` — + /// `SpongeVar::squeeze_bits` calls `squeeze_cell` first, and the byte arm + /// calls `next_candidate` first — so zero bits needs no special case beyond + /// letting it through. The resulting `bit_dec(_, 0)` is a well-formed row + /// that exposes no bits; it is left unspecial-cased on purpose, because the + /// smallest correct change is the right one in a Fiat–Shamir file. + /// + /// ⚠ A desync here is INVISIBLE to a value differential on the table itself: + /// every index is 0 whether the draw happened or not, and `iota_bits` is the + /// last thing `epoch::emit_table_challenges` samples, so nothing downstream + /// in that fork would disagree either. The gate that holds this is + /// `per_table_aggregator_tests::a_zero_bit_query_draw_consumes_what_the_host_does`, + /// which samples an extension element AFTER the zero-bit draw on both sides — + /// the only place the missing squeeze shows up. pub fn sample_u64_pow2(&mut self, b: &mut LfmBuilder, nbits: usize) -> Vec { assert!( - (1..=32).contains(&nbits), - "sample_u64_pow2: nbits must be in 1..=32, got {nbits} — above 32 the \ + nbits <= 32, + "sample_u64_pow2: nbits must be at most 32, got {nbits} — above 32 the \ answer would span both halves of the candidate" ); let Some(h) = b.wrap_hash().byte_hash() else { From 84d8cb090884aa0fd5df7124390c149f8e222501 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Tue, 8 Sep 2026 16:53:07 -0300 Subject: [PATCH 12/17] feat(lfm): the inner node, and the L2G asymmetry building it found MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A node whose children are NODE proofs. The emitter needed no change — a child is a plain per-table MultiProof whichever level produced it, so `real_child` reads a node's proof exactly as it reads a wrap's — which is what "the same emitter serves every level" means operationally. ★ Building the arm found a real bug in the leaf work. A node published its L2G fold as digest CELLS (four lanes in one word) while a wrap publishes its root as lanes (one lane per word), and `emit_node_publishes` reads `lanes[0]` of each published l2g word. A node child would have handed ONE felt to `digest_from_lanes` where four are required — the inner node could not have been built. Fixed by publishing the fold in the wrap's own shape, so both layouts read alike; the asymmetry is removed rather than parameterised. Three things the leaf gate could not reach are exercised here: the node layout rather than the wrap layout, a label RANGE per child (each leaf carries its subtree's two ends, and pinning both is what makes contiguity across sibling subtrees a consequence of the pins), and the fold COMPOSING — each leaf folded its own wraps' roots and the inner node folds those folds. A single-child node folds to identity, so this needs two real leaves. The epoch requirement is asserted, not worked around: a two-level tree at fan-in N needs N^2 epochs, and padding would mean a pad child with no epoch to belong to, breaking the register chain and the label pin — the same trade already rejected when the tree shape was priced. The closing assertion is the composition property itself: an inner node's published schema has the same total as its children's, which is what lets the level above use the identical emitter. --- prover/src/lfm/per_table_aggregator.rs | 18 +- prover/src/lfm/per_table_aggregator_tests.rs | 178 +++++++++++++++++++ 2 files changed, 194 insertions(+), 2 deletions(-) diff --git a/prover/src/lfm/per_table_aggregator.rs b/prover/src/lfm/per_table_aggregator.rs index 9dbbb62f0..1eef5769d 100644 --- a/prover/src/lfm/per_table_aggregator.rs +++ b/prover/src/lfm/per_table_aggregator.rs @@ -477,7 +477,18 @@ impl SchemaLayout { num_reg: crate::tables::register::NUM_REGISTER_ADDRESSES, label_words: 4, out_halves, - l2g_words: super::proof_arena::words_per_root(), + // ★ THE SAME SHAPE A WRAP PUBLISHES ITS ROOT IN — `lanes_per_root` + // base words, one lane each — not the fold's digest CELLS. + // + // Publishing cells would have been one word instead of four, and it + // would have made a node child and a wrap child structurally + // different to read: `emit_node_publishes` takes `lanes[0]` of each + // published l2g word, which is right for a wrap's lane-per-word + // layout and silently wrong for a four-lane digest word — it would + // hand ONE felt to `digest_from_lanes` where four are required. + // Building the inner-node arm is what surfaced that; the asymmetry + // is removed here rather than parameterised around. + l2g_words: super::proof_arena::lanes_per_root(), tail: 0, } } @@ -763,8 +774,11 @@ pub fn emit_node_publishes(b: &mut LfmBuilder, p: &NodePublishes<'_>) { }) .collect(); let folded = fold_l2g(b, &digests); + // Unpacked to lanes, so a node's L2G item reads exactly like a wrap's. for cell in folded.cells() { - b.public(*cell); + for lane in b.unpack(*cell) { + b.public(lane.as_cell()); + } } } diff --git a/prover/src/lfm/per_table_aggregator_tests.rs b/prover/src/lfm/per_table_aggregator_tests.rs index 0dcb835cf..f1a0bdedd 100644 --- a/prover/src/lfm/per_table_aggregator_tests.rs +++ b/prover/src/lfm/per_table_aggregator_tests.rs @@ -1298,3 +1298,181 @@ fn a_zero_bit_query_draw_consumes_what_the_host_does() { emitter skipped the squeeze, this is the ONLY place it shows" ); } + +/// Prove one aggregation node and hand it back as a CHILD of the next level. +/// +/// The whole composition argument in one function: a node's proof is a plain +/// per-table `MultiProof`, so `real_child` reads it exactly as it reads a wrap's, +/// and the layout that describes it is `SchemaLayout::node`. Nothing about the +/// level appears here — which is what "the same emitter serves every level" +/// means operationally. +fn prove_node_as_child( + children: &[RealChild], + layouts: &[super::per_table_aggregator::SchemaLayout], + labels: &[&[u64]], + label_range: (u64, u64), + out_halves: usize, + opts: &crate::ProofOptions, +) -> (RealChild, super::per_table_aggregator::SchemaLayout) { + use super::per_table_aggregator::{NodePublishSet, SchemaLayout}; + + let program = node_program( + children, + layouts, + labels, + label_range, + NodePublishSet::Aggregation, + ); + let arenas: Vec> = children.iter().flat_map(child_arena_words).collect(); + let artifacts = + super::registry::build_artifacts_with_hasher(&program, opts, crate::hash_pin::BLOCK_HASHER); + let proved = super::proof::lfm_prove(&program, &artifacts, &arenas, opts) + .expect("an aggregation node must prove"); + let layout = SchemaLayout::node(out_halves); + layout.assert_covers(proved.public_words.len()); + (real_child(artifacts, opts.clone(), &proved), layout) +} + +/// ★ THE INNER NODE — a node whose children are NODE proofs. +/// +/// # What this adds over the leaf gate +/// +/// The leaf verifies wraps; this verifies leaves. Three things differ and each +/// is exercised here for the first time: +/// +/// 1. **`SchemaLayout::node`** rather than `::wrap` — a different head (a node +/// has FAN_IN Phase A's and so no single `(z, α)`), a four-word label run +/// rather than two, and no trailing bus total. +/// 2. **A label RANGE per child**: each leaf carries the first and last label of +/// its subtree, and the inner node pins both ends of both. That is what makes +/// contiguity across sibling subtrees a consequence of the pins rather than a +/// separate check. +/// 3. **The L2G fold composing**: each leaf published a fold over ITS wraps' +/// roots, and the inner node folds those two folds. A single-child node folds +/// to identity and would not exercise `hash_pair` at this level, which is why +/// this needs two real leaves rather than one. +/// +/// ⚠ Building this arm is what found the bug it now covers: a node used to +/// publish its fold as digest CELLS (four lanes in one word) while a wrap +/// publishes its root as lanes (one lane per word), and `emit_node_publishes` +/// reads `lanes[0]` of each published l2g word. A node child would have handed +/// ONE felt to `digest_from_lanes` where four are required. The fix removed the +/// asymmetry rather than parameterising it, so both layouts now read alike. +/// +/// # Cost, and why the epoch requirement is asserted rather than worked around +/// +/// A two-level tree at fan-in N needs N² epochs: N wraps per leaf, N leaves. +/// Padding the shortfall would mean a pad child with no epoch to belong to, +/// which breaks the register chain and the label pin — the same trade rejected +/// when the tree shape was priced. So this asserts the fixture is deep enough +/// and names the number if it is not. +#[test] +#[ignore = "box tier: proves FAN_IN^2 wraps, FAN_IN leaf nodes and one inner node"] +fn the_inner_node_verifies_two_leaf_nodes() { + use super::epoch_tests::Publishes; + use super::per_table_aggregator::{FAN_IN, SchemaLayout}; + use super::proof::lfm_prove; + use super::registry::build_artifacts_with_hasher; + use std::time::Instant; + + let elf_bytes = super::proof_fixture::read_inner_elf(); + let inner = super::proof_fixture::fixture_options(); + let bundle = crate::continuation::prove_continuation( + &elf_bytes, + &[], + super::proof_fixture::FIXTURE_EPOCH_LOG2, + &inner, + ) + .expect("the fixture continuation must prove"); + let needed = FAN_IN * FAN_IN; + assert!( + bundle.num_epochs() >= needed, + "a two-level fan-in-{FAN_IN} tree needs {needed} epochs, the fixture has {}. \ + Raise FIXTURE_EPOCH_LOG2 or use a longer guest — do NOT pad, a pad child \ + belongs to no epoch and breaks the register chain and the label pin", + bundle.num_epochs() + ); + + let wrap_opts = super::proof::aggregation_wrap_options(); + let label_of = |k: usize| crate::tables::local_to_global::epoch_label(k as u64); + + // ---- level 0: one wrap per epoch, then level 1: one leaf per FAN_IN wraps. + let t = Instant::now(); + let mut leaves = Vec::with_capacity(FAN_IN); + let mut leaf_layouts = Vec::with_capacity(FAN_IN); + let mut leaf_labels: Vec<[u64; 2]> = Vec::with_capacity(FAN_IN); + for leaf in 0..FAN_IN { + let mut wraps = Vec::with_capacity(FAN_IN); + let mut wrap_layouts = Vec::with_capacity(FAN_IN); + let mut wrap_labels: Vec<[u64; 1]> = Vec::with_capacity(FAN_IN); + let mut out_halves = 0usize; + for i in 0..FAN_IN { + let k = leaf * FAN_IN + i; + let e = super::epoch_tests::real_epoch_from_continuation( + &inner, &elf_bytes, &bundle, k, None, + ) + .expect("every epoch must reconstruct from proofs alone"); + out_halves = e.statement.public_output_len.div_ceil(4); + let program = + super::epoch_tests::epoch_program_publishing(&e, true, Publishes::Aggregation); + let arenas = super::epoch_tests::epoch_arena_words(&e, true); + let artifacts = + build_artifacts_with_hasher(&program, &wrap_opts, crate::hash_pin::BLOCK_HASHER); + let proved = lfm_prove(&program, &artifacts, &arenas, &wrap_opts) + .expect("the epoch wrap must prove"); + let layout = SchemaLayout::wrap(out_halves); + layout.assert_covers(proved.public_words.len()); + wrap_layouts.push(layout); + wrap_labels.push([label_of(k)]); + wraps.push(real_child(artifacts, wrap_opts.clone(), &proved)); + } + let refs: Vec<&[u64]> = wrap_labels.iter().map(|l| &l[..]).collect(); + let range = ( + label_of(leaf * FAN_IN), + label_of(leaf * FAN_IN + FAN_IN - 1), + ); + let (child, layout) = + prove_node_as_child(&wraps, &wrap_layouts, &refs, range, out_halves, &wrap_opts); + println!( + " leaf {leaf}: {} published words, {} sub-proofs", + child.public_words.len(), + child.tables.len() + ); + leaves.push(child); + leaf_layouts.push(layout); + leaf_labels.push([range.0, range.1]); + } + println!( + " {FAN_IN} leaf nodes over {needed} wraps in {:.1}s", + t.elapsed().as_secs_f64() + ); + + // ---- level 2: the inner node, over NODE proofs. + let refs: Vec<&[u64]> = leaf_labels.iter().map(|l| &l[..]).collect(); + let range = (leaf_labels[0][0], leaf_labels[FAN_IN - 1][1]); + let out_halves = leaf_layouts[FAN_IN - 1].out_halves; + let t = Instant::now(); + let (inner_node, inner_layout) = + prove_node_as_child(&leaves, &leaf_layouts, &refs, range, out_halves, &wrap_opts); + println!( + "\n★ INNER NODE PROVED AND VERIFIED (a node over {FAN_IN} NODE proofs)\n \ + prove+harvest {:.1}s\n {} published words, {} sub-proofs\n \ + schema {} + head {}\n peak RSS {:?} GiB", + t.elapsed().as_secs_f64(), + inner_node.public_words.len(), + inner_node.tables.len(), + inner_layout.schema_words(), + inner_layout.head, + super::wrap_tests::peak_rss_gib(), + ); + + // ---- the composition property, asserted rather than implied: an inner + // node's published schema has the SAME shape as its children's, which is + // what lets the level above it use the identical emitter. + assert_eq!( + inner_layout.total(), + leaf_layouts[0].total(), + "a node's published schema must not change with its level — that is what \ + makes the same emitter serve the level above" + ); +} From 0ccf9ae832c6525f2eecf91eac0e5e19911e2328 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Tue, 8 Sep 2026 17:00:19 -0300 Subject: [PATCH 13/17] fix(lfm): a one-leaf Merkle tree is a legal shape, and it still binds MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The panic moved downstream exactly as predicted: relaxing the query sampler's guard let emission reach `SubProofShape::check`, whose `merkle_depth >= 1` refused the same one-row table. A one-pair domain has a single leaf, so the tree has no levels and the LEAF HASH IS THE ROOT. Settled before touching the assert, and it is the reason this is safe: BOTH SIDES already handle depth 0 without a special case. The host's `verify_merkle_path_from_leaf_hash` loops over an empty path and returns `root_hash == hashed_value`; `emit_group_authentication` hashes the leaf, walks zero levels through `wrap_merkle_walk`, and asserts the result equals the committed root. So the walk at depth 0 is NOT a no-op — it is exactly the binding — and the assert refused a shape the code verifies correctly. Swept the rest of the path for other asserts predicated on a non-empty tree, as the last fix's lesson demands: `sub_proof.rs:364` compares bits against merkle_depth (0 == 0), and the remaining `> 0` asserts are about query counts, composition parts and frame step size, none of which depend on depth. This was the only one. That also closes the FRI question left open by reasoning: `terminal_log` is `(blowup_log + final_poly_log_degree).min(log2_lde_length)`, so at log2_lde = 1 it clamps to 1, `total_folds` is 0, and the FRI walk is vacuous by construction rather than by luck. ⚠ The gate's REJECTION arm is the load-bearing one. If relaxing the shape check had let the walk skip its root comparison, the honest arm would still pass and only the rejection arm would fail. The root it compares against is the emitter's own leaf hash, whose agreement with the host backend is gated separately by algebraic_commit's leaf/parent differential — composing the two is what makes this emitter-versus-host rather than emitter-versus-itself. --- prover/src/lfm/per_table_aggregator_tests.rs | 115 +++++++++++++++++++ prover/src/lfm/sub_proof.rs | 24 +++- 2 files changed, 135 insertions(+), 4 deletions(-) diff --git a/prover/src/lfm/per_table_aggregator_tests.rs b/prover/src/lfm/per_table_aggregator_tests.rs index f1a0bdedd..7a172dc9e 100644 --- a/prover/src/lfm/per_table_aggregator_tests.rs +++ b/prover/src/lfm/per_table_aggregator_tests.rs @@ -1476,3 +1476,118 @@ fn the_inner_node_verifies_two_leaf_nodes() { makes the same emitter serve the level above" ); } + +/// ★ A DEPTH-ZERO MERKLE WALK STILL BINDS THE LEAF TO THE ROOT. +/// +/// # The shape +/// +/// A one-row trace at blowup 2 has a two-leaf LDE, one row PAIR, and therefore a +/// Merkle tree with a single leaf and no levels — the leaf hash IS the root. +/// `SubProofShape::check` refused it outright (`merkle_depth >= 1`), which is +/// what `the_leaf_node_verifies_and_binds_two_wraps` hit once the query sampler +/// stopped refusing zero index bits. +/// +/// # Why this is not "make the walk a no-op" +/// +/// It is not a no-op and must not become one. Both sides do the same thing at +/// depth 0 and neither needs a special case: +/// +/// - host `verify_merkle_path_from_leaf_hash` loops over an empty path and +/// returns `root_hash == hashed_value`; +/// - `emit_group_authentication` hashes the leaf, walks zero levels, and asserts +/// the result equals the committed root. +/// +/// The compare is the entire binding, and it survives. **The rejection arm below +/// is what proves that** — if relaxing the shape check had let the walk skip its +/// root comparison, the honest arm would still pass and only this one would fail. +/// +/// # Where the host enters +/// +/// The root is not invented here: it is the leaf hash the emitter itself +/// computes, and `emit_leaf_hash`'s agreement with the host's backend is gated +/// separately by `algebraic_commit`'s leaf/parent differential. Composing the two +/// is what makes this emitter-versus-host rather than emitter-versus-itself, and +/// it is stated rather than assumed because the composition is the argument. +#[test] +fn a_depth_zero_walk_still_binds_leaf_to_root() { + use super::sub_proof::{ + GroupCommitment, GroupOpening, GroupShape, emit_group_authentication, emit_leaf_hash, + }; + + const COLS: usize = 3; + let shape = GroupShape { + num_columns: COLS, + is_ext: false, + }; + let values: Vec = (0..shape.num_values() as u64) + .map(|i| FE::from(7 * i + 1)) + .collect(); + + // ---- the root, from the emitter's own leaf hash over those values. + let mut b = LfmBuilder::new().with_wrap_hash(super::edsl::WrapHash::production()); + let arena = b.declare_arena(shape.num_values() as u32); + let cells: Vec<_> = (0..shape.num_values() as u32) + .map(|i| b.hint_word(arena, i)) + .collect(); + let leaf = emit_leaf_hash(&mut b, shape, &cells); + for cell in leaf.cells() { + b.public(*cell); + } + let leaf_program = compile(b.finish()); + let leaf_arena: Vec = values.iter().map(|v| base_word(*v)).collect(); + let leaf_exec = execute( + &leaf_program, + std::slice::from_ref(&leaf_arena), + &crate::hash_pin::BLOCK_HASHER, + ) + .expect("the leaf hash must execute"); + let root_words: Vec = leaf_exec.public_words.iter().map(|(_, w)| *w).collect(); + + // ---- the authentication at depth ZERO: no bits, no siblings. + let build = || { + let mut b = LfmBuilder::new().with_wrap_hash(super::edsl::WrapHash::production()); + let a_vals = b.declare_arena(shape.num_values() as u32); + let a_root = b.declare_arena(root_words.len() as u32); + let vals: Vec<_> = (0..shape.num_values() as u32) + .map(|i| b.hint_word(a_vals, i)) + .collect(); + let commitment = GroupCommitment::hint(&mut b, a_root, 0, shape); + emit_group_authentication( + &mut b, + &commitment, + &GroupOpening { + values: vals, + siblings: Vec::new(), + }, + &[], + ); + compile(b.finish()) + }; + let program = build(); + + // ---- the honest arm: the leaf hash IS the root, so this must execute. + execute( + &program, + &[leaf_arena.clone(), root_words.clone()], + &crate::hash_pin::BLOCK_HASHER, + ) + .expect("★ a one-leaf tree must authenticate against its own leaf hash"); + + // ---- ★ THE REJECTION ARM — the one that proves the compare survives. + let mut wrong = root_words.clone(); + wrong[0][0] += FE::one(); + assert!( + execute( + &program, + &[leaf_arena, wrong], + &crate::hash_pin::BLOCK_HASHER + ) + .is_err(), + "a depth-zero walk must still REJECT a root that is not the leaf hash — \ + if this passes, the walk stopped binding and the honest arm proves nothing" + ); + println!( + " ✓ depth-0 walk: {} column pair binds to its root, and a moved root is rejected", + COLS + ); +} diff --git a/prover/src/lfm/sub_proof.rs b/prover/src/lfm/sub_proof.rs index 663441405..d11cce3c6 100644 --- a/prover/src/lfm/sub_proof.rs +++ b/prover/src/lfm/sub_proof.rs @@ -173,10 +173,26 @@ impl SubProofShape { self.merkle_depth, self.log2_lde_length ); - assert!( - self.merkle_depth >= 1, - "a tree with no levels has no path to walk" - ); + // ⚠ NO `merkle_depth >= 1`. A ONE-PAIR domain — a one-row trace at blowup + // 2 — has a single leaf, so the tree has no levels and the LEAF HASH IS + // THE ROOT. That is a legitimate degenerate shape, and both sides already + // handle it without a special case: + // + // · the host's `verify_merkle_path_from_leaf_hash` loops over an empty + // path and returns `root_hash == hashed_value`; + // · `emit_group_authentication` hashes the leaf, walks zero levels, and + // asserts the result equals the committed root. + // + // So the walk at depth 0 is NOT a no-op — it is exactly the binding, and + // the old assert refused a shape the code below verifies correctly. It + // read "a tree with no levels has no path to walk", which is true and + // beside the point: there is no path, none is walked, and the leaf-versus + // -root compare still happens. + // + // Found by the leaf-node gate at a real continuation epoch's sub-proof + // #10; gated by + // `per_table_aggregator_tests::a_depth_zero_walk_still_binds_leaf_to_root`, + // whose REJECTION arm is what proves the compare survives. } } From e666d8317cd23dd89fba596f10dd8ecc4acaef07 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Tue, 8 Sep 2026 17:25:30 -0300 Subject: [PATCH 14/17] test(lfm): a local epoch size for the inner node, and per-phase RSS MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two changes, both about not letting one number stand for several things. The inner-node gate needs FAN_IN^2 epochs and the shared FIXTURE_EPOCH_LOG2 selects two. `epoch_size_log2` is a PARAMETER of `prove_continuation` with a floor of 2, so this passes a smaller one locally instead of shrinking the shared constant. The nine gates that already run green against that constant keep their baseline; nothing is re-baselined to give one test more epochs. Smaller epochs mean shallower tables, which is exactly where the two degenerate shapes were found, so the cheap place to find a third is here. And the leaf gate now prints the RSS high-water mark at each phase boundary. `peak_rss_gib` is VmHWM: a PROCESS mark that only rises, so a single figure at the end spans the wrap proves, the diagnostic arm and the node prove alike — three proves and a 6.7M-instruction program that production never emits, in one process. The run's 40.6 GiB is that conflation, not the node's peak. Per-boundary readings bound each phase instead: the node's own prove costs at most the rise from the last mark before it. --- prover/src/lfm/per_table_aggregator_tests.rs | 48 ++++++++++++++------ 1 file changed, 35 insertions(+), 13 deletions(-) diff --git a/prover/src/lfm/per_table_aggregator_tests.rs b/prover/src/lfm/per_table_aggregator_tests.rs index 7a172dc9e..b7630eb22 100644 --- a/prover/src/lfm/per_table_aggregator_tests.rs +++ b/prover/src/lfm/per_table_aggregator_tests.rs @@ -1087,10 +1087,11 @@ fn the_leaf_node_verifies_and_binds_two_wraps() { let label_range = (labels[0][0], labels[FAN_IN - 1][0]); println!( " {FAN_IN} epoch wraps proved in {:.1}s, {} published words each, \ - {} sub-proofs each", + {} sub-proofs each\n RSS high-water AFTER the wrap proves: {:?} GiB", t.elapsed().as_secs_f64(), children[0].public_words.len(), children[0].tables.len(), + super::wrap_tests::peak_rss_gib(), ); // ---- the node. Same pre-flight on the CHILD side, so a zero bit width is @@ -1141,9 +1142,10 @@ fn the_leaf_node_verifies_and_binds_two_wraps() { } println!( " ✓ differential: every leg reaches its child's OWN (z, alpha) \ - ({:.1}s, {} instructions)", + ({:.1}s, {} instructions)\n RSS high-water AFTER the diagnostic arm: {:?} GiB", t.elapsed().as_secs_f64(), - diagnostic.instrs.len() + diagnostic.instrs.len(), + super::wrap_tests::peak_rss_gib(), ); // ---- the node a parent would verify. @@ -1172,6 +1174,15 @@ fn the_leaf_node_verifies_and_binds_two_wraps() { node_layout.schema_words(), node_layout.head, ); + // ★ The reading the fan-in arithmetic needs. `peak_rss_gib` is `VmHWM`, a + // PROCESS high-water mark that only ever rises, so the run's final figure + // spans the wrap proves, the diagnostic arm and the node alike. Printing it + // at each boundary turns one conflated number into a bound per phase: what + // the node's own prove costs is at most the rise from here. + println!( + " RSS high-water BEFORE the node prove: {:?} GiB", + super::wrap_tests::peak_rss_gib() + ); // ---- the node's own proof, so the level above has something to verify. let artifacts = @@ -1377,19 +1388,30 @@ fn the_inner_node_verifies_two_leaf_nodes() { let elf_bytes = super::proof_fixture::read_inner_elf(); let inner = super::proof_fixture::fixture_options(); - let bundle = crate::continuation::prove_continuation( - &elf_bytes, - &[], - super::proof_fixture::FIXTURE_EPOCH_LOG2, - &inner, - ) - .expect("the fixture continuation must prove"); + // ★ A LOCAL epoch size, NOT the shared `FIXTURE_EPOCH_LOG2`. + // + // A two-level tree needs FAN_IN^2 epochs and the shared constant selects two. + // `epoch_size_log2` is a PARAMETER of `prove_continuation` (floor 2), so a + // smaller epoch here yields more of them from the same guest without moving + // the ground under the nine gates that already run against the shared + // constant — every one of which would otherwise be re-baselined by a change + // whose only purpose is to give THIS test more epochs. + // + // ⚠ Smaller epochs mean shallower tables, which is where the degenerate + // shapes live. That is a feature: the one-row sub-proof and the one-leaf + // Merkle tree were both found this way, and both are now gated in + // milliseconds. If a third appears, it is a shape the emitter has to handle + // and this is the cheapest place to find it. + let epoch_log2 = super::proof_fixture::FIXTURE_EPOCH_LOG2 - 1; + let bundle = crate::continuation::prove_continuation(&elf_bytes, &[], epoch_log2, &inner) + .expect("the fixture continuation must prove"); let needed = FAN_IN * FAN_IN; assert!( bundle.num_epochs() >= needed, - "a two-level fan-in-{FAN_IN} tree needs {needed} epochs, the fixture has {}. \ - Raise FIXTURE_EPOCH_LOG2 or use a longer guest — do NOT pad, a pad child \ - belongs to no epoch and breaks the register chain and the label pin", + "a two-level fan-in-{FAN_IN} tree needs {needed} epochs; at epoch_log2 \ + {epoch_log2} this guest gives {}. Lower `epoch_log2` further (its floor is \ + 2) or use a longer guest — do NOT pad, a pad child belongs to no epoch \ + and breaks the register chain and the label pin", bundle.num_epochs() ); From efa4c40a7364ae3aadd4a1581ff20c02f5b705fd Mon Sep 17 00:00:00 2001 From: MauroFab Date: Tue, 8 Sep 2026 18:01:18 -0300 Subject: [PATCH 15/17] test(lfm): split the node's RSS mark, and print the floor beside it MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The single "before the node prove" mark was taken before `build_artifacts_with_hasher`, which is not bookkeeping: it runs `lde_columns` + `commit_lde_columns` over every chip group and builds the prep round, a full commitment pass over the program. So the +35.25 GiB that run attributed to "the node prove" actually brackets the artifact build AND the prove together and cannot say which costs what. Three marks now split artifacts, prove and verify. And the census is printed beside the measurement so the two are never quoted apart. The empty LFM machine costs 26,482,828 base-field-equivalent cells — the 0-word row of the cost instrument — against this node's 35,244,192. So 75% of a fixture node's census is the machine's padding FLOOR and only 25% is verification work, which is why a fixture node and a production node are not on the same part of the curve and why the affine RSS law reading 8x optimistic here does not transfer to either direction without a node measured where the linear term dominates. --- prover/src/lfm/per_table_aggregator_tests.rs | 36 ++++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/prover/src/lfm/per_table_aggregator_tests.rs b/prover/src/lfm/per_table_aggregator_tests.rs index b7630eb22..74ecd6625 100644 --- a/prover/src/lfm/per_table_aggregator_tests.rs +++ b/prover/src/lfm/per_table_aggregator_tests.rs @@ -1185,12 +1185,48 @@ fn the_leaf_node_verifies_and_binds_two_wraps() { ); // ---- the node's own proof, so the level above has something to verify. + // + // ⚠ THREE marks, not one. The mark above is taken BEFORE + // `build_artifacts_with_hasher`, which is not a bookkeeping call: it runs + // `lde_columns` + `commit_lde_columns` over every chip group and builds the + // prep round — a full commitment pass over the whole program. So a single + // "before the prove" mark brackets the artifact build and the prove TOGETHER + // and cannot say which of them costs what. These split it. + let t = Instant::now(); let artifacts = build_artifacts_with_hasher(&program, &wrap_opts, crate::hash_pin::BLOCK_HASHER); + println!( + " RSS high-water AFTER build_artifacts ({:.1}s): {:?} GiB", + t.elapsed().as_secs_f64(), + super::wrap_tests::peak_rss_gib() + ); let t = Instant::now(); let proved = lfm_prove(&program, &artifacts, &arenas, &wrap_opts).expect("★ THE LEAF NODE MUST PROVE"); let prove_secs = t.elapsed().as_secs_f64(); + println!( + " RSS high-water AFTER lfm_prove: {:?} GiB", + super::wrap_tests::peak_rss_gib() + ); + // ★ The census beside the measurement, so the two are never quoted apart. + // The empty LFM machine costs 26,482,828 base-field-equivalent cells — the + // 0-word row of `the_node_cost_model_is_measured` — so at fixture scale most + // of a node's census is the machine's padding FLOOR rather than its + // verification work, and a fixture node sits on a different part of the curve + // from a production one. + { + let (main, aux) = + super::airs::lfm_cell_counts_with_hasher(&program, crate::hash_pin::BLOCK_HASHER); + let cells = main + 3 * aux; + const EMPTY_MACHINE_CELLS: u64 = 26_482_828; + println!( + " node census: {cells} cells, of which {} are the empty machine's \ + floor ({:.0}%) and {} are verification work", + EMPTY_MACHINE_CELLS, + 100.0 * EMPTY_MACHINE_CELLS as f64 / cells as f64, + cells.saturating_sub(EMPTY_MACHINE_CELLS), + ); + } let t = Instant::now(); assert!( super::proof::verify_against_artifacts( From 68aae7e82b938be84febdc6012403316abbf891d Mon Sep 17 00:00:00 2001 From: MauroFab Date: Tue, 8 Sep 2026 18:08:07 -0300 Subject: [PATCH 16/17] test(lfm): per-level RSS marks, so flatness is a within-run comparison One gate's peak against another's cannot settle whether node cost grows per level. The leaf gate runs at FIXTURE_EPOCH_LOG2 and the inner gate at FIXTURE_EPOCH_LOG2 - 1, so their nodes sit over different-sized epochs and their peaks describe different workloads. Only levels measured inside ONE run are comparable, and `prove_node_as_child` is where every level's prove happens, so the mark goes there and every node reports its own. --- prover/src/lfm/per_table_aggregator_tests.rs | 34 +++++++++++++++++--- 1 file changed, 30 insertions(+), 4 deletions(-) diff --git a/prover/src/lfm/per_table_aggregator_tests.rs b/prover/src/lfm/per_table_aggregator_tests.rs index 74ecd6625..460eebeaa 100644 --- a/prover/src/lfm/per_table_aggregator_tests.rs +++ b/prover/src/lfm/per_table_aggregator_tests.rs @@ -1353,7 +1353,9 @@ fn a_zero_bit_query_draw_consumes_what_the_host_does() { /// and the layout that describes it is `SchemaLayout::node`. Nothing about the /// level appears here — which is what "the same emitter serves every level" /// means operationally. +#[allow(clippy::too_many_arguments)] fn prove_node_as_child( + label: &str, children: &[RealChild], layouts: &[super::per_table_aggregator::SchemaLayout], labels: &[&[u64]], @@ -1375,6 +1377,16 @@ fn prove_node_as_child( super::registry::build_artifacts_with_hasher(&program, opts, crate::hash_pin::BLOCK_HASHER); let proved = super::proof::lfm_prove(&program, &artifacts, &arenas, opts) .expect("an aggregation node must prove"); + // ★ PER-LEVEL marks, so flatness is a WITHIN-RUN comparison. One gate's peak + // against another's cannot settle it: the leaf gate runs at + // FIXTURE_EPOCH_LOG2 and this one at FIXTURE_EPOCH_LOG2 - 1, so their nodes + // sit over different-sized epochs. Only levels measured inside ONE run are + // comparable, and this is what makes that comparison possible. + println!( + " RSS high-water AFTER proving {label}: {:?} GiB ({} instructions)", + super::wrap_tests::peak_rss_gib(), + program.instrs.len(), + ); let layout = SchemaLayout::node(out_halves); layout.assert_covers(proved.public_words.len()); (real_child(artifacts, opts.clone(), &proved), layout) @@ -1489,8 +1501,15 @@ fn the_inner_node_verifies_two_leaf_nodes() { label_of(leaf * FAN_IN), label_of(leaf * FAN_IN + FAN_IN - 1), ); - let (child, layout) = - prove_node_as_child(&wraps, &wrap_layouts, &refs, range, out_halves, &wrap_opts); + let (child, layout) = prove_node_as_child( + &format!("leaf {leaf} (level 1)"), + &wraps, + &wrap_layouts, + &refs, + range, + out_halves, + &wrap_opts, + ); println!( " leaf {leaf}: {} published words, {} sub-proofs", child.public_words.len(), @@ -1510,8 +1529,15 @@ fn the_inner_node_verifies_two_leaf_nodes() { let range = (leaf_labels[0][0], leaf_labels[FAN_IN - 1][1]); let out_halves = leaf_layouts[FAN_IN - 1].out_halves; let t = Instant::now(); - let (inner_node, inner_layout) = - prove_node_as_child(&leaves, &leaf_layouts, &refs, range, out_halves, &wrap_opts); + let (inner_node, inner_layout) = prove_node_as_child( + "the INNER node (level 2)", + &leaves, + &leaf_layouts, + &refs, + range, + out_halves, + &wrap_opts, + ); println!( "\n★ INNER NODE PROVED AND VERIFIED (a node over {FAN_IN} NODE proofs)\n \ prove+harvest {:.1}s\n {} published words, {} sub-proofs\n \ From fdd2e0d1d5325ee84a3691afeb17614abe9b396c Mon Sep 17 00:00:00 2001 From: MauroFab Date: Wed, 9 Sep 2026 11:49:53 -0300 Subject: [PATCH 17/17] test(lfm): the >32 guard's expected string, after the lower bound went MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `sample_u64_pow2_rejects_more_than_32_bits` pinned the old combined text "nbits must be in 1..=32". The continuation-epoch fix did not split that assert in two — it REMOVED the lower bound, leaving one `nbits <= 32` check with a new message. The guard still guards: 33 is rejected at the same site with the same effect; only the wording moved. The new expected string names "at most 32" rather than anything a future lower-bound assert could also produce. A substring loose enough to match any assert in the function would pass on a reintroduced lower bound as readily as on this one, which is the failure this test exists to catch. And the doc names its counterpart, because the pair is the contract: the UPPER bound is pinned here, and that nbits = 0 is accepted AND still consumes a draw is pinned by `per_table_aggregator_tests::a_zero_bit_query_draw_consumes_what_the_host_does`. Widening a bound and keeping only the old rejection test would leave the widening itself unguarded. --- prover/src/lfm/machine_tests.rs | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/prover/src/lfm/machine_tests.rs b/prover/src/lfm/machine_tests.rs index ec92da94f..85487e040 100644 --- a/prover/src/lfm/machine_tests.rs +++ b/prover/src/lfm/machine_tests.rs @@ -1510,8 +1510,17 @@ fn transcript_replay_cell_counts() { // ------------------------- emitter-contract guards ------------------------- +/// The UPPER bound only. There is no lower bound any more: `nbits = 0` is legal +/// (a one-row trace at blowup 2 has a two-leaf LDE, one query index, and that +/// index is 0), and that the emitter still CONSUMES a draw for it is pinned by +/// `per_table_aggregator_tests::a_zero_bit_query_draw_consumes_what_the_host_does`. +/// +/// ⚠ The expected string names "at most 32" deliberately. A substring loose +/// enough to match any assert in this function would pass on a reintroduced +/// lower bound as readily as on this one, which is the failure mode this test +/// exists to catch. #[test] -#[should_panic(expected = "nbits must be in 1..=32")] +#[should_panic(expected = "nbits must be at most 32")] fn sample_u64_pow2_rejects_more_than_32_bits() { use super::transcript_replay::TranscriptReplay; let mut b = super::builder::LfmBuilder::new();