Add opt-in CUDA acceleration for Aiur proofs - #597
Merged
Merged
Conversation
arthurpaulino
force-pushed
the
ap/gpu
branch
11 times, most recently
from
August 27, 2026 18:07
135cd84 to
7ce551a
Compare
Member
Author
|
!benchmark |
Contributor
|
| 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 |
8.908 s | 9.001 s | +1.0% | 30.577 s | 44.594 s | +45.8% (1.46× slower) |
90.750 | 62.230 | -31.4% (1.46× slower) |
70.72 GiB | 70.79 GiB | +0.1% | 11.33 MiB | 11.33 MiB | +0.0% | 77.6 ms | 77.2 ms | -0.5% | 134.35B | 134.35B | +0.0% |
Char.ofOrdinal_le_of_le |
6.883 s | 6.915 s | +0.5% | 26.298 s | 38.839 s | +47.7% (1.48× slower) |
105.070 | 71.140 | -32.3% (1.48× slower) |
63.76 GiB | 63.78 GiB | +0.0% | 11.33 MiB | 11.33 MiB | +0.0% | 73.7 ms | 76.9 ms | +4.4% |
102.60B | 102.60B | +0.0% |
Array.extract_append |
6.599 s | 6.687 s | +1.3% | 23.333 s | 33.603 s | +44.0% (1.44× slower) |
68.830 | 47.790 | -30.6% (1.44× slower) |
51.98 GiB | 51.99 GiB | +0.0% | 11.24 MiB | 11.24 MiB | +0.0% | 73.7 ms | 84.8 ms | +15.1% (1.15× slower) |
97.08B | 97.08B | +0.0% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
3.559 s | 3.799 s | +6.7% (1.07× slower) |
14.599 s | 20.975 s | +43.7% (1.44× slower) |
127.890 | 89.010 | -30.4% (1.44× slower) |
33.94 GiB | 33.98 GiB | +0.1% | 11.26 MiB | 11.26 MiB | +0.0% | 77.5 ms | 79.6 ms | +2.7% | 55.68B | 55.68B | +0.0% |
Std.HashMap |
4.127 s | 4.255 s | +3.1% |
15.985 s | 22.940 s | +43.5% (1.44× slower) |
127.750 | 89.020 | -30.3% (1.44× slower) |
36.31 GiB | 36.32 GiB | +0.0% | 11.26 MiB | 11.26 MiB | +0.0% | 77.9 ms | 83.3 ms | +6.9% (1.07× slower) |
61.88B | 61.88B | +0.0% |
String.append |
426.3 ms | 720.8 ms | +69.1% (1.69× slower) |
2.241 s | 2.915 s | +30.1% (1.30× slower) |
145.920 | 112.180 | -23.1% (1.30× slower) |
4.90 GiB | 5.65 GiB | +15.1% (1.15× larger) |
9.94 MiB | 9.94 MiB | +0.0% | 64.2 ms | 73.4 ms | +14.4% (1.14× slower) |
3.37B | 3.37B | +0.0% |
Nat.add_comm |
265.6 ms | 506.9 ms | +90.8% (1.91× slower) |
1.122 s | 1.333 s | +18.9% (1.19× slower) |
41.010 | 34.500 | -15.9% (1.19× slower) |
4.45 GiB | 4.85 GiB | +9.0% (1.09× larger) |
9.09 MiB | 9.09 MiB | +0.0% | 53.6 ms | 60.4 ms | +12.6% (1.13× slower) |
308.40M | 308.40M | +0.0% |
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 |
5.541 s | 7.111 s | +28.3% (1.28× slower) |
32.084 s | 54.819 s | +70.9% (1.71× slower) |
86.490 | 50.620 | -41.5% (1.71× slower) |
100.63 GiB | 101.25 GiB | +0.6% | 3.97 MiB | 3.97 MiB | +0.0% | 29.8 ms | 46.1 ms | +54.6% (1.55× slower) |
210.23B | 210.23B | -0.0% |
Char.ofOrdinal_le_of_le |
5.497 s | 7.038 s | +28.0% (1.28× slower) |
31.798 s | 53.868 s | +69.4% (1.69× slower) |
86.890 | 51.290 | -41.0% (1.69× slower) |
98.96 GiB | 99.72 GiB | +0.8% | 3.97 MiB | 3.97 MiB | +0.0% | 25.0 ms | 40.7 ms | +62.7% (1.63× slower) |
207.18B | 207.18B | -0.0% |
Array.extract_append |
5.242 s | 6.755 s | +28.9% (1.29× slower) |
30.457 s | 51.611 s | +69.5% (1.69× slower) |
52.730 | 31.120 | -41.0% (1.69× slower) |
94.37 GiB | 94.54 GiB | +0.2% | 3.97 MiB | 3.97 MiB | +0.0% | 24.8 ms | 62.0 ms | +149.7% (2.50× slower) |
200.65B | 200.65B | -0.0% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
5.451 s | 6.955 s | +27.6% (1.28× slower) |
31.693 s | 53.894 s | +70.1% (1.70× slower) |
58.910 | 34.640 | -41.2% (1.70× slower) |
98.45 GiB | 99.09 GiB | +0.6% | 3.97 MiB | 3.97 MiB | +0.0% | 24.9 ms | 41.7 ms | +67.4% (1.67× slower) |
205.59B | 205.59B | -0.0% |
Std.HashMap |
5.219 s | 6.731 s | +29.0% (1.29× slower) |
30.453 s | 51.607 s | +69.5% (1.69× slower) |
67.050 | 39.570 | -41.0% (1.69× slower) |
94.26 GiB | 95.19 GiB | +1.0% | 3.97 MiB | 3.97 MiB | +0.0% | 24.9 ms | 43.3 ms | +73.8% (1.74× slower) |
203.35B | 203.35B | -0.0% |
String.append |
4.394 s | 5.546 s | +26.2% (1.26× slower) |
28.005 s | 47.868 s | +70.9% (1.71× slower) |
11.680 | 6.830 | -41.5% (1.71× slower) |
87.83 GiB | 87.87 GiB | +0.0% | 3.97 MiB | 3.97 MiB | +0.0% | 24.6 ms | 32.5 ms | +31.8% (1.32× slower) |
168.67B | 168.67B | -0.0% |
Nat.add_comm |
3.566 s | 4.562 s | +27.9% (1.28× slower) |
18.916 s | 31.621 s | +67.2% (1.67× slower) |
2.430 | 1.450 | -40.3% (1.68× slower) |
58.63 GiB | 58.66 GiB | +0.1% | 3.97 MiB | 3.97 MiB | +0.0% | 24.6 ms | 28.3 ms | +15.1% (1.15× slower) |
130.84B | 130.84B | -0.0% |
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 |
1m 2.7s | 1m 39.4s | +58.7% (1.59× slower) |
44.290 | 27.910 | -37.0% (1.59× slower) |
100.63 GiB | 101.25 GiB | +0.6% |
Char.ofOrdinal_le_of_le |
58.096 s | 1m 32.7s | +59.6% (1.60× slower) |
47.560 | 29.800 | -37.3% (1.60× slower) |
98.96 GiB | 99.72 GiB | +0.8% |
Array.extract_append |
53.790 s | 1m 25.2s | +58.4% (1.58× slower) |
29.860 | 18.850 | -36.9% (1.58× slower) |
94.37 GiB | 94.54 GiB | +0.2% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
46.292 s | 1m 14.9s | +61.7% (1.62× slower) |
40.330 | 24.940 | -38.2% (1.62× slower) |
98.45 GiB | 99.09 GiB | +0.6% |
Std.HashMap |
46.438 s | 1m 14.5s | +60.5% (1.61× slower) |
43.970 | 27.390 | -37.7% (1.61× slower) |
94.26 GiB | 95.19 GiB | +1.0% |
String.append |
30.246 s | 50.783 s | +67.9% (1.68× slower) |
10.810 | 6.440 | -40.4% (1.68× slower) |
87.83 GiB | 87.87 GiB | +0.0% |
Nat.add_comm |
20.037 s | 32.955 s | +64.5% (1.64× slower) |
2.300 | 1.400 | -39.1% (1.64× slower) |
58.63 GiB | 58.66 GiB | +0.1% |
Member
Author
|
!benchmark fresh |
Contributor
|
| 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 |
8.796 s | 8.767 s | -0.3% | 29.920 s | 29.907 s | -0.0% | 92.750 | 92.790 | +0.0% | 70.74 GiB | 70.72 GiB | -0.0% | 11.33 MiB | 11.33 MiB | +0.0% | 68.9 ms | 68.3 ms | -0.9% | 134.35B | 134.35B | +0.0% |
Char.ofOrdinal_le_of_le |
6.825 s | 6.767 s | -0.8% | 25.871 s | 25.705 s | -0.6% | 106.800 | 107.490 | +0.6% | 63.88 GiB | 63.89 GiB | +0.0% | 11.33 MiB | 11.33 MiB | +0.0% | 78.1 ms | 68.1 ms | -12.8% (1.15× faster) 🟢 | 102.60B | 102.60B | +0.0% |
Array.extract_append |
6.479 s | 6.431 s | -0.7% | 22.829 s | 22.685 s | -0.6% | 70.350 | 70.800 | +0.6% | 52.01 GiB | 51.99 GiB | -0.0% | 11.24 MiB | 11.24 MiB | +0.0% | 69.9 ms | 70.4 ms | +0.7% | 97.08B | 97.08B | +0.0% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
3.557 s | 3.481 s | -2.1% | 14.321 s | 14.252 s | -0.5% | 130.370 | 131 | +0.5% | 33.95 GiB | 33.96 GiB | +0.0% | 11.26 MiB | 11.26 MiB | +0.0% | 69.8 ms | 70.0 ms | +0.3% | 55.68B | 55.68B | +0.0% |
Std.HashMap |
3.987 s | 4.023 s | +0.9% | 15.554 s | 15.492 s | -0.4% | 131.290 | 131.810 | +0.4% | 36.33 GiB | 36.30 GiB | -0.1% | 11.26 MiB | 11.26 MiB | +0.0% | 78.1 ms | 78.6 ms | +0.6% | 61.88B | 61.88B | +0.0% |
String.append |
421.0 ms | 430.3 ms | +2.2% | 2.290 s | 2.263 s | -1.2% | 142.770 | 144.510 | +1.2% | 5.55 GiB | 4.97 GiB | -10.4% (1.12× smaller) 🟢 | 9.94 MiB | 9.94 MiB | +0.0% | 62.7 ms | 62.8 ms | +0.0% | 3.37B | 3.37B | +0.0% |
Nat.add_comm |
262.2 ms | 263.1 ms | +0.3% | 1.072 s | 1.087 s | +1.5% | 42.920 | 42.300 | -1.4% | 3.98 GiB | 4.10 GiB | +3.1% |
9.09 MiB | 9.09 MiB | +0.0% | 53.9 ms | 53.1 ms | -1.5% | 308.40M | 308.40M | +0.0% |
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 |
5.532 s | 5.498 s | -0.6% | 31.312 s | 31.437 s | +0.4% | 88.620 | 88.270 | -0.4% | 100.45 GiB | 101.15 GiB | +0.7% | 3.97 MiB | 3.97 MiB | +0.0% | 29.8 ms | 26.3 ms | -11.8% (1.13× faster) 🟢 | 210.23B | 210.23B | -0.0% |
Char.ofOrdinal_le_of_le |
5.556 s | 5.504 s | -0.9% | 31.017 s | 30.949 s | -0.2% | 89.080 | 89.270 | +0.2% | 99.09 GiB | 99.87 GiB | +0.8% | 3.97 MiB | 3.97 MiB | +0.0% | 25.1 ms | 24.9 ms | -0.7% | 207.18B | 207.18B | -0.0% |
Array.extract_append |
5.264 s | 5.305 s | +0.8% | 29.680 s | 29.606 s | -0.2% | 54.110 | 54.250 | +0.3% | 94.33 GiB | 94.55 GiB | +0.2% | 3.97 MiB | 3.97 MiB | +0.0% | 24.5 ms | 25.7 ms | +4.6% |
200.65B | 200.65B | -0.0% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
5.395 s | 5.401 s | +0.1% | 30.974 s | 31.026 s | +0.2% | 60.280 | 60.180 | -0.2% | 98.60 GiB | 98.75 GiB | +0.2% | 3.97 MiB | 3.97 MiB | +0.0% | 27.8 ms | 28.0 ms | +0.8% | 205.59B | 205.59B | -0.0% |
Std.HashMap |
5.287 s | 5.324 s | +0.7% | 29.756 s | 29.706 s | -0.2% | 68.630 | 68.740 | +0.2% | 94.25 GiB | 94.98 GiB | +0.8% | 3.97 MiB | 3.97 MiB | +0.0% | 24.8 ms | 25.1 ms | +1.5% | 203.35B | 203.35B | -0.0% |
String.append |
4.372 s | 4.313 s | -1.4% | 27.325 s | 27.302 s | -0.1% | 11.970 | 11.980 | +0.1% | 87.79 GiB | 87.84 GiB | +0.1% | 3.97 MiB | 3.97 MiB | +0.0% | 24.7 ms | 32.2 ms | +30.6% (1.31× slower) |
168.67B | 168.67B | -0.0% |
Nat.add_comm |
3.561 s | 3.547 s | -0.4% | 18.470 s | 18.417 s | -0.3% | 2.490 | 2.500 | +0.4% | 58.68 GiB | 58.65 GiB | -0.1% | 3.97 MiB | 3.97 MiB | +0.0% | 24.4 ms | 24.6 ms | +0.9% | 130.84B | 130.84B | -0.0% |
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 |
1m 1.2s | 1m 1.3s | +0.2% | 45.320 | 45.240 | -0.2% | 100.45 GiB | 101.15 GiB | +0.7% |
Char.ofOrdinal_le_of_le |
56.888 s | 56.655 s | -0.4% | 48.570 | 48.770 | +0.4% | 99.09 GiB | 99.87 GiB | +0.8% |
Array.extract_append |
52.509 s | 52.291 s | -0.4% | 30.590 | 30.710 | +0.4% | 94.33 GiB | 94.55 GiB | +0.2% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
45.295 s | 45.278 s | -0.0% | 41.220 | 41.230 | +0.0% | 98.60 GiB | 98.75 GiB | +0.2% |
Std.HashMap |
45.309 s | 45.198 s | -0.2% | 45.070 | 45.180 | +0.2% | 94.25 GiB | 94.98 GiB | +0.8% |
String.append |
29.615 s | 29.565 s | -0.2% | 11.040 | 11.060 | +0.2% | 87.79 GiB | 87.84 GiB | +0.1% |
Nat.add_comm |
19.542 s | 19.504 s | -0.2% | 2.350 | 2.360 | +0.4% | 58.68 GiB | 58.65 GiB | -0.1% |
johnchandlerburnham
previously approved these changes
Aug 30, 2026
arthurpaulino
marked this pull request as ready for review
August 30, 2026 13:03
Expose multi-stark's first-party CUDA prover through Aiur and the Ix FFI while keeping ordinary Cargo, Lake, and Nix builds CPU-only and independent of the CUDA toolkit. Enable it explicitly with IX_CUDA=1, IX_CUDA=true, or IX_CUDA=yes for Lake commands, or with the cuda Cargo feature for Rust consumers. Forward the feature through aiur and ix-ffi and keep Cargo.lock synchronized with the selected multi-stark revision. Merge the multi-stark PR first, then replace the temporary topic-branch pin with the resulting main-branch revision before merging Ix; Ix must not ship with a long-lived topic-branch dependency. Make Lake feature selection part of the Rust archive dependency trace and snapshot feature-specific artifacts. Switching IX_CUDA now rebuilds and relinks lake exe bench-typecheck directly instead of silently retaining the backend from a previous build, and the selected Rust feature set is printed during the build. Contain prover panics, including CUDA initialization and runtime failures, at every Lean proving FFI boundary and return ordinary Except String errors instead of unwinding across the C ABI and aborting the Lean process. Update CLI, benchmarks, and tests for the explicit error path. Restore parallel, net, and test-ffi coverage in ordinary release clippy/check CI. Keep CUDA out of Nix's host-feature aggregation, include the Rust trace inputs required by Lake's prebuilt archive target, and add a toolkit-only CUDA job that compiles the Rust workspace and links a CUDA-enabled Lean benchmark executable without requiring a GPU. Move hardware-specific performance numbers out of the stable README and document the reproducible Vector.extract_append recursive workflow. On an RTX PRO 6000 Blackwell, Vector.extract_append recursive q50 reduces the post-execution-and-trace portion of inner and outer proving from 71.87s on CPU to 8.74s with CUDA (8.22x), with unchanged proof sizes and successful verification. End-to-end proving also includes Aiur execution and trace construction, which remain outside this comparison. Fifty queries is a development benchmark parameter, not a production security recommendation.
johnchandlerburnham
approved these changes
Aug 30, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Expose multi-stark's first-party CUDA prover through Aiur and the Ix FFI while keeping ordinary Cargo, Lake, and Nix builds CPU-only and independent of the CUDA toolkit. Enable it explicitly with IX_CUDA=1, IX_CUDA=true, or IX_CUDA=yes for Lake commands, or with the cuda Cargo feature for Rust consumers.
Forward the feature through aiur and ix-ffi and keep Cargo.lock synchronized with the selected multi-stark revision. Merge the multi-stark PR first, then replace the temporary topic-branch pin with the resulting main-branch revision before merging Ix; Ix must not ship with a long-lived topic-branch dependency.
Make Lake feature selection part of the Rust archive dependency trace and snapshot feature-specific artifacts. Switching IX_CUDA now rebuilds and relinks lake exe bench-typecheck directly instead of silently retaining the backend from a previous build, and the selected Rust feature set is printed during the build.
Contain prover panics, including CUDA initialization and runtime failures, at every Lean proving FFI boundary and return ordinary Except String errors instead of unwinding across the C ABI and aborting the Lean process. Update CLI, benchmarks, and tests for the explicit error path.
Restore parallel, net, and test-ffi coverage in ordinary release clippy/check CI. Keep CUDA out of Nix's host-feature aggregation, include the Rust trace inputs required by Lake's prebuilt archive target, and add a toolkit-only CUDA job that compiles the Rust workspace and links a CUDA-enabled Lean benchmark executable without requiring a GPU. Move hardware-specific performance numbers out of the stable README and document the reproducible Vector.extract_append recursive workflow.
On an RTX PRO 6000 Blackwell, Vector.extract_append recursive q50 reduces the post-execution-and-trace portion of inner and outer proving from 71.87s on CPU to 8.74s with CUDA (8.22x), with unchanged proof sizes and successful verification. End-to-end proving also includes Aiur execution and trace construction, which remain outside this comparison. Fifty queries is a development benchmark parameter, not a production security recommendation.