Status: Accepted
Date: October 2, 2026 (D24-D26: October 6, 2026, #478)
History: the records this one replaces are archived in docs/history/adr; read them only for how the decision was reached
Answers: the owner’s questions whether the prover can get an intermediate
layer now, so that the solver it feeds can later serve other problems and
other languages; how that solver becomes a universal one that is fast by the
world’s measure, not only for the queries the compiler asks today; the
owner’s decision that the solver’s search need not be deterministic, on
the condition that what one machine proved is never rejected by CI or by a
colleague’s machine; and the owner’s decision that the solver is written
in Nikaia from its first engine on, not first in Rust
Related: ADR-269 D4 (a check is dropped where a proof shows
it holds), D7 (--asserts), D8 (a refutation names values), D9-D10 (what the
prover reads and how it decides), D18-D19 (the ledger publishes contracts; a
breaking change is said); ADR-294 (self-hosting a module at a
time, leaves first; no i128 in the language);
ADR-296 (SIMD lives behind std, a SWAR baseline first);
ADR-290 (a Nikaia piece joins a Rust program as a Cargo
module); ADR-294 D14 (a representation is chosen by
measurement); ADR-021 (a build is keyed on content); Part III
13.1 and 13.5 (nikaia.lock, nikaia.contracts, the determinism guarantee,
--locked); ADR-258 (the four weights). The method and the
tables behind the numbers: docs/solver-workload.md
Where does the line run between the Nikaia-specific part of the prover and the part that only does logic; what does the solver behind it become; and what must be reproducible when it is fast?
The prover is three things: the walk over the syntax tree that collects facts, the formulas, and a decision procedure. The formulas mention nothing of Nikaia, so the cut between them is cheap, and dearer with every theory added. What has to be decided is not where - that is nearly forced - but which promises the interface makes, because those are what a later solver can or cannot break: whether the interface is a text format or a data structure; whether a question is self-contained or part of a conversation with hidden state; whether the compiler has to trust the solver.
Behind the interface the goal is a solver that wins the QF_LIA division of SMT-LIB against z3 and cvc5 and then widens, written in Nikaia, and parallel where Nikaia is strong. Which architecture it is built on - so that each later engine is a part that fits, not a rewrite - is decided here before the first algorithm, together with how fast it may be: a search held to determinism is slower, and a search that is not makes the answer depend on the machine. The answer decides whether a check is emitted (ADR-269 D4), whether a contract is published (ADR-269 D18) and whether a warning is said; one commit must build the same program everywhere.
The checker stays small - every strategy, engine and theory produces the same proof format - and is a condition, not an option weighed below.
| Tool | Its answer | What it costs there | Source |
|---|---|---|---|
| Dafny → Boogie → SMT-LIB → Z3 | three layers: the language, an intermediate verification language, the solver’s standard input; proofs are searched again at every build | a proof that passes on one Z3 version, seed or machine can fail on the next (“brittleness”), fought with resource limits | from memory, not checked |
| Why3 (used by SPARK) | one intermediate language, many solvers through drivers that translate to each one’s input | each driver is a translation to maintain; the solvers are external processes | from memory, not checked |
| SMT-LIB 2 | the standard text format: declarations, assertions, check-sat, and an assertion stack (push/pop) |
a command language with global state - a session, not a question; parsing text is a cost of its own | the SMT-LIB 2.6 standard, from memory |
| z3 | CDCL(T); a general simplex over rationals with bound propagation (Dutertre and de Moura), branch-and-bound, Gomory and GCD cuts; model-based theory combination; tactics with time limits; rationals with a small-integer fast path | answers depend on time limits; proofs exist but are not the default and are not small | from memory, not checked |
| cvc5 | CDCL(T); simplex with several arithmetic solvers; theory combination by a care graph; proofs in Alethe, LFSC and its own format | a checker for every rule it can emit is large; proof production costs a measurable factor | from memory, not checked |
| Yices 2 | CDCL(T) with a fast simplex; MCSAT for non-linear arithmetic | no proofs; MCSAT is a second search architecture | from memory, not checked |
| MathSAT 5, SMTInterpol | CDCL(T); for integers branch-and-cut, “cuts from proofs” (Dillig, Dillig and Aiken, CAV 2009), Diophantine equality handling | interpolation drives the design | from memory, not checked |
| Kissat, CaDiCaL (SAT) | clause arena with 32-bit references, blocking literals, binary clauses held apart, inprocessing, mode switching at conflict counts; LRAT proofs | not SMT; the floor for the Boolean core | from memory, not checked |
| SAT competition | an unsatisfiable answer comes with a proof (DRAT/LRAT) that a small checker verifies | the solver may be as clever and as parallel as it likes; trust lives in the checker | from memory, not checked |
| Mallob, Painless | parallel and distributed SAT: portfolios whose engines share learned clauses | the exchange is timed, so runs are not reproducible; the answer is, the effort is not | from memory, not checked |
| Cube-and-conquer (march, Treengeling) | a look-ahead solver splits a hard problem into independent cubes solved in parallel | the split pays on hard combinatorial problems, not on easy ones | from memory, not checked |
| Local search for LIA (Cai et al., CAV 2022) | critical moves over integer assignments find models fast | proves nothing unsat | from memory, not checked |
| Alethe (veriT, cvc5; checked by Carcara) | a proof format for SMT with rules per theory; a linear-arithmetic step carries the Farkas coefficients | a large rule set, so a checker for all of it is not small | from memory, not checked |
| egg (equality saturation) | an e-graph applies rewrite rules until nothing changes | can grow without bound; helps with equalities between terms, not inequalities | from memory, not checked |
| Cargo | Cargo.lock records what resolution found; --locked fails where a build would change it |
resolution may depend on the registry; the build does not, once the lock is committed | Cargo documentation, from memory |
| Coq, Lean; Isabelle (Sledgehammer) | the proof is in the source and is checked, never searched, at build; external provers search freely and what they find is replayed and written into the theory | a proof is written once, when it is found | from memory, not checked |
What transfers: the three layers (Dafny, Why3); certificates checked by a small checker (the SAT competition); the CDCL(T) skeleton every leading SMT solver shares; the SAT solvers’ memory layout; and from Coq, Lean and Isabelle: search when writing, check when building, and keep what was found in the source - which, with Cargo’s lock file, is how a free search and a reproducible build go together.
What does not: SMT-LIB’s assertion stack - state one question leaves
for the next - is the opposite of what a parallel solver wants; Dafny’s
re-search at every build is what makes a proof brittle; GMP and other
libraries (the solver has no dependency outside Nikaia’s std); a proof
format that grew with the solver (cvc5’s checker is large; here the format
is fixed first, D5); a tactics language users write (a strategy is a
component, D14).
Option A — leave prove.rs as it is. The first theory beyond linear
arithmetic is added in the same file, next to the syntax tree.
Option B — SMT-LIB text is the interface. The frontend prints a query; the solver, built-in or external, parses it.
(declare-const total Int)
(assert (> total 0))
(assert (not (> total 0)))
(check-sat)Option C — a logic of our own in memory; SMT-LIB only at the edge. The frontend builds a query as data - terms by id, facts, a goal - and hands it to a solver interface.
Option D — adopt an existing intermediate language (Boogie, Why3).
| D1 the special case pays | D2 the compiler works | D3 no cost for the common case | D4 consistent with itself | If it is wrong | |
|---|---|---|---|---|---|
| A | every new theory pays for the tangle | — | nothing now | the logic cannot be reused or ported on its own | the cut gets dearer with each theory |
| B | — | external solvers for free | every query is printed and parsed; the stack’s state is a sequential conversation | a standard, but a command language | a parallel solver works around the format |
| C | a second format exists only for those who ask for it | the frontend writes one data structure | no text on the path; queries independent, so parallel for free | one structure from the frontend to any backend | undone by writing the exporter B needed anyway |
| D | — | a mature toolchain | an external process for every build | a second language between Nikaia and the solver | the plan - the solver is Nikaia - is given up |
C wins on D3 and on the plan.
Option E — keep Fourier-Motzkin with case splitting, and tune it. Exact, certificates are Farkas combinations by construction; the elimination grows doubly exponentially in the variables (D9 shows it on twelve).
Option F — CDCL(T) with a general simplex, theories behind one interface. The Boolean search learns from conflicts; the simplex is incremental and backtracks by restoring bounds; a conflict’s explanation is a row, which is a Farkas certificate.
Option G — MCSAT as the skeleton. Strong for non-linear arithmetic; for linear integer arithmetic it does not beat F, and its proofs are less settled.
Option H — bind z3 or cvc5 and keep only a checker.
| D1 the special case pays | D2 the compiler works | D3 no cost for the common case | D4 consistent | If it is wrong | |
|---|---|---|---|---|---|
| E | No: one hard query with many variables costs the build | Yes | Yes for tiny queries | Yes | hard queries stay unknown: a check at run time, not a wrong answer |
| F | Yes: work goes where conflicts are | Yes | only with a fast path (D12): a CDCL(T) set-up costs more than a 2-atom query | Yes: one proof format | a rewrite of the engine, not of the interfaces |
| G | Yes | Yes | same as F | two architectures if F is still needed for proofs | a second skeleton beside F |
| H | Yes | Yes | No: about 1.5 ms per query through z3’s API, several hundred times the reference solver | a second solver’s semantics and version decide | undoing a dependency; no road to a solver in Nikaia |
F is chosen. E lost on D1, G on D4 for linear arithmetic (kept for non-linear arithmetic, §6), H on D3 and on the plan.
Option I — the search itself is deterministic: an answer depends on the query and a budget counted in work, never on time or threads. Costs the speed of a portfolio that stops at the first engine to finish, of clause sharing at any moment, and of anything learned in an earlier run.
Option J — free search, nothing recorded. Fastest, and the build depends on the machine: CI and a colleague may reject what worked.
Option K — free search, proofs in a local cache. The same failure as J one step later: CI and a colleague do not have the cache.
Option L — free search, every answer the build uses recorded in a committed file, every entry of which is checked when read.
| D1 the special case pays | D2 the compiler works | D3 no cost for the common case | D4 consistent | If it is wrong | |
|---|---|---|---|---|---|
| I | No: every query pays for determinism | Yes | No: a parallel solver waits at epochs | Yes | slow, never wrong |
| J | Yes | No: the developer chases machine-dependent builds | Yes | No | builds differ by machine |
| K | Yes | No, for the same reason | Yes | No | builds differ by cache |
| L | Yes: only a new query searches | Yes: the build writes the file | Yes: CI checks, it does not search | Yes: one file decides | a forgotten commit fails --locked, with the fix in the message |
L is chosen.
Option M — Rust first, ported when its shape has settled. The engine is measured against z3 and cvc5 in a language whose code generation is known, and ported later.
Option N — Nikaia from the first engine.
| D1 the special case pays | D2 the compiler works | D3 no cost for the common case | D4 consistent | If it is wrong | |
|---|---|---|---|---|---|
| M | every engine is written twice | — | Rust’s code generation from the start | the claim Nikaia is fast and parallel is never tested by its largest program until the end | a second port of a large body of code |
| N | a slow lowering is found by the solver first, and fixed in the compiler | the solver drives what the language and its lowering need | depends on the lowering; measured before the first engine (D8) | the solver is what the plan says it is | a language feature the solver needs waits on a record of its own |
N is chosen, by the owner’s decision. M’s reasons do not hold: the numbers of D11 need no overflow-reporting arithmetic, and measuring against z3 and cvc5 works in Nikaia as well. What N risks - code the lowering makes slower than hand-written Rust - is measured first (D8 step 1) and is a fault of the lowering to be fixed there, not a reason to write the solver elsewhere.
| layer | holds | knows Nikaia’s syntax |
|---|---|---|
frontend (prove.rs) |
the walk over the syntax tree: which facts hold at a claim, which claims are preconditions, what a call substitutes; and what an answer means for the program (ADR-269 D4-D7) | yes |
logic (nikaia-logic) |
sorts, terms, formulas, queries, answers, certificates and their checker, SMT-LIB and Alethe at the edge | no |
solvers (in nikaia-logic, behind one interface) |
decision procedures | no |
The logic and the solvers are a Nikaia package that depends on nothing but
Nikaia’s std - not on the compiler, not on its syntax tree, not on a
crate from crates.io - and reach the compiler the way the compiler’s own
.nika tools do, lowered to Rust (ADR-290). That is what lets
another language or tool feed it, and what makes it a leaf in
ADR-294’s order. A Rust implementation is the reference only
until the Nikaia package answers every query the same way (D8), and is then
removed.
A term is named by a TermId (a u32) into an arena the query owns; a term
never changes once built, so a query can be read from any number of threads
without a lock. Sorts are open: Bool and Int (unbounded integers, as
ADR-269 D9 reads a program’s numbers) first, and each further theory is added
by a record of its own. What the solver holds of a number is D11’s.
Whether ids are hash-consed (one id per distinct term) is decided the way ADR-294 D14 decides a representation: by measuring. The interface allows it and does not depend on it.
No table of terms is shared and written by several threads. The query’s arena is frozen when the query is handed over. A solver thread that builds new terms - a cube, a learned lemma - builds them in an arena of its own, layered over the query’s, and carries over what crosses to another thread or into a certificate. A table every thread writes to behind a lock is the bottleneck a parallel solver is built to avoid.
A query holds its declarations, its facts and its goal, and nothing else: there is no assertion stack and no state left behind for the next query. The answer is
| answer | carries |
|---|---|
| proved | a certificate (D5) |
| refuted | a model: values that make the facts true and the goal false - what ADR-269 D8 shows |
| unknown | the reason, in words - what ADR-269 D7 shows |
Independent queries are parallel without anything being written: a program’s claims are thousands of questions no one of which waits for another. A solver may keep state across queries inside itself - learned lemmas, a cache (D15); what a build uses is fixed by D4.
The search may limit itself by time, run engines against each other and take the first answer, share learned facts whenever it likes, use every thread the machine has, and read and write caches of its own. Nothing about it has to be reproducible.
What a build uses is a function of the sources, nikaia.proofs and the
toolchain. Every query the prover asks while building a package has an entry
in that package’s nikaia.proofs, committed beside nikaia.contracts
(D19-D23). The emitted code, the published contracts (ADR-269 D18) and the
diagnostics NK1207 and NK1208 are computed from the entries, never from a
search that was not recorded. Part III 13.5’s determinism guarantee holds with
nikaia.proofs among its inputs: the same sources, the same nikaia.proofs
and the same toolchain give the same program, the same ledger and the same
diagnostics on every machine and at every thread count. A proof found once -
on a fast machine, in a long run, by a newer solver - serves every machine from
then on.
A proved answer carries a certificate that a small checker in
nikaia-logic replays. The compiler drops a check (ADR-269 D4) only on a
certificate it has checked - never on the bare word of a solver.
The certificate is one proof log, append-only, that every engine, strategy and theory writes into. Its steps:
¬a₁ ∨ … ∨ ¬aₖ justified
by a Farkas combination of the atoms’ bounds: non-negative multipliers
for inequalities, any sign for equalities, rational multipliers written as
integers over one common denominator, ending in 0 < 0 or c <= 0 with
c > 0; strict bounds carry their strictness.L <= k ∨ L >= k + 1 for an integer form L with
integer coefficients and an integer k: valid by itself, checked by
looking at L and k. Branch-and-bound is a split and a resolution.q defined by
0 <= L - m·q <= m - 1 for an integer form L and an integer m > 0:
q is the floor of L / m, which exists for every value of L, so the
definition cannot make a satisfiable problem unsatisfiable. SMT-LIB’s div
and mod by a constant are exactly this, and it keeps some proofs short:
twelve numbers that are each -1 or 1 never sum to 1, which splits take
2¹² cases to show and which q = ⌊(x + 1) / 2⌋ per number, a two-case lemma
each (x + 1 - 2q = 0) and one rounding show in linear size.A case split is part of the proof. A disjunction - an ||, a !=, the
negation of a guard’s == - is split only where a branch needs it: a split
node names a disjunction by its number in the query and proves every
alternative, and the checker numbers the query itself, so a split cannot
leave an alternative out. A branch whose refutation did not need the
alternative it was given answers for the whole disjunction. A bound every
alternative implies - on one form, the weakest of their constants - holds
without a split; the checker computes it by the same rule.
Which cuts are allowed: every cut that is a Chvátal-Gomory derivation (a combination and a rounding) - Gomory’s fractional cuts, the GCD test on an equality, Hermite-normal-form cuts on equality rows - and every split cut (valid on both sides of a split: Gomory mixed-integer, mixed-integer rounding, lift-and-project, cuts from proofs), written as the split, one derivation per side and the resolution. A heuristic may find a cut by any means, floating point included; it is written as one of these, exactly, or not used.
Small means: the checker replays, it never searches. Its rules are the
five above plus one per further theory (D13), each a replay; the checker for
linear integer arithmetic and clauses stays under 1 500 lines, and a rule
that would push it past needs a record. Alethe stays an export (D6): each step
has an Alethe counterpart (resolution, la_generic with integer
strengthening), which is how the format is checked by a checker this package
did not write.
Rejected: Alethe as the internal format (a large rule set); a certificate per engine (one checker per engine is not small); no certificate for cuts (the most error-prone code of an integer solver would be trusted); extension with arbitrary definitions (one not satisfiable for every value would be unsound; the floor is the form needed and the one always satisfiable).
nikaia-logic writes any query as SMT-LIB 2 and reads the part of SMT-LIB 2
its sorts cover, and writes a certificate as an Alethe proof. It is used for
comparing an answer with another solver’s, running public benchmark sets
against the solver (D17), and letting a reader see what the compiler asked. A
build never needs an external solver; one may be used to cross-check, never to
decide what is emitted (D4, D5).
A query carries opaque ids for its facts and goal. Which claim, line or precondition an id stands for is the frontend’s to know and to put into a message; the logic layer prints no Nikaia.
The reference solver - three layers behind D3’s interface, its certificates
and their checker, SMT-LIB and Alethe at the edge, models for refuted,
i64 numbers, case splitting on demand - is where the order starts. Every
step is written in Nikaia:
| Step | What | Measured by |
|---|---|---|
| 1 | A performance probe: three kernels written in Nikaia and in Rust - combining two rows (multiply-add with D11’s range check), scanning a watch list, multiplying big integers - lowered, built and timed side by side | Each kernel’s time in Nikaia against Rust. Where Nikaia is slower by more than the noise, the cause in the lowering is named and fixed in the compiler before the engines are written; nothing is moved back to Rust |
| 2 | The reference solver in Nikaia: terms, Fourier-Motzkin with case splitting, the checker, SMT-LIB and Alethe - the Rust crate’s content, as a Nikaia package (D1) | Every recorded, suite and stress query answered as the Rust crate answers it, every certificate checked by both checkers, every Alethe proof valid under Carcara; the Rust crate removed |
| 3 | u32 variables and sparse rows (D10), D11’s numbers, D5’s proof log and its checker, D12’s theory interface - with Fourier-Motzkin behind it and equalities eliminated exactly before it |
The 92 unknown queries of D9 answered (56 proved, 36 refuted); every other query answered as before, z3 agrees; the compiler’s queries no slower (4.2 µs to solve and 1.9 µs to check a certificate, on average); big numbers agree with an independent implementation on randomised operations; the checker under 1 500 lines |
| 4 | nikaia.proofs (D19-D23), parallel across queries (D18), the local caches and measurements (D15) |
A --locked build byte-identical on every machine and at every thread count; every entry checks; a batch of SMT-LIB-sized queries speeds up by at least 0.7 × threads, and the compiler’s batch does not slow down (work below a threshold stays on one thread) |
| 5 | The CDCL(T) core with the simplex as its first theory; preprocessing; interval and difference fast paths (D12) | All of the sets above; the compiler’s queries at or under step 3’s time; on QF_LIA, the solved count against z3’s and cvc5’s on the same machine, and every proved checks |
| 6 | Cuts (D5’s forms), local search for models, the strategy layer (D14) | Parity with twelve variables proved in linear size (D5’s extension); on QF_LIA, more solved than z3 and cvc5 single-threaded, then a lower PAR-2; the strategy beats the best single configuration on a held-out half of the set |
| 7 | Cube-and-conquer, portfolios and clause sharing (D18) | On QF_LIA’s hard unsatisfiable instances, solved count and PAR-2 against z3 and cvc5 in their parallel modes |
Step 4’s first criterion is “no harm”. The compiler’s queries cost 4 µs each and 7 ms for the whole test suite; a thread costs more than the work. Parallel across queries pays for SMT-LIB runs and for large projects, behind a work threshold that keeps the compiler’s batch on one thread.
Fourier-Motzkin stays as the cross-check of every later engine and as an engine the strategy may keep for tiny dense problems, where it is measured.
The workload is the queries the prover asks while the compiler’s test suite
runs, with a stress set for four families the suite does not reach (guards,
unrelated disjunctions, +1 or +2 paths, parity). The numbers that decide: no
query has more than four variables; 83 % hold only interval or difference
atoms (x - y), at about one non-zero per atom and every coefficient 1 or 2; a
query takes 4.2 µs on average, 60 % of it in Fourier-Motzkin; and the 92
queries Fourier-Motzkin leaves unknown are all an equality with the
coefficient 2 (blank = 2·n), whose parity it loses over the rationals. For
scale, z3 spends about 1.5 ms on a trivial query with a fresh solver, and on
parity with twelve variables z3 answers in 12 ms while Fourier-Motzkin runs out
of budget.
What the numbers decide: the compiler’s workload is tiny and almost all intervals, so it decides the fast paths and the rule that the common case pays nothing (D12, D16); it does not decide the core, which is sized by SMT-LIB (D17).
Rejected: designing from the benchmark literature alone (the compiler’s queries would pay a general engine’s set-up on every one); designing from the compiler’s queries alone (four variables decide nothing about a core that has to win QF_LIA).
u32; rows are sparse; small problems run dense.A variable, a term, a clause and a literal are u32 indices into arenas
(D2). A row - an atom, a tableau row, a derived bound - is sparse: two
parallel arrays, column indices (u32, ascending) and coefficients (D11’s
numbers). A query whose variables fit one vector register - eight or fewer;
no query the compiler asks has more than four - runs on a
dense kernel of fixed width instead, chosen by the strategy layer (D14).
Why sparse: the compiler’s atoms hold 1.05 non-zeros each; the stress
set’s chains hold two of 33 variables (6 %); SMT-LIB’s linear problems are
sparse by construction (from memory, not checked). Why a dense kernel at
all: below eight variables the bookkeeping of a sparse row costs more than
the arithmetic, and eight i64 lanes are one AVX-512 register or two AVX2
ones (D16).
Rejected: dense everywhere (fails every large problem); a map from names to coefficients (each combination compares strings; it is most of Fourier-Motzkin’s 60 %); a hash map per row (slower than a sorted merge at these sizes, and its iteration order would make certificates differ between runs).
i64 fast path, and a fall-back to big integers and fractions.Σ aⱼxⱼ / d), so the inner
loop is integer multiply-add; the row is reduced by its gcd after a pivot.i64 while it fits in 32 bits,
so one product fits 63 bits and one combination a·x + b·y cannot overflow;
the result is compared with the 32-bit range, and a coefficient that leaves
it promotes that one number to a big integer.u32 limbs with u64 products.
A 52-bit-limb kernel using AVX-512 IFMA is a kernel behind the same type
(ADR-296), not a second representation.u64.
Nikaia’s integers as they are suffice (ADR-294 keeps i128
out, and nothing here asks for it).δ for strict bounds (Dutertre and de Moura).Rejected: i64 only (a proof lost to overflow is a check at run time, acceptable for the compiler, not for SMT-LIB); i128
(ADR-294); floating point with exact repair (every answer and certificate must
be exact anyway, for a gain no measurement has shown); full rationals
everywhere (a gcd per operation in the inner loop).
The search is a CDCL loop over Boolean literals - decisions, unit propagation, conflict analysis to a first-UIP clause, backjumping, restarts, clause-database reduction - and every theory sits behind one interface:
| call | what it does |
|---|---|
assert(lit) |
a literal became true at the current level; the theory takes its bound or equality, and may answer with a conflict at once |
propagate() |
literals the theory implies cheaply (bound propagation), each explained later on demand |
check(final: bool, limit) |
consistency of what is asserted: consistent, a conflict (a clause and its proof step), or lemmas to add (a split, a cut) |
explain(lit) |
the clause and proof step behind a literal it propagated |
backtrack(level) |
forget what was asserted above level; the simplex keeps its basis and restores bounds |
model() |
values that satisfy what is asserted, checked by evaluation (D3) |
shared() |
the terms and equalities it shares with other theories (D13) |
The simplex is built against this interface from its first line: general simplex with bounds on variables, one slack variable per distinct linear form, pivoting by a fixed rule with Bland’s rule as the fall-back that guarantees termination.
Fast paths are the same interface, cheaper: a query with no Boolean choice skips the CDCL loop; interval atoms (68 % of the compiler’s queries hold nothing else) are decided by bounds on single variables; difference atoms (a further 15 %) by negative-cycle detection, whose certificate is the cycle - a Farkas sum with every multiplier one. No fast path allocates for a query below the dense width: the common case pays nothing for the skeleton (ADR-258 D3).
Rejected: CDCL as a later step (the simplex would be built against Fourier-Motzkin’s interface and rebuilt); enumerating Boolean models and asking the theory each (exponential in the disjunctions); MCSAT as the skeleton (§3, Option G).
Only linear integer arithmetic is built first; the procedure is decided now so that the others fit.
Rejected: Nelson-Oppen with eager equality propagation (needs convex, stably infinite theories, which bit-vectors and integers are not); Shostak (needs canonisers and solvers per theory); a care graph as cvc5 builds it (a refinement of the same idea, open to measurement later).
A strategy chooses before the start and switches during the search; it is not inside an engine:
Rejected: strategies inside the engines (no engine could be measured alone or replaced); user-written tactic scripts (a language to maintain for a choice the features already make).
All of it lives under target/nikaia/, is not committed, and is never read by
a --locked build (D22). It may make the search find more and find it
sooner; what the build uses is still only what nikaia.proofs records (D4).
Measured: a cache hit saves a 4.2 µs solve minus a 1.9 µs re-check, so for the compiler’s queries the cache is worth little; it is for the hard ones and for SMT-LIB runs.
u32 words: a header (size, flags, the
learned clause’s glue) followed by the literals; a clause reference is a
u32 word index. Literals are u32 (variable << 1 | sign).std with a SWAR baseline and multiversioning per target
(ADR-296). A kernel the solver needs and std lacks is added
to std by a record of its own.Rejected: pointer-based clauses (Box, Rc: twice the memory and no
compaction); hashing with a random seed (a certificate’s content, and so the
proof file’s diff, would vary between runs).
Rejected: measuring on the compiler’s queries alone (they are 4 µs each, D9); comparing on different machines.
Every answer carries its proof, so a race changes how soon a query is answered and never what is true; what a build uses is fixed by D4.
nikaia.proofs is a key and an answer, and the answer carries its evidence.nikaia.lock already uses. It does not include the solver’s
version: a proof stays a proof when the solver changes.proved with its certificate (D5’s proof
log, about the normal form); refuted with its model; unknown with the
version of the solver that gave up - no evidence, because an unknown only
keeps a check and says nothing.nikaia.proofs.d/, named by its key, and the line points to it.A proved entry’s certificate is replayed by the checker (D5) against the
query in hand; a refuted entry’s model is evaluated. An entry that does not
check - a corrupt file, a hand edit, a hash collision, a frontend that now asks
a different query under the same key - counts as missing. Nothing in the
file can make the compiler drop a check that does not hold or say a warning
that is not true: the file needs no more trust than the solver does.
For each query: an entry that checks is used. A missing one is searched for,
freely (D4), and its answer written. An unknown entry is searched again only
when the solver is newer than the version it records, or when the developer
asks for it (nikaia prove, with a larger limit). Entries no query asked are
removed. The file is written before the ledger is derived, so the ledger
follows from the file as it now stands. A changed nikaia.proofs is part of
the change the developer commits, as a changed nikaia.contracts is.
--locked searches nothing and fails on any difference.nikaia build --locked reads the file, checks every entry it uses, and
compares the set of keys the build asks with the set the file holds. A query
with no entry, or an entry that no longer checks, fails the build and names the
query’s source position and the fix - run nikaia build and commit
nikaia.proofs; an entry nothing asks fails it too, so the file cannot rot.
An unknown entry is used as it is: the check stays. CI with --locked
therefore never rejects what a developer’s machine built and committed, and
never accepts what it did not; its prover cost is a check per entry, not a
search.
nikaia.proofs is resolved like a lock file’s: take
both sides’ entries, or either, and run nikaia build. Taking both is always
safe, because every entry is checked (D20).nikaia.proofs for the queries its own build
asks. A query asked while building the consumer - a precondition at a call
into the dependency - is the consumer’s.verify are public, its solvers are not.Added October 6, 2026 (#478).
D1’s package is not the compiler’s private part. A driver’s grammar that asks
whether a WHERE clause rules out a NULL
(ADR-299 D18; it may call it by ADR-321 D13), or any other package with a question in linear
integer arithmetic, depends on it and asks. It is Nikaia code that only
computes - sync, touching nothing - so it runs while a program is built under
the rule every Nikaia dependency meets (ADR-321 D2, D8), with no
exception of its own.
What a caller sees is what D1 puts in the logic layer: building terms, a query (D3), its answer, and the checker (D5). The solvers, their representation (D2, D10) and the strategy (D14) stay behind it, so they can change by measurement without breaking a caller.
Rejected: keeping the package the compiler’s, which leaves every tool that needs the same question to write a second, weaker solver; and making the solvers’ interface public, which turns D2’s and D10’s measured choices into promises.
A query a package asks at build time is not an entry of nikaia.proofs (D4):
it arises in each consumer’s build, from that consumer’s input. Its answer is
the reference solver’s, under a budget counted in units of work, never in
time, so the same query gets the same answer on every machine and at every
thread count, and Part III 13.5’s guarantee holds with the package’s version in
nikaia.lock among its inputs. A proved answer comes with its certificate,
which the caller may check with verify. Unknown, the budget spent, is
not a proof, and a caller acts as if nothing were proved: in a driver, the
column stays one that may be NULL, which refuses at worst and never admits a
wrong value.
Rejected: recording such answers in the consumer’s nikaia.proofs, which
would make a file about the program’s claims hold a dependency’s questions; and
the free search of D4, which would let one machine’s build accept what
another’s refuses.
std.It keeps its own version, and a caller states which one it builds against. std
does not grow by a solver that most programs never call; and the rule of D24
needs no std exception, since the package is Nikaia that the build derives.
Rejected: std::logic, which would tie the solver’s releases to the
toolchain’s and make every program carry it.
nikaia.proofs. A
developer commits it with the code that needed it; CI says when they did not,
and how to fix it. A toolchain upgrade can change it, as it can change
nikaia.contracts.use.nikaia.proofs is shipped or rebuilt by the
consumer when its sources are present; shipped like its ledger until a case
says otherwise.std
kernel for wide multiply-add, prefetching, anything the probe of D8 step 1
names - each by a record of its own.Real sort, for QF_LRA, and whether δ-rationals are a number type
of the package or of the simplex alone.push/pop): D3 keeps queries self-contained;
decided when that track is a goal.h(9) makes n = 9 known inside h - are
the frontend’s, and a later record.forall is asked when a claim does.