Repository navigation
STARK no-epoch (prove-and-retire) prover: block 25368371 — work in progress - #1013
Draft
MauroToscano wants to merge 1427 commits into
Draft
MauroToscano wants to merge 1427 commits into
MauroToscano wants to merge 1427 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.
The windowed build with the lean walk, with the old walk and with each lean part alone, against the whole-run build: six programs (keccak calls, narrow and odd-offset loads and stores), windows of 1 to the whole run, with and without dropping the streamed ops. And each part against what it replaces: the decode table answers exactly the map's pcs (gaps, misaligned pcs, the top of the address space); lean memory accesses read and write what the per-byte ones do (an access across a page, a first touch between two allocated pages, wrapping past u64::MAX, 40k random accesses); the counted lookups equal the listed ones, and differ without the LOAD ops' part on programs with narrow loads; the one-pass routing builds the per-segment routing's segments; the knob's values parse.
column_max_col_major (one block row per column, a shared-memory reduce and atomicMax) gives each column's width; pack_col_major writes every word at its column's width into the stark crate's NarrowMain layout. pack_trace_snapshot packs the trace snapshot a commit leaves in its handle, after the handle's ready event, and downloads only the packed bytes. pack_col_major_from_host is the same from a host trace, for the test against the host pack.
…is freed FAST 505/506: packing the streamed traces on the host cost the record block 0.65-0.71 s, all on phase A's tail (the committers). Under RecomputeLdeDevice with kept top levels a plain table's commit already holds the trace on the card as a column-major snapshot, which it frees. With set_default_pack_after_commit(true) the commit packs that snapshot on the device first and hands the packed trace back in the precommit (take_narrow); TraceTable::install_main_narrow takes it and frees the 64-bit copy. Round 1 does the same for the tables it commits itself, so they are packed for the rest of phase B. Off unless a caller sets it. Tests (card, box): the device pack equals the host pack at every width; traces packed by the device prove Retain's bytes both as precommits and when Round 1 packs them, each widened on the device.
The streamed instances take the trace their commit packed on the device (the host pack stays the fallback for a table committed on the host), and phase B's Round 1 packs the other plain tables after their commits. The BLOCK NARROW line says how many instances the device packed and how long the host packed.
coset_lde_narrow_with_merkle_tree_keep_rpl is the row-major commit with its tree kept on the device, fed a packed trace: the packed columns are widened on the commit's stream into the rows the host upload would have filled (InnerInput::Narrow), as the kept-top recompute already does.
A table packed before its Round-1 commit (the block's finish-built tables) commits on the device from its packed columns (try_expand_leaf_and_tree_narrow_keep); every other commit path reads a widened copy and the trace stays packed. Its fused task then widens it on the device as for the streamed instances, and the commit does not pack it again from its snapshot. Tests: traces packed before Round 1 prove the unpacked bytes under Retain, RecomputeLde and RecomputeLdeDevice (host build: the widened copy); on the card (box) they commit and widen on the device and prove Retain's bytes.
WindowedTraceBuilder::pack_finished_tables (StreamSkip::pack) packs each table finish generates at the bytes its columns need right after it is generated, inside the generation task, so the finish never holds many 64-bit tables at once: on the 4.13x block the finish-built tables are about 29 GiB at 8 bytes a cell. Off unless called; the whole-run build never packs. Test: a windowed build with dropped ops and packed finished tables widens back to the whole-run build, table for table, and did pack.
…sh builds The measurement arm for D-MEMORY M3b: =1 packs every plain table on the device after its commit; =2 also packs the finish-built tables as they are generated, so phase A ends with every table packed and their Round-1 commits read the packed columns. The words are the same.
The executor kept guest memory in a map of 4-byte words keyed by their address through the identity hasher. hashbrown takes its 7-bit control tag from the hash's top bits, so every address below 2^57 gets the same tag and a probe compares keys one by one; the cost grows with the memory a run touches: 31.6 ns a cycle on block 25368371, 108.5 on the median block 25475471 (FAST 591), where the executor becomes the producer's serial floor once the walk is lean. Memory now keeps 64 KiB pages: page n of the low 8 GiB (code, data, heap, private input) and of the top 8 GiB (the stack) is an index into a directory, any other page an entry of a BTreeMap. A page records which of its 4-byte words were written, so iter_bytes yields exactly the bytes it yielded before (as a set; the order differs). Every load and store, its overflow refusals and load_bytes answer as before. LAMBDA_VM_EXEC_MEMORY=words keeps the word map, as the control the pages are measured against; the differential test drives both through 200k random accesses of every width across pages, directories and the top of the address space.
…ARROW=0 keeps it wide) Unset now behaves as LAMBDA_VM_BLOCK_NARROW=2: every plain table's main trace is packed after its Round-1 commit, and the tables phase A's finish builds are packed as they are generated. =1 keeps the device pack after each commit alone, =0 is the 64-bit path. The words are the same, so no proof byte moves (FAST 504/505/508: packed and wide proofs share one digest). The lead accepted the flip on FAST 508's rows (I-MEM.md §6.7).
A measurement knob, off by default: a BLOCK MEM line every half second from the block's start to its proof, and at the marks (start, windows walked, finish done, phase A end, prove end). Each line puts the process's VmRSS beside jemalloc's live / active / resident / mapped / retained bytes (read in the lib's tests, which install jemalloc) and beside what phase A holds where it knows: the streamed chunks waiting for a committer and their ops, what the committers hold, the committed chunks (packed and 64-bit), the builder's run so far, the walk's memory state and the executor's memory. A BLOCK MEM traces line gives the main traces the prove starts from, packed and at 8 B/cell. Lists count at their capacities. No trace changes.
LAMBDA_VM_BLOCK_QUEUE_MIB=n: the streamed chunks waiting for a committer hold at most n MiB of ops; the producer waits for room (and with it the walk and the executor), and a chunk bigger than the budget still goes alone. A chunk leaves the queue once its committer has generated it. Unset, the queue is unbounded as before. LAMBDA_VM_BLOCK_COMMITTERS=n (1..=8) sets the committer threads (3). A BLOCK QUEUE line reports the most bytes and chunks that waited and how long the producer waited for room. A committer that stops on an error frees a waiting producer. Measurement knobs until their gate; no trace changes. Builds on i-mem2's CommitQueue (mem/stark-q1 6c6868635), bounded by bytes instead of chunks.
…at once A packing build (StreamSkip::pack) generates each chunk at 8 bytes a cell and packs it at once, but phase 5 generates every table in one rayon scope, so up to a worker per chunk holds a 64-bit copy at the same time (KECCAK_RND chunks are 2^16 x 1480 cells, 776 MB each). StreamSkip::wide_chunks / the builder's bound_finished_generation(n) give phase 5 n permits: a generator holds one from before it allocates its table until the table is packed (serial work only, so a waiting rayon worker never blocks a holder). The block sets it from LAMBDA_VM_BLOCK_FINISH_WIDE=n (unset or 0: no bound), a measurement knob until its gate. Tables unchanged: the finish-pack builder test also runs at a bound of one.
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.
…(P3a) WrapHash::Poseidon1 is the configuration of a level-0 program verifying a Poseidon1 base proof: a one-cell digest like Algebraic's (one_cell_digest now decides digest_words, words_per_root, the root halves and constant roots), but ZisK's leaf, 4-ary walk and tree (p1w16_emit) behind leaf_hash, merkle_walk and merkle_tree_root, arity() 4 and path_hints(). TranscriptReplay gains a Poseidon1 arm before the algebraic one, under P1Transcript's encodings: a root is [32] then its four lanes, a felt [8] then the felt, an extension element its three coefficients, appended bytes [len] then 8-byte big-endian felts; draws are squeezed felts (three for an extension element, the low bits of one for an index), and state() is the flush of a copy. emit_grinding_check gains the Poseidon1 arm: P1GrindDigest's two width-8 permutations, emulated, then lane 0's top bits. Tests (executed against the host): the replay arm against P1Transcript over every append kind and draw; the grinding check accepts the host's nonce and refuses a miss.
…at through the block plan (P3a) The in-guest verifier's trees follow the base format: SubProofShape gains the trees' arity, FriShape takes it from format.base, and caps count that arity's levels (StarkCaps::for_options_arity, cap_policy_at_arity: at arity 2 exactly today's). CapCells takes its height in tree levels; a P1 cap is 4^c or 2*4^(c-1) nodes under the same mux, its root the 4-ary build, its path three hints per walked 4-ary level. The closed forms count node hashes per path (path_permutations), equal to the hint count at arity 2. The block plan takes BaseFormat from the caller's options: leaves emit under WrapHash::for_base (nodes stay on the pin), the statement replay absorbs hash_pin::statement_tag, and the partition uses the base's cost model (CostModel::for_base; the RPX model and id unchanged, P1 v1 with a provisional fork constant until the census). harvest_block_over dispatches on the format to the P1 verifier on ZisK's transcript, and the legs lay each arity-4 path out in the walk's hint order at the transcript's leaf index. BlockTreeConfig.base and verify_block_tree_for carry the base; no environment read decides it.
The arity-4 cap against the host's own Poseidon1 trees: every depth 1..7 and cap height, the owner path as the proof carries it laid out by the harvest (path_to_cap) and checked in-guest; every hint, cap node, leaf and root word bound. A small spread plan under a P1 base derives its whole tree (socket leaves, pin nodes and top; no id shared with RPX's). The census at production heights splits each leaf's hash rows into the front, the legs' closed form and the forks: P1 forks 123.5 socket rows a sub-proof (P1_FORK_PERMS 124), and RPX's cap scaled by the hash rows a sub-proof (0.580) keeps P1 leaves at RPX's sub-proof counts and ALU heights (P1_LEAF_PERMS_CAP 162,000; at 279,000 a leaf took 26 sub-proofs and 2^21 XALU rows).
fixture_block_options takes the harness's base (NOEPOCH_BASE, NOEPOCH_P1_CAP; RPX unset), leaves execute under their program's hasher and the test-built leaves use the base's wrap hash, so the real-proof leaf suite and the fixture tree prove a Poseidon1 base's leaves on a box. The leaf suite also moves an opening sibling, a FRI sibling and a cap node of each leaf's last instance and expects a refusal. hash_pin_enumeration allows stark::config::cap_policy_at_arity: it reads the caller's format at the caller's arity and names no configuration.
…uction evaluator From the socket review (R-P1SOCKET, SOUND-WITH-ADVISORIES) as p1w16_proof_tests: a Hash16 program proved and verified end to end, and constraint-consistent rows over wrong inputs (or a real witness parked on padding) refused by the verifier (R1); the other square root of x3 and a moved x7 each violate exactly their own constraint, 150 of 150 (R2); the socket's LFM_HASH AIR lowered in-guest agrees with the IR interpreter and the host verifier folder (R3). New: a transposed OnBus coefficient matrix, built test-side from the production interactions, misreads the outputs (the review's chip mutation, run without editing the chip). A3: the_tokens_carry_the_input_and_output_cells reads bus values through BusValue::combine_from instead of its own i64 conversion.
A2: Poseidon1W16Narrow's twelve-felt hashing refuses (permute panics, and every derived hashing method goes through it), as BLAKE3's missing permute does: any value it returned would be a hash no AIR proves. The IV stays the zero constant, because the executor reads mode_iv to build the state that admits then refuses, so the refusal stays a typed executor error. A test pins both. A4: LfmProgram::hash16 is private, set only by compile from the instructions, read through hash16(). A1: the P1 small-tree test asserts the parent derives a P1 leaf's LFM_HASH as the socket from the child's artifacts, the hasher its pinned program id names.
Every production entry point that hashes a twelve-felt row with a program's hasher (the executor under all three schedules, the trace filler) is driven under the width-16 socket with a row of each mode: each refuses with the typed HasherRejected and none reaches the refusing permute. The host block transcript's hasher is pinned at compile time: BLOCK_HASHER can never be the socket.
…ainst RPX) p1_node_leg_census prices a node's legs per child table at production heights; p1_node_program_census emits the small plan's top over a P1 and an RPX leaf and prints each child table's cost drivers. Together they show RYZEN 010's +15 % node instructions is the P1 leaf's second LFM_HASH table: socket rows at the 162k cap sit between 2^17 and 3/4 of 2^18, so HashChunking splits them, where RPX's 1x leaves stay one table.
…mitter LAMBDA_VM_TREE_PROGRAM_BUDGET (auto by default) admits each tree program, in prove order, before it is emitted: auto while VmRSS plus the program stays under the pipeline's host target, off never refusing, <GiB> capping the programs alive. Past the room, the next AHEAD (4) programs the provers will take are always admitted, and no program jumps a lower waiter, so a tight budget cannot deadlock the tree and its emission still runs ahead. emit_ordered streams the deferred programs on several threads and delivers them in order. Generic, shared by both block pipelines; nothing is wired yet.
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.
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.