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`

[coord-e]

Summary

Vec<T> is modeled as a Seq value, i.e. the pair (array, length) (impl<T> Model for Vec<T>, std.rs:366). Equality on vectors (v1 == v2) has no Vec-specific extern spec, so it falls through to the blanket

// std.rs:990-996
#[thrust_macros::ensures(result == (*x == *y))]
fn _extern_spec_partialeq_eq<T>(x: &T, y: &T) -> bool
  where T: thrust_models::Model + PartialEq, T::Ty: PartialEq
{ PartialEq::eq(x, y) }

*x == *y on two Vec values is lowered to SMT equality of the whole (array, length) datatype. By array extensionality that requires the two backing arrays to agree at every index — including slots beyond length. But Rust's Vec::eq (and [T]::eq) compares only the first length elements.

The pop and truncate specs deliberately keep the full backing array and only shrink length:

// _extern_spec_vec_pop (std.rs:785):     (!vec).array == (*vec).array   // array kept, length-1
// _extern_spec_vec_truncate (std.rs:807): !vec == Seq { array: (*vec).array, length: len }

so after a pop/truncate the array retains a stale element past the new length. Two vectors that are equal in Rust but whose stale slots differ are therefore modeled as unequal. When such a comparison guards a branch, Thrust treats the branch as dead and accepts programs that panic at runtime.

Reproduction (minimal, no &mut/enum/generics/negative literals)

vec_eq.rs:

#[thrust::callable]
fn check() {
    let mut v1 = Vec::new();
    v1.push(1);
    v1.push(2);
    v1.pop();          // v1 == [1] ; backing array still holds 2 at index 1
    let mut v2 = Vec::new();
    v2.push(1);
    v2.push(3);
    v2.pop();          // v2 == [1] ; backing array still holds 3 at index 1
    if v1 == v2 {      // Rust: [1] == [1] is TRUE  → branch is taken
        assert!(false);
    }
}

fn main() {}

Under plain rustc the two vectors are equal, the branch is taken, and the program panics:

$ rustc --edition 2021 -C debug-assertions=off run.rs && ./run   # main calls check()
v1=[1] v2=[1] eq=true
thread 'main' panicked at run.rs: reached: v1 == v2

Yet Thrust certifies it safe:

$ cargo run --quiet -- --edition 2021 -Adead_code -C debug-assertions=false vec_eq.rs && echo 'accepted: safe'
accepted: safe

Control — same shape, matching stale slots, correctly rejected

The defect is specific to the stale slots differing. Constructing both vectors identically (so the arrays agree past length) makes v1 == v2 provable and the panic is correctly reported:

// REJECTED (Unsat) — correct: v1 and v2 built identically, arrays agree, v1 == v2 holds, assert!(false) reachable
#[thrust::callable]
fn check() {
    let mut v1 = Vec::new(); v1.push(1); v1.push(9); v1.pop();
    let mut v2 = Vec::new(); v2.push(1); v2.push(9); v2.pop();
    if v1 == v2 { assert!(false); }
}

matching stale slots (9 vs 9): REJECTED (unsafe)  ✔ correct
differing stale slots (2 vs 3): ACCEPTED as SAFE  ✘ UNSOUND

truncate triggers it identically (replace pop() with push(2)/push(3) then truncate(1)).

Incompleteness face of the same defect

Because the modeled equality evaluates to a definite false where Rust gives true, the same root cause also rejects valid programs when the comparison is asserted rather than used as a guard:

// REJECTED (Unsat) — but v1 == v2 is true in Rust, so this should verify
#[thrust::callable]
fn check() {
    let mut v1 = Vec::new(); v1.push(1); v1.push(2); v1.pop();
    let mut v2 = Vec::new(); v2.push(1); v2.push(3); v2.pop();
    assert!(v1 == v2);
}

Root cause

Vec is (array, length), and the blanket _extern_spec_partialeq_eq models == as equality of the entire representation. The generated SMT compares the whole tuple, e.g. the modeled vector value has sort tuple<Array<Int-Int>-Int> and v1 == v2 becomes (= (tuple <arr1> 1) (tuple <arr2> 1)), which is false because arr1 and arr2 disagree at index 1 (the popped slot: 2 vs 3). The stale slots exist because _extern_spec_vec_pop/_extern_spec_vec_truncate copy the old array unchanged and only decrement/reset length.

The mismatch is: Rust vector/slice equality is defined over [0, length), but the model compares the full untruncated array. Any two Seq-modeled values (Vec, and slices, which share the (array, length) model) that agree on [0, length) but differ past length are wrongly deemed unequal.

Expected behavior

Vec/slice == should compare only the live prefix, i.e. equal lengths and array[i] == array[i] for all 0 <= i < length, rather than whole-array structural equality. This needs a Vec/slice-specific PartialEq extern spec (the blanket structural spec is unsound for containers whose model carries data past the logical length), or the container operations must canonicalize array contents beyond length (e.g. pop/truncate clearing the vacated slots) so full-array equality coincides with Rust equality.

Why it is unsound (not merely incomplete)

In the reproduction the if v1 == v2 guard is modeled as false, so the assert!(false) arm is discharged as unreachable and Thrust returns safe. At runtime v1 == v2 is true, the arm runs, and the program panics — the defining shape of a soundness hole (safe reported for a program that panics for its only input).

Distinct from existing issues

• Not Unsound: negative SwitchInt match targets are sign-truncated to large positives, making match arms verify under a wrong path assumption #132 (negative SwitchInt targets): no negative literals or match on integers; the guard is a Vec PartialEq call.
• Not Unsound: enum variants after an explicit discriminant get the wrong datatype_discr value, making match arms vacuously verify #126 (enum discriminants) / Incompleteness: a refinement on a generic type argument in #[param] position is dropped for multi-variant enums, so the payload refinement is never assumed in the callee #193 (generic enum payload refinement): no user enum, no generics; Vec<i32> with concrete i32.
• Not Incompleteness: refinement on a reference's pointee (&{ v | φ } / &mut { v | φ }) in parameter position is not assumed by the callee #166 (refinement on a reference pointee in parameter position): no annotations at all.
• Not a numeric-range issue (values are 1, 2, 3) and not a lack-of-support panic — Vec equality is supported and verifies; it just verifies wrongly.

Environment

• thrust @ 6953863
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 5.0.0, default solver configuration