Feat/fext recursion wiring

[jotabulacios]

No description provided.

[github-actions]

Benchmark Results for unmodified programs 🚀

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base binary_search	65.8 ± 1.8	64.0	69.8	1.00 ± 0.04
head binary_search	65.5 ± 1.9	64.1	70.5	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base bitwise_ops	65.8 ± 0.6	65.1	66.7	1.01 ± 0.02
head bitwise_ops	65.4 ± 0.9	64.6	66.4	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base ecsm	3.4 ± 0.0	3.3	3.4	1.00
head ecsm	3.6 ± 0.1	3.4	3.7	1.06 ± 0.03

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base fibonacci_26	71.4 ± 7.1	66.8	89.9	1.05 ± 0.11
head fibonacci_26	68.3 ± 1.1	67.0	70.0	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base hashmap	134.7 ± 3.7	129.3	140.5	1.00
head hashmap	135.9 ± 3.9	130.5	141.3	1.01 ± 0.04

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base keccak	132.0 ± 2.3	128.0	134.8	1.01 ± 0.03
head keccak	131.1 ± 3.3	126.3	136.2	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base matrix_multiply	67.9 ± 0.8	67.0	69.1	1.00
head matrix_multiply	68.0 ± 0.6	67.1	68.7	1.00 ± 0.01

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base modular_exp	64.8 ± 0.5	64.4	65.8	1.00
head modular_exp	65.5 ± 0.9	64.4	67.2	1.01 ± 0.02

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base quicksort	68.7 ± 0.8	67.7	69.6	1.00
head quicksort	69.0 ± 0.6	67.8	69.8	1.01 ± 0.02

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base sieve	70.6 ± 0.7	69.3	71.3	1.00
head sieve	72.8 ± 4.4	69.3	80.9	1.03 ± 0.06

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base sum_array	80.1 ± 0.8	79.3	81.6	1.00 ± 0.01
head sum_array	79.8 ± 0.6	79.1	80.8	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base syscall_commit	97.3 ± 1.5	96.0	100.9	1.00 ± 0.02
head syscall_commit	97.2 ± 1.2	95.9	98.6	1.00

[MauroToscano]

⚠️ AI-generated review. Produced by an automated agent and posted from this account — not written by hand. Findings below are leads to verify, not confirmed conclusions.

This PR wires a riscv64 FEXT accelerator into FieldExtension, bans FEXT ops under continuation (μ = 0 on the four FEXT AIRs via build_epoch_airs, used by both prove_epoch and the epoch verify path, so the ban binds the verifier), and substitutes four FieldExtension::fma calls in reconstruct_deep_composition_poly_evaluation_pair that are value-identical to the arithmetic they replace over the post-#826 fused loop, with no new proof-derived indexing or transcript movement. Two blockers: the stack cannot prove the guest it just accelerated, and much of the new API has no callers.

prover/src/continuation.rs:440 (with crypto/crypto/src/field_ext.rs:132, prover/src/tables/trace_builder.rs:3388) — the two halves contradict. Fp3Fma for riscv64 is gated on target_arch alone, no feature, so the recursion guest ELF emits fext_load/fext_fma/fext_store on every FRI query (GoldilocksExtension = Degree3GoldilocksExtensionField, so the guest Verifier picks the accelerated impl, not the software default). Yet build_traces returns Err(FextInContinuation) whenever l2g_memory_bookend is set and any FEXT op exists, and this PR forces the four FEXT AIRs empty every epoch. The recursion guest is proven only through continuation — prove_outer_and_commit (recursion_smoke_test.rs:107) calls prove_and_verify_continuation, and OuterMode is only ExecuteOnly/Prove — so once make compile-recursion-elfs picks this up, outer prove errors out. CI misses it: test_recursion_prove_empty/test_recursion_prove_1query are #[ignore]d, the merge-queue filter -E 'test(test_prove_elfs_all_instructions_64_full) | test(test_recursion_execute)' --run-ignored ignored-only matches neither, and the execute-only tier passes because the executor has no continuation-mode FEXT guard. test_recursion_prove_1query should run against a rebuilt ELF before landing, plus one of: carry field storage across epochs (FEXT_PAGE bookend under continuation), feature-gate the guest impl so the continuation-proven guest falls back to software Fp3, or hold the verifier wiring. The merge-queue -E also needs a prove-tier recursion test.

crypto/crypto/src/field_ext.rs:37 — ProdAcc/prod_acc_new/prod_acc_add/prod_acc_finish, ext_mul, the guest GuestAcc double-buffer with its H_T/H_ACC0/H_ACC1/H_ZERO handles, and ~155 lines of executor differential tests have zero callers; a workspace grep for prod_acc, ext_mul, GuestAcc outside field_ext.rs and fext_tests.rs is empty. daa03a8 wired prod_acc_* into the old per-column fold and fma into the composition-parts fold (verifier.rs:742-753 and :768 at c14ce62); 4fb663b's conflict resolution against main's fused reconstruct_deep kept only the four fma sites. Three docs now describe unshipped code: the module doc ("the generic verifier can call FieldExtension::fma(..) / ext_mul(..)"), the ProdAcc doc (removing the per-op LOAD/STORE roundtrip), and the fext_tests.rs header ("the exact syscall sequences the in-guest STARK verifier emits"). Either re-wire the resident accumulator onto the fused loop shape — needs a two-factor variant, prod_acc_add being a*b*c while the fused accumulations are 2-factor — or delete the machinery, the handles, and fext_prod_acc_chain_matches_reference/fext_ext_mul_via_unwritten_zero_matches_reference, and fix the docs. Unreferenced guest code with cross-call handle-state invariants (two live GuestAccs corrupt each other) invites a bad reuse.

prover/src/tests/fext_page_tests.rs:257 — the last-row half of fext_page_rejects_non_bit_sel_same covers the exact hole the new constraint closes (idx 6 is exempt there) but never evaluates constraint 11: it reads the tampered cell back and asserts sel * (1 - sel) != 0, i.e. that (-1)·2 ≠ 0, true regardless of the AIR. Changing idx 11 to emit_base_rows(.., RowDomain::except_last(1), ..) would reopen the hole with this test still green. The binding property is metadata, not evaluation (emit_is_bit → emit_base → end_exemptions == 0), so assert assert_eq!(FextPageConstraints.meta()[11].end_exemptions, 0), or build the wraparound frame (last, 0) by hand as fext_page_forbid_empty_rejects_active_row does and check base[11] != 0. The row-0 half (sel_same = 2) is fine.

Nits:

• prover/src/test_utils.rs:1016 — ForbidEmpty names the opposite of its behaviour (its own doc: "forcing the table to be empty"); ForceEmpty is accurate.
• prover/src/test_utils.rs:1024 — let mu0_idx = self.base.meta().len(); inside eval re-runs the base body through a MetaBuilder and allocates + sorts a Vec<ConstraintMeta> per evaluation, against meta()'s "runs once at setup — never on the per-row prover path" contract; the index is a per-table constant, pass it from the create_*_forbidden factories.
• Only create_fext_page_air_forbidden tests that μ = 0 fires on an active row; create_fext_load/fma/store_air_forbidden pass fext_*_cols::MU unexercised, so a wrong mu_col after a column reshuffle silently no-ops the ban while positive continuation tests stay green (μ = 0 holds trivially on empty tables).
• crypto/stark/src/verifier.rs:947 — h_sum += h_i_upsilon * gamma is ext × ext in the same per-query function and still on the software path, while the comment two hunks above says ext × ext routes through the accelerator; convert it or note why not.