Skip to content

fix(stark): review follow-ups for OOD pruning (docs, saturating_sub, hard assert)#833

Merged
MauroToscano merged 3 commits into
feat/logup-acc-current-rowfrom
fix/logup-ood-pruning-review-nits
Jul 16, 2026
Merged

fix(stark): review follow-ups for OOD pruning (docs, saturating_sub, hard assert)#833
MauroToscano merged 3 commits into
feat/logup-acc-current-rowfrom
fix/logup-ood-pruning-review-nits

Conversation

@MauroToscano

@MauroToscano MauroToscano commented Jul 16, 2026

Copy link
Copy Markdown
Contributor

Review follow-ups for #823 (forward LogUp accumulation + next-row OOD opening pruning). Docs and consistency only; no behavior change.

  • Stale doc in logup_single_source_tests (lookup.rs): the module doc claimed the 2-absorbed branch "reads aux(1, ·) next-row cells". That described pre-refactor(logup): forward accumulation so acc is the sole next-row OOD read #823 backward accumulation; after forward accumulation both branches' only next-row read is acc_next, and absorbed operands read offset 0. Replaced with the branch's real distinction — it folds two absorbed interactions (degree 3).
  • Narrow doc in ood.rs module header: reworded the OOD-table illustration so it is no longer pinned to offsets [0, 1]. The layout is generic over transition_offsets.len() (repo has [0] and [0,1,2] example AIRs): offset 0 is the current-row block, every later offset contributes a next-row block.
  • Consistency nit in verifier.rs: num_eval_points - step_sizenum_eval_points.saturating_sub(step_size), matching the shared ood.rs helper for the identical quantity. Purely defensive; the underflow is unreachable (would require an AIR with empty transition_offsets, which does not exist and is not proof-controlled).
  • Doc-only precondition note in build_pruned_trace_term_coeffs (ood.rs): added a Precondition: line to the doc comment stating that powers.len() must equal num_surviving_trace_openings(...) for the same layout args (both AIR-metadata-derived, invariant I3), checked in debug builds. Code is unchanged: the per-slot if p < powers.len() guards and the debug_assert_eq! power-count check stay. Rationale: this is a shared helper the verifier calls, and the verifier must never contain a panic path — an invalid proof is a false proof, not a crash — so the release-mode bounds check is intentional and stays.

Also in this PR (clears the base branch's latent Lint failure, which is inherited here):

  • Clippy fixes in the refactor(logup): forward accumulation so acc is the sole next-row OOD read #823-added forward-accumulation tests (lookup.rs accumulated_column_is_forward_and_circular, logup_gpu.rs reference_accumulate): iterate slices directly instead of 0..n (needless_range_loop) and deref instead of .clone() on Copy field elements (clone_on_copy). make lint runs cargo clippy --workspace --all-targets; --all-targets covers these test targets. The logup_gpu.rs one only surfaces under the cuda-feature clippy pass.
  • A one-line rustfmt reflow of an over-width test call in ood.rs, the only cargo fmt --check --all violation on the base.

Validation: make lint (fmt --check --all + all four --workspace --all-targets clippy passes incl. cuda) green; cargo test --release -p stark passes ood:: (4), logup_single_source (7), and bus_tests (75).

- 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.
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.
@MauroToscano

Copy link
Copy Markdown
Contributor Author

Second commit (009f6de) clears the Lint job, which was latently red on the base branch: make lint runs cargo clippy --workspace --all-targets, and the --all-targets flag covers test code that the initial crate-scoped lib clippy skipped. Five -D warnings errors in tests added on the #823 branch:

  • 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). This one only surfaces under the cuda-feature clippy pass (make lint's 4th clippy invocation), which the earlier passes stop short of.

Verified locally by running the exact CI make lint (fmt --check --all + all four --workspace --all-targets clippy passes incl. --features lambda-vm-prover/cuda) to green, and re-running the release-mode ood::, logup_single_source, and bus_tests suites (plus the rewritten test) — all pass. Test semantics are unchanged.

…erm_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
MauroToscano merged commit 9c5a449 into feat/logup-acc-current-row Jul 16, 2026
8 checks passed
@MauroToscano
MauroToscano deleted the fix/logup-ood-pruning-review-nits branch July 16, 2026 15:27
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.

1 participant