Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757use super::super::prelude::*;use super::super::slice::SliceIndexSpec;use super::core::IndexSpec;use super::iter::IteratorSpec;use super::range::{ ExRange, RangeBoundsSpec, slice_range_end, slice_range_start, slice_range_valid, spec_range_inclusive_slice_bounds,};
use core::ops::{ Index, IndexMut, Range, RangeFrom, RangeFull, RangeInclusive, RangeTo, RangeToInclusive,};use core::slice::{Chunks, Iter, IterMut, SliceIndex};
use verus as verus_skip_verusfmt;verus_skip_verusfmt! {
impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for usize { open spec fn in_bounds(&self, slice: &[T]) -> bool { *self < slice@.len() }
open spec fn index_postcondition(&self, slice: &[T], r: &T) -> bool { r == slice@[self as int] }
open spec fn index_mut_postcondition( &self, old_slice: &[T], final_slice: &[T], immediate_output: &T, final_output: &T, ) -> bool { &&& *immediate_output == old_slice@[*self as int] &&& final_slice@ == old_slice@.update(*self as int, *final_output) }}
pub assume_specification<T>[ <usize as SliceIndex<[T]>>::get ](i: usize, slice: &[T]) -> Option<&T>;
pub assume_specification<T>[ <usize as SliceIndex<[T]>>::index ](i: usize, slice: &[T]) -> &T;
pub assume_specification<T>[ <usize as SliceIndex<[T]>>::get_mut ](i: usize, slice: &mut [T]) -> Option<&mut T>;
pub assume_specification<T>[ <usize as SliceIndex<[T]>>::index_mut ](i: usize, slice: &mut [T]) -> (output: &mut T);
pub open spec fn generic_slice_in_bounds<R: RangeBoundsSpec<usize>, T>( range: &R, s: Seq<T>) -> bool { slice_range_valid(range, s.len())}
pub open spec fn generic_slice_index_postcondition<R: RangeBoundsSpec<usize>, T>( range: &R, slice: Seq<T>, r: Seq<T>,) -> bool { r == slice[slice_range_start(range)..slice_range_end(range, slice.len())]}
pub open spec fn generic_slice_index_mut_postcondition<R: RangeBoundsSpec<usize>, T>( range: &R, old_slice: Seq<T>, final_slice: Seq<T>, immediate_output: Seq<T>, final_output: Seq<T>,) -> bool { &&& immediate_output == old_slice[slice_range_start(range)..slice_range_end(range, old_slice.len())] &&& final_slice.len() == old_slice.len() &&& final_slice[..slice_range_start(range)] == old_slice[..slice_range_start(range)] &&& final_slice[slice_range_start(range)..slice_range_end(range, old_slice.len())] == final_output &&& final_slice[slice_range_end(range, old_slice.len())..old_slice.len()] == old_slice[slice_range_end(range, old_slice.len())..old_slice.len()] // The following conjunct can be derived from the above four, but // it's useful to include anyway. &&& final_slice == old_slice[..slice_range_start(range)] + final_output + old_slice[ slice_range_end(range, old_slice.len())..old_slice.len()]}
impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for Range<usize> { open spec fn in_bounds(&self, slice: &[T]) -> bool { generic_slice_in_bounds(self, slice@) }
open spec fn index_postcondition(&self, slice: &[T], r: &[T]) -> bool { generic_slice_index_postcondition(self, slice@, r@) }
open spec fn index_mut_postcondition( &self, old_slice: &[T], final_slice: &[T], immediate_output: &[T], final_output: &[T] ) -> bool { generic_slice_index_mut_postcondition(self, old_slice@, final_slice@, immediate_output@, final_output@) }}
pub assume_specification<T>[ <Range<usize> as SliceIndex<[T]>>::get ](i: Range<usize>, slice: &[T]) -> Option<&[T]>;
pub assume_specification<T>[ <Range<usize> as SliceIndex<[T]>>::index ](i: Range<usize>, slice: &[T]) -> (r: &[T]);
pub assume_specification<T>[ <Range<usize> as SliceIndex<[T]>>::get_mut ](i: Range<usize>, slice: &mut [T]) -> Option<&mut [T]>;
pub assume_specification<T>[ <Range<usize> as SliceIndex<[T]>>::index_mut ](i: Range<usize>, slice: &mut [T]) -> (r: &mut [T]);
impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for RangeTo<usize> { open spec fn in_bounds(&self, slice: &[T]) -> bool { generic_slice_in_bounds(self, slice@) }
open spec fn index_postcondition(&self, slice: &[T], r: &[T]) -> bool { generic_slice_index_postcondition(self, slice@, r@) }
open spec fn index_mut_postcondition( &self, old_slice: &[T], final_slice: &[T], immediate_output: &[T], final_output: &[T] ) -> bool { generic_slice_index_mut_postcondition(self, old_slice@, final_slice@, immediate_output@, final_output@) }}
pub assume_specification<T>[ <RangeTo<usize> as SliceIndex<[T]>>::get ](i: RangeTo<usize>, slice: &[T]) -> Option<&[T]>;
pub assume_specification<T>[ <RangeTo<usize> as SliceIndex<[T]>>::index ](i: RangeTo<usize>, slice: &[T]) -> (r: &[T]);
pub assume_specification<T>[ <RangeTo<usize> as SliceIndex<[T]>>::get_mut ](i: RangeTo<usize>, slice: &mut [T]) -> Option<&mut [T]>;
pub assume_specification<T>[ <RangeTo<usize> as SliceIndex<[T]>>::index_mut ](i: RangeTo<usize>, slice: &mut [T]) -> (r: &mut [T]);
impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for RangeFrom<usize> { open spec fn in_bounds(&self, slice: &[T]) -> bool { generic_slice_in_bounds(self, slice@) }
open spec fn index_postcondition(&self, slice: &[T], r: &[T]) -> bool { generic_slice_index_postcondition(self, slice@, r@) }
open spec fn index_mut_postcondition( &self, old_slice: &[T], final_slice: &[T], immediate_output: &[T], final_output: &[T] ) -> bool { generic_slice_index_mut_postcondition(self, old_slice@, final_slice@, immediate_output@, final_output@) }}
pub assume_specification<T>[ <RangeFrom<usize> as SliceIndex<[T]>>::get ](i: RangeFrom<usize>, slice: &[T]) -> Option<&[T]>;
pub assume_specification<T>[ <RangeFrom<usize> as SliceIndex<[T]>>::index ](i: RangeFrom<usize>, slice: &[T]) -> (r: &[T]);
pub assume_specification<T>[ <RangeFrom<usize> as SliceIndex<[T]>>::get_mut ](i: RangeFrom<usize>, slice: &mut [T]) -> Option<&mut [T]>;
pub assume_specification<T>[ <RangeFrom<usize> as SliceIndex<[T]>>::index_mut ](i: RangeFrom<usize>, slice: &mut [T]) -> (r: &mut [T]);
impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for RangeToInclusive<usize> { open spec fn in_bounds(&self, slice: &[T]) -> bool { generic_slice_in_bounds(self, slice@) }
open spec fn index_postcondition(&self, slice: &[T], r: &[T]) -> bool { generic_slice_index_postcondition(self, slice@, r@) }
open spec fn index_mut_postcondition( &self, old_slice: &[T], final_slice: &[T], immediate_output: &[T], final_output: &[T] ) -> bool { generic_slice_index_mut_postcondition(self, old_slice@, final_slice@, immediate_output@, final_output@) }}
pub assume_specification<T>[ <RangeToInclusive<usize> as SliceIndex<[T]>>::get ](i: RangeToInclusive<usize>, slice: &[T]) -> Option<&[T]>;
pub assume_specification<T>[ <RangeToInclusive<usize> as SliceIndex<[T]>>::index ](i: RangeToInclusive<usize>, slice: &[T]) -> (r: &[T]);
pub assume_specification<T>[ <RangeToInclusive<usize> as SliceIndex<[T]>>::get_mut ](i: RangeToInclusive<usize>, slice: &mut [T]) -> Option<&mut [T]>;
pub assume_specification<T>[ <RangeToInclusive<usize> as SliceIndex<[T]>>::index_mut ](i: RangeToInclusive<usize>, slice: &mut [T]) -> (r: &mut [T]);
impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for RangeFull { open spec fn in_bounds(&self, slice: &[T]) -> bool { generic_slice_in_bounds(self, slice@) }
open spec fn index_postcondition(&self, slice: &[T], r: &[T]) -> bool { generic_slice_index_postcondition(self, slice@, r@) }
open spec fn index_mut_postcondition( &self, old_slice: &[T], final_slice: &[T], immediate_output: &[T], final_output: &[T] ) -> bool { generic_slice_index_mut_postcondition(self, old_slice@, final_slice@, immediate_output@, final_output@) }}
pub assume_specification<T>[ <RangeFull as SliceIndex<[T]>>::get ](i: RangeFull, slice: &[T]) -> Option<&[T]>;
pub assume_specification<T>[ <RangeFull as SliceIndex<[T]>>::index ](i: RangeFull, slice: &[T]) -> (r: &[T]);
pub assume_specification<T>[ <RangeFull as SliceIndex<[T]>>::get_mut ](i: RangeFull, slice: &mut [T]) -> Option<&mut [T]>;
pub assume_specification<T>[ <RangeFull as SliceIndex<[T]>>::index_mut ](i: RangeFull, slice: &mut [T]) -> (r: &mut [T]);
impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for RangeInclusive<usize> { open spec fn in_bounds(&self, slice: &[T]) -> bool { generic_slice_in_bounds(&spec_range_inclusive_slice_bounds(self), slice@) }
open spec fn index_postcondition(&self, slice: &[T], r: &[T]) -> bool { generic_slice_index_postcondition(&spec_range_inclusive_slice_bounds(self), slice@, r@) }
open spec fn index_mut_postcondition( &self, old_slice: &[T], final_slice: &[T], immediate_output: &[T], final_output: &[T] ) -> bool { generic_slice_index_mut_postcondition(&spec_range_inclusive_slice_bounds(self), old_slice@, final_slice@, immediate_output@, final_output@) }}
pub assume_specification<T>[ <RangeInclusive<usize> as SliceIndex<[T]>>::get ](i: RangeInclusive<usize>, slice: &[T]) -> Option<&[T]>;
pub assume_specification<T>[ <RangeInclusive<usize> as SliceIndex<[T]>>::index ](i: RangeInclusive<usize>, slice: &[T]) -> (r: &[T]);
pub assume_specification<T>[ <RangeInclusive<usize> as SliceIndex<[T]>>::get_mut ](i: RangeInclusive<usize>, slice: &mut [T]) -> Option<&mut [T]>;
pub assume_specification<T>[ <RangeInclusive<usize> as SliceIndex<[T]>>::index_mut ](i: RangeInclusive<usize>, slice: &mut [T]) -> (r: &mut [T]);
// starts_with// Rust compares `needle == &slice[..needle.len()]`pub open spec fn spec_slice_starts_with<T: PartialEq>(slice: &[T], needle: &[T]) -> bool { &&& needle@.len() <= slice@.len() &&& forall|i: int| #![auto] 0 <= i < needle@.len() ==> <T as super::cmp::PartialEqSpec<T>>::eq_spec( &needle@[i], &slice@[i], )}
#[verifier::when_used_as_spec(spec_slice_starts_with)]pub assume_specification<T: PartialEq>[ <[T]>::starts_with ]( slice: &[T], needle: &[T],) -> (result: bool) ensures needle@.len() > slice@.len() ==> !result, <T as super::cmp::PartialEqSpec<T>>::obeys_eq_spec() ==> (result == spec_slice_starts_with( slice, needle, )),;
// ends_with// Rust compares `needle == &slice[slice.len() - needle.len()..]`.pub open spec fn spec_slice_ends_with<T: PartialEq>(slice: &[T], needle: &[T]) -> bool { &&& needle@.len() <= slice@.len() &&& forall|i: int| #![auto] 0 <= i < needle@.len() ==> <T as super::cmp::PartialEqSpec<T>>::eq_spec( &needle@[i], &slice@[slice@.len() - needle@.len() + i], )}
#[verifier::when_used_as_spec(spec_slice_ends_with)]pub assume_specification<T: PartialEq>[ <[T]>::ends_with ]( slice: &[T], needle: &[T],) -> (result: bool) ensures needle@.len() > slice@.len() ==> !result, <T as super::cmp::PartialEqSpec<T>>::obeys_eq_spec() ==> (result == spec_slice_ends_with( slice, needle, )),;
impl<T, I: SliceIndex<[T]>> super::core::IndexSpecImpl<I> for [T] { open spec fn index_req(&self, index: &I) -> bool { index.in_bounds(self) }}
pub assume_specification<T, I>[ <[T]>::get::<I> ](slice: &[T], i: I) -> (b: Option< &<I as SliceIndex<[T]>>::Output,>) where I: SliceIndex<[T]> ensures call_ensures(<I as SliceIndex<[T]>>::get, (i, slice), b),;
pub assume_specification<T, I>[ <[T]>::get_mut::<I> ](slice: &mut [T], i: I) -> (b: Option< &mut <I as SliceIndex<[T]>>::Output,>) where I: SliceIndex<[T]> ensures call_ensures(<I as SliceIndex<[T]>>::get_mut, (i, slice), b),;
pub assume_specification<T, I: SliceIndex<[T]>>[ <[T] as Index<I>>::index ]( slice: &[T], index: I,) -> (output: &<I as SliceIndex<[T]>>::Output) ensures call_ensures(<I as SliceIndex<[T]>>::index, (index, slice), output),;
pub assume_specification<T, I: SliceIndex<[T]>>[ <[T] as IndexMut<I>>::index_mut ]( slice: &mut [T], index: I,) -> (output: &mut <I as SliceIndex<[T]>>::Output) ensures call_ensures(<I as SliceIndex<[T]>>::index_mut, (index, slice), output),;
// `get_unchecked(i)`/`get_unchecked_mut(i)` share the contract of `index`/`index_mut`, with// the in-bounds check as a safety precondition (UB if violated) rather than a panic.pub assume_specification<T, I>[ <[T]>::get_unchecked::<I> ]( slice: &[T], index: I,) -> (output: &<I as SliceIndex<[T]>>::Output) where I: SliceIndex<[T]> requires index.in_bounds(slice), ensures index.index_postcondition(slice, output),;
pub assume_specification<T, I>[ <[T]>::get_unchecked_mut::<I> ]( slice: &mut [T], index: I,) -> (output: &mut <I as SliceIndex<[T]>>::Output) where I: SliceIndex<[T]> requires index.in_bounds(&*old(slice)), ensures index.index_mut_postcondition(&*old(slice), &*final(slice), output, &*final(output)),;
impl<T, I, const N: usize> super::core::IndexSpecImpl<I> for [T; N]where [T]: Index<I>,{ open spec fn index_req(&self, index: &I) -> bool { <[T] as IndexSpec<I>>::index_req(self, index) }}
pub assume_specification<T, I, const N: usize>[ <[T; N]>::index ](array: &[T; N], index: I) -> (output: &<[T; N] as Index<I>>::Output) where [T]: Index<I>, ensures call_ensures(<[T]>::index, (array, index), output),;
pub assume_specification<T, I, const N: usize>[ <[T; N]>::index_mut ](array: &mut [T; N], index: I) -> (output: &mut <[T; N] as Index<I>>::Output) where [T]: IndexMut<I>, ensures exists|slice: &mut [T]| { &&& #[trigger] slice@ == old(array)@ &&& final(slice)@ == final(array)@ &&& call_ensures(<[T]>::index_mut, (slice, index), output) },;
pub assume_specification[ core::hint::unreachable_unchecked ]() -> ! requires false,;
// slice == slicepub assume_specification<T: PartialEq<U>, U>[ <[T] as PartialEq<[U]>>::eq ]( left: &[T], right: &[U],) -> bool;
impl<T, U> super::cmp::PartialEqSpecImpl<[U]> for [T] where T: PartialEq<U> + super::cmp::PartialEqSpec<U> { open spec fn obeys_eq_spec() -> bool { <T as super::cmp::PartialEqSpec<U>>::obeys_eq_spec() }
open spec fn eq_spec(&self, other: &[U]) -> bool { &&& self@.len() == other@.len() &&& forall|i: int| #![auto] 0 <= i < self@.len() ==> <T as super::cmp::PartialEqSpec<U>>::eq_spec(&self@[i], &other@[i]) }}
// containspub open spec fn spec_slice_contains<T: PartialEq<T>>(slice: &[T], value: &T) -> bool { exists |i: int| #![auto] 0 <= i < slice@.len() && <T as super::cmp::PartialEqSpec<T>>::eq_spec(&slice[i], value)}
#[verifier::when_used_as_spec(spec_slice_contains)]pub assume_specification<T>[ <[T]>::contains ] (slice: &[T], value: &T) -> (result: bool) where T: PartialEq<T>, ensures <T as super::cmp::PartialEqSpec<T>>::obeys_eq_spec() ==> result == spec_slice_contains(slice, value),;
// reversepub assume_specification<T>[ <[T]>::reverse ](slice: &mut [T]) ensures final(slice)@ == old(slice)@.reverse(),;
// swappub assume_specification<T>[ <[T]>::swap ](slice: &mut [T], a: usize, b: usize) requires a < old(slice)@.len(), b < old(slice)@.len(), ensures final(slice)@ == old(slice)@.update(a as int, old(slice)@[b as int]).update(b as int, old(slice)@[a as int]), no_unwind;
// The `iter` method of a `<T>` returns an iterator of type `Iter<'_, T>`,// so we specify that type here.#[verifier::external_type_specification]#[verifier::external_body]#[verifier::accept_recursive_types(T)]pub struct ExIter<'a, T: 'a>(Iter<'a, T>);
// To allow reasoning about the "contents" of the slice iterator, without using// a prophecy, we need a function that gives us the underlying sequence of the original slice.pub uninterp spec fn into_iter_elts<'a, T: 'a>(i: Iter<'a, T>) -> Seq<T>;
impl <'a, T: 'a> super::iter::IteratorSpecImpl for Iter<'a, T> { open spec fn obeys_prophetic_iter_laws(&self) -> bool { true }
uninterp spec fn remaining(&self) -> Seq<Self::Item>; #[verifier::prophetic] open spec fn produces(&self) -> Seq<bool> { Seq::new(IteratorSpec::remaining(self).len(), |i: int| true) } uninterp spec fn decrease(&self) -> Option<nat>;
open spec fn peek(&self, index: int) -> Option<Self::Item> { if 0 <= index < into_iter_elts(*self).len() { Some(&into_iter_elts(*self)[index]) } else { None } }}
pub assume_specification<'a, T>[ <[T]>::iter ](s: &'a [T]) -> (iter: Iter<'a, T>) ensures IteratorSpec::remaining(&iter) == s@.as_ref(), into_iter_elts(iter) == IteratorSpec::remaining(&iter).unref(), IteratorSpec::decrease(&iter) is Some,;
pub assume_specification<'a, T> [<&'a [T] as core::iter::IntoIterator>::into_iter] (s: &'a [T]) -> (iter: Iter<'a, T>) ensures IteratorSpec::remaining(&iter) == s@.as_ref(), into_iter_elts(iter) == IteratorSpec::remaining(&iter).unref(), IteratorSpec::decrease(&iter) is Some,;
/*********************************************************************************************** * Definitions for `slice::IterMut` (the iterator behind `<[T]>::iter_mut` and `Vec::iter_mut`) ***********************************************************************************************/#[verifier::external_type_specification]#[verifier::external_body]#[verifier::accept_recursive_types(T)]pub struct ExIterMut<'a, T: 'a>(IterMut<'a, T>);
// See exampes/iterators/slice_iter_mut.rs for a verified implementation of this interface.// Any changes here should first be verified over there.impl<'a, T: 'a> super::iter::IteratorSpecImpl for IterMut<'a, T> { open spec fn obeys_prophetic_iter_laws(&self) -> bool { true }
#[verifier::prophetic] uninterp spec fn remaining(&self) -> Seq<Self::Item>;
#[verifier::prophetic] open spec fn produces(&self) -> Seq<bool> { Seq::new(IteratorSpec::remaining(self).len(), |i: int| true) }
uninterp spec fn decrease(&self) -> Option<nat>;
open spec fn peek(&self, index: int) -> Option<Self::Item> { None }}
// Also covers `vec.iter_mut(), which reaches this slice fn through `Vec`'s `DerefMut`pub assume_specification<'a, T>[ <[T]>::iter_mut ](slice: &'a mut [T]) -> (iter: IterMut<'a, T>) ensures IteratorSpec::remaining(&iter).len() == old(slice)@.len() == final(slice)@.len(), // Each yielded reference initially points at the corresponding element... forall|i: int| #![trigger IteratorSpec::remaining(&iter)[i]] 0 <= i < old(slice)@.len() ==> *(IteratorSpec::remaining(&iter)[i]) == old(slice)@[i], // ...and its eventual value flows back to the corresponding element. forall|i: int| #![trigger IteratorSpec::remaining(&iter)[i]] #![trigger final(slice)@[i]] 0 <= i < old(slice)@.len() ==> *final(IteratorSpec::remaining(&iter)[i]) == final(slice)@[i], IteratorSpec::obeys_prophetic_iter_laws(&iter), IteratorSpec::produces(&iter).all(|p: bool| p), IteratorSpec::decrease(&iter) is Some,;
pub assume_specification<T> [ <[T]>::first ](slice: &[T]) -> (res: Option<&T>) ensures slice.len() == 0 ==> res.is_none(), slice.len() != 0 ==> res.is_some() && res.unwrap() == slice[0] no_unwind;
pub assume_specification<T> [ <[T]>::last ](slice: &[T]) -> (res: Option<&T>) ensures slice.len() == 0 ==> res.is_none(), slice.len() != 0 ==> res.is_some() && res.unwrap() == slice@.last() no_unwind;
#[doc(hidden)]pub assume_specification<T> [ <[T]>::first_mut ](slice: &mut [T]) -> (res: Option<&mut T>) ensures old(slice).len() == 0 ==> res.is_none() && final(slice)@ == seq![], old(slice).len() != 0 ==> res.is_some() && *res.unwrap() == old(slice)[0] && final(slice)@ == old(slice)@.update(0, *final(res.unwrap())) no_unwind;
#[doc(hidden)]pub assume_specification<T> [ <[T]>::last_mut ](slice: &mut [T]) -> (res: Option<&mut T>) ensures old(slice).len() == 0 ==> res.is_none() && final(slice)@ == seq![], old(slice).len() != 0 ==> res.is_some() && *res.unwrap() == old(slice)@.last() && final(slice)@ == old(slice)@.update(old(slice).len() - 1, *final(res.unwrap())) no_unwind;
pub assume_specification<T> [ <[T]>::split_at ](slice: &[T], mid: usize) -> (ret: (&[T], &[T])) requires 0 <= mid <= slice.len(), ensures ret.0@ == slice@[..mid], ret.1@ == slice@[mid..], no_unwind;
#[doc(hidden)]pub assume_specification<T> [ <[T]>::split_at_mut ](slice: &mut [T], mid: usize) -> (ret: (&mut [T], &mut [T])) requires 0 <= mid <= slice.len(), ensures ret.0@ == old(slice)@[..mid], ret.1@ == old(slice)@[mid..], final(slice)@ == final(ret.0)@ + final(ret.1)@, no_unwind;
// The non-panicking (`Option`-returning) form of `split_at`: `Some((a, b))` split at `mid`// when `mid <= len`, else `None`.pub assume_specification<T> [ <[T]>::split_at_checked ](slice: &[T], mid: usize) -> (ret: Option<(&[T], &[T])>) ensures mid <= slice.len() ==> (ret matches Some((a, b)) && a@ == slice@[..mid] && b@ == slice@[mid..]), mid > slice.len() ==> ret is None, no_unwind;
pub assume_specification<T> [ <[T]>::split_at_unchecked ](slice: &[T], mid: usize) -> (ret: (&[T], &[T])) requires 0 <= mid <= slice.len(), ensures ret.0@ == slice@[..mid], ret.1@ == slice@[mid..], no_unwind;
#[doc(hidden)]pub assume_specification<T> [ <[T]>::split_at_mut_unchecked ](slice: &mut [T], mid: usize) -> (ret: (&mut [T], &mut [T])) requires 0 <= mid <= slice.len(), ensures ret.0@ == old(slice)@[..mid], ret.1@ == old(slice)@[mid..], final(slice)@ == final(ret.0)@ + final(ret.1)@, no_unwind;
pub assume_specification<T> [ <[T]>::split_first ](slice: &[T]) -> (ret: Option<(&T, &[T])>) ensures slice.len() == 0 ==> ret.is_none(), slice.len() > 0 ==> (ret matches Some((a, b)) && a == slice[0] && b@ == slice@[1..]) no_unwind;
pub assume_specification<T> [ <[T]>::split_first_mut ](slice: &mut [T]) -> (ret: Option<(&mut T, &mut [T])>) ensures old(slice).len() == 0 ==> ret.is_none() && final(slice)@ == seq![], old(slice).len() > 0 ==> (ret matches Some((a, b)) && *a == old(slice)[0] && b@ == old(slice)@[1..] && b@.len() == final(b)@.len() && final(slice)@ == seq![*final(a)] + final(b)@ ) no_unwind;
/// Copy the contents of `src` into `dst`, which must have the same length.pub assume_specification<T: Copy>[ <[T]>::copy_from_slice ](dst: &mut [T], src: &[T]) requires old(dst)@.len() == src@.len(), ensures final(dst)@ == src@,;
/// The sequence resulting from copying `old_slice[src_start..src_end]` to start/// at index `dest`, leaving all other positions unchanged. Reads are taken from/// `old_slice`, so overlapping source and destination ranges are handled like/// std's `<[T]>::copy_within` (which uses `ptr::copy`).pub open spec fn copy_within_result<T>( old_slice: Seq<T>, src_start: int, src_end: int, dest: int,) -> Seq<T> { let count = src_end - src_start; Seq::new( old_slice.len(), |i: int| if dest <= i && i < dest + count { old_slice[src_start + (i - dest)] } else { old_slice[i] }, )}
/// Copy the elements in range `src` within the slice to start at index `dest`.pub assume_specification<T: Copy, R: core::ops::RangeBounds<usize>>[ <[T]>::copy_within::<R> ]( slice: &mut [T], src: R, dest: usize,) requires slice_range_valid(&src, old(slice)@.len()), (dest as int) + (slice_range_end(&src, old(slice)@.len()) - slice_range_start(&src)) <= old(slice)@.len(), ensures final(slice)@ == copy_within_result( old(slice)@, slice_range_start(&src), slice_range_end(&src, old(slice)@.len()), dest as int, ),;
// The `chunks` method of a `[T]` returns an iterator of type `Chunks<'_, T>`,// so we specify that type here.#[verifier::external_type_specification]#[verifier::external_body]#[verifier::accept_recursive_types(T)]pub struct ExChunks<'a, T: 'a>(Chunks<'a, T>);
// To allow reasoning about the "chunks" of the slice iterator, without using// a prophecy, we need a function that gives us the the sequence of chunk slices// remaining in the iterator.pub uninterp spec fn after_chunks_elts<'a, T: 'a>(i: Chunks<'a, T>) -> Seq<&'a [T]>;
impl<'a, T: 'a> super::iter::IteratorSpecImpl for Chunks<'a, T> { open spec fn obeys_prophetic_iter_laws(&self) -> bool { true }
uninterp spec fn remaining(&self) -> Seq<Self::Item>;
#[verifier::prophetic] open spec fn produces(&self) -> Seq<bool> { Seq::new(IteratorSpec::remaining(self).len(), |i: int| true) }
uninterp spec fn decrease(&self) -> Option<nat>;
open spec fn peek(&self, index: int) -> Option<Self::Item> { if 0 <= index < after_chunks_elts(*self).len() { Some(after_chunks_elts(*self)[index]) } else { None } }}
pub assume_specification<'a, T>[ <[T]>::chunks ](s: &'a [T], chunk_size: usize) -> (iter: Chunks< 'a, T,>) requires chunk_size > 0, ensures IteratorSpec::remaining(&iter) == after_chunks_elts(iter), IteratorSpec::remaining(&iter).len() == (s@.len() + chunk_size as int - 1) / ( chunk_size as int), forall|i: int| #![trigger IteratorSpec::remaining(&iter)[i]] 0 <= i < IteratorSpec::remaining(&iter).len() ==> { let start = i * chunk_size as int; let end = if start + chunk_size as int <= s@.len() { start + chunk_size as int } else { s@.len() as int };
IteratorSpec::remaining(&iter)[i]@ == s@.subrange(start, end) }, IteratorSpec::decrease(&iter) is Some,;
} // verus!