Give the Seq model named array and length fields

src/analyze/annot_fn.rs

@@ -621,6 +621,28 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                 let terms = exprs.iter().map(|e| self.to_term(e)).collect();
                 FormulaOrTerm::Term(chc::Term::tuple(terms))
             }
+            ExprKind::Struct(_qpath, fields, tail) => {
+                if !matches!(tail, rustc_hir::StructTailExpr::None) {
+                    unimplemented!("struct update syntax is not supported in formulas");
+                }
+                let adt = self
+                    .expr_ty(hir)
+                    .ty_adt_def()
+                    .expect("struct literal on a non-ADT type");
+                let mut terms = Vec::new();
+                let variant = adt.non_enum_variant();
+                for variant_field in &variant.fields {
+                    let Some(field) = fields.iter().find(|f| f.ident.name == variant_field.name)
+                    else {
+                        self.tcx.dcx().span_fatal(
+                            hir.span,
+                            format!("missing field `{}` in struct literal", variant_field.name),
+                        );
+                    };
+                    terms.push(self.to_term(field.expr));
+                }
+                FormulaOrTerm::Term(chc::Term::tuple(terms))
+            }
             ExprKind::Field(expr, field) => {
                 // Tuples use numeric field names (`.0`); structs (represented as
                 // tuples in the logic) use named fields resolved to their position.

std.rs

@@ -188,7 +188,10 @@ mod thrust_models {
         }
 
         #[thrust::def::seq_model]
-        pub struct Seq<T: ?Sized>(pub Array<Int, T>, pub Int);
+        pub struct Seq<T: ?Sized> {
+            pub array: Array<Int, T>,
+            pub length: Int,
+        }
 
         impl<T, U> PartialEq<U> for Seq<T> where U: super::Model<Ty = Self> {
             #[thrust::ignored]
@@ -716,14 +719,14 @@ fn _extern_spec_i32_is_negative(x: i32) -> bool {
 
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result.1 == 0)]
+#[thrust_macros::ensures(result.length == 0)]
 fn _extern_spec_vec_new<T>() -> Vec<T> where T: thrust_models::Model, T::Ty: PartialEq {
     Vec::<T>::new()
 }
 
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
-#[thrust_macros::ensures(!vec == thrust_models::model::Seq((*vec).0.store((*vec).1, elem), (*vec).1 + 1))]
+#[thrust_macros::ensures(!vec == thrust_models::model::Seq { array: (*vec).array.store((*vec).length, elem), length: (*vec).length + 1 })]
 fn _extern_spec_vec_push<T>(vec: &mut Vec<T>, elem: T)
     where T: thrust_models::Model, T::Ty: PartialEq
 {
@@ -732,24 +735,24 @@ fn _extern_spec_vec_push<T>(vec: &mut Vec<T>, elem: T)
 
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result == vec.1)]
+#[thrust_macros::ensures(result == (*vec).length)]
 fn _extern_spec_vec_len<T>(vec: &Vec<T>) -> usize where T: thrust_models::Model, T::Ty: PartialEq {
     Vec::len(vec)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust_macros::requires(index < vec.1)]
-#[thrust_macros::ensures(*result == vec.0[index])]
+#[thrust_macros::requires(index < (*vec).length)]
+#[thrust_macros::ensures(*result == (*vec).array[index])]
 fn _extern_spec_vec_index<T>(vec: &Vec<T>, index: usize) -> &T where T: thrust_models::Model, T::Ty: PartialEq {
     <Vec<T> as std::ops::Index<usize>>::index(vec, index)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust_macros::requires(index < (*vec).1)]
+#[thrust_macros::requires(index < (*vec).length)]
 #[thrust_macros::ensures(
-    *result == (*vec).0[index] &&
-    !result == (!vec).0[index] &&
-    !vec == thrust_models::model::Seq((*vec).0.store(index, !result), (*vec).1)
+    *result == (*vec).array[index] &&
+    !result == (!vec).array[index] &&
+    !vec == thrust_models::model::Seq { array: (*vec).array.store(index, !result), length: (*vec).length }
 )]
 fn _extern_spec_vec_index_mut<T>(vec: &mut Vec<T>, index: usize) -> &mut T
     where T: thrust_models::Model, T::Ty: PartialEq
@@ -759,22 +762,22 @@ fn _extern_spec_vec_index_mut<T>(vec: &mut Vec<T>, index: usize) -> &mut T
 
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
-#[thrust_macros::ensures((!vec).1 == 0)]
+#[thrust_macros::ensures((!vec).length == 0)]
 fn _extern_spec_vec_clear<T>(vec: &mut Vec<T>) where T: thrust_models::Model, T::Ty: PartialEq {
     Vec::clear(vec)
 }
 
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (!vec).0 == (*vec).0 && (
+    (!vec).array == (*vec).array && (
         (
-            (*vec).1 > 0 &&
-            (!vec).1 == (*vec).1 - 1 &&
-            result == Some((*vec).0[(*vec).1 - 1])
+            (*vec).length > 0 &&
+            (!vec).length == (*vec).length - 1 &&
+            result == Some((*vec).array[(*vec).length - 1])
         ) || (
-            (*vec).1 == 0 &&
-            (!vec).1 == 0 &&
+            (*vec).length == 0 &&
+            (!vec).length == 0 &&
             result == None
         )
     )
@@ -785,7 +788,7 @@ fn _extern_spec_vec_pop<T>(vec: &mut Vec<T>) -> Option<T> where T: thrust_models
 
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result == ((*vec).1 == 0))]
+#[thrust_macros::ensures(result == ((*vec).length == 0))]
 fn _extern_spec_vec_is_empty<T>(vec: &Vec<T>) -> bool where T: thrust_models::Model, T::Ty: PartialEq {
     Vec::is_empty(vec)
 }
@@ -794,10 +797,10 @@ fn _extern_spec_vec_is_empty<T>(vec: &Vec<T>) -> bool where T: thrust_models::Mo
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
     (
-        (*vec).1 > len &&
-        !vec == thrust_models::model::Seq((*vec).0, len)
+        (*vec).length > len &&
+        !vec == thrust_models::model::Seq { array: (*vec).array, length: len }
     ) || (
-        (*vec).1 <= len &&
+        (*vec).length <= len &&
         !vec == *vec
     )
 )]
@@ -834,7 +837,7 @@ fn _extern_spec_vec_as_ref<T>(vec: &Vec<T>) -> &[T]
 
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result == slice.1)]
+#[thrust_macros::ensures(result == (*slice).length)]
 fn _extern_spec_slice_len<T>(slice: &[T]) -> usize
     where T: thrust_models::Model, T::Ty: PartialEq
 {
@@ -843,7 +846,7 @@ fn _extern_spec_slice_len<T>(slice: &[T]) -> usize
 
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result == (slice.1 == 0))]
+#[thrust_macros::ensures(result == ((*slice).length == 0))]
 fn _extern_spec_slice_is_empty<T>(slice: &[T]) -> bool
     where T: thrust_models::Model, T::Ty: PartialEq
 {
@@ -853,8 +856,8 @@ fn _extern_spec_slice_is_empty<T>(slice: &[T]) -> bool
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (index < slice.1 && result == Some(&slice.0[index]))
-    || (slice.1 <= index && result == None)
+    (index < (*slice).length && result == Some(&(*slice).array[index]))
+    || ((*slice).length <= index && result == None)
 )]
 fn _extern_spec_slice_get<T>(slice: &[T], index: usize) -> Option<&T>
     where T: thrust_models::Model, T::Ty: PartialEq
@@ -865,17 +868,17 @@ fn _extern_spec_slice_get<T>(slice: &[T], index: usize) -> Option<&T>
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (index < (*slice).1
+    (index < (*slice).length
         && result == Some(thrust_models::model::Mut::new(
-            (*slice).0[index],
-            (!slice).0[index],
+            (*slice).array[index],
+            (!slice).array[index],
         ))
-        && !slice == thrust_models::model::Seq(
-            (*slice).0.store(index, (!slice).0[index]),
-            (*slice).1,
-        )
+        && !slice == thrust_models::model::Seq {
+            array: (*slice).array.store(index, (!slice).array[index]),
+            length: (*slice).length,
+        }
     )
-    || ((*slice).1 <= index && result == None && !slice == *slice)
+    || ((*slice).length <= index && result == None && !slice == *slice)
 )]
 fn _extern_spec_slice_get_mut<T>(slice: &mut [T], index: usize) -> Option<&mut T>
     where T: thrust_models::Model, T::Ty: PartialEq
@@ -886,8 +889,8 @@ fn _extern_spec_slice_get_mut<T>(slice: &mut [T], index: usize) -> Option<&mut T
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (slice.1 > 0 && result == Some(&slice.0[0]))
-    || (slice.1 == 0 && result == None)
+    ((*slice).length > 0 && result == Some(&(*slice).array[0]))
+    || ((*slice).length == 0 && result == None)
 )]
 fn _extern_spec_slice_first<T>(slice: &[T]) -> Option<&T>
     where T: thrust_models::Model, T::Ty: PartialEq
@@ -898,17 +901,17 @@ fn _extern_spec_slice_first<T>(slice: &[T]) -> Option<&T>
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    ((*slice).1 > 0
+    ((*slice).length > 0
         && result == Some(thrust_models::model::Mut::new(
-            (*slice).0[0],
-            (!slice).0[0],
+            (*slice).array[0],
+            (!slice).array[0],
         ))
-        && !slice == thrust_models::model::Seq(
-            (*slice).0.store(0, (!slice).0[0]),
-            (*slice).1,
-        )
+        && !slice == thrust_models::model::Seq {
+            array: (*slice).array.store(0, (!slice).array[0]),
+            length: (*slice).length,
+        }
     )
-    || ((*slice).1 == 0 && result == None && !slice == *slice)
+    || ((*slice).length == 0 && result == None && !slice == *slice)
 )]
 fn _extern_spec_slice_first_mut<T>(slice: &mut [T]) -> Option<&mut T>
     where T: thrust_models::Model, T::Ty: PartialEq
@@ -919,8 +922,8 @@ fn _extern_spec_slice_first_mut<T>(slice: &mut [T]) -> Option<&mut T>
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (slice.1 > 0 && result == Some(&slice.0[slice.1 - 1]))
-    || (slice.1 == 0 && result == None)
+    ((*slice).length > 0 && result == Some(&(*slice).array[(*slice).length - 1]))
+    || ((*slice).length == 0 && result == None)
 )]
 fn _extern_spec_slice_last<T>(slice: &[T]) -> Option<&T>
     where T: thrust_models::Model, T::Ty: PartialEq
@@ -931,20 +934,20 @@ fn _extern_spec_slice_last<T>(slice: &[T]) -> Option<&T>
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    ((*slice).1 > 0
+    ((*slice).length > 0
         && result == Some(thrust_models::model::Mut::new(
-            (*slice).0[(*slice).1 - 1],
-            (!slice).0[(*slice).1 - 1],
+            (*slice).array[(*slice).length - 1],
+            (!slice).array[(*slice).length - 1],
         ))
-        && !slice == thrust_models::model::Seq(
-            (*slice).0.store(
-                (*slice).1 - 1,
-                (!slice).0[(*slice).1 - 1],
+        && !slice == thrust_models::model::Seq {
+            array: (*slice).array.store(
+                (*slice).length - 1,
+                (!slice).array[(*slice).length - 1],
             ),
-            (*slice).1,
-        )
+            length: (*slice).length,
+        }
     )
-    || ((*slice).1 == 0 && result == None && !slice == *slice)
+    || ((*slice).length == 0 && result == None && !slice == *slice)
 )]
 fn _extern_spec_slice_last_mut<T>(slice: &mut [T]) -> Option<&mut T>
     where T: thrust_models::Model, T::Ty: PartialEq
@@ -956,23 +959,23 @@ fn _extern_spec_slice_last_mut<T>(slice: &mut [T]) -> Option<&mut T>
 //       a generic index (I: SliceIndex) that isn't specific to usize, maybe once #83 is implemented.
 
 #[thrust::extern_spec_fn]
-#[thrust_macros::requires(index < slice.1)]
-#[thrust_macros::ensures(*result == slice.0[index])]
+#[thrust_macros::requires(index < (*slice).length)]
+#[thrust_macros::ensures(*result == (*slice).array[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::requires(index < (*slice).length)]
 #[thrust_macros::ensures(
-    *result == (*slice).0[index] &&
-    !result == (!slice).0[index] &&
-    !slice == thrust_models::model::Seq(
-        (*slice).0.store(index, !result),
-        (*slice).1,
-    )
+    *result == (*slice).array[index] &&
+    !result == (!slice).array[index] &&
+    !slice == thrust_models::model::Seq {
+        array: (*slice).array.store(index, !result),
+        length: (*slice).length,
+    }
 )]
 fn _extern_spec_slice_index_mut<T>(slice: &mut [T], index: usize) -> &mut T
     where T: thrust_models::Model, T::Ty: PartialEq

tests/ui/fail/loop_invariant_fn_param_at_entry.rs

@@ -2,15 +2,15 @@
 //@compile-flags: -C debug-assertions=off
 
 #[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result.1 == v.1 + 2)]
+#[thrust_macros::ensures(result.length == v.length + 2)]
 #[thrust_macros::invariant_context]
 fn push_two(v: Vec<i64>) -> Vec<i64> {
     let mut w = v;
     let mut i = 0_i64;
     while i < 2 {
         thrust_macros::invariant!(
             |i: i64, w: Vec<i64>, v: thrust_models::FnParam<Vec<i64>>|
-                w.1 == v.at_entry().1 + i && i <= 2
+                w.length == v.at_entry().length + i && i <= 2
         );
         w.push(i);
         w.push(i);

tests/ui/fail/seq_specs_vec_build.rs

@@ -6,11 +6,11 @@ use thrust_models::model::Seq;
 
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    result.1 == Seq::empty().push(10).push(20).push(30).len()
-        && result.0[0] == Seq::empty().push(10).push(20).push(30)[0]
-        && result.0[1] == Seq::empty().push(10).push(20).push(30)[1]
+    result.length == Seq::empty().push(10).push(20).push(30).len()
+        && result.array[0] == Seq::empty().push(10).push(20).push(30)[0]
+        && result.array[1] == Seq::empty().push(10).push(20).push(30)[1]
         // wrong: last element should be 30, not 99
-        && result.0[2] == Seq::empty().push(10).push(20).push(99)[2]
+        && result.array[2] == Seq::empty().push(10).push(20).push(99)[2]
 )]
 fn build_three() -> Vec<i64> {
     let mut v = Vec::new();

tests/ui/fail/slice_first_mut.rs

@@ -4,7 +4,7 @@
 #[thrust::trusted]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (*result).1 > 0 && (*result).0[0] == 10
+    (*result).length > 0 && (*result).array[0] == 10
 )]
 fn slice() -> &'static mut [i32] {
     unimplemented!()

tests/ui/fail/slice_index.rs

@@ -3,7 +3,7 @@
 
 #[thrust::trusted]
 #[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result.1 == 1 && result.0[0] == 10)]
+#[thrust_macros::ensures((*result).length == 1 && (*result).array[0] == 10)]
 fn slice() -> &'static [i32] {
     unimplemented!()
 }

tests/ui/fail/slice_index_mut.rs

@@ -4,7 +4,7 @@
 #[thrust::trusted]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (*result).1 > 1 && (*result).0[1] == 20
+    (*result).length > 1 && (*result).array[1] == 20
 )]
 fn slice() -> &'static mut [i32] {
     unimplemented!()

tests/ui/fail/slice_last_mut.rs

@@ -4,8 +4,8 @@
 #[thrust::trusted]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (*result).1 > 0
-        && (*result).0[(*result).1 - 1] == 30
+    (*result).length > 0
+        && (*result).array[(*result).length - 1] == 30
 )]
 fn slice() -> &'static mut [i32] {
     unimplemented!()

tests/ui/fail/slice_methods.rs

@@ -4,9 +4,9 @@
 #[thrust::trusted]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    result.1 == 2
-        && result.0[0] == 10
-        && result.0[1] == 20
+    (*result).length == 2
+        && (*result).array[0] == 10
+        && (*result).array[1] == 20
 )]
 fn slice() -> &'static [i32] {
     unimplemented!()