Performance: the engine, measured

Every argument the library adds makes every later check dearer: a dispute's defeat table is one decision per ordered pair of parties, each decided in the kernel over the parties' premises and the argument's meaning postulates. So the engine is made faster and lighter as a loop, measured at each step, until a further change makes no significant difference. How to run the loop is in the optimising-the-engine skill (.claude/skills/optimising-the-engine); this page is its ledger: what was measured, what was tried, and what came of it.

How it is measured

• Benchmarks (arguments/bench/Engine.lean, run by scripts/bench.sh): copies of real proofs and checks, each timed with the kernel's work included, with its peak memory above what its process held before. Each benchmark runs in a Lean process of its own.
• Comparison (scripts/bench-ab.sh, scripts/bench-compare.py): an ablation. The code with a change and without it are built side by side on one machine and run interleaved, and each benchmark is compared by the two-sided Mann-Whitney U test, as Google Benchmark's compare.py does it. A change counts when p < 0.05 and it is larger than the variance bound. Peak memory is compared by threshold. A calibration benchmark, which no change can move, shows whether the machine drifted during the run.
• CI runs the A/B on every pull request, against the base it merges into, and fails on a regression that the pull request does not accept, with its reason, in arguments/bench/accepted.toml.
• Build and kernel replay are measured by hand, as below, until they have a gate of their own.

Baseline

Measured on 30 October 2026, at main after #171, on a 4-core, 16 GB cloud container (the shape of CI's runner), three runs per benchmark, one run of each check.

The first run of each benchmark is 10–40% slower than the rest: warm-up, not a cache that would let later runs skip the work.

The slowest modules of the arguments' build: SolaFide.Ratings (150 s), Checks (101 s, most of it the AIF check), SolaFide.Dispute (81 s), Meanings.SolaFide (74 s) and CanonicalWitness.Results (46 s).

Rounds

Round 3, measured on one side of a scripts/bench-ab.sh run against main, five interleaved rounds: each table is benchmarked twice, searched in the kernel as before and certified, and the two are compared. A profile of one sola fide cell found that converting a party's position to clauses took 17 ms a question, and propagating to a fixed point, in the kernel, about 85 ms; atom comparisons cost nothing that mattered. So the search now runs at elaboration, and the kernel checks what it found: a model, against every clause once, or the clauses that fired, replayed once (Horn.clausesSatisfiableBy?, Testimony.Logic.Certificate). Each position is converted once per cell, and the search is not specialized at each call, which had cost 50 ms a cell in compilation. Half of sola fide's table fell from 14.2 s to 7.1 s (−50%, p = 0.008) and its peak memory from 185 to 92 MiB; the Septuagint's from 3.25 s to 1.53 s (−53%, p = 0.008), 32 to 16 MiB; one cell from 101 to 61 ms (p = 0.016). Every searched benchmark matched main (every p ≥ 0.06), and the calibration benchmark showed no drift. Measured by hand on the same machine, clean: the arguments' lake build fell from 363.5 s to 308.7 s (−15%), SolaFide.Dispute from 70 s to 48 s; the build's peak, about 13.8 GiB summed over its parallel jobs, did not move, and the kernel replay took 261 s at 8.5 GiB against main's 329 s at 8.1 GiB, one run each.

Round 2, scripts/bench-ab.sh against the commit before, five interleaved rounds. Horn.clausesSatisfiable? propagated up to five times per question, Horn.stepRebuts? and Horn.defeats? made their checks twice, and Aif.attacks re-asked, for its preferences, what the attack checks had just asked. Run by the interpreter, as the checks over every argument are, each copy was evaluated: the AIF check fell from 67.4 s to 3.75 s (−94%, p = 0.008), the postulates check by 20% (p = 0.008) and the refutations check by 24% (p = 0.016). The kernel-decided benchmarks did not move (every p ≥ 0.17): the kernel was already sharing the repeated terms. Peak memory did not move, and the calibration benchmark showed no drift. One side of a benchmark run fell from 146 s to 76 s.

Round 1 was measured by hand, before the benchmarks existed. leanchecker replays each module as a task of its own, each importing that module's whole environment, and Lean runs one task per core: four environments at once ran out of memory. Two run in 293 s; one in 500 s with about 5.2 GiB.

Fixed points

None yet. After round 3 the largest benchmarks are still the defeat tables, now about 100 ms a sola fide cell: half of it the kernel's check, of which the conversion of both positions to clauses is most, and half the search at elaboration, in the interpreter. The next hypotheses are bitmask sets for the replay as well as the model (#180), and the certified forms for the verdicts, assessments and ratings, which still search in the kernel.