Add Vec-to-slice coercion extern specs

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)]

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
+}

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);
+}