Skip to content

refactor(logup): forward accumulation so acc is the sole next-row OOD read#823

Merged
MauroToscano merged 10 commits into
mainfrom
feat/logup-acc-current-row
Jul 16, 2026
Merged

refactor(logup): forward accumulation so acc is the sole next-row OOD read#823
MauroToscano merged 10 commits into
mainfrom
feat/logup-acc-current-row

Conversation

@diegokingston

Copy link
Copy Markdown
Collaborator

What

Switches the circular LogUp accumulator from backward (next-row) to forward (current-row) accumulation:

  • Before: acc[i+1] − acc[i] = terms[i+1] − L/N, acc[N-1] = 0. The committed term columns and every absorbed interaction's main-trace operands (multiplicity + bus values) were read at the next frame row (offset 1).
  • After: acc[i+1] − acc[i] = terms[i] − L/N, acc[0] = 0. Only acc_next reads offset 1; all terms and absorbed operands read the current row (offset 0).

Result: acc is now the only column any constraint reads at the next row across the entire system. This is the enabler for pruning the g·z trace-OOD block down to a single column in a follow-up PR (large proof-size / verifier-work win on wide tables like CPU-74, MEMW-49).

How

Three CPU sites in lookup.rs:

  1. emit_logup_accumulated — committed-term sum and absorbed emit_multiplicity/emit_fingerprint flip offset 10; acc_next stays at 1. This is the sole accumulator path (monomorphized into ProverEvalFolder/VerifierEvalFolder, mirrored by the constraint_ir interpreter), so one edit covers prover and verifier identically.
  2. build_accumulated_column_from_terms — write acc[row] before folding the current row's terms (acc[0]=0).
  3. Boundary pin moved acc[N-1]=0acc[0]=0 (removes the same constant-shift DOF, now at the start of the forward sum).

Soundness

Unchanged. The circular transition telescopes to force Σterms = N·(L/N) = L regardless of the accumulator's constant offset; the boundary pin only canonicalizes that free constant. table_contribution (L) and the cross-table bus-balance check are untouched. Corrupting the acc OOD evaluation is still rejected (existing soundness test).

GPU

The on-device accumulate (logup.cu logup_finalize_accum_ext3) switches from an inclusive to an exclusive prefix scan: acc[i] = scan[i-1] − i·offset, acc[0]=0. The parity reference in logup_gpu.rs mirrors it. ⚠️ The CUDA path needs GPU-server validation — it isn't buildable in this environment (local clang lacks the riscv build-attributes flag). CPU and GPU must stay in lockstep here since the accumulator column definition is shared.

Testing

  • Full stark suite: 190 passed, including LogUp completeness (real multi-table proofs verify — which structurally require acc[0]=0 via the boundary), soundness negatives, and the prover/verifier/IR three-way folder-equivalence regression on both the 1- and 2-absorbed branches.
  • New focused test accumulated_column_is_forward_and_circular asserts the build contract directly (acc[0]=0 + the current-row circular recurrence on every row incl. wraparound).
  • Inline prover prove+verify modules green: bitwise (19), bitwise_bus (11), bus_tests group (61). The only failures in this environment are missing prebuilt ELF artifacts (test_utils.rs:236 "Failed to read ELF"), unrelated to this change — the full ELF-based _fast/comprehensive suite runs in CI.

… read

The circular LogUp accumulator previously summed each row's terms at the
NEXT frame row: `acc[i+1] − acc[i] = terms[i+1] − L/N`. That made the
committed term columns AND the absorbed interactions' main-trace columns
(multiplicity + bus values) all next-row (offset-1) reads, so the OOD
opening had to send the full trace width at g·z.

Switch to forward accumulation — `acc[i+1] − acc[i] = terms[i] − L/N`,
`acc[0] = 0` — by reading the committed-term sum and the absorbed
multiplicity/fingerprint operands at the CURRENT row (offset 0) in
`emit_logup_accumulated`, and writing `acc[row]` before folding in the
current row's terms in `build_accumulated_column_from_terms`. `acc_next`
stays the one offset-1 operand. Since `emit_logup_accumulated` is now the
sole accumulator path (monomorphized into ProverEvalFolder /
VerifierEvalFolder and mirrored by the constraint_ir interpreter), the
single edit covers prover and verifier identically.

`acc` is thus the ONLY column any constraint reads at the next row across
the whole system — the enabler for pruning the g·z trace-OOD block down to
one column in a follow-up.

Soundness: unchanged. The circular transition telescopes to force
`Σterms = N·(L/N) = L` regardless of the accumulator's constant offset;
the boundary pin (moved from `acc[N-1]=0` to `acc[0]=0`) only removes that
constant-shift DOF. `table_contribution` L and the cross-table bus-balance
check are untouched. Corrupting the acc OOD is still rejected.

GPU: the on-device accumulate (`logup.cu` `logup_finalize_accum_ext3`)
switches from an inclusive to an exclusive prefix scan (`acc[i] =
scan[i-1] − i·offset`, `acc[0]=0`); the parity reference in `logup_gpu.rs`
mirrors it. The CUDA path needs GPU-server validation (not buildable in
CI without the toolchain).

Tests: full `stark` suite (190) green, including LogUp completeness (real
proofs verify — which structurally require `acc[0]=0`), soundness
negatives, and the prover/verifier/IR three-way folder-equivalence
regression on the 1- and 2-absorbed branches. Added a focused
forward-accumulation contract test on the build function. Inline prover
prove+verify modules (bitwise/lt/branch/l2g/bitwise-bus) all green; the
only failures in this env are missing prebuilt ELF artifacts.
* harden(verifier): derive OOD table shape from AIR metadata, not the proof

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).

* feat(air): trace_ood_next_row_columns — the per-column transition window

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).

* feat(stark): prune redundant g·z (next-row) trace-OOD openings

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

Copy link
Copy Markdown
Collaborator Author

/bench-verify

@github-actions

Copy link
Copy Markdown

Benchmark started on the bench server. The verifier bench takes ~5 min; the recursion-guest cycle comparison then adds guest builds — a few minutes when cached, up to ~1h on a cold run. The bench server is occupied until it finishes.

@github-actions

github-actions Bot commented Jul 15, 2026

Copy link
Copy Markdown

Verifier benchmark — 43351e1adf vs main (20 pairs)

=== Verify ABBA result ===

Metric main PR Δ
Verify time (per-side) 3.626s 3.594s -0.88% 🟢
Proof size 204.46 MiB 204.30 MiB -0.08% 🟢

Per-side (PR can't deserialize the baseline's proof — proof-format change): A/B/B/A cancels machine drift but not proof-specific variance — read the Verify-time Δ as approximate.

  pairs: 20   mean A (PR): 3.594s   mean B (main): 3.626s
  [parametric] paired-t   mean -0.88%   sd 0.78%   se 0.17%
               95% CI: [-1.24%, -0.51%]   (t df=19 = 2.093)
  [robust]     median -0.84%   Wilcoxon W+=13 W-=197  p(exact)=0.0002  (z=-3.42)

  run-to-run jitter:    A CV 0.50%   B CV 0.62%        (lower = steadier)
  within-session drift: +0.48% over the run, 1st->2nd half +0.36%

🟢 REAL IMPROVEMENT — PR verifies ~0.88% faster (paired-t and Wilcoxon agree).

Drift-free interleaved A/B/B/A measurement. - = PR faster. Trust the verdict when paired-t and Wilcoxon agree.


Recursion guest cycles (main vs PR)

=== Recursion-guest cycle comparison — single query (blowup=2, 1 query) — deterministic to ~±100k cycles ===
REF_B (baseline) origin/main 18f3b8f guest=recursion-min.elf
REF_A (PR) 43351e1 43351e1 guest=recursion-min.elf

Metric REF_B (baseline) REF_A (PR) Δ (A-B)
Guest cycles 47.6M 43.9M -3.7M (-7.72%)
Keccak calls 3885 3025 -860

note: cycles reproduce to ~±100k (build codegen + proof nondeterminism); treat sub-100k deltas as noise, not signal.

raw (exact integer counts)
ref_b_sha=18f3b8f27e3d3fa3b13d22fd16596b03a3abc881 ref_b_elf=recursion-min.elf ref_b_cycles=47567091 ref_b_keccak=3885 ref_b_execute_wall_s=1
ref_a_sha=43351e1adf2737fd8d8ee6d836f3cc1030e34ae0 ref_a_elf=recursion-min.elf ref_a_cycles=43893476 ref_a_keccak=3025 ref_a_execute_wall_s=1
delta_cycles=-3673615 delta_keccak=-860

Resolve the g·z-pruning conflicts against the rkyv in-place verifier (#769)
and the OOD-shape guard (#815) that landed on main.

The verifier no longer reads proof fields directly — it goes through
`StarkProofView` (Owned | Archived) so the recursion guest can verify
zero-copy from the rkyv archive. Ported the pruning onto that model:

- proof/view.rs: new `trace_ood_next_evaluations()` accessor returning a
  `StarkTableView` (parallel to `trace_ood_evaluations()`), plus the field in
  the compile-enforced exhaustiveness guard.
- ood.rs: `reconstruct_ood_full` now takes row-major slices (a `Table`'s or a
  view's `row_major_data()`) instead of `&Table`, and is bounds-safe (`.get`)
  so a malformed archive yields a zero-filled grid rather than a panic.
- verifier.rs: step_2 validates both pruned blocks (incl. `dimensions_consistent`)
  and builds the frame from `StarkTableView::Owned(&ood_full)`; step_3 rebuilds
  the grid from the two view blocks; the DEEP loop reads the reconstructed grid
  and keeps the pruned-term skip; the Fiat-Shamir absorb walks both blocks
  column-major through the view; kept main's `checked_sub` main-width derivation
  (the current-row block still carries full width under pruning).

New `trace_ood_next_evaluations` is the same `Table<E>` as the existing OOD
field, so rkyv needs no new machinery. The pruning test now also verifies the
pruned proof through the archived read-in-place path (the recursion guest's
path), exercising `StarkTableView::Archived` over the pruned next-row block.

stark lib suite green (198, incl. archived roundtrip); prover checks clean;
clippy clean; disk-spill config compiles.
@diegokingston

Copy link
Copy Markdown
Collaborator Author

/bench-verify

@github-actions

Copy link
Copy Markdown

Benchmark started on the bench server. The verifier bench takes ~5 min; the recursion-guest cycle comparison then adds guest builds — a few minutes when cached, up to ~1h on a cold run. The bench server is occupied until it finishes.

@diegokingston diegokingston marked this pull request as ready for review July 16, 2026 14:30
@diegokingston

Copy link
Copy Markdown
Collaborator Author

/bench-verify

@github-actions

Copy link
Copy Markdown

Benchmark started on the bench server. The verifier bench takes ~5 min; the recursion-guest cycle comparison then adds guest builds — a few minutes when cached, up to ~1h on a cold run. The bench server is occupied until it finishes.

MauroToscano added a commit that referenced this pull request Jul 16, 2026
Pre-existing -D warnings clippy errors in test code added on the #823
branch; CI's `make lint` (cargo clippy --workspace --all-targets) flags
them but a crate-scoped lib-only clippy did not.

- lookup.rs accumulated_column_is_forward_and_circular: iterate
  `&term_columns` instead of `0..n_term_cols` (needless_range_loop, two
  sites) and deref the two `get_aux(..).clone()` reads (clone_on_copy;
  FieldElement<Degree3GoldilocksExtensionField> is Copy).
- logup_gpu.rs reference_accumulate: `out.push(acc.clone())` ->
  `out.push(acc)` (clone_on_copy). Only surfaces under the cuda-feature
  clippy pass, which the earlier passes stop short of.
…hard assert) (#833)

* fix(stark): review nits for forward-accumulation OOD pruning

- lookup.rs: fix the logup_single_source_tests module doc — after
  forward accumulation the 2-absorbed branch no longer reads next-row
  aux(1, ·) cells; describe it by what it actually does (folds two
  absorbed interactions, degree 3).
- ood.rs: reword the module doc so the offset illustration is not pinned
  to [0, 1] — offset 0 is the current-row block, every later offset
  contributes a next-row block (generic over transition_offsets.len()).
- verifier.rs: use num_eval_points.saturating_sub(step_size) to match
  the shared ood.rs helper (defensive consistency; underflow unreachable).
- ood.rs: harden build_pruned_trace_term_coeffs — drop the per-slot
  `if p < powers.len()` guards and promote the trailing power-count check
  from debug_assert_eq! to a hard assert_eq!. Both operands are pure
  functions of AIR metadata (invariant I3), never proof-controlled, so a
  mismatch is a programmer bug that must not be masked in release builds.

* fix(stark): clippy lints in forward-accumulation tests

Pre-existing -D warnings clippy errors in test code added on the #823
branch; CI's `make lint` (cargo clippy --workspace --all-targets) flags
them but a crate-scoped lib-only clippy did not.

- lookup.rs accumulated_column_is_forward_and_circular: iterate
  `&term_columns` instead of `0..n_term_cols` (needless_range_loop, two
  sites) and deref the two `get_aux(..).clone()` reads (clone_on_copy;
  FieldElement<Degree3GoldilocksExtensionField> is Copy).
- logup_gpu.rs reference_accumulate: `out.push(acc.clone())` ->
  `out.push(acc)` (clone_on_copy). Only surfaces under the cuda-feature
  clippy pass, which the earlier passes stop short of.

* fix(stark): keep debug-only power-count check in build_pruned_trace_term_coeffs

build_pruned_trace_term_coeffs is a shared helper the verifier calls, and
the verifier must never contain a panic path: an invalid proof is just a
false proof, not a crash. Revert the hardening — restore the per-slot
`if p < powers.len()` guards and the `debug_assert_eq!` power-count check.

The doc comment still states the strict precondition (powers.len() ==
num_surviving_trace_openings for the same layout args); that is pure
documentation and stays.
MauroToscano added a commit that referenced this pull request Jul 16, 2026
…h verify

PR #823 added g·z OOD trace-opening pruning. The layout metadata and the
full-grid reconstruction were then derived redundantly at several sites that
had to be kept in lockstep by hand:

  - `num_eval_points`/`next_row_cols` + `num_surviving_trace_openings` +
    `build_pruned_trace_term_coeffs` recomputed in verifier `step_2`, `step_3`,
    the round-4 transcript replay, and prover round-4.
  - `reconstruct_ood_full` built TWICE per verify — once in `step_2` (behind the
    block-shape guard) and again, unguarded, in `step_3`, which silently relied
    on `step_2` having validated the shapes first.
  - `split_ood_blocks` args recomputed in prover round-3.

Introduce `ood::OodLayout`, a small struct bundling the AIR-derived layout
(`num_total_cols`, `num_eval_points`, `step_size`, `next_row_cols`) with methods
that forward to the existing free functions (`num_surviving`, `flags`,
`build_trace_term_coeffs`, `split_full`, `reconstruct_full`, plus the guard's
`expected_next_{width,height}`). The free functions and their pub API are
unchanged; the struct only wraps them and adds no new arithmetic. It stays
decoupled from the AIR trait — a one-line `ood_layout` helper per crate reads
the four raw values and hands them to `OodLayout::new`.

The verifier now builds the layout, the block-shape guard, the single grid
reconstruction, and the next-row flags ONCE per proof in `verify_rounds_2_to_4`
and passes borrows into `step_2` and `step_3`. The guard runs before both steps
(same checks, same `return false` semantics, same order relative to grinding and
the steps), removing the hidden step_2-before-step_3 ordering dependency and
doing one reconstruction instead of two (a small guest-cycle saving). The
transcript-replay and prover metadata sites now derive from the same struct.

Zero behavior change: Fiat-Shamir absorption/sampling order is untouched; the
metadata sites keep using `trace_columns`; `next_row_flags` stays keyed on the
reconstructed grid's width (the current-row block width) exactly as `step_3`
did, so a malformed-width proof is handled identically. The verifier gains no
new panics/asserts/unwraps and every `return false` path is preserved. Validated
with the full `cargo test --release -p stark` suite (194 passed, incl. a new
`OodLayout`-delegates-to-free-functions test) and `make lint` (fmt + all four
clippy passes incl. cuda) at exit 0.
…sorption (#835)

* fix(verifier): validate next-row OOD block shape before transcript absorption

The next-row (g·z) OOD block (`trace_ood_next_evaluations`, new with OOD
pruning) is absorbed into the transcript in Round 3 via `get_row` -- an
unchecked `data[start..start + width]` slice -- BEFORE step_2's shape guard
runs. rkyv bytecheck does not enforce `width * height == data.len()`, so a
hostile archive advertising e.g. width=1000/height=1000 with a single data
element panics the verifier out of bounds (guest trap / host crash) instead
of being rejected as a false proof.

Extend the Round-1 Phase A guard in `multi_verify_views` (where block0 is
already validated) with the block1 shape check, derived from AIR metadata
only and mirroring step_2 exactly (width, height, dimensions_consistent).
Constant per-proof integer comparisons, no loop over data -- the verifier
stays cycle-lean and never panics on a malformed proof. step_2's own
post-absorption guard is left in place as defense-in-depth.

Tests (soundness_tests.rs): a next-row block whose advertised dims disagree
with its backing data is rejected, not panicked, on both the owned and
archived paths. Confirmed the archived case panics in table.rs `get_row`
without this guard.

* refactor(verifier): fold both OOD shape checks into one helper

step_2 and the pre-absorption guard in multi_verify_views each derived
step_size, num_eval_points and the expected next-row dims, then ran the
same three checks on the next-row block. Extract ood_blocks_well_formed
and call it from both; the comment keeps only what the code cannot say
(the Round 3 absorption ordering, and why the width check is load-bearing).

The pre-absorption guard also still described the pre-split table: it
accepted any nonzero height that was a multiple of step_size, which was
correct when trace_ood_evaluations held the whole OOD grid. Since the
current/next split, block0 is exactly step_size rows tall -- what step_2
already required. Both sites now use the stricter equality, which also
subsumes the height-0 case as no AIR reports step_size 0.

Net -23 lines; stark suite 195 passing.
Composes #826's deep-composition fuse+hoist with this branch's g·z OOD
pruning in crypto/stark/src/verifier.rs (union resolution, replayed via
rerere from the pre-merge dry run): the QueryInvariantDeepTerms hoist
reads the reconstructed full OOD grid, and next rows iterate only the
transition-window columns in both the hoisted and per-query sums.
Exact because pruned positions have zero coefficient and zero grid
value. All guards from both sides preserved; no new panic paths.
Everything else from main merged clean.
@MauroToscano

Copy link
Copy Markdown
Contributor

/bench-verify

@github-actions

Copy link
Copy Markdown

Benchmark started on the bench server. The verifier bench takes ~5 min; the recursion-guest cycle comparison then adds guest builds — a few minutes when cached, up to ~1h on a cold run. The bench server is occupied until it finishes.

MauroToscano added a commit that referenced this pull request Jul 16, 2026
…h verify

PR #823 added g·z OOD trace-opening pruning. The layout metadata and the
full-grid reconstruction were then derived redundantly at several sites that
had to be kept in lockstep by hand:

  - `num_eval_points`/`next_row_cols` + `num_surviving_trace_openings` +
    `build_pruned_trace_term_coeffs` recomputed in the verifier round-4
    transcript replay and prover round-4.
  - `reconstruct_ood_full` built TWICE per verify — once in `step_2` (after the
    `ood_blocks_well_formed` shape guard) and again, unguarded, in `step_3`,
    which silently relied on `step_2`/Phase A having validated the shapes first.
  - `split_ood_blocks` args recomputed in prover round-3.

Introduce `ood::OodLayout`, a small struct bundling the AIR-derived layout
(`num_total_cols`, `num_eval_points`, `step_size`, `next_row_cols`) with methods
that forward to the existing free functions (`num_surviving`, `flags`,
`build_trace_term_coeffs`, `split_full`, `reconstruct_full`, plus
`expected_next_{width,height}` and a `next_row_cols`/`step_size` accessor). The
free functions and their pub API are unchanged; the struct only wraps them and
adds no new arithmetic. It stays decoupled from the AIR trait — a one-line
`ood_layout` helper per crate reads the four raw values and hands them to
`OodLayout::new`.

`verify_rounds_2_to_4` now builds the layout, runs the `ood_blocks_well_formed`
guard, reconstructs the full grid ONCE, and passes borrows into `step_2` and
`step_3` (which now take `ood_full`/`step_size`, and `ood_full`/`next_row_cols`/
`step_size` respectively — extending the precedent #826 set when it threaded
these through the fused `reconstruct_deep_composition_poly_evaluations_for_all_queries`
and `compute_query_invariant_deep_terms`). The guard runs before both steps
(same check, same `return false` semantics, same "Composition Polynomial
verification failed" log on failure, same order relative to grinding), removing
the hidden step_2-before-step_3 ordering dependency and doing one reconstruction
instead of two — a small guest-cycle saving on the recursion verifier. The
transcript-replay and prover metadata sites derive from the same struct.

`ood_blocks_well_formed` is left as-is: its width check uses
`trace_layout().0 + num_auxiliary_rap_columns()` (an overridable metadata source
I cannot prove equals `trace_columns`), so folding it fully onto OodLayout is not
provably behavior-preserving, and a partial fold would force a layout
construction in the Phase A hot loop for no net simplification.

Zero behavior change: Fiat-Shamir absorption/sampling order is untouched; the
metadata sites keep using `trace_columns`; the DEEP reconstruction keeps reading
`next_row_cols` on the reconstructed grid exactly as before. The verifier gains
no new panics/asserts/unwraps and every `return false` path is preserved; net
work strictly decreases (one reconstruction instead of two, no added
allocations). Validated with the full `cargo test --release -p stark` suite
(196 passed, incl. a new `OodLayout`-delegates-to-free-functions test) and
`make lint` (fmt + all four clippy passes incl. cuda) at exit 0.
The next-row fill loop scanned next_row_cols per output cell (O(width
x mask_width) per row, degrading toward O(width^2) for AIRs using the
conservative all-columns next-row window). Replace it with a zero-fill
followed by a direct scatter of each masked value into its column.

Preserves the documented never-panic contract (bounds-checked reads via
.get, malformed/short archives yield zero-filled cells) and silently
ignores out-of-range indices in next_row_cols. The scatter is
last-write-wins on duplicate indices where the old scan was
first-match-wins; both agree in practice because split_ood_blocks
never emits duplicate indices with differing values, but the two are
not bit-identical for a pathologically malformed next_row_cols.

Adds unit tests for out-of-range next_row_cols indices and a
short/truncated next_block, both exercising the no-panic path.
…h verify (#837)

PR #823 added g·z OOD trace-opening pruning. The layout metadata and the
full-grid reconstruction were then derived redundantly at several sites that
had to be kept in lockstep by hand:

  - `num_eval_points`/`next_row_cols` + `num_surviving_trace_openings` +
    `build_pruned_trace_term_coeffs` recomputed in the verifier round-4
    transcript replay and prover round-4.
  - `reconstruct_ood_full` built TWICE per verify — once in `step_2` (after the
    `ood_blocks_well_formed` shape guard) and again, unguarded, in `step_3`,
    which silently relied on `step_2`/Phase A having validated the shapes first.
  - `split_ood_blocks` args recomputed in prover round-3.

Introduce `ood::OodLayout`, a small struct bundling the AIR-derived layout
(`num_total_cols`, `num_eval_points`, `step_size`, `next_row_cols`) with methods
that forward to the existing free functions (`num_surviving`, `flags`,
`build_trace_term_coeffs`, `split_full`, `reconstruct_full`, plus
`expected_next_{width,height}` and a `next_row_cols`/`step_size` accessor). The
free functions and their pub API are unchanged; the struct only wraps them and
adds no new arithmetic. It stays decoupled from the AIR trait — a one-line
`ood_layout` helper per crate reads the four raw values and hands them to
`OodLayout::new`.

`verify_rounds_2_to_4` now builds the layout, runs the `ood_blocks_well_formed`
guard, reconstructs the full grid ONCE, and passes borrows into `step_2` and
`step_3` (which now take `ood_full`/`step_size`, and `ood_full`/`next_row_cols`/
`step_size` respectively — extending the precedent #826 set when it threaded
these through the fused `reconstruct_deep_composition_poly_evaluations_for_all_queries`
and `compute_query_invariant_deep_terms`). The guard runs before both steps
(same check, same `return false` semantics, same "Composition Polynomial
verification failed" log on failure, same order relative to grinding), removing
the hidden step_2-before-step_3 ordering dependency and doing one reconstruction
instead of two — a small guest-cycle saving on the recursion verifier. The
transcript-replay and prover metadata sites derive from the same struct.

`ood_blocks_well_formed` is left as-is: its width check uses
`trace_layout().0 + num_auxiliary_rap_columns()` (an overridable metadata source
I cannot prove equals `trace_columns`), so folding it fully onto OodLayout is not
provably behavior-preserving, and a partial fold would force a layout
construction in the Phase A hot loop for no net simplification.

Zero behavior change: Fiat-Shamir absorption/sampling order is untouched; the
metadata sites keep using `trace_columns`; the DEEP reconstruction keeps reading
`next_row_cols` on the reconstructed grid exactly as before. The verifier gains
no new panics/asserts/unwraps and every `return false` path is preserved; net
work strictly decreases (one reconstruction instead of two, no added
allocations). Validated with the full `cargo test --release -p stark` suite
(196 passed, incl. a new `OodLayout`-delegates-to-free-functions test) and
`make lint` (fmt + all four clippy passes incl. cuda) at exit 0.
@MauroToscano MauroToscano enabled auto-merge July 16, 2026 17:50
@MauroToscano MauroToscano added this pull request to the merge queue Jul 16, 2026
Merged via the queue into main with commit a864832 Jul 16, 2026
15 checks passed
@MauroToscano MauroToscano deleted the feat/logup-acc-current-row branch July 16, 2026 18:16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants