Issue #640: The prover reads through a loop: Horn clauses in the logic layer, a portfolio of strategies, every invariant checked, proposers (an LLM among them) only checked (ADR-361)

Open and answer this issue on GitHub.

ready · opened 2026-10-17 · updated 2026-10-17 · 2 comments

How it came up

The owner’s second example program:

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)
   ...
}

Today both claims about b are reported checked at run time: b is not a whole number the prover reads. The cause:

• total is changed by the loop;
• the prover reads only names that do not change (ADR-269 D9);
• ADR-269 D16 stops at a loop, and its §6 left loop invariants to a later record.

The same program also showed a checker hole, [0..181] printed as a range. That is #638.

Checked before deciding:

• ADR-269: loop invariants are left open there.
• ADR-270:
  • three layers, and the logic layer knows no Nikaia syntax;
  • queries are self-contained, and every proof has a certificate;
  • the search is free, and a build uses the committed nikaia.proofs;
  • a strategy layer;
  • the logic is a public package.
• ADR-306 D7: an inductive bound, kept only where it carries itself.
• ADR-314 §2: SPARK unrolls short loops; Dafny and Wuffs need written invariants.
• #599 point 4: “state or infer loop invariants and prove initialization, preservation, and the loop-exit consequence”, plus the balance between user invariants, inference and search.

The decision in short

The owner decided this in four rounds. ADR-361 gives the reasons; Part III 13.2, 13.3 and 14.2 give the rule.

• D1, the form: a loop is a problem in Horn clauses, written in the logic layer without Nikaia syntax. It is public, so #599 and outside tools can use it too. SMT-LIB HORN is used at the edge. break, continue and return are each a way out of their own.
• D2, when it is asked: a claim that reads a name a loop changes, and is left open without the loop, is asked once more through the loop. Only the claim that needs it pays.
• D3, writing invariants: nobody has to write one, because the compiler finds it. An assert in a loop is a claim by the flow and by the names it reads, not by its place in the body. Once proved, it is a fact the search may use.
• D4, checking: every invariant used is checked with three queries and their certificates: it holds at entry, a turn keeps it, and with each way out it gives the claim. It is kept in nikaia.proofs together with its origin. The origin never decides whether it is believed.
• D5, the portfolio: strategies are added one by one:
  1. closed forms;
  2. intervals and octagons;
  3. k-induction;
  4. guess and check;
  5. PDR/IC3, when the others are exhausted and we are ready.
• D6, proposers: programs named in [prove] proposers, for example an LLM, a learner from test runs, or another solver.
  • They run only under nikaia prove --propose, never in a build.
  • They receive the open loop problems and answer with candidate invariants, and each candidate goes through D4.
  • Code leaves the machine only through that command.
  • The exchange (round 4, 0.0.998): each proposer runs as a child process, with one JSON line per problem in each direction, the way protoc plugins and language servers work. HTTP and MCP were rejected; ADR-361 §3 gives the reasons.
• D7, the report: --asserts names the invariant and its origin, or the loop and the names it changes.
• Unrolling for special cases is #639.

To build

1. The loop’s form in the logic layer (D1). Add a language-neutral type to the logic .nika files for a loop problem:
   • state names;
   • entry facts;
   • condition;
   • the step relation over primed names;
   • the exits;
   • goals at points.

   Add SMT-LIB HORN export next to logic_smtlib.nika. Tests: the problem of §1 written out, and its SMT-LIB text.

2. Checking an invariant (D4). One operation turns a loop problem plus a candidate into the three queries, and answers proved only when all three come back proved with certificates. Store the invariant and its origin in the nikaia.proofs entry. Tests:
   • a true invariant passes;
   • an invariant that holds at entry but is not kept by a turn fails;
   • an invariant that is kept but too weak for the goal fails.
3. Translating loops in the frontend (D1, D2). Turn a while or a for whose body changes names that an open claim reads into the loop problem. break, continue and return become exits. Ask only for a claim left open, as ADR-359 D2 does.
4. Closed forms (D5.1). A name changed by the same constant on every path of a turn becomes start + k·n, with a fresh n >= 0. A counter with condition i < a and step +1 ends at i == a when a >= start, and otherwise stays at its start. Tests:
   • the owner’s program with b > 40 and b < 181 proved;
   • a loop with break where the end value must not be claimed;
   • a countdown;
   • two counters with different steps.
5. Intervals (D5.2). Intervals with widening, and each bound confirmed through step 2. Tests: while x < 100 { x = x + 3 } gives x <= 102.
6. The report (D7). --asserts names the invariant and its origin for a claim proved through a loop, and the loop and the names it changes for one left open. Keep the red/light-blue/green groups from 0.0.990.
7. Measure. Count instructions with callgrind over lower-std and the standalone files; the limit is at most +5 %. Check every new refutation by hand.
8. Proposers (D6, Part III 13.2 and 13.3). Build [prove] proposers = ["cmd arg", …] in the manifest, nikaia prove --propose, and --propose=CMD for a single run. The exchange:
   • Start each proposer once as a child process.
   • Write one JSON line per open loop problem to its stdin: {"version": 1, "id": …, "problem": …, "source": …, "names": […]}. problem is SMT-LIB HORN, source is the loop’s source text, names are the names it reads. Close stdin after the last line.
   • Read one JSON line per answer from its stdout: {"id": …, "candidates": […]}. Each candidate is an SMT-LIB term over the names.
   • Show the proposer’s stderr to the user.
   • Skip a proposer that crashes, ends early, or writes a line in another shape; the other proposers and the built-in strategies continue.
   • D4 checks each candidate. Write the ones that pass to nikaia.proofs, with the proposer as their origin.

   Tests, with a stub proposer written in Nikaia and run with nikaia run:

   • one true and one false candidate: only the true one is written;
   • a proposer that crashes: the run continues;
   • a line in the wrong shape is skipped;
   • an unknown version is refused with a message;
   • nikaia build never starts a proposer;
   • --locked reads the written entry.
9. Later, each as its own step: octagons, k-induction, guess and check, and PDR when D5 says.

Steps 1-7 close the owner’s program. Step 8 is the LLM interface. Step 9 stays open after that.

Comments

keywan-ghadami, 2026-10-17

Status after d3d27e2 (steps 1-2) and 8bfd1a0 (steps 3-6, while only). The owner’s program has assert(b > 40) and assert(b < 181) proved through the loop, with the invariant i >= 0 && total >= 0 && 10 * i == total && i < a + 1 found by closed forms.

Still missing for steps 1-7:

1. Step 3, for loops. Only while is translated today (prover_loops.nika, loop_record). prover_for only forgets what its body changes.
2. Step 2, the invariant’s own line in nikaia.proofs. The three queries are recorded as ordinary entries. A line KEY invariant origins;smt-term (an Entry::Invariant in proofs.rs, the invariant kind accepted by pb_read, with ProverState.invariants_noted filled in through_loops and handed over in prove.rs) was written and then taken out unbuilt. Rebuild it from that description and add a test with a project build.
3. Step 4 test, two counters: the test uses steps +1/-3. With +2/-5, i == 10 is not proved: it needs parity, and Fourier-Motzkin tightening does not find it.
4. Step 7, the counts.
   • 26 standalone files (benches/, examples/) with the new binary: 3 844.1 M instructions. No baseline was counted.
   • lower-std was not counted.
   • No new refutation can come from a loop, because loop facts are never used to refute. A let mut now gives facts until its next assignment, so new NK1207s are possible. lower-std raised none, but the corpus has not been checked yet.
5. The counters: NIKAIA_PROVER_COUNTS prints loop claims and loop queries. For the owner’s program it printed 64 / 192: the invariant is found again on every fresh ProverState, that is each prove() round and each check. It could be cached across rounds.
6. Lowering defect: D45 is filed in docs/lowering-defects.md.

---

Generated by Claude Code

keywan-ghadami, 2026-10-17

State after 0.0.1002:

• while (8bfd1a0, package.rs regenerated in 184e2fb) and for over a range (fbfeef9) read through the invariant. Verified on develop 02363f6: prove_loops, logic_horn, prove, assert, main_parameters pass; the owner’s program proves b > 40 and b < 181 “through the loop”, and nikaia run main.nika -- 5 prints Hello, Nikaia! 110 1 110.
• A for over a list or map stays open by design (ADR-361 “not decided here”: quantified facts).
• let mut followed through every assignment outside loops is #642 (ADR-361 D9).

Still open here:

1. Step 2: the invariant’s own line in nikaia.proofs (with the strategy that found it); today only the three queries are recorded.
2. Step 7: baseline counts — callgrind of the standalone files and lower-std before (409af5d) and after; the new binary alone was 3 844.1 M on 26 files. The invariant is found again for every fresh ProverState (64 loop claims, 192 loop queries on the owner’s program): a cache may be needed for the 5 % limit.
3. Step 8: proposers.

---

Generated by Claude Code

Back to Open Issues