fix(verifier): pin each trace-opening column width to the AIR, not just their sum

[MauroToscano]

A query opening carries the trace row as three prover-supplied vectors — precomputed ‖ main (base field) and aux (extension field) — which the DEEP reconstruction consumes as one concatenated row. The verifier pinned only their sum, against the AIR-pinned OOD width (verifier.rs:972-979, with ood_width fixed by ood_blocks_well_formed at :191-196).

Nothing pinned the individual terms, and the Merkle leaf hash pins neither split: hash_data_from_slices (crypto/crypto/src/merkle_tree/backends/field_element_vector.rs:173-179) streams evaluations ‖ evaluations_sym with no length prefix and no separator, so a leaf can be re-split freely. The verifier never called num_precomputed_columns() at all — its only non-definition use in the repo was prover.rs:3171.

Each of the three trees is transcript-bound at a different time, so the split was a soundness parameter the prover was choosing. Both splits were live breaks, each demonstrated end to end by a false statement the stock verifier accepts.

This PR changes the verifier only — prover.rs is byte-identical to main.

precomputed↔main

For a non-preprocessed AIR the precomputed root is never absorbed — verifier.rs:1208 is the only absorption and it sits inside the is_preprocessed() branch. A prover declares real trace columns "precomputed", leaving them bound by nothing, reads the round-2 challenge beta, and solves for them.

It works because step_2 folds boundary and transition constraints into a single sum with all coefficients powers of one beta — so the composition identity imposes exactly one condition per trace row, and one unbound column supplies exactly one free value per row. Executed on 2-col Fibonacci with a public output: the verifier accepts a claimed output of 999 where the only valid execution for (a0,a1)=(1,1) yields 2178309, with 30 of 30 constraint instances violated.

main↔aux

The aux root is absorbed only in round 1 phase C (verifier.rs:1269-1271), after the shared LogUp challenges are sampled (:1221-1227). Moving a column from main into the aux tree therefore lets the prover choose it after z and alpha.

Demonstrated on the in-repo LogReadOnlyRAP (read-only memory) by moving the multiplicity column into the aux tree. The verifier's frame split (:290) uses the AIR's honest aux count, so it still evaluates the column as main — only the binding time changes. That collapses LogUp from a multiset equality (which must hold as a rational identity in z) into one scalar equation the prover solves after the fact. The in-test diagnostic states it exactly:

LogUp residual at the protocol's (z,alpha) = 0
LogUp residual at a FRESH (z',alpha')      = 4745845707844760936, ...

The accepted proof asserts address 3 holds both 30 and 999999 — false for any single-valued memory. No fingerprint collision is needed, no prover modification is needed (prover and verifier absorb main-root-then-aux-root either way, so the transcripts agree), and it survives the rkyv wire: 3272 bytes, accepted by multi_verify_archived, the recursion-guest path.

This is the more dangerous of the two — LogUp is the VM's entire cross-table integrity argument, and traits.rs:182-188 notes the trailing main columns of every preprocessed table are exactly the multiplicities.

The fix

trace_opening_widths_well_formed(air, proof, num_queries) — a sibling of ood_blocks_well_formed — pins all three widths, independently for evaluations() and evaluations_sym():

precomputed == if air.is_preprocessed() { air.num_precomputed_columns() } else { 0 }
main        == air.trace_layout().0 - precomputed          (checked_sub; malformed AIR rejects)
aux         == air.num_auxiliary_rap_columns()

Called once per table from verify_rounds_2_to_4, immediately after the query_list_len guard — before the challenge replay and before step_3_verify_fri, the first consumer of any opening. It needs no challenges: the query count comes from air.options().fri_number_of_queries, identical to challenges.iotas.len(). Absent optional openings count as 0, matching the .unwrap_or(&[]) in the reconstruction.

The old sum guards remain, but as pure panic guards; their comment now says so rather than implying they are the soundness argument.

The fourth opening vector — composition parts — was already pinned (number_of_parts from composition_parts_ood.len(), itself pinned to air.composition_poly_degree_bound(trace_length)/trace_length at :1167-1170, with per-query lengths checked at :1135). So the "prover chooses a width" class is now closed across trace and composition openings.

Supersedes #906

#906 guards one shape (root.is_some() for a non-preprocessed AIR) at one site. Every proof it rejects is rejected here, earlier and for the general reason — including the root-absent variant it misses (its own PoC 3). Its regression test also passes on unpatched main, so it does not pin its own fix. #906 can be closed in favour of this.

Three comments that claimed guarantees which did not exist

This class hid behind its own documentation, and that is worth as much attention as the diff:

1. :972-979 — presented as a runtime panic guard and implying a width guarantee. It only ever checked the sum. Now says so and points at the authoritative pin.
2. The precomputed arm of verify_trace_openings — "Mismatched presence is unreachable in practice (multi_verify rejects such proofs upstream)". Upstream rejected nothing; the claim was simply false. Now states exactly what that arm still catches (the degenerate zero-width opening).
3. The aux arm had no comment at all, and reading it you would assume authentication implied a width. It now says the authentication constrains no width, and points upstream.

Tests

• Three end-to-end regressions that fail on stock main — precomputed_opening_narrower_than_the_air_declares_is_rejected, mis_split_aux_opening_is_rejected, and false_memory_read_under_aux_split_is_rejected (the last also asserts the archived/wire path).
• Seven controls that pass on both main and this branch, so the pin is not vacuous — including honest_preprocessed_proof_still_verifies (a table with num_precomputed_columns() > 0, which must keep verifying), honest_logup_rap_proof_still_verifies, and the two "same lie without the split" / "split without the challenge solve" cases that show the split itself is what buys the attack.
• Direct guard tests covering every width in both slots, per-query enforcement, and truncated opening lists, plus the compiled-in tripwire.

Discrimination was verified by running the same test files against a stock-main control worktree with prover.rs stock in both: 3 failed, 7 passed there.

cargo test --release -p stark → 217 passed, 0 failed (15 of them new). cargo test --release -p lambda-vm-prover → 520 passed; the 5 failures are the pre-existing missing program_artifacts/recursion/*.elf panics, verified identical on the control worktree. make lint → exit 0.

Two notes for review

No prover changes. The aux break needs none by nature — prover and verifier absorb
main-root-then-aux-root either way, so the transcripts agree. The precomputed term is reached
hook-free by handing the prover an AIR declaring 1 precomputed column and the verifier one declaring
2, with the same commitment constant.

One honest caveat on that precomputed test's strength, which is stated in its doc comment rather than
left to read as a second exploit: for a real preprocessed table the round-1 root equality would
also catch that shape, since an honest constant is a root over exactly num_precomputed_columns()
columns. That defence is incidental — nothing states the invariant, nothing checks it, and it does
not exist at all for a non-preprocessed AIR. The stronger precomputed demonstration (a false
statement accepted, against a hostile prover — which is what a real attacker runs) is preserved
outside this branch; it needs a test-only prover switch to be discriminating, and that did not seem
worth a permanent oddity in a security-critical file.

A tripwire, not a source hash. precheck_the_width_pin_is_compiled_in asserts the guard is both
defined and called in the compiled verifier — deleting the call site while keeping the function is
the refactor that would otherwise turn this file green for the wrong reason. A source-hash check was
considered and rejected: right for a throwaway branch, wrong in-repo where it breaks on every
unrelated verifier edit. The three break tests additionally assert attribution behaviourally, each
calling the guard on the very proof it rejects, so a green "rejected" cannot come from elsewhere.

Guest-cycle cost is unmeasured. The check is O(queries × tables) length reads, and the recursion
verifier runs it in-circuit — roughly 219 queries × ~20 tables. If /profile_recursion later shows
it, the zero-extra-pass variant is to thread the three expected widths into the existing per-query
loop in reconstruct_deep_composition_poly_evaluations_for_all_queries: same coverage, later and
repeated rather than early and once. Placement here favours rejecting before any consumer reads
attacker-shaped data.