fix(verifier): reject unexpected precomputed commitment for normal AIRs

[diegokingston]

A proof for a non-preprocessed AIR could include an optional precomputed trace commitment. The verifier neither rejected nor absorbed that root before sampling Fiat-Shamir challenges, yet later authenticated and used the corresponding openings in verify_trace_openings and the DEEP composition reconstruction. A malicious prover could therefore choose security-critical trace columns (e.g. bitwise) after learning the challenges.

The normal-table branch of the round-1 replay now rejects any proof carrying a precomputed commitment. Honest provers never set it for non-preprocessed AIRs, so rejection is safe. The fix lives in multi_verify_views, the single implementation shared by multi_verify and multi_verify_archived (recursion guest).

[MauroToscano]

Reviewed adversarially — a prosecutor and a defense working the premise independently, then reproduced end to end. The issue is real, the fix is correct and load-bearing, and the regression test is vacuous and needs replacing. Details and a ready-made replacement below.

The issue is real — confirmed by execution

A forged proof is accepted by the stock origin/main verifier for a trace that violates 30 of 30 constrained instances of Fibonacci2ColsAIR:

POC906/2 forged trace violates 30 real constraint instances
POC906/2 main root unchanged by column 0 = true
POC906/2 opening widths: precomputed=1 main=1 (AIR width=2)
POC906/2 FORGED PROOF ACCEPTED BY STOCK VERIFIER = true

Controls discriminate, so the harness is not simply accepting everything:

POC906/CONTROL-A no-split forgery accepted            = false
POC906/CONTROL-B honest split proof accepted           = true
POC906/CONTROL-B corrupted precomputed opening accepted = false
POC906/3 mirror shape (root=None, openings=Some)       = false

The only non-test change is attacker-side: a #[cfg(test)] switch in the prover that skips absorbing the precomputed root in round 1. That is the threat model, not cheating — an attacker runs their own prover, and nothing compels them to absorb a root the verifier never reads. The verifier is byte-for-byte stock. Applying the fix from this PR rejects the forgery, so it is load-bearing.

The mechanism is a re-partition, not extra columns — worth correcting in the PR body

Extra columns are impossible, and there are two real guards:

• ood_blocks_well_formed (verifier.rs:191-196, run at :1181) pins the OOD width to air.trace_layout().0 + air.num_auxiliary_rap_columns().
• verifier.rs:972-979 pins num_precomputed + num_main + num_aux == ood_width.

But nothing pins num_precomputed and num_main individually. So a prover splits the W real columns as N unbound + (W−N) bound, and base_at (verifier.rs:951-957) serves the first N from the tree with no transcript binding. Above: precomputed=1, main=1 against an AIR of width 2.

The exploit then follows from what the composition polynomial actually proves — that a random linear combination of constraints vanishes, not that each does:

1. Declare column 0 "precomputed". Round 1 commits only column 1 — hence main root unchanged by column 0 = true.
2. Read beta off the transcript.
3. Solve c0 + beta·c1 = 0 for column 0 given an arbitrary column 1:
   A_{i+1} = [A_i + B_i(1+beta) − beta·B_{i+1}] / (1 − beta).

Every individual constraint is violated while the combination vanishes identically, so the quotient really is low-degree and FRI/DEEP/OOD all pass honestly. The PR body's framing ("choose security-critical trace columns after learning the challenges") is right, but it undersells it: this is arbitrary constraint forgery for any non-preprocessed table, not merely unbound extra columns.

Scope note (inferred from reading shared code paths, not executed at VM level): all VM tables except bitwise and keccak_rc are non-preprocessed (traits.rs:178 default), and prover/src/lib.rs:1412, continuation.rs:851, continuation.rs:1013 all funnel through the same multi_verify_views. LogUp challenges are sampled at verifier.rs:1221, i.e. after round-1 phase A — so unbound base columns could likewise be chosen after the bus challenge, putting cross-table bus soundness in scope.

⚠️ The regression test is vacuous — it passes on unpatched main

This is the one thing I would ask you to change before merging.

Applying only the air_tests.rs hunk to an otherwise-stock origin/main:

test tests::air_tests::test_reject_unexpected_precomputed_commitment ... ok

It passes without the fix. The test sets lde_trace_precomputed_merkle_root = Some([0x42; 32]) but leaves every precomputed_trace_polys: None, so origin/main already rejects it — at verify_trace_openings via the pre-existing (Some, None) => _ => false arm at verifier.rs:555, nothing to do with the new check. The new check never executes in this test. It would not have caught the bug and will not catch its regression.

The replacement needs the (Some, Some) shape with a narrowed main opening — i.e. the forgery above. poc906_forged_trace_accepted_for_normal_air is a ready-made drop-in: it fails on main and passes with the fix, which is the pass→fail hinge a regression test needs. Happy to hand over the PoC file.

(For the record, one worry of mine that turned out unfounded: Verifier::verify (verifier.rs:1340-1355) is a thin wrapper over multi_verify_views, so the test's entry point does reach the patched code. The problem is the proof shape, not the entry point.)

Two gaps that survive the fix

1. The mirror shape is still only caught by accident. root = None + openings = Some(...) sails past the new is_some() guard, and the reindexed columns are consumed by the DEEP/FRI reconstruction (verifier.rs:866) before anything rejects them. PoC 3 confirms it is still rejected today — but solely by the (None, Some) arm at verifier.rs:555, the arm whose own comment calls it unreachable defensive code. Suggest also rejecting precomputed_trace_polys.is_some() for normal AIRs in round 1.

2. The comment at verifier.rs:546-548 claims mismatched presence "is unreachable in practice (multi_verify rejects such proofs upstream)". On origin/main that was simply false, and it is a good candidate for why this went unnoticed — a doc comment asserting a guarantee nothing provided. This PR makes it true in one direction; worth updating to say which guard, where, and for which direction, rather than leaving the blanket claim.

Also suggested: an explicit width check, num_precomputed == air.num_precomputed_columns(). Today the safety of preprocessed tables rests indirectly on the hardcoded root pinning their leaf width; an explicit check makes the invariant local instead of emergent, and would have closed this class outright.

Summary

Is the issue real?	Yes — forged proof accepted by stock main, reproduced independently
Is the fix correct?	Yes — rejects the forgery; correctly placed in the shared multi_verify_views
Is the test adequate?	No — passes on unpatched main, proves nothing
Severity	High — arbitrary constraint forgery for any non-preprocessed AIR

Method: adversarial prosecutor/defense on the premise, then the PoC re-run by me in a separate clean worktree with verifier.rs verified stock before running. My first run showed rejection because the prosecutor's worktree still had the fix applied — worth mentioning so nobody repeats that and concludes the opposite.

[MauroToscano]

Corrections and an upgrade to my review above, after an independent adjudication pass re-ran everything. One item I posted was factually wrong — correcting it publicly. The verdict on the PR is unchanged: the issue is real, the fix is correct, the test needs replacing.

Upgrade: severity is Critical, and it is now executed rather than argued

My review demonstrated an invalid witness accepted. That is weaker than it sounds, because for Fibonacci2ColsAIR with (a0=1, a1=1) a valid trace does exist — the honest one. The distinction between "invalid witness accepted" and "false statement accepted" is the whole severity question, and neither my review nor the original PoC closed it.

It is closed now, by execution on a stock origin/main verifier. Adding one boundary constraint pinning the last row to a public output makes the statement falsifiable:

POC906J true b[15] for (a0,a1)=(1,1) = 2178309
POC906J claimed public output out      = 999
POC906J CONTROL honest trace w/ false out accepted    = false   <- boundary is live
POC906J CONTROL true statement, honest proof accepted = true    <- completeness intact
POC906J forged trace violates 30 real constraint instances
POC906J forged boundaries: a[0]=1 b[0]=1 b[15]=999              <- all boundaries satisfied
POC906J FALSE STATEMENT ACCEPTED BY STOCK VERIFIER = true

The verifier accepts "there is a valid 2-col Fibonacci execution of length 16 with a0=1, a1=1 and public output 999" when the only such execution outputs 2178309. Both polarities controlled; with this PR's hunk applied it flips to false and the true-statement control still verifies. I re-ran this myself with verifier.rs hash-verified against origin/main before trusting it.

Why it generalises, and why this is not a Fibonacci artefact: step_2 folds boundary and transition constraints into a single sum with all coefficients powers of one beta (verifier.rs:1397-1401, lookup.rs:73-83). The composition identity therefore imposes exactly one condition per trace row, and one unbound column supplies exactly one free value per row — so the attacker fixes every other column arbitrarily and solves the free one. Demonstrated on two AIRs; generic by that argument. I would still not claim a VM-table forgery exists until someone builds one — for a real high-degree AIR the per-row solve is generically-but-not-provably feasible.

❌ Correction: my scope note was wrong

I wrote that all VM tables except bitwise and keccak_rc are non-preprocessed. That is incorrect — it omits three preprocessed families. The seven with_preprocessed sites in prover/src/lib.rs are:

site	table
:709	bitwise (when !minimal_bitwise; all production callers pass false)
:748	decode
:770	keccak_rc
:780 / :786	register
:811 / :825	page — zero-init and ELF-data; private-input pages are explicitly not preprocessed

So the preprocessed set is {bitwise, decode, keccak_rc, register, page-except-private-input}. Still vulnerable: CPU, CPU32, LT, SHIFT, MEMW, MEMW_ALIGNED, MEMW_REGISTER, LOAD, STORE, MUL, DVRM, BRANCH, EQ, BYTEWISE, HALT, COMMIT (which carries the public output), KECCAK, KECCAK_RND, ECSM, ECDAS, private-input PAGEs, and in continuations L2G (continuation.rs:187-203) — the cross-epoch memory linkage.

The conclusion is unchanged — the execution core is in scope — but the sentence as I wrote it was wrong. Also, for VM AIRs is_preprocessed() resolves at lookup.rs:1347-1349, not the traits.rs:178 default; cite the former.

Entry points, corrected and extended: prover/src/lib.rs:1412, continuation.rs:851, continuation.rs:1013, Verifier::verify (:1340-1355), and multi_verify_archived (verifier.rs:1108→1118) — the recursion guest. All share the patched body, so recursion and continuations are both in scope and both covered by the fix.

❌ Correction: my wording on the vacuous test was rebuttable

I wrote "the new check never executes in this test". That is imprecise — on a patched build the new check does fire and is the reason for rejection. The accurate and load-bearing claim is:

the test's outcome does not depend on the fix — it passes with and without it.

The finding stands (it is not a regression test), but state it that way; as I first wrote it, the rebuttal would have been correct.

One practical note on replacing the test

Worth saying up front, because it is the main friction: any behavioural regression test here needs a small #[cfg(test)] hook on the prover's round-1 absorption (crypto/stark/src/prover.rs:3196). Without it a tampered honest proof diverges on the transcript and is rejected for an unrelated reason — which is exactly why the current test cannot work.

The cheapest discriminating test is not the forgery at all: it is an honest trace under a split declaration (CONTROL-B above) — accepted on main, rejected with the fix, no forged trace needed. Happy to hand over either.

One thing that survives the fix, worth its own look

The same defect class exists on the main↔aux split and this PR does not close it. num_auxiliary_rap_columns() is used only at verifier.rs:192 (OOD total width) and :290 (frame split) — the aux opening width is never pinned, so a prover can move base columns into the aux tree exactly as it moves them into the precomputed tree. The aux root is absorbed at :1269-1271, after the LogUp challenges are sampled at :1221-1227.

Constraint enforcement survives (aux is bound before beta), but base columns chosen after z/alpha is precisely what LogUp soundness forbids — with bus tuples longer than the extension degree, fingerprint collisions become computable once alpha is known. This is inferred, not executed, and I would not block this PR on it. It is the strongest argument for pinning all three opening widths in one place rather than special-casing precomputed:

num_precomputed == if air.is_preprocessed() { air.num_precomputed_columns() } else { 0 }

…checking both evaluations() and evaluations_sym(), since the leaf hash pins neither split (field_element_vector.rs:173-179 streams a ‖ b with no length prefix or separator, and the verifier never calls num_precomputed_columns() at all — its only non-definition use in the repo is prover.rs:3171).

For the record, that also resolves a question I raised above: the preprocessed branch does not need an analogous check, but not because the hardcoded root pins the leaf width — it doesn't. It is because on that branch both roots are absorbed at :1208-1209, before beta at :1380, so every openable value is committed before any challenge exists and no post-challenge freedom remains.

Everything else in my review re-derived cleanly: the re-partition mechanism, both guard citations, base_at at :951-957, the vacuous-test finding, the stale comment at :546-548, the mirror-shape gap, and that the fix is correct and load-bearing.

[MauroToscano]

Superseded by #909, which closes this defect class generally rather than this one shape.

#909 pins all three trace-opening widths to the AIR (precomputed, main, aux — in both the regular and symmetric slot), once per table, before any opening is read. Relative to this PR:

• It rejects everything this PR rejects, earlier and for the general reason — a non-preprocessed AIR must have precomputed opening width 0, so the columns cannot be smuggled at all.
• It also catches the root-absent variant this PR misses (root = None, openings = Some) — the shape poc906_mirror_shape_root_none_openings_some covers, which currently survives the is_some() guard and is only caught downstream by the arm whose own comment calls it unreachable.
• It closes a second live break in the same class: the aux opening width is equally unpinned, and the aux root is absorbed after the LogUp challenges. Moving a multiplicity column into the aux tree collapses LogUp's multiset equality into one scalar equation solved after z/alpha. That one is executed too — a false memory read accepted on stock main, needing no prover modification, and surviving the rkyv wire through multi_verify_archived.

The diagnosis in this PR was correct and the fix works — I verified it rejects the forgery. The only reason to close rather than merge both is that #909 makes this guard redundant, and one authoritative check reads better than two partial ones.

One thing worth carrying over regardless of what happens here: this PR's regression test passes on unpatched main (it leaves precomputed_trace_polys: None, so the pre-existing (Some, None) arm rejects it and the new check never runs). #909's equivalents were each verified to fail on main and pass with the fix.