feat(prover): LFM — field-native recursion machine, epoch-verifier e2e, and the measured hash matrix - #915
Draft
MauroToscano wants to merge 115 commits into
Draft
feat(prover): LFM — field-native recursion machine, epoch-verifier e2e, and the measured hash matrix#915MauroToscano wants to merge 115 commits into
MauroToscano wants to merge 115 commits into
Conversation
The Lambda Field Machine (LFM): a fixed, straight-line, field-native machine for verifying our STARK proofs. The program is the machine's preprocessed columns — addresses, opcode selectors and multiplicities are committed program data, the main trace carries values only — and memory is write-once, closed by pure LogUp balance with no timestamps and no ordering lookups. No pc, no branches, no fetch/decode. Fourteen chips, frozen order: CONST, BALU, XALU (Fp3), SELECT, BITDEC, HASH, KECCAK, LANES, HINT, PUBLIC, RANGE, then the production KECCAK_RND / KECCAK_RC / BITWISE AIRs hosted unchanged. Three new buses (LfmMem/LfmRange/LfmPublic, ids 32-34) are the only prover-side additions; no VM table is touched and VmAirs is untouched, so this is a sibling AIR set proved by the same multi_prove/multi_verify_views machinery. Program identity is a digest over the instruction column groups plus the static roots and heights, pinned in LFM_REGISTRY (regenerated by compute_lfm_registry, drift-tested). Resolution fails hard on a miss; there is no runtime off-switch, by design — the registry check is the first premise of the soundness argument in prover/src/lfm/SOUNDNESS.md, which the release-mode admission validator discharges (uniqueness, acyclicity, multiplicity equality, one-hot selectors, padding, arena discipline, keccak tag uniqueness). What the machine can prove today, all end to end and verified through the registry: a trivial program over every chip; a structurally real FRI commitment-opening proof (sponge transcript, Merkle-authenticated openings, unnormalized folds, terminal check); real keccak-f[1600] permutations through the unchanged production AIRs; keccak256 over byte streams, bit-exact against PlatformKeccak256 at eight boundary lengths; and a scripted DefaultTranscript interleaving whose every sampled value matches the real transcript, including buffer refill, absorb invalidation and a raw squeeze. Two soundness holes were found by adversarial construction and are now pinned by permanent guard tests: without preprocessed per-permutation tags a prover can swap two permutations' outputs while every bus still balances, and once the keccak adapter's absorb mode splits PERM_IN from STATE, permute rows need an explicit pass-through constraint or the permutation input is free. Both tests build coherent forgeries — every bus balanced, every claimed value consistent — and confirm that neutralising the single constraint accepts them. The transcript replay is zero-rejection: a straight-line program cannot follow the production sampler's data-dependent rejection loop, so it encodes the no-rejection schedule and is unprovable for a transcript that rejects. That costs completeness only, bounded below 1e-6 per proof at production draw counts (SOUNDNESS.md 6.3).
Two absorb primitives the statement leg needs, both bit-exact against the real DefaultTranscript. append_felt / append_ext render a field element the way append_field_element streams it: the canonical u64 big-endian, and for the cubic extension the three coordinates in order 0, 1, 2. The endianness flip is real work here — with v = hi·2^32 + lo the halves are byteswap32(hi), byteswap32(lo) — so it goes through the canonical bit decomposition with the byte permutation folded into the constant weights, which are the powers 2^0..2^31 interned once and shared by both halves. One BitDec and 64 BALU rows per element. Coordinate order was read from the source rather than assumed: the same file also implements 2, 1, 0, but that impl belongs to the raw [FpE; 3] array type, not to FieldElement<Degree3GoldilocksExtensionField>, whose write_bytes_be — the one stream_bytes calls — writes 0, 1, 2. The splice replaces the segment packer with a byte-granular one. A machine half still drops straight in when the cursor is 4-byte aligned, emitting no instructions, so every aligned program's digest is unchanged (all registry drift tests confirm). When the cursor is misaligned the half straddles two output halves and is split byte-wise: a bit decomposition, two weighted sums over disjoint ranges, and a recomposition assert that pins the input below 2^32 — bit_dec alone bounds it only by p, and a half at or above 2^32 has no four-byte rendering. About one BitDec and 34 BALU rows per spliced half, and only ever on the statement leg. This is deliberately not the single-prefix helper the plan called for. The continuation-epoch statement alternates constant and dynamic runs, and its one-byte fri_final_poly_log_degree field moves every later value from shift 2 to shift 3, so a helper taking one constant prefix and one dynamic run cannot express it. The packer tracks the cursor instead and splices wherever it must; a test pins the alternating shape, and latching the shift instead of tracking it fails that test alone.
The first leg of a real verifier the machine runs end to end: everything a multi_verify does to its transcript before the per-table forks. absorb_epoch_statement emits absorb_statement(ContinuationEpoch) byte for byte — domain tag, ELF digest, length-prefixed public output, the fourteen TableCounts, the private-input page count, the FRI terminal degree, the runtime page ranges and the trailing epoch label. replay_phase_a then absorbs each sub-proof's preprocessed commitment (only when the air has one) and its main trace root, and samples the shared LogUp challenges z and alpha. Every multi-byte field in this encoding is little-endian, unlike append_field_element's big-endian rendering, so a u64 carried as [low32, high32] halves needs no byte manipulation — the only cost is misalignment. The domain tag is 30 bytes and the fri_final_poly_log_degree field is one, so the statement runs 207 + public_output_len + 16*page_ranges bytes, which is always three past a half boundary. Every Phase-A root absorb is therefore spliced, at one BitDec and about 34 BALU rows per half; a single pad byte in the statement encoding would make all of it free, which is worth considering whenever that encoding is next versioned. Shape-static fields are program constants rather than arena reads, because they determine the shape: the table counts and page-range list fix how many sub-proofs Phase A absorbs, and num_private_input_pages fixes the AIR layout. A program reading them from an arena would claim to verify a shape it was not compiled for. Only the ELF digest, public output and epoch label are per-proof. The acceptance test's oracle is the production absorb_statement_with_digest itself, not a reimplementation — that encoding has ten fields and is exactly where a replay would go wrong. Phase A is a four-line transcription of replay_transcript_phase_a_view, since calling it would mean synthesising AIRs and proof views for three fake tables and would test the fakes. The machine's z and alpha match, executed and proved, and both tamper vectors reject. The continuation tag is now pub(crate) so the replay emits the identical literal; a second copy would drift silently on a version bump, and the tag only works if both sides agree on it.
…ifact Constraints exist today only as compiled code plus a program the AIR hash-conses on demand. A recursion machine that evaluates constraints needs them as DATA, and capture is far too expensive to run in a guest. Add `ConstraintArtifact`: the flat program, the per-constraint metadata capture discards (kind and end_exemptions, i.e. the zerofier shapes), the AIR shape scalars, and the composition degree multiplier. That last one is easy to miss — it lives in neither AirContext nor ConstraintMeta, only inside the ConstraintSet impl and the LogUp layout, yet the verifier needs it to size the composition polynomial. Stored as `composition_poly_degree_bound(n)/n` so it is an observable of the public trait rather than a new trait method. ProofOptions is deliberately excluded: AirContext bundles the options in with the shape scalars, but the captured program does not depend on them, so one artifact per table covers every blowup factor. That premise is pinned by a test rather than assumed. Scope the verify-path prohibition to what it was always about. The rule was "never call constraint_program() at verify time"; the real hazard is CAPTURE, not constraint programs as such. `constraint_program()` still panics by default and may still capture. The new `precaptured_constraint_program()` never captures under any circumstance, so it is safe on a guest path, and `AirWithBuses::with_precaptured()` supplies a build-time program. The two are separate methods rather than one with a flag so an accidental verify-path call to the capturing one still hits the panic. Nothing is wired into the production verify path. Tests: all 25 production tables' artifacts are serialized, read back, and evaluated against the compiled folders on random frames — on the prover shape, the verifier/OOD shape, and the flat device blob. Everything after the codec runs the DESERIALIZED artifact, so a codec bug cannot hide behind the in-memory object. Nonzero end_exemptions and the rejection paths are covered in the stark crate, because no production constraint uses exemptions and a suite where every artifact validates cannot show that validation is able to reject. The 25-table list had been hand-copied into three test suites, so a table added to one and forgotten in the others lost that suite's coverage silently. It is now `test_utils::production_airs` once. Measured: 73,539 nodes / 1,220,256 bytes across the 25 tables; ECDAS, ECSM and KECCAK_RND are 85% of it.
An epoch's public_output is collected one byte per COMMIT operation, so its length carries no alignment guarantee and the aligned-only path was not enough for the target. append_bytes_misaligned takes a byte length, absorbs the whole halves, and masks the trailing one to its live bytes. The mask pins the unused high bytes to zero, which is a soundness obligation rather than tidiness: those bytes are arena data past the encoding's length prefix, so without the pin a prover could put anything there and change the absorbed byte string while the length said otherwise. Dropping the pin makes the machine accept exactly that, which is what the new test catches. Placing a value at the cursor is now one routine for both a whole half and a masked tail, since they differ only in width. The aligned case still emits no instructions, so every existing program's digest is unchanged. Two corrections to earlier analysis, both now machine-checked rather than asserted in prose. The statement is 207 + |public_output| + 16*ranges bytes, not 223. And the shift Phase A inherits is (3 + |public_output|) mod 4, not unconditionally 3 — that claim quietly assumed an output length divisible by four. It is zero whenever the length is 1 mod 4, so the Phase-A splice cost is workload-dependent and vanishes entirely for about one workload in four. The acceptance shape now uses a 14-byte public output so it exercises both new paths at once: an unaligned length, hence a masked trailing half, and a nonzero inherited cursor, hence a spliced Phase A.
KECCAK_RND costs 24 rows per permutation at 1480 columns, so a single instance saturates a 2^19-row table at ~21.8k permutations while a real proof wrap needs ~460k. Split it the way the RV64 VM splits its own tables, with one simplification: the chunk count is static program shape, fixed at compile time, pinned in the registry and bound into the program digest -- never derived at prove time, never read off the proof. Splitting the rows needs no pairing logic because KECCAK_RND has no row-to-row transition constraints: its 24-round chain is carried by Keccak bus tokens rather than row adjacency, so LogUp cannot tell which instance a row lived in. KECCAK_RC and BITWISE stay single shared instances -- their multiplicities are totals over the whole proof. roots and log_heights stay 14-wide chip-class arrays; only the AIR and trace lists expand at slot 11. The digest now absorbs the chunk count, which moves all five program_ids; every root and log_height survived unchanged. Registry regenerated. 105 lfm tests pass (was 92).
Brings KECCAK_RND chunking together with the transcript and statement replay. Both sides had grown since the split, so this is a real merge: the chunking work was written against the machine before the replay legs existed, and the replay legs against a single-instance KECCAK_RND. Two conflicts, both mechanical. machine_tests.rs: each side appended its own tests at the same point, so both blocks are kept. registry.rs: both sides moved the generated program digests, so the block is regenerated rather than resolved by hand — the chunk count now enters the digest, and all six programs re-derive cleanly. Chunking is a saving, not a cost: one table pads once to a power of two for the whole program, N chunks each pad to their own, so at wrap scale (460k permutations) 22 chunks total 11.0M rows against a single table's 16.8M — 34% fewer, and the single table would be unbuildable anyway. The split needs no pairing logic because KECCAK_RND has no row-to-row transition constraints: the 24-round chain is carried by the Keccak bus, so rounds are linked by token matching rather than row adjacency, and LogUp cannot tell which instance a row lived in. Chunk boundaries need not even fall on permutation boundaries, which is pinned positively by a test that re-splits 2+1 as 1+2 and still verifies. 118 tests green, lint clean.
Everything the machine has consumed so far was synthetic or self-generated. This produces an actual continuation proof in exactly the encoding the RV64 recursion guest receives, so the next slice can read production bytes. The encoding is not invented. The guest never sees a ContinuationProof — it gets a blob in private input and reads it zero-copy through rkyv — so a machine-side reader over bytes is the direct analogue of the guest's reader, and a disagreement between the two is a meaningful signal rather than an artifact. Reaching into the in-memory bundle would exercise a path production does not have. The existing dump test produces the same bytes but is #[ignore]d as a diagnostic, driven by five environment variables, and writes to a fixed /tmp path, none of which works from a deterministic unit test. So this reuses its two encoder calls — prove_continuation then encode_continuation_guest_input, both already public — and none of the harness around them. The encoder is the part that must not drift. The epoch size is measured rather than assumed: the fibonacci guest yields one epoch at 2^6, 2^8 and 2^10 cycles and two at 2^4, so it runs somewhere between 17 and 64 cycles and only a 16-cycle epoch splits it. A single-epoch fixture would defeat the point when the target is a continuation. The cache lives outside the repository. A checked-in binary can drift from the encoder without anything noticing, so the generation path is what a cold run exercises.
The three continuation-only AIRs — l2g_global_air, l2g_memory_air and global_memory_air — were private fns in continuation.rs and appeared in none of the per-table IR suites. None of those suites asserted a count, so the blind spot was uniform and silent. It is not a tidiness problem. The proofs the recursion path verifies are continuation proofs, and these three are exactly what such a proof adds. A per-table sweep that stops at 25 is complete for a shape we do not care about. l2g_memory_air carries real constraints; the other two are EmptyConstraints but still need shape, metadata and a degree bound. production_airs() now yields all 28 and every suite asserts its length, which is worth more than the dedup itself: without it the next added table escapes every per-table suite at once, exactly as these three did. Three new tests: - artifacts_are_invariant_across_trace_length. The axis is structurally absent — no AIR constructor takes a trace length — so the only route to the artifact is composition_poly_degree_bound(n), which the artifact stores divided by n. That division is sound only if the bound is exactly linear, so this sweeps n = 2^4..2^24 per table instead of trusting capture's two probe points. - parameterized_airs_vary_per_parameter_value. Four tables fold a workload-dependent value into their IR as a constant: PAGE and GLOBAL_MEMORY a page base, both L2G tables an epoch label. The test characterizes rather than asserts this away, and it corrected my own assumption: the variation is NOT confined to constant values. The builder interns constants, so a value already in the table costs no node while a fresh one appends, shifting later node ids and the constraint ROOTS. L2G_GLOBAL moves 47->48 nodes between epoch labels 1 and 7. "Emit one program and swap a constant" is therefore not an available fix; what is invariant is the algebra, which is what makes the runtime-uniform promotion viable. Proposed in others/lfm-page-base-uniform-proposal.md; no semantics touched here. - global_memory_private_input_is_a_second_shape_not_a_second_program. is_private_input is a second axis but an enumerable one: same program, differing only in the preprocessed-column fields. Also records what the all-zero end_exemptions finding actually buys: production zerofiers are uniform, so the GPU path's uniform-zerofier precondition holds in fact rather than by luck, and a consumer needs one zerofier per AIR rather than one per distinct exemption value. The ExemptConstraints coverage stays so the field cannot rot into being untested. Measured, 28 tables: 73,722 nodes / 1,223,896 bytes. The continuation tables are small — 47, 93 and 43 nodes.
The arena filler's first half: open the guest's wire-format blob, read the archived bundle in place as the recursion guest does, and lay an epoch's main-trace Merkle roots out as arena halves. Reaching the epochs needed an accessor, and the shape of it matters. The archived struct's fields inherit their visibility from the source, so relaxing ContinuationProof::epochs would have opened the owned type at the same time — which is the thing worth avoiding, since the recursion guest never holds an owned bundle. The accessors are therefore methods on ArchivedContinuationProof alone, exposing only the path verify_continuation_archived already traverses. Each root is packed into its own eight halves. An arena is a vector of words, not a byte stream, so concatenating fields and packing afterwards would let any field of non-multiple-of-four length shift everything behind it — silently, since the halves count still comes out right. Measured on the fixture: the intermediate epoch has 24 sub-proofs and an 8-byte public output, the final one 25 and an empty output. That matches the expected per-epoch table count (split-table chunks, plus ten fixed tables on the final epoch and nine elsewhere, plus pages, plus the epoch-local L2G), and it independently confirms the 24-table structural minimum the completeness bound in SOUNDNESS.md quotes. One thing the bytes cannot supply: the preprocessed commitment Phase A absorbs comes from the AIR set rather than the proof, so replaying Phase A against a real proof will need the epoch's AIRs rebuilt, not just its blob. Flagged here rather than discovered later.
… in the blob The completeness bound in SOUNDNESS.md instantiated its worked example at 24 tables and said so as a structural minimum, hedged because nothing had checked it. Reading a real two-epoch continuation proof gives 24 sub-proofs for an intermediate epoch and 25 for the final one, the extra being HALT, so the hedge can go. Also adds the check behind the preprocessed-root question: the guest input carries the DECODE commitment and the per-page genesis commitments as public fields, so replaying Phase A needs no access to the epoch's AIR builder. Worth noting the fixture has no page commitments at all — fibonacci touches no data pages — so that path exists but is not exercised by this test.
Design (α) from lfm-design.md §3 — how a serialized ConstraintArtifact becomes LFM instructions. Design only; no semantics touched. Adds constraint_op_census as the instrument behind it: a per-AIR breakdown of nodes into leaves, pooled constants, foldable subtrees and extension ALU work, so the instruction estimate is measured rather than asserted. Printed with only a loose ceiling, because pinning exact counts would turn every constraint edit into a test failure. Budget holds. 28 AIRs give 64,842 constraint-leg instructions plus 2,150 beta-folds = 66,992, against the design doc's ~69K at 25 — and a MulAdd peephole takes it to 57,923. The correction that matters: the IR's dim tags describe the PROVER, and the machine runs the verifier. At the OOD point the frame is all-extension, so a node is base only when its whole subtree is constants. The IR declares 42,137 base arithmetic nodes; 2,916 are actually base at verify time. Anyone sizing this leg from the declared dims would understate extension traffic by 14x. MulBase eligibility falls from 9,413 to 5,041 for the same reason — and the 2,916 that are genuinely base are constant-only subtrees the emitter folds at build time for zero instructions. Two lowering arms are not the obvious ones. Op::Neg has no instruction — ExtOp is Add|Sub|Mul|Div|MulAdd|MulBase with no unary negate — so it lowers to a subtract from the pooled zero. Op::Embed emits nothing at all: under the [F;4] lane-3-zero word model a base value (v,0,0,0) is already its own extension embedding. Both are measured at zero occurrences in production, along with ConstExt, so all three arms are correctness-only today and should stay. The uniform-zerofier finding is worth ~50,900 instructions: with every constraint sharing Z = zeta^N - 1, the division factors out of the beta sum and is evaluated once per AIR instead of once per constraint. Two scaling caveats recorded rather than buried. The total is per distinct AIR, not per epoch — each sub-proof needs its own evaluation and chunking gives a family several, which is the one place the design doc's figure reads optimistically. And the leg is workload-shaped: ECDAS, ECSM and KECCAK_RND are 86.9% of it, so an epoch with no elliptic-curve work drops 65%. Nothing in the IR is structurally inexpressible on a straight-line machine. The stronger statement: the IR's own invariant that nodes[i] references only nodes < i is identical to the machine's acyclicity premise, so dense address assignment in node order satisfies it by construction.
The ISA inventory landed four facts that move the estimate, so the design and the census are updated to match rather than left to be reconciled by a reader. MulAdd costs the same single row as Mul. That makes fusion mandatory, not an optimization: emitting Mul then Add where one instruction would do is pure waste, and the node count is an upper bound rather than an estimate until it is applied. 9,069 fusable pairs take the leg from 66,652 to 57,583 — so against the design doc's ~69K, which implicitly assumed roughly 1:1 with nodes, the real figure lands 16.5% under. Constants are interned program-wide, keyed on the canonical 4-lane word, so summing per-AIR pools overcounts: 655 becomes 315 actual Const rows. More than half the apparent constant cost was the same small structural values duplicated across tables. MulBase is reframed. It costs the same row as Mul, so it is not a reduction — it is a routing obligation, since lowering an ext-by-base multiply by hand costs 4+ rows. 5,041 sites, and the count would be 9,413 and wrong if taken from the prover-side dims. Base-to-extension conversion is free, which confirms independently that Op::Embed emits nothing. The converse costs a LANES row, but this leg never needs it: nothing in the IR narrows an extension value, since Dim only ever widens through binop's join. The doc now also separates what I verified myself — the op inventory, Neg having no ISA counterpart, Embed and ConstExt being unused, the absence of narrowing, and every count — from what I took from the inventory on report, so a wrong cost fact invalidates the row conclusions without touching the instruction counts.
Adds epoch_chunk_multiplier, which builds real traces so the chunk counts are the prover's own splitting rather than a reconstruction of it, and weights them by each AIR's constraint-leg instruction count. Measured: 64,712 instructions at 1M cycles, 65,996 at 2M, 95,532 at 20M — a 1.01-1.49x multiplier over the per-distinct-AIR figure. Small, and for a structural reason: chunking multiplies the cheap AIRs (CPU is 489 instructions, MEMW_R 153) while the expensive ones are never chunked at all. So lfm-design.md §5.2's ~69K was closer to right than my earlier warning implied; the correction is a growth term in epoch size, not a multiplier on the whole figure. CORRECTION to my own claim. The design doc previously said the leg was workload-shaped — that ECDAS, ECSM and KECCAK_RND being 87% of the total meant an epoch without elliptic-curve work would drop 65%. That is false. FIXED_TABLE_COUNT is documented as tables that always contribute exactly one sub-proof regardless of TableCounts, and ecsm and ecdas are on that list: a zero-row table still needs its sub-proof, since dropping it would remove its constraints from verification. The fib fixtures use neither elliptic-curve nor keccak work and still carry the full 60,389-instruction fixed block. The leg is essentially workload-INDEPENDENT. I asserted the reverse from the census alone, and the census cannot see how sub-proofs are assembled. The uniform proposal is revised against the gate ruling. The gate cleared, but my premise was wrong in my own favour: I argued the promotion was safe because page_base is already bound by the preprocessed commitment, and it is bound by nothing — not the commitment, not the transcript, and program_id only for ELF-backed data pages. The conclusion survives and is stronger, but the reason was backwards, so the invariant is now stated as load-bearing rather than as a note: the uniform must be populated from the same verifier-side sources as today and never from the proof or trace, precisely because nothing downstream would catch it if it were. Also retargeted: continuation epochs pass page_configs = &[], so create_page_air is never called there and GLOBAL_MEMORY is the AIR on the critical path. And epoch_label is not symmetric with page_base — it comes from the verifier's own enumerate() position, so there is no supply route to get wrong; recommending they move together as equal risk was wrong. Per the ruling, the hash-consing-versus-fusion trap now lives as a comment on ConstraintArtifact rather than only in the design doc.
…ed shape The monolithic multiplier was the wrong shape for the target. A continuation epoch passes page_configs = &[], so PAGE never appears, and it carries an L2G_MEMORY sub-proof instead; intermediate epochs also drop HALT. Computed: 63,393 instructions over 24 sub-proofs for an intermediate epoch, 64,094 over 25 for a final one — 14 split families at their minimum one chunk each (3,640), nine fixed tables (59,688), one L2G_MEMORY (65). The 24/25 sub-proof count was measured independently on the LFM fibonacci epoch fixture, so the test asserts this composition reproduces it. That turns the epoch shape from something the design doc infers into something a test pins: if the composition changes, the arithmetic stops matching and this fails rather than the doc quietly going stale. 94% of the epoch leg is the fixed block, which is the sharpest form of the workload-independence correction — the leg is ~63K regardless of what the workload computes, growing only with epoch size as the cheap AIRs chunk. Also records the global proof's contribution: 27 instructions per epoch for L2G_GLOBAL plus 25 per touched page for GLOBAL_MEMORY. That is what settles the page-base question as an identity problem rather than a size one — even a four-figure page count is noise against a 63K leg. What remains inferred is narrower than before: only the chunk growth curve for a large continuation epoch, which is still derived from monolithic runs.
Closes the last inference in the epoch numbers. The previous §8.2 figures came from monolithic runs, which cover a whole execution rather than one epoch's 2^epoch_size_log2 cycles and carry a different table set. continuation_epoch_chunk_counts_measured drives the actual continuation path — Executor::resume_with_limit for one epoch, then Traces::from_image_and_logs. Proving is deliberately skipped: epoch 0's register_init comes from the entry point rather than a previous epoch, and every intermediate epoch runs exactly epoch_size cycles by construction, so epoch 0 is representative and the register chaining that would need proving has no bearing on table sizes. At 2^20 cycles an epoch has 16 chunked sub-proofs (CPU and MEMW_R each split in two), 26 in total, for 64,035 instructions — against the 24-sub-proof, 63,393-instruction minimum at 2^19 or below. Doubling the epoch past CPU's chunk bound costs 642 instructions, and that is the whole growth term, so the leg is 63-65K across any plausible epoch size. The monolithic 1.49x at 20M cycles was an over-estimate for an epoch, which is capped by construction. Two things fell out of running it that are worth more than the numbers. fib_iterative_2M and array_multipass_20M produce identical chunk counts for their first 2^20 cycles — workload independence visible directly rather than argued from FIXED_TABLE_COUNT. And the test asserts page_configs is empty, so "a continuation epoch never builds PAGE" is now pinned by a run instead of read off a comment. The design doc also now states the consequence that was buried in an erratum: a leg that is 94% fixed means the emitted program barely varies with workload, so the registry's profile ladder is one-dimensional in epoch size rather than a cross-product of workload classes and shapes. And the census's own doc comment now records what that instrument cannot see — how sub-proofs are assembled — naming the false claim it produced, since the next reader will reach for the per-AIR table the same way.
…l path Follows from the epoch composition already measured, and I had not taken the step. An epoch proof is 14 split families plus 9 or 10 fixed tables plus one L2G_MEMORY: no PAGE, since page_configs is empty, and no GLOBAL_MEMORY, which lives in the global proof. So the only parameterized AIR in an epoch proof is L2G_MEMORY, whose parameter is epoch_label. epoch_label is index + 1, so unpromoted the registry needs one distinct program per epoch index and the ladder grows linearly with epoch count — exactly the workload-dependence a 94%-fixed constraint leg was just shown not to have. page_base reaches the machine only through GLOBAL_MEMORY, which is the global-proof leg and a later concern. Records the epoch_label threat model, which is sharper than the page case rather than softer. epoch_label pins an epoch's POSITION in the chain: it is the constant in the IsB20 cross-epoch ordering check, and the fini_epoch the next epoch's token consumes. Today the verifier builds that AIR from its own enumerate() index, so a prover cannot assert a different position. If the uniform were ever sourced from the bundle, inflating the label would relax the ordering range check, and free choice of labels would permit two epochs to claim one position (replay) or to claim positions out of order (reorder). page_base risks a wrong address; this risks the integrity of the chain itself. The invariant is therefore the same shape as the page one for a different reason, and it is easier to honour — the value is a loop counter the verifier already computes, so no plausible implementation reads it from the proof unless someone deliberately adds a route. It is written down so that nobody does. Acceptance is three criteria, and the second is the real one: the existing epoch-ordering rejection tests, which pop and swap epochs in a proved bundle, must pass unchanged. A promotion that required editing them is a promotion that broke something.
R1f (c)+(d). The machine now walks one FRI query's main-trace opening from a real two-epoch continuation proof to that proof's own committed root, proved and verified. This is the first time it touches production-committed data. The walk could not reuse edsl::merkle_walk: that one compresses with LFM_HASH/TestPermutation, the non-cryptographic Milestone-C placeholder, so it can only authenticate the Milestone-C fixture tree. Production trees are keccak throughout, so edsl::keccak_merkle_walk is new, built on the bit-exact keccak256 emitter and the big-endian element rendering. Conventions read from source and re-verified: a leaf is the ROW PAIR 2i, 2i+1 written column by column with every element big-endian, and a parent is keccak(left || right) — 64 bytes, no domain separation, no ordering flag, so one permutation per level and the ordering carried entirely by the index bit. The leaf index is not in the proof: it is the FRI query challenge, and deriving it needs the epoch's statement and AIR set, neither of which a byte blob carries. It is recovered by exhaustion against production's own path checker, which asks the proof rather than inventing an answer. The opening this leg authenticates is the only one of the fixture's 49 sub-proofs that combines a deep tree with a unique index — most tables are mostly padding, so identical rows give identical leaves and every index verifies, which would make the index-tamper vector vacuous. A test pins that property. Tamper runs both ways round. Incoherent (change an input, still claim the real root) fails the in-machine root assert. Coherent (also claim the root the tampered inputs really fold to) proves cleanly and then fails on the one thing it cannot fake: the published root is not the committed one. MEASURED, and it refutes the prediction the leg was set up to confirm. The handoff expected byteswapping to dominate the leaf, reading row counts: 20 BITDEC + 1280 BALU rows against 22 permutations. The rows are right and the conclusion is not, because rows of different chips are not comparable — an LFM_BALU row is 4 non-preprocessed columns while a permutation expands into 24 KECCAK_RND rounds of 1480. In main-trace cells one permutation costs 113 byteswaps, and hashing dominates at every width in the fixture: 124x at the 10-column table, 8.9x at 511, 7.4x at 1480, flattening near 6.6x rather than inverting. A byteswap chiplet is not the lever it looked like.
Planning the implementation surfaced a better design than the proposal specified, so it is captured before any code rather than made unilaterally in it. The first sketch threaded a uniform slice through every evaluation entry point — eval_program, eval_program_verifier, eval_device_program and the shared interp helper — which is substantial churn across both walkers, the CUDA host side and every caller, for a value that behaves exactly like a constant at evaluation time. Instead the uniforms resolve into the program struct alongside the constants: ConstraintProgram and DeviceProgram each gain a base_uniforms table that OP_BASE_UNIFORM indexes exactly as OP_CONST_BASE indexes base_consts, while the artifact stores only the count. No evaluation signature changes at all; the CUDA kernel gains a buffer uploaded the same way base_consts already is rather than a new host parameter; and the AIR fills the table at construction from its own verifier-derived value, which is where that value naturally lives. The refinement creates a hazard worth stating rather than discovering: ConstraintProgram becomes a hybrid of program identity and per-instance values. Anything that hashed one including its uniforms would reintroduce the per-epoch digest this whole change exists to remove. It is latent today, since only the artifact is hashed and it carries the count alone, but it belongs in review either way. Also makes program() error when uniforms are required rather than defaulting them to zero, so a forgotten supply is loud. Implementation is deliberately not started. A multi-file semantics-adjacent change half-built is worse than one not begun, and this design decision wants agreement before it lands. The handoff records state, what to read first, the falsifications that are not optional, the instruments left behind, and the things a successor would otherwise rediscover.
…lying on it Recovering the same opening twice across runs gave two different leaf indices, which should not happen if proving is a function of its inputs. It is not: two generate() calls on identical inputs — same ELF, same empty input, same epoch size, same options — differ in ~65k of 587k bytes, and the difference reaches the committed data rather than being rkyv padding. Some sub-proofs commit to different roots, that moves the Fiat-Shamir challenges, and different leaves get opened. The tree SHAPE (column counts, depths) is stable across runs; the values in it are not. Two consequences, both handled here. Nothing derived from a specific blob may be pinned as a constant. R1f already works this way — it pins shape and recovers the leaf index from whatever blob it is handed — but that was a judgement call at the time and is now a rule with evidence behind it, recorded on load_or_generate. A pinned index would have passed for exactly as long as the cache file survived, then failed on the next cold run. The cache write is now atomic. The test that regenerates the fixture runs in parallel with tests that read the same path, so a non-atomic write can hand a reader a truncated blob; since blobs legitimately differ run to run, "it worked last time" was never evidence that the race was safe. fixture_generation_is_not_reproducible carries the measurement. It is #[ignore]d because it costs two continuation proofs, and it asserts the divergence is semantic — so if the prover is ever made reproducible, it fails and says which rule can be relaxed.
A partial-tracking accident nearly cost a method rule. Two of these files were swept into a commit on a side branch, then merged back as stale copies: the committed standing-decisions had four method rules where the live one had six, so a fresh checkout would have silently dropped "a deferral's safety argument is itself a claim needing evidence" and "mark provenance; never assert past your evidence" — from the file every agent reads before deciding whether to stop and ask. The fix is to stop having some of them tracked and some not. All of them are versioned now, at their current content: - standing-decisions: pre-authorizations, the stop-and-ask list, and the six method rules, each of which exists because it caught something. - target-shape: what we actually verify (continuation epochs, 28 AIRs), the shape-static principle, and that alignment is a property of the cursor rather than of the field. - migration-riders: changes that are near-free if they ride the hash migration and not worth a proof-breaking change alone. - the team-lead rulings and the agent handoffs, which record why several designs are shaped the way they are rather than the obvious way. - the status log, now carrying both tracks' entries in one timeline. These are working documents, not polished design notes. They are worth keeping because the reasoning in them is expensive to reconstruct: most entries exist because an assumption turned out to be wrong.
The inline values on `chips::keccak::cols` (52 / 252 / 388 / 588 / 788) drifted when R1d widened `PREP_WIDTH` for the reversed-digest columns. The constants were always right — they are derived — but the comments were four low, and reading them instead of evaluating the constants is exactly what produced a wrong per-permutation figure on the first pass through the R1f cost measurement. Real values: 56 / 256 / 392 / 592 / 792. A comment cannot be tested, so the widths the cost model actually depends on get an assertion instead: LFM_KECCAK 792 total and 56 preprocessed, LFM_BALU 4 and LFM_BITDEC 66 non-preprocessed, KECCAK_RND 1480, and the two derived figures — 322 main cells per byteswap, 36,256 per permutation. A wrong width rescales every number in keccak_merkle_opening_cost silently, which is the failure this pins.
The note explaining why R1f authenticates epoch 0's table 0 said it was the only one of the 49 sub-proofs combining a deep tree with a unique leaf index, and my status log put the degenerate count at 47 of 49. Both came from eyeballing a probe rather than counting. Measured: 24 sub-proofs have exactly one verifying index and 25 have several. The real reason the target is right is depth, not uniqueness. It is one of two depth-20 trees; nothing else exceeds 7 and half the sub-proofs are depth 2. Depth is shape, so it survives the blob changing, which the unique/degenerate split does not — that split is therefore described as blob-dependent and left to the run-time assertion that was already there, rather than written down as a fact about the fixture.
Adds the constraint-evaluation leg of the epoch verifier: a host-side pass that turns one AIR's captured transition constraints into straight-line machine instructions, plus the differential that pins it. The pass constant-folds verify-time-base subtrees, eliminates nodes no root reaches, routes ext-by-base products through MulBase, aliases Embed to zero rows, lowers Neg as a subtract from the pooled zero, and fuses Mul/Add pairs into MulAdd under a single-consumer guard (the IR is hash-consed, so fusing a shared product would recompute it per consumer). Acceptance: for all 28 production AIRs, over random all-extension OOD frames with the verifier's next-row pruning applied, the machine's constraint values equal eval_program_verifier run on the deserialized artifact. The cost census reproduces the design's per-AIR table exactly at 64,187 unfused rows; fusion brings the emitted total to 55,147.
Completes the constraint-evaluation leg. emit_quotient computes the shared zerofier by repeated squaring, folds the constraint values against the powers of beta, divides once per AIR rather than once per constraint, and Horners the composition parts the proof claims. Boundary terms are pre-scaled by the zerofier so they keep their own beta powers inside the same fold while still sharing that single division. Both denominators are inverted against the interned one rather than divided directly: the machine reads 0/0 as 1, so a direct divide would silently accept a vanishing zerofier, whereas 1/0 has no satisfying assignment. Checked against a real STARK proof of L2G_MEMORY, with the challenges replayed through the production verifier's own rounds and the out-of-domain grid reconstructed by its own layout, so the oracle is the prover and verifier together rather than a transcription of one formula. Six tamper vectors reject, and the program proves and verifies against its own committed artifacts. Measured: an intermediate continuation epoch's leg is 54,358 instructions plus 2,894 of recombination over 24 sub-proofs, against a 63,393 budget.
…esign Three corrections, all measured by standing tests: MulBase is cost-neutral rather than a 4x routing obligation, fusion saves 9,040 rather than 9,069, and the three dead nodes cost no rows while a separate 2,376 unreachable constants must not be added to the fold column twice. The design's per-AIR table and its 63,393 per-epoch budget both reproduce exactly; the emitter lands 9.7% under with the recombination included.
# Conflicts: # others/lfm-agent-status.log
R1g obligation (ii). The machine ties each epoch's own committed L2G root to the corresponding sub-proof of the global proof — `verify_l2g_commitment_ binding_view` (`lib.rs:993`), emitted and proved against the real fixture. This is the first time the machine reads ACROSS structures; R1f stayed inside one epoch's own sub-proof. Two accessors on the ARCHIVED bundle only, as methods rather than relaxed fields, since rkyv mirrors field visibility onto the archived struct and opening `epochs` would open the owned type at the same time: `epoch_l2g_root` and `global_proof`. Verified on the real bundle first — 2 epochs, 4 global sub-proofs, epoch i's root equals global sub-proof i's main root for both. The epoch count is program shape, so production's `final_proof.len() >= epoch_l2g_roots.len()` guard has no counterpart: a program compiled for n epochs cannot read an n+1-epoch bundle, the arena schema would not match. Tamper covers position sensitivity, which is the point of the check — a bundle whose L2G roots are right as a SET but wrong in ORDER must reject. That vector is only meaningful because the per-epoch roots are pairwise distinct on real data, so a test asserts that rather than assuming it; F35 confirms the assertion fires when the roots are made to coincide. F32 found a real hole in the first version of these vectors. A digest spans two machine words and needs an assert on each, but every tamper byte was in byte 0, so deleting the second assert left all five tests passing. The vectors now straddle both words (byte 0 and byte 31) and F32 fails as it should.
The epoch verifier now runs constraint evaluation, the quotient check, the opening authentication, the DEEP fold and the FRI walk on the cells the Fiat-Shamir spine bound, over a real 24-sub-proof continuation epoch that production accepts. Every check is an in-program assert, so execution is the verdict; the 111 published challenges are still differentialled against production's own replay. New prover/src/lfm/epoch_verify.rs is the seam emitter. epoch_challenge_program becomes epoch_program(e, with_legs) so one spine emitter serves both programs and the leg program cannot drift from the one the challenge differential covers. programs::emit_register_commitment extracts reg-tree's derivation from its isolation program so the spine can call it on cells it already holds. Measured at the min preset over 24 sub-proofs: spine 1,095,553 instructions / 1,211 permutations / 5,716 arena words; assembled 2,184,360 / 2,616 / 16,478. The leg permutation count matches a closed form over the shapes exactly (927 leaves + 304 Merkle levels + 174 FRI = 1,405), the constraint lowering reproduces the design's 54,358 ALU rows to the digit, and FRI at blowup 8 lands on the pinned 14,454. Discharges assembly ledger entry 3 and corrects entry 7: DECODE's preprocessed commitment is ELF-dependent, not a compile-time constant.
… leg wiring Falsification found a hole in the wave-5 coverage: deleting the quotient check's assert_eq_ext failed nothing, and no arena tamper can catch it because every input to the identity is transcript-absorbed, so moving one moves the challenges and the run dies at the Merkle walk instead. Closed with an absolute count — assert_eq_ext lowers to a division by the interned zero, which nothing else emits — against a closed form over the shapes: one check per sub-proof plus one FRI terminal check per query when the codeword folds and two when it does not. 24 + 47 = 71, measured 71, both branches exercised. Also records the ledger's new entries: 3 discharged, 7's taxonomy corrected, 9 (the constraint leg's frame-step view of the OOD grid is invisible at step_size = 1, demonstrated) and 10 (per-epoch numbers must name their epoch shape).
… attestation join)
…DE to the attestation Closes assembly ledger entries 7 and 2. Each preprocessed commitment now comes from the source its provenance admits, and which source that is comes from a classifier that recomputes production's candidate functions rather than from a sub-proof index: - options-only (BITWISE, KECCAK_RC, PAGE zero-init) intern as program text and absorb as literal bytes; - REGISTER is COMPUTED in Phase A from the register-boundary arena the spine already declares plus a new reg_fini arena, which is what binds start_index — it is now the same cell the derivation consumed, not a second read of it; - DECODE stays an arena cell and is bound by the attestation join: the same cell Phase A absorbs is the cell the program_id fold consumes. The join is denied structurally by two absolute guards, hinted-once for a second read and an exact arena schema for a second word, and falsified with a coherent forgery: a control program with the cell split runs the substitution and attests to another program's id, which the joined program cannot express. Reading the production side also amends the ruling's PAGE premise. No continuation epoch of any guest carries a PAGE sub-proof -- prove_epoch rejects one and both build_epoch_airs call sites pass no page configs -- so the epoch taxonomy is 2 constants + 1 derived + 1 ELF-dependent, and the ELF-data page roots the attestation folds belong to the global proof's GlobalMemory AIRs.
Closes assembly ledger entries 8 and 9, with two fixtures instead of the one the plan called for. The plan wanted a single AIR with three transition offsets and step_size > 1; neither half is available: - AirWithBuses hardcodes transition_offsets [0, 1], so three offsets means an AIR impl, and every one outside crypto/**'s example tree is in that tree; - step_size > 1 is not provable at all. The CPU transition evaluator borrows one row per offset and asserts the single-row shape, so the prover rejects any such AIR. Recorded as a should_panic test on that assert's own message, so the ceiling is self-updating. Entry 8 needs no synthetic AIR: FibonacciMultiColumnAIR already has three offsets and is generic over the extension, so at three columns its next-row OOD block is 3 columns by 2 rows -- the first block in this phase where a column-major and a row-major absorb differ. The proof is production's and so is the challenge oracle. Entry 9 needs no proof: the defect is the machine's grid-to-frame-step mapping, and production has a pure function for exactly that mapping, so frame_step_view is differentialled against into_frame at step sizes 1, 2 and 4. The rule is extracted out of emit_table_verification for that purpose. Both denied defects were injected and watched fail. The row-major absorb leaves every pre-existing test green, which is entry 8's claim demonstrated rather than argued.
…ledger Ledger entry 1 said to emit the range check if the "no >u32 register column" argument was still unverified when assembly arrived. It is, and wiring the REGISTER derivation is what made the boundary vectors live arena data, so epoch::assert_u32 now runs on all 134 cells. It sits at the assembly call site rather than inside emit_register_commitment: the isolated derivation's hazard guard is right that an isolated derivation binds nothing. The obvious test for this is vacuous and was written first -- a wide value moves the derived root, so the epoch fails with the check removed too. What replaces it is the check in isolation plus a structural guard that every register-arena hint feeds a 32-bit decomposition, which is what catches a check applied to a prefix. Writing that test also pinned the size of the gap: an arena word is a field element, so FE::from(u64::MAX - 1) is the felt 2^32 - 3, a valid u32. The widening is the interval [2^32, p) and nothing beyond. Ledger and RESUME updated: entries 1, 2, 7, 8 and 9 discharged with their evidence, leaving only entry 10, which is the wrap run's reporting rule rather than a debt. Two items are surfaced for the user instead of worked around: the step_size > 1 framework ceiling in crypto/**, and the fact that the entry-7 ruling's PAGE witness epoch cannot exist because page roots belong to the global proof.
…es to global scope
Splits airs::lfm_cell_counts into a per-chip census plus a summing wrapper so a census and a total are the same arithmetic, and adds the wrap run's harness: prove+verify of the assembled epoch verifier, the chip census, and the census' own falsification against the traces the prover builds and the AIRs the verifier builds.
…ce it The machine now proves and verifies its own epoch verifier. Adds the blowup axis to the epoch fixture (real_epoch_with), a wrap run that is one call per inner-proof option set, the production-shaped census at blowup 8 with 73 queries, and the hash share the whole measurement is for: 84.0% of the cells per verify are the keccak family. Closes assembly ledger entry 10 with the table of numbers, each naming its epoch's trace-length profile.
The spine/legs split now prints per run and reproduces wave 6's six numbers exactly. It also shows the spine grows with the query count, so per-query cost is taken from the difference: 1,581.0 permutations per query at one query and at seventy-three, measured at both ends rather than assumed linear. Adds the recursion ratio (machine cells against the verified epoch's own trace cells) with the warning it needs: the denominator is a sixteen-cycle epoch, so the ratio is not a machine constant.
… rate penalty Slice 0 of wave 8 is a scoping report, not a build. Three things it establishes that change how the matrix should be built: - The machine already has a hash swap surface (hash.rs, LfmHasher + LFM_HASH), and it is NOT the socket keccak is hosted in. edsl.rs states the two walks are not interchangeable. A candidate column is that second socket carrying the epoch verifier's real workload for the first time. - 53.5% of keccak's per-permutation cost is aux alone, and essentially all of it is KECCAK_RND's BITWISE lookups. Aux are cubic-extension cells, so they count triple. An algebraic hash has no lookups, so that collapses structurally. - The rate penalty runs the other way: keccak absorbs 17 felts per permutation, the LFM sponge 8, so a candidate pays up to 2.125x more permutations. That is a consequence of the frozen HASH_STATE_FELTS = 12. The census formula is verified from source and reproduces entry 10's measured numbers exactly, which is what lets the predictions be stated as arithmetic. The predicted Poseidon-original column is ~1.9-2.1 billion cells against keccak's measured 11.17 billion, i.e. a projected 58-65 GiB — inside the box. Round counts behind that are my own domain knowledge and are flagged as the report's weakest link.
…g a hash query_permutations was already a closed form over shapes, so a candidate's permutation count needs only arithmetic: substitute the sponge rate. At blowup 8 / 73 queries on the fixture epoch, keccak's rate of 17 felts per permutation gives 115,413 and the LFM_HASH sponge's 8 gives 187,902 — 1.63x, not the 2.125x ceiling, because 41.4% of the bill is path and FRI work that costs one permutation at any rate. The keccak side reproduces the ledger's own legs figure of 115,413 exactly, which is what makes the candidate side worth believing: same function, different rate. The new form is written through felts where the existing one goes through bytes and keccak_host::num_blocks, and neither delegates to the other. That is deliberate: delegation would have made the rate-17 differential vacuous the moment it was introduced. Both asserts were falsified and restored, and they catch different defects — a rate-sensitive path term slips past the differential because blocks_at_rate(8, 17) is 1, and is caught by the decomposition assert. Also corrects the scope report's arithmetic: aux cells scale with rows, so a 30-row layout pays 90 aux cells per permutation rather than 3, which settles the layout choice.
…no parameters Structural search, run after the dispatched inventory leg went silent: - crypto/crypto/src/hash/poseidon/ is a HADES permutation — full/partial/full, which is Poseidon-original's structure and confirms the round shape the scope report's estimate assumed. It has no concrete PermutationParameters anywhere, so it is a generic skeleton rather than a usable hash: what is missing is a parameter set, which is a cryptographic input and not an engineering one. - TreePoseidon and BatchPoseidonTree already implement IsMerkleTreeBackend over field elements. That partly overturns the report's assumption that swapping the inner prover's hash is necessarily invasive, though whether the prover is generic over the backend trait is still unestablished. - sha256 AIR specs exist under spec/src with no generated AIR; they are the nearest in-tree precedent for a bit-oriented hash and worth reading before costing blake. - No blake, RPO, Monolith, Griffin or Anemoi in any spelling. The 26 'monolith' hits in prover/src are all the monolithic-proof concept. Records two search traps: unquoted --include=*.rs fails in the shell in a way that reads exactly like grep finding nothing, and a term-only search would have reported a Monolith hash that does not exist.
…e box The corpus extraction supplies a measured anchor that normalizes onto our socket for free: Miden's BlakeG keeps state 12 / rate 8 / digest 4, which is exactly the frozen LFM_HASH contract, so per-2-to-1 figures transfer and every field-native candidate shares the one permutation count slice A measured. The result reverses my first pass. I had argued blake would not buy the memory relief the wrap needs, reasoning from its bit-oriented mechanism. The premise holds — blake does pay 48x aux — but keccak-like in mechanism is not keccak-like in magnitude: KECCAK_RND is 1,480 columns over 24 rows against BlakeG's 128 over 32, the same mechanism 12x apart. Blake lands at 3.68x better than keccak and about 79 GiB, inside the box, and so does every other candidate. The hash decision is not cost-gated. Also: the naive ranking inverts. RPO is the cheapest predicted column and has no donor AIR anywhere, while buying about 1 GiB of a 49 GiB wrap; Poseidon-original is within 7% of it and has a direct poseidon1-air donor in the vendored Plonky3 tree the corpus never scoped. Since the already-measured residue dominates every algebraic row, choosing among them on predicted wrap size is choosing on noise. Adds the 2-to-1 normalization explicitly: our 118,080 permutations are 47,742 compression-shaped plus 67,671 wide leaf absorbs, so we are 6.2x Airbender rather than 15.4x, and the corpus's divergence argument at 900,000 compressions does not transfer to this machine. Records the two-stage governance shape so stage 1 does not block on a crypto/** authorization, and a corrections ledger for the claims this supersedes — including the falsified one-parameter memory model and my own misattribution of chunking.rs' commit date.
…ector Slice 1a of the Poseidon column: the permutation behind LfmHasher, with parameters whose provenance is citable and an oracle that is not ours. Parameters come from the vendored Plonky3 tree, which documents them as Grain-LFSR generated per the Poseidon paper's Appendix E at t=12, alpha=7, R_F=8, R_P=22 with a circulant MDS. That independently confirms the round shape the scope report had estimated from domain knowledge alone. alpha=7 is forced: p-1 factors as 2^32*3*5*17*257*65537, so neither 3 nor 5 is coprime to it. The brief asked for a differential against the in-tree HADES skeleton. That skeleton hardcodes an x^3 S-box, which is therefore NOT a permutation over Goldilocks, so differentialling against it would have validated this code against a non-permutation. Pinned against Plonky3's own known-answer vector instead, which nothing here produced. A second test encodes the skeleton's bug as a guard by asserting gcd(alpha, p-1) = 1 and that 3 and 5 fail it. The vector was falsified three ways and restored: a wrong exponent, a transposed circulant MDS, and the partial-round S-box on the wrong lane each fail it, so one vector pins all three conventions at once. Ship-grade parameter selection and domain separation stay open cryptographic decisions; compress_iv is zero capacity and says so. Cells depend on round counts and S-box degree rather than on the constants' values, so the measurement this enables is valid regardless. Adds two standing-decisions rules earned this wave: a shell-errored search reads exactly like an empty one, and a donor's parameters are not a donor's correctness.
…ilding it Context ran thin, and the coordination rule says checkpoint rather than hand over a half-built slice. A 612-column constraint set that compiles but is unfalsified would be worth less than this spec, so the spec is the deliverable. It gives the column layout with offsets, all 601 constraints, the argument that the degree is exactly 3 (so the wrap's blowup 2 is unaffected), the padding obligation and why the existing round-constant-times-mode-sum trick already discharges it, the trace generator's association requirement, and a five-part test plan whose last step is prove+verify — because execute-only tests prove nothing about a chip. Two findings worth more than the code would have been. Registration is far smaller than adding a chip: LFM_HASH is already slot-registered, so only the column count, the constraint body and the trace filler move, and the census picks the width up on its own. And the real hazard is that the chips bake the hasher's constants into their constraints, so making the chip Poseidon breaks every call site that executes with TestPermutation — about thirty of them. That swap is a decision about what the machine's default hash is, and it should not be taken as a side effect of wanting a cell count.
Final status line. Slice 1a is complete and externally pinned; slice 1b is specified but deliberately unbuilt, per the ruling that a half-built chip is worse than none. Also records one claim verified rather than assumed for wave 9's benefit: the census per_chip array and build_air both read hash::cols::NUM_COLUMNS, so widening the chip propagates on its own and no census edit is owed.
…er choice The chips bake their hasher's round constants into their constraints, so execution, trace generation and the AIR set must agree. `HasherKind` is what carries that agreement: one value reaches the executor, the trace filler and `LfmAirs`, threaded rather than global so a single process can prove under both. Nothing flips. `Test` is the default and every existing entry point keeps its signature, delegating to a `_with_hasher` form — the machine's real hash is the open ecosystem decision this measurement feeds, not a side effect of it. The Poseidon layout appends its witness columns AFTER the frozen IN/S/OUT prefix and lets the final round's post-MDS output be the OUT columns themselves, so `bus_interactions()` is hasher-independent and the LFM_HASH tuple contract stays literally frozen: 28 + 7*36 + 24 + 22*14 = 612 value columns, one row per permutation. Not yet the measurement — the chip is unproved until an AIR runs it.
…lt for Fifteen tests over the chip §6.4 specified: the layout (612 value columns, 601 constraints, every column claimed exactly once so an off-by-one inside the block arithmetic cannot hide behind a correct total), the degree bound (<= 3, and something actually reaching 3 — a decomposition that quietly went quadratic would mean the S-box had stopped being computed), satisfaction in both modes, rejection, padding, and prove+verify. The prove+verify is the point. Per method rule 2 an execute-only test says nothing about a chip, so until the production prover built this AIR and the production verifier accepted it, 612 was a declaration rather than a measurement. It is now a measurement: 612 + 3*3 = 621 base-equivalent cells per permutation, read off the same census instrument that produced the keccak column, confirming wave 8's pinned prediction exactly. Two properties asserted rather than assumed: no program digest moves with the hasher (PREP_WIDTH is 11 in both layouts and the preprocessed group is untouched, so the registry cannot be silently reassigned by a hash experiment), and a proof does not verify under the other hasher in either direction.
…nits The prediction held number for number: 612 value columns, 601 constraints, degree 3, 621 base-equivalent cells per permutation, 121.5 M / 162.8 M hash cells, 1.906 B / 1.947 B epoch totals at 5.86x / 5.74x under keccak. One correction, and it is a units error rather than a cells error. "RSS ~50-51 GiB" does not reproduce from the two-term model it cites: that is the cell term computed in GB, labelled GiB, with the per-sub-proof term dropped. Both terms in GiB give ~52-53 GiB. Nothing downstream moves — the only claim the number carries is "far inside the 124 GiB box" — but the other rows of the matrix were computed the same way and are flagged for re-derivation. Also records the four falsifications, and why F4 is the interesting one: removing the round constant's mode-sum scaling breaks the padding row and nothing else, which is what makes "load-bearing, not decoration" a demonstration rather than an assertion.
Vendors the BLAKE3 6-round compression primitive and its chip from PR #903 (head 89aeeb8) into the LFM tree, replacing the chip's VM-coupled I/O side with LfmMem word tokens in the LFM_KECCAK adapter's discipline, and proves it standalone against the unchanged production BITWISE table. Measured: 3,056 main columns + 1,259 bus interactions (630 aux) = 4,946 base-field-equivalent cells per compression, 769 constraints, degree 3.
The blake column lands where the scoping report predicted (4.06x under keccak). The finding is what it was measured against: the non-hash residue every candidate row sits on is 95.8% the felt_be_halves byteswap gadget, which the field-native candidates delete — so their rows move ~10x, and the matrix's spread is 4x to 109x rather than 3.7x to 6.2x. Also prices the delegation topology (a net loss of 66% at these shapes) and re-derives the RSS rows with both terms and the correct sub-proof count.
The byteswap's cell share is 95.84% padding-aware and 51.38% unpadded, which resolves the disagreement: both prior estimates were right about different quantities and the gap is a 1.87x padding multiplier neither included. Poseidon's 0.18B survives (measured 0.195B). BLAKE3's 1.10B does not, as built (measured 2.752B), because the hosted chip consumes u32 lanes and so cannot shed the gadget that produces them — but a felt-absorbing variant lands at 1.097B, and the gap is exactly that unbuilt variant.
…CCAK_RC exactly; R_native stands at 73M
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.
What
LFM (Lambda Field Machine) — a straight-line, field-native recursion machine in
prover/src/lfm/. This draft carries the complete campaign: the machine, the assembled continuation-epoch verifier, the wrap run, and the measured hash matrix.Status — what works
start_index) and the attestationprogram_idjoin all run in-machine.make lintexit 0.The measured hash matrix
Epoch profile log2
[2 ×14, 3, 4 ×4, 5 ×3, 7, 20], inner proof at blowup 8 / 73 queries. Base-field-equivalent cells per epoch verify:Key structural finding: 95.8 % of the old "non-hash residue" (census base) is the felt→byte serialization gadget that exists only because keccak eats bytes; field-native candidates delete it. Full provenance and reconciliation:
others/lfm-hash-matrix-scope.md,others/lfm-assembly-obligations.md.Hash status
KECCAK_RND/KECCAK_RC/BITWISE) is hosted unchanged behind an LFM adapter chip speaking its bus contract.LFM_HASHswap surface via a construction-timeHasherKind(parameters: Plonky3Poseidon1Goldilocks<12>, α=7, R_F=8/R_P=22, externally KAT-pinned). The machine default remains the non-cryptographicTestPermutationplaceholder — the production hash is an open ecosystem decision this matrix informs.89aeeb8c2b0389e9d21a861c9e3a10a7b1b5704e) and hosted asLFM_BLAKE3, proved+verified standalone against productionBITWISE. Deliberately NOT registered in the 14-chip set — registration moves every program digest and is a separate decision. Depends on feat(prover,executor): BLAKE3 6-round compression accelerator #903 landing; the vendored copy carries a deletion note. Security rests on feat(prover,executor): BLAKE3 6-round compression accelerator #903's named assumption A6R (6-round, unratified).Known gaps / pending decisions
LFM_BLAKE3unregistered; A6R unratified.others/on this branch.Draft on purpose: for review of the machine and the matrix, not for merge as-is.