WHIR recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 40.20 s - #1010
Draft
MauroToscano wants to merge 1134 commits into
Draft
MauroToscano wants to merge 1134 commits into
MauroToscano wants to merge 1134 commits into
Conversation
`the_process_wide_counter_tracks_the_same_passes` asserted that a tree and a leaf pass are the same event -- `tree_builds() == leaf_hash_calls()`, and that an opening moves the global counter by one. With the leaf layer retained they are no longer the same event by design, so this test would have reddened on the box for the one reason the gate was not looking for: an invariant that expired when the code under it changed, in a file whose other tests were rewritten and this one was not. It now asserts the relationship that replaced it, in deltas because the three counters are process-wide and diverge on purpose: a commit assembles one tree and pays one pass; an opening assembles a tree and pays NOTHING, recording one saving instead; and over any window, trees == passes + savings. That identity fails in both directions -- a tree that skipped its pass without recording a saving breaks it, and so does a saving recorded for a tree never assembled -- where the old equality could only fail in one.
`run_grind` declared its result `uint64_t` and handed the address to the kernel as `volatile unsigned long long *`. Those are the same type on Darwin/arm64 and different types of the same width on LP64 glibc, so on Linux the cast type-punned; with `#include "rpx.cu"` putting the whole kernel in this translation unit, GCC 13.3 at -O2 was free under TBAA to assume a write through `unsigned long long *` could not touch an `unsigned long`, and to keep `result` in a register across the inlined call. It did. `run_grind` returned UINT64_MAX for every input, so layer 8's two checks per vector that expect the SENTINEL passed VACUOUSLY while the two that expect a found nonce failed. Six rows, at every sha back to the gated base c00342c, on a target that passes on a clang/arm64 laptop where the two types coincide. Measured on the box at this sha: -O2 6 FAILURE(S) -O2 -fno-strict-aliasing ALL HOST KAT CHECKS PASS -O0 ALL HOST KAT CHECKS PASS None of it was ever a statement about the device grind. This file is a HOST replay of the kernel source through `cuda_host_shim.h` — no nvcc, no cubin, no device — so the defect was in the harness holding the result, not in the kernel it tests. The production path re-validates every device nonce with the host predicate, and the block pins read `host fallbacks 0` throughout. `crypto/math-cuda/tests/host_kat/` holds exactly one instance of the pattern and this is it: the shim's `atomicMin` takes `unsigned long long *` as a parameter, and the kernels' casts there only drop `volatile` from an already-matching type. Test-only; no production code and no proof bytes move. It also unblocks this lineage's CI `host-kat` job, which has been failing since the device grind landed.
`a_group_holds_only_its_codewords_before_any_open` took `free_before` AFTER a `drain_and_trim()` and `free_after` without one. `free_vram_bytes()` is the driver's count and the device pool is configured to retain all freed blocks, so that difference measured the code PLUS every transient the four commits made. A delta between two samples is about the code only if both are taken at the same pool state, and the test's own comment says exactly that about the first drain. It read 301,989,888 B — nine codewords on a bound of nine, where the model says eight are held. The old one-sided bound was `8 x codeword` against four codewords held, so it carried 128 MiB of margin the pool had been living in unnoticed; the leaf-layer retention did not add pool retention, it consumed that margin. The slack was never sized against the transients either: `build_tree` allocates `(2L-1)*32` = 64 MiB, twice the bound's 32. The mutation arm settles which it is. Holding a whole node array instead of a layer moved the measurement to 480 MiB where the code then holds 384 - an excess of 96 against the honest run's 32, tripling while the holding grew by half. No "the code holds one more object" form fits both: 4*(cw+tree)+tree = 448, +cw = 416, and 5*(cw+tree) = 480 fits that run exactly but dies on the honest one, where 5*(cw+leaf) = 320 != 288. Every peak-demand model misses on BOTH sides (320 and 448 predicted). That is driver suballocation, not an accounting this tree keeps. So the driver's count is sampled at the same pool state on both sides, and the assertion messages now carry the CODE's own number beside it: the delta of `Backend::reserved_bytes()` across the window, the pool's share as the difference, and each held codeword's `reserved_bytes()`/`retained_leaf_bytes()`. A future failure says which of the two it is instead of posing the question. Pre-registered for the next card run: the honest case falls 288 -> ~256 and the whole-tree mutation 480 -> ~384. If the honest case still reads 288, the ninth block is the CODE and this reasoning is wrong. The assertion is not weakened: drained on both sides, four kept layers read ~256 below the 288 bound and four kept TREES still read ~384 above it, so the 128 MiB of separation the bound was designed around is restored rather than spent. Test-only.
The ledger the previous commit added is built inside the two assertion messages, so it appears only when the test FAILS. On the passing path its numbers were inferred rather than read, and what a pass alone establishes is `driver < bound` — pool share under one codeword — and nothing narrower. That is not enough for this guard. The mutation run that keeps a whole node array reads `driver 448 MiB · promised 383 MiB · pool share 64 MiB` even after the symmetric drain: a fragmentation floor of one largest transient, because a best-effort pool trim cannot release a chunk still backing a live allocation. If the honest path sits anywhere near that floor, this test has a margin of a few MiB and will flake, and a green run would never say so. 0 MiB and 31 MiB are the same observation today. So the line is printed unconditionally, under --nocapture, which is how the box gate runs this suite. Once its honest value is known a ceiling can be asserted against it, which is a gate change rather than a test change and is not made here. `promised` is worth having in the log for its own sake: at the mutation it read 383 MiB against a model of 4 x 96.00, exact to the MiB, which is what settled that the excess is the pool rather than a ninth object the code holds. Test-only; no assertion changes, no production code.
…olumns) The only fallback number the WHIR campaign read was `multilinear::gpu::host_fallbacks()`, which has exactly one caller — the COMMIT path in `whir_chain.rs` — so every `host fallbacks 0` certified that no commitment fell back and said nothing about the per-table argument. wt16 read as a slot-level win for exactly that blind spot: the leaf-layer retention grew `be.reserved`, argue's `reserve` then refused, and its work moved to the host uncounted while `tree_rebuild` alone showed the saving. Add a process-wide counter in `device.rs` beside `reserve` (`device_fallbacks` / `reset_device_fallbacks` / `note_device_fallback`), always compiled and reading zero on a non-cuda build, bumped at the five argue-side `reserve`->`None` sites in math-cuda: `sumcheck.rs` (x3), `gkr.rs` (x1), `columns.rs` (x1). The doc states this scope precisely and records the multilinear residual (`gpu.rs:177`/`:1572`) as a follow-up that needs each caller traced, and why `gpu.rs:1551` — a speculative reserve whose `None` selects a lazy on-device path — must never be counted. Tests: a card test drives the cheapest site (`DeviceColumns::upload`) with the budget fully reserved (an atomic bump, no device memory) and asserts the counter reads one; a card-free unit test covers the counter API; a card-free source-count test asserts the call appears at exactly the five sites, so the four undriven sites fail without four card fixtures.
…e-run block The WHIR tree harness printed no fallback line at all, so the launcher had nothing to gate on and (v9) voided every run by reading a `host fallbacks` line that only the lb-class grind harness prints. Print BOTH fallback surfaces, whole-run scope, at the WHOLE-RUN block of the production-tree test: `commit fallbacks` (`multilinear::gpu::host_fallbacks`, the commit path) and `device fallbacks` (`math_cuda::device::device_fallbacks`, the argue surface added in the previous commit). The launcher (A-tree-whir.v10) refuses a block number unless both read zero and refuses loudly if either line is absent — closing the blind spot wt16 read as a slot-level win, where argue's per-table work fell to the host uncounted.
…er instruments The evictable retention (round 2's fix) and any honest reading of the leaf-layer lever need two numbers the code lacked. RETAIN_BYTES_LIVE: the SIMULTANEOUS retained device footprint — fetch_add on admit, fetch_sub in a new Drop on RetainedLeaves — plus its per-run peak. Unlike the cumulative RETAIN_BYTES_ADMITTED (39,057 MiB in wt16), this rises and falls with the live layers, so it is the ~2 GiB that actually contends with argue for the budget. The peak is printed on the retention line; the instantaneous count is ~0 by the time the base readback prints (the codewords have dropped). reserved_high_water: the peak be.reserved, updated by note_reserved on every rise in Backend::reserve and DeviceReservation::grow. This is the reservation quantity argue's reserve is checked against, which the raw device trace cannot report — never-purge inflates the raw peak above the budget. Printed at the whole-run block. Tests: a card test asserts the live footprint rises with a held layer, the peak and high-water bound it, and — the balance the eviction relies on — the footprint returns to baseline when the codeword drops. Card-free unit tests cover the high-water's monotone max.
…e bytes instead of falling to host wt16 read the leaf-layer retention net-negative at the block: it grew be.reserved during commit and the openings, argue's per-table reserve then refused and fell to the host uncounted (+11.3 s argue vs the -9.45 s tree_rebuild saved). The cause was a single byte budget raced between the retention and argue. Make the retention SUBORDINATE to argue by eviction, so it holds only genuinely spare bytes and gives them back the instant a real caller needs them: - Backend::reserve, on a budget miss, consults an evictor ONCE before returning None and retries after it frees. grow (the retention's own capture) never evicts, so the retention can only ever yield to argue, never displace it. - whir installs the evictor (a fn pointer, via OnceLock) and keeps a registry of Weak handles to each codeword's (leaves mutex, reservation), registered once at first capture and pruned when the codeword drops. Eviction takes a layer out under its own mutex (a concurrent serve sees None and rebuilds -> no UAF; the evicted nodes' free is stream-ordered on the codeword's own stream, cited to cudarc core.rs:776-795 in the code), drops it, and shrinks the reservation -- freeing the BUDGET while never-purge keeps the raw bytes pooled. The evictor never calls reserve/grow (no reentrancy); lock order is registry -> one layer at a time, be.reserved lock-free -- acyclic. LFM_WHIR_RETENTION=0 disables capture entirely, so the ABBA control arm runs off the same binary as the retention arm. RETAIN_EVICTED / RETAIN_BYTES_EVICTED and the live-footprint peak are on the retention print. Tests: a card test fills the budget below a held layer's size and asserts the next reserve SUCCEEDS by evicting it (the layer reads None after) -- the arm that fails when the evictor is disabled.
…counted twin Round 3's poll fix is blocked on one bench reading: does the grind's stale-poll overrun FALL, RISE, or stay FLAT as the poll rate is lowered? That sign — not a magnitude — decides whether the "poll less" family of kernel fixes lives. O2 falsified the scan-factor lever; O4 read the SASS and closed the cache-qualifier lever (the poll is already LDG.E.64.STRONG.SYS). The one surviving hypothesis is CONTENTION on the single *result address. rpx_grind_search_counted (the diagnostic twin, on no proving path) gains a poll_period launch parameter: it polls *result for the early exit only every poll_period-th iteration, STAGGERED by thread via (n + tid) & (poll_period-1) so at any one iteration only 1/poll_period of the resident threads issue the system-scope load — average AND peak request rate both fall by poll_period. poll_period == 1 (mask 0) reproduces the shipped every-iteration poll exactly; the production rpx_grind_search is untouched. n is the thread's own loop counter (not i/stride, whose identity holds only while tid < stride). search_counted threads poll_period through to the launch (arg LAST) behind a zero/not-power-of-two guard, and echoes it back in GrindCounts so a report quotes the knob as read on the path. The rewritten rpx_grind_counted test sweeps k = 1/4/16/64 at scan 8 / grid 1024 over O3's 256 seeds, paired and rotated, and reads the overrun vs k. Controls: k=1 admissibility against the shipped kernel; the winning nonce identical across every k — the soundness control, since atomicMin only ever lowers *result, so a staler poll can only delay an exit, never change the nonce a launch returns. The verdict prints a granularity-adjusted (overrun - (k-1)/2) column to isolate the contention component from the poll-coarseness term.
…gister sweep of the RPX permutation The poll k-sweep falsified contention (POLL FAMILY DEAD), so round 3's lever must speed the RPX permutation itself: grind + two hashing passes all share it, and the file's cost model shows it is compute-heavy (inverse S-box = 95% of the field mults). The open question that picks the lever: is the permutation latency-bound (raising occupancy speeds it) or compute/issue-bound (it does not)? The card runs RPX at ~2/3 occupancy, register-limited. This adds the discriminator, card-free authored, as a whole-cubin register cap rather than __launch_bounds__: the SHIPPED grind kernel — which the sweep must move — is off-limits for a per-kernel annotation, and launch-bounds variants would need new kernels loaded in the off-limits device.rs. A -maxrregcount cap moves the untouched production kernels at build time. - build.rs: opt-in LAMBDA_VM_RPX_MAXRREGCOUNT ⇒ nvcc -maxrregcount, mirroring the existing -lineinfo knob; empty/unset ⇒ no cap ⇒ production cubins byte-stable. - math-cuda::rpx::permute_probe_sweep: times the pure permutation probe (htod once, so the cross-build delta is kernel time) and reports the ACHIEVED regs / blocks-per-SM read back from the loaded function. - math-cuda::grinding::grind_occupancy: the shipped grind kernel's achieved regs / blocks-per-SM. - prover/tests/rpx_occupancy_sweep.rs: one point per build — probe ns/permutation and grind mean ms at the achieved occupancy, one OCCSWEEP line to collect across the caps. The sign is read ACROSS builds (unset/85/51/42 ⇒ ~8/6/10/12 blocks/SM): time FALLS as occupancy rises ⇒ latency-bound ⇒ build the register-pressure lever; RISES/FLAT ⇒ compute-bound ⇒ occupancy and LDL.64 are dead, only a KAT-preserving arithmetic lever remains or round 3 lands at the arithmetic floor. A register cap cannot change a kernel result, so there is no soundness question; permutation parity stays pinned by rpx_device_parity. No default and no shipped kernel change.
…ytes probe (STEP 2, ncu-free)
The occupancy sweep put the RPX permutation at its arithmetic floor, so round
3's only remaining stage is argue (the WHIR field-argument: sumcheck + gkr +
columns, ~16.6s). STEP 1 (the O5 device-fallback counter, read from the round-2
logs) established argue does NOT host-fall-back at the tip — it is device-side
and stable. This is STEP 2's instrument: does argue's device work hit the HBM
roofline (memory-bound ⇒ an MLE layout/reuse lever exists) or run far below it
(compute-bound ⇒ near a floor, like the permutation)?
ncu is unavailable on the box (ERR_NVGPUCTRPERM), so the roofline is read by
ARITHMETIC: a new `math_cuda::argue_probe` records, per surface, the DEVICE-path
bytes reserved and the op count, at the same five reserve sites the fallback
counter already guards (sumcheck.rs x3, gkr.rs, columns.rs). Divided by the
`argue` wall time the harness already prints, the total bytes give an achieved
HBM bandwidth. Reserved bytes ≈ the HBM working set (a resident buffer re-read
within an op is L2/L1, not HBM), and it is additive — unlike a wall-timer at
these sites, which would double-count when gkr's layer sumcheck nests inside a
reserve; a per-surface time / device-host split is STEP 2b, only if the byte
roofline is borderline.
- crypto/math-cuda/src/argue_probe.rs: per-surface {bytes, calls} atomics +
note_device / surface_totals / reset (mirrors the DEVICE_FALLBACKS pattern).
- the five reserve-SUCCESS sites call note_device beside the else's
note_device_fallback.
- per_table_aggregator_tests.rs prints `argue probe: sumcheck B/ops · gkr · columns
· total` beside the existing `device fallbacks` line.
Diagnostic only, on no production decision path; a reservation is unchanged, so
this cannot move a proof. No default and no shipped kernel change.
… argue discriminator
The argue census put the WHIR argument at ~2% of the HBM roofline and single-digit-%
of compute on LARGE kernels — GPU-under-utilized, not floored. ncu is driver-locked
on our box (ERR_NVGPUCTRPERM), but Mauro has a profiler-capable server. This gives
him one representative launch to profile.
`ncu_sumcheck_round_block_scale` (an #[ignore] test in tests/sumcheck.rs) builds a
block-scale sumcheck — num_vars=21 (KECCAK_RND scale, the census byte-leader), a
Builder-lowered program at the tested (width 4, degree 5) shape — and runs a handful
of round + fold launches so Nsight Compute can profile sumcheck_round_ext3 (and
sum_partials_ext3 / sumcheck_fold_ext3) at realistic dims. It reuses the file's
existing factor()/program() helpers, so the program is a valid lowering, not a
hand-fabricated node stream. No host cross-check (a 2^21 host round is far too slow)
and no correctness claim — parity is device_rounds_match_the_host_sumcheck's job;
this exists only to hand the profiler a launch. On no production path.
⚠ ncu -c 1 profiles ONE kernel = that kernel's own occupancy/SoL, NOT the inter-round
host-sync idle (round() synchronizes every round to cross the transcript answer to
the host — sumcheck.rs's own note: "more time than the rounds themselves"), which is
a timeline property for nsys. So it answers "is the round kernel itself
under-occupied?" — the complement to the host-sync finding.
Build + profile (WHIR branch only — the argue stack is not on main):
cargo test -p math-cuda --release --test sumcheck --no-run
ncu --set full --section SpeedOfLight --section WarpStateStats --section Occupancy \
--section MemoryWorkloadAnalysis -k regex:'sumcheck_round_ext3' -c 1 \
<target/release/deps/sumcheck-*> ncu_sumcheck_round_block_scale --exact --ignored
…n discriminator) Round 3's concurrency lever is soundness-dead: the whole argue is one sequential Fiat-Shamir chain (run_rounds is a per-round chain; multilinear_table.rs:444 argues all tables in one transcript), so no sumcheck round can overlap another — the challenge order is the proof. Argue's ~2% GPU utilization is therefore mostly INHERENT per-round host-sync latency, not a recoverable inefficiency. This sizes it, on our own box (ncu is driver-locked): a gated, opt-in device-busy probe measures how many seconds the sumcheck round kernels are actually executing, so idle = argue wall − device-busy is the total gap. It is not a recoverable ceiling by itself — the recoverable-without-a-rewrite part is only what transcript-independent prefetch can fill. - argue_probe: DEVICE_BUSY_NS + add_device_busy_ns/device_busy_ns, and busy_probe_enabled() (reads LAMBDA_VM_ARGUE_BUSY_PROBE once, cached). - sumcheck.rs round(): when enabled, a reusable TIMING-enabled CUDA event pair (thread-local, created ONCE — a mid-prove cuEventCreate convoys the driver lock) brackets the round kernels; the elapsed is read after the EXISTING per-round synchronize(), so no extra sync and no perf change. Off by default: production round() only reads a cached bool and skips it. - per_table_aggregator_tests.rs: prints `argue device-busy (round kernels): X s` beside the argue probe line. Round kernels only (fold + setup excluded), so idle = wall − this slightly OVER-estimates. Diagnostic; no default and no shipped-kernel behavior change when the env is unset.
The per-table argue is a serial Fiat-Shamir chain: each sumcheck round syncs to the host for the next challenge, leaving the GPU idle ~9.5s of the 16.6s argue wall. A table's fraction tree depends only on the global (z, alpha) and the table's trace — not on the transcript at that table's turn — so it can be built ahead, during the previous table's argue, to fill those host round-trip gaps. - gpu.rs: DeviceTree's output fraction becomes a lazily-read OnceLock. input_layer_tree_deferred builds the tree WITHOUT the one output() sync (the fold kernels stay in flight); the read happens at the consume site (FractionTree::from_device), before GKR spends any level. Gated by a non-evicting headroom check (vram_budget - reserved, which already includes the round-2 retention) so a second tree never displaces argue or the retained leaves — reserve-or-skip. math-cuda untouched. - logup.rs: resident_tree_deferred / PrefetchedTree wrap that path; into_tree() finalizes (reads output) at the consume site. - multilinear_table.rs: prove() takes an optional prebuilt tree; multi_prove runs a depth-1 pipeline behind LFM_WHIR_PREFETCH. LFM_WHIR_PREFETCH unset/0 is byte-for-byte the current serial path (prove builds its own tree eagerly). =1 enables the pipeline for a one-binary A/B/B/A. Prefetch is strictly subordinate: argue > retention > prefetch, reserve-or-skip, never an eviction of round-2 leaves. The overlap depends on the residency handing consecutive tables distinct streams and on non-evicting headroom; where neither holds the pipeline skips and the wall is unchanged, which the A/B settles empirically.
…iminator) Round 3 measured the WHIR BASE at two floors (the RPX permutation's arithmetic floor; argue's Fiat-Shamir sequencing floor). The ~55s ABOVE the base — level 0's epoch wraps, the cross-epoch GLOBAL child, the interior fold levels, the block-artifact root — was never examined for concurrency slack, and three of its four stages print no occupancy number at all. The serialising resource there is the card PERMIT, not SM utilization: device_permit is mutual exclusion over a proof's two device phases (build_artifacts' per-dispatch admission has no running total; each multi_prove builds its own full-budget VramGate), so even a card idle INSIDE a device phase cannot be filled by another sibling. The ceiling on every concurrency lever in this phase is therefore the permit-held total, and held/stage-wall is what separates "the card is the wall" (a floor) from "the host is the wall" (a lever). What was missing, and why: - The interior's permit line is printed only from compose_interior_levels' BARRIER loop. The production harness runs LFM_TREE_LEVEL_POOL=1 with LFM_TREE_LEVEL_POOL_FROM at its default 1, so barrier_levels is 0 and the whole interior goes through the POOLED span, which calls no take_stats. The reading is absent on the configuration that runs. - The GLOBAL child and the ROOT run with the permit armed at 1, where hold() returns before a guard exists and Drop accumulates nothing into HELD_NANOS. Their device-phase time appears in no summary. - reserved_high_water is whole-run, so the base's reservation is the only number any tree stage could report. - tree_probe: the probe's own per-label held/queued counters, a device commit dispatch total, and a running maximum of the reservation high-water. It never touches HELD_NANOS, ACQUISITIONS or take_stats, so every line the drivers already print keeps its exact meaning. - device_permit: CardPermit carries the phase and its queue time when the probe is on, and Drop feeds tree_probe OUTSIDE the guard branch — which is what lets the K=1 stages be priced. - commit.rs: a host stopwatch around try_commit_row_major, the only device work inside the build_artifacts hold. NO CUDA event and NO added synchronize: the call already blocks until it has a root. The total is WORKER-SECONDS (both walks go through map_maybe_parallel), and the banner prints LFM_ARTIFACT_PARALLEL and LFM_ARTIFACT_GROUPS_IN_FLIGHT read on the path so a ratio above 100% reads as concurrency. - per_table_aggregator_tests: one TREE PROBE line per tree stage, the interior's missing permit line, and the reservation high-water split at each stage boundary. Taken in the WHIR driver, so compose_interior_levels and the STARK driver are untouched. LAMBDA_VM_TREE_BUSY_PROBE unset, empty or 0 is byte-for-byte the current behaviour: no counter moves, no line prints, no counter is cut, and the only cost anywhere is one cached OnceLock read per card hold. On, the reservation high-water is cut per stage, so the harness's whole-run line reads the last stage — the probe prints the run maximum beside it and says so in the same line.
… answer The free read of wt27 and wt28 landed before this probe was ever built, and it answered most of what the probe was for. Three shipped instruments already partition the tree phase: the per-hold CARD HOLD lines (62 of them, with held seconds and epoch brackets), the per-node LFM PROVE line (execute / fill / multi_prove / permit wait), and the per-prove PROVE SPLIT line. Summed by hand they give every stage's permit-held fraction, and the 10 Hz nvidia-smi trace the harness already keeps splits device memory by phase. So two parts of this probe were measuring settled quantities and one of them had a cost. Removed: - The per-stage device reservation high-water. Splitting it meant CUTTING a process-wide counter at every stage boundary, which cost the harness's own whole-run `reserved high-water` line its meaning. The number did not buy that: the whole-run figure is 25,003 MiB against a 32,607 MiB card, no tree stage is near the budget, and the sampler already splits device memory by phase. A measurement that degrades an existing one has to buy more. ⇒ the probe now has NO side effect on any line the harness already prints, on or off. - The interior's extra `device_permit::take_stats()` line. The interior's permit-held fraction is settled at 0.92 of its wall from the CARD HOLD lines of both runs — a floor under the mutual-exclusion permit — and reading that counter CLEARS it, which belongs to the lines the drivers already own. Kept, because nothing else prints them: the per-label held/queued accounting for the stages that run with the permit armed at 1 (the WHIR global child and the block-artifact root, where `hold` returns before a guard exists and `Drop` accumulates nothing), the four stage lines that partition the tree phase, and the device commit dispatch total inside the build_artifacts hold. The four stage lines stay even where they decide nothing: `take` clears, so a stage that printed nothing would fold its holds into the next stage's line. LAMBDA_VM_TREE_BUSY_PROBE unset, empty or 0 remains byte-for-byte the current behaviour.
… its mover The lineage's first PR CI (run 35533170457, PR #999) turned up four red prover tests. All four are pre-existing at the base c00342c, all four have ONE mover, and hypothesis B — a posture or env dependence, the campaign's LAMBDA_VM_MAX_ROWS_LOG2=21 or LAMBDA_VM_WHIR_HASH=rpx — is ruled out for every one of them: the registry path reads no env (REGISTRY_HASHER is a const and `build_artifacts` passes it explicitly), and the one knob that IS read, `max_rows_log2_override`, points the other way, since CI's bare env uses the LARGER production caps. THE MOVER is `FIXED_TABLE_COUNT` 11 -> 5, which arrived with 892c7d1 (main's c2ac5d5, #977). COMMIT, KECCAK, KECCAK_RND, ECSM, ECDAS and HINT stopped being always-on and became `TableCounts` fields — a run that never reaches one carries no sub-proof for it. That has two arms, and every red pin sits on one: (i) THE TABLE SET SHRANK. `air_trace_pairs` pushes only BITWISE, DECODE, KECCAK_RC and REGISTER unconditionally; everything else comes from a `Vec<VmAir>` that is empty when the count is zero. (ii) THE STATEMENT ENCODING GREW 49 BYTES. The six counts joined the absorbed epoch statement and #977 bound `is_final` into it as the last byte: `NUM_TABLE_COUNTS` 15 -> 21 and a trailing `+ 1` on `EpochStatementShape::byte_len`. Recomputed from the code rather than from the prose, with a 30-byte CONTINUATION_EPOCH_TAG: 30+32+8+8*15+8+1+8+8 = 215, and 30+32+8+8*21+8+1+8+8+1 = 264. Each re-blessed assertion names 892c7d1 and its arm, so the next reader can trace it without the thread this came from. None of these is a regression. Each pin caught a deliberate production change that was ported without re-running it, which is the pin working. The port DID update everything that fails to COMPILE — algebraic_transcript's `[u64; NUM_TABLE_COUNTS]` literal, logup_tests' `[...; FIXED_TABLE_COUNT - 1]` census, whir_statement_tests, statement_replay's own derivation and module doc — and missed every pin that fails only at runtime. These test files exist on no other branch and the lineage had no PR CI until #999, so nothing ever ran them against #977. Confirmed independently: the four names appear in none of the box gate logs either, and every earlier box `cargo test -p lambda-vm-prover` run was a filtered `--exact` run of a single unrelated test. LFM_REGISTRY, regenerated. StatementReplayV0 is the one registered program that replays the epoch statement, so arm (ii) moved its script by one Blake3Chain compression and seven of its fifteen roots with `program_id`. Regenerated with `compute_lfm_registry`; `compute_static_commitments` was not re-run and did not need to be, this being no hash-pin change. EXACTLY ONE ENTRY MOVED, checked rather than assumed: the other five programs build no epoch statement, and every root, log-height, `keccak_rnd_chunks`, `hasher` and `chip_set` of each came back byte-identical — slots 13 and 14, the statics, included. `log_heights[11]` did not move even for StatementReplayV0, 9 and 10 compressions both padding to the 16-row group. And the regenerated `roots[11]` equals the value the pin computes from the program (`7a 3b 86 1b ...`), which is what says the paste closes the gap the pin found instead of moving the pin to meet the paste. The runtime pins: - blake3_chip_tests, arm (ii): STATEMENT_REPLAY_BLAKE3_ROWS 9 -> 10. 49 bytes is under one 64-byte Blake3Chain block, so it is worth exactly one more compression. TRANSCRIPT_REPLAY_BLAKE3_ROWS stays 8 — TranscriptReplayV0 replays no statement, and that is what keeps the two an oracle rather than two literals: a change that moved BOTH would not be this one. - epoch_verify_tests, arm (i): SUB_PROOFS 25 -> 16, CHALLENGES_AT_MIN_PRESET 115 -> 79. Six of the nine that left are the accelerators; the pre-#977 25 was 14 split families + 10 intermediate fixed + 1 L2G_MEMORY, and the fixed term is now 4, which lands at 19. The remaining three are split families this fixture leaves empty and are NOT named, because the measurement does not name them. 79 falls out twice: from the stated model, 111 + 4*(16-24); and from the loop's own counter, 2 + 16*4 + 13, the 13 zetas being 115 - 2 - 25*4. The `checked` assertion is the real oracle and fails if the four-challenge model stops describing the move. The accounting identity had to be respelled, not just re-blessed. SUB_PROOFS is now BELOW the 24 it is measured against, and `SUB_PROOFS - 24` on a usize is an underflow rather than a failed assertion. Both sides are positive now, so it still fails in either direction. - machine_tests, arm (ii): `epoch_statement_cursor_is_three_plus_output_len` was never red on CI because nextest cancelled its shard first, and it is red — 215 + L + 16R against an actual 264 + L + 16R, 261 versus 310 at the acceptance shape. Renamed to `..._is_the_output_len_alone`: the constant term's own shift is gone, so Phase A inherits `L mod 4` where it inherited `(3 + L) mod 4`. The rider asking for a one-byte pad at the end of the statement encoding got it from #977 without anyone aiming there, tag bump included, and is marked resolved. - constraint_artifact_tests, arm (i): `continuation_epoch_constraint_leg` asserted `fixed_final.len() == FIXED_TABLE_COUNT`, i.e. 11 == 5. Also never reached by CI. The list splits into `always_on` (five, the census target) and `accelerators` (six), which stay in the COST sum because that sum is the figure a recursion budget has to clear. So (25, 26) survives, as a CEILING rather than as the composition — 19/20 is the accelerator-free floor. Swept by VALUE and not only by test name — 215/264, 261/310, 207/223, 11/5, 15/21, 24/25/26, 79/111/115/119, the moved root and program_id prefixes, and the spelled-out counts — across prover/ and crypto/, tests and non-tests. Two hits beyond the six were pins in substance: - SOUNDNESS.md's `T = 24`. Two corrections, and the bound survives both. `T` is now smaller (16 on the fibonacci fixture), and since `E = 4 + sum_t (3 + L_t)` is increasing in `T` and `P <= 3E * 2^-32` in `E`, a smaller `T` only lowers `P`: the quoted `P ~ 2.5e-7` stays a valid, now conservative, upper bound, and the `T ~ 60` figure that matters for a real block is untouched. The second correction is sharper: the test the paragraph cites as the measurement, `arena_filler_reads_real_committed_roots`, asserts `tables > 0` and that no root is all-zero — never a count. "Measured, not assumed" was true of the run somebody did and false of the suite, so nothing would have failed when `T` moved, and nothing did. `T` for that two-epoch continuation fixture is unmeasured since #977 and is now read against the 25/26 ceiling. - logup_tests' "all 25 sub-proofs declare interactions". Corrected without spelling a count: the loop walks `census`, so a literal there would be a second, driftable copy of a length the loop already holds. Judged NOT pins, and left alone: `FE::new(215)` (fri_tests, a polynomial coefficient); 215 squeezes (crypto's transcript_counters, a different quantity); 16,777,215 (math-cuda, 2^24-1); 261 (ecdas column index); 1,261 and 1,397 (blake3 interaction counts); 223,380 and 229,290 (continuation page census); BLOCK_MARGINAL = 111 (continuation page cost); `rejects >= 20` (machine_tests, a rejection count); `i >= 26` (blake3_socket_tests); the blake3 KAT "all ten vectors"; and every `FIXED_TABLE_COUNT`/`NUM_TABLE_KINDS` use that names the constant instead of a literal, since those adapt. Left for a measurement rather than an edit: wrap_tests' measured record table (25 sub-proofs, 210,782 instructions, 82,059,828 cells, 45,953,352 proof bytes) and epoch_verify_tests' `[pinned: see the run output]` figures. Re-blessing a measured record without a measurement is the thing the rules forbid. STILL OPEN: multilinear_table_tests' three `>= 20` table-set assertions, which want the argued set BY NAME rather than a count, and therefore one run first.
…gued `prove_and_verify_all_tables` returned a count, and its three callers asserted `>= 20` against it. Two of the three are red on the lineage since 892c7d1 (#977) elided empty tables, and between them they produced one usable diagnostic and one that said nothing at all: every_live_table_is_proved_and_verified "expected the full table set, argued 10" the_whole_instruction_set_..._verified "assertion failed: ... >= 20" The second is a bare `assert!`, so neither CI nor the box could say what it argued — which is why a red gate on the lineage base needed a second run to diagnose at all. The helper now returns the argued tables BY NAME, in `air_trace_pairs` order, and each of the three assertions prints the whole list. Captured from `pairs` rather than from the AIR set, so it is the proof's own sub-proof order, and pinned against `tables.len()` so a census that described a different proof cannot pass. This is a diagnostic step, taken separately on purpose: the `>= 20` bound itself is what wants replacing, and it wants the measured sets first. Since #977 the set is workload-dependent — an empty table is elided rather than padded — so "how many" stopped being the question and "which ones" became it. A count cannot tell a table that vanished from one that gained a chunk while another vanished, which is exactly the class of move #977 made. The bound is left at `>= 20` here and is expected to stay red for two of the three; the named-set pins land once the three lists are in hand.
`make fmt` from the repo root. One line, in the `fixed_final` construction the re-bless added: the `always_on.iter().chain(accelerators.iter())` chain sat at 93 columns, which rustfmt breaks onto one method per line. Nothing else moved, which is the useful part. The registry regeneration in 8cedf2e hand-reproduced rustfmt's 14/14/4 wrapping for eight `[u8; 32]` literals rather than running the formatter over them, and rustfmt touched none of the eight — so the reconstruction was exact. Had any been wrong, `cargo fmt --check --all` would have failed as `make lint`'s first step instead of passing.
…hild as task 0 of level 0's pool)
The WHIR global child runs ALONE between level 0 and the interior. Measured
from wt27's and wt28's 62 CARD HOLD brackets, its stage is 6.48 s of which only
2.09 s is time inside a device phase: 4.4 s of host work — the cross-epoch
harvest and verify (1.1 s), the emit and arena build (1.2 s), its census, its
own host verify — performed with NO other proof on the card, because nothing
else is scheduled.
The refusal this replaces said so itself: "overlapping it is an optimisation
round's item, not an unset knob's". This is that round.
- whir_level_zero gains `fan_in` and `top_overlap` and returns an
Option<WhirGlobalChild>. Under the knob it runs the global child as task 0 of
its existing pool via PoolOut / split_pool_out / in_index_order — the shape
the STARK level 0 has run since the overlap landed there, and the shape its
four unit tests already cover (split_pool_out_keeps_index_order_when_completion_is_reversed,
the_overlap_does_not_move_a_single_wrap, a_panicking_global_task_re_raises_with_its_message,
a_missing_global_task_is_caught_at_the_drain).
- The global task is called from INSIDE whir_level_zero rather than handed in as
a closure, for the same `H` that makes level 0 a function at all:
prove_whir_global_child is generic in H too, so calling it there reuses the
level's own H. The return type still names no H — WhirGlobalChild is a
RealChild plus a GlobalLayout.
- The consume site becomes `match overlapped_global { Some(done) => done, None =>
prove it here }`, so the stage is consumed at the same point in the program on
both arms and nothing downstream can tell which produced it.
- ONE MORE TASK, NOT ONE MORE WORKER: at most LFM_TREE_SIBLINGS_L0 working sets
are ever live and one of them is the global child INSTEAD of a wrap. The card
is unaffected — the global task takes the same permit every wrap takes, so
`max holders 1` still holds and still asserts.
- The fixture-scale driver passes `false` explicitly and asserts it got no
overlapped child, so what the card-free test covers does not depend on the
caller's shell.
WHY THIS CANNOT REORDER A TRANSCRIPT APPEND
Not "the appends are still in order" but "there is no shared order to disturb":
1. Every LFM proof builds its OWN transcript. prove_traces_with_hasher opens
`block_transcript(&[])` fresh per call and absorbs that proof's own
program_id and public words. So the 15 wraps and the global child construct
15 + 1 independent transcripts; no append by one is ever observed by another,
and their relative timing is not a quantity the proofs can see.
2. The global child reads nothing level 0 produced. Its signature takes the
bundle, the ELF bytes, the options, the ceiling and fan_in; its own doc says
"it reads NOTHING any level-0 wrap produced". The register chain between
siblings is bound by emit_chain_bindings and the memory chain closes at the
ROOT.
3. The ROOT's transcript is unmoved. It absorbs the interior children's arenas
and then the global child's, a plain concatenation in declaration order, and
the driver still performs that declaration in the same order — the overlap
changes when the global child was PROVED, not where its bytes sit.
4. The drain is by INDEX, not by completion. split_pool_out preserves index
order and asserts the global ran exactly when the knob is on, so the wraps
arrive as the serial loop built them and a knob that silently stopped
scheduling the task fails at the drain rather than at a root with no child.
Unset or 0 is byte-for-byte today's behaviour: l0_offset is 0, the pool is the
same 15 tasks, and the global stage runs where it always ran.
REPORTING CHANGE, ON THE `=1` ARM ONLY, stated because a reader could mistake it
for a regression: the global child's prints — including `MARK AFTER the WHIR
global child` — are emitted by a worker DURING level 0, so slicing phases by
that MARK gives level 0 and the global child as ONE window. Its TREE PROBE line
relabels itself to say its cost is inside level 0 rather than reporting ~0 s as
though the stage had vanished.
… gap The three multilinear table-set cases asserted `>= 20` argued tables. Two went red when the main-sync merge `892c7d1bc` (main's `c2ac5d546`, #977) took `FIXED_TABLE_COUNT` 11 -> 5 and made COMMIT, KECCAK, KECCAK_RND, ECSM, ECDAS and HINT counted: an empty table is ELIDED from the proof now rather than padded into it, so the argued set is workload-dependent and "the full table set" stopped being something a bound could describe. A count is the wrong instrument for that move, twice over. It cannot tell a table that VANISHED from one that gained a chunk while another vanished, and it says nothing about ORDER — which `air_trace_pairs` calls the proof's sub-proof layout in as many words, since `air_refs` has to reproduce it. So the bound is replaced by the ordered census, MEASURED on the box at 788f36a, CPU-only, no campaign env: sub 10 BITWISE DECODE KECCAK_RC REGISTER HALT CPU[0] LT[0] MEMW_A[0] PAGE:0x0 MEMW_R[0] all_instructions_64 15 ... + SHIFT[0] MUL[0] DVRM[0] BYTEWISE[0] CPU32[0] The first five of each are exactly `FIXED_TABLE_COUNT`'s five, in `air_trace_pairs` order, which is a third independent confirmation of the 11->5 move — after the epoch's 25 -> 16 sub-proofs and the statement's +49 bytes. `ALWAYS_ON_TABLES` holds them once and `the_always_on_prefix_is_the_constants_own` pins its length against the constant, so the shared half of both censuses cannot drift from the machine the way `constraint_artifact_tests`' sibling list did (it named eleven while the constant said five). ⚠ `all_instructions_64` IS NOT THE FULL TABLE SET, and the old bound is what hid that. Fifteen argued, and six counted families absent: MEMW (the unaligned one — only MEMW_A and MEMW_R appear), LOAD, STORE, BRANCH, EQ and COMMIT, plus every accelerator. Since #977 an absent table is a table with NO ROWS, so the fixture executes no branch, no load, no store and no `eq` — a narrower program than its name suggests. Not fixed here: widening it edits `executor/programs/asm`, and this census is the thing that would notice. Pinned, with a non-vacuity check that the five tables it does add over `sub` are actually present, so the two censuses cannot decay into one test written twice. The precompile case keeps its bound and is the only one without an ordered census, deliberately: it PASSED the measuring run, so its assertion never fired and never printed its set, and pinning a list nobody has read would be a literal invented to fit a bound. It gains instead the checks its doc has always claimed and never made — that KECCAK_RND and COMMIT are argued at all, which is the whole reason it sits beside the two asm cases. Since #977 those are counted tables, so a workload that stopped reaching the precompile would drop them silently and still clear any bound. Matched as "equal, or followed by `[`" so a bare prefix cannot let KECCAK_RC answer for the family. Every assertion prints the full set, so the run that fails one is the run that supplies the census.
…al-nonce control ⛔ DROPPABLE, AND NOT THIS LANE'S CODE. `prover/tests/rpx_grind_counted.rs` is O6's grind poll k-sweep (27be22c) and this is its cross-k IDENTICAL-NONCE soundness control — the check that witnesses that a poll period never changed a winning nonce. Nothing else is touched. `make lint` has been red on the whir/lfm-o6-grind lineage since that commit: the FIRST clippy pass (`cargo clippy --workspace --all-targets -- -D warnings`) fails with two `needless_range_loop` errors at :264 and :266, so passes 2-4 never run and `make lint` exits 2. It was missed because that lane's recorded gate was per-package — `cargo clippy -p math-cuda` — which does not reach lambda-vm-prover's test targets. The repo rule is the opposite: do not substitute per-package clippy for the Makefile target. The rewrite keeps the comparisons, the failure message and the bounds exactly: `nonces` is `vec![Vec::with_capacity(RUNS); n_arms]` and the seed loop pushes once per (seed, arm) with no early exit, so `nonces.len() == n_arms` and every row is `RUNS` long. Iterating `nonces[0]` IS the old `0..RUNS`, and `take(n_arms).skip(1)` IS the old `1..n_arms`. ⚠ And the comment now records why clippy's own suggestion must not be applied: it offers `take(n_arms).skip(1)` for the OUTER loop as well, which drops the `s` index. The body compares `nonces[a][s]` against `nonces[0][s]` and needs both, so that suggestion would have compared whole arms instead of per-seed nonces — turning a control that can fail into one that cannot.
… that proved the wrong guest The full lib suite at 413b3a3 (plain libtest, every test regardless of failures) found four red. One was mine to expect; three were pre-existing at the lineage base and invisible to nextest's fail-fast. Three are fixed here. The fourth is a MEASUREMENT and is left red on purpose — see the end. ⛔ THE PRECOMPILE TEST HAS BEEN PROVING THE WRONG GUEST. `a_program_using_a_precompile_is_proved_and_verified` loaded `keccak.elf`, which is `executor/programs/rust/keccak`: a guest whose Cargo.toml depends on `tiny-keccak` and whose `main` hashes in SOFTWARE, issuing no syscall but `commit`. It has never touched a precompile. The accelerator guest is `keccak_precompile`, whose `main` calls `lambda_vm_syscalls::keccak::keccak256` — the `keccak_permute` ecall — over five padding edge cases. ★ And the doc's claim was false BEFORE #977 too; it was merely unfalsifiable. KECCAK and KECCAK_RND were always-on then, so they sat in the table set of every workload whether reached or not, and "which brings KECCAK, KECCAK_RND and KECCAK_RC in" described MACHINE shape while reading as program behaviour. `892c7d1bc` (main's `c2ac5d546`, #977) made them counted and turned a latent falsehood into a visible one — the same shape as SOUNDNESS.md's `T = 24`: a claim no assertion defended. The census that finally said so carries COMMIT[0] and no keccak table at all. Worse, `keccak_precompile.elf` is built by the Makefile's `RUST_PROGRAM_DIRS` wildcard and the prover proved it NOWHERE — its only reference in the tree is `executor/tests/rust.rs`, which runs it in the executor. So the suite had no precompile coverage on the multilinear path at all. Both halves land rather than one: - the precompile case now loads `keccak_precompile.elf` and asserts KECCAK, KECCAK_RND and COMMIT are argued. By PRESENCE, not an ordered census: this guest has never been proved on this path, so there is no measured set, and inventing one would repeat the mistake above. Its prove cost is likewise unmeasured. KECCAK_RC is deliberately not in that list — it is always-on and covered by the prefix, so matching it would let a run reaching no precompile satisfy a check named for one, which is exactly how the software guest passed for as long as it did. - `a_software_hash_guest_argues_the_widest_table_set` keeps the software guest and pins its MEASURED 21-table census, because it is the widest set in the suite: it reaches MEMW, LOAD, STORE, BRANCH and EQ, the five families `the_whole_instruction_set_is_proved_and_verified` does not despite its name, plus public output and two PAGE tables including the stack page. A Rust guest doing ordinary work exercises more of the VM than the asm fixture named for the instruction set. `state_depends_on_every_table_count` read 21 against a literal 20. ✓ VERIFIED cause: #977 moved COMMIT into `TableCounts` — `pub commit: usize` is absent at `892c7d1bc^1` and present now — so `each_count_mut` grew a field and the literal did not. The fix is not 21. It is `statement::NUM_TABLE_KINDS`, the same length `table_count_values` returns as `[u64; NUM_TABLE_KINDS]` and the guest absorbs as `statement_replay::NUM_TABLE_COUNTS`; a bare literal there says nothing about WHICH count is missing and is a second copy of a number the crate already holds. `no_call_site_outside_the_pin_reaches_a_default_alias` flagged `lfm/algebraic_commit.rs`, and it is a FALSE POSITIVE — but not blessed away as one. Both matches are in `#[test] the_host_search_finds_a_valid_nonce_under_rpx` (added by `80d746321`): `GrindingDigest<RpxStarkHash>` and `GrindingDigest<Blake3StarkHash>`. Neither reaches a DEFAULT; both name their hash, which is what §6.7 asks for. The second is a cross-hash CONTROL — BLAKE3 work must not satisfy the RPX predicate — and deleting it makes the test a tautology. The two halves are treated differently on purpose, because the allowlist's own doc says it holds hash-AGNOSTIC items: - `GrindingDigest` joins CONFIG_ALLOWED. Generic over the tag, selects nothing. - `Blake3StarkHash` does NOT. The file joins BLESSED instead, so the concrete tag keeps flagging everywhere else — a site naming it on the block path under an RPX pin is precisely what this gate is for. The BLESSED entry answers the reachability question the list demands rather than stopping at "test-only", which that doc calls one scope too wide: the consumers are `stark::grinding::generate_nonce::<T>` and `is_valid_nonce::<T>`, generic over the tag passed at the call site, so no global is read; and the value never leaves the test body, so the paired-default failure the list exists to catch has no subject here. ⚠ LEFT RED, DELIBERATELY: `the_blake3_tenant_socket_matches_the_record`. `BLAKE3_TENANT_SOCKET` is `Test` and `BLOCK_HASHER` has been `Rpx` since `603c1e155` (2026-09-08), while the census it is a ratio against is `bench_cache/optladder_2026-08-21/TIP/tip-wrappt-24.stdout` — eighteen days older. The instrument is working: it says the module measures a shape nothing proves. Moving the constant to `Rpx` is not a fix, because `RECORDED = (28, 3)` is the *Test* socket's width pair, and that number's own doc says it moves the headline ratio by a third in the FLATTERING direction if wrong. It needs a re-recorded CHIP CENSUS under the current pin, which is a run, not an edit.
…ames its hasher `the_blake3_tenant_socket_matches_the_record` is red and is right to be: `BLAKE3_TENANT_SOCKET` is `Test`, `BLOCK_HASHER` has been `Rpx` since `603c1e155` (2026-09-08), and the record this whole census is a ratio against is `bench_cache/optladder_2026-08-21/TIP/tip-wrappt-24.stdout` — eighteen days older than the pin. The instrument is doing its job: it says the module may be measuring a shape nothing proves. It could not SAY what the shape is, though. The socket assertion fires before any tenant is built, so a red run yielded no number at all — and the obvious cheap run does not yield one either. `wrap_tests::the_wrap_census` reaches `lfm_chip_census`, which is `lfm_chip_census_with_hasher(program, HasherKind::default())`, and `HasherKind::default()` is `Test` (`hash.rs:251`, `#[default] Test = 0`). It reports this very pair under ANY pin: a confirmation that cannot fail, on the one number whose error is flattering. That symbol is itself one of the three `IMPLIED_HASH_SYMBOLS` the §6.7 gate hunts for, which is what a census defaulting its hasher looks like from the other side. So the test now prints every tenant's MEASURED `LFM_HASH` width before it asserts anything, one line per tenant, each naming its `HasherKind` and flagging the one that IS `BLOCK_HASHER`. A width without the tag that produced it is the mistake this finding is about, so no line omits it. All eight tenants are walked; both halves already go through `tenant.airs` + `tenant_tables` in the algebraic and non-algebraic loops elsewhere in the module, so this adds no new construction. Nothing is re-blessed. `RECORDED` keeps its value and the assertions keep their polarity, because the replacement pair has not been measured yet — that is one cheap CPU run away, and this commit is what makes that run informative. ⛔ AND THE 2^24 REAL-BLOCK RUN IS NOT NEEDED, which the doc comment now says so nobody schedules it later. The quantities split, and only the first is in question: socket WIDTH (main, aux) depends on the HasherKind alone static per tag idle socket HEIGHT (4 rows) the group floor static non-hash heights, 670,468,916 the workload socket-independent the 0.774x lever-0 ratio arithmetic over the above recompute `tenant_log_heights` overrides `h[HASH_SLOT]` only for ALGEBRAIC tenants and every non-hash height is socket-independent, so `RECORDED_WRAP_LOG_HEIGHTS` survives the pin move intact. What is stale is one width pair, the socket identity, and the ratio that is arithmetic over them. The stakes are in the doc too, because the direction matters: `wrap_tests` already puts the socket at 436 columns for RPO against the 28 of an idle `Test`, and this module's own note says mistaking the idle chip for a live one moves lever 0 from 0.774x to 0.632x — bigger, i.e. the flattering way.
…ve pin MEASURED at c8c7c03 on the box, CPU-only, env clean — `LFM_HASH` main columns by socket: Test 28, Rpx 316, Rpo 436, Poseidon 612, 3 ext aux throughout. Two things fall out that nobody had: the pinned socket is 316, not the 436 the RPO figure in `wrap_tests.rs` would have implied, and it is 11x the idle 28 rather than the 106x a BLAKE3 socket would have been. ⛔ AND NOTHING NEEDS RE-BLESSING. `the_blake3_tenant_socket_matches_the_record` was red because its assertion was wrong, not because its numbers were stale. Both obvious repairs would have been mistakes: - Re-bless the pair. No: `RECORDED = (28, 3)` is a faithful record of the BLAKE3 tenant, and that tenant did not change when the block path's pin did. - Point `BLAKE3_TENANT_SOCKET` at `BLOCK_HASHER`. No, and this is the one worth writing down. A tenant's socket width is a property of the build that PRODUCED the wrap proof, not of the build reading it. A byte-arm program emits no `Instr::Hash` and never consults the socket, so a BLAKE3-committing build has no reason to instantiate an algebraic one — `Test` is that build's own pin. Giving this tenant a 316-column socket would price a build nobody would ship, a socket paid for and never used, and would move the lever-0 baseline on the way past. The 0.774x stands, unrecomputed, because its inputs did not move. So the constant and the pair both keep their values and the assertion is replaced. It required assert_eq!(BLAKE3_TENANT_SOCKET, hash_pin::BLOCK_HASHER) which ties a COUNTERFACTUAL tenant to the CURRENT build — a category error a pin move was always going to expose, and `603c1e155` (2026-09-08) exposed it. What it was reaching for is checkable, and is now two assertions that can each fail. ✓ VERIFIED by reading: `hash_pin::BlockStarkHash = RpxStarkHash`, so `BLOCK_COMMITMENT_HASH` is `Rpx256`, and `WrapHash::production()` maps Rpo256/Rpx256/Poseidon to `Algebraic` — the production wrap EMITS `Instr::Hash` and USES the socket, so it is the RPX tenant and the BLAKE3 tenant is the comparison arm lever 0 is a ratio against. - `WrapHash::production() == WrapHash::Algebraic`. A commitment pin moved to a byte hash makes production a BYTE tenant: baseline and subject swap places and every ratio in this module needs re-reading before it is quoted. - some tenant is algebraic AND at `BLOCK_HASHER`. If the TENANTS table stops covering the pin, the census prices only builds nobody ships. The message prints the pin and the algebraic tenants so the failure names its own cause. The panel from c8c7c03 stays and keeps printing before any assertion, so a future red run yields numbers rather than a bare mismatch. Its measured widths are now in the doc comment, as is the reason the obvious cheap census cannot answer this question: `lfm_chip_census` is `lfm_chip_census_with_hasher(program, HasherKind::default())` and that default is `Test`, so it reports 28 under ANY pin. ⚠ The fork is recorded rather than hidden, because it is a modelling judgement with a campaign number attached: taking the other reading is two lines, `BLAKE3_TENANT_SOCKET = BLOCK_HASHER` and `RECORDED = (316, 3)`, and would put lever 0 near 0.757x — ? INFERRED, from a linear fit of the doc's own two points (28 cols -> 16 blocks/query, 2,980 -> 1,201) and then the algebra of its two stated ratios, never measured. The module's own gate recomputes that number from the tenant bills and prints it, so quote the gate and not this estimate. Either way it clears the gate's thresholds (> 0.4255, within 0.30..0.95).
`run_grind` declared its result `uint64_t` and handed the address to the kernel as `volatile unsigned long long *`. Those are the same type on Darwin/arm64 and different types of the same width on LP64 glibc, so on Linux the cast type-punned; with `#include "rpx.cu"` putting the whole kernel in this translation unit, GCC 13.3 at -O2 was free under TBAA to assume a write through `unsigned long long *` could not touch an `unsigned long`, and to keep `result` in a register across the inlined call. It did. `run_grind` returned UINT64_MAX for every input, so layer 8's two checks per vector that expect the SENTINEL passed VACUOUSLY while the two that expect a found nonce failed. Six rows, at every sha back to the gated base c00342c, on a target that passes on a clang/arm64 laptop where the two types coincide. Measured on the box at this sha: -O2 6 FAILURE(S) -O2 -fno-strict-aliasing ALL HOST KAT CHECKS PASS -O0 ALL HOST KAT CHECKS PASS None of it was ever a statement about the device grind. This file is a HOST replay of the kernel source through `cuda_host_shim.h` — no nvcc, no cubin, no device — so the defect was in the harness holding the result, not in the kernel it tests. The production path re-validates every device nonce with the host predicate, and the block pins read `host fallbacks 0` throughout. `crypto/math-cuda/tests/host_kat/` holds exactly one instance of the pattern and this is it: the shim's `atomicMin` takes `unsigned long long *` as a parameter, and the kernels' casts there only drop `volatile` from an already-matching type. Test-only; no production code and no proof bytes move. It also unblocks this lineage's CI `host-kat` job, which has been failing since the device grind landed. (cherry picked from commit 90a38ec)
…nstruments (env-gated off)
A WHIR run with no environment knobs set now reproduces the campaign's landed number (128.3 s on block 25368371) instead of a slower shape the launcher had to remember to correct. Two defaults move, both on the WHIR driver alone. FAN-IN 3, VIA A SECOND CONSTANT. `FAN_IN`'s doc has said since it was written that "the measured host peak decides; until it has, the conservative value stands". On the WHIR tree that peak now exists: the arity-3 tree reads 31.1-31.5 GiB against a 33.5 GiB gate with `device fallbacks 0` and `commit fallbacks 0` on every arm, and three is worth -8.05 s of interior card time (wt29-32, A/B/B/A). The constant's own criterion is met, so the default follows it. It follows it in a NEW constant rather than in `FAN_IN` itself. Both tree drivers read their arity as the fallback for `LFM_CENSUS_FAN_IN`, so moving the shared value would silently re-base every STARK tree number on record. `WHIR_FAN_IN = 3` confines the change; `FAN_IN` stays 2 and now says why it stays for a CARD reason rather than a host one — the STARK arity-3 interior node does not fit the device (ds15/ds16), which is a constraint the host peak says nothing about. The cost is that "one place to change" becomes one place per tree. TOP OVERLAP ON. `tree_top_overlap` takes the caller's default instead of hard-coding one, so the parse, the explicit `0`, the explicit `1` and the panic on anything else are still written once. The WHIR driver passes `true` — the lever measured -3.85 s alone (wt33-36) and -11.85 s beside fan-in 3 (wt37-38), with the 15 wrap `program_id`s and the `whir global IDENTITY` unmoved on both arms. The STARK driver passes `false`, which is what an unset knob already selected there, so its behaviour is unchanged. `LFM_CENSUS_FAN_IN` and `LFM_TREE_TOP_OVERLAP` still override on both drivers, with the same parse and the same 2..=4 bound. `0` remains the explicit off and is now the way back to the WHIR control arm, so a level-0 wall from this binary stays comparable to every earlier WHIR run by naming one variable. The WHIR level-0 banner prints on both arms for that reason; the on-arm line still begins `★ TOP OVERLAP:` exactly, so the gate that greps for it is unchanged. Scheduling and tree shape only. Nothing here touches a transcript or a challenge.
…the pure-WHIR landing Merges fix2/lean-program @ 965e13d into land/pure-whir @ 6a6e266. S1a read EFFECTIVE on FAST (job 223): the whole run 1.35 s faster, the big batches' early device rounds 1,527 -> 442 ms, the argue 1.43 s faster, every arm proved and verified with equal identities. The merge brings S1a's ancestry from gfs/a45 with it, every knob default off: A4 (LAMBDA_VM_ARGUE_LEAN_READS), A5 (LAMBDA_VM_ARGUE_LEAN_TAIL), the device GKR layer timers under LAMBDA_VM_BASE_SPLIT, and the S0 census test. One conflict, in stark's multilinear_table tests: both sides added tests at the same place (the preprocessed-prefix tests here, the argue-knob tests there). Both are kept.
LAMBDA_VM_ARGUE_LEAN_PROGRAM is now on unless set to 0, which is the opt-out and the old path exactly. Its WHIR A/B on the block (FAST, job 223, at 965e13d) read EFFECTIVE: - the whole run 1.35 s faster (band [-1.6, -0.5]); - the big batches' early device rounds 1,527 -> 442 ms, the argue 1.43 s faster, the other batches' rounds +8 ms, and the late rounds held (no S1b); - every arm proved and verified on the record's identities and census, and the untimed cross-check arm, which walks today's program beside every big session round by round, clean. The proof does not change. The program on demand is the same steps on the same operands in another order, so every round's values are the same field elements, and so are the transcript and every challenge. The stark identity test, the device parity test on the four big VM batches and the cross-check arm showed it. The round sums of a big batch are added over another launch shape, so their raw representatives, and a device proof's rkyv bytes, may differ, as between any two launch shapes. No pin moves. Only a batch whose lowered program holds more than 341 values a thread takes the path, and only on a device: the WHIR byte gate builds without cuda, and its EQ fixture holds 26. The W-LFM pins count the W-leg's permutations, operations and hints, which no argue path changes. No STARK path reaches the argue. A unit test pins that the knob reads its variable the default-on way (unset on, 0 off). A mutation restoring the old reading fails it.
MauroToscano
changed the title
Under pure WHIR the recursion proves its LFM programs with the base's argue, so the lean program's gate reaches their zerocheck batches too. A census of the W-LFM chips (the WHIR recursion chip set at the recursion's hasher, as whir_lfm_airs builds it) finds one big batch: LFM_HASH holds 365 values a thread today, a 61,286-thread ceiling, and 34 on demand, 657,930, at 41 % more steps. LFM_BITDEC holds 233 and stays under the gate. - every_w_lfm_batch_on_demand_is_the_same_program: host parity on every W-LFM batch, and LFM_HASH as the only big one. - the device parity test now finds its batches by the gate, over the VM's and the W-LFM's AIRs, and pins the five. - the_w_lfm_zerocheck_programs_and_their_live_sets: the printing census, ignored.
Both RPX implementations (prover lfm::rpo::Rpo256::mds, used by the block path's RpxStarkHash, and crypto::hash::rpx::mds) built each output lane with a core::array::from_fn closure. The closure's generic from_fn wrapper is placed in a codegen unit of rustc's choosing and is inlined into mds only when that unit happens to be mds's own. When it is not, every lane is an out-of-line call that recomputes (j - i) mod 12 with a 64-bit multiply per term: about a fifth more instructions per permutation. That is the two-speed host verify on the STARK tree. A Linux x86-64 cross build of the prover test crate at 8934b59, ef6d4be and 3fd644e shows mds inlined (2499 B, no calls) only at ef6d4be, the one FAST build, and twelve closure calls at the other two, the SLOW builds. Crypto's mds makes the twelve calls in its current partitioning too. Loops over a precomputed circulant compile the same way in every build. The permutation's values are unchanged: the RPO and RPX known-answer vectors, the two-implementation agreement test and a new test against the circulant definition all pass.
Under `parallel` the grind is `find_any`. It returns any valid nonce, 0 included, and the nonce it returns is absorbed, so every later state varies from run to run. Two tests assumed otherwise and were flaky there: - a_ground_proof_verifies asserted every spent nonce was non-zero, but nonce 0 passes an 8-bit PoW with probability 2^-8. - a_query_only_chain_checks_its_query_nonce_in_every_round accepted only Ok or GrindingRejected for a flipped query nonce. A flip that still passes the PoW is absorbed, moves the transcript and fails elsewhere. The tests now read the verifier's grind checks through a logging transcript that records each check's state and nonce: - A ground proof's checks are exactly its spent slots, in order, and each nonce passes the PoW at its own state. - A forged nonce is the first value above the honest one that fails the PoW at that state, so the check itself must refuse it with GrindingRejected. The three a_forged_*_nonce_is_rejected tests forged nonce + 1 and carried the same latent flake; they now take the same forgery. Tests only.
Two P2-W tests read a nonce that grinding picks with find_any under the parallel feature: one asserted it non-zero, the other expected a flipped query nonce that still passes the proof of work to verify. Both now assert what the proof of work guarantees. Tests only.
Every device entry point calls device::backend() before it touches the card. A process-wide, monotone count of those calls (backend_entries()) lets a test bracket a phase and show it never reached the device. The first user is the W-LFM prove's host prep, which LFM_CARD_AFTER_PREP=1 moves outside the card permit. This is one relaxed atomic add per backend() call, with no other change.
…REP, default off) prove_traces_whir_opening takes the card permit as its first statement, so the card is held idle, and closed to every other proof, while the prove builds its tables on the host. At job 222 that prep was 2.05 s of the pure-WHIR recursion's 9.89 s of W-LFM holds, 1.68 s of it at level 1. The prep moves unchanged into prep_whir_tables: the plan's layouts, each table's main columns moved into its layout, and the prefix check. It takes no device handle. LFM_CARD_AFTER_PREP=1 takes the permit after that function instead of before. Unset, empty or 0 keeps today's order; any other value panics. The setting is read once and named once on stdout. The split line's wall stays prep + the held part in both settings, so the wait for the card is in neither. Tests: - Laptop: the knob parse and the test override. - Box, #[ignore]: the fixture's wraps and a wide node, proved with the setting off and on, serially and three at a time with the permit armed, under the deterministic grind. Every proof must equal the default's bytes. - Box, cuda: device::backend_entries() must not move across prep_whir_tables for any job. The paired control requires that it moves across the prove that follows.
MauroToscano
changed the title
The W-LFM prove now takes the card permit after prep_whir_tables, so its host prep runs while another proof holds the card instead of holding the card idle. LFM_CARD_AFTER_PREP=0 restores the permit before the prep. Only the lock moves: card_after_prep_tests proves the same programs under both settings, serially and three at a time, to the same bytes. Measured on block 25368371 (FAST, A B B A): -0.65 s at fan-in 3 (job 234) and -0.90 s together with fan-in 4 (job 236).
An unset LFM_CENSUS_FAN_IN now selects WHIR_WIDE_FAN_IN (4) when level 1 is wide, which it is by default under the W-LFM prover. Fifteen epochs then make four wide level-1 nodes (4/4/4/3), and the block-artifact root takes them directly beside the global wrap, so the interior level is gone. The WHIR trees without a wide level 1 (LAMBDA_VM_LFM_PROVER=stark and LAMBDA_VM_LFM_WIDE=off) keep WHIR_FAN_IN (3), and the STARK tree keeps FAN_IN (2), so their shapes and program ids do not move. LFM_CENSUS_FAN_IN=3 restores the previous pure-WHIR tree. Measured on block 25368371 (FAST, A B B A): -0.70 s alone (job 235) and -0.90 s with the card permit after the host prep (job 236). The tree-shape and root tests gain fan-in-4 rows. The production root (15 epochs at fan-in 4) joins the honest control, the fixed-size schema and both L2G tamper tests.
On a wide tree, level 1 verifies epochs rather than proofs. With two to fan-in epochs there is one wide node and no proofs below it, so root option A, which takes level top-1's output, would hand the root that one node against a fold shape expecting one digest per epoch; the drivers' child-count assert then refuses the block. RootOption::for_tree maps A to B there, so the root sits above the single node. One epoch needs no mapping: its one node folds a single root to itself. Tests: for 1..=40 epochs at fan-in 2..=4 the children a wide tree hands the root equal what the option's fold shape refolds to, and A as named fails exactly at 2..=fan-in epochs; the root over every small wide tree (1..=6 epochs at fan-in 4) executes at the artifact's fixed width; the moved-L2G tamper test covers one epoch and one node of three.
Both WHIR tree drivers now run the root option through RootOption::for_tree, so a block of at most fan-in epochs composes under the default wide tree. Such blocks failed the root's child-count assert: up to 3 epochs at fan-in 3, up to 4 at fan-in 4. The 15-epoch block's tree is unchanged. The fixture tree becomes a body over a block (guest, private input, epoch size, arity and the epoch count the run must reach); the three-epoch fixture runs as before. the_whir_fixture_tree_proves_every_ small_block (box tier) proves 1..=6 epochs of a new guest, test_private_input_spin, whose private input sets its spin count and so its cycle count, each to a verified root at the default arity. the_spin_guest_lands_every_small_epoch_count executes the guest on the host and checks each input reaches its epoch count.
MauroToscano
changed the title
The WHIR production driver's arity bound becomes 2..=5 so that fan-in 5 can be measured: LFM_CENSUS_FAN_IN=5 puts 15 epochs into three wide level-1 nodes of five, and the root takes them beside the global wrap. The default stays 4. The two STARK drivers keep 2..=4: nothing above four has been costed on them, and their arity-3 node did not fit the card. The tree-shape test gains the fan-in-5 row (15 epochs: 2 levels, 4 nodes); the root's fold-shape tests run at fan-in 5 as well, and the fan-in-5 root (15 epochs, 3 nodes) joins the root gates' shapes.
WHIR_WIDE_FAN_IN becomes 5: fifteen epochs make three wide level-1 nodes of five, and the root takes them beside the global wrap. LFM_CENSUS_FAN_IN=4 or 3 opts out; the stark opt-out and LAMBDA_VM_LFM_WIDE=off keep fan-in 3, and the STARK tree keeps 2. Measured on block 25368371 (FAST, A B B A, job 238) against fan-in 4: -1.55 s (level 1 -0.76, root -0.70). Level 1's census falls from 1,052.8 M to 852.6 M cells and the root's from 270.9 M to 149.6 M (its hash table stays under 2^18). The W-LFM argue's reservation peaked at 24.3 GiB of the 25.7 GiB budget: 1.4 GiB of margin, so a block with heavier epochs should be measured before relying on five. The small-block fixture test runs at the new default: one epoch, one node of two to five epochs, and two nodes at six. The root tests gain the fan-in-5 root in the tamper arms and the small-tree execution test.
MauroToscano
changed the title
The WHIR_WIDE_FAN_IN doc comment, and b682091's commit message, read the RESERVED HW figures, which the tree log prints in MiB, as GiB by dividing by 1000. The W-LFM argue's reservation peaked at 24,342 MiB (23.8 GiB) of a 25,688 MiB (25.1 GiB) budget at fan-in 5: 1,346 MiB of margin, not 1.4 GiB. Fan-in 4 peaked at 21,754 MiB. The ratio, and so the claim, stands. Comment only.
When the card refuses a GKR fraction tree's carry and handing it back saves enough to be worth it, input_layer_tree_impl asks for one promise for the whole tree. If the budget refuses that too on the consume path, logup::resident_tree gets None and the per-table argue builds the table's factors and whole tree on the host: slower, never wrong, and until now uncounted. The refusal is now counted where it happens, in multilinear::gpu::gkr_tree_refusals and in math-cuda's argue-surface device_fallbacks, and logged as it happens. A prefetch refused the same way is not counted: it only means no prefetch, and the consume site asks again. The WHIR production tree prints "gkr tree refusals N" beside "device fallbacks N", which now includes it. DEVICE_FALLBACKS' doc names its six sites by function instead of line numbers that had moved, and says why the other argue-side reservations in multilinear::gpu are not fallbacks: the carry is speculative, a prefetch is optional, and reserve_room's two callers keep the work on the card. A test-only hand-back threshold (set_hand_back_threshold_for_tests) lets a table smaller than the widest precompiles reach the whole-tree promise. multilinear's call-site census pins the one counted site; math-cuda's keeps its five.
A box test (cuda, ignored, run alone) on an ADD table of 2^12 rows, whose factors go to the card. At the normal budget the card builds the tree and nothing is counted. With every carry handed back and the rest of the budget held by the test, a prefetch is declined uncounted, and the consume path's refusal reads one GKR tree refusal and one argue-side device fallback. The host's tree, the path the refusal hands the table to, has the card's output fraction.
stark's cuda feature does not turn on multilinear's, and without it upload_factors_from_columns is the host stub, so the table's factors never go to the card and the test cannot reach the tree. The first gate run failed on exactly that precondition. The test's doc, ignore reason and expect message now name the feature set to run it with: --features cuda,multilinear/cuda.
…_WHIR_HEAD_AHEAD) Before the WHIR base's producer starts, the head commits DECODE's univariate root on the host (about a second on the block ELF) and then its prepared commitment on the device. On FAST job 239's default arms, epoch 0 began executing 1.50 / 1.42 s into the base and the first card commit came at 2.62 / 2.55 s, with the card idle the whole time. Epoch 0 needs neither value to execute. Its preparation reads the root and its prove reads the prepared commitment. With LAMBDA_VM_WHIR_HEAD_AHEAD=1: - a helper thread computes the root while epoch 0 executes, collects and builds, and the preparation waits for it at its first read; - the prepared commitment keeps its place on the calling thread, so CUDA still comes up on the thread that proves, and the DECODE derivation count stays on that thread; - the observer hears the shared DECODE work from the consumer, before the first epoch it proves, instead of before the pipeline. Unset or 0 is the serial head, today's schedule. Anything else stops the run. Every committed value is the same: the root comes from the same host function of the ELF and the options, computed on another thread. Both settings stamp the head under LAMBDA_VM_BASE_SPLIT=1: its start, the root and the prepared commitment. Ahead mode also stamps epoch 0's wait for the root, so an A/B can split the head. A test proves a run serial and ahead under both preparation schedules and compares: - the DECODE root and prepared roots; - every epoch's bookend root, shapes, output and register fini; - the cross-epoch roots and the touched pages. It checks that the ahead bundle verifies, and that the observer hears the shared DECODE once, with the serial values, before any epoch is proved.
The WHIR base now computes DECODE's univariate root on a helper beside epoch 0 by default. LAMBDA_VM_WHIR_HEAD_AHEAD unset, empty or 1 runs the head ahead. 0 is the named opt-out: it runs the serial head, exactly as before. FAST job 241 (wt1030-1033, two arms each against the serial head): - epoch 0 began executing 1.03 s earlier; - the first card commit came 0.73 s earlier; - the base took 0.65 s less and the block 0.55 s less (40.65 -> 40.10 s); - level 1 was unchanged, and the program ids were unchanged; - epoch 0's preparation never waited for the root. The switch's test now pins the new reading, ahead unless exactly 0. The byte-identity test still proves both heads through the explicit parameter.
MauroToscano
changed the title
…default The wide lead-in's helpers claimed a node only once the base reported its epoch count, which it does when it executes its last epoch (t0+24 s at fan-in 5, 15 epochs). Nodes 0 and 1 had their epochs by t0+10 and t0+19, yet their prologues ran in the base's tail and finished after the base. A node whose epochs have landed AND whose next epoch has landed cannot be the run's last, so none of its epochs is final and its range is its full span. Those are the only things a prologue reads from the count. The helpers now claim such a node before the count and hand the builder the epochs known to exist, (k + 1)·span + 1; the builder then builds exactly what it would build with the count. The last node, and any run of at most fan-in epochs, never qualifies and still waits for the count. LFM_TREE_EARLY_CLAIM unset or 1 is the default; 0 waits for the count as before. The driver prints which one ran, and the lead-in prints a line per early claim. Measured on block 25368371 (FAST job 244, arms A B C C B A): the claim alone, against the default, whole run -0.50 s, level 1 -0.60 s, base +0.10 s; the 5 program ids unchanged. Card-free tests: the switch, the claim at the next epoch's landing, and the boundary (the last node and a one-node run wait for the count; without the claim nothing is built before the count). Box tier: the_early_claim_moves_no_node_byte proves the fixture's wide level 1 with the count and with the claim, and compares every node's program id, heights, published words and proof bytes.
…unt, by default" This reverts commit deb9726. Its A/B read -0.50 s (job 244), but at the landed head it measured no effect: 40.30 s with the claim and 40.30 s without it (job 245). The code stays on land/1010-early-claim and fix2/1010-early-claim.
MauroToscano
added a commit
that referenced
this pull request
Sep 30, 2026
Fills G6-LEDGER.md section 4 from job 249 (tags wt1200-1203) and sizes the SOTA levers c.3 (GPU trace generation) and c.5 (jagged PCS, real-row argue) against their measured terms. - The base card sits idle 7.50 s of 31.54 s (nsys arm). The idle splits as head 1.85, argue 4.27, open 0.53, commit 0.27 and global 0.29 s. - The trace upload is 35.6 GB of pageable H2D, 97 % of it serialized with no kernel alongside. The producer waits 9.6-10.6 s per run, so it is not on the critical path after the head. - Padding, corrected for a DECODE join error in the census: 13.62 % of the tables' cells, 27.43 % of the stack. The argue padded share is 17.04 %. - c.3 caps at 2.57 s. c.5 caps at 3.8-4.3 s gross, and only with stack chunks of 2^24 or smaller. - Triages the census's 17 consistency findings: 15 benign (an empty L2G trace built per epoch), 2 a DECODE join error, corrected in the note. Adds the box driver, the three analysis tools and the job's text output (secrets-scanned).
MauroToscano
added a commit
that referenced
this pull request
Sep 30, 2026
The process pool kept its two 3.22 GB slots for the life of the process. On #1010's production tree the host peak is in level 1 (16.2 GiB against the base's 9.6), where no epoch needs a slot, so kept slots would add all 6.4 GB of them to the whole run's peak. D-TRACE-1B §3.4 sized the base's peak only. SlotPool::release_free frees every block nobody holds; a later fill makes them again, and until then a lease misses as not ready. The WHIR base calls it on a helper as soon as the last epoch is proved, beside the cross-epoch proof, and joins the helper before it returns (PINNED SLOTS: released … line). Tests: releasing frees only unheld blocks, a held block survives and comes back, the next fill remakes them (heap blocks, laptop); the one-slot pipeline test now asserts the slot is back and released after the run.
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 made it fast, ranked
These are the optimizations that took block 25368371 from 104.2 minutes to 40.20 s, ranked by the speedup each
measured when it landed. Each row is its own before/after at that time, so the rows do not add up.
¹ The move also changed the hardware, from a CPU box to one RTX 5090 on a Ryzen 9950X host.
² On a Ryzen 9950X + RTX 5090 box. The base alone fell from 156.3 to 67.9 s.
107.45 s, STARK 157.45 → 121.65 s. On STARK the caps add no wall on top of the 2^d folds, though they remove
another 1.4 M permutations.
161.4 s, 18 Sep), and is 1.52× faster today (40.20 against 60.95 s). Rows 6, 9, 10 and 12, and most of 14, are
WHIR-only; row 7 and the one-row openings are STARK-only.
11.2× and 6.7× on 28 Sep.
The number
Block 25368371 on the FAST box (Ryzen 9 9950X, RTX 5090 32 GB), RPX commitments, 15 epochs at 2^21. At this head,
33232d688(this head,9e2728955, has the same tree), the two default arms of the last ABBA read 40.1 s and40.3 s (mean 40.20 s). Host peak 17.3 GiB,
device peak 27.1 GiB (27,794 MiB).
Each step below is its own ABBA on one binary: two arms per setting, alternated.
d1dc455145f15641b94ab853c6cb682091a3¹ Measured on its stage branch (
34c17603b), before P2-W and A1.² Two builds, alternated X XF X XF, at
6a6e26611: the MDS fix has no knob.In the third row's A arms, every fix in the next table is switched off by its opt-out. Their program ids and census equal
those before the batch (
668a89a4c). The one change with no opt-out of its own, the WHIR encoding through the engine,is in both arms. A fifth arm, the defaults with only the level-0 lead-in off, read 61.4 s, so the lead-in is worth
−1.20 s here. The STARK PR (#1009) measured the same batch at −28.75 s (107.55 → 78.80 s).
The gap fixes
Each fix was measured first in its own ABBA, mostly on the base before the engine. Those rows do not add up to the
cumulative −39.65 s; the last row above is the measurement.
LAMBDA_VM_ZF_WHIR_STACK=25LAMBDA_VM_RPX_LIMB_PERMUTE=0LAMBDA_VM_RPX_GRIND_QUEUE=0LAMBDA_VM_BASE_PREP_ON_PROVER=1LAMBDA_VM_LFM_KEEP_BITWISE=1LAMBDA_VM_RPX_WARP_MERKLE=0LFM_TREE_PROLOGUES_AT_LEVEL0=1d1dc45514LAMBDA_VM_WHIR_FOLD_CLASSIC=1LAMBDA_VM_STAGING_SHARED_SLAB=1LAMBDA_VM_NO_WHIR_FUSED_FOLD=1,LAMBDA_VM_WHIR_LEAN_ROUNDS=0LFM_TREE_REDERIVE_DECODE=1LAMBDA_VM_LDE_LEGACY=1, which also reverts every other LDELAMBDA_VM_DEEP_INV_LEGACY=1LAMBDA_VM_NO_WHIR_ROOM_PARK=1,LAMBDA_VM_NO_WHIR_ROOM_RESIZE=1LAMBDA_VM_LFM_HASH_SPLIT=1turns it onAlso in the batch, with no knob:
Grinding only before the queries (P2-W)
What changed. Each round of a WHIR base chain used to grind 20 bits before three challenges: the first folding
challenge, the out-of-domain batching challenge γ and the query positions. It now grinds before the query positions
only.
1,472.
whir_grind, defaultquery; the banner reads… whir_stack=27 whir_grind=query.The proof carries only the nonces it spends (
NonceLayout::Spent).1,036 fewer a block.
nonzero value in a field the format does not carry.
Measured on block 25368371 (FAST, one binary, arms A B B A, wt820–823):
LAMBDA_VM_ZF_WHIR_GRIND=allpredicted from the grind count.
Soundness: no proven bits are lost. Of a round's three grinds, only the query grind raises the proven minimum as
placed:
challenge by varying that message, without grinding again, so this grind earned no credit.
with no grind at all.
Every phase keeps its bits:
security/zisk_calc.py).[0,0,20]against[20,20,20]), so a proofground one way does not verify the other.
red.
Opt-out.
LAMBDA_VM_ZF_WHIR_GRIND=allrestores the grinds before all three challenges and the three-nonce format:the previous proofs, program ids and census, byte for byte. Golden tests on the chain programs, arenas and host proof
bytes pin it, and so does the A arms' match above.
The argue's short, wide tables on the GPU (A1)
What changed. In the WHIR base's argue, a table whose columns are already resident on the card is now valued there
once it holds 2^16 cells (width × rows). Before, each column needed 2^16 rows. The few columns left on the host are
walked across the thread pool.
fall from 24,195 to 3,478 a block.
Measured on block 25368371 (FAST, one binary, arms A B B A):
LAMBDA_VM_ARGUE_DEVICE_COLUMNS=093a2b5643, wt831–834)8930490e5, wt850–853)The whole saving is in the base (41.90 → 40.95 s in the stage's ABBA); level 0 and the interior stay within noise.
Soundness: the proof does not change. The card computes each column's multilinear value exactly, the same field
element the host computes, so the transcript, every challenge and the serialized proof are identical, and so are the
program ids and census.
LAMBDA_VM_ARGUE_XCHECK=1) re-evaluated every card value on the host: 30,086 of 30,086 matched.on the card; a wrong card value is refused.
Opt-out.
LAMBDA_VM_ARGUE_DEVICE_COLUMNS=0restores the height rule and the one-at-a-time host walk, line for line.The argue's challenge tables on the GPU (A2+A3)
What changed. The WHIR base's argue built its challenge-dependent tables on the host and uploaded them: the
zerocheck's
eq(r)andeq(row)weights, and the claim reduce's shift tables and batched columns. It now builds themon the card from the columns already resident there.
eq(α)table; each batched column is one kernel over theresident columns.
pageable uploads a block (1.16 s of copies).
Measured on its stage branch (
34c17603b, before P2-W and A1; wt836–839): A 59.65 s (59.5, 59.8) → B 54.45 s(54.4, 54.5), −5.20 s. The base fell 41.65 → 36.65 s and the argue 19.7 → 14.7 s; the card built 1,364 tables an
arm.
Soundness: the proof does not change. The card builds the same field elements the host built, so the transcript,
every challenge and the serialized proof are identical.
LAMBDA_VM_ARGUE_XCHECK=1) compared every card table with the host's before its first round.the fault inert fails that test.
Opt-out.
LAMBDA_VM_ARGUE_DEVICE_TABLES=0builds the tables on the host and uploads them, as before.Pure WHIR recursion
What changed. The recursion's LFM proofs (the global wrap, the nodes and the block-artifact root) are proved by the
base's own stacked-WHIR prover instead of one STARK per table. Each parent verifies a child with the WHIR verifier the
wraps already run, over the child's LFM statement.
three times, then the node's own bindings and publishes. The 15 wraps and their proofs are gone. With three epochs a
node, the tree's fan-in, the node schema, the root's L2G fold and every level above are unchanged.
own point. The main stack holds the value columns only.
harvests and the emission.
global wrap's program is the same one.
Measured on block 25368371 (FAST, one binary per row, arms A B B A):
4150afab6, wt860–863)6a6e26611, wt880–883; A =LAMBDA_VM_LFM_PROVER=stark)against the wraps' 7.4 s, the interior 1.8 s against 9.0 s, the root 1.0 s against 1.4 s.
≥ 4. The base is 9 s faster than when that row was set, which leaves the two helpers a 4.7 s tail. The property the
count stood for held: the GPU's first hold came 0.17 s after level 1 started.
Soundness: every phase keeps ≥ 128 proven bits, and the recursion's minimum rises.
stacks of 2^24–2^27. Their minimum is 130.393 bits, the n = 27 first fold, unground, the same as the base's. It
replaces the STARK recursion's 128.946 bits, which came from its LFM query phase. Measured by the calculator on each
run's own chain lines.
statement built from the AIR's column list would count zero and bind nothing: a forged program would verify.
statement. The sponge receives each as a base token, so a non-canonical upper lane is unprovable.
next one's INIT, each epoch at its tree position. It reads these from what the wraps would have published. Its L2G
item is the fold of the epochs' bookend roots, the fold a node over those wraps takes.
AIR's count. A forged instruction column is refused by the prepared opening. A deleted opening, a restated table
height, a tampered or reordered public word and a prepared root absorbed after
zare each refused.that nothing settles are each refused.
disagreeing attestation id are each refused, each beside a control without the bindings that executes.
verifies with the count at zero and is refused with the AIR's count.
Opt-outs.
LAMBDA_VM_LFM_PROVER=starkrestores the per-table STARK recursion. The A arms above print8930490e5's 24 programids byte for byte.
LAMBDA_VM_LFM_WHIR_PREP=bothalso keeps each table's instruction columns in the main stack.LAMBDA_VM_LFM_WIDE=offkeeps the wraps under the WHIR recursion.Narrow sumcheck rounds on demand (N1′)
What changed. In the WHIR argue's zerocheck, a big batch's device rounds now walk its program on demand.
Each step is emitted where the step that uses it first needs it, in Sethi–Ullman order: of two operands, the one
needing more values goes first.
Every read, a column's value or a constant, is emitted again at each use instead of once and held.
The steps are the same operations on the same operands. What changes is how many values a thread holds at once,
which sizes the round kernel's per-thread slot file and so how many threads a round can run.
The slot file is also sized for every interpolation node from the first round.
A batch is big when its program holds more than 341 values a thread, which leaves a round under 64 k threads at the
512 MiB slot budget. Five batches are big:
Every other batch keeps its program as it was, the byte gate's EQ fixture (26 values) included.
Measured on block 25368371 (FAST, one binary):
LAMBDA_VM_ARGUE_LEAN_PROGRAM=0965e13de2, wt890–894)a28ad36af, wt910–914)Where the gain lands: the base.
fell 1.28 s.
2 of 5 programs are ready, and the card waits in the gaps between them, so the saving does not reach the wall.
column values instead of 331, over up to ≈ 4 GB of columns.
Soundness: the proof does not change. The program on demand is the same steps on the same operands in another
order, so every round's values are the same field elements.
and the census: equal in every arm of both runs.
LAMBDA_VM_ARGUE_XCHECK=1) walked the old program in a shadow session over the same card-residentvalues. It compared every big session's rounds, round by round, in the base and in every W-LFM proof, and every one
matched.
BatchMismatch), and by the cross-checkbefore a proof exists (
DeviceFailed);Opt-out.
LAMBDA_VM_ARGUE_LEAN_PROGRAM=0keeps every batch's program as before and sizes the slot file for onethread an index, line for line.
The RPX MDS compiled the same way in every build
What changed. Both RPX implementations compute the MDS over a compile-time circulant with plain loops, instead of a
core::array::from_fnclosure. The closure's wrapper was inlined only when rustc's codegen-unit partitioning placed itin
mds's own unit; otherwise each output lane was an out-of-line call. That made the host's hashing about 20 % slowerin some builds than in others, decided by unrelated edits.
Measured at
6a6e26611(two builds, X XF X XF): −0.50 s (45.65 → 45.15 s). The executor's hashing runs at0.81 of its old time per permutation; most of the gain is in the base (−0.30 s). The STARK PR (#1009), where host
hashing sits on more of the critical path, measured −5.95 s.
Soundness. The same values: the RPO and RPX known-answer vectors, the two implementations' agreement test and a new
test against the circulant's definition pin it, and transposing the matrix fails six of them. No knob.
The card permit after the host prep, and fan-in 4
What changed.
them, the prefix check) is host-only work. It used to run inside the exclusive permit, with the card idle and locked:
1.68 s of level 1's card holds at job 222. It now runs while another proof holds the card.
the block-artifact root takes them directly beside the global wrap.
prove and +0.3 s in its emission, census and build.
LAMBDA_VM_LFM_PROVER=stark,LAMBDA_VM_LFM_WIDE=off) keep fan-in 3, and the STARK tree keeps 2.Measured on block 25368371 (FAST, one binary per row, arms A B B A):
533a22926, wt960–963)5f15641b9, wt970–973)533a22926, wt980–983)because the wall replicated: the whole-run row hit its pre-registered band in all three, each beyond its A arms'
spread (0.20 s).
and the tree takes the fan-in-4 shape.
Soundness: nothing a proof commits to changes. The tree's shape does change, and the verifier already takes any
arity.
three at a time, give the same proofs (
card_after_prep_tests). The prep never enters the device layer: every entryinto it is counted. The first A/B's program ids are equal across A and B.
root's L2G fold regroups the global wrap's roots exactly as the interior did. The root gates now include pure WHIR's
root (15 epochs at fan-in 4) in:
fallbacks. The root still publishes 180 words.
Opt-outs.
LFM_CARD_AFTER_PREP=0takes the permit before the prep. The proofs are the same.LFM_CENSUS_FAN_IN=3restores the previous pure-WHIR tree and its nine program ids.Fan-in 5
What changed. The wide pure-WHIR tree defaults to fan-in 5.
beside the global wrap.
LFM_CENSUS_FAN_INbound widens, to 2..=5. The STARK drivers keep 2..=4: nothing above fourhas been costed on them.
starkopt-out andLAMBDA_VM_LFM_WIDE=offkeep fan-in 3, and the STARK tree keeps 2.Measured on block 25368371 (FAST, one binary per row, arms A B B A):
8b2896c59, wt1000–1003)b682091a3, wt1010–1013)falls from 1.9 to 1.2 s.
270.9 M to 149.6 M cells.
The device peak after the base was 25,586 MiB.
slower, never wrong.
counted since
7650b53c7(a declined prefetch is not a fallback). The production tree at fan-in 5 reads 0refusals and 0 fallbacks.
LFM_CENSUS_FAN_IN=4is the opt-out.Soundness: nothing a proof commits to changes except the tree's shape, which the verifier takes at any arity.
node at two to five, two nodes at six.
Opt-outs.
LFM_CENSUS_FAN_IN=4restores the fan-in-4 tree and its six program ids.LFM_CENSUS_FAN_IN=3restores the fan-in-3 tree and its nine program ids.The WHIR base's head ahead
What changed. The WHIR base computes DECODE's univariate root on a helper thread, beside epoch 0, instead of
before the pipeline starts.
leaves over DECODE's columns), then the prepared DECODE commitment on the device. Only then did epoch 0 execute.
the thread that proves, and the DECODE derivation count stays on that thread.
it heard it before the pipeline. The level-1 lead-in reads it at its first claim, in the base's tail.
LAMBDA_VM_BASE_SPLIT=1: its start, the root, the prepared commitment and epoch 0'swait for the root.
Measured on block 25368371 (FAST, arms A B B A; all rows but the last are the decision A/B at
d117ffedd,wt1030–1033):
33232d688, wt1060–1063; A =LAMBDA_VM_WHIR_HEAD_AHEAD=0)executed.
waited 0.00 s.
1.10–1.11 s. Its collect, sharing the CPU with the root, grew from 0.32 to 0.52–0.54 s.
chain starts earlier.
Soundness: the proofs are byte-identical by construction.
The same values, only earlier. The root is the same pure host function of the ELF and the options
(
commitment_from_elf), computed on another thread. The prepared commitment is unchanged and committed in the sameplace. Epoch 0's preparation receives the same root. Only where and when the root is computed changes, never what
any proof commits to.
The test.
the_head_ahead_proves_what_the_serial_head_provesproves a run serial and ahead, under bothpreparation schedules. It compares:
It checks that the ahead bundle verifies, and that the observer hears the shared DECODE work once, with the serial
head's values, before any epoch is proved. It passed on the CPU build and on FAST's device build.
What the test does not compare: an epoch's first group root. Its rows follow
HashMaporder, so it differsbetween any two proves. The existing preparation-schedule test skips it for the same reason.
The tree: the 5 program ids are equal in all four arms and equal to the fan-in-5 landing's.
Opt-out.
LAMBDA_VM_WHIR_HEAD_AHEAD=0restores the serial head, with the same program ids. Any other value stopsthe run.
What is in the branch
for the block.
(−8.3 s).
inside level 0's pool, saved −11.9 s. Together they took the block to 128.3 s.
ZfFormat(prover/src/zf_format.rs) parses sevenLAMBDA_VM_ZF_*knobs once and prints oneZF FORMAT:banner. The default iscap=auto whir_cap=auto fri=dp one_row=0 whir_folds=first6 whir_stack=27 whir_grind=query.end of each tree's first path, so the proof structs are unchanged.
chain.
8–11 of 2^25.
whir_grind, defaultquery: one grind and one nonce a round inthe WHIR chains; see "Grinding only before the queries" above.
LAMBDA_VM_ZF_ONE_ROW=auto) are built on host, on the GPU andin-guest, but are off here: they cost +3.2 s on this pipeline. They are on in the STARK pipeline's PR (STARK recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 60.95 s #1009).
ZfFormat::LEGACYstays pinned by a golden test. The RV64 recursion guestverifies only the legacy format.
crypto/math-cuda/src/lde_cm.rs,kernels/ntt_cm.cu).zero fill, and a transpose before a row-major commit.
launch in registers and shared memory, so a 2^22 transform is three passes. The coset spread is fused into the
first pass, and the output is column-major, so the commits lose their transpose.
commit's encoding. LDEs that keep a host copy (below 2^19 rows) stay on the old path.
LAMBDA_VM_LDE_LEGACY=1sends every LDE back to the per-level pipeline.gap-fix/ntt(da2da9d93),gap-fix/wbatch-int(7e3eac501),gap-fix/harness(f81f0a80f),gap-fix/rec-int(c679a771b),gap-fix/stack-int(8c2450ff6) andgap-fix/idle-a-int(d3c76d2ed), eacha signed merge;
gap-fix/idle-b-int(bdb2d37b6) andgap-fix/hash-int(e041e9fb0), each a signed merge;gap-fix/kern-int, one commit (d1dc45514).the stack.
9cea599a3(the nonce layout, default off),ce292de3e(the default)and
b4506b719(comments).93a2b5643(behind its knob), merged asc7228f310, and8930490e5(the default).34c17603b, merged as7364d1292, andb9698b05d(thedefault).
whir/full-recursion(4150afab6), merged as3722e7376;70cdb3719(its pins under P2-W)and
6a6e26611(the default).1177d5a13(the census) and965e13de2(behind its knob), merged as06d2d48e8;26adbf501(the default) anda28ad36af(the W-LFM parity tests). The merge also carries two argue knobswhose A/Bs read MECHANISM-ONLY,
LAMBDA_VM_ARGUE_LEAN_READSandLAMBDA_VM_ARGUE_LEAN_TAIL, both off.d61a3c729) and deterministic whir_chain grind tests (d6648e653, merged as5f15641b9).1e3c39d5e(a device-entry counter),533a22926(behind itsknob),
78781f7cf(the default) and4ab853c6c(the pure-WHIR tree's default fan-in 4).529589d9d(a tree of one wide level runs root option A as option B) and61b025b7d(a spin guest anda test that proves 1 to 6 epochs to a verified root). A block of 2 to fan-in epochs used to stop at the root's
child-count check; block 25368371's tree is unchanged.
e783f29d5(the WHIR driver takes fan-in 5 fromLFM_CENSUS_FAN_IN) andb682091a3(the default).d117ffedd(behind its knob) andeb20fe04f(the default). The GKR tree'srefusals counted:
fd3146a0b(the fan-in-5 margin quoted in MiB),7650b53c7(the counter),a28690b7f(itsforced-refusal test) and
4593752a7(the test's feature note). Merged as33232d688.deb9726b3, reverted by9e2728955(this head, whose treeequals
33232d688's). Its A/B read −0.50 s (job 244), but at the landed head it measured no effect: 40.30 s with theclaim and 40.30 s without (job 245). Level 1 gained ≈ 0.2 s and the base paid it back.
main: perf(alloc): compile jemalloc's never-purge policy into the binary #996 (jemalloc never-purge compiled into the CLI).Soundness
Query counts and blowup are unchanged.
The format levers
cap node the query index selects. Path lengths are checked exactly, including at c = 0.
changes, in a term that stays more than 50 bits below the dominant one.
layout Plonky3 uses. The query index is uniform over the whole domain.
fewer rounds, and queries stay 112 per round.
The gap fixes
all take the layout from
global_layout(shapes, cap), never from a proof.table. It stays 112 at every production shape.
security/zisk_calc.py): the WHIRchain minimum is 130.393 bits at 27, against 130.926 at 25. With the per-table STARK recursion
(
LAMBDA_VM_LFM_PROVER=stark) the pipeline minimum is 128.946 bits, set by the query phase of every LFM proof; withthe default pure WHIR recursion it is 130.393 bits (see "Pure WHIR recursion").
message, so a cheating prover can re-draw α₁ by varying h₁ without grinding again. The bits above are the unground
ones. P2-W drops the folding and out-of-domain grinds (see "Grinding only before the queries"); K4 changes only how
the card searches for the nonce.
sender, its honest multiplicities are all zero and the table constrains nothing.
instantiated chip's interactions, stored in the artifacts and folded into
program_id, and the verifier re-checksit against the mask it was handed. No proof supplies it.
LAMBDA_VM_LFM_KEEP_BITWISE=1reproduces the legacy registry digests.emissions compute the same field value on accepted and on tampered chains (tests). The WHIR wrap program ids move.
program_idand never read from aproof. Tests refuse a forged tail root, the single-table door and a wrong chunk root.
parity through either staging, on the card;
reference, and the fault suite under both settings.
the 64-bit multiply. Its bytes were shown equal three ways:
with a failing control). It also replays the cooperative kernels lane by lane (the half-warp Merkle kernels and
the queue grind) against the shipped ones. CI runs it on every PR;
path and, where cheap, against the host oracle (
rpx_device_paths);Fixed along the way
tables, which rejected honest proofs that publish values.
failed, the error was dropped, and every such commit fell back to the host; the base took 647 s. The grid now splits
into z, and device commit and tree errors are logged and counted.
source codeword dropped.
GPU.
Gate and CI
The head ahead and the refusal counter were gated at this head,
33232d688, on the FAST2 box: 14 steps, all green(the lib suite 1,634 / 0 / 96). Besides the standard steps:
LAMBDA_VM_WHIR_HEAD_AHEAD=0, each with the fan-in-5 landing's 5program ids;
A supplementary gate ran the per-table argument's suite on the card, 5 steps, all green. An audit found that the
suite's earlier gate line (
-p stark --features cuda) ran multilinear's host paths only: stark'scudadoes notturn on
multilinear/cuda. The supplement names both features and requires every device arm's own output line.Fan-in 5 was gated at
b682091a3, on the FAST2 box: 15 steps, all green (the lib suite 1,631 / 0 / 96).Besides the standard steps: the root, tree-shape and knob suites; 1 to 6 epochs proved to a verified root at the
default (fan-in 5), under
LAMBDA_VM_LFM_WIDE=offand understark; the fixture tree to a block artifact; and theproduction tree four times, at the default (its 5 program ids), under
LFM_CENSUS_FAN_IN=4(4ab853c6c's 6), underLFM_CENSUS_FAN_IN=3(5f15641b9's 9) and underLAMBDA_VM_LFM_PROVER=stark(the STARK recursion's 24).Small blocks was gated at
61b025b7d, on the FAST2 box: 12 steps, all green (the lib suite 1,631 / 0 / 96),including 1 to 6 epochs proved to a verified root at the default, under
LAMBDA_VM_LFM_WIDE=offand understark, andthe production tree's 6 program ids unchanged.
The permit after the prep and fan-in 4 were gated at
4ab853c6c, on the FAST2 box: 14 steps, all green (thelib suite 1,628 / 0 / 95). Besides the standard steps: the permit's byte gate and device-entry gate, the fixture tree at
the new defaults and under
LFM_CARD_AFTER_PREP=0, and the production tree three times, at the defaults (its 6 programids), under
LFM_CENSUS_FAN_IN=3(5f15641b9's 9) and underLAMBDA_VM_LFM_PROVER=stark(the STARK recursion's 24).N1′, the MDS fix and the grind tests were gated at
5f15641b9, on the FAST2 box: 21 steps, all green (thelib suite 1,625 / 0 / 94): the standard six, N1′'s 13 (card parity on the five big batches, the whole argument's
identity and its negative control, the slot-budget pin, multilinear's lib at the default and under the opt-out, and the
byte gate for both hashes and under the opt-out) and the MDS fix's 2 (the RPX suites).
Pure WHIR was gated at
6a6e26611, on the FAST2 box: 14 steps, all green (the lib suite 1,622 / 0 / 92). These are the standard steps,plus the WHIR recursion's prover, verifier, leg, wide-node, switch and lead-in suites on the card with their negative
tests, the fixture tree at the default and under the opt-out, and the opt-out's byte gate: the production tree under
LAMBDA_VM_LFM_PROVER=starkprints8930490e5's 24 program ids.A2+A3 was gated at
b9698b05don FAST2: 17 steps, all green.A1 was gated at
8930490e5, on the FAST2 box (the second RTX 5090): 14 steps, all green. These are thestandard steps, plus A1's device tests, the whole argument's identity and its negative control, the multilinear suite at
the new default and under the opt-out, and the WHIR byte gate on both hashes and under the opt-out.
P2-W was gated at
b4506b719on the FAST box: 11 steps, all green. These are the standard steps, plus themultilinear suite, the WHIR chain gates with their production-shape emissions, the WHIR byte gate on both hashes, and
the WHIR epoch verifier programs under the opt-out.
The batch was gated at
d1dc45514on the FAST box: 81 steps, every one at its exact pre-registered count.The standard steps:
The 75 targeted lines cover:
the room on the card;
tests;
For each switch of the last two rounds, a gate line runs each setting and reads the banner its process printed. The
previous candidate without K6 (
41549ebad) passed its own 70-step gate. The cumulative ABBA in the first table ranafter the gate.
In CI at
d1dc45514, these pass: lint, the host known-answer tests (including the RPX lane-by-lane replay), the provertest build, the stark cuda-feature tests, and the CLI and executor tests. The spec structure check fails on a key the
spec tooling does not know (
spec/src/blake3.toml:constants). The prover shards were still running when this waswritten.
Open decisions
b4506b719). Since then this PR added the WHIR-sidefixes (A1, A2+A3, pure WHIR, N1′, the permit after the prep, small blocks, fan-in 5) and STARK recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 60.95 s #1009 the STARK-side ones
(R1b, F-SIDLE, NICE v2); both carry the MDS fix. The shared defaults differ in the recursion prover (WHIR here, STARK
in STARK recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 60.95 s #1009),
one_row(off here, auto in STARK recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 60.95 s #1009) and the LFM_HASH split (off here, on in STARK recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 60.95 s #1009). A per-pipeline defaultwould let one PR carry both.
LAMBDA_VM_MEMPOOL_RELEASE_MB=0, which releases thedevice memory pool; the code's default retains it. Retaining measured −4.50 s on this pipeline before the engine, but
only −0.45 s at the current head (inside noise), so this PR keeps reporting with the release. The STARK PR (STARK recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 60.95 s #1009)
measured −2.00 s and reports with the retain.
budget at 27. A block that adds one polynomial to such an epoch moves that argument's reservation to the host:
counted, proof unchanged, slower. The device peak at this head is 27,794 MiB (the highest of the last ABBA's four
arms) of the card's 32,607 MiB. Worth a run on a heavier block before relying on 27 there.
Fan-in 5 leaves level 1's argue 1,346 MiB under the same budget; the same run would check it.
keeps 128 bits.
iteration.