recursion: populate the ix_aggr and verifier function groupings (192 … - #620
Merged
Merged
Conversation
…-> 39, 191 -> 72) Same cost-aware greedy merging as the kernel, over profiles of the `ix_aggr` join of two lifted shards and of the standalone verifier over two IxVM proofs (Nat.sub_le_of_le_add, Lean.Syntax.rec), within an average 2% (max 4%) modelled cost increase per workload. The standalone verifier gets the same groups restricted to its own functions. ix_aggr: 21 groups over 174 circuits, 192 -> 39 circuits; the join's measured FFT cost 1.475e11 -> 1.495e11 (+1.4%), proof 4.98 MB -> 2.42 MB, prove time unchanged (58.8s -> 58.4s), verify 28 ms -> 14 ms. Standalone verifier: 20 groups over 139 circuits, 191 -> 72 circuits; FFT +1.4% / +1.5% on the two proofs, outer proof 4.20 MB -> 2.31 MB, prove time unchanged (30.7s -> 30.6s), verify 25 ms -> 14 ms.
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.842 s | 9.115 s | +3.1% |
35.093 s | 36.049 s | +2.7% | 79.080 | 76.980 | -2.7% | 73.53 GiB | 73.50 GiB | -0.1% | 5.06 MiB | 5.06 MiB | +0.0% | 28.0 ms | 28.6 ms | +1.9% | 137.19B | 137.19B | +0.0% |
Char.ofOrdinal_le_of_le |
6.911 s | 6.906 s | -0.1% | 30.131 s | 30.015 s | -0.4% | 91.700 | 92.050 | +0.4% | 66.24 GiB | 66.20 GiB | -0.0% | 5.05 MiB | 5.05 MiB | +0.0% | 28.0 ms | 27.9 ms | -0.4% | 105.30B | 105.30B | +0.0% |
Array.extract_append |
6.427 s | 6.570 s | +2.2% | 25.971 s | 26.474 s | +1.9% | 61.840 | 60.660 | -1.9% | 53.78 GiB | 53.70 GiB | -0.1% | 4.92 MiB | 4.92 MiB | +0.0% | 29.0 ms | 30.3 ms | +4.6% |
99.03B | 99.03B | +0.0% |
Std.HashMap |
3.989 s | 4.045 s | +1.4% | 17.167 s | 17.017 s | -0.9% | 118.950 | 120 | +0.9% | 37.85 GiB | 37.61 GiB | -0.6% | 4.97 MiB | 4.97 MiB | +0.0% | 28.9 ms | 28.9 ms | +0.2% | 63.51B | 63.51B | +0.0% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
3.666 s | 3.649 s | -0.5% | 15.918 s | 15.797 s | -0.8% | 117.290 | 118.180 | +0.8% | 35.32 GiB | 35.49 GiB | +0.5% | 4.95 MiB | 4.95 MiB | +0.0% | 27.9 ms | 27.7 ms | -0.6% | 57.01B | 57.01B | +0.0% |
String.append |
424.7 ms | 426.9 ms | +0.5% | 1.731 s | 1.777 s | +2.7% | 188.940 | 184.050 | -2.6% | 5.39 GiB | 6.02 GiB | +11.8% (1.12× larger) |
4.70 MiB | 4.70 MiB | +0.0% | 26.6 ms | 26.5 ms | -0.4% | 3.51B | 3.51B | +0.0% |
Nat.add_comm |
263.2 ms | 264.6 ms | +0.5% | 725.6 ms | 731.4 ms | +0.8% | 63.390 | 62.890 | -0.8% | 4.29 GiB | 4.10 GiB | -4.6% 🟢 | 4.50 MiB | 4.50 MiB | +0.0% | 24.1 ms | 24.6 ms | +2.1% | 321.32M | 321.32M | +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 |
2.371 s | 2.457 s | +3.6% |
20.669 s | 20.921 s | +1.2% | 134.260 | 132.640 | -1.2% | 54.89 GiB | 56.13 GiB | +2.3% | 4.01 MiB | 2.21 MiB | -44.8% (1.81× smaller) 🟢 | 22.8 ms | 12.5 ms | -45.1% (1.82× faster) 🟢 | 107.18B | 108.59B | +1.3% |
Char.ofOrdinal_le_of_le |
2.390 s | 2.371 s | -0.8% | 20.766 s | 20.636 s | -0.6% | 133.050 | 133.890 | +0.6% | 54.99 GiB | 56.02 GiB | +1.9% | 4.01 MiB | 2.21 MiB | -44.7% (1.81× smaller) 🟢 | 22.1 ms | 20.1 ms | -8.9% (1.10× faster) 🟢 | 106.08B | 107.48B | +1.3% |
Array.extract_append |
2.299 s | 2.418 s | +5.2% (1.05× slower) |
19.800 s | 20.465 s | +3.4% |
81.110 | 78.480 | -3.2% |
52.13 GiB | 52.97 GiB | +1.6% | 4.01 MiB | 2.21 MiB | -44.8% (1.81× smaller) 🟢 | 22.8 ms | 12.5 ms | -45.0% (1.82× faster) 🟢 | 103.56B | 104.92B | +1.3% |
Std.HashMap |
2.369 s | 2.365 s | -0.2% | 20.456 s | 20.104 s | -1.7% | 99.820 | 101.570 | +1.8% | 53.59 GiB | 54.53 GiB | +1.7% | 4.00 MiB | 2.22 MiB | -44.6% (1.81× smaller) 🟢 | 22.6 ms | 12.4 ms | -45.2% (1.83× faster) 🟢 | 104.43B | 105.80B | +1.3% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
2.347 s | 2.383 s | +1.5% | 19.775 s | 19.719 s | -0.3% | 94.410 | 94.680 | +0.3% | 51.97 GiB | 52.84 GiB | +1.7% | 4.01 MiB | 2.21 MiB | -44.9% (1.82× smaller) 🟢 | 27.5 ms | 12.3 ms | -55.1% (2.23× faster) 🟢 | 103.95B | 105.31B | +1.3% |
String.append |
2.155 s | 2.223 s | +3.1% |
19.184 s | 19.440 s | +1.3% | 17.050 | 16.820 | -1.3% | 50.03 GiB | 50.67 GiB | +1.3% | 4.01 MiB | 2.21 MiB | -44.8% (1.81× smaller) 🟢 | 21.6 ms | 12.8 ms | -40.6% (1.68× faster) 🟢 | 95.13B | 96.36B | +1.3% |
Nat.add_comm |
2.023 s | 2.101 s | +3.8% |
18.973 s | 19.192 s | +1.2% | 2.420 | 2.400 | -0.8% | 49.79 GiB | 50.59 GiB | +1.6% | 4.01 MiB | 2.21 MiB | -44.9% (1.82× smaller) 🟢 | 21.6 ms | 12.2 ms | -43.6% (1.77× faster) 🟢 | 87.91B | 89.07B | +1.3% |
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 |
55.762 s | 56.970 s | +2.2% | 49.770 | 48.710 | -2.1% | 73.53 GiB | 73.50 GiB | -0.1% |
Char.ofOrdinal_le_of_le |
50.898 s | 50.651 s | -0.5% | 54.290 | 54.550 | +0.5% | 66.24 GiB | 66.20 GiB | -0.0% |
Array.extract_append |
45.771 s | 46.939 s | +2.6% | 35.090 | 34.210 | -2.5% | 53.78 GiB | 53.70 GiB | -0.1% |
Std.HashMap |
37.623 s | 37.120 s | -1.3% | 54.280 | 55.010 | +1.3% | 53.59 GiB | 54.53 GiB | +1.7% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
35.693 s | 35.516 s | -0.5% | 52.310 | 52.570 | +0.5% | 51.97 GiB | 52.84 GiB | +1.7% |
String.append |
20.915 s | 21.217 s | +1.4% | 15.630 | 15.410 | -1.4% | 50.03 GiB | 50.67 GiB | +1.3% |
Nat.add_comm |
19.699 s | 19.924 s | +1.1% | 2.340 | 2.310 | -1.3% | 49.79 GiB | 50.59 GiB | +1.6% |
johnchandlerburnham
approved these changes
Sep 9, 2026
samuelburnham
pushed a commit
that referenced
this pull request
Sep 10, 2026
After the rebase: Stage 1 leaf prove unchanged (171.6 -> 171.7 s), leaf proofs 22.8 -> 11.1 MB; Stage 2 subtree 0-31 direct joins 1810 -> 1078 s (direct join 190 -> 94 s, ~400 -> ~200 GiB resident), slice peak 1146 -> 599 GiB, root proof 9.7 -> 4.8 MB. The Lean aggregate command skips the exact proof-count check under IX_AGGREGATE_SHARDS. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013o1MyfH4zr7LbbQNMCQbRD
samuelburnham
added a commit
that referenced
this pull request
Sep 10, 2026
…pelines crates/ffi/src/numa.rs: topology from sysfs and sched_getaffinity, per-thread pinning (sched_setaffinity + set_mempolicy MPOL_BIND), one Rayon pool per domain, cgroup memory limit, resident bytes per node. Knobs IX_NUMA, IX_NUMA_POLICY, IX_NUMA_THREADS, IX_NUMA_PACK. Stage 1: `ix prove --lookahead` runs one execute-next-while-proving pipeline per NUMA domain inside a single process (leaves split by measured peak, IX_PROVE_LANES), sharing the environment and proving systems. Stage 2: every join is placed on a domain under a per-lane budget (90% of the node, capped by --max-ram and the cgroup limit), at most two per node, solo tail unpinned. Dependency-free joins run on per-lane queues that prepare the next slot's execution record while the current one proves; with packing on a lane runs two such queues when both fit. Static RAM weights per join shape: direct/mixed 180 GiB (a direct join is ~200 GiB resident after main's function groups), lifts/structural 195 GiB + 1.25 MiB per subject with a 390 GiB floor above 65,536 subjects. Parallel proof import; every slot logs its node's resident peak; `ix aggregate --texray`. IX_AGGREGATE_SHARDS=a-b,c aggregates one subtree of a manifest from an existing run's leaf proofs (experiments; leaf claims do not depend on the manifest size). Rebased on main's function groups (#619/#620): the verify command's backend construction compiles with the IxVM and ix_aggr groupings.
samuelburnham
added a commit
that referenced
this pull request
Sep 10, 2026
…pelines crates/ffi/src/numa.rs: topology from sysfs and sched_getaffinity, per-thread pinning (sched_setaffinity + set_mempolicy MPOL_BIND), one Rayon pool per domain, cgroup memory limit, resident bytes per node. Knobs IX_NUMA, IX_NUMA_POLICY, IX_NUMA_THREADS, IX_NUMA_PACK. Stage 1: `ix prove --lookahead` runs one execute-next-while-proving pipeline per NUMA domain inside a single process (leaves split by measured peak, IX_PROVE_LANES), sharing the environment and proving systems. Stage 2: every join is placed on a domain under a per-lane budget (90% of the node, capped by --max-ram and the cgroup limit), at most two per node, solo tail unpinned. Dependency-free joins run on per-lane queues that prepare the next slot's execution record while the current one proves; with packing on a lane runs two such queues when both fit. Static RAM weights per join shape: direct/mixed 180 GiB (a direct join is ~200 GiB resident after main's function groups), lifts/structural 195 GiB + 1.25 MiB per subject with a 390 GiB floor above 65,536 subjects. Parallel proof import; every slot logs its node's resident peak; `ix aggregate --texray`. IX_AGGREGATE_SHARDS=a-b,c aggregates one subtree of a manifest from an existing run's leaf proofs (experiments; leaf claims do not depend on the manifest size). Rebased on main's function groups (#619/#620): the verify command's backend construction compiles with the IxVM and ix_aggr groupings.
samuelburnham
added a commit
that referenced
this pull request
Sep 10, 2026
…pelines crates/ffi/src/numa.rs: topology from sysfs and sched_getaffinity, per-thread pinning (sched_setaffinity + set_mempolicy MPOL_BIND), one Rayon pool per domain, cgroup memory limit, resident bytes per node. Knobs IX_NUMA, IX_NUMA_POLICY, IX_NUMA_THREADS, IX_NUMA_PACK. Stage 1: `ix prove --lookahead` runs one execute-next-while-proving pipeline per NUMA domain inside a single process (leaves split by measured peak, IX_PROVE_LANES), sharing the environment and proving systems. Stage 2: every join is placed on a domain under a per-lane budget (90% of the node, capped by --max-ram and the cgroup limit), at most two per node, solo tail unpinned. Dependency-free joins run on per-lane queues that prepare the next slot's execution record while the current one proves; with packing on a lane runs two such queues when both fit. Static RAM weights per join shape: direct/mixed 180 GiB (a direct join is ~200 GiB resident after main's function groups), lifts/structural 195 GiB + 1.25 MiB per subject with a 390 GiB floor above 65,536 subjects. Parallel proof import; every slot logs its node's resident peak; `ix aggregate --texray`. IX_AGGREGATE_SHARDS=a-b,c aggregates one subtree of a manifest from an existing run's leaf proofs (experiments; leaf claims do not depend on the manifest size). Rebased on main's function groups (#619/#620): the verify command's backend construction compiles with the IxVM and ix_aggr groupings.
Draft
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.
Recursion function groupings: ix_aggr 192 → 39 circuits, verifier 191 → 72
Stacked on #. Applies the same cost-aware grouping to
the two recursion toplevels that the base PR left empty.
Groups were built from profiles of the
ix_aggrjoin of two lifted shardsand of the standalone verifier over two IxVM proofs (Nat.sub_le_of_le_add,
Lean.Syntax.rec), ranking merges by active committed width saved per unit
of modelled prover cost relative to each workload, within an average 2%
(max 4%) increase, ≤ 16 members per group. The standalone verifier gets
the same groups restricted to its own functions.
Measured with
bench-typecheck --recursive --join:Active width drops ~55% on all three; the FFT increase stays under budget
because the verifier's cost sits in a few tall circuits (blake3, FRI
folding) the partitioner leaves alone. The
ix_aggrverifying keychanges; existing aggregate proofs will not verify against this build.
Tests: primary suite (
recursive-verifier,ix-aggr,aggregate-first,multi-stark), theaggregate-activationaudit, andix codegen --checkpass. No codegen change.