vstd/iter: Add spec for Iterator::find

source/vstd/std_specs/iter.rs

@@ -94,6 +94,38 @@ pub trait ExIterator {
             self.obeys_prophetic_iter_laws() && self.initial_value_relation(&self) ==>
                 FromIteratorSpec::from_iter_ensures(self.remaining(), collection),
     ;
+
+    /// Users may need extra proofs to trigger the `old(self).peek(i)`
+    fn find<P>(&mut self, predicate: P) -> (r: Option<Self::Item>)
+        where Self: Sized,
+            P: FnMut(&Self::Item) -> bool
+        default_ensures
+            // The iterator consistently obeys, completes, and decreases throughout its lifetime
+            final(self).obeys_prophetic_iter_laws() == old(self).obeys_prophetic_iter_laws(),
+            final(self).obeys_prophetic_iter_laws() ==> final(self).will_return_none() == old(self).will_return_none(),
+            final(self).obeys_prophetic_iter_laws() ==> (old(self).decrease() is Some <==> final(self).decrease() is Some),
+            // The final remaining elements are a subsequence of the old remaining.
+            final(self).obeys_prophetic_iter_laws() ==> {
+                &&& old(self).remaining().len() >= final(self).remaining().len()
+                &&& final(self).remaining() == old(self).remaining().skip(old(self).remaining().len() - final(self).remaining().len())
+            },
+            // If the iterator returns None, then the final remaining elements are empty and
+            // the predicate is false for all old remaining elements.
+            final(self).obeys_prophetic_iter_laws() && r.is_none() ==> {
+                &&& final(self).remaining().len() == 0
+                &&& forall |i| (0 <= i < old(self).remaining().len()) ==> predicate.ensures((&(#[trigger]old(self).peek(i)).unwrap(),), false)
+            },
+            // If the iterator returns Some, the last element is the one that satisfies the predicate,
+            // and all previous elements do not satisfy the predicate.
+            final(self).obeys_prophetic_iter_laws() && r.is_some() ==> {
+                let idx = old(self).remaining().len() - final(self).remaining().len() - 1;
+                {
+                    &&& old(self).remaining().len() > 0
+                    &&& predicate.ensures((&r.unwrap(),), true)
+                    &&& old(self).peek(idx) == r
+                    &&& forall |i| (0 <= i < idx) ==> predicate.ensures((&(#[trigger]old(self).peek(i)).unwrap(),), false)
+                }
+            };
 }
 
 #[verifier::external_trait_specification]