BLAKE3 as the LFM machine's real hash — F3.4 retired (draft) - #930
Draft
MauroToscano wants to merge 151 commits into
Draft
BLAKE3 as the LFM machine's real hash — F3.4 retired (draft)#930MauroToscano wants to merge 151 commits into
MauroToscano wants to merge 151 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.
… tag Ratified today: leaf/parent domain separation is the reserved "LFML" tag (RFC 6962's split in the tag scheme), not a fixed-depth-only policy and not BLAKE3's PARENT flag, which would break the direct blake3::hash KAT. Doc-only; nothing implements leaf hashing yet, the obligation binds review of any future leaf-hashing or variable-depth-tree change.
The previous note claimed no leaf-hashing path exists. Wrong: FriToyV0 already forms leaf digests by compressing raw data rows under the same LFMC tag (programs.rs, leaf = compress(row_even, row_odd) feeding merkle_walk), so leaves and parents are not domain-separated today. The actual safety argument is that every current tree is a fixed-depth static circuit — the eDSL builder fixes program shape at build time, hints supply values, never structure. The LFML obligation is unchanged; only its stated justification is corrected.
… permute socket) The FS sponge is now a compress chain over one cell for all hashers: absorb = 1 compress, absorb2 = 2, squeeze = out-then-advance with an SQ(i) counter operand (a free program constant that breaks the fixed-map iteration structure). SpongeVar and its host mirror HostSponge are rewritten in lockstep; programs keep their call-site signatures. The permute socket is never built: the AIR keeps MODE_P pinned to 0 under BLAKE3 and TrivialV0's raw permute became a third compress, so it now proves and verifies under BLAKE3. Permute coverage moved to a test-only fixture with no registry identity. Transcript rows hash under a new domain: m[8] = MODE_C*TAG_LFMC + MODE_T*TAG_LFMT, a linear form over preprocessed mode columns (MODE_T is new; PREP_WIDTH 11 -> 12, selectors kept contiguous for the admission one-hot span, multiplicity columns shifted by name not position). At 7 rounds every transcript step remains a direct crate KAT: blake3::hash(state || operand || "LFMT")[0..16]. Constraint-level mode blending (fractional selectors forging any tag) is demonstrated by the M5/M6/M8 controls and excluded by the preprocessed binding plus the registrar's one-hot check - both asserted by test, and the z3 board reproduces the forgery and its exclusion independently (chip gate re-run: PASS 79/79, re-pinned). The epoch verifier's hash-cost model is corrected with the sponge it described: LFM_HASH_RATE_FELTS is now derived (= HASH_DIGEST_FELTS = 4) instead of a literal 8 from the deleted duplex; the absorption ceiling vs keccak restates as 17/4 = 4.25x, a 6-felt FRI-layer leaf is rate-sensitive (2 blocks at rate 4), and an ELF-free test pins the model to its derivation so the constant cannot outlive its source again. Registry re-blessed once (all six program_ids move with the preprocessed root). FriToyV0 still does not prove under BLAKE3: its leaves hash arbitrary Goldilocks felts and the socket rejects non-u32 lanes (O1) - a tripwire test pins that the refusal is O1 and nothing else. Adversarially reviewed (no soundness defect; review record in thoughts/shared/lfm-real-hash/b1-verify.md, fixes in transcript-impl-report.md section 9). Before any merge to main this branch must rebase past #909's opening-width pin and re-run the M-controls.
…F3.4 retired
A fourth preprocessed selector MODE_L gives the socket a felt-input
leaf mode under the "LFML" tag. A leaf row reads one cell as four
Goldilocks felts, splits each into a checked lo/hi u32 pair, and hashes
the eight halves through the same socket every other mode uses. The
u32 bound comes free from the existing lane AreBytes (which carry all
three modes); only canonicity was missing, and over two halves that is
the LFM_BITDEC Z/GINV idiom exactly — v < p iff NOT(hi = 2^32-1 AND
lo >= 1), since p-1 = 0xFFFFFFFF_00000000. Two witness columns and four
constraints per felt, zero new sends, max degree still 3.
This is what lets FriToyV0 — a real verification program over real FRI
data, 124 of 128 committed values >= 2^32 — prove and verify under the
machine's BLAKE3 and be accepted by the production verifier. With
TrivialV0 already there, both registered programs run on the real hash:
the F3.4 placeholder disclosure is retired. Field data entering the
transcript takes the same route (absorb_felts = leaf then absorb), one
uniform rule: absorb for digests, absorb_felts for data.
Leaves and parents are now domain-separated by construction under
BLAKE3 ("LFML" vs "LFMC"), so O5's fixed-depth crutch is gone for that
hasher; the ISA docs record that single-domain hashers do not separate
them. PREP_WIDTH 12 -> 13, selectors kept contiguous for the one-hot
span, registry re-blessed once.
Adversarial review found one HIGH soundness defect and it is fixed
here: MODE_L's unread input cells were pinned in the BLAKE3 arm but not
in eval_test/eval_poseidon, leaving four free felts on a leaf row under
those hashers — an executed Fiat-Shamir break under Poseidon. The fix
is one emit_unread_input_pins derived from HashMode::num_input_cells(),
called by all three arms, pinning every unread cell; a WA9-shaped test
proves the pins load-bearing (the consistent forgery's violated set is
exactly those pins — accepted without them, rejected with them) under
every hasher, with the honest leaf row still proving. The lesson is on
the record: hygiene in one arm was soundness in another.
Chip gate re-run PASS 86/86, re-pinned to this content; full lfm:: 306
pass / 19 fail (the pre-existing fibonacci.elf fixture set, unchanged);
lint clean. Review record: thoughts/shared/lfm-real-hash/leaf-verify.md;
fixes in leaf-impl-report.md section 10. Before any merge this branch
must rebase past #909's opening-width pin and re-run the M-controls.
The oracle, all four chip-gate boards, the specs, the options papers, the cost scripts, and the artifact pin that ties the PASS 86/86 verdict to 1c2e98d — 45 files, docs + python, no build impact. These were living untracked in a working tree; commit them alongside the code they certify (the same convention thoughts/blake3/ already follows on the accelerator branch), so artifact_pin.py --check and every gate board is reproducible by anyone, not just on the machine that ran them. Contents: gate-oracle/ (ORACLE.md, CHIP-GATE.md, chip_model.py, gate.py, contracts.py, blake3_oracle.py, socket_ref.py, socket_kats, artifact_pin .py + .json, the captured run logs), transcript-spec/, leaf-spec/, the phase/verify reports, A6R-signoff.md, the permute-socket and leaf-convention options papers, PLAN.md, ORCHESTRATION.md.
…502,047 The correction was already in the body; the top-of-doc board summary still carried the stale 91 / 502,047 with a ✓ EXECUTED marker (the builder flagged it on handoff). Now consistent with the cost table and leaf-impl-report.md §6.
…ccak HWSL fork sync Brings the LFM machine + BLAKE3 campaign up to date with origin/main (528a841). - Artifact feature reconciled to main's redesigned constraint-IR (approach A): main's DeviceProgram/lower() stays authoritative; the build-time ConstraintArtifact now owns a node-index POD ArtifactNode and re-derives the device blob via main's lower() (its lossy slot-form cannot be inverted). Round-trip 11/11. - keccak_adapter::bitwise_ops_for dropped the 120 theta/rho HWSL sends per round to match main's KECCAK_RND (main replaced the HWSL lookups with inline mu-gated linear identities); the forked receiver-side multiplicity collector agrees with main's collect_bitwise_from_keccak again. Per-round count 1148 -> 1028. This restores the cross-table LogUp bus balance for every keccak-touching program — the reason 20 machine/fri/join tests failed post-merge. Root-cause + adversarial review in thoughts/shared/lfm-real-hash/merge-plan/. - 5 merge conflicts resolved: lookup.rs (main's Arc-wrapped constraint_program + the branch's precaptured_program), continuation.rs, 3 IR test files (generic production_airs iteration); HINT coverage added (production_airs + NUM_PRODUCTION_AIRS 29). - Test expectations updated to main's semantics: preprocessed_tags asserts verify-time rejection (main's precomputed-tree cache moves the tag-rewrite check prove->verify; soundness intact, confirmed by probe); HINT design count 418 + KECCAK_RND 14016 -> 12998; epoch budget 63393 -> 62375 attributed entirely to KECCAK_RND's HWSL->inline swap; private-page preprocessing follows main's OFFSET soundness fix. Validation: lfm:: 306 pass / 19 fail (only the pre-existing fibonacci.elf fixtures, identical to baseline); stark opening_width/aux_opening_width 15/15; artifact round-trip 11/11; make fmt + make lint clean.
…loration The 4-agent debate that caught the merge's soundness trap (FIX-PLAN, the two defenses, the attack, the judge verdict) and the GPU-recursion exploration (row-only LDE gate excludes KECCAK_RND). Untracked working-tree docs, committed so a git clean cannot lose them.
…e 0) Resets the process-global GPU call counters after the inner epoch is built (the inner RV64 continuation prove has its own GPU traffic) and prints all 15 counters around lfm_prove alone, so the machine's device coverage is measured rather than inferred. First run on a 5090 confirmed the map's predictions: composition 2, merkle 13, device_only 0 at the default threshold — and LAMBDA_VM_GPU_LDE_THRESHOLD=262144 flips device_only to 1 (KECCAK_RND fully device-resident) at -57% prove time with no code change.
…ION Stages 0/1) Stage 0 on a 5090: every falsifiable prediction held (composition 2, merkle 13, device_only 0 at the default threshold). Stage 1: LAMBDA_VM_GPU_LDE_THRESHOLD=262144 flips device_only to 1 and takes the min-preset wrap from 16.7s to 7.2s, ABBA-tight, verify green, 12.7 GiB peak VRAM; the knee is exactly 2^18 and KECCAK_RND is the entire win. Composition A/B falsifies the 'small like the VM' prediction (disabling it costs 2x on LFM). Stage 3 is rescoped: gpu_lde_threshold() has 18 consumers and handle-bearing sites re-derive admission, so the permanent cell-aware gate is an admission-token redesign, not a 4-site patch. Also identifies the fibonacci.elf fixture drift behind the 19 known failures (fresh builds finish inside one 16-cycle epoch).
… step 0) Three places would stamp a non-keccak label on keccak-derived data the moment a second commitment backend exists. All three type-check today and none fails loudly, so they are hardened before that backend lands, not after. `KeccakTreeBackend` — a marker implemented only by the three keccak backend aliases — replaces `IsMerkleTreeBackend<Node = [u8; 32]>` on the seven `gpu_lde` tree entries. Those entries never call `B`: leaf and parent hashing happens in the math-cuda keccak kernels and `B` only types the host `MerkleTree` the root is wrapped in. The old bound admitted any 32-byte-node backend, so a blake3 one would have compiled there and handed back keccak trees wearing its name. Now that is a compile error. Runtime behavior is unchanged; every call site already passes `BatchedMerkleTreeBackend`. `CommitmentHash` and `COMMITMENT_HASH` in `stark::config` name the hash the crate's Merkle layer actually uses, tied to the aliases by a static assertion so repointing one fails in the file that makes the claim. `build_artifacts_with_hasher` matches on it exhaustively: a second commitment hash cannot land without someone deciding what LFM artifacts should say. Today they name a `HasherKind` — the LFM_HASH chip, not the commitment — over roots keccak built, which the corrected `build_artifacts` doc now states instead of asserting that no commitment moves with the hasher. `ALL_HASHERS` gains `Blake3`, so digest-distinctness and cross-hasher rejection now cover the third candidate. Both tests pass unchanged.
…tep 2) The Merkle backend stops being hardwired in `config.rs`'s aliases. `StarkHash` carries the backend families the prover and verifier build trees with — `Batched` (row-group leaves) and `Pair` (FRI layers) — plus the `CommitmentHash` they all are. `KeccakStarkHash` is the only implementation, and `Prover`/`Verifier` are now aliases of `GenericProver`/`GenericVerifier` at that instance, so every existing call site resolves unchanged; the whole workspace compiles with the aliases untouched. The members are generic over the field (GATs) because one proof commits over both the base field and the extension. `Node` is deliberately not an associated type — it is `Commitment` for every implementation, which is what keeps `StarkProof`'s fields and their rkyv derives byte-identical. No wire format moves. `IsStreamingLeafBackend` lifts the two leaf routes the prover and verifier actually use (`hash_bytes`, `hash_data_from_slices`) off the concrete backend's inherent impl and onto a trait, so a configuration can reach them by name. `commit_bit_reversed` keeps its keccak-pinned signature — its six production callers are untouched — with `commit_bit_reversed_with` as the generic sibling the prover uses; `keccak_leaves_*` likewise stay keccak wrappers over a generic core rather than becoming generic under a name that says keccak. Two things the parameterization surfaced, both pre-existing and both now stated rather than assumed: - The prover builds FRI-layer trees with the pair backend while the verifier authenticates those openings with the batched one. Under keccak they coincide and the split was invisible. It is now a documented `StarkHash` invariant with a test, so a configuration that breaks it fails there instead of rejecting every honest proof at its first FRI query. - The GPU tree entries hash with keccak kernels and only label the result, so under `cuda` a configuration's batched backend must be `KeccakTreeBackend`. The bound says it at compile time; it comes off when the kernels do. Oracles: full suite 859 passed / 34 failed, identical to the measured baseline at eefd308 (the 34 are missing rust-guest and recursion ELF fixtures); stark 236/0; crypto 51/0. King gate — an LFM TrivialV0 proof and three RV64 asm-ELF proofs generated at eefd308 verify under this build, and proofs built here verify under the eefd308 CLI, both directions. make lint green on all four feature combinations including cuda.
A prove/verify round trip inside one build cannot see a self-consistent drift — a version that changes how it commits still accepts its own proofs. This exchanges proof bytes across versions instead: generate at the ref before a change, verify at the ref after. It is the LFM-side counterpart of scripts/cross_verify_vm.sh, which already does this for RV64 ELF proofs. Ignored by default: it is an oracle, not a regression test, needing two builds, an out-of-tree byte store and an operator choosing the two refs. Usage is in the module doc. It gated step 2 (an eefd308 TrivialV0 archive verified under the StarkHash parameterization) and is the gate for steps 3-7, where the Blake3 backends, the B1 transcript, the lfm_prove wiring and the registry rows each have to keep Test-hasher proofs verifying.
…replay (D0 step 5) `absorb_lfm_statement` and `replay_transcript_phase_a_view` named `DefaultTranscript<E>` while using only `IsTranscript<E>` methods — `append_bytes` in the first, plus `sample_field_element` in the second. Both are hash-agnostic: the same call sequence under any sponge. Pinning them to the concrete transcript would have forced the machine's own transcript to fork these functions rather than call them, and two copies of a statement encoding is precisely the drift `absorb_lfm_statement`'s "exhaustive by construction" contract exists to prevent. Callers are unchanged — `DefaultTranscript` still satisfies the bound. Workspace compiles clean; lfm:: suite at the 306/19 baseline.
Emission built every group twice: once as `Vec<Vec<FE>>`, once as the flat matrix `ColumnGroup` holds, with both alive until the struct literal consumed them. The per-row Vecs are grown by extend/push rather than sized, so a 10-wide BALU row lands at capacity 18 — and there is one heap allocation per instruction. `ColumnGroupBuilder` appends straight into the final buffer: no second materialization, no headers, no rounding waste, no ~271M malloc/free pairs. Rows are written by named layout column instead of by position, which is also how the emitter now reads. `read_counts` becomes a dense `Vec<u64>` indexed by address. `alloc` hands out addresses sequentially from zero, so the key space is exactly `0..num_addrs` with no holes and the map was paying ~16 bytes plus control per entry for a permutation of the identity. Its emptiness check becomes an all-zero check, which means the same thing: every read had a writer. Both it and `written` are then dropped before `emit_column_groups`, so the emitter's peak no longer carries them. Bit-identical by construction and by test: the same values land at the same row-major offsets with the same zero padding, and all six registry drift tests still recompute their pinned roots and program_ids. Nothing about the AIR set, bus topology or soundness moves. lfm:: suite at the 306/19 baseline.
… builds
`EmitTracker`'s "constraint {idx} emitted twice" assert is
`#[cfg(debug_assertions)]`, and this workspace declares no `[profile.release]`
override — so under the house convention of `cargo test --release` it is a
no-op and a second `emit_base(idx, ..)` silently overwrites the first.
Nothing else notices. A body that emits one index twice and another never still
fills the declared number of slots, so the constraint count, any hand-written
predicted-count test, and `assert_complete` all pass while a constraint has been
deleted. That is the shape COMMIT.md §1.4.4 H1 describes for the `NUM_LANES`
widening: the lane identities would run 6..17 over the unused-output pins at
14..17, losing lanes 8-11 — the four that pin `m[9..13]` to zero on digest rows.
`check_dense_index_set` runs the real body through `ConstraintSet::meta` (which
is not cfg-gated) and demands the emitted index multiset be exactly
`0..num_constraints`, naming the repeated and the missing indices. It returns
rather than panics, so a caller on a proving or verifying path can decide;
the tests assert.
`every_hash_candidate_emits_each_constraint_index_exactly_once` applies it to
all three `LFM_HASH` candidates, guarding the chip as it stands.
The guard is shown to fail before it is trusted, twice over: on a synthetic
lane body in `constraint_index_tests`, and — checked by hand, not committed —
on the real socket with the count-preserving H1 shape injected (lanes 8->12,
pins 8->4), where it reports `emitted twice [14, 15, 16, 17], never emitted
[18, 19, 20, 21]`.
Required by COMMIT.md §6. stark 241/0, lfm:: 307 passed / 19 pre-existing
fixture failures.
`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.
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.