test(lfm): lever-0 census — the tenant-width bill of a per-table aggregator leg - #955
Merged
Conversation
…egator leg Measures what a per-table aggregator pays to open a wrap proof whose hash matrix is 316/436/612 columns wide instead of 3,056, by closed form over the real AIR shapes plus an emission arm at fixture scale. No proving. The correction it exists to make: MEMORY-MODEL lever 0 reads P3-CENSUS-AB's "1,247 hash-matrix blocks of 1,846 per query" and concludes 0.370x. 1,846 is a BATCHED per-query bill. In the per-table format every table walks its own Merkle path, so the path terms are 63% of the bill and the hash matrix is 30%, not 68%. Second axis the census surfaced: the recorded wrap program emits exactly one keccak permutation (program_id is keccak over bytes whatever the configuration commits under), and that one row instantiates LFM_KECCAK, KECCAK_RND and KECCAK_RC — three sub-proofs at 736+88 and 1,480+516 columns. Both readings are carried because that axis, not the hash, decides the aggregator's fan-in. Emission runs under WrapHash::Blake3 on both arms: SubProofShape::opening_words and FriShape::query_words size their arena stride from the production pin while emit_table_verification advances by the builder's digest width, so an explicit algebraic build trips the stride assertion on a BLAKE3-pinned branch. It changes no count — blocks_for's algebraic and BLAKE3 arms are equal at rate 8, which the new hash-invariance test re-checks over exactly these groups.
…alsification The keccak family has to be held fixed on both sides of a ratio for the ratio to mean anything, so the census now carries a keccak-less BLAKE3 tenant beside the recorded one and prints both like-for-like pairs. Also prints the check that matters more than my arithmetic: MEMORY-MODEL §1.2 puts the per-table/batched compression ratio at the aggregator at 2.44x, and the leaf term is format-invariant, so a hash matrix at 67.6% of the batched bill is necessarily 27.7% of the per-table one. That is what the census measures. The 0.370x is the model disagreeing with itself.
The block is 10 epochs of 2^22 on the measured 39.6M-cycle guest, not the 18 PLAN T2 carried from the older one. The fan-in decision does not move with the count: a level-1 node costs f*leg + glue, a function of the fan-in alone, so the wrap count sets how many nodes there are and not how big the biggest one is. What the tree walk makes visible is the node COUNT beside the node SIZE — 11 aggregator proofs at fan-in 2 against 7 at fan-in 3.
The box run caught this: the BLAKE3 tenant named HasherKind::Blake3, which instantiates the BLAKE3 SOCKET as LFM_HASH — 2,980 main + 599 aux — a chip the real proof does not carry. hash_pin::BLOCK_HASHER is Test on a BLAKE3-pinned build, and the record agrees: LFM_HASH at 4 rows, 0 used, 28 main, 3 aux. Under a byte hash the emitter's Merkle work lowers to the dedicated LFM_BLAKE3 chip and emits no Instr::Hash at all, so the socket idles. The socket permutation and the commitment hash are orthogonal axes and this is what confusing them costs: +1,196 leaf blocks per query on the BLAKE3 baseline, which the whole census is a ratio against. It made lever 0 look BIGGER than it is — 0.632x printed against the true 0.774x. Decision numbers are RPX's own leg and did not move: fan-in 3 at 13.6% headroom, fan-in 2 at 34.9%. the_blake3_tenant_socket_matches_the_record asserts the widths against the recorded census so this cannot regress silently. Also prints the tree at 10 and 18 wraps, which makes the invariance explicit: a level-1 node is f*leg + glue and carries no wrap count, so only the node count moves.
The emission arm measured glue at +56-60% of the leg and that was quoted as one
percentage, which is not a number that can be extrapolated: glue(q) = F + P*q,
and F and P reach production's 110 queries by factors 55 apart — the difference
between the glue being under 1% of the leg there and 57% of it.
So the arm now sweeps q over {2,4,8}, fits the line through the endpoints, and
checks it against the middle point (asserted within 5%, since the split is what
licenses the extrapolation). It prints F, P and the extrapolation to 110
queries, with the caveat that fixture heights understate F: 4 FRI layers per
table against production's 12, 13 Merkle levels against 21-25.
The decision block now applies the measured glue multiplicatively as well —
the pessimistic bound, where none of the +57.2% decays with the query count.
Under it a fan-in 3 node crosses 2^21 outright and doubles its hash table,
while fan-in 2 still clears the rule at 32.9%. That is asserted; the crossing
itself is only printed, because its margin is 0.58% and a tripwire that flips
on a 0.6% drift is noise.
…ement Reviewer's decision-grade point, accepted: the tree test's verdict rests on GLUE_ADDITIVE, imported from the batched six-leg model, which this PR does not measure. The emission arm's own ~1.1% at 110 queries does not replace it, because that arm emits ONE leg and a single-leg fixture structurally cannot contain INTER-LEG glue — the binding between the legs of a real multi-leg aggregator has no counterpart in it. The two numbers are not in conflict and neither settles the question. So the test is renamed from _is_derived_from_the_measured_leg to _applies_the_rule (the leg is measured; the glue is not, and the verdict turns on the glue), the constant's comment says outright that it is imported, and the printed verdict now reads: fan-in 2 is the conservative default; if the inter-leg glue is at the single-leg level, fan-in 3 clears with ~36% headroom and the rule selects 3; lane A's first real two-leg emission settles it. Nits in the same commit: - module doc: the socket bug inflated the baseline by 1,185 blocks/query (1,201 against the idle chip's 16), not 1,196, and the true ratio is 0.774x not 0.776x - the tree header said '18 wraps' while WRAPS = 10; it now names the constant - slots come from airs.rs (BLAKE3_SLOT, KECCAK_SLOT, KECCAK_RND_SLOT, KECCAK_RC_SLOT) instead of literals, so a reordering of the frozen chip order cannot silently re-point the census; HASH_SLOT stays local because airs.rs exports none, and says so - the socket guard now also asserts BLAKE3_TENANT_SOCKET == hash_pin::BLOCK_HASHER, so a re-pinned branch fails here rather than measuring a shape nothing proves
The deciding measurement, per the lead's go. the_rpx_leg_emits_at_production_heights
re-fits glue(q) = F + P*q at the recorded per-table wrap's own heights, so the
fan-in verdict stops resting on a height extrapolation from 2^12.
It emits at ONE leg and at TWO, because a single-leg fixture is exactly what
could not answer the open question: F(2 legs) - 2*F(1 leg) is the inter-leg
glue, the part of a multi-leg node that is not its legs added up. The emitter
is generalised to N legs (tenant_node_program) with every sub-proof of every
leg getting its own fork index over the whole set, which is what a real
multi-leg aggregator does.
The query sweep stays at {2,4,8} on purpose: F is the query-INVARIANT
intercept, so measuring it needs production HEIGHTS, not production queries.
A 110-query emission at these heights pads LFM_BLAKE3 to 2^19 x 3,112 -- about
13 GB for that chip alone -- and yields the same intercept that 8 queries does
at ~800 MB.
The rule is then applied at 110 queries with the measured F and P, extending
the per-leg increment linearly to f = 3 (the one modelled step, named as such).
Stated in the doc, the printout and the assertions: this is a LOWER BOUND on
the inter-leg glue. The two-leg node shares a transcript, a Phase A and a
LogUp closure but carries no binding legs -- no register chain, no attestation
join, no published-root compare -- because those are lane A's design and
inventing them here would measure my guess rather than the machine. Safe in
one direction: if fan-in 3 misses the rule even here, it misses.
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.
Measures lever 0 — what a per-table aggregator pays to open a wrap proof whose hash matrix is 316/436/612 columns wide instead of 3,056 — by closed form over the real AIR shapes, plus an emission arm at fixture scale. No proving, no box time on the critical path.
Box status: green. All five tests pass on box B at
a8d7d081(5 passed; 0 failed; 0 ignored, 1.68s) andmake lintat the same head exits 0. Logs:relays/C_rerun2_a8d7d081.log.An earlier run at
1de0e3b4found a bug in the census itself — the BLAKE3 tenant namedHasherKind::Blake3, which instantiates the BLAKE3 socket asLFM_HASH(2,980 main + 599 aux), a chip the real proof does not carry.hash_pin::BLOCK_HASHERisTeston a BLAKE3-pinned build and the record agrees (LFM_HASH: 4 rows, 0 used, 28 main, 3 aux). Fixed in84940a3fand pinned bythe_blake3_tenant_socket_matches_the_record. It inflated the BLAKE3 baseline by 1,185 blocks/query (1,201 for the socket against the idle chip's 16) and so made lever 0 look bigger than it is; the table below is post-fix.The ratio
Per-query blocks over the aggregator's whole leg, at the recorded per-table wrap's widths and heights (
bench_cache/optladder_2026-08-21/TIP/tip-wrappt-24.stdout, wrap preset blowup 4 / 110 q). The keccak axis is held fixed on both sides of each ratio, because it moves the answer more than the hash does.MEMORY-MODEL§7 lever 0 predicts 0.370× for RPX. That reading takes "1,247 hash-matrix blocks of 1,846 per query" — a batched per-query bill — and applies its share to the per-table format. In the per-table format every table walks its own Merkle path, so the path terms are 63% of the bill and the hash matrix is 24-30% of it, not 68%.The model contradicts its own multiplier, which is a stronger check than my arithmetic disagreeing with its arithmetic. §1.2 puts the per-table/batched compression ratio at the aggregator at 2.44×, and the leaf term is format-invariant (each table's leaf is absorbed once per query either way; only the paths multiply). A hash matrix at 67.6% of the batched bill is therefore necessarily 67.6/2.44 = 27.7% of the per-table one. That is what the census measures.
Agreement with the record, which is what says the method is sound and only the reading was wrong:
The fan-in rule, applied
The block is 10 epochs of 2^22 (measured guest, 39.6M cycles), so 10 wraps. The fan-in decision does not move with that count: a level-1 node costs
f · leg + glue, a function of the fan-in alone, so the wrap count sets how many nodes there are and not how big the biggest one is.Rule: ≥ 25% headroom under 2^21 at fan-in 3 ⇒ 3, else 2.
All four rows are box-MEASURED at
1de0e3b4and are unaffected by the socket fix, which touched only the BLAKE3 baseline.⇒ fan-in 2. Three independent reasons and they agree. The rule fails at fan-in 3 on today's shape (13.5% < 25%). The glue term is known to be under-counted by 34-42% (
MEMORY-MODEL§1.3(iii)), a band wider than fan-in 3's entire headroom; fan-in 2 survives it. And under the emission arm's own measured glue read multiplicatively — the pessimistic bound — a fan-in 3 node lands at 2,109,260 invocations against the 2^21 cliff of 2,097,152: it crosses, and doubles its hash table. Fan-in 2 lands at 1,406,173, still 32.9% clear.MEMORY-MODEL§1.3(iii), +469,710/node)Fan-in 2 clears the rule under all three. Fan-in 3 clears only under the third, which is the least defensible because it assumes the glue has no per-query term at all. The recommendation does not rest on the 0.58% by which fan-in 3 crosses in the second row: it already fails the rule in the first.
The tree is treated as flat in node size: every level reuses the wrap leg, on the assumption that a leg over a level-1 aggregator proof costs about the same, since the chip set and widths are identical and only
LFM_HASH's height moves one power of two. That is the modelling assumption behind reusing one leg cost per level, not a measured figure. Under it the trade is 11 proofs of similar size (fan-in 2) against 7 similar but 33% bigger each (fan-in 3).Level-1 RPX memory over 10 wraps, both affine laws, non-hash floor as a band (863.7 cells/invocation MEASURED from the recorded wrap census, to 1,727.4 DERIVED from §4's aggregator back-out):
Both fit the 128 GiB envelope; only fan-in 2 fits once the glue band is applied.
Two findings this surfaced
F3 — the wrap program's one keccak permutation costs three sub-proofs.
program_idis deliberately keccak over bytes whatever the configuration commits under, and the recorded wrap program's instruction mix readskeccak 1. That single row instantiatesLFM_KECCAK(736+88),KECCAK_RND(1,480+516) andKECCAK_RC, all of which the aggregator must then open: 1,031 leaf blocks per query — 25.3% of RPX's 4,067-block bill, 19.6% of BLAKE3's 5,252. Retiring it is what takes fan-in 3 from 13.5% to 30.6% headroom.F4 — the algebraic emitter arm cannot be exercised on a BLAKE3-pinned branch.
sub_proof.rs:149(SubProofShape::opening_words) andfri.rs:164(FriShape::query_words) size their arena stride fromproof_arena::words_per_root(), which readsWrapHash::production(), whileepoch_verify.rsadvances its cursor byedsl::digest_words(b), which reads the builder. An explicitWrapHash::Algebraicbuild therefore strides 1 against a declared stride of 2 and tripsemit_table_verification's own assertion. It costs this PR nothing — both arms are emitted underWrapHash::Blake3and the block counts are equal at rate 8, which the new hash-invariance test re-checks over exactly these groups — but it blocks the per-table aggregator emitter. Fix: thread the builder's digest width into both functions.What is in the diff
One new file,
prover/src/lfm/per_table_census_tests.rs, plus itsmodline. Four tests:the_lever_zero_factor_is_measured_per_tenant— the gate: the ratio table, the decomposition, the falsification.the_per_table_aggregator_tree_applies_the_rule— the tree, the cliffs, the RSS band, the rule applied under the imported glue constant.the_block_rule_is_hash_invariant_on_every_tenant_group— guards the rate-8 premise the whole method rests on.the_blake3_tenant_socket_matches_the_record— guards the baseline against the socket-vs-commitment-hash confusion the box run caught, and ties the tenant socket tohash_pin::BLOCK_HASHER.the_tenant_leg_emits_and_censuses—#[ignore]d emission arm; puts the closed forms through the real emitter at fixture scale and measures the glue, sweeping the query count so the glue can be split rather than quoted as one percentage.The glue, and why one percentage was not enough
Box B measured emitted − closed form at +56-60% of the leg across all eight tenants (fixture heights 2^12, 2 queries). That is not a number that can be extrapolated. The glue is
F + P·q:Fis the query-invariant per-table spine — the OOD blocks, the 128 terminal coefficients per table, the layer roots, the grinding check — andPis the per-query remainder. At 2 queries the two are indistinguishable, and they reach production's 110 queries by factors 55 apart: the difference between the glue being under 1% of the leg there and 57% of it.Structurally most of it must be
F. For the 14-table RPX tenant the OOD current block alone is Σnum_total_cols= 3,595 extension cells absorbed per leg, and the terminal coefficients add 14 × 128 = 1,792 more — both query-invariant, and together already larger than the whole 3,003-compression glue measured at q=2. So the +57% is a fixture artifact of running only two queries.The emission arm sweeps
qover {2, 4, 8}, fits the line through the endpoints, and asserts the middle point lands within 5% of it, since that affine split is what licenses the extrapolation at all. Measured, box B ata8d7d081:glue(q) = 4398 + 2.5·q2998 + 2.3·q3043 + 2.3·q3109 + 2.3·q1563 + 1.8·q1608 + 1.8·q1674 + 1.8·q2963 + 2.0·qThe glue is a fixed spine with a per-query slope of about two compressions. The structural prediction above holds to the digit: +57% at two queries, 1.1% at 110. ⚠ It is taken at fixture heights, where each table commits 4 FRI layers against production's 12 and walks 13 Merkle levels against 21-25, so
Fis understated at real heights. Correcting for the eight extra layer roots and their ζ samples across 14 tables putsFat roughly 3,222 for RPX, and the glue at production heights and 110 queries at ≈3,600 per leg, about 0.8% of the leg.⚠ This falsifies two of the three glue readings, and the second one was load-bearing
The multiplicative reading is dead: the per-query slope is ~2.3 compressions, not the ~2,000 a ×1.5716 multiplier would require. Its row in the table above should be read as a bound that has now been ruled out, not as a live scenario.
More seriously, the production-anchored additive reading —
MEMORY-MODEL§1.3(iii)'s +469,710 per node, which is what put fan-in 3 at 13.6% headroom — is a residual against a different and coarser leg model. Its own note says the model "counts the 6 verify legs, misses the glue", so the shortfall was attributed wholesale to glue without decomposition. The residual measured here is against a closed form that is pinned to the emitter byepoch_verify_tests, and it is 23× smaller per leg. Those are not the same quantity, and the smaller one is the better-grounded.Under the measured glue, with production-height legs:
⇒ How to read the verdict
Fan-in 2 is the conservative default, not a measured result. The leg is measured; the glue is not, and the verdict turns on the glue.
The two glue numbers do not contradict each other, and this is the reason: this PR's emission arm emits ONE leg, and a single-leg fixture structurally cannot contain inter-leg glue — the binding between the legs of a real multi-leg aggregator has no counterpart in it. So the ~1.1% measured here is a lower bound on a different quantity, and §1.3(iii)'s constant is a residual against a coarser model. Neither settles it.
Fan-in is decided by
Ffrom the production-height emission below; fan-in 2 is the default until it prints. The tree test is namedthe_per_table_aggregator_tree_applies_the_rulerather than anything with "measured" in it, precisely so the name cannot be read as a claim the evidence does not support.The deciding measurement
the_rpx_leg_emits_at_production_heights(#[ignore]d) re-fitsglue(q) = F + P·qat the recorded per-table wrap's own heights, so the verdict stops resting on a height extrapolation from 2^12. It emits at one leg and at two, because a single-leg fixture is exactly what could not answer the open question:F(2 legs) − 2·F(1 leg)is the inter-leg glue, the part of a multi-leg node that is not its legs added up. The emitter is generalised to N legs, every sub-proof of every leg taking its own fork index over the whole set.The query sweep stays at {2, 4, 8} deliberately.
Fis the query-invariant intercept, so measuring it needs production heights, not production queries: a 110-query emission at these heights padsLFM_BLAKE3to 2^19 × 3,112, roughly 13 GB for that chip alone, and yields the same intercept that 8 queries does at about 800 MB. The rule is then applied at 110 queries with the measuredFandP, extending the per-leg increment linearly to fan-in 3 — the one modelled step, named as such.⚠ It is a lower bound on the inter-leg glue, and the verdict is safe in one direction only. The two-leg node shares a transcript, a Phase A and a LogUp closure over a fork space of 2 × tables, but carries no binding legs: no register chain, no attestation join, no published-root compare. Those are lane A's design, and inventing them here would measure a guess rather than the machine. So if fan-in 3 misses the rule even at this bound, it misses; if it clears here, lane A's real node still decides.
Open risks
The non-hash floor is a band, not a number; the emission arm is what closes it. Every non-hash chip height is held at its recorded value under the algebraic tenant, which is conservative for
BITWISEandLFM_BITDEC. The 2^22-epoch correction to the wrap-proof shape is unapplied and runs in the helpful direction, a few percent at most.make lintexits 0 ata8d7d081. The one number still imported rather than measured is the inter-leg glue; the ratio column above is the box's own per-sub-proof output with the bogus 2,980-columnLFM_HASHsub-proof replaced by the record's 28-column one.