A loop bound that MIR folds into a debug-info constant cannot be named in `invariant!`: `let n = 10; while i < n` fatally errors with "not a live variable", and under shadowing the name silently binds to the wrong variable

[coord-e]

Summary

local_of_name_in_bb (src/analyze/local_def.rs:794-819) resolves an invariant! parameter name by scanning body.var_debug_info and skipping every entry whose contents is VarDebugInfoContents::Const. rustc's SingleUseConsts MIR pass rewrites a const-initialized local that has a single use into exactly that shape — debug n => const 10_i64, with no Place left — so a plain

let n = 10;
while i < n { thrust_macros::invariant!(|i: i64, n: i64| .. ); .. }

has no resolvable n. Two things follow:

1. n alone in scope → fatal error. Thrust aborts with loop invariant refers to \n`, which is not a live variable at the loop header, even though n` is in scope and read at the loop header on every iteration. The invariant cannot be written at all.
2. Another n in scope → silent misbinding. The Some(_) => fatal ambiguity guard right below only counts Place entries, so a shadowed outer n is picked with no diagnostic, and the loop is verified against an invariant over a different variable than the one written.

The sibling resolver for ghost terms, operand_of_name (src/analyze/basic_block.rs:1009-1039), already handles this case — it maps a VarDebugInfoContents::Const entry to Operand::Constant. Only the loop-invariant path drops it, which is what makes this look like an oversight rather than a design decision.

Reproduction

repro.rs — an ordinary counted loop, no annotations beyond the invariant:

fn main() {
    let n = 10_i64;
    let mut i = 0_i64;
    let mut sum = 0_i64;
    while i < n {
        thrust_macros::invariant!(|i: i64, n: i64, sum: i64| 0 <= i && i <= n && sum == i * 2);
        sum += 2;
        i += 1;
    }
    assert!(sum >= 0);
}

$ cargo run --quiet -- -Adead_code -C debug-assertions=false repro.rs
error: loop invariant refers to `n`, which is not a live variable at the loop header

error: aborting due to 1 previous error

Spelling the bound literally in the invariant (i <= 10, dropping the n parameter) verifies the very same loop:

$ cargo run --quiet -- -Adead_code -C debug-assertions=false repro_literal.rs && echo safe
safe

The MIR Thrust analyzes

-Zdump-mir=main on the failing program, runtime-optimized (the body tcx.optimized_mir returns):

scope 1 {
    debug n => const 10_i64;      // <- no Place, so local_of_name_in_bb skips it
    let mut _1: i64;
    scope 2 {
        debug i => _1;
    }
}

Turning the responsible pass off makes the same file verify unchanged, which pins the mechanism:

$ cargo run --quiet -- -Adead_code -C debug-assertions=false \
    -Zmir-enable-passes=-SingleUseConsts repro.rs && echo safe
safe

Evidence matrix

All at -Adead_code -C debug-assertions=false, thrust @ 10fa12d, z3 5.0.0, default solver config. Every row is the same loop with the same invariant 0 <= i && i <= n; only how n is bound changes.

how n is bound	debug n => in optimized MIR	result
let n = 10;, read only by the loop condition	const 10_i64	fatal: "not a live variable"
let n = 10; let m = n; (second use keeps the local)	_2	safe
let n = ten(); (#[thrust::trusted] #[ensures(result == 10)])	_2	safe
fn count(n: i64) — a function parameter	_1	safe
let n = 10;, single use, -Zmir-enable-passes=-SingleUseConsts	_2	safe

So whether an invariant can mention a value depends on how many times unrelated code happens to read it.

Second symptom: the ambiguity guard is defeated, and the name binds to the wrong variable

E4.rs — an outer n shadowed by the loop's own n:

fn main() {
    let mut n = 100_i64;
    {
        let n = 3_i64;
        let mut i = 0_i64;
        while i < n {
            thrust_macros::invariant!(|i: i64, n: i64| 0 <= i && i <= n);
            i += 1;
        }
        assert!(i == 3);
    }
    n += 1;
}

$ cargo run --quiet -- -Adead_code -C debug-assertions=false E4.rs
error: verification error: Unsat

The inner n is the single-use const and is skipped; the outer n is a live loop-carried local, so it is what the invariant's n binds to. The invariant becomes i <= n_outer, the loop exit yields only i >= 3 && i <= n_outer, and the correct assert!(i == 3) is rejected. Written with the bound as a literal (while i < 3, i <= 3) the identical program is safe.

That this is a misbinding and not an ordinary Unsat is visible by turning the pass off — the diagnostic the code deliberately implements for exactly this situation then fires:

$ cargo run --quiet -- -Adead_code -C debug-assertions=false \
    -Zmir-enable-passes=-SingleUseConsts E4.rs
error: loop invariant refers to `n`, which is ambiguous at the loop header: multiple live
variables share this name (e.g. through shadowing). Rename the variables to disambiguate.

The guard cannot see the shadowing it was written to catch, because one of the two bindings is a Const entry it skipped.

Scope

Nothing here is &mut-, container- or solver-specific; it is name resolution for annotations, so it hits the first counted loop anyone writes an invariant for. It is also not limited to let n = <literal>: at -C opt-level=1 const-propagation folds far more locals into debug-info constants, and loops that verify at the default opt level start failing the same way — e.g.

let n = 3_usize;         // two uses, so `debug n => _2` at -C opt-level=0 → safe
let mut i = 0_usize;
while i < n {
    thrust_macros::invariant!(|i: usize, n: usize| i <= n);
    i += 1;
}
assert!(i >= n);

is safe by default and error: loop invariant refers to \n`, which is not a live variable at the loop headerat-C opt-level=1, where its MIR carries debug n => const 3_usize. (-Zmir-enable-passes=-SingleUseConstsdoes not rescue the-C opt-level=1` cases; other passes fold the same way.)

One -C opt-level=1 failure with the same message has a different cause and is not covered by a fix here: when the optimizer rewrites every *p access of a let p = &mut x back to x, p becomes dead at the loop header, so bty.param_of_local legitimately finds nothing. That one is about optimized MIR erasing the reference, not about Const debug info.

Suggested direction

Make local_of_name_in_bb mirror operand_of_name instead of ignoring half the debug info: let it resolve a name to either a basic-block parameter local or a VarDebugInfoContents::Const, and count both kinds toward the ambiguity check so shadowing is still reported.

build_invariant_precondition (src/analyze/local_def.rs:851-905) then needs its mapping: Vec<rty::FunctionParamIdx> widened to a vector of chc::Terms, so a name that resolved to a constant substitutes that constant (chc::Term::int(..), as const_ty/const_value_ty already build elsewhere) rather than a parameter variable. A constant is not loop-carried and is not havoc'd, so no predicate argument is needed for it — which is also why the literal spelling works today.

Environment

• thrust @ 10fa12d (clean tree)
• rustc 1.91.0-nightly (12eb345e5 2025-09-07) (nightly-2025-09-08, per rust-toolchain.toml)
• Z3 5.0.0 (x64-glibc-2.39, the version .github/actions/setup-z3 pins), default THRUST_SOLVER_ARGS