Status: Superseded by ADR-270 — restated there, D1-D8 with the same numbers, together with ADR-267 and ADR-268
Amended by: ADR-267 — D8’s order: the engine is built and measured in Rust before the port, which follows its CDCL(T) core; ADR-268 — D4 is superseded: the search is free, and what a build uses is the committed nikaia.proofs
Date: October 2, 2026
Answers: the owner’s question whether the prover can get an intermediate
layer now, so that the solver it feeds can later serve other problems and
other languages — checked against the long-term plan: a solver written in
Nikaia that outdoes the existing ones where this language is strong,
parallelism and performance, because it carries no legacy
Related: ADR-264 D9-D10 (what the prover reads and how it
decides), D7 (--asserts) and D8 (a refutation names values),
ADR-250 (self-hosting a module at a time, leaves first),
ADR-257 D3 (a representation is chosen by measurement), Part I
1.2 (a program means the same at user_parallelism = no and yes),
ADR-021 (a build is keyed on content), ADR-258
(the four weights this is weighed by)
Where does the line run between the Nikaia-specific part of the prover and the part that only does logic — and what must that line promise so that the logic part can become a fast, parallel solver written in Nikaia without being redesigned?
Today crates/nikaia/src/prove.rs is one file holding three things: the walk
over the syntax tree that collects facts, the formulas (Lin, Formula), and
the decision procedure (Fourier-Motzkin elimination with a fixed amount of
work, CASES). The formulas already mention nothing of Nikaia, so the cut is
cheap now and gets dearer with every theory added. What has to be decided
before cutting is not where — that is nearly forced — but which promises
the interface makes, because those are what a later solver can or cannot
break:
Each of these, answered the conventional way, is a known obstacle to parallel solving or to a reproducible build. That is the check this record makes.
| 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 | a proof that passes on one Z3 version can fail on the next or under a different random seed (“brittleness”); the toolchain pins the solver version | 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 |
| cvc5, Z3 | incremental solving through the assertion stack; proofs as an option (cvc5: Alethe, LFSC) | sequential cores; parallelism mostly as a portfolio or by splitting the problem into cubes | from memory, not checked |
| SAT competition | an unsatisfiable answer must come 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 lookahead solver splits a hard problem into many independent sub-problems (cubes), solved in parallel without shared state | the split itself is expensive and pays on hard combinatorial problems more than on easy ones | from memory, not checked |
| ManySAT, deterministic mode | engines exchange learned clauses only at barriers fixed by work counts, so the run is reproducible | every barrier waits for the slowest engine | 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, then extracts the best form | can grow without bound and needs a limit of its own; helps with equalities between terms, not with inequalities | from memory, not checked |
What transfers: the three layers (Dafny, Why3) are the established shape, certificates (the SAT competition) are how a fast, unproven solver is used without being trusted, and cube-and-conquer and deterministic clause sharing are two ways of being parallel inside one query that a reproducible answer does not rule out. What does not: SMT-LIB’s assertion stack — state that one question leaves for the next — is the opposite of what a parallel solver wants, and Dafny’s brittleness is what a timeout does to a build. A compiler whose output depends on a solver’s timeout produces a different program on a slower machine.
prove.rs as it isNothing to write; the first theory beyond linear arithmetic is added inside the same file, next to the syntax tree.
The frontend prints a query in SMT-LIB 2; the solver, built-in or external, parses it.
(declare-const total Int)
(assert (> total 0))
(assert (not (> total 0)))
(check-sat)The frontend builds a query as data — terms by id, facts, a goal — and hands it to a solver interface. SMT-LIB is an export (and an import, for testing the solver), not the interface.
The frontend translates to it; its toolchain does the rest.
| 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, not a data structure | a parallel solver has to work 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 that B would have needed anyway |
| D | — | a mature toolchain | an external process and its runtime for every build | a second language with its own semantics between Nikaia and the solver | the plan — the solver is Nikaia — is given up |
C wins on D3 and on the plan. B’s text and session cost on every query what only an export needs, and D gives the solver away.
| layer | holds | knows Nikaia |
|---|---|---|
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-264 D4-D7) | yes |
logic (nikaia-logic) |
sorts, terms, formulas, queries, answers, certificates, and SMT-LIB export and import | no |
solvers (in nikaia-logic, behind one interface) |
decision procedures; the first is today’s Fourier-Motzkin | no |
nikaia-logic is a crate that depends on nothing but the standard library:
not on the compiler, not on the syntax tree, not on a crate from crates.io.
That is what lets another language or tool feed it, and what makes it a
leaf in ADR-250’s order — the first whole piece of the
prover that can move to Nikaia.
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-264 D9 reads a program’s numbers) first, and each further theory —
lengths and sequences, arrays, fixed-width integers with wrap-around — is
added by a record of its own.
Whether ids are hash-consed (one id per distinct term, so equality is an integer comparison) is a representation choice and is decided the way ADR-257 D3 decides one: 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 whatever crosses to another thread or into a certificate is carried over at a point D4 fixes. A table that every thread writes to behind a lock is the bottleneck a parallel solver is built to avoid.
A number is an i64. The sort Int is unbounded; what the solver holds
of it - a constant, a coefficient, a multiplier in a certificate, a value in
a model - is an i64, the widest integer Nikaia has (ADR-252
keeps i128 out, and the solver is no reason to let it in). A step that
leaves i64 answers unknown for its reason (overflow), never a wrong
answer, so the width decides how much is proved and not whether a proof is
right. A program literal no i64 holds is not read; its claim stays checked
at run time. When overflow stops proofs a program needs, the step is exact
arithmetic - an integer of any size, built from u32 pieces whose products
fit a u64, beside an i64 fast path - and not a wider type in the language.
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, where the solver produces one (D5) |
| refuted | a model: values for the query’s names that make the facts true and the goal false — what ADR-264 D8 shows |
| unknown | the reason, in words — what ADR-264 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 — as long as no answer depends on it (D4).
A solver is given a budget in units of work it counts itself — steps,
cases, conflicts — never in seconds. For the same query and budget, every
solver answers the same at any number of threads and on any machine. This is
Part I 1.2 — a program means the same at user_parallelism = no and yes —
held by the compiler’s own solver, and it is what keeps a build reproducible:
whether a check is emitted (ADR-264 D4) cannot depend on how loaded the
machine was.
It costs a parallel solver less than it sounds. A portfolio may still race: proved is final the moment any engine proves within its budget, so the others can be stopped; unknown is the answer only when every engine has spent its budget; and a refuted answer gives a canonical model — the smallest by a fixed order — so that a message does not change between runs. What D4 forbids is only an answer decided by which thread finished first.
Within one query, parallelism takes two shapes that keep D4:
Which of the two a solver uses, and when, is the solver’s record, not this one. A compiler’s queries are mostly many and easy, so the parallelism that pays first is across queries (D3), and both shapes are for the few hard ones.
Counting is coarse and local. A unit of work is an expensive step — a conflict, an eliminated variable, a split — so counting it is one addition among thousands of instructions, cheaper than reading a clock, which a time limit has to do as well. Each engine or cube counts its own budget in its own register: a counter shared between threads would make them contend for one cache line, which is the slowdown a parallel solver exists to avoid.
A proved answer may carry a certificate that a small checker in
nikaia-logic verifies — for linear arithmetic, the non-negative combination
of facts that yields a contradiction (Farkas’ lemma), which Fourier-Motzkin
derives anyway; for a SAT core, a clause proof in the spirit of DRAT/LRAT.
The certificate is per theory and as small as the theory allows, because the checker is the part that has to be trusted. A general SMT proof format such as Alethe is a large rule set, and a checker for all of it is no longer small; it is an export (D6), so that another tool — Carcara, cvc5 — can check what this solver claims. The two meet where it matters: Alethe’s linear-arithmetic step carries the same Farkas coefficients. The compiler drops a check (ADR-264 D4) on the word of the reference solver, the one it ships with, or on a certificate it has checked — never on the bare word of any other.
A case split is part of the certificate. A disjunction - an ||, a
!=, the negation of a guard’s == - is split only where a branch needs it,
and the certificate is the tree of splits: a node names a disjunction by its
number in the query and holds a certificate for every alternative, a leaf is
a Farkas refutation of the atoms its branch holds. 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, and the others are not looked at. 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, and the Alethe export proves
it by one lemma per alternative.
This is what lets the later solver be as clever and as parallel as it can be: its bugs are caught by the checker, not by a program that stops in production.
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 where the theory
has one. It is used for three things: comparing an answer with
another solver’s, running public benchmark sets against the solver, 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.
Lin, Formula and Fourier-Motzkin into nikaia-logic behind D3’s
interface. The suite (tests/prove.rs, tests/assert.rs) is the proof
that nothing a program sees changed.nikaia-logic in Nikaia, as a leaf (ADR-250). It needs
overflow found rather than aborted on (D2’s numbers): wrapping_* and a
sign test, or checked operations, by a record of their own.prove.rs shrinks to
the part only Nikaia can do.h(9) makes n = 9 known inside h —
are the frontend’s, not the logic’s, and are a later record.forall is asked when a claim
does.