Open and answer this issue on GitHub.
ready · opened 2026-10-31 · updated 2026-10-31 · 5 comments
agent: builder model: opus max_turns: 120 budget_usd: 25 — Facts: Where things live, Traps already met, Commands
Goal (owner, 2026-10-31): 100 % of the indexes and arithmetic steps in the compiler’s Nikaia code (crates/nikaia-std/src/tools/*.nika) proved, not a share. This is claim (b) of docs/formal-verification.md (#796, decided 2026-10-24). The lane is docs/briefs/prover/, and its state is docs/briefs/prover/state.md.
target/fast/nikaia, 2026-10-31, d206915)nikaia check --bounds on each of the 246 files on its own gives 1,821 indexes, 965 proved (53 %); 1,381 operations, 560 proved (41 %). That figure is not reliable: the check refuses 227 of the 246 files, because the types and functions from the package’s other files are unknown to it (NK1135, NK1117…). So sites inside code it cannot type are missing from the count (indexed.atoms[atom] in logic_search.nika:63 is not listed, for example). The figure in formal-verification.md (1,473 / 802, 1,101 / 491) dates from 214 files.
Why the remaining checks stay, from the same run: 1,580 fall under the catch-all no fact bounds what it reads, 57 under a call’s result, 27 under list of lists, 6 under product of two unknowns, 3 under field. 281 of the unproved operations are x += 1 counters.
while i < n { assert(i >= 0); i += 1 } is refused, while the same claim after the loop is proved with the invariant found by closed forms. Filed as #1054.if c { n += 1 }) gets no bound relative to the loop’s counter (n <= i). ADR-361 D5 item 2 (intervals and octagons) decides it, but it is not built.docs/briefs/prover/state.md)nikaia lower-std --bounds prints the --bounds report of each tools file as the package lowers it, and scripts/proved.nika sums the report and sorts it by reason and by file. The figure goes into formal-verification.md §2/§4. (brief p1)if value, a parameter, an element read from a list, a field, a length of another list), each naming its issue. (brief p3)n - n@ <= k·(i - i@)) for a name that grows on some paths of a turn, and a for loop’s turns bounded by its list’s length (ADR-361 D5, ADR-306 D12; #432 for the loop case).logic_search.nika lg_verify, lg_follow, lg_replay, lg_replayed; the Farkas and rounding steps in logic_lia.nika): preconditions such as assert(at == made.len()), and guards that reject a malformed certificate instead of stopping.asserts in the compiler’s code where they state an invariant the prover then uses, file by file, until each file reaches zero unproved checks.formal-verification.md §4, docs/writing-guide.md) once measured. Later, by the score: the prover as a product of its own, and proposals from outside programs (ADR-361 D6, nikaia prove --propose).As in docs/briefs/common.part. No compiler code works around a prover gap: a gap that is not decided gets a decision issue.
Generated by Claude Code
Figure on 1ebd8fc (lower-std --bounds + scripts/proved.nika): under off, 1,493/2,583 indexes (57.8 %) and 712/1,594 operations (44.7 %); under prove-through-loops:on, 1,525 (59.0 %) and 719 (45.1 %). The headline is counted at prove-through-loops:on: claim (b) is about what is proved. 4 files were refused because the binary predates 578fd67. 1,862 of the 1,972 unproved sites have the catch-all reason. Next batch: p3 (step 3, reasons by binding), then p4 (#1054 step 2).
Generated by Claude Code
Prover lane, architect 2026-10-31 (ecf435a): figure on today’s binary, lower-std --bounds + scripts/proved.nika: off 1,518/2,628 indexes, 729/1,612 operations; prove-through-loops:on 1,550/2,628 (59.0 %), 736/1,612 (45.7 %). Unproved under on by reason: 693 catch-all, 542 counter, 379 parameter, 127 list element, 96 another list’s length, 60 call result, 37 list of lists, 7 if/match, 6 product, 4 lower bound, 3 field. Next batch: p5 #1069 (.bounds expectations, so every proof is guarded by a test), p6 step 4 (ADR-361 D13, written today: a for counts its turns; counters bounded by k times the turns). Then the certificate checker (step 5) and the asserts at the 379 parameter sites (step 8), which need the claim count in the figure (a precondition moves a check to the callers; the figure must count those too).
Generated by Claude Code
Prover lane, architect run after p6 (28acd94, 2026-10-31).
prove-through-loops:on 1,552/2,646, 740/1,620. Counter reason 541 (on).for over a range gets a turn limit, because the checker records a collection’s length only for .len() receivers. Decided (architect, obvious, no language change): check_core_stmt_for records the iterable in std_lengths/sized_lengths (brief p7).for c in text over a String passes check, fails in rustc), #1074 (tools lowering of ref T? ?? ref T, p6’s Found), both for the bug lane.lower-std --asserts, proved.nika counts claims and the 13 panics, left at run time, formal-verification.md §2/§4). Then the prover walk’s for turn count (claims after for x in xs { n += 1 } cannot read n today).Generated by Claude Code
Prover architect, 2026-10-31, after p11 (3ebe381, #1090) and p9 (9e657f7, claims and panics in the figure), both pushed.
Figure (21:11 binary at 9e657f7, lower-std --bounds --asserts --optimization prove-through-loops:on + scripts/proved.nika): 1,576 / 2,677 indexes (58.9 %), 846 / 1,633 operations (51.8 %), 0 claims, left at run time: 1891 (off: 1,543 / 2,676, 840 / 1,633, 1,929).
Decided (ADR-385, obvious under Language decisions): D1 every length is at most 2^63 - 1 for a proof, sized or not (while i < xs.len() { i += 1 } over zero-size elements is checked today); D2 a std sequence’s ledger entry may state its count (ensures_count: split >= 1, chars between len/4 and len, bytes = len), read at collect(), count() and a for.
Next batch: p12 (D1, and lists of a struct declared in another tools file taken as unsized: cexport.nika :179 index += 1 checked where the same shape proves in one file), p13 (D2, and the panic count: modules.nika’s panic( is in generated text, so 2 panics, not 3). After: #388’s fill case (two lists pushed together), the catch-all re-split, the certificate checker. State: docs/briefs/prover/state.md.
Generated by Claude Code
Prover lane lands (owner, 2026-10-31). State: docs/briefs/prover/state.md; how a session restarts the lane is written there.
Figure (after p12, ae09d77; lower-std --bounds --asserts + scripts/proved.nika): off 1,544 / 2,677 indexes (57.7 %), 923 / 1,633 operations (56.5 %), left at run time 1,846; prove-through-loops:on 1,576 / 2,677, 929 / 1,633 (56.9 %), left 1,808. Start of the lane: 1,929 / 1,891 left.
To build, status: 1 done (p1, lower-std --bounds, scripts/proved.nika); 2 done (#1054); 3 first half done (reasons, p3), second half is #1105; 4 done for for/while counters (p6, p7, p12, ADR-361 D13, ADR-385 D1), the relational candidate for counters grown on some paths (ADR-361 D5 item 2) is still open; 5 is #1104; 6 open: ADR-385 D2 is #1103, #388 fill case (comment there), #384, #385, #386, postconditions on a program’s own function (61 call-result sites, needs a decision paper when reached); 7 open (#797, #798); 8 open (parameter asserts, 382 sites); 9 the honest claim in formal-verification.md §4 carries today’s figure.
Order: #1103 (brief p13 written), #388 fill decision, #1105, #1104, then 6-8 by the score. wip removed: no lane holds it until the lane restarts.
Generated by Claude Code