Unsound: calling a non-capturing closure with an argument, inside a function that has parameters, leaves the outer parameter's precondition predicate unconstrained — panicking programs verify as `safe`

[coord-e]

Summary

When a non-capturing closure (a closure with no upvars) is called with at least one argument from inside a function that has one or more parameters, the generated CHC system omits the grounding fact clause for the outer function parameter's precondition predicate. That predicate then occurs only in clause bodies (as an assumption) and never in a clause head, so the CHC solver satisfies the whole system by interpreting it as the empty relation (false).

The effect is that the verification context becomes inconsistent right after the call: every subsequent proof obligation — a trivially false assertion, or even a guaranteed out-of-bounds slice access — is discharged vacuously. As a result, programs that always panic at runtime are verified as safe.

Minimal reproducer

#[thrust::callable]
fn check(v: i32) {
    let f = |a: i32| a;   // non-capturing closure, takes one argument
    f(v);                 // calling it poisons the verification context
    assert!(1 == 2);      // always panics at runtime
}
fn main() {}

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

Thrust reports safe, but the program panics unconditionally (assert!(1 == 2)).

Stronger witness — a real memory-safety panic is masked

#[thrust::callable]
fn check(v: i32) {
    let f = |a: i32| a;
    let _ = f(v);
    let arr = [1i32, 2, 3];
    let s: &[i32] = &arr;
    let _ = s[10];        // out-of-bounds: always panics
}
fn main() {}

This also verifies as safe, even though s[10] on a length-3 slice always panics with "index out of bounds". Removing the closure call (or the let f/f(v) lines) makes Thrust correctly report Unsat.

Trigger conditions

The unsoundness requires all of the following. Removing any one makes Thrust behave correctly (reports Unsat/verification error):

1. The enclosing function has ≥1 parameter.
   • fn main() or a #[thrust::callable] function with no parameters is not affected.
2. A non-capturing closure (no upvars) is called.
   • A closure that captures a variable is not affected (e.g. let mut x = 0; let mut f = |a: i32| { x += a; }; f(v); correctly rejects a following false assertion).
3. The closure is called with an argument.
   • A no-argument closure such as let f = || 5; f(); is not affected.
4. The call is an actual invocation.
   • Defining but not calling the closure is not affected.

Calls to ordinary named functions with arguments are unaffected.

Behavior matrix (all with -Adead_code -C debug-assertions=false)

Program	Expected	Thrust
check(v){ let f=|a:i32| a; f(v); assert!(1==2); }	UNSAFE	safe ❌
check(v){ let f=|a:i32| a; let _=f(v); let s:&[i32]=&[1,2,3]; s[10]; }	UNSAFE	safe ❌
check(v){ assert!(1==2); } (no closure)	UNSAFE	Unsat ✔
check(){ let f=|a:i32| a; f(1); assert!(1==2); } (no outer param)	UNSAFE	Unsat ✔
check(v){ let mut x=0; let mut f=|a:i32|{x+=a;}; f(v); assert!(1==2); } (capturing)	UNSAFE	Unsat ✔
main(){ let f=|x| x+1; assert!(f(1)==3); } (in main, no params)	UNSAFE	Unsat ✔

Note the last row: the existing passing test tests/ui/pass/closure_no_capture.rs (let incr = |x| x+1; assert!(incr(1) == 2);) is in main, so it is not poisoned and passes legitimately. Moving the same code into a function with a parameter would cause any assertion — true or false — to verify.

Root cause (CHC evidence)

Dumping the CHC system (THRUST_OUTPUT_DIR) for the minimal reproducer shows predicate p4 (the outer parameter's precondition) used in the bodies of the clauses derived from the closure call and the assertion, but never appearing in any clause head:

(declare-fun p4 (Int Int) Bool)   ; outer-parameter precondition — never in a head

; c2  (the assert!(1==2) failure path must be unreachable)
(assert (forall (...) (=> (and (= v5 (= 1 2)) (p5 v2 v1 v3 v4)
                               (= v3 (tuple<Int> v1)) (= v4 v1)
                               (p4 v4 v1) ...      ; <-- assumes p4
                               (= v5 false) ...) false)))
; ... p4 also appears in the bodies of c0 and c1, but there is NO fact clause with p4 in the head

Because p4 is only ever assumed and never asserted, the solver is free to set p4 ≡ false, which makes every clause body mentioning p4 unsatisfiable and therefore trivially true — including the assertion-failure clause c2. The system is reported SAT ⇒ safe.

Contrast with the control (same function, same false assertion, but no closure call), where the outer parameter's precondition predicate p2 is grounded by a fact clause encoding requires(true):

(declare-fun p2 (Int Int) Bool)

; c1 — fact clause grounding the precondition (present in the correct encoding)
(assert (forall ((v0 Int) (v1 Int)) (=> (and true) (p2 v1 v1))))

; c0 — assertion-failure path, now genuinely reachable ⇒ Unsat ⇒ UNSAFE (correct)
(assert (forall (...) (=> (and (= v2 (= 1 2)) (p2 v3 v1) (= v2 false) ...) false)))

So the defect is that the analysis path for calling a non-capturing closure (whose value is modeled as the unit tuple, cf. const_value_ty treating a zero-upvar Closure as ()) fails to emit the grounding fact for the enclosing function parameter's refinement predicate, leaving it as a free (empty) relation that vacuously discharges all downstream obligations.

Notes

• This is distinct from the existing closure issues (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 &mut-capturing closures out of aggregates; Undefined sort name in SMT2 when predicate argument is a struct containing a closure #47 predicate arg containing a closure).
• #[thrust::callable] expands to requires(true)/ensures(true), so this affects the canonical way users mark functions for verification whenever such a function takes a parameter and calls a non-capturing closure.
• Numerical-range / overflow concerns are not involved here.

Environment

• branch main @ 6953863
• solver: Z3 (HORN / Spacer)