vstd/std_specs/
iter.rs

1use super::super::prelude::*;
2use super::super::seq::{
3    axiom_seq_empty, axiom_seq_subrange_index, axiom_seq_subrange_len, group_seq_axioms,
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    /// Invariant relating the iterator to the initial expression that created it
67    /// (e.g., `my_vec.iter()`).  This allows for more ergonomic/intuitive invariants.
68    /// When the analysis can infer a spec initial value (by discovering a `when_used_as_spec`
69    /// annotation), the analysis places the value in init.
70    #[verifier::prophetic]
71    spec fn initial_value_relation(&self, init: &Self) -> bool;
72
73    // If we can make a useful guess as to what the i-th value will be, return it.
74    // Otherwise, return None.
75    spec fn peek(&self, index: int) -> Option<Self::Item>;
76
77    // Provided methods
78
79    // TODO: Once we can add when_used_as_spec to provided trait methods, this would be a simpler encoding:
80    //#[verifier::when_used_as_spec(into_rev_spec)]
81    fn rev(self) -> (r: Rev<Self>)
82        where Self: Sized,
83        default_ensures
84            self.obeys_prophetic_iter_laws() && self.initial_value_relation(&self) ==>
85                r == into_rev_spec(self) && rev_post(self, r),
86    ;
87
88    fn collect<B>(self) -> (collection: B)
89        where
90            B: FromIterator<Self::Item>,
91            Self: Sized,
92        default_ensures
93            self.will_return_none(),
94            self.obeys_prophetic_iter_laws() && self.initial_value_relation(&self) ==>
95                FromIteratorSpec::from_iter_ensures(self.remaining(), collection),
96    ;
97}
98
99#[verifier::external_trait_specification]
100#[verifier::external_trait_extension(DoubleEndedIteratorSpec via DoubleEndedIteratorSpecImpl)]
101pub trait ExDoubleEndedIterator : Iterator {
102    type ExternalTraitSpecificationFor: DoubleEndedIterator;
103
104    // In the specs below, we write out the type parameters explicitly, rather than using the more concise form,
105    // e.g., `final(self).obeys_prophetic_iter_laws()`.  If we use the latter, then Rust elaborates it to
106    // `(&final(self)).obeys_prophetic_iter_laws()`, which means the type of the argument is `& &mut Self`,
107    // which means the type argument inferred for `obeys_prophetic_iter_laws` is `&mut Self`.
108    // This happens because of the existing Rust [trait impl](https://doc.rust-lang.org/std/iter/trait.Iterator.html#impl-Iterator-for-%26mut+I):
109    // ```
110    // impl<I> Iterator for &mut I
111    // where
112    //     I: Iterator + ?Sized,[4:21 AM]
113    // ```
114    fn next_back(&mut self) -> (ret: Option<<Self as core::iter::Iterator>::Item>)
115        ensures
116            // The iterator consistently obeys, completes, and decreases throughout its lifetime
117            <Self as IteratorSpec>::obeys_prophetic_iter_laws(final(self)) == <Self as IteratorSpec>::obeys_prophetic_iter_laws(old(self)),
118            <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)),
119            <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),
120            // `next` pops the tail of the prophesized remaining(), or returns None
121            <Self as IteratorSpec>::obeys_prophetic_iter_laws(final(self)) ==>
122            ({
123                if <Self as IteratorSpec>::remaining(old(self)).len() > 0 {
124                    <Self as IteratorSpec>::remaining(final(self)) == <Self as IteratorSpec>::remaining(old(self)).drop_last()
125                        && ret == Some(<Self as IteratorSpec>::remaining(old(self)).last())
126                } else {
127                    <Self as IteratorSpec>::remaining(final(self)) == <Self as IteratorSpec>::remaining(old(self)) && ret == None && <Self as IteratorSpec>::will_return_none(final(self))
128                }
129            }),
130            // If the iterator isn't done yet, then it successfully decreases its metric (if any)
131            <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 ==>
132                <Self as IteratorSpec>::decrease(old(self))->0 > <Self as IteratorSpec>::decrease(final(self))->0,
133    ;
134
135    /******* Mechanisms that support ergonomic `for` loops *********/
136
137    // If we can make a useful guess as to what the i-th value from the back will be, return it.
138    // Otherwise, return None.
139    spec fn peek_back(&self, index: int) -> Option<Self::Item>;
140}
141
142/********************************************************************************
143 * Definitions for `IntoIterator` and `FromIterator``
144 ********************************************************************************/
145#[verifier::external_trait_specification]
146pub trait ExIntoIterator {
147    type ExternalTraitSpecificationFor: core::iter::IntoIterator;
148}
149
150pub open spec fn iter_into_iter_spec<I: Iterator>(i: I) -> I {
151    i
152}
153
154#[verifier::when_used_as_spec(iter_into_iter_spec)]
155pub assume_specification<I: Iterator>[ <I as IntoIterator>::into_iter ](i: I) -> (r: I)
156    ensures
157        r == i,
158;
159
160// Uninterpreted function representing the sequence of elements that will be
161// produced by the iterator obtained from an IntoIterator value.
162// This avoids requiring IteratorSpec bounds in from_iter's ensures clause.
163pub uninterp spec fn into_iter_remaining<A, T>(iter: T) -> Seq<A>;
164
165// Connects into_iter_remaining to remaining() for types implementing Iterator + IteratorSpec.
166// This allows callers of from_iter to relate the result to the iterator's remaining elements.
167pub broadcast axiom fn axiom_from_iterator_ensures<A, I: Iterator<Item = A> + IteratorSpec>(iter: I)
168    ensures
169        #[trigger] into_iter_remaining::<A, I>(iter) == iter.remaining(),
170;
171
172#[verifier::external_trait_specification]
173#[verifier::external_trait_extension(FromIteratorSpec via FromIteratorSpecImpl)]
174pub trait ExFromIterator<A>: Sized {
175    type ExternalTraitSpecificationFor: FromIterator<A>;
176
177    spec fn from_iter_ensures(remaining: Seq<A>, s: Self) -> bool;
178
179    fn from_iter<T>(iter: T) -> (s: Self)
180       where T: IntoIterator<Item = A>
181        ensures
182            Self::from_iter_ensures(into_iter_remaining(iter), s),
183    ;
184}
185
186/********************************************************************************
187 * Definitions for `rev()`
188 ********************************************************************************/
189#[verifier::external_body]
190#[verifier::external_type_specification]
191#[verifier::reject_recursive_types(I)]
192pub struct ExRev<I>(Rev<I>);
193
194// Ghost accessor for the inner iterator
195pub uninterp spec fn rev_iter<I>(r: Rev<I>) -> I;
196
197// Spec version of Rev::new
198pub uninterp spec fn into_rev_spec<I>(i: I) -> Rev<I>;
199
200// Ideally, we would write this postcondition directly on the definition of
201// Iterator::rev above.  However, to do so, we would need to impose a trait
202// bound of `Self: DoubleEndedIteratorSpec`.  However, this introduces a cyclic
203// dependency, since DoubleEndedIteratorSpec depends on Iterator.  Hence,
204// we introduce a layer of indirection via this uninterp spec function.
205pub uninterp spec fn rev_post<I>(i: I, r: Rev<I>) -> bool;
206
207pub broadcast axiom fn rev_postcondition<I: DoubleEndedIteratorSpec>(i: I)
208    requires
209        i.obeys_prophetic_iter_laws(),
210        i.initial_value_relation(&i),
211        rev_post(i, into_rev_spec(i)),
212    ensures
213        {
214            let r = #[trigger] into_rev_spec(i);
215            &&& IteratorSpec::remaining(&r) == IteratorSpec::remaining(&i).reverse()
216            &&& IteratorSpec::will_return_none(&r) == i.will_return_none()
217            &&& IteratorSpec::decrease(&r) is Some == i.decrease() is Some
218            &&& IteratorSpec::initial_value_relation(&r, &r)
219        },
220;
221
222impl <I> IteratorSpecImpl for Rev<I>
223    where I: DoubleEndedIterator + DoubleEndedIteratorSpec {
224    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
225        rev_iter(*self).obeys_prophetic_iter_laws()
226    }
227
228    #[verifier::prophetic]
229    closed spec fn remaining(&self) -> Seq<Self::Item> {
230        rev_iter(*self).remaining().reverse()
231    }
232
233    #[verifier::prophetic]
234    closed spec fn will_return_none(&self) -> bool {
235        rev_iter(*self).will_return_none()
236    }
237
238    #[verifier::prophetic]
239    open spec fn initial_value_relation(&self, init: &Self) -> bool {
240        &&& IteratorSpec::remaining(init) == IteratorSpec::remaining(self)
241        &&& rev_iter(*self).initial_value_relation(&rev_iter(*init))
242    }
243
244    closed spec fn decrease(&self) -> Option<nat> {
245        rev_iter(*self).decrease()
246    }
247
248    open spec fn peek(&self, index: int) -> Option<Self::Item> {
249        rev_iter(*self).peek_back(index)
250    }
251}
252
253impl <I> DoubleEndedIteratorSpecImpl for Rev<I>
254    where I: DoubleEndedIterator + IteratorSpec {
255
256    open spec fn peek_back(&self, index: int) -> Option<Self::Item> {
257        rev_iter(*self).peek(index)
258    }
259}
260
261/********************************************************************************
262 * Defines a convenient wrapper type that bundles state and invariants needed
263 * for ergonomic for-loop support.
264 ********************************************************************************/
265
266pub struct VerusForLoopWrapper<'a, I: Iterator> {
267    pub index: Ghost<int>,
268    pub snapshot: Ghost<I>,
269    pub init: Ghost<Option<&'a I>>,
270    pub iter: I,
271    pub history: Ghost<Seq<I::Item>>,
272}
273
274impl <'a, I: Iterator> VerusForLoopWrapper<'a, I> {
275    #[verifier::prophetic]
276    pub open spec fn seq(self) -> Seq<I::Item> {
277        self.snapshot@.remaining()
278    }
279
280    // Keep the interface for history and seq the same
281    pub open spec fn history(self) -> Seq<I::Item> {
282        self.history@
283    }
284
285    pub open spec fn index(self) -> int {
286        self.index@
287    }
288
289    /// These properties help maintain the properties in wf,
290    /// but they don't need to be exposed to the client
291    #[verifier::prophetic]
292    pub closed spec fn wf_inner(self) -> bool {
293        &&& self.iter.remaining().len() == self.seq().len() - self.index()
294        &&& forall |i| 0 <= i < self.iter.remaining().len() ==> #[trigger] self.iter.remaining()[i] == self.seq()[self.index() + i]
295        &&& self.iter.will_return_none() ==> self.snapshot@.will_return_none()
296    }
297
298    /// These properties are needed for the client code to verify
299    #[verifier::prophetic]
300    pub open spec fn wf(self) -> bool {
301        &&& 0 <= self.index() <= self.seq().len()
302        &&& self.init@ matches Some(init) ==> self.snapshot@.initial_value_relation(init)
303        &&& self.wf_inner()
304        &&& self.iter.obeys_prophetic_iter_laws() ==> {
305                &&& self.history@.len() == self.index()
306                &&& forall |i| 0 <= i < self.index() ==> #[trigger] self.history@[i] == self.seq()[i]
307            }
308    }
309
310    /// Bundle the real iterator with its ghost state and loop invariants
311    pub fn new(iter: I, init: Ghost<Option<&'a I>>) -> (s: Self)
312        requires
313            init@ matches Some(i) ==> iter.initial_value_relation(i),
314        ensures
315            s.index == 0,
316            s.snapshot == iter,
317            s.init == init,
318            s.iter == iter,
319            s.history@ == Seq::<I::Item>::empty(),
320            s.wf(),
321    {
322        broadcast use axiom_seq_empty;
323        VerusForLoopWrapper {
324            index: Ghost(0),
325            snapshot: Ghost(iter),
326            init: init,
327            iter,
328            history: Ghost(Seq::empty()),
329        }
330    }
331
332    /// Advance the underlying (real) iterator and prove
333    /// that the loop invariants are preserved.
334    pub fn next(&mut self) -> (ret: Option<I::Item>)
335        requires
336            old(self).wf(),
337        ensures
338            final(self).seq() == old(self).seq(),
339            final(self).index() == old(self).index() + if ret is Some { 1int } else { 0 },
340            final(self).snapshot == old(self).snapshot,
341            final(self).init == old(self).init,
342            final(self).iter.obeys_prophetic_iter_laws() ==> final(self).wf(),
343            final(self).iter.obeys_prophetic_iter_laws() && ret is None ==>
344                final(self).snapshot@.will_return_none() && final(self).index() == final(self).seq().len(),
345            final(self).iter.obeys_prophetic_iter_laws() ==> (ret matches Some(r) ==>
346                r == old(self).seq()[old(self).index()]),
347            // History updates always hold
348            ret matches Some(i) ==> final(self).history@ == old(self).history@.push(i),
349            ret is None ==> final(self).history@ == old(self).history@,
350            // TODO: Uncomment this line to replace everything below, once general mutable refs are supported
351            //call_ensures(I::next, (old(self).iter,), ret),
352            final(self).iter.obeys_prophetic_iter_laws() == old(self).iter.obeys_prophetic_iter_laws(),
353            final(self).iter.obeys_prophetic_iter_laws() ==> final(self).iter.will_return_none() == old(self).iter.will_return_none(),
354            final(self).iter.obeys_prophetic_iter_laws() ==> (old(self).iter.decrease() is Some <==> final(self).iter.decrease() is Some),
355            final(self).iter.obeys_prophetic_iter_laws() ==>
356            ({
357                if old(self).iter.remaining().len() > 0 {
358                    &&& final(self).iter.remaining() == old(self).iter.remaining().drop_first()
359                    &&& ret == Some(old(self).iter.remaining()[0])
360                } else {
361                    final(self).iter.remaining() == old(self).iter.remaining() && ret == None && final(self).iter.will_return_none()
362                }
363            }),
364            final(self).iter.obeys_prophetic_iter_laws() && old(self).iter.remaining().len() > 0 && final(self).iter.decrease() is Some ==>
365                decreases_to!(old(self).iter.decrease()->0 => final(self).iter.decrease()->0),
366    {
367        let ghost old_history = self.history@;
368        let ret = self.iter.next();
369        if ret.is_some() {
370            self.history = Ghost(old_history.push(ret->0));
371        }
372        proof {
373            broadcast use group_seq_axioms;
374            if ret.is_some() {
375                self.index@ = self.index@ + 1;
376            }
377        }
378        ret
379    }
380}
381
382// Artificial function used when we desguar a for loop.
383// It helps bring the definition of `peek` into scope,
384// resulting in better automation for some proofs.
385pub open spec fn trigger_peek_implications<T>(x: T) -> bool { true }
386
387/********************************************************************************
388 * Definitions for the Step trait
389 ********************************************************************************/
390#[verifier::external_trait_specification]
391#[verifier::external_trait_extension(StepSpec via StepSpecImpl)]
392pub trait ExIterStep: Clone + PartialOrd + Sized {
393    type ExternalTraitSpecificationFor: core::iter::Step;
394
395    // REVIEW: it would be nice to be able to use SpecOrd::spec_lt (not yet supported)
396    // TODO: We should now be able to use cmp_spec or partial_cmp_spec here.
397    spec fn spec_is_lt(self, other: Self) -> bool;
398
399    spec fn spec_steps_between(self, end: Self) -> Option<usize>;
400
401    spec fn spec_steps_between_int(self, end: Self) -> int;
402
403    spec fn spec_forward_checked(self, count: usize) -> Option<Self>;
404
405    spec fn spec_forward_checked_int(self, count: int) -> Option<Self>;
406
407    spec fn spec_backward_checked(self, count: usize) -> Option<Self>;
408
409    spec fn spec_backward_checked_int(self, count: int) -> Option<Self>;
410}
411
412
413/********************************************************************************
414 * Collect our broadcast definitions
415 ********************************************************************************/
416
417pub broadcast group group_iter_axioms {
418    rev_postcondition,
419}
420
421} // verus!
vstd/std_specs/iter.rs

vstd/std_specs/
iter.rs
