From 7449228bd66ca6987b99c28a8a83d54e8125ff53 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 22 Jun 2026 17:02:45 +0000 Subject: [PATCH 1/4] 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. This commit introduces only the type and its `Model` impl; the operations (`empty`, `singleton`, `len`, `push`, `concat`, `subsequence`, indexing) are added in follow-up commits. 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 30e5e9cf0d3d54fbf04c69d12f20c299f909e4ff Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 22 Jun 2026 17:09:57 +0000 Subject: [PATCH 2/4] Add basic Seq operations: empty, singleton, len, push, indexing MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds the non-recursive operations of `Seq`. Each lowers mechanically to existing CHC primitives — no SMT-side function definition or peephole is involved here: | API | Lowering | |--------------------|-----------------------------------------------------| | `Seq::::empty()`| `(seq_default_arr_int, 0)` | | `Seq::singleton(e)`| `(store(seq_default_arr_int, 0, e), 1)` | | `s.len()` | `tuple_proj(s, 1)` | | `s.push(e)` | `(store(fst(s), snd(s), e), snd(s) + 1)` | | `s[i]` | `select(fst(s), i)` | `seq_default_arr_int` is a designated constant array `((as const (Array Int Int)) 0)` always emitted in the SMT preamble; its concrete contents are irrelevant because callers never access indices past the length they keep track of. The `s[i]` lowering reuses the existing `ExprKind::Index` analyzer path, gated on `def_ids.seq_model()` to detect `Seq`-typed receivers (otherwise the path expects an `Array`). Paired pass/fail tests for each operation, plus two end-to-end program tests that drive verification of a Vec-manipulating loop through Seq specs. Co-Authored-By: Claude Opus 4.7 Claude-Session: https://claude.ai/code/session_01A7nMxM1sJ8wxVJmMvsEvSX --- src/analyze/annot.rs | 40 ++++++++++++++++++++ src/analyze/annot_fn.rs | 44 +++++++++++++++++++++- src/analyze/did_cache.rs | 41 ++++++++++++++++++++ src/chc.rs | 46 +++++++++++++++++++++++ src/chc/smtlib2.rs | 27 ++++++++++--- std.rs | 45 +++++++++++++++++++--- tests/ui/fail/seq_empty.rs | 10 +++++ tests/ui/fail/seq_index.rs | 13 +++++++ tests/ui/fail/seq_len_push.rs | 13 +++++++ tests/ui/fail/seq_singleton.rs | 12 ++++++ tests/ui/fail/seq_specs_loop_invariant.rs | 26 +++++++++++++ tests/ui/fail/seq_specs_vec_build.rs | 23 ++++++++++++ tests/ui/pass/seq_empty.rs | 10 +++++ tests/ui/pass/seq_index.rs | 13 +++++++ tests/ui/pass/seq_len_push.rs | 13 +++++++ tests/ui/pass/seq_singleton.rs | 12 ++++++ tests/ui/pass/seq_specs_loop_invariant.rs | 31 +++++++++++++++ tests/ui/pass/seq_specs_vec_build.rs | 33 ++++++++++++++++ 18 files changed, 440 insertions(+), 12 deletions(-) create mode 100644 tests/ui/fail/seq_empty.rs create mode 100644 tests/ui/fail/seq_index.rs create mode 100644 tests/ui/fail/seq_len_push.rs create mode 100644 tests/ui/fail/seq_singleton.rs create mode 100644 tests/ui/fail/seq_specs_loop_invariant.rs create mode 100644 tests/ui/fail/seq_specs_vec_build.rs create mode 100644 tests/ui/pass/seq_empty.rs create mode 100644 tests/ui/pass/seq_index.rs create mode 100644 tests/ui/pass/seq_len_push.rs create mode 100644 tests/ui/pass/seq_singleton.rs create mode 100644 tests/ui/pass/seq_specs_loop_invariant.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..8474b957 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -623,9 +623,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 +653,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 +743,24 @@ 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 arr = chc::Term::App(chc::Function::SEQ_DEFAULT_ARR_INT, vec![]); + return FormulaOrTerm::Term(chc::Term::tuple(vec![ + arr, + 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 arr = chc::Term::App(chc::Function::SEQ_DEFAULT_ARR_INT, vec![]); + let new_arr = arr.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..81fa525a 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -414,6 +414,7 @@ impl Function { }; *elem } + Self::SEQ_DEFAULT_ARR_INT => Sort::array(Sort::int(), Sort::int()), _ => unimplemented!(), } } @@ -432,6 +433,14 @@ impl Function { pub const NEG: Function = Function::new("-"); pub const STORE: Function = Function::new("store"); pub const SELECT: Function = Function::new("select"); + + /// Designated empty/default array of element sort `Int`. Used by + /// `Seq::empty()` and `Seq::singleton(_)` to fill the array slot of + /// an otherwise length-determined sequence. Defined as + /// `((as const (Array Int Int)) 0)` in the SMT preamble; the + /// concrete contents are irrelevant because the length (0 or 1) is + /// the only thing reasoned about. + pub const SEQ_DEFAULT_ARR_INT: Function = Function::new("seq_default_arr_int"); } /// A logical term. @@ -745,6 +754,36 @@ impl Term { } pub fn select(self, index: Self) -> Self { + // 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) + }; + } + // Re-build the original term if we couldn't simplify. + return Term::App( + Function::SELECT, + vec![ + Term::App(Function::STORE, vec![base, stored_index, stored_value]), + index, + ], + ); + } Term::App(Function::SELECT, vec![self, index]) } @@ -757,6 +796,13 @@ impl Term { } pub fn tuple_proj(self, i: usize) -> Self { + // Peephole: `tuple_proj(tuple(t0,...,tn), i)` ↦ `ti`. Without this, + // HORN solvers like Spacer struggle to reduce datatype constructors + // appearing inside clauses, which makes downstream reasoning brittle. + 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/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index 7904d58d..753ed56a 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -152,12 +152,16 @@ impl<'ctx, 'a> std::fmt::Display for Term<'ctx, 'a> { ) } chc::Term::App(fn_, args) => { - write!( - f, - "({} {})", - fn_, - List::open(args.iter().map(|t| Term::new(self.ctx, self.clause, t))) - ) + if args.is_empty() { + write!(f, "{}", fn_) + } else { + write!( + f, + "({} {})", + fn_, + List::open(args.iter().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(); @@ -624,6 +628,17 @@ impl<'a> std::fmt::Display for System<'a> { writeln!(f, "{}\n", RawCommand::new(raw_command))?; } + // Designated default array used as the array slot of `Seq::empty()` / + // `Seq::singleton(_)`. Always emitted even when unused — harmless, + // and lets the analyzer emit references unconditionally. Defined + // (not declared) so pcsat does not treat it as a synthesis target; + // the concrete value is irrelevant because indices ≥ length are + // never accessed. + writeln!( + f, + "(define-fun seq_default_arr_int () (Array Int Int) \ + ((as const (Array Int Int)) 0))\n" + )?; for user_defined_pred_def in &self.inner.user_defined_pred_defs { writeln!( f, 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_empty.rs b/tests/ui/fail/seq_empty.rs new file mode 100644 index 00000000..dde487cd --- /dev/null +++ b/tests/ui/fail/seq_empty.rs @@ -0,0 +1,10 @@ +//@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() == 1)] +fn empty_has_zero_len() -> () {} + +fn main() {} diff --git a/tests/ui/fail/seq_index.rs b/tests/ui/fail/seq_index.rs new file mode 100644 index 00000000..cc147cae --- /dev/null +++ b/tests/ui/fail/seq_index.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.push(x)[s.len()] == x + 1)] +fn push_index(s: Seq, x: Int) -> () { + let _ = s; + let _ = x; +} + +fn main() {} diff --git a/tests/ui/fail/seq_len_push.rs b/tests/ui/fail/seq_len_push.rs new file mode 100644 index 00000000..d485752c --- /dev/null +++ b/tests/ui/fail/seq_len_push.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.push(x).len() == s.len() + 2)] +fn push_increments(s: Seq, x: Int) -> () { + let _ = s; + let _ = x; +} + +fn main() {} diff --git a/tests/ui/fail/seq_singleton.rs b/tests/ui/fail/seq_singleton.rs new file mode 100644 index 00000000..5bbe41e5 --- /dev/null +++ b/tests/ui/fail/seq_singleton.rs @@ -0,0 +1,12 @@ +//@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::singleton(x).len() == 2)] +fn singleton_holds_one(x: Int) -> () { + let _ = x; +} + +fn main() {} diff --git a/tests/ui/fail/seq_specs_loop_invariant.rs b/tests/ui/fail/seq_specs_loop_invariant.rs new file mode 100644 index 00000000..eb7b3412 --- /dev/null +++ b/tests/ui/fail/seq_specs_loop_invariant.rs @@ -0,0 +1,26 @@ +//@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)] +// wrong: should be `.push(0).push(1).push(2).len()` (== 3), not 4 pushes +#[thrust_macros::ensures( + result.1 == Seq::::empty().push(0).push(1).push(2).push(3).len() +)] +#[thrust_macros::invariant_context] +fn push_three() -> Vec { + let mut w: Vec = Vec::new(); + let mut i: i64 = 0; + while i < 3 { + thrust_macros::invariant!( + |i: i64, w: Vec| 0 <= i && i <= 3 && w.1 == i + ); + w.push(i); + i += 1; + } + w +} + +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..9849df49 --- /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_empty.rs b/tests/ui/pass/seq_empty.rs new file mode 100644 index 00000000..a412f12b --- /dev/null +++ b/tests/ui/pass/seq_empty.rs @@ -0,0 +1,10 @@ +//@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)] +fn empty_has_zero_len() -> () {} + +fn main() {} diff --git a/tests/ui/pass/seq_index.rs b/tests/ui/pass/seq_index.rs new file mode 100644 index 00000000..6a5b6f81 --- /dev/null +++ b/tests/ui/pass/seq_index.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.push(x)[s.len()] == x)] +fn push_index(s: Seq, x: Int) -> () { + let _ = s; + let _ = x; +} + +fn main() {} diff --git a/tests/ui/pass/seq_len_push.rs b/tests/ui/pass/seq_len_push.rs new file mode 100644 index 00000000..bb62ae92 --- /dev/null +++ b/tests/ui/pass/seq_len_push.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.push(x).len() == s.len() + 1)] +fn push_increments(s: Seq, x: Int) -> () { + let _ = s; + let _ = x; +} + +fn main() {} diff --git a/tests/ui/pass/seq_singleton.rs b/tests/ui/pass/seq_singleton.rs new file mode 100644 index 00000000..697398c2 --- /dev/null +++ b/tests/ui/pass/seq_singleton.rs @@ -0,0 +1,12 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(Seq::singleton(x).len() == 1 && Seq::singleton(x)[0] == x)] +fn singleton_holds_one(x: Int) -> () { + let _ = x; +} + +fn main() {} diff --git a/tests/ui/pass/seq_specs_loop_invariant.rs b/tests/ui/pass/seq_specs_loop_invariant.rs new file mode 100644 index 00000000..f5abba9a --- /dev/null +++ b/tests/ui/pass/seq_specs_loop_invariant.rs @@ -0,0 +1,31 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +// A loop builds a Vec by repeatedly pushing values; the loop invariant +// links the Vec's runtime length with a Seq value built by the same +// pushes in spec position. The Seq-side reasoning (`Seq::empty().len() +// == 0`, `s.push(x).len() == s.len() + 1`) drives the loop bound check. + +use thrust_models::model::Seq; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result.1 == Seq::::empty().push(0).push(1).push(2).len())] +#[thrust_macros::invariant_context] +fn push_three() -> Vec { + let mut w: Vec = Vec::new(); + let mut i: i64 = 0; + while i < 3 { + thrust_macros::invariant!( + |i: i64, w: Vec| 0 <= i && i <= 3 && w.1 == i + ); + w.push(i); + i += 1; + } + w +} + +fn main() { + let v = push_three(); + assert!(v.len() == 3); +} 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..bf290c15 --- /dev/null +++ b/tests/ui/pass/seq_specs_vec_build.rs @@ -0,0 +1,33 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +// A runtime function (builds a Vec) specified via Seq operations. +// The spec uses `Seq::empty().push(x).push(y)` to describe the contents, +// and the analyzer must reduce both sides syntactically (length and +// indexed access) to discharge each conjunct. + +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 42f3b46c5c4884068a35e25b4dde293a7f04638d Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 22 Jun 2026 17:15:35 +0000 Subject: [PATCH 3/4] Add Seq::concat / Seq::subsequence via define-fun-rec MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `s.concat(t)` and `s.subsequence(l, r)` lower in `annot_fn.rs` to two new CHC function symbols whose bodies are emitted as recursive SMT-LIB2 `define-fun-rec`s: (define-fun-rec seq_concat_arr_int ((sa (Array Int Int)) (sn Int) (ta (Array Int Int)) (tn Int)) (Array Int Int) (ite (<= tn 0) sa (store (seq_concat_arr_int sa sn ta (- tn 1)) (+ sn (- tn 1)) (select ta (- tn 1))))) (define-fun-rec seq_subseq_arr_int ((a (Array Int Int)) (l Int) (r Int)) (Array Int Int) (ite (<= r l) seq_default_arr_int (store (seq_subseq_arr_int a l (- r 1)) (- (- r 1) l) (select a (- r 1))))) The Thrust analyzer wraps each result in the usual `(array, length)` tuple, with the length computed inline as `s.len + t.len` / `r - l` so length-only properties (`len(concat(s, t)) == len(s) + len(t)`) verify on z3 + pcsat directly — the SMT obligation simply never references the recursive function. The emissions are gated by `System::uses_seq_concat` / `uses_seq_subseq`, set when the analyzer lowers the operation. pcsat treats unused `declare-fun` returning arrays as synthesis targets and fails to parse if the declaration is in scope even when unused, so gating is necessary. pcsat unfolds the definitions for any concrete recursion bound (e.g. `select(seq_concat_arr_int(_, _, _, 3), i)` reduces to a finite ite chain). Universally quantified bounds (the unbounded indexed case, `s.concat(t)[i] == s[i]`) are out of reach without further optimisation — solved in the follow-up peephole commit. z3-Spacer in HORN logic treats every `define-fun-rec` as uninterpreted and returns `unknown` (by user direction, we don't aim to support indexed reasoning on Z3). Paired pass/fail length tests for both operations. Co-Authored-By: Claude Opus 4.7 Claude-Session: https://claude.ai/code/session_01A7nMxM1sJ8wxVJmMvsEvSX --- src/analyze.rs | 8 ++++++ src/analyze/annot.rs | 16 ++++++++++++ src/analyze/annot_fn.rs | 35 ++++++++++++++++++++++++++ src/analyze/did_cache.rs | 16 ++++++++++++ src/chc.rs | 43 +++++++++++++++++++++++++++++++- src/chc/smtlib2.rs | 36 ++++++++++++++++++++++++++ src/chc/unbox.rs | 4 +++ std.rs | 17 +++++++++++++ tests/ui/fail/seq_concat.rs | 13 ++++++++++ tests/ui/fail/seq_subsequence.rs | 14 +++++++++++ tests/ui/pass/seq_concat.rs | 13 ++++++++++ tests/ui/pass/seq_subsequence.rs | 14 +++++++++++ 12 files changed, 228 insertions(+), 1 deletion(-) create mode 100644 tests/ui/fail/seq_concat.rs create mode 100644 tests/ui/fail/seq_subsequence.rs create mode 100644 tests/ui/pass/seq_concat.rs create mode 100644 tests/ui/pass/seq_subsequence.rs diff --git a/src/analyze.rs b/src/analyze.rs index a4ffa5f4..6ba7faea 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -271,6 +271,14 @@ impl<'tcx> Analyzer<'tcx> { self.def_ids.clone() } + pub fn mark_uses_seq_concat(&self) { + self.system.borrow_mut().uses_seq_concat = true; + } + + pub fn mark_uses_seq_subseq(&self) { + self.system.borrow_mut().uses_seq_subseq = true; + } + pub fn add_clause(&mut self, clause: chc::Clause) { self.system.borrow_mut().push_clause(clause); } diff --git a/src/analyze/annot.rs b/src/analyze/annot.rs index 76d92ab1..ae74ca94 100644 --- a/src/analyze/annot.rs +++ b/src/analyze/annot.rs @@ -177,6 +177,22 @@ 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 seq_subsequence_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("seq_subsequence"), + ] +} + pub fn exists_path() -> [Symbol; 3] { [ Symbol::intern("thrust"), diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index 8474b957..7edd1c55 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -668,6 +668,41 @@ 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"); + self.analyzer.mark_uses_seq_concat(); + 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); + // The array half is the recursive SMT-defined + // function `seq_concat_arr_int(sa, sn, ta, tn)`; + // the length half is computed inline so length + // properties remain provable on any solver (the + // SMT obligation never has to mention the array). + let new_arr = chc::Term::App( + chc::Function::SEQ_CONCAT_ARR_INT, + vec![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])); + } + if Some(def_id) == self.def_ids.seq_subsequence() { + assert_eq!(args.len(), 2, "Seq::subsequence takes exactly 2 arguments"); + self.analyzer.mark_uses_seq_subseq(); + let t = self.to_term(receiver); + let l = self.to_term(&args[0]); + let r = self.to_term(&args[1]); + let arr = t.tuple_proj(0); + let new_arr = chc::Term::App( + chc::Function::SEQ_SUBSEQ_ARR_INT, + vec![arr, l.clone(), r.clone()], + ); + let new_len = r.sub(l); + 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..650d3756 100644 --- a/src/analyze/did_cache.rs +++ b/src/analyze/did_cache.rs @@ -29,6 +29,8 @@ struct DefIds { seq_singleton: OnceCell>, seq_len: OnceCell>, seq_push: OnceCell>, + seq_concat: OnceCell>, + seq_subsequence: OnceCell>, exists: OnceCell>, forall: OnceCell>, @@ -220,6 +222,20 @@ 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 seq_subsequence(&self) -> Option { + *self + .def_ids + .seq_subsequence + .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_subsequence_path())) + } + pub fn exists(&self) -> Option { *self .def_ids diff --git a/src/chc.rs b/src/chc.rs index 81fa525a..63fa34b9 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -414,7 +414,9 @@ impl Function { }; *elem } - Self::SEQ_DEFAULT_ARR_INT => Sort::array(Sort::int(), Sort::int()), + Self::SEQ_DEFAULT_ARR_INT | Self::SEQ_CONCAT_ARR_INT | Self::SEQ_SUBSEQ_ARR_INT => { + Sort::array(Sort::int(), Sort::int()) + } _ => unimplemented!(), } } @@ -441,6 +443,38 @@ impl Function { /// concrete contents are irrelevant because the length (0 or 1) is /// the only thing reasoned about. pub const SEQ_DEFAULT_ARR_INT: Function = Function::new("seq_default_arr_int"); + /// The array of `Seq::concat(_, _)` for element sort `Int`. Defined + /// in the SMT preamble via `define-fun-rec` as the structural + /// recursion over the second sequence's length: + /// ```smt2 + /// (define-fun-rec seq_concat_arr_int + /// ((sa (Array Int Int)) (sn Int) (ta (Array Int Int)) (tn Int)) + /// (Array Int Int) + /// (ite (<= tn 0) sa + /// (store (seq_concat_arr_int sa sn ta (- tn 1)) + /// (+ sn (- tn 1)) + /// (select ta (- tn 1))))) + /// ``` + /// pcsat unfolds this for any concrete `tn`. Universally quantified + /// `tn` is currently out of reach (no inductive invariant found in a + /// reasonable budget); the follow-up peephole commit sidesteps this + /// for indexed access. z3-Spacer in HORN logic treats every + /// `define-fun-rec` as uninterpreted and returns `unknown` — by user + /// direction, we don't aim to support indexed reasoning on Z3. + pub const SEQ_CONCAT_ARR_INT: Function = Function::new("seq_concat_arr_int"); + /// The array of `Seq::subsequence(_, l, r)` for element sort `Int`. + /// Defined via `define-fun-rec` as the structural recursion over + /// `r - l`: + /// ```smt2 + /// (define-fun-rec seq_subseq_arr_int + /// ((a (Array Int Int)) (l Int) (r Int)) + /// (Array Int Int) + /// (ite (<= r l) seq_default_arr_int + /// (store (seq_subseq_arr_int a l (- r 1)) + /// (- (- r 1) l) + /// (select a (- r 1))))) + /// ``` + pub const SEQ_SUBSEQ_ARR_INT: Function = Function::new("seq_subseq_arr_int"); } /// A logical term. @@ -1897,6 +1931,13 @@ pub struct System { pub user_defined_pred_defs: Vec, pub clauses: IndexVec, pub pred_vars: IndexVec, + /// Set by the analyzer when `Seq::concat` is lowered, gating the + /// `seq_concat_arr_int` declaration in the SMT preamble. pcsat would + /// otherwise treat the unused function as a synthesis target and + /// fail to parse. + pub uses_seq_concat: bool, + /// Same as [`Self::uses_seq_concat`] but for `Seq::subsequence`. + pub uses_seq_subseq: bool, } impl System { diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index 753ed56a..81245ba9 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -639,6 +639,42 @@ impl<'a> std::fmt::Display for System<'a> { "(define-fun seq_default_arr_int () (Array Int Int) \ ((as const (Array Int Int)) 0))\n" )?; + // Recursive definitions of `seq_concat_arr_int(sa, sn, ta, tn)` and + // `seq_subseq_arr_int(a, l, r)`: the array half of the + // `Seq::concat` / `Seq::subsequence` result. Emitted via + // `define-fun-rec` so pcsat can unfold them for any concrete + // recursion bound (`tn` for concat, `r - l` for subsequence). + // Universally quantified bounds are out of reach without further + // optimisation; see the follow-up peephole commit and + // `chc::Function::SEQ_CONCAT_ARR_INT`. + // + // The length half of both operations is computed inline by the + // analyzer (`a.len + b.len` for concat, `r - l` for subsequence), + // so the length-only reasoning that worked under z3 before still + // works — the SMT obligation simply never references the array + // half. + if self.inner.uses_seq_concat { + writeln!( + f, + "(define-fun-rec seq_concat_arr_int \ + ((sa (Array Int Int)) (sn Int) (ta (Array Int Int)) (tn Int)) (Array Int Int) \ + (ite (<= tn 0) sa \ + (store (seq_concat_arr_int sa sn ta (- tn 1)) \ + (+ sn (- tn 1)) \ + (select ta (- tn 1)))))\n" + )?; + } + if self.inner.uses_seq_subseq { + writeln!( + f, + "(define-fun-rec seq_subseq_arr_int \ + ((a (Array Int Int)) (l Int) (r Int)) (Array Int Int) \ + (ite (<= r l) seq_default_arr_int \ + (store (seq_subseq_arr_int a l (- r 1)) \ + (- (- r 1) l) \ + (select a (- r 1)))))\n" + )?; + } for user_defined_pred_def in &self.inner.user_defined_pred_defs { writeln!( f, diff --git a/src/chc/unbox.rs b/src/chc/unbox.rs index bfb782eb..eaf8ba88 100644 --- a/src/chc/unbox.rs +++ b/src/chc/unbox.rs @@ -181,6 +181,8 @@ pub fn unbox(system: System) -> System { user_defined_pred_defs, clauses, pred_vars, + uses_seq_concat, + uses_seq_subseq, } = system; let datatypes = datatypes.into_iter().map(unbox_datatype).collect(); let clauses = clauses.into_iter().map(unbox_clause).collect(); @@ -195,5 +197,7 @@ pub fn unbox(system: System) -> System { user_defined_pred_defs, clauses, pred_vars, + uses_seq_concat, + uses_seq_subseq, } } diff --git a/std.rs b/std.rs index 3bf49cc8..62a88015 100644 --- a/std.rs +++ b/std.rs @@ -244,6 +244,23 @@ mod thrust_models { unimplemented!() } + #[allow(dead_code)] + #[thrust::def::seq_concat] + #[thrust::ignored] + pub fn concat(self, _other: Self) -> Self { + unimplemented!() + } + + #[allow(dead_code)] + #[thrust::def::seq_subsequence] + #[thrust::ignored] + pub fn subsequence(&self, _l: L, _r: R) -> Self + where + L: super::Model, + R: super::Model, + { + 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_subsequence.rs b/tests/ui/fail/seq_subsequence.rs new file mode 100644 index 00000000..dccae619 --- /dev/null +++ b/tests/ui/fail/seq_subsequence.rs @@ -0,0 +1,14 @@ +//@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.subsequence(l, r).len() == r - l + 1)] +fn subsequence_length(s: Seq, l: Int, r: Int) -> () { + let _ = s; + let _ = l; + let _ = r; +} + +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_subsequence.rs b/tests/ui/pass/seq_subsequence.rs new file mode 100644 index 00000000..aef50700 --- /dev/null +++ b/tests/ui/pass/seq_subsequence.rs @@ -0,0 +1,14 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(s.subsequence(l, r).len() == r - l)] +fn subsequence_length(s: Seq, l: Int, r: Int) -> () { + let _ = s; + let _ = l; + let _ = r; +} + +fn main() {} From b470807923bb554f0dda309fcf76436e35951740 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 22 Jun 2026 17:53:02 +0000 Subject: [PATCH 4/4] Peephole-rewrite Seq::concat / Seq::subsequence index access MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `select(seq_concat_arr_int(sa, sn, ta, tn), i)` and `select(seq_subseq_arr_int(a, l, r), i)` are simplified at `chc::Term::select` construction time to equivalent `(ite ...)` expressions over the underlying sequences: select(seq_concat_arr_int(sa, sn, ta, tn), i) ↦ ite(i < sn, select(sa, i), select(ta, i - sn)) select(seq_subseq_arr_int(a, l, r), i) ↦ ite(0 <= i < r - l, select(a, l + i), select(seq_default_arr_int, 0)) The `define-fun-rec` definitions from the previous commit remain the ground truth — the rewrites are exactly one unfolding step of those definitions — but pcsat can prove unbounded indexed properties against the inlined ITE form, where unfolding through `define-fun-rec` over a universally quantified recursion bound requires an inductive invariant pcsat doesn't find in a reasonable budget. Bounded (constant) cases still work via direct unfolding of the recursive definitions. `chc::Function::ITE` and `chc::Term::ite` are introduced for this rewrite, and `Term::select` gains a `V: Clone` bound (the rewrites need to duplicate `index` and `sn`). That bound cascades into `Resolver::Output: Clone` plus matching bounds on the three `Resolver` impls (`RefinementResolver`, `MappedResolver`, `StackedResolver`) — all concrete usages already satisfy `Clone`, so this is a non-breaking strengthening. Paired pass/fail indexed tests for both operations, plus an end-to-end `seq_specs_concat_run` test exercising the same rewrites through a real runtime function. 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/fail/seq_concat_index_right.rs | 15 +++++++ tests/ui/fail/seq_specs_concat_run.rs | 21 +++++++++ tests/ui/fail/seq_subseq_index.rs | 16 +++++++ tests/ui/pass/seq_concat_index.rs | 15 +++++++ tests/ui/pass/seq_concat_index_right.rs | 15 +++++++ tests/ui/pass/seq_specs_concat_run.rs | 29 +++++++++++++ tests/ui/pass/seq_subseq_index.rs | 16 +++++++ 10 files changed, 203 insertions(+), 5 deletions(-) create mode 100644 tests/ui/fail/seq_concat_index.rs create mode 100644 tests/ui/fail/seq_concat_index_right.rs create mode 100644 tests/ui/fail/seq_specs_concat_run.rs create mode 100644 tests/ui/fail/seq_subseq_index.rs create mode 100644 tests/ui/pass/seq_concat_index.rs create mode 100644 tests/ui/pass/seq_concat_index_right.rs create mode 100644 tests/ui/pass/seq_specs_concat_run.rs create mode 100644 tests/ui/pass/seq_subseq_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 63fa34b9..13c31fae 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -414,6 +414,10 @@ impl Function { }; *elem } + Self::ITE => { + // (ite cond then_ else_) : sort_of(then_) + args.into_iter().nth(1).expect("ITE takes 3 args") + } Self::SEQ_DEFAULT_ARR_INT | Self::SEQ_CONCAT_ARR_INT | Self::SEQ_SUBSEQ_ARR_INT => { Sort::array(Sort::int(), Sort::int()) } @@ -435,6 +439,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"); /// Designated empty/default array of element sort `Int`. Used by /// `Seq::empty()` and `Seq::singleton(_)` to fill the array slot of @@ -787,7 +792,10 @@ 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 @@ -818,9 +826,57 @@ impl Term { ], ); } + // Peephole 2: inline one step of the `seq_concat_arr_int` / + // `seq_subseq_arr_int` 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(seq_concat_arr_int(sa, sn, ta, tn), i) + // ↦ ite(i < sn, select(sa, i), select(ta, i - sn))` + if let Term::App(Function::SEQ_CONCAT_ARR_INT, _) = &self { + let Term::App(_, mut args) = self else { + unreachable!() + }; + assert_eq!(args.len(), 4, "SEQ_CONCAT_ARR_INT takes 4 args"); + let _tn = args.pop().unwrap(); + let ta = args.pop().unwrap(); + let sn = args.pop().unwrap(); + let sa = args.pop().unwrap(); + let cond = index.clone().lt(sn.clone()); + let then_ = sa.select(index.clone()); + let else_ = ta.select(index.sub(sn)); + return Term::ite(cond, then_, else_); + } + // `select(seq_subseq_arr_int(a, l, r), i) + // ↦ ite(0 <= i < r - l, select(a, l + i), select(seq_default_arr_int, 0))` + // The `r - l` bound matches the recursive definition's base + // case. Out-of-range indices fall through to the designated + // default array, mirroring the base case `r <= l → default`. + if let Term::App(Function::SEQ_SUBSEQ_ARR_INT, _) = &self { + let Term::App(_, mut args) = self else { + unreachable!() + }; + assert_eq!(args.len(), 3, "SEQ_SUBSEQ_ARR_INT takes 3 args"); + let r = args.pop().unwrap(); + let l = args.pop().unwrap(); + let a = args.pop().unwrap(); + let len = r.sub(l.clone()); + let in_range = index.clone().ge(Term::int(0)).and(index.clone().lt(len)); + let then_ = a.select(l.add(index)); + let else_ = Term::App(Function::SEQ_DEFAULT_ARR_INT, vec![]).select(Term::int(0)); + return Term::ite(in_range, 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]) } 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/fail/seq_concat_index_right.rs b/tests/ui/fail/seq_concat_index_right.rs new file mode 100644 index 00000000..03f7cb78 --- /dev/null +++ b/tests/ui/fail/seq_concat_index_right.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(s.len() <= i && i < s.len() + t.len())] +#[thrust_macros::ensures(s.concat(t)[i] == s[i - s.len()])] +fn concat_index_right(s: Seq, t: Seq, i: Int) -> () { + let _ = s; + let _ = t; + let _ = i; +} + +fn main() {} diff --git a/tests/ui/fail/seq_specs_concat_run.rs b/tests/ui/fail/seq_specs_concat_run.rs new file mode 100644 index 00000000..772bc92f --- /dev/null +++ b/tests/ui/fail/seq_specs_concat_run.rs @@ -0,0 +1,21 @@ +//@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: swap order + result.1 == Seq::::singleton(x).concat(Seq::::singleton(y)).len() + && result.0[0] == Seq::::singleton(y).concat(Seq::::singleton(x))[0] + && result.0[1] == Seq::::singleton(y).concat(Seq::::singleton(x))[1] +)] +fn pair(x: i64, y: i64) -> Vec { + let mut v = Vec::new(); + v.push(x); + v.push(y); + v +} + +fn main() {} diff --git a/tests/ui/fail/seq_subseq_index.rs b/tests/ui/fail/seq_subseq_index.rs new file mode 100644 index 00000000..c41d589c --- /dev/null +++ b/tests/ui/fail/seq_subseq_index.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(0 <= l && l <= r && r <= s.len() && 0 <= i && i < r - l)] +#[thrust_macros::ensures(s.subsequence(l, r)[i] == s[i])] +fn subseq_index(s: Seq, l: Int, r: Int, i: Int) -> () { + let _ = s; + let _ = l; + let _ = r; + 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() {} diff --git a/tests/ui/pass/seq_concat_index_right.rs b/tests/ui/pass/seq_concat_index_right.rs new file mode 100644 index 00000000..f7db4eb2 --- /dev/null +++ b/tests/ui/pass/seq_concat_index_right.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(s.len() <= i && i < s.len() + t.len())] +#[thrust_macros::ensures(s.concat(t)[i] == t[i - s.len()])] +fn concat_index_right(s: Seq, t: Seq, i: Int) -> () { + let _ = s; + let _ = t; + let _ = i; +} + +fn main() {} diff --git a/tests/ui/pass/seq_specs_concat_run.rs b/tests/ui/pass/seq_specs_concat_run.rs new file mode 100644 index 00000000..b6719059 --- /dev/null +++ b/tests/ui/pass/seq_specs_concat_run.rs @@ -0,0 +1,29 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper + +// A real runtime function returns the concatenation of two singletons. +// The post relates the result Vec to `Seq::singleton(x).concat(Seq::singleton(y))`, +// and the analyzer must reduce `concat[0]` / `concat[1]` syntactically. + +use thrust_models::model::{Int, Seq}; + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + result.1 == Seq::::singleton(x).concat(Seq::::singleton(y)).len() + && result.0[0] == Seq::::singleton(x).concat(Seq::::singleton(y))[0] + && result.0[1] == Seq::::singleton(x).concat(Seq::::singleton(y))[1] +)] +fn pair(x: i64, y: i64) -> Vec { + let mut v = Vec::new(); + v.push(x); + v.push(y); + v +} + +fn main() { + let v = pair(7, 8); + assert!(v.len() == 2); + assert!(v[0] == 7); + assert!(v[1] == 8); +} diff --git a/tests/ui/pass/seq_subseq_index.rs b/tests/ui/pass/seq_subseq_index.rs new file mode 100644 index 00000000..3531cd17 --- /dev/null +++ b/tests/ui/pass/seq_subseq_index.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(0 <= l && l <= r && r <= s.len() && 0 <= i && i < r - l)] +#[thrust_macros::ensures(s.subsequence(l, r)[i] == s[l + i])] +fn subseq_index(s: Seq, l: Int, r: Int, i: Int) -> () { + let _ = s; + let _ = l; + let _ = r; + let _ = i; +} + +fn main() {}