Unsound: a two-phase borrow (`v.push(v.len())`) havocs the receiver before the arguments are evaluated, so reads in the argument see the prophecy — panicking programs verify as `safe`

[coord-e]

Summary

When a method call takes its receiver by &mut and another argument reads the same place (accepted by rustc via two-phase borrows), Thrust processes the &mut borrow at its creation point: mutable_borrow immediately replaces the receiver's binding in the environment with the prophecy variable. The argument is evaluated after that, so any read of the receiver inside the argument expression observes the prophecy (post-call) value instead of the current value.

This is both unsound (a program that panics at runtime verifies as safe) and incomplete (the corresponding true assertion is rejected as Unsat).

Reproduction (unsound direction)

tp_unsound.rs:

fn main() {
 let mut v = Vec::new();
 v.push(v.len());
 assert!(v[0] == 1);
}

In real Rust, v.len() is evaluated before the push and yields 0, so v[0] == 0 and the assertion panics:

$ rustc -C debug-assertions=off --edition=2021 tp_unsound.rs -o tp_run && ./tp_run
thread 'main' panicked at tp_unsound.rs:4:5:
assertion failed: v[0] == 1

Thrust verifies it as safe:

$ thrust-rustc -Adead_code -C debug-assertions=off --edition=2021 tp_unsound.rs && echo safe
safe

Dual reproduction (incompleteness direction)

Asserting the value the program actually has is rejected:

fn main() {
 let mut v = Vec::new();
 v.push(v.len());
 assert!(v[0] == 0); // true at runtime
}

$ thrust-rustc -Adead_code -C debug-assertions=off --edition=2021 tp_correct.rs
error: verification error: Unsat

Sequencing the read manually (let n = v.len(); v.push(n);) makes both directions behave correctly, which isolates the two-phase borrow as the trigger.

Analysis

The MIR for v.push(v.len()) creates the mutable borrow of v before evaluating the argument (this is exactly what two-phase borrows permit):

bb1: {
 _3 = &mut _1; // two-phase borrow of v
 _5 = &_1; // shared borrow of v, still allowed
 _4 = Vec::<usize>::len(move _5) -> [return: bb2, ...];
}
bb2: {
 _2 = Vec::<usize>::push(move _3, move _4) -> ...;
}

Thrust handles the first statement in analyze_assignment (src/analyze/basic_block.rs:1117):

if let Rvalue::Ref(_, mir::BorrowKind::Mut { .. }, referent) = rvalue {
 // mutable borrow
 let rty = self.mutable_borrow(stmt_idx, *referent);
 ...
}

The pattern matches every BorrowKind::Mut, including MutBorrowKind::TwoPhaseBorrow, and mutable_borrow (src/analyze/basic_block.rs:1028) calls self.env.borrow_place(place, temp_var), which rebinds _1 to the fresh prophecy variable right away. When _5 = &_1 and Vec::len(_5) are analyzed next, they read that prophecy, i.e. the value of v after push returns. The extern spec for push then constrains the final length to initial length + 1 = 1, so the solver concludes the pushed element is 1 and proves v[0] == 1.

In RustHorn terms, a two-phase borrow must not conflate the reservation point with the activation point: between _3 = &mut _1 and the first use of _3 (its activation at the push call), reads of _1 still see the current value. Treating the reservation as an activation swaps current and prophecy for that whole window.

Notes

• A Vec-free variant shows the same root cause. Verifying it currently dies with a solver error (z3 4.13.4 segfaults on the emitted clause system, so there is no verdict to observe, but the encoding exhibits the same prophecy-for-current substitution):

  struct C { x: i32 }
  impl thrust_models::Model for C { type Ty = Self; }
  impl C {
   fn add(&mut self, y: i32) { self.x = self.x + y; }
   fn get(&self) -> i32 { self.x }
  }
  fn main() {
   let mut c = C { x: 1 };
   c.add(c.get()); // two-phase: rustc accepts, adds 1
   assert!(c.x == 2);
  }

• Not related to integer ranges; the same shape appears for any recv.method(arg_reading_recv) call.

• Reproduced at a148b9d with z3 4.13.4.