Sb/cluster

[samuelburnham]

Prove Mathlib on one metal-48xl box in 4 h 36 min: NUMA lanes, lane pipelines, native verify, peak-model fix

Summary

This branch makes ix prove and ix aggregate use a large NUMA box as three
isolated proving domains instead of one flat machine, and fixes two things
found on the way. Measured end to end on Mathlib (679,499 constants, 246 leaf
shards) on an r8i.metal-48xl (Xeon 6975P-C, 96 cores / 192 threads, 1.5 TiB,
three sub-NUMA domains of ~504 GiB):

	production, one 64-vCPU box (#598)	this branch, before main's function groups	this branch on current main
Stage 1 (246 leaf proofs)		2 h 38 min	2 h 44 min
Stage 2 (245 recursive joins)		3 h 25 min	1 h 52 min
total proving	28 h 17 min	6 h 20 min	4 h 36 min
root proof		9.85 MB	4.91 MB

The root proof b060ee48… verifies all 679,499 constants with 0 undischarged
assumptions in 5 s. Root and leaf proofs halved in size with main's function
groups (#619/#620), which this branch is rebased on.

What the branch does

NUMA lanes (crates/ffi/src/numa.rs, new). Detects the topology
(sysfs ∩ sched_getaffinity), pins threads with sched_setaffinity +
set_mempolicy(MPOL_BIND), builds one Rayon pool per domain, reads the cgroup
memory limit, and reports resident memory per node. Env knobs IX_NUMA,
IX_NUMA_POLICY, IX_NUMA_THREADS, IX_NUMA_PACK.

Why: a single proof cannot use more than one domain (whole box 1.08–1.18x over
one node, the prover is memory-latency bound), but three pinned lanes scale
3.0x. Unpinned in-process slots reached only ~1.7x.

Stage 1: one process, one lane per domain. ix prove --lookahead splits
the selected leaves across lanes (LPT by measured peak, IX_PROVE_LANES) and
runs the existing execute-next-while-proving pipeline once per lane, sharing
the environment and proving systems. Replaces three numactl processes.

Stage 2: NUMA-pinned scheduler and lane pipelines. 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 joins share a node; the dependency tail
runs unpinned. The dependency-free joins (all direct joins) run on per-lane
queues that prepare the next slot's execution record while the current one
proves, hiding ~30 s per join; with packing on, a lane runs two such queues
when both fit (2 × (180 + 40) GiB ≤ 453 GiB), so Mathlib's 105 direct joins
run six-wide. RAM weights are static per join shape: direct/mixed 180 GiB
(measured ≈ 200 GiB resident after function groups), lifts/structural
195 GiB + 1.25 MiB per subject with a 390 GiB floor above 65,536 subjects
(the subject term is the join's own claim work; the old flat weight OOM-killed
a node). Proof import is parallel; every slot logs its node's resident peak.

Native ix verify --ixes (composed verdict). The Lean path reconstructed
each shard's claim on one core (~15 s per Mathlib shard, an hour for the
manifest). It now runs through the Stage 2 import: claims in Rust, every proof
bound to its shard and verified in parallel, exactly one valid proof per
shard — 1.6 s of work inside a 54 s process (environment load).

Peak-model fix (crates/aiur/src/synthesis.rs). After #619 the prover RAM
projection charged circuit i with function i's rows. Projections came out
0.83–1.72x off (median 1.30x) while measured peaks were unchanged, and one
Mathlib leaf that needs 284 GiB was projected at 481 GiB and split at prove
time. The model now sums a circuit's member rows; shard 0 projects 250 GiB
against 248 GiB measured. This is a regression in main and could go upstream on
its own, as could the native verify.

Experiment knob. IX_AGGREGATE_SHARDS=a-b,c aggregates only that subtree
of a manifest from an existing run's leaf proofs (leaf claims do not depend on
the manifest size). It is what made the A/B measurements below cheap.

Docs. docs/shard-pipeline.md documents the workflow (shard → refine →
Stage 1 → Stage 2, one cgroup slice, THP always) and has a self-contained
end-to-end reproduce section: build, per-boot box setup, every command, what
the first log lines should show, resume semantics, and how to run a Stage 2
experiment on a subtree. docs/numa-slot-pinning.md is the design and
calibration note. The raw logs and per-run records behind the numbers below
are kept outside the PR.

Measurements behind the decisions

question	result
THP	prover 1.5–1.7x faster with enabled=always (87 M → 0.66 M first-touch faults); set per boot
direct joins vs wrap-first (Mathlib subtree, 32 leaves)	direct 1810 s; wrap-first 2147 s pipelined, 2106 s packed; a direct join verifies two leaves for the price of two lifts and saves the extra join. Wrap-first does not lower the process peak under packing. Direct joins kept.
main's function groups on the same subtree	1810 s → 1078 s (direct join 190 → 94 s, ~400 → ~200 GiB resident); leaf proofs 22.8 → 11.1 MB; Stage 1 leaf time unchanged (171.6 vs 171.7 s)
two queues per lane	1078 s → 967 s; packed direct joins 155 s each, node peak 409 of 504 GiB; +22 % direct-phase throughput
packing two slots on one 64-thread pool	1.63x per slot (net +20–28 % throughput) with a straggler tail of a few slots at 2–6x; core-disjoint half-pools removed the tail but were left out for simplicity
mimalloc fork vs glibc	glibc ~10 % faster on the prover, mimalloc ~4 % faster on the executor; kept mimalloc
Stage 2 memory, full run	slice peak 1207 GiB, nodes ≤ 425 of 504 GiB, no OOM

Not in this branch

Half-pools (rejected for complexity), PoW substitution in the recursion
parameters (measured only), kernel pinning.

Checks

lake build ix and lake build IxTests build; the shard-pipeline runner
(IxTests --ignored shard-pipeline, whose summary is now per NUMA lane) and
the ffi/aiur test suites pass; workspace clippy with warnings denied and
rustfmt are clean.

Reproduce

Section 5 of docs/shard-pipeline.md is the runbook: THP always and
numa_balancing=0 per boot, one cgroup slice sized from the machine,
ix shard → ix shard refine → ix prove --lookahead → ix verify --ixes →
ix aggregate --direct-joins --jobs 0 --max-ram 1350 → ix verify --aggregate,
each a single command under systemd-run --scope, all resumable by rerunning.