Add an offset field to the Seq model

src/analyze/annot_fn.rs

@@ -672,12 +672,15 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                 let is_seq = array_ty
                     .ty_adt_def()
                     .is_some_and(|adt| Some(adt.did()) == self.def_ids.seq_model());
-                let array_inner = if is_seq {
-                    array_term.tuple_proj(0)
+                if is_seq {
+                    // Indexing a sequence is offset-aware: `s[i]` reads the underlying array at
+                    // `offset + i`.
+                    let offset = array_term.clone().tuple_proj(1);
+                    let array_inner = array_term.tuple_proj(0);
+                    FormulaOrTerm::Term(array_inner.select(offset.add(index_term)))
                 } else {
-                    array_term
-                };
-                FormulaOrTerm::Term(array_inner.select(index_term))
+                    FormulaOrTerm::Term(array_term.select(index_term))
+                }
             }
             ExprKind::MethodCall(method, receiver, args, _) => {
                 if let Some(def_id) = self.typeck.type_dependent_def_id(hir.hir_id) {
@@ -699,28 +702,34 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                     if Some(def_id) == self.def_ids.seq_len() {
                         assert!(args.is_empty(), "Seq::len does not take any arguments");
                         let t = self.to_term(receiver);
-                        return FormulaOrTerm::Term(t.tuple_proj(1));
+                        return FormulaOrTerm::Term(t.tuple_proj(2));
                     }
                     if Some(def_id) == self.def_ids.seq_push() {
                         assert_eq!(args.len(), 1, "Seq::push takes exactly 1 argument");
                         let t = self.to_term(receiver);
                         let v = self.to_term(&args[0]);
                         let arr = t.clone().tuple_proj(0);
-                        let len = t.tuple_proj(1);
-                        let new_arr = arr.store(len.clone(), v);
+                        let offset = t.clone().tuple_proj(1);
+                        let len = t.tuple_proj(2);
+                        let new_arr = arr.store(offset.clone().add(len.clone()), v);
                         let new_len = len.add(chc::Term::int(1));
-                        return FormulaOrTerm::Term(chc::Term::tuple(vec![new_arr, new_len]));
+                        return FormulaOrTerm::Term(chc::Term::tuple(vec![
+                            new_arr, offset, new_len,
+                        ]));
                     }
                     if Some(def_id) == self.def_ids.seq_concat() {
                         assert_eq!(args.len(), 1, "Seq::concat takes exactly 1 argument");
                         let elem_sort = self.adt_arg_type_at(receiver, 0).to_sort();
                         let t = self.to_term(receiver);
                         let other = self.to_term(&args[0]);
-                        let a_len = t.clone().tuple_proj(1);
-                        let b_len = other.clone().tuple_proj(1);
+                        let a_offset = t.clone().tuple_proj(1);
+                        let a_len = t.clone().tuple_proj(2);
+                        let b_len = other.clone().tuple_proj(2);
                         let new_arr = chc::Term::array_concat(elem_sort, t, other);
                         let new_len = a_len.add(b_len);
-                        return FormulaOrTerm::Term(chc::Term::tuple(vec![new_arr, new_len]));
+                        return FormulaOrTerm::Term(chc::Term::tuple(vec![
+                            new_arr, a_offset, new_len,
+                        ]));
                     }
                 }
                 unimplemented!("unsupported method call in formula: {:?}", method)
@@ -803,6 +812,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                             return FormulaOrTerm::Term(chc::Term::tuple(vec![
                                 chc::Term::array_empty(chc::Sort::int(), elem_sort),
                                 chc::Term::int(0),
+                                chc::Term::int(0),
                             ]));
                         }
                         if Some(def_id) == self.def_ids.seq_singleton() {
@@ -813,6 +823,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                                 .store(chc::Term::int(0), v);
                             return FormulaOrTerm::Term(chc::Term::tuple(vec![
                                 new_arr,
+                                chc::Term::int(0),
                                 chc::Term::int(1),
                             ]));
                         }

src/analyze/basic_block.rs

@@ -544,8 +544,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             Rvalue::Aggregate(kind, fields) => {
                 match *kind {
                     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.
+                        // Build Seq<T> = (Box<Array<Int,T>>, Box<Int>, Box<Int>) from array literal
+                        // elements, pinning each element at its index via store folds. The offset
+                        // of a freshly built array is 0.
                         //
                         // TODO: Stop embedding knowledge of `<[T; N] as Model>::Ty` in the analyzer
                         let mut builder = PlaceTypeBuilder::default();
@@ -561,12 +562,18 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                             rty::ArrayType::new(rty::Type::int(), elem_ty).into(),
                             arr_term,
                         );
+                        let offset_pty =
+                            PlaceType::with_ty_and_term(rty::Type::int(), chc::Term::int(0));
                         let size = fields.len();
                         let size_pty = PlaceType::with_ty_and_term(
                             rty::Type::int(),
                             chc::Term::int(size as i64),
                         );
-                        PlaceType::tuple(vec![arr_pty.boxed(), size_pty.boxed()])
+                        PlaceType::tuple(vec![
+                            arr_pty.boxed(),
+                            offset_pty.boxed(),
+                            size_pty.boxed(),
+                        ])
                     }
                     mir::AggregateKind::Adt(did, variant_idx, args, _, _)
                         if self.tcx.def_kind(did) == DefKind::Enum =>

src/chc.rs

@@ -871,15 +871,19 @@ impl<V> Term<V> {
         // indexed properties against the inlined ITE for *any* recursion bound, where unfolding
         // through `define-fun-rec` would require an inductive invariant pcsat can't find.
         //
-        // `select(concat_int_array(s, t), i)
-        //   ↦ ite(i < len(s), select(array(s), i), select(array(t), i - len(s)))`
-        // where `s`/`t` are `(array, length)` tuples.
+        // `select(concat_int_array(s, t), i)`
+        //   ↦ ite(i < offset(s) + length(s),
+        //         select(array(s), i),
+        //         select(array(t), offset(t) + i - (offset(s) + length(s))))`
+        // where `s`/`t` are `(array, offset, length)` tuples and `i` is an absolute index into
+        // the concatenated array (which reuses `s`'s offset).
         if let Term::ArrayConcat(_, t) = self {
             let ArrayConcatTerm { seq1, seq2 } = *t;
-            let len1 = seq1.clone().tuple_proj(1);
-            let cond = index.clone().lt(len1.clone());
+            let split = seq1.clone().tuple_proj(1).add(seq1.clone().tuple_proj(2));
+            let offset2 = seq2.clone().tuple_proj(1);
+            let cond = index.clone().lt(split.clone());
             let then_ = seq1.tuple_proj(0).select(index.clone());
-            let else_ = seq2.tuple_proj(0).select(index.sub(len1));
+            let else_ = seq2.tuple_proj(0).select(offset2.add(index.sub(split)));
             return Term::ite(cond, then_, else_);
         }
         Term::App(Function::SELECT, vec![self, index])

src/chc/format_context.rs

@@ -283,13 +283,14 @@ impl FormatContext {
                 _ => None,
             })
             .collect();
-        // The `concat_int_array` definitions operate on `(array, length)` sequence tuples, so
-        // make sure that tuple datatype is declared for every element sort we emit one for, even
-        // when no sequence value of that element sort otherwise appears in the system.
+        // The `concat_int_array` definitions operate on `(array, offset, length)` sequence
+        // tuples, so make sure that tuple datatype is declared for every element sort we emit one
+        // for, even when no sequence value of that element sort otherwise appears in the system.
         for elem in &int_array_elem_sorts {
             sorts.insert(chc::Sort::tuple(vec![
                 chc::Sort::array(chc::Sort::int(), elem.clone()),
                 chc::Sort::int(),
+                chc::Sort::int(),
             ]));
         }
         let datatypes: Vec<_> = sorts

src/chc/smtlib2.rs

@@ -641,25 +641,29 @@ impl<'a> std::fmt::Display for System<'a> {
         for elem in self.ctx.int_array_elem_sorts() {
             let name = self.ctx.concat_int_array(elem);
             let elem_ty = self.ctx.fmt_sort(elem);
-            // The sequences are passed as `(array, length)` tuples; project their fields
-            // instead of taking the array and length as separate parameters.
+            // The sequences are passed as `(array, offset, length)` tuples; project their fields
+            // instead of taking the array and length as separate parameters. The concatenated
+            // array keeps `s`'s offset: `s`'s elements stay in place and `t`'s elements are
+            // appended right after them.
             let seq_fields = [
                 chc::Sort::array(chc::Sort::int(), elem.clone()),
                 chc::Sort::int(),
+                chc::Sort::int(),
             ];
             let seq_ty = self.ctx.fmt_sort(&chc::Sort::tuple(seq_fields.to_vec()));
             let ctor = self.ctx.tuple_ctor(&seq_fields);
             let array = self.ctx.tuple_proj(&seq_fields, 0);
-            let len = self.ctx.tuple_proj(&seq_fields, 1);
+            let off = self.ctx.tuple_proj(&seq_fields, 1);
+            let len = self.ctx.tuple_proj(&seq_fields, 2);
             writeln!(
                 f,
                 "(define-fun-rec {name} \
                   ((s {seq_ty}) (t {seq_ty})) \
                   (Array Int {elem_ty}) \
                   (ite (<= ({len} t) 0) ({array} s) \
-                       (store ({name} s ({ctor} ({array} t) (- ({len} t) 1))) \
-                              (+ ({len} s) (- ({len} t) 1)) \
-                              (select ({array} t) (- ({len} t) 1)))))\n",
+                       (store ({name} s ({ctor} ({array} t) ({off} t) (- ({len} t) 1))) \
+                              (+ ({off} s) ({len} s) (- ({len} t) 1)) \
+                              (select ({array} t) (+ ({off} t) (- ({len} t) 1))))))\n",
             )?;
         }
 

std.rs

@@ -190,6 +190,7 @@ mod thrust_models {
         #[thrust::def::seq_model]
         pub struct Seq<T: ?Sized> {
             pub array: Array<Int, T>,
+            pub offset: Int,
             pub length: Int,
         }
 
@@ -719,14 +720,14 @@ fn _extern_spec_i32_is_negative(x: i32) -> bool {
 
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result.length == 0)]
+#[thrust_macros::ensures(result.offset == 0 && 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 { array: (*vec).array.store((*vec).length, elem), length: (*vec).length + 1 })]
+#[thrust_macros::ensures(!vec == thrust_models::model::Seq { array: (*vec).array.store((*vec).offset + (*vec).length, elem), offset: (*vec).offset, length: (*vec).length + 1 })]
 fn _extern_spec_vec_push<T>(vec: &mut Vec<T>, elem: T)
     where T: thrust_models::Model, T::Ty: PartialEq
 {
@@ -742,17 +743,17 @@ fn _extern_spec_vec_len<T>(vec: &Vec<T>) -> usize where T: thrust_models::Model,
 
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(index < (*vec).length)]
-#[thrust_macros::ensures(*result == (*vec).array[index])]
+#[thrust_macros::ensures(*result == (*vec).array[(*vec).offset + 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).length)]
 #[thrust_macros::ensures(
-    *result == (*vec).array[index] &&
-    !result == (!vec).array[index] &&
-    !vec == thrust_models::model::Seq { array: (*vec).array.store(index, !result), length: (*vec).length }
+    *result == (*vec).array[(*vec).offset + index] &&
+    !result == (!vec).array[(!vec).offset + index] &&
+    !vec == thrust_models::model::Seq { array: (*vec).array.store((*vec).offset + index, !result), offset: (*vec).offset, 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
@@ -762,19 +763,21 @@ 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).length == 0)]
+#[thrust_macros::ensures(
+    (!vec).array == (*vec).array && (!vec).offset == (*vec).offset && (!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).array == (*vec).array && (
+    (!vec).array == (*vec).array && (!vec).offset == (*vec).offset && (
         (
             (*vec).length > 0 &&
             (!vec).length == (*vec).length - 1 &&
-            result == Some((*vec).array[(*vec).length - 1])
+            result == Some((*vec).array[(*vec).offset + (*vec).length - 1])
         ) || (
             (*vec).length == 0 &&
             (!vec).length == 0 &&
@@ -798,7 +801,7 @@ fn _extern_spec_vec_is_empty<T>(vec: &Vec<T>) -> bool where T: thrust_models::Mo
 #[thrust_macros::ensures(
     (
         (*vec).length > len &&
-        !vec == thrust_models::model::Seq { array: (*vec).array, length: len }
+        !vec == thrust_models::model::Seq { array: (*vec).array, offset: (*vec).offset, length: len }
     ) || (
         (*vec).length <= len &&
         !vec == *vec
@@ -856,7 +859,7 @@ fn _extern_spec_slice_is_empty<T>(slice: &[T]) -> bool
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (index < (*slice).length && result == Some(&(*slice).array[index]))
+    (index < (*slice).length && result == Some(&(*slice).array[(*slice).offset + index]))
     || ((*slice).length <= index && result == None)
 )]
 fn _extern_spec_slice_get<T>(slice: &[T], index: usize) -> Option<&T>
@@ -870,11 +873,12 @@ fn _extern_spec_slice_get<T>(slice: &[T], index: usize) -> Option<&T>
 #[thrust_macros::ensures(
     (index < (*slice).length
         && result == Some(thrust_models::model::Mut::new(
-            (*slice).array[index],
-            (!slice).array[index],
+            (*slice).array[(*slice).offset + index],
+            (!slice).array[(*slice).offset + index],
         ))
         && !slice == thrust_models::model::Seq {
-            array: (*slice).array.store(index, (!slice).array[index]),
+            array: (*slice).array.store((*slice).offset + index, (!slice).array[(*slice).offset + index]),
+            offset: (*slice).offset,
             length: (*slice).length,
         }
     )
@@ -889,7 +893,7 @@ 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).length > 0 && result == Some(&(*slice).array[0]))
+    ((*slice).length > 0 && result == Some(&(*slice).array[(*slice).offset]))
     || ((*slice).length == 0 && result == None)
 )]
 fn _extern_spec_slice_first<T>(slice: &[T]) -> Option<&T>
@@ -903,11 +907,12 @@ fn _extern_spec_slice_first<T>(slice: &[T]) -> Option<&T>
 #[thrust_macros::ensures(
     ((*slice).length > 0
         && result == Some(thrust_models::model::Mut::new(
-            (*slice).array[0],
-            (!slice).array[0],
+            (*slice).array[(*slice).offset],
+            (!slice).array[(*slice).offset],
         ))
         && !slice == thrust_models::model::Seq {
-            array: (*slice).array.store(0, (!slice).array[0]),
+            array: (*slice).array.store((*slice).offset, (!slice).array[(*slice).offset]),
+            offset: (*slice).offset,
             length: (*slice).length,
         }
     )
@@ -922,7 +927,7 @@ 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).length > 0 && result == Some(&(*slice).array[(*slice).length - 1]))
+    ((*slice).length > 0 && result == Some(&(*slice).array[(*slice).offset + (*slice).length - 1]))
     || ((*slice).length == 0 && result == None)
 )]
 fn _extern_spec_slice_last<T>(slice: &[T]) -> Option<&T>
@@ -936,14 +941,15 @@ fn _extern_spec_slice_last<T>(slice: &[T]) -> Option<&T>
 #[thrust_macros::ensures(
     ((*slice).length > 0
         && result == Some(thrust_models::model::Mut::new(
-            (*slice).array[(*slice).length - 1],
-            (!slice).array[(*slice).length - 1],
+            (*slice).array[(*slice).offset + (*slice).length - 1],
+            (!slice).array[(*slice).offset + (*slice).length - 1],
         ))
         && !slice == thrust_models::model::Seq {
             array: (*slice).array.store(
-                (*slice).length - 1,
-                (!slice).array[(*slice).length - 1],
+                (*slice).offset + (*slice).length - 1,
+                (!slice).array[(*slice).offset + (*slice).length - 1],
             ),
+            offset: (*slice).offset,
             length: (*slice).length,
         }
     )
@@ -960,7 +966,7 @@ fn _extern_spec_slice_last_mut<T>(slice: &mut [T]) -> Option<&mut T>
 
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(index < (*slice).length)]
-#[thrust_macros::ensures(*result == (*slice).array[index])]
+#[thrust_macros::ensures(*result == (*slice).array[(*slice).offset + index])]
 fn _extern_spec_slice_index<T>(slice: &[T], index: usize) -> &T
     where T: thrust_models::Model, T::Ty: PartialEq
 {
@@ -970,10 +976,11 @@ fn _extern_spec_slice_index<T>(slice: &[T], index: usize) -> &T
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(index < (*slice).length)]
 #[thrust_macros::ensures(
-    *result == (*slice).array[index] &&
-    !result == (!slice).array[index] &&
+    *result == (*slice).array[(*slice).offset + index] &&
+    !result == (!slice).array[(!slice).offset + index] &&
     !slice == thrust_models::model::Seq {
-        array: (*slice).array.store(index, !result),
+        array: (*slice).array.store((*slice).offset + index, !result),
+        offset: (*slice).offset,
         length: (*slice).length,
     }
 )]

tests/ui/fail/seq_specs_vec_build.rs

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