Trait ExIterator 

pub trait ExIterator {
    type ExternalTraitSpecificationFor: Iterator;
    type Item;

    // Required methods
    spec fn obeys_prophetic_iter_laws(&self) -> bool;
    spec fn remaining(&self) -> Seq<Self::Item>;
    spec fn produces(&self) -> Seq<bool>;
    exec fn next(&mut self) -> ret : Option<Self::Item>;
    spec fn decrease(&self) -> Option<nat>;
    spec fn peek(&self, index: int) -> Option<Self::Item>;
    exec fn all<F>(&mut self, f: F) -> r : bool
       where Self: Sized,
             F: FnMut(Self::Item) -> bool;
    exec fn any<F>(&mut self, f: F) -> r : bool
       where Self: Sized,
             F: FnMut(Self::Item) -> bool;
    exec fn collect<B>(self) -> collection : B
       where B: FromIterator<Self::Item>,
             Self: Sized;
    exec fn filter<P>(self, predicate: P) -> r : Filter<Self, P> 
       where Self: Sized,
             P: FnMut(&Self::Item) -> bool;
    exec fn find<P>(&mut self, predicate: P) -> r : Option<Self::Item>
       where Self: Sized,
             P: FnMut(&Self::Item) -> bool;
    exec fn find_map<B, F>(&mut self, f: F) -> r : Option<B>
       where Self: Sized,
             F: FnMut(Self::Item) -> Option<B>;
    exec fn map<B, F>(self, f: F) -> r : Map<Self, F> 
       where Self: Sized,
             F: FnMut(Self::Item) -> B;
    exec fn position<P>(&mut self, predicate: P) -> r : Option<usize>
       where Self: Sized,
             P: FnMut(Self::Item) -> bool;
    exec fn rev(self) -> r : Rev<Self> 
       where Self: Sized;
    exec fn size_hint(&self) -> (usize, Option<usize>);
    exec fn skip(self, n: usize) -> s : Skip<Self> 
       where Self: Sized;
    exec fn take(self, n: usize) -> t : Take<Self> 
       where Self: Sized;
    exec fn zip<U>(self, other: U) -> r : Zip<Self, <U as IntoIterator>::IntoIter> 
       where Self: Sized,
             U: IntoIterator;
}

Required Associated Types

type ExternalTraitSpecificationFor: Iterator

type Item

Required Methods

spec 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.

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

Sequence of all potentially returned items

spec 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 next(&mut self) -> ret : Option<Self::Item>

ensures

iter_state_preserved!(old(self), final(self)),

final(self).obeys_prophetic_iter_laws()
    ==> ({
        if old(self).remaining().len() > 0 {
            &&& final(self).remaining() == old(self).remaining().drop_first()
            &&& final(self).produces() == old(self).produces().drop_first()
            &&& ret == Some(old(self).remaining()[0])
            &&& old(self).produces()[0]

        } else {
            &&& final(self).remaining() == old(self).remaining()
            &&& final(self).produces() == old(self).produces()
            &&& ret == None

        }
    }),

final(self).obeys_prophetic_iter_laws() && old(self).remaining().len() > 0
    && final(self).decrease() is Some
    ==> decreases_to!(old(self).decrease() -> 0 => final(self).decrease() -> 0),

Advances the iterator and returns the next value.

spec 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.

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

exec fn all<F>(&mut self, f: F) -> r : bool

where Self: Sized, F: FnMut(Self::Item) -> bool,

requires

self.obeys_prophetic_iter_laws()
    ==> forall |k| {
        0 <= k < self.remaining().len() && self.produces()[k]
            ==> f.requires((#[trigger] self.remaining()[k],))
    },

!self.obeys_prophetic_iter_laws() ==> forall |x: Self::Item| #[trigger] f.requires((x,)),

ensures

iter_state_preserved!(old(self), final(self)),

final(self).obeys_prophetic_iter_laws()
    ==> {
        let num_consumed = old(self).remaining().len() - final(self).remaining().len();
        &&& final(self).remaining().is_suffix_of(old(self).remaining())
        &&& final(self).produces() == old(self).produces().skip(num_consumed)
        &&& old(self).produces().take(num_consumed).all(|p: bool| p)

    },

final(self).obeys_prophetic_iter_laws() && r
    ==> {
        &&& final(self).remaining().len() == 0
        &&& forall |i| {
            0 <= i < old(self).remaining().len()
                ==> f.ensures((#[trigger] old(self).remaining()[i],), true)
        }

    },

final(self).obeys_prophetic_iter_laws() && !r
    ==> {
        let idx = old(self).remaining().len() - final(self).remaining().len() - 1;
        {
            &&& final(self).remaining().len() < old(self).remaining().len()
            &&& f.ensures((old(self).remaining()[idx],), false)
            &&& forall |i| {
                0 <= i < idx ==> f.ensures((#[trigger] old(self).remaining()[i],), true)
            }

        }
    },

exec fn any<F>(&mut self, f: F) -> r : bool

where Self: Sized, F: FnMut(Self::Item) -> bool,

requires

self.obeys_prophetic_iter_laws()
    ==> forall |k| {
        0 <= k < self.remaining().len() && self.produces()[k]
            ==> f.requires((#[trigger] self.remaining()[k],))
    },

!self.obeys_prophetic_iter_laws() ==> forall |x: Self::Item| #[trigger] f.requires((x,)),

ensures

iter_state_preserved!(old(self), final(self)),

final(self).obeys_prophetic_iter_laws()
    ==> {
        let num_consumed = old(self).remaining().len() - final(self).remaining().len();
        &&& final(self).remaining().is_suffix_of(old(self).remaining())
        &&& final(self).produces() == old(self).produces().skip(num_consumed)
        &&& old(self).produces().take(num_consumed).all(|p: bool| p)

    },

final(self).obeys_prophetic_iter_laws() && !r
    ==> {
        &&& final(self).remaining().len() == 0
        &&& forall |i| {
            0 <= i < old(self).remaining().len()
                ==> f.ensures((#[trigger] old(self).remaining()[i],), false)
        }

    },

final(self).obeys_prophetic_iter_laws() && r
    ==> {
        let idx = old(self).remaining().len() - final(self).remaining().len() - 1;
        {
            &&& final(self).remaining().len() < old(self).remaining().len()
            &&& f.ensures((old(self).remaining()[idx],), true)
            &&& forall |i| {
                0 <= i < idx ==> f.ensures((#[trigger] old(self).remaining()[i],), false)
            }

        }
    },

exec fn collect<B>(self) -> collection : B

where B: FromIterator<Self::Item>, Self: Sized,

ensures

self.obeys_prophetic_iter_laws()
    ==> FromIteratorSpec::from_iter_ensures(
        self.remaining(),
        self.produces(),
        collection,
    ),

exec fn filter<P>(self, predicate: P) -> r : Filter<Self, P>

where Self: Sized, P: FnMut(&Self::Item) -> bool,

requires

self.decrease() is Some,

self.obeys_prophetic_iter_laws()
    ==> forall |k| {
        0 <= k < self.remaining().len() && self.produces()[k]
            ==> predicate.requires((#[trigger] &self.remaining()[k],))
    },

!self.obeys_prophetic_iter_laws()
    ==> forall |x: &Self::Item| #[trigger] predicate.requires((x,)),

ensures

self.obeys_prophetic_iter_laws() ==> filter_post(self, predicate, r),

exec fn find<P>(&mut self, predicate: P) -> r : Option<Self::Item>

where Self: Sized, P: FnMut(&Self::Item) -> bool,

requires

self.obeys_prophetic_iter_laws()
    ==> forall |k| {
        0 <= k < self.remaining().len() && self.produces()[k]
            ==> predicate.requires((#[trigger] &self.remaining()[k],))
    },

!self.obeys_prophetic_iter_laws()
    ==> forall |x: &Self::Item| #[trigger] predicate.requires((x,)),

ensures

iter_state_preserved!(old(self), final(self)),

final(self).obeys_prophetic_iter_laws()
    ==> final(self).produces()
        == old(self)
            .produces()
            .skip(old(self).remaining().len() - final(self).remaining().len()),

final(self).obeys_prophetic_iter_laws()
    ==> {
        &&& final(self).remaining().is_suffix_of(old(self).remaining())
        &&& old(self)
            .produces()
            .take(old(self).remaining().len() - final(self).remaining().len())
            .all(|p: bool| p)

    },

final(self).obeys_prophetic_iter_laws() && r.is_none()
    ==> {
        &&& final(self).remaining().len() == 0
        &&& forall |i| {
            0 <= i < old(self).remaining().len()
                ==> predicate.ensures((#[trigger] &old(self).remaining()[i],), false)
        }

    },

final(self).obeys_prophetic_iter_laws() && r.is_some()
    ==> {
        let idx = old(self).remaining().len() - final(self).remaining().len() - 1;
        {
            &&& 0 <= final(self).remaining().len() < old(self).remaining().len()
            &&& predicate.ensures((&r.unwrap(),), true)
            &&& old(self).remaining()[idx] == r.unwrap()
            &&& forall |i| {
                0 <= i < idx
                    ==> predicate.ensures((#[trigger] &old(self).remaining()[i],), false)
            }

        }
    },

exec fn find_map<B, F>(&mut self, f: F) -> r : Option<B>

where Self: Sized, F: FnMut(Self::Item) -> Option<B>,

requires

self.obeys_prophetic_iter_laws()
    ==> forall |k| {
        0 <= k < self.remaining().len() && self.produces()[k]
            ==> f.requires((#[trigger] self.remaining()[k],))
    },

!self.obeys_prophetic_iter_laws() ==> forall |x: Self::Item| #[trigger] f.requires((x,)),

ensures

iter_state_preserved!(old(self), final(self)),

final(self).obeys_prophetic_iter_laws()
    ==> {
        let num_consumed = old(self).remaining().len() - final(self).remaining().len();
        &&& final(self).remaining().is_suffix_of(old(self).remaining())
        &&& final(self).produces() == old(self).produces().skip(num_consumed)
        &&& old(self).produces().take(num_consumed).all(|p: bool| p)

    },

final(self).obeys_prophetic_iter_laws() && r.is_none()
    ==> {
        &&& final(self).remaining().len() == 0
        &&& forall |i| {
            0 <= i < old(self).remaining().len()
                ==> f.ensures((#[trigger] old(self).remaining()[i],), None)
        }

    },

final(self).obeys_prophetic_iter_laws() && r.is_some()
    ==> {
        let idx = old(self).remaining().len() - final(self).remaining().len() - 1;
        {
            &&& 0 <= final(self).remaining().len() < old(self).remaining().len()
            &&& f.ensures((old(self).remaining()[idx],), r)
            &&& forall |i| {
                0 <= i < idx ==> f.ensures((#[trigger] old(self).remaining()[i],), None)
            }

        }
    },

exec fn map<B, F>(self, f: F) -> r : Map<Self, F>

where Self: Sized, F: FnMut(Self::Item) -> B,

requires

self.obeys_prophetic_iter_laws()
    ==> forall |k| {
        0 <= k < self.remaining().len() && self.produces()[k]
            ==> f.requires((#[trigger] self.remaining()[k],))
    },

!self.obeys_prophetic_iter_laws() ==> forall |x: Self::Item| #[trigger] f.requires((x,)),

ensures

self.obeys_prophetic_iter_laws() ==> map_post(self, f, r),

exec fn position<P>(&mut self, predicate: P) -> r : Option<usize>

where Self: Sized, P: FnMut(Self::Item) -> bool,

requires

self.obeys_prophetic_iter_laws(),

self.remaining().len() <= usize::MAX as int,

forall |k| {
    0 <= k < self.remaining().len() && self.produces()[k]
        ==> predicate.requires((#[trigger] self.remaining()[k],))
},

ensures

iter_state_preserved!(old(self), final(self)),

final(self).obeys_prophetic_iter_laws()
    ==> {
        let num_consumed = old(self).remaining().len() - final(self).remaining().len();
        &&& final(self).remaining().is_suffix_of(old(self).remaining())
        &&& final(self).produces() == old(self).produces().skip(num_consumed)
        &&& old(self).produces().take(num_consumed).all(|p: bool| p)

    },

final(self).obeys_prophetic_iter_laws() && r.is_none()
    ==> {
        &&& final(self).remaining().len() == 0
        &&& forall |i| {
            0 <= i < old(self).remaining().len()
                ==> predicate.ensures((#[trigger] old(self).remaining()[i],), false)
        }

    },

final(self).obeys_prophetic_iter_laws() && r.is_some()
    ==> {
        let index = r.unwrap();
        {
            &&& index as int
                == (old(self).remaining().len() - final(self).remaining().len() - 1)
            &&& 0 <= final(self).remaining().len() < old(self).remaining().len()
            &&& predicate
                .ensures((#[trigger] old(self).remaining()[index as int],), true)
            &&& forall |i| {
                0 <= i < index as int
                    ==> predicate.ensures((#[trigger] old(self).remaining()[i],), false)
            }

        }
    },

exec fn rev(self) -> r : Rev<Self>

where Self: Sized,

ensures

self.obeys_prophetic_iter_laws() ==> rev_post(self, r),

exec fn size_hint(&self) -> (usize, Option<usize>)

ensures

self.obeys_prophetic_iter_laws()
    ==> lower <= self.remaining().len()
        && (upper matches Some(b) ==> self.remaining().len() <= b),

exec fn skip(self, n: usize) -> s : Skip<Self>

where Self: Sized,

ensures

self.obeys_prophetic_iter_laws() ==> skip_post(self, n, s),

exec fn take(self, n: usize) -> t : Take<Self>

where Self: Sized,

ensures

self.obeys_prophetic_iter_laws() ==> take_post(self, n, t),

exec fn zip<U>(self, other: U) -> r : Zip<Self, <U as IntoIterator>::IntoIter>

where Self: Sized, U: IntoIterator,

ensures

self.obeys_prophetic_iter_laws() ==> zip_post(self, other, r),

Dyn Compatibility

This trait is dyn compatible.

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

Implementors