Add more APIs into `std_specs` #2009

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft

hiroki-chen wants to merge 7 commits into verus-lang:main from hiroki-chen:std-slice-specs

source/vstd/std_specs/control_flow.rs

-Original file line number
+Diff line change
@@ Expand Up / @@ -15,6 +15,11 @@ pub struct ExControlFlow<B, C>(ControlFlow<B, C>); @@
     #[verifier::external_body]
     pub struct ExInfallible(Infallible);
+    pub assume_specification[ core::hint::unreachable_unchecked ]() -> !
+        requires
+            false,
+    ;
     pub assume_specification<T, E>[ Result::<T, E>::branch ](result: Result<T, E>) -> (cf: ControlFlow<
         <Result<T, E> as Try>::Residual,
         <Result<T, E> as Try>::Output,
@@ Expand Down @@

source/vstd/std_specs/core.rs

-Original file line number
+Diff line change
@@ Expand Up / @@ -103,6 +103,21 @@ pub trait ExMetaSized { @@
         type ExternalTraitSpecificationFor: core::marker::MetaSized;
     }
+    #[verifier::external_trait_specification]
+    #[verifier::external_trait_extension(DefaultSpec via DefaultSpecImpl)]
+    pub trait ExDefault: Sized {
+        type ExternalTraitSpecificationFor: core::default::Default;
+        spec fn obeys_default_spec() -> bool;
+        spec fn default_spec() -> Self;
+        fn default() -> (r: Self)
+            ensures
+                Self::obeys_default_spec() ==> r == Self::default_spec(),
+        ;
+    }
     pub assume_specification<T>[ core::mem::swap::<T> ](a: &mut T, b: &mut T)
         ensures
             *a == *old(b),
@@ Expand Down Expand Up @@
     #[verifier::external_body]
     #[verifier::accept_recursive_types(T)]
     pub struct ExAssertParamIsClone<T: Clone + PointeeSized>(core::clone::AssertParamIsClone<T>);
+    macro_rules! impl_default_spec {
+        ($t:ty, $default_value:expr) => {
+            verus_! {
+                pub assume_specification [ <$t as core::default::Default>::default ]() -> (r: $t);
+                impl DefaultSpecImpl for $t {
+                    open spec fn obeys_default_spec() -> bool {
+                        true
+                    }
+                    open spec fn default_spec() -> Self {
+                        $default_value
+                    }
+                }
+            }
+        };
+    }
+    impl_default_spec!(u8, 0u8);
+    impl_default_spec!(u16, 0u16);
+    impl_default_spec!(u32, 0u32);
+    impl_default_spec!(u64, 0u64);
+    impl_default_spec!(u128, 0u128);
+    impl_default_spec!(usize, 0usize);
+    impl_default_spec!(i8, 0i8);
+    impl_default_spec!(i16, 0i16);
+    impl_default_spec!(i32, 0i32);
+    impl_default_spec!(i64, 0i64);
+    impl_default_spec!(i128, 0i128);
+    impl_default_spec!(isize, 0isize);
+    impl_default_spec!(bool, false);

source/vstd/std_specs/slice.rs

-Original file line number
+Diff line change
@@ -1,14 +1,269 @@
     use super::super::prelude::*;
+    use super::cmp::{OrdSpec, PartialEqSpec, PartialOrdSpec};
     use super::core::IndexSetTrustedSpec;
     use super::core::TrustedSpecSealed;
+    use core::cmp::Ordering;
     use core::slice::Iter;
     use verus as verus_;
     verus_! {
-    impl<T, const N: usize> TrustedSpecSealed for [T; N] {}
+    pub open spec fn is_sorted_spec<T: PartialOrd>(s: Seq<T>) -> bool {
+        forall|i: int, j: int|
+            #![trigger s[i].partial_cmp_spec(&s[j])]
+<= i < j < s.len() ==> s[i].partial_cmp_spec(&s[j]) == Some(Ordering::Less)
+                || s[i].partial_cmp_spec(&s[j]) == Some(Ordering::Equal)
+    }
+    pub open spec fn is_sorted_by_spec<'a, T: 'a, F: FnMut(&'a T, &'a T) -> bool>(
+        s: Seq<T>,
+        f: F,
+    ) -> bool {
+        forall|i: int, j: int, b: bool|
+            #![trigger f.ensures((&s[i], &s[j]), b)]
+<= i < j < s.len() ==> f.ensures((&s[i], &s[j]), b) ==> b
+    }
+    pub open spec fn is_sorted_by_pivot_spec<'a, T: 'a, F: FnMut(&'a T) -> Ordering>(
+        s: Seq<T>,
+        f: F,
+    ) -> bool {
+        // The sequence is partitioned into [Less*, Equal*, Greater*]
+        forall|i: int, j: int, ord1: Ordering, ord2: Ordering|
+            #![trigger f.ensures((&s[i],), ord1), f.ensures((&s[j],), ord2)]
+<= i < j < s.len() && f.ensures((&s[i],), ord1) && f.ensures(
+                (&s[j],),
+                ord2,
+            )
+            // Ordering itself is total.
+             ==> ord1.cmp_spec(&ord2) != Ordering::Greater
+    }
+    pub open spec fn is_sorted_by_key_spec<'a, T: 'a, F: FnMut(&'a T) -> K, K: PartialOrd>(
+        s: Seq<T>,
+        f: F,
+    ) -> bool {
+        forall|i: int, j: int, k1: K, k2: K|
+            #![trigger f.ensures((&s[i],), k1), f.ensures((&s[j],), k2)]
+<= i < j < s.len() && f.ensures((&s[i],), k1) && f.ensures(
+                (&s[j],),
+                k2,
+            )
+            // K is partially ordered.
+             ==> k1.partial_cmp_spec(&k2) == Some(Ordering::Less) || k1.partial_cmp_spec(&k2) == Some(
+                Ordering::Equal,
+            )
+    }
+    pub assume_specification<T: PartialOrd>[ <[T]>::is_sorted ](s: &[T]) -> (r: bool)
+        ensures
+            r == is_sorted_spec(s@),
+    ;
+    pub assume_specification<'a, T, F: FnMut(&'a T, &'a T) -> bool>[ <[T]>::is_sorted_by ](
+        s: &'a [T],
+        compare: F,
+    ) -> (r: bool)
+        ensures
+            r == is_sorted_by_spec(s@, compare),
+    ;
+    pub assume_specification<'a, T, F: FnMut(&'a T) -> K, K: PartialOrd>[ <[T]>::is_sorted_by_key ](
+        s: &'a [T],
+        compare: F,
+    ) -> (r: bool)
+        ensures
+            r == is_sorted_by_key_spec(s@, compare),
+    ;
+    /// Binary searches this slice for a given element.
+    ///
+    /// Please be extra careful that if the slice is not properly sorted, the result is
+    /// unspecified and meaningless.
+    ///
+    /// See [here](https://doc.rust-lang.org/stable/core/primitive.slice.html#method.binary_search).
+    pub assume_specification<T: Ord>[ <[T]>::binary_search ](s: &[T], x: &T) -> (r: Result<
+        usize,
+        usize,
+    >)
+        ensures
+            is_sorted_spec(s@) ==> match r {
+                Ok(index) => {
+                    &&& 0 <= index < s.len()
+                    &&& s[index as int] == *x
+                },
+                Err(insert_index) => {
+                    &&& 0 <= insert_index <= s.len()
+                    &&& forall|i: int|
+                        #![trigger s[i].cmp_spec(x)]
+<= i < s.len() ==> {
+                            if i < insert_index {
+                                s[i].cmp_spec(x) != Ordering::Greater
+                            } else {
+                                s[i].cmp_spec(x) != Ordering::Less
+                            }
+                        }
+                },
+            },
+    ;
+    /// Binary searches this slice with a comparator function.
+    ///
+    /// Similar to `binary_search`, but allows the caller to provide a custom comparator function
+    /// that compares each element to the desired pivot value.
+    pub assume_specification<'a, T, F: FnMut(&'a T) -> Ordering>[ <[T]>::binary_search_by ](
+        s: &'a [T],
+        f: F,
+    ) -> (r: Result<usize, usize>)
+        ensures
+            is_sorted_by_pivot_spec(s@, f) ==> match r {
+                Ok(index) => {
+                    &&& 0 <= index < s.len()
+                    &&& forall|ord: Ordering|
+                        #![trigger f.ensures((&s[index as int],), ord)]
+                        f.ensures((&s[index as int],), ord) ==> ord == Ordering::Equal
+                },
+                Err(insert_index) => {
+                    &&& 0 <= insert_index <= s.len()
+                    &&& forall|i: int, ord: Ordering|
+                        #![trigger f.ensures((&s[i],), ord)]
+<= i < s.len() && i < insert_index && f.ensures((&s[i],), ord) ==> ord
+                            != Ordering::Greater
+                    &&& forall|i: int, ord: Ordering|
+                        #![trigger f.ensures((&s[i],), ord)]
+<= i < s.len() && i >= insert_index && f.ensures((&s[i],), ord) ==> ord
+                            != Ordering::Less
+                },
+            },
+    ;
+    /// Binary searches this slice with a key extraction function.
+    pub assume_specification<'a, T, B: Ord, F: FnMut(&'a T) -> B>[ <[T]>::binary_search_by_key ](
+        s: &'a [T],
+        b: &B,
+        f: F,
+    ) -> (r: Result<usize, usize>)
+        ensures
+            is_sorted_by_key_spec(s@, f) ==> match r {
+                Ok(index) => {
+                    &&& 0 <= index < s.len()
+                    &&& forall|key: B|
+                        #![trigger f.ensures((&s[index as int],), key)]
+                        f.ensures((&s[index as int],), key) ==> key.cmp_spec(b) == Ordering::Equal
+                },
+                Err(insert_index) => {
+                    &&& 0 <= insert_index <= s.len()
+                    &&& forall|i: int, key: B|
+                        #![trigger f.ensures((&s[i],), key)]
+<= i < s.len() && i < insert_index && f.ensures((&s[i],), key)
+                            ==> key.cmp_spec(b) != Ordering::Greater
+                    &&& forall|i: int, key: B|
+                        #![trigger f.ensures((&s[i],), key)]
+<= i < s.len() && i >= insert_index && f.ensures((&s[i],), key)
+                            ==> key.cmp_spec(b) != Ordering::Less
+                },
+            },
+    ;
+    pub assume_specification<T: PartialEq>[ <[T]>::contains ](s: &[T], x: &T) -> (r: bool)
+        ensures
+            r <==> exists|i: int| 0 <= i < s.len() && #[trigger] s[i].eq_spec(x),
+    ;
+    pub assume_specification<T: PartialEq>[ <[T]>::starts_with ](s: &[T], needle: &[T]) -> (r: bool)
+        ensures
+            r <==> {
+                &&& needle@.len() <= s@.len()
+                &&& forall|i: int| 0 <= i < needle@.len() ==> #[trigger] s[i].eq_spec(&needle[i])
+            },
+    ;
+    pub assume_specification<T: PartialEq>[ <[T]>::ends_with ](s: &[T], needle: &[T]) -> (r: bool)
+        ensures
+            r <==> {
+                &&& needle@.len() <= s@.len()
+                &&& forall|i: int|
+<= i < needle@.len() ==> s[(s@.len() - needle@.len()) + i].eq_spec(&needle[i])
+            },
+    ;
+    pub assume_specification<T>[ <[T]>::swap ](s: &mut [T], i: usize, j: usize)
+        requires
+<= i < old(s).len(),
+<= j < old(s).len(),
+        ensures
+            s@ =~= old(s)@.update(i as int, old(s)@[j as int]).update(j as int, old(s)@[i as int]),
+    ;
+    pub assume_specification<T>[ <[T]>::reverse ](s: &mut [T])
+        ensures
+            s@ =~= old(s)@.reverse(),
+    ;
+    pub assume_specification<T>[ <[T]>::first ](s: &[T]) -> (r: Option<&T>)
+        ensures
+            r == if s@.len() == 0 {
+                None
+            } else {
+                Some(&s@.first())
+            },
+    ;
+    pub assume_specification<T>[ <[T]>::last ](s: &[T]) -> (r: Option<&T>)
+        ensures
+            r == if s@.len() == 0 {
+                None
+            } else {
+                Some(&s@.last())
+            },
+    ;
+    pub assume_specification<T>[ <[T]>::split_at_checked ](s: &[T], mid: usize) -> (r: Option<
+        (&[T], &[T]),
+    >)
+        ensures
+            mid <= s@.len() ==> {
+                &&& r matches Some((left, right)) && {
+                    &&& left@ =~= s@.subrange(0, mid as int)
+                    &&& right@ =~= s@.subrange(mid as int, s@.len() as int)
+                }
+            },
+            mid > s@.len() ==> r matches None::<(&[T], &[T])>,
+    ;
+    pub assume_specification<T>[ <[T]>::split_at ](s: &[T], mid: usize) -> (r: (&[T], &[T]))
+        ensures
+            mid <= s@.len() ==> {
+                &&& r.0@ =~= s@.subrange(0, mid as int)
+                &&& r.1@ =~= s@.subrange(mid as int, s@.len() as int)
+            },
+    ;
+    pub assume_specification<T>[ <[T]>::rotate_left ](s: &mut [T], mid: usize)
+        ensures
+            mid <= s@.len() ==> s@ =~= old(s)@.subrange(mid as int, s@.len() as int) + old(s)@.subrange(
+,
+                mid as int,
+            ),
+    ;
+    pub assume_specification<T>[ <[T]>::rotate_right ](s: &mut [T], mid: usize)
+        ensures
+            mid <= s@.len() ==> s@ =~= old(s)@.subrange((s@.len() - mid as int), s@.len() as int) + old(
+                s,
+            )@.subrange(0, (s@.len() - mid as int)),
+    ;
+    pub assume_specification<T, const N: usize>[ <[[T; N]]>::as_flattened ](s: &[[T; N]]) -> (r: &[T])
+        ensures
+            r@ =~= Seq::new(s@.len() as nat, |i: int| s@[i]@).flatten(),
+    ;
+    impl<T, const N: usize> TrustedSpecSealed for [T; N] {
+    }
     impl<T, const N: usize> IndexSetTrustedSpec<usize> for [T; N] {
         open spec fn spec_index_set_requires(&self, index: usize) -> bool {
@@ Expand All @@
         }
     }
-    impl<T> TrustedSpecSealed for [T] {}
+    impl<T> TrustedSpecSealed for [T] {
+    }
     impl<T> IndexSetTrustedSpec<usize> for [T] {
         open spec fn spec_index_set_requires(&self, index: usize) -> bool {
@@ Expand All / @@ -32,11 +289,6 @@ impl<T> IndexSetTrustedSpec<usize> for [T] { @@
         }
     }
-    pub assume_specification[ core::hint::unreachable_unchecked ]() -> !
-        requires
-            false,
-    ;
     // The `iter` method of a `<T>` returns an iterator of type `Iter<'_, T>`,
     // so we specify that type here.
     #[verifier::external_type_specification]
@@ Expand Down @@

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add more APIs into `std_specs` #2009

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Add more APIs into std_specs #2009

Are you sure you want to change the base?

Uh oh!

Add more APIs into std_specs #2009

Uh oh!

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Add more APIs into `std_specs` #2009

Add more APIs into `std_specs` #2009