vstd/std_specs/
iter.rs

1use super::super::prelude::*;
2use super::super::seq::{
3    group_seq_lemmas, lemma_seq_empty, lemma_seq_subrange_index, lemma_seq_subrange_len,
4};
5use core::iter::{Filter, FromIterator, Iterator, Rev, Skip, Take, Zip};
6
7use verus as verus_skip_verusfmt;
8verus_skip_verusfmt! {
9
10#[verifier::external_trait_specification]
11#[verifier::external_trait_extension(IteratorSpec via IteratorSpecImpl)]
12pub trait ExIterator {
13    type ExternalTraitSpecificationFor: Iterator;
14
15    type Item;
16
17    /// This iterator obeys the specifications below on `next`,
18    /// expressed in terms of prophetic spec functions.
19    /// Only iterators that terminate (i.e., eventually return None
20    /// and then continue to return None) should use this interface.
21    spec fn obeys_prophetic_iter_laws(&self) -> bool;
22
23    /// Sequence of items that will (eventually) be returned
24    #[verifier::prophetic]
25    spec fn remaining(&self) -> Seq<Self::Item>;
26
27    /// Does this iterator complete with a `None` after the above sequence?
28    /// (As opposed to hanging indefinitely on a `next()` call)
29    /// Trivially true for most iterators but important for iterators
30    /// that apply an exec closure that may not terminate.
31    #[verifier::prophetic]
32    spec fn will_return_none(&self) -> bool;
33
34    /// Advances the iterator and returns the next value.
35    fn next(&mut self) -> (ret: Option<Self::Item>)
36        ensures
37            // The iterator consistently obeys, completes, and decreases throughout its lifetime
38            final(self).obeys_prophetic_iter_laws() == old(self).obeys_prophetic_iter_laws(),
39            final(self).obeys_prophetic_iter_laws() ==> final(self).will_return_none() == old(self).will_return_none(),
40            final(self).obeys_prophetic_iter_laws() ==> (old(self).decrease() is Some <==> final(self).decrease() is Some),
41            // `next` pops the head of the prophesized remaining(), or returns None
42            final(self).obeys_prophetic_iter_laws() ==>
43            ({
44                if old(self).remaining().len() > 0 {
45                    &&& final(self).remaining() == old(self).remaining().drop_first()
46                    &&& ret == Some(old(self).remaining()[0])
47                } else {
48                    final(self).remaining() == old(self).remaining() && ret == None && final(self).will_return_none()
49                }
50            }),
51            // If the iterator isn't done yet, then it successfully decreases its metric (if any)
52            final(self).obeys_prophetic_iter_laws() && old(self).remaining().len() > 0 && final(self).decrease() is Some ==>
53                decreases_to!(old(self).decrease()->0 => final(self).decrease()->0),
54    ;
55
56    /******* Mechanisms that support ergonomic `for` loops *********/
57
58    /// Value used by default for the decreases clause when no explicit decreases clause is provided
59    /// (the user can override this with an explicit decreases clause).
60    /// If there's no appropriate metric to decrease, this can return None,
61    /// and the user will have to provide an explicit decreases clause.
62    spec fn decrease(&self) -> Option<nat>;
63
64    // If we can make a useful guess as to what the i-th value will be, return it.
65    // Otherwise, return None.
66    spec fn peek(&self, index: int) -> Option<Self::Item>;
67
68
69
70    /******* Provided methods (in alphabetical order) *********/
71    // For provided method that returns a new iterator (e.g., filter, map, or zip),
72    // ideally we would write their postconditions here.  However, this requires
73    // a trait bound of `Self: IteratorSpec`, which introduces a cyclic dependency.
74    // Hence, we introduce a layer of indirection via an uninterp spec function that
75    // describes the postconditions.
76
77    // TODO: The Rust implementations of `all` and `any` depend on a correct implementation of `try_fold`
78    //       For now, we assume obeys_prophetic_iter_laws() entails such an implementation, but we should
79    //       eventually constrain implementations of `try_fold` to actually be correct enough to uphold the specs below.
80
81    fn all<F>(&mut self, f: F) -> (r: bool)
82        where Self: Sized,
83            F: FnMut(Self::Item) -> bool
84        requires
85            forall |k| #![auto] 0 <= k < self.remaining().len() ==> call_requires(f, (self.remaining()[k], )),
86        ensures
87            // The iterator consistently obeys, completes, and decreases throughout its lifetime
88            final(self).obeys_prophetic_iter_laws() == old(self).obeys_prophetic_iter_laws(),
89            final(self).obeys_prophetic_iter_laws() ==> final(self).will_return_none() == old(self).will_return_none(),
90            final(self).obeys_prophetic_iter_laws() ==> (old(self).decrease() is Some <==> final(self).decrease() is Some),
91            final(self).obeys_prophetic_iter_laws() ==> {
92                final(self).remaining().is_suffix_of(old(self).remaining())
93            },
94            // If all returns true, then the iterator has no remaining elements,
95            // and the predicate was true for all of the original iterator's elements.
96            final(self).obeys_prophetic_iter_laws() && r ==> {
97                &&& final(self).remaining().len() == 0
98                &&& forall |i| 0 <= i < old(self).remaining().len() ==>
99                    f.ensures((#[trigger] old(self).remaining()[i],), true)
100            },
101            // If all returns false, then there is some element for which the
102            // predicate was false, and all previous elements satisfied the predicate.
103            final(self).obeys_prophetic_iter_laws() && !r ==> {
104                let idx = old(self).remaining().len() - final(self).remaining().len() - 1;
105                {
106                    // The failing element was consumed, so the remaining sequence strictly shrank
107                    &&& final(self).remaining().len() < old(self).remaining().len()
108                    &&& f.ensures((old(self).remaining()[idx],), false)
109                    &&& forall |i| 0 <= i < idx ==>
110                        f.ensures((#[trigger] old(self).remaining()[i],), true)
111                }
112            };
113
114    fn any<F>(&mut self, f: F) -> (r: bool)
115        where Self: Sized,
116            F: FnMut(Self::Item) -> bool
117        requires
118            forall |k| #![auto] 0 <= k < self.remaining().len() ==> call_requires(f, (self.remaining()[k], )),
119        ensures
120            // The iterator consistently obeys, completes, and decreases throughout its lifetime
121            final(self).obeys_prophetic_iter_laws() == old(self).obeys_prophetic_iter_laws(),
122            final(self).obeys_prophetic_iter_laws() ==> final(self).will_return_none() == old(self).will_return_none(),
123            final(self).obeys_prophetic_iter_laws() ==> (old(self).decrease() is Some <==> final(self).decrease() is Some),
124            final(self).obeys_prophetic_iter_laws() ==> {
125                final(self).remaining().is_suffix_of(old(self).remaining())
126            },
127            // If any returns false, then the iterator has no remaining elements,
128            // and the predicate was false for all of the original iterator's elements.
129            final(self).obeys_prophetic_iter_laws() && !r ==> {
130                &&& final(self).remaining().len() == 0
131                &&& forall |i| 0 <= i < old(self).remaining().len() ==>
132                    f.ensures((#[trigger] old(self).remaining()[i],), false)
133            },
134            // If any returns true, then there is some element that satisfied the predicate,
135            // and all previous elements did not satisfy the predicate.
136            final(self).obeys_prophetic_iter_laws() && r ==> {
137                let idx = old(self).remaining().len() - final(self).remaining().len() - 1;
138                {
139                    // The satisfying element was consumed, so the remaining sequence strictly shrank
140                    &&& final(self).remaining().len() < old(self).remaining().len()
141                    &&& f.ensures((old(self).remaining()[idx],), true)
142                    &&& forall |i| 0 <= i < idx ==>
143                        f.ensures((#[trigger] old(self).remaining()[i],), false)
144                }
145            };
146
147    fn collect<B>(self) -> (collection: B)
148        where
149            B: FromIterator<Self::Item>,
150            Self: Sized,
151        ensures
152            self.obeys_prophetic_iter_laws() ==>
153                self.will_return_none() &&
154                FromIteratorSpec::from_iter_ensures(self.remaining(), collection),
155    ;
156
157    fn filter<P>(self, predicate: P) -> (r: core::iter::Filter<Self, P>)
158        where
159            Self: Sized,
160            P: FnMut(&Self::Item) -> bool,
161        requires
162            self.obeys_prophetic_iter_laws(),
163            // `filter`'s implementation loops over the inner iterator until the predicate accepts an element,
164            // so it needs a decreases metric to prove termination.
165            self.decrease() is Some,
166            forall |k| #![auto] 0 <= k < self.remaining().len() ==> call_requires(predicate, (&self.remaining()[k], )),
167        ensures
168            self.obeys_prophetic_iter_laws() ==> filter_post(self, predicate, r),
169    ;
170
171    fn find<P>(&mut self, predicate: P) -> (r: Option<Self::Item>)
172        where Self: Sized,
173            P: FnMut(&Self::Item) -> bool
174        requires
175            forall |k| #![auto] 0 <= k < self.remaining().len() ==> call_requires(predicate, (&self.remaining()[k], )),
176        ensures
177            // The iterator consistently obeys, completes, and decreases throughout its lifetime
178            final(self).obeys_prophetic_iter_laws() == old(self).obeys_prophetic_iter_laws(),
179            final(self).obeys_prophetic_iter_laws() ==> final(self).will_return_none() == old(self).will_return_none(),
180            final(self).obeys_prophetic_iter_laws() ==> (old(self).decrease() is Some <==> final(self).decrease() is Some),
181            final(self).obeys_prophetic_iter_laws() ==> {
182                final(self).remaining().is_suffix_of(old(self).remaining())
183            },
184            // If find returns None, then the iterator has no remaining
185            // elements, and the predicate was false for all of the original
186            // iterator's elements.
187            final(self).obeys_prophetic_iter_laws() && r.is_none() ==> {
188                &&& final(self).remaining().len() == 0
189                &&& forall |i| 0 <= i < old(self).remaining().len() ==>
190                    predicate.ensures((#[trigger]&old(self).remaining()[i],), false)
191            },
192            // If find returns Some, then the returned value satisfies the
193            // predicate, and all previous elements did not satisfy the
194            // predicate.
195            final(self).obeys_prophetic_iter_laws() && r.is_some() ==> {
196                let idx = old(self).remaining().len() - final(self).remaining().len() - 1;
197                {
198                    &&& 0 <= final(self).remaining().len() < old(self).remaining().len()
199                    &&& predicate.ensures((&r.unwrap(),), true)
200                    &&& old(self).remaining()[idx] == r.unwrap()
201                    &&& forall |i| 0 <= i < idx ==>
202                        predicate.ensures((#[trigger] &old(self).remaining()[i],), false)
203                }
204            };
205
206    fn map<B, F>(self, f: F) -> (r: core::iter::Map<Self, F>)
207        where
208            Self: Sized,
209            F: FnMut(Self::Item) -> B,
210        requires
211            self.obeys_prophetic_iter_laws(),
212            forall |k| #![auto] 0 <= k < self.remaining().len() ==> call_requires(f, (self.remaining()[k], )),
213        ensures
214            self.obeys_prophetic_iter_laws() ==> map_post(self, f, r),
215    ;
216
217    fn rev(self) -> (r: Rev<Self>)
218        where Self: Sized,
219        ensures
220            self.obeys_prophetic_iter_laws() ==> rev_post(self, r),
221    ;
222
223    fn skip(self, n: usize) -> (s: Skip<Self>)
224        where Self: Sized,
225        ensures
226            self.obeys_prophetic_iter_laws() ==> skip_post(self, n, s),
227    ;
228
229    fn take(self, n: usize) -> (t: Take<Self>)
230        where Self: Sized,
231        ensures
232            self.obeys_prophetic_iter_laws() ==> take_post(self, n, t),
233    ;
234
235    #[verifier::impls_cannot_extend_spec]
236    fn zip<U>(self, other: U) -> (r: Zip<Self, <U as IntoIterator>::IntoIter>)
237        where
238            Self: Sized,
239            U: IntoIterator,
240        ensures
241            self.obeys_prophetic_iter_laws() ==> zip_post(self, other, r),
242    ;
243}
244
245#[verifier::external_trait_specification]
246#[verifier::external_trait_extension(DoubleEndedIteratorSpec via DoubleEndedIteratorSpecImpl)]
247pub trait ExDoubleEndedIterator : Iterator {
248    type ExternalTraitSpecificationFor: DoubleEndedIterator;
249
250    // In the specs below, we write out the type parameters explicitly, rather than using the more concise form,
251    // e.g., `final(self).obeys_prophetic_iter_laws()`.  If we use the latter, then Rust elaborates it to
252    // `(&final(self)).obeys_prophetic_iter_laws()`, which means the type of the argument is `& &mut Self`,
253    // which means the type argument inferred for `obeys_prophetic_iter_laws` is `&mut Self`.
254    // This happens because of the existing Rust [trait impl](https://doc.rust-lang.org/std/iter/trait.Iterator.html#impl-Iterator-for-%26mut+I):
255    // ```
256    // impl<I> Iterator for &mut I
257    // where
258    //     I: Iterator + ?Sized,[4:21 AM]
259    // ```
260    fn next_back(&mut self) -> (ret: Option<<Self as core::iter::Iterator>::Item>)
261        ensures
262            // The iterator consistently obeys, completes, and decreases throughout its lifetime
263            <Self as IteratorSpec>::obeys_prophetic_iter_laws(final(self)) == <Self as IteratorSpec>::obeys_prophetic_iter_laws(old(self)),
264            <Self as IteratorSpec>::obeys_prophetic_iter_laws(final(self)) ==> <Self as IteratorSpec>::will_return_none(final(self)) == <Self as IteratorSpec>::will_return_none(old(self)),
265            <Self as IteratorSpec>::obeys_prophetic_iter_laws(final(self)) ==> (<Self as IteratorSpec>::decrease(old(self)) is Some <==> <Self as IteratorSpec>::decrease(final(self)) is Some),
266            // `next` pops the tail of the prophesized remaining(), or returns None
267            <Self as IteratorSpec>::obeys_prophetic_iter_laws(final(self)) ==>
268            ({
269                if <Self as IteratorSpec>::remaining(old(self)).len() > 0 {
270                    <Self as IteratorSpec>::remaining(final(self)) == <Self as IteratorSpec>::remaining(old(self)).drop_last()
271                        && ret == Some(<Self as IteratorSpec>::remaining(old(self)).last())
272                } else {
273                    <Self as IteratorSpec>::remaining(final(self)) == <Self as IteratorSpec>::remaining(old(self)) && ret == None && <Self as IteratorSpec>::will_return_none(final(self))
274                }
275            }),
276            // If the iterator isn't done yet, then it successfully decreases its metric (if any)
277            <Self as IteratorSpec>::obeys_prophetic_iter_laws(final(self)) && <Self as IteratorSpec>::remaining(old(self)).len() > 0 && <Self as IteratorSpec>::decrease(final(self)) is Some ==>
278                <Self as IteratorSpec>::decrease(old(self))->0 > <Self as IteratorSpec>::decrease(final(self))->0,
279    ;
280
281    /******* Mechanisms that support ergonomic `for` loops *********/
282
283    // If we can make a useful guess as to what the i-th value from the back will be, return it.
284    // Otherwise, return None.
285    spec fn peek_back(&self, index: int) -> Option<Self::Item>;
286}
287
288#[verifier::external_trait_specification]
289#[verifier::external_trait_extension(ExactSizeIteratorSpec via ExactSizeIteratorSpecImpl)]
290pub trait ExExactSizeIterator: Iterator {
291    type ExternalTraitSpecificationFor: ExactSizeIterator;
292
293    // An `ExactSizeIterator` can specify its length non-prophetically,
294    // i.e., without using `self.remaining().len()`.
295    spec fn exact_len(&self) -> usize;
296
297    fn len(&self) -> (len: usize)
298        ensures
299            self.obeys_prophetic_iter_laws() ==> len == self.exact_len() == self.remaining().len();
300}
301
302/********************************************************************************
303 * Definitions for `IntoIterator` and `FromIterator``
304 ********************************************************************************/
305#[verifier::external_trait_specification]
306pub trait ExIntoIterator {
307    type ExternalTraitSpecificationFor: core::iter::IntoIterator;
308
309    type Item;
310    type IntoIter: Iterator<Item = Self::Item>;
311
312    fn into_iter(self) -> Self::IntoIter;
313}
314
315pub open spec fn iter_into_iter_spec<I: Iterator>(i: I) -> I {
316    i
317}
318
319#[verifier::when_used_as_spec(iter_into_iter_spec)]
320pub assume_specification<I: Iterator>[ <I as IntoIterator>::into_iter ](i: I) -> (r: I)
321    ensures
322        r == i,
323;
324
325// Uninterpreted function representing the sequence of elements that will be
326// produced by the iterator obtained from an IntoIterator value.
327// This avoids requiring IteratorSpec bounds in from_iter's ensures clause.
328pub uninterp spec fn into_iter_remaining<A, T>(iter: T) -> Seq<A>;
329
330// Connects into_iter_remaining to remaining() for types implementing Iterator + IteratorSpec.
331// This allows callers of from_iter to relate the result to the iterator's remaining elements.
332pub broadcast axiom fn axiom_from_iterator_ensures<A, I: Iterator<Item = A> + IteratorSpec>(iter: I)
333    ensures
334        #[trigger] into_iter_remaining::<A, I>(iter) == iter.remaining(),
335;
336
337#[verifier::external_trait_specification]
338#[verifier::external_trait_extension(FromIteratorSpec via FromIteratorSpecImpl)]
339pub trait ExFromIterator<A>: Sized {
340    type ExternalTraitSpecificationFor: FromIterator<A>;
341
342    spec fn from_iter_ensures(remaining: Seq<A>, s: Self) -> bool;
343
344    #[verifier::impls_cannot_extend_spec]
345    fn from_iter<T>(iter: T) -> (s: Self)
346       where T: IntoIterator<Item = A>
347        ensures
348            Self::from_iter_ensures(into_iter_remaining(iter), s),
349    ;
350}
351
352/********************************************************************************
353 * Definitions for `&mut I`
354 ********************************************************************************/
355// Forwarding spec impl for the Rust-supplied blanket `impl<I> Iterator for &mut I`.
356// Without this, bare method-call syntax on a `i: &mut I` receiver (e.g. `i.remaining()`)
357// resolves to these (otherwise uninterpreted) functions on `&mut I` rather than on `I`,
358// silently disconnecting clients from `I`'s actual specs.
359impl <I> IteratorSpecImpl for &mut I
360    where I: Iterator {
361    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
362        <I as IteratorSpec>::obeys_prophetic_iter_laws(*self)
363    }
364
365    #[verifier::prophetic]
366    open spec fn remaining(&self) -> Seq<Self::Item> {
367        <I as IteratorSpec>::remaining(*self)
368    }
369
370    #[verifier::prophetic]
371    open spec fn will_return_none(&self) -> bool {
372        <I as IteratorSpec>::will_return_none(*self)
373    }
374
375    open spec fn decrease(&self) -> Option<nat> {
376        <I as IteratorSpec>::decrease(*self)
377    }
378
379    open spec fn peek(&self, index: int) -> Option<Self::Item> {
380        <I as IteratorSpec>::peek(*self, index)
381    }
382}
383
384/********************************************************************************
385 * Definitions for `filter()`
386 ********************************************************************************/
387#[verifier::external_body]
388#[verifier::external_type_specification]
389#[verifier::reject_recursive_types(I)]
390#[verifier::reject_recursive_types(F)]
391pub struct ExFilter<I, F>(Filter<I, F>);
392
393// Ghost accessor for the inner iterator
394pub uninterp spec fn filter_iter<I, F>(r: Filter<I, F>) -> I;
395
396// Ghost accessor for the inner predicate
397pub uninterp spec fn filter_fun<I, F>(r: Filter<I, F>) -> F;
398
399// Ghost accessor for the sequence of predicate decisions made for the (prefix of) the
400// inner iterator's elements
401#[verifier::prophetic]
402pub uninterp spec fn filter_keep<I, F>(r: Filter<I, F>) -> Seq<bool>;
403
404// Define Iter::filter's postcondition
405pub uninterp spec fn filter_post<I, F>(i: I, f: F, r: Filter<I, F>) -> bool;
406
407pub broadcast axiom fn filter_postcondition<I, F>(i: I, f: F, r: core::iter::Filter<I, F>)
408    where
409        I: IteratorSpec,
410        F: FnMut(&I::Item) -> bool,
411    requires
412        i.obeys_prophetic_iter_laws(),
413        i.decrease() is Some,
414        forall |k| #![auto] 0 <= k < i.remaining().len() ==> call_requires(f, (&i.remaining()[k], )),
415        #[trigger] filter_post(i, f, r),
416    ensures
417        {
418            let keep = filter_keep(r);
419            {
420            // `keep` records, for each inspected inner element, the predicate's decision
421            &&& keep.len() <= i.remaining().len()
422            &&& forall |j| 0 <= j < keep.len() ==> call_ensures(f, (&i.remaining()[j],), #[trigger] keep[j])
423            // Completeness: Every inner element the predicate keeps is retained and in order.
424            &&& IteratorSpec::remaining(&r) == i.remaining()[..keep.len()].filter_index(|j: int| keep[j])
425            // The two facts below follow from the `filter_index` above; we expose them directly for convenience.
426            &&& IteratorSpec::remaining(&r).len() <= i.remaining().len()
427            &&& forall |k| #![trigger IteratorSpec::remaining(&r)[k]] 0 <= k < IteratorSpec::remaining(&r).len() ==>
428                    exists |j| 0 <= j < i.remaining().len()
429                        && IteratorSpec::remaining(&r)[k] == #[trigger] i.remaining()[j]
430                        && call_ensures(f, (&i.remaining()[j],), true)
431            &&& IteratorSpec::will_return_none(&r) ==> i.will_return_none() && keep.len() == i.remaining().len()
432            &&& IteratorSpec::decrease(&r) is Some == i.decrease() is Some
433            &&& filter_iter(r) == i
434            &&& filter_fun(r) == f
435            }
436        },
437;
438
439// See examples/iterators/map_and_filter.rs for a verified version of this interface.
440// Any changes here should first be verified over there.
441impl <I, P> IteratorSpecImpl for core::iter::Filter<I, P>
442    where
443        I: Iterator + IteratorSpec,
444        P: FnMut(&I::Item) -> bool,
445{
446    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
447        filter_iter(*self).obeys_prophetic_iter_laws()
448    }
449
450    #[verifier::prophetic]
451    uninterp spec fn remaining(&self) -> Seq<Self::Item>;
452
453    #[verifier::prophetic]
454    uninterp spec fn will_return_none(&self) -> bool;
455
456    uninterp spec fn decrease(&self) -> Option<nat>;
457
458    // `filter` cannot make a useful static guess about which element will be returned at a given index,
459    // since that depends on prophetic evaluations of the predicate.
460    open spec fn peek(&self, index: int) -> Option<Self::Item> {
461        None
462    }
463}
464
465/********************************************************************************
466 * Definitions for `map()`
467 ********************************************************************************/
468#[verifier::external_body]
469#[verifier::external_type_specification]
470#[verifier::reject_recursive_types(I)]
471#[verifier::reject_recursive_types(F)]
472pub struct ExMap<I, F>(core::iter::Map<I, F>);
473
474// Ghost accessor for the inner iterator
475pub uninterp spec fn map_iter<I, F>(r: core::iter::Map<I, F>) -> I;
476
477// Ghost accessor for the inner function
478pub uninterp spec fn map_fun<I, F>(r: core::iter::Map<I, F>) -> F;
479
480// Define Iter::map's postcondition
481pub uninterp spec fn map_post<I, F>(i: I, f: F, r: core::iter::Map<I, F>) -> bool;
482
483pub broadcast axiom fn map_postcondition<I, F>(i: I, f: F, r: core::iter::Map<I, F>)
484    where
485        I: IteratorSpec,
486        F: FnMut<(I::Item,)>,
487    requires
488        i.obeys_prophetic_iter_laws(),
489        #[trigger] map_post(i, f, r),
490    ensures
491        IteratorSpec::remaining(&r).len() <= i.remaining().len(),
492        forall |k| #![auto] 0 <= k < IteratorSpec::remaining(&r).len() ==> call_ensures(f, (i.remaining()[k],), IteratorSpec::remaining(&r)[k]),
493        IteratorSpec::will_return_none(&r) ==> i.will_return_none() && IteratorSpec::remaining(&r).len() == i.remaining().len(),
494        IteratorSpec::decrease(&r) is Some == i.decrease() is Some,
495        map_iter(r) == i,
496        map_fun(r) == f,
497;
498
499// See examples/iterators/map_and_filter.rs for a verified version of this interface.
500// Any changes here should first be verified over there.
501impl <B, I, F> IteratorSpecImpl for core::iter::Map<I, F>
502    where
503        I: Iterator + IteratorSpec,
504        F: FnMut(I::Item) -> B,
505{
506
507    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
508        map_iter(*self).obeys_prophetic_iter_laws()
509    }
510
511    #[verifier::prophetic]
512    uninterp spec fn remaining(&self) -> Seq<B>;
513
514    #[verifier::prophetic]
515    uninterp spec fn will_return_none(&self) -> bool;
516
517    uninterp spec fn decrease(&self) -> Option<nat>;
518
519    open spec fn peek(&self, index: int) -> Option<B> {
520        match map_iter(*self).peek(index) {
521            Some(v) => {
522                let x = choose |x| map_fun(*self).ensures((v,), x);
523                Some(x)
524            }
525            None => None,
526        }
527    }
528}
529
530impl <B, I, F> DoubleEndedIteratorSpecImpl for core::iter::Map<I, F>
531    where I: DoubleEndedIterator + IteratorSpec,
532          F: FnMut(I::Item) -> B,
533{
534    open spec fn peek_back(&self, index: int) -> Option<B> {
535        match map_iter(*self).peek_back(index) {
536            Some(v) => {
537                let x = choose |x| map_fun(*self).ensures((v,), x);
538                Some(x)
539            }
540            None => None,
541        }
542    }
543}
544
545/********************************************************************************
546 * Definitions for `rev()`
547 ********************************************************************************/
548#[verifier::external_body]
549#[verifier::external_type_specification]
550#[verifier::reject_recursive_types(I)]
551pub struct ExRev<I>(Rev<I>);
552
553// Ghost accessor for the inner iterator
554pub uninterp spec fn rev_iter<I>(r: Rev<I>) -> I;
555
556// Define Iter::rev's postcondition
557pub uninterp spec fn rev_post<I>(i: I, r: Rev<I>) -> bool;
558
559pub broadcast axiom fn rev_postcondition<I: DoubleEndedIteratorSpec>(i: I, r: Rev<I>)
560    requires
561        #[trigger] rev_post(i, r),
562    ensures
563        IteratorSpec::remaining(&r) == IteratorSpec::remaining(&i).reverse(),
564        IteratorSpec::will_return_none(&r) == i.will_return_none(),
565        IteratorSpec::decrease(&r) is Some == i.decrease() is Some,
566;
567
568impl <I> IteratorSpecImpl for Rev<I>
569    where I: DoubleEndedIterator + DoubleEndedIteratorSpec {
570    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
571        rev_iter(*self).obeys_prophetic_iter_laws()
572    }
573
574    #[verifier::prophetic]
575    closed spec fn remaining(&self) -> Seq<Self::Item> {
576        rev_iter(*self).remaining().reverse()
577    }
578
579    #[verifier::prophetic]
580    closed spec fn will_return_none(&self) -> bool {
581        rev_iter(*self).will_return_none()
582    }
583
584    closed spec fn decrease(&self) -> Option<nat> {
585        rev_iter(*self).decrease()
586    }
587
588    open spec fn peek(&self, index: int) -> Option<Self::Item> {
589        rev_iter(*self).peek_back(index)
590    }
591}
592
593impl <I> DoubleEndedIteratorSpecImpl for Rev<I>
594    where I: DoubleEndedIterator + IteratorSpec {
595
596    open spec fn peek_back(&self, index: int) -> Option<Self::Item> {
597        rev_iter(*self).peek(index)
598    }
599}
600
601/********************************************************************************
602 * Definitions for `skip()`
603 ********************************************************************************/
604#[verifier::external_body]
605#[verifier::external_type_specification]
606#[verifier::reject_recursive_types(I)]
607pub struct ExSkip<I>(Skip<I>);
608
609// Ghost accessor for the inner iterator
610pub uninterp spec fn skip_iter<I>(s: Skip<I>) -> I;
611
612// Ghost accessor for the initial count of items to skip
613pub uninterp spec fn skip_init_n<I>(s: Skip<I>) -> usize;
614
615// Define Iter::skip's postcondition
616pub uninterp spec fn skip_post<I>(i: I, n: usize, s: Skip<I>) -> bool;
617
618pub broadcast axiom fn skip_postcondition<I: IteratorSpec>(i: I, n: usize, r: Skip<I>)
619    requires
620        i.obeys_prophetic_iter_laws(),
621        #[trigger] skip_post(i, n, r),
622    ensures
623        IteratorSpec::remaining(&r) == if i.remaining().len() < n { Seq::empty() } else { i.remaining()[n..] },
624        skip_iter(r) == i,
625        skip_init_n(r) == n,
626        IteratorSpec::will_return_none(&r) <==> i.will_return_none(),
627        IteratorSpec::decrease(&r) is Some == i.decrease() is Some,
628;
629
630impl <I> IteratorSpecImpl for Skip<I>
631    where I: Iterator {
632    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
633        skip_iter(*self).obeys_prophetic_iter_laws()
634    }
635
636    #[verifier::prophetic]
637    uninterp spec fn remaining(&self) -> Seq<Self::Item>;
638
639    #[verifier::prophetic]
640    uninterp spec fn will_return_none(&self) -> bool;
641
642    uninterp spec fn decrease(&self) -> Option<nat>;
643
644    open spec fn peek(&self, index: int) -> Option<Self::Item> {
645        skip_iter(*self).peek(skip_init_n(*self) + index)
646    }
647}
648
649impl <I> DoubleEndedIteratorSpecImpl for Skip<I>
650    where I: DoubleEndedIteratorSpec + ExactSizeIteratorSpec
651{
652    open spec fn peek_back(&self, index: int) -> Option<Self::Item> {
653        // Skip only drops elements from the front, so the back of the skipped
654        // sequence coincides with the back of the inner iterator, as long as
655        // `index` stays within the (un-skipped) remaining elements.
656        let len = skip_iter(*self).exact_len();
657        if len < skip_init_n(*self) || index >= len - skip_init_n(*self) {
658            None
659        } else {
660            skip_iter(*self).peek_back(index)
661        }
662    }
663}
664
665/********************************************************************************
666 * Definitions for `take()`
667 ********************************************************************************/
668#[verifier::external_body]
669#[verifier::external_type_specification]
670#[verifier::reject_recursive_types(I)]
671pub struct ExTake<I>(Take<I>);
672
673// Ghost accessor for the inner iterator
674pub uninterp spec fn take_iter<I>(r: Take<I>) -> I;
675
676// Ghost accessor for the count
677pub uninterp spec fn take_count<I>(r: Take<I>) -> usize;
678
679// Define Iter::take's postcondition
680pub uninterp spec fn take_post<I>(i: I, n: usize, t: Take<I>) -> bool;
681
682pub broadcast axiom fn take_postcondition<I: IteratorSpec>(i: I, n: usize, r: Take<I>)
683    requires
684        i.obeys_prophetic_iter_laws(),
685        #[trigger] take_post(i, n, r),
686    ensures
687        IteratorSpec::remaining(&r) == if i.remaining().len() < n { i.remaining() } else { i.remaining()[..n] },
688        take_iter(r) == i,
689        take_count(r) == n,
690        IteratorSpec::will_return_none(&r) <==> i.will_return_none() || i.remaining().len() >= n,
691        IteratorSpec::decrease(&r) is Some,
692;
693
694// See examples/iterators/take.rs for a verified version of this interface.
695// Any changes here should first be verified over there.
696impl <I> IteratorSpecImpl for Take<I>
697    where I: Iterator {
698    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
699        take_iter(*self).obeys_prophetic_iter_laws()
700    }
701
702    #[verifier::prophetic]
703    uninterp spec fn remaining(&self) -> Seq<Self::Item>;
704
705    #[verifier::prophetic]
706    uninterp spec fn will_return_none(&self) -> bool;
707
708    uninterp spec fn decrease(&self) -> Option<nat>;
709
710    open spec fn peek(&self, index: int) -> Option<Self::Item> {
711        take_iter(*self).peek(index)
712    }
713}
714
715impl <I> DoubleEndedIteratorSpecImpl for Take<I>
716    where I: DoubleEndedIteratorSpec + ExactSizeIteratorSpec
717{
718    open spec fn peek_back(&self, index: int) -> Option<Self::Item> {
719        let len = take_iter(*self).exact_len();
720        if len < take_count(*self) {
721            None
722        } else {
723            take_iter(*self).peek_back(len - take_count(*self) - index - 1)
724        }
725    }
726}
727
728/********************************************************************************
729 * Definitions for `zip()`
730 ********************************************************************************/
731#[verifier::external_body]
732#[verifier::external_type_specification]
733#[verifier::reject_recursive_types(A)]
734#[verifier::reject_recursive_types(B)]
735pub struct ExZip<A, B>(Zip<A, B>);
736
737// Ghost accessor for the first inner iterator
738pub uninterp spec fn zip_iter_fst<A, B>(z: Zip<A, B>) -> A;
739
740// Ghost accessor for the second inner iterator
741pub uninterp spec fn zip_iter_snd<A, B>(z: Zip<A, B>) -> B;
742
743impl<A, B> IteratorSpecImpl for Zip<A, B>
744    where A: Iterator + IteratorSpec, B: Iterator + IteratorSpec
745{
746    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
747        &&& zip_iter_fst(*self).obeys_prophetic_iter_laws()
748        &&& zip_iter_snd(*self).obeys_prophetic_iter_laws()
749    }
750
751    #[verifier::prophetic]
752    closed spec fn remaining(&self) -> Seq<Self::Item> {
753        zip_iter_fst(*self).remaining().zip_truncate(zip_iter_snd(*self).remaining())
754    }
755
756    #[verifier::prophetic]
757    closed spec fn will_return_none(&self) -> bool {
758        zip_iter_fst(*self).will_return_none() || zip_iter_snd(*self).will_return_none()
759    }
760
761    closed spec fn decrease(&self) -> Option<nat> {
762        match (zip_iter_fst(*self).decrease(), zip_iter_snd(*self).decrease()) {
763            (Some(a), Some(b)) => if a <= b { Some(a) } else { Some(b) },
764            (Some(a), None) => Some(a),
765            (None, Some(b)) => Some(b),
766            (None, None) => None,
767        }
768    }
769
770    open spec fn peek(&self, index: int) -> Option<Self::Item> {
771        match (zip_iter_fst(*self).peek(index), zip_iter_snd(*self).peek(index)) {
772            (Some(a), Some(b)) => Some((a, b)),
773            _ => None,
774        }
775    }
776}
777
778// Define Iter::zip's postcondition
779pub uninterp spec fn zip_post<I, U, Z>(i: I, other: U, r: Z) -> bool;
780
781pub broadcast axiom fn zip_postcondition<I, U>(i: I, other: U, r: Zip<I, <U as IntoIterator>::IntoIter>)
782    where
783            I: Sized + IteratorSpec,
784            U: IntoIterator, //Spec,
785    requires
786        i.obeys_prophetic_iter_laws(),
787        #[trigger] zip_post(i, other, r),
788    ensures
789        call_ensures(U::into_iter, (other,), zip_iter_snd(r)),
790        zip_iter_fst(r) == i,
791        IteratorSpec::remaining(&r) == i.remaining().zip_truncate(zip_iter_snd(r).remaining()),
792        IteratorSpec::will_return_none(&r) ==> i.will_return_none() || zip_iter_snd(r).will_return_none(),
793        IteratorSpec::decrease(&r) is Some == (i.decrease() is Some || zip_iter_snd(r).decrease() is Some),
794;
795
796/********************************************************************************
797 * Defines a convenient wrapper type that bundles state and invariants needed
798 * for ergonomic for-loop support.
799 ********************************************************************************/
800
801pub struct VerusForLoopWrapper<I: Iterator> {
802    pub index: Ghost<int>,
803    pub snapshot: Ghost<I>,
804    pub iter: I,
805    pub history: Ghost<Seq<I::Item>>,
806}
807
808impl <I: Iterator> VerusForLoopWrapper<I> {
809    #[verifier::prophetic]
810    pub open spec fn seq(self) -> Seq<I::Item> {
811        self.snapshot@.remaining()
812    }
813
814    // Keep the interface for history and seq the same
815    pub open spec fn history(self) -> Seq<I::Item> {
816        self.history@
817    }
818
819    pub open spec fn index(self) -> int {
820        self.index@
821    }
822
823    /// These properties help maintain the properties in wf,
824    /// but they don't need to be exposed to the client
825    #[verifier::prophetic]
826    pub closed spec fn wf_inner(self) -> bool {
827        &&& self.iter.remaining().len() == self.seq().len() - self.index()
828        &&& forall |i| 0 <= i < self.iter.remaining().len() ==> #[trigger] self.iter.remaining()[i] == self.seq()[self.index() + i]
829        &&& self.iter.will_return_none() ==> self.snapshot@.will_return_none()
830    }
831
832    /// These properties are needed for the client code to verify
833    #[verifier::prophetic]
834    pub open spec fn wf(self) -> bool {
835        &&& 0 <= self.index() <= self.seq().len()
836        &&& self.wf_inner()
837        &&& self.iter.obeys_prophetic_iter_laws() ==> {
838                &&& self.history@.len() == self.index()
839                &&& forall |i| 0 <= i < self.index() ==> #[trigger] self.history@[i] == self.seq()[i]
840            }
841    }
842
843    /// Bundle the real iterator with its ghost state and loop invariants
844    pub fn new(iter: I) -> (s: Self)
845        ensures
846            s.index == 0,
847            s.snapshot == iter,
848            s.iter == iter,
849            s.history@ == Seq::<I::Item>::empty(),
850            s.wf(),
851    {
852        broadcast use lemma_seq_empty;
853        VerusForLoopWrapper {
854            index: Ghost(0),
855            snapshot: Ghost(iter),
856            iter,
857            history: Ghost(Seq::empty()),
858        }
859    }
860
861    /// Advance the underlying (real) iterator and prove
862    /// that the loop invariants are preserved.
863    pub fn next(&mut self) -> (ret: Option<I::Item>)
864        requires
865            old(self).wf(),
866        ensures
867            final(self).seq() == old(self).seq(),
868            final(self).index() == old(self).index() + if ret is Some { 1int } else { 0 },
869            final(self).snapshot == old(self).snapshot,
870            final(self).iter.obeys_prophetic_iter_laws() ==> final(self).wf(),
871            final(self).iter.obeys_prophetic_iter_laws() && ret is None ==>
872                final(self).snapshot@.will_return_none() && final(self).index() == final(self).seq().len(),
873            final(self).iter.obeys_prophetic_iter_laws() ==> (ret matches Some(r) ==>
874                r == old(self).seq()[old(self).index()]),
875            // History updates always hold
876            ret matches Some(i) ==> final(self).history@ == old(self).history@.push(i),
877            ret is None ==> final(self).history@ == old(self).history@,
878            // All of the standard Iterator::next guarantees still hold
879            exists |m: &mut I| #![auto] call_ensures(I::next, (m,), ret) && *m == old(self).iter && *final(m) == final(self).iter,
880    {
881        let ghost old_history = self.history@;
882        let ret = self.iter.next();
883        if ret.is_some() {
884            self.history = Ghost(old_history.push(ret->0));
885        }
886        proof {
887            broadcast use group_seq_lemmas;
888            if ret.is_some() {
889                self.index@ = self.index@ + 1;
890            }
891        }
892        ret
893    }
894}
895
896// Artificial function used when we desguar a for loop.
897// It helps bring the definition of `peek` into scope,
898// resulting in better automation for some proofs.
899pub open spec fn trigger_peek_implications<T>(x: T) -> bool { true }
900
901/********************************************************************************
902 * Definitions for the Step trait
903 ********************************************************************************/
904#[verifier::external_trait_specification]
905#[verifier::external_trait_extension(StepSpec via StepSpecImpl)]
906pub trait ExIterStep: Clone + PartialOrd + Sized {
907    type ExternalTraitSpecificationFor: core::iter::Step;
908
909    // REVIEW: it would be nice to be able to use SpecOrd::spec_lt (not yet supported)
910    // TODO: We should now be able to use cmp_spec or partial_cmp_spec here.
911    spec fn spec_is_lt(self, other: Self) -> bool;
912
913    spec fn spec_steps_between(self, end: Self) -> Option<usize>;
914
915    spec fn spec_steps_between_int(self, end: Self) -> int;
916
917    spec fn spec_forward_checked(self, count: usize) -> Option<Self>;
918
919    spec fn spec_forward_checked_int(self, count: int) -> Option<Self>;
920
921    spec fn spec_backward_checked(self, count: usize) -> Option<Self>;
922
923    spec fn spec_backward_checked_int(self, count: int) -> Option<Self>;
924}
925
926
927/********************************************************************************
928 * Collect our broadcast definitions
929 ********************************************************************************/
930
931pub broadcast group group_iter_axioms {
932    rev_postcondition,
933    zip_postcondition,
934    filter_postcondition,
935    take_postcondition,
936    skip_postcondition,
937    map_postcondition,
938}
939
940} // verus!
vstd/std_specs/iter.rs

vstd/std_specs/
iter.rs
