Support static array literals, &[T;N] → &[T] coercion, and &mut [T] element writes

src/refine/env.rs

@@ -1051,6 +1051,7 @@ enum Path {
     Deref(Box<Path>),
     TupleProj(Box<Path>, usize),
     Downcast(Box<Path>, VariantIdx, FieldIdx),
+    Index(Box<Path>, Local),
 }
 
 impl<'tcx> From<Place<'tcx>> for Path {
@@ -1067,6 +1068,7 @@ impl<'tcx> From<Place<'tcx>> for Path {
                     };
                     Path::Downcast(Box::new(path), variant_idx, field_idx)
                 }
+                Some(PlaceElem::Index(local)) => Path::Index(Box::new(path), local),
                 None => break,
                 _ => unimplemented!(),
             };
@@ -1099,6 +1101,26 @@ where
                 self.path_type(path)
                     .downcast(*variant_idx, *field_idx, &self.enum_defs)
             }
+            Path::Index(path, idx_local) => {
+                let inner_pty = self.path_type(path);
+                let idx_pty = self.local_type(*idx_local);
+                // Seq<T> = (Box<Array<Int,T>>, Box<Int>): get field 0 then deref the box.
+                let arr_pty = match inner_pty.ty.clone() {
+                    rty::Type::Tuple(_) => inner_pty.tuple_proj(0).deref(),
+                    ty => unimplemented!("PlaceElem::Index on non-Seq type: {:?}", ty),
+                };
+                let rty::Type::Array(arr_ty) = arr_pty.ty.clone() else {
+                    unreachable!("expected Array type after index normalization")
+                };
+                let elem_refined_ty = *arr_ty.elem;
+                let mut builder = refine::PlaceTypeBuilder::default();
+                let (_, arr_term) = builder.subsume(arr_pty);
+                let (_, idx_term) = builder.subsume(idx_pty);
+                let (elem_ty, value_var_ex) = builder.subsume_rty(elem_refined_ty);
+                let elem_term = crate::chc::Term::var(value_var_ex.into());
+                builder.push_formula(elem_term.clone().equal_to(arr_term.select(idx_term)));
+                builder.build(elem_ty, elem_term)
+            }
         }
     }
 

std.rs

@@ -364,6 +364,14 @@ mod thrust_models {
         type Ty = model::Seq<<T as Model>::Ty>;
     }
 
+    impl<T: Model> Model for [T] {
+        type Ty = model::Seq<<T as Model>::Ty>;
+    }
+
+    impl<T: Model, const N: usize> Model for [T; N] {
+        type Ty = model::Seq<<T as Model>::Ty>;
+    }
+
     impl<T> Model for Option<T> where T: Model {
         type Ty = Option<<T as Model>::Ty>;
     }
@@ -825,3 +833,43 @@ fn _extern_spec_partialord_gt<T>(x: &T, y: &T) -> bool
 {
     PartialOrd::gt(x, y)
 }
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result == slice.1)]
+fn _extern_spec_slice_len<T>(slice: &[T]) -> usize
+    where T: thrust_models::Model, T::Ty: PartialEq
+{
+    <[T]>::len(slice)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(index < slice.1)]
+#[thrust_macros::ensures(*result == slice.0[index])]
+fn _extern_spec_slice_index<T>(slice: &[T], index: usize) -> &T
+    where T: thrust_models::Model, T::Ty: PartialEq
+{
+    <[T] as std::ops::Index<usize>>::index(slice, index)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(index < (*slice).1)]
+#[thrust_macros::ensures(
+    *result == (*slice).0[index] &&
+    !result == (!slice).0[index] &&
+    !slice == thrust_models::model::Seq((*slice).0.store(index, !result), (*slice).1)
+)]
+fn _extern_spec_slice_index_mut<T>(slice: &mut [T], index: usize) -> &mut T
+    where T: thrust_models::Model, T::Ty: PartialEq
+{
+    <[T] as std::ops::IndexMut<usize>>::index_mut(slice, index)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result == (slice.1 == 0))]
+fn _extern_spec_slice_is_empty<T>(slice: &[T]) -> bool
+    where T: thrust_models::Model, T::Ty: PartialEq
+{
+    <[T]>::is_empty(slice)
+}

tests/ui/fail/array_literal_1.rs

@@ -0,0 +1,9 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let arr = [1i32, 2, 3];
+    let s: &[i32] = &arr;
+    let v = s[0];
+    assert!(v == 99);
+}

tests/ui/fail/array_literal_2.rs

@@ -0,0 +1,8 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let arr = [0i32, 0, 0, 0];
+    let s: &[i32] = &arr;
+    let _ = s[4];
+}

tests/ui/fail/array_literal_3.rs

@@ -0,0 +1,9 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let mut arr = [1i32, 2, 3];
+    let s: &mut [i32] = &mut arr;
+    s[0] = 42;
+    assert!(s[0] == 1); // old value → Unsat
+}

tests/ui/fail/array_literal_4.rs

@@ -0,0 +1,10 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let mut x = 1i32;
+    let mut y = 2i32;
+    let arr: [&mut i32; 2] = [&mut x, &mut y];
+    let vx = *arr[0];
+    assert!(vx == 99);
+}

tests/ui/fail/slice_1.rs

@@ -0,0 +1,14 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result.len() == 0)]
+fn empty_slice() -> &'static [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let s = empty_slice();
+    let _ = s[0];
+}

tests/ui/fail/slice_2.rs

@@ -0,0 +1,14 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result.len() >= 2)]
+fn two_elem_slice() -> &'static [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let s = two_elem_slice();
+    let _ = s[2];
+}

tests/ui/pass/array_literal_1.rs

@@ -0,0 +1,9 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let arr = [1i32, 2, 3];
+    let s: &[i32] = &arr;
+    let v = s[0];
+    assert!(v == 1);
+}

tests/ui/pass/array_literal_2.rs

@@ -0,0 +1,8 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let arr = [0i32, 0, 0, 0];
+    let s: &[i32] = &arr;
+    let _ = s[3];
+}

tests/ui/pass/array_literal_3.rs

@@ -0,0 +1,10 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let mut arr = [1i32, 2, 3];
+    let s: &mut [i32] = &mut arr;
+    s[0] = 42;
+    assert!(s[0] == 42);
+    assert!(s[1] == 2);
+}

tests/ui/pass/array_literal_4.rs

@@ -0,0 +1,12 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let mut x = 1i32;
+    let mut y = 2i32;
+    let arr: [&mut i32; 2] = [&mut x, &mut y];
+    let vx = *arr[0];
+    let vy = *arr[1];
+    assert!(vx == 1);
+    assert!(vy == 2);
+}

tests/ui/pass/slice_1.rs

@@ -0,0 +1,15 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result.len() > 0)]
+fn nonempty_slice() -> &'static [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let s = nonempty_slice();
+    assert!(s.len() > 0);
+    let _ = s[0];
+}

tests/ui/pass/slice_2.rs

@@ -0,0 +1,15 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result.len() >= 2)]
+fn two_elem_slice() -> &'static [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let s = two_elem_slice();
+    let _ = s[0];
+    let _ = s[1];
+}