From 173d69661c2de0c9a4e0008f8f06d269d2de36ae Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 1 Jul 2026 20:32:22 +0000 Subject: [PATCH 1/3] Add a subsequence operation to the Seq model `Seq::subsequence(start, end)` produces a view over the same underlying array with the offset advanced by `start` and the length set to `end - start`. It is used to describe the tail/init views returned by the slice split operations. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01GzapTuen2mKHkkN3B7d8qi --- src/analyze/annot.rs | 8 ++++++++ src/analyze/annot_fn.rs | 15 +++++++++++++++ src/analyze/did_cache.rs | 8 ++++++++ std.rs | 11 +++++++++++ 4 files changed, 42 insertions(+) diff --git a/src/analyze/annot.rs b/src/analyze/annot.rs index b246df43..7a0342dd 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_subsequence_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("seq_subsequence"), + ] +} + pub fn seq_concat_path() -> [Symbol; 3] { [ Symbol::intern("thrust"), diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index 9cb6bc91..4d816453 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -715,6 +715,21 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { new_arr, offset, new_len, ])); } + if Some(def_id) == self.def_ids.seq_subsequence() { + assert_eq!(args.len(), 2, "Seq::subsequence takes exactly 2 arguments"); + let t = self.to_term(receiver); + let start = self.to_term(&args[0]); + let end = self.to_term(&args[1]); + let arr = t.clone().tuple_proj(0); + let offset = t.tuple_proj(1); + // A subsequence shares the underlying array, advances the offset by + // `start`, and sets the length to `end - start`. + return FormulaOrTerm::Term(chc::Term::tuple(vec![ + arr, + offset.add(start.clone()), + end.sub(start), + ])); + } 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(); diff --git a/src/analyze/did_cache.rs b/src/analyze/did_cache.rs index 4dbcf110..78b35fb5 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_subsequence: OnceCell>, seq_concat: OnceCell>, exists: OnceCell>, @@ -221,6 +222,13 @@ impl<'tcx> DefIdCache<'tcx> { .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_push_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 seq_concat(&self) -> Option { *self .def_ids diff --git a/std.rs b/std.rs index 62d29442..4048b75a 100644 --- a/std.rs +++ b/std.rs @@ -239,6 +239,17 @@ mod thrust_models { unimplemented!() } + #[allow(dead_code)] + #[thrust::def::seq_subsequence] + #[thrust::ignored] + pub fn subsequence(self, _start: U, _end: V) -> Self + where + U: super::Model, + V: super::Model, + { + unimplemented!() + } + #[allow(dead_code)] #[thrust::def::seq_concat] #[thrust::ignored] From 0414d6bac850e8b03731ff79f34ca63f38e297cf Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 1 Jul 2026 20:35:00 +0000 Subject: [PATCH 2/3] Add split_first and split_last slice specs Both return the boundary element together with a subsequence view of the rest: `split_first` pairs `&slice[0]` with `slice[1..]`, and `split_last` pairs `&slice[len - 1]` with `slice[..len - 1]`. Paired pass/fail tests cover the returned element and the length and contents of the remaining view. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01GzapTuen2mKHkkN3B7d8qi --- std.rs | 34 ++++++++++++++++++++++++++++++ tests/ui/fail/slice_split_first.rs | 19 +++++++++++++++++ tests/ui/fail/slice_split_last.rs | 19 +++++++++++++++++ tests/ui/pass/slice_split_first.rs | 20 ++++++++++++++++++ tests/ui/pass/slice_split_last.rs | 20 ++++++++++++++++++ 5 files changed, 112 insertions(+) create mode 100644 tests/ui/fail/slice_split_first.rs create mode 100644 tests/ui/fail/slice_split_last.rs create mode 100644 tests/ui/pass/slice_split_first.rs create mode 100644 tests/ui/pass/slice_split_last.rs diff --git a/std.rs b/std.rs index 4048b75a..f2f24669 100644 --- a/std.rs +++ b/std.rs @@ -972,6 +972,40 @@ fn _extern_spec_slice_last_mut(slice: &mut [T]) -> Option<&mut T> <[T]>::last_mut(slice) } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + ((*slice).length > 0 + && result == Some(( + &(*slice).array[(*slice).offset], + &(*slice).subsequence(1, (*slice).length), + )) + ) + || ((*slice).length == 0 && result == None) +)] +fn _extern_spec_slice_split_first(slice: &[T]) -> Option<(&T, &[T])> + where T: thrust_models::Model, T::Ty: PartialEq +{ + <[T]>::split_first(slice) +} + +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + ((*slice).length > 0 + && result == Some(( + &(*slice).array[(*slice).offset + (*slice).length - 1], + &(*slice).subsequence(0, (*slice).length - 1), + )) + ) + || ((*slice).length == 0 && result == None) +)] +fn _extern_spec_slice_split_last(slice: &[T]) -> Option<(&T, &[T])> + where T: thrust_models::Model, T::Ty: PartialEq +{ + <[T]>::split_last(slice) +} + // TODO: The following specs for Index/IndexMut methods are too specific; we should write specs for // a generic index (I: SliceIndex) that isn't specific to usize, maybe once #83 is implemented. diff --git a/tests/ui/fail/slice_split_first.rs b/tests/ui/fail/slice_split_first.rs new file mode 100644 index 00000000..6857e4e9 --- /dev/null +++ b/tests/ui/fail/slice_split_first.rs @@ -0,0 +1,19 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off +#[thrust::trusted] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + (*result).length == 2 + && (*result).array[(*result).offset] == 10 + && (*result).array[(*result).offset + 1] == 20 +)] +fn slice() -> &'static [i32] { + unimplemented!() +} + +fn main() { + let slice = slice(); + let (first, _tail) = slice.split_first().unwrap(); + // wrong: the first element is 10, not 11 + assert!(*first == 11); +} diff --git a/tests/ui/fail/slice_split_last.rs b/tests/ui/fail/slice_split_last.rs new file mode 100644 index 00000000..776d903f --- /dev/null +++ b/tests/ui/fail/slice_split_last.rs @@ -0,0 +1,19 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off +#[thrust::trusted] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + (*result).length == 2 + && (*result).array[(*result).offset] == 10 + && (*result).array[(*result).offset + 1] == 20 +)] +fn slice() -> &'static [i32] { + unimplemented!() +} + +fn main() { + let slice = slice(); + let (last, _init) = slice.split_last().unwrap(); + // wrong: the last element is 20, not 21 + assert!(*last == 21); +} diff --git a/tests/ui/pass/slice_split_first.rs b/tests/ui/pass/slice_split_first.rs new file mode 100644 index 00000000..0ecd79d1 --- /dev/null +++ b/tests/ui/pass/slice_split_first.rs @@ -0,0 +1,20 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +#[thrust::trusted] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + (*result).length == 2 + && (*result).array[(*result).offset] == 10 + && (*result).array[(*result).offset + 1] == 20 +)] +fn slice() -> &'static [i32] { + unimplemented!() +} + +fn main() { + let slice = slice(); + let (first, tail) = slice.split_first().unwrap(); + assert!(*first == 10); + assert!(tail.len() == 1); + assert!(*tail.first().unwrap() == 20); +} diff --git a/tests/ui/pass/slice_split_last.rs b/tests/ui/pass/slice_split_last.rs new file mode 100644 index 00000000..5a180dde --- /dev/null +++ b/tests/ui/pass/slice_split_last.rs @@ -0,0 +1,20 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +#[thrust::trusted] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + (*result).length == 2 + && (*result).array[(*result).offset] == 10 + && (*result).array[(*result).offset + 1] == 20 +)] +fn slice() -> &'static [i32] { + unimplemented!() +} + +fn main() { + let slice = slice(); + let (last, init) = slice.split_last().unwrap(); + assert!(*last == 20); + assert!(init.len() == 1); + assert!(*init.first().unwrap() == 10); +} From c643ac6c626bb2a48cc4212acde6dcc33aa2c5c2 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 1 Jul 2026 20:38:18 +0000 Subject: [PATCH 3/3] Add split_first_mut and split_last_mut slice specs Both hand back a mutable reference to the boundary element together with a mutable subsequence view of the rest, mirroring the immutable split specs. Read-only pass/fail tests cover the returned element and the remaining view. A mutation through the first reference is not yet propagated back to the original slice when the reference is returned inside a tuple, which is unsound; `slice_split_first_mut_mutation_unsound` reproduces this and is expected to keep failing until the fix lands on main. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01GzapTuen2mKHkkN3B7d8qi --- std.rs | 47 +++++++++++++++++++ tests/ui/fail/slice_split_first_mut.rs | 19 ++++++++ .../slice_split_first_mut_mutation_unsound.rs | 28 +++++++++++ tests/ui/fail/slice_split_last_mut.rs | 19 ++++++++ tests/ui/pass/slice_split_first_mut.rs | 20 ++++++++ tests/ui/pass/slice_split_last_mut.rs | 20 ++++++++ 6 files changed, 153 insertions(+) create mode 100644 tests/ui/fail/slice_split_first_mut.rs create mode 100644 tests/ui/fail/slice_split_first_mut_mutation_unsound.rs create mode 100644 tests/ui/fail/slice_split_last_mut.rs create mode 100644 tests/ui/pass/slice_split_first_mut.rs create mode 100644 tests/ui/pass/slice_split_last_mut.rs diff --git a/std.rs b/std.rs index f2f24669..3428336d 100644 --- a/std.rs +++ b/std.rs @@ -1006,6 +1006,53 @@ fn _extern_spec_slice_split_last(slice: &[T]) -> Option<(&T, &[T])> <[T]>::split_last(slice) } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + ((*slice).length > 0 + && (!slice).offset == (*slice).offset + && (!slice).length == (*slice).length + && result == Some(( + thrust_models::model::Mut::new((*slice)[0], (!slice)[0]), + thrust_models::model::Mut::new( + (*slice).subsequence(1, (*slice).length), + (!slice).subsequence(1, (!slice).length), + ), + )) + ) + || ((*slice).length == 0 && result == None && !slice == *slice) +)] +fn _extern_spec_slice_split_first_mut(slice: &mut [T]) -> Option<(&mut T, &mut [T])> + where T: thrust_models::Model, T::Ty: PartialEq +{ + <[T]>::split_first_mut(slice) +} + +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + ((*slice).length > 0 + && (!slice).offset == (*slice).offset + && (!slice).length == (*slice).length + && result == Some(( + thrust_models::model::Mut::new( + (*slice)[(*slice).length - 1], + (!slice)[(!slice).length - 1], + ), + thrust_models::model::Mut::new( + (*slice).subsequence(0, (*slice).length - 1), + (!slice).subsequence(0, (!slice).length - 1), + ), + )) + ) + || ((*slice).length == 0 && result == None && !slice == *slice) +)] +fn _extern_spec_slice_split_last_mut(slice: &mut [T]) -> Option<(&mut T, &mut [T])> + where T: thrust_models::Model, T::Ty: PartialEq +{ + <[T]>::split_last_mut(slice) +} + // TODO: The following specs for Index/IndexMut methods are too specific; we should write specs for // a generic index (I: SliceIndex) that isn't specific to usize, maybe once #83 is implemented. diff --git a/tests/ui/fail/slice_split_first_mut.rs b/tests/ui/fail/slice_split_first_mut.rs new file mode 100644 index 00000000..504a026d --- /dev/null +++ b/tests/ui/fail/slice_split_first_mut.rs @@ -0,0 +1,19 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off +#[thrust::trusted] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + (*result).length == 2 + && (*result).array[(*result).offset] == 10 + && (*result).array[(*result).offset + 1] == 20 +)] +fn slice() -> &'static mut [i32] { + unimplemented!() +} + +fn main() { + let slice = slice(); + let (first, _tail) = slice.split_first_mut().unwrap(); + // wrong: the first element is 10, not 11 + assert!(*first == 11); +} diff --git a/tests/ui/fail/slice_split_first_mut_mutation_unsound.rs b/tests/ui/fail/slice_split_first_mut_mutation_unsound.rs new file mode 100644 index 00000000..abc11ff5 --- /dev/null +++ b/tests/ui/fail/slice_split_first_mut_mutation_unsound.rs @@ -0,0 +1,28 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +// KNOWN LIMITATION: mutation through a `&mut` returned inside a tuple (as +// `split_first_mut` does) does not currently propagate back to the original +// slice, which is unsound. This test is expected to be rejected (`Unsat`) once +// that is fixed; it is kept here as a reproduction until the fix lands. +#[thrust::trusted] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + (*result).length == 2 + && (*result).array[(*result).offset] == 10 + && (*result).array[(*result).offset + 1] == 20 +)] +fn slice() -> &'static mut [i32] { + unimplemented!() +} + +fn main() { + let slice = slice(); + { + // Destructure the returned tuple, then mutate through its first reference. + let (first, _tail) = slice.split_first_mut().unwrap(); + *first = 11; + } + // The mutation makes slice[0] equal to 11, so this must be rejected. + assert!(slice[0] == 12); +} diff --git a/tests/ui/fail/slice_split_last_mut.rs b/tests/ui/fail/slice_split_last_mut.rs new file mode 100644 index 00000000..98c0f202 --- /dev/null +++ b/tests/ui/fail/slice_split_last_mut.rs @@ -0,0 +1,19 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off +#[thrust::trusted] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + (*result).length == 2 + && (*result).array[(*result).offset] == 10 + && (*result).array[(*result).offset + 1] == 20 +)] +fn slice() -> &'static mut [i32] { + unimplemented!() +} + +fn main() { + let slice = slice(); + let (last, _init) = slice.split_last_mut().unwrap(); + // wrong: the last element is 20, not 21 + assert!(*last == 21); +} diff --git a/tests/ui/pass/slice_split_first_mut.rs b/tests/ui/pass/slice_split_first_mut.rs new file mode 100644 index 00000000..6370b970 --- /dev/null +++ b/tests/ui/pass/slice_split_first_mut.rs @@ -0,0 +1,20 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +#[thrust::trusted] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + (*result).length == 2 + && (*result).array[(*result).offset] == 10 + && (*result).array[(*result).offset + 1] == 20 +)] +fn slice() -> &'static mut [i32] { + unimplemented!() +} + +fn main() { + let slice = slice(); + let (first, tail) = slice.split_first_mut().unwrap(); + assert!(*first == 10); + assert!(tail.len() == 1); + assert!(*tail.first().unwrap() == 20); +} diff --git a/tests/ui/pass/slice_split_last_mut.rs b/tests/ui/pass/slice_split_last_mut.rs new file mode 100644 index 00000000..1a2b8ab7 --- /dev/null +++ b/tests/ui/pass/slice_split_last_mut.rs @@ -0,0 +1,20 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off +#[thrust::trusted] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures( + (*result).length == 2 + && (*result).array[(*result).offset] == 10 + && (*result).array[(*result).offset + 1] == 20 +)] +fn slice() -> &'static mut [i32] { + unimplemented!() +} + +fn main() { + let slice = slice(); + let (last, init) = slice.split_last_mut().unwrap(); + assert!(*last == 20); + assert!(init.len() == 1); + assert!(*init.first().unwrap() == 10); +}