Result: done
Files: crates/nikaia-std/src/tools/prover_loops.nika crates/nikaia-std/src/tools/lowered/prover_loops.rs crates/nikaia-std/src/tools/lowered.rs docs/specification/30-nikaia-tooling.md assets/badges/self-hosted.svg tests/compiler/tests/prove_a_constant_step_loop_needs_no_turns.nika tests/compiler/tests/prove_a_constant_step_loop_needs_no_turns.stdout tests/compiler/tests/prove_a_throw_in_a_loop_is_an_exit.nika tests/compiler/tests/prove_a_throw_in_a_loop_is_an_exit.stdout tests/compiler/tests/prove_an_unread_whole_let_in_a_loop_is_a_name.nika tests/compiler/tests/prove_an_unread_whole_let_in_a_loop_is_a_name.stdout tests/compiler/tests/prove_turn_indexed_intervals_cover_sixteen_turns.nika tests/compiler/tests/prove_turn_indexed_intervals_cover_sixteen_turns.stdout tests/compiler/tests/prove_turn_indexed_intervals_of_a_for_range.nika tests/compiler/tests/prove_turn_indexed_intervals_of_a_for_range.stdout tests/compiler/tests/prove_turn_indexed_intervals_of_a_while_counter.nika tests/compiler/tests/prove_turn_indexed_intervals_of_a_while_counter.stdout tests/compiler/tests/prove_turn_indexed_intervals_reach_the_caller.nika tests/compiler/tests/prove_turn_indexed_intervals_reach_the_caller.stdout tests/compiler/tests/prove_turn_indexed_intervals_stop_at_sixteen_turns.nika tests/compiler/tests/prove_turn_indexed_intervals_stop_at_sixteen_turns.stderr tests/compiler/tests/prove_turn_indexed_intervals_through_a_throw.nika tests/compiler/tests/prove_turn_indexed_intervals_through_a_throw.stdout
Commit: prover: per-turn interval candidates for a loop of at most 16 turns, a throw as a loop exit (ADR-361 D12)
Body: Steps 2-4 in one commit, built from the spike 09a7d79f. Kept: LoopTurn per turn path, loop_unrolled (counter from a known start by a constant to a literal limit, at most 16 turns; for each other whole-number state name with a known start one candidate per turn, counter > start + j*k || lo_j <= x <= hi_j), loop_atoms, loop_whole_let (a typed or cast whole-number let nothing reads is a fresh name), throw as a way out like return. Not taken from the spike as it was: the extra Houdini rounds (4 -> 4+16) now go only to a loop that got turn-indexed candidates (ADR-258 D2); the falsum queries that drop dead turn paths are counted in asked; new functions are declared sync (#1014). One addition: the spike proved nothing past 6 turns, because the final check asked the turn query of the whole invariant as one query and the solver ran out of its 1024 cases (TooManyCases, found by instrumenting proofs.rs for one run, then removed). lg_loop_check’s queries now go through loop_proved_each, which asks a conjunction goal part by part under the same facts, each with its own certificate (the last Houdini round already proved exactly these). With that, 16 turns are proved and 17 are not proposed. --asserts names the origin as “turn indexed intervals”. There is no Rust test for the 17-turn case under unproved-claims = “warn”, because a test program cannot set the manifest; the test is a refusal (.stderr, NK1300) instead. e_caller is not a test: it stays open, because its callee has no assert and ADR-359 D1 result summaries do not read a body with a loop, and its untyped let d = ds[k] is y7b. c_acc_for (also untyped) stays open for the same reason. Part of #1003.
Fixes: #639
Part: #1003
Pushed: 204c5836 (pushed by drive.nika)
Tests: pre-flight on develop’s compiler: a_const already proved by closed forms (not open, unlike the brief’s sketch), b2_typed open (NK1300); c2_typed, d_throw and e2_post were open too. 7 of the 9 new tests/compiler programs fail on the unfixed compiler (NK1300); prove_a_constant_step_loop_needs_no_turns (a baseline) and prove_turn_indexed_intervals_stop_at_sixteen_turns (open on purpose) pass on both. nikaia test --both-settings --project tests/compiler: 377 passed. it -- prove unproved_claims plus the guard set: 151 passed, 1 failed (sequences, see Found). Clippy clean, pre-push-check clean.
Gate: red
Deviation: none
Found: it sequences::the_corpus_has_no_more_unanswered_method_calls_than_it_had is red on develop 7c0ff303 without this change (18 against a ceiling of 16, also with prover_loops.nika put back to HEAD); this commit adds none
Needs: supervisor rebase and push of 204c5836 (push rejected, develop moved)
Changelog: The prover follows a loop of a constant number of turns, at most 16, turn by turn: each whole-number name it changes gets one interval per turn, each checked as an invariant, so n = n * 16 + d over four turns proves n <= 0xFFFF; a throw in a loop body is a way out of the loop, and a whole-number let the prover does not read is a name of its own (ADR-361 D12).
Owner: none
Disk freed: 0.04 GB (scratch binary copies; nikaia-project-tests 5.8G, new entry over 100 MB: run-bundle/b2db8b4e959f1cfc 341 MB; disk 11G free)
Rs2nika: none
