ADR-268: The Search Is Free; What a Build Uses Is a Committed Proof File

Status: Superseded by ADR-270 — its D1-D2 are D4, D3-D7 are D19-D23, D8 is D15 there Date: October 2, 2026 Answers: the owner’s decision not to hold the solver’s search to determinism - it slows a solver that is meant to be fast, and a proof one machine, one cache or one long run has found is legitimate on every other - together with the owner’s condition that what one machine proved must not be rejected by CI or by a colleague’s machine Supersedes: ADR-265 D4 (an answer depends on the query and the budget, never on time or threads); ADR-267 D7 (switching only at work counts), D8 (a result cache keyed with the budget, lemmas shared only as a committed input), D11 (the parallel rules) and D12’s criteria that rest on them - see D9 Related: ADR-264 D4 (a check is dropped where a certificate shows it holds), ADR-265 D5 (a certificate makes a solver usable without trusting it), ADR-266 D5-D6 (the ledger publishes contracts; a contract changed in the breaking direction is said), Part III 13.1 and 13.5 (nikaia.lock, nikaia.contracts, the determinism guarantee and --locked), ADR-021 (a build is keyed on content). Sizes: docs/solver-workload.md

1. Question

ADR-265 D4 made every answer of the solver a function of the query and a budget counted in work, so that two machines build the same program. It is paid for in speed: no portfolio that stops at the first engine to finish, no time limits, clause sharing only at epochs where every thread waits for the slowest, nothing learned in one run used in the next.

The answer matters beyond the run that asked. It decides whether a check is emitted (ADR-264 D4), whether a precondition or postcondition is published in nikaia.contracts (ADR-266 D5), and whether NK1207 and NK1208 are said. If one machine proves what another does not, the two build different programs from one commit, CI rejects a ledger that a developer’s machine wrote, and a warning appears on one desk and not on the next.

Can the search be free and the build still the same everywhere?

2. How others do it

Tool	Its answer	Source
Cargo	Cargo.lock records what resolution found; --locked fails where a build would change it. Resolution may depend on the registry’s state; the build does not, once the lock is committed	Cargo documentation, from memory
Dafny, F*, Verus	Proofs are re-searched by z3 on every build; a proof that passes on one machine and times out on another is a known source of “brittle” or “flaky” verification, fought with resource limits (rlimit) instead of time	from memory, not checked
Coq, Lean	The proof term is in the source and is checked, never searched, at build; a tactic that searches runs when the proof is written	from memory, not checked
Isabelle (Sledgehammer)	External provers search freely; what they find is replayed by the kernel and written into the theory as a reconstructable step	from memory, not checked

What the last two do is what this record takes: search when writing, check when building, and keep what was found in the source. What does not transfer: the proof here is not written by the developer; the compiler finds it, so the file holding it is generated - as a lock file is.

3. Options, weighed

Option A — keep ADR-265 D4: the search itself is deterministic

Every machine finds the same proofs within the same work budget. Costs the speed the owner will not pay, and still does not let one machine’s long run help another.

Option B — free search, nothing recorded

Fastest, and the build depends on the machine: CI and a colleague may reject what worked, and a warning comes and goes. Rejected by the owner’s condition.

Option C — free search, proofs in a local cache or database

A machine reuses its own finds; CI and a colleague do not have them. The same failure as B one step later.

Option D — free search, every answer the build uses recorded in a committed file

The search may do anything; the build uses only what the file holds, every entry of which is checked when read. A new find changes the file, and the file is committed with the code that needed it.

Weighed

	D1 the special case pays	D2 the compiler works	D3 no cost for the common case	D4 consistent	If it is wrong
A	No: every query pays for determinism	Yes	No: a parallel solver waits at epochs	Yes	Slow, never wrong
B	Yes	No: the developer chases machine-dependent builds	Yes	No	Builds differ by machine
C	Yes	No, for the same reason	Yes	No	Builds differ by cache
D	Yes: only a new query searches	Yes: the file is written by the build	Yes: CI checks, it does not search	Yes: one file decides	A forgotten commit fails --locked, with the fix in the message

D is chosen.

4. Decision

D1 — The search is free.

A solver may limit itself by time, run engines against each other and take the first answer, share clauses whenever it likes, use every thread the machine has, and read and write caches and lemma stores of its own. Nothing about the search has to be reproducible. Work counters stay what they are good for: measuring, and the features a strategy reads (ADR-267 D7).

D2 — 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. The emitted code, the published contracts 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 nikaia.contracts and the same diagnostics on every machine.

D3 — An entry is a key and an answer, and the answer carries its evidence.

• The key is the SHA-256 of the query in normal form - variables numbered by first occurrence, atoms normalised, facts in a canonical order - the digest nikaia.lock already uses. It does not include the solver’s version: a proof stays a proof when the solver changes.
• The answer is one of three:
  • proved with its certificate (ADR-267 D4’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.
• The format is one line per entry, sorted by key, so that two branches that add entries merge without a conflict. A certificate is written compact and encoded as text; one longer than 4 KiB goes into its own file under nikaia.proofs.d/, named by its key, and the line points to it.
• Size, measured: the compiler’s certificates are 10 bytes in the median and 22 at most in a compact encoding; the 1 697 queries of the test suite are 105 distinct ones. A project’s file is lines, not megabytes. The stress set’s hardest certificate (parity with ten variables) is 35 KB, which is what the side directory is for.

D4 — Every entry is checked when it is read.

A proved entry’s certificate is replayed by the checker (ADR-265 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. Checking costs 1.9 µs per certificate on average today.

D5 — A normal build searches what is missing and writes the file.

For each query: an entry that checks is used. A missing one is searched for, freely (D1), 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.

D6 — --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: the difference is the uncommitted file, and the message says so. A CI build with --locked costs a check per entry, not a search.

D7 — Conflicts, dependencies and upgrades.

• A merge conflict in 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 (D4).
• A dependency ships its own 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, and lives in the consumer’s file.
• A toolchain upgrade that changes how the frontend builds a query changes its key; the old entry is removed and the new one searched. The build says that the change came from the toolchain, as Part III 13.5 does for the ledger.

D8 — What stays on one machine only speeds the search.

A local result cache, a lemma store, measurements per query and anything a strategy learns live under target/nikaia/, are not committed and are never read under --locked. They are the search’s, and D1 lets the search do what it likes.

D9 — What changes in ADR-265 and ADR-267.

• ADR-265 D4 is superseded by D1-D2: an answer may depend on time, threads and the machine; what a build uses may not. Its budget in work remains as a measure and as a feature, not as the rule an answer obeys.
• ADR-267 D7: a strategy may switch on any signal, time included, and needs no checkpoints; its parameters are still named and versioned, because that is what makes them tunable.
• ADR-267 D8: the result cache is D8 of this record (local, a speed-up) and the committed store is nikaia.proofs (D2-D3). The lemma store may grow during builds; it is local.
• ADR-267 D11: a portfolio may race, cubes may be answered in any order, clauses may be shared at any moment. ADR-267 D3’s promotion to big numbers stays as it is - a function of the values - because it is exact, not because D4 asked it.
• ADR-267 D12’s criteria: answers and certificates identical at 1 and n threads becomes a --locked build is byte-identical on every machine and at every thread count, and every entry checks. Step 2 builds nikaia.proofs, D5 and D6 in place of the result cache.

5. Consequences

• A project has one more generated, committed file. A developer commits it with the code that needed it; CI tells them when they did not, and how to fix it.
• CI does not search: its prover cost is checking, about 2 µs per entry.
• A proof found once - on a fast machine, in a long run, by a newer solver - serves every machine from then on.
• A toolchain upgrade can change nikaia.proofs as it can change nikaia.contracts, and is narrated the same way.
• The solver is free to be as fast as it can, and its speed is still compared with z3 and cvc5 by ADR-267 D10’s measuring rod, under time limits that are now its own as well as theirs.

6. What this does not decide

• The compact encoding of a certificate, and its version mark, which the first build of ADR-267 step 1 fixes with the proof log.
• How long a normal build may search a new query, and whether that limit is time, work or both; a default the measurement of ADR-267 step 3 sets.
• Whether a published package’s nikaia.proofs is shipped or rebuilt by the consumer when its sources are present; it is shipped like its ledger until a case says otherwise.

This site is open source. Improve this page.