vstd/iter: Add spec for Iterator::find

source/rust_verify_test/tests/iterators.rs

@@ -22,6 +22,33 @@ test_verify_one_file! {
     } => Ok(())
 }
 
+test_verify_one_file! {
+    #[test] find_works verus_code! {
+        use vstd::prelude::*;
+        use vstd::std_specs::iter::IteratorSpec;
+
+        fn test(v: Vec<u32>)
+        {
+            let v_result = v.into_iter().find(
+                |i| -> (ret: bool)
+                ensures ret == (*i < 10)
+                {*i < 10}
+            );
+            if let Some(i) = v_result {
+                assert(i < 10);
+            } else {
+                proof{
+                    if v.len() > 0  {
+                        assert(v[0] >= 10) by {
+                            assert(v.into_iter().peek(0).unwrap() >= 10);
+                        }
+                    }
+                }
+            }
+        }
+    } => Ok(())
+}
+
 test_verify_one_file! {
     #[test] map_can_be_implemented verus_code! {
         use vstd::prelude::*;

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),
+            final(self).obeys_prophetic_iter_laws() ==> {
+                final(self).remaining().is_suffix_of(old(self).remaining())
+            },
+            // If find returns None, then the iterator has no remaining
+            // elements, and the predicate was false for all of the original
+            // iterator's 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 find returns Some, then the returned value satisfies the
+            // predicate, and all previous elements did 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]