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

[coord-e]

Summary

When a closure that mutates a captured variable is passed to a generic higher-order function whose specification refers to the closure's pre-/post-condition via pre!(f()) / post!(f(), result), Thrust emits type-inconsistent SMT: the closure's inferred precondition/postcondition predicate variable is declared over the FnMut receiver sort Mut<env> but applied over the bare environment sort env. The .smt2 therefore uses a predicate constant at a sort different from its declaration, and the solver aborts:

error: verification error: Error { stdout: "(error \"line 52 column 82: unknown constant p2 (A1_Tuple<Mut<Int>>)
declared: (declare-fun p2 (A2_Mut<Tuple<Mut<Int>>>) Bool) \") ... sat\n", stderr: "" }

No verdict is produced for a program that otherwise runs fine. The trigger is specifically the mutation of a capture — the structurally identical read-only-capture and non-capturing versions verify safe.

Reproduction

closure_mut_capture_hof.rs:

//@compile-flags: -C debug-assertions=off
#[thrust_macros::requires(thrust_macros::pre!(f()))]
#[thrust_macros::ensures(thrust_macros::post!(f(), result))]
fn call<F: FnMut() -> i64>(mut f: F) -> i64 {
    f()
}

fn main() {
    let mut cnt: i64 = 0;
    let f = || -> i64 { cnt += 1; cnt };   // mutates the captured `cnt`
    let r = call(f);
    assert!(r == 1);
}

• True runtime behavior: never panics. call invokes f once, cnt goes 0 -> 1, f returns 1, so r == 1. Confirmed with plain rustc --edition 2021 -C debug-assertions=off: prints r = 1, assertion holds, exit 0.
• Thrust verdict: aborts with the unknown constant p2 (A1_Tuple<Mut<Int>>) / declared: … (A2_Mut<Tuple<Mut<Int>>>) solver error above (and the analogous p3 for the postcondition). No safe/Unsat is emitted.

This uses no macros beyond pre!/post! — the closure is an ordinary || { cnt += 1; cnt }.

Controls that isolate the trigger (all verify correctly)

The bug appears only when the closure mutates a capture. Everything else identical:

// read-only capture -> `safe`
fn main() {
    let k: i64 = 1;
    let f = || -> i64 { k };            // captures, does not mutate
    let r = call(f);
    assert!(r == 1);
}

// non-capturing -> `safe`
fn main() {
    let f = || -> i64 { 1 };
    let r = call(f);
    assert!(r == 1);
}

The existing passing test tests/ui/pass/closure_postcondition.rs is the same pre!/post! HOF pattern with a non-mutating FnOnce closure and verifies safe; this report is that pattern with a mutating capture.

Further narrowing (all abort with the same sort-mismatch error):

• Only the precondition pinned matters: dropping #[ensures(post!(…))] and keeping only #[requires(pre!(f()))] still aborts (only p2 is mismatched).
• Not FnMut-specific: an FnOnce HOF (fn call<F: FnOnce() -> i64>(f: F)) with a move || { cnt += 1; cnt } closure aborts identically. The common factor is a mutated capture in the closure environment, not the trait bound.

Root cause (SMT-level evidence)

Dumping the generated CHC for the reproduction (THRUST_OUTPUT_DIR=…) shows the closure's precondition predicate p2 and postcondition predicate p3 declared over the FnMut receiver sort A2_Mut<Tuple<Mut<Int>>> (i.e. &mut env, where the environment is the 1-tuple Tuple<Mut<Int>> holding the mutable-reference capture of cnt):

(declare-fun p2 (A2_Mut<Tuple<Mut<Int>>>) Bool)
(declare-fun p3 (Int A2_Mut<Tuple<Mut<Int>>>) Bool)

They are used consistently at that sort in the clauses that model the closure receiver / the call site:

; c0 — v12 : A2_Mut<Tuple<Mut<Int>>>   (ok)
(… (= v12 (mut<Tuple<Mut<Int>>> …)) true) (p2 v12)
; c10 — v1 : A2_Mut<Tuple<Mut<Int>>>   (ok)
(=> (and (p2 v1) true) (p9 v1 v1))

but at the bare environment sort A1_Tuple<Mut<Int>> in the clauses generated for the HOF body, where pre!(f()) / post!(f(), result) are applied:

; c3 — v1 : A1_Tuple<Mut<Int>>   (MISMATCH: p2 expects A2_Mut<Tuple<Mut<Int>>>)
(forall ((v0 A1_Tuple<Mut<Int>>) (v1 A1_Tuple<Mut<Int>>)) (=> (and (p2 v1)) (p6 v1 v1)))
; c4 — v9 : A1_Tuple<Mut<Int>>   (MISMATCH)
(… (= v9 v0) (not (p2 v9))) false)
; c2 — v18 : A1_Tuple<Mut<Int>>   (MISMATCH, postcondition)
(… (= v18 v1) (= v19 v0) (not (p3 v19 v18))) false)
; c5 — v8 : A1_Tuple<Mut<Int>>   (MISMATCH, postcondition)
(… (= v8 v0) (p3 v9 v8)) (p5 …))

So the closure's pre-/post-condition predicate is threaded through the FnMut &mut self receiver on one side (declared/used as Mut<env>) and through the pre!/post! application on the other side (used as bare env), and the two are never reconciled. When the closure does not mutate a capture, the receiver carries no Mut<…> wrapper (or the environment is trivial), the two sorts coincide, and the SMT is well-typed — hence the read-only/non-capturing controls verify.

Emitting a predicate constant at a sort different from its declaration is always malformed output regardless of the backend solver.

Why this is not an already-filed / excluded issue

• Not a panic / unimplemented!: raw output is a verification error: Error { … } from the solver on Thrust's own .smt2; there is no panicked at / not implemented.
• Not numeric-range/overflow: the only values are 0 and 1; no MAX/MIN/casts.
• Not a solver timeout/unknown of a well-typed system: the query is ill-typed (a constant used at a sort other than its declaration); every SMT-LIB solver rejects it. It reproduces deterministically.
• Distinct from Undefined sort name in SMT2 when predicate argument is a struct containing a closure #47 ("Undefined sort name … predicate argument is a struct containing a closure"): Undefined sort name in SMT2 when predicate argument is a struct containing a closure #47 is an undefined sort name (Tuple referenced but never declared) arising from a #[predicate] on a struct-with-closure. Here the sort A2_Mut<Tuple<Mut<Int>>> is declared; the defect is a sort mismatch between a predicate variable's declaration and its use, triggered by a mutating closure capture flowing through pre!/post!.
• Distinct from Unsound: moving a &mut-capturing closure out of a tuple/struct field into a by-value FnOnce/FnMut verifies panicking programs as safe #177 ("moving a &mut-capturing closure out of a tuple/struct field into a by-value FnOnce/FnMut verifies panicking programs as safe"): 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 an unsoundness (a safe verdict for a panicking program) involving a closure stored in and moved out of an aggregate field. Here there is no aggregate/field move, and the outcome is an ill-typed SMT abort, not a verdict.
• Distinct from Boolean comparisons (<, <=, >, >=) emit ill-typed SMT (< Bool Bool), so any program comparing bools fails to verify #136 / Unsound: a #[param(name: { v | φ })] precondition combined with #[ensures(..)] is dropped at call sites too, so a #[thrust::trusted] function with a violated precondition verifies panicking programs as safe #196 (ill-typed (< Bool Bool) / (< Tuple Tuple)): those are ordering operators emitting comparisons at the wrong sort; this is a predicate-variable declaration/use sort mismatch in the closure pre!/post! machinery.
• Exercised by the pre!/post! closure-spec support (Ability to refer to pre-/post-conditions of closures in specifications #71/Allow user-specified closure pre/post via closure! macro #189); the reproduction needs no closure! macro.

Environment

• thrust @ a148b9d
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 5.0.0, default solver configuration (fp.spacer.global=true fp.validate=true)
• Confirmed by running thrust-rustc (not inspection-only): the reproduction aborts with the quoted solver error before any verification result, while the read-only-capture and non-capturing controls verify safe.