Be sure to check trait-impl methods against the trait method's spec

[coord-e]

Summary

A hand-written trait-method impl was never checked against the trait method's (extern) spec, so an implementation that contradicts the spec was accepted as safe. For example, this program verified even though the assertion can fail:

enum A { X(i32) }
impl thrust_models::Model for A { type Ty = Self; }
impl PartialEq for A {
    fn eq(&self, other: &A) -> bool {
        match (self, other) { (Self::X(l), Self::X(r)) => !l.eq(r) } // note the `!`
    }
}
#[thrust::trusted]
#[thrust_macros::requires(true)]
#[thrust_macros::ensures(true)]
fn rand() -> A { unimplemented!() }
fn main() { let x = rand(); assert!(x == x); }

x == x lowers to <A as PartialEq>::eq, which Thrust models with the blanket extern spec result == (*x == *y) (structural equality). The impl above returns the negation, so x == x is really false and the assertion can fail — yet Thrust reported the program safe.

Root cause

A trait-impl method without its own annotation is meant to be checked against the trait method's spec, which expected_ty obtains via trait_item_ty → def_ty_with_args on the trait method def. That lookup returns None unless the trait method's (extern) spec is already registered. Because refine_local_defs walked mir_keys in a single pass, a user impl PartialEq for A (low DefId) was refined before the blanket PartialEq::eq extern spec injected by std.rs (high DefId), so the impl fell back to an unconstrained template and its body was never checked against the spec.

The pass also double-registered keys in an order-dependent way: a trait method and its extern-spec companion both register the same defs entry, and correctness relied on the companion being inserted last.

Changes

• Stop register_def of the target of an extern_spec_fn. The plain target is dropped from the refine set so only the extern spec registers that key, removing the order-dependent double-registration. The ignored / predicate / formula_fn classification is done in the same pre-scan, so a trusted/ignored target still lands in skip_analysis and its body is not analyzed.
• Prioritize trait-method spec keys. Refine formula functions and trait-method (AssocFn) extern specs before ordinary defs, so a trait method's spec is registered before trait-impl methods consult it via trait_item_ty, independent of mir_keys iteration order.

Tests

• tests/ui/fail/partialeq_impl.rs — a PartialEq impl that negates structural equality is now rejected (Unsat).
• tests/ui/pass/partialeq_impl.rs — a PartialEq impl consistent with structural equality still verifies.

The full ui suite passes.

---

Generated by Claude Code

[Copilot]

Pull request overview

This PR fixes an unsoundness where unannotated trait-impl methods could be refined/checked before the corresponding trait method’s extern spec was registered, allowing implementations that contradict the trait spec (e.g., PartialEq::eq negating structural equality) to be accepted as safe.

Changes:

• Refactors Analyzer::refine_local_defs to pre-scan MIR keys, avoid order-dependent double-registration for extern_spec_fn targets, and refine trait-method extern specs first.
• Adds UI regression tests that ensure a PartialEq impl contradicting the blanket spec is rejected, while a consistent impl still verifies.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.

File	Description
src/analyze/crate_.rs	Pre-scans MIR keys to prioritize trait-method spec registration and avoid extern-spec target double-registration/order dependence.
tests/ui/pass/partialeq_impl.rs	Positive regression test: PartialEq impl consistent with structural equality continues to verify.
tests/ui/fail/partialeq_impl.rs	Negative regression test: PartialEq impl that negates structural equality is now rejected (Unsat).

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[coord-e]

local_def_analyzer の構築は重くないということにしています