Status: Accepted; D10 (the checks the compiler writes itself are asked through a loop under prove-through-loops:on) added October 20, 2026; D12 (per-turn intervals as candidates for a loop of at most 16 turns) added October 30, 2026 (#639); D13 (a for counts its turns, counters bounded by them) added October 31, 2026 (#1053)
Date: October 17, 2026
Answers: what the prover knows after a loop that changes a name a claim
reads, left open by ADR-269 §6 (Loop invariants) and D16;
whether an invariant must be written; how invariants are found; and how a
tool outside the compiler, an LLM among them, may help find them (issue
#640)
Related:
ADR-269 D9, D15, D16 (what the prover reads; a claim carried back
through code; where the calculus stops); ADR-270 D1, D3-D7, D14,
D21, D22, D24, D25 (the three layers, self-contained queries, the committed
proof file, certificates, SMT-LIB at the edge, the strategy layer, --locked,
the logic as a public package, a counted budget); ADR-258 D2
(only who needs it pays); ADR-359 D2 (a second query only for a
claim left open); ADR-306 D7 (an inductive bound, kept only
where it carries itself); ADR-314 §2 (what other tools do with
loops); issue #599
point 4; issue #639
(unrolling for special cases); Part III 13.2, 13.3, 14.2
fn main(a: int) {
assert(a > 0)
assert(a <= 10)
let mut i = 0
let mut total = 0
while i < a {
i = i + 1
total = total + 10
}
let b = 4 * example(a) + total
assert(b > 40)
assert(b < 181)
}After the loop i == a and total == 10 * a, so b lies between 54 and 180.
The prover reads only names that do not change (ADR-269 D9), and ADR-269 D16
stops at a loop that changes a name a claim reads, so both claims are checks at
run time. Carrying a claim through a loop needs an invariant. Who supplies it -
the author, the compiler, or a tool beside it - and how, is the question.
| Method | Tools | Strength | Weakness |
|---|---|---|---|
| A written invariant | Dafny, Wuffs, Frama-C WP, Why3 | exact, readable | the author writes and maintains it for every loop |
| Unrolling a short loop | SPARK (a for of at most 20 turns), CBMC, Kani |
nothing to write | its cost grows with the turns; it stops at a limit |
| Closed forms of recurrences | LLVM’s scalar evolution, Aligator | exact and cheap for counters and sums | only those |
| Abstract interpretation | Astrée, Frama-C EVA, IKOS, Clousot | always ends; a fact for every loop with nothing written | not directed at a claim; widening loses precision |
| k-induction | CBMC, ESBMC, Kind 2 | ordinary queries only | weak alone |
| Templates (Farkas) | Colón, Sankaranarayanan and Sipma | complete for the form chosen | the form is chosen in advance |
| Guess and check | Daikon, ICE learning, LLM-proposed invariants | strong; candidates from runs or a model | the guess is not deterministic |
| Property-directed reachability (PDR/IC3) on Horn clauses | z3’s Spacer, Eldarica, Golem; SeaHorn, JayHorn, RustHorn translate programs to them | the strongest single method for integers, directed at the claim | large to build; it may search without end; its invariants are hard to read |
Horn clauses (CHC) are the problem these methods share: an unknown relation per
loop head, a clause for entry, one for a turn, one per claim. SMT-LIB writes
them in the logic HORN. This table is from memory, not checked against
sources.
| Option | Example | Why it lost | See |
|---|---|---|---|
| Keep today’s stop | both claims of §1 checked at run time | the compiler sees every line and proves nothing | D2 |
| Only written invariants | assert(i <= a && total == 10 * i) required in the loop |
the author proves what the compiler can see; Nikaia does not make the author write what can be found | D3 |
| Only simple counters | x = x + k found, nothing else |
the prover is meant to grow strong, not stop at the first easy case | D5 |
| One method, PDR from the start | Spacer’s algorithm in the solver first | the largest piece first, while cheaper ones prove the common loops; it comes when the others are exhausted | D5 |
| Unrolling as the general way | a <= 10, so ten copies of the body |
its cost follows the turns, not the claim; kept for special cases in #639 | D5 |
| The loop’s form in the frontend | a Nikaia-only walk that knows while |
another tool using the logic package (ADR-270 D24, #599) would get nothing | D1 |
| An LLM in the build | a model asked during nikaia build |
a build would depend on a network, a service and chance; ADR-270 D4 and D22 keep a build to what the committed file holds | D6 |
| Trust a proposal | an invariant an LLM gave is used as given | a wrong one would prove a false claim | D4 |
| The compiler calls a service over HTTP | nikaia prove posts the problem to an LLM’s address |
the compiler would carry network code, keys and knowledge of providers that change faster than it does | D6 |
A let mut known only until its first assignment |
x = x + 1; assert(x == 1) checked at run time |
every verifier follows assignments; the prover would stop at the first += 1 outside a loop |
D9 |
| MCP as the exchange | the proposer is an MCP server | made for LLM tools; a learner from test runs or a foreign solver fits it badly, and an MCP server can stand behind a proposer program | D6 |
The logic layer (ADR-270 D1) states a loop without Nikaia’s syntax: its state
names, what holds at entry, its condition, what one turn makes of the names,
each way out, and the goals at points in it or after it. This is the shape of
constrained Horn clauses over the logic’s sorts. It is public as the rest of
the logic layer is (ADR-270 D24), and SMT-LIB’s HORN is its import and export
at the edge (ADR-270 D6). The frontend translates a while or a for into it,
and the answer back into the program’s words (ADR-270 D7). A break, a
continue or a return in the loop is a way out of its own, never folded into
the condition.
A claim that reads a name a loop changes, after the loop or inside it, is first asked as today. Where that leaves it neither proved nor refuted, it is asked once more through the loop’s problem (D1), as ADR-359 D2 asks once more with a callee’s summary. A claim decided without the loop never pays for it. This replaces the first stop of ADR-269 D16.
assert may be one, by the flow, not by its place.The compiler finds the invariant itself (D5). An assert in a loop that reads
names the loop changes is a claim where it stands in the program’s flow: it is
proved through the loop, and once proved it is a fact the search may use. What
makes it relate to the loop is which names it reads and how the flow reaches
it, carried back as ADR-269 D15 carries any claim, not whether it stands at the
top of the body.
An invariant is used only once three ordinary queries (ADR-270 D3) are proved,
each with its certificate (ADR-270 D5): it holds at entry, a turn keeps it, and
it with each way out gives the goal. The invariant is kept in nikaia.proofs
with the strategy or the program that found it. Where it came from never
decides whether it is believed.
The strategy layer (ADR-270 D14) holds the methods and the order they are tried in, each under the build’s counted budget (ADR-270 D25). They are added one by one:
asserts and from test
runs;A claim none of them proves stays a check at run time; nothing is proved that the certificate does not show.
A proposer is a program named in the manifest’s [prove] table. It is run
only by nikaia prove --propose, never by nikaia build, run or test. It
is handed, in a versioned format on its standard input, each loop problem the
build left open, in SMT-LIB HORN, with the source of the loop and the names
it reads; it answers with candidate invariants as terms over those names. Each
candidate goes through D4; what passes is written to nikaia.proofs, which the
next build reads and --locked checks without searching (ADR-270 D22). A wrong
proposal costs time and nothing else. Sending the program’s code to a service
outside the machine happens only by that command and that entry, never by
itself. The same interface takes an LLM, a tool that learns from test runs, or
another solver that already does what D5 has not built yet.
The exchange is a child process and one JSON line per problem, each way, as
protoc plugins and language servers talk to their host. The compiler starts
each proposer once, writes one line per open problem to its standard input -
{"version": 1, "id": …, "problem": …, "source": …, "names": […]}, the problem
in SMT-LIB HORN - and closes the input after the last; the proposer writes
one line per problem it answers to its standard output -
{"id": …, "candidates": [ … ]}, each candidate an SMT-LIB term over the
names - and ends. What it writes to standard error is shown to the user. A
proposer that fails, ends early or writes a line that is not this is one helper
lost: the others and the built-in strategies go on, and nothing is proved by
it. What a provider, a model, a key or a prompt is lives in the proposer, not in
the compiler. --propose=CMD names a proposer for one run without the
manifest.
--asserts names, for a claim proved through a loop, the invariant it used and
where that came from; for one left open, the loop and the names it changes.
Built in this order: D1 and D4 with D2; D5’s closed forms and intervals with
D7; D6; then octagons, k-induction, guess and check; PDR when D5 says. The first
step is done when §1’s two claims are proved, lowering the standalone files and
std’s tools costs at most 5 % more instructions, and every invariant used
passed D4.
let mut binding is followed through each assignment.A let mut whole-number binding that no call is handed and no lambda or
deferred body changes is a name of the prover from its let on, with its
value. An assignment gives it a new value the prover reads as a new name
(x = x + 1: the new x is the old one plus 1, the static single assignment
form of Dafny, SPARK, CBMC and Kani); after a branch that changes it on one side
or both, it is one side’s value or the other’s, as the branch it took says;
what a loop changes is read through the loop’s invariant (D2). Before its first
assignment it is a binding that does not change, as ADR-269 D9 reads one. A
binding handed to a call or changed from a lambda stays outside: another piece
of code could change it while the prover believes a value. A claim decided
without these names never pays for them (D2, ADR-258 D2).
prove-through-loops:on.optimization = "remove-bounds-checks:on,remove-overflow-checks:on,prove-through-loops:on"assert(xs.len() == 16384)
while true {
if xs[at] == 0 { return at }
at = (at + 1) & 16383
}An index’s check and an overflow check are claims as an assert is. Under the optimization prove-through-loops:on each one that
reads a name a loop changes, and that the walk of ADR-306 leaves open, is asked
once more through the loop’s problem (D2), and is proved or stays as D4 says.
Under off, the default, these checks are asked as ADR-306 asks them and
never through a loop; an assert is asked through a loop under either.
The switch changes what is proved and therefore what is written, never what a
program means: a check that is not proved stays, and the program stops where it
would stop with every optimization off.
Why. The fastest loops over a buffer carry their bounds from one turn to
the next - a position that only grows below a length, a slot masked into a
table - and a program should not have to restate them as an assert to lose
the check, as D3 says for every invariant. Asking every check of every loop
through its problem costs compile time that most builds do not want: a check
the walk leaves open is far more common than an assert, and each costs the
three queries of D4. The choice of how much to prove, for how much compile time,
is the build’s, as the choice of what proved checks to drop already is.
A check that is not asked today - a shift count’s - is asked through a loop
once it is a claim at all. Rejected: always on, which makes every debug build pay for the release’s
proofs; an assert per loop in the program, against D3; a separate flag per
kind of check, which nobody would set apart.
Decided October 20, 2026.
prove-through-loops:on, a field of every element of a list is one summary.A loop that writes xs[at].f for a whole-number field f keeps one fact for
f over all of xs’s elements (array smashing, as Astrée and Frama-C/EVA do):
a write to one element is a weak update, so the summary afterwards holds the
old value or the new. The summary is related to the loop’s counters by two
templates, f <= c + n (an octagon) and |f| <= K * g for a field g written
in the same turn, where each turn adds at most K to f and at most 1 to g.
That is what a table of counts and sums per key needs: count is at most the
rows seen, which the input’s length bounds, and |sum| at most the largest
value times count. Where per-worker tables are merged, the counts add up to
at most the whole input’s rows, as ADR-367 says of a fold’s accumulator.
The summary is carried across calls too: where the list is a field of a fold’s
accumulator (Table.slots in a Par::fold), each element’s field is bounded
over the whole fold as ADR-367 bounds a counter of the accumulator: every call
of the step and of the merge is one turn, so count is at most the rows the
fold has read and |sum| at most K times that, wherever the step is split
into methods. A fact a method cannot see at its entry is not needed then.
Rejected: quantified invariants and ghost variables written by the program
(Dafny, SPARK), which the owner did not pursue; array partitioning (Cousot,
Cousot and Logozzo), whose cost buys precision per slot that no check here
needs; full polyhedra, where the two templates suffice. Like D10 it changes
what is proved, never what a program means; std and the tools are lowered
with it off.
Decided by the supervising session on the owner’s direction (October 20, 2026: decide what is needed for the goal), from #770.
(Owner, 2026-10-30, #639.) Where a loop’s number of turns is a constant the
prover reads (a range over literal bounds, a counter against a literal limit)
and at most 16, the portfolio (D5) proposes, for each whole-number name the
loop changes, an interval indexed by the turn: at the start of turn k the
name lies in the interval that k turns of the body give from its start. Each
candidate is checked like any other (D4); one that does not hold is dropped,
and the claim falls back to the other strategies. A throw inside such a loop
is an exit of the loop, not a turn. This is unrolling for a special case, not
the general way (ADR-314 §2: SPARK unrolls up to 20 turns): beyond 16 turns, or
with a trip count the prover does not read, nothing is proposed, and only a
claim that needs the candidate pays for it (ADR-258 D2). It lets a range built
up digit by digit over a few turns (v = v * 16 + d, four turns) be proved,
which interval widening loses. Part III 14.2 says it with the build.
for loop counts its turns; a name that grows by at most k a turn is bounded by k times the turns.(Architect, 2026-10-31, under Language decisions, #1053 step 4: D5 item 2
names octagons, ADR-306 D12 bounds every length below 2^60; this joins them.
It changes what is proved, never what a program means.) A for over a list, a
map, a set or another collection with a length has a turn count t the
program cannot name: at the start of each turn 0 <= t < len, where len is
the collection’s length where the loop is reached (a for cannot change what
it walks), and t grows by one at each end of a turn, a continue included.
A for over a..b has t < b - a and its binding equal to a + t. A
while has no turn count of its own; a name the loop grows by exactly 1 on
every path of a turn stands in for it (i - i@). For each whole-number name
n the loop changes only by adding constants of one sign, at most k in
size along any path of one turn, the portfolio proposes n - n@ <= k * t
(or n@ - n <= k * t), and n - n@ == k * t where every path adds exactly
k. Each candidate is checked like any other (D4). So at += 1 in
for x in xs, from at = 0, is proved: at < xs.len() < 2^60. The walk of
the checks (ADR-306) takes these candidates at both settings of
prove-through-loops, as it takes #711’s growing counters; under on they
are also the portfolio’s for D10. A name grown by an inner loop, by a
non-constant amount, or reset in the loop gets none of them. Part III 14.2
says it with the build.
nikaia.proofs; a build reads it (ADR-270 D4).let mut through its assignments (D9) and a name a loop changes through the loop’s invariant
and says what --asserts shows; 13.2 has nikaia prove --propose;
13.3 the [prove] table. ADR-269 D16’s first stop and its open item on
loop invariants point here.Not decided here: invariants over a list’s elements and other quantified facts; loops in a function’s result summary (ADR-359); unrolling beyond D12’s constant trip count of at most 16 turns; which proposers the project ships, if any.
Decided October 17, 2026 (#640).