Issue #642: The prover follows a `let mut` through each assignment (ADR-361 D9)

ready · opened 2026-10-17 · updated 2026-10-17 · 1 comment

How it came up

For the owner’s loop program (#640), the prover had to read let mut i = 0 and let mut total = 0, or it would not know the loop’s start. Commit 8bfd1a0 made a let mut a name of the prover until its first assignment (where no call is handed it and no lambda changes it); after an assignment outside a loop, it forgets it. Part III 14.2 and ADR-269 D9 said only “bindings that do not change”, so the build went past the text.

let mut x = 0
assert(x == 0)   // proved today: x has not changed yet
x = x + 1
assert(x == 1)   // checked at run time today; proved after this issue

Decision (owner, 2026-10-17)

Option B: follow every assignment, the static single assignment form Dafny, SPARK, CBMC and Kani use. Before the first assignment no SSA is needed: the binding has not changed (as built). Rejected: knowing a let mut only until its first assignment.

Why: ADR-361 D9; ADR-269 D9 notes the change.
What: Part III 14.2, What the prover reads.

To build

An assignment x = e to a tracked let mut (no call handed it, no lambda or deferred body changes it) gives x a new name with e’s value over the old one; compound assignments (+=, -=, *= by a constant) likewise. Test: x = x + 1; assert(x == 1) proved; x = x * 3; assert(x == 3) after x = 1 proved.
After an if/else that changes x on one side or both, x is either side’s value with that side’s condition (a disjunction over the branch condition), and an if without else keeps the old value on the other side. Test: if c { x = 1 } else { x = 2 }; assert(x >= 1 && x <= 2) proved; assert(x == 1) not proved.
A match arm that changes x forgets it after the match (as today), unless the arms are read; not required here. A loop keeps reading through its invariant (#640).
A binding handed to a call (f(ref mut x) or any mut parameter) or changed from a lambda stays out, from its let on. Test: such an x after x = 1 gives no fact; never a false proof.
A claim decided without the new names never pays: second query only for a claim left open (ADR-361 D2). Counters: NIKAIA_PROVER_COUNTS before/after on the standalone files and lower-std; callgrind ≤ +5 %.
Refutations: a claim the assignments make false is NK1207 only under ADR-269’s rule for what reaches; check every new NK1207 in the corpus by hand.

Related: #640 (loops), ADR-269 D9, D16.

Comments

keywan-ghadami, 2026-10-17

Steps 1-2 built in 4cc925d (0.0.1009): an assignment (=, +=, -=, *= by a constant) and an if/else are followed with SSA names (x#<byte>); an old value known to be a number is substituted, so a loop after it still knows its start. The new facts are asked only for a claim still open (a second query), and used for refutation and a loop’s entry. The owner’s program’s prover counters are unchanged. Tests: crates/nikaia/tests/prove_mutables.rs (8).

Still open:

preconditions and index bounds at a call read only the ordinary facts, not the history;
a loop after x was assigned from another variable (not a known number) finds no invariant;
steps 3-6 of the list (match arms, the measurement, refutations checked by hand).

Generated by Claude Code

Back to Open Issues

Issue #642: The prover follows a let mut through each assignment (ADR-361 D9)