From 6a3f455b6ecb981fb0aebdd254935d9e77df1511 Mon Sep 17 00:00:00 2001 From: Ziqiao Zhou Date: Sat, 23 May 2026 03:32:52 +0000 Subject: [PATCH 1/3] vstd/iter: Add spec for Iterator::find Signed-off-by: Ziqiao Zhou --- source/vstd/std_specs/iter.rs | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/source/vstd/std_specs/iter.rs b/source/vstd/std_specs/iter.rs index 283b144e54..486db98dad 100644 --- a/source/vstd/std_specs/iter.rs +++ b/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

(&mut self, predicate: P) -> (r: Option) + 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] From ea4d54834ff36f2e2a1eb4c7d7af2cf6eeb9fe40 Mon Sep 17 00:00:00 2001 From: Ziqiao Zhou Date: Fri, 29 May 2026 16:45:58 +0000 Subject: [PATCH 2/3] Add test code for Iterator::find --- source/rust_verify_test/tests/iterators.rs | 27 ++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/source/rust_verify_test/tests/iterators.rs b/source/rust_verify_test/tests/iterators.rs index a77d948f4c..bfdc54fde5 100644 --- a/source/rust_verify_test/tests/iterators.rs +++ b/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) + { + 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::*; From 9d73d30555aa82dd3da1157b76dc8ed1707b3bf0 Mon Sep 17 00:00:00 2001 From: Ziqiao Zhou Date: Fri, 29 May 2026 16:50:19 +0000 Subject: [PATCH 3/3] improve find spec and comments --- source/vstd/std_specs/iter.rs | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/source/vstd/std_specs/iter.rs b/source/vstd/std_specs/iter.rs index 486db98dad..0a876576f2 100644 --- a/source/vstd/std_specs/iter.rs +++ b/source/vstd/std_specs/iter.rs @@ -104,19 +104,19 @@ pub trait ExIterator { 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()) + final(self).remaining().is_suffix_of(old(self).remaining()) }, - // If the iterator returns None, then the final remaining elements are empty and - // the predicate is false for all old remaining elements. + // 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 the iterator returns Some, the last element is the one that satisfies the predicate, - // and all previous elements do not satisfy the predicate. + // 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; {