Result: partial
Files: assets/badges/self-hosted.svg crates/nikaia-std/src/tools/check_facts.nika crates/nikaia-std/src/tools/lowered.rs crates/nikaia-std/src/tools/lowered/check_facts.rs crates/nikaia-std/src/tools/lowered/prover_loops.rs crates/nikaia-std/src/tools/lowered/prover_scope.rs crates/nikaia-std/src/tools/lowered/prover_state.rs crates/nikaia-std/src/tools/lowered/prover_walk.rs crates/nikaia-std/src/tools/prover_loops.nika crates/nikaia-std/src/tools/prover_scope.nika crates/nikaia-std/src/tools/prover_state.nika crates/nikaia-std/src/tools/prover_walk.nika tests/compiler/tests/prove_an_assert_false_at_a_turn_of_its_loop_is_refused.nika tests/compiler/tests/prove_an_assert_false_at_a_turn_of_its_loop_is_refused.stderr tests/compiler/tests/prove_an_assert_inside_a_loop_is_asked_through_it.nika tests/compiler/tests/prove_an_assert_inside_a_loop_is_asked_through_it.stdout
Commit: prover: an assert inside a loop body is asked through the loops it stands in (ADR-361 D2, D3)
Body: At the head of each turn the walk ties every state name of the loop’s record to name^S (loop_turn_name, prover_turn_ties in prover_walk.nika, for a while and a for over a range) and keeps the record in the new ProverScope.around, outermost first. An assignment since moves the tie into the history (D9); a name bound again drops it. A claim still open is asked with each enclosing loop’s invariant at that head (loop_turn_facts), the facts before the loop, the condition and the path from the head; the invariant search moved out of through_loops into ProverState::loop_invariant, shared with the claims past a loop and cached as before. --asserts says proved inside the loop that changes ... and counts it under through a loop. Probed sound: a claim false at the last turn, after an assignment in the body, in a nested loop, after a jump the invariant does not cover: all stay refused.
Part: #1054
Pushed: rejected (7f13fa5d committed locally on develop)
Tests: the new test’s functions f, h were refused NK1300 by the unfixed compiler (probe at the start of the run, same bodies); prove_an_assert_inside_a_loop_is_asked_through_it now passes (4 claims proved, 3 of them inside a loop) and prove_an_assert_false_at_a_turn_of_its_loop_is_refused (assert(i < 3) in h(5)) stays refused; it:: assert:: assume:: facts_at_calls:: field_paths:: integer_types:: main_parameters:: prove:: prove_through_loops:: unproved_claims:: 105 passed; step 2 probe check --bounds --optimization prove-through-loops:on: j += 1 in f still checked (see Needs); step 3 logic_search.nika bounds ... 12 indexes, 4 proved; 6 operations, 3 proved after, the same before (this change touches no file of the bounds walk); lane figure unchanged from p1 (1,535 indexes, 726 operations at prove-through-loops:on) for the same reason
Gate: green
Deviation: step 2 not built: the bounds walk (bounds_walk.nika, bounding_loop_guesses, bounding_fits) cannot prove j += 1 in f by any invariant
Found: none
Needs: architect decision on step 2 (D10). Two causes, probe in the commit’s tests’ f and in fn k() { let mut i = 0; let mut s = 0; while i < 10 { s += 1; i += 1 } }: (1) the bounds walk’s candidates are only halves of the entry facts (bounding_loop_guesses), never the prover’s closed forms, so s == i (needed for s += 1 in k) is never guessed: D10 says “through the loop’s problem (D2)”, but the bounds walk has its own guess-and-check, not a LoopRecord; feeding it the prover’s invariants or loop_candidates is a design choice; (2) bounding_fits asks j + 1 <= solvable() (2^62), so with an unbounded parameter n even i += 1 under while i < n (no invariant needed) is not proved: f’s j += 1 would need n’s type bound as a fact and the goal at the type’s maximum
Changelog: An assert inside a loop body that reads a name the loop changes is proved through that loop’s invariant at the head of the turn, with the loop condition and the path from the head (ADR-361 D2, D3); before, only a claim after the loop was.
Owner: none
Disk freed: 0 GB (cache 1.3G, 23G free; new entries over 100 MB: rlib 265+265, run-bundle 286, build-time-bundle 484 MB)
Rs2nika: none
