Unsound: an uncalled generic function (a type param appears in its signature) has its body skipped entirely, so a `#[thrust::callable]` entry point whose body always panics — or whose body violates its own `ensures` — verifies as `safe`

[coord-e]

Summary

refine_fn_def routes every function whose signature contains a generic parameter (a type/const/region param appears in an input or output type) to register_deferred_def, deferring analysis of its body to monomorphized call sites. analyze_local_defs then skips deferred defs outright (a deferred def has no concrete_def_ty, so the loop continues). Consequently, a generic function that is never called anywhere in the analyzed crate has its body verified against nothing at all — not against its requires/ensures/callable contract, and not for in-body panics.

This means:

• A #[thrust::callable] generic function whose body unconditionally panics (e.g. an out-of-bounds index) is reported safe.
• A generic function whose body provably violates its own declared ensures is reported safe.

The equivalent non-generic function is checked correctly, and any intra-crate call to the generic function also makes it checked (via monomorphization), so this is a discrepancy that defeats the purpose of #[thrust::callable] — which exists precisely to say "verify this function is safe to run for any argument."

Minimal reproduction

(A) A #[thrust::callable] entry point that panics for every input, reported safe

A.rs:

#[thrust::callable]
fn f<T>(_t: T) -> i64 {
 let v: Vec<i64> = Vec::new();
 v[0] // index out of bounds: this function panics for every input
}

fn main() {}

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

#[thrust::callable] is requires(true) + ensures(true), i.e. "this is an entry point; check that it cannot panic when called with any argument." f panics for every argument, yet Thrust certifies the crate safe. Remove <T> (or the _t: T parameter) and the same body is correctly rejected.

(B) A generic function whose body violates its declared ensures, reported safe

B.rs:

#[thrust_macros::ensures(result == x + 1)]
fn f<T>(x: i64, _t: T) -> i64 { x + 2 } // body returns x + 2, not x + 1

fn main() {}

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

The identical non-generic body is correctly rejected:

// B_concrete.rs -> `error: verification error: Unsat` (correct)
#[thrust_macros::ensures(result == x + 1)]
fn f(x: i64, _y: i64) -> i64 { x + 2 }

fn main() {}

Observed vs. expected

program	Thrust	expected
#[callable] fn f<T>(_t: T) -> i64 { Vec::<i64>::new()[0] }, uncalled	safe	error (panics for all inputs)
#[ensures(result==x+1)] fn f<T>(x: i64, _t: T) -> i64 { x+2 }, uncalled	safe	error (result == x+2 ≠ x+1)
#[ensures(result==x+1)] fn f(x: i64, _y: i64) -> i64 { x+2 } (non-generic), uncalled	error	error
#[ensures(result==x+1)] fn f<T>(x: i64) -> i64 { x+2 } (T absent from the signature), uncalled	error	error
#[callable] fn f<T>(_t: T) -> i64 { Vec::<i64>::new()[0] }, called from main	error	error

The trigger is precisely a generic parameter appearing in the signature. Position is irrelevant (first/last param), and it fires for T, &T, etc. A generic function whose type parameter does not appear in its input/output types (row 4) is checked normally.

Root cause

src/analyze/crate_.rs, refine_fn_def (around lines 143–158):

use mir_ty::TypeVisitableExt as _;
if sig.has_param() {
 // TODO: needs clear criteria on whether extern_spec'ed target fn is analyzed or not
 if target_def_id.as_local().is_none_or(|def_id| {
 self.skip_analysis.contains(&def_id) || !self.tcx.is_mir_available(def_id)
 }) {
 self.ctx.register_deferred_def_without_analysis(target_def_id, local_def_id);
 } else {
 self.ctx.register_deferred_def(target_def_id, local_def_id); // <-- generic fn: body deferred
 }
} else {
 let expected = analyzer.expected_ty();
 self.ctx.register_def(target_def_id, expected); // <-- non-generic: body analyzed eagerly
}

When sig.has_param(), f is registered as a deferred def, so its body is analyzed only when a call site instantiates it. analyze_local_defs (around lines 168–172) then skips it because a deferred def has no concrete type:

let Some(expected) = self.ctx.concrete_def_ty(local_def_id.to_def_id()) else {
 // when the local_def_id is deferred it would be skipped
 continue;
};

So with no call site, the body of f is never analyzed. Confirmed via RUST_LOG=info — the two cases register differently for the same intended spec:

# non-generic f (B_concrete.rs): eagerly registered, body analyzed
register_def def_id=..::f rty=(int, int) → { int | true ∧ ν = ($0 + 1) }

# generic f (B.rs): deferred, body never analyzed while uncalled
register_deferred_def target_def_id=..::f local_def_id=.._thrust_extern_spec_f mode=Analyze

This is consistent with the invariant already noted at src/analyze/local_def.rs:234–237:

// Note that we do not expect predicate variables to be generated here
// when type params are still present in the type. Callers should ensure either
// - type params are fully instantiated, or
// - the function is fully annotated

An uncalled generic function is neither instantiated nor (for the _t: T parameter) annotated — so instead of generating unsound predicate templates, the current code simply defers and then skips the body.

Scope / when it bites

• Reproduces whenever the offending generic function is not called anywhere in the analyzed crate. Any intra-crate call/instantiation forces monomorphized analysis and the violation is then caught (last table row).
• Unlike a plain uncalled non-generic helper (which Thrust does verify — row 3), an uncalled generic definition is silently exempt. It is a genuine problem for the use cases #[thrust::callable] and the sig/ret/param surface syntax target: verifying a function against a declared contract as documentation/regression protection, and verifying library-style code whose annotated generic API functions are consumed by callers outside the analyzed set. In those settings Thrust certifies a generic signature its body does not satisfy — and, as (A) shows, will certify a callable entry point that cannot run without panicking.

Suggested direction

A generic function that carries an explicit contract (requires/ensures/callable, or sig/ret/param) should have its body checked once even when uncalled, using the same placeholder-instantiation that analyze_local_defs already performs for polymorphic defs (subst_ty_params with an opaque type + placeholder_generic_args). Concretely, such a function should be registered eagerly (register_def with expected_ty()) rather than only via register_deferred_def, so the else branch's guarantee ("uncalled bodies are still verified") also holds for generic functions.

Distinct from existing issues

• Not Unsound: a function annotated only with sig/ret/param whose body violates the declared refinement verifies as safe when it is not called (unspecified param precondition becomes an inference template that is discharged vacuously) #179. Unsound: a function annotated only with sig/ret/param whose body violates the declared refinement verifies as safe when it is not called (unspecified param precondition becomes an inference template that is discharged vacuously) #179 is specific to the sig/ret/param front-end, where the unspecified last parameter becomes an inference-template predicate discharged vacuously; Unsound: a function annotated only with sig/ret/param whose body violates the declared refinement verifies as safe when it is not called (unspecified param precondition becomes an inference template that is discharged vacuously) #179 explicitly states the ensures front-end "is checked correctly." This report shows the ensures/callable front-end is also unsound once a generic parameter appears in the signature, and the mechanism is different (the whole body is deferred and never analyzed, not a template being satisfied vacuously).
• Residual of Generic functions with requires/ensures are not verified against their bodies (treated as trusted summaries) #103 (closed). Generic functions with requires/ensures are not verified against their bodies (treated as trusted summaries) #103's fix makes called generic functions check their bodies against their spec via monomorphization, but leaves uncalled generic functions unanalyzed.
• Not a numeric-range issue: (A) is an out-of-bounds panic and (B)'s result == x + 1 is violated at every x (x + 2), independent of i32/i64 bounds.

Environment

• thrust @ 6953863
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 5.0.0 (the repository default THRUST_SOLVER_ARGS uses fp.spacer.global, unsupported by older Z3; the bug is solver-independent — it is about which definitions get analyzed, before any solver call).