From a7d35f51898f4b79f5327fa1250c032c8a358211 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 22 Jun 2026 17:02:45 +0000 Subject: [PATCH 1/5] Add Seq ghost type A spec-only `thrust_models::model::Seq` analogous to the existing `model::Vec`: the logical representation is `(Array, Int)` (the array carries elements, the int carries length). The `#[thrust::def::seq_model]` marker lets the analyzer recognise `Seq` ADTs in future patches. Co-Authored-By: Claude Opus 4.7 Claude-Session: https://claude.ai/code/session_01A7nMxM1sJ8wxVJmMvsEvSX --- std.rs | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/std.rs b/std.rs index 87e5bde2..11d2b9c3 100644 --- a/std.rs +++ b/std.rs @@ -195,6 +195,25 @@ mod thrust_models { unimplemented!() } } + + /// `Seq` is the ghost sequence type used in specifications. + /// Like `Vec`, it is represented logically as `(Array, Int)` + /// — the array carries elements, the int carries length. Concrete + /// operations (indexing, push, concat, …) are added incrementally + /// in follow-up commits. + #[thrust::def::seq_model] + pub struct Seq(pub Array, pub Int); + + impl PartialEq for Seq where U: super::Model { + #[thrust::ignored] + fn eq(&self, _other: &U) -> bool { + unimplemented!() + } + } + } + + impl Model for model::Seq where T: Model { + type Ty = model::Seq<::Ty>; } impl Model for model::Int { From 5c9606bcd13f3e173b90741668c3f5fec4ba3237 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 22 Jun 2026 17:09:57 +0000 Subject: [PATCH 2/5] Add basic Seq operations: empty, singleton, len, push, indexing Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01A7nMxM1sJ8wxVJmMvsEvSX --- src/analyze/annot.rs | 40 +++++++++++++++++++++ src/analyze/annot_fn.rs | 53 +++++++++++++++++++++++++++- src/analyze/did_cache.rs | 41 +++++++++++++++++++++ src/chc.rs | 32 +++++++++++++++++ src/chc/format_context.rs | 1 + src/chc/smtlib2.rs | 10 ++++++ src/chc/unbox.rs | 1 + src/rty.rs | 4 +++ std.rs | 45 ++++++++++++++++++++--- tests/ui/fail/seq_basic.rs | 20 +++++++++++ tests/ui/fail/seq_specs_vec_build.rs | 23 ++++++++++++ tests/ui/pass/seq_basic.rs | 19 ++++++++++ tests/ui/pass/seq_specs_vec_build.rs | 28 +++++++++++++++ 13 files changed, 311 insertions(+), 6 deletions(-) create mode 100644 tests/ui/fail/seq_basic.rs create mode 100644 tests/ui/fail/seq_specs_vec_build.rs create mode 100644 tests/ui/pass/seq_basic.rs create mode 100644 tests/ui/pass/seq_specs_vec_build.rs diff --git a/src/analyze/annot.rs b/src/analyze/annot.rs index 76e76e22..76d92ab1 100644 --- a/src/analyze/annot.rs +++ b/src/analyze/annot.rs @@ -137,6 +137,46 @@ pub fn array_model_store_path() -> [Symbol; 3] { ] } +pub fn seq_model_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("seq_model"), + ] +} + +pub fn seq_empty_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("seq_empty"), + ] +} + +pub fn seq_singleton_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("seq_singleton"), + ] +} + +pub fn seq_len_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("seq_len"), + ] +} + +pub fn seq_push_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("seq_push"), + ] +} + pub fn exists_path() -> [Symbol; 3] { [ Symbol::intern("thrust"), diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index 0249e4aa..e1eae205 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -430,6 +430,14 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { FormulaOrTerm::Formula(fn_ty.postcondition_formula(¶m_args, result)) } + fn node_arg_type_at(&self, hir_id: HirId, idx: usize) -> rty::Type { + let generic_args = self.typeck.node_args(hir_id); + let generic_args = + mir_ty::EarlyBinder::bind(generic_args).instantiate(self.tcx, self.generic_args); + let elem_ty = generic_args.type_at(idx); + self.type_builder.build(elem_ty) + } + fn variant_ctor_term( &self, ctor_did: rustc_span::def_id::DefId, @@ -623,9 +631,18 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { FormulaOrTerm::Term(term.tuple_proj(index)) } ExprKind::Index(array, index, _) => { + let array_ty = self.expr_ty(array); let array_term = self.to_term(array); let index_term = self.to_term(index); - FormulaOrTerm::Term(array_term.select(index_term)) + 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) + } else { + array_term + }; + FormulaOrTerm::Term(array_inner.select(index_term)) } ExprKind::MethodCall(method, receiver, args, _) => { if let Some(def_id) = self.typeck.type_dependent_def_id(hir.hir_id) { @@ -644,6 +661,21 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { let t = self.to_term(receiver); return FormulaOrTerm::Term(t); } + 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)); + } + 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 new_len = len.add(chc::Term::int(1)); + return FormulaOrTerm::Term(chc::Term::tuple(vec![new_arr, new_len])); + } } unimplemented!("unsupported method call in formula: {:?}", method) } @@ -719,6 +751,25 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { let t = self.to_term(&args[0]); return FormulaOrTerm::Term(chc::Term::box_(t)); } + if Some(def_id) == self.def_ids.seq_empty() { + assert!(args.is_empty(), "Seq::empty does not take any arguments"); + let elem_sort = self.node_arg_type_at(func_expr.hir_id, 0).to_sort(); + return FormulaOrTerm::Term(chc::Term::tuple(vec![ + chc::Term::array_empty(chc::Sort::int(), elem_sort), + chc::Term::int(0), + ])); + } + if Some(def_id) == self.def_ids.seq_singleton() { + assert_eq!(args.len(), 1, "Seq::singleton takes exactly 1 argument"); + let v = self.to_term(&args[0]); + let elem_sort = self.node_arg_type_at(func_expr.hir_id, 0).to_sort(); + let new_arr = chc::Term::array_empty(chc::Sort::int(), elem_sort) + .store(chc::Term::int(0), v); + return FormulaOrTerm::Term(chc::Term::tuple(vec![ + new_arr, + chc::Term::int(1), + ])); + } if let rustc_hir::def::DefKind::Ctor(ctor_of, _) = def_kind { let terms = args.iter().map(|e| self.to_term(e)).collect(); match ctor_of { diff --git a/src/analyze/did_cache.rs b/src/analyze/did_cache.rs index 15149120..49fbaf70 100644 --- a/src/analyze/did_cache.rs +++ b/src/analyze/did_cache.rs @@ -24,6 +24,12 @@ struct DefIds { box_model_new: OnceCell>, array_model_store: OnceCell>, + seq_model: OnceCell>, + seq_empty: OnceCell>, + seq_singleton: OnceCell>, + seq_len: OnceCell>, + seq_push: OnceCell>, + exists: OnceCell>, forall: OnceCell>, implies: OnceCell>, @@ -179,6 +185,41 @@ impl<'tcx> DefIdCache<'tcx> { .get_or_init(|| self.annotated_def(&crate::analyze::annot::array_model_store_path())) } + pub fn seq_model(&self) -> Option { + *self + .def_ids + .seq_model + .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_model_path())) + } + + pub fn seq_empty(&self) -> Option { + *self + .def_ids + .seq_empty + .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_empty_path())) + } + + pub fn seq_singleton(&self) -> Option { + *self + .def_ids + .seq_singleton + .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_singleton_path())) + } + + pub fn seq_len(&self) -> Option { + *self + .def_ids + .seq_len + .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_len_path())) + } + + pub fn seq_push(&self) -> Option { + *self + .def_ids + .seq_push + .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_push_path())) + } + pub fn exists(&self) -> Option { *self .def_ids diff --git a/src/chc.rs b/src/chc.rs index 2a61f375..f2db09c0 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -448,6 +448,7 @@ pub enum Term { MutCurrent(Box>), MutFinal(Box>), App(Function, Vec>), + ArrayEmpty(Sort, Sort), Tuple(Vec>), TupleProj(Box>, usize), DatatypeCtor(DatatypeSort, DatatypeSymbol, Vec>), @@ -499,6 +500,7 @@ where f.append(allocator.line()).append(inner.nest(2)).group() } } + Term::ArrayEmpty(_, _) => allocator.text("[]"), Term::Tuple(ts) => { let separator = allocator.text(",").append(allocator.line()); if ts.len() == 1 { @@ -562,6 +564,7 @@ impl Term { Term::App(fun, args) => { Term::App(fun, args.into_iter().map(|t| t.subst_var(&mut f)).collect()) } + Term::ArrayEmpty(s1, s2) => Term::ArrayEmpty(s1, s2), Term::Tuple(ts) => Term::Tuple(ts.into_iter().map(|t| t.subst_var(&mut f)).collect()), Term::TupleProj(t, i) => Term::TupleProj(Box::new(t.subst_var(f)), i), Term::DatatypeCtor(sort, c_sym, args) => Term::DatatypeCtor( @@ -608,6 +611,7 @@ impl Term { let mut var_sort: Box Sort> = Box::new(var_sort); fun.sort(args.iter().map(|t| t.sort(&mut var_sort))) } + Term::ArrayEmpty(index, elem) => Sort::array(index.clone(), elem.clone()), Term::Tuple(ts) => { // TODO: remove this let mut var_sort: Box Sort> = Box::new(var_sort); @@ -627,6 +631,7 @@ impl Term { | Term::Bool(_) | Term::Int(_) | Term::String(_) + | Term::ArrayEmpty { .. } | Term::FormulaQuantifiedVar { .. } => Box::new(std::iter::empty()), Term::Box(t) => t.fv_impl(), Term::Mut(t1, t2) => Box::new(t1.fv_impl().chain(t2.fv_impl())), @@ -665,6 +670,29 @@ impl Term { Term::String(s) } + /// Some canonical value of the given sort. The exact value is unspecified; + /// callers must only use it where any well-typed value would do (e.g. the + /// element value of an [`Term::ArrayEmpty`]). + pub fn default_for(sort: &Sort) -> Self { + match sort { + Sort::Null => Term::Null, + Sort::Int => Term::Int(0), + Sort::Bool => Term::Bool(false), + Sort::String => Term::String(String::new()), + Sort::Box(s) => Term::Box(Box::new(Self::default_for(s))), + Sort::Mut(s) => Term::Mut( + Box::new(Self::default_for(s)), + Box::new(Self::default_for(s)), + ), + Sort::Tuple(ts) => Term::Tuple(ts.iter().map(Self::default_for).collect()), + Sort::Array(i, e) => Term::ArrayEmpty((**i).clone(), (**e).clone()), + // TODO: defaults for Datatype and Param. + Sort::Datatype(_) | Sort::Param(_) => { + unimplemented!("no default value for sort {sort:?}") + } + } + } + pub fn box_(t: Term) -> Self { Term::Box(Box::new(t)) } @@ -673,6 +701,10 @@ impl Term { Term::Mut(Box::new(t1), Box::new(t2)) } + pub fn array_empty(index: Sort, elem: Sort) -> Self { + Term::ArrayEmpty(index, elem) + } + pub fn boxed(self) -> Self { Term::Box(Box::new(self)) } diff --git a/src/chc/format_context.rs b/src/chc/format_context.rs index f4a79fd4..6e282f27 100644 --- a/src/chc/format_context.rs +++ b/src/chc/format_context.rs @@ -45,6 +45,7 @@ fn term_sorts(clause: &chc::Clause, t: &chc::Term, sorts: &mut BTreeSet {} chc::Term::Tuple(ts) => { for t in ts { term_sorts(clause, t, sorts); diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index 7904d58d..b9e6acd6 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -159,6 +159,16 @@ impl<'ctx, 'a> std::fmt::Display for Term<'ctx, 'a> { List::open(args.iter().map(|t| Term::new(self.ctx, self.clause, t))) ) } + chc::Term::ArrayEmpty(index, elem) => { + let index_sort = self.ctx.fmt_sort(index); + let elem_sort = self.ctx.fmt_sort(elem); + let default = chc::Term::default_for(elem); + write!( + f, + "((as const (Array {index_sort} {elem_sort})) {})", + Term::new(self.ctx, self.clause, &default) + ) + } chc::Term::Tuple(ts) => { let ss: Vec<_> = ts.iter().map(|t| self.clause.term_sort(t)).collect(); if ss.is_empty() { diff --git a/src/chc/unbox.rs b/src/chc/unbox.rs index bfb782eb..62c455bd 100644 --- a/src/chc/unbox.rs +++ b/src/chc/unbox.rs @@ -11,6 +11,7 @@ fn unbox_term(term: Term) -> Term { Term::MutCurrent(t) => Term::MutCurrent(Box::new(unbox_term(*t))), Term::MutFinal(t) => Term::MutFinal(Box::new(unbox_term(*t))), Term::App(fun, args) => Term::App(fun, args.into_iter().map(unbox_term).collect()), + Term::ArrayEmpty(s1, s2) => Term::ArrayEmpty(unbox_sort(s1), unbox_sort(s2)), Term::Tuple(ts) => Term::Tuple(ts.into_iter().map(unbox_term).collect()), Term::TupleProj(t, i) => Term::TupleProj(Box::new(unbox_term(*t)), i), Term::DatatypeCtor(s1, s2, args) => Term::DatatypeCtor( diff --git a/src/rty.rs b/src/rty.rs index 28209bb4..591698d5 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -1974,6 +1974,10 @@ fn subst_ty_params_in_term(term: &mut chc::Term, subst: &TypeParamSubst subst_ty_params_in_term(arg, subst); } } + chc::Term::ArrayEmpty(s1, s2) => { + subst_ty_params_in_sort(s1, subst); + subst_ty_params_in_sort(s2, subst); + } chc::Term::DatatypeCtor(s, _, args) => { for arg in s.args_mut() { subst_ty_params_in_sort(arg, subst); diff --git a/std.rs b/std.rs index 11d2b9c3..3bf49cc8 100644 --- a/std.rs +++ b/std.rs @@ -196,11 +196,6 @@ mod thrust_models { } } - /// `Seq` is the ghost sequence type used in specifications. - /// Like `Vec`, it is represented logically as `(Array, Int)` - /// — the array carries elements, the int carries length. Concrete - /// operations (indexing, push, concat, …) are added incrementally - /// in follow-up commits. #[thrust::def::seq_model] pub struct Seq(pub Array, pub Int); @@ -210,6 +205,46 @@ mod thrust_models { unimplemented!() } } + + impl std::ops::Index for Seq where U: super::Model { + type Output = T; + + #[thrust::ignored] + fn index(&self, _index: U) -> &Self::Output { + unimplemented!() + } + } + + impl Seq { + #[allow(dead_code)] + #[thrust::def::seq_empty] + #[thrust::ignored] + pub fn empty() -> Self { + unimplemented!() + } + + #[allow(dead_code)] + #[thrust::def::seq_singleton] + #[thrust::ignored] + pub fn singleton(_x: T) -> Self { + unimplemented!() + } + + #[allow(dead_code)] + #[thrust::def::seq_len] + #[thrust::ignored] + pub fn len(&self) -> Int { + unimplemented!() + } + + #[allow(dead_code)] + #[thrust::def::seq_push] + #[thrust::ignored] + pub fn push(self, _x: T) -> Self { + unimplemented!() + } + + } } impl Model for model::Seq where T: Model { diff --git a/tests/ui/fail/seq_basic.rs b/tests/ui/fail/seq_basic.rs new file mode 100644 index 00000000..ff340d90 --- /dev/null +++ b/tests/ui/fail/seq_basic.rs @@ -0,0 +1,20 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + Seq::::empty().len() == 0 + && Seq::singleton(x).len() == 1 + && Seq::singleton(x)[0] == x + // wrong: should be s.len() + 1 + && s.push(x).len() == s.len() + 2 + && s.push(x)[s.len()] == x +)] +fn seq_basic(s: Seq, x: Int) -> () { + let _ = s; + let _ = x; +} + +fn main() {} diff --git a/tests/ui/fail/seq_specs_vec_build.rs b/tests/ui/fail/seq_specs_vec_build.rs new file mode 100644 index 00000000..1f083b2f --- /dev/null +++ b/tests/ui/fail/seq_specs_vec_build.rs @@ -0,0 +1,23 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +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] + // wrong: last element should be 30, not 99 + && result.0[2] == Seq::empty().push(10).push(20).push(99)[2] +)] +fn build_three() -> Vec { + let mut v = Vec::new(); + v.push(10); + v.push(20); + v.push(30); + v +} + +fn main() {} diff --git a/tests/ui/pass/seq_basic.rs b/tests/ui/pass/seq_basic.rs new file mode 100644 index 00000000..99ff2286 --- /dev/null +++ b/tests/ui/pass/seq_basic.rs @@ -0,0 +1,19 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + Seq::::empty().len() == 0 + && Seq::singleton(x).len() == 1 + && Seq::singleton(x)[0] == x + && s.push(x).len() == s.len() + 1 + && s.push(x)[s.len()] == x +)] +fn seq_basic(s: Seq, x: Int) -> () { + let _ = s; + let _ = x; +} + +fn main() {} diff --git a/tests/ui/pass/seq_specs_vec_build.rs b/tests/ui/pass/seq_specs_vec_build.rs new file mode 100644 index 00000000..a1936ca5 --- /dev/null +++ b/tests/ui/pass/seq_specs_vec_build.rs @@ -0,0 +1,28 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +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.0[2] == Seq::empty().push(10).push(20).push(30)[2] +)] +fn build_three() -> Vec { + let mut v = Vec::new(); + v.push(10); + v.push(20); + v.push(30); + v +} + +fn main() { + let v = build_three(); + assert!(v.len() == 3); + assert!(v[0] == 10); + assert!(v[1] == 20); + assert!(v[2] == 30); +} From 57449504a8852bfe72274f1556a9d8672242200d Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 22 Jun 2026 17:15:35 +0000 Subject: [PATCH 3/5] Add Seq::concat via define-fun-rec Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01A7nMxM1sJ8wxVJmMvsEvSX --- src/analyze/annot.rs | 8 +++ src/analyze/annot_fn.rs | 30 +++++++++++ src/analyze/did_cache.rs | 8 +++ src/chc.rs | 83 +++++++++++++++++++++++++++++++ src/chc/format_context.rs | 28 ++++++++++- src/chc/smtlib2.rs | 24 +++++++++ src/chc/unbox.rs | 22 ++++++++ src/rty.rs | 6 +++ std.rs | 6 +++ tests/ui/fail/seq_concat.rs | 13 +++++ tests/ui/fail/seq_concat_const.rs | 16 ++++++ tests/ui/pass/seq_concat.rs | 13 +++++ tests/ui/pass/seq_concat_const.rs | 16 ++++++ 13 files changed, 272 insertions(+), 1 deletion(-) create mode 100644 tests/ui/fail/seq_concat.rs create mode 100644 tests/ui/fail/seq_concat_const.rs create mode 100644 tests/ui/pass/seq_concat.rs create mode 100644 tests/ui/pass/seq_concat_const.rs diff --git a/src/analyze/annot.rs b/src/analyze/annot.rs index 76d92ab1..b246df43 100644 --- a/src/analyze/annot.rs +++ b/src/analyze/annot.rs @@ -177,6 +177,14 @@ pub fn seq_push_path() -> [Symbol; 3] { ] } +pub fn seq_concat_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("seq_concat"), + ] +} + pub fn exists_path() -> [Symbol; 3] { [ Symbol::intern("thrust"), diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index e1eae205..029db1d1 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -438,6 +438,17 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { self.type_builder.build(elem_ty) } + fn adt_arg_type_at( + &self, + expr: &'tcx rustc_hir::Expr<'tcx>, + idx: usize, + ) -> rty::Type { + let mir_ty::TyKind::Adt(_, args) = self.expr_ty(expr).kind() else { + panic!("expected ADT"); + }; + self.type_builder.build(args.type_at(idx)) + } + fn variant_ctor_term( &self, ctor_did: rustc_span::def_id::DefId, @@ -676,6 +687,25 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { let new_len = len.add(chc::Term::int(1)); return FormulaOrTerm::Term(chc::Term::tuple(vec![new_arr, 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_arr = t.clone().tuple_proj(0); + let a_len = t.tuple_proj(1); + let b_arr = other.clone().tuple_proj(0); + let b_len = other.tuple_proj(1); + let new_arr = chc::Term::array_concat( + elem_sort, + a_arr, + a_len.clone(), + b_arr, + b_len.clone(), + ); + let new_len = a_len.add(b_len); + return FormulaOrTerm::Term(chc::Term::tuple(vec![new_arr, new_len])); + } } unimplemented!("unsupported method call in formula: {:?}", method) } diff --git a/src/analyze/did_cache.rs b/src/analyze/did_cache.rs index 49fbaf70..4dbcf110 100644 --- a/src/analyze/did_cache.rs +++ b/src/analyze/did_cache.rs @@ -29,6 +29,7 @@ struct DefIds { seq_singleton: OnceCell>, seq_len: OnceCell>, seq_push: OnceCell>, + seq_concat: OnceCell>, exists: OnceCell>, forall: OnceCell>, @@ -220,6 +221,13 @@ impl<'tcx> DefIdCache<'tcx> { .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_push_path())) } + pub fn seq_concat(&self) -> Option { + *self + .def_ids + .seq_concat + .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_concat_path())) + } + pub fn exists(&self) -> Option { *self .def_ids diff --git a/src/chc.rs b/src/chc.rs index f2db09c0..ea8c3db2 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -434,6 +434,66 @@ impl Function { pub const SELECT: Function = Function::new("select"); } +#[derive(Debug, Clone)] +pub struct ArrayConcatTerm { + pub array1: Term, + pub len1: Term, + pub array2: Term, + pub len2: Term, +} + +impl<'a, D, V> Pretty<'a, D, termcolor::ColorSpec> for &ArrayConcatTerm +where + V: Var, + D: pretty::DocAllocator<'a, termcolor::ColorSpec>, + D::Doc: Clone, +{ + fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> { + allocator + .text("concat") + .append(allocator.line()) + .append(self.array1.pretty_atom(allocator)) + .append(allocator.text(",")) + .append(allocator.line()) + .append(self.len1.pretty_atom(allocator)) + .append(allocator.text(",")) + .append(allocator.line()) + .append(self.array2.pretty_atom(allocator)) + .append(allocator.text(",")) + .append(allocator.line()) + .append(self.len2.pretty_atom(allocator)) + .parens() + } +} + +impl ArrayConcatTerm { + pub fn iter_args(&self) -> impl Iterator> { + std::iter::once(&self.array1) + .chain(std::iter::once(&self.len1)) + .chain(std::iter::once(&self.array2)) + .chain(std::iter::once(&self.len2)) + } + + pub fn iter_args_mut(&mut self) -> impl Iterator> { + std::iter::once(&mut self.array1) + .chain(std::iter::once(&mut self.len1)) + .chain(std::iter::once(&mut self.array2)) + .chain(std::iter::once(&mut self.len2)) + } + + pub fn subst_var(self, mut f: F) -> ArrayConcatTerm + where + F: FnMut(V) -> Term, + { + ArrayConcatTerm { + array1: self.array1.subst_var(&mut f), + len1: self.len1.subst_var(&mut f), + array2: self.array2.subst_var(&mut f), + len2: self.len2.subst_var(f), + } + } +} + /// A logical term. #[derive(Debug, Clone)] pub enum Term { @@ -449,6 +509,7 @@ pub enum Term { MutFinal(Box>), App(Function, Vec>), ArrayEmpty(Sort, Sort), + ArrayConcat(Sort, Box>), Tuple(Vec>), TupleProj(Box>, usize), DatatypeCtor(DatatypeSort, DatatypeSymbol, Vec>), @@ -501,6 +562,7 @@ where } } Term::ArrayEmpty(_, _) => allocator.text("[]"), + Term::ArrayConcat(_, t) => t.pretty(allocator), Term::Tuple(ts) => { let separator = allocator.text(",").append(allocator.line()); if ts.len() == 1 { @@ -565,6 +627,7 @@ impl Term { Term::App(fun, args.into_iter().map(|t| t.subst_var(&mut f)).collect()) } Term::ArrayEmpty(s1, s2) => Term::ArrayEmpty(s1, s2), + Term::ArrayConcat(s, t) => Term::ArrayConcat(s, Box::new(t.subst_var(f))), Term::Tuple(ts) => Term::Tuple(ts.into_iter().map(|t| t.subst_var(&mut f)).collect()), Term::TupleProj(t, i) => Term::TupleProj(Box::new(t.subst_var(f)), i), Term::DatatypeCtor(sort, c_sym, args) => Term::DatatypeCtor( @@ -612,6 +675,7 @@ impl Term { fun.sort(args.iter().map(|t| t.sort(&mut var_sort))) } Term::ArrayEmpty(index, elem) => Sort::array(index.clone(), elem.clone()), + Term::ArrayConcat(elem, _) => Sort::array(Sort::int(), elem.clone()), Term::Tuple(ts) => { // TODO: remove this let mut var_sort: Box Sort> = Box::new(var_sort); @@ -639,6 +703,7 @@ impl Term { Term::MutCurrent(t) => t.fv_impl(), Term::MutFinal(t) => t.fv_impl(), Term::App(_, args) => Box::new(args.iter().flat_map(|t| t.fv_impl())), + Term::ArrayConcat(_, t) => Box::new(t.iter_args().flat_map(|t| t.fv_impl())), Term::Tuple(ts) => Box::new(ts.iter().flat_map(|t| t.fv_impl())), Term::TupleProj(t, _) => t.fv_impl(), Term::DatatypeCtor(_, _, args) => Box::new(args.iter().flat_map(|t| t.fv_impl())), @@ -705,6 +770,24 @@ impl Term { Term::ArrayEmpty(index, elem) } + pub fn array_concat( + elem_sort: Sort, + array1: Term, + len1: Term, + array2: Term, + len2: Term, + ) -> Self { + Term::ArrayConcat( + elem_sort, + Box::new(ArrayConcatTerm { + array1, + len1, + array2, + len2, + }), + ) + } + pub fn boxed(self) -> Self { Term::Box(Box::new(self)) } diff --git a/src/chc/format_context.rs b/src/chc/format_context.rs index 6e282f27..7b0a76ff 100644 --- a/src/chc/format_context.rs +++ b/src/chc/format_context.rs @@ -21,6 +21,7 @@ use crate::chc::{self, hoice::HoiceDatatypeRenamer}; pub struct FormatContext { renamer: HoiceDatatypeRenamer, datatypes: Vec, + int_array_elem_sorts: BTreeSet, } // FIXME: this is obviously ineffective and should be replaced @@ -46,6 +47,11 @@ fn term_sorts(clause: &chc::Clause, t: &chc::Term, sorts: &mut BTreeSet {} + chc::Term::ArrayConcat(_, t) => { + for arg in t.iter_args() { + term_sorts(clause, arg, sorts); + } + } chc::Term::Tuple(ts) => { for t in ts { term_sorts(clause, t, sorts); @@ -270,6 +276,13 @@ impl FormatContext { datatypes.push(mono_datatype); } } + let int_array_elem_sorts: BTreeSet<_> = sorts + .iter() + .filter_map(|s| match s { + chc::Sort::Array(index, elem) if **index == chc::Sort::int() => Some(*elem.clone()), + _ => None, + }) + .collect(); let datatypes: Vec<_> = sorts .into_iter() .flat_map(builtin_sort_datatype) @@ -277,13 +290,21 @@ impl FormatContext { .filter(|d| d.params == 0) .collect(); let renamer = HoiceDatatypeRenamer::new(&datatypes); - FormatContext { renamer, datatypes } + FormatContext { + renamer, + datatypes, + int_array_elem_sorts, + } } pub fn datatypes(&self) -> &[chc::Datatype] { &self.datatypes } + pub fn int_array_elem_sorts(&self) -> &BTreeSet { + &self.int_array_elem_sorts + } + pub fn box_ctor(&self, sort: &chc::Sort) -> impl std::fmt::Display { let ss = SortSymbol::new(sort).sorts(); format!("box{ss}") @@ -348,6 +369,11 @@ impl FormatContext { format!("matcher_pred<{}>", self.fmt_datatype_symbol(sym)) } + pub fn concat_int_array(&self, elem: &chc::Sort) -> impl std::fmt::Display { + let elem = SortSymbol::new(elem); + format!("concat_int_array<{}>", elem) + } + fn fmt_sort_impl(&self, sort: &chc::Sort) -> Box { match sort { chc::Sort::Array(s1, s2) => { diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index b9e6acd6..89e1710d 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -169,6 +169,15 @@ impl<'ctx, 'a> std::fmt::Display for Term<'ctx, 'a> { Term::new(self.ctx, self.clause, &default) ) } + chc::Term::ArrayConcat(elem, t) => { + let name = self.ctx.concat_int_array(elem); + write!( + f, + "({} {})", + name, + List::open(t.iter_args().map(|t| Term::new(self.ctx, self.clause, t))) + ) + } chc::Term::Tuple(ts) => { let ss: Vec<_> = ts.iter().map(|t| self.clause.term_sort(t)).collect(); if ss.is_empty() { @@ -629,6 +638,21 @@ impl<'a> std::fmt::Display for System<'a> { writeln!(f, "{}", MatcherPredFun::new(&self.ctx, datatype))?; } + 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); + writeln!( + f, + "(define-fun-rec {name} \ + ((sa (Array Int {elem_ty})) (sn Int) (ta (Array Int {elem_ty})) (tn Int)) \ + (Array Int {elem_ty}) \ + (ite (<= tn 0) sa \ + (store ({name} sa sn ta (- tn 1)) \ + (+ sn (- tn 1)) \ + (select ta (- tn 1)))))\n", + )?; + } + // insert command from #![thrust::raw_command()] here for raw_command in &self.inner.raw_commands { writeln!(f, "{}\n", RawCommand::new(raw_command))?; diff --git a/src/chc/unbox.rs b/src/chc/unbox.rs index 62c455bd..b13ab96c 100644 --- a/src/chc/unbox.rs +++ b/src/chc/unbox.rs @@ -2,6 +2,25 @@ use super::*; +fn unbox_array_concat_term(t: ArrayConcatTerm) -> ArrayConcatTerm { + let ArrayConcatTerm { + array1, + len1, + array2, + len2, + } = t; + let array1 = unbox_term(array1); + let len1 = unbox_term(len1); + let array2 = unbox_term(array2); + let len2 = unbox_term(len2); + ArrayConcatTerm { + array1, + len1, + array2, + len2, + } +} + fn unbox_term(term: Term) -> Term { match term { Term::Var(_) | Term::Bool(_) | Term::Int(_) | Term::String(_) | Term::Null => term, @@ -12,6 +31,9 @@ fn unbox_term(term: Term) -> Term { Term::MutFinal(t) => Term::MutFinal(Box::new(unbox_term(*t))), Term::App(fun, args) => Term::App(fun, args.into_iter().map(unbox_term).collect()), Term::ArrayEmpty(s1, s2) => Term::ArrayEmpty(unbox_sort(s1), unbox_sort(s2)), + Term::ArrayConcat(s, t) => { + Term::ArrayConcat(unbox_sort(s), Box::new(unbox_array_concat_term(*t))) + } Term::Tuple(ts) => Term::Tuple(ts.into_iter().map(unbox_term).collect()), Term::TupleProj(t, i) => Term::TupleProj(Box::new(unbox_term(*t)), i), Term::DatatypeCtor(s1, s2, args) => Term::DatatypeCtor( diff --git a/src/rty.rs b/src/rty.rs index 591698d5..35e07769 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -1978,6 +1978,12 @@ fn subst_ty_params_in_term(term: &mut chc::Term, subst: &TypeParamSubst subst_ty_params_in_sort(s1, subst); subst_ty_params_in_sort(s2, subst); } + chc::Term::ArrayConcat(sort, t) => { + subst_ty_params_in_sort(sort, subst); + for arg in t.iter_args_mut() { + subst_ty_params_in_term(arg, subst); + } + } chc::Term::DatatypeCtor(s, _, args) => { for arg in s.args_mut() { subst_ty_params_in_sort(arg, subst); diff --git a/std.rs b/std.rs index 3bf49cc8..692e84bc 100644 --- a/std.rs +++ b/std.rs @@ -244,6 +244,12 @@ mod thrust_models { unimplemented!() } + #[allow(dead_code)] + #[thrust::def::seq_concat] + #[thrust::ignored] + pub fn concat(self, _other: Self) -> Self { + unimplemented!() + } } } diff --git a/tests/ui/fail/seq_concat.rs b/tests/ui/fail/seq_concat.rs new file mode 100644 index 00000000..bba0a6cd --- /dev/null +++ b/tests/ui/fail/seq_concat.rs @@ -0,0 +1,13 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(s.concat(t).len() == s.len() + t.len() + 1)] +fn concat_lengths_add(s: Seq, t: Seq) -> () { + let _ = s; + let _ = t; +} + +fn main() {} diff --git a/tests/ui/fail/seq_concat_const.rs b/tests/ui/fail/seq_concat_const.rs new file mode 100644 index 00000000..8285c026 --- /dev/null +++ b/tests/ui/fail/seq_concat_const.rs @@ -0,0 +1,16 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + // wrong: empty.concat(singleton(x)) is singleton(x), not empty + Seq::::empty().concat(Seq::singleton(x)) == Seq::::empty() +)] +fn concat_eq_singleton(x: Int) -> () { + let _ = x; +} + +fn main() {} diff --git a/tests/ui/pass/seq_concat.rs b/tests/ui/pass/seq_concat.rs new file mode 100644 index 00000000..1821bbe9 --- /dev/null +++ b/tests/ui/pass/seq_concat.rs @@ -0,0 +1,13 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(s.concat(t).len() == s.len() + t.len())] +fn concat_lengths_add(s: Seq, t: Seq) -> () { + let _ = s; + let _ = t; +} + +fn main() {} diff --git a/tests/ui/pass/seq_concat_const.rs b/tests/ui/pass/seq_concat_const.rs new file mode 100644 index 00000000..ca2120be --- /dev/null +++ b/tests/ui/pass/seq_concat_const.rs @@ -0,0 +1,16 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + Seq::singleton(x).concat(Seq::empty()) == Seq::singleton(x) + && Seq::empty().concat(Seq::singleton(x)) == Seq::singleton(x) +)] +fn concat_eq_singleton(x: Int) -> () { + let _ = x; +} + +fn main() {} From 6e76c4f64fb88d4f72b3e36ace94c5c8028db119 Mon Sep 17 00:00:00 2001 From: coord_e Date: Tue, 23 Jun 2026 23:10:50 +0900 Subject: [PATCH 4/5] Add some peephole optimization of tuple/array operations Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01A7nMxM1sJ8wxVJmMvsEvSX --- src/annot.rs | 8 ++--- src/chc.rs | 58 ++++++++++++++++++++++++++++++- tests/ui/fail/seq_concat_index.rs | 15 ++++++++ tests/ui/pass/seq_concat_index.rs | 15 ++++++++ 4 files changed, 91 insertions(+), 5 deletions(-) create mode 100644 tests/ui/fail/seq_concat_index.rs create mode 100644 tests/ui/pass/seq_concat_index.rs diff --git a/src/annot.rs b/src/annot.rs index e51836e9..8457f60b 100644 --- a/src/annot.rs +++ b/src/annot.rs @@ -91,7 +91,7 @@ pub struct AnnotPathSegment { /// A trait for resolving variables in annotations to their logical representation and their sorts. pub trait Resolver { - type Output; + type Output: Clone; fn resolve(&self, ident: Ident) -> Option<(Self::Output, chc::Sort)>; } @@ -1222,7 +1222,7 @@ struct RefinementResolver<'a, T> { self_: Option<(Ident, chc::Sort)>, } -impl<'a, T> Resolver for RefinementResolver<'a, T> { +impl<'a, T: Clone> Resolver for RefinementResolver<'a, T> { type Output = rty::RefinedTypeVar; fn resolve(&self, ident: Ident) -> Option<(Self::Output, chc::Sort)> { if let Some((self_ident, sort)) = &self.self_ { @@ -1256,7 +1256,7 @@ pub struct MappedResolver<'a, T, F> { map: F, } -impl<'a, T, F, U> Resolver for MappedResolver<'a, T, F> +impl<'a, T: Clone, F, U: Clone> Resolver for MappedResolver<'a, T, F> where F: Fn(T) -> U, { @@ -1290,7 +1290,7 @@ impl<'a, T> Default for StackedResolver<'a, T> { } } -impl<'a, T> Resolver for StackedResolver<'a, T> { +impl<'a, T: Clone> Resolver for StackedResolver<'a, T> { type Output = T; fn resolve(&self, ident: Ident) -> Option<(Self::Output, chc::Sort)> { for resolver in &self.resolvers { diff --git a/src/chc.rs b/src/chc.rs index ea8c3db2..1dba68d5 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -414,6 +414,7 @@ impl Function { }; *elem } + Self::ITE => args.into_iter().nth(1).unwrap(), _ => unimplemented!(), } } @@ -432,6 +433,7 @@ impl Function { pub const NEG: Function = Function::new("-"); pub const STORE: Function = Function::new("store"); pub const SELECT: Function = Function::new("select"); + pub const ITE: Function = Function::new("ite"); } #[derive(Debug, Clone)] @@ -859,10 +861,59 @@ impl Term { Term::App(Function::NEG, vec![self]) } - pub fn select(self, index: Self) -> Self { + pub fn select(self, index: Self) -> Self + where + V: Clone, + { + // Peephole 1: when both indices are concrete integer literals, reduce `select(store(a, i, + // v), j)` to `v` (`i == j`) or `select(a, j)` (`i != j`). Same motivation as the + // `tuple_proj` simplifier: keep datatype/array constructors from leaking into Spacer + // clauses where it can't reduce them. Non-literal indices are deferred to the solver via + // the general select-of-store axiom. + if let (Term::App(Function::STORE, _), Term::Int(j)) = (&self, &index) { + let Term::App(_, mut args) = self else { + unreachable!() + }; + assert_eq!(args.len(), 3, "STORE takes 3 args"); + let stored_value = args.pop().unwrap(); + let stored_index = args.pop().unwrap(); + let base = args.pop().unwrap(); + if let Term::Int(i) = &stored_index { + return if i == j { + stored_value + } else { + base.select(index) + }; + } + return Term::App( + Function::SELECT, + vec![ + Term::App(Function::STORE, vec![base, stored_index, stored_value]), + index, + ], + ); + } + // Peephole 2: inline one step of the `concat_int_array` recursive definitions to reduce + // indexed access to terms over the underlying sequences. The SMT-defined functions are + // still emitted (so the rewrites use exactly their unfolded form), but pcsat can prove + // 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(sa, sn, ta, tn), i) + // ↦ ite(i < sn, select(sa, i), select(ta, i - sn))` + if let Term::ArrayConcat(_, t) = self { + let cond = index.clone().lt(t.len1.clone()); + let then_ = t.array1.select(index.clone()); + let else_ = t.array2.select(index.sub(t.len1)); + return Term::ite(cond, then_, else_); + } Term::App(Function::SELECT, vec![self, index]) } + pub fn ite(cond: Self, then_: Self, else_: Self) -> Self { + Term::App(Function::ITE, vec![cond, then_, else_]) + } + pub fn store(self, index: Self, elem: Self) -> Self { Term::App(Function::STORE, vec![self, index, elem]) } @@ -872,6 +923,11 @@ impl Term { } pub fn tuple_proj(self, i: usize) -> Self { + // Spacer doesn't unfold tuple projections of literal constructors. + if let Term::Tuple(mut ts) = self { + assert!(i < ts.len(), "tuple_proj index out of bounds"); + return ts.swap_remove(i); + } Term::TupleProj(Box::new(self), i) } diff --git a/tests/ui/fail/seq_concat_index.rs b/tests/ui/fail/seq_concat_index.rs new file mode 100644 index 00000000..15587a70 --- /dev/null +++ b/tests/ui/fail/seq_concat_index.rs @@ -0,0 +1,15 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(0 <= i && i < s.len())] +#[thrust_macros::ensures(s.concat(t)[i] == t[i])] +fn concat_index_left(s: Seq, t: Seq, i: Int) -> () { + let _ = s; + let _ = t; + let _ = i; +} + +fn main() {} diff --git a/tests/ui/pass/seq_concat_index.rs b/tests/ui/pass/seq_concat_index.rs new file mode 100644 index 00000000..f28e5d92 --- /dev/null +++ b/tests/ui/pass/seq_concat_index.rs @@ -0,0 +1,15 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(0 <= i && i < s.len())] +#[thrust_macros::ensures(s.concat(t)[i] == s[i])] +fn concat_index_left(s: Seq, t: Seq, i: Int) -> () { + let _ = s; + let _ = t; + let _ = i; +} + +fn main() {} From f678f8cfdcf7edd644fbaab09d5ce84d30cebfd3 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 23 Jun 2026 12:27:47 +0000 Subject: [PATCH 5/5] Use Seq as the model of Vec Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01A7nMxM1sJ8wxVJmMvsEvSX --- std.rs | 25 ++++++------------------- 1 file changed, 6 insertions(+), 19 deletions(-) diff --git a/std.rs b/std.rs index 692e84bc..9d1a883f 100644 --- a/std.rs +++ b/std.rs @@ -187,15 +187,6 @@ mod thrust_models { unimplemented!() } - pub struct Vec(pub Array, pub Int); - - impl PartialEq for Vec where U: super::Model { - #[thrust::ignored] - fn eq(&self, _other: &U) -> bool { - unimplemented!() - } - } - #[thrust::def::seq_model] pub struct Seq(pub Array, pub Int); @@ -253,8 +244,8 @@ mod thrust_models { } } - impl Model for model::Seq where T: Model { - type Ty = model::Seq<::Ty>; + impl Model for model::Seq { + type Ty = model::Seq; } impl Model for model::Int { @@ -370,11 +361,7 @@ mod thrust_models { } impl Model for Vec where T: Model { - type Ty = model::Vec<::Ty>; - } - - impl Model for model::Vec { - type Ty = model::Vec; + type Ty = model::Seq<::Ty>; } impl Model for Option where T: Model { @@ -727,7 +714,7 @@ fn _extern_spec_vec_new() -> Vec where T: thrust_models::Model, T::Ty: Par #[thrust::extern_spec_fn] #[thrust_macros::requires(true)] -#[thrust_macros::ensures(!vec == thrust_models::model::Vec((*vec).0.store((*vec).1, elem), (*vec).1 + 1))] +#[thrust_macros::ensures(!vec == thrust_models::model::Seq((*vec).0.store((*vec).1, elem), (*vec).1 + 1))] fn _extern_spec_vec_push(vec: &mut Vec, elem: T) where T: thrust_models::Model, T::Ty: PartialEq { @@ -753,7 +740,7 @@ fn _extern_spec_vec_index(vec: &Vec, index: usize) -> &T where T: thrust_m #[thrust_macros::ensures( *result == (*vec).0[index] && !result == (!vec).0[index] && - !vec == thrust_models::model::Vec((*vec).0.store(index, !result), (*vec).1) + !vec == thrust_models::model::Seq((*vec).0.store(index, !result), (*vec).1) )] fn _extern_spec_vec_index_mut(vec: &mut Vec, index: usize) -> &mut T where T: thrust_models::Model, T::Ty: PartialEq @@ -799,7 +786,7 @@ fn _extern_spec_vec_is_empty(vec: &Vec) -> bool where T: thrust_models::Mo #[thrust_macros::ensures( ( (*vec).1 > len && - !vec == thrust_models::model::Vec((*vec).0, len) + !vec == thrust_models::model::Seq((*vec).0, len) ) || ( (*vec).1 <= len && !vec == *vec