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};
5
6use verus as verus_;
7
8use core::iter::{FromIterator, Iterator, Rev};
9
10verus_! {
11
12#[verifier::external_trait_specification]
13#[verifier::external_trait_extension(IteratorSpec via IteratorSpecImpl)]
14pub trait ExIterator {
15    type ExternalTraitSpecificationFor: Iterator;
16
17    type Item;
18
19    /// This iterator obeys the specifications below on `next`,
20    /// expressed in terms of prophetic spec functions.
21    /// Only iterators that terminate (i.e., eventually return None
22    /// and then continue to return None) should use this interface.
23    spec fn obeys_prophetic_iter_laws(&self) -> bool;
24
25    /// Sequence of items that will (eventually) be returned
26    #[verifier::prophetic]
27    spec fn remaining(&self) -> Seq<Self::Item>;
28
29    /// Does this iterator complete with a `None` after the above sequence?
30    /// (As opposed to hanging indefinitely on a `next()` call)
31    /// Trivially true for most iterators but important for iterators
32    /// that apply an exec closure that may not terminate.
33    #[verifier::prophetic]
34    spec fn will_return_none(&self) -> bool;
35
36    /// Advances the iterator and returns the next value.
37    fn next(&mut self) -> (ret: Option<Self::Item>)
38        ensures
39            // The iterator consistently obeys, completes, and decreases throughout its lifetime
40            final(self).obeys_prophetic_iter_laws() == old(self).obeys_prophetic_iter_laws(),
41            final(self).obeys_prophetic_iter_laws() ==> final(self).will_return_none() == old(self).will_return_none(),
42            final(self).obeys_prophetic_iter_laws() ==> (old(self).decrease() is Some <==> final(self).decrease() is Some),
43            // `next` pops the head of the prophesized remaining(), or returns None
44            final(self).obeys_prophetic_iter_laws() ==>
45            ({
46                if old(self).remaining().len() > 0 {
47                    &&& final(self).remaining() == old(self).remaining().drop_first()
48                    &&& ret == Some(old(self).remaining()[0])
49                } else {
50                    final(self).remaining() == old(self).remaining() && ret == None && final(self).will_return_none()
51                }
52            }),
53            // If the iterator isn't done yet, then it successfully decreases its metric (if any)
54            final(self).obeys_prophetic_iter_laws() && old(self).remaining().len() > 0 && final(self).decrease() is Some ==>
55                decreases_to!(old(self).decrease()->0 => final(self).decrease()->0),
56    ;
57
58    /******* Mechanisms that support ergonomic `for` loops *********/
59
60    /// Value used by default for the decreases clause when no explicit decreases clause is provided
61    /// (the user can override this with an explicit decreases clause).
62    /// If there's no appropriate metric to decrease, this can return None,
63    /// and the user will have to provide an explicit decreases clause.
64    spec fn decrease(&self) -> Option<nat>;
65
66    // If we can make a useful guess as to what the i-th value will be, return it.
67    // Otherwise, return None.
68    spec fn peek(&self, index: int) -> Option<Self::Item>;
69
70    // Provided methods
71
72    // TODO: Once we can add when_used_as_spec to provided trait methods, this would be a simpler encoding:
73    //#[verifier::when_used_as_spec(into_rev_spec)]
74    fn rev(self) -> (r: Rev<Self>)
75        where Self: Sized,
76        ensures
77            self.obeys_prophetic_iter_laws() ==>
78                r == into_rev_spec(self) && rev_post(self, r),
79    ;
80
81    fn collect<B>(self) -> (collection: B)
82        where
83            B: FromIterator<Self::Item>,
84            Self: Sized,
85        ensures
86            self.obeys_prophetic_iter_laws() ==>
87                self.will_return_none() &&
88                FromIteratorSpec::from_iter_ensures(self.remaining(), collection),
89    ;
90
91    fn find<P>(&mut self, predicate: P) -> (r: Option<Self::Item>)
92        where Self: Sized,
93            P: FnMut(&Self::Item) -> bool
94        requires
95            forall |k| #![auto] 0 <= k < self.remaining().len() ==> call_requires(predicate, (&self.remaining()[k], )),
96        ensures
97            // The iterator consistently obeys, completes, and decreases throughout its lifetime
98            final(self).obeys_prophetic_iter_laws() == old(self).obeys_prophetic_iter_laws(),
99            final(self).obeys_prophetic_iter_laws() ==> final(self).will_return_none() == old(self).will_return_none(),
100            final(self).obeys_prophetic_iter_laws() ==> (old(self).decrease() is Some <==> final(self).decrease() is Some),
101            final(self).obeys_prophetic_iter_laws() ==> {
102                final(self).remaining().is_suffix_of(old(self).remaining())
103            },
104            // If find returns None, then the iterator has no remaining
105            // elements, and the predicate was false for all of the original
106            // iterator's elements.
107            final(self).obeys_prophetic_iter_laws() && r.is_none() ==> {
108                &&& final(self).remaining().len() == 0
109                &&& forall |i| 0 <= i < old(self).remaining().len() ==>
110                    predicate.ensures((#[trigger]&old(self).remaining()[i],), false)
111            },
112            // If find returns Some, then the returned value satisfies the
113            // predicate, and all previous elements did not satisfy the
114            // predicate.
115            final(self).obeys_prophetic_iter_laws() && r.is_some() ==> {
116                let idx = old(self).remaining().len() - final(self).remaining().len() - 1;
117                {
118                    &&& 0 <= final(self).remaining().len() < old(self).remaining().len()
119                    &&& predicate.ensures((&r.unwrap(),), true)
120                    &&& old(self).remaining()[idx] == r.unwrap()
121                    &&& forall |i| 0 <= i < idx ==>
122                        predicate.ensures((#[trigger] &old(self).remaining()[i],), false)
123                }
124            };
125
126    // TODO: The Rust implementations of `all` and `any` depend on a correct implementation of `try_fold`
127    //       For now, we assume obeys_prophetic_iter_laws() entails such an implementation, but we should
128    //       eventually constrain implementations of `try_fold` to actually be correct enough to uphold the specs below.
129
130    fn all<F>(&mut self, f: F) -> (r: bool)
131        where Self: Sized,
132            F: FnMut(Self::Item) -> bool
133        requires
134            forall |k| #![auto] 0 <= k < self.remaining().len() ==> call_requires(f, (self.remaining()[k], )),
135        ensures
136            // The iterator consistently obeys, completes, and decreases throughout its lifetime
137            final(self).obeys_prophetic_iter_laws() == old(self).obeys_prophetic_iter_laws(),
138            final(self).obeys_prophetic_iter_laws() ==> final(self).will_return_none() == old(self).will_return_none(),
139            final(self).obeys_prophetic_iter_laws() ==> (old(self).decrease() is Some <==> final(self).decrease() is Some),
140            final(self).obeys_prophetic_iter_laws() ==> {
141                final(self).remaining().is_suffix_of(old(self).remaining())
142            },
143            // If all returns true, then the iterator has no remaining elements,
144            // and the predicate was true for all of the original iterator's elements.
145            final(self).obeys_prophetic_iter_laws() && r ==> {
146                &&& final(self).remaining().len() == 0
147                &&& forall |i| 0 <= i < old(self).remaining().len() ==>
148                    f.ensures((#[trigger] old(self).remaining()[i],), true)
149            },
150            // If all returns false, then there is some element for which the
151            // predicate was false, and all previous elements satisfied the predicate.
152            final(self).obeys_prophetic_iter_laws() && !r ==> {
153                let idx = old(self).remaining().len() - final(self).remaining().len() - 1;
154                {
155                    // The failing element was consumed, so the remaining sequence strictly shrank
156                    &&& final(self).remaining().len() < old(self).remaining().len()
157                    &&& f.ensures((old(self).remaining()[idx],), false)
158                    &&& forall |i| 0 <= i < idx ==>
159                        f.ensures((#[trigger] old(self).remaining()[i],), true)
160                }
161            };
162
163    fn any<F>(&mut self, f: F) -> (r: bool)
164        where Self: Sized,
165            F: FnMut(Self::Item) -> bool
166        requires
167            forall |k| #![auto] 0 <= k < self.remaining().len() ==> call_requires(f, (self.remaining()[k], )),
168        ensures
169            // The iterator consistently obeys, completes, and decreases throughout its lifetime
170            final(self).obeys_prophetic_iter_laws() == old(self).obeys_prophetic_iter_laws(),
171            final(self).obeys_prophetic_iter_laws() ==> final(self).will_return_none() == old(self).will_return_none(),
172            final(self).obeys_prophetic_iter_laws() ==> (old(self).decrease() is Some <==> final(self).decrease() is Some),
173            final(self).obeys_prophetic_iter_laws() ==> {
174                final(self).remaining().is_suffix_of(old(self).remaining())
175            },
176            // If any returns false, then the iterator has no remaining elements,
177            // and the predicate was false for all of the original iterator's elements.
178            final(self).obeys_prophetic_iter_laws() && !r ==> {
179                &&& final(self).remaining().len() == 0
180                &&& forall |i| 0 <= i < old(self).remaining().len() ==>
181                    f.ensures((#[trigger] old(self).remaining()[i],), false)
182            },
183            // If any returns true, then there is some element that satisfied the predicate,
184            // and all previous elements did not satisfy the predicate.
185            final(self).obeys_prophetic_iter_laws() && r ==> {
186                let idx = old(self).remaining().len() - final(self).remaining().len() - 1;
187                {
188                    // The satisfying element was consumed, so the remaining sequence strictly shrank
189                    &&& final(self).remaining().len() < old(self).remaining().len()
190                    &&& f.ensures((old(self).remaining()[idx],), true)
191                    &&& forall |i| 0 <= i < idx ==>
192                        f.ensures((#[trigger] old(self).remaining()[i],), false)
193                }
194            };
195}
196
197#[verifier::external_trait_specification]
198#[verifier::external_trait_extension(DoubleEndedIteratorSpec via DoubleEndedIteratorSpecImpl)]
199pub trait ExDoubleEndedIterator : Iterator {
200    type ExternalTraitSpecificationFor: DoubleEndedIterator;
201
202    // In the specs below, we write out the type parameters explicitly, rather than using the more concise form,
203    // e.g., `final(self).obeys_prophetic_iter_laws()`.  If we use the latter, then Rust elaborates it to
204    // `(&final(self)).obeys_prophetic_iter_laws()`, which means the type of the argument is `& &mut Self`,
205    // which means the type argument inferred for `obeys_prophetic_iter_laws` is `&mut Self`.
206    // This happens because of the existing Rust [trait impl](https://doc.rust-lang.org/std/iter/trait.Iterator.html#impl-Iterator-for-%26mut+I):
207    // ```
208    // impl<I> Iterator for &mut I
209    // where
210    //     I: Iterator + ?Sized,[4:21 AM]
211    // ```
212    fn next_back(&mut self) -> (ret: Option<<Self as core::iter::Iterator>::Item>)
213        ensures
214            // The iterator consistently obeys, completes, and decreases throughout its lifetime
215            <Self as IteratorSpec>::obeys_prophetic_iter_laws(final(self)) == <Self as IteratorSpec>::obeys_prophetic_iter_laws(old(self)),
216            <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)),
217            <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),
218            // `next` pops the tail of the prophesized remaining(), or returns None
219            <Self as IteratorSpec>::obeys_prophetic_iter_laws(final(self)) ==>
220            ({
221                if <Self as IteratorSpec>::remaining(old(self)).len() > 0 {
222                    <Self as IteratorSpec>::remaining(final(self)) == <Self as IteratorSpec>::remaining(old(self)).drop_last()
223                        && ret == Some(<Self as IteratorSpec>::remaining(old(self)).last())
224                } else {
225                    <Self as IteratorSpec>::remaining(final(self)) == <Self as IteratorSpec>::remaining(old(self)) && ret == None && <Self as IteratorSpec>::will_return_none(final(self))
226                }
227            }),
228            // If the iterator isn't done yet, then it successfully decreases its metric (if any)
229            <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 ==>
230                <Self as IteratorSpec>::decrease(old(self))->0 > <Self as IteratorSpec>::decrease(final(self))->0,
231    ;
232
233    /******* Mechanisms that support ergonomic `for` loops *********/
234
235    // If we can make a useful guess as to what the i-th value from the back will be, return it.
236    // Otherwise, return None.
237    spec fn peek_back(&self, index: int) -> Option<Self::Item>;
238}
239
240/********************************************************************************
241 * Definitions for `IntoIterator` and `FromIterator``
242 ********************************************************************************/
243#[verifier::external_trait_specification]
244pub trait ExIntoIterator {
245    type ExternalTraitSpecificationFor: core::iter::IntoIterator;
246}
247
248pub open spec fn iter_into_iter_spec<I: Iterator>(i: I) -> I {
249    i
250}
251
252#[verifier::when_used_as_spec(iter_into_iter_spec)]
253pub assume_specification<I: Iterator>[ <I as IntoIterator>::into_iter ](i: I) -> (r: I)
254    ensures
255        r == i,
256;
257
258// Uninterpreted function representing the sequence of elements that will be
259// produced by the iterator obtained from an IntoIterator value.
260// This avoids requiring IteratorSpec bounds in from_iter's ensures clause.
261pub uninterp spec fn into_iter_remaining<A, T>(iter: T) -> Seq<A>;
262
263// Connects into_iter_remaining to remaining() for types implementing Iterator + IteratorSpec.
264// This allows callers of from_iter to relate the result to the iterator's remaining elements.
265pub broadcast axiom fn axiom_from_iterator_ensures<A, I: Iterator<Item = A> + IteratorSpec>(iter: I)
266    ensures
267        #[trigger] into_iter_remaining::<A, I>(iter) == iter.remaining(),
268;
269
270#[verifier::external_trait_specification]
271#[verifier::external_trait_extension(FromIteratorSpec via FromIteratorSpecImpl)]
272pub trait ExFromIterator<A>: Sized {
273    type ExternalTraitSpecificationFor: FromIterator<A>;
274
275    spec fn from_iter_ensures(remaining: Seq<A>, s: Self) -> bool;
276
277    fn from_iter<T>(iter: T) -> (s: Self)
278       where T: IntoIterator<Item = A>
279        ensures
280            Self::from_iter_ensures(into_iter_remaining(iter), s),
281    ;
282}
283
284/********************************************************************************
285 * Definitions for `rev()`
286 ********************************************************************************/
287#[verifier::external_body]
288#[verifier::external_type_specification]
289#[verifier::reject_recursive_types(I)]
290pub struct ExRev<I>(Rev<I>);
291
292// Ghost accessor for the inner iterator
293pub uninterp spec fn rev_iter<I>(r: Rev<I>) -> I;
294
295// TODO: Do we still need this?
296
297// Spec version of Rev::new
298pub uninterp spec fn into_rev_spec<I>(i: I) -> Rev<I>;
299
300// Ideally, we would write this postcondition directly on the definition of
301// Iterator::rev above.  However, to do so, we would need to impose a trait
302// bound of `Self: DoubleEndedIteratorSpec`.  However, this introduces a cyclic
303// dependency, since DoubleEndedIteratorSpec depends on Iterator.  Hence,
304// we introduce a layer of indirection via this uninterp spec function.
305pub uninterp spec fn rev_post<I>(i: I, r: Rev<I>) -> bool;
306
307pub broadcast axiom fn rev_postcondition<I: DoubleEndedIteratorSpec>(i: I)
308    requires
309        i.obeys_prophetic_iter_laws(),
310        rev_post(i, into_rev_spec(i)),
311    ensures
312        {
313            let r = #[trigger] into_rev_spec(i);
314            &&& IteratorSpec::remaining(&r) == IteratorSpec::remaining(&i).reverse()
315            &&& IteratorSpec::will_return_none(&r) == i.will_return_none()
316            &&& IteratorSpec::decrease(&r) is Some == i.decrease() is Some
317        },
318;
319
320impl <I> IteratorSpecImpl for Rev<I>
321    where I: DoubleEndedIterator + DoubleEndedIteratorSpec {
322    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
323        rev_iter(*self).obeys_prophetic_iter_laws()
324    }
325
326    #[verifier::prophetic]
327    closed spec fn remaining(&self) -> Seq<Self::Item> {
328        rev_iter(*self).remaining().reverse()
329    }
330
331    #[verifier::prophetic]
332    closed spec fn will_return_none(&self) -> bool {
333        rev_iter(*self).will_return_none()
334    }
335
336    closed spec fn decrease(&self) -> Option<nat> {
337        rev_iter(*self).decrease()
338    }
339
340    open spec fn peek(&self, index: int) -> Option<Self::Item> {
341        rev_iter(*self).peek_back(index)
342    }
343}
344
345impl <I> DoubleEndedIteratorSpecImpl for Rev<I>
346    where I: DoubleEndedIterator + IteratorSpec {
347
348    open spec fn peek_back(&self, index: int) -> Option<Self::Item> {
349        rev_iter(*self).peek(index)
350    }
351}
352
353// Forwarding spec impl for the Rust-supplied blanket `impl<I> Iterator for &mut I`.
354// Without this, bare method-call syntax on a `i: &mut I` receiver (e.g. `i.remaining()`)
355// resolves to these (otherwise uninterpreted) functions on `&mut I` rather than on `I`,
356// silently disconnecting clients from `I`'s actual specs.
357impl <I> IteratorSpecImpl for &mut I
358    where I: Iterator {
359    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
360        <I as IteratorSpec>::obeys_prophetic_iter_laws(*self)
361    }
362
363    #[verifier::prophetic]
364    open spec fn remaining(&self) -> Seq<Self::Item> {
365        <I as IteratorSpec>::remaining(*self)
366    }
367
368    #[verifier::prophetic]
369    open spec fn will_return_none(&self) -> bool {
370        <I as IteratorSpec>::will_return_none(*self)
371    }
372
373    open spec fn decrease(&self) -> Option<nat> {
374        <I as IteratorSpec>::decrease(*self)
375    }
376
377    open spec fn peek(&self, index: int) -> Option<Self::Item> {
378        <I as IteratorSpec>::peek(*self, index)
379    }
380}
381
382/********************************************************************************
383 * Defines a convenient wrapper type that bundles state and invariants needed
384 * for ergonomic for-loop support.
385 ********************************************************************************/
386
387pub struct VerusForLoopWrapper<I: Iterator> {
388    pub index: Ghost<int>,
389    pub snapshot: Ghost<I>,
390    pub iter: I,
391    pub history: Ghost<Seq<I::Item>>,
392}
393
394impl <I: Iterator> VerusForLoopWrapper<I> {
395    #[verifier::prophetic]
396    pub open spec fn seq(self) -> Seq<I::Item> {
397        self.snapshot@.remaining()
398    }
399
400    // Keep the interface for history and seq the same
401    pub open spec fn history(self) -> Seq<I::Item> {
402        self.history@
403    }
404
405    pub open spec fn index(self) -> int {
406        self.index@
407    }
408
409    /// These properties help maintain the properties in wf,
410    /// but they don't need to be exposed to the client
411    #[verifier::prophetic]
412    pub closed spec fn wf_inner(self) -> bool {
413        &&& self.iter.remaining().len() == self.seq().len() - self.index()
414        &&& forall |i| 0 <= i < self.iter.remaining().len() ==> #[trigger] self.iter.remaining()[i] == self.seq()[self.index() + i]
415        &&& self.iter.will_return_none() ==> self.snapshot@.will_return_none()
416    }
417
418    /// These properties are needed for the client code to verify
419    #[verifier::prophetic]
420    pub open spec fn wf(self) -> bool {
421        &&& 0 <= self.index() <= self.seq().len()
422        &&& self.wf_inner()
423        &&& self.iter.obeys_prophetic_iter_laws() ==> {
424                &&& self.history@.len() == self.index()
425                &&& forall |i| 0 <= i < self.index() ==> #[trigger] self.history@[i] == self.seq()[i]
426            }
427    }
428
429    /// Bundle the real iterator with its ghost state and loop invariants
430    pub fn new(iter: I) -> (s: Self)
431        ensures
432            s.index == 0,
433            s.snapshot == iter,
434            s.iter == iter,
435            s.history@ == Seq::<I::Item>::empty(),
436            s.wf(),
437    {
438        broadcast use lemma_seq_empty;
439        VerusForLoopWrapper {
440            index: Ghost(0),
441            snapshot: Ghost(iter),
442            iter,
443            history: Ghost(Seq::empty()),
444        }
445    }
446
447    /// Advance the underlying (real) iterator and prove
448    /// that the loop invariants are preserved.
449    pub fn next(&mut self) -> (ret: Option<I::Item>)
450        requires
451            old(self).wf(),
452        ensures
453            final(self).seq() == old(self).seq(),
454            final(self).index() == old(self).index() + if ret is Some { 1int } else { 0 },
455            final(self).snapshot == old(self).snapshot,
456            final(self).iter.obeys_prophetic_iter_laws() ==> final(self).wf(),
457            final(self).iter.obeys_prophetic_iter_laws() && ret is None ==>
458                final(self).snapshot@.will_return_none() && final(self).index() == final(self).seq().len(),
459            final(self).iter.obeys_prophetic_iter_laws() ==> (ret matches Some(r) ==>
460                r == old(self).seq()[old(self).index()]),
461            // History updates always hold
462            ret matches Some(i) ==> final(self).history@ == old(self).history@.push(i),
463            ret is None ==> final(self).history@ == old(self).history@,
464            // All of the standard Iterator::next guarantees still hold
465            exists |m: &mut I| #![auto] call_ensures(I::next, (m,), ret) && *m == old(self).iter && *final(m) == final(self).iter,
466    {
467        let ghost old_history = self.history@;
468        let ret = self.iter.next();
469        if ret.is_some() {
470            self.history = Ghost(old_history.push(ret->0));
471        }
472        proof {
473            broadcast use group_seq_lemmas;
474            if ret.is_some() {
475                self.index@ = self.index@ + 1;
476            }
477        }
478        ret
479    }
480}
481
482// Artificial function used when we desguar a for loop.
483// It helps bring the definition of `peek` into scope,
484// resulting in better automation for some proofs.
485pub open spec fn trigger_peek_implications<T>(x: T) -> bool { true }
486
487/********************************************************************************
488 * Definitions for the Step trait
489 ********************************************************************************/
490#[verifier::external_trait_specification]
491#[verifier::external_trait_extension(StepSpec via StepSpecImpl)]
492pub trait ExIterStep: Clone + PartialOrd + Sized {
493    type ExternalTraitSpecificationFor: core::iter::Step;
494
495    // REVIEW: it would be nice to be able to use SpecOrd::spec_lt (not yet supported)
496    // TODO: We should now be able to use cmp_spec or partial_cmp_spec here.
497    spec fn spec_is_lt(self, other: Self) -> bool;
498
499    spec fn spec_steps_between(self, end: Self) -> Option<usize>;
500
501    spec fn spec_steps_between_int(self, end: Self) -> int;
502
503    spec fn spec_forward_checked(self, count: usize) -> Option<Self>;
504
505    spec fn spec_forward_checked_int(self, count: int) -> Option<Self>;
506
507    spec fn spec_backward_checked(self, count: usize) -> Option<Self>;
508
509    spec fn spec_backward_checked_int(self, count: int) -> Option<Self>;
510}
511
512
513/********************************************************************************
514 * Collect our broadcast definitions
515 ********************************************************************************/
516
517pub broadcast group group_iter_axioms {
518    rev_postcondition,
519}
520
521} // verus!
vstd/std_specs/iter.rs

vstd/std_specs/
iter.rs
