BLAKE3 as the LFM machine's real hash — F3.4 retired (draft) - #930
Draft
MauroToscano wants to merge 213 commits into
Draft
BLAKE3 as the LFM machine's real hash — F3.4 retired (draft)#930MauroToscano wants to merge 213 commits into
MauroToscano wants to merge 213 commits into
Conversation
…anscripts The 2026-07-23 BLAKE3 work — an independent reference implementation, a three-anchor oracle harness, a chip design and a z3 soundness gate — was written to a session scratchpad under /private/tmp, never committed, and the scratchpad was gone by the time anyone went looking. Nothing named blake exists anywhere in this repo's history. Recovered by replaying the Write and Edit tool calls out of the subagent transcripts (5 Writes + 11 Edits, every Edit applied cleanly). Committing it so this cannot happen a third time: the keccak spike's artifacts went the same way, and the EC campaign's audits spent two days in the same state before being pushed. Evidence the recovery is faithful rather than plausible-looking: the gate runs and its structural negative controls all fire, 5/5 — rot_wrong_amount / swap_g_operand / wrong_iv / drop_ff_xor / wrong_msg_index each SAT as designed. Two fixtures are absent because they were downloaded or generated rather than written by a tool call, so the transcript never held them: the upstream official_test_vectors.json, and canonical_6round_vectors.json (regenerated by running test_oracle.py). The gate's positive controls and oracle anchors 1-2 therefore have NOT been re-run. Anchor 3 needs nothing external — Plonky3 is vendored at others/Plonky3/blake3-air. README.md says exactly how to restore full validation. Status is unchanged from when it stopped: design gate-proved, no Rust written, blocked on a protocol decision — sign-off on a named "6-round collision resistance" assumption. The gate proves the chip matches the reference, not that 6 rounds are secure. One correction this recovery makes possible: the EC lincomb2 design study justified its NUMS assumption with "like blake3's 6-round assumption". No such assumption was ever recorded in the spec, because this work never shipped — it was cited as precedent for something that had not happened.
…h run green
The recovery left two fixtures absent because they had been downloaded or
generated rather than written by a tool call, so no transcript held them. Both
are now restored, and every claim in DESIGN.md §9 reproduces end to end:
oracle [1] official vector set PASS 35/35 x 3 modes
[2] blake3 PyPI package SKIP (not installed)
[3] Plonky3 blake3-air PASS 20,000 compressions
gate G-function UNSAT, init+feed-forward UNSAT, 5/5 negative controls SAT,
4/4 positive controls SAT (6-round seeds 0-2 and 7-round),
width audit both bounds necessary. OVERALL: PASS
The positive controls were the gap that mattered: they are the only check that
would catch a per-instance wiring bug across the 48 unrolled G-functions, and
they were unrunnable until now.
PROVENANCE, because the label matters: official_test_vectors.json was
REGENERATED from the official blake3 Rust crate v1.8.5 (generator kept in
ground-truth/), not downloaded from upstream. It carries the official
parameters — the Elvish key, the 2019-12-27 context string, the same 35 input
lengths — and case 0 matches the independently known published digest. That is
a genuine, non-circular anchor: the crate is the authors' reference
implementation and is independent of blake3_ref.py. It is NOT the published
artifact, and test_oracle.py still calls it "Official test_vectors.json". Read
it as "checked against the official reference implementation using the official
vector parameters". Keeping the generator in-tree means this is reproducible
rather than another thing that evaporates.
Two independent reviews (different models, no coordination) found no
discrepancy in the primitive. One wrote a from-scratch BLAKE3 structured
deliberately differently and differentially tested 100k random compressions,
all 128 flag values x {6,7} rounds, a rounds sweep 0..8, and whole-hash over
227 lengths x 4 modes, with zero mismatches; it confirmed r < rounds-1, so the
classic 6-permutes-for-7-rounds off-by-one is absent. Independently,
blake3_ref.py reproduces the published known-answer vectors for "" and "abc"
exactly, which pins IV, G, all four rotations, the permutation and its count,
the feed-forward, the flag bits and LE packing in one shot.
README records what review found and did not fix:
- the harness prints "VALIDATION STATUS: VALIDATED ... anchored on official
test vectors + official PyPI package + Plonky3" even when anchor 2 SKIPs;
the status dict is written and never consulted. Observed firing.
- test_internal_consistency documents a feed-forward recomputation it does not
implement.
- DESIGN's internal Blake3 bus omits the input-to-output timestamp binding that
keccak — its own cited precedent — carries in both halves of its tuple.
Without it two compressions can swap outputs with every bus still balancing.
The gate models arithmetic only and cannot see it.
Two reviews, different models, no coordination between them. Both reached the same verdict independently: NO discrepancy in the primitive. Recording what each pinned, and — more usefully — what neither covered. Settled that no anchor covers: - Counter split order at t >= 2^32: t_lo -> v[12], t_hi -> v[13], verified BEHAVIOURALLY against the official crate via two independent counter paths (OutputReader::set_position, hazmat::HasherExt::set_input_offset) over counters 0..2^47, 44/44. Negative control breaks 5 of 6 chunk cases; the sixth is counter=0, correctly invariant under the swap. Closes ORACLE.md's O5. - Message schedule count AND direction: iterating permute from the identity reproduces all seven rows of the crate's MSG_SCHEDULE. Three mutants caught; a fourth (permute after the last round) is provably a no-op, so the guard cannot hide an off-by-one in either direction. - compress does not mutate its arguments; incremental update() == one-shot. Four more harness defects beyond the two already recorded: - the missing-file FileNotFoundError CASCADES — it kills anchors 2 and 3 and the canonical-vector emitter, which is why the gate's positive controls were blocked on an unrelated download. That single coupling is what made this recovery look worse than it was. - test_6round_derivation's first assertion is a tautology: compress_6round's body IS compress(rounds=6). ORACLE.md §2.6 calls it the "Code-diff anchor"; it establishes nothing. - compress() defaults to rounds=7, so a 6-round caller that omits the kwarg silently gets 7. Trace generators must use compress_6round — this should be enforced, not conventional. - ORACLE.md §5's ratio is internally inconsistent (~1/6 by its own numbers, not the "1/4-1/3" its prose claims); superseded by DESIGN.md §6's derived ~1/15. And the honest gap, recorded as the next reviewer's target: both passes established that the ORACLE defines the right function, so the gate's UNSATs are about the right function. NOBODY has audited the gate's transcription of that oracle into constraints — only its constants block was spot-checked. The EC campaign's equivalent audit found three premises the gate asserted and never read, one hiding a working forgery, so this is not hypothetical. The dangerous direction is a model STRONGER than what it models: it yields UNSAT where the real object is forgeable, and no positive anchor can catch it, because honest inputs satisfy a correct model and an over-strong one equally well.
…e banner Three findings from the review were recorded as "open" instead of being fixed. Fixing them; they were small. DESIGN — the input/output binding on the internal Blake3 bus is now MANDATORY. §1.1 defined a receive of (h, m, t, block_len, flags) and a separate send of out[0..16], both at multiplicity mu, and §3 listed TIMESTAMP_0/1 as "bus binding (internal variant may omit)". Omitting it is a real hole: with two compressions in a trace, row A can receive inputs_A and send out_B while row B does the reverse — every tuple appears exactly once on each side, so the bus BALANCES, and both callers read a result that is not the compression of their own input. keccak.rs, the chip this design copies its I/O idiom from, carries the timestamp in both halves of its internal bus precisely for this reason. §1.1 now states the requirement with the attack and the precedent, §3's "may omit" is gone, and it is item 10 of §7's soundness-critical list — together with the fact that the gate CANNOT catch a violation, because it models arithmetic and has no bus layer at all. Added item 11 for the same reason: MAIN 0 proves one G under free inputs, so a wrong column index in one of the 48 emitted instances is invisible to it; the concrete positive controls are what cover that. The third finding (the 3-op carry admits (1,0) and (0,1) for carry 1) is left alone on purpose — it does not admit a wrong sum, so it is a note, not a defect, and the README says so to stop someone "fixing" it into a bug. test_oracle.py — the banner no longer lies, and a missing fixture no longer cascades. It printed "VALIDATION STATUS: VALIDATED ... anchored on official test vectors + official PyPI package + Plonky3" unconditionally, including on runs where an anchor SKIPped: the status dict was written and never read. It now reports what actually ran (VALIDATED / PARTIALLY VALIDATED / NOT VALIDATED) and names the anchors it is NOT anchored on. Separately, one FileNotFoundError used to abort anchors 2 and 3 AND the canonical-vector emitter, which is what silently blocked the z3 gate's positive controls on an unrelated download; anchors are now independent and a missing fixture skips only itself. Anchor 1 is relabelled "Official-parameter vectors" and prints its provenance, because the shipped file is regenerated from the blake3 crate rather than downloaded — a genuine non-circular anchor, but not the published artifact. Both fixes verified to bite: with official_test_vectors.json removed, anchor 3 still runs, the canonical vectors are still emitted, and the banner degrades to PARTIALLY VALIDATED naming what it lost. Gate re-run after the changes: OVERALL PASS, positive controls included.
Two independent transcription audits of z3_blake_verify.py — one authored elsewhere (TRANSCRIPTION-AUDIT.md), one an executable 74-check suite (audit_gate_transcription.py + GATE-TRANSCRIPTION-AUDIT.md). Both ask the only dangerous question: is the gate's model STRONGER than the thing it models? A weaker model yields spurious SAT, which is safe; a stronger one yields UNSAT on a forgeable object, and no positive anchor can see that, because an honest witness satisfies a correct model and an over-strong one equally well. Headline: every equation in the gate matches the design it encodes, and the gate's bref_* reference is element-wise identical to the externally-anchored oracle (IV, MSG_PERMUTATION, G_CALLS, counter split across 2^32, and permute applications = max(rounds-1,0)). So the "gate proves the wrong function" risk is closed. The mutation sweep fires on 7/7 bug classes that ship no negative control, including a wrong column in G instance #7 — the per-instance wiring gap recorded as §7.11. One audit also ran anchor 2 live (PyPI, 92/92), so the historical counts now reproduce as recorded rather than on trust. THE FINDING, agreed by both and now written into DESIGN §7.4/§7.5: the "free range check" invariant is DECLARED, not derived. build_g returns each add output as fresh_word() = 4x BitVec(...,8), so byte range holds by construction in the model, and the gate proves the identical UNSAT for a chip that has the downstream XOR and for one that does not. Dropped, the sum is forgeable — a = b = 0x80000000, honest s = 0, forged s = 2^32 with carry = 0, satisfying every modelled constraint. Same blind spot for the message columns: m is declared as bytes, so the 32 explicit AreBytes sends §4.7 requires are unverifiable here, and without them a word has many F_p cell representations of one value. These invariants rest on the implementer; a green board is not evidence for them. Corrections forced into DESIGN.md: - §4.2/§7.3: the load-bearing bound set is AT LEAST ONE of {SLL_lo, SLL_hi} — the two SLLC bounds are not load-bearing at all, so only half the AreBytes sends per rotation carry soundness weight. The composed forgery with both SLL bounds dropped exists for exactly ONE input, X = 0xFFFFFFFF (forged Y = 0), exhaustive for r = 4 and r = 9 — the isolated control made it look reachable for arbitrary inputs. And the rotation OUTPUT needs no range check of its own; the recombine identities pin it. - §4.8: the recombine identity's body is linear, so 1 -> 2 after x mu, not the 2 -> 3 claimed. Overstated in the safe direction; "no constraint exceeds 3" is unaffected. - ground-truth/Cargo.toml needed an empty [workspace] table or cargo absorbs it into the parent workspace and the documented regeneration flow fails out of the box. That was a real bug in what I committed. Both audits independently verified the previous commit's fixes are real: the TIMESTAMP binding (with the keccak precedent confirmed at keccak.rs:264-319), the banner honesty fix, and the cascade fix — the last two exercised live by renaming the fixture away. Also committing the t >= 2^32 counter probe (ground-truth/src/bin/), and a .gitignore for target/, Cargo.lock, __pycache__ and the 114 MB venv. Re-verified after all edits: suite 74/74, gate OVERALL PASS.
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).
DESIGN.md defers twice to `../keccak-verify/` — the cost model (tier2_cost_model.md) and the shift-identity bound-necessity proof (hwsl_inline_test.py Part 2). That directory died in the same 2026-07-23 session scratchpad this design was recovered from and was never committed: it exists on no branch, and `git log --all --diff-filter=A` finds it zero times. A reader following either citation chases nothing. Nothing rests on them. The cost arithmetic was recomputed from scratch (per-G 62 cells x 48 = 2,976; columns 3,155; sends 1,250; aux 1,875; total ~5,030, and ~1/15 of keccak-f) and checks out. The shift-identity result was re-derived symbolically over all 2^32 inputs by the 2026-07-29 transcription audits, which is stronger than the single-point check the lost file made — one audit flagged the missing file precisely because it had re-derived the result rather than trusting the citation. Fourth dead-citation instance this week. The others: lincomb2's "blake3 6-round assumption" precedent, which never existed because this very work never shipped; the EC gate's C5 pointing at a document containing no soundness argument; and the EC board's C4 invoked well outside its own text. Marking rather than deleting, so the provenance stays legible. Gate re-run after the edit: OVERALL PASS.
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.
`commit_phase_from_evaluations`, `query_phase` and `batched_commit_phase` take the `H: StarkHash` the rest of the stack already threads and build their layer trees with `H::Pair`, where they named the concrete keccak alias before. The invariant this maintains: the prover's FRI layer trees and the verifier's authentication of those openings are one hash, by construction rather than by coincidence. `verify_fri_layer_openings` re-hashes each opened pair through `H::Batched`, and `StarkHash`'s two-element invariant says `Batched` and `Pair` agree on a pair — so naming a single configuration is what makes the two sides agree, instead of two call sites happening to reach the same alias. A configuration other than the default previously had the prover commit with one hash while the verifier checked with another, rejecting every honest proof at its first FRI query. Keccak stays the default everywhere: the aliases are untouched, and at `KeccakStarkHash` every one of these functions builds exactly the tree it built before, so proof bytes on the default path do not move. Under `cuda`, `StarkHash::Pair` gains the `KeccakTreeBackend` bound `Batched` already carries, for the same reason: `gpu_lde`'s FRI commit hashes every layer on the device with the keccak kernels and only labels the result, so a cuda build cannot honour another configuration for FRI layers either. The four GPU FRI entries become generic over that labelled backend, matching the tree entries next to them.
The oracle for the configuration threading: `GenericProver` and `GenericVerifier` at `Blake3StarkHash` round-trip a real folding STARK, so the invariant that the prover's `H::Pair` layer trees are authenticable by the verifier's `H::Batched` is checked against a hash that is not the default. Six tests, each earning its place: * the BLAKE3 round trip, asserting the proof carries committed FRI layers so it cannot pass vacuously on a trace that never folds; * the keccak round trip, as the honest-path control over the same rewritten code path; * two falsifications — a flipped FRI layer root, and a tampered symmetric evaluation that leaves the transcript intact so only the Merkle check can catch it; * the stark-proof-level control that the two configurations are actually different hashes: same trace, same transcript seed, different roots, and each verifier rejects the other's proof; * and the producer-side pin — every committed layer's root must equal an `H::Pair` tree rebuilt from that layer's own evaluations, at both configurations, with layer 0 (whose codeword is identical either way) differing only because the hash does. Behind `cfg(not(cuda))`, as `Blake3StarkHash` is.
`FieldElement<GoldilocksField>` is `Copy`, so `clippy::clone_on_copy` rejects the pair construction. Same leaves, same roots — the assertion is unchanged.
The root comparison across configurations only means "the hash differs" if the codeword being hashed is the same. That was stated in a comment — ζ₀ is drawn before anything is appended, so both configurations fold the same input with the same challenge — and is now asserted, so a change that made the two arms fold differently would fail here rather than quietly weaken the claim.
Completes the device side of PA-PLAN §6.1. The compression function, the Merkle parent/level compressors and the byte serialization already landed; what was blocked was the multi-block leaf path, which needs a chaining construction across a leaf's 64-byte blocks. That construction is now specified — `Blake3Chain`, PA-PLAN §1.7: standard BLAKE3 restricted to a single chunk that never ends, `t = 0` throughout, CHUNK_START on the first block, CHUNK_END|ROOT and the true byte count on the last, digest = the low 8 output words little-endian. The device struct is a transcription of the host `Blake3Chain`, and holds a full block rather than compressing it for the same reason the host does: whether a block is the last is not known until the message ends, and the last block's flags and block_len differ from every other's. Compressing eagerly on fill would hash a 64-byte message as two blocks and break P2, the property that makes a 64-byte message exactly a Merkle parent. Seven leaf kernels, twin for twin with keccak's, same read pattern in every case — the leaf BYTE layout does not move under P-a, only the hash over it: blake3_leaves_base_batched keccak.cu:152 blake3_leaves_base_row_pair_batched keccak.cu:196 blake3_leaves_ext3_batched keccak.cu:237 blake3_comp_poly_leaves_ext3 keccak.cu:277 blake3_fri_leaves_ext3 keccak.cu:326 blake3_leaves_base_row_major_row_pair keccak.cu:473 blake3_leaves_base_row_major_row_pair_range keccak.cu:511 `merkle_gather_paths` gets no twin: it copies sibling nodes and never hashes, so both trees share it. Wrapper twins in src/blake3.rs for all six merkle.rs entry points named in §6.1, plus test-reachable wrappers for the two row-major kernels (the keccak ones are driven privately from the LDE pipeline; blake3 has no production caller yet) and a `chain_probe` harness so the construction can be checked against known-answer tables from host code. The construction is a DRAFT pending ratification of forks F1-F3 (PA-PLAN §1.7.3) and is implemented as the working default by standing decision. Keccak remains the prover's hash: `StarkHash` still requires `KeccakTreeBackend` under `cuda`, so nothing dispatches here.
…ernels
Two layers, because they fail for different reasons.
GPU parity (needs a GPU, runs on a rented box):
blake3_leaves.rs all seven leaf kernels vs the CPU leaf function
blake3_fri_layer_tree.rs full FRI-layer tree, node for node
blake3_comp_poly_tree.rs comp-poly tree through BOTH build wrappers
blake3_chain_kat.rs the device chain vs external references
blake3_merkle_gather.rs paths over a BLAKE3 tree
The CPU side is the production `leaves_bit_reversed_grouped` at the BLAKE3
backend plus the production tree builder, so nothing in the comparison is
written for the test. Each file asserts the crypto/math-cuda `blake3-6round`
lockstep first: out of lockstep every assertion compares a 6-round device
tree against a 7-round host one and fails with a wall of unequal bytes that
names nothing.
Host KAT (no GPU, no cargo, seconds — the per-PR gate):
The existing harness compiles blake3.cu as host C++ through a shim. Extended
with a thread-replay macro so a whole launch can be reproduced on host, which
means every leaf kernel's read pattern is now checked locally rather than
only on a GPU box.
★ On risk R13 — "track G would be checking a device port against the same
code path it was derived from". The anchoring is layered so that nothing is
checked against itself:
1. the compression function official BLAKE3 vectors (7r), oracle-
derived canonical vectors (6r)
2. a byte-level chain reference official MULTI-BLOCK vectors (7r, new
table 3) and the committed CHAIN_KAT_6ROUND
3. the device Blake3Chain vs (2), 151 lengths across block boundaries
4. each leaf kernel vs (2) over the byte stream the CPU leaf
function specifies
Layer 2 is new and is what R13 was missing: `Blake3Chain` over a message of
at most one chunk IS `blake3::hash`, so the published vectors are a direct
known-answer test for the framing — the flag schedule across blocks, the
chaining value, the final block's block_len — not merely for the round
function. The 1025 and 2048 rows are the P3 negative control: without them
every matching row would pass identically had the full chunk tree been
implemented instead of the single unbounded chunk.
The harness was mutation-tested. Six deliberate kernel breaks — eager
compression on block fill, CHUNK_START on every block, block_len 64 on the
final block, no bit reversal, swapped row-pair order, swapped felt word
order — are all caught, the first at exactly the 64-byte P2 case.
`make test-blake3-host-kat` now builds and runs BOTH round counts. The
6-round arm is the one the campaign ships and the one no other CI job
compiles (risk R10), and the round count is a compile-time knob, so a
single-arm run left the shipping configuration ungated.
§4.1 described a parameterization that stopped short of FRI. It now describes the one that reaches it, and states the invariant that makes prover and verifier agree: the prover builds layer trees with `H::Pair`, the verifier re-hashes each opened pair with `H::Batched`, and `StarkHash`'s two-element invariant is what joins them. Also records the `cuda` fork's extension to `Pair`, and why the `FriLayerMerkleTree` aliases survive as the default configuration's names. §4.4's open question is answered: continuation chaining binds NO commitment-hash-derived value across epochs. The epoch-to-epoch carry is a plain register file plus the GlobalMemory bus, every epoch's transcript is fresh, and the one chained `Commitment` binds an epoch to the global proof inside the same bundle, so it moves with a flip rather than against it. The real format surface is a PINNED constant rather than a chained root — `static_zero_page_commitment`, deliberately excluded from the private-input mechanism and therefore baked into both the host verifier and the guest ELFs. Also upgrades the checked-in-proof-blob bullet from inferred to verified, and records that the rkyv wire format does not move. §4.6's emitter census was one short. `emit_register_commitment` builds a whole Merkle tree in eDSL over the cross-epoch register carry, so the carry that §4.4 finds hash-free on the host path is fed through the commitment hash in-machine by the wrap. Its one call site is why a `merkle_walk` grep missed it.
…ors do NOT pin Three findings from an independent re-derivation of the 6-round provenance chain. Two are corrections to claims that were about to be overstated; one is a validation harness that has been silently dead. ★ check.py was broken by P-a Stage 1 and nothing noticed. `thoughts/blake3/reference-impl/check.py` validates the committed 6-round vectors against upstream BLAKE3's own portable C with its round loop parameterised. Stage 1 moved CANONICAL_VECTORS out of prover/src/lfm/blake3.rs into crypto, and the harness still read the old path — so it died on a bare `ValueError: substring not found` partway through, taking checks [D] and [E] with it. [E] alone is a 5000-case randomised differential against the Python oracle at both round counts. Both have been dead since the move. Repaired: the path now points at crypto/crypto/src/hash/blake3/vectors.rs (the parser itself is layout-independent and needed no change), and a missing table now reports where to look instead of raising ValueError. A harness that dies with a traceback when the code it validates is refactored gets deleted rather than fixed. It had no make target, which is why nothing ran it. It has one now: `make test-blake3-second-source`. All 13 checks green, including the two that had never run against the post-Stage-1 tree. ★ The official vectors do NOT pin the counter split. Measured, not argued: a compression with v[12] and v[13] transposed reproduces the official BLAKE3 vectors at ALL 65 single-block lengths, and passes the multi-block chain vectors too — because both hash whole messages and so only ever exercise t = 0. Only CANONICAL_VECTORS catches it, whose ten vectors all carry t >= 2^32: 320 failing words against 0 from either official table. Recorded in both places a future cleanup would look, because "the standard already covers this" is exactly the reasoning that would retire the only check on the counter split. ★ The `if (r < ROUNDS - 1)` permutation guard is unobservable. Also measured: removing it — permuting after every round including the last — passes the entire host KAT at both round counts, since the schedule permuted after the final round is never read. It is an optimization, not a convention any known-answer test can validate, and upstream expresses the same schedule as an indexed table with no guard at all. Noted so it is not cited as validated. Also: the P3 divergence is now located rather than sampled. Sweeping all 35 official cases puts agreement at every length <= 1024 and failure at every one of the 18 lengths >= 1025 — the boundary sits exactly on the one-chunk edge. And the 6-round provenance is no longer Python-only: the upstream C reference reproduces both committed columns 10/10, and encodes the message schedule as an indexed table where our Rust and CUDA compose one permutation between rounds, so its agreement cross-validates the schedule instead of restating it.
…aw schedule `DefaultTranscript` becomes generic over a `TranscriptHash` configuration carrying two things that are decided together: the digest the sponge runs on, and how many candidates a field-coordinate draw consumes. `Blake3Transcript` is the BLAKE3 instance; every method body was already hash-agnostic. The invariant this maintains: the keccak transcript does not move. `T` defaults to `KeccakTranscriptHash`, so `DefaultTranscript::<F>::new(..)` names exactly the transcript this system has always produced, and that configuration keeps the unbounded rejection schedule — its bytes, its challenges and its proofs are untouched. Rider 1 (`others/lfm-migration-riders.md`) is adopted for the BLAKE3 configuration: a coordinate draws exactly two candidates and takes the first in range, so the consumption schedule no longer depends on which bytes the sponge happened to produce. That is what a straight-line machine needs — the LFM transcript replay encodes one schedule and cannot follow a data-dependent one. Two decisions inside that are not obvious and are load-bearing: * The fallback when every candidate misses is to keep drawing, NOT to reduce into range. A modular fallback would bias challenges by ~2⁻³² per draw, which at production draw counts is ~2⁻¹⁹ of statistical distance and would dominate this system's soundness error. Drawing on keeps the distribution exactly uniform and leaves a fixed schedule that holds except on a ~2⁻⁶⁴ tail. Failing instead would make challenge sampling fallible on the verifier's replay path, which the no-panic policy forbids. * The seam is the transcript, not the field. `HasDefaultTranscript` gains only the acceptance predicate `candidate_in_range`; the transcript pre-filters the candidate stream with it, so the field's own rejection loop exits on its first call and consumption is exactly `n` per coordinate. No second sampler exists to disagree with the first.
`generate_nonce` and `is_valid_nonce` take the digest as a parameter, and `StarkHash` names the Fiat-Shamir configuration it is paired with, so the prover's search and the verifier's re-check both reach it through `GrindingDigest<H>` instead of a hard-wired keccak. The invariant this maintains: the proof-of-work is the proof's own hash. The grinding seed is `transcript.state()`, so a configuration that transcripts with BLAKE3 and grinds with keccak would be doing work over a digest nothing else in the proof uses — and prover and verifier could still agree with each other, which is exactly why it needs to be structural rather than checked. Nothing about the construction changes: two hashes of one block each (41 bytes inner, 40 outer), seed and digest `[u8; 32]` on both sides, so this is the type substitution PA-PLAN §3 describes and the keccak numbers are unmoved — the existing vectors still pass, now naming their digest explicitly. `D` is deliberately a parameter with no default. A defaulted one would let a configuration that had moved everything else keep grinding on keccak silently. `find_any` is kept as-is: the `find_first` determinism change is a separate unratified item and does not ride here. Tests: a nonce ground under BLAKE3 satisfies the BLAKE3 check and, as the control that the substitution happened at all, does NOT satisfy the keccak one — at grinding factor 20, so a chance pass is 2^-20.
…ull configuration Three things needed oracles and none of them could borrow one. The sponge: `state()` is the grinding seed, so it is pinned against `Blake3Chain` computed directly — which is itself anchored from outside, its 7-round arm against the `blake3` crate at every length within a chunk. The squeeze chain is reimplemented rather than compared against itself, because a hash swap that dropped the reverse-and-reabsorb step would leave prover and verifier agreeing with each other while producing a transcript nobody else can reproduce. Writing it caught a real misreading: the squeeze is `finalize_reset`, so squeeze k+1 hashes the reversed output of squeeze k alone and not the absorbed history. That is now pinned rather than assumed. The schedule: consumption is not visible in a draw's output — the value cannot distinguish "took the first and stopped" from "took the first and kept drawing", and it is the stopping that a machine cannot follow. So the schedule is driven by a counting closure over streams with the acceptable candidate at every position, including none, and separately reconstructed from the raw squeeze stream to show an extension draw reads candidates (0,1), (2,3), (4,5) rather than 0, 1, 2. The keccak arm gets the honest-path partner: it still reads one candidate per coordinate, so the branch is a branch and the default did not move. The configuration end to end: BLAKE3 commitments, a BLAKE3 transcript and BLAKE3 grinding proving and verifying together, with the falsification that a keccak transcript replaying it rejects. Grinding is on at factor 1, so a port left wired to keccak fails here.
…question answered Rider 1 is adopted, and §2.3 now carries what adopting it costs: two candidates per coordinate instead of ~1, so challenge sampling consumes twice the squeeze bytes. That is small in the prover and lands in the recursion guest, which is where the cycles have been fought over — "the cheapest item in the whole plan" understated it. Also records why the fallback cannot be a modular reduction: the ~2^-32 per-draw bias would dominate the ~92 proven bits. Rider 2's premise was wrong and the correction reverses its verdict. The `(3 + L) mod 4` shift is modulo BYTES_PER_HALF = 4 — the eDSL's half width — not the sponge's rate; the machine test that pins it says so, and the rate appears only in the block count. Since 4 divides both 136 and 64 and the message bytes are identical, the shift and the splice cost are INVARIANT under the hash change. So P-a is not this rider's forcing function: by the riders file's own admission rule it does not belong to a migration that need not touch that code. Left open for Mauro with the numbers, and pointed at Stage 5 or 6 as the natural host. Also notes that "one-byte pad" is a misnomer — L is workload-determined, so the pad is the 0-3 bytes to the next multiple of 4. §3's open question is answered the other way from what it expected: the wrap DOES re-check the grinding nonce. The search had looked in epoch_verify.rs; the check is in the challenge spine, where the absorbs are. What that turns up instead is a Stage 5 item §4.6 does not list — the check reaches keccak through a sponge-FRAMING emitter that encodes the 136-byte rate and pad10*1, so a BLAKE3 port there is a framing rewrite rather than a compression swap.
The 6-round cross-check is reproducible, and two places said otherwise: the `CHAIN_KAT_6ROUND` doc comment and PA-PLAN §1.7.4 both described the Python oracle as surviving only in `__pycache__`, its source and `canonical_6round_vectors.json` gone, and re-running it as depending on an artifact `git clean` removes. What is actually there: `thoughts/blake3/blake3-oracle/` holds `blake3_ref.py` (vendored at 6502509) with raw `compress` / `compress_cv` / `compress_6round` entry points as well as `blake3_hash`, plus `canonical_6round_vectors.json`, `official_test_vectors.json` and `test_oracle.py`. The cross-check runs at compression level, not only at full-hash level. Both passages now also name the second source, which neither mentioned: `thoughts/blake3/reference-impl/` is upstream BLAKE3 1.8.5's portable C with its round loop parameterised, the entire edit being PARAMETERISATION.diff. It reproduces CANONICAL_VECTORS at both round counts and the §1.7.5 chain digests at 6 rounds up to one chunk, diverging past it. It earns its place by encoding the message schedule as an indexed MSG_SCHEDULE[r] table where the Rust and CUDA compose one permutation between rounds — a bug in the iterative composition is exactly what a single source cannot catch. `make test-blake3-second-source`. Two corrections to what the tables are claimed to establish, both measured: * Nothing in §1.7.4 pins the counter split. Every message there is hashed with t = 0, so a compression with v[12] and v[13] transposed reproduces the official vectors at all 65 single-block lengths AND the multi-block chain vectors; only CANONICAL_VECTORS catches it, at 320 failing words against 0 from either official table. The chain and compression tables cover different axes and neither is redundant — "the standard already covers it" is the reasoning that would retire the only check on the counter split. * The `r < rounds - 1` permutation guard is unobservable: always permuting gives identical output at both round counts, because the schedule permuted after the final round is never read. An optimization, not a convention any known-answer test can validate. The claim that the chain table is worth more than "the compression vectors it sits next to" goes with them; it was comparing things that measure different properties.
`Blake3StarkHash` does not exist under `cuda` — the device kernels are keccak-only, so `StarkHash`'s bounds admit no second configuration there. The two tests using it were already gated; the type alias naming it was not, so the cuda clippy pass could not compile the test target.
Brings #903's BLAKE3 compression accelerator onto the campaign branch: the `u64::MAX-2` syscall and its executor implementation, the `prover/src/tables/ blake3.rs` chip, the spec pages, and the oracle/gate material under thoughts/blake3/. Four conflicts, three of them trivial. `prover/src/lib.rs` is the one that mattered, and it is a semantic merge git could not do. Both sides added an always-on table to the same lists — this branch added HINT, #903 added BLAKE3 — and both sides therefore left `FIXED_TABLE_COUNT` at 11 while meaning different sets of eleven. The merged tree has both tables: `air_refs` pushes eleven always-on AIRs plus HALT conditionally, and the constructor builds both `blake3` and `hint`. So the constant is **12**, and getting this wrong would reject every proof on a sub-proof count mismatch rather than fail to compile. The import list and the doc comment take the union, keeping #903's warning that an always-on table costs every proof a near-empty AIR. The other three are add/add on files both branches inherited from the `spike/blake3-recovered` lineage — `blake3-chip/DESIGN.md`, `blake3-oracle/test_oracle.py`, `ground-truth/Cargo.toml`. #903's copies are taken: it is the authoritative home of its own chip documentation, and its later commits refine exactly the lines this branch still carried (the six lines unique to our side are pre-correction text, including the `../keccak-verify` citations that `820fe7f1` marked historical). Keccak remains the default everywhere; nothing here selects BLAKE3. ⚠ #903 implements the 6-round internal variant, resting on the A6R assumption its own spec page records as "to be ratified in the spec before production use". That is unchanged by this merge and remains open.
…itive Merging #903 reintroduced a second host transcription of the BLAKE3 compression function. `executor::vm::instruction::execution::blake3_compress_6round` has its own `blake3_g`, its own `BLAKE3_IV` and its own `BLAKE3_ROUNDS = 6`, and does not call `crypto`'s `blake3_compress_rounds` — the primitive P-a Stage 1 hoisted into `crypto` precisely so there would be one definition, and which the CUDA reference was already made to re-export rather than restate. Two independently written encodings of one function is what PA-PLAN §1.4 forbids. This does not unify them — that is a change to #903's code and belongs with whoever owns the chip — but it makes the divergence a test failure instead of a silent one, which matters more here than usual: the executor is what the guest's syscall actually runs, so a mismatch is a guest hashing differently from the host prover, and R5 says that surfaces only as in-guest proof rejection, never as a host test failure. They agree today, over the flag and counter shapes the chain framing emits (CHUNK_START, interior, CHUNK_END|ROOT with a partial block, and both halves of a full 64-bit counter) at 64 pseudo-random states each. The control checks the comparison is round-count sensitive, so it is not passing because both sides ignore the parameter.
…iles Follow-up to 865eb26 carrying nothing of its own. `prover/src/lib.rs` is that merge's union import list run through rustfmt. The conflict resolution took both sides' `create_*_air` names and left the wrapping mid-list; no name is added, removed or reordered. The two guest-program lockfiles are cargo's own output from building the guest artifacts against the current workspace. They drop `rand 0.8.x` and `rand_chacha 0.3.1` from `crypto` and `math`, neither of which is a real dependency of either crate: #841 removed crypto's when it dropped ChaCha20, and math's are dev-only, which a path-dependent guest package does not resolve. The entries were stale rather than newly dead. The remainder is the format disambiguation a single surviving `rand` version no longer needs. No version moved and nothing was added.
…mBlake3 A BLAKE3 guest today hashes every Merkle node in software. The `TypeId` specializations in `merkle_tree::backends::field_element_vector` dispatch on the concrete `PlatformKeccak256` type, so a BLAKE3 `D` correctly falls through to the generic `D::new()/update/finalize` path — it cannot be mis-routed, but it also reaches no precompile. #903 landed one; this connects it. The connection is made at the compression, not at the hash. `Blake3Chain`'s two calls into `blake3_compress_rounds` become one `compress_block`, and that is where the riscv64 arm marshals into the syscall. Everything above it — single chunk, 64-byte blocks, CHUNK_START / CHUNK_END|ROOT, `t = 0`, the true byte count as the final block's `block_len` (PA-PLAN §1.7) — stays one piece of code running on host and guest alike. Writing the framing a second time inside a guest adapter is the trap §1.4 names and the one the executor's duplicate compression already cost us a gating test to contain, so `platform_blake3.rs` is a re-export of `Blake3Chain` and nothing else. Two couplings are made mechanical rather than documented: - The executor's `BLAKE3_ROUNDS` is a hard 6 with no feature behind it, so the syscall arm is only the host prover's hash while this crate is at six rounds. A `const _` assert ties them, and inverting `blake3-6round`'s polarity is now a guest build failure instead of a root the verifier rejects. - `with_rounds` exists so the 7-round external anchor is reachable from one build, and the accelerator implements six and nothing else. Any count but the crate-global one takes the software path, so a machine with the precompile cannot answer the anchor at the wrong round count. The dword packing is the last link between the two hashes that no test covered: `executor_primitive_parity` gates the compression and `crypto` gates the framing, but a transposed dword or a swapped counter half would leave both green and still desync the guest. It needs no guest to check — the executor's handler is ordinary host code — so `executor_syscall_packing` lays the packed state into a VM `Memory`, runs a real `EcallEbreak`, and unpacks the result through the same two functions the guest calls, over the flag shapes the chain emits plus both halves of the counter. Its control shows the counter's halves are distinguishable, so agreement is not agreement-under-a-swap. Nothing selects BLAKE3: keccak remains the default on every path.
`continuation_fixture_generates_two_epochs` and the 18 tests downstream of it fail: the fixture yields one epoch, so there is no INTERMEDIATE epoch for `epoch_tests` to build a trace from and no second epoch for `machine_tests` to find. The cause is the fixture's own premise, which is no longer true. `FIXTURE_EPOCH_LOG2`'s doc records the inner guest as running "somewhere between 17 and 64 cycles", so that only a 16-cycle epoch splits it. Measured now, by running the ELF to completion under `Executor::resume_with_limit` and counting logs: it runs **15 cycles**. Fifteen does not split at 16. It splits at 8, into exactly two epochs, which is what the constant now selects. Nothing in this tree moved it. `bench_vs/lambda/fibonacci` is a dependency-free `no_std` crate in its own workspace, and the ELF the pinned nightly builds from it is byte-identical at `8e4cb0cf` and at HEAD (sha256 117a716c99c87da39f3536ce25fa40814555815ec5ac4d3746d813543dd4799c). The canary fails the same way at `8e4cb0cf`, before the accelerator merge, with the same `epochs=1`. The count is a property of the compiled artifact — the toolchain and sysroot — not of anything under review here, so the doc now says so and gives the recipe for re-deriving it rather than leaving a range to be trusted.
|
Benchmark Results for modified programs 🚀
|
`prover/src/lfm/blake3_chip.rs` has been a complete, unregistered chip since track G: column layout, AIR, trace filler, bus interactions and BITWISE multiplicities, but no slot in the fixed AIR set. This registers it as slot 11 — last of the chips this machine owns, before the hosted keccak family — and wires the eight plumbing surfaces `LFM_KECCAK` occupies: an instruction, a builder emitter, a column group, an executor arm, admission checks, a trace, an AIR slot and a registry root. ★ This is a proof-format break for every LFM proof, by construction, and it lands whether or not any emitter switches. `NUM_LFM_CHIPS` is the WIDTH of the roots and log-heights arrays that every registry entry stores, that `lfm_program_id` folds and that `absorb_lfm_statement` feeds the transcript, so 14 -> 15 moves every root, every program_id, every challenge and the sub-proof count. The re-bless below is therefore intended rather than investigated — `cargo run --bin compute_lfm_registry --release`, all six entries, cause: chip count 14 -> 15. Slot 11 carries the new group at log-height 2 (an empty group pads to the 4-row minimum) in every entry, which is the visible signature of the move. It is the LFM-side analogue of the RV64 `FIXED_TABLE_COUNT` 11 -> 12 break the #903 merge already shipped, and both want one announced format bump. Keccak remains the machine's default hasher and nothing selects BLAKE3: this commit adds a chip and an emitter, not a switch. Two design decisions worth naming: - **Slot 11, not 14.** `KECCAK_RND_SLOT` moves 11 -> 12 as a result, but it stays the boundary between owned chips and hosted tables, which is the shape every index expression in `airs.rs` is written against. Appending would have put a program-dependent group after two fixed tables. - **The chip carries the free reversed digest.** `DefaultTranscript::sample()` reverses the 32 digest bytes and re-absorbs them, hash-agnostically, so the BLAKE3 configuration squeezes exactly as the keccak one does. Reversal is a different `Linear` over byte columns the plain digest send already covers: two interactions and four preprocessed columns, and no value columns. Without it every in-machine squeeze would pay eight explicit byteswaps. The value-column filler is now one function, `fill_blake3_witness`, shared by the standalone probe's trace and the machine's — registration made two callers out of one, and a second transcription of 3,056 columns in a fixed order is exactly what the single-dataflow rule exists to prevent. Also in the blast radius, fixed rather than shifted: - `resolve` rejects a duplicate `(kind, blowup_factor)` instead of taking the first match. The generator's doc promises a second hasher "becomes additional rows, never a silent replacement", but the key carries no hasher, so the second row would have been unreachable data — and `resolve` is the soundness argument's first premise. `the_registry_is_six_unambiguous_rows` pins the count so adding rows stays deliberate. - `logup_tests`' fixed-table census listed NINE tables while `FIXED_TABLE_COUNT` was 12. It now lists all eleven an intermediate epoch carries, in `VmAirs::air_refs` order (HALT is final-epoch only), and asserts its own length against the constant. - `epoch_verify_tests`' 111-challenge pin was written when an epoch was 24 sub-proofs. It is 119 over 26, with the accounting asserted — four challenges per always-on RV64 table — so the next one fails saying which input moved. - The R1f fixture cache is keyed on `FIXTURE_EPOCH_LOG2` and the inner ELF, so a fixture change misses the cache instead of silently reading the previous configuration's proof.
…evel hash The chip landed in the previous commit; this is what reaches it. Three layers: the `Blake3Chain` sponge framing, a construction layer parameterized on the digest rather than duplicated per hash, and the call-site switch. ★ **The hash is a value on the builder, not a parameter threaded through every emitter, and that placement is the safety argument.** The campaign's standing risk (R-3) is that a missed emitter site keeps hashing keccak after the flip and produces a valid proof of the wrong digest. With `LfmBuilder::wrap_hash` there is no site to miss: every `edsl::wrap_*` construction reads the one value. What stays visible is the opposite and much smaller list — the emitters that must NOT follow the configuration still name `keccak256` explicitly, so a grep for the pinned hash in `lfm/` returns exactly the deliberate exceptions. Nine sites, and the two traps the naive sweep walks into: | site | fate | |---|---| | `sub_proof::emit_leaf_hash` (both branches) | follows | | trace Merkle path, `emit_group_authentication` | follows | | FRI-layer leaf + path (`fri.rs`) | follows | | transcript squeeze / state (`transcript_replay.rs`) | follows, + rider 1 | | register commitment leaf + tree (`programs.rs`) | follows | | grinding, inner and outer (`epoch.rs`) | follows | | ★ `ByteString` | **split**: a second method, not a substitution | | ⛔ `programs::emit_program_id` | **pinned keccak** | | R1c / fixture / registry instruments | keccak by argument | `ByteString` is the live trap: `emit_program_id` and `emit_grinding_check` share it and have opposite fates. The host counterpart of the first names `PlatformKeccak256` explicitly (`recursion::program_id_from_digest`), so switching it would make the attestation join disagree with every host consumer — and the disagreement would surface as a consumer-side compare failing, not as an unprovable program. It now has `keccak256` (pinned) and `wrap_hash` (follows), and each caller selects one. ★ **The transcript site is not a hash swap.** Under BLAKE3 the configuration draws TWO candidates per base coordinate (P-a Stage 3, rider 1), which moves every refill boundary and therefore the squeeze count. `sample_felt` now draws `n`, SELECTS the first in range and asserts only the selection — asserting candidate 0 would reinstate exactly the restriction the rider was adopted to remove. `n` is read from `crypto`'s own `TranscriptHash` impls, never restated. The claim for review, stated rather than self-certified: the emitted program is complete except when every candidate misses (≈ 2⁻³²ⁿ per coordinate, ≈ 2⁻⁶⁴ at n = 2), where the host draws another `n` and the machine has no program to run — the restriction shrinks by 2³² and does not vanish. `sample_u64_pow2` is untouched in both configurations: production's `sample_u64` reaches the raw candidate stream, not the fixed schedule. The framing schedule is hoisted into `crypto` (`num_blocks`, `block_flags`, `block_len_of`) and `Blake3Chain::flags` now reaches it, so the emitter READS the host hasher's schedule instead of restating it. A second statement of "which block carries CHUNK_START" is the likeliest way for an in-machine hash to differ from the host's by one compression's flags, and that difference is a valid proof of the wrong digest. **Keccak remains the default and the default emission is byte-identical**: regenerating `LFM_REGISTRY` after this commit reproduces the previous commit's table exactly, which is the strongest available honest-path control — every root, every program_id and every challenge unmoved. Shapes left for the batched (MMCS) emitter, so it adds one construction and not one per hash: `WrapDigest` is one type under both hashes; `leaf_stream` makes the group's boundary explicit data; the walk is a loop over supplied siblings with no arity or height assumption. `blake3_chip_tests` is the new falsification suite — the release-visible constraint-index check (R-1), framing controls one choice at a time, the external anchor against the host chain, mutual unverifiability in both directions, and an honest-path control that keccak still proves and verifies through the rewritten emitters.
…ures `the_blake_column_and_the_residue_split` computed `[p_lo, p_hi]` — the wrap's compressions at BLAKE3's rate — printed it, and then drove its whole matrix from a hardcoded `let p = 192_000`. On this tree the measured interval is [287216, 291032], so every "x under keccak" row was taken at a hash count about a third under what the same function had just measured, in the direction that flatters every non-keccak column. The delegation instrument carried an independent copy of the same literal, so the two could drift from each other as well as from the truth. Both now read the measurement. The matrix prices at both ends of the interval, because the spine is absorption-bound and only bounded — a single number would be a choice about which end to quote, where two bracket the answer. The delegation instrument uses the legs' exact term and says outright that excluding the spine makes its "cost of delegating" a lower bound. What it costs the campaign's own headline, measured on the promoted tree (chunked, blowup 8, 73 queries, the 8-cycle fibonacci fixture): BLAKE3-7r 5.04x -> 4.24x / 4.21x at [p_lo, p_hi] BLAKE3-6r -> 4.53x / 4.51x Both still clear PA-PLAN section 5's 4.06x, and the 6-round arm — the one the campaign targets — clears it by 11%. The old 5.04x did not mean what it said.
…finition `TAG_SELECTOR`'s doc said `m[8] = MODE_C·"LFMC" + MODE_T·"LFMT"`, which is wrong twice: the tag sits at `m[NUM_LANES]` — `m[12]` at the RATE-4 lane count — and the selector is three terms, `MODE_L` having joined it when the leaf mode got its own domain. `message_word_ref` and the module header both already say so at the point of USE, so the definition was the one place a reader could pick up the old shape. `instr.rs`'s `HashMode::Transcript` carried the same `m[8]` claim. Comments only; no constant, selector or constraint moved.
Review finding (rev-chip F2): `BLAKE3_ROUNDS` is a configuration axis nothing binds. One registry entry describes two machines — `blake3-6round` moves `LFM_BLAKE3`'s `NUM_COLUMNS` 3556 -> 3076, `NUM_CONSTRAINTS` 897 -> 769 and the interaction count 1453 -> 1261 — and a proof built under one round count and verified under the other is rejected on an OOD width mismatch. That fails CLOSED, but it fails on a width rather than on the axis being NAMED, which is exactly what `hasher` gets a `program_id` fold for and `CommitmentHash` gets a compile-time guard for. Checked before pinning: regenerating `LFM_REGISTRY` under `--features blake3-6round` reproduces the committed table exactly — all 3,072 root and digest bytes, all six `log_heights`, all six `program_id`s. The blessing is invariant, so one table for two builds is correct rather than lucky. The mechanism is that the round count lives entirely in the VALUE columns while what the table commits is the preprocessed instruction group — addresses, multiplicities, the reversed-digest pair and MU, none of which mention `NUM_G`. `the_registry_blessing_is_round_count_invariant` asserts that separation in both directions (the prefix does not move, the witness does, and the two round counts really are different machines) and passes under both features. The generated block now states which configuration it assumes, and what would have to change if the round count ever became a per-deployment choice rather than a compile-time one.
… the framing gap Two review findings, one commit — both are the same failure mode, a claim the suite states without executing. **rev-emit E1: the BLAKE3 replay had no host oracle.** The keccak side has one (`machine_tests::transcript_replay_matches_the_host`); the BLAKE3 side had single-coordinate tests only, and those are structurally blind to exactly the bug Stage 5 could introduce. Demonstrated rather than asserted: forcing `candidates_per_coordinate` back to 1 for the BLAKE3 arm leaves `the_in_range_predicate_is_canonicity_as_a_bit` PASSING and the FIRST challenge correct — candidate 0 is in range with probability 1 − 2⁻³², so it is the answer under either schedule. The divergence appears at the SECOND, where a schedule that consumed 8 bytes instead of 16 reads from the wrong buffer offset. The oracle is a SCRIPT — two base draws, an extension draw, an absorb that invalidates the output buffer, a `sample_u64` draw (which takes the raw candidate stream in both configurations and must NOT move), a further base draw, a raw `sample()` whose reversed digest becomes the next segment, and a last draw on the far side of it — with all eight published values compared against the real `DefaultTranscript` under the same configuration. It exercises the three Stage-5 transcript changes together: the n = 2 schedule across refill boundaries, the select chain, and the BLAKE3 squeeze with its reversed-digest re-absorb. Adapted from the prosecution's probe, which passed on this tree. With two controls, because one oracle proves nothing on its own: the keccak arm of the identical harness reproduces the keccak host (also the statement that threading the wrap hash through `TranscriptReplay` did not move the default), and the two configurations must publish DIFFERENT values on this script. The select chain's RULE is pinned separately against the host's `candidate_under_fixed_schedule` at all four two-candidate patterns including both-miss, which the oracle cannot reach (≈ 2⁻⁶⁴). Its doc says outright that it pins the spec the emitter follows, not the instructions it emits — the oracle is what covers the second, and neither subsumes the other. **rev-emit E2: `FRAMING_LENS` stopped at 256**, which left the construction's most consequential seam untested by any digest comparison — at 1024 this chain is still standard BLAKE3 and past it the construction knowingly leaves the standard. Now 19 lengths through 2048, bracketing that seam from both sides (1023/1024/1025, 1087/1088) and an interior multiple (511/512/513). The prosecutor ran 32 extended lengths and all matched, so this closes a gap that was empty rather than fixing a defect.
Three additions, all closing gaps the adversarial review named. **The flip inventory** (rev-emit E3). Every registered program now has a stated fate at the Stage-6 flip — inert, must-flip, or deliberately pinned keccak — and the classification is MEASURED by counting emitted hash instructions rather than asserted by reading: TrivialV0 0, FriToyV0 0, KeccakChainV0 2, KeccakSpongeV0 2, TranscriptReplayV0 6, StatementReplayV0 5. So the production surface the flip moves is exactly the transcript and statement replays. The test fails if a registered program is added without a fate, which is the half of the checklist that can go stale silently; the site list and procedure are in PA-PLAN 6.0. **The reversed-digest send, PROVED** (review's next-attack). It was reached by the executor and by nothing on the AIR side: the value test only executes, and the prove-and-verify test goes through `blake3_256`, which leaves the two extra sends at multiplicity zero. That left the flipped-coefficient `Linear` — the one piece of column arithmetic transcribed from `chips::keccak` onto a different chip's OUT block — unexercised by any proof. Now proved and verified at three lengths, with an assertion that the multiplicities really are nonzero so the inert send cannot masquerade as the tested one. **R-8: both BLAKE3 surfaces in one machine.** The socket and the chip run the same `run_flow` under different `FlowConfig`s and feed lookups into the same 2^20-row BITWISE table, which is the shape where two producers could balance that table between each other rather than each against it — leaving one computation unconstrained with the bus still balanced. Each surface alone and the two together prove and verify, with row-count assertions so the three programs really do differ in which surface they carry.
… widths Both sit in places whose whole hazard is the thing they got wrong. `airs.rs`'s census loop said "chip classes 0..=10" after `LFM_BLAKE3` took slot 11 — in the one function whose correctness IS index arithmetic, mapping `per_chip` array slots onto `LFM_CHIP_NAMES` across the `KECCAK_RND` splice, where nothing about a height or a width can see the mapping being off by one. `blake3_chip::cols` gave its trailing column literals at one round count without saying which. Everything from `OUT` on is a function of `NUM_G = 8 x BLAKE3_ROUNDS`, so each is now given at both counts, with a pointer to the test that pins the preprocessed prefix — what the registry actually commits — as moving with neither. The Stage-6 flip checklist the review asked for went into PA-PLAN section 6.0, which is not in this diff: `thoughts/` is gitignored and therefore per-worktree.
`f8333e28` says the Stage-6 flip checklist "is not in this diff: `thoughts/` is gitignored and therefore per-worktree". Both halves are wrong and the commit it describes contains the file, so the record needs correcting rather than leaving. `thoughts/shared/block-compression/PA-PLAN.md` is TRACKED — it was committed at `bb30f1c1`, and .gitignore does not apply to already-tracked files. What happened is that an earlier `git add -A thoughts prover/src` exited non-zero on the untracked ignored paths under `thoughts/` while still staging the tracked, modified PA-PLAN; the compound short-circuited, so the staged file was picked up by the next commit instead. `f8333e28` therefore carries all 81 lines of section 6.0, correctly, with a note claiming it does not. Verified while checking: the copy this branch edited is the canonical one. The `lambda_vm-blake3-impl` worktree's PA-PLAN is byte-identical to `bb30f1c1`'s, so the section propagates on merge and no other worktree needs touching. The 900-line copy in the `lambda_vm` worktree is `main`'s and is three days stale. Empty commit: nothing to change but the record.
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.