feat(lfm): the per-table aggregation node — step 9, a tree that composes - #975
Merged
Conversation
An aggregation node over epoch wraps sees exactly two things about a child: its `program_id`, an emit-time constant of the parent, and its PUBLISHED WORDS. The per-table wrap published neither the register boundary vectors, nor the epoch label, nor the public-output bytes, nor the L2G re-commit root — so the cross-wrap bindings an aggregator must CHECK (register fini->init across every seam, the label pinned to a chain position, the L2G root equality against the global proof) were not weak, they were unbuildable. In the batched format these four were the CARVED schema, published by the carve rather than by the program. The carve went with the format. Publishing costs no soundness: each value is already bound elsewhere. The register vectors derive the REGISTER preprocessed commitment Phase A absorbs, the label and the output halves are absorbed by `absorb_epoch_statement`, and the L2G root is a Phase A absorb. The L2G bookend's position (the epoch's last sub-proof) is asserted rather than assumed: publishing another sub-proof's root would bind an aggregator's L2G compare to an unrelated table and still look like a passing gate. `schema_words` names the run's width so a reader walks past it by name. `the_assembled_epoch_verifier_runs` uses it: with a literal, that gate would start checking `beta of table 0` against a register slot the next time the schema moves, and would report a pass while doing it.
A wrap's published words are the only thing an aggregation node can read about it, and a node pays per word: eight hinted halves, four canonicity guards, four recombinations, thirty-six bytes of statement absorb and one extension-field inverse in the LfmPublic balance — per word, per child. So what a wrap publishes is the size of the layer above it. At the production posture the wrap publishes 10,507 words; the binding set is around eighty. The other ~10,400 have no consumer above: `composition` is already asserted equal to the claimed Horner inside `emit_table_verification`, the DEEP invariants are documented as exposed for tests, and the beta/z/gamma/zeta/iota runs are challenges the machine derives for itself. They are this crate's differential surface against production's replay, not a binding — a node that hinted them would pay to re-read numbers it can recompute. `Publishes::Diagnostic` stays the default and every existing gate keeps exactly the words it had; `Publishes::Aggregation` is chosen per emission by the aggregator. Dropping the differential surface globally would trade the evidence that this machine derives production's challenges for the saving, so the lever is local. The new gate asserts the containment rather than assuming it: the binding head is identical cell for cell, the bus total still ends the list, and what was dropped is counted from the epoch's own shapes — so a diagnostic added later fails here naming the count instead of silently widening what every node above pays for.
The emitted verifier of one child LFM proof, and the cross-child checks a tree of them needs. A leg is the machine twin of `verify_against_chunked`, which is four steps and no more: absorb the LFM statement, fork and replay Phase A for the shared LogUp pair, recompute the LfmPublic balance from the CLAIMED public words, and verify every sub-proof against it. So this reuses the spine the epoch wrap and the global-memory leg already gate — `emit_table_challenges`, `emit_table_verification`, `replay_phase_a`, `emit_bus_closure` — and adds only the LFM-shaped statement, the canonicity-guarded public-word hinting, the balance target and the bindings. There is no new cryptographic arithmetic here. ⚠ ONE TRANSCRIPT PER CHILD. Each child was produced against a transcript seeded by its own statement, so a node runs one replay per child: two Phase A's, two challenge pairs, two closures. A shared spine that re-indexed every sub-proof over the union of both children would be verifying one proof with 2n tables — a different statement, and not one either child ever made. `per_table_census_tests::tenant_node_program` is shaped that way on purpose, as a census instrument, and is not a template. `SchemaLayout` is the reader of the schema the wrap now publishes, and `assert_covers` pins it against the child's actual published count so a layout applied to the wrong level fails at assembly instead of mis-binding fifty asserts later. The L2G compare is a separate entry point rather than part of the chain bindings: in a tree the epoch wrap and the global proof are not generally in the same node, so it is emitted where both sides are in scope and nowhere else.
Three emission-only measurements, in the order the per-table format makes correct rather than the order lane C's narrowing implies. C narrowed the fan-in question to the binding legs, and did so under the batched assumption that a child publishes ~285 words. The per-table diagnostic wrap publishes 10,507, and a leg pays LINEARLY per published word — eight hints, four canonicity guards, four recombinations, thirty-six bytes of statement absorb and one extension-field inverse. So the term that actually grew by 37x is the per-word one, and it is measured first. (a) is sampled at seven counts rather than fitted from two: the statement's sponge absorbs in rate-sized blocks, so the hash term is a step function whose average is linear, and a two-point fit would hide the step. The linearity is asserted with a tolerance that admits the step and nothing wider. (b) is the bindings as a with/without delta over the same hinted words, so what is left is the bindings alone. (c) needs no second emission. This leg is `tenant_node_program` plus the statement, the balance and the bindings; the balance is field arithmetic and hashes nothing, so in COMPRESSIONS the only term added to C's F is the statement's — which is (a)'s hash column. ⚠ C's F(1) = 2,886 and F(2) = 5,771 are COMPRESSIONS over a glue delta, not cells. The instrument prints all three units side by side so the two are not compared by accident.
One emitter for every level: declare each child's arenas in absorb order, verify each child, bind them, publish the node's own schema. A child is a plain per-table MultiProof whether a wrap or another node produced it, so nothing here is level-specific — the harvest proves it, since `host_table_forked` and `build_table_legs` take (&dyn AIR, StarkProofView) and read a wrap proof exactly as they read a VM epoch's. ★ THE L2G FOLD. The batched aggregator compared each epoch's published L2G root against the global proof's re-commit root for that epoch, and could do it as a local assert because all six legs sat in ONE program. A tree splits them — the epoch wraps are in leaf nodes and the global wrap rides at the root — so the compare must defer to their common ancestor. Re-publishing the subtree's roots as a LIST would grow the node schema with the subtree and make every level's published width a function of the block's epoch count. Folding them with the production hash's two-to-one compression keeps the node schema FIXED SIZE at every level; the root recomputes the same fold over the global wrap's published roots and compares one digest. The fold rule is documented where the root must replicate it. `SchemaLayout` now covers a wrap child and a node child. They differ in their head (a node has FAN_IN Phase A's and no single pair), in their labels (a node covers a RANGE and publishes both ends, which is what gives a parent contiguity across siblings for free) and in their L2G item. That is a constructor apiece rather than a flag, because the differences are real. `digest_from_lanes` is the both-arms inverse of `RootCells::lanes_flat`, written rather than reused: `from_halves` asserts eight halves and is byte-arm-only by construction. FAN_IN is a default, not an assumption — every emitter takes a slice, so the arity is the caller's and the measured host peak still decides it. The gate carries one tamper arm per binding leg, and three rather than one because "both children verified" is exactly what a broken binding looks like: each arm moves one published word in one child's arena and nothing else, so what fails is named by which arm failed.
…pair Closes the evidence gap named when the node was built. A node under the aggregation publish set publishes no challenges, so the only thing saying its legs derived their CHILDREN's challenges was that the node executes at all — a leg on different challenges cannot authenticate the child's walks, so execution implies agreement. Implication is weaker than what every other emitted verifier in this crate is held to. The epoch wrap and the global leg both publish their pair and compare it against production's own replay; the node was the one that did not, and only because its publish set had no room for it. `NodePublishSet::Diagnostic` publishes each child's pair AFTER the schema, so no schema index moves and `SchemaLayout::node` reads both variants identically. It is a gate shape and never a child — nothing verifies a diagnostic node. The oracle is the pair `verify_against_chunked`'s own Phase A recovers host-side from the same proof, which is why `RealChild` keeps `z_alpha` again: it now has a consumer, where before it would have been a dead field.
The re-tune holds q=110 by moving security_bits 128 -> 120 at blowup 4 rather than by taking the count to 119, so the cost instrument's 10,507 sample point is current rather than a value that may go stale. The coefficient the instrument produces was never a function of it.
The assertion read `assert_eq!(diag[last], agg[last])`, and a published word is an `(index, value)` pair. The two indices cannot be equal — making the lists different lengths is the entire point of R2 — so the gate asserted the negation of the property it exists to prove. Box A caught it with the four field elements matching exactly and only the indices differing, 307 against 144: the emitter doing precisely what it should, failed by a test asserting something it never meant. 144 is also the predicted Aggregation size (5 + schema_words), so the profile is doing its job at fixture scale. The replacement checks each profile on its own against production's COMMIT bus balance, which is a stronger oracle than "the other profile agrees with me": the last published word must be the closure's total AND reach the target production computed. Position is asserted separately, as what "ends the list" actually means for an auto-incrementing index.
`the_epoch_challenge_spine_matches_production` failed on box A with "beta of table 0" reading an all-zero challenge. It is not an underived challenge and it is not a leak: `epoch_challenge_program` is `epoch_program(e, false)` — the SAME emitter with the legs off, as its own doc says and says why — so it gained R1's schema like every other caller, and a literal cursor of 4 landed on register INIT slot 0. x0 is hard-wired zero, so the mismatch printed zeroes and read like a derivation failure. This is the exact failure the R1 commit message described, at a second site that commit missed. The audit that missed it read the function's NAME and concluded "different emitter" without opening its two-line body — a claim about what code does, made from a name. The re-audit walked every caller of `epoch_program`/`epoch_challenge_program`/`epoch_program_with` and every positional read of `public_words`: this was the last one. The rest read index 0, 1, 2 or the final word, all of which sit outside the inserted run. Also adds a samplability pre-flight to the leaf gate. `emit_table_challenges` samples each query index with `sample_u64_pow2(index_bits())`, and a one-row trace at blowup 2 makes that zero; the sampler's assert then fires deep inside emission naming neither the table nor which side of the tree it came from, which is how it reached box A as a bare "got 0". The pre-flight names the sub-proof and prints the shallowest shape on both the inner-epoch and the wrap-child side, so the next run attributes it instead of reporting it. It is a diagnostic, not a fix: if it fires the shape is real.
The emitted verifier could not be built over a legal continuation epoch. A one-row trace at blowup 2 has a two-leaf LDE, so production samples `sample_u64(domain_size >> 1)` = `sample_u64(1)` for each of that table's queries, and `sample_u64_pow2` refused the corresponding `nbits = 0` outright. Found by the leaf-node gate at inner epoch 1's sub-proof #10; `emit_table_challenges` and `sample_u64_pow2` are untouched by every other commit on this branch, so this is a latent defect on the tip. The obvious fix would have been the bug. "One index, so skip the sample" is wrong: production does NOT skip it. The byte arm's threshold is `1u64.wrapping_neg() % 1 = 0`, so `next_sample_u64()` runs once and advances `out_pos`; the pinned algebraic arm squeezes a cell and only then masks with `& (upper_bound - 1)`. An emitter that skipped would be one squeeze short for that table and every challenge after it in that fork would diverge. Both emitted arms already consume before reading `nbits` — `squeeze_bits` calls `squeeze_cell` first, the byte arm calls `next_candidate` first — so letting zero through is the whole change. The lower bound was unjustified: the assert message and the doc paragraph both justify only `<= 32`. Every downstream consumer degenerates correctly, checked rather than assumed: `point_factors(1)` is empty and matches the empty bit vector, `pow_bits` over no bits returns the coset offset (which IS the query point for a two-leaf domain), and `merkle_depth + 1 == log2_lde_length` makes the depth zero, so the leaf hash is the root — correct for a one-pair tree. ⚠ The gate is not "the panic is gone". A consumption desync here is invisible to a value differential: every index is 0 whether the draw happened or not, and `iota_bits` is the last thing sampled in that fork, so nothing later disagrees either. The new test samples an extension element AFTER the zero-bit draw on both sides and compares against the HOST's — the only observable that moves if the squeeze is missing.
A node whose children are NODE proofs. The emitter needed no change — a child is a plain per-table MultiProof whichever level produced it, so `real_child` reads a node's proof exactly as it reads a wrap's — which is what "the same emitter serves every level" means operationally. ★ Building the arm found a real bug in the leaf work. A node published its L2G fold as digest CELLS (four lanes in one word) while a wrap publishes its root as lanes (one lane per word), and `emit_node_publishes` reads `lanes[0]` of each published l2g word. A node child would have handed ONE felt to `digest_from_lanes` where four are required — the inner node could not have been built. Fixed by publishing the fold in the wrap's own shape, so both layouts read alike; the asymmetry is removed rather than parameterised. Three things the leaf gate could not reach are exercised here: the node layout rather than the wrap layout, a label RANGE per child (each leaf carries its subtree's two ends, and pinning both is what makes contiguity across sibling subtrees a consequence of the pins), and the fold COMPOSING — each leaf folded its own wraps' roots and the inner node folds those folds. A single-child node folds to identity, so this needs two real leaves. The epoch requirement is asserted, not worked around: a two-level tree at fan-in N needs N^2 epochs, and padding would mean a pad child with no epoch to belong to, breaking the register chain and the label pin — the same trade already rejected when the tree shape was priced. The closing assertion is the composition property itself: an inner node's published schema has the same total as its children's, which is what lets the level above use the identical emitter.
The panic moved downstream exactly as predicted: relaxing the query sampler's guard let emission reach `SubProofShape::check`, whose `merkle_depth >= 1` refused the same one-row table. A one-pair domain has a single leaf, so the tree has no levels and the LEAF HASH IS THE ROOT. Settled before touching the assert, and it is the reason this is safe: BOTH SIDES already handle depth 0 without a special case. The host's `verify_merkle_path_from_leaf_hash` loops over an empty path and returns `root_hash == hashed_value`; `emit_group_authentication` hashes the leaf, walks zero levels through `wrap_merkle_walk`, and asserts the result equals the committed root. So the walk at depth 0 is NOT a no-op — it is exactly the binding — and the assert refused a shape the code verifies correctly. Swept the rest of the path for other asserts predicated on a non-empty tree, as the last fix's lesson demands: `sub_proof.rs:364` compares bits against merkle_depth (0 == 0), and the remaining `> 0` asserts are about query counts, composition parts and frame step size, none of which depend on depth. This was the only one. That also closes the FRI question left open by reasoning: `terminal_log` is `(blowup_log + final_poly_log_degree).min(log2_lde_length)`, so at log2_lde = 1 it clamps to 1, `total_folds` is 0, and the FRI walk is vacuous by construction rather than by luck. ⚠ The gate's REJECTION arm is the load-bearing one. If relaxing the shape check had let the walk skip its root comparison, the honest arm would still pass and only the rejection arm would fail. The root it compares against is the emitter's own leaf hash, whose agreement with the host backend is gated separately by algebraic_commit's leaf/parent differential — composing the two is what makes this emitter-versus-host rather than emitter-versus-itself.
Two changes, both about not letting one number stand for several things. The inner-node gate needs FAN_IN^2 epochs and the shared FIXTURE_EPOCH_LOG2 selects two. `epoch_size_log2` is a PARAMETER of `prove_continuation` with a floor of 2, so this passes a smaller one locally instead of shrinking the shared constant. The nine gates that already run green against that constant keep their baseline; nothing is re-baselined to give one test more epochs. Smaller epochs mean shallower tables, which is exactly where the two degenerate shapes were found, so the cheap place to find a third is here. And the leaf gate now prints the RSS high-water mark at each phase boundary. `peak_rss_gib` is VmHWM: a PROCESS mark that only rises, so a single figure at the end spans the wrap proves, the diagnostic arm and the node prove alike — three proves and a 6.7M-instruction program that production never emits, in one process. The run's 40.6 GiB is that conflation, not the node's peak. Per-boundary readings bound each phase instead: the node's own prove costs at most the rise from the last mark before it.
The single "before the node prove" mark was taken before `build_artifacts_with_hasher`, which is not bookkeeping: it runs `lde_columns` + `commit_lde_columns` over every chip group and builds the prep round, a full commitment pass over the program. So the +35.25 GiB that run attributed to "the node prove" actually brackets the artifact build AND the prove together and cannot say which costs what. Three marks now split artifacts, prove and verify. And the census is printed beside the measurement so the two are never quoted apart. The empty LFM machine costs 26,482,828 base-field-equivalent cells — the 0-word row of the cost instrument — against this node's 35,244,192. So 75% of a fixture node's census is the machine's padding FLOOR and only 25% is verification work, which is why a fixture node and a production node are not on the same part of the curve and why the affine RSS law reading 8x optimistic here does not transfer to either direction without a node measured where the linear term dominates.
One gate's peak against another's cannot settle whether node cost grows per level. The leaf gate runs at FIXTURE_EPOCH_LOG2 and the inner gate at FIXTURE_EPOCH_LOG2 - 1, so their nodes sit over different-sized epochs and their peaks describe different workloads. Only levels measured inside ONE run are comparable, and `prove_node_as_child` is where every level's prove happens, so the mark goes there and every node reports its own.
MauroToscano
marked this pull request as draft
September 8, 2026 21:57
`sample_u64_pow2_rejects_more_than_32_bits` pinned the old combined text "nbits must be in 1..=32". The continuation-epoch fix did not split that assert in two — it REMOVED the lower bound, leaving one `nbits <= 32` check with a new message. The guard still guards: 33 is rejected at the same site with the same effect; only the wording moved. The new expected string names "at most 32" rather than anything a future lower-bound assert could also produce. A substring loose enough to match any assert in the function would pass on a reintroduced lower bound as readily as on this one, which is the failure this test exists to catch. And the doc names its counterpart, because the pair is the contract: the UPPER bound is pinned here, and that nbits = 0 is accepted AND still consumes a draw is pinned by `per_table_aggregator_tests::a_zero_bit_query_draw_consumes_what_the_host_does`. Widening a bound and keeping only the old rejection test would leave the widening itself unguarded.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Step 9 of the per-table redo: the aggregation node — the emitted verifier of a child
LFM proof, the cross-child bindings, and the two changes to the epoch wrap that make either possible.
Full suite green at
fdd2e0d1:prover --lib1091 passed / 8 failed / 46 ignored = 1145, and the eight failures are by name the same eight #973 and #974 both gated — nothing added, nothing retired.stark271/0/3,math-cuda171/0, both matching #974.--listconfirms 1145 independently.make lintexit 0 over all three feature sets;make fmta no-op.Against
per-table-gpu@1d92fea0(both deletion phases merged). Sixteen signed commits.What a node is, in four steps
A leg is the machine twin of
proof::verify_against_chunked, which is four steps and no more:absorb the LFM statement, fork and replay Phase A for the shared LogUp pair, recompute the
LfmPublicbalance from the claimed public words, and verify every sub-proof against it.per_table_aggregator::emit_legemits exactly those four, so the leg and the host verifier are tworenderings of one contract rather than two implementations of one idea.
That is why this PR adds almost no cryptographic arithmetic. The spine is
epoch::emit_table_challenges, the per-sub-proof verification isepoch_verify::emit_table_verification, Phase A isstatement_replay::replay_phase_a, the closureis
logup::emit_bus_closure— all already gated by the epoch wrap and the global-memory leg. Newhere: the LFM-shaped statement, the canonicity-guarded public-word hinting, the balance target, and
the bindings.
One transcript per child. Each child was produced against a transcript seeded by its own
statement, so a node runs one replay per child: N Phase A's, N challenge pairs, N closures. A shared
spine that re-indexed every sub-proof over the union of both children would be verifying one proof
with
2ntables — a different statement, and not one either child ever made.(
per_table_census_tests::tenant_node_programis shaped that way deliberately, as a censusinstrument; it is not a template, and this is noted where someone would otherwise copy it.)
Two changes to the epoch wrap, and why they are not optional
R1 — the wrap publishes the block-binding schema
A node sees exactly two things about a child: its
program_id, an emit-time constant of the parent,and its published words. The per-table wrap published neither the register boundary vectors, nor
the epoch label, nor the public-output bytes, nor the L2G re-commit root — so the bindings a node
must check (register fini→init across every seam, the label pinned to a chain position, the L2G
root equality against the global proof) were not weak, they were unbuildable.
In the batched format those four were the carved schema, published by the carve rather than by the
program. The carve went with the format.
Publishing costs no soundness: each value is already bound. The register vectors derive the REGISTER
preprocessed commitment Phase A absorbs; the label and the output halves are absorbed by
absorb_epoch_statement; the L2G root is a Phase A absorb.R2 — the wrap gets a publish profile, and it is the largest lever in the node
A node pays per published word: eight hinted halves, four canonicity guards, four
recombinations, thirty-six bytes of statement absorb and one extension-field inverse. So what a
child publishes is the size of the layer above it.
At the production posture the wrap publishes 10,507 words; the binding set is ~145. The
other ~10,400 have no consumer above:
compositionis already asserted equal to the claimedHorner inside
emit_table_verification, the DEEP invariants are documented as exposed for tests,and the β/z/γ/ζ/ι runs are challenges the machine derives for itself. They are this crate's
differential surface against production's replay — evidence, not binding.
Publishes::Diagnosticstays the default and every existing gate keeps exactly the words it had;Publishes::Aggregationis chosen per emission by the aggregator.The L2G fold — what makes the tree compose
The batched aggregator compared each epoch's published L2G root against the global proof's
re-commit root for that epoch, and could do it as a local assert because all six legs sat in one
program. A tree splits them: the epoch wraps are in leaf nodes and the global wrap rides at the
root, so the compare must defer to their common ancestor.
Re-publishing a subtree's roots as a list would grow the node schema with the subtree, making
every level's published width a function of the block's epoch count — and therefore the parent's leg
shape too. Folding them with the production hash's two-to-one compression keeps the node schema
fixed-size at every level; the root recomputes the same fold over the global wrap's published
roots and compares one digest. The fold rule (left fold, tree order, identity on a singleton) is
documented where the root must replicate it.
SchemaLayouthas awrapand anodeconstructor rather than a flag, because the differences arereal: a node has N Phase A's and so no single
(z, α), and it covers a label range rather thanone label. Publishing the range's two ends is what gives a parent contiguity across siblings for
free — pin both ends to constants and a child covering the wrong range cannot satisfy the pins.
The inner node, and the bug building it found
emit_nodeneeded no change to serve a node whose children are node proofs: a child is a plainper-table
MultiProofwhichever level produced it, andreal_childreads a node's proof exactly asit reads a wrap's. That is what "the same emitter serves every level" means operationally — the
emitter is shared, the programs are not, because each level compiles it against different
program_idconstants and shapes.★ Building that arm found a real bug in the leaf work. A node published its L2G fold as digest
cells (four lanes in one word) where a wrap publishes its root as lanes (one lane per word),
and
emit_node_publishesreadslanes[0]of each published l2g word — correct for a wrap, one feltwhere four are needed for a node child. The inner node could not have been built, and no leaf gate
could ever have caught it, because a leaf's children are always wraps. Fixed by publishing the fold
in the wrap's own shape, so both layouts read alike; the asymmetry is removed rather than
parameterised around.
⛔ A found defect: the emitted verifier could not verify a legal epoch
Two degenerate shapes, one story, both surfaced by the leaf gate and neither caused by it —
emit_table_challenges,sample_u64_pow2andSubProofShape::checkare untouched by every othercommit here. A one-row trace at blowup 2 is a legal continuation-epoch sub-proof (epoch 1 of the
fixture bundle carries one at index #10), and the emitted per-table epoch verifier refused it twice
over.
1. The query sampler refused zero index bits.
index_bits() = log2_trace + log2_blowup − 1iszero for a two-leaf LDE, and
sample_u64_pow2asserted1..=32. ⚠ The obvious fix would have beenthe bug: production does not skip the draw. The byte arm's
threshold = 1u64.wrapping_neg() % 1is 0, so
next_sample_u64()runs once and advancesout_pos; the pinned algebraic arm callssqueeze_cell()and only then masks with& (upper_bound − 1). An emitter that skipped would be onesqueeze short for that table and every challenge after it in that fork would diverge. Both emitted
arms already consume before reading
nbits, so letting zero through is the whole change.⚠ A desync there is invisible to a value differential: every index is 0 whether the draw happened
or not, and
iota_bitsis the last thing sampled in that fork. So the gate samples an extensionelement after the zero-bit draw on both sides and compares against the host's — the only
observable that moves if the squeeze is missing.
2. The shape check refused a one-leaf Merkle tree. With one row pair the tree has no levels and
the leaf hash is the root;
SubProofShape::checkassertedmerkle_depth >= 1. The walk at depth 0is not a no-op —
emit_group_authenticationhashes the leaf, walks zero levels, and still assertsthe result equals the committed root, which is the entire binding. The host degenerates identically:
verify_merkle_path_from_leaf_hashloops over an empty path and returnsroot_hash == hashed_value.So the assert refused a shape the code beneath it verifies correctly. Its gate's rejection arm is
the load-bearing half — had the relaxation let the walk skip its root comparison, the honest arm would
still pass.
The rest of that path was swept for asserts predicated on a non-empty tree:
sub_proof.rs:364compares
bits.len()againstmerkle_depth(0 == 0), and the remaining> 0asserts are about querycounts, composition parts and frame step size. That sweep also settled the FRI side by construction —
terminal_log = (blowup_log + final_poly_log_degree).min(log2_lde_length)clamps to 1, sototal_foldsis 0 and the FRI walk is vacuous.Evidence
The node cost model — measured, emission only
Three columns kept apart on purpose: instructions, hash ops and cells are three different
measurements, and collapsing them is how
F(1) = 2,886 / F(2) = 5,771came to be quoted as cellswhen they are compressions.
⚠ The rows in (a) are not legs.
publics_only_programis statement + hint + balance with PhaseA over zero tables, so the 0-word row's 26,482,828 cells is the empty machine's chip-padding
floor, which any LFM program pays before doing anything. Separating it out: the publish term is
1.73M cells at 153 words and 113.6M at 10,655 — R2 saves 111.8M cells per child ≈ 6.11
GiB on the corrected 58.7 B/cell line.
⚠ The coefficient does not extrapolate as a constant. Cells are not additive across programs:
work below a chip's padding floor is free until it crosses a power of two, so 12,176 cells/word
measured at low occupancy need not hold inside a full leg whose chips are already past their floors.
Order of magnitude robust; exact figure not.
The bindings are free — ~10k cells per child, zero hash ops, ~0.01% of a leg. Everything
lane C established about the inter-leg glue holds; what made it look otherwise was the publish term,
which R2 removes.
What a node costs — measured
The leaf gate's phase marks, on the fixture, one run:
build_artifacts_with_hasheris +2.25 GiBagainst
lfm_prove's +31.5.blowup-4 line (2.5 GiB + 58.7 B/cell) against 33.76 GiB measured for the node's own
artifacts+prove delta — 1.14×, inside the law's own stated ~15% cross-program transfer (1.32×
against the 39.10 whole-process peak).
size — the cost instrument's 0-word row.
⚠ Two census lines measure different programs, 14× apart, and reading the wrong one produced two
confident and wrong findings before this was traced:
wrap_tests::fixture_wrap_runprints a censusof
epoch_program(35,244,192, the epoch WRAP) and the aggregator gate prints one of the NODEprogram (497,620,736). Trace a census to the program it was computed on before dividing anything
by it.
Phase 2's prep-round deletion makes node proves 2.34× faster
A one-change arm: the same sixteen commits at two bases,
b433674fagainst1d92fea0(deletionphases 1 and 2). Pre-registered before the run — 600–640 s if the rebase is the cause, under ~350 s
to falsify.
★ The mechanism — and it is not the obvious one. The speedup is concentrated in
build_artifacts_with_hasher(8.5×) and absent fromlfm_prove(1.13×, run-to-run variance atn=1), which is where the deleted code lived. ⚠ But "a second commitment pass over every chip group"
naively predicts ~2×, not 8.5× — and the deletion removed the round's absorb, not the
expansion: both arms still expand every group exactly once. The gap is in how that pass was
implemented, and it is two things in the deleted
StreamingMmcsBuilder(
99d25bcf:crypto/stark/src/fri/mmcs.rs), both read rather than inferred:new()eagerly allocates2^(h-1)leaf hashers for every distinct height in the round(
:731-739), in the constructor, before a byte of data arrives, and holds them until thatheight's last matrix is absorbed. Under an algebraic hash each is a sponge state, so the
round's tallest matrix sets a large up-front allocation that lives across the whole of
build_artifacts. The per-slot commit path has no counterpart, and this is paid on constructionregardless of absorb cost.
absorbheap-allocates inside the parallel inner loop —Vec::with_capacity(2 * width)perleaf, per matrix (
:777). Twelve slots plus the BLAKE3 chunks is twelve-plus allocations perleaf where the one-shot path pays one.
★ The comment directly above that loop reads "the same shape, and the same cost, as
commit'sone-shot group hash." Same shape; not the same cost — the 8.5× is the measurement that
disproves it.
⚠ This is a property of that implementation, not of mixed-height MMCS as a concept. A
mixed-height MMCS is not inherently 8.5×; allocating lazily per height on first absorb and hoisting
the row-pair buffer per thread would remove both terms. ⇒ Phase 1's "Where a new proof format
attaches" table names
fri/mmcs.rsas what a future format would reuse — whoever picks it up shouldknow it cost 8.5× on
build_artifactsand why, or the cost is reimported with the file.⚠ n = 1 per side. One run at each base, not a paired series. The two components above account for
~324 s of the 351.6 s delta, leaving ~27 s (8%) unexplained — other phases, or run-to-run
variance. Both 2.34× and 8.5× should be quoted with that caveat attached.
⇒ A measured payoff for a deletion made as dead-structure cleanup, on a path neither lane had
connected to it.
The tree does not grow per level — measured within one run
⛔ STRUCK 2026-09-09 — THIS SECTION'S MEMORY CLAIM IS UNSUPPORTED (found by lane M; struck in
STATE.md §3). The three figures below are one process-wide
VmHWMsampled at three times, after abase continuation and four wraps in the same process, with no mark before leaf 0 — so they attribute
no cost to any level, level 1 included. The instruction counts stand; the GiB column does not.
The published #975 body carries this heading uncorrected. Kept in place, not deleted, so nobody
re-derives it.
Same run, same epoch size, same process. ⛔ The sentence that stood here — "leaf 0 set the mark and
nothing after it exceeded it: level 2 ≤ level 1" — assumed leaf 0 set the mark. Nothing in the run
shows that; there is no mark before leaf 0, and the base plus four wraps ran first. What survives:
the inner node runs 56% of a leaf's instructions.
⚠ This has to be a within-run comparison. The leaf and inner gates run at different epoch sizes
(
FIXTURE_EPOCH_LOG2and−1), so comparing one gate's peak against the other's compares differentworkloads — an earlier cross-gate reading was withdrawn for exactly that reason, and the identical
144-word schema hides the difference because the schema is dominated by the register vectors, which
do not move with epoch size, while the sub-proof shapes do.
Gates
the_aggregation_publish_profile_drops_only_diagnosticsthe_assembled_epoch_verifier_runsthe_epoch_challenge_spine_matches_productionthe_global_verifier_leg_runs_and_rejects_tampersthe_node_cost_model_is_measuredthe_leaf_node_verifies_and_binds_two_wraps(z, α)against its child's own, then prove + verify, then one tamper arm per binding legthe_inner_node_verifies_two_leaf_nodesa_zero_bit_query_draw_consumes_what_the_host_doesa_depth_zero_walk_still_binds_leaf_to_root⚠ The suite was gated on the failure-NAME SET, not the counts — and twice that was the only thing that saw the state
This branch went red twice on the way to that green, and neither red was visible in a total:
1090 / 9 / 46 = 1145should_panicstring — the guard still rejectednbits = 33at the same line, only the message had moved1090 / 9 / 46 = 11451091 / 8 / 46 = 1145⇒ A count is a checksum over the wrong thing. One test failing more is arithmetically
indistinguishable from one added as ignored, so run 1's regression hid inside a matching total;
run 2 then produced the same three numbers as run 1 while measuring a different reality.
--listread 1145 in every case and CI's total agreed throughout — three instruments, all blind, all
agreeing. Only the set of failure names distinguished them. Pre-register the set.
Three tamper arms rather than one, because "both children verified" is exactly what a broken binding
looks like: each moves a single published half in one child's arena and nothing else, so what fails
is named by which arm failed.
Open, and stated rather than buried
ten of ten in one run. A samplability pre-flight remains in both, naming any offending sub-proof and
printing the shallowest shape on the inner-epoch and wrap-child sides, so a future degenerate shape
is attributed rather than reported as a bare panic. That is how both of the defects above were
localised.
FAN_IN²epochs and asserts it, naming the number and the remedies ifthe fixture is short. Padding was rejected: a pad child belongs to no epoch and breaks the register
chain and the label pin. ✓ It gets its epochs by passing
FIXTURE_EPOCH_LOG2 - 1locally —epoch_size_log2is a parameter ofprove_continuation(floor 2), not a constant — so the sharedfixture is untouched and the other gates keep their baseline.
binding leg tamper-tested and the
(z, α)differential holding at every level. The schema isfixed-size across levels: leaf 0 and leaf 1 publish 144 words over 11 sub-proofs, and the inner
node over two node proofs publishes 144 words over 11 sub-proofs — identical. That is the L2G
fold's purpose landing as a measurement rather than a design claim; had a node re-published its
subtree's roots as a list, the inner node's schema would have grown with the subtree.
Node cost does not grow per level — measured within one run— the instrument was aVmHWMthat never moved, which is an upper bound on the WHOLE process (base + wraps + leaves + inner node), not a per-level cost; there is no mark before leaf 0, so level 1 is unsupported by the same argument. See the struck section above. What stands: the inner node ran 56% of a leaf's instructions (3,757,992 vs 6,714,341). Level-2 memory is re-measured with one arm per process andVmRSSsampled before any per-level claim is made. Level 2 set no new high-watermark and ran 3.76M instructions against a leaf's 6.71M (56%). ⚠ It had to be a within-run
comparison: the two gates run at different epoch sizes, so an earlier cross-gate reading
(40.578 GiB leaf against 37.559 GiB inner) was withdrawn as comparing different workloads. The
identical 144-word schema hides that, because the schema is dominated by the register vectors, which
do not move with epoch size, while the sub-proof shapes do.
against — 322M cells → 20.1 GiB at fan-in 2 — was right in its law and 1.47× low in its cell
count: implied per-leg here is ~236M against a 161M point estimate, inside the pre-registered
80–240M band at its very top. So the METHOD stands — the fan-in question reduces to predicting a
node's cell count, and the law converts it — but a fixture node is not a production node, and
no production node has been measured. Whether a tree fits box A's 120.6 GiB is still open.
FAN_INis a default, not an assumption — every emitter takes a slice, so the arity is thecaller's and the measurement still decides it.
program_idas an emit-time constant, andprogram_idis derived from the compiled program, so aprogram verifying its own shape would need its own id inside its own instruction stream. It costs
zero registry entries —
LfmProgramKindblesses six toy programs and the wrap path neverresolves — so nothing here reaches step 8b.