Incompleteness: a local `impl PartialEq` is checked against the blanket `_extern_spec_partialeq_eq` (structural model equality), so any non-structural `eq` — even one that is never used — makes the whole crate fail with `Unsat`

[coord-e]

Summary

A local impl PartialEq for T is never checked against its own body-derived spec: LocalDefAnalyzer::expected_ty takes the trait method's registered type, and the type registered for core::cmp::PartialEq::eq is the blanket extern spec in std.rs

// std.rs:989-996
#[thrust::extern_spec_fn]
#[thrust_macros::requires(true)]
#[thrust_macros::ensures(result == (*x == *y))]     // <- model-level structural equality
fn _extern_spec_partialeq_eq<T>(x: &T, y: &T) -> bool
  where T: thrust_models::Model + PartialEq, T::Ty: PartialEq
{ PartialEq::eq(x, y) }

instantiated at T. The user's eq body is then verified against structural equality of the whole model representation. PartialEq in Rust carries no such requirement — it only has to be symmetric and transitive — so the extremely common pattern of comparing on a subset of the fields (ignoring a cache, a generation counter, an id/handle, a #[doc(hidden)] field) is rejected.

The rejection is whole-crate and unconditional: it fires on the mere presence of the impl, even when == is never used anywhere in the program. There is no way to opt out (see "No workaround" below).

Reproduced on 6f06fa0 with Z3 5.0.0.

Minimal reproduction

repro.rs — an idiomatic "compare the identity fields, ignore the cache" impl, and a main that never mentions Point:

struct Point { x: i64, y: i64, cached: i64 }
impl thrust_models::Model for Point { type Ty = Self; }

impl PartialEq for Point {
    fn eq(&self, other: &Self) -> bool { self.x == other.x && self.y == other.y }
}

fn main() { assert!(1 + 1 == 2); }

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

error: aborting due to 1 previous error

The program has no assert that can fail and no call to eq at all. Adding the third field to the comparison — i.e. making eq coincide with structural equality — makes the identical program verify:

fn eq(&self, other: &Self) -> bool {
    self.x == other.x && self.y == other.y && self.cached == other.cached   // -> safe
}

The comparison is also mis-evaluated when it is used

struct Point { x: i64, y: i64, cached: i64 }
impl thrust_models::Model for Point { type Ty = Self; }
impl PartialEq for Point {
    fn eq(&self, other: &Self) -> bool { self.x == other.x && self.y == other.y }
}
fn main() {
    let p = Point { x: 1, y: 2, cached: 10 };
    let q = Point { x: 1, y: 2, cached: 20 };
    assert!(p == q);          // Rust: true — the assert never fires
}

$ rustc --edition 2021 -C debug-assertions=off repro2.rs -o repro2 && ./repro2 ; echo "exit=$?"
no panic; p == q is true
exit=0

$ cargo run -q -- -Adead_code -C debug-assertions=false --edition 2021 repro2.rs && echo safe
error: verification error: Unsat

Controls

Every row below differs from its neighbours in exactly one respect; each is decisive.

program	Thrust	expected
impl PartialEq compares 2 of 3 fields, never used	Unsat	safe
same, on an enum (match (self, other), compares one payload field)	Unsat	safe
same, and p == q actually evaluated (true at runtime)	Unsat	safe
eq compares all fields (= structural), never used	safe	safe
#[derive(PartialEq)] instead of the manual impl	safe	safe
eq body { true }, compared values structurally different	Unsat	safe
identical body as an inherent method fn eq_custom(&self, other: &Self) -> bool	safe	safe
identical body as a method of a user trait trait Same { fn same(..) }	safe	safe

The last two rows isolate the trigger precisely: the body is unproblematic on its own; it is being related to a spec it never declared, and only implementing PartialEq (a trait Thrust ships a blanket extern spec for) does that.

Generated SMT-LIB evidence

THRUST_OUTPUT_DIR=… on the minimal repro emits, alongside the trivial main clauses (c4–c7), the obligation

; A0_Tuple<Int-Int-Int> is the model of `Point`; p2 is the inferred body predicate of `eq`
; c2
(assert (forall ((v0 Bool) (v1 A0_Tuple<Int-Int-Int>) (v2 A0_Tuple<Int-Int-Int>)
                 (v3 A0_Tuple<Int-Int-Int>) (v4 A0_Tuple<Int-Int-Int>) (v5 Bool))
  (=> (and (p2 v2 v0 v1) (= v3 v1) (= v4 v2) (= v5 v0)
           (not (= v5 (= v3 v4))))                       ; result must equal *structural* (= v3 v4)
      false)))

c2 is the whole reason the query is Unsat: the body's result v5 is forced to agree with SMT = on the full three-field datatype. main contributes nothing but (= v0 (+ 1 1)).

RUST_LOG=thrust=info shows the same thing at the type level — the user's eq is registered with the extern spec's return refinement, not one derived from its body:

deferred def def_id=DefId(core::cmp::PartialEq::eq)
  rty=(&immut (own int, own int, own int), &immut (own int, own int, own int))
      → { bool | true ∧ ν = (*$0 = *$1) }        generic_args=[Point, Point]
register_def def_id=DefId(repro::{impl#1}::eq)
  rty=(&immut (own int, own int, own int), &immut (own int, own int, own int))
      → { bool | true ∧ ν = (*$0 = *$1) }

Root cause

1. refine_local_defs (src/analyze/crate_.rs:62-107) registers #[thrust::extern_spec_fn] targets that are AssocFn first, so the trait method core::cmp::PartialEq::eq already has a registered refined type — the blanket _extern_spec_partialeq_eq — before any impl is refined. (The comment there, "so that they are always available when refining trait impl functions; see the partialeq_impl.rs case", names this intent.)

2. LocalDefAnalyzer::expected_ty (src/analyze/local_def.rs:281, :304-305) gives an unannotated impl method its trait item's type verbatim:

   let trait_item_ty = self.trait_item_ty();
   // ...
   } else if let Some(trait_item_ty) = trait_item_ty {
       trait_item_ty            // <- the blanket extern spec, instantiated at Self
   } else {

   with trait_item_ty resolved through def_ty_with_args(trait_item_did, trait_ref.args) (src/analyze/local_def.rs:194-208).

3. analyze_local_defs then checks the impl body against that type, producing clause c2. Because <Point as Model>::Ty = Point, *x == *y is SMT = on the whole datatype, i.e. all fields.

The blanket spec is a sound description of PartialEq::eq only for types whose eq happens to be structural (#[derive(PartialEq)], and the primitives it was written for). Used as the expected type of a local impl, it silently upgrades "here is what callers may assume" into "here is what your impl must be" — and PartialEq does not require that. The TODO immediately above the spec (std.rs:986-987, "these specs … are too restrictive; we should allow for a per-impl spec once we can describe the spec of blanket impls") anticipates the direction but not this consequence: the current behaviour is not merely a weak spec, it rejects otherwise-verifiable crates.

Note that the two existing tests/ui/{pass,fail}/partialeq_impl.rs cases do not discriminate between "the impl body is used" and "the blanket spec is used": the pass impl is structural, and the fail impl (!lhs.eq(rhs)) is Unsat under either reading.

No workaround

The impl cannot opt out of the imposed spec:

impl PartialEq for Point {
    #[thrust::trusted]
    #[thrust_macros::requires(true)]
    #[thrust_macros::ensures(true)]
    fn eq(&self, other: &Self) -> bool { self.x == other.x && self.y == other.y }
}

error: Wrap the surrounding impl block or trait definition with #[thrust_macros::context] to annotate methods

and adding #[thrust_macros::context] to the impl block does not compile, because the companion functions it expands to are not members of PartialEq:

error[E0407]: method `_thrust_requires_eq` is not a member of trait `PartialEq`

So the only way to analyze a crate containing a non-structural PartialEq is to delete or rewrite the impl.

Secondary effect: unsound acceptance when the impl block is generic

The same imposed spec is handed to callers. When the impl block is generic its body is never analyzed (#190), so nothing contradicts the spec and the mismatch surfaces in the accepting direction — a program that panics on every run verifies as safe:

struct W<T>(T, T);
impl<T> thrust_models::Model for W<T> where T: thrust_models::Model { type Ty = W<T::Ty>; }
impl<T: PartialEq> PartialEq for W<T> {
    fn eq(&self, _o: &Self) -> bool { true }        // always equal
}
fn main() {
    let a = W(1i64, 2i64);
    let b = W(3i64, 4i64);
    if a == b { assert!(false); }                   // Rust: branch IS taken -> panics
}

$ rustc --edition 2021 -C debug-assertions=off w.rs -o w && ./w ; echo "exit=$?"
thread 'main' panicked at w.rs:6:17: assertion failed: false
exit=101

$ cargo run -q -- -Adead_code -C debug-assertions=false --edition 2021 w.rs && echo safe
safe

Thrust proves the branch dead from ν = (*$0 = *$1) at W<i64>, which is false for (1,2) vs (3,4). The skip of the generic impl body is #190; what this issue adds is that even with no user annotation anywhere, callers are handed a concrete, wrong postcondition to reason from. Making the impl concrete flips this case back to Unsat (the rejecting direction above).

Relationship to existing issues

• Ordering comparisons (<, >) on tuple/aggregate values emit ill-typed SMT (< Tuple Tuple) via the generic PartialOrd::lt/gt extern specs, so safe programs comparing tuples are falsely rejected #195 (PartialOrd::lt/gt on tuples emit ill-typed SMT) shares the "blanket cmp extern spec applied at every type" family, but its defect is in lowering model < at a non-Int sort — the spec is fine, the SMT it produces is not, and no user impl is involved. Here the SMT is well-typed and the solver answers correctly; the defect is that the impl is related to a spec it never declared. Different fix site: Ordering comparisons (<, >) on tuple/aggregate values emit ill-typed SMT (< Tuple Tuple) via the generic PartialOrd::lt/gt extern specs, so safe programs comparing tuples are falsely rejected #195 is fixed in how < is emitted, this one in how an impl method's expected type is chosen.
• Unsound: Vec equality (==) is modeled as structural equality of the whole (array, length) representation, so vectors equal in Rust but differing in stale slots past length (after pop/truncate) compare unequal — dead-branch panics verify as safe #203 (Vec equality includes stale slots) and Unsound: == on &mut references compares the prophecy too, so the comparison's result depends on writes made *after* it — panicking programs verify as safe #210 (== on &mut compares the prophecy) are "the model of this type's equality ≠ Rust's equality" for types whose PartialEq comes from outside the crate. This issue is the converse situation: the crate does define eq, and its definition is discarded.
• 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 #190 enables the secondary unsound variant above but does not cover the rejecting direction, which reproduces with a fully concrete, non-generic impl.

Suggested direction

An impl method should not inherit a trait spec that was supplied as an external model of the trait method rather than as a contract the trait declares. Options:

• (a) Treat an #[thrust::extern_spec_fn] registered against a trait method as a fallback used only when the receiver type has no local impl; when a local impl exists, infer that impl's spec from its body as for any other function — the inherent-method and user-trait rows in the table above show this already works for the identical body under a different name.
• (b) Keep the blanket spec but relate the impl body to it by subtyping in the caller direction only — the impl provides its own (inferred) postcondition and callers see it — rather than making it an equality obligation on the body.
• (c) At minimum, distinguish specs that are contracts (a #[requires]/#[ensures] written on a trait method, which an impl legitimately must satisfy) from specs that are extern models of a foreign method, and never apply the latter to a local impl.

Option (a) also makes #[derive(PartialEq)] keep working unchanged, since a derived eq is a local impl whose inferred spec is structural equality.

Environment

• thrust @ 6f06fa0
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 5.0.0 (the version .github/actions/setup-z3 pins), default THRUST_SOLVER_ARGS