A variable read only by an invariant! or ghost! term is dead to MIR liveness and gets pruned, so it cannot be named: "not a live variable" fatal error on correct programs (entry-value snapshots, ghost histories) #343

Summary

Basic-block parameters and implicit drop points come from MIR liveness (MaybeLiveLocals, used in refine_basic_blocks in src/analyze/local_def.rs). A spec term does not count as a use. The invariant!/ghost! marker call only receives the formula-fn item, so a variable that only the spec mentions is dead as far as MIR is concerned. It is pruned from the env and from the basic-block parameters.

The two name resolvers then refuse it:

• local_of_name_in_bb, for invariants, only accepts locals that have a bty.param_of_local.
• operand_of_name, for ghosts, only accepts locals for which is_defined holds.

So writing a spec over such a variable is a fatal error, even though the variable is in scope and holds the right value. Whether a spec may name a variable then depends on whether ordinary code happens to read it later.

This is a different mechanism from #257. That issue is about SingleUseConsts folding a local into a VarDebugInfoContents::Const. Here the variable is an ordinary Place local that is simply dead.

Reproduction 1: snapshot of an entry value used by an invariant

#[thrust_macros::requires(true)] #[thrust_macros::ensures(true)] #[thrust::trusted]
fn rand() -> i64 { unimplemented!() }

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

error: loop invariant refers to `start`, which is not a live variable at the loop header

If you add assert!(x == start + 20); after the loop, start becomes live and the program verifies. With start + 22 it is correctly Unsat.

Reproduction 2: a ghost over a variable that is not used afterwards

use thrust_models::Ghost;
#[thrust_macros::requires(true)] #[thrust_macros::ensures(result > 0)] #[thrust::trusted]
fn rand_pos() -> i64 { unimplemented!() }
#[thrust_macros::requires(g > 0)]
fn check(g: Ghost<i64>) {}

fn main() {
    let a = rand_pos();
    let g = thrust_macros::ghost!(|a: i64| -> i64 { a });
    check(g);
}

error: ghost term refers to `a`, which is not a live variable here

• Adding assert!(a > 0); after check(g) makes it verify.
• The existing ghost tests pass only because the named variable is defined in the same basic block as the ghost, so it has not been dropped yet.

Practical impact

This rules out building a ghost history step by step, which is the usual pattern:

let h = ghost!(|| -> Seq<Int> { Seq::empty() });
let h2 = ghost!(|h: Seq<Int>, x: i64| -> Seq<Int> { h.push(x) });

Here h is dead after it is consumed, so h2 cannot be formed unless h is used again by dummy code. The same goes for "remember the old value" invariants, which are the most common kind.

Suggested direction

Count the variables an invariant!/ghost! formula fn names (they are already resolved by name via var_debug_info) as uses at the marker's location when computing liveness and drop points. Then they stay in the env and the block parameters up to that point.

Environment

• thrust @ 187a1e9
• rustc nightly-2025-09-08
• Z3 5.0.0, plus PCSat for the Seq variant