Unsound: moving a `&mut`-capturing closure out of any aggregate (incl. `enum`/`Option`), with no higher-order call, drops its prophecy and verifies panicking programs as `safe` (generalizes #177)

[coord-e]

Summary

Moving a non-Copy closure that captures a variable by &mut out of an aggregate (a tuple, a struct field, or an enum/Option variant) and then calling it silently drops the captured &mut's prophecy. The post-state collapses to a contradictory (⊥) environment — so the closure's mutation is never reflected onto the captured variable, and everything after the call verifies vacuously (including assert!(false)). Thrust reports programs that always panic at runtime as safe.

This is a generalization of #177. #177 documents the failure for a closure moved out of a tuple/struct field and passed by value to a higher-order function taking FnOnce/FnMut, and localizes it to the call-site projection check in rust_call.rs "case 3". The reproductions below show the real trigger is the move out of the aggregate itself:

• it needs no higher-order function — the closure is called directly through an ordinary local;
• it fires for enum/Option variants (a Downcast extraction), not only tuple/struct fields;
• the call goes through a projection-less local, which Unsound: moving a &mut-capturing closure out of a tuple/struct field into a by-value FnOnce/FnMut verifies panicking programs as safe #177 explicitly lists as a sound control.

Consequently a fix limited to rust_call.rs "case 3" (the if arg_closure_place.projection.is_empty() guard) would not close these holes.

Reproduction (minimal)

Both programs always panic under rustc but verify safe under Thrust. Neither uses a higher-order function or any annotation.

R1 — &mut-capturing closure moved out of an Option variant

fn main() {
    let mut x = 0i64;
    let e = Some(|| { x += 8; });   // closure captures `x` by &mut, stored in Option::Some
    if let Some(mut g) = e {        // moved out of the enum variant (Downcast projection)
        g();                        // called directly through a plain local — no HOF
    }
    assert!(x == 0);                // runtime: x == 8, so this panics; Thrust: SAFE
}

$ rustc --edition 2021 r1.rs -o r1 && ./r1 ; echo "exit:$?"
thread 'main' panicked at r1.rs:7:5:
assertion failed: x == 0
exit:101                                   # actually panics

$ THRUST_SOLVER=z3 thrust-rustc --edition 2021 -Adead_code -C debug-assertions=false r1.rs ; echo "exit:$?"
exit:0                                     # Thrust: SAFE

R2 — same failure with a struct field and no higher-order function

struct W<F> { f: F }

fn main() {
    let mut x = 0i64;
    let w = W { f: || { x += 8; } };   // &mut-capturing closure in a struct field
    let mut g = w.f;                   // moved out into a projection-less local
    g();                               // called directly — no HOF
    assert!(x == 0);                   // runtime: x == 8, panics; Thrust: SAFE
}

R3 — the ⊥-collapse tell-tale (assert!(false) verifies)

fn main() {
    let mut x = 0i64;
    let e = Some(|| { x += 8; });
    if let Some(mut g) = e { g(); }
    assert!(false);                    // ALWAYS panics; Thrust: SAFE (vacuous post-state)
}

assert!(false) passing is the tell-tale (same as #177) that the environment after the call is unsatisfiable, so any assertion is discharged.

What isolates the cause

All rows verified at commit a148b9d with Z3 4.15.4 (the version pinned by .github/actions/setup-z3). "safe" is wrong wherever rustc exits 101.

| Program (closure is || { x += 8; }, capturing x by &mut) | Thrust | Correct? |
| --- | --- | --- |
| Some(closure) → if let Some(mut g)=e { g(); } (enum, no HOF) | safe | ✗ (panics) |
| W{f:closure} → let mut g=w.f; g(); (struct, no HOF) | safe | ✗ |
| (closure,) → let mut g=t.0; g(); (1-tuple, no HOF) | safe | ✗ |
| (closure, 1) → let (mut g,_)=t; g(); (full destructure, no HOF) | safe | ✗ |
| Some(closure) → if let Some(g)=e { apply(g); } (enum, via HOF) | safe | ✗ |
| Control: let mut g = closure; g(); (never in an aggregate) | Unsat | ✓ |
| Control: let g0 = closure; let mut g = g0; g(); (local→local move) | Unsat | ✓ |
| Control: (\|\| 5i64,) → let g=t.0; let v=g(); (no &mut capture) | Unsat | ✓ |

Two facts fall out:

1. The move out of an aggregate is the trigger. A closure that is never placed in an aggregate (control rows 1–2) is handled soundly, even after a local→local move. As soon as the same closure is extracted from a tuple/struct/enum, the mutation is lost. This holds for a full destructure too, so it is not a partial-move-remnant effect (cf. Unsoundness: partially-moved locals are still implicitly dropped, resolving prophecies of moved-out &mut borrows #121/Unsound: aggregate dropped wholesale after a partial field-move double-resolves the field's &mut prophecy #122).
2. A captured &mut is required. A closure with no mutable capture (control row 3) is sound — the defect is specifically the loss of the captured &mut's prophecy.

Relationship to #177 (why this is broader)

#177's reproductions all pass the closure by value directly from the field to an HOF (apply(t.0)), so at the FnOnce::call_once terminator arg_closure_place has a non-empty projection and the guard

// src/analyze/basic_block/visitor/rust_call.rs, "case 3"
if arg_closure_place.projection.is_empty() {
    self.analyzer.drop_after_terminator(arg_closure_place.local);
}

is skipped. #177 lists "move through a projection-less local" as a sound control.

In R1/R2/R3 the closure is first moved out of the aggregate into a plain local (g) and then called; the call terminator's arg_closure_place is g (empty projection), so that guard is satisfied — yet the program is still accepted. The prophecy is therefore lost before the call, at the move-out of the aggregate, not at the case-3 call-site handling. The enum/Option variants additionally involve a Downcast extraction that #177 does not mention. So the unsoundness is not confined to the case-3 path #177 identifies.

Mechanism (what is established)

The captured &mut's prophecy obligation is not carried through when a closure value is moved out of an aggregate place (tuple element, struct field, or enum-variant field via Downcast). After the closure is invoked, the mutation performed through the captured &mut is never propagated back to the referent, and Thrust's post-state becomes ⊥ (hence assert!(false) verifies). The projection-less-origin path (closure born in a local) resolves the prophecy correctly, which is why the controls pass. This matches #177's ⊥-collapse symptom but is reached through the aggregate move-out rather than the by-value HOF call site.

Expected behavior

Moving a &mut-capturing closure out of an aggregate and calling it must resolve the captured &mut's prophecy exactly as when the closure is called from a projection-less local: after g() the referent (x) must reflect the closure's write, so R1/R2 report Unsat and R3 (with assert!(false)) reports Unsat.

Why this is unsound (not merely incomplete)

In every reproduction the program panics for its only execution (rustc exit 101), yet Thrust returns safe — a safe verdict for an always-panicking program. R3 makes the vacuous post-state explicit: assert!(false) is discharged.

Distinct from existing issues

• Generalizes Unsound: moving a &mut-capturing closure out of a tuple/struct field into a by-value FnOnce/FnMut verifies panicking programs as safe #177, but is not covered by it: Unsound: moving a &mut-capturing closure out of a tuple/struct field into a by-value FnOnce/FnMut verifies panicking programs as safe #177 is scoped to a tuple/struct field closure passed by value to an HOF, with the mechanism at the rust_call.rs case-3 call-site projection guard. These repros need no HOF, fire for enum/Option variants, and go through a projection-less local (Unsound: moving a &mut-capturing closure out of a tuple/struct field into a by-value FnOnce/FnMut verifies panicking programs as safe #177's own sound control), so the case-3 guard is satisfied and fixing only that guard would leave them unsound.
• Not Ill-typed SMT: a closure that mutates a captured variable, passed to a generic HOF spec'd with pre!/post!, has its pre/postcondition predicate declared at the FnMut receiver sort Mut<env> but applied at the bare env sort, so verification aborts with a solver sort mismatch #206: Ill-typed SMT: a closure that mutates a captured variable, passed to a generic HOF spec'd with pre!/post!, has its pre/postcondition predicate declared at the FnMut receiver sort Mut<env> but applied at the bare env sort, so verification aborts with a solver sort mismatch #206 is an ill-typed SMT abort from pre!/post! closure specs; these produce a wrong safe verdict and use no annotations.
• Not Unsoundness: partially-moved locals are still implicitly dropped, resolving prophecies of moved-out &mut borrows #121/Unsound: aggregate dropped wholesale after a partial field-move double-resolves the field's &mut prophecy #122: those concern dropping partially-moved data aggregates; here a full destructure also triggers it and the subject is a closure's captured &mut, and the outcome is a ⊥ post-state.
• Not a lack-of-support panic (no panicked at/not implemented) and not numeric-range/overflow (only 0 and 8).

Environment

• thrust @ a148b9d
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 4.15.4 (the version pinned by .github/actions/setup-z3), default solver configuration; reproduces identically at the default edition and --edition 2021.