ZisK-style proof-format levers: Merkle caps, DP FRI folding, WHIR first fold - #1007
Merged
Merged
Conversation
A tree of depth D can publish its cap, the 2^c nodes c levels below the
root, once, and cut every authentication path to D - c siblings. The
verifier folds each path onto cap[index >> (D - c)] and checks once per
tree that the cap hashes to the committed root. The root stays the
commitment, so no transcript changes.
New merkle_tree::cap module (design/CAP.md sections 1-2):
- MerkleTree::depth / MerkleTree::cap (heap slice, disk-spill safe;
None for a root-only tree or c > depth: fail closed, never clamp).
- Proof::truncate_to_cap, cap_root, verify_cap, and
verify_merkle_path_to_cap_from_leaf_hash, which checks the exact path
length, index < 2^D and the cap length, then runs the unchanged
verify_merkle_path_from_leaf_hash against the cap node.
- The owner-path wire encoding (split_owner_path / embed_cap): the cap
rides at the end of the tree's first opening, so c = 0 moves no byte.
- CappedRoot: one per tree; its only capped constructor authenticates the
cap against the root before handing it out.
- CapPolicy { Off, Auto, Fixed(c) } with the integer cost-law weights
(AUTO_WEIGHTS) that give c = 3 at >= 20 openings, 2 at 4-19, 0 below,
clamped to the depth; FromStr/Display for the knob spellings.
Nothing calls it yet. Tests: the cap is the heap slice and hashes to the
root for 1..1024 leaves and every height; every leaf verifies against its
cap node, and at c = 0 agrees with the full-path check; tamper tests (cap
byte, path node, swapped cap nodes, foreign cap, flipped index bit, path
length +-1, cap on the wrong opening, wrong height); mutation-style tests
that run the same property against copies without the length check, with
the wrong cap index, and without the cap-to-root check, and show each
copy fails; the Auto heights and weights pinned.
The host verifier folded an authentication path of any length and compared the result with the root. A path one node short compares an internal node with the root. No exploit is known: it needs a leaf hash equal to an internal node, a cross-function collision under the algebraic backend (design/CAP.md section 9.4). But every tree depth is a verifier constant, so it is now enforced: - trace, precomputed, aux and composition trees: log2(lde) - 1 (row-pair leaves; 0 for a two-point LDE, where the leaf hash is the root); - committed FRI layer i: log2(lde) - i - 2. Every opening now goes through CappedRoot::uncapped(root, depth), the cap primitive at c = 0: the same fold as before, plus the exact-length and index < 2^depth checks. Honest proofs already meet these lengths, so they verify unchanged. Only malformed proofs see a difference. No proof byte, root or transcript moves. The archived (guest) path shares these functions, so it is hardened too. Tests (tests::path_length_tests, small AIR, 1024 rows): honest proofs carry exactly the verifier depths for main, composition and every FRI layer, and verify. A path one node short or long is rejected for main (first and last query), composition, and the first and last FRI layer. With honest data, the old code also rejected these lengths, because a forgery needs a collision. The check is shown load-bearing at the primitive level (merkle_tree::cap mutation test with an identity leaf hash).
…ields
The ZF campaign's levers get one config and one banner before any lever
lands, so the option structs stay stable while the lanes fill them in.
prover/src/zf_format.rs: ZfFormat { cap, whir_cap, fri, one_row,
whir_folds }, parsed from LAMBDA_VM_ZF_CAP / _WHIR_CAP / _FRI / _ONE_ROW /
_WHIR_FOLDS through from_lookup (tests pass a map; none sets the env).
ZfFormat::global() reads it once and prints
"ZF FORMAT: cap=off whir_cap=off fri=pair one_row=0 whir_folds=uniform4"
on every setting, including the default. An unknown value aborts. So
does a knob set to a lever this build does not implement yet, because
otherwise a run could print a non-default format and prove the default
one. Each lane flips its *_IMPLEMENTED constant; all are false here.
The format travels in the crypto crates' own option types (RULINGS 9):
- stark::ProofOptions.format: ProofFormat { merkle_cap, fri_mode,
one_row }. FriMode and OneRowMode are defined next to it.
- multilinear::ChainConfig.format: ChainFormat { cap, folds } with
WhirFolds { Uniform, Dp, List(FoldList) }.
Each is grouped in one field, so a literal names the format in one line
and a lever added later touches only its format struct. Literal sites
get format: ...::DEFAULT (mechanical).
RULINGS 10, what I found: repo-wide, nothing serializes a ProofOptions
into pinned bytes. The one by-value holder, AirContext, derives no serde
or rkyv, and no rkyv/bincode/serde_json call takes options. ChainConfig
has no serde or rkyv derive. To make this hold by construction,
ProofOptions.format is #[serde(skip)] and #[rkyv(with = Skip)] (default
on deserialize), so serialized options keep today's bytes whatever the
format; a test pins that for rkyv and serde_json. The WHIR statement
absorbs (push_config, multilinear absorb x3) bind format: _ and do not
absorb it: absorbing it would move every transcript at the default.
Production format sites: aggregation_wrap_options (every LFM proof),
chain_config (WHIR base), and the new block_base_options (STARK base
epochs: the Blowup4 preset plus the format), used by the three
production drivers in per_table_aggregator_tests. With nothing set,
each builds today's value (tested).
RULINGS 11: both RV64 recursion-guest entries (verify_and_attest_blob,
verify_continuation_and_attest) refuse options with a non-default
format, returning an error rather than panicking.
No lever does anything yet. Defaults are today's bytes.
…ed FriFoldLayout New `fri::schedule`: the integer dynamic program of FRI.md §2.1 that picks the fold exponent of each committed FRI layer from public shape constants only (first committed size, terminal size, query count, the cap-height function as a parameter, DMAX = 6). Cost is kept in units of 1/Q so the format function is u64-only, with the (cost, trees) lexicographic tie rule (smallest d first). Also the FriMode / OneRowMode enums and FriFormat, the verifier-side constants a layout is built from. `FriFoldLayout` gains `schedule` (per committed layer) and `one_row`; `num_committed = schedule.len()`. `FriFoldLayout::new` is now `for_format(.., FriFormat::LEGACY)`, i.e. the all-ones schedule through the general constructor, and produces the same total_folds / num_committed / terminal_len / effective_k as before. The struct is no longer Copy (it owns a Vec); no call site copied it. No caller uses a non-legacy format yet, so no behaviour changes; ProofOptions and every serialized type are untouched. Tests (fri_schedule_tests): the FRI.md §2.2 table pinned for T = 9 and 10 under three cap functions (off, the design model's, CAP.md §2 Auto, implemented locally until the cap primitive lands); brute-force optimality of the DP for b0 <= 16; legacy_layout_equals_old_layout against a verbatim copy of the old constructor over B <= 30, blowup_log 1..4, k 0..10.
…fold word
WhirFolds becomes { Uniform, First(FirstFold) }: the first round folds k0
variables (all of them when the chain has fewer) and every later round is
today's walk, log_folding with the remainder last. A config serves chains of
every height, so a per-round list would have to say what a shorter chain
does with it; the lever design/WHIR.md measured is the first fold alone.
The C2 skeleton's Dp and List variants are removed (RULINGS 15: no DP, and
the knob is uniform4 | first5 | first6). FirstFold holds 1..=MAX_FOLD (6),
the widest fold the stack is tested at; nothing else is constructible.
- schedule(): Uniform runs today's body verbatim (tested against a copy of
it for n <= 40, k 1..=6).
- with_security_folds(): Q is charged the worst round count of any chain of
<= tallest variables under the schedule. Uniform gives exactly today's
config (tested on the grid); first5/first6 never add a round at any height,
so Q never rises, and it is 112 at 25 (6 rounds instead of 7).
- fold_word(): the statement word. Uniform = log_folding (4u64 at the
default, today's bytes); First(k0) = 1<<63 | log_folding<<52 | 1<<48 | k0
(design/WHIR.md's prefix encoding, one entry). Not absorbed yet.
- zf_format: LAMBDA_VM_ZF_WHIR_FOLDS accepts uniform4 | first5 | first6 and
refuses dp, lists and other first<k>. WHIR_FOLDS_IMPLEMENTED stays false.
Host prove/verify at k0 = 5, 6 (n = 3..11), a tampered 64-wide base block
rejected, and a first6 proof refused under uniform4 (and back).
S5: CapPolicy::Auto is now RULINGS 1's table stated directly (3 from 20 openings, 2 from 4, else 0, clamped to the depth), with the thresholds as named format constants. No arithmetic runs on the policy path, so no verifier can disagree on an overflow. cap_gain stays (the FRI schedule DP prices with the same weights) but is bounded: a height past MAX_CAP_HEIGHT returns i128::MIN instead of shifting, and every term fits i128 for any usize opening count, on 32-bit wasm too. Pinned: the table is the cost-law argmax for every opening count up to 10^6 and at the usize extremes. The depth-clamped table and a depth-bounded argmax differ at exactly one point (4 openings, depth 1: table 1, argmax 0); a test pins that single difference. M1: two fixtures that only one check rejects, on the real keccak backend: - the real internal node above leaf 0 / leaf 2^D-1 presented as a leaf hash with a path one sibling short: the length-agnostic fold accepts it, only siblings.len() == D - c rejects it (every c < D, c = 0 is C1b); - an unreached cap node flipped with 3 queries at c = 3: every per-query check passes, only the cap-to-root check rejects it. Checked by hand: deleting the length check or the verify_cap call in from_owner makes the matching test fail.
…itments agree on it The three host absorbs (monolithic, epoch, global) and the LFM emitter's push_config write ChainConfig::fold_word() where they wrote log_folding. At the default schedule that is log_folding itself, 4u64, so every default statement, transcript KAT and byte gate keeps its bytes; under first5/first6 it is a tagged word, so the 245-byte statement keeps its length and moves in those 8 bytes only. The schedule of every chain is f(word, num_vars) and the heights are already bound, so the word binds every schedule, including the heights (num_vars <= 4) where first6 and uniform4 give the same schedule and the same Q and only the word tells two proofs apart. agrees_with (DecodePrepared, GenesisPrepared, GlobalPrepared) now compares (log_blowup, log_folding, folds): commit_stacked blocks tree 0 at the schedule's first fold, so a first6 commitment has 64-wide leaves that a uniform4 epoch would open as 16-wide ones. One helper, committed_under, makes the comparison for all three. Tests: a_first_fold_statement_moves_only_its_fold_word (length kept, only the fold word moves, the machine draws the host's challenge under first5 and first6); the_fold_word_alone_separates_two_schedules_that_agree (mutation gate: two configs equal in every field and schedule but the policy draw different challenges at all three host sites; with fold_word() forced to log_folding it and the test above FAIL, checked by hand); a_decode_commitment_refuses_another_fold_schedule.
chain_config now builds through chain_config_under(format, shapes), which calls ChainConfig::with_security_folds with the format's fold schedule, so Q is charged the schedule's own worst round count rather than the uniform one with the format stamped on afterwards. At the default this is exactly the previous config (tested: chain_config_under(DEFAULT) == chain_config); under first5/first6 Q stays 112 at the block's tallest stack (25), with 6 rounds instead of 7. decode_prepared_config and the five continuation call sites go through chain_config and inherit the schedule. ZfFormat::global() prints a second line under the banner, on every setting: "ZF WHIR SCHEDULES: whir_folds=… q=… n=20:[…] … n=25:[…]", the schedules the base chains run at the production heights, so a log states the rounds it proved and not only the knob's name. WHIR_FOLDS_IMPLEMENTED stays false until the GPU and in-guest gates land.
…ut, schedule override RULINGS 13 / REVIEW-FRI F2: the fold-schedule DP now minimises the same cost-law objective as the cap policy, per query per committed layer: leaf blocks and walk levels priced with the cap policy's AUTO_WEIGHTS (compress, select), minus the tree's cap gain; plus the slot mux (2^d - 1 selects), the group fold (2^d - 1 binary folds at 5 XALU rows, edsl::fri_fold) and the twiddle chain (d BALU muls). XALU and BALU rows are priced from the node cost law at their committed widths (18 and 10 cells: 522 and 477 ns). FRI_COST_WEIGHTS is a format constant, pinned. The generic DP (fri_schedule_by) keeps the design model's permutation objective as a second instance, still pinned against the FRI.md 2.2 table, so the DP machinery stays checked against an independent model. U1 is re-pinned from the Rust DP (T = 9 and 10, B = 6..24, cap Off and Auto, S3 and S2 chains); at T = 9 under Auto it matches REVIEW-FRI F2's independent cost-law column at every B it lists. U2 brute-forces the new objective (4 cap policies x 3 query counts x 4 dmax, b0 <= 16). RULINGS 18: FriMode / OneRowMode now come from stark::proof::options (the local enums are gone); the cap input is a CapPolicy, and the test- local Auto cap is CapPolicy::Auto.height. FriFoldLayout::for_options builds the layout from ProofOptions (the format is a verifier-side constant) and records the encoding: legacy (pair leaves, one sibling per layer) exactly for fri=pair with row-pair openings, decided by the format, not the schedule's values. A one-row mode other than Off is an error (S2 is not built), never a silent row-pair proof. REVIEW-FRI F1.3: ProofFormat.fri_schedule_override, a test hook that replaces the DP's schedule under fri=dp so round trips can use schedules the DP never picks. No knob sets it (ZfFormat leaves it None); a schedule that does not cover the table's folds is an error; is_default() requires it None. ProofFormat is not serialized (skipped by serde and rkyv), so no pinned byte moves. No prover or verifier path uses the new layout yet; defaults unchanged.
W2's first6 schedule folds 6 variables in round 0, so tree 0's leaves are 64 base felts and the first fold runs six levels in one residency. GPU parity covered k <= 5. - whir_commit every_shape (both hashes): parity at (14, 2, 6), (12, 2, 6) and (7, 1, 6) (four leaves). Root, codeword, and openings against the host pipeline, through commit_codeword_to_host, which has no host fallback. - whir_fold: the_device_folds_six_levels_as_the_host_does, six levels on the base codeword at 2^16, 2^14 and 2^8, against fold_codeword_k_on_host. It calls math_cuda::whir::fold_codeword_base directly, because whir::fold_codeword_k falls back to the host silently (size threshold, kill switch) and a comparison through it can be the host against itself. Box only: the laptop has no CUDA (clippy with stub cubins is green).
…ifier (W1, C6)
Every WHIR commitment tree can now be opened under a Merkle cap: each
authentication path stops c levels below the root, and the tree's cap
(its 2^c nodes at that height) rides once, at the end of the tree's
first opening in proof order (the owner-path encoding, design/CAP.md
section 3). No struct changes, nothing new absorbed: the root is still the
commitment. At the default (CapPolicy::Off) every height is 0 and the
proof bytes are today's.
- ChainConfig::tree_caps: one height per tree from config.format.cap,
CapPolicy::height(openings, depth) with depth = D_t - k_t and openings Q
for tree 0, 2Q for every later tree (the last included). Shared by the
prover, the host verifier and (next commit) the LFM ChainShape.
- CodewordCommitment::open_many_capped(indices, c, owner): paths cut to
depth - c, the owner's first path carrying the cap. Host trees read
MerkleTree::cap; device codewords read the cap in the SAME with_tree
rebuild as the paths (DeviceCodeword::paths_and_cap, math-cuda + the
multilinear gpu.rs wrapper), so the cap costs no extra tree build and
retention/eviction are untouched. open_many is open_many_capped(.., 0, _).
- whir_round::prove takes RoundCaps; round 0 owns tree 0, every round owns
its successor. final_openings likewise (a one-round chain's tree 0 is
owned by the final openings).
- Verifier: TreeCheck { Owner, Checked }. A tree is authenticated ONCE,
by CappedRoot::from_owner on its owner opening; round t opens tree t
against the check round t-1 returned and never re-reads a cap (a cap on
round t's first current opening fails its exact length). The checks are
built after the opening-count guards, from .first(), so a short proof is
refused, never a panic (REVIEW-CAP M2).
- Default-path hardening, the WHIR analogue of C1b (RULINGS 3/16):
whir_commit::verify_opening now takes the tree depth and requires an
exact-length path (CappedRoot::uncapped). Honest proofs are unaffected;
only malformed proofs see a difference. New verify_opening_capped.
- New errors: CapRejected (verifier), CapEmbedFailed (prover).
Tests (laptop, multilinear --lib whir_*): capped chains round-trip at
Fixed(1..3) and Auto, Q 3 and 25, one-round, multi-round, remainder,
base and extension rounds, keccak and RPX, with every path length pinned
(depth - c, owner + 2^c); Off and Fixed(0) give identical rkyv bytes;
transcript invariance Off vs Fixed(3)/Auto (REVIEW-CAP S2); tamper arm
(tree-0 cap, tree-t cap in rounds[t-1].next[0], a second cap on round t's
current[0], owner path +-1, non-owner path +-1, cap moved to query 1, a
sibling, a proof read under another policy); M1(b) an unreached cap node
that every per-query check accepts, refused as CapRejected only by the
cap-to-root check (both trees of a round); M1(a) a keccak leaf forged
from an internal node (8 base values = 64 bytes = a parent input) that
the raw fold accepts, refused by the exact length alone; M2 an empty
capped round refused without a panic; tree_caps pinned at production
(Auto [3,3,3,3,3,3,2]).
No emitter change: ChainShape builds from config.schedule, so the closed forms, the arena layout, the query phase and the slot mux follow the schedule. What was missing is gates at k = 5 and 6. - whir_fold_tests SHAPES gain (12, 5, 7) and (13, 6, 7): blocks of 32 and 64, closed form, interned constants by value, and the fold against the host over extension and base blocks. - whir_chain_tests: KNOB_COST_SHAPES (S = 9 first6 [6,3], S = 11 first5 [5,4,2] at grind 0 and 8; S = 6 [6] and S = 7 [6,1] under first6) join the schedule gate (the emitter's hash schedule is the host transcript's) and the closed-form gate, through a cost_configs() list that keeps COST_SHAPES at the default schedule. A first-fold chain executes on a proof the host accepts; the tamper arm refuses the last value of a 64-wide base block, a round-0 sibling and the successor block, each rejected by the host too. - Knob-on production pins at S = 25, Q = 112, grind 20, derived by hand (parents, leaf blocks) and equal to design/WHIR.md's independent model: first6 19,600 opening / 19,877 chain permutations / 201,318 rows; first5 20,832 / 21,109 / 189,028. The ignored F1 at the production shape emits both programs and matches (run on the laptop: 0.08 s, 153 MB). - PREPARED_LEG_ROWS stays fixed (RULINGS 15); a knob-on test asserts it still covers the 20-variable stack: 137,321 rows under first5, 155,889 under first6, against 175,066. Default pins unchanged (22,512 / 22,828 / 185,509 and the band test).
Every tree of a univariate STARK proof (main, precomputed, aux, composition and each committed FRI layer) now honours ProofOptions.format.merkle_cap. - merkle_caps.rs (new): StarkCaps, the one place the heights are computed from public shape (policy, query count, log2(lde), committed layer count; trace trees log2(lde)-1 deep, FRI layer i log2(lde)-i-2); TreeCheck, the verifier's per-tree check (built once, then used for every query); TableTreeChecks. - Prover: a post-pass in round 4 after the openings. Per capped tree it reads the cap from the host tree and embeds it on the owner path (query 0), cutting every path to D - c. Round 4 now returns a Result. A device-resident tree (root-only host tree) is a hard DevicePath error that names the tree until the device read lands (REVIEW-CAP S6); a host tree whose depth is not the format's is refused. - Verifier: table_tree_checks builds every tree's check once, after the query-count and opening-width guards and with length-checked access only, so a malformed proof rejects and never panics (REVIEW-CAP M2). At c = 0 it reads no opening at all and is exactly the C1b exact-length check. Every opening (trace, precomputed, aux, composition, FRI layer) goes through its tree's check with its query position; query 0 of a capped tree uses the owner siblings split off once. Nothing is absorbed, so the transcript is unchanged, and at the default every height is 0: no path is cut, no cap is appended, the bytes are the same. MERKLE_CAP_IMPLEMENTED stays false until the device arm (C4) is in. Tests (tests::merkle_cap_tests, small AIRs, laptop): - round trips at Fixed(1..=4) and Auto, 3/8/30 queries, blowup 2 and 4, owned and archived (rkyv, multi_verify_archived), with the path shapes pinned (owner D-c+2^c, others D-c, the cap hashes to the root); - a preprocessed table and a RAP (aux) table capped, every cap node bound; - Off == Fixed(0) == Auto-at-3-queries, byte for byte; - REVIEW-CAP S2: Off vs Auto at grinding 0 give equal roots, OOD values, final coefficients, nonce and opened values; only paths differ, each the full path cut to D - c (+ the cap on the owner); - tampers: every cap node of main/composition/first and last FRI layer, every node of a later query's path, the owner one node short/long, the cap on a non-owner, the cap moved to query 1, and a proof made under one policy verified under another (both directions); - REVIEW-CAP M1 at the verifier level: an unreached cap node (3 queries, c = 3) that only the cap-to-root check rejects, and the real internal node above a queried leaf passed as a leaf hash, which the verifier's own TreeCheck refuses and the length-agnostic fold accepts. Deleting verify_cap or the length check from the primitive fails both (checked by hand); - S6: a root-only tree with no device read is an Err naming the tree.
…1, C7) The device side of W1 landed with the host commit (the Codeword::Device arm of open_many_capped must compile): DeviceCodeword::paths_and_cap reads the cap as the heap slice [2^c - 1, 2^(c+1) - 1) of the node buffer the paths are gathered from, inside ONE with_tree rebuild. These are its box gates; the laptop has no CUDA, so they only compile here. - math-cuda/tests/whir_cap.rs: for k = 1..5 under keccak and RPX, every cap height up to min(depth, 6): the device paths equal the host tree's full paths, the height-0 cap is the root, and the device cap equals the cap the host owner encoding appends. In three leaf-layer regimes: served from the retained layer (0 extra leaf passes), rehashed at another blocking (1), and after the allocator's evictor reclaimed the layer. Each call is exactly one tree build (tree_builds + 1): the cap costs no extra rebuild. - multilinear/tests/whir_cap_device.rs (cuda-gated): a 2^16-variable chain whose codeword stays on the card (asserted) proves the same rkyv bytes as the chain over a host-held codeword at Off, Auto and Fixed(5), both hashes, and the host verifier accepts it; tree 0's owner path length is pinned.
LAMBDA_VM_ZF_WHIR_FOLDS=first5 | first6 is now selectable: host chain, statement word, agrees_with, the production config, the GPU parity cases at k = 6 and the in-guest gates at k = 5 and 6 are in. The GPU parity tests run on the box (no CUDA on the laptop); the knob-on block proofs are the box request that follows.
REVIEW-FRI F1: nothing proved the default FRI format byte-identical. A round trip cannot (a drifted prover accepts its own proofs), and proof bytes are not reproducible under grinding (parallel nonce search). These goldens prove at grinding_factor = 0, where the bytes ARE reproducible (checked: two runs, identical), and pin, per case, the digest of the proof's rkyv bytes plus separately its FRI layer roots, terminal coefficients, FRI decommitments and trace/composition openings, so a failure names the field that drifted. Generated before any S3 prover code, on the schedule-DP commits (which change no prover path): - stark::tests::zf_golden_tests (SHA3-256): Keccak and Blake3; SimpleAddition (E = F) and LogReadOnlyRAP (E = F^3, aux); blowup 2 and 4; total_folds 0, 1, 2, 3, 4, 6; one CPU/ADD/MUL multi_prove bus proof. - prover tests::zf_rpx_golden_tests (SHA-256): the same AIRs under the production RPX pin (RpxStarkHash), which the stark crate cannot name. Shown able to fail: swapping the pair order of the FRI layer leaves in the CPU prover turns default_format_goldens_are_byte_identical red. sha3 becomes a stark dev-dependency (the version crypto already links).
…ippy) assertions_on_constants: WHIR_FOLDS_IMPLEMENTED is a const, so the check is a const block. make fmt and make lint green.
The R4 cap post-pass now reads a device-resident tree's cap instead of
refusing it: math_cuda::merkle::read_cap_dev is one D2H of the heap slice
[(2^c-1)*32, (2^{c+1}-1)*32) (the device heap has the host layout, so these
are the nodes MerkleTree::cap returns), and gpu_lde::read_cap_dev wraps it
with shape checks that fail closed with a message, never a panic. The
device arms: main and aux (gpu_main/gpu_aux trees, the table's bound
stream), composition (gpu_composition_tree) and each FRI layer (gpu_tree, a
fresh backend stream as the device FRI query phase uses). The precomputed
tree is always a full host tree. No kernel, no commit-phase change: paths
are still gathered in full and cut on the host (the merkle_gather parity is
untouched). New counter gpu_cap_read_calls.
MERKLE_CAP_IMPLEMENTED is now true (C3 + C4 are both in), so
LAMBDA_VM_ZF_CAP no longer aborts. The in-guest LFM verifier (C5) does not
verify caps yet: a recursion run that wraps a capped proof fails there, so
the knob is for STARK-level tests until C5.
Tests (box only; the laptop has no CUDA, cuda clippy is the laptop gate):
- math-cuda tests/merkle_cap.rs: keccak trees 2^1..2^8, 2^12, 2^18, 2^22
leaves, every c <= min(D, 6): the device read equals the host cap and the
heap slice, c = 0 the root; RPX trees equal the device's own heap slice;
a kept composition tree (GpuMerkleTree) serves its cap and root;
- stark tests::merkle_cap_tests::device_trees_serve_their_caps (ignored,
cuda): a 2^14-row cubic LogUp table proved at Auto/30 queries takes caps
off the device (counter moves), verifies owned and archived, and matches
an Off proof of the same witness with every path cut to D - c;
- zf_format::the_merkle_cap_knob_is_selectable.
prover/tests/merkle_cap_vm.rs proves an ELF through prove_with_options_and_inputs with the options the process format names (ZfFormat::from_env, so LAMBDA_VM_ZF_CAP), verifies it under the same options, and checks the default-format verifier refuses it (Ok(false) or Err, never a panic or an accept). Every production table is capped: preprocessed precomputed + main trees, LogUp aux trees, composition trees, FRI layers. CPU fixture all_instructions_64; under cuda fib_iterative_1M, whose tables commit on the device, and the caps must come off the resident trees (gpu_cap_read_calls moves). Knob-on only: #[ignore], and it refuses to run with the cap off. Box only (it proves a real trace).
… cost model (W1, C8)
The level-0 WHIR wrap now verifies capped chains (design/CAP.md 6.2).
Everything is derived from ChainShape.caps = ChainConfig::tree_caps, the
same heights the host prover and verifier use; at the default every
height is 0 and the emitted program, the arena and every pin are today's
(no new arena, no new word, the root path instruction for instruction).
- whir_open: CapCells, whose only constructor authenticate() hashes the
hinted cap to its root (2^c - 1 compressions) and asserts it equals the
tree's root lanes, once per tree. TreeAuth { Root, Cap }: every opening
goes through TreeAuth::verify_opening with the WHOLE index; it walks the
low bits and a private mux (2^c - 1 Selects, pairs (2t, 2t+1), low bit
first) consumes exactly the top c, then compares two variable cells. So
the cap the mux reads is the cap the root check read (REVIEW-CAP (e)),
and no caller splits the index for the mux ((d), S1 in its WHIR form).
Closed forms: verify_opening_{rows,perms}_capped, cap_check_{rows,perms}.
- whir_chain: ChainShape.caps, current_path (the sibling count; current_depth
stays the index-bit count, the two meanings the map flagged). Tree 0's
cap is authenticated at the top of emit_verify_weighted, each successor's
where its root is unpacked, and carried to the next round with it.
Arena: tree 0's 2^c words right after round 0's nonces, tree r+1's right
after round r's successor root and ood value, paths depth - c
(round_words, RoundStorage::hint, push_round_words split the owner path).
Cost model: chain_opening_perms carries depth - c per opening plus
chain_cap_perms; chain_query_rows the capped opening rows; chain_fixed_rows
the per-tree cap checks. Hints stay arena words (the chain's plumbing).
Pins that move only with the knob on (all default pins unchanged):
production chain S=25 k=4 Q=112 grind=20 at Auto, caps [3,3,3,3,3,3,2]:
opening perms 22,512 -> 18,413 (-4,144 + 45), perms 22,828 -> 18,729,
shape rows 184,673 -> 187,245, rows 185,509 -> 188,081 (hand-derived in the
test doc, then run). Emitted at the production shape (ignored, laptop-safe):
188,081 rows / 18,729 perms == the forms; 37,968 Select (+5,152 a chain).
PREPARED_LEG_ROWS stays fixed (RULINGS 4): under Auto it is within 2% of
the 24-variable chain and still covers the 20-variable stack (tested).
Tests (laptop): capped chains execute on host-accepted proofs at Fixed(1),
Fixed(2), Auto, Q 3 and 25, one and three rounds; emitted rows and perms ==
the forms at Fixed(2), Fixed(3), Auto; the host transcript schedule is
unchanged under the cap; tamper: an UNREACHED tree-0 cap node (positions
from the host's own draws: only the cap-to-root check can refuse it), a
reached one, and a successor's cap node, each rejected by the host and with
no execution; the cap mux selects every index (all 64 leaves of a depth-6
tree, c = 1..3) and refuses the right leaf claimed in another subtree; an
unreached tampered cap word cannot execute; capped opening and cap check
closed forms at every height of a depth-6 tree.
…able WHIR_CAP_IMPLEMENTED flips to true now that the cap is in the host prover and verifier (C6), on the device (C7) and in the in-guest verifier and its cost model (C8). ZfFormat no longer aborts on LAMBDA_VM_ZF_WHIR_CAP=auto or a fixed height; the default (off) is unchanged. A zf_format test pins that the knob is selectable.
…verifier (H2)
Under LAMBDA_VM_ZF_FRI=dp (ProofFormat.fri_mode = Dp) committed FRI layer
j folds by 2^{d_j}, d_j from the verifier-side schedule DP (FRI.md 1-3,
with REVIEW-FRI F5/F6 applied). The legacy format (fri = pair) runs
today's code, byte for byte: the H0 goldens are unchanged.
Prover (fri/mod.rs): commit_phase_with_layout. Per committed layer:
sample zeta, fold d_{j-1} times with zeta, zeta^2, ... (d_{-1} = 1: fold
0 is the binary fold of the DEEP pair; F6's fold-count fix), commit the
result, append the root; the final zeta folds d_last times into the
terminal. The fold is the unchanged binary fold. Group trees hash each
2^d-value group with H::Batched and build parents with H::Pair, as
today's layer trees (built with Pair, verified with Batched).
query_phase_with_layout opens the full group (the query's own value
included, FRI.md 3.4) and the path of leaf p >> d. Proof structs are
unchanged: the flat layers_evaluations_sym carries every layer's group
under a non-legacy format (its length a verifier constant).
Verifier: fri_termination_params builds the layout from the AIR's
options (never the proof); a format it cannot lay out is rejected. The
group checks live in fri::group::verify_query_groups: per layer the
group is hashed in full and authenticated at the exact depth, the slot
check group[p & (2^d - 1)] == v, and the group fold (d binary levels on
the fiber, x_g^-1 from the query point and the slot). The structural
check pins the value count per query before any loop.
The legacy/group encoding is decided by the format, not the schedule's
values (F5's per-table predicate reduces to the format until S2).
Device: every device FRI arm (DEEP-to-FRI on device, the device commit,
the device query gather) runs only for the legacy encoding; a dp table
takes the CPU FRI loop (DEEP may still run on the device, its values are
format-independent). One-row modes are refused (Err), not proved.
Round 4 now returns Result: an unsupported format is a ProvingError.
Tests (tests::fri_group_tests, prover tests::zf_rpx_golden_tests):
- U4 group_fold_equals_d_binary_folds (d = 1..6, every group and slot,
and 2^d * sum zeta^i f_i from the polynomial);
- U5 group_leaf_is_a_coset (b <= 10);
- U6 round trips at dp: every fold count 0..9 at blowup 2 and 4; explicit
schedules [1,3,3] [3,1,3] [2,1,2,2] [1]*7 [6,1] [1,6] [4,3]; ext3 with
aux; a multi-table bus proof; Keccak, Blake3 and RPX; a non-covering
override is a proving error;
- the format is a verifier constant (dp proof rejected under pair and
vice versa);
- F1.2 generic_path_at_all_ones_equals_legacy (Keccak and RPX): same
roots, terminal, openings, paths; each group is the legacy pair;
- T1-T3: every group value of a query (slot and non-slot), a path
sibling, a root, values one short / long, a short path, a missing layer;
- M1 the slot check and M2 the group authentication are load-bearing:
a p0 + c FRI forgery / a foreign root is ACCEPTED with the check
switched off (test-only thread-local mutation) and rejected with it.
Shown able to fail: folding d_j instead of d_{j-1} (F6's bug) turns 8
S3 tests red while the goldens and the all-ones differential stay green.
FRI.md 10, "Vectors the host lane exports" (a)-(d), checked in under
crypto/stark/tests/vectors/zf_fri/ with a README (conventions: field and
limbs, bit-reversed coset layers, the binary and group folds, group-leaf
hashing, query/leaf/slot arithmetic, transcript, proof encoding):
(a) a_schedules.json: the DP's schedules and cost-law costs, T in
{4, 9, 10}, Q in {3, 110}, cap off/auto, B = 6..24, S3 and S2 chains;
(b) b_group_folds.json: a SplitMix64 KAT codeword (2^7 ext3 values, the
generator documented) folded d = 1..6 times; the generator asserts
the verifier's group fold of every group reproduces the prover's;
(c) c_leaf_digests_{keccak,blake3,rpx}.json: the first group's leaf
digest and the whole group-leaf layer root, d = 1..6;
(d) d_proof_{keccak,blake3,rpx}_{pair,dp,dp_3_1_3}.{rkyv,json}: a
LogReadOnlyRAP proof (B = 12, blowup 4, k = 2, Q = 3, grinding 0) per
format, with the layout, roots, every zeta, the terminal
coefficients, and per query iota, the DEEP pair and per layer the
position, leaf, slot, opened values and path length.
The generators live in stark::fri::vectors (test / test-utils only, so
the prover crate generates the RPX files with the same code). zeta,
iota and the DEEP values come from the host verifier itself, through a
test-only thread-local capture (stark::fri::capture). The tests
zf_fri_vectors::vectors_are_current (stark) and
tests::zf_rpx_vectors::rpx_vectors_are_current (prover) regenerate every
file in memory and require it byte-equal to the checked-in copy.
prover tests::zf_vm_dp_tests::a_vm_proof_round_trips_at_fri_dp: a real
multi-table VM proof (test_mul_8, the preprocessed tables included,
RPX, CPU FRI) proved and host-verified at fri = dp, rejected by the
default-format verifier and after a group value is tampered. It builds a
full VM trace, so it is a box test (lib suite), not run on the laptop.
The ZF FORMAT banner's fri field (fri=pair|dp) already exists (C2).
LAMBDA_VM_ZF_FRI=dp is now selectable: ZfFormat no longer aborts on it. Implemented: the CPU prover (group-leaf layer commits, scheduled folds, group openings) and the host verifier, owned and archived views. On a cuda build every device FRI arm runs only for fri = pair; a dp table takes the CPU FRI loop (DEEP may still run on the device). Not implemented: device group-leaf FRI (I-FRI-D); the in-guest LFM verifier of a dp proof (I-FRI-G: lfm::fri::FriShape still derives the legacy layout, so emitting a wrap or node over a dp proof fails its committed-layer assert); the RV64 recursion guest (default-only by RULINGS 11, it refuses a non-default format). So a block run at LAMBDA_VM_ZF_FRI=dp proves and host-verifies its STARK proofs but cannot recurse over them yet. The zf_format lever test now pins that fri=dp is not reported as unimplemented.
production_sites_prove_at_the_process_format proves and host-verifies a small ext3 STARK under RPX with block_base_options() and aggregation_wrap_options(), the two univariate production format sites, and checks the encoding the process format implies. Without a knob it pins today's legacy encoding; under LAMBDA_VM_ZF_FRI=dp (the box's knob-on line) it asserts both sites stamp FriMode::Dp and the proofs carry group layers. Checked on the laptop both ways (the dp run prints "ZF FORMAT: ... fri=dp ...").
…path lengths in the STARK verifier, and the ZfFormat skeleton C1 ab7208f adds the cap primitive and the auto cap-height policy (height at most 3, chosen by the recursion cost law). C1b f82e42b makes the host STARK verifier require exact authentication-path lengths. C2 77ea1ab adds ZfFormat, the one proof-format config, parsed once from LAMBDA_VM_ZF_*; every lever is unimplemented at this commit, so any knob aborts and the default is byte-identical. Gates on FAST at 77ea1ab (default format): prover lib 1466 passed / 0 failed / 82 ignored (base 1456 + 10), stark 325 / 0, crypto 158 / 0, multilinear 310 / 0, rpx device parity 11 / 11, math-cuda 207 / 0, whir_transcript_configuration (hash-metrics) 3 / 0, byte and identity gates green.
Merges d281c3b (lane I-CAP-W, zf/cap-whir): Merkle caps on WHIR chains, host (C6), device parity tests (C7) and in-guest (C8), and WHIR_CAP_IMPLEMENTED = true. Conflicts resolved: - prover/src/zf_format.rs (tests): I-CAP-S added the_merkle_cap_knob_is_selectable and I-CAP-W added the_whir_cap_is_implemented_and_selectable at the same spot. Both tests are kept verbatim; no other hunk conflicted.
Merges ac73346 (lane I-WHIR-F, zf/whir-folds): WhirFolds::First, with_security_folds, the statement fold word, committed_under in agrees_with, the production config under the format, GPU k = 6 parity tests, in-guest k = 5/6 gates, and WHIR_FOLDS_IMPLEMENTED = true. Auto-merged without conflict: crypto/multilinear/src/whir_chain.rs (with_security delegates to with_security_folds; tree_caps derives from config.schedule(), so W1 caps follow the W2 schedule), math-cuda whir_commit.rs / whir_fold.rs tests. Conflicts resolved (tests only, no behaviour change): - prover/src/zf_format.rs: the_whir_fold_lever_is_selectable added at the same spot as the two cap-selectable tests; all three kept verbatim. - prover/src/lfm/whir_chain_tests.rs: - imports: the union (CapPolicy from I-CAP-W; ChainFormat, FirstFold, WhirFolds from I-WHIR-F). - both lanes introduced a helper named fixture_with with different signatures. I-WHIR-F's general fixture_with(&ChainConfig, num_vars) keeps the name; I-CAP-W's (num_vars, Q, grind, cap) helper is renamed fixture_capped and now builds config_with(Q, grind, cap) and calls the general one (the same config it built before). Its three call sites in the W1 section are renamed; nothing else changed. - the two appended sections (W1 cap tests, W2 first-fold tests) are both kept verbatim, W1 first.
Merges 6092c77 (lane I-FRI-H, zf/fri-host rebased on 77ea1ab): the cost-law FRI schedule DP, the fri_schedule_override test hook, S3 group FRI on the CPU prover and host verifier, goldens and vectors, and FRI_MODE_IMPLEMENTED = true. Auto-merged without conflict: crypto/stark/src/proof/options.rs (ProofFormat now carries merkle_cap, fri_mode, one_row and fri_schedule_override; MERKLE_CAP_IMPLEMENTED and FRI_MODE_IMPLEMENTED both true), prover/src/zf_format.rs (proof_format sets the override to None), crypto/stark/src/tests/mod.rs. Conflicts resolved: - crypto/stark/src/prover.rs, round 4: - the query phase: I-CAP-S made query_list mutable (the cap post-pass embeds caps into it); I-FRI-H switched it to query_phase_with_layout. Resolved as a mutable binding of query_phase_with_layout(&fri_layers, &iotas, &fri_layout). - I-CAP-S's embed_stark_caps / tree_cap helpers were one side of an add/nothing hunk; kept verbatim. - crypto/stark/src/verifier.rs (textually clean, semantically broken, fixed without changing either lane's behaviour): - table_tree_checks (I-CAP-S) read fri_termination_params(..).num_committed, which I-FRI-H changed to return Option. Now `?`: a format the verifier cannot lay out makes table_tree_checks None, which rejects the proof, the same verdict step 3 gives it. - I-CAP-S removed step 3's `lde_log` binding (its legacy path takes the per-tree checks instead); I-FRI-H's group path still passes lde_log to verify_query_groups. The binding is restored, with I-FRI-H's comment, before the terminal codeword. Not resolved here (reported to the lead, no code change): StarkCaps derives FRI layer depths from the legacy layout; the group (fri=dp) verifier path authenticates full paths and ignores FRI caps. So cap on together with fri=dp fails closed (prover depth Err or verifier rejection), a completeness gap, not a soundness one.
… it verifies at one row A parseable ZFS2NODE line per child (the process format's banner, the sub-proof count and the one-row leg count) so the box run of the leaf node under LAMBDA_VM_ZF_ONE_ROW shows that the node verified one-row LFM proofs rather than only that it executed.
S2 commits every trace tree with one bit-reversed row per leaf. The row-pair
row-major kernels read rows brev(2i), brev(2i+1) and cannot be reused at
another width (I-FRI-D note 1), so each hash gets its own one-row kernel
({keccak256,blake3,rpx}_leaves_base_row_major_row_range: row brev(i), a
column range).
- lde.rs: launch_row_major_leaves dispatches by rows_per_leaf (2 launches
exactly the kernels it did before); coset_lde_row_major_inner and the split
trees take rows_per_leaf; *_rpl public variants, the old names stay as the
row-pair wrappers. row_major_leaves is a host-matrix parity harness.
- merkle.rs / blake3.rs / rpx.rs: composition trees take rows_per_leaf; one
row uses the existing per-row ext3 kernels (same arguments).
- host KATs: the blake3 and rpx one-row kernels replayed thread by thread
against the CPU one-row leaf spec, every column range, plus a control that a
one-row leaf is not the row-pair leaf.
The default (rows_per_leaf = 2) launches the same kernels with the same
arguments.
…input tree Lifts I-S2-H's CPU-only gating for one-row tables: every device arm now follows the table's leaf layout (table_leaf_layout, per table under auto, so one proof may mix device row-pair and device one-row tables). - gpu_lde: the fused main commit, the preprocessed split, the aux commits (host input and resident) and both composition-tree entries take rows_per_leaf; LFM artifact commit via try_commit_row_major_with. Counters gpu_one_row_trees / gpu_one_row_tree_peak_bytes / gpu_one_row_fri_calls (tests assert on them so a host fallback fails). - FRI: the group drive commits layer 0 (the input tree) from the codeword with zero folds and NO challenge before it under one row (the CPU loop's pending = 0); the one_row declines in fri_commit_gpu_drive, fri/mod.rs and the DEEP->FRI arm are gone, so the tree is built off the resident DEEP codeword. - prover: device openings at row r (device_query_rows / device_rows by layout, the host cross-checks by layout); one-row tables may be device-only and keep the resident aux build. - device_set: tree_bytes_for(lde, rows_per_leaf) — a one-row tree is (2*lde-1)*32 bytes; commit/table sets and the VRAM gate estimates take the layout; FRI admission uses the one-row bound under one row. - lfm/commit.rs: REVIEW-FRI F8.1 lifted (device one-row artifact roots) with a cuda parity test against the host one-row root. Default format: rows_per_leaf = 2 everywhere, the same kernels and the same admission numbers (device_set test pins table_device_set_rpl(_, 2) == table_device_set).
…ee, (e) vectors, VM bytes - stark::s2_device_parity (cuda, test/test-utils): one-row and row-pair device trees against the host over the same evaluations — fused main, preprocessed split, aux (host input and resident), composition (host parts and resident slabs); roots, leaf counts, paths gathered off the resident trees, and the device row gathers at the query rows; the (e) leaf-digest KAT; 13 cases per hash, one S2DEV line each. - fri::device_parity: fri_parity runs one-row layouts (layer 0 = input tree, queries over the whole LDE); one_row_cases (40) and one_row_resident_cases (5), pinned by count. - tests::zf_s2_device_tests (Keccak, Blake3) and zf_rpx_device_tests (RPX): trees, FRI and resident FRI parity, and the (e) vector proofs proved on the device equal the checked-in CPU bytes (one one-row device FRI commit per proof, >= 3 one-row device trees per proof). - zf_vm_one_row_tests::one_row_vm_proof_bytes_for_the_device_comparison (ignored, box): writes the one-row VM proof bytes (grinding 0) from a CPU build and a cuda build for a byte compare; the cuda run asserts the device one-row paths fired and prints the ZF S2 DEVMEM line.
…(RULINGS 22) The fri=dp schedule DP now prices every row the in-guest verifier emits for one query's opening of a committed FRI layer, not only the slot mux, the group fold and the twiddle chain: the x_g derivation (d selects + d BALU), fold-level scaling (max(0, d-2) XALU + [d>=2] BALU), the slot assert (2 XALU), the root compare (8 BALU + 1 unpack), the group's 2^d value hints and unpacks, the leaf's ceil(3*2^d/4) Pack rows, and the path's sibling hints (depth - c: a cap now also saves c hints per query). fri_group_layer_rows and fri_pair_layer_rows are the row model; lfm::fri_group_tests pins them against the emitter kind by kind and in total, for d = 1..6 and today's pair layer, at caps 0, 1 and 2. The legacy pair-layer body moves into emit_pair_layer (the same instructions in the same order) so it can be measured. The S2 auto rule gains the in-guest DEEP term: row pairs evaluate DEEP at two points, one row at one, each num_surviving + 4E + P + 3 XALU rows (deep_point_xalu_rows, pinned against emit_deep_point); TableWidths carries it from the AIR's OOD layout. The FRI chain is priced by FriFormat::chain_cost_q, with today's pair encoding priced as pair layers when the format is legacy. Format changes (default proofs unchanged; goldens green): - U1: cap auto unchanged; cap off T=9 B=16 S2 and B=17 S3 [4,3] -> [3,2,2], T=10 B=14 S2 and B=15 S3 [4] -> [2,2]. - a_schedules.json regenerated (12 of 456 schedules move, every cost moves, weights_ns gains xalu/balu). No proof vector (d, e) moved. - auto pins: the MEMW-like and the narrow short preprocessed cases now go one row. - the device parity shape list drops [4] from the DP's own set; [4] is kept as an extra shape so the sweep still covers it (29 cases).
The box wrapper names a fresh directory per run; creating it in the test keeps the extras line self-contained.
…RI row priced, the S2 DEEP term)
… folds, FRI host S3) and the gate fixes 737415e = zf/candidate-b f985944 (merges of e6ea359 I-CAP-S wave B, d281c3b I-CAP-W, ac73346 I-WHIR-F, 6092c77 I-FRI-H) + I-FIX-B's five commits: the AIR prototype cache in prover/src/test_utils.rs now keys the whole ProofOptions (format included); the WHIR eviction test evicts before every cap height; the cuda-size tests prove the bus_permutation AirWithBuses example; merkle_cap_vm asserts the cap engaged. Gates on FAST at 737415e (default format): zf-gates GATES GREEN in 19 steps; prover lib 1494 passed / 0 failed / 86 ignored; math-cuda 214 / 0 / 10 (the lane pre-registered 197: a count error, zero failures); the 13 knob-on extras at their counts; CAPDEV 9 and CAPVM 112 device cap reads; capped tables 14 of 14 (CPU and cuda). Measured (block A/B/B/A on FAST): W2 first6 -9.30 s, W1 -0.95 s, W1+first6 -9.10 s on the WHIR block.
…LINGS 26) ZfFormat::DEFAULT, what every production site stamps when no knob is set, becomes the configuration the block runs measured net positive: cap=auto, whir_cap=auto, fri=dp, whir_folds=first6 (one_row stays 0 here; it flips in its own commit). ZfFormat::LEGACY is every lever off, and every knob keeps its off spelling (cap=off, whir_cap=off, fri=pair, one_row=0, whir_folds=uniform4), so all five at off reproduce the pre-campaign format for rollback and A/B. Security parameters (queries, grinding, blowup) do not move. The crypto crates' own defaults (stark ProofFormat::DEFAULT, multilinear ChainFormat::DEFAULT) stay the legacy format: ProofFormat gains LEGACY and is_legacy(), ProofOptions gains has_legacy_format(). ProofOptions' format is still skipped by serde and rkyv, so no serialized byte moves (RULINGS 10). The RV64 recursion guest stays on the legacy format explicitly: every Preset and MIN_PROOF_OPTIONS name ProofFormat::LEGACY, and both guest entries refuse anything but the legacy format, the production default included (the_recursion_guest_stays_on_the_legacy_format). Pins: - RPX goldens: the legacy set is kept (legacy_format_rpx_goldens_are_byte_identical, bytes unmoved) and a production-default set is added. - WHIR production chain at the default (first6 under the auto cap, S=25, Q=112, grind 20): 16,443 permutations, 203,426 rows, emitted == closed form; the legacy chain pins (22,828 / 185,509) are unchanged. - whir_epoch_program_tests::the_production_epoch_recount is a record of sh1, measured at the legacy format: its config is now named LEGACY, and the default's 6 rounds at 25 are asserted beside it. - The hash-metrics transcript pins were measured at the legacy WHIR format: their closed-form tests use the legacy config, the runtime pins skip (and say so) at any other WHIR format, and the DECODE opening's schedule assert follows the process format ([6,4,4,4,4,1] at the default; same counts). - transcript_counts drives ChainConfig::schedule instead of a uniform fold width, so its closed form prices first6 as proved.
… format It asserted that the PROCESS format is not legacy, so the legacy A/B arm (every ZF knob at off) turned it red. It now checks ZfFormat::DEFAULT for that, and refuses block_base_options() only when the process format is not legacy (always, with no knob set).
…ULINGS 26) ZfFormat::DEFAULT gains S2 one_row=auto: per table, one-row openings where the shared cost function prices them cheaper, row pairs elsewhere. It is PROVISIONAL (pre-registered net positive on STARK, neutral on WHIR) and is its own commit so it reverts cleanly if the ds30-35 / wt72-77 arms disagree. LAMBDA_VM_ZF_ONE_ROW=0 keeps selecting row pairs. No pinned byte moves: the production RPX goldens' AIRs all resolve to row pairs under auto (now asserted), one-row bytes stay pinned by the (e) vectors and the VM device comparison, the static one-row twins exist at blowup 4 (the production blowup), and the LFM registry policy is read off the options each caller passes (a one-row format builds the roots at run time), not off the process format. Banner: cap=auto whir_cap=auto fri=dp one_row=auto whir_folds=first6.
…ding the process format It built the production chain through chain_config, so the legacy A/B arm (every ZF knob off) read uniform4's seven rounds where the assert expects the default's six. It now builds ZfFormat::DEFAULT's config explicitly.
… leaf layout Under one-row openings (S2) the STARK prover absorbs a preprocessed table's root of that table's leaf layout (`precomputed_commitment_for(layout)`) before sampling the shared LogUp challenges z and alpha, and the STARK verifier does the same. `replay_transcript_phase_a_view`, which the LFM verify path and the VM/continuation commit-bus balance use to recover z and alpha, still absorbed the row-pair root (`precomputed_commitment()`) for every table. For a one-row preprocessed table the replay diverged, the expected public balance was computed at the wrong z and alpha, and `multi_verify_views` rejected an honest proof whenever that balance depended on them: every LFM proof (the published words) and every VM proof with public output. This is why the block tree's level-0 wraps failed `verify_against_artifacts` at one_row=auto (wt73, ds31) while the base epochs, which publish nothing, verified. The replay now resolves the layout exactly as the prover and verifier do (`table_leaf_layout(air, proof.trace_length())`) and absorbs that layout's root; a table with no root for its layout returns None and the caller rejects (RULINGS 14), so the replay returns Option<(z, alpha)>. Verifier-side only: no proof byte moves. At the default format every layout is row pairs and the absorbed root is byte-identical to before.
… auto, VM with public output) Two round trips that fail before the replay fix and pass after: - an LFM proof (TrivialV0) at the wrap's options (blowup 4, terminal 2^8, 128-bit queries) under one_row=auto: layouts mix within the proof and 8 preprocessed chips go one-row (asserted, so the test keeps exercising the bug); verified through verify_against_artifacts, the call the tree harness makes, and through lfm_verify; a moved public word still rejects. - a VM proof with public output (test_commit_4) at one_row=1; a moved output byte still rejects.
The CUDA composition arm evaluates `AIR::constraint_program()` once main and aux are device-resident. `LogReadOnlyRAP`, the AIR of the checked-in S3 (d) and S2 (e) proof vectors, had none, so the four device full-proof byte tests (`proved_vectors_equal_the_cpu_bytes`, `proved_one_row_vectors_equal_the_cpu_bytes` and their RPX twins) panicked in the trait default before comparing a byte. The program is captured once (OnceLock) from the same `LogReadOnlyRAPConstraints` body the CPU folders run, so the device composes the same polynomials and no vector byte can move; the CPU prover never reads the program. New CPU tests pin folder == interpreted program == lowered device program (host model of the kernel) on random frames. The four device tests now also assert that every proof composed on the device (`gpu_composition_calls` moves once per proof), next to their existing FRI and one-row tree counters, so a host composition fallback fails them.
…ed twice per process
`one_row_vm_proof_bytes_for_the_device_comparison` compared a CPU-build and a
cuda-build RV64 VM proof of `test_mul_8`, on the premise that at grinding 0
the proof is a function of the ELF and the format. It is not: six base-table
builders dedup through a std HashMap (RandomState) and lay rows out in
iteration order, so the main roots and the whole transcript change per
process; the lead's control showed the same build differing from itself in
~80% of the bytes. The test is deleted (pinning the VM row order would move
every proof and is not this lane's call).
The replacement, `zf_lfm_bytes_tests::lfm_proof_bytes_for_the_device_comparison`
(ignored, box), proves the `TrivialV0` LFM machine program (public output,
so the balance depends on z, alpha) at blowup 4, 128-bit queries, grinding 0,
under `legacy`, `one_row_1` and `production` (cap auto, fri dp, one_row auto),
proves each TWICE in the same process and asserts the two byte strings equal,
writes `$ZF_S2_PROOF_DIR/{cpu,cuda}_<fmt>.rkyv`, then verifies. Under cuda the
`one_row_1` arm must build one-row trees and take the one-row FRI commit on
the device; the legacy arm must do neither.
…ry arm Under cuda each format must commit FRI on the device for its two large chips (2^16 and 2^20 rows, above the default device floor), so a host proof cannot pass as a device proof in the cross-build cmp; the counter is printed on the `ZF LFM DEVICE` line. Also make fmt.
… the layout root) Lane I-FIX-S2, second parent 91764db: 6a4a244 replay_transcript_phase_a_view absorbs precomputed_commitment_for(table_leaf_layout) and returns Option (a missing root rejects, RULINGS 14); 91764db adds two one-row regression tests (LFM at the wrap options under auto, VM with public output). Conflicts: none.
…OnlyRAP program, LFM bytes oracle) Lane I-FIX-D2, second parent 39dea55: LogReadOnlyRAP gets a constraint program captured from its CPU constraint body (+ tests), the four device byte tests assert one device composition per proof, the LFM bytes oracle lands in prover/src/tests/zf_lfm_bytes_tests.rs, and the invalid VM-bytes test one_row_vm_proof_bytes_for_the_device_comparison is deleted. Conflict: prover/src/tests/zf_vm_one_row_tests.rs (one file). Resolution: kept I-FIX-S2's two regression tests (an_lfm_proof_at_the_wrap_options_round_trips_ at_one_row_auto, a_vm_proof_with_public_output_round_trips_at_one_row) and its module-doc bullet; kept I-FIX-D2's deletion of the VM-bytes test and its doc comment; dropped the module-doc bullet that described the deleted test.
…nally (RULINGS 26)" This reverts commit 0dd6341 (I-FLIP commit B). The DROP-B variant of candidate-f, prepared for the lead's decision on the provisional one_row=auto default (RULINGS 26): the default format keeps commit A (cap=auto whir_cap=auto fri=dp whir_folds=first6) with one_row=0. LAMBDA_VM_ZF_ONE_ROW=auto still selects S2. Commits cfbff6a and 5ed2f15 belong with A and stay.
…levers as separate arms The `production` arm proved cap auto + fri dp + one_row auto, which is no longer the prover's default format (one_row stays off by default). The oracle now has four arms: - legacy: every lever off (bytes unchanged); - one_row_1: legacy + one row on every chip (bytes unchanged); - production: the STARK part of ZfFormat::DEFAULT (cap auto, fri dp, one_row off), asserted equal to what the default stamps so the arm cannot drift; - all_levers: cap auto + fri dp + one_row auto, the former `production` arm, with the same bytes. Every existing assertion is kept: twice-equal bytes per process, verify, and the cuda counters (one-row device work only where one_row is on).
Comments only. Every comment line added since the proof-format work began now states its reason in place instead of pointing to material outside the repository (design notes, review findings, rulings, run tags, work-lane names). Soundness reasons are written out where they apply: a one-row layout with no preprocessed root is a hard miss, never a recompute; exact path lengths keep a leaf hash from being compared with an internal node; the RV64 recursion guest verifies the legacy format only. The ZfFormat::DEFAULT doc now says why one_row stays off: in ABBA block runs it costs +3.2 s on the WHIR pipeline and saves 8.0 s and 8 GiB of host memory on the STARK pipeline, so it is a knob (LAMBDA_VM_ZF_ONE_ROW=auto) recommended for the STARK pipeline. Unchanged because they are code, not comments: the test name the_production_shape_reproduces_the_campaigns_permutation_count (and its two doc links) and one assertion message in whir_chain_tests.rs.
Merkle caps on every STARK and WHIR tree, FRI folds by 2^d with a verifier-side DP schedule, and a six-variable first WHIR fold are the new default format (cap=auto whir_cap=auto fri=dp one_row=0 whir_folds=first6). One-row openings with a committed FRI input are built and selectable (LAMBDA_VM_ZF_ONE_ROW=auto); they stay off by default. Also: the Phase-A replay absorbs each preprocessed root at its leaf layout, and the device byte-parity tests run on a card.
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.
Proof-format levers taken from ZisK's recursion (pil2-proofman), implemented on both RPX pipelines of this branch. With the new defaults, block 25368371 proves 16.1 % faster on the WHIR pipeline and 18.7 % faster on the STARK pipeline. The recursion verifiers run 37–39 % fewer hash permutations. Security parameters (queries, grinding bits, blowup) are unchanged.
Results
Block 25368371, FAST box (Ryzen 9 9950X, RTX 5090). Each delta is an ABBA on one binary: two arms per setting, alternated.
The default was checked end to end: a run with no knob reproduces the knob-set runs' permutation census and program ids exactly. Explicit legacy knobs reproduce the base exactly.
Each lever alone, and combined (Δ wall against legacy, ABBA):
LAMBDA_VM_ZF_CAP=autoLAMBDA_VM_ZF_FRI=dpLAMBDA_VM_ZF_WHIR_CAP=autoLAMBDA_VM_ZF_WHIR_FOLDS=first6LAMBDA_VM_ZF_ONE_ROW=autoS2 is built, tested, and correct on both pipelines, but it is not in the default. On the WHIR pipeline it costs 3.2 s: the prover pays for one-row LFM proofs, and the in-guest saving is small because the wraps verify WHIR proofs. On the STARK pipeline it saves 8.0 s and 7–8 GiB of host memory.
LAMBDA_VM_ZF_ONE_ROW=autois the recommended setting there.Every permutation census matched its pre-registered model, most of them exactly.
What changed
prover/src/zf_format.rsparses the fiveLAMBDA_VM_ZF_*knobs once and prints oneZF FORMAT: …banner. It hands the format to the crypto crates through their option types:ProofOptions.formatandChainConfig.format. Those fields are skipped by serde and rkyv, so serialized options are unchanged. Every knob keeps its off value:cap=off,fri=pair,one_row=0,whir_cap=off,whir_folds=uniform4.ZfFormat::LEGACYnames the old format, and a golden test still pins it byte for byte.crypto/crypto/src/merkle_tree/cap.rs). Paths stop at a verifier-chosen height c ≤ 3 (theautopolicy, priced by the LFM cost law). The cap rides at the end of each tree's first authentication path, so the proof structs are unchanged. Host verifiers, GPU openings and the in-guest verifiers are all updated. The in-guest cap is hinted once and checked against the root; the cap node is picked by a mux on the transcript's index bits.crypto/stark/src/fri/). There is one challenge ζ per committed layer, applied as d binary folds with ζ, ζ², ζ⁴, …. This is the standard arity-2^d fold, so the existing binary fold kernels are reused. The schedule is a DP over public shape data that minimises the in-guest cost of every emitted row. The GPU gains group-leaf layer commits and a multi-fold commit; the in-guest verifier gains group folds.crypto/stark/src/leaf_layout.rs). One LDE row per leaf, plus a committed DEEP input tree whose root is absorbed before the first fold challenge. The verifier opens one row per query and checks the DEEP value at that point against the input tree's slot. Preprocessed tables get one-row static roots at blowup 4; a missing root is a proving error.autopicks the layout per table from the AIR widths. Host, GPU and in-guest paths are all implemented.crypto/multilinear/src/whir_*). The schedule at 25 variables becomes [6,4,4,4,4,3] instead of [4,4,4,4,4,4,1]. That is one round fewer, so 3 fewer grinds per chain and a smaller tree 0.Soundness
log2 Rmargin shrinks.Fixed along the way
prover/src/lib.rs). The Phase-A transcript replay absorbed the row-pair root of one-row preprocessed tables. The prover and verifier absorb the root of the table's own layout. So honest one-row LFM proofs, and one-row VM proofs with public output, were rejected. Now fixed, with regression tests.prover/src/test_utils.rs) keyed AIR prototypes without the proof format, so tests of different formats in one process shared verifier constants. It is now keyed by the whole options. It also exposed a hazard: the verifier reads its format fromair.options(), not from the options passed toverify.Gate
FAST box, at
d8ffc0702, whose tree is this PR's head:tests::multilinear_continuation_testsunder legacy knobs at full test parallelism. It was killed for memory at the box's 57.5 GiB limit. The same line on the same commit with the lib suite's--test-threads=3passes 23 / 0 / 1.CI: every job passes except prover shard 4/4. Its hosted runner receives a shutdown signal and SIGKILLs
tests::constraint_artifact_tests::epoch_chunk_multiplierat test 280 of 533. That happened twice here, and it is the same failure as shard 4/4 on #1004. The other 279 tests in the shard pass, andepoch_chunk_multiplierpasses in the box lib suite.Decisions for you
whir/recursion-rpx.autorule that also prices the prover's one-row cost; today's rule prices only the in-guest verifier.