perf(verifier): reconcile DEEP point-invariant hoist + factoring + fusion; drop verifier divu

[diegokingston]

Stacked on #830 (perf/verifier-amortize-tier01). Targets recursion-guest verifier cycles (verifier.rs doubles as the in-VM recursion guest). Two independent changes, one commit each.

1. Combined optimal DEEP reconstruction (supersedes #826)

#826 hoists the point-invariant OOD/γ sums out of the per-query DEEP loop, but it was authored on a pre-pruning base (reads the full OOD grid, old denominators/root). My stack (#823 g·z pruning → #829 batched DEEP denominators → #830 inv_den[row] factoring) conflicts with it. This commit reconciles all of them into a single traversal rather than layering #826 on top:

• Hoist once per proof (new QueryInvariantDeepTerms + compute_query_invariant_deep_terms): ood_row_sum[row] = Σ_col γ·ood and h_ood_gamma = Σ_j γ_j·H_j(zᴺ) are query-point-independent, computed a single time and reused across all 2·Q points. Pruning-aware — skips the same next-row columns the per-point loop skips.
• The underrated win: with the extension-valued OOD term hoisted out, the per-point base-column product becomes base·γ (F×E, ~3 base muls) instead of (base − ood)·γ (E×E, ~9). ~3× on the dominant base columns.
• Keeps perf(verifier): amortize per-table/per-query verifier work (Tier 0 + Tier 1) #830's row-major inv_den[row] factoring (1 ext-mul/row, not /cell) and the single shared batched-denominator inverse.
• Fuses primary + symmetric (−x) points into one row traversal (reconstruct_deep_composition_poly_evaluation_pair), replacing the two single-point calls. Drops the now-dead sym branch from query_challenge_to_evaluation_point (symmetric = −primary always).

Byte-identical to #830: (a−b)·c = a·c − b·c, base·γ = embed(base)·γ, and Σ(aᵢ) − Σ(bᵢ) = Σ(aᵢ−bᵢ) hold exactly in the field. The γ-grid shape guard is validated once and reused; each opening's composition-part count is checked against the invariant so both H sums span the same terms (malformed proofs fail closed).

2. Remove the last runtime-divisor divu from the verify path

lde_length / trace_length (fri_termination_params) and codeword_len / coeffs.len() (terminal_codeword_from_coeffs) divided by a runtime value — a real divu on RISC-V. Both divisors are powers of two, so each ratio is exactly a shift by the difference of trailing_zeros(). Cold (once per table), but it means the verifier now has no runtime-divisor division left: field ops are already division-free (Goldilocks reduce128 + Fermat inv), and the hot per-query/per-layer index math (iota % 2, merkle is_multiple_of(2) + index >>= 1, FRI /2 folds) lowers to shifts/masks.

Validation

• 198 stark tests pass (real prove→verify roundtrips hit every changed line — any DEEP drift desyncs the codeword from the FRI fold).
• clippy clean.
• Recursion-cycle benchmark + GPU: server (no local RISC-V toolchain).

Closes #826 (this subsumes it).

[diegokingston]

/bench-verify

[github-actions]

⏳ 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]

Verifier benchmark — bc0bc9a1d8 vs main (20 pairs)

=== Verify ABBA result ===

Metric	main	PR	Δ
Verify time (per-side)	3.779s	3.681s	-2.58% 🟢
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.681s   mean B (main): 3.779s
  [parametric] paired-t   mean -2.58%   sd 0.81%   se 0.18%
               95% CI: [-2.96%, -2.20%]   (t df=19 = 2.093)
  [robust]     median -2.46%   Wilcoxon W+=0 W-=210  p(exact)=1.9e-06  (z=-3.90)

  run-to-run jitter:    A CV 0.43%   B CV 0.80%        (lower = steadier)
  within-session drift: -0.59% over the run, 1st->2nd half -0.14%

🟢 REAL IMPROVEMENT — PR verifies ~2.58% 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 4c108a1 guest=recursion-min.elf
REF_A (PR) bc0bc9a bc0bc9a guest=recursion-min.elf

Metric	REF_B (baseline)	REF_A (PR)	Δ (A-B)
Guest cycles	51.4M	52.7M	+1.4M (+2.64%)
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=4c108a10ff5e3c0556a5406e531ff43039f2350d ref_b_elf=recursion-min.elf ref_b_cycles=51388059 ref_b_keccak=3885 ref_b_execute_wall_s=2
ref_a_sha=bc0bc9a1d8ae28b7e969a62fe416adbd678c8ff2 ref_a_elf=recursion-min.elf ref_a_cycles=52745916 ref_a_keccak=3025 ref_a_execute_wall_s=2
delta_cycles=1357857 delta_keccak=-860