Feat/fext accelerator - #818
Conversation
|
Benchmark Results for modified programs 🚀
|
|
Benchmark Results for unmodified programs 🚀
|
2f8ac34 to
3bf6794
Compare
… a canonical order
…gen-sensitive CI failure
|
/ai-review |
Codex Code Review
|
AI ReviewPR #818 · 49 changed files
Findings
Status column reflects the verdict from the verifier: deepseek-verifier (openrouter/deepseek/deepseek-v4-pro). AI-002: auto_storage peak-RAM estimate omits the four FEXT tables
Claim table_specs builds the per-table memory estimate used by peak_bytes/decide, but it has no entries for fext_load, fext_fma, fext_store or fext_page. Even if count_table_lengths were updated, these fixed-size tables would still be ignored, so disk-spill decisions for FEXT-heavy proofs will underestimate peak RAM. Evidence The loop in count_table_lengths (lines 4133-4216) counts ECALL Commit and Keccak/ECSM, but never checks cpu_op.ecall_fext_load/fext_fma/fext_store. It also never calls any FEXT-specific LT/bitwise collectors. The comment at line 4077 says it 'Must stay in sync with Traces::from_elf_and_logs', but the FEXT additions in collect_ops_from_cpu/build_traces are not mirrored here. Suggested fix Mirror the FEXT accounting from the trace builder in count_table_lengths: add FEXT ecall counts, add their register reads to memw_register_count, add their LT and bitwise lookup counts to lt_count, and account for FEXT_PAGE/FEXT_L2G addr-LT lookups when present. AI-007: `fext_baseline` Rust program is dead code added by the PR
Claim A new Rust program ( Evidence The only references to Suggested fix Either delete the Reviewer Lanes
Verification Lanes
Native Codex and Claude reviews run separately and post their own comments. They are not included in this structured provenance report. Discarded candidates (5) — rejected by the verifier
Raw lane outputs, candidates, final issues, and model metrics are uploaded as workflow artifacts. |
|
/bench-verify |
|
⏳ 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. |
Verifier benchmark —
|
| Metric | main | PR | Δ |
|---|---|---|---|
| Verify time (per-side) | 3.479s | 3.657s | +5.10% 🔴 |
| Proof size | 204.30 MiB | 205.52 MiB | +0.60% 🔴 |
Per-side (
⚠️ PR REJECTS the baseline's valid proof — likely a VERIFY REGRESSION, not a 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.657s mean B (main): 3.479s
[parametric] paired-t mean +5.10% sd 0.86% se 0.19%
95% CI: [+4.70%, +5.51%] (t df=19 = 2.093)
[robust] median +5.06% Wilcoxon W+=210 W-=0 p(exact)=1.9e-06 (z=+3.90)
run-to-run jitter: A CV 0.67% B CV 0.39% (lower = steadier)
within-session drift: -0.20% over the run, 1st->2nd half +0.01%
🔴 REAL REGRESSION — PR verifies ~5.10% slower (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)
preset=min work=/tmp/recursion_cycles_run sysroot=/home/app/.lambda-vm-sysroot
==> Building MEASURE_CLI (cli, release) from 3ea4f9165f ...
==> [baseline] Adding worktree /tmp/recursion_cycles_run/wt_3ea4f916 @ 3ea4f916
Preparing worktree (detached HEAD 3ea4f916)
==> [baseline] make compile-recursion-elfs @ 3ea4f916 (this can take 10-20 min the first time) ...
==> [baseline] guest ELF: recursion-min.elf
==> [baseline] dumping recursion input blob (cargo test test_dump_recursion_input) ...
==> [baseline] blob: 284904 bytes -> /tmp/recursion_cycles_run/blob_3ea4f916_min.bin
==> [baseline] measuring: /tmp/recursion_cycles_run/measure_cli execute recursion-min.elf --private-input <blob> --cycles
==> [baseline] cycles=41715803 keccak=3025 (execute wall-time 1s)
==> [PR] Adding worktree /tmp/recursion_cycles_run/wt_bd80ef42 @ bd80ef42
Preparing worktree (detached HEAD bd80ef42)
==> [PR] make compile-recursion-elfs @ bd80ef42 (this can take 10-20 min the first time) ...
==> [PR] guest ELF: recursion-min.elf
==> [PR] dumping recursion input blob (cargo test test_dump_recursion_input) ...
==> [PR] blob: 296416 bytes -> /tmp/recursion_cycles_run/blob_bd80ef42_min.bin
==> [PR] measuring: /tmp/recursion_cycles_run/measure_cli execute recursion-min.elf --private-input <blob> --cycles
ERROR: [PR] MEASURE_CLI execute failed for bd80ef4255ef1f249f05d627fc03ede2a9d620d0 (bd80ef42). Tail of stderr:
Reading private input file...
Execution failed: ExecutionError(UnknownSyscall(18446744073709551596))
|
/ai-review |
Codex Code Review
|
![claude[bot]](https://avatars.githubusercontent.com/in/1236702?s=60&v=4){kind=small}
Review: FEXT accelerator (
|
There was a problem hiding this comment.
⚠️ 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.
Adds the FEXT precompile (a·b + c over native Fp3) end to end: three ecalls plus a field-storage address space in the executor, four prover chips sharing a (domain, addr) sorted-keys uniqueness argument, a cross-epoch carry (FEXT_L2G + GlobalFieldMemory + GLOBAL_FIELD_MEMORY), and the guest verifier's Fp3 multiplies routed through it. Chip-level design holds up; two items block merge: continuation epochs keep both field-storage bookends live, which is forgeable, and the always-on cost hits every proof while the offsetting win is unmeasured.
prover/src/lib.rs:539 (also air_refs :617, via build_epoch_airs continuation.rs:698) — FEXT_PAGE is a fixed table, so it stays in the AIR set for continuation epochs, which also carry FEXT_LOCAL_TO_GLOBAL; RAM avoids this by dropping PAGE (page_configs = &[]), FEXT_PAGE has no equivalent. Both bookend the Memory bus with identical token shape, FextPageConstraints::eval emits only LAYOUT.emit_constraints (leaving FINAL_TS_0/1 and FINAL_VAL, fext_page.rs cols 3–5, unconstrained), and uniqueness is per-table. So for a cell carried in with value V, one forged FEXT_PAGE row DOMAIN=d, ADDR=a, MU=1, FINAL_TS=0, FINAL_VAL=V cancels FEXT_L2G's carried-init token exactly and substitutes its own init token (value hard-coded 0): the epoch's first access reads 0 instead of V, while FEXT_L2G's GlobalFieldMemory tokens still carry init_val = V, so cross-epoch aggregation still balances. The row passes the sorted-keys argument (one active row ⇒ sel_same = 0, no LT send; padding domain 3 satisfies the ungated domain check), and nothing pins the trace length — verify_epoch's expected_proof_count counts sub-proofs, not rows. Fix as PAGE is: an include_fext_page flag on VmAirs (mirroring include_halt), dropped from air_trace_pairs/air_refs and from fixed_tables in verify_epoch; a splice test would pin it.
prover/src/lib.rs:87 — FIXED_TABLE_COUNT 10 → 14 and VmAirs::new builds all four FEXT chips unconditionally, so every proof carries four extra sub-proofs; FEXT_FMA is 50 main columns with 41 bus interactions (effective width ~173, wider than MEMW), so its OOD block and per-query deep-composition work stay wide even at the 4-row padding floor. Branch bench: +5.10% verify time (95% CI +4.70..+5.51, Wilcoxon p=1.9e-06), +0.60% proof size. The offsetting recursion-cycle comparison never ran: the measuring CLI was built from main and rejected the PR guest ELF with UnknownSyscall(u64::MAX-19). That ~5% also lands inside the guest verifier, eating the Fp3 savings on the target path. Re-run with a CLI built from the PR and publish the guest-cycle delta at blowup 2/4, ~219/110 queries; if the net is negative for non-FEXT programs, gate the FEXT tables on the ELF referencing the syscalls, or fold LOAD/STORE/PAGE into fewer chips.
prover/src/continuation.rs:1021 — prove_global unconditionally builds bitwise::generate_bitwise_trace() (2^20 rows × 21 cols, serial), an LT table, the GLOBAL_FIELD_MEMORY anchor and one FEXT_L2G table per epoch, and verify_global mirrors it. Nothing is gated on anchor_cells being non-empty, so every continuation proof — including programs that never issue a FEXT ecall — pays a 2^20-domain LDE, Merkle tree, constraint eval and FRI in the global proof, which is what a recursion layer verifies. prove_global hard-codes StorageMode::Ram, so this peak can't spill and isn't modeled by auto_storage. Only the anchor consumes those BITWISE/LT lookups; skipping anchor + BITWISE + LT (and the per-epoch FEXT_L2G tables) when no field cell was touched fails closed, since genesis receives on GlobalFieldMemory would have no partner and the bus can't balance.
prover/src/tests/prove_elfs_tests.rs:491 — the doc comment's causal chain does not hold. Permuting a provider table's rows changes only the committed root, hence the derived LogUp challenges; AIR constraints and bus balance are permutation-invariant, and an honest trace passes the composition check for all but a negligible fraction of Fp3 challenge sets. A CI-observable FEXT_PAGE failure as challenges move therefore points at FEXT_PAGE or the sorted-keys aux trace; sorting only froze one passing challenge set for test_fext, and any content change (different guest, added column, rebase) redraws them. Confirm by proving+verifying test_fext under several transcript seeds, or with LT rows permuted into another valid order. Keep the sorting for determinism, but make the multi-seed run the regression guard and reword the comment.
prover/src/tables/trace_builder.rs:4299 — lt_count += 3 * fext_load_count + 12 * fext_fma_count + 3 * fext_store_count + fext_page_count; under-counts LOAD and STORE by half: fext_load::bus_interactions sends 3 coeff_lt_p plus 3 old_ts < ts, and collect_lt_from_fext_load pushes 6/op; fext_store is the same shape, also 6/op. Those values are nearly all distinct in a real workload, so LT dedup doesn't absorb the gap — the recursion guest (3 LOADs + 1 FMA + 1 STORE per fma) is ~36 actual vs ~24 predicted. lt_padded_rows feeds auto_storage::table_specs, so the spill decision under-estimates peak RAM on the FEXT-heavy workload this targets, and the comment claiming an upper bound "as the drift test requires" is wrong. Use 6 * for both; fix that comment and the stale doc at trace_builder.rs:1800 (collect_lt_from_fext_store says "3 field reads" but also pushes coeff < p). count_table_lengths_matches_fext_traces cannot fail today — fext_bench is 3 LOADs / 4096 FMAs / 0 STOREs; extend it to a program with FEXT_STOREs so the >= assertion binds.
prover/src/tests/constraint_program_tests.rs:181 — the four new table AIRs are missing from all_table_programs_match_folders and from the device twin (constraint_program_device_tests.rs:183); both lists still end at ECDAS. That test asserts no captured constraint root sits at the never-captured sentinel and diffs the captured IR against the compiled folders over 200 random frames. ood_window_ir_tests.rs was extended and its module doc says the list mirrors this one, so the enumerations have silently drifted — which matters because assert_ood_window_matches_ir derives FEXT_PAGE's next-row read set from air.constraint_program(), making the IR capture the unvalidated oracle for a soundness-critical declaration. Add check_air/check_air_device for FEXT_LOAD/FEXT_FMA/FEXT_STORE/FEXT_PAGE, plus global_field_memory_air and fext_l2g_memory_air.
prover/src/tests/prove_elfs_tests.rs:501 — test_prover_deterministic_fext uses fixture test_fext, whose asm is only li and ecall. Per the collection filters at trace_builder.rs:3272-3327 that yields zero BRANCH, MUL, DVRM, EQ and BYTEWISE ops, so five of the six canonical sorts added here are unobservable — only lt.rs is exercised, and deleting the sort from mul.rs/dvrm.rs/eq.rs/bytewise.rs/branch.rs fails nothing. Use a fixture populating all six (e.g. all_instructions_64) or add a second prove_core_hash loop over one, and assert those traces exceed the 4-row padding floor.
prover/src/continuation.rs:1636 — the cross-epoch FEXT_L2G binding (per-epoch root check at :927, plus verify_fext_l2g_commitment_binding_view with fext_offset) has only the positive fext_works_under_continuation; the RAM twin it mirrors has four negatives, including the only test reaching the helper's reject branch. fext_l2g_global_air is EmptyConstraints and inherits all checks from equal roots, so the binding is load-bearing: add a tampered-fext_l2g_root test and a cross-run splice test with a FEXT-issuing fixture, plus the archived-bundle variant (existing blob tests use programs issuing no FEXT ecalls).
Nits:
- prover/src/lib.rs:1014 —
verify_fext_l2g_commitment_binding_viewisverify_l2g_commitment_binding_view(:999) plus an offset; add the parameter to the existing function instead of keeping two copies. - prover/src/tables/fext_local_to_global.rs:163 and :215 —
epoch_halfwordsandwordare character-for-character copies of thelocal_to_globalversions (:254, :299); make thosepub(crate)and reuse them, since the two epoch-label encodings must agree bit-for-bit for theIsB20ordering check.
3 participants
Motivation
Recursion — the STARK verifier running as an in-VM guest — spends most of its
arithmetic in the VM's native degree-3 Goldilocks extension field
Fp3 = Fp[x]/(x³ − 2)(DEEP composition, FRI folding, constraint evaluation). Asplain RISC-V, one
Fp3multiply-add expands to a dozen-plus fieldmul/adds plusthe surrounding load/store traffic, all charged to the CPU,
MEMWandLTtables.This PR adds the FEXT precompile (spec PR #809,
spec/fext):a·b + coverFp3in a single ecall, backed by a small degree-2 AIR — the
Fp3analog of the existingKECCAK/ECSM accelerators