Skip to content

perf(aiur): reduce witness memory and proving FFT costs - #635

Open
arthurpaulino wants to merge 7 commits into
mainfrom
ap/perf
Open

perf(aiur): reduce witness memory and proving FFT costs#635
arthurpaulino wants to merge 7 commits into
mainfrom
ap/perf

Conversation

@arthurpaulino

@arthurpaulino arthurpaulino commented Sep 16, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

Reduce Aiur's witness memory and modeled proving FFT work by extracting the independent optimizations from #631, on top of the correctness fixes merged in #634.

This PR contains six Aiur optimizations and a measured FFT-pin refresh, in seven atomic commits:

  • Cache claim shapes. Summarize function return arities during system construction and reuse them for call validation and public claim checks, preserving the existing acceptance semantics.
  • Tune lookup grouping. Choose accumulator groups using compiled expression degrees and the commitment parameters. Require no increase in modeled FFT work at any integer trace height, including small traces, and keep the circuit metadata consistent with the chosen grouping.
  • Compact witness metadata and correct memory estimates. Store member metadata once and two indices per active row. Account for grouped functions, extension-field storage, lookup writers, and witness metadata in prover-memory estimates.
  • Consolidate byte tables. Express byte AND/OR through XOR lookups and byte comparison through subtraction, sharing their existing table multiplicities.
  • Shrink u32 comparison witnesses. Replace twelve byte auxiliaries with six u16 limbs while retaining six range lookups and bounded inputs. Add the distinct scalar u16 range channel needed by these comparisons.
  • Remove the intermediate u32 comparison carry constraint. Express the result directly as the whole-word carry (b + c - a) / 2^32, with c = a.wrapping_sub(b). This replaces two boolean carry constraints with one, without allocating a carry column. Keep all six limb range checks and both input-recomposition constraints: they bound the equation so field wraparound cannot admit a false comparison.

Cycle defenses and their associated ranks, completion timestamps, component analysis, and unit counters are excluded. No IxVM program optimizations are ported, including the BLAKE3 reader change labeled perf(aiur) in #631. Packed query storage is also excluded: its encoding and decoding costs trade execution speed for memory without lowering FFT costs. The generated Rust executors are updated for Aiur's comparison layout; Ix/IxVM source is unchanged.

All 83 kernel FFT pins were measured again after rebasing onto Ixon v3 (519d2c49) and decrease by 6.6–16.3% relative to that main baseline. These are modeled FFT costs, not wall-clock speedups. The whole-word carry-constraint removal leaves the FFT costs unchanged; it removes one polynomial constraint per comparison, with no runtime improvement measured yet. The measured pin refresh is the final commit.

Case Before After Reduction
Nat.add_comm 322,598,714 286,989,161 11.0%
Shard pipeline 7,072,190,269 6,434,780,974 9.0%

Validation passes:

  • All 52 active Aiur Rust tests, including exhaustive byte/u16 lookup checks, supplied-trace rejection tests for each comparison limb bound and field wraparound, verifying-key roundtrips, and grouped-witness tests.
  • Lean suites: aiur-cross, aiur-cost, aiur-prove, aiur-hashes, rbtree-map, multi-stark, recursive-verifier, and ix-aggr. Recursive verification explicitly exercises quotient degrees two and four in one proof.
  • Full ixvm suite: 843 passing assertions, including refreshed pins, adversarial fixtures, and all 249 interpreter/generated-executor parity assertions.
  • All three generated executors pass lake exe ix codegen --check.
  • cargo fmt --all -- --check and strict workspace Clippy:
cargo clippy --locked --release --workspace --all-targets \
  --features ix-ffi/parallel,ix-ffi/net,ix-ffi/test-ffi -- -D warnings

@argumentcomputer argumentcomputer deleted a comment from argument-ci-bot Bot Sep 16, 2026
@argumentcomputer argumentcomputer deleted a comment from argument-ci-bot Bot Sep 16, 2026
@arthurpaulino

arthurpaulino commented Sep 16, 2026

Copy link
Copy Markdown
Member Author

!benchmark fresh

@argument-ci-bot

argument-ci-bot Bot commented Sep 16, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

!benchmark — main vs 3d4dcae

backends: aiur=prove · envs: InitStd · baseline: fresh (benchmark products rebuilt, base-SHA run, bencher bypassed)

aiur · InitStd · prove — main from: base run @ cf77c95 (fresh — bencher bypassed)

7 constants · 4 with regressions · 7 with improvements (|Δ| > 3.0% on any metric).

IxVM on FRI (7 constants)
constant execute-time (main) execute-time (PR) Δ% prove-time (main) prove-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ% proof-size (main) proof-size (PR) Δ% verify-time (main) verify-time (PR) Δ% fft-cost (main) fft-cost (PR) Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append 9.173 s 8.838 s -3.6% 🟢 37.501 s 35.382 s -5.7% (1.06× faster) 🟢 74 78.430 +6.0% (1.06× faster) 🟢 72.67 GiB 68.87 GiB -5.2% (1.06× smaller) 🟢 5.20 MiB 4.95 MiB -4.9% (1.05× smaller) 🟢 31.5 ms 28.4 ms -10.0% (1.11× faster) 🟢 133.40B 125.32B -6.1% (1.06× fewer) 🟢
Char.ofOrdinal_le_of_le 6.491 s 6.312 s -2.8% 31.089 s 28.156 s -9.4% (1.10× faster) 🟢 88.870 98.130 +10.4% (1.10× faster) 🟢 62.91 GiB 59.40 GiB -5.6% (1.06× smaller) 🟢 5.20 MiB 4.94 MiB -5.0% (1.05× smaller) 🟢 32.0 ms 29.3 ms -8.6% (1.09× faster) 🟢 95.82B 89.69B -6.4% (1.07× fewer) 🟢
Array.extract_append 6.040 s 6.376 s +5.6% (1.06× slower) ⚠️ 25.874 s 26.390 s +2.0% 62.070 60.860 -1.9% 53.31 GiB 51.40 GiB -3.6% 🟢 5.06 MiB 4.80 MiB -5.1% (1.05× smaller) 🟢 30.4 ms 28.6 ms -5.9% (1.06× faster) 🟢 95.44B 91.58B -4.0% 🟢
Std.HashMap 4.052 s 3.924 s -3.2% 🟢 18.647 s 17.359 s -6.9% (1.07× faster) 🟢 109.510 117.630 +7.4% (1.07× faster) 🟢 36.57 GiB 34.64 GiB -5.3% (1.06× smaller) 🟢 5.13 MiB 4.85 MiB -5.4% (1.06× smaller) 🟢 31.8 ms 27.8 ms -12.8% (1.15× faster) 🟢 61.21B 57.21B -6.5% (1.07× fewer) 🟢
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq 3.637 s 3.517 s -3.3% 🟢 16.694 s 15.819 s -5.2% (1.06× faster) 🟢 111.840 118.020 +5.5% (1.06× faster) 🟢 35.21 GiB 33.32 GiB -5.4% (1.06× smaller) 🟢 5.09 MiB 4.83 MiB -5.3% (1.06× smaller) 🟢 29.3 ms 28.7 ms -2.1% 55.75B 52.26B -6.3% (1.07× fewer) 🟢
String.append 425.5 ms 436.1 ms +2.5% 1.759 s 1.769 s +0.5% 185.870 184.860 -0.5% 4.87 GiB 6.03 GiB +23.6% (1.24× larger) ⚠️ 4.84 MiB 4.59 MiB -5.3% (1.06× smaller) 🟢 26.8 ms 25.7 ms -4.0% 🟢 3.46B 3.20B -7.6% (1.08× fewer) 🟢
Nat.add_comm 259.3 ms 263.8 ms +1.7% 738.1 ms 740.1 ms +0.3% 62.330 62.150 -0.3% 4.07 GiB 4.40 GiB +8.2% (1.08× larger) ⚠️ 4.65 MiB 4.41 MiB -5.2% (1.06× smaller) 🟢 25.6 ms 25.8 ms +0.8% 321.01M 285.49M -11.1% (1.12× fewer) 🟢
FRI verifier on FRI (7 constants)
constant execute-time (main) execute-time (PR) Δ% prove-time (main) prove-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ% proof-size (main) proof-size (PR) Δ% verify-time (main) verify-time (PR) Δ% fft-cost (main) fft-cost (PR) Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append 2.572 s 2.420 s -5.9% (1.06× faster) 🟢 22.441 s 19.965 s -11.0% (1.12× faster) 🟢 123.660 138.990 +12.4% (1.12× faster) 🟢 56.67 GiB 50.75 GiB -10.4% (1.12× smaller) 🟢 2.21 MiB 2.00 MiB -9.6% (1.11× smaller) 🟢 13.2 ms 19.1 ms +44.9% (1.45× slower) ⚠️ 111.05B 91.16B -17.9% (1.22× fewer) 🟢
Char.ofOrdinal_le_of_le 2.696 s 2.408 s -10.7% (1.12× faster) 🟢 23.856 s 19.709 s -17.4% (1.21× faster) 🟢 115.820 140.190 +21.0% (1.21× faster) 🟢 56.54 GiB 51.02 GiB -9.8% (1.11× smaller) 🟢 2.20 MiB 2.01 MiB -8.6% (1.09× smaller) 🟢 14.2 ms 12.0 ms -15.5% (1.18× faster) 🟢 110.96B 90.44B -18.5% (1.23× fewer) 🟢
Array.extract_append 2.480 s 2.355 s -5.0% (1.05× faster) 🟢 22.177 s 19.260 s -13.2% (1.15× faster) 🟢 72.420 83.390 +15.1% (1.15× faster) 🟢 55.21 GiB 48.32 GiB -12.5% (1.14× smaller) 🟢 2.21 MiB 2.02 MiB -8.7% (1.10× smaller) 🟢 12.9 ms 12.0 ms -7.4% (1.08× faster) 🟢 107.38B 87.27B -18.7% (1.23× fewer) 🟢
Std.HashMap 2.583 s 2.374 s -8.1% (1.09× faster) 🟢 23.222 s 20.036 s -13.7% (1.16× faster) 🟢 87.930 101.920 +15.9% (1.16× faster) 🟢 55.93 GiB 48.71 GiB -12.9% (1.15× smaller) 🟢 2.21 MiB 2.00 MiB -9.2% (1.10× smaller) 🟢 13.8 ms 12.0 ms -13.2% (1.15× faster) 🟢 109.21B 88.35B -19.1% (1.24× fewer) 🟢
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq 2.483 s 2.371 s -4.5% 🟢 21.907 s 19.238 s -12.2% (1.14× faster) 🟢 85.220 97.050 +13.9% (1.14× faster) 🟢 55.16 GiB 48.85 GiB -11.4% (1.13× smaller) 🟢 2.21 MiB 2.02 MiB -8.7% (1.10× smaller) 🟢 12.6 ms 11.7 ms -7.0% (1.08× faster) 🟢 108.09B 87.57B -19.0% (1.23× fewer) 🟢
String.append 2.197 s 2.205 s +0.4% 19.438 s 18.807 s -3.2% 🟢 16.820 17.390 +3.4% 🟢 51.35 GiB 45.33 GiB -11.7% (1.13× smaller) 🟢 2.21 MiB 2.01 MiB -9.0% (1.10× smaller) 🟢 12.6 ms 12.8 ms +1.2% 98.51B 80.87B -17.9% (1.22× fewer) 🟢
Nat.add_comm 2.169 s 2.082 s -4.0% 🟢 19.386 s 18.453 s -4.8% (1.05× faster) 🟢 2.370 2.490 +5.1% (1.05× faster) 🟢 50.71 GiB 44.47 GiB -12.3% (1.14× smaller) 🟢 2.20 MiB 2.01 MiB -8.7% (1.10× smaller) 🟢 13.4 ms 12.2 ms -8.8% (1.10× faster) 🟢 93.37B 75.50B -19.1% (1.24× fewer) 🟢
Aggregate flat join (7 constants)
constant execute-time (main) execute-time (PR) Δ% prove-time (main) prove-time (PR) Δ% peak-ram (main) peak-ram (PR) Δ% proof-size (main) proof-size (PR) Δ% verify-time (main) verify-time (PR) Δ% fft-cost (main) fft-cost (PR) Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a
Char.ofOrdinal_le_of_le n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a
Array.extract_append n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a
Std.HashMap n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a
String.append n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a
Nat.add_comm n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a
Pipeline total (7 constants)
constant total-time (main) total-time (PR) Δ% pipeline-throughput (const/s) (main) pipeline-throughput (const/s) (PR) Δ% pipeline-peak-ram (main) pipeline-peak-ram (PR) Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append 59.942 s 55.347 s -7.7% (1.08× faster) 🟢 46.300 50.140 +8.3% (1.08× faster) 🟢 72.67 GiB 68.87 GiB -5.2% (1.06× smaller) 🟢
Char.ofOrdinal_le_of_le 54.945 s 47.865 s -12.9% (1.15× faster) 🟢 50.290 57.720 +14.8% (1.15× faster) 🟢 62.91 GiB 59.40 GiB -5.6% (1.06× smaller) 🟢
Array.extract_append 48.051 s 45.650 s -5.0% (1.05× faster) 🟢 33.420 35.180 +5.3% (1.05× faster) 🟢 55.21 GiB 51.40 GiB -6.9% (1.07× smaller) 🟢
Std.HashMap 41.869 s 37.395 s -10.7% (1.12× faster) 🟢 48.770 54.610 +12.0% (1.12× faster) 🟢 55.93 GiB 48.71 GiB -12.9% (1.15× smaller) 🟢
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq 38.601 s 35.057 s -9.2% (1.10× faster) 🟢 48.370 53.260 +10.1% (1.10× faster) 🟢 55.16 GiB 48.85 GiB -11.4% (1.13× smaller) 🟢
String.append 21.198 s 20.576 s -2.9% 15.430 15.890 +3.0% 51.35 GiB 45.33 GiB -11.7% (1.13× smaller) 🟢
Nat.add_comm 20.124 s 19.193 s -4.6% 🟢 2.290 2.400 +4.8% 🟢 50.71 GiB 44.47 GiB -12.3% (1.14× smaller) 🟢

Workflow logs

arthurpaulino and others added 7 commits September 16, 2026 22:11
@arthurpaulino @johnchandlerburnham
perf(aiur): cache validated function claim shapes
e2d7daf 
Summarize constrained return arities once during system construction and
reuse them for call validation and public claim checks. Preserve existing
acceptance semantics, including empty and inconsistent return trees.

Extract claim caching from a8ee603 in PR #631 without callee-rank changes.
Differential tests compare cached arities with the recursive predicate on
nested branches and continuations. All 36 Aiur tests pass.

Co-authored-by: John C. Burnham <john@agathic.com>
@arthurpaulino @johnchandlerburnham
perf(aiur): tune lookup groups from compiled degree costs
f1534a8 
Retune accumulator grouping using actual expression degrees and the PCS
quotient budget. Require no greater modeled FFT work at every integer row
height, including one-row traces, and synchronize all circuit metadata
before exposing the system or its transcript.

Port c7a5a97 from PR #631 with rank-free fixtures. Cover degree budgets,
verifying-key roundtrips, false claims, and mixed quotient degrees in the
existing recursive-verifier suite. Preserve the corrected lookup gates.

Co-authored-by: John C. Burnham <john@agathic.com>
@arthurpaulino @johnchandlerburnham
perf(aiur): compact witness metadata and correct memory estimates
c00a791 
Store member metadata once and two indices per active row, allocating the
row index vector exactly once. Account for grouped member rows, actual
extension-field storage, lookup writers and compact function metadata in
prover-memory and shard estimates.

Extract the host-side changes from 470eaea in PR #631. Omit its IxVM byte
hint rewrite and all completion/rank machinery. Test reordered grouped
members, advice-only rows, fixed tables and split estimates, plus an
opt-in million-row witness construction measurement.

Co-authored-by: John C. Burnham <john@agathic.com>
@arthurpaulino @johnchandlerburnham
perf(aiur): consolidate byte lookup tables
1ea7a68 
Express byte AND/OR through affine XOR messages and byte comparison
through subtraction. Merge their multiplicities into the existing tables,
removing three fixed-table columns and lookup channels while preserving
operation outputs and function trace layouts. Keep old channel IDs reserved.

Extract 9c8a654 from PR #631 without rank-related witness/test changes.
Exhaustively check all byte pairs in singleton and grouped circuits, reject
forged outputs and nonbyte inputs, and roundtrip proofs and verifying keys.
All 56 active Aiur tests and strict Clippy pass.

Co-authored-by: John C. Burnham <john@agathic.com>
@arthurpaulino @johnchandlerburnham
perf(aiur): use u16 limbs for u32 comparisons
f29f77e 
Replace twelve byte auxiliaries with six u16 limbs while preserving six
range lookups, both input bounds, strict comparison and boolean carries.
Add a distinct scalar u16 range channel to the shared byte table, and
update compiler layouts, execution, witnesses and generated executors.

Port 09e9531 from PR #631 plus only the generic range-table support it
needs from e1d74d1. No call-rank encoding or cycle defense is introduced.
Tests exhaust the scalar table, cover grouped and singleton boundaries,
reject supplied invalid limbs and verify constrained advice promotion.

Co-authored-by: John C. Burnham <john@agathic.com>
@arthurpaulino
perf(aiur): remove the intermediate u32 comparison carry constraint
84b2396 
Use b + c = a + carry * 2^32 with c = a.wrapping_sub(b), returning the whole-word carry directly. Keep all six u16 range checks and both input recomposition constraints, and constrain the carry to be boolean once.

Update execution, witnesses, and generated executors together. Extend supplied-trace tests to cover each limb bound and Goldilocks wraparound.

Validated Aiur Rust tests, Lean integration suites, full IxVM tests, codegen checks, formatting, and strict workspace Clippy. All 83 kernel FFT pins and the shard pin are unchanged.
@arthurpaulino @johnchandlerburnham
test(aiur): refresh FFT pins for independent optimizations
eaf84e0 
Measure the Ixon v3 programs from main (519d2c4) against the independent
Aiur optimizations, then update all 83 kernel pins and the shard pin.
Keep the upstream fixtures and change only their measured costs.

Every measured cost decreases: kernel cases by 6.6-16.3%, Nat.add_comm
by 11.0%, and the shard pipeline by 9.0%. These measure modeled FFT work,
not wall time. The whole-word carry simplification does not reduce FFT
costs further.

The measurement run passes every non-cost assertion, including generated
executor parity checks. No IxVM optimization or cycle defense from #631
is included.

Co-authored-by: John C. Burnham <john@agathic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@arthurpaulino