Incompleteness: an explicit `invariant!` havocs live locals it doesn't mention, even when the loop never modifies them, wrongly rejecting safe programs

[coord-e]

Summary

When a while loop carries a user-supplied thrust_macros::invariant!, any local variable that

1. is live at the loop header,
2. holds a non-singleton value (a computed value such as n + 5, or a variable that has been assigned more than once — a "flow" local), and
3. is not restated in the invariant,

is havoc'd (its value is forgotten) across the loop — even though the loop never reads or writes it. Any assertion about that variable after the loop then fails to verify.

A user-supplied invariant fully replaces the inferred loop precondition, but the framing that the inference path performs for unmodified live locals is not reproduced for non-singleton locals, so their value is dropped. Singleton locals (a plain constant like let x = 5;, or a direct copy let x = n;) are carried through the frame and preserved, which makes the asymmetry visible.

This is a soundness-preserving over-approximation (incompleteness), not an unsoundness — the variable is left unconstrained, not set to a wrong value (assert!(x == v) and assert!(x != v) are both rejected, while assert!(x == v || x != v) verifies).

Minimal reproduction

//@compile-flags: -C debug-assertions=false

#[thrust::callable]
fn c(n: i64) {
    let x = n + 5;                       // x holds a *computed* value
    let mut j = 0_i64;
    while j < 3 {                        // loop never reads or writes x
        thrust_macros::invariant!(|j: i64| j >= 0 && j <= 3);
        j += 1;
    }
    assert!(x == n + 5);                 // holds in real Rust
}

fn main() {}

Expected: safe — x is never touched by the loop, so x == n + 5 at the assertion.
Actual:

error: verification error: Unsat

error: aborting due to 1 previous error

Isolation

All variants below differ only in the marked line; each was cross-checked (a flipped assert! is correctly rejected, and assert!(x == v || x != v) verifies, confirming x is havoc'd, not miscomputed).

Case	Verdict
computed value let x = n + 5; + explicit invariant! omitting x	Unsat (bug)
same, but no explicit invariant (inference) — while j < 3 { j += 1; }	safe ✅
flow local let mut sum = 0; sum += 5; + explicit invariant! omitting sum, then assert!(sum == 5)	Unsat (bug)
constant let x = 5; (single assignment) + explicit invariant! omitting x	safe ✅
direct copy let x = n; + explicit invariant! omitting x	safe ✅
computed value, invariant restates it: invariant!(|j, sum| ... && sum == 5)	safe ✅

So the trigger is precisely: a live, non-singleton local, not modified by the loop, not restated in an explicit invariant. The inference path frames it correctly; the explicit-invariant path does not.

Aggravating factor: no workaround when the value depends on a parameter

The "restate it in the invariant" workaround only exists when the value is a self-contained constant. When the value depends on a function parameter, the frame condition cannot even be written, because the invariant closure cannot capture the parameter:

thrust_macros::invariant!(|j: i64, x: i64| j >= 0 && j <= 3 && x == n + 5);
//                                                                  ^ error[E0434]: can't capture
//                                                                    dynamic environment in a fn item

So for let x = n + 5; while … { invariant!(…) } assert!(x == n + 5); there is currently no way to make it verify.

Why this matters

The pattern "compute a value, run a loop that works on something else, then use the value" is common:

let total = base + bonus;
let mut i = 0;
while i < len { invariant!(|i: i64| 0 <= i && i <= len); /* work over i, not total */ i += 1; }
assert!(total == base + bonus);   // wrongly rejected

Likely root cause

src/analyze/local_def.rs:939-954: when a header has user invariants, the block type is built from live_locals and its precondition is set only to the AND of the user invariants (rty::Refinement::top() conjoined with each invariant!), discarding the inferred precondition entirely:

if let Some(invariants) = loop_invariants.get(&bb) {
    let mut bty = self.type_builder.build_basic_block(&self.body, live_locals, ret_ty);
    let mut inv = rty::Refinement::top();
    for &(formula_def_id, generic_args) in invariants {
        inv.push_conj(self.build_invariant_precondition(formula_def_id, generic_args, &bty));
    }
    bty.set_precondition(inv);
    ...
} else if analyze::basic_block::needs_own_precondition(&self.body, bb) {
    // inference: build_basic_block(...).for_template(...) — a precondition pvar that
    // captures the relationships of *all* live locals, so unmodified locals are framed
    ...
}

When bind_locals (src/analyze/basic_block.rs:1370-1399) then materializes the header, a live local whose sort is_singleton() is short-circuited (basic_block.rs:1390) and carried by its term; a non-singleton local's refinement comes only from the invariant precondition, so if the invariant does not mention it, it is bound unrefined ≈ havoc'd. is_non_flow_local/the singleton check (src/refine/env.rs:925, basic_block.rs:1417) is what lets constants and copies survive while computed/flow values do not.

A fix would frame live locals that the loop body does not assign (carry their incoming refinement into the invariant precondition), matching what the inference path already does.

Environment

Analyzed at af7cd99, solver Z3 (THRUST_SOLVER=z3), -C debug-assertions=false. Uses only supported features (i64, assignment, while + invariant!, assert!) — not overflow/range/unsigned, and distinct from the listed known issues.