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

[coord-e]

Summary

When an impl overrides a trait method that has a default body, Thrust uses the trait method's inferred refined type as the impl method's expected type, and it also analyzes the trait's default body against that same inference template. As a result the default body's return value and the override's return value are both accumulated into a single return predicate, so at every call site the method's result is only known to be "the default value or the override value", never the actual (override) value.

Any program that relies on the return value of an overridden defaulted method therefore fails to verify, even though it provably cannot panic. This is an incompleteness / accepts-safe-rejects direction (false positive), not a soundness hole — the override body itself is still checked (see tr_I below).

The trigger is narrow and precise: a trait method with a default body that an impl overrides. A required method (no default) with the identical impl body verifies correctly, and an un-overridden default also verifies correctly.

Minimal reproduction

repro.rs:

trait Gen { fn get(&self) -> i64 { 1 } }   // default body returns 1
struct A;
impl Gen for A { fn get(&self) -> i64 { 100 } }   // override returns 100
fn main() { assert!(A.get() == 100); }

$ cargo run -- -Adead_code -C debug-assertions=false repro.rs && echo safe
error: verification error: Unsat

error: aborting due to 1 previous error

At runtime A::get dispatches to the override and returns 100, so assert!(A.get() == 100) never panics; the program is safe. Thrust rejects it.

Removing the default body (making get a required method) makes the identical program verify correctly:

trait Gen { fn get(&self) -> i64; }        // required (no default)
struct A;
impl Gen for A { fn get(&self) -> i64 { 100 } }
fn main() { assert!(A.get() == 100); }     // -> safe (correct)

Observed vs. expected

program	Thrust	expected
default get→1, impl overrides →100, assert!(A.get()==100)	error (Unsat)	safe
required get (no default), impl →100, assert!(A.get()==100)	safe	safe
default get→7, not overridden, assert!(A.get()==7)	safe	safe
default f(x)→x, impl overrides →x+1, assert!(A.f(10)==11)	error (Unsat)	safe
default get→1 overridden →100, called through generic fn c<T:Gen>(t:&T){t.get()}, assert!(c(&A)==100)	error (Unsat)	safe
default get→1 overridden →100, let x=A.get(); assert!(x==x)	safe	safe
default get→1 overridden →100, assert!(A.get()==1)	error (Unsat)	error*
override body is { assert!(false); 100 }, result unused	error (Unsat)	error

* A.get()==1 is genuinely false at runtime, so error is the correct verdict here — but Thrust rejects it for the wrong reason (it cannot rule out the default value 1), not because it knows the result is 100. Combined with the x==x row (which passes), this shows the call result is treated as an unconstrained value admitting both 1 and 100, rather than pinned to 100.

The last row (assert!(false) inside the override) is still caught, so the override body is analyzed — this is why the bug is a false-positive (incompleteness) rather than a soundness hole.

Root cause

LocalDefAnalyzer::expected_ty (src/analyze/local_def.rs:238-309) computes the type an impl method is checked against. When the method is not fully annotated but is a trait item, it takes the trait method's type verbatim (src/analyze/local_def.rs:281, :304-305):

let trait_item_ty = self.trait_item_ty();
// ...
if is_fully_annotated {
    rty::RefinedType::unrefined(builder.build().into())
} else if let Some(trait_item_ty) = trait_item_ty {
    trait_item_ty                     // <-- impl method reuses the trait method's inferred type
} else {
    rty::RefinedType::unrefined(builder.build().into())
}

and trait_item_ty is obtained by analyzing the trait method itself (src/analyze/local_def.rs:194-208):

pub fn trait_item_ty(&mut self) -> Option<rty::RefinedType> {
    // ...
    let trait_item_did = self.tcx.associated_item(self.local_def_id.to_def_id())
        .trait_item_def_id.unwrap();
    self.ctx.def_ty_with_args(trait_item_did, trait_ref.args)   // analyzes the DEFAULT body
}

For an unannotated defaulted trait method, def_ty_with_args(trait_item_did, ..) builds an inference template with a fresh return predicate p1 and analyzes the default body against it, emitting p1(1). The impl's override body is then checked against that same type, so analyzing the override emits p1(100). The two bodies are conflated under one predicate: p1 = {1, 100}.

This is visible in the logs for repro.rs (RUST_LOG=thrust=debug): both return statements are analyzed —

stmt=Some(_0 = const 1_i64)     local_def_id=DefId(..{impl#0}::get)   # default body
stmt=Some(_0 = const 100_i64)   local_def_id=DefId(..{impl#0}::get)   # override body
register_def def_id=DefId(..{impl#0}::get) rty=({ &immut () | p0 }) -> { int | p1 ν }

and at the call in main the callee return refinement p1 is used, so the switch switchInt(move _1) -> [100: ok, otherwise: panic] produces false <= p1(v) ∧ v != 100, which is UNSAT because p1 also contains 1.

The defect: the override should be checked against the trait method's declared type (default true/an inference template that the override alone constrains, or the concrete trait signature), not against a template that the trait's default body has already been analyzed into. Analyzing the default body's return value into the predicate that the override reuses is what pollutes the spec.

Scope / when it bites

• Reproduces for any impl that overrides a defaulted trait method whose return value a caller depends on — both via direct method calls and via monomorphized generic dispatch (fn c<T: Gen>(t: &T)).
• Does not affect required methods (no default) or un-overridden defaults, both of which analyze exactly one body and verify correctly.
• The effect (default value pollutes the override's inferred return refinement) also applies to methods with parameters (A.f(10) row).
• Not a numeric-range issue: the constants 1, 7, 100 are small; the discrepancy is purely about which body's return value the caller sees.

Suggested direction

When an impl overrides a defaulted trait method, the override's body should be checked against a type that is not also constrained by the trait's default body. Options: (a) give the overriding impl method its own fresh inference template (only the override body constrains it), letting it be related to the declared trait signature by subtyping as usual; or (b) skip analyzing / skip accumulating the default body's obligations into the template whenever an override exists for that (trait method, Self) pair.

Notes

• Related to 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 in that both stem from parameter/return inference templates standing in for a declared type, but the mechanism is distinct: 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 a template parameter precondition left unconstrained for uncalled sig-annotated functions (accepts-bad); this is a template return predicate over-constrained by the trait default body for overridden defaulted methods (rejects-good).
• Trait objects (&dyn Trait) are separately unsupported (unimplemented! panic at src/refine/template.rs:440) and are out of scope here.

Environment

• thrust @ af7cd99
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 (default THRUST_SOLVER_ARGS = fp.spacer.global=true fp.validate=true)