Add basic support for Iter::collect (#2449)

Author: parno

source/rust_verify_test/tests/iterators.rs

@@ -3,6 +3,25 @@
 mod common;
 use common::*;
 
+test_verify_one_file! {
+    #[test] collect_works verus_code! {
+        use vstd::prelude::*;
+
+        fn test(u: &Vec<u32>)
+        {
+            let v: Vec<u32> = vec![1, 2, 3, 4];
+            let w: Vec<u32> = v.into_iter().collect();
+            assert(v@ == w@);
+            let x: Vec<u32> = w.into_iter().rev().collect();
+            assert(x@ == seq![4u32, 3, 2, 1]);
+
+            let y: Vec<u32> = vec![1, 2, 3, 4];
+            let z: Vec<u32> = y.into_iter().rev().rev().collect();
+            assert(z@ == y@);
+        }
+    } => Ok(())
+}
+
 test_verify_one_file! {
     #[test] map_can_be_implemented verus_code! {
         use vstd::prelude::*;

source/vstd/std_specs/core.rs

@@ -150,16 +150,6 @@ pub struct ExOption<V>(core::option::Option<V>);
 #[verifier::reject_recursive_types_in_ground_variants(E)]
 pub struct ExResult<T, E>(core::result::Result<T, E>);
 
-pub open spec fn iter_into_iter_spec<I: Iterator>(i: I) -> I {
-    i
-}
-
-#[verifier::when_used_as_spec(iter_into_iter_spec)]
-pub assume_specification<I: Iterator>[ <I as IntoIterator>::into_iter ](i: I) -> (r: I)
-    ensures
-        r == i,
-;
-
 // I don't really expect this to be particularly useful;
 // this is mostly here because I wanted an easy way to test
 // the combination of external_type_specification & external_body

source/vstd/std_specs/iter.rs

@@ -5,16 +5,10 @@ use super::super::seq::{
 
 use verus as verus_;
 
-use core::iter::{Iterator, Rev};
+use core::iter::{FromIterator, Iterator, Rev};
 
 verus_! {
 
-#[verifier::external_trait_specification]
-pub trait ExIntoIterator {
-    type ExternalTraitSpecificationFor: core::iter::IntoIterator;
-}
-
-
 #[verifier::external_trait_specification]
 #[verifier::external_trait_extension(IteratorSpec via IteratorSpecImpl)]
 pub trait ExIterator {
@@ -91,6 +85,15 @@ pub trait ExIterator {
                 r == into_rev_spec(self) && rev_post(self, r),
     ;
 
+    fn collect<B>(self) -> (collection: B)
+        where
+            B: FromIterator<Self::Item>,
+            Self: Sized,
+        default_ensures
+            self.will_return_none(),
+            self.obeys_prophetic_iter_laws() && self.initial_value_relation(&self) ==>
+                FromIteratorSpec::from_iter_ensures(self.remaining(), collection),
+    ;
 }
 
 #[verifier::external_trait_specification]
@@ -136,6 +139,50 @@ pub trait ExDoubleEndedIterator : Iterator {
     spec fn peek_back(&self, index: int) -> Option<Self::Item>;
 }
 
+/********************************************************************************
+ * Definitions for `IntoIterator` and `FromIterator``
+ ********************************************************************************/
+#[verifier::external_trait_specification]
+pub trait ExIntoIterator {
+    type ExternalTraitSpecificationFor: core::iter::IntoIterator;
+}
+
+pub open spec fn iter_into_iter_spec<I: Iterator>(i: I) -> I {
+    i
+}
+
+#[verifier::when_used_as_spec(iter_into_iter_spec)]
+pub assume_specification<I: Iterator>[ <I as IntoIterator>::into_iter ](i: I) -> (r: I)
+    ensures
+        r == i,
+;
+
+// Uninterpreted function representing the sequence of elements that will be
+// produced by the iterator obtained from an IntoIterator value.
+// This avoids requiring IteratorSpec bounds in from_iter's ensures clause.
+pub uninterp spec fn into_iter_remaining<A, T>(iter: T) -> Seq<A>;
+
+// Connects into_iter_remaining to remaining() for types implementing Iterator + IteratorSpec.
+// This allows callers of from_iter to relate the result to the iterator's remaining elements.
+pub broadcast axiom fn axiom_from_iterator_ensures<A, I: Iterator<Item = A> + IteratorSpec>(iter: I)
+    ensures
+        #[trigger] into_iter_remaining::<A, I>(iter) == iter.remaining(),
+;
+
+#[verifier::external_trait_specification]
+#[verifier::external_trait_extension(FromIteratorSpec via FromIteratorSpecImpl)]
+pub trait ExFromIterator<A>: Sized {
+    type ExternalTraitSpecificationFor: FromIterator<A>;
+
+    spec fn from_iter_ensures(remaining: Seq<A>, s: Self) -> bool;
+
+    fn from_iter<T>(iter: T) -> (s: Self)
+       where T: IntoIterator<Item = A>
+        ensures
+            Self::from_iter_ensures(into_iter_remaining(iter), s),
+    ;
+}
+
 /********************************************************************************
  * Definitions for `rev()`
  ********************************************************************************/

source/vstd/std_specs/vec.rs

@@ -1,5 +1,5 @@
 use super::super::prelude::*;
-use super::iter::IteratorSpec;
+use super::iter::{FromIteratorSpecImpl, IteratorSpec};
 use verus_builtin::*;
 
 use super::super::slice::SliceIndexSpec;
@@ -462,6 +462,12 @@ pub assume_specification<'a, T, A: Allocator> [<&'a Vec<T, A> as core::iter::Int
         IteratorSpec::initial_value_relation(&iter, &iter),
 ;
 
+impl<T>  FromIteratorSpecImpl<T> for Vec<T> {
+    open spec fn from_iter_ensures(remaining: Seq<T>, s: Self) -> bool {
+        remaining == s@
+    }
+}
+
 pub broadcast proof fn lemma_vec_obeys_eq_spec<T: PartialEq>()
     requires
         super::super::laws_eq::obeys_eq::<T>(),