From 66f7a4ee6a38318c24b316b7cc72d62b671fce4c Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 1 Jul 2026 14:47:05 +0000
Subject: [PATCH] Add Vec-to-slice coercion extern specs

Specify the postcondition `*result == *vec` for the three ways a `Vec<T>`
can be coerced to `&[T]`: `as_slice`, `Deref::deref` (implicit `&v`
coercion), and `AsRef::as_ref` (`v.as_ref()`). This lets the refinement
checker propagate Seq refinements from Vec through all standard coercion paths.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013oVufAKCMzsLRnQ8F58PdP
---
 std.rs                     | 27 +++++++++++++++++++++++++++
 tests/ui/fail/vec_deref.rs | 10 ++++++++++
 tests/ui/pass/vec_deref.rs | 12 ++++++++++++
 3 files changed, 49 insertions(+)
 create mode 100644 tests/ui/fail/vec_deref.rs
 create mode 100644 tests/ui/pass/vec_deref.rs

diff --git a/std.rs b/std.rs
index 32525a2b..4a4b5db5 100644
--- a/std.rs
+++ b/std.rs
@@ -800,6 +800,33 @@ fn _extern_spec_vec_truncate<T>(vec: &mut Vec<T>, len: usize) where T: thrust_mo
     Vec::truncate(vec, len)
 }
 
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(*result == *vec)]
+fn _extern_spec_vec_as_slice<T>(vec: &Vec<T>) -> &[T]
+    where T: thrust_models::Model, T::Ty: PartialEq
+{
+    Vec::as_slice(vec)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(*result == *vec)]
+fn _extern_spec_vec_deref<T>(vec: &Vec<T>) -> &[T]
+    where T: thrust_models::Model, T::Ty: PartialEq
+{
+    <Vec<T> as std::ops::Deref>::deref(vec)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(*result == *vec)]
+fn _extern_spec_vec_as_ref<T>(vec: &Vec<T>) -> &[T]
+    where T: thrust_models::Model, T::Ty: PartialEq
+{
+    <Vec<T> as AsRef<[T]>>::as_ref(vec)
+}
+
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(result == slice.1)]
diff --git a/tests/ui/fail/vec_deref.rs b/tests/ui/fail/vec_deref.rs
new file mode 100644
index 00000000..57852710
--- /dev/null
+++ b/tests/ui/fail/vec_deref.rs
@@ -0,0 +1,10 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let mut v: Vec<i32> = Vec::new();
+    Vec::push(&mut v, 10);
+    Vec::push(&mut v, 20);
+    let s: &[i32] = &v;
+    assert!(s[0] == 99); // wrong value → Unsat
+}
diff --git a/tests/ui/pass/vec_deref.rs b/tests/ui/pass/vec_deref.rs
new file mode 100644
index 00000000..54b3e760
--- /dev/null
+++ b/tests/ui/pass/vec_deref.rs
@@ -0,0 +1,12 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let mut v: Vec<i32> = Vec::new();
+    Vec::push(&mut v, 10);
+    Vec::push(&mut v, 20);
+    let s: &[i32] = &v;
+    assert!(s.len() == 2);
+    assert!(s[0] == 10);
+    assert!(s[1] == 20);
+}