diff --git a/prover/src/lfm/epoch_tests.rs b/prover/src/lfm/epoch_tests.rs index 678ed51f7..e9ebd802e 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()); @@ -1760,6 +1806,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() { @@ -1831,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()); + } } } @@ -1892,6 +1989,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(); @@ -2039,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}"); @@ -2295,7 +2422,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, @@ -2345,7 +2472,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/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 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(); 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..1eef5769d --- /dev/null +++ b/prover/src/lfm/per_table_aggregator.rs @@ -0,0 +1,874 @@ +//! 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 — for a WRAP child and for a NODE child alike. +/// +/// 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, + pub l2g_words: usize, + /// Words published after the schema run. + pub tail: usize, +} + +impl SchemaLayout { + /// 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, + } + } + + /// 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, + // ★ 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, + } + } + + pub fn schema_words(&self) -> usize { + 2 * self.num_reg + self.label_words + self.out_halves + self.l2g_words + } + + /// Every word the child publishes. + pub fn total(&self) -> usize { + self.head + self.schema_words() + self.tail + } + + /// Pin the layout against what the child actually publishes. + /// + /// 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 \ + (head={}, num_reg={}, label_words={}, out_halves={}, l2g_words={}, tail={})", + self.head, + self.num_reg, + self.label_words, + self.out_halves, + self.l2g_words, + self.tail, + ); + } + + pub fn id(&self, half: usize) -> usize { + self.id_at + 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, i: usize) -> usize { + self.head + 2 * self.num_reg + i + } + pub fn out_half(&self, i: usize) -> usize { + self.head + 2 * self.num_reg + self.label_words + i + } + pub fn l2g_word(&self, w: usize) -> usize { + self.head + 2 * self.num_reg + self.label_words + self.out_halves + w + } +} + +/// 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. + // + // 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() + ); + 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, + ); + } + } +} + +// ============================ 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 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, + 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); + // Unpacked to lanes, so a node's L2G item reads exactly like a wrap's. + for cell in folded.cells() { + for lane in b.unpack(*cell) { + b.public(lane.as_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), + /// 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. +pub fn emit_node(b: &mut LfmBuilder, inputs: &NodeInputs<'_>) { + let NodeInputs { + children, + 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"); + 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, + }, + ); + // 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 b5af6b284..460eebeaa 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() @@ -462,3 +462,1216 @@ 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 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 + // 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, + ); +} + +// ===================== 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::wrap(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::wrap(OUT_HALVES)) + .collect(); + // 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) +} + +/// ★ 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::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 + // 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!( + "\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." + ); +} + +// ======================= 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 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), +} + +/// 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, + z_alpha: (lookup[0], lookup[1]), + } +} + +/// 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), + 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(); + super::per_table_aggregator::emit_node( + &mut b, + &super::per_table_aggregator::NodeInputs { + children: &shapes, + layouts, + labels, + label_range, + publishes, + }, + ); + 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. +/// +/// # 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, NodePublishSet, 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); + // 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); + 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\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 + // 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); + + // ---- ★ 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)\n RSS high-water AFTER the diagnostic arm: {:?} GiB", + t.elapsed().as_secs_f64(), + diagnostic.instrs.len(), + super::wrap_tests::peak_rss_gib(), + ); + + // ---- 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(), + program.instrs.len() + ); + + let t = Instant::now(); + let exec = execute(&program, &arenas, &crate::hash_pin::BLOCK_HASHER) + .expect("★ the leaf node must execute"); + 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 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. + // + // ⚠ 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( + &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"); + } +} + +/// ★ 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" + ); +} + +/// 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. +#[allow(clippy::too_many_arguments)] +fn prove_node_as_child( + label: &str, + 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"); + // ★ 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) +} + +/// ★ 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(); + // ★ 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; 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() + ); + + 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( + &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(), + 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( + "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 \ + 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" + ); +} + +/// ★ 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. } } 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 {