Unsound: a generic trait `impl` method's body is never checked against the trait method's spec, so callers assume an unverified `ensures` and panicking programs verify as `safe`

[coord-e]

Summary

When a generic impl block implements a trait method, the impl method's body is never analyzed against the trait method's spec, yet callers are still handed the trait method's #[ensures(..)] as an assumption. A generic impl whose body violates the trait's postcondition is therefore accepted, and every caller trusts the (false) postcondition, so always-panicking programs verify as safe.

The trigger is narrow and precise: the impl block is generic (impl<T> Tr for W<T>). The identical program with a concrete impl (impl Tr for W) is correctly rejected, because a concrete impl method is analyzed eagerly and a generic one is not.

Minimal reproduction

repro.rs:

#[thrust_macros::context]
trait Tr {
    #[thrust_macros::requires(true)]
    #[thrust_macros::ensures(result > 0)]
    fn m(&self) -> i32;
}

#[derive(PartialEq)]
struct W<T>(T);
impl<T> thrust_models::Model for W<T> where T: thrust_models::Model { type Ty = Self; }

impl<T> Tr for W<T> {
    fn m(&self) -> i32 { -1 } // body returns -1, violating `ensures(result > 0)`
}

fn main() {
    let w = W(0i32);
    let r = w.m();
    assert!(r > 0); // proved from the (unchecked) trait `ensures`; panics at runtime
}

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

Thrust reports safe. At runtime m() returns -1, so assert!(r > 0) always panics — the equivalent plain-Rust program aborts with exit code 101:

thread 'main' panicked at 'assertion failed: r > 0'

So a program that unconditionally panics is verified safe: a soundness hole.

Diagnostic contrast

Only two things change across these rows; each is decisive.

program	Thrust	expected
generic impl<T> Tr for W<T>, body -1, assert!(m()>0)	safe	error
concrete impl Tr for W, body -1, assert!(m()>0)	error (Unsat)	error
generic trait impl, body { assert!(false); 1 }, result unused	safe	error
concrete trait impl, body { assert!(false); 1 }, result unused	error (Unsat)	error
inherent generic method impl<T> W<T> { fn m(&self)->i32 { assert!(false); 1 } }, called	error (Unsat)	error
generic free fn fn f<T>(_:T)->i32 { -1 } with ensures(result>0), called, assert!(f(0)>0)	error (Unsat)	error

Reading:

• Row 3 (assert!(false) in the generic trait-impl body is not caught) proves the generic trait-impl body is not analyzed at all — this is not merely a "checked against a too-weak spec" case.
• Rows 5 and 6 show that generic inherent methods and generic free functions are analyzed against their bodies when called (their assert!(false) / violated ensures is caught). The skip is specific to generic methods dispatched through a trait.

Root cause

Concrete and generic function defs are registered differently in refine_fn_def (src/analyze/crate_.rs:143-157):

if sig.has_param() {
    // generic def -> registered as a *deferred* def, analyzed lazily on instantiation
    self.ctx.register_deferred_def(target_def_id, local_def_id); // (or _without_analysis)
} else {
    // concrete def -> registered eagerly
    let expected = analyzer.expected_ty();
    self.ctx.register_def(target_def_id, expected);
}

The eager whole-crate analysis pass, analyze_local_defs (src/analyze/crate_.rs:160-190), only runs bodies for concrete defs — it skips anything deferred, because concrete_def_ty returns None for DefTy::Deferred (src/analyze.rs:420-424):

let Some(expected) = self.ctx.concrete_def_ty(local_def_id.to_def_id()) else {
    continue; // deferred defs are skipped here
};
// ... expected.subst_ty_params(opaque int); analyzer.run(&expected);

So a generic impl method's body is only ever analyzed lazily, through def_ty_with_args (src/analyze.rs:473-533), whose should_analyze() branch is the sole place a deferred body is run(&expected). That branch fires only when the callee is resolved to the impl method's own def-id. For a call dispatched through the trait, the callee type is obtained from the trait method def-id instead (that is where the annotated spec lives), so def_ty_with_args is never invoked on the generic impl method — and its body is never checked. Generic inherent methods don't have this problem: a call resolves directly to the method's def-id, so their deferred body is analyzed (contrast row 5).

Meanwhile the caller still receives the trait's postcondition. expected_ty (src/analyze/local_def.rs:238-308) folds the trait method's requires/ensures into the method's expected type (:255-268), and — since the impl method carries no direct annotations, is_fully_annotated() is false (:166-177) — returns trait_item_ty (:304-305), i.e. the trait method's analyzed type -> { result | result > 0 }. That type is what a call site assumes. The postcondition is thus assumed by callers but never discharged against the generic impl body.

This is exactly the generic-impl gap in the fix from #188 ("check trait-impl methods against the trait method's spec"): #188 makes the check work for concrete impls (which flow through the eager register_def / analyze_local_defs path), but generic impls take the deferred path and slip past it.

Distinct from existing issues

• Not Incompleteness: overriding a defaulted trait method reuses the trait method's inference template, so the default body's return value pollutes the override's inferred spec — safe programs are wrongly rejected #187 (overriding a defaulted trait method reuses the trait's inference template). Incompleteness: overriding a defaulted trait method reuses the trait method's inference template, so the default body's return value pollutes the override's inferred spec — safe programs are wrongly rejected #187 is an incompleteness (safe programs rejected) on a concrete struct, and it explicitly notes that a required method with a concrete impl "verifies correctly". Here the method is required (no default body), the impl is generic, and the direction is unsoundness (panicking program accepted). Incompleteness: overriding a defaulted trait method reuses the trait method's inference template, so the default body's return value pollutes the override's inferred spec — safe programs are wrongly rejected #187's own reproduction rejects assert!(false) inside the body, whereas here that body is not analyzed at all.
• 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 (sig/ret/param-only function whose body violates it when it is never called). Here the method is called and the panic is real at runtime; the spec is requires/ensures on a trait method, and the failure is that the impl body is never checked, not that an uninstantiated template is discharged vacuously.
• Not a numeric-range issue: the constant is -1; no overflow, truncation, or unsigned wraparound is involved.

Scope / when it bites

• Any generic impl<..> Trait for Type<..> of a trait method with a spec, whose body violates the trait's ensures (or that internally can panic), called on a concrete instance. The body is silently unverified and callers trust the spec.
• Does not affect concrete impl blocks, generic inherent methods, or generic free functions — all three analyze their bodies.

Suggested direction

Ensure a generic impl method's body is analyzed against its (trait-derived) expected type at least once. Options: (a) in analyze_local_defs, additionally analyze deferred trait-impl-method defs by substituting opaque type params for their generics (mirroring the existing polymorphic-body handling already used there for generic free functions / inherent methods), rather than relying on a call site resolving to the impl def-id; or (b) when a trait-dispatched call resolves the callee spec from the trait method, also force def_ty_with_args on the corresponding impl method so its deferred body is run against the trait spec.

Environment

• thrust @ 6953863
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 4.15.x, default THRUST_SOLVER_ARGS