Repository navigation
STARK no-epoch (prove-and-retire) prover: block 25368371 — work in progress - #1013
Draft
MauroToscano wants to merge 1440 commits into
Draft
MauroToscano wants to merge 1440 commits into
MauroToscano wants to merge 1440 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.
KECCAK_RND chunks are 2^16 x 1480 cells, 776 MB at 8 bytes a cell, and the finish generates them all at once in phase 5 (at the median about 37 of them, the finish's long pole). With StreamSkip::pack each chunk is now built 128 permutations (36 MB) at a time into stark::narrow::NarrowBuilder, which packs each block into its columns and re-encodes a column that a later block needs wider: the result is NarrowMain::pack of the whole table, byte for byte (narrow and keccak_rnd identity tests), and TraceTable::from_narrow_main holds it with no 64-bit copy ever made. KECCAK_RND then takes no wide-chunk permit, so its parallelism is kept. Other builds, debug-checks and disk-spill keep the 64-bit path.
LAMBDA_VM_BLOCK_GENERATORS=n (1..=16): n generator threads take each streamed chunk's job, generate it and (under narrow storage) pack it on the host, and hand it to the committers through a second queue, so the committers only commit and a chunk waits packed (about 2 B/cell) rather than as its ops. LAMBDA_VM_BLOCK_READY_MIB=n bounds that queue by bytes (QueueRoom, as the ops queue). Unset or 0: the committers generate, as before. A committer that stops on an error frees both queues. BLOCK QUEUE reports both queues; BLOCK MEM the chunks ready. build_streamed takes a StreamConfig (read from the environment by the block) so a host test can drive it: the stream builds the same traces and precommits the same instances with 3 generators and every queue held to one chunk, or 1 and 1, as with the committers generating. A measurement knob until its gate.
The finish generates LT from the MEMW-derived ops kept to its end (10 of the record block's 11 LT tables), every chunk at once in phase 5: 2^21 x 17 cells, 285 MB each at 8 bytes a cell. As KECCAK_RND, a packing build now deduplicates each chunk as before and writes its rows 4096 at a time into a NarrowBuilder, so no 64-bit LT table is ever held and no permit is taken. The rows keep their order (one map, one hash state per process): the packed build is the 64-bit build packed, byte for byte (lt_tests).
…m's threads The executor's log windows on their way to the walker and the walked windows on their way to the accumulator (two bounded channels plus the windows each thread holds): at 4.13x on BIG about 7.5 GiB of phase A's live heap was not named by the ledger, and these are its first candidates. Measurement only.
…ore the finish On BIG at 4.13x the posture's never-purge allocator left the finish's working set on top of the pages the windows phase had freed (resident 55.4 GiB at the finish against 50.7 live); a run with decay 0 throughout peaked 10.3 GiB lower but walked 1.8x slower. This purges once instead: when the run is walked, every arena's decay is set to 0 (which purges at once) and back. A BLOCK PURGE line reports the time and VmRSS before and after. In the lib's tests, which install jemalloc; a measurement knob, off by default.
Phase 4 round-robins its collectors into at most eight 80 MiB histograms, but LT, KECCAK and the other per-op sources were one collector each: at the median block LT (2.6 G cells of its ops kept to the finish) and KECCAK were single long poles, and each built one list of every lookup it sends (LT 8 lookups per op, KECCAK about 5,000 per permutation) before counting it. Every source that is a sum over its ops is now cut into slices of whole ops (LT, SHIFT, BRANCH, BYTEWISE, EQ, STORE 2^20; MEMW_A 2^22; KECCAK 2^11; ECDAS 2^16), and MUL and DVRM, which deduplicate per instance, into one slice per instance. The histogram is a commutative sum, so BITWISE does not move: the 187 whole-run trace digests (four programs at small and default caps) are equal before and after.
…rn freed pages during the finish On BIG at 7.42x the finish ends with 40 GiB of jemalloc's resident pages not live: among them the streamed chunks' ops, allocated by the walker and the accumulator and freed by the committers while the finish runs, which no other thread's arena reuses. This sets those two arenas' dirty and muzzy decay to 0 (purge at once, and on every later free) from the walk's end until the committers are done, then puts back what they had; every other arena keeps the posture. BLOCK DRAIN PURGE reports the arenas. In the lib's tests, which install jemalloc; a measurement knob, off by default.
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.
…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.
With LAMBDA_VM_BLOCK_MEMLOG=1 the block installs a finish-marks hook (trace_builder::set_finish_marks) for phase A: build_traces calls it after phase 3 (LT), phase 4 (BITWISE), as each phase-5 generator finishes and when phase 5 is done, and each call prints a BLOCK MEM line on the ledger's clock, so the finish's memory (+23 GiB live at the median) can be read per phase and per table. Unset, nothing is called; no table changes.
…sed walk At the median block (BR-MED, BIG 440b) the heaviest-first fused walk puts the 36 KECCAK_RND instances ahead of CPU, and with packing every slot freed in the first ~28 s goes to the next KECCAK_RND, LT or PAGE table: the card runs at ~68 % there and at 100 % for the rest, with the gate full throughout. LAMBDA_VM_FUSED_WALK=mix keys the j-th of a type's n tables (j + 1/2)/n and walks the keys ascending, so every prefix of the walk holds each type in its share of the whole. Unset or `heaviest` keeps today's walk; anything else stops the run. The walk only orders the drivers' claims: each table proves on its own transcript fork and the proofs are drained in index order, so no proof byte depends on it. With LAMBDA_VM_TABLE_TIMELINE=1 and LFM_PROVE_SPLIT=1 each TABLE TL line now also carries that table's own stage seconds (recommit, aux build and commit, rounds 2-4), from a per-driver-thread copy of the per-table slots: the stages run on the driver thread that claimed the table. Both off by default.
… 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.
…_VM_BLOCK_GENERATORS=0 keeps the committers generating) Each streamed chunk is generated, and packed on the host, by one of six generator threads before a committer takes it, so the committers only commit and a chunk waits packed rather than as its ops. On BIG at the median block (25475471) with E1 and E4 the ops waiting for a committer fell from 32.8 to 1.4 GiB, the peak from 96.1 to 82.3 GiB and the base from 231.8 to 219.6 s; at 7.42x 75.4 to 66.8 GiB and 178.5 to 172.7 s; at 1x the base moved -0.05 s (BIG 103, D g6 g6 D). The digest under fixed+dgrind was ac406fc8... with generators on (BIG 101). No trace changes.
…ish marks and six generators, the base for levers 1 and 3
… then packs them The A arm of the packed builds (badec90, ab807a2): with narrow storage the finish builds KECCAK_RND and LT at 8 bytes a cell and packs each afterwards, as every other table, instead of a block at a time (WindowedTraceBuilder::build_wide_then_pack, StreamSkip::wide_builds). i-median measured the median's phase B 7 s slower on a head with the packed builds than on one without; this knob is the in-run control. The words are the same either way (the finish-pack builder test also runs the wide arm).
… gate The committer side of the finish's hand-off (I-SCHED levers 1 and 3), on the generators' stream: - The committers' unit is a FinishedTable: a streamed chunk or a table the finish handed off. BlockFinishSink puts a handed table into the committers' queue behind the streamed chunks without waiting (no ops budget: it is built already); a generator passes it through ungenerated, and the committer makes its Round-1 commit under finish_sink::air_for, which replaces stream_air. Every committed table goes back with finish_sink::insert_finished. - A finished table the device packed after its commit drops its 64-bit copy there, as phase B's Round 1 does after the same commit. - LAMBDA_VM_BLOCK_FINISH_COMMIT=after hands every plain table the finish built to the committers once it returns (finish_sink::hand_built): the finish does not hand its tables off while it builds them yet, so this is a measurement arm and the committer side's gate, not the overlap itself. Unset: phase B commits them, as before. - Phase A's card gate: each commit is admitted by its device set (the estimate phase B's Round 1 uses) under the card's admission budget, so more committers cannot over-fill the card; before, each commit was admitted alone against the whole budget. LAMBDA_VM_BLOCK_CARD_GATE=0 drops it. A BLOCK CARD GATE line reports the most it held, the committers' wait and the finished tables committed. The roots are still absorbed in AIR order and each precommit is placed by name, so no proof byte moves. Test: the stream with the finish's tables committed in phase A, the committers generating or generators ahead of them, under a gate that admits one commit at a time, builds the same traces, precommits every plain table, and leaves the ledger empty (a sink that declines everything fails it).
…, finish permits, queue budgets) BIG 101 and BIG 103 read no effect for the purge before the finish (LAMBDA_VM_BLOCK_PURGE), the drain purge of the producer's arenas (LAMBDA_VM_BLOCK_DRAIN_PURGE) and the finish's wide-chunk permits (LAMBDA_VM_BLOCK_FINISH_WIDE, StreamSkip::wide_chunks, WidePermits); the queue budgets (LAMBDA_VM_BLOCK_QUEUE_MIB, LAMBDA_VM_BLOCK_READY_MIB) are not needed once generators keep the queues short. Their records stay in FAILED-LEVERS.md and I-MEM.md. QueueRoom keeps counting what waits, for BLOCK QUEUE; the stream test runs 2, 1 and 6 generators. No trace changes.
…LOCK_PACKED_BUILD=1 turns them on) BIG 104's in-run A/B at the median (one binary, P W W P): with the packed builds phase B was 6.32 s slower (P 145.75 / 141.34, W 138.29 / 136.16 s) and the base 3.80 s slower, against a peak 14.75 GiB lower (82.9 vs 97.6 GiB). That is over the lead's 3 s line for a default, so the finish builds every table at 8 bytes a cell and packs it afterwards unless the knob is set. The words are the same either way.
…g them Phase 3 extended the kept LT tail with the MEMW and MEMW_A prefixes (the LT ops of the MEMW chunks already handed out), the ops it derives from the MEMW tails and the HINT range checks: at the median block several GiB of LtOperation copied by Vec reallocation (BIG 103's finish marks: jemalloc resident +5.9 GiB across phase 3 with live flat). The segments are now kept apart (Segmented): phase 4 counts them slice by slice, and LT's chunks are cut from them by chunk_and_generate_segmented, each chunk borrowed from one segment or copied only when it straddles two, when its generation starts. generate_chunks_with is generate_chunks over such views. The chunks are the concatenation's: a test checks every split, chunk size, streamed-chunk mode and the empty list against chunk_and_generate_skipping (a straddling chunk that is not copied fails it), and the 187 whole-run trace digests are equal before and after.
…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.
Under LAMBDA_VM_TREE_PROGRAM_BUDGET (auto by default; the pipeline mode without an emission window), every leaf and node program is admitted in prove order before it is emitted. Beside phase B the late emission admits leaves in order while the budget has room; the builder emits the rest on four streaming threads as the budget admits them; each early node is admitted before its emission. A permit travels in the slot and is dropped with its program by the prover. On a host with room nothing waits, so the schedule is the one before. The programs are the same, so no id moves.
…the cap in the tag (REV-P1-JUDGE) The adversarial P1 review (REV-P1-JUDGE, SOUND-AFTER-FIXES) requires four P1-local items before landing; this builds them. 1. Leaf width tag. Every P1 leaf's first-block capacity is [len, LEAF_DOMAIN, 0, 0] (LEAF_DOMAIN = poseidon1_w16::DOMAIN_LEAF, "P1WL"), mirroring RPX's leaf capacity: poseidon1_stark::linear_hash, the P1 backends through it, the production p1s_* device leaf kernels (zisk_leaf<V, TAG>; the measurement kernels keep ZisK's untagged leaf) and the emitted p1w16_emit::leaf_hash. ZisK's untagged leaf stays as zisk_linear_hash for its known-answer vectors. A leaf now binds its width: the judge's shape-dual family (w = 12, 18, 24, 30) parts, and the node(a,b,c,0) = leaf and in-block zero-padding identities are gone. No extra permutation. Every P1 byte and id moves; RPX's do not. 2. F4: at arity 4, cap 0 and odd depth the host requires the top group's two padding siblings to be the padding node, as the in-guest walk supplies them (cap.rs). 3. F2: the P1 statement tag names the policy (C0 for Off/Fixed(0), C<h>, Cauto), and checked_base refuses Fixed(c) above the arity-4 clamp (8). 4. The M8 gap: B's every-cap-node-is-bound test lands. The reviewers' public tests land, flipped where these change them (A: the inverse-permutation collision, the F4 pair, the tag, the raw sample; B: the cap root, cross-verification, the W8 grind, the zero-padded opening with its RPX control, the tag; the judge's width-tag family and identity tests on the production leaf). Tests naming the inherited heights premise stay out. The tagged leaf is pinned in Rust and, through the host shim, in the device kernels' host KAT.
…H_ELF_CONSTS) The constants took the four-thread pool beside the base and committed the block ELF's twelve data pages one at a time. At P1's 12.2 s 1x base that was 12.9 s, so the harvest waited 3.7 s and every leaf program, which needs the constants, was emitted after the base (RYZEN 011). They now compute on a host-only pool of their own, eight threads by default, DECODE and the pages at once (ElfConstants::compute_parallel); the pool beside the base keeps its four for the leaf programs. NOEPOCH_ELF_CONSTS=0 restores the old path. The constants are the same: tests pin compute_parallel to compute at widths 1, 3 and 8, on synthetic pages and on an ELF, and the plan still refuses another ELF's or other options' constants. A box instrument checks the block ELF at 4, 8 and 16.
…nstrument) p1_one_table_per_leaf_sizing derives the P1 cap-1 plan over a real block's shape (AIR-name rows reconstructed from a box run's census and table walk) and, per leaf cap, emits every leaf: the socket tables (one, or split by HashChunking), the instructions, cells and FAST cost law, and the node legs a parent pays for its children; and the no-split rule's cells and legs at the same cap. Emission only, no proof. partition_at_cap re-runs the rule under another cap (test-only).
…short LAMBDA_VM_TREE_LEVEL_PURGE (auto by default) purges every arena after a tree level once the block's memory is short and VmRSS has reached 90 % of the host target: a level frees its programs and working sets into pages the next level rarely reuses (the p90 recursion held 12.9-30 GiB over its live heap on a 74 GiB emulated host, BIG 662). A host with room never purges there; off never purges there; always purges after every level.
LFM_PRECOMPUTED_TREE_CACHE_CAP, when the environment leaves it unset, is set by the CLI's posture from the host target (the spill target): 64 entries (about 6.2 GiB once full) from a 64 GiB target up, 16 below it. A miss only rebuilds a tree whose root is the key, so nothing moves in a proof. The BLOCK POSTURE line compares the knob against the same rule.
…H table a leaf) At v1's 162,000 every production P1 leaf held 2^17 to 3/4 * 2^18 socket rows, so HashChunking split its LFM_HASH table in two and each parent verified both. At 260,000 the leaves fill one 2^18 table: over the real block shapes (reconstructed from RYZEN 011/012), 5 leaves at 1x instead of 8 and 32 at the median instead of 52, socket rows 219,516-227,012 and 249,805-257,341, the parents' legs -41 % and -43 %, the leaves' cost law +0.31 s and -1.07 s. A new model id (0x5031_0002) moves only the P1 tree ids; RPX's model, its partitions and every RPX id are unchanged. no_production_height_p1_leaf_ splits_its_hash_table checks the production-height plan's leaves; the sizing instrument also prints each leaf's socket rows against its closed form.
NOEPOCH_LEAVES forced the partition in the harvest only, while the pipeline's leaf programs were emitted beside the base over the plan's own partition, so level 0 took programs of another tree than its arenas. The forced count now partitions the plan beside the base too (test builds only, as before), so a forced arm proves one tree.
Brings #1013's six commits since 1a98537 (the staged precomputed-tree download as the default, its per-path harness prints, no disk only where live regeneration can drop) under the Poseidon1 base, P3a level 0, the ELF constants' own pool and the P1 cost model v2. The memory default lands in prove_block_under, the body both hashes share. One conflict, in the tree harness: it keeps the base-format lines and reads the download totals after the P1 statics are warmed.
…he GPU suite) Per PR, the host-KAT job also runs the Poseidon1 width-16 kernels' known answers (g++, seconds): the permutation, the base's width-tagged leaf kernels against the host's tagged leaf, ZisK's untagged leaf, the 4-ary node and the W8 grind. On the merge-queue GPU suite, group 7 proves add.elf's no-epoch base under RPX and under Poseidon1 and runs the P1 refusals (other format, other dispatch arm, RPX's statement tag, flipped bytes): about 16 s of proving on an RTX 5090.
A walk's lists, and the kept rest built from them, counted ECSM ops at their inline size, so the double/add steps every witness holds (one Vec of ECDAS steps a call) showed up only as unnamed memory. The ECSM list now counts each op's steps buffer too. Logging only; the tables are unchanged. (#1014's 02cb536, on this builder.)
… byte-identical) collect_ecsm_ops cloned each witness's steps into the ECDAS ops and kept the whole witness, steps included, in the ECSM op for the rest of the run. Nothing reads an ECSM op's steps: its table and its BITWISE lookups read the witness's other fields. The steps are now taken out of the witness and moved into the ECDAS ops, so each call's steps are held once. Tables are unchanged: a test builds a call's ops for six scalars and checks the ECDAS rows against a fresh witness's steps, the ECSM row against the fresh witness, and that the ECSM op keeps no steps. (#1014's b09c122, on this builder.)
Unset, NOEPOCH_ELF_CONSTS now decides by the base: a pool of their own of 8 threads under P1, whose 12 s 1x base cannot hide them (RYZEN 022: the whole -3.40 s), and the pool beside the base under RPX, whose longer base already hides them and where their own pool was neutral (+0.04 s) and held the leaf programs 6 s longer (+0.65 GiB of host peak, RYZEN 021). RPX's default is #1013's in bytes, time and memory. 0 and <threads> apply to both hashes.
Brings the program budget (the tree's programs emitted under a host budget, level purges, the CLI's cache-cap posture) and the S0e port (ECSM steps in the ECDAS ops) under the Poseidon1 base. One conflict: BlockTreeConfig gains both the base format and the program budget. P1 leaves go through the budget as RPX's do: the budget takes the plan the pool beside the base derives (after the harness's forced count), sizes each leaf's estimate from leaf 0's own program, and the builder builds every program's artifacts under the program's own hasher.
…d the builder The ledger's builder term was stored during the walk and never reset, so every line after the finish (phase B's included) still showed the run's builder as held. The finish consumes the builder (finish_handing takes it by value), so the term is set to 0 before the 'finish done' line. Logging only; nothing reads the term.
…te-identical) Port of #1014's S3c-BRANCH (5170a9e, 2b4ae41). The BRANCH segment (32 bytes an op, 2.44 GiB at p90 on #1014) is kept as a DeltaStream: a flags byte and three zigzag LEB128 varints an op, in 64 MiB blocks never reallocated, with a sparse index every 4096 ops so any range expands on its own. Every op takes at most 31 bytes, so it is lossless with no raw form. The run's segments take each op as it is routed (route_ops_into pushes into the stream); a window's routing is appended op for op. p4 counts BRANCH's lookups range by range, and its tables are chunked off the stream as a compact segment (chunk_and_generate_segmented with no skip, optional: the chunks chunk_and_generate_optional makes). Tests: the codec's (any range across the index and small blocks, chunks starting past a mark, the worst op at 31 bytes, the table of the expanded ops); the lean routing tests compare the stream by its ops; the whole-run and windowed builds, plain and dropping, make the same tables with an index mark every three ops. The digest probe's 351 table-set digests are identical against 20f8d3b.
…ical) Port of #1014's S3c-EQ (c8612fb). The EQ segment (24 bytes an op, 1.20 GiB at p90 on #1014) is a DeltaStream: a flags byte (invert, and how each operand is coded) and two zigzag varints, `a` as it is or from the previous op's, `b` as it is, from the op's own `a` or from the previous op's, each the cheapest. Every op takes at most 21 bytes, so any op is kept losslessly. The run's segments push each op as it is routed; p4 counts EQ's lookups range by range; its tables are chunked off the stream as a compact segment. Tests: the codec's (any range across the index and small blocks, every chunk size around the index's spacing and at marks every three ops, the worst op at 21 bytes, the table of the expanded ops); the routing and dense-mark build tests pass. The digest probe's 351 digests are identical against 20f8d3b.
…; byte-identical) Port of #1014's S3c-BYTEWISE (34ab1aa). The BYTEWISE segment (24 bytes an op, 1.03 GiB at p90 on #1014) is a DeltaStream: a flags byte (how each operand is coded, and the opcode when it is under 8; a larger one follows in a byte of its own) and two zigzag varints, `a` as it is or from the previous op's, `b` as it is, from the op's own `a` or from the previous op's, each the cheapest. Every op takes at most 22 bytes, so any op is kept losslessly. The run's segments push each op as it is routed; p4 counts BYTEWISE's lookups range by range; its tables are chunked off the stream as a compact segment. Tests: the codec's (any range across the index and small blocks, every chunk size around the index's spacing and at marks every three ops, operands at both ends of u64 / i64 and an opcode past the flags byte, the worst op at 22 bytes, the table of the expanded ops); the routing and dense-mark build tests pass. The digest probe's 351 digests are identical against 20f8d3b.
…ort; byte-identical) Port of #1014's S3c-ECDAS (in 6f0dc78). An ECDAS row is 1.87 KB, 1.5 KB of it the carries c0 / c1 / c2 (three [i64; 64]), which the table range-checks as offset 16-bit values. The walk now keeps each row as a CompactEcdasOp, its carries offset to u16 (about 0.72 KB a row); a row any of whose carries does not fit keeps all three as they are (boxed), so every row widens back to exactly its op whatever the input, with no release assert relied on. An ECSM call's rows are converted as the walk emits them, so the run's ECDAS list never exists wide. Phase 4 counts each row's lookups from the widened op (the lookups are split out as ecdas_lookups); the tables are generated by generate_ecdas_rows_of, which widens each row as it fills it, at the padded height generate_ecdas_trace_as uses, chunked as before. Tests: a compact row widens to its op, carries at both ends of their 16-bit range held offset and any carry outside it (by one, or at either end of i64) held raw; the table of compact rows is the table of the ops, wide and packed, the raw rows included; real ECSM calls' rows are all held offset, count the ops' lookups and build the ops' table. The digest probe's 351 digests are identical against 20f8d3b.
…e (byte-identical) The table phase's generators borrowed every op list, so every list lived until the last family's tables were made (LT's, at p90). A generator that is the only reader of its lists now owns them (a move closure, run once through `run`, in the rayon scope and in the sequential path alike), so each list is freed as its own family finishes: MEMW, MEMW_A, MEMW_R, LOAD, SHIFT, MUL, DVRM, BRANCH, EQ, BYTEWISE, STORE, CPU32, COMMIT, BLAKE3, ECSM, ECDAS and HINT, plus BITWISE's histogram and the register map. The lists two generators read (CPU, KECCAK) and LT's segments stay borrowed. Phase 4's serial path consumes its collectors so none still borrows a list. Only when the memory is freed changes; the tables are the same. The digest probe's 351 digests are identical against 20f8d3b; the trace_builder, ecdas and windowed-builder suites pass.
One line after the top proof's size: blake3 over every base instance's main-trace root, in AIR order. Under LAMBDA_VM_FIXED_TRACE_HASH=1 two runs that build the same traces print the same digest whatever their grinding, so a box gate can check trace identity at any block size without the deterministic grind (whose base at 1x takes ~12x longer). Test harness only.
…estamp The CPU holds its clock in one column and sends a zero high word on the Memw bus; MEMW_R receives the timestamp as two 32-bit words. Below 2^32 the messages are one; past it only the two timestamp slots differ. The block's clock is 4·cycle + 4 over the whole execution, so a block past 2^30 cycles cannot balance the Memw bus (T200-R, 1.83 G cycles, refused with BusImbalance).
…imestamp) A cycle's timestamp is 4·cycle + 4 over the whole run, and the CPU sends it with a zero high word while the tables it talks to take two 32-bit words. At 2^32 the two encodings part, the buses cannot balance and the proof cannot verify (T200-R, 1.83 G cycles: BusImbalance). The walk now refuses, with Error::ClockPastLimit, the window whose last cycle would reach 2^32 (cycle 2^30 − 1), and the finish refuses a final PC token the last chunk's padding rows would put there. Below the bound nothing changes. LAMBDA_VM_BLOCK_UNVERIFIABLE_CLOCK=1 proves past the bound anyway, for memory and timing measurements, with a warning that the proof will not verify.
…the knob is release-only The REGISTER table's final PC token, halt_timestamp + 4·padding_rows + 1, is the largest timestamp a run's trace holds: the last CPU padding row's PC write. The finish now takes it from clock::final_pc_timestamp, and a test builds a run just under 2^30 cycles whose padding rows cross 2^32: every window fits, the CPU trace's last padded row writes the PC at the final PC token, and that token is refused. LAMBDA_VM_BLOCK_UNVERIFIABLE_CLOCK=1 proves past the bound only in a release build: HALT and HINT debug-assert 32-bit timestamps, so a build with debug assertions refuses instead of proving into them.
LAMBDA_VM_ALLOC_WATERMARK (auto by default) runs one monitor thread for the block: every 0.5 s it reads VmRSS, and once the block's memory is short, VmRSS has reached 90 % of the host target and the allocator holds at least 4 GiB of freed pages, it purges every arena, at most once per 5 s. It reaches the pages a phase frees and does not reuse inside the phase, which the boundary points cannot (at the p90 block on a 48 GiB emulated host, phase A's end and level 1's end, BIG 683). A host with room never fires it. Each fire prints one ALLOC WATERMARK line with the time, VmRSS before and after and the purge's duration; the driver prints the count at the end.
…tree cache's live bytes The watermark monitor now samples every 0.5 s whatever its setting (off only stops it purging): the highest-VmRSS reading of a window, with jemalloc's allocated and resident bytes at it. The driver prints one ALLOC PEAK line for the base and for each tree level, with the precomputed-tree cache's live node bytes (a new reading in the stark crate: inserts add, the cap's evictions remove). Measurement only.
auto admitted a tree program by room while VmRSS plus the program stayed under the host target, so it spent again whatever the allocator's watermark (at 0.9 of the target) returned: at the p90 block on a 48 GiB emulated host, level 1's live heap was 42-46 GiB with the watermark against 30-32 without it (RYZEN 050). The room line is now a share of the target, 0.75 by default, below the watermark's; above it, programs come in by the AHEAD rule alone. LAMBDA_VM_TREE_PROGRAM_BUDGET_SHARE sets the share; 1.0 is the line at the target, the budget before.
MauroToscano
added a commit
that referenced
this pull request
Oct 7, 2026
… block) LFM_PRECOMPUTED_TREE_CACHE_CAP, when the environment leaves it unset, is set by the CLI's posture from the host target (block_whir's spill target): 64 entries (about 6.2 GiB once full) from a 64 GiB target up, 16 below it, as #1013's CLI does (49c4bb5). A miss only rebuilds a tree whose root is the key, so nothing moves in a proof. The BLOCK POSTURE line compares the knob against the same rule, and a note says when the posture set 16.
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.
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.