Repository navigation
STARK no-epoch (prove-and-retire) prover: block 25368371 — work in progress - #1013
Draft
MauroToscano wants to merge 1459 commits into
Draft
MauroToscano wants to merge 1459 commits into
MauroToscano wants to merge 1459 commits into
Conversation
|
Benchmark Results for modified programs 🚀
|
|
Benchmark Results for unmodified programs 🚀
|
MauroToscano
added a commit
that referenced
this pull request
Oct 2, 2026
On block 25368371, 10 of 11 LT tables come from finish's phase 3 (LT ops derived from MEMW and MEMW_A), about one group of cells in phase A's tail. Each MEMW op's LT ops depend on that op alone, so WindowedTraceBuilder::stream_memw_lt derives each window's as the window arrives, into the window's LT list, and LT's full chunks stream with them. StreamSkip counts the MEMW/MEMW_A ops already converted, and phase 3 derives LT only from the ops past them. Block path only, under the lead's ruling: the LT ops are the whole-run build's in another order (a window's MEMW-derived ops follow its walk's), so a chunk holds other ops than the whole-run chunk at that index. LT deduplicates per chunk, but every op keeps its whole-run multiplicity summed over the chunks, which is what LT's constraints and the bus see. The whole-run order, and so every epoch proof, is untouched. For a given window length the chunks are a function of the run. Off unless called. Test: with it on, every table but LT is the whole-run build's; LT has as many chunks and the same op multiplicities summed over them; dropping one row of one chunk breaks that (the mutation); and more LT chunks stream. Cherry-picked from noepoch/windowed-builder 074b772 onto #1013's builder, without the KECCAK_RND streaming it sat on (f5a3503): #1013 chunks KECCAK_RND through MaxRowsConfig::keccak_rnd instead.
MauroToscano
added a commit
that referenced
this pull request
Oct 2, 2026
… leaves The builder kept every walked window until finish, so at the run's end all of its op lists were resident, about 300 B per cycle (0.28 GiB per M cycles: 8.6 GiB on block 25368371 and about 100 GiB on a median mainnet block). WindowedTraceBuilder::drop_streamed_ops keeps only the ops not yet in a handed-out chunk for each of the 8 streamed tables (Tail: the windows' lists moved in whole and freed once used up). As a chunk leaves, the builder takes what the table phase would have read from its ops. It counts BITWISE's lookups from LT, SHIFT, STORE, MEMW_A and MEMW_R, plus DECODE's lookups and the last ECALL from CPU. It derives and keeps the phase-3 LT ops of MEMW and MEMW_A, unless stream_memw_lt already put them in the windows' LT lists. The other walk lists are appended window by window instead of being concatenated at finish. The in-walk BITWISE lookups are counted and dropped. finish runs the table phase over the tails (StreamSkip::tails), padding the dropped CPU chunks and placing the kept LT ops where phase 3 would have derived them. The tables are the same. The new tests compare every table with the whole-run build, and with stream_memw_lt every table with the builder that keeps its windows, plus LT's multiplicities. Both go through push and the split, at window lengths 1 to the whole run, and with chunks small enough that all 8 tables drop. The same comparison runs with KECCAK_RND streamed. Another test checks that after each window each table holds less than a chunk of ops. Removing any one accounting step (LT, MEMW_R or DECODE counts, the CPU padding, either LT prefix) fails the first test. Off by default. Cherry-picked from mem/m1 74e1df1 onto #1013's builder: no streamed KECCAK_RND here (KECCAK_RND chunks are built by finish from the run's keccak ops, which dropping keeps), so its test checks the MaxRowsConfig::keccak_rnd split against the whole-run build instead.
MauroToscano
added a commit
that referenced
this pull request
Oct 2, 2026
mem/stark-flip (narrow storage: the M3a/M3c/M3b chain, on by default, with the BLOCK MEM measurement knob) on top of E1's lean walk and E4's paged executor memory. One conflict, in executor/src/vm/memory.rs: Memory::heap_bytes (BLOCK MEM's executor term) now reads E4's store, the pages and their directories, or the word map under LAMBDA_VM_EXEC_MEMORY=words.
MauroToscano
added a commit
that referenced
this pull request
Oct 2, 2026
…rge 3be24ab The packed KECCAK_RND / LT builds, the queue, finish, generator, purge and drain-purge knobs, the in-flight BLOCK MEM terms and phase 4 in slices, on #1013's head with E1 and E4. One conflict: both sides appended a test to windowed_builder_tests.rs (E1's lean-walk identity test and the stream's generator test); both kept.
…the segments' A arm) StreamSkip::concat_lt / WindowedTraceBuilder::concat_lt: phase 3 extends one LT list with every segment, as it did before 5d4cca3f8, for an in-run A/B of the segments' memory and time at the median. The tables are the same (the finish-pack builder test also runs this arm).
Each BLOCK MEM line now carries /proc/self/stat's minor faults (millions): a fresh page's first touch. BIG 104 read phase B 6.3 s slower at the median when the finish leaves 15 GiB fewer freed pages resident; this counts the faults per phase to confirm or refute that mechanism. Measurement only.
… committers The interface for committing the tables the block's finish builds while the finish still runs (I-SCHED lever 1), instead of in phase B's main commit: - FinishSink: the finish hands each plain table it generates, by value, as soon as it exists; hand_or_keep is the one call per table, leaving the streamed chunks' placeholder in the slot when the sink takes the table and the table itself when the sink declines (its committers stopped). - FinishedKind: the plain tables Traces holds in a Vec. The preprocessed tables and the singletons stay with phase B. - air_for: the AIR VmAirs::new builds for an instance (same constructor, same name); precommit_finished makes the Round-1 commit under it; insert_finished puts the tables back into their placeholders, refusing any other slot. - ChannelSink sends into a committer queue and declines once it is closed. The prove still places each precommit on its AIR by name and absorbs every root in AIR order, so no proof byte depends on when a table was committed. Nothing calls the sink yet: the finish's calls come with the bounded finish, the committer pool's with the phase-A gate. Tests: the AIRs match VmAirs::new's by name, layout and constraints for every kind (a swapped constructor fails it); a finish double hands every table off from rayon workers and the build comes back whole; a table only lands on a placeholder; the channel sink declines after its receiver is gone. A GPU-box test proves one build with every plain table precommitted through the module against phase-B commits: the same bytes, verified, and a precommit of another trace is not accepted.
… generated WindowedTraceBuilder::finish_handing(logs, sink) builds what finish builds, but each of the 20 plain kinds (finish_sink::FinishedKind) goes to the sink through finish_sink::hand_or_keep as soon as its chunk is generated and packed, on the rayon worker that made it: a table the sink takes leaves the streamed chunks' placeholder in its slot, one it declines stays. finish is finish_handing with no sink, so every existing build is unchanged. The instance a table is handed as is its slot in Traces: the chunk's place among those generated, past the streamed chunks' placeholders (skipping and segmented builds). BITWISE, DECODE, KECCAK_RC, REGISTER, PAGE, HALT and BLAKE3 stay with the build, and disk mode keeps every table (it spills them). Packing carries the hand-off with its packing flag, since both say what the build does with each table it generates. Test: a windowed build with streamed ops dropped, packed or not, chunks of 4 rows streamed ahead, keeps no plain table when the sink takes them, and the handed tables put back with insert_finished plus the streamed chunks give the whole-run build; a declining sink leaves the build as finish makes it. Mutations each fail it: the skip offset dropped (MEMW_R lands on a streamed slot), the segmented offset dropped (LT), KECCAK_RND not handed.
At the median block the builder holds 9.5 GiB once the run is walked, and the finish frees about 13.4 GiB when it returns, but nothing says which lists those are. Under LAMBDA_VM_BLOCK_MEMLOG=1 the "windows walked" mark is now followed by one "BLOCK MEM builder parts" line: the kept tails and lists, the kept windows, each routed segment, what was counted ahead and the walk's memory state, largest first (capacities, at least 0.01 GiB). The "p3 lt" mark also carries the bytes of LT's ops and how many segments hold them. WindowedTraceBuilder::heap_parts is the breakdown; it changes nothing. Test: the parts add up to the accumulator's held bytes plus the walker's memory state after every window, with the streamed ops dropped or kept.
…LL kind derived (D-EXEC E1 v2) The walk materializes one CpuOperation per cycle, and the windowed producer is bound by the bytes it moves. arg2 (CPU-A1's multiplex), branch_cond and the seven ECALL-kind flags are functions of the decode entry and rv1/rv2 (an ECALL reads a7 into rv1), so they become methods; COMMIT's buffer and count and KECCAK's and BLAKE3's state address share two operand slots (ecall_args). 128 -> 96 bytes, pinned by a const assertion. Every reader calls the method of the same name; the values are the same.
An op routed to MEMW_A has one old timestamp for all its bytes, and its eight value (old) elements fit one u64: bytes for a memory access, the two 32-bit halves for a register access that missed MEMW_R. The walk's MEMW_A bucket, the windowed builder's MEMW_A tail and chunk jobs, and the table phase keep AlignedRow (memw_aligned.rs) instead of MemwOperation: 152 -> 48 bytes, pinned by a const assertion. The MEMW_A generator, the MEMW_A LT derivation and its BITWISE lookups read the row; the cells are the same (the 187 trace digests equal; a round-trip test over every width, memory and register).
The finish's hand-off (finish_handing), LT kept as segments, the minor faults in BLOCK MEM, and the stripped memory knobs (queue budgets, purges, finish permits). Conflicts: - finish_sink.rs (add/add): ours, a superset of t2c's cherry-pick of 7898d69 (identical to it) plus From<StreamedChunk> and hand_built. - block.rs: t2c's stripped queue (no budgets) taken; the committer side re-applied on it. The card gate, which leaned on the old QueueRoom's budget, is a CardGate of its own. LAMBDA_VM_BLOCK_FINISH_COMMIT becomes three-way: unset/0 phase B, 1 handed as the finish builds each table (finish_handing with BlockFinishSink), after once it returns.
… in flight With the packed builds off (the default), the finish builds every KECCAK_RND chunk at 8 bytes a cell and packs it afterwards; at the median block about 0.71 GiB a chunk, and as many at once as rayon has workers free, which set the median's peak (BIG 104 / 106: about 13.7 GiB above the packed builds). The cap builds them in waves of n chunks instead: each wave is one parallel batch, so at most n 64-bit copies exist at once and the workers not in the wave stay free for the other tables (a permit would park them). Packing gains a wave size; generate_chunks_with goes wave by wave when it is set, keeping the chunks' order. StreamSkip::kr_wide_cap and WindowedTraceBuilder::cap_kr_wide carry it; block.rs reads the knob only with the wide builds. Unset (the default), nothing changes. Tests: a build in waves of 1, 2, 3, 37 and 100 never has more than a wave in its generator at once and gives the unbounded build's tables in order (the waves removed: 11 at once; a wave reversed: the order check fails); the packing test gains a capped arm (KECCAK_RND chunked into many) that widens back to the whole-run build.
…ayon pool of their own BIG 462: with the finish handing its tables to phase A's committers, the finish handed 140 tables during its generation (p5) and none was committed until p5 ended (BLOCK MEM committed flat, the card at 12-16 %); then they drained at 99 % card after the finish, and the base did not move. A commit's host-side parallel work (a small table's host LDE and tree, a packed trace's widening) runs on the global rayon pool, which p5's scope holds with its generators. With LAMBDA_VM_BLOCK_COMMIT_POOL=n (1..=32) each committer makes its commit inside a pool of n threads built for the stream; a committer is an OS thread of the stream's scope, never a worker of either pool, so `install` only parks it until its commit is done. Unset or 0: the global pool, as before. No trace or proof byte changes. Test: a commit beside a global pool whose every worker is held waits for the workers (2.99 s of a 3 s hold on the laptop) and does not in a pool of its own; the stream's phase-A commit test now also runs with the pool.
…mes) For the phase-B head lever (I-MEDIAN §7.2's instrument spec): why the fused region's first 30 s leave the card idle for 2.5 s in some median runs and 9.5 s in others. - With LAMBDA_VM_TABLE_TIMELINE=1 + LFM_PROVE_SPLIT=1 each TABLE TL line now also names its driver thread (thread=name/tid) and gives every stage's span in unix seconds (at=[stage start-end · ...]), from a per-driver-thread record opened at the table's claim (prove_split::table_begin). - run_admitted's drivers are named <phase>-<n> (fused-3); the block stream's threads block-exec, block-walk, gen-<n>, commit-<n>; with the timeline on, the global rayon pool's workers rayon-<n> when the block is the first to build the pool. Names and stamps change no trace and no proof byte; the stamps are off by default.
…_VM_BLOCK_PACKED_BUILD=0 turns them off) The sizing law (I-MEM.md §8) puts a block at the top of the July median range (about 12x) at up to 127 GiB with the wide builds, over BIG's 120.7 GiB, which is the packed builds' revisit condition. BIG 107 ran the two levers that remove the wide KECCAK_RND chunks in flight against the defaults at the median block, one binary, D A B B A D: - packed builds: peak 82.7 GiB (defaults 96.7), base -1.85 s (phase B +0.7 s, finish -2.6 s), projected 100.8 GiB at 11.9x; - KECCAK_RND's wide chunks capped at 4: peak 82.8 GiB, base +3.08 s (the waves made KECCAK_RND the finish's critical path, +1.6 s). Both fit the 110 GiB line at 11.9x; the packed builds cost less, so they are the default. The cap stays as a knob for the wide builds. No trace changes.
T2 and the median peak lever onto the CPU op at 96 B and MEMW_A's aligned rows: LT kept as segments (LAMBDA_VM_BLOCK_LT_CONCAT=1 concatenates), the finish's hand-off to a FinishSink (inert: no sink is passed), BLOCK MEM's minor faults and the builder's parts, KECCAK_RND's wide-chunk cap (LAMBDA_VM_BLOCK_KR_WIDE_CAP, off), and the packed KECCAK_RND / LT builds on by default again (BIG 107's pick). No textual conflicts; the aligned rows reach the breakdown and the tails through the generic heap_bytes helpers.
…ommitters' own pool BIG 463 (median, three runs an arm, one binary): handing each plain table the finish builds to phase A's committers as it is built, with the commits in a rayon pool of their own, takes the base -7.85 s (t -2.6): phase B -13.32 s (its main commit 14.4 -> 1.3 s), phase-A end +5.45 s; 127-141 of the 180 finish tables committed during the finish's generation (53 without the pool, BIG 462); digest ac406fc8, every median and 1x run verified, peak unchanged. - LAMBDA_VM_BLOCK_FINISH_COMMIT: unset or 1 hands them off (the default), 0 leaves them to phase B's Round 1. The `after` measurement arm is gone. - LAMBDA_VM_BLOCK_COMMIT_POOL: unset is 8 threads, 0 the global pool. - LAMBDA_VM_FUSED_WALK (the mixed phase-B walk) is gone: MECHANISM-ONLY at the median (BIG 460), the fused region is bound by the VRAM gate's packing. The roots are still absorbed in AIR order and each precommit is placed by its AIR name; no proof byte moves.
BLOCK_FAN_IN goes from 2 to 4 (approved by Mauro, 2026-10-02). On the record block's 8 leaves the tree proves 3 nodes instead of 7: two nodes of four under a two-child top. FAST 399 measured the recursion at -1.02 s against fan-in 2, and FAST 450 measured fan-in 3 at +1.15 s against 4. The fan-in is a tree-format constant: every node program and so the top depend on it, and verify_block_tree derives under the same constant. NOEPOCH_BLOCK_FAN_IN=2 keeps the old tree measurable. The epoch tree's FAN_IN stays 2. A laptop test pins the default and the 8-leaf layout. (cherry picked from commit e4323ee)
NarrowMain::digest mixes the shape, the column widths and every packed byte in four 64-bit lanes and finishes with MurmurHash3's finalizer: a non-cryptographic check that a trace built again is the one committed (the threat is a prover bug, not an adversary), for the regeneration work of D-MEMORY A1/A2. Test: equal traces digest alike; one flipped bit at the head, the middle or in the tail past the last 32-byte block, or one row fewer, changes it.
…pth by its row width Under kept top levels every query rebuilds its subtree on the host from rows gathered off the device, so a rebuild costs the row's width times 2^k leaves, while the kept top it saves grows with the row count. At the median block KECCAK_RND (1,480 columns, 2^16 rows) spent 0.45-0.58 s a table on its queries at k = 6 while holding 7.8 GiB of phase B's VRAM gate (BIG 464), the head of the fused region's host-bound stretch. With LAMBDA_VM_KEPT_SUBTREE_ELEMS=n each plain table leaves out the most levels, from 1 to 8, whose rebuilt subtree holds at most n field elements; at n = 8192: KECCAK_RND 1, ECDAS 2, KECCAK 3, CPU 6, LT 7, MEMW_R 8. Unset or 0: the single depth, as before. The cap is the only knob. Same tree at any depth, so the openings and the proof bytes do not move.
…state A block too big for the host holds, from each instance's Round-1 commit to its fused task, one thing it could keep elsewhere: the packed main trace. `spill::SpillStore` writes packed traces to one unnamed file on a local drive (O_TMPFILE, else created and unlinked), refuses a tmpfs or ramfs directory, uses O_DIRECT when an aligned probe write and read succeed and otherwise buffered I/O with each slot synced and dropped from the page cache. Slots are append-only and 4 KiB-aligned; writer threads drain a queue bounded in bytes, and a full queue blocks the spiller. A write error (ENOSPC, EIO) fails the store: the bytes it could not write stay in memory and later spills are declined, so the prove goes on resident. Each slot carries the digest taken before its write (NarrowMain::digest); every read is checked against it. `TraceTable::spill_main` moves a uniquely owned packed trace to a store, `unspill_main` brings the same bytes back, `is_main_spilled` says which. Nothing calls them yet: production is untouched. libc becomes a plain dependency of `stark` (it was optional, under disk-spill; it is already in the lock).
When any trace of a prove is spilled, a read-back thread reads the slots in the order their readers take them (the Round-1 commits of traces spilled before them, in R1's walk, then every fused task, in its walk), at most a window ahead (LAMBDA_VM_SPILL_PREFETCH_GIB, 4 by default), checks each against its digest and parks it. `run_admitted` takes an optional readiness hook that a driver waits on BEFORE the VRAM gate (the packing arm passes over an unready table), so no permit is held across disk I/O. A Round-1 commit of a spilled trace commits a copy holding its packed words (the trace stays spilled); the fused task unspills it first, before any device work. A slot that does not come back refuses the proof: SpilledTraceMismatch(<AIR>) on a digest mismatch, SpilledTraceRead on an I/O error. Without a spilled trace nothing changes: no thread, no wait. Tests: round trip at every width mix and odd row counts (O_DIRECT where it probes, buffered forced); a byte flipped on disk refused; a RAM-backed directory refused; ENOSPC keeps traces resident and the prove completes; every trace spilled (after its precommit, or before Round 1) proves the resident bytes under every residency; a slow disk; the digest off and a perturbed slot never accepted; the read-back keeps to its window; a driver waits for its inputs holding no permit. Card versions are #[ignore]d.
MauroToscano
added a commit
that referenced
this pull request
Oct 11, 2026
Lead ruling: the recursion legs use #1013's hint-order walk4, three placing Selects a 4-ary level against walk4_child's five (27 against 45 Select rows an opening at nine levels), which keeps the node SELECT chip near 2^21. Both walks place every node by an index bit, so either is sound (REV-P1W A1). The harvest lays each trace and FRI path out in hint order at the transcript's leaf index (HostTable::iotas, shifted by the layer's G_j + d_j for a FRI tree), as #1013 does; sub_proof::authenticate_leaf walks with walk4 / CapCells:: verify_path. Binary paths and their emission are unchanged. The WHIR leaf's openings keep walk4_child.
…in's socket Two box-tier fixture tests still named the legacy hasher on block paths: the_block_verifier_derives_the_tree_and_accepts_only_its_top built its ahead artifacts under RPX, so they could not equal the proved P1 leaves, and the_block_fixture_tree_proves_and_refuses_another_blocks_leaf ran its P1 nodes under RPX, which refuses every width-16 row: the negatives held for the wrong reason and the positives failed. Both now take program.hasher(BLOCK_SOCKET), as production's artifacts_of does.
MauroToscano
added a commit
that referenced
this pull request
Oct 11, 2026
The lead's pick after #1013's box arms (ULTRA 131): C2 was 1.46 s faster in median recursion than C1 with 2.9 GiB less peak VRAM, and #1014's node census under the hint-order walk puts C2 4.5 % under C1 (C1's top node crosses the LFM_HASH 2^17 step). P1_STARK_CAP = 2, the LFM statement tag names C2, and the P1 STARK goldens return to their C2 bytes.
MauroToscano
added a commit
that referenced
this pull request
Oct 11, 2026
The lead's #1013 lesson: a refusal test must fail at its intended check, not on any error. The stacked layer reported every chain refusal as ColumnOpeningRejected, and the in-guest negatives only saw the machine refuse. Host (multilinear): - stacked_eval::verify_traced returns the refusal with its cause (Refusal::{Before, Chain { chain, poly, cause }}); verify is it mapped exactly as before (a shape refusal by name, any other chain refusal as the chain's first polynomial's ColumnOpeningRejected), so PerPoly's verdicts and errors do not move. - whir_round::verify_grouped reports a round-0 tree's failed opening as the new Error::GroupedOpeningRejected { query, tree } (appended last). - whir_group_tests assert the cause of every negative: the tree and query of each tampered, swapped, moved or combination-preserving block; the fold for rho swapped in the combine, the final check for the weight's faults; the per-polynomial count for a grouped proof under PerPoly; the cap check or the root for a proof read under another cap. Guest (prover): - whir_chain::onechain_steps (test only, recording only, nothing emitted): marks of each emitted check (chain, sumcheck, out-of-domain and grinds, each tree's opening, the successor's, the fold, the final check); failed_at names the check whose assert failed. - whir_onechain_tests name each forgery's refusal on the serial schedule (program order, the host's) and require the machine to refuse at the check the host does; the faults refuse at round 0's first fold or the final check; B1-2's shapes refuse as another arena length. Forgery fixtures run eight queries and every forgery applies to every case (no silent skip): the one-round case at blowup 2^6, P1's at 2^10. - block_whir::verify_block_whir_traced carries the multilinear refusal (verify_block_whir_with is it, as a bool). The block tests assert the other mode's verifier refuses by the statement (the two statements are one bit apart, the fold word's 47) before any opening's shape, and the Indexed leaf refuses a forged round-0 value at tree 1's opening of that chain, as the host does at that chain's opening.
The P3b review (SOUND, three REQUIRED test items) found checks on the block's LFM path that no test pinned: the in-guest P1 grind (one bit weaker passed every test, the_grinding_check_is_p1s included) and the cap-to-root comparison at C2, on the host and in-guest (T5 never moves an unqueried cap node; T6's cap tamper is refused by the cap mux). p3b_check_tests (laptop: emission, execution or no work): - the guest's grind accepts exactly the host's nonces: exhaustive small windows; the boundary bit at small factors and at the block's own, read from block_tree_options(); seeds near p; nonces at and past p; and the leg's sequence (state, check, nonce absorbed, the host's state after); - the configuration check refuses every mismatch and names the hash, not the cap; the block verifier and the tree's base harvest refuse a legacy hash before any work; - only Fixed(2) renders the block's LFM tag, and no LFM tree at C2 is uncapped (REV-P1-JUDGE's F2 and F4 on the LFM path); - aliased public lanes absorb alike while the LfmPublic closure tells them apart. p3b_lfm_tests, box tier (#[ignore], they prove): - at nine queries every cap node of every sub-proof is bound on the host, and every caps-arena word is refused in-guest by a check; - a proof at C0, C1 or C4 is refused at C2, with the tag and without it; - a node refuses a moved word in every arena at three positions, each by a check; C1/C4 children by layout; an untagged child by a check. T4's negatives say where they are refused (the configuration check, or the proof with the check passing); T6's tampers must be refused by a check, never by the arenas' layout.
…ads names as tokens The review showed the_production_block_paths_name_only_the_pin defeatable: its skipper ran from a #[cfg(test)] field (a line ending in a comma) to the next brace at that indent, hiding 83 production lines of block_tree.rs (hex_id, the head of prove_block_tree, BlockTreeProof), so planted legacy presets passed; names were substrings, so a grouped import or a turbofish evaded them; tree_run.rs was not scanned. The skipper now masks comments and literals and skips exactly the attribute's target (to its ; or , at its own depth, or the brace that closes it). Names are whole identifiers in code (29 legacy items), plus the HasherKind::Rpx path and the legacy env words in string literals. Each scanned file names production items the scan must still reach, and the_production_scan_reads_every_production_item holds the skipper to the tree's file. block_leaf.rs, block_node.rs and tree_run.rs join the list; tree_run's census panel takes its socket from the caller (the block's BLOCK_SOCKET, the legacy trees' LEGACY_HASHER), the same hasher for every block program, all of them width-16.
P3b made tree_ids derive every plan under the block pin while the pinned plan stayed on the RPX base: a mixed tree no prover builds, so the small-tree pin test went red. The pinned plan now plans over the block's base (block_tree_base_options) and its tree derives under the block pin (tree_recursion picks the recursion from the plan's base, never a mix). The laptop's small-tree ids are re-recorded (68548044 / 2e2020c5); the RPX-era box rows and the production-height rows are dropped, so a box refuses by its digest until record_small_tree_ids / record_production_height_tree_ids record its own. The census and the P1 small tree keep their RPX reference as legacy_spread_plan. The fixture trees' negatives say where they are refused: the node and top negatives by a check, never the arenas' layout; another output by the top's claims; another ELF and a lying shape before the claims. The S5 instruments' spread plans say they plan over the legacy RPX base.
…heir items verify_block_tree_with's constants are computed under block_tree_base_options (the block pin), not the legacy block_base_options; WrapHash::for_base's fallback is Self::legacy, the name the rename gave Self::production.
…ree gets a laptop pin The judge accepted keeping the compact program form's pins on the RPX tree, each plan derived under its own base's recursion (the form is hash-independent), and advised a laptop pin of the block's own small tree between box gates. So the RPX pins and their plan return as they were at e740589 (legacy_spread_plan; the laptop and FAST rows, green on the laptop), and the_block_trees_small_ids_hold pins the small plan over the block's base, derived under the pin, at the laptop's ids recorded at P3b (68548044 / 2e2020c5; a box refuses by its digest). The recording instruments go: the pins print their ids before they compare.
…ld is refused by layout RYZEN 103a timed the review's proving tests: the cross-cap refusal 3.9 s, the host cap-root test 2.9 s and the in-guest one 3.1 s, so they lose #[ignore] and run with the lane's T4-T6. The widened arena tamper (23.7 s on a 32-thread box) stays box tier. The same run printed T6's legacy child refused by ArenaCountMismatch (244 arenas expected, 234 found): T6 now asserts a layout error, the refusal meant there.
…the row that sees it removed RYZEN 103b removed the configuration check and one mismatched pairing still verified: the legacy verifier, over its own roots and a legacy proof, handed options that name the block's base. Nothing false: the hash is bound by the type (the configuration's transcript, tag and trees), and the check is the only guard of the options' and artifacts' labels. Its doc now says so, and T4 gains that pairing as a row, which is the one that fails if only the verify entry's call is removed.
MauroToscano
added a commit
that referenced
this pull request
Oct 11, 2026
… -> 72 bytes) Ported from #1013 b68dd7b (i-exec2 lever 1, D-SPEED lever 1 stage 1). The walk materializes one CpuOperation per cycle, and the routing, the in-walk lookup counting, the hand-out and the CPU generator each read every op again. The op carried a copy of its 32-byte DecodeEntry; it now carries the entry's DECODE row (u32). The entries live once per instruction in a DecodeTable (decode.rs), built in generate_decode_trace's row order (pcs sorted, the CPU padding entry's row after the last), shared with the threads that generate CPU chunks. Readers pair an op with its entry through CpuOp (DecodeTable::op), which holds arg2, branch_cond and the ECALL accessors. The row also replaces the pc search in the DECODE counts: the hand-out and the finish count each CPU op's lookup by row (decode::count_rows) instead of collecting its pc and hashing it through pc_to_row. #1014's own readers, ported here: the streamed finish (FinishPlan's halt search, its CPU and DECODE units in both emit paths), the frozen finish oracle, the regenerator (its walk, its STORE filter and its CPU cut), the G-pack CPU generator (generate_cpu_trace_as takes the decode), the clock tests (one collector now) and the S0 hand-out stamps. The tables do not change: the 187 trace digests equal 3f33e1f's, and the windowed identity, lean-walk, regen, finish, stream, clock, CPU and DECODE tests pass. Two segmented_tests stop on an overflow in their own test data under debug overflow checks; that generator is unchanged from the base. cpu.rs is #1013's head version (its generator fills rows from segments, which the slice functions call with one).
MauroToscano
added a commit
that referenced
this pull request
Oct 11, 2026
Ported from #1013 d4eea70 (i-exec2 lever 2, D-SPEED lever 1 stage 1). LoadOperation held its eight result bytes as [u64; 8]; it now holds [u8; 8] (each is a loaded byte or the 0/0xFF fill). The walk keeps one per load (0.22 per cycle at the median block), and the hand-out takes them into chunks, so the op is now 32 bytes, pinned by a const assertion. The LOAD trace and its MSB8 lookups read the same bytes.
MauroToscano
added a commit
that referenced
this pull request
Oct 11, 2026
…a copy Ported from #1013 4883b15 (i-exec2 lever 3, D-SPEED lever 1 stage 1). A streamed table's tail holds each walked window's list as one part. A chunk taken out of it was copied into a new list unless one part was exactly the chunk; at #1014's windows of 2^20 cycles not even CPU's parts ever were (every CPU chunk is two window lists), so every streamed chunk was a copy, on the accumulator thread that binds the median's windows phase under P1. The tail now keeps its parts behind Arc and a chunk takes the ranges of the parts it lies in (Segments); a part a chunk uses only the front of stays shared with the tail and with the next chunk. The generators fill the rows from the segments (generate_*_segments_as; the slice functions call them with one segment), and the hand-out counts the chunk's lookups segment by segment. LAMBDA_VM_HANDOUT_COPY=1 copies as before (the control). #1014's own pieces: the G-pack forms (every generator's _segments_as), the regenerator's cut (CPU and the walk's tables as segments; STORE's list, which a chunk holds whole, copied as before), and the S0 stamps (the take counts the ops it copied: none as parts). This removes the copy rather than moving it to the generators (FAILED-LEVERS row "E2 hand-out", revisit "the copy is removed rather than moved").
MauroToscano
added a commit
that referenced
this pull request
Oct 11, 2026
Ported from #1013 08294a8 (i-exec2 lever 4, D-SPEED lever 1 stage 1). The walker collected a whole window's CPU ops (2^20 x 72 bytes in the block build), then walked them: the walk read every op back from memory. The walk is a left fold over the ops, so the walker now collects a batch of cycles and walks it at once, while its ops are still in cache; the window's lists are the same. LAMBDA_VM_WALK_BATCH sets the batch (0 = the whole window first, as before). A new identity test (batches of 1, 7, 64 and the whole window, windows of 33 and 1000, ops kept and dropped, three programs) builds the whole-run tables.
MauroToscano
added a commit
that referenced
this pull request
Oct 11, 2026
…ace and counts its lookups in the same pass Ported from #1013 54d92e7 (i-exec2 lever 5, D-SPEED lever 1 stage 1). The accumulator routed each window into segments of its own (growing from empty), appended them to the run's (a copy), then read every CPU op again to count its BITWISE lookups. route_ops_into pushes into the run's segments directly, derives the DVRM-implied LT and MUL ops from the window's part of each DVRM list, and counts each CPU op's lookups as it routes it: the same segments and the same counts. LAMBDA_VM_ROUTE_FUSED=0 routes, appends and counts as before. On #1014 the run's segments are blocks (RoutedBlocks: BlockVec, and the delta-coded BRANCH, EQ and BYTEWISE streams), so the ops go into them one at a time, and CPU32's few ops go through lists of the window's own. A new test (windows of 1, 37 and the run, four programs, blocks of four ops so a window's DVRM part straddles blocks) finds the in-place segments and counts equal to the appended ones.
MauroToscano
added a commit
that referenced
this pull request
Oct 11, 2026
…engths Ported from #1013 db3aae1 (i-exec2 lever 6, D-SPEED lever 1 stage 1). A window's MEMW_A and MEMW lists started empty and grew by doubling (about 20 reallocations and twice the list copied, every window), and LOAD, LT and SHIFT started at fixed per-cycle guesses below what a block walks (LOAD 1/8 per cycle against 0.22 at the median block). The walker now remembers the last window's lengths per cycle and allocates the next window's streamed lists an eighth over that, once; the first window keeps the guesses. MEMW_R's 3 rows per cycle shrink to what the run walks. LAMBDA_VM_WALK_SIZED=0 sizes them as before. The lists do not change (capacities only).
MauroToscano
added a commit
that referenced
this pull request
Oct 11, 2026
… in the tree harness #1013 walks its block a CPU chunk (2^21 cycles) at a time; #1014 walks 2^20. With the window-part hand-out the size no longer decides any copy, but it does decide the order the chunks leave in across tables, so the groups (statement data) differ at 2^21 while the tables are the same. The knob lets a box measure #1013's window; unset is production's 2^20, and any value but 20 or 21 is refused (a test pins both).
MauroToscano
added a commit
that referenced
this pull request
Oct 11, 2026
…UT_COPY says Tail::take hands out the parts unless LAMBDA_VM_HANDOUT_COPY=1, when it copies; the tail tests (from #1013 4883b15) check the parts against the copies, so under the knob they compared copies with copies, and the straddling-part test failed. The parts' path is now Tail::take_segments, which take calls unless the knob is set, and the tests call it directly, so a suite run with the control's knobs still tests the parts.
MauroToscano
added a commit
that referenced
this pull request
Oct 11, 2026
The knob is read by the tree harness and by the CLI (both go through WhirTreeConfig::from_env), so its 21 would have let a production prove walk #1013's 2^21 windows: the same tables, but the chunks leave in another order across tables and the groups (statement data) move. The window stays 2^20; the knob now names that and refuses any other value, 21 included. The test pins it.
MauroToscano
added a commit
that referenced
this pull request
Oct 12, 2026
StarkHash gains ARITY (default 2) and ARITY4_CAP (default Off). At arity 4 the format's binary cap policy does not apply: effective_cap_policy runs the configuration's own ARITY4_CAP, so a prover and a verifier naming one configuration agree on the cap by construction, and no format field, knob or proof byte moves it. StarkCaps counts each tree's levels at the configuration's arity (from_layout_arity, tree_cap_height, with_depths_arity); the prover's cap post-pass embeds at that arity and checks a host tree's own level count; the verifier lays its checks out the same way. P1StarkHashCapped<CAP> is ZisK's Poseidon1 as a STARK configuration over crypto's P1 backends and transcript hash: 4-ary trees, arity-4 caps at height CAP (0 uncapped). The P1 backends are DeviceTreeBackends under CommitmentHash::Poseidon1, and const checks tie the arity, the device key and the transcript to the configuration. Device: gather_proofs_dev gathers three siblings per 4-ary level from a 4-ary resident tree, and read_cap_dev reads an arity-4 cap level off the top-down node buffer. Ported from #1013 (1a676a5, 544b1b0, 29a2488) except that the cap is the configuration's rather than an environment knob or a format field. At arity 2 every path is today's: the RPX goldens and the stark KATs are unchanged.
MauroToscano
added a commit
that referenced
this pull request
Oct 12, 2026
…evice twins lfm::p1_commit names the P1 STARK configuration the recursion will commit under: P1StarkHash = P1StarkHashCapped<P1_STARK_CAP>, cap C2 (the WHIR base's), pending the node census. p1_stark_tests (ported from #1013's p1_stark_tests and REV-P1-B's configuration tests): SimpleAddition and the LogUp RAP round trip at even and odd LDE depths under the legacy, dp and one-row formats, uncapped and capped, on ZisK's transcript and the byte transcript; caps at heights 1-4 round trip and are refused by the neighbouring heights' configurations; the format's binary cap policy does not reach arity 4 (the production format's P1 proof is the cap-off format's, byte for byte); a cap shortens the paths by its height; tampered siblings, roots, cap nodes, owner and opening lengths, a moved cap and the nonce are refused; every cap node is bound by the cap root; a zero-padded opening is refused by the P1 leaf and the verifier; P1 and RPX proofs do not cross-verify, nor does the production cap's proof under the uncapped configuration. Four goldens pin the host bytes of P1 proofs at the production cap. zf_p1_device_tests (cuda, ignored, box): the FRI device parity cases and the tree parity under P1StarkHash, and the goldens proved on the card, which must take the device FRI, trace-tree, composition-tree, gather and cap-read paths and give the host's bytes.
MauroToscano
added a commit
that referenced
this pull request
Oct 12, 2026
Under P1 the LFM statement's first call is LAMBDAVM_LFM_STATEMENT_V1/P1W16/C<c> in place of LAMBDAVM_LFM_STATEMENT_V1 (lead ruling, shared with #1013). The legacy family's tag is LAMBDAVM_LFM_STATEMENT_V1 itself, so its statements stay today's bytes. STATEMENT_TAG and ChildShape.statement_tag become plain byte strings; the host absorb and the in-guest replay take the tag in place of the V1 call. Tests pin the call sequence by hand and refuse the prepended form.
MauroToscano
added a commit
that referenced
this pull request
Oct 12, 2026
The node census put C1 at 6 % fewer node cells than C2 (I-P1REC §P2.3), so the lead picked C1 for both PRs pending #1013's C1/C2/C4 timing. P1_STARK_CAP = 1, the LFM statement tag names C1, and the P1 STARK goldens are regenerated at the new cap. The WHIR base keeps its own C2 geometry.
MauroToscano
added a commit
that referenced
this pull request
Oct 12, 2026
Lead ruling: the recursion legs use #1013's hint-order walk4, three placing Selects a 4-ary level against walk4_child's five (27 against 45 Select rows an opening at nine levels), which keeps the node SELECT chip near 2^21. Both walks place every node by an index bit, so either is sound (REV-P1W A1). The harvest lays each trace and FRI path out in hint order at the transcript's leaf index (HostTable::iotas, shifted by the layer's G_j + d_j for a FRI tree), as #1013 does; sub_proof::authenticate_leaf walks with walk4 / CapCells:: verify_path. Binary paths and their emission are unchanged. The WHIR leaf's openings keep walk4_child.
MauroToscano
added a commit
that referenced
this pull request
Oct 12, 2026
The lead's pick after #1013's box arms (ULTRA 131): C2 was 1.46 s faster in median recursion than C1 with 2.9 GiB less peak VRAM, and #1014's node census under the hint-order walk puts C2 4.5 % under C1 (C1's top node crosses the LFM_HASH 2^17 step). P1_STARK_CAP = 2, the LFM statement tag names C2, and the P1 STARK goldens return to their C2 bytes.
The switch that makes Poseidon1 LFM statements take the legacy tag was a process-global flag. Three tests set it around a prove, a verify or a harvest, and four others read the block's LFM tag, so in one process (plain cargo test) a reader could see the tag dropped by another test. CI runs a process per test and never saw it. The flag is now a thread-local set by a guard: omit_p1_lfm_tag() drops the tag on the calling thread until the guard drops, on an unwind too. The LFM prove, verify and harvest entries read the tag on their caller's thread, so the three tests keep their meaning. A unit test pins the scope: another thread still renders the tag while the guard lives, and the tag is back at the guard's end. Test builds only; no production path changes.
MauroToscano
added a commit
that referenced
this pull request
Oct 12, 2026
The lead's #1013 lesson: a refusal test must fail at its intended check, not on any error. The stacked layer reported every chain refusal as ColumnOpeningRejected, and the in-guest negatives only saw the machine refuse. Host (multilinear): - stacked_eval::verify_traced returns the refusal with its cause (Refusal::{Before, Chain { chain, poly, cause }}); verify is it mapped exactly as before (a shape refusal by name, any other chain refusal as the chain's first polynomial's ColumnOpeningRejected), so PerPoly's verdicts and errors do not move. - whir_round::verify_grouped reports a round-0 tree's failed opening as the new Error::GroupedOpeningRejected { query, tree } (appended last). - whir_group_tests assert the cause of every negative: the tree and query of each tampered, swapped, moved or combination-preserving block; the fold for rho swapped in the combine, the final check for the weight's faults; the per-polynomial count for a grouped proof under PerPoly; the cap check or the root for a proof read under another cap. Guest (prover): - whir_chain::onechain_steps (test only, recording only, nothing emitted): marks of each emitted check (chain, sumcheck, out-of-domain and grinds, each tree's opening, the successor's, the fold, the final check); failed_at names the check whose assert failed. - whir_onechain_tests name each forgery's refusal on the serial schedule (program order, the host's) and require the machine to refuse at the check the host does; the faults refuse at round 0's first fold or the final check; B1-2's shapes refuse as another arena length. Forgery fixtures run eight queries and every forgery applies to every case (no silent skip): the one-round case at blowup 2^6, P1's at 2^10. - block_whir::verify_block_whir_traced carries the multilinear refusal (verify_block_whir_with is it, as a bool). The block tests assert the other mode's verifier refuses by the statement (the two statements are one bit apart, the fold word's 47) before any opening's shape, and the Indexed leaf refuses a forged round-0 value at tree 1's opening of that chain, as the host does at that chain's opening.
MauroToscano
added a commit
that referenced
this pull request
Oct 12, 2026
…(N4a) With LAMBDA_VM_BLOCK_REGEN and LAMBDA_VM_BLOCK_SPILL both unset, the production block now regenerates: whenever auto arms, the streamed chunks are dropped and rebuilt in phase B (the adaptive N2b window) instead of written, and the spill tier stays for the rest. A knob that is set keeps the meaning it had, as #1013's 1a98537: a set regen is read when the prove starts, and an unset regen beside a set spill is off, so scripts that pin the spill behave as before. Options a caller builds keep None as off. Measured with REGEN=auto: p90 disk 23 against 83 GiB, whole +0.05 s; T200-R disk 60 against 354 GiB, prove +0.3 %, takers never waited; the phase-A peak lower at both. Every prove now says the mode and the knobs (BLOCK REGEN mode). No proof byte depends on the mode.
MauroToscano
added a commit
that referenced
this pull request
Oct 12, 2026
With both LAMBDA_VM_BLOCK_SPILL and LAMBDA_VM_BLOCK_REGEN unset, BlockOptions::production() now pairs regeneration `auto` (N4a) with the spill policy NoDisk: `off` whenever live regeneration runs, so a table `auto` moves off the host is dropped when phase B can build it again (the streamed chunks, and KECCAK_RND's and LT's rest tables since N3) and stays otherwise, with no store opened. Without live regeneration (chunks not generated packed) NoDisk is `auto`, so no block loses its relief. Either knob set keeps the meaning it had, as #1013's 1a98537: a set spill reads as ever, an unset spill beside a set regen is `auto`. The BLOCK REGEN mode line is printed once the policy is resolved and ends with `no disk` when it runs with none. LAMBDA_VM_BLOCK_SPILL_RESERVE_PER_G (GiB per G cells committed, default 1.65 = today) is a measurement knob for the reserve retune D-FINISH S4 names; the default is unchanged until a gate reads the median at defaults. The proof's bytes are the same under every policy (tests under the deterministic grind).
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
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.
One STARK proof per block, with no epochs (the prove-and-retire / VADCOP shape). This is a second prover next to #1009's epoch-based one. #1009 stays the reference and this branch does not touch it. The branch starts from #1009's head
cc411aa2c, so the diff against main includes #1009. Compare againstcc411aa2cto see only this work.Whole block: 31.78 s (FAST 456 at the head
08ecc4310, mean of 3 default arms), against the epoch tree's 60.15 s (#1009; FAST 389's same-binary reference, not re-run since). Base 21.28 s, recursion 10.25 s (level 0 5.18 · interior 4.88).Head
d8a422962(10-05): the generators write the block's packed traces directly (G-pack). Every streamed chunk and every table the finish packs is written straight into its packed columns, with no table at 8 bytes a cell and no separate pack pass;LAMBDA_VM_BLOCK_GPACK=0restores the old path. Prover-only, the same bytes: under the fixed trace hash and the deterministic grind the base digest is0224203e…with G-pack on and off, and every table of the 1× block has the old path's packed bytes (BIG 634). Median block 25475471 on BIG, one binary, 3 + 3 (BIG 635): generator thread-seconds 399.8 → 105.7 (−73.6 %), phase A −7.47 s (t −10.2), base −7.35 s (t −10.6), phase B +0.10 s, VmRSS −3.28 GiB. See G-pack.Head
58a58be95(10-05): the production CLI proves and verifies a whole block.cli prove-block <ELF> --input <block> -o <proof>runs the whole-block harness's own driver (lfm::block_tree::prove_block_tree; the harness is now a wrapper around it, its output unchanged but for a firstBLOCK POSTUREline), andcli verify-block <proof> <ELF>runs the block verifier over the proof file. The binary installs its jemalloc as the prover's allocator hooks, so theautopurge and the late leaf emission act in the shipped CLI, and it sets the measurement posture for every knob the environment leaves unset. Prover and CLI only: no proof byte moves. ULTRA 016, 8 + 8 against the harness after a warm-up: CLI − harness whole −0.161 s (t −2.4), base digest0224203e…and top2ef0e0d2…equal the harness's. BIG 632: the p90 25481021 proves through the CLI at 112.33 GiB with both purges (whole 553.77 s) andverify-blockpasses in 72.86 s. See Production CLI.Head
4fc4b7b12(10-05): LogUp k4 is the default on the base tables (Mauro, 10-05;LAMBDA_VM_ZF_LOGUP=pairrestores the previous bytes). 1× tree on ULTRA, 8 + 8: base −0.89 s (t −15.6), whole −0.92 s (t −11.7); the p90 proves and verifies under k4 at the defaults (BIG 626: whole 555.29 s, 113.50 GiB, against 590.95 s and 115.79 GiB under pair in BIG 591).Head
035aef5d6(10-03): the p90 and full-gas blocks prove end to end at the defaults on BIG (128 GiB host, 120.69 GiB cgroup), and the block verifier passes on both. p90 25481021 (52.0 M gas, 612.3 M cycles, 20.1× the bench block): whole 590.95 s at 115.79 GiB (BIG 591). Full gas 25431071 (60.0 M gas, 602.9 M cycles): whole 541.51 s at 110.62 GiB (BIG 125). Before this head,autoalone ran out of memory in level 0 on the p90 (BIG 120). Prover and harness only: digestac406fc8…is unchanged (FAST 515). At 1× nothing arms or purges (default against spill off, base −0.065 s, t −0.6, 8 + 8; FAST 515 + 516). Four changes:autocounts the cgroup's working set (the charge less its inactive file pages), not its page cache.autofell from +3.6 to +1.12 s (BIG 118 → BIG 122).auto, once the budgets arm). Blocks that fit pay nothing.LAMBDA_VM_ALLOC_PURGE=off|all|<points>. It acts in the lib's test builds (the harness's jemalloc); the production CLI has no purge yet. (Since58a58be95the CLI purges too, through its allocator hooks.)Head
00871b913(10-03): under the shared VRAM gate, a carrying proof now claims its resident bytes plus one headroom shared with the claims in force. These tight claims are on by default;LAMBDA_VM_SHARED_GATE_CLAIMS=wholerestores the first form. This is scheduling only: digestac406fc8…and top93aa7097…are unchanged. Median block (BIG 474, 5 + 5): recursion −1.25 s (t −5.4), with level-0 claim waits falling from 8–10 s a run to 0. Whole −0.05 s: the base moved +1.18 s, which is scatter. At 1× there is no regression (FAST landing gate: recursion −0.01 s). See Recursion: sibling proofs share the card.Head
edddc6873(10-03): the trace spill store is on by default asauto. A block that fits spills nothing. A block above the host's limit spills the committed traces that would not fit, instead of running out of memory.LAMBDA_VM_BLOCK_SPILL=offkeeps every trace. This is prover-only: digestac406fc8…is unchanged. BIG 117 at the median block: the default spilled 0 B, with phase-A end −0.97 s against off; forced to a 70 GiB target it spilled 30.1 GiB, cost +1.43 s and verified. The same head adds the spill writer's step timings and splits the AIRs out of BLOCK MEM's unnamed heap; both are diagnostics only. See Disk spill: auto by default.Head
a93018974(10-03): the block tree's sibling proofs now share the card through one VRAM gate, on by default (LAMBDA_VM_SHARED_VRAM_GATE=0restores the exclusive card permit). This is scheduling only: digestac406fc8…and top93aa7097…are unchanged. Against564dd02bb(FAST 871): 1× recursion −0.68 s, whole −0.48 s. Median recursion −4.72 s (BIG 471, measured before the arming drained the device); at this head −4.24 s (BIG 472). See Recursion: sibling proofs share the card.Head
564dd02bb(10-03): adds LogUp k4 as an opt-in (LAMBDA_VM_ZF_LOGUP=k4; defaultpair= the same bytes; under k4, median phase B −9.56 s and 1× whole −1.04 s).Head
8f2ce57d5(10-03): three block-tree changes, all with the same proof bytes and program ids (FAST 673 merge gate green: 1× top93aa7097…, pinned ids unchanged; median top6d85454d…, BIG 586).NOEPOCH_TREE_EMIT_LATE=auto): when leaf 0 puts the other leaves' programs at ≥ 8 GiB, they are emitted in phase B onto pages the retired traces freed; smaller trees emit at the shape as before. Median, spill off (BIG 585): base-phase VmRSS −10.37 GiB, whole-run peak 98.99 → 86.49 GiB, recursion −0.31 s, whole −2.15 s; inert with spill on.NOEPOCH_TREE_EMIT_LATE=offrestores the old behaviour, and A/Bs against it must set that.verify_block_tree): each program and its artifacts are dropped once its child is derived. Verifier alone in a fresh process at the median (BIG 587): peak 32.33 → 22.89 GiB, derive −1.48 s.LAMBDA_VM_BLOCK_DERIVE_HOLD=levelrestores the old hold.Note on drivers: the whole-block numbers here come from the test harness's tree driver (
block_tree_pipeline,cfg(test)). The library has the base prover (block::prove_block), the per-node program emitters (BlockTreePlan::leaf_program/node_program) and the production verifier (verify_block_tree), but no production driver that chains them into a whole-block proof yet; that is a landing item.Head
dacbd5b4e(10-03): KECCAK_RND, ECDAS and KECCAK compose on a bounded-slot interpreter by default (LAMBDA_VM_GPU_INTERP_SI=0restores the slot-file interpreter). Prover-only: digestac406fc8…unchanged, FAST 784's landing gate green (1× default − off −0.05 s).Constraint composition on a bounded-slot interpreter (prover-only; proof bytes unchanged). The three programs too large for the compiled kernels (KECCAK_RND, ECDAS, KECCAK) now compose on a bounded-slot GPU interpreter. The slot-file interpreter it replaces (from OpenVM v1) keeps every value of a row in a per-thread file in global memory: 4,350 words for KECCAK_RND, 2.1 GiB per composition, not counted by the VRAM gate. The new lowering evaluates each constraint's cone on demand in constraint-index order, reads trace cells as operands, and fits a row in 16–128 words of shared memory or a local array, recomputing past the budget; each program gets its measured best shape. On one binary, the three programs compose in 0.58–0.63× the time. At the median block (25475471, 3 + 3) the deciding figure is card work −0.43 s (t −1.9), with the slot-file scratch 80 GiB a run → 0 and the phase-B device peak −1.9 GiB (t −3.4); base −1.03 s is not significant (t −1.0); at 1× base −0.06 s. The digest is unchanged (
ac406fc8…);LAMBDA_VM_GPU_INTERP_SI=0restores the slot-file interpreter. Running all 39 programs on it is slower (1.25–2.1× the compiled kernels, +0.16 s at 1×), so the compiled kernels stay for the other 36.Head
d740eb5d5(10-03): the block tree emits each node's program as soon as its children land, instead of level by level (NOEPOCH_TREE_NODE_EMIT=levelrestores the old order). This is scheduling only: the same top program id in all 14 arms.NOEPOCH_TREE_EMIT_WINDOW; −12.9 GiB median base peak for +6.2 s recursion) and a cap on concurrent derivation builds (LAMBDA_VM_BLOCK_DERIVE_BUILDS).Head
86e71de77(10-03). Three landings sincef805464f6:aa726ce2b: block fan-in 4 (Mauro approved 10-02; see (f)).5e4176961: KECCAK and ECSM chunked, and tree partition rule v2, a format change. See the format section below.7ef261724+86e71de77: producer and memory work, all prover-only with identical proof bytes:LAMBDA_VM_BLOCK_GENERATORS=6restores six);LAMBDA_VM_BLOCK_SPILL=alwaysturns it on).The median block 25475471 on BIG (job 112, Zen 3 host):
ac406fc8…unchanged.Disk spill (BIG 111, base only):
The walker levers with eight generators end the median's phase A 3.45 s sooner (BIG 468) and cost +0.14 s on the 1× base (FAST 470).
Head
f805464f6: two more producer and memory changes, both prover-only with identical proof bytes:6cb6cd557, smaller per-step records: the CPU op shrinks from 128 to 96 B (arg2, the branch decision and the ECALL kind are derived) and MEMW_A ops become 48-byte aligned rows. FAST 612 at 1×: base −0.38 s, digest equal. BIG 424 at the median: phase-A end −6.0 s.f805464f6: LT ops kept as segments rather than concatenated, and the packed KECCAK_RND / LT finish builds back on by default. BIG 107 picked them over capping wide KECCAK_RND chunks: at the median they save about 14 GiB and end phase A 2.6 s sooner.BIG 108 at this head: 1× verified at 15.1–16.2 GiB with digest
ac406fc8…. The median block verifies at 81.8 / 82.4 GiB with base 212.4 / 216.0 s. Phase B scatters run to run by about 2.7 s (sd) at the median.Head
330057f2a: the packed KECCAK_RND / LT finish builds are now off by default (LAMBDA_VM_BLOCK_PACKED_BUILD=1turns them on), and the memory knobs that had no effect are removed. Two one-binary A/Bs at the median (BIG 104, 105): packed builds save 13–15 GiB of host peak but cost phase B ≈ 3–6 s. BIG 105 at this head: 1× verified at 18.32 GiB, digestac406fc8…; median block 96.2 GiB, base 218–224 s on BIG.Head
161b82415: six generator threads by default (LAMBDA_VM_BLOCK_GENERATORS=0keeps the committers generating). With the faster walk the three committers, which also generated every chunk, fell behind: at the median block 32.8 GiB of op lists waited and phase A ended 19 s after the finish. Generators build and pack each chunk; the committers only commit. KECCAK_RND and LT in the finish are built packed a block at a time (LAMBDA_VM_BLOCK_PACKED_BUILD=0builds them wide). BIG 103/104 on the median block 25475471: base 231.8 → 222–226 s, host peak 96.1 → 82.7–83.0 GiB; 1× base flat; digestac406fc8…unchanged. Within one binary, packed builds cost phase B ≈ 6 s at the median against wide builds and save 14.75 GiB; see the head above for the current default.Head
3be24abab: narrow storage on by default (merged froma2cd24207). Main-trace cells are stored at about 2 B each instead of 8 and widened on the card;LAMBDA_VM_BLOCK_NARROW=0keeps them wide. BIG 100 (A/B on one binary, the 128 GiB box): proof digests packed = wide =ac406fc8…; 1× host peak 31.2 → 17.7–19.0 GiB; 1× base −1.29 s on that box. A median mainnet block (25475471, 9.78× this one, 941 sub-proofs) proves and verifies within 128 GiB: host peak 106.87 GiB, base 259 s on BIG's Zen 3 host (BIG 100; that binary predates the E1+E4 producer changes below). BIG 102 re-gated the merged head: 1× verified, digestac406fc8…, peak 19.29 GiB.Head
2c440b8dc: base 19.61 s (FAST 602, mean of 2). It adds two producer changes to19fe5e9e5, whose memory changes are in Memory: a lean walk (the walker builds only what the tables need) and the executor's guest memory in 64 KiB pages instead of a hash map of words. A B B A on one binary: base 20.38 → 19.61 s (Δ −0.77, no overlap); proof bytes equal underLAMBDA_VM_FIXED_TRACE_HASH=1+LAMBDA_VM_DETERMINISTIC_GRIND(digestac406fc8…in both arms); host peak flat. At a median-size block (25475471, harness, windows only) the producer's windows phase falls from 42.4 to 25.2 s and the executor from 108 to 11 ns per cycle.LAMBDA_VM_WALK_LEAN=0andLAMBDA_VM_EXEC_MEMORY=wordsrestore the old paths. The whole tree has not been re-run at this head.The whole block, epoch tree vs no-epoch tree (FAST 389, one binary at
e4ff3f8fb, means of 2 arms)Block 25368371. Both trees run on one test binary, and its md5 is checked after every arm. The epoch arm is #1009's record harness, unchanged.
a0954fd1bthe lists are the plan's: D-NOEPOCH §12.2's rule over the closed-form costs, a pure function of the block's shape. On this block the rule gives other lists than §12.2's, which came from legmodel.py's costs, but the leaf tiers are the same. FAST 392 atcda620461(means of 2): level 0 6.21 s, interior 7.19 s, harvest 2.03 s, whole 40.38 s, which is 389's numbers. The verifier's own derivation of the top program takes 8.35 s; that is outside the whole, and the derived top equals the proved top. A tree over another partition, a skipped instance or a duplicated instance is refused at the final check (fixture gate).The plan's gate and the harvest lever (block 25368371, means of 2 arms, 389's posture)
cda620461(the plan)a684f4f3f(+ ELF constants beside the base)a1a3a2c22(+ F1 follow-ups)e7406d6b5(+ rebuilt windowed builder)6b86432a2(+ verifier derive)verify_block_tree, no proof read, outside the whole)e7406d6b5and FAST 397's6b86432a2are both on this branch;6b86432a2is the head.-x) ofnoepoch/windowed-builder6e99c74..1d24a2c, not a merge of that branch (90 WHIR commits, 6 conflicting files), plus ourparallelgating, which compiles the recursion ELFs (5fe8316, now byte-identical to the builder branch's bcccdef).verify_block_tree_with(elf, &ElfConstants, …)lets a consumer compute the per-ELF constants once (3.05 s cold), and each node level is now emitted and built in parallel (level 1: 1.31 s wall for 5.0 s of work). Split at 397: constants 3.05 · plan 0.16 · leaves 2.17 · L1 1.31 · L2 0.93 · L3 0.72 · check 0.24.noepoch/stark-s3at3992a56f9, gated by FAST 399; A/B on one binary each):f6445c8b6(FAST 452, gated: −2.48 s againstNOEPOCH_TREE_AHEAD=0, P8 10/10). The leaf programs are emitted beside the base. Leaf and node artifacts are built on the card during level 0, and each node program is emitted as soon as its children's artifacts exist. Base +0.01 s; every child proof verified.c9c29cb5b,NOEPOCH_BUILDER_FIRST, off): recursion −0.60 s in its A/B, but not by the mechanism pre-registered. It cannot pre-empt a leaf'smulti_prove, so the level-1 artifacts are still late; what it did was remove level 0's slow mode (≈ −0.4 s pooled over 451–453). Not the default.7da2a45d0; the default since08ecc4310, gated by FAST 456 and 457): recursion −0.29 s, level 0 −0.40 s. Level 0 was bimodal (5.2 or 5.8 s). In the slow runs, one leaf'smulti_proveheld the card for 1.2 s at about a third busy, starting at the instant the builder began emitting the level-1 programs on the global rayon pool (FAST 454's card trace). With a 4-thread host-only pool of its own, the stalled hold is gone in every run.NOEPOCH_EMIT_POOL=0restores the global pool.e029731f7; FAST 456): base −0.57 s (P8, 5 against 5 on one binary, no overlap), replicating WHIR's FAST 417 (−0.52 s).LAMBDA_VM_BUILDER_CONCAT=serialrestores the old copy.NOEPOCH_TREE_EAGER): recursion −0.06 s, because level 1 is limited by the card, not by waiting. The card trace (FAST 454) puts the idle inside the recursion's card holds at 1.2–1.8 s, 13–19 %.f6445c8b6(FAST 452); 35.03 s withNOEPOCH_TREE_AHEAD=0. Fan-in 4 was measured on the inline path (33.82–33.95 s there).a1a3a2c22through production's block verifier, all verified (bases 24.52–25.17 s), so the race fix (a) is shown on the plan's code.ElfConstants) and the per-(AIR, length) shapes can be reused across blocks.Memory: toward typical blocks (head
19fe5e9e5)A median mainnet block (25475471) is 9.78× this one, and the host peak grows about linearly with the block. The head carries three changes for that; none changes a proof byte.
drop_streamed_ops, default on;LAMBDA_VM_BLOCK_DROP_OPS=0keeps them)BLOCK_RECOMMIT_TOP_LEVELS)LAMBDA_VM_FIXED_TRACE_HASH=1)LAMBDA_VM_FIXED_TRACE_HASH=1andLAMBDA_VM_DETERMINISTIC_GRIND, two processes produce the same block proof (digestac406fc8…); a random-key control differs. Byte-identity gates on the block use this.What it is
VmProof. Every table is cut into instances of 2^21 rows, and KECCAK_RND into 2^16-row instances. There is no L2G table and no global proof; memory uses the monolithic PAGE argument.ResidencyMode::RecomputeLdeDevice: after Round 1 only each instance's root is kept. Each instance's fused task commits its trace on the device again, and the prover refuses the proof unless the new root equals the absorbed one, so the proof bytes are unchanged.RetainandRecomputeLdebehave as before.prover::block::prove_block/verify_block. The block verifier is the only one that accepts a chunked KECCAK_RND (AcceleratorShape::KeccakRndChunked). Every other verifier keeps KECCAK_RND to one table.LAMBDA_VM_GATE_PACKING(VRAM-gate packing admission),LAMBDA_VM_TABLE_TIMELINE(per-table timeline),LAMBDA_VM_RECOMMIT_TOP_LEVELS(kept top levels).WindowedTraceBuilder, and every full chunk of CPU, MEMW_R, MEMW_A, MEMW, LOAD, LT, SHIFT and STORE is committed as soon as it exists. Host tests show it equals the serial build.0fe8e4f2f; k = 3 before) areprove_block's default. The ELF data pages' preprocessed roots are computed on the device during execution.Base, block 25368371 on FAST (A/B on one binary; the epoch base is #1009's
prove_continuationon the same binary)e7406d6b5, FAST 396)At
e7406d6b5the block base is about 4.5 s below the epoch base (21.55 against 26.05). The first shared builder cut Round 1's span from 6.3 to 2.4 s, but its window builds sat on the executor's path (execute 1.35 → 6.9 s). With the rebuilt builder and the walk on its own thread, execute is 3.35 s and phase A 7.13 s, and the prove is 14.4 s against the serial build's 18.4 s. Nsight on FAST shows the fused phase is 98.6 % card-busy, so the block is card-bound. Most of that card time was the second hash, which kept top levels remove: phase B recomputes the LDE alone, and the openings rebuild each queried 8-leaf subtree and check it against the kept node. The architecture's main gain is in the recursion (above).S0 census: main 3.301 G elements, aux 1.036 G.
Format change: ECDAS chunked; KECCAK_RND and ECDAS heights capped
Landed at
23b3c8173(FAST 531 gates GREEN; FAST 533 A/B on 25512221: base −0.17 s, no effect on time, as expected; ECDAS cells −25 %, host peak −0.40 GiB).ECDAS is one row per double/add step (≈ 382 per ECSM call, ≈ 4.2 calls per transaction), so a median mainnet block
makes ≈ 420 k rows: one table at 2^19 proves 127.91 bits at DEEP batching on a ≈ 22.5 GiB device set, and a p90 block's
2^20 (126.91 bits, 44.7 GiB) no longer fits a 32 GiB card. The block now cuts ECDAS into instances of at most 2^17 rows;
a scalar multiplication may straddle two instances, its steps chaining only through the Ecdas bus, keyed by the call's
timestamp and the step's
(round, op).AcceleratorShape::KeccakRndChunkedis renamedBlockChunkedand lifts theone-table bound for ECDAS as for KECCAK_RND (count bounded by the sub-proof cross-check). New verifier constants, checked
in
verify_blockand in the tree'scheck_shape: every KECCAK_RND instance ≤ 2^16 rows (129.43 bits) and every ECDASinstance ≤ 2^17 (129.91 bits). This closes G1 (REV-JUDGE item 13, R-NOEPOCH-S3 F1-M1) for KECCAK_RND and ECDAS
only; every other table's height is still bounded by two-adicity alone, and the rest of G1's per-type list (ECSM,
KECCAK, the CPU family, the fixed tables) stays parked.
LAMBDA_VM_BLOCK_KECCAK_RND_LOG2takes 5..=16 (nooff).A block whose ECDAS fits one 2^17 table (25368371: 2^16) builds the same ECDAS table as before (one chunk of every step is the table
generate_optionalbuilt; by construction, not byte-compared on a block); 25512221 (2^18 today, 128.91 bits, 0.04under the minimum of record) now proves 2^17 + 2^16. The epoch and recursion verifiers (
Single) are unchanged.Format change: KECCAK and ECSM chunked; tree partition rule v2 (
5e4176961)Landed with the any-block target. Approved by the lead; Mauro to confirm. It is listed for the cryptography review as S-6 and S-9.
The caps. KECCAK is cut into instances of at most 2^18 rows (129.213 bits) and ECSM into instances of at most 2^17 (129.488 bits), as ECDAS is.
LAMBDA_VM_BLOCK_KECCAK_LOG2(2..=18) andLAMBDA_VM_BLOCK_ECSM_LOG2(2..=17) lower the caps, for tests.Partition rule v2 (
PARTITION_COST_MODEL = 2). Rule v1 pinned every chunk of a table to one leaf. Now the first instance keeps its seeded leaf and later chunks of KECCAK, ECSM and ECDAS fill by load. Without this, a p99 block's ≈ 15 ECDAS chunks overflowed the leaf cap and the plan was refused. The verifier derives the partition by the rule from the shape alone.Evidence:
Known cost (deferred): a table just over a power of two is cut after padding, so for example 2^20 + 1 KECCAK calls make 8 instances, about half of them padding. This matters only on keccak-heavy blocks.
G-pack: generators write the packed traces directly
Default since
d8a422962.LAMBDA_VM_BLOCK_GPACK=0builds each table at 8 bytes a cell and packs it afterwards, as before. Under narrow storage the producer used to generate every main trace as a 64-bit table and then pack it (NarrowMain::pack). At 1× the generators spent more time packing than generating (ULTRA u004a: generate 6.25 thread-s, host pack 9.21).stark::narrow::NarrowWriterstores each word's low bytes at a per-column width chosen up front, and keeps the OR of every word written to each column.finish()narrows in place the columns that were given more bytes than their largest word needs. When a word did not fit, it names the widths the trace needs instead. Either way the bytes areNarrowMain::pack's of the same words, whatever the guess.VmTableand runs throughgenerate_main!(tables::gpack) in aTraceForm:Wideis the old table, used by every build outside the block's narrow storage.Narrowwrites the packed columns at the widths the table kind needed so far in the process (oneWidthHintper kind) and writes the trace again on a miss. A kind's first trace is built wide and packed, to learn the widths (KECCAK_RND and LT through their packed block builds).ChunkJob::generate_as(TraceForm::Narrow), and the finish runs underWindowedTraceBuilder::generate_packed().BLOCK NARROWreports how each trace was built: written packed, narrowed after, written again, or built wide then packed. At the median about 600 traces are written packed, 105 narrowed after, 4 written again and 23 built wide then packed.LAMBDA_VM_FIXED_TRACE_HASH=1+LAMBDA_VM_DETERMINISTIC_GRIND=1gives digest0224203e…with G-pack on and off. Every table of the 1× block built through the windowed builder has the old path's packed bytes (138 tables, twice: before the widths are learned and after).58a58be95: −73.5 % and phase A −7.75 s.Production CLI: prove-block and verify-block
Since
58a58be95. Until this head every whole-block number came from the test harness; the shipped CLI could not prove a block as a tree, had no CUDA build and never purged.lfm::block_tree::prove_block_tree: the base, the harvest, the leaves, the interior and the top, with every in-run check (the base and every child verified beside the run, each leaf's published words, the top's claim, the final check) returning an error instead of panicking. Every knob is read once, byBlockTreeConfig::from_env, under the harness's names and defaults. The harness test is a wrapper that keeps its post-run block verifier; the proof readers it used (HostTable,TableLegs, the child harvest) live inlfm::harvest, re-exported under their old names.alloc_purge::AllocatorHooks(statistics andarena.<all>.purge), so the purge points underauto, the BLOCK MEM columns and the late leaf emission run as in the harness. It still compiles in the never-purge posture; a CLI unit test now reads that setting back, and another shows the installed purge returns freed pages (each fails under its mutation).prove-blockandverify-block, every knob inlfm::block_tree::POSTUREthat the environment leaves unset is set before any thread starts:TABLE_PARALLELISM=8,LAMBDA_VM_VRAM_BUDGET_MB=24000(only whennvidia-smireports a card of at least 31 GiB),LAMBDA_VM_GATE_PACKING=1,LAMBDA_VM_MAX_ROWS_LOG2=21,LFM_PRECOMPUTED_TREE_CACHE_CAP=64,LFM_EXEC_PARALLEL=1,LFM_TREE_SIBLINGS_L0=8,LFM_TREE_SIBLINGS=4. ABLOCK POSTUREline on stderr says what was set; the harness prints how its own environment compares.BlockTreeProof: the claimed shape, the public output and the top node's proof, behind a magic, a version and a pipeline tag.verify-blockisblock_plan::verify_block_treeover those claims, unchanged: the plan and the top program are derived from the trusted ELF under the block presets, and nothing about the format is read from the file.--digestunder the fixed trace hash and the deterministic grind, the CLI's base digest equals the harness's digest test at the same sha (0224203e…, the k4 reference), top2ef0e0d2…; a small asm guest proves and verifies through the CLI.cli prove-blockwith only the instrumentation knobs set: whole 553.77 s, VmRSS 112.33 GiB, purges phase-a 121.39 → 78.73 GiB and base 109.30 → 52.96 GiB, 54.56 GiB spilled;cli verify-blockin its own process passes in 72.86 s at 37.47 GiB (BIG 626, the harness at the same base: 555.29 s, 113.50 GiB).LogUp: four interactions per aux column (the default since
4fc4b7b12)Default
k4(Mauro, 10-05);LAMBDA_VM_ZF_LOGUP=pairrestores the previous bytes. Each base table commits four bus interactions per LogUp aux column instead of two, where that commits fewer extension columns: groups of four have degree 5, which blowup 4 admits, at the price of four composition parts instead of two. The rule is per table and verifier-side (⌈N/k⌉ aux columns + parts, ties keep pairs): KECCAK_RND 516 + 2 → 258 + 4, ECSM 290 → 145, ECDAS 194 → 97, CPU 10 + 2 → 5 + 4, MEMW_A 10 → 5; LT, STORE, MEMW_R, LOAD, PAGE and the small tables keep pairs. The LFM chips keep pairs; #1014 is untouched.ProofFormat.logup(stark), the group/accumulator emitters for k ≥ 3 (one body for the prover folder, the verifier folder and the IR capture), the host and device aux builds grouped by arity, the four-part composition split on the card (radix-2 twice) and its host mirror, compiled kernels for the k4 table programs, the knob atblock_base_options, and one new verifier refusal (parts > blowup).=pairthe 1× digest is ac406fc8 and every program id, kernel key and golden is as before (the small-tree id pin derives under pair and passes; the 44-program golden holds); with the knob unset the base tables prove k4 (1× tree top 2ef0e0d2).4fc4b7b12(Mauro 10-05; ULTRA 018: both arms verify, base −0.89 s, whole −0.92 s; BIG 626: the p90 verifies under k4 at 113.50 GiB).Recursion: sibling proofs share the card through one VRAM gate (on by default)
Before: the recursion's card permit was a mutex, so one proof at a time ran inside
multi_prove. The card then sat idle while the holder ran its host stages: uploads, absorbs, queries. At the median block that was 24.6 s of card idle inside the holds (BIG 469).Now: every
multi_provein the tree admits its tables through one process-wide byte gate, and the artifact commit takes its bytes from the same gate. Sibling proofs overlap wherever their bytes fit. Three parts keep the gate's account matching the card:Retainprove keeps each table's main LDE, trace snapshot and tree on the card from its Round-1 commit until its fused task ends. Those bytes stay in the gate the whole time: the Round-1 task carries them past its own permit, and the fused task takes them over and is admitted only for the rest of its set.multi_proveat once.LAMBDA_VM_SHARED_VRAM_GATE=0restores the exclusive permit.LAMBDA_VM_SHARED_GATE_TRACE=1prints the gate's account (SGATElines). The gate acts only while the tree arms it for concurrent proofs, so the base and every single-proof path are unchanged.Bytes: unchanged, since the gate only reorders admission. The digest is
ac406fc8…, and every A/B arm has the same top program id.Measured:
a93018974against564dd02bb, 4 + 4):Tight claims (head
00871b913, on by default). A claim is a held part R plus a headroom H.LAMBDA_VM_SHARED_GATE_CLAIMS=wholerestores the first form (residents plus the largest table's whole set).278e6a8c6); no regression.Readout note: FAST 871's "claims in force" row read OUT because it counted from the optional trace, which that gate ran without. From each claim's own log line, every gate-on run peaked at 3 claims and the off runs had none.
Tests:
Disk spill: auto by default
What it does. Once Round 1 has committed an instance, its packed main trace can go to a spill file that phase B reads back ahead of its walks. The words that come back are the words that went out, so no proof byte depends on the policy.
LAMBDA_VM_BLOCK_SPILL=auto(default) |off|always|<GiB>(a resident budget for committed packed traces).How
autodecides (prover/src/block.rs,spill_target_bytes/spill_decision). A committed instance is spilled when the host's bytes, plus the reserve, plus the instance's own bytes would pass the target.memory.current, v1memory.usage_in_bytes) less its inactive file pages frommemory.stat, which the kernel reclaims first. Sincecf253d235; the charge alone counted the page cache, and at 1× on FAST it read 25.57 GiB against a working set of 17.09.LAMBDA_VM_BLOCK_SPILL_TARGET_GIB, if set;MemTotal, less 10 GiB. The limit is v2memory.max, or v1memory.limit_in_bytes, read at the process's cgroup path and then at the hierarchy root, which is what a container without a cgroup namespace sees. Since278e6a8c6: FAST 509 read 47.5 GiB on FAST's v1 limit, where the v2-only rule read 49.9;fb0dc0057, underautothey arm only once a spill is plausible (the host's bytes plus the reserve reach 85 % of the target) and then stay armed;alwaysand a fixed budget arm them from the start. At the median they never arm (waits 0.01 / 0.18 s, BIG 122). At the p75 they armed at 59.7 s, for a phase-A cost of +1.12 s against off; armed from the start, the same block cost +3.6 s (BIG 118).Measured, median block 25475471 on BIG (3 runs per arm, one binary per job):
auto(default)auto, 70 GiB targetalwaysalwaysalways(first measurement)ac406fc8…holds under the default (BIG 117) and underalways(BIG 114–116).Blocks up to full gas on BIG (128 GiB host, 120.69 GiB cgroup; one run each):
edddc6873035aef5d6035aef5d6autopurged at phase-a (121.19 → 82.32 GiB) and at the base (116.53 → 48.45). Its verifier passed cold and warm (66.59 / 61.61 s, pool high-water 17.39 GiB; BIG 125). With both purges forced on the pre-gate train it read 549.32 s at 111.30 GiB (BIG 1215).The allocator purge. The harness's jemalloc never purges (
dirty_decay_ms:-1), and a phase rarely reuses the pages the phase before it freed, so the host ratchets from phase to phase. Onearena.<all>.purgehands every arena's dirty pages back.autopurges only once the spill's budgets arm, so a block that fits printsALLOC PURGE <point>: skipped (auto, no memory pressure)and pays nothing (FAST 515 at 1×, BIG 123 at the median).What the cost follows. While the writer runs, the generators slow by ≈ 16 %. The writer's two passes over every spilled byte (digest, then the aligned copy) and the frees of the spilled buffers both contribute; BIG 115 and 116 could not split them further. At the median, phase A is bound by the generators during the walk, so the walk waits on them.
alwayshands ≈ 39 GiB to the writer during the walk, for +6–7 s.always: digest 22, aligned copy 28, pwrite 14. The pwrite runs at the disk's own rate (3.7 GiB/s raw). The BLOCK SPILL line prints the split.Measured and not landed (each has a FAILED-LEVERS row):
Tests:
always, a zero budget andautobuilds the resident traces;autoreads the host's working set, and the target reads v2 and v1 cgroup limits;autopurges only under memory pressure.