feat(stark): prune redundant g·z (next-row) trace-OOD openings#827
Merged
diegokingston merged 3 commits intoJul 15, 2026
Merged
Conversation
…roof The verifier read the trace-OOD table's shape from the (prover-controlled) proof dimensions (`num_main = trace_ood_evaluations.width - num_aux`), only indirectly cross-checked. Reject any proof whose OOD table is not exactly the AIR-derived size — height = transition_offsets.len() * step_size, width = main + aux — before any use of the table, and take the main width from the AIR rather than the proof. A malicious prover can no longer reshape the table (e.g. drop a column) to dodge a constraint check or trigger an out-of-bounds read in the frame reconstruction. This is the shape-from-metadata invariant (I3) that the upcoming g·z OOD pruning relies on: once the next-row block is pruned to just the accumulator column, the verifier must reconstruct the reduced shape purely from public AIR metadata, identically to the prover. Test: `test_malformed_ood_table_shape_rejected` (drop a column from an otherwise-valid ADD proof's OOD table → rejected). Full stark suite green (192).
Adds an AIR-metadata method (default empty) naming the full-width `[main|aux]` column indices that transition constraints read at the NEXT row (offset 1) — lambda_vm's fine-grained analogue of Plonky3's transition window (a whole-row "uses next row?" flag). `AirWithBuses` overrides it to return exactly the accumulator column, the sole next-row read after forward accumulation. This is the public, prover=verifier-identical source of truth for which OOD openings survive at g·z. The upcoming pruning consumes it on both sides so the reduced OOD shape is derived from AIR metadata, never from the proof. Test: `test_trace_ood_next_row_columns_is_accumulator_only`. stark suite green (193).
Only the columns a transition constraint reads at the next row (the AIR transition window, `trace_ood_next_row_columns`) need an OOD opening at g·z. After forward accumulation that is just the LogUp accumulator, so the next-row half of the trace-OOD collapses from the full width W to one column per bus table — a smaller proof and, more importantly, ~halved DEEP trace-term work in the verifier / recursion guest (the cycle win). Design (CUDA-safe — the GPU DEEP kernel is untouched): - New `crate::ood` module of pure, prover=verifier-identical helpers deriving the surviving-opening layout from public AIR metadata (invariant I3). - Fiat-Shamir: both sides sample `num_surviving_trace_openings` DEEP gamma powers (was `2·step_size·W`). The gamma is one field element either way, so transcript consumption is unchanged; only the trace/composition split moves. - Prover keeps its rectangular W×(2·step_size) DEEP (CPU and GPU) by scattering the sampled powers into the full grid with ZEROS at pruned positions — zero terms vanish, so the DEEP polynomial is identical with no kernel change. The proof carries only the two surviving blocks (`trace_ood_evaluations` = current-row S×W, new `trace_ood_next_evaluations` = next-row S×|window|), and the transcript absorbs only those. - Verifier reconstructs the full grid from the two blocks and SKIPS pruned next-row terms in the DEEP loop (the cycle saving), after validating both block shapes against AIR metadata (extends the I3 guard). Default `trace_ood_next_row_columns` is conservative (every column — no pruning), so any AIR that reads the next row stays correct without overriding; `AirWithBuses` overrides to the accumulator column. Proof is bincode/serde, so the wire change is transparent; the recursion guest recompiles the same source. Tests: full stark suite green (198) incl. multi_prove_ram roundtrips (pruned proofs verify), soundness negatives (tampered/mis-shaped OOD rejected), a `test_gz_pruning_reduces_next_row_openings` win check (next-row block = 1 col vs full width, still verifies), and `ood` unit tests. Inline VM-table prove+ verify (bitwise/lt/branch/bus) green. GPU DEEP path unchanged (no cuda build here; kernel needs no change by construction).
diegokingston
merged commit 6939c35
into
feat/logup-acc-current-row
7 of 8 checks passed
MauroToscano
added a commit
that referenced
this pull request
Jul 16, 2026
Bring the batched (unified-shard) prove/verify path to full optimization parity with main's non-batched g·z OOD trace-opening pruning (#823/#827), so recursive-verifier benchmarks compare like-for-like. Fiat-Shamir changes for batched proofs — both sides change together; the format is unreleased draft-PR-only. Format (`BatchedTableData`): - `trace_ood_evaluations` now carries only the current-row block (step_size rows, all columns); new `trace_ood_next_evaluations` carries the pruned next-row block (transition-window columns only, empty when the AIR reads none). Mirrors `StarkProof`'s post-#823 split. Prover: - `prove_rounds_1_to_3`: split the full OOD via `OodLayout::split_full` and absorb the two blocks (current then pruned-next) — same order/semantics as the non-batched round-3 absorption. - `batched_table_deep_codeword`: draw only `layout.num_surviving()` trace-term powers and scatter them with `build_trace_term_coeffs` (rectangular grid, zeros at pruned positions) — identical DEEP codeword to non-batched round 4. - `batched_round_4`: store the split blocks in `BatchedTableData`. Verifier: - `batched_verify_rounds_1_to_3`: absorb the two split blocks; add the I3 OOD-shape guard (mirrors `ood_blocks_well_formed`) in Phase A, before Round 3 absorbs the next-row block. The current-block width is checked against `context().trace_columns` (the physical OOD width) rather than `trace_layout().0 + num_aux`, since the batched lane includes step-packed AIRs (BitFlags) whose `trace_layout().0` is a logical, not physical, count. - `batched_verify_round_4`: build one `OodLayout` per table (shared across the coeff replay, reconstruction, step 2, the #826 query-invariant hoist, and the per-query DEEP); draw pruned trace-term coeffs; reconstruct the full OOD grid once via `reconstruct_full`; drive the DEEP pair with the AIR-derived `next_row_cols` (real g·z pruning, replacing the previous all-columns hoist). - `batched_synthetic_table_proof`: carry both split blocks. Both epoch lanes are consistent: the VM lane prunes (this change); the L2G lane already prunes via `prove_rounds_2_to_4` / `verify_rounds_2_to_4`. `batched_verify_epoch` and `EpochProof` make no full-grid assumptions. Tests: three batched soundness negatives for the split format — a current-row trace-OOD tamper (transcript/step-2 desync) and the two I3 shape guards (malformed current-row and next-row blocks). Full `stark` suite 225 passing.
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.
Step 2 of OOD g·z pruning. Stacked on #823 (forward accumulation) — review/merge that first; this PR's base is
feat/logup-acc-current-row, so the diff shows only the pruning.What
A transition constraint only reads a handful of columns at the next row (
z·g). After step 1 made the LogUp accumulator the sole next-row reader, the entire next-row half of the trace-OOD block — every column except the accumulator — is redundant. This PR stops sending and stops opening it.Concretely the next-row OOD block shrinks from the full trace width
Wto|transition window|columns (one per bus table, the accumulator). Proof shrinks; more importantly the verifier / recursion guest does ~half the DEEP trace-term work (2·W·S → (W + |window|)·S), which is the cycle win the benchmark measures.How (CUDA-safe by construction)
crate::oodmodule — pure, prover=verifier-identical helpers that derive the surviving-opening layout purely from public AIR metadata (step_size, column count,trace_ood_next_row_columns()), never from proof dimensions.AIR::trace_ood_next_row_columns()(Plonky3's "transition window", per-column). Default is conservative (all columns → no pruning) so any AIR reading the next row stays correct without opting in;AirWithBusesoverrides to[accumulator].W×2SDEEP (CPU and GPU) by scattering the sampled γ-powers into the full grid with zeros at pruned positions — zero terms vanish, so the DEEP polynomial is identical and the GPU kernel needs no change. The proof carries only the two surviving blocks and the transcript absorbs only those.New proof field
trace_ood_next_evaluations(next-row block);trace_ood_evaluationsis now just the current-row block. Wire format is bincode/serde so the change is transparent; the recursion guest recompiles the same verifier source.Tests
starklib suite green (198), incl. multi_prove_ram roundtrips (pruned proofs verify) and soundness negatives (tampered / mis-shaped OOD rejected).test_gz_pruning_reduces_next_row_openings— next-row block is 1 column vs full width, and still verifies.oodmodule unit tests (split/reconstruct/scatter-zeros/surviving-count).