Unsound: `==` on `&mut` references compares the prophecy too, so the comparison's result depends on writes made *after* it — panicking programs verify as `safe`

[coord-e]

Summary

Comparing two &mut references with == is dispatched to the generic extern spec _extern_spec_partialeq_eq (std.rs:989-996), whose postcondition is model equality: result == (*x == *y). For T = &mut i32 the model is Mut<Int> (std.rs:342-344), which is the pair ⟨current, final⟩ — so the emitted SMT equality is at sort (Mut Int) and compares the prophecy (final) component as well. At runtime, <&mut A as PartialEq<&mut B>>::eq compares only the current referent values.

The result: the truth value Thrust assigns to ra == rb depends on writes performed after the comparison. Both directions go wrong on straight-line, deterministic programs:

• a program that panics at runtime verifies as safe (unsoundness), and
• its always-safe twin is rejected as Unsat (incompleteness).

Reproduced on a148b9d with z3 4.13.4.

Reproduction (unsoundness)

fn main() {
    let mut a = 1;
    let mut b = 1;
    let ra = &mut a;
    let rb = &mut b;
    let eq = ra == rb;   // true at runtime: 1 == 1
    *ra = 10;
    *rb = 20;
    assert!(!eq);        // always FAILS at runtime
}

$ rustc -O --edition 2021 -o real muteq_unsafe.rs && ./real ; echo "exit=$?"
thread 'main' panicked at muteq_unsafe.rs:9:5:
assertion failed: !eq
exit=101                                # panics on every execution

$ cargo run -q -- -Adead_code -C debug-assertions=false muteq_unsafe.rs && echo safe
safe                                    # <- WRONG: this program always panics

Thrust proves !eq because in its model eq ⟺ (⟨1, fin_a⟩ = ⟨1, fin_b⟩), and the later writes pin the finals to fin_a = 10 ≠ 20 = fin_b.

The safe twin — identical except the last line is assert!(eq);, which holds on every execution — is rejected as Unsat for the same reason.

Controls — the verdict flips on future writes

program (all share the same prefix up to let eq = ra == rb;)	runtime	Thrust	correct?
divergent later writes (*ra = 10; *rb = 20;), assert!(eq)	ok	Unsat	❌ bug
divergent later writes (*ra = 10; *rb = 20;), assert!(!eq)	panic	safe	❌ UNSOUND
identical later writes (*ra = 10; *rb = 10;), assert!(eq)	ok	safe	✅ (only because the finals coincide)
no writes after the comparison, assert!(eq)	ok	safe	✅ (drop resolves fin = cur, finals coincide)
shared references (&a == &b), assert!(eq)	ok	safe	✅

The first three rows are the smoking gun: the programs are identical up to and including the comparison, and only the writes after it differ — yet Thrust's verdict on the earlier assert flips. A comparison executed at a given program point cannot legitimately depend on later stores; the prophecy component must not participate in ==.

Root cause

1. ra == rb lowers to <&mut i32 as std::cmp::PartialEq>::eq(_6, _7). fn_def_ty serves the trait method from the registered extern spec, so the call is given the spec of _extern_spec_partialeq_eq (std.rs:989-996):

   #[thrust_macros::ensures(result == (*x == *y))]
   fn _extern_spec_partialeq_eq<T>(x: &T, y: &T) -> bool

2. With T = &mut i32, <&mut i32 as Model>::Ty = Mut<Int> (std.rs:342-344), so *x and *y are terms of sort (Mut Int) and *x == *y is emitted as SMT = at that sort. Sort::Mut is a two-field datatype ⟨current, final⟩ (src/chc/smtlib2.rs:117-126), so the equality is componentwise — including the prophecy.

3. Runtime <&mut A as PartialEq<&mut B>>::eq forwards to A: PartialEq<B> on the pointees: it compares the current values only.

The same divergence exists for any equality spec applied at a type whose model embeds Mut: e.g. _extern_spec_box_partialeq_eq at Box<&mut T>, _extern_spec_option_partialeq_eq at Option<&mut T>, and tuple equality via the generic spec — all say "model equality", which over-constrains by the prophecy component.

Expected vs. actual

• Expected: ra == rb is true iff the current referent values are equal at the comparison point; assert!(eq) above verifies and assert!(!eq) is rejected as Unsat.
• Actual: the comparison is modeled as ⟨current, final⟩ pair equality, so assert!(!eq) verifies as safe (program panics on every run) and assert!(eq) is rejected.

Relationship to existing issues

Same family as #203 ("model equality ≠ runtime equality", there: Vec's stale slots past length), but a distinct component: here the divergence comes from the prophecy field of the Mut model, so the modeled result depends on future writes, and it affects bare &mut comparisons (no container involved). Not related to the drop/partial-move prophecy issues (#121/#122/#175): no aggregate is dropped here, and the misbehaving value is an ordinary bool local.

Suggested direction

Equality at a type whose model contains Mut should compare only the current components: either instantiate the PartialEq extern specs at reference types by dereferencing down to current values (the runtime semantics), or define model equality on Mut as equality of the current projection. The prophecy is analysis bookkeeping and must be invisible to program-observable operations.

Environment

• thrust @ a148b9d
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• z3 4.13.4, default solver configuration