Function groups by gabriel-barrett · Pull Request #619 · argumentcomputer/ix

gabriel-barrett · 2026-09-08T16:45:50Z

Aiur function grouping: prove several functions with one circuit (IxVM proofs −50–56%)

An IxVM proof commits and opens only the circuits active in the run, and every
column of an active circuit is opened at every FRI query. A kernel check
activates 500–575 of the kernel's 744 function circuits, most of them a few
rows tall, for a summed active width of 21–24k columns — so proof size is
dominated by how many circuits are active, not by the hot ones. This PR lets
several functions share one circuit, and uses that to cut IxVM proofs roughly
in half at +1–2% prover cost.

Mechanism (`aiur: circuit-level function grouping`)

A circuit can back several functions. Members are walked like the branches of
a single function: auxiliary columns and lookup slots are shared across members
(the same save/restore sharing match arms already use), selector columns are
laid out consecutively per member, and every member folds its selector-gated
return message (with its own function index) into the shared lookup slot 0
against one multiplicity column. One extra constraint enforces cross-member
exclusivity: the sum of the members' top-block selectors must be boolean.

Grouping is a circuit-level choice, not a property of the function library:
callers still target function indices on the function channel, so execution,
the query record, the interpreter and codegen are untouched.
Source.Toplevel.compile builds the default singleton partition
(Bytecode.Toplevel.circuits, behavior-identical to before) and
CompiledToplevel.groupFunctions regroups it by function name (validated:
known, constrained, non-entry, no duplicates). The merged layout is max inputs,
summed selectors, max auxiliaries, max lookups. Rust consumes the partition
directly via FFI; constraints, trace and synthesis iterate circuits, and
witness rows concatenate the members' queried rows in member order.

Wiring (`aiur: wire optional function-grouping application points`)

Every site that compiles a production toplevel for proving or verifying goes
through compileWithGroups with a per-toplevel datum:

IxVM.functionGroups — the kernel (check/prove/verify/refine/aggregate, the
batch checker, the ixvm test runner, the benches)
Aggr.functionGroups — the ix_aggr recursion system (empty)
MultiStark.verifierFunctionGroups — the standalone verifier (empty)

Members are resolved by the exact string the statistics print, so measured
groupings feed back verbatim. The recursion groupings stay empty on purpose.

The IxVM grouping (`ixvm: populate the function grouping …`)

function-groups/ixvm/ holds the profiles, the model, the partitioner and a
README with the method. In short:

Model. Committed width and the FFT cost model of
Ix/Aiur/Statistics.lean are reproduced from the static layout alone,
validated to the column on every circuit, so a candidate grouping's widths
and costs are known before building anything.
Partitioner. Greedy agglomerative merging. Benefit = active committed
width saved on the training workloads (String.split, Array.extract_append,
and a 2^16384 big-nat reduction whose hot circuit is cold everywhere else).
Cost = modelled prover cost added (FFT model plus a constraint-evaluation
term), relative to each workload. Merges are taken by benefit per unit cost
within an average 2% (max 4%) increase per workload, ≤ 16 members and ≤ 40
selectors per group.
Result. 83 groups over 656 circuits: 744 → 171 circuits, total
committed width 33,693 → 12,729.

Measured on the grouped kernel (held-out constants included):

workload	active circuits	active fn width	FFT cost
String.split (train)	575 → 171	24,094 → 10,163 (−57.8%)	+1.0%
Array.extract_append (train)	572 → 171	23,884 → 10,163 (−57.4%)	+1.1%
nat_pow_big (train)	461 → 163	19,688 → 9,452 (−52.0%)	+1.9%
Nat.sub_le_of_le_add	503 → 167	21,332 → 9,870 (−53.7%)	+1.6%
String.Internal.append	494 → 166	20,937 → 9,941 (−52.5%)	+1.9%
Lean.Syntax.rec	509 → 174	21,886 → 10,942 (−50.0%)	+2.0%

End to end (bench-typecheck --ixe InitStd.ixe, 100 queries):

constant	proof bytes	prove	verify
Nat.sub_le_of_le_add	19,765,334 → 9,414,761 (−52.4%)	2.79s → 2.32s	0.103s → 0.051s
Lean.Syntax.rec	20,233,436 → 10,325,344 (−49.0%)	3.06s → 2.47s	0.099s → 0.054s
String.split	22,452,866 → 9,895,153 (−55.9%)	21.49s → 20.32s	0.121s → 0.056s

Proving got slightly faster despite the modelled +1–2%: the per-circuit fixed
costs of the ~570 shed circuits outweigh the extra columns on the few-row
merged traces. For comparison, the earlier shape-band heuristic on the old
group-functions branch bought −43% active width for +9–14% FFT cost.

Tests

aiur-prove proves the same toplevel ungrouped and with a 3-member test
group (different arities, matches, cross-member call, recursion), plus
structural checks on the partition.
Kernel FFT pins re-measured (median +1.7%, max +3.8%; shard pipeline
+1.3%). The ixvm ignored suite, the primary suite (including
recursive-verifier, ix-aggr, aggregate-first), the Rust aiur tests,
fmt, clippy and ix codegen --check are green.
The Mathlib Stage 2 fixture stays fenced as obsolete (it already predates the
protocol bump; the IxVM verifying key changes again here).

Notes

The IxVM verifying key changes; existing IxVM proofs will not verify against
this build.
A stale grouping stays sound (grouping never affects semantics), only less
efficient, and fails loudly if a member name disappears. Regeneration steps
are in function-groups/ixvm/README.md.

Several functions can now be proven by ONE circuit: the members are walked like branches of a single function - auxiliary columns and lookup slots are shared across members (the same save/restore sharing match arms already use), selector columns are laid out consecutively per member, and every member folds its selector-gated return message (carrying its own function index) into the shared lookup slot 0 against a single shared multiplicity column. One extra constraint enforces cross-member exclusivity: the sum of the members' top-block selectors must be boolean. Callers are untouched - calls still target function indices on the function channel - so grouping is invisible to execution, the query record, and the interpreter. Grouping is a CIRCUIT-level choice, not a property of the function library, so there is no source annotation: Source.Toplevel.compile builds the default singleton partition (Bytecode.Toplevel.circuits, one circuit per constrained function - behavior-identical to before), and CompiledToplevel.groupFunctions optionally regroups it by function NAME (validated: known, constrained, non-entry, no duplicates). The merged layout is max inputs, summed selectors, max auxiliaries, max lookups - so grouping fits rarely-called functions of similar shape: each (rare) row pays the group's selector count while the system sheds one circuit (vk entry, commitment matrix, verifier work) per absorbed member. Rust consumes the partition directly (bytecode Circuit via FFI; constraints/trace/synthesis iterate circuits, witness rows concatenate the members' queried rows in member order). The stage-2 lookup group size and the branchless raw-argument rule now key on the CIRCUIT layout: multi-member circuits are branching by construction, so their arguments are selector-superposed exactly like match arms. Tests: the aiur suite proves the same toplevel twice - ungrouped and with a 3-member test group (different arities, matches, cross-member call, recursion) - plus structural checks on the partition (members, merge-rule layout, every constrained function in exactly one circuit). All suites pass unchanged (ixvm FFT pins identical - the default partition is behavior-neutral); codegen is unaffected (execution ignores the partition).

…ings) Route every site that compiles a production toplevel for proving or verifying through `compileWithGroups` with a per-toplevel grouping datum: `IxVM.functionGroups` for the kernel (CLI check/prove/verify/refine/ aggregate, the batch checker, the ixvm test runner, the benches), `Aggr.functionGroups` for the `ix_aggr` recursion system (aggregate prove/verify, the aggregation tests and benches), and `MultiStark.verifierFunctionGroups` for the standalone Multi-STARK verifier (its end-to-end tests, recursion-debug, bench-typecheck). `groupFunctions` resolves members by STRING name (the exact `toString` of the Global, the inverse of what statistics print, so measured groupings feed back verbatim). All three groupings start EMPTY, i.e. singleton circuits - behavior-identical to before; the data files are the single knob later commits turn.

…4 -> 171) Built from fresh execute-only kernel-check profiles of the current circuits (String.split, Array.extract_append, and a 2^16384 big-nat reduction whose hot circuit is cold in every typechecking workload), with a partitioner that ranks merges by the ACTIVE committed width they save - what a proof actually opens, at every FRI query - per unit of modelled prover cost (the FFT model of Ix/Aiur/Statistics.lean plus a constraint-evaluation term, relative to each workload), within an average 2% (max 4%) cost increase per workload, <= 16 members and <= 40 selectors per group. The width/FFT model reproduces the measured statistics to the column, so the emitted grouping is exactly what the prover builds. 83 groups over 656 of 743 groupable circuits: 744 -> 171 circuits, total committed width 33,693 -> 12,729 (-62%), active width on kernel checks -50% to -58% (three held-out constants included) at +1.0% to +2.0% measured FFT cost. End to end, proofs of Nat.sub_le_of_le_add / Lean.Syntax.rec / String.split shrink from 19.8 / 20.2 / 22.5 MB to 9.4 / 10.3 / 9.9 MB, proving is slightly faster (fewer per-circuit fixed costs than extra columns) and verification takes half the time. Kernel FFT pins re-measured (median +1.7%, max +3.8%; shard pipeline +1.3%).

arthurpaulino · 2026-09-08T16:53:11Z

!benchmark fresh

argument-ci-bot · 2026-09-08T16:59:00Z

`!benchmark` — main vs `d25f459`

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

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

7 constants · 3 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`	8.793 s	8.775 s	-0.2%	35.924 s	35.194 s	-2.0%	77.250	78.850	+2.1%	72.86 GiB	73.41 GiB	+0.8%	11.11 MiB	5.06 MiB	-54.4% (2.19× smaller) 🟢	61.3 ms	28.5 ms	-53.6% (2.15× faster) 🟢	136.01B	137.19B	+0.9%
`Char.ofOrdinal_le_of_le`	6.798 s	6.691 s	-1.6%	30.976 s	29.883 s	-3.5% 🟢	89.200	92.460	+3.7% 🟢	65.88 GiB	66.27 GiB	+0.6%	11.11 MiB	5.05 MiB	-54.6% (2.20× smaller) 🟢	60.9 ms	28.2 ms	-53.8% (2.16× faster) 🟢	104.21B	105.30B	+1.0%
`Array.extract_append`	6.401 s	6.498 s	+1.5%	26.666 s	26.050 s	-2.3%	60.230	61.650	+2.4%	53.18 GiB	53.70 GiB	+1.0%	11.02 MiB	4.92 MiB	-55.4% (2.24× smaller) 🟢	54.9 ms	29.0 ms	-47.2% (1.89× faster) 🟢	98.00B	99.03B	+1.1%
`Std.HashMap`	4.009 s	3.988 s	-0.5%	17.805 s	17.146 s	-3.7% 🟢	114.680	119.100	+3.9% 🟢	37.40 GiB	37.65 GiB	+0.7%	11.06 MiB	4.97 MiB	-55.0% (2.22× smaller) 🟢	60.4 ms	28.8 ms	-52.3% (2.10× faster) 🟢	62.93B	63.51B	+0.9%
`_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq`	3.588 s	3.639 s	+1.4%	16.456 s	15.927 s	-3.2% 🟢	113.450	117.220	+3.3% 🟢	35.01 GiB	35.39 GiB	+1.1%	11.05 MiB	4.95 MiB	-55.2% (2.23× smaller) 🟢	57.4 ms	28.1 ms	-51.1% (2.04× faster) 🟢	56.49B	57.01B	+0.9%
`String.append`	427.1 ms	437.3 ms	+2.4%	2.112 s	1.740 s	-17.6% (1.21× faster) 🟢	154.840	187.960	+21.4% (1.21× faster) 🟢	6.11 GiB	5.88 GiB	-3.6% 🟢	9.78 MiB	4.70 MiB	-51.9% (2.08× smaller) 🟢	49.5 ms	26.1 ms	-47.3% (1.90× faster) 🟢	3.45B	3.51B	+1.6%
`Nat.add_comm`	261.0 ms	261.9 ms	+0.3%	964.2 ms	732.9 ms	-24.0% (1.32× faster) 🟢	47.710	62.770	+31.6% (1.32× faster) 🟢	4.54 GiB	4.43 GiB	-2.4%	8.95 MiB	4.50 MiB	-49.7% (1.99× smaller) 🟢	40.8 ms	24.3 ms	-40.4% (1.68× faster) 🟢	314.33M	321.32M	+2.2%

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`	4.693 s	2.468 s	-47.4% (1.90× faster) 🟢	41.944 s	20.766 s	-50.5% (2.02× faster) 🟢	66.160	133.630	+102.0% (2.02× faster) 🟢	101.81 GiB	55.01 GiB	-46.0% (1.85× smaller) 🟢	4.00 MiB	4.01 MiB	+0.0%	21.2 ms	21.7 ms	+2.4%	209.69B	107.18B	-48.9% (1.96× fewer) 🟢
`Char.ofOrdinal_le_of_le`	4.832 s	2.421 s	-49.9% (2.00× faster) 🟢	41.233 s	20.771 s	-49.6% (1.99× faster) 🟢	67.010	133.020	+98.5% (1.99× faster) 🟢	101.80 GiB	55.05 GiB	-45.9% (1.85× smaller) 🟢	4.00 MiB	4.01 MiB	+0.2%	21.9 ms	22.0 ms	+0.7%	208.66B	106.08B	-49.2% (1.97× fewer) 🟢
`Array.extract_append`	4.578 s	2.354 s	-48.6% (1.94× faster) 🟢	37.243 s	19.994 s	-46.3% (1.86× faster) 🟢	43.120	80.320	+86.3% (1.86× faster) 🟢	91.84 GiB	52.12 GiB	-43.2% (1.76× smaller) 🟢	4.00 MiB	4.01 MiB	+0.2%	22.1 ms	22.9 ms	+3.4% ⚠️	198.51B	103.56B	-47.8% (1.92× fewer) 🟢
`Std.HashMap`	4.746 s	2.359 s	-50.3% (2.01× faster) 🟢	39.634 s	20.459 s	-48.4% (1.94× faster) 🟢	51.520	99.810	+93.7% (1.94× faster) 🟢	97.31 GiB	53.69 GiB	-44.8% (1.81× smaller) 🟢	4.00 MiB	4.00 MiB	-0.0%	21.6 ms	22.4 ms	+3.3% ⚠️	208.71B	104.43B	-50.0% (2.00× fewer) 🟢
`_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq`	4.709 s	2.358 s	-49.9% (2.00× faster) 🟢	40.445 s	19.900 s	-50.8% (2.03× faster) 🟢	46.160	93.820	+103.2% (2.03× faster) 🟢	99.56 GiB	52.06 GiB	-47.7% (1.91× smaller) 🟢	4.02 MiB	4.01 MiB	-0.2%	21.5 ms	21.8 ms	+1.4%	203.56B	103.95B	-48.9% (1.96× fewer) 🟢
`String.append`	3.902 s	2.228 s	-42.9% (1.75× faster) 🟢	36.000 s	19.246 s	-46.5% (1.87× faster) 🟢	9.080	16.990	+87.1% (1.87× faster) 🟢	89.27 GiB	50.01 GiB	-44.0% (1.79× smaller) 🟢	4.00 MiB	4.01 MiB	+0.2%	22.7 ms	21.9 ms	-3.7% 🟢	169.61B	95.13B	-43.9% (1.78× fewer) 🟢
`Nat.add_comm`	3.083 s	2.047 s	-33.6% (1.51× faster) 🟢	23.497 s	19.105 s	-18.7% (1.23× faster) 🟢	1.960	2.410	+23.0% (1.23× faster) 🟢	58.76 GiB	49.87 GiB	-15.1% (1.18× smaller) 🟢	4.01 MiB	4.01 MiB	+0.0%	21.1 ms	22.0 ms	+3.8% ⚠️	129.00B	87.91B	-31.9% (1.47× 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`	1m 17.9s	55.960 s	-28.1% (1.39× faster) 🟢	35.640	49.590	+39.1% (1.39× faster) 🟢	101.81 GiB	73.41 GiB	-27.9% (1.39× smaller) 🟢
`Char.ofOrdinal_le_of_le`	1m 12.2s	50.654 s	-29.9% (1.43× faster) 🟢	38.260	54.550	+42.6% (1.43× faster) 🟢	101.80 GiB	66.27 GiB	-34.9% (1.54× smaller) 🟢
`Array.extract_append`	1m 3.9s	46.045 s	-28.0% (1.39× faster) 🟢	25.130	34.880	+38.8% (1.39× faster) 🟢	91.84 GiB	53.70 GiB	-41.5% (1.71× smaller) 🟢
`Std.HashMap`	57.439 s	37.605 s	-34.5% (1.53× faster) 🟢	35.550	54.300	+52.7% (1.53× faster) 🟢	97.31 GiB	53.69 GiB	-44.8% (1.81× smaller) 🟢
`_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq`	56.901 s	35.827 s	-37.0% (1.59× faster) 🟢	32.810	52.110	+58.8% (1.59× faster) 🟢	99.56 GiB	52.06 GiB	-47.7% (1.91× smaller) 🟢
`String.append`	38.112 s	20.986 s	-44.9% (1.82× faster) 🟢	8.580	15.580	+81.6% (1.82× faster) 🟢	89.27 GiB	50.01 GiB	-44.0% (1.79× smaller) 🟢
`Nat.add_comm`	24.461 s	19.837 s	-18.9% (1.23× faster) 🟢	1.880	2.320	+23.4% (1.23× faster) 🟢	58.76 GiB	49.87 GiB	-15.1% (1.18× smaller) 🟢

Workflow logs

For testing and measurement against the ungrouped systems without editing the data files: when the variable is set to anything but `0` or the empty string, `compileWithGroups` ignores its grouping and compiles the singleton partition, at every site that applies one (kernel, ix_aggr, standalone verifier). Read once per process through an `implemented_by` opaque, so the pure compile path stays pure. The prover and the verifier must see the same setting - grouping changes the verifying key.

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

After function groups (#619) CircuitType::Function { idx } enumerates circuits, but raw_of still read record.function_queries[idx], charging circuit i with function i's rows. Projections came out 0.83-1.72x (median 1.30x) off on Mathlib shards while measured peaks were unchanged, splitting shard 217 (481 GiB projected, 284 real) at prove time. Sum the members' query counts instead. Shard 0: 378 -> 250 GiB projected vs 248 measured. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013o1MyfH4zr7LbbQNMCQbRD

…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.

After function groups (#619) CircuitType::Function { idx } enumerates circuits, but raw_of still read record.function_queries[idx], charging circuit i with function i's rows. Projections came out 0.83-1.72x (median 1.30x) off on Mathlib shards while measured peaks were unchanged, splitting shard 217 (481 GiB projected, 284 real) at prove time. Sum the members' query counts instead. Shard 0: 378 -> 250 GiB projected vs 248 measured.

…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.

After function groups (#619) CircuitType::Function { idx } enumerates circuits, but raw_of still read record.function_queries[idx], charging circuit i with function i's rows. Projections came out 0.83-1.72x (median 1.30x) off on Mathlib shards while measured peaks were unchanged, splitting shard 217 (481 GiB projected, 284 real) at prove time. Sum the members' query counts instead. Shard 0: 378 -> 250 GiB projected vs 248 measured.

…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.

After function groups (#619) CircuitType::Function { idx } enumerates circuits, but raw_of still read record.function_queries[idx], charging circuit i with function i's rows. Projections came out 0.83-1.72x (median 1.30x) off on Mathlib shards while measured peaks were unchanged, splitting shard 217 (481 GiB projected, 284 real) at prove time. Sum the members' query counts instead. Shard 0: 378 -> 250 GiB projected vs 248 measured.

gabriel-barrett added 3 commits September 8, 2026 16:03

gabriel-barrett force-pushed the gb/function-groups branch from 7cbfa19 to d25f459 Compare September 8, 2026 16:47

arthurpaulino approved these changes Sep 8, 2026

View reviewed changes

johnchandlerburnham added this pull request to the merge queue Sep 9, 2026

Merged via the queue into main with commit eea8f5d Sep 9, 2026
14 checks passed

johnchandlerburnham deleted the gb/function-groups branch September 9, 2026 12:43

johnchandlerburnham mentioned this pull request Sep 9, 2026

WIP: Scale FLT IxVM execution with native setup, compact records, and incremental refinement #621

Open

samuelburnham mentioned this pull request Sep 10, 2026

Sb/cluster #623

Draft

Navigation Menu

Uh oh!

Function groups - #619

Function groups#619
johnchandlerburnham merged 4 commits into
mainfrom
gb/function-groups

gabriel-barrett commented Sep 8, 2026

Uh oh!

arthurpaulino commented Sep 8, 2026

Uh oh!

argument-ci-bot Bot commented Sep 8, 2026 •

edited

Loading

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

gabriel-barrett commented Sep 8, 2026

Aiur function grouping: prove several functions with one circuit (IxVM proofs −50–56%)

Mechanism (aiur: circuit-level function grouping)

Wiring (aiur: wire optional function-grouping application points)

The IxVM grouping (ixvm: populate the function grouping …)

Tests

Notes

Uh oh!

arthurpaulino commented Sep 8, 2026

Uh oh!

argument-ci-bot Bot commented Sep 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

!benchmark — main vs d25f459

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

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Mechanism (`aiur: circuit-level function grouping`)

Wiring (`aiur: wire optional function-grouping application points`)

The IxVM grouping (`ixvm: populate the function grouping …`)

argument-ci-bot Bot commented Sep 8, 2026 •

edited

Loading

`!benchmark` — main vs `d25f459`

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