pub trait IteratorSpecImpl: Iterator {
// Required methods
exec fn obeys_prophetic_iter_laws(&self) -> bool;
exec fn remaining(&self) -> Seq<Self::Item>;
exec fn will_return_none(&self) -> bool;
exec fn decrease(&self) -> Option<nat>;
exec fn initial_value_relation(&self, init: &Self) -> bool;
exec fn peek(&self, index: int) -> Option<Self::Item>;
}Required Methods§
Sourceexec fn obeys_prophetic_iter_laws(&self) -> bool
exec fn obeys_prophetic_iter_laws(&self) -> bool
This iterator obeys the specifications below on next,
expressed in terms of prophetic spec functions.
Only iterators that terminate (i.e., eventually return None
and then continue to return None) should use this interface.
Sourceexec fn remaining(&self) -> Seq<Self::Item>
exec fn remaining(&self) -> Seq<Self::Item>
Sequence of items that will (eventually) be returned
Sourceexec fn will_return_none(&self) -> bool
exec fn will_return_none(&self) -> bool
Does this iterator complete with a None after the above sequence?
(As opposed to hanging indefinitely on a next() call)
Trivially true for most iterators but important for iterators
that apply an exec closure that may not terminate.
Sourceexec fn decrease(&self) -> Option<nat>
exec fn decrease(&self) -> Option<nat>
Value used by default for the decreases clause when no explicit decreases clause is provided (the user can override this with an explicit decreases clause). If there’s no appropriate metric to decrease, this can return None, and the user will have to provide an explicit decreases clause.
Sourceexec fn initial_value_relation(&self, init: &Self) -> bool
exec fn initial_value_relation(&self, init: &Self) -> bool
Invariant relating the iterator to the initial expression that created it
(e.g., my_vec.iter()). This allows for more ergonomic/intuitive invariants.
When the analysis can infer a spec initial value (by discovering a when_used_as_spec
annotation), the analysis places the value in init.
Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.
Implementations on Foreign Types§
Source§impl<'a> IteratorSpecImpl for Chars<'a>
Available on verus_keep_ghost and crate feature alloc only.
impl<'a> IteratorSpecImpl for Chars<'a>
Available on
verus_keep_ghost and crate feature alloc only.Source§open spec fn obeys_prophetic_iter_laws(&self) -> bool
open spec fn obeys_prophetic_iter_laws(&self) -> bool
{ true }Source§uninterp spec fn will_return_none(&self) -> bool
uninterp spec fn will_return_none(&self) -> bool
Source§open spec fn initial_value_relation(&self, init: &Self) -> bool
open spec fn initial_value_relation(&self, init: &Self) -> bool
{
&&& IteratorSpec::remaining(init) == IteratorSpec::remaining(self)
&&& into_iter_elts(*self) == IteratorSpec::remaining(self)
}Source§impl<'a, K> IteratorSpecImpl for Iter<'a, K>
impl<'a, K> IteratorSpecImpl for Iter<'a, K>
Source§open spec fn obeys_prophetic_iter_laws(&self) -> bool
open spec fn obeys_prophetic_iter_laws(&self) -> bool
{ true }Source§uninterp spec fn will_return_none(&self) -> bool
uninterp spec fn will_return_none(&self) -> bool
Source§open spec fn initial_value_relation(&self, init: &Self) -> bool
open spec fn initial_value_relation(&self, init: &Self) -> bool
{
&&& IteratorSpec::remaining(init) == IteratorSpec::remaining(self)
&&& into_iter_hash_keys(*self) == IteratorSpec::remaining(self).unref()
}Source§impl<'a, K, V> IteratorSpecImpl for Iter<'a, K, V>
impl<'a, K, V> IteratorSpecImpl for Iter<'a, K, V>
Source§open spec fn obeys_prophetic_iter_laws(&self) -> bool
open spec fn obeys_prophetic_iter_laws(&self) -> bool
{ true }Source§uninterp spec fn will_return_none(&self) -> bool
uninterp spec fn will_return_none(&self) -> bool
Source§open spec fn initial_value_relation(&self, init: &Self) -> bool
open spec fn initial_value_relation(&self, init: &Self) -> bool
{
&&& IteratorSpec::remaining(init) == IteratorSpec::remaining(self)
&&& into_iter(*self) == IteratorSpec::remaining(self).unref()
}Source§impl<'a, K, V> IteratorSpecImpl for Keys<'a, K, V>
impl<'a, K, V> IteratorSpecImpl for Keys<'a, K, V>
Source§open spec fn obeys_prophetic_iter_laws(&self) -> bool
open spec fn obeys_prophetic_iter_laws(&self) -> bool
{ true }Source§uninterp spec fn will_return_none(&self) -> bool
uninterp spec fn will_return_none(&self) -> bool
Source§open spec fn initial_value_relation(&self, init: &Self) -> bool
open spec fn initial_value_relation(&self, init: &Self) -> bool
{
&&& IteratorSpec::remaining(init) == IteratorSpec::remaining(self)
&&& into_iter_keys(*self) == IteratorSpec::remaining(self).unref()
}Source§impl<'a, K, V> IteratorSpecImpl for Values<'a, K, V>
impl<'a, K, V> IteratorSpecImpl for Values<'a, K, V>
Source§open spec fn obeys_prophetic_iter_laws(&self) -> bool
open spec fn obeys_prophetic_iter_laws(&self) -> bool
{ true }Source§uninterp spec fn will_return_none(&self) -> bool
uninterp spec fn will_return_none(&self) -> bool
Source§open spec fn initial_value_relation(&self, init: &Self) -> bool
open spec fn initial_value_relation(&self, init: &Self) -> bool
{
&&& IteratorSpec::remaining(init) == IteratorSpec::remaining(self)
&&& into_iter_values(*self) == IteratorSpec::remaining(self).unref()
}Source§impl<'a, K, V> IteratorSpecImpl for Iter<'a, K, V>
impl<'a, K, V> IteratorSpecImpl for Iter<'a, K, V>
Source§open spec fn obeys_prophetic_iter_laws(&self) -> bool
open spec fn obeys_prophetic_iter_laws(&self) -> bool
{ true }Source§uninterp spec fn will_return_none(&self) -> bool
uninterp spec fn will_return_none(&self) -> bool
Source§open spec fn initial_value_relation(&self, init: &Self) -> bool
open spec fn initial_value_relation(&self, init: &Self) -> bool
{
&&& IteratorSpec::remaining(init) == IteratorSpec::remaining(self)
&&& into_iter(*self) == IteratorSpec::remaining(self).unref()
}Source§impl<'a, K, V> IteratorSpecImpl for Keys<'a, K, V>
impl<'a, K, V> IteratorSpecImpl for Keys<'a, K, V>
Source§open spec fn obeys_prophetic_iter_laws(&self) -> bool
open spec fn obeys_prophetic_iter_laws(&self) -> bool
{ true }Source§uninterp spec fn will_return_none(&self) -> bool
uninterp spec fn will_return_none(&self) -> bool
Source§open spec fn initial_value_relation(&self, init: &Self) -> bool
open spec fn initial_value_relation(&self, init: &Self) -> bool
{
&&& IteratorSpec::remaining(init) == IteratorSpec::remaining(self)
&&& into_iter_keys(*self) == IteratorSpec::remaining(self).unref()
}Source§impl<'a, K, V> IteratorSpecImpl for Values<'a, K, V>
impl<'a, K, V> IteratorSpecImpl for Values<'a, K, V>
Source§open spec fn obeys_prophetic_iter_laws(&self) -> bool
open spec fn obeys_prophetic_iter_laws(&self) -> bool
{ true }Source§uninterp spec fn will_return_none(&self) -> bool
uninterp spec fn will_return_none(&self) -> bool
Source§open spec fn initial_value_relation(&self, init: &Self) -> bool
open spec fn initial_value_relation(&self, init: &Self) -> bool
{
&&& IteratorSpec::remaining(init) == IteratorSpec::remaining(self)
&&& into_iter_values(*self) == IteratorSpec::remaining(self).unref()
}Source§impl<'a, T> IteratorSpecImpl for Iter<'a, T>
impl<'a, T> IteratorSpecImpl for Iter<'a, T>
Source§open spec fn obeys_prophetic_iter_laws(&self) -> bool
open spec fn obeys_prophetic_iter_laws(&self) -> bool
{ true }Source§uninterp spec fn will_return_none(&self) -> bool
uninterp spec fn will_return_none(&self) -> bool
Source§open spec fn initial_value_relation(&self, init: &Self) -> bool
open spec fn initial_value_relation(&self, init: &Self) -> bool
{
&&& IteratorSpec::remaining(init) == IteratorSpec::remaining(self)
&&& into_iter_btree_keys(*self) == IteratorSpec::remaining(self).unref()
}Source§impl<'a, T: 'a> IteratorSpecImpl for Iter<'a, T>
impl<'a, T: 'a> IteratorSpecImpl for Iter<'a, T>
Source§open spec fn obeys_prophetic_iter_laws(&self) -> bool
open spec fn obeys_prophetic_iter_laws(&self) -> bool
{ true }Source§uninterp spec fn will_return_none(&self) -> bool
uninterp spec fn will_return_none(&self) -> bool
Source§open spec fn initial_value_relation(&self, init: &Self) -> bool
open spec fn initial_value_relation(&self, init: &Self) -> bool
{
&&& IteratorSpec::remaining(init) == IteratorSpec::remaining(self)
&&& into_iter_elts(*self) == IteratorSpec::remaining(self)
}Source§impl<'a, T: 'a> IteratorSpecImpl for Iter<'a, T>
impl<'a, T: 'a> IteratorSpecImpl for Iter<'a, T>
Source§open spec fn obeys_prophetic_iter_laws(&self) -> bool
open spec fn obeys_prophetic_iter_laws(&self) -> bool
{ true }Source§uninterp spec fn will_return_none(&self) -> bool
uninterp spec fn will_return_none(&self) -> bool
Source§open spec fn initial_value_relation(&self, init: &Self) -> bool
open spec fn initial_value_relation(&self, init: &Self) -> bool
{
&&& IteratorSpec::remaining(init) == IteratorSpec::remaining(self)
&&& into_iter_elts(*self) == IteratorSpec::remaining(self).unref()
}Source§impl<A: Step> IteratorSpecImpl for Range<A>
impl<A: Step> IteratorSpecImpl for Range<A>
Source§open spec fn obeys_prophetic_iter_laws(&self) -> bool
open spec fn obeys_prophetic_iter_laws(&self) -> bool
{ true }Source§open spec fn remaining(&self) -> Seq<Self::Item>
open spec fn remaining(&self) -> Seq<Self::Item>
{
Seq::new(
self.start.spec_steps_between_int(self.end) as nat,
|i: int| self.start.spec_forward_checked_int(i).unwrap(),
)
}Source§uninterp spec fn will_return_none(&self) -> bool
uninterp spec fn will_return_none(&self) -> bool
Source§open spec fn initial_value_relation(&self, init: &Self) -> bool
open spec fn initial_value_relation(&self, init: &Self) -> bool
{
&&& (self.start.spec_steps_between_int(self.end) <= 0
&& IteratorSpec::remaining(self).len() == 0)
|| (self.start.spec_steps_between_int(self.end)
== IteratorSpec::remaining(self).len() as int)
&&& forall |i: int| {
0 <= i < IteratorSpec::remaining(self).len()
==> #[trigger] IteratorSpec::remaining(self)[i]
== self.start.spec_forward_checked_int(i).unwrap()
}
&&& self.start == init.start
&&& self.end == init.end
&&& (init.start.spec_steps_between_int(init.end) <= 0
&& IteratorSpec::remaining(self).len() == 0)
|| (init.start.spec_steps_between_int(self.end)
== IteratorSpec::remaining(self).len() as int)
&&& forall |i: int| {
0 <= i < IteratorSpec::remaining(self).len()
==> #[trigger] IteratorSpec::remaining(self)[i]
== init.start.spec_forward_checked_int(i).unwrap()
}
}Source§impl<I> IteratorSpecImpl for Rev<I>where
I: DoubleEndedIterator + DoubleEndedIteratorSpec,
impl<I> IteratorSpecImpl for Rev<I>where
I: DoubleEndedIterator + DoubleEndedIteratorSpec,
Source§open spec fn obeys_prophetic_iter_laws(&self) -> bool
open spec fn obeys_prophetic_iter_laws(&self) -> bool
{ rev_iter(*self).obeys_prophetic_iter_laws() }Source§closed spec fn will_return_none(&self) -> bool
closed spec fn will_return_none(&self) -> bool
Source§open spec fn initial_value_relation(&self, init: &Self) -> bool
open spec fn initial_value_relation(&self, init: &Self) -> bool
{
&&& IteratorSpec::remaining(init) == IteratorSpec::remaining(self)
&&& rev_iter(*self).initial_value_relation(&rev_iter(*init))
}Source§impl<T, A: Allocator> IteratorSpecImpl for IntoIter<T, A>
impl<T, A: Allocator> IteratorSpecImpl for IntoIter<T, A>
Source§open spec fn obeys_prophetic_iter_laws(&self) -> bool
open spec fn obeys_prophetic_iter_laws(&self) -> bool
{ true }Source§uninterp spec fn will_return_none(&self) -> bool
uninterp spec fn will_return_none(&self) -> bool
Source§open spec fn initial_value_relation(&self, init: &Self) -> bool
open spec fn initial_value_relation(&self, init: &Self) -> bool
{
&&& IteratorSpec::remaining(init) == IteratorSpec::remaining(self)
&&& into_iter_elts(*self) == IteratorSpec::remaining(self)
}