Trait IteratorSpecImpl 

pub trait IteratorSpecImpl: Iterator {
    // Required methods
    exec fn obeys_prophetic_iter_laws(&self) -> bool;
    exec fn remaining(&self) -> Seq<Self::Item>;
    exec fn produces(&self) -> Seq<bool>;
    exec fn decrease(&self) -> Option<nat>;
    exec fn peek(&self, index: int) -> Option<Self::Item>;
}

Required Methods

exec fn obeys_prophetic_iter_laws(&self) -> bool

This iterator obeys the specifications below on next, expressed in terms of prophetic spec functions. Only finite iterators (i.e., those that eventually return None and then continue to return None) or infinite iterators that never return None should use this interface.

exec fn remaining(&self) -> Seq<Self::Item>

Sequence of all potentially returned items

exec fn produces(&self) -> Seq<bool>

For each potential item in remaining(), does the item actually get returned, or does the iterator get “stuck” trying to produce it, e.g., because a client supplied a closure that diverges?

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.

exec fn peek(&self, index: int) -> Option<Self::Item>

Dyn Compatibility

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementations on Foreign Types

impl<'a, K, V> IteratorSpecImpl for Iter<'a, K, V>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

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(*self).len() {
        let (k, v) = into_iter(*self)[index];
        Some((&k, &v))
    } else {
        None
    }
}

impl<'a, K, V> IteratorSpecImpl for Iter<'a, K, V>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

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(*self).len() {
        let (k, v) = into_iter(*self)[index];
        Some((&k, &v))
    } else {
        None
    }
}

impl<'a, K, V> IteratorSpecImpl for Keys<'a, K, V>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

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_keys(*self).len() {
        Some(&into_iter_keys(*self)[index])
    } else {
        None
    }
}

impl<'a, K, V> IteratorSpecImpl for Keys<'a, K, V>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

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_keys(*self).len() {
        Some(&into_iter_keys(*self)[index])
    } else {
        None
    }
}

impl<'a, K, V> IteratorSpecImpl for Values<'a, K, V>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

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_values(*self).len() {
        Some(&into_iter_values(*self)[index])
    } else {
        None
    }
}

impl<'a, K, V> IteratorSpecImpl for Values<'a, K, V>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

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_values(*self).len() {
        Some(&into_iter_values(*self)[index])
    } else {
        None
    }
}

impl<'a, K> IteratorSpecImpl for Iter<'a, K>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

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_hash_keys(*self).len() {
        Some(&into_iter_hash_keys(*self)[index])
    } else {
        None
    }
}

impl<'a, T: 'a> IteratorSpecImpl for Chunks<'a, T>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

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
    }
}

impl<'a, T: 'a> IteratorSpecImpl for Iter<'a, T>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

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
    }
}

impl<'a, T: 'a> IteratorSpecImpl for Iter<'a, T>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

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
    }
}

impl<'a, T: 'a> IteratorSpecImpl for IterMut<'a, T>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

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 }

impl<'a, T> IteratorSpecImpl for Iter<'a, T>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

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_btree_keys(*self).len() {
        Some(&into_iter_btree_keys(*self)[index])
    } else {
        None
    }
}

impl<'a> IteratorSpecImpl for Chars<'a>

Available on verus_keep_ghost and crate feature alloc only.

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

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
    }
}

impl<A, B> IteratorSpecImpl for Zip<A, B>

where A: Iterator + IteratorSpec, B: Iterator + IteratorSpec,

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{
    &&& zip_iter_fst(*self).obeys_prophetic_iter_laws()
    &&& zip_iter_snd(*self).obeys_prophetic_iter_laws()

}

closed spec fn remaining(&self) -> Seq<Self::Item>

closed spec fn produces(&self) -> Seq<bool>

closed spec fn decrease(&self) -> Option<nat>

open spec fn peek(&self, index: int) -> Option<Self::Item>

{
    match (zip_iter_fst(*self).peek(index), zip_iter_snd(*self).peek(index)) {
        (Some(a), Some(b)) => Some((a, b)),
        _ => None,
    }
}

impl<A: Step> IteratorSpecImpl for Range<A>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ obeys_range_step_spec::<A>() }

open spec fn remaining(&self) -> Seq<Self::Item>

{
    let steps = self.start.spec_steps_between_int(self.end);
    let len = if steps > 0 { steps } else { 0 };
    Seq::new(len as nat, |i: int| self.start.spec_forward_checked_int(i).unwrap())
}

open spec fn produces(&self) -> Seq<bool>

{ Seq::new(IteratorSpec::remaining(self).len(), |i: int| true) }

open spec fn decrease(&self) -> Option<nat>

{ Some(self.start.spec_steps_between_int(self.end) as nat) }

open spec fn peek(&self, index: int) -> Option<Self::Item>

{
    if 0 <= index <= self.start.spec_steps_between_int(self.end) {
        Some(self.start.spec_forward_checked_int(index).unwrap())
    } else {
        None
    }
}

impl<A: Step> IteratorSpecImpl for RangeInclusive<A>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ obeys_range_step_spec::<A>() }

open spec fn remaining(&self) -> Seq<Self::Item>

{
    Seq::new(
        spec_range_inclusive_len(self),
        |i: int| self@.start.spec_forward_checked_int(i).unwrap(),
    )
}

open spec fn produces(&self) -> Seq<bool>

{ Seq::new(IteratorSpec::remaining(self).len(), |i: int| true) }

open spec fn decrease(&self) -> Option<nat>

{ Some(spec_range_inclusive_len(self)) }

open spec fn peek(&self, index: int) -> Option<Self::Item>

{
    if 0 <= index <= spec_range_inclusive_len(self) {
        Some(self@.start.spec_forward_checked_int(index).unwrap())
    } else {
        None
    }
}

impl<B, I, F> IteratorSpecImpl for Map<I, F>

where I: Iterator + IteratorSpec, F: FnMut(I::Item) -> B,

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ map_iter(*self).obeys_prophetic_iter_laws() }

uninterp spec fn remaining(&self) -> Seq<B>

uninterp spec fn produces(&self) -> Seq<bool>

uninterp spec fn decrease(&self) -> Option<nat>

open spec fn peek(&self, index: int) -> Option<B>

{
    match map_iter(*self).peek(index) {
        Some(v) => {
            let x = choose |x| map_fun(*self).ensures((v,), x);
            Some(x)
        }
        None => None,
    }
}

impl<I, P> IteratorSpecImpl for Filter<I, P>

where I: Iterator + IteratorSpec, P: FnMut(&I::Item) -> bool,

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ filter_iter(*self).obeys_prophetic_iter_laws() }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

uninterp spec fn produces(&self) -> Seq<bool>

uninterp spec fn decrease(&self) -> Option<nat>

open spec fn peek(&self, index: int) -> Option<Self::Item>

{ None }

impl<I> IteratorSpecImpl for &mut I

where I: Iterator,

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ <I as IteratorSpec>::obeys_prophetic_iter_laws(*self) }

open spec fn remaining(&self) -> Seq<Self::Item>

{ <I as IteratorSpec>::remaining(*self) }

open spec fn produces(&self) -> Seq<bool>

{ <I as IteratorSpec>::produces(*self) }

open spec fn decrease(&self) -> Option<nat>

{ <I as IteratorSpec>::decrease(*self) }

open spec fn peek(&self, index: int) -> Option<Self::Item>

{ <I as IteratorSpec>::peek(*self, index) }

impl<I> IteratorSpecImpl for Rev<I>

where I: DoubleEndedIterator + DoubleEndedIteratorSpec,

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ rev_iter(*self).obeys_prophetic_iter_laws() }

closed spec fn remaining(&self) -> Seq<Self::Item>

closed spec fn produces(&self) -> Seq<bool>

closed spec fn decrease(&self) -> Option<nat>

open spec fn peek(&self, index: int) -> Option<Self::Item>

{ rev_iter(*self).peek_back(index) }

impl<I> IteratorSpecImpl for Skip<I>

where I: Iterator,

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ skip_iter(*self).obeys_prophetic_iter_laws() }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

uninterp spec fn produces(&self) -> Seq<bool>

uninterp spec fn decrease(&self) -> Option<nat>

open spec fn peek(&self, index: int) -> Option<Self::Item>

{ skip_iter(*self).peek(skip_init_n(*self) + index) }

impl<I> IteratorSpecImpl for Take<I>

where I: Iterator,

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ take_iter(*self).obeys_prophetic_iter_laws() }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

uninterp spec fn produces(&self) -> Seq<bool>

uninterp spec fn decrease(&self) -> Option<nat>

open spec fn peek(&self, index: int) -> Option<Self::Item>

{ take_iter(*self).peek(index) }

impl<K, V, A: Allocator> IteratorSpecImpl for IntoIter<K, V, A>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

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_entries(*self).len() {
        Some(into_iter_entries(*self)[index])
    } else {
        None
    }
}

impl<T, A: Allocator> IteratorSpecImpl for IntoIter<T, A>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

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
    }
}

Implementors