Add Vec-to-slice coercion extern specs

[coord-e]

Specifies the postcondition *result == *vec for the three standard ways a Vec<T> can be coerced to &[T], letting the refinement checker propagate Seq refinements through all of them.

Changes

std.rs

• Vec::as_slice: explicit call Vec::as_slice(&v)
• Deref::deref: implicit coercion let s: &[T] = &v
• AsRef::as_ref: v.as_ref()

All three specs have the postcondition *result == *vec.

Tests

2 new UI tests covering the implicit deref coercion path:

Test	What it checks
pass/vec_deref.rs	Push 10, 20; implicit &v coercion; assert len and element values
fail/vec_deref.rs	Wrong expected value → Unsat

[Copilot]

Pull request overview

This PR extends Thrust’s injected std.rs extern specs so the refinement checker can propagate Seq-style refinements through the three common Vec<T> -> &[T] coercion paths (as_slice, Deref, AsRef). It also adds UI coverage for the implicit deref coercion route (&v to &[T]).

Changes:

• Add extern specs for Vec::as_slice, <Vec<T> as Deref>::deref, and <Vec<T> as AsRef<[T]>>::as_ref, each ensuring *result == *vec.
• Add a passing UI test validating slice contents obtained via implicit deref coercion (let s: &[T] = &v;).
• Add a failing UI test that triggers an Unsat when asserting an incorrect element value through the same coercion path.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated no comments.

File	Description
std.rs	Adds three extern specs to equate the resulting slice model with the source Vec model for all standard Vec -> &[T] coercions.
tests/ui/pass/vec_deref.rs	New passing test covering implicit &Vec<T> → &[T] deref coercion and basic slice property checks.
tests/ui/fail/vec_deref.rs	New failing test ensuring the deref coercion path produces an Unsat when asserting an incorrect slice element.

---

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