Trait IteratorSpec 

pub trait IteratorSpec: Iterator {
    // Required methods
    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool;
    fn completed(&mut self) -> bool;
    fn produces_refl(self);
    fn produces_trans(
        a: Self,
        ab: Seq<Self::Item>,
        b: Self,
        bc: Seq<Self::Item>,
        c: Self,
    );

    // Provided method
    fn map_inv<B, F>(self, func: F) -> MapInv<Self, F> 
       where Self: Sized,
             F: FnMut(Self::Item, Snapshot<Seq<Self::Item>>) -> B { ... }
}

Required Methods

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(prophetic)

fn completed(&mut self) -> bool

(prophetic)

fn produces_refl(self)

(law)

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

Provided Methods

fn map_inv<B, F>(self, func: F) -> MapInv<Self, F>

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

terminates

ghost

requires

forall<e, i2>
                    self.produces(Seq::singleton(e), i2) ==>
                    func.precondition((e, Snapshot::new(Seq::empty())))

requires

MapInv::<Self, F>::reinitialize()

requires

MapInv::<Self, F>::preservation(self, func)

ensures

result == MapInv { iter: self, func, produced: Snapshot::new(Seq::empty())}

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

impl<'a, I, T> IteratorSpec for Cloned<I>

where I: IteratorSpec<Item = &'a T>, T: Clone + 'a,

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! {
    exists<inner: &mut _> *inner == self.iter() && ^inner == (^self).iter() && inner.completed()
}

fn produces(self, visited: Seq<T>, o: Self) -> bool

(open, prophetic)

pearlite! {
    exists<s: Seq<&'a T>>
           self.iter().produces(s, o.iter())
        && visited.len() == s.len()
        && forall<i> 0 <= i && i < s.len() ==> T::clone.postcondition((s[i],), visited[i])
}

fn produces_refl(self)

(law)

ensures

self.produces(Seq::empty(), self)

fn produces_trans(a: Self, ab: Seq<T>, b: Self, bc: Seq<T>, c: Self)

(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<'a, I, T> IteratorSpec for Copied<I>

where I: IteratorSpec<Item = &'a T>, T: Copy + 'a,

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! {
    exists<inner: &mut _> *inner == self.iter() && ^inner == (^self).iter() && inner.completed()
}

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open, prophetic)

pearlite! {
    exists<s: Seq<&'a T>>
           self.iter().produces(s, o.iter())
        && visited.len() == s.len()
        && forall<i> 0 <= i && i < s.len() ==> visited[i] == *s[i]
}

fn produces_refl(self)

(law)

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<'a, K: DeepModel, V> IteratorSpec for Iter<'a, K, V>

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open, prophetic, inline)

// `self@` equals the union of `visited` (viewed as a finite map) and `o@`
pearlite! {
    self@.len() == visited.len() + o@.len()
    && (forall<k: &K, v: &V> visited.contains((k, v))
        ==> self@.get(k.deep_model()) == Some(*v) && o@.get(k.deep_model()) == None)
    && (forall<k: K::DeepModelTy, v: V> o@.get(k) == Some(v)
        ==> self@.get(k) == Some(v) && !exists<k2: &K, v2: &V> k2.deep_model() == k && visited.contains((k2, v2)))
    && (forall<k: K::DeepModelTy, v: V> self@.get(k) == Some(v)
        ==> (exists<k2: &K> k2.deep_model() == k && visited.contains((k2, &v))) || o@.get(k) == Some(v))
    && (forall<i1, i2>
        0 <= i1 && i1 < visited.len() && 0 <= i2 && i2 < visited.len()
        && visited[i1].0.deep_model() == visited[i2].0.deep_model()
        ==> i1 == i2)
}

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! { resolve(self) && self@.is_empty() }

fn produces_refl(self)

(open, law)

{}

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(open, law)

proof_assert! { forall<i> 0 <= i && i < bc.len() ==> bc[i] == ab.concat(bc)[ab.len() + i] }

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<'a, K: DeepModel, V> IteratorSpec for IterMut<'a, K, V>

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open, prophetic, inline)

// self@ equals the union of visited (viewed as a fmap) and o@
pearlite! {
    self@.len() == visited.len() + o@.len()
    && (forall<k: K, v: &mut V> visited.contains((&k, v))
        ==> self@.get(k.deep_model()) == Some(v) && o@.get(k.deep_model()) == None)
    && (forall<k: K::DeepModelTy, v: &mut V> o@.get(k) == Some(v)
        ==> self@.get(k) == Some(v) && !exists<k2: &K, v2: &mut V> k2.deep_model() == k && visited.contains((k2, v2)))
    && (forall<k: K::DeepModelTy, v: &mut V> self@.get(k) == Some(v)
        ==> (exists<k1: &K> k1.deep_model() == k && visited.contains((k1, v))) || o@.get(k) == Some(v))
    && (forall<i1, i2>
        0 <= i1 && i1 < visited.len() && 0 <= i2 && i2 < visited.len()
        && visited[i1].0.deep_model() == visited[i2].0.deep_model()
        ==> i1 == i2)
}

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! { resolve(self) && self@.is_empty() }

fn produces_refl(self)

(open, law)

{}

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(open, law)

proof_assert! { forall<i> 0 <= i && i < bc.len() ==> bc[i] == ab.concat(bc)[ab.len() + i] }

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

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

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! { resolve(self) && (*self@)@ == Seq::empty() }

fn produces(self, visited: Seq<Self::Item>, tl: Self) -> bool

(open)

pearlite! {
    self@.to_ref_seq() == visited.concat(tl@.to_ref_seq())
}

fn produces_refl(self)

(open, law)

{}

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(open, law)

{}

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

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

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! { resolve(self) && (*self@)@ == Seq::empty() }

fn produces(self, visited: Seq<Self::Item>, tl: Self) -> bool

(open)

pearlite! {
    self@.to_ref_seq() == visited.concat(tl@.to_ref_seq())
}

fn produces_refl(self)

(open, law)

{}

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(open, law)

{}

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<'a, T> IteratorSpec for IterMut<'a, T>

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! { resolve(self) && (*self@)@ == Seq::empty() }

fn produces(self, visited: Seq<Self::Item>, tl: Self) -> bool

(open)

pearlite! {
    self@.to_mut_seq() == visited.concat(tl@.to_mut_seq())
}

fn produces_refl(self)

(open, law)

{}

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(open, law)

{}

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<'a, T: DeepModel> IteratorSpec for Iter<'a, T>

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open, prophetic)

set_produces(self, visited, o)

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! { (self@).is_empty() }

fn produces_refl(self)

(open, law)

{}

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(open, law)

set_produces_trans(a, ab, b, bc, c);

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<'a, T: Eq + Hash + DeepModel, S: BuildHasher> IteratorSpec for Difference<'a, T, S>

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open, prophetic)

set_produces(self, visited, o)

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! { resolve(self) && (self@).is_empty() }

fn produces_refl(self)

(open, law)

{}

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(open, law)

set_produces_trans(a, ab, b, bc, c);

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<'a, T: Eq + Hash + DeepModel, S: BuildHasher> IteratorSpec for Intersection<'a, T, S>

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open, prophetic)

set_produces(self, visited, o)

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! { resolve(self) && (self@).is_empty() }

fn produces_refl(self)

(open, law)

{}

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(open, law)

set_produces_trans(a, ab, b, bc, c);

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<A: IteratorSpec, B: IteratorSpec> IteratorSpec for Zip<A, B>

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! {
    exists<a: &mut A, b: &mut B>
           *a == (*self).itera() && *b == (*self).iterb()
        && ^a == (^self).itera() && ^b == (^self).iterb()
        && (a.completed() && resolve(b)
            || exists<x: A::Item> inv(x) && (*a).produces(Seq::singleton(x), ^a) &&
                                  resolve(x) && (*b).completed())
}

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open, prophetic)

pearlite! {
    // Using an `unzip` definition doesn't work well because of issues related to datatypes and `match`
    exists<p1: Seq<_>, p2: Seq<_>>
           p1.len() == p2.len() && p2.len() == visited.len()
        && (forall<i> 0 <= i && i < visited.len() ==> visited[i] == (p1[i], p2[i]))
        && self.itera().produces(p1, o.itera()) && self.iterb().produces(p2, o.iterb())
}

fn produces_refl(self)

(law)

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<I: DoubleEndedIteratorSpec> IteratorSpec for Rev<I>

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! { self.iter_mut().completed() }

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open, prophetic)

pearlite! {
    self.iter().produces_back(visited, o.iter())
}

fn produces_refl(self)

(law)

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<I: IteratorSpec + ?Sized> IteratorSpec for &mut I

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open, prophetic)

pearlite! { (*self).produces(visited, *o) && ^self == ^o }

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! { (*self).completed() && ^*self == ^^self }

fn produces_refl(self)

(open, law)

{}

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(open, law)

{}

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<I: IteratorSpec> IteratorSpec for Enumerate<I>

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! {
    exists<inner: &mut _> *inner == self.iter() && ^inner == (^self).iter()
        && inner.completed()
        && self.n()@ == (^self).n()@
}

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open, prophetic)

pearlite! {
    visited.len() == o.n()@ - self.n()@
    && exists<s: Seq<I::Item>>
           self.iter().produces(s, o.iter())
        && visited.len() == s.len()
        && forall<i> 0 <= i && i < s.len() ==> visited[i].0@ == self.n()@ + i && visited[i].1 == s[i]
}

fn produces_refl(self)

(law)

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<I: IteratorSpec> IteratorSpec for Fuse<I>

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! {
    (self@ == None || exists<it:&mut I> it.completed() && self@ == Some(*it)) &&
    (^self)@ == None
}

fn produces(self, prod: Seq<Self::Item>, other: Self) -> bool

(open, prophetic)

pearlite! {
    match self@ {
        None => prod == Seq::empty() && other@ == self@,
        Some(i) => match other@ {
            Some(i2) => i.produces(prod, i2),
            None => false,
        },
    }
}

fn produces_refl(self)

(open, law)

{}

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(open, law)

{}

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<I: IteratorSpec> IteratorSpec for Skip<I>

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! {
    (^self).n()@ == 0 &&
    exists<s: Seq<Self::Item>, i: &mut I>
           s.len() <= (*self).n()@
        && self.iter().produces(s, *i)
        && (forall<i> 0 <= i && i < s.len() ==> resolve(s[i]))
        && i.completed()
        && ^i == (^self).iter()
}

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open, prophetic)

pearlite! {
    visited == Seq::empty() && self == o ||
    o.n()@ == 0 && visited.len() > 0 &&
    exists<s: Seq<Self::Item>>
           s.len() == self.n()@
        && self.iter().produces(s.concat(visited), o.iter())
        && forall<i> 0 <= i && i < s.len() ==> resolve(s[i])
}

fn produces_refl(self)

(law)

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<I: IteratorSpec> IteratorSpec for Take<I>

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! {
    self.n()@ == 0 && resolve(self) ||
    (*self).n()@ > 0 && (*self).n()@ == (^self).n()@ + 1 && self.iter_mut().completed()
}

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open, prophetic)

pearlite! {
    self.n()@ == o.n()@ + visited.len() && self.iter().produces(visited, o.iter())
}

fn produces_refl(self)

(law)

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<I: IteratorSpec, B, F: FnMut(I::Item) -> Option<B>> IteratorSpec for FilterMap<I, F>

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! {
    (exists<s: Seq<_>, e: &mut I > self.iter().produces(s, *e) && e.completed() &&
        forall<i> 0 <= i && i < s.len() ==> (*self).func().postcondition_mut((s[i],), (^self).func(), None))
    && (*self).func() == (^self).func()
}

fn produces(self, visited: Seq<Self::Item>, succ: Self) -> bool

(open, prophetic)

pearlite! {
    private_invariant(self) ==>
    self.func().hist_inv(succ.func()) &&
    // f here is a mapping from indices of `visited` to those of `s`, where `s` is the whole sequence produced by the underlying iterator
    // Interestingly, Z3 guesses `f` quite readily but gives up *totally* on `s`. However, the addition of the final assertions on the correctness of the values
    // blocks z3's guess for `f`.
    exists<s: Seq<I::Item>, f: Mapping<Int, Int>> self.iter().produces(s, succ.iter()) &&
        (forall<i> 0 <= i && i < visited.len() ==> 0 <= f.get(i) && f.get(i) < s.len()) &&
        // `f` is a monotone mapping
        (forall<i, j> 0 <= i && i < j && j < visited.len() ==> f.get(i) < f.get(j)) &&
        // `f` points to elements produced in `s` (by the underlying `iter`) for which the predicate `self.func()` returned `Some`.
        (forall<i> 0 <= i && i < visited.len() ==> self.func().postcondition_mut((s[f.get(i)],), self.func(), Some(visited[i]))) &&
        // For other elements not in the image of `f`, the predicate `self.func()` returned `None`.
        (forall<j> 0 <= j && j < s.len()
            ==> (!exists<i> 0 <= i && i < visited.len() && f.get(i) == j) == self.func().postcondition_mut((s[j],), self.func(), None))
}

fn produces_refl(self)

(law)

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<I: IteratorSpec, B, F: FnMut(I::Item) -> B> IteratorSpec for Map<I, F>

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! {
    (exists<inner: &mut _> *inner == self.iter() && ^inner == (^self).iter() && inner.completed())
    && (*self).func() == (^self).func()
}

fn produces(self, visited: Seq<Self::Item>, succ: Self) -> bool

(open, prophetic, inline)

pearlite! {
    self.func().hist_inv(succ.func())
    && exists<fs: Seq<&mut F>> fs.len() == visited.len()
    && exists<s: Seq<I::Item>>
        #[trigger(self.iter().produces(s, succ.iter()))]
        s.len() == visited.len() && self.iter().produces(s, succ.iter())
    && (forall<i> 1 <= i && i < fs.len() ==>  ^fs[i - 1] == *fs[i])
    && if visited.len() == 0 { self.func() == succ.func() }
       else { *fs[0] == self.func() &&  ^fs[visited.len() - 1] == succ.func() }
    && forall<i> 0 <= i && i < visited.len() ==>
         self.func().hist_inv(*fs[i])
         && (*fs[i]).precondition((s[i],))
         && (*fs[i]).postcondition_mut((s[i],), ^fs[i], visited[i])
}

fn produces_refl(self)

(law)

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<I: IteratorSpec, F: FnMut(&I::Item) -> bool> IteratorSpec for Filter<I, F>

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! {
    (exists<s: Seq<_>, e: &mut I > self.iter().produces(s, *e) && e.completed() &&
        forall<i> 0 <= i && i < s.len() ==> (*self).func().postcondition_mut((&s[i],), (^self).func(), false))
    && (*self).func() == (^self).func()
}

fn produces(self, visited: Seq<Self::Item>, succ: Self) -> bool

(open, prophetic)

pearlite! {
    private_invariant(self) ==>
    self.func().hist_inv(succ.func()) &&
    // f here is a mapping from indices of `visited` to those of `s`, where `s` is the whole sequence produced by the underlying iterator
    // Interestingly, Z3 guesses `f` quite readily but gives up *totally* on `s`. However, the addition of the final assertions on the correctness of the values
    // blocks z3's guess for `f`.
    exists<s: Seq<Self::Item>, f: Mapping<Int, Int>> self.iter().produces(s, succ.iter()) &&
        (forall<i> 0 <= i && i < visited.len() ==> 0 <= f.get(i) && f.get(i) < s.len()) &&
        // `f` is a monotone mapping
        (forall<i, j> 0 <= i && i < j && j < visited.len() ==> f.get(i) < f.get(j)) &&
        (forall<i> 0 <= i && i < visited.len() ==> visited[i] == s[f.get(i)]) &&
        (forall<i> 0 <= i &&  i < s.len() ==>
            (exists<j> 0 <= j && j < visited.len() && f.get(j) == i) == self.func().postcondition_mut((&s[i],), self.func(), true))
}

fn produces_refl(self)

(law)

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<Idx: DeepModel<DeepModelTy = Int> + Step> IteratorSpec for Range<Idx>

Available on crate feature nightly only.

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! {
    resolve(self) && self.start.deep_model() >= self.end.deep_model()
}

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open)

pearlite! {
    self.end == o.end && self.start.deep_model() <= o.start.deep_model()
    && (visited.len() > 0 ==> o.start.deep_model() <= o.end.deep_model())
    && visited.len() == o.start.deep_model() - self.start.deep_model()
    && forall<i> 0 <= i && i < visited.len() ==>
        visited[i].deep_model() == self.start.deep_model() + i
}

fn produces_refl(self)

(law)

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<Idx: DeepModel<DeepModelTy = Int> + Step> IteratorSpec for RangeInclusive<Idx>

Available on crate feature nightly only.

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! {
    self.is_empty_log() && (^self).is_empty_log()
}

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open)

pearlite! {
    visited.len() == range_inclusive_len(self) - range_inclusive_len(o) &&
    (self.is_empty_log() ==> o.is_empty_log()) &&
    (o.is_empty_log() || self.end_log() == o.end_log()) &&
    forall<i> 0 <= i && i < visited.len() ==>
        visited[i].deep_model() == self.start_log().deep_model() + i
}

fn produces_refl(self)

(open, law)

{}

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(open, law)

{}

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<K: DeepModel, V> IteratorSpec for IntoIter<K, V>

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open, prophetic, inline)

// self@ equals the union of visited (viewed as a fmap) and o@
pearlite! {
    self@.len() == visited.len() + o@.len()
    && (forall<k: K, v: V> visited.contains((k, v))
        ==> self@.get(k.deep_model()) == Some(v) && o@.get(k.deep_model()) == None)
    && (forall<k: K::DeepModelTy, v: V> o@.get(k) == Some(v)
        ==> self@.get(k) == Some(v) && !exists<k2: K, v2: V> k2.deep_model() == k && visited.contains((k2, v2)))
    && (forall<k: K::DeepModelTy, v: V> self@.get(k) == Some(v)
        ==> (exists<k1: K> k1.deep_model() == k && visited.contains((k1, v))) || o@.get(k) == Some(v))
    && (forall<i1, i2>
        0 <= i1 && i1 < visited.len() && 0 <= i2 && i2 < visited.len()
        && visited[i1].0.deep_model() == visited[i2].0.deep_model()
        ==> i1 == i2)
}

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! { resolve(self) && self@.is_empty() }

fn produces_refl(self)

(open, law)

{}

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(open, law)

proof_assert! { forall<i> 0 <= i && i < bc.len() ==> bc[i] == ab.concat(bc)[ab.len() + i] }

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<T> IteratorSpec for Empty<T>

fn completed(&mut self) -> bool

(open, prophetic)

resolve(self)

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open)

pearlite! { visited == Seq::empty() && self == o }

fn produces_refl(self)

(law)

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<T> IteratorSpec for Once<T>

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! { (*self)@ == None && resolve(self) }

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open, prophetic)

pearlite! {
    visited == Seq::empty() && self == o ||
    exists<e: Self::Item> self@ == Some(e) && visited == Seq::singleton(e) && o@ == None
}

fn produces_refl(self)

(law)

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<T> IteratorSpec for IntoIter<T>

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! { (*self)@ == None && resolve(self) }

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open)

pearlite! {
    visited == Seq::empty() && self == o ||
    exists<e: Self::Item> self@ == Some(e) && visited == Seq::singleton(e) && o@ == None
}

fn produces_refl(self)

(law)

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<T> IteratorSpec for Iter<'_, T>

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! { (*self)@ == None && resolve(self) }

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open)

pearlite! {
    visited == Seq::empty() && self == o ||
    exists<e: Self::Item> self@ == Some(e) && visited == Seq::singleton(e) && o@ == None
}

fn produces_refl(self)

(law)

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<T> IteratorSpec for IterMut<'_, T>

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! { (*self)@ == None && resolve(self) }

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open)

pearlite! {
    visited == Seq::empty() && self == o ||
    exists<e: Self::Item> self@ == Some(e) && visited == Seq::singleton(e) && o@ == None
}

fn produces_refl(self)

(law)

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

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

Available on crate feature nightly only.

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! { resolve(self) && self@ == Seq::empty() }

fn produces(self, visited: Seq<T>, rhs: Self) -> bool

(open)

pearlite! {
    self@ == visited.concat(rhs@)
}

fn produces_refl(self)

(open, law)

{}

ensures

self.produces(Seq::empty(), self)

fn produces_trans(a: Self, ab: Seq<T>, b: Self, bc: Seq<T>, c: Self)

(open, law)

{}

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<T, const N: usize> IteratorSpec for IntoIter<T, N>

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open, prophetic)

pearlite! { self@ == visited.concat(o@) }

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! { resolve(self) && self@ == Seq::empty() }

fn produces_refl(self)

(open, law)

{}

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(open, law)

{}

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<T: DeepModel> IteratorSpec for IntoIter<T>

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open, prophetic)

set_produces(self, visited, o)

fn completed(&mut self) -> bool

(open, prophetic)

pearlite! { (self@).is_empty() }

fn produces_refl(self)

(open, law)

{}

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(open, law)

set_produces_trans(a, ab, b, bc, c);

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<T: Clone> IteratorSpec for Repeat<T>

fn completed(&mut self) -> bool

(open)

pearlite! { false }

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

(open)

pearlite! {
    self == o &&
    forall<i> 0 <= i && i < visited.len() ==> T::clone.postcondition((&self@,), visited[i])
}

fn produces_refl(self)

(law)

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

Implementors

impl<'a, T> IteratorSpec for SeqIterRef<'a, T>

impl<I: IteratorSpec, B, F: FnMut(I::Item, Snapshot<Seq<I::Item>>) -> B> IteratorSpec for MapInv<I, F>

impl<T> IteratorSpec for SeqIter<T>