BLAKE3 as the LFM machine's real hash — F3.4 retired (draft) - #930
Draft
MauroToscano wants to merge 168 commits into
Draft
BLAKE3 as the LFM machine's real hash — F3.4 retired (draft)#930MauroToscano wants to merge 168 commits into
MauroToscano wants to merge 168 commits into
Conversation
The Lambda Field Machine (LFM): a fixed, straight-line, field-native machine for verifying our STARK proofs. The program is the machine's preprocessed columns — addresses, opcode selectors and multiplicities are committed program data, the main trace carries values only — and memory is write-once, closed by pure LogUp balance with no timestamps and no ordering lookups. No pc, no branches, no fetch/decode. Fourteen chips, frozen order: CONST, BALU, XALU (Fp3), SELECT, BITDEC, HASH, KECCAK, LANES, HINT, PUBLIC, RANGE, then the production KECCAK_RND / KECCAK_RC / BITWISE AIRs hosted unchanged. Three new buses (LfmMem/LfmRange/LfmPublic, ids 32-34) are the only prover-side additions; no VM table is touched and VmAirs is untouched, so this is a sibling AIR set proved by the same multi_prove/multi_verify_views machinery. Program identity is a digest over the instruction column groups plus the static roots and heights, pinned in LFM_REGISTRY (regenerated by compute_lfm_registry, drift-tested). Resolution fails hard on a miss; there is no runtime off-switch, by design — the registry check is the first premise of the soundness argument in prover/src/lfm/SOUNDNESS.md, which the release-mode admission validator discharges (uniqueness, acyclicity, multiplicity equality, one-hot selectors, padding, arena discipline, keccak tag uniqueness). What the machine can prove today, all end to end and verified through the registry: a trivial program over every chip; a structurally real FRI commitment-opening proof (sponge transcript, Merkle-authenticated openings, unnormalized folds, terminal check); real keccak-f[1600] permutations through the unchanged production AIRs; keccak256 over byte streams, bit-exact against PlatformKeccak256 at eight boundary lengths; and a scripted DefaultTranscript interleaving whose every sampled value matches the real transcript, including buffer refill, absorb invalidation and a raw squeeze. Two soundness holes were found by adversarial construction and are now pinned by permanent guard tests: without preprocessed per-permutation tags a prover can swap two permutations' outputs while every bus still balances, and once the keccak adapter's absorb mode splits PERM_IN from STATE, permute rows need an explicit pass-through constraint or the permutation input is free. Both tests build coherent forgeries — every bus balanced, every claimed value consistent — and confirm that neutralising the single constraint accepts them. The transcript replay is zero-rejection: a straight-line program cannot follow the production sampler's data-dependent rejection loop, so it encodes the no-rejection schedule and is unprovable for a transcript that rejects. That costs completeness only, bounded below 1e-6 per proof at production draw counts (SOUNDNESS.md 6.3).
Two absorb primitives the statement leg needs, both bit-exact against the real DefaultTranscript. append_felt / append_ext render a field element the way append_field_element streams it: the canonical u64 big-endian, and for the cubic extension the three coordinates in order 0, 1, 2. The endianness flip is real work here — with v = hi·2^32 + lo the halves are byteswap32(hi), byteswap32(lo) — so it goes through the canonical bit decomposition with the byte permutation folded into the constant weights, which are the powers 2^0..2^31 interned once and shared by both halves. One BitDec and 64 BALU rows per element. Coordinate order was read from the source rather than assumed: the same file also implements 2, 1, 0, but that impl belongs to the raw [FpE; 3] array type, not to FieldElement<Degree3GoldilocksExtensionField>, whose write_bytes_be — the one stream_bytes calls — writes 0, 1, 2. The splice replaces the segment packer with a byte-granular one. A machine half still drops straight in when the cursor is 4-byte aligned, emitting no instructions, so every aligned program's digest is unchanged (all registry drift tests confirm). When the cursor is misaligned the half straddles two output halves and is split byte-wise: a bit decomposition, two weighted sums over disjoint ranges, and a recomposition assert that pins the input below 2^32 — bit_dec alone bounds it only by p, and a half at or above 2^32 has no four-byte rendering. About one BitDec and 34 BALU rows per spliced half, and only ever on the statement leg. This is deliberately not the single-prefix helper the plan called for. The continuation-epoch statement alternates constant and dynamic runs, and its one-byte fri_final_poly_log_degree field moves every later value from shift 2 to shift 3, so a helper taking one constant prefix and one dynamic run cannot express it. The packer tracks the cursor instead and splices wherever it must; a test pins the alternating shape, and latching the shift instead of tracking it fails that test alone.
The first leg of a real verifier the machine runs end to end: everything a multi_verify does to its transcript before the per-table forks. absorb_epoch_statement emits absorb_statement(ContinuationEpoch) byte for byte — domain tag, ELF digest, length-prefixed public output, the fourteen TableCounts, the private-input page count, the FRI terminal degree, the runtime page ranges and the trailing epoch label. replay_phase_a then absorbs each sub-proof's preprocessed commitment (only when the air has one) and its main trace root, and samples the shared LogUp challenges z and alpha. Every multi-byte field in this encoding is little-endian, unlike append_field_element's big-endian rendering, so a u64 carried as [low32, high32] halves needs no byte manipulation — the only cost is misalignment. The domain tag is 30 bytes and the fri_final_poly_log_degree field is one, so the statement runs 207 + public_output_len + 16*page_ranges bytes, which is always three past a half boundary. Every Phase-A root absorb is therefore spliced, at one BitDec and about 34 BALU rows per half; a single pad byte in the statement encoding would make all of it free, which is worth considering whenever that encoding is next versioned. Shape-static fields are program constants rather than arena reads, because they determine the shape: the table counts and page-range list fix how many sub-proofs Phase A absorbs, and num_private_input_pages fixes the AIR layout. A program reading them from an arena would claim to verify a shape it was not compiled for. Only the ELF digest, public output and epoch label are per-proof. The acceptance test's oracle is the production absorb_statement_with_digest itself, not a reimplementation — that encoding has ten fields and is exactly where a replay would go wrong. Phase A is a four-line transcription of replay_transcript_phase_a_view, since calling it would mean synthesising AIRs and proof views for three fake tables and would test the fakes. The machine's z and alpha match, executed and proved, and both tamper vectors reject. The continuation tag is now pub(crate) so the replay emits the identical literal; a second copy would drift silently on a version bump, and the tag only works if both sides agree on it.
…ifact Constraints exist today only as compiled code plus a program the AIR hash-conses on demand. A recursion machine that evaluates constraints needs them as DATA, and capture is far too expensive to run in a guest. Add `ConstraintArtifact`: the flat program, the per-constraint metadata capture discards (kind and end_exemptions, i.e. the zerofier shapes), the AIR shape scalars, and the composition degree multiplier. That last one is easy to miss — it lives in neither AirContext nor ConstraintMeta, only inside the ConstraintSet impl and the LogUp layout, yet the verifier needs it to size the composition polynomial. Stored as `composition_poly_degree_bound(n)/n` so it is an observable of the public trait rather than a new trait method. ProofOptions is deliberately excluded: AirContext bundles the options in with the shape scalars, but the captured program does not depend on them, so one artifact per table covers every blowup factor. That premise is pinned by a test rather than assumed. Scope the verify-path prohibition to what it was always about. The rule was "never call constraint_program() at verify time"; the real hazard is CAPTURE, not constraint programs as such. `constraint_program()` still panics by default and may still capture. The new `precaptured_constraint_program()` never captures under any circumstance, so it is safe on a guest path, and `AirWithBuses::with_precaptured()` supplies a build-time program. The two are separate methods rather than one with a flag so an accidental verify-path call to the capturing one still hits the panic. Nothing is wired into the production verify path. Tests: all 25 production tables' artifacts are serialized, read back, and evaluated against the compiled folders on random frames — on the prover shape, the verifier/OOD shape, and the flat device blob. Everything after the codec runs the DESERIALIZED artifact, so a codec bug cannot hide behind the in-memory object. Nonzero end_exemptions and the rejection paths are covered in the stark crate, because no production constraint uses exemptions and a suite where every artifact validates cannot show that validation is able to reject. The 25-table list had been hand-copied into three test suites, so a table added to one and forgotten in the others lost that suite's coverage silently. It is now `test_utils::production_airs` once. Measured: 73,539 nodes / 1,220,256 bytes across the 25 tables; ECDAS, ECSM and KECCAK_RND are 85% of it.
An epoch's public_output is collected one byte per COMMIT operation, so its length carries no alignment guarantee and the aligned-only path was not enough for the target. append_bytes_misaligned takes a byte length, absorbs the whole halves, and masks the trailing one to its live bytes. The mask pins the unused high bytes to zero, which is a soundness obligation rather than tidiness: those bytes are arena data past the encoding's length prefix, so without the pin a prover could put anything there and change the absorbed byte string while the length said otherwise. Dropping the pin makes the machine accept exactly that, which is what the new test catches. Placing a value at the cursor is now one routine for both a whole half and a masked tail, since they differ only in width. The aligned case still emits no instructions, so every existing program's digest is unchanged. Two corrections to earlier analysis, both now machine-checked rather than asserted in prose. The statement is 207 + |public_output| + 16*ranges bytes, not 223. And the shift Phase A inherits is (3 + |public_output|) mod 4, not unconditionally 3 — that claim quietly assumed an output length divisible by four. It is zero whenever the length is 1 mod 4, so the Phase-A splice cost is workload-dependent and vanishes entirely for about one workload in four. The acceptance shape now uses a 14-byte public output so it exercises both new paths at once: an unaligned length, hence a masked trailing half, and a nonzero inherited cursor, hence a spliced Phase A.
KECCAK_RND costs 24 rows per permutation at 1480 columns, so a single instance saturates a 2^19-row table at ~21.8k permutations while a real proof wrap needs ~460k. Split it the way the RV64 VM splits its own tables, with one simplification: the chunk count is static program shape, fixed at compile time, pinned in the registry and bound into the program digest -- never derived at prove time, never read off the proof. Splitting the rows needs no pairing logic because KECCAK_RND has no row-to-row transition constraints: its 24-round chain is carried by Keccak bus tokens rather than row adjacency, so LogUp cannot tell which instance a row lived in. KECCAK_RC and BITWISE stay single shared instances -- their multiplicities are totals over the whole proof. roots and log_heights stay 14-wide chip-class arrays; only the AIR and trace lists expand at slot 11. The digest now absorbs the chunk count, which moves all five program_ids; every root and log_height survived unchanged. Registry regenerated. 105 lfm tests pass (was 92).
Brings KECCAK_RND chunking together with the transcript and statement replay. Both sides had grown since the split, so this is a real merge: the chunking work was written against the machine before the replay legs existed, and the replay legs against a single-instance KECCAK_RND. Two conflicts, both mechanical. machine_tests.rs: each side appended its own tests at the same point, so both blocks are kept. registry.rs: both sides moved the generated program digests, so the block is regenerated rather than resolved by hand — the chunk count now enters the digest, and all six programs re-derive cleanly. Chunking is a saving, not a cost: one table pads once to a power of two for the whole program, N chunks each pad to their own, so at wrap scale (460k permutations) 22 chunks total 11.0M rows against a single table's 16.8M — 34% fewer, and the single table would be unbuildable anyway. The split needs no pairing logic because KECCAK_RND has no row-to-row transition constraints: the 24-round chain is carried by the Keccak bus, so rounds are linked by token matching rather than row adjacency, and LogUp cannot tell which instance a row lived in. Chunk boundaries need not even fall on permutation boundaries, which is pinned positively by a test that re-splits 2+1 as 1+2 and still verifies. 118 tests green, lint clean.
Everything the machine has consumed so far was synthetic or self-generated. This produces an actual continuation proof in exactly the encoding the RV64 recursion guest receives, so the next slice can read production bytes. The encoding is not invented. The guest never sees a ContinuationProof — it gets a blob in private input and reads it zero-copy through rkyv — so a machine-side reader over bytes is the direct analogue of the guest's reader, and a disagreement between the two is a meaningful signal rather than an artifact. Reaching into the in-memory bundle would exercise a path production does not have. The existing dump test produces the same bytes but is #[ignore]d as a diagnostic, driven by five environment variables, and writes to a fixed /tmp path, none of which works from a deterministic unit test. So this reuses its two encoder calls — prove_continuation then encode_continuation_guest_input, both already public — and none of the harness around them. The encoder is the part that must not drift. The epoch size is measured rather than assumed: the fibonacci guest yields one epoch at 2^6, 2^8 and 2^10 cycles and two at 2^4, so it runs somewhere between 17 and 64 cycles and only a 16-cycle epoch splits it. A single-epoch fixture would defeat the point when the target is a continuation. The cache lives outside the repository. A checked-in binary can drift from the encoder without anything noticing, so the generation path is what a cold run exercises.
The three continuation-only AIRs — l2g_global_air, l2g_memory_air and global_memory_air — were private fns in continuation.rs and appeared in none of the per-table IR suites. None of those suites asserted a count, so the blind spot was uniform and silent. It is not a tidiness problem. The proofs the recursion path verifies are continuation proofs, and these three are exactly what such a proof adds. A per-table sweep that stops at 25 is complete for a shape we do not care about. l2g_memory_air carries real constraints; the other two are EmptyConstraints but still need shape, metadata and a degree bound. production_airs() now yields all 28 and every suite asserts its length, which is worth more than the dedup itself: without it the next added table escapes every per-table suite at once, exactly as these three did. Three new tests: - artifacts_are_invariant_across_trace_length. The axis is structurally absent — no AIR constructor takes a trace length — so the only route to the artifact is composition_poly_degree_bound(n), which the artifact stores divided by n. That division is sound only if the bound is exactly linear, so this sweeps n = 2^4..2^24 per table instead of trusting capture's two probe points. - parameterized_airs_vary_per_parameter_value. Four tables fold a workload-dependent value into their IR as a constant: PAGE and GLOBAL_MEMORY a page base, both L2G tables an epoch label. The test characterizes rather than asserts this away, and it corrected my own assumption: the variation is NOT confined to constant values. The builder interns constants, so a value already in the table costs no node while a fresh one appends, shifting later node ids and the constraint ROOTS. L2G_GLOBAL moves 47->48 nodes between epoch labels 1 and 7. "Emit one program and swap a constant" is therefore not an available fix; what is invariant is the algebra, which is what makes the runtime-uniform promotion viable. Proposed in others/lfm-page-base-uniform-proposal.md; no semantics touched here. - global_memory_private_input_is_a_second_shape_not_a_second_program. is_private_input is a second axis but an enumerable one: same program, differing only in the preprocessed-column fields. Also records what the all-zero end_exemptions finding actually buys: production zerofiers are uniform, so the GPU path's uniform-zerofier precondition holds in fact rather than by luck, and a consumer needs one zerofier per AIR rather than one per distinct exemption value. The ExemptConstraints coverage stays so the field cannot rot into being untested. Measured, 28 tables: 73,722 nodes / 1,223,896 bytes. The continuation tables are small — 47, 93 and 43 nodes.
The arena filler's first half: open the guest's wire-format blob, read the archived bundle in place as the recursion guest does, and lay an epoch's main-trace Merkle roots out as arena halves. Reaching the epochs needed an accessor, and the shape of it matters. The archived struct's fields inherit their visibility from the source, so relaxing ContinuationProof::epochs would have opened the owned type at the same time — which is the thing worth avoiding, since the recursion guest never holds an owned bundle. The accessors are therefore methods on ArchivedContinuationProof alone, exposing only the path verify_continuation_archived already traverses. Each root is packed into its own eight halves. An arena is a vector of words, not a byte stream, so concatenating fields and packing afterwards would let any field of non-multiple-of-four length shift everything behind it — silently, since the halves count still comes out right. Measured on the fixture: the intermediate epoch has 24 sub-proofs and an 8-byte public output, the final one 25 and an empty output. That matches the expected per-epoch table count (split-table chunks, plus ten fixed tables on the final epoch and nine elsewhere, plus pages, plus the epoch-local L2G), and it independently confirms the 24-table structural minimum the completeness bound in SOUNDNESS.md quotes. One thing the bytes cannot supply: the preprocessed commitment Phase A absorbs comes from the AIR set rather than the proof, so replaying Phase A against a real proof will need the epoch's AIRs rebuilt, not just its blob. Flagged here rather than discovered later.
… in the blob The completeness bound in SOUNDNESS.md instantiated its worked example at 24 tables and said so as a structural minimum, hedged because nothing had checked it. Reading a real two-epoch continuation proof gives 24 sub-proofs for an intermediate epoch and 25 for the final one, the extra being HALT, so the hedge can go. Also adds the check behind the preprocessed-root question: the guest input carries the DECODE commitment and the per-page genesis commitments as public fields, so replaying Phase A needs no access to the epoch's AIR builder. Worth noting the fixture has no page commitments at all — fibonacci touches no data pages — so that path exists but is not exercised by this test.
Design (α) from lfm-design.md §3 — how a serialized ConstraintArtifact becomes LFM instructions. Design only; no semantics touched. Adds constraint_op_census as the instrument behind it: a per-AIR breakdown of nodes into leaves, pooled constants, foldable subtrees and extension ALU work, so the instruction estimate is measured rather than asserted. Printed with only a loose ceiling, because pinning exact counts would turn every constraint edit into a test failure. Budget holds. 28 AIRs give 64,842 constraint-leg instructions plus 2,150 beta-folds = 66,992, against the design doc's ~69K at 25 — and a MulAdd peephole takes it to 57,923. The correction that matters: the IR's dim tags describe the PROVER, and the machine runs the verifier. At the OOD point the frame is all-extension, so a node is base only when its whole subtree is constants. The IR declares 42,137 base arithmetic nodes; 2,916 are actually base at verify time. Anyone sizing this leg from the declared dims would understate extension traffic by 14x. MulBase eligibility falls from 9,413 to 5,041 for the same reason — and the 2,916 that are genuinely base are constant-only subtrees the emitter folds at build time for zero instructions. Two lowering arms are not the obvious ones. Op::Neg has no instruction — ExtOp is Add|Sub|Mul|Div|MulAdd|MulBase with no unary negate — so it lowers to a subtract from the pooled zero. Op::Embed emits nothing at all: under the [F;4] lane-3-zero word model a base value (v,0,0,0) is already its own extension embedding. Both are measured at zero occurrences in production, along with ConstExt, so all three arms are correctness-only today and should stay. The uniform-zerofier finding is worth ~50,900 instructions: with every constraint sharing Z = zeta^N - 1, the division factors out of the beta sum and is evaluated once per AIR instead of once per constraint. Two scaling caveats recorded rather than buried. The total is per distinct AIR, not per epoch — each sub-proof needs its own evaluation and chunking gives a family several, which is the one place the design doc's figure reads optimistically. And the leg is workload-shaped: ECDAS, ECSM and KECCAK_RND are 86.9% of it, so an epoch with no elliptic-curve work drops 65%. Nothing in the IR is structurally inexpressible on a straight-line machine. The stronger statement: the IR's own invariant that nodes[i] references only nodes < i is identical to the machine's acyclicity premise, so dense address assignment in node order satisfies it by construction.
The ISA inventory landed four facts that move the estimate, so the design and the census are updated to match rather than left to be reconciled by a reader. MulAdd costs the same single row as Mul. That makes fusion mandatory, not an optimization: emitting Mul then Add where one instruction would do is pure waste, and the node count is an upper bound rather than an estimate until it is applied. 9,069 fusable pairs take the leg from 66,652 to 57,583 — so against the design doc's ~69K, which implicitly assumed roughly 1:1 with nodes, the real figure lands 16.5% under. Constants are interned program-wide, keyed on the canonical 4-lane word, so summing per-AIR pools overcounts: 655 becomes 315 actual Const rows. More than half the apparent constant cost was the same small structural values duplicated across tables. MulBase is reframed. It costs the same row as Mul, so it is not a reduction — it is a routing obligation, since lowering an ext-by-base multiply by hand costs 4+ rows. 5,041 sites, and the count would be 9,413 and wrong if taken from the prover-side dims. Base-to-extension conversion is free, which confirms independently that Op::Embed emits nothing. The converse costs a LANES row, but this leg never needs it: nothing in the IR narrows an extension value, since Dim only ever widens through binop's join. The doc now also separates what I verified myself — the op inventory, Neg having no ISA counterpart, Embed and ConstExt being unused, the absence of narrowing, and every count — from what I took from the inventory on report, so a wrong cost fact invalidates the row conclusions without touching the instruction counts.
Adds epoch_chunk_multiplier, which builds real traces so the chunk counts are the prover's own splitting rather than a reconstruction of it, and weights them by each AIR's constraint-leg instruction count. Measured: 64,712 instructions at 1M cycles, 65,996 at 2M, 95,532 at 20M — a 1.01-1.49x multiplier over the per-distinct-AIR figure. Small, and for a structural reason: chunking multiplies the cheap AIRs (CPU is 489 instructions, MEMW_R 153) while the expensive ones are never chunked at all. So lfm-design.md §5.2's ~69K was closer to right than my earlier warning implied; the correction is a growth term in epoch size, not a multiplier on the whole figure. CORRECTION to my own claim. The design doc previously said the leg was workload-shaped — that ECDAS, ECSM and KECCAK_RND being 87% of the total meant an epoch without elliptic-curve work would drop 65%. That is false. FIXED_TABLE_COUNT is documented as tables that always contribute exactly one sub-proof regardless of TableCounts, and ecsm and ecdas are on that list: a zero-row table still needs its sub-proof, since dropping it would remove its constraints from verification. The fib fixtures use neither elliptic-curve nor keccak work and still carry the full 60,389-instruction fixed block. The leg is essentially workload-INDEPENDENT. I asserted the reverse from the census alone, and the census cannot see how sub-proofs are assembled. The uniform proposal is revised against the gate ruling. The gate cleared, but my premise was wrong in my own favour: I argued the promotion was safe because page_base is already bound by the preprocessed commitment, and it is bound by nothing — not the commitment, not the transcript, and program_id only for ELF-backed data pages. The conclusion survives and is stronger, but the reason was backwards, so the invariant is now stated as load-bearing rather than as a note: the uniform must be populated from the same verifier-side sources as today and never from the proof or trace, precisely because nothing downstream would catch it if it were. Also retargeted: continuation epochs pass page_configs = &[], so create_page_air is never called there and GLOBAL_MEMORY is the AIR on the critical path. And epoch_label is not symmetric with page_base — it comes from the verifier's own enumerate() position, so there is no supply route to get wrong; recommending they move together as equal risk was wrong. Per the ruling, the hash-consing-versus-fusion trap now lives as a comment on ConstraintArtifact rather than only in the design doc.
…ed shape The monolithic multiplier was the wrong shape for the target. A continuation epoch passes page_configs = &[], so PAGE never appears, and it carries an L2G_MEMORY sub-proof instead; intermediate epochs also drop HALT. Computed: 63,393 instructions over 24 sub-proofs for an intermediate epoch, 64,094 over 25 for a final one — 14 split families at their minimum one chunk each (3,640), nine fixed tables (59,688), one L2G_MEMORY (65). The 24/25 sub-proof count was measured independently on the LFM fibonacci epoch fixture, so the test asserts this composition reproduces it. That turns the epoch shape from something the design doc infers into something a test pins: if the composition changes, the arithmetic stops matching and this fails rather than the doc quietly going stale. 94% of the epoch leg is the fixed block, which is the sharpest form of the workload-independence correction — the leg is ~63K regardless of what the workload computes, growing only with epoch size as the cheap AIRs chunk. Also records the global proof's contribution: 27 instructions per epoch for L2G_GLOBAL plus 25 per touched page for GLOBAL_MEMORY. That is what settles the page-base question as an identity problem rather than a size one — even a four-figure page count is noise against a 63K leg. What remains inferred is narrower than before: only the chunk growth curve for a large continuation epoch, which is still derived from monolithic runs.
Closes the last inference in the epoch numbers. The previous §8.2 figures came from monolithic runs, which cover a whole execution rather than one epoch's 2^epoch_size_log2 cycles and carry a different table set. continuation_epoch_chunk_counts_measured drives the actual continuation path — Executor::resume_with_limit for one epoch, then Traces::from_image_and_logs. Proving is deliberately skipped: epoch 0's register_init comes from the entry point rather than a previous epoch, and every intermediate epoch runs exactly epoch_size cycles by construction, so epoch 0 is representative and the register chaining that would need proving has no bearing on table sizes. At 2^20 cycles an epoch has 16 chunked sub-proofs (CPU and MEMW_R each split in two), 26 in total, for 64,035 instructions — against the 24-sub-proof, 63,393-instruction minimum at 2^19 or below. Doubling the epoch past CPU's chunk bound costs 642 instructions, and that is the whole growth term, so the leg is 63-65K across any plausible epoch size. The monolithic 1.49x at 20M cycles was an over-estimate for an epoch, which is capped by construction. Two things fell out of running it that are worth more than the numbers. fib_iterative_2M and array_multipass_20M produce identical chunk counts for their first 2^20 cycles — workload independence visible directly rather than argued from FIXED_TABLE_COUNT. And the test asserts page_configs is empty, so "a continuation epoch never builds PAGE" is now pinned by a run instead of read off a comment. The design doc also now states the consequence that was buried in an erratum: a leg that is 94% fixed means the emitted program barely varies with workload, so the registry's profile ladder is one-dimensional in epoch size rather than a cross-product of workload classes and shapes. And the census's own doc comment now records what that instrument cannot see — how sub-proofs are assembled — naming the false claim it produced, since the next reader will reach for the per-AIR table the same way.
…l path Follows from the epoch composition already measured, and I had not taken the step. An epoch proof is 14 split families plus 9 or 10 fixed tables plus one L2G_MEMORY: no PAGE, since page_configs is empty, and no GLOBAL_MEMORY, which lives in the global proof. So the only parameterized AIR in an epoch proof is L2G_MEMORY, whose parameter is epoch_label. epoch_label is index + 1, so unpromoted the registry needs one distinct program per epoch index and the ladder grows linearly with epoch count — exactly the workload-dependence a 94%-fixed constraint leg was just shown not to have. page_base reaches the machine only through GLOBAL_MEMORY, which is the global-proof leg and a later concern. Records the epoch_label threat model, which is sharper than the page case rather than softer. epoch_label pins an epoch's POSITION in the chain: it is the constant in the IsB20 cross-epoch ordering check, and the fini_epoch the next epoch's token consumes. Today the verifier builds that AIR from its own enumerate() index, so a prover cannot assert a different position. If the uniform were ever sourced from the bundle, inflating the label would relax the ordering range check, and free choice of labels would permit two epochs to claim one position (replay) or to claim positions out of order (reorder). page_base risks a wrong address; this risks the integrity of the chain itself. The invariant is therefore the same shape as the page one for a different reason, and it is easier to honour — the value is a loop counter the verifier already computes, so no plausible implementation reads it from the proof unless someone deliberately adds a route. It is written down so that nobody does. Acceptance is three criteria, and the second is the real one: the existing epoch-ordering rejection tests, which pop and swap epochs in a proved bundle, must pass unchanged. A promotion that required editing them is a promotion that broke something.
R1f (c)+(d). The machine now walks one FRI query's main-trace opening from a real two-epoch continuation proof to that proof's own committed root, proved and verified. This is the first time it touches production-committed data. The walk could not reuse edsl::merkle_walk: that one compresses with LFM_HASH/TestPermutation, the non-cryptographic Milestone-C placeholder, so it can only authenticate the Milestone-C fixture tree. Production trees are keccak throughout, so edsl::keccak_merkle_walk is new, built on the bit-exact keccak256 emitter and the big-endian element rendering. Conventions read from source and re-verified: a leaf is the ROW PAIR 2i, 2i+1 written column by column with every element big-endian, and a parent is keccak(left || right) — 64 bytes, no domain separation, no ordering flag, so one permutation per level and the ordering carried entirely by the index bit. The leaf index is not in the proof: it is the FRI query challenge, and deriving it needs the epoch's statement and AIR set, neither of which a byte blob carries. It is recovered by exhaustion against production's own path checker, which asks the proof rather than inventing an answer. The opening this leg authenticates is the only one of the fixture's 49 sub-proofs that combines a deep tree with a unique index — most tables are mostly padding, so identical rows give identical leaves and every index verifies, which would make the index-tamper vector vacuous. A test pins that property. Tamper runs both ways round. Incoherent (change an input, still claim the real root) fails the in-machine root assert. Coherent (also claim the root the tampered inputs really fold to) proves cleanly and then fails on the one thing it cannot fake: the published root is not the committed one. MEASURED, and it refutes the prediction the leg was set up to confirm. The handoff expected byteswapping to dominate the leaf, reading row counts: 20 BITDEC + 1280 BALU rows against 22 permutations. The rows are right and the conclusion is not, because rows of different chips are not comparable — an LFM_BALU row is 4 non-preprocessed columns while a permutation expands into 24 KECCAK_RND rounds of 1480. In main-trace cells one permutation costs 113 byteswaps, and hashing dominates at every width in the fixture: 124x at the 10-column table, 8.9x at 511, 7.4x at 1480, flattening near 6.6x rather than inverting. A byteswap chiplet is not the lever it looked like.
Planning the implementation surfaced a better design than the proposal specified, so it is captured before any code rather than made unilaterally in it. The first sketch threaded a uniform slice through every evaluation entry point — eval_program, eval_program_verifier, eval_device_program and the shared interp helper — which is substantial churn across both walkers, the CUDA host side and every caller, for a value that behaves exactly like a constant at evaluation time. Instead the uniforms resolve into the program struct alongside the constants: ConstraintProgram and DeviceProgram each gain a base_uniforms table that OP_BASE_UNIFORM indexes exactly as OP_CONST_BASE indexes base_consts, while the artifact stores only the count. No evaluation signature changes at all; the CUDA kernel gains a buffer uploaded the same way base_consts already is rather than a new host parameter; and the AIR fills the table at construction from its own verifier-derived value, which is where that value naturally lives. The refinement creates a hazard worth stating rather than discovering: ConstraintProgram becomes a hybrid of program identity and per-instance values. Anything that hashed one including its uniforms would reintroduce the per-epoch digest this whole change exists to remove. It is latent today, since only the artifact is hashed and it carries the count alone, but it belongs in review either way. Also makes program() error when uniforms are required rather than defaulting them to zero, so a forgotten supply is loud. Implementation is deliberately not started. A multi-file semantics-adjacent change half-built is worse than one not begun, and this design decision wants agreement before it lands. The handoff records state, what to read first, the falsifications that are not optional, the instruments left behind, and the things a successor would otherwise rediscover.
…lying on it Recovering the same opening twice across runs gave two different leaf indices, which should not happen if proving is a function of its inputs. It is not: two generate() calls on identical inputs — same ELF, same empty input, same epoch size, same options — differ in ~65k of 587k bytes, and the difference reaches the committed data rather than being rkyv padding. Some sub-proofs commit to different roots, that moves the Fiat-Shamir challenges, and different leaves get opened. The tree SHAPE (column counts, depths) is stable across runs; the values in it are not. Two consequences, both handled here. Nothing derived from a specific blob may be pinned as a constant. R1f already works this way — it pins shape and recovers the leaf index from whatever blob it is handed — but that was a judgement call at the time and is now a rule with evidence behind it, recorded on load_or_generate. A pinned index would have passed for exactly as long as the cache file survived, then failed on the next cold run. The cache write is now atomic. The test that regenerates the fixture runs in parallel with tests that read the same path, so a non-atomic write can hand a reader a truncated blob; since blobs legitimately differ run to run, "it worked last time" was never evidence that the race was safe. fixture_generation_is_not_reproducible carries the measurement. It is #[ignore]d because it costs two continuation proofs, and it asserts the divergence is semantic — so if the prover is ever made reproducible, it fails and says which rule can be relaxed.
A partial-tracking accident nearly cost a method rule. Two of these files were swept into a commit on a side branch, then merged back as stale copies: the committed standing-decisions had four method rules where the live one had six, so a fresh checkout would have silently dropped "a deferral's safety argument is itself a claim needing evidence" and "mark provenance; never assert past your evidence" — from the file every agent reads before deciding whether to stop and ask. The fix is to stop having some of them tracked and some not. All of them are versioned now, at their current content: - standing-decisions: pre-authorizations, the stop-and-ask list, and the six method rules, each of which exists because it caught something. - target-shape: what we actually verify (continuation epochs, 28 AIRs), the shape-static principle, and that alignment is a property of the cursor rather than of the field. - migration-riders: changes that are near-free if they ride the hash migration and not worth a proof-breaking change alone. - the team-lead rulings and the agent handoffs, which record why several designs are shaped the way they are rather than the obvious way. - the status log, now carrying both tracks' entries in one timeline. These are working documents, not polished design notes. They are worth keeping because the reasoning in them is expensive to reconstruct: most entries exist because an assumption turned out to be wrong.
The inline values on `chips::keccak::cols` (52 / 252 / 388 / 588 / 788) drifted when R1d widened `PREP_WIDTH` for the reversed-digest columns. The constants were always right — they are derived — but the comments were four low, and reading them instead of evaluating the constants is exactly what produced a wrong per-permutation figure on the first pass through the R1f cost measurement. Real values: 56 / 256 / 392 / 592 / 792. A comment cannot be tested, so the widths the cost model actually depends on get an assertion instead: LFM_KECCAK 792 total and 56 preprocessed, LFM_BALU 4 and LFM_BITDEC 66 non-preprocessed, KECCAK_RND 1480, and the two derived figures — 322 main cells per byteswap, 36,256 per permutation. A wrong width rescales every number in keccak_merkle_opening_cost silently, which is the failure this pins.
The note explaining why R1f authenticates epoch 0's table 0 said it was the only one of the 49 sub-proofs combining a deep tree with a unique leaf index, and my status log put the degenerate count at 47 of 49. Both came from eyeballing a probe rather than counting. Measured: 24 sub-proofs have exactly one verifying index and 25 have several. The real reason the target is right is depth, not uniqueness. It is one of two depth-20 trees; nothing else exceeds 7 and half the sub-proofs are depth 2. Depth is shape, so it survives the blob changing, which the unique/degenerate split does not — that split is therefore described as blob-dependent and left to the run-time assertion that was already there, rather than written down as a fact about the fixture.
Adds the constraint-evaluation leg of the epoch verifier: a host-side pass that turns one AIR's captured transition constraints into straight-line machine instructions, plus the differential that pins it. The pass constant-folds verify-time-base subtrees, eliminates nodes no root reaches, routes ext-by-base products through MulBase, aliases Embed to zero rows, lowers Neg as a subtract from the pooled zero, and fuses Mul/Add pairs into MulAdd under a single-consumer guard (the IR is hash-consed, so fusing a shared product would recompute it per consumer). Acceptance: for all 28 production AIRs, over random all-extension OOD frames with the verifier's next-row pruning applied, the machine's constraint values equal eval_program_verifier run on the deserialized artifact. The cost census reproduces the design's per-AIR table exactly at 64,187 unfused rows; fusion brings the emitted total to 55,147.
Completes the constraint-evaluation leg. emit_quotient computes the shared zerofier by repeated squaring, folds the constraint values against the powers of beta, divides once per AIR rather than once per constraint, and Horners the composition parts the proof claims. Boundary terms are pre-scaled by the zerofier so they keep their own beta powers inside the same fold while still sharing that single division. Both denominators are inverted against the interned one rather than divided directly: the machine reads 0/0 as 1, so a direct divide would silently accept a vanishing zerofier, whereas 1/0 has no satisfying assignment. Checked against a real STARK proof of L2G_MEMORY, with the challenges replayed through the production verifier's own rounds and the out-of-domain grid reconstructed by its own layout, so the oracle is the prover and verifier together rather than a transcription of one formula. Six tamper vectors reject, and the program proves and verifies against its own committed artifacts. Measured: an intermediate continuation epoch's leg is 54,358 instructions plus 2,894 of recombination over 24 sub-proofs, against a 63,393 budget.
…esign Three corrections, all measured by standing tests: MulBase is cost-neutral rather than a 4x routing obligation, fusion saves 9,040 rather than 9,069, and the three dead nodes cost no rows while a separate 2,376 unreachable constants must not be added to the fold column twice. The design's per-AIR table and its 63,393 per-epoch budget both reproduce exactly; the emitter lands 9.7% under with the recombination included.
# Conflicts: # others/lfm-agent-status.log
R1g obligation (ii). The machine ties each epoch's own committed L2G root to the corresponding sub-proof of the global proof — `verify_l2g_commitment_ binding_view` (`lib.rs:993`), emitted and proved against the real fixture. This is the first time the machine reads ACROSS structures; R1f stayed inside one epoch's own sub-proof. Two accessors on the ARCHIVED bundle only, as methods rather than relaxed fields, since rkyv mirrors field visibility onto the archived struct and opening `epochs` would open the owned type at the same time: `epoch_l2g_root` and `global_proof`. Verified on the real bundle first — 2 epochs, 4 global sub-proofs, epoch i's root equals global sub-proof i's main root for both. The epoch count is program shape, so production's `final_proof.len() >= epoch_l2g_roots.len()` guard has no counterpart: a program compiled for n epochs cannot read an n+1-epoch bundle, the arena schema would not match. Tamper covers position sensitivity, which is the point of the check — a bundle whose L2G roots are right as a SET but wrong in ORDER must reject. That vector is only meaningful because the per-epoch roots are pairwise distinct on real data, so a test asserts that rather than assuming it; F35 confirms the assertion fires when the roots are made to coincide. F32 found a real hole in the first version of these vectors. A digest spans two machine words and needs an assert on each, but every tamper byte was in byte 0, so deleting the second assert left all five tests passing. The vectors now straddle both words (byte 0 and byte 31) and F32 fails as it should.
`FriMerkleTreeBackend` and `FriMerkleTree` had zero consumers anywhere in the workspace — the FRI layer commits through `FriLayerMerkleTree` (the pair backend) and everything else through `BatchedMerkleTree`. `Keccak256Backend` fed nothing but those two, so it goes with them. `FieldElementBackend`, the struct underneath, stays: crypto's own `field_element_tests` and `merkle_tests` instantiate it directly across four digest/width combinations. Surfaced while parameterizing the commitment hash — this is why `StarkHash` carries only `Batched` and `Pair`, with no third member for a leaf shape nothing commits. Kept out of that commit so the pure refactor stayed pure.
… its parity oracle Track G of P-a, first piece: the device mirror of the host `blake3_compress_rounds` (prover/src/lfm/blake3.rs:125), which is the reference the CUDA port has to match bit-for-bit. `blake3_compress<ROUNDS>` is a template rather than two functions, so one cubin serves both round counts and the 7-round arm — where the `blake3` crate is a known-answer test — certifies the whole code path (G function, message schedule, counter split, feed-forward) for the 6-round arm that differs from it by a loop bound alone. The round count is a compile-time knob keeping the host's polarity: 7 by default, 6 when the new `blake3-6round` feature makes build.rs pass `-DBLAKE3_ROUNDS=6`. That feature and the host tree's are separate crates' and nothing forces them equal, and a mismatch would be a GPU tree committing under a different hash than the CPU one — no panic, just a proof that fails to verify. `blake3_rounds_probe` exports the cubin's own round count so that is a test failure instead. The parity harness needs a device entry point because the compression is otherwise unreachable from host code; `compress_probe` is that, in the role `build_fri_layer_tree_from_evals_ext3` already plays for the keccak tree. The host reference is duplicated into the test tree rather than depended on: math-cuda cannot depend on `prover`. P-a Stage 1 sinks the real one into `crypto/crypto` and the copy has a TODO naming it. Meanwhile the copy is itself anchored — host-only tests check it against the `blake3` crate over 65 message lengths, so a device-vs-host failure is unambiguously the kernel. Keccak remains the prover's default hash; nothing in the production dispatch reaches this cubin.
… framing The half of the leaf path that does not depend on the open chaining question. The leaf byte encoding does not move under P-a: `leaves_bit_reversed_grouped` serializes each element in canonical big-endian form and concatenates, and `hash_bytes` hashes that buffer. BLAKE3 reads a block as 16 little-endian u32 words, so one 8-byte element becomes the byte-reverse of its canonical high half then of its low half — the whole of the serialization difference from keccak, which absorbs the same bytes as one byte-swapped u64 lane. `Blake3Block` is where the block boundaries, the zero-padded tail and the byte count a final `block_len` comes from live, and it deliberately leaves the sink to its caller: a leaf kernel compresses each completed block into a chaining value, and which chaining construction that is (bare cv-chain vs standard chunk tree, PA-PLAN §1.6) is still open. Everything the struct itself does is the same under either, so the chaining loop drops in on top without touching it. It works at word rather than element granularity because ext3 elements are three felts and straddle block boundaries routinely. The parity tests check the device words against the same `AsBytes` route the CPU commit serializes through, over element counts that both align to and straddle the block boundary, and over deliberately non-canonical raws — the case that canonicalisation is the only thing standing between.
…vice tree walk Twins of `keccak_merkle_level` and `keccak_merkle_tail`, plus the Rust level driver and tree builder mirroring `merkle.rs`. A parent is ONE compression over the 64 bytes of its two child digests: h = IV, t = 0, block_len = 64, flags = CHUNK_START|CHUNK_END|ROOT, digest = the low 8 output words little-endian. That is `hash_bytes(left ‖ right)` — what `hash_new_parent` already is for every host backend — and at 7 rounds it is literally `blake3::hash(left ‖ right)`, so the framing is externally anchored and not merely self-consistent. The framing matches the live LFM socket's `FLAGS_LFMC = 0x0B`. Parents need no chaining, and the reason is stronger than PA-PLAN §1.6 states: the message is a SINGLE block, and over a single block the standard chunk tree and a bare cv-chain are bit-identical. §1.6's answer cannot change a parent unless it introduces a distinct parent domain constant, which §1.3/§1.4's "one family, byte-oriented hash_bytes" argues against — so this part is settled either way. No byte swapping on this path, and not by accident: a digest's 32 bytes ARE its 8 output words little-endian, and BLAKE3 reads message bytes as little-endian words, so on a little-endian device reading a child as uint32_t[8] yields exactly the message words. The leaf path is the opposite case — its input is big-endian field bytes — which is why the two look different. The CPU side of the parity test is the production tree walk (`MerkleTree::build_from_hashed_leaves`) over a backend whose only new code is `hash_new_parent`, so what it compares is the parent compression and the node layout rather than a second tree builder. Tree depths are chosen to run the per-level kernel and the single-block tail kernel both alone and in sequence.
…e kernels `make test-math-cuda` is the authority on these kernels, and it runs only where a GPU does — GPU CI is merge_group-only, so the per-PR runners have none. The kernels therefore had NO per-PR gate: an edit to blake3.cu that broke the hash would reach the merge queue before anything caught it. This closes that. `cuda_host_shim.h` defines away the CUDA execution-space qualifiers and stubs `blockIdx`/`threadIdx`/`blockDim`, `__syncthreads` and `__umul64hi`, so `blake3.cu` can be #included into a host program and its device functions called directly. `make test-blake3-host-kat` then runs, in about a second and with no GPU, nvcc or cargo: the official BLAKE3 vectors at 7 rounds, the same vectors as a 6-round negative control, the ten canonical vectors at BOTH round counts across all 16 output words, the field-element serialization including non-canonical raws, the block framing and its zero-padded tail, and the Merkle parent. The two vector tables are embedded rather than read at run time. That is deliberate: a test that loads its vectors from a file passes silently when the load finds nothing, which is a failure mode this harness actually hit while it was being written. A table cannot have a zero-vector run, and main() asserts the counts as well. Provenance is recorded per table — the official vectors from the tracked reference JSON, the 6-round column from #903's Python oracle, which is what makes it a known-answer test for the six-round arm rather than a comparison against the code the expectations came from. Checked that the gate can fail, three ways, each restored afterwards: a rotation constant 16 -> 17 (331 failures), two message-permutation indices swapped (322), and the counter halves swapped (320). Scope, stated in the target's comment so nobody over-trusts it: arithmetic only. Whether nvcc accepts the file, and every property of execution rather than arithmetic — grid indexing, the Merkle tail's barrier walk, device alignment, register pressure — stays with the GPU suite. Necessary, never sufficient. Left standalone rather than folded into an aggregate target; wiring it into pr_main.yaml is a separate call. Verified under clang++ on macOS and g++ 13.3 on Linux, warning-free on both, same digests.
`lfm/proof.rs` passed `StorageMode::default()` to `multi_prove`, so the wrap proved in RAM no matter how the prover was built or configured — `disk-spill` was compiled out by default and pinned off even when compiled in. The wrap is the one prove call whose peak is a sum over sub-proofs, which makes it the call that most wants the option. `auto_storage::decide_lfm` is deliberately not `decide`: that one estimates from the RV64 executor's `TableLengths`, and the wrap has no analogue of one — its table set is program shape, fixed before execution, and its dominant family (`KECCAK_RND`, one table per chunk) has a column profile the estimate was never calibrated against. `FORCE_DISK_SPILL` decides it instead. Two test knobs, both defaulting to today's behaviour exactly: `LFM_WRAP_QUERIES` raises the blowup-8 wrap's inner query count above 1, which is how the residency ladder walks it up until a box refuses it, and `LFM_CENSUS_INPUT` supplies the inner guest's private input. The second is what makes the fixture path runnable at all: the fibonacci guest reads its iteration count from private input and the fixture passes none, so it halts inside the first epoch and every test asserting an INTERMEDIATE epoch fails.
…te it in the fused task Round 1's main commit is a phase-wide barrier, so today every table's main LDE stays resident from its commit until its fused task runs: O(N x main_cols x lde_size), and on the LFM wrap that is the dominant term (11.56 of the 13.4 GiB marginal per KECCAK_RND chunk, 532-1,538 GiB summed over a real epoch's chunks). Fiat-Shamir needs the main ROOTS absorbed before the shared LogUp challenges are sampled; it needs nothing of the buffers. `ResidencyMode::RecomputeLde` takes that seam: the commit runs unchanged, the root goes into the transcript, the Merkle tree is KEPT, and the LDE is dropped. The table's fused task rebuilds it from the still-resident trace into a buffer that dies with the task, turning the N-way retention into a k-way transient. Keeping the tree is what makes the rebuild one forward NTT and not an NTT plus a full leaf re-hash — and it removes the "recomputed root must match" hazard entirely, because the root openings are checked against is the one Round 1 absorbed. The commit and the recompute now share `expand_main_lde_row_major`, so the recomputed buffer is bit-identical to the one the tree was built from by construction rather than by argument. `Retain` is the default and every existing caller passes it, so nothing moves. Under `RecomputeLde` the mode also releases each table's aux columns from the caller-owned trace once that table's proof exists — documented on the enum, since it mutates caller-visible state — and forces the host path per table under cuda, the same posture disk-spill takes. `debug-checks` forces `Retain`: it reconstructs Round 1 from retained state between the aux and rounds stages. The dropped slot carries no buffer at all (`MainLdeSlot::Dropped`), so a consumer added between Round 1 and the fused task cannot read empty data believing it is an LDE — it handles the recompute arm or it does not compile.
Four oracles on the three-table LogUp instance, all on the mechanism rather than on a golden blob: every commitment root is unchanged; the whole serialized proof is byte-identical (openings, FRI decommitments and grinding nonce included); a proof made under RecomputeLde verifies with the standard verifier; and the caller-visible half of the contract — aux columns freed under RecomputeLde, still there under Retain — is pinned so a caller that needs them after proving finds out here. Comparing serialized proof bytes is normally avoided because a committed golden blob turns every format change into a failure. There is no blob here: both sides are produced in this process from the same traces and differ only in the mode, which makes byte equality the sharpest available statement of "invisible to the proof". It is the oracle the closed streaming-prover work used for the same change. Checked against a control: injecting a one-field-element error into the recomputed buffer fails all four.
An explicit knob for the same reason the wrap's storage mode is one: there is no calibrated peak estimate for the wrap to decide from, and the trade — one extra forward NTT per table against dropping the O(N) main-LDE retention — is only worth taking when N is large. The fixture wrap has one or two KECCAK_RND chunks and would just pay the NTT; a real epoch has 23 to 133. `lfm_prove_with_residency` takes the mode explicitly so a test can prove the same program under both modes in one process without touching global state. That is what the wrap-level oracle uses: it proves and verifies the fixture wrap twice and compares the rkyv bytes. Unlike the stark-crate oracle it covers preprocessed tables (whose main LDE carries the precomputed columns the split trees were built from), KECCAK_RND chunks, and the real transcript — and because both runs execute and build traces from scratch, a byte match also says the LFM trace build is deterministic across runs, which is the precondition the oracle rests on.
…poch `real_epoch_with` hardcoded the 16-cycle fibonacci fixture. `EpochInputs` names the three things that make an epoch — the guest ELF, its private input, and the epoch size — and `real_epoch_from` builds from them. `EpochInputs::fixture()` is the old path exactly; `EpochInputs::from_env()` is that with LFM_CENSUS_ELF / LFM_CENSUS_INPUT / LFM_CENSUS_EPOCH_LOG2 applied, and it is what `real_epoch_with` uses, so with nothing set every existing caller keeps the path it had. Only epoch 0 is reachable — the boundary starts from genesis provenance — and that is now said in the doc rather than implied by a hardcoded label. `the_real_block_epoch_wraps` is Gate B: one epoch of a real mainnet block at blowup 4 / 110 queries, wrapped, verified, falsified. It requires the ELF and input by path and asserts they are set, because the failure mode of a missing override is proving the fixture and reporting it under a name that claims a block. Epoch size stays a knob: the largest that fits is a property of the box. The residency oracle changes shape, and the reason is a measured finding rather than a preference. Proving is not reproducible run to run: two runs of the same wrap build BYTE-IDENTICAL LFM traces and produce IDENTICAL roots at every stage, yet serialize to different proof bytes. The cause is `grinding::generate_nonce`, which under the `parallel` feature is `into_par_iter().find_any(..)` — any valid nonce, so which one comes back depends on thread scheduling, and the nonce is absorbed before the query indices are sampled. Both proofs verify; grinding is a proof of work and any witness satisfies it. This also corrects the fixture-blob note's attribution, which blames sub-proofs committing to different roots — not what happens on this path. The oracle therefore compares everything the nonce cannot reach (every root, the OOD evaluations, the final polynomial, the bus contribution), which is everything the recomputed LDE feeds, and proves Retain twice so the run carries its own control. The nonce difference is printed rather than asserted.
Measured on a 60 GiB box: the real-block wrap at the secure blowup4/110q preset is OOM-killed at 56.9 GiB after 2m30s, and it dies BEFORE proving starts — the spill volume is zero and the disk is untouched, so nothing the prover does about residency is reached. The wall is `build_traces_with_hasher`, which materializes every `KECCAK_RND` chunk trace into one Vec (trace.rs:162-167, the audit's S6 seam): 15 chunks at 2^16, 5.78 GiB of main trace each. That makes the query count the knob worth having. Chunk count is `(spine + per_query x queries) / 21,845` permutations, and per-query cost is dominated by leaf absorption — set by table WIDTH, so it barely moves with epoch size. Shrinking the epoch does not meaningfully shrink the chunk count; shrinking the query count does, linearly. The epoch-size knob alone cannot walk this workload down to something a 60 GiB box builds. `LFM_WRAP_QUERIES` therefore overrides the inner query count, defaulting to the preset's 110. Below 110 it is not a security parameter set, the banner says so on every run, and the count travels with every number — the same discipline `the_wrap_proves_at_blowup_8_geometry` already applies to its own reduction.
The campaign's plans, censuses, audits, and the ratification-ready commit spec lived only in an untracked thoughts/ directory on one laptop — one disk away from gone, while the whole team cites them. Committed following the EXPLORATION.md/BOX-RESULTS.md precedent: PLAN, CENSUS (with today's measured corrections), the S3/PA/MMCS/HASH-SPLIT/SOLUTION-ARRAY plans, both seam audits, D0-DESIGN, BLAKE3-COST-MODEL, and commit-spec with its reference implementation and KATs (85/85 board). Box endpoints excluded.
A leaf row carried four felts' halves in eight message lanes and nothing
else, so chaining a wide leaf needed a second compression — an `"LFMC"`
parent folding two leaf digests. That is 2 felts per compression, and
leaf absorption is ~70% of a recursion tower node's bill.
Put the chaining accumulator in the message instead. A leaf row now reads
TWO cells — the accumulator, then the felts — and one compression both
absorbs and chains: 4 felts per compression, no fold. `NUM_LANES` goes
8 to 12 and `block_len` 36 to 52, which is +16 columns and +8 bus
interactions on a 3,444-column chip against a 2.0x cut in the dominant
term (COMMIT.md 1.2, 1.4.1).
52 < 64, so a row is still ONE BLAKE3 block and the crate-KAT anchor
survives in all three domains. The tag stays the message's LAST word
rather than sitting at a fixed m[8], which is what keeps the byte string
`LE32(lanes) || tag` at any lane count.
The hazards COMMIT.md 1.4.4 registers, and what each needed:
H1 the framing constraint indices are derived from NUM_LANES, never
written as literals. The lane block grew by four and the unread-IN
pins shrank by four, so NUM_CONSTRAINTS does not move and a
hand-numbered block would have overwritten the output pins in
silence — the duplicate-emit assert is debug-only and the suite
runs in release.
H2 `emit_unread_input_pins` skips a slot every mode reads instead of
asserting one exists; NUM_UNREAD_INPUT_PINS is derived, 8 -> 4.
H3 the second `LfmMem` receive gains MODE_L. It excluded it because a
leaf read one cell; leaving it would mean the felts were never read
from memory at all. Arity unchanged, multiplicity changed.
H4 the felts move to the second cell: `leaf_lo_lane`/`leaf_hi_lane`
and the halves binding read above the accumulator.
H5 a row is now a HYBRID — cell 0 as digest lanes, cell 1 as halves —
and `lanes_from_cells` is the single place that splits it, so the
witness filler and the BITWISE histogram cannot disagree.
H6 the lane identity gate is per lane RANGE: lanes 0-3 on the full mu
(they are a digest cell under every mode, and this is the only
thing that range-checks the accumulator), lanes 4-11 on digest_mu.
Gating 0-3 on digest_mu would leave a leaf row's accumulator
unconstrained and unbind the chain.
H7 `admits` inspects both cells in the cells the AIR reads them from,
so a non-canonical felt is REJECTED rather than panicking later in
the filler.
H8 `LfmHasher::leaf` takes (acc, felts) on every arm; the Test and
Poseidon defaults become `compress_out(acc, felts)`.
`leaf_hash_pair` is the win at the program level: one two-row chain
instead of two leaf rows and a parent. FriToyV0 drops from 93 hash rows
to 81 with its leaf-row count unchanged at 26 — the folds are what left.
Only FriToyV0 moves. It is the one registered program with leaf rows, and its instruction stream changed by design — twelve fewer hash rows, one more interned constant for the chain start — so every chip carrying its instructions re-commits its preprocessed trace. The five programs without leaf rows are byte-identical, roots AND program_id, TrivialV0 included; so is every fixed table (LFM_RANGE, KECCAK_RND, KECCAK_RC, BITWISE) and every log_height. That is the anti-launder control: a re-bless this wide would be laundering a regression, and a re-bless this narrow is the change it claims to be.
`block_len` is v[14], hence the vd operand of round-0 G #2 and from there an XOR operand, so it cannot be mode-dependent: moving it 36 -> 52 for the leaf moves the Merkle and transcript domains with it. Every pinned digest re-blesses (COMMIT.md 1.4.4 H9) — 30 socket vectors, 12 transcript steps, both FriToyV0 end-to-end vectors and the leaf table. The vectors come from `blake3_oracle.py` — the from-scratch Python BLAKE3 the originals came from — via a new `rate4_kat_gen.py`, not from the Rust under test. The socket and transcript tables are rewritten digest-line by digest-line out of their own input fields, so their diff is exactly the digests and a reviewer can check that nothing structural moved. The leaf table is re-rendered whole because the row genuinely gained an input. `acc_ignored_control` is new and is the discrimination the table was missing: same felts as `zeros`, different accumulator. A row that absorbed its felts and dropped the chaining value would satisfy every canonicity and halves constraint and still be a good hash of the felts — it just would not be a chain. What the socket budget now prices, from the layout rather than from a literal: +16 main columns, +8 bus interactions, +28 census cells at 7 rounds (5,517 -> 5,545), and a constraint count that does not move at all. FriToyV0 goes 93 hash rows -> 81 and 513,081 cells -> 449,145. Read -12.9% as this program's number, not the tower's: FriToyV0 is Merkle-walk-heavy at a toy width, and what the RATE halves is leaf absorption. D1's unread-pin control moves up to the third cell. The break it regression-tests was on the SECOND, back when a leaf read one cell; the RATE closed that structurally by making the second cell a cell the mode reads. Kept rather than deleted because what it guards is the derivation.
…them `blake3_probe`'s comparison carried "4,741 at 6 rounds and 5,509 at 7" as prose. Those predated the leaf mode's canonicity block, nothing recomputed them, and they were wrong by 8 from the day that block landed — then wrong by 36 once the leaf RATE widened the socket. The claim they support (hosting is cheaper than the standalone chip at both round counts) was true throughout, which is exactly why nobody noticed. It now calls `blake3_socket_tests::predicted_cells` and asserts the inequality, so the comparison cannot outlive its numbers. The saving reads -3.4% at 6r and -3.0% at 7r. phase2-report.md gets a correction box rather than an edit: it is a dated snapshot and its figures are what was measured on 2026-08-10. The box tracks both moves since — the canonicity block and the RATE — and points at the derivation rather than restating literals, since copying them is what let the first correction sit unnoticed.
Where the branch stands, the H-register disposition item by item, and the two things a reviewer must look at: the message layout follows COMMIT.md 1.2 rather than the task brief's m[8] assumption, and the registry drift is one entry rather than six.
COMMIT.md 1.4.2 asks for a control on the lane-identity gate in the WA1/WA2 style, because one direction of getting it wrong is a soundness break rather than a broken build: gate lanes 0-3 on digest_mu and a leaf row's accumulator carries no identity at all, so the prover chooses the chain's message words freely and the leaf chain unbinds. Nothing in the suite would have noticed — every existing leaf test passes either way, since they only exercise rows whose accumulator is honest. Two tests, one per direction, because a gate that is wrong EITHER way passes the other: h6_a_leaf_rows_accumulator_lanes_carry_the_identity moves the accumulator FELT and leaves its bytes honest — a prover claiming one accumulator in IN while the mixing core consumes another — and asserts the violated set is EXACTLY that lane's own identity. WA9 shape: with the identity the row is rejected, without it every other constraint still evaluates to zero, so it would be accepted. h6_the_felt_lanes_do_not_satisfy_the_lane_identity asserts the other direction is real, and refuses to be vacuous: if every felt equalled its low half the claim would be empty, so the test says so instead of passing. `LANE_IDX` becomes pub for the same reason `UNREAD_IDX` and `LEAF_IDX` are: a control that located the constraint by a literal would silently point somewhere else the next time the framing grows. Also: the tag has not been `m[8]` since the socket widened — it is the word straight after the lanes, `m[NUM_LANES]`. Eight doc comments still said otherwise, and one described the message as 36 bytes. They are claims about the framing, so they are wrong rather than merely stale.
…veats The Gate D1 node fits at 78 GiB, and the two ways that number can be over-read are written next to it: the realized factor is 1.60-1.65x rather than 2.0x (the 2.0x is on leaf absorption, ~75% of the node), and 78 GiB is a one-proof-verify node rather than the arity-2 aggregating one the campaign already identified as the binding constraint.
…c the byte hash
The compression function had three callers that could not share a copy: the
Merkle backends (in `crypto`), the `LFM_BLAKE3` chip and `LFM_HASH` socket (in
`prover`), and the CUDA kernels' parity reference (in `math-cuda`). `crypto` is
the only crate all three reach, so `blake3_compress_rounds` and its canonical
vectors move there and `prover::lfm::blake3` becomes a re-export. The chips and
the commitment backends now hash identically because they call one function,
which is a different claim from agreeing today.
The round count moves with it. `lambda-vm-prover/blake3-6round` forwards to
`crypto/blake3-6round` rather than declaring a second knob, so BLAKE3_ROUNDS —
and SOCKET_ROUNDS, which aliases it — is one symbol for the whole host tree.
Polarity is unchanged: off = 7 rounds, the externally anchored default.
Adds `Blake3Chain`, the byte hash the commitments will be built from: standard
BLAKE3 restricted to a single chunk that never ends. PA-PLAN §1.7 is the
normative spec, written first and marked DRAFT pending ratification. Two
properties are why it has this shape rather than a bare chain with one flag
constant:
* up to 1024 bytes at 7 rounds it IS `blake3::hash`, so the official crate is
a direct known-answer test for the framing — the block splitting, the
padding, the final `block_len`, the flag schedule — and not merely for the
round function;
* a 64-byte message degenerates to exactly the Merkle parent form the device
kernel implements, which is what will make the StarkHash two-element
invariant hold by construction.
Past one chunk it deliberately leaves the standard, and a test pins that it
does, so the claim is falsifiable rather than decorative.
The prover's falsification suite stays where it is, testing the primitive
through the path the chips use, so the re-export itself is covered.
crypto 51 -> 61 tests, green at both round counts. prover lfm:: at its 310/19
baseline, unchanged.
The second commitment configuration, over the BLAKE3 backends. Its two families are the same generic backends the keccak instance uses with the digest swapped, so the two-element invariant `StarkHash` documents holds because they are one function over one 64-byte message, not because two encodings were shown to coincide. Tested anyway, plus a control that the two configurations really are different hashes — without which every BLAKE3 test here would pass just as well if the aliases had been left pointing at keccak. Nothing selects it. The aliases, and therefore COMMITMENT_HASH, stay keccak. A full prove->verify under it does not work yet and the reason is specific: `fri/` still builds layer trees with the concrete keccak alias while the verifier authenticates them through `H::Batched`, so an honest proof would reject at its first FRI query. Threading the configuration through `fri/` is Stage 2 and is not done here; what is covered is the commitment layer, through the production `commit_bit_reversed_with` path, commit -> open -> verify with a negative control, same-reference only. Under `cuda` the configuration does not exist at all. `StarkHash::Batched` requires `KeccakTreeBackend` there because the GPU tree entries hash with the keccak kernels and only label the result — implementing that marker for a BLAKE3 backend to get past it is exactly the deliberate false statement the marker exists to require. Adding the enum variant trips the exhaustive match in `lfm::registry` by design. Resolved by deciding rather than defaulting: the guard stays pointed at the aliases and the Blake3 arm is a hard stop, because if the aliases move, `program_id` names a hasher but nothing about the commitment hash, so two builds committing under different hashes would give one program one id. `COMMITMENT_HASH`'s doc now states that it describes the DEFAULT configuration only — the half-truth PA-PLAN §4.2 flagged, written down rather than left implicit. stark 245 -> 248 tests.
…and lint the round counts in lockstep Track G left a TODO for this: `tests/blake3_reference` carried a transcription of the host compression function because `prover`, its old home, depends on this crate and could never be imported here. Now that it lives in `crypto` — a dev-dependency — the copy is gone and the module re-exports the real one. The device kernels, the host commitment backends and the in-circuit chip are checked against one function rather than three transcriptions. What stays local is the parent framing, which is a property of the kernel rather than of the primitive. It gains a second anchor: as well as being `blake3::hash(a || b)` at 7 rounds, it must equal what the production host backend's `hash_new_parent` computes at the build's round count — so a GPU tree and a CPU tree over the same leaves are the same tree. That test doubles as the lockstep alarm, since it compares crypto's BLAKE3_ROUNDS with the cubin's. `make lint` gains one pass with BOTH crates' blake3-6round features set. One rather than two on purpose: setting either alone means the GPU committing under a different hash than the CPU, so linting them apart would certify a combination nothing should build. This also closes the blind spot recorded in lfm-real-hash/phase2-report.md — the 6-round arm was not linted at all. All five lint passes green.
…pinned PA-PLAN §1.6 said no external artifact exists at 6 rounds. Too pessimistic, and this was the campaign's weakest provenance link, so it is worth correcting. #903's Python oracle is a full standard-BLAKE3 implementation with the round count as a parameter. At 7 rounds it reproduces the official blake3 package bit-for-bit at every length checked, multi-chunk ones included — so it is standard BLAKE3 pinned from outside at the TREE level, not only at the compression level. And standard BLAKE3 over at most one chunk is this construction, by an argument that never mentions the round function. So its 6-round evaluation is an independent computation of Blake3Chain for every message up to 1024 bytes. Run over all twelve KAT messages: the eleven at <=1024 bytes agree, and 1088 differs. The second half is worth as much as the first. The 7-round control only says "not standard at 7 rounds"; this says the divergence is the CHUNKING, since a reference that is standard at 6 rounds too still parts from us at exactly the chunk boundary. The oracle survives only as __pycache__ bytecode in an untracked directory — the .py source and the canonical vectors JSON are gone. The digests are recorded in the spec so the result outlives the artifact, and a copy of the bytecode is in the bench artifact cache under blake3_oracle_2026-08-14/.
P2 conflated two claims. The parent form is a 64-byte message; the two-element LEAF invariant is about 16 bytes, and it holds for a different reason — Pair and Batched are the same generic backend over the same digest. Both still hold by construction, but they are not the same statement and the spec should not suggest a 64-byte leaf.
…e parent claim is separate Same conflation the spec had. Pair and Batched agree on a two-element leaf because they are one backend over one digest serializing the same 16 bytes; that a 64-byte message is a single compression in the device parent framing is a different statement, about the parent layer.
Ports #768's two standalone primitives — `fri/mmcs.rs` (mixed-height row-pair MMCS) and `fri/batched.rs` (height-bucketed FRI) — onto the current branch. Primitives only: nothing in prover.rs/verifier.rs is wired to them yet, and the wire types are untouched. Three things are corrected rather than inherited. The hash path. Both files hard-coded `BatchedMerkleTreeBackend`. They are now generic over `H: StarkHash` and go through `H::Batched<E>`'s `hash_data` / `hash_new_parent` — the same two functions the per-table row-pair tree already commits with. A single-matrix MMCS is therefore byte-identical to that tree by construction, so there is no second leaf encoding to keep in step, and no third `StarkHash` member is needed: `MixedMmcs` builds its own layers and only ever needs a leaf hash and a 2-input compression. The terminal-polynomial early stop. `batched_commit_phase` folded to a scalar and appended it, ignoring `fri_final_poly_log_degree` — nine extra committed layers at a real epoch. It now derives its fold count through the shared `FriFoldLayout` and sends the terminal polynomial's coefficients, exactly as `commit_phase_from_evaluations` does. One batched-only floor comes with it: the terminal may not sit above the SHORTEST bucket, or that codeword would never be folded into the running word, so the stop is `min(blowup_log + k, h_min)` and the bucket AT the terminal height is injected by the final fold. The index convention. `verify_batch` consumes the LOW bits of `iota`, which is correct only when this MMCS's `h_max` equals the FRI's. The module header now states the reduction the caller owes as a hard precondition, and `verify_batch` rejects an `iota` outside this tree's leaf range — turning most of a silent mis-binding into a rejection. Every malformed-shape path returns false instead of panicking, so a verifier can call it on adversarial data. Also: `absorb_height_histogram` becomes `absorb_shape_histogram` and binds (height, width) pairs, and `HeightCombiner` absorbs codewords one at a time so a prover need not hold every table's quotient at once. `combine_by_height` remains as the materialized convenience wrapper.
#768's `batched_soundness_tests.rs` tampers a `BatchedMultiProof` and calls `Verifier::batched_multi_verify`; neither exists here, so it cannot come along with a primitives-only port. This is the part of that suite the primitives can actually decide, plus the forgeries the shared path opens up that #768's file did not cover. Reaching down from it: a tampered row in EVERY height group (not only the tall one — short matrices are bound through injection, and a tall-only control would miss a wrong injection level entirely), a tampered or mis-sized authentication path, and widths that disagree with the opening. New here: an opening replayed at any other index is rejected — asserted over the whole leaf range, not one sample; two same-shape matrices' openings swapped within a height group is rejected, so input order is part of the commitment; a relabelled injection height is rejected; and tampering the FRI transcript (a layer root, a terminal coefficient, a height, a width) moves the query indices. Deferred with the integration: per-query FRI layer evaluations, OOD values, the bus balance, the query count, the grinding nonce.
Where the branch stands, the M-12/M-13a/M-14 dispositions, and the two things whoever wires this up must read before starting: #768's soundness tests are integration-bound and could not come along, and the ported leaf layout streams per height GROUP rather than per matrix, so §3.3's chained-absorb pseudocode does not describe what the primitive provides. Named RESUME-MMCS.md, not RESUME.md: the worktree root already carries the RATE-4 lane's RESUME.md from the base branch, and this branch is slated to merge into blake3-real-hash.
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.
BLAKE3 as the LFM machine's real hash — F3.4 retired
Draft, for testing and exploration. Replaces the LFM role-2
LFM_HASHTestPermutationplaceholder with real BLAKE3 across every hash domain, so both registered
LFM_HASHprograms (
TrivialV0,FriToyV0) prove and verify under the production hash.The campaign is the top of the branch — these commits, in order:
b693eeceLFM_HASHhasher — the Option-A compress socket, 7-round default (crate is a direct KAT)9bcc9ee2TrivialV0proves under BLAKE3)1c2e98d3LFMLfelt-input leaf mode —FriToyV0proves under BLAKE3, F3.4 retirede16110ddthoughts/shared/lfm-real-hash/Every domain — Merkle parents (
LFMC), FRI leaves (LFML), the FS transcript (LFMT) —is real BLAKE3: tagged, prover-unchosen (preprocessed mode selectors + registrar one-hot),
and z3-gated. Chip gate: PASS 86/86, pinned to
1c2e98d3;lfm::suite 306 pass / 19fail (the pre-existing
fibonacci.elffixture set). Every phase was adversarially reviewed;the review records and gate boards are in
thoughts/shared/lfm-real-hash/.Status / how to read this PR
feat/lfm→pr915→ this work), noneof which is in
mainyet, so the diff againstmainincludes the whole stack. The BLAKE3campaign proper is the four commits above; everything below
65025095is the underlyingmachine.
main. Bringing it current surfaced a real blocker (below); it isa decision, not a mechanical rebase, so it is deliberately left for a follow-up.
Before this can merge (recorded, not done here)
and tighten
TRANSCRIPT.md§3.3 to name which mechanism carries the preprocessed-ness argumentunder the post-fix(verifier): pin each trace-opening column width to the AIR, not just their sum #909 verifier. On this ancestry the "tag is prover-unchosen" argument rests on
the precomputed leaf-hash binding alone.
main's device-IR redesign.mainreworked the constraint-IR device form(operands moved from raw node indices to OPK-tagged slots;
DeviceNode.dimremoved in favour ofres & RES_EXT_BIT;DeviceProgramgained slot-class sizes). This is incompatible with thisbranch's build-time constraint-artifact feature (
crypto/stark/src/constraint_ir/artifact.rs),whose
validate_self/program()/ census assume the old node-index operand model. A trialmerge compiles after mechanical fixes but fails the artifact round-trip suite — the feature needs
reimplementing against the new IR, which is soundness-critical and warrants its own pass.