Implement slice construction from array literals and Vec::as_slice

src/analyze/basic_block.rs

@@ -454,7 +454,13 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                     .unwrap();
                 self.const_value_ty(&val, ty)
             }
-            _ => unimplemented!("const: {:?}", const_),
+            mir::Const::Ty(ty, _) => {
+                let scalar_int = const_
+                    .try_to_scalar_int()
+                    .expect("type-level const must be a primitive scalar");
+                let val = mir::ConstValue::Scalar(mir::interpret::Scalar::Int(scalar_int));
+                self.const_value_ty(&val, ty)
+            }
         }
     }
 
@@ -473,6 +479,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     fn rvalue_type(&mut self, rvalue: Rvalue<'tcx>) -> PlaceType {
         match rvalue {
             Rvalue::Use(operand) => self.operand_type(operand),
+            Rvalue::CopyForDeref(place) => self.env.place_type(self.elaborate_place(&place)),
             Rvalue::UnaryOp(op, operand) => {
                 let operand_ty = self.operand_type(operand);
 
@@ -535,63 +542,98 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 builder.build(rty::PointerType::immut_to(ty).into(), chc::Term::box_(term))
             }
             Rvalue::Aggregate(kind, fields) => {
-                // elaboration: all fields are boxed
-                let field_tys: Vec<_> = fields
-                    .into_iter()
-                    .map(|operand| self.operand_type(operand).boxed())
-                    .collect();
                 match *kind {
-                    mir::AggregateKind::Adt(did, variant_idx, args, _, _)
-                        if self.tcx.def_kind(did) == DefKind::Enum =>
-                    {
-                        let enum_def = self.ctx.get_or_register_enum_def(did);
-                        let variant_def = &enum_def.variants[variant_idx];
-                        let variant_rtys = variant_def
-                            .field_tys
-                            .clone()
+                    mir::AggregateKind::Array(mir_elem_ty) => {
+                        // Build Seq<T> = (Box<Array<Int,T>>, Box<Int>) from array literal elements,
+                        // pinning each element at its index via store folds.
+                        let elem_ptys: Vec<_> = fields
                             .into_iter()
-                            .map(|ty| rty::RefinedType::unrefined(ty.vacuous()));
-
-                        let rty_args: IndexVec<_, _> = args
-                            .types()
-                            .map(|ty| {
-                                self.type_builder
-                                    .for_template(&mut self.ctx)
-                                    .with_scope(&self.env)
-                                    .build_refined(ty)
-                            })
+                            .map(|operand| self.operand_type(operand))
                             .collect();
-                        for (field_pty, mut variant_rty) in
-                            field_tys.clone().into_iter().zip(variant_rtys)
-                        {
-                            variant_rty.instantiate_ty_params(rty_args.clone());
-                            let cs = self
-                                .env
-                                .relate_sub_refined_type(&field_pty.into(), &variant_rty.boxed());
-                            self.ctx.extend_clauses(cs);
-                        }
-
-                        let sort_args: Vec<_> =
-                            rty_args.iter().map(|rty| rty.ty.to_sort()).collect();
-                        let ty = rty::EnumType::new(enum_def.name.clone(), rty_args).into();
-
+                        let n = elem_ptys.len();
                         let mut builder = PlaceTypeBuilder::default();
-                        let mut field_terms = Vec::new();
-                        for field_ty in field_tys {
-                            let (_, field_term) = builder.subsume(field_ty);
-                            field_terms.push(field_term);
+                        let elem_ty = elem_ptys.first().map_or_else(
+                            || self.type_builder.build(mir_elem_ty).vacuous(),
+                            |p| p.ty.clone(),
+                        );
+                        let base_idx = builder.push_existential(chc::Sort::array(
+                            chc::Sort::int(),
+                            elem_ty.to_sort(),
+                        ));
+                        let mut arr_term: chc::Term<PlaceTypeVar> = chc::Term::var(base_idx.into());
+                        for (i, pty) in elem_ptys.into_iter().enumerate() {
+                            let (_, elem_term) = builder.subsume(pty);
+                            arr_term = arr_term.store(chc::Term::int(i as i64), elem_term);
+                        }
+                        let arr_pty = builder.build(
+                            rty::ArrayType::new(rty::Type::int(), elem_ty).into(),
+                            arr_term,
+                        );
+                        let n_pty =
+                            PlaceType::with_ty_and_term(rty::Type::int(), chc::Term::int(n as i64));
+                        PlaceType::tuple(vec![arr_pty.boxed(), n_pty.boxed()])
+                    }
+                    other => {
+                        // elaboration: all fields are boxed
+                        let field_tys: Vec<_> = fields
+                            .into_iter()
+                            .map(|operand| self.operand_type(operand).boxed())
+                            .collect();
+                        match other {
+                            mir::AggregateKind::Adt(did, variant_idx, args, _, _)
+                                if self.tcx.def_kind(did) == DefKind::Enum =>
+                            {
+                                let enum_def = self.ctx.get_or_register_enum_def(did);
+                                let variant_def = &enum_def.variants[variant_idx];
+                                let variant_rtys = variant_def
+                                    .field_tys
+                                    .clone()
+                                    .into_iter()
+                                    .map(|ty| rty::RefinedType::unrefined(ty.vacuous()));
+
+                                let rty_args: IndexVec<_, _> = args
+                                    .types()
+                                    .map(|ty| {
+                                        self.type_builder
+                                            .for_template(&mut self.ctx)
+                                            .with_scope(&self.env)
+                                            .build_refined(ty)
+                                    })
+                                    .collect();
+                                for (field_pty, mut variant_rty) in
+                                    field_tys.clone().into_iter().zip(variant_rtys)
+                                {
+                                    variant_rty.instantiate_ty_params(rty_args.clone());
+                                    let cs = self.env.relate_sub_refined_type(
+                                        &field_pty.into(),
+                                        &variant_rty.boxed(),
+                                    );
+                                    self.ctx.extend_clauses(cs);
+                                }
+
+                                let sort_args: Vec<_> =
+                                    rty_args.iter().map(|rty| rty.ty.to_sort()).collect();
+                                let ty = rty::EnumType::new(enum_def.name.clone(), rty_args).into();
+
+                                let mut builder = PlaceTypeBuilder::default();
+                                let mut field_terms = Vec::new();
+                                for field_ty in field_tys {
+                                    let (_, field_term) = builder.subsume(field_ty);
+                                    field_terms.push(field_term);
+                                }
+                                builder.build(
+                                    ty,
+                                    chc::Term::datatype_ctor(
+                                        enum_def.name,
+                                        sort_args,
+                                        variant_def.name.clone(),
+                                        field_terms,
+                                    ),
+                                )
+                            }
+                            _ => PlaceType::tuple(field_tys),
                         }
-                        builder.build(
-                            ty,
-                            chc::Term::datatype_ctor(
-                                enum_def.name,
-                                sort_args,
-                                variant_def.name.clone(),
-                                field_terms,
-                            ),
-                        )
                     }
-                    _ => PlaceType::tuple(field_tys),
                 }
             }
             Rvalue::Cast(
@@ -608,6 +650,15 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 };
                 PlaceType::with_ty_and_term(func_ty.vacuous(), chc::Term::null())
             }
+            Rvalue::Cast(
+                mir::CastKind::PointerCoercion(mir_ty::adjustment::PointerCoercion::Unsize, _),
+                operand,
+                _ty,
+            ) => {
+                // &[T; N] → &[T] and similar unsizings: both sides share the same Seq model,
+                // so the coercion is identity.
+                self.operand_type(operand)
+            }
             Rvalue::Discriminant(place) => {
                 let place = self.elaborate_place(&place);
                 let ty = self.env.place_type(place);

src/analyze/reconstruct_slice_indexing.rs

@@ -269,7 +269,7 @@ fn reconstruct_access<'tcx>(
         result_local,
     );
     let receiver = receiver_operand(tcx, body, &bounds_check, &access, region);
-    remove_bounds_check_setup(body, &bounds_check);
+    remove_bounds_check_setup(body, &bounds_check, access.receiver.local);
 
     let (lang_item, method_name) = if access.mutable {
         (LangItem::IndexMut, sym::index_mut)
@@ -358,7 +358,11 @@ fn receiver_operand<'tcx>(
 }
 
 /// Removes the MIR temporaries that only supported the now-replaced bounds check.
-fn remove_bounds_check_setup<'tcx>(body: &mut Body<'tcx>, bounds_check: &BoundsCheck<'tcx>) {
+fn remove_bounds_check_setup<'tcx>(
+    body: &mut Body<'tcx>,
+    bounds_check: &BoundsCheck<'tcx>,
+    receiver_local: Local,
+) {
     let mut lowered_locals: Vec<_> = bounds_check.condition_local.into_iter().collect();
     if let Some(len_place) = bounds_check
         .len
@@ -373,7 +377,13 @@ fn remove_bounds_check_setup<'tcx>(body: &mut Body<'tcx>, bounds_check: &BoundsC
                 continue;
             };
             if lhs.local == len_place.local {
-                if let Some(raw_place) = operand.place().filter(|place| place.projection.is_empty())
+                // Only include the PtrMetadata operand if it is a distinct temporary — i.e.
+                // not the receiver that the reconstructed Index::index call will use.
+                // When PtrMetadata is applied directly to the slice reference (the receiver),
+                // that local must not be NOP'd: its assignment may be in this same block.
+                if let Some(raw_place) = operand
+                    .place()
+                    .filter(|place| place.projection.is_empty() && place.local != receiver_local)
                 {
                     lowered_locals.push(raw_place.local);
                 }

std.rs

@@ -368,6 +368,10 @@ mod thrust_models {
         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>;
     }
@@ -800,6 +804,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/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/vec_as_ref.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.as_ref();
+    assert!(s[0] == 99); // wrong value → Unsat
+}

tests/ui/fail/vec_as_slice.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 = Vec::as_slice(&v);
+    assert!(s[0] == 99); // wrong value → Unsat
+}

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/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/vec_as_ref.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.as_ref();
+    assert!(s.len() == 2);
+    assert!(s[0] == 10);
+    assert!(s[1] == 20);
+}

tests/ui/pass/vec_as_slice.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 = Vec::as_slice(&v);
+    assert!(s.len() == 2);
+    assert!(s[0] == 10);
+    assert!(s[1] == 20);
+}