From 3c91dc54956d167e32d350f21f045a002854a50c Mon Sep 17 00:00:00 2001 From: Hiroki Date: Sun, 23 Nov 2025 20:48:00 -0500 Subject: [PATCH 1/6] Implement `Default` --- source/vstd/std_specs/core.rs | 47 +++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) diff --git a/source/vstd/std_specs/core.rs b/source/vstd/std_specs/core.rs index 16f516e606..2514adb6e6 100644 --- a/source/vstd/std_specs/core.rs +++ b/source/vstd/std_specs/core.rs @@ -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[ core::mem::swap:: ](a: &mut T, b: &mut T) ensures *a == *old(b), @@ -211,3 +226,35 @@ pub fn index_set(container: &mut T, index: Idx, val: E) where #[verifier::external_body] #[verifier::accept_recursive_types(T)] pub struct ExAssertParamIsClone(core::clone::AssertParamIsClone); + +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); From 942e4e0bdfaa55332e44c21c93f7a6e06d64e316 Mon Sep 17 00:00:00 2001 From: Hiroki Date: Mon, 24 Nov 2025 12:05:23 -0500 Subject: [PATCH 2/6] Add slice sorting and search specifications --- source/vstd/std_specs/slice.rs | 167 ++++++++++++++++++++++++++++++++- 1 file changed, 165 insertions(+), 2 deletions(-) diff --git a/source/vstd/std_specs/slice.rs b/source/vstd/std_specs/slice.rs index b15dfa079f..a73c5c50fc 100644 --- a/source/vstd/std_specs/slice.rs +++ b/source/vstd/std_specs/slice.rs @@ -1,14 +1,175 @@ 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 TrustedSpecSealed for [T; N] {} +pub open spec fn is_sorted_spec(s: Seq) -> bool { + forall|i: int, j: int| + #![trigger s[i].partial_cmp_spec(&s[j])] + 0 <= 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, + f: F, +) -> bool { + forall|i: int, j: int, b: bool| + #![trigger f.ensures((&s[i], &s[j]), b)] + 0 <= 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, + 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)] + 0 <= 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, + f: F, +) -> bool { + forall|i: int, j: int, k1: K, k2: K| + #![trigger f.ensures((&s[i],), k1), f.ensures((&s[j],), k2)] + 0 <= 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]>::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 https://doc.rust-lang.org/stable/core/primitive.slice.html#method.binary_search +pub assume_specification[ <[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)] + 0 <= 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) where + 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)] + 0 <= 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)] + 0 <= 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) + 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)] + 0 <= 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)] + 0 <= i < s.len() && i >= insert_index && f.ensures((&s[i],), key) + ==> key.cmp_spec(b) != Ordering::Less + }, + }, +; + +impl TrustedSpecSealed for [T; N] { + +} impl IndexSetTrustedSpec for [T; N] { open spec fn spec_index_set_requires(&self, index: usize) -> bool { @@ -20,7 +181,9 @@ impl IndexSetTrustedSpec for [T; N] { } } -impl TrustedSpecSealed for [T] {} +impl TrustedSpecSealed for [T] { + +} impl IndexSetTrustedSpec for [T] { open spec fn spec_index_set_requires(&self, index: usize) -> bool { From 7ed0346fc04ff46a1eec379efaa8b79438e85e8f Mon Sep 17 00:00:00 2001 From: Hiroki Date: Mon, 24 Nov 2025 12:54:10 -0500 Subject: [PATCH 3/6] Add specifications for additional slice methods --- source/vstd/std_specs/slice.rs | 94 ++++++++++++++++++++++++++++++++++ 1 file changed, 94 insertions(+) diff --git a/source/vstd/std_specs/slice.rs b/source/vstd/std_specs/slice.rs index a73c5c50fc..0fa1604746 100644 --- a/source/vstd/std_specs/slice.rs +++ b/source/vstd/std_specs/slice.rs @@ -167,6 +167,100 @@ pub assume_specification<'a, T, B: Ord, F: FnMut(&'a T) -> B>[ <[T]>::binary_sea }, ; +pub assume_specification[ <[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]>::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]>::ends_with ](s: &[T], needle: &[T]) -> (r: bool) + ensures + r <==> { + &&& needle@.len() <= s@.len() + &&& forall|i: int| + 0 <= i < needle@.len() ==> s[(s@.len() - needle@.len()) + i].eq_spec(&needle[i]) + }, +; + +pub assume_specification[ <[T]>::swap ](s: &mut [T], i: usize, j: usize) + requires + 0 <= i < old(s).len(), + 0 <= 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]>::reverse ](s: &mut [T]) + ensures + s@ =~= old(s)@.reverse(), +; + +pub assume_specification[ <[T]>::first ](s: &[T]) -> (r: Option<&T>) + ensures + r == if s@.len() == 0 { + None + } else { + Some(&s@.first()) + }, +; + +pub assume_specification[ <[T]>::last ](s: &[T]) -> (r: Option<&T>) + ensures + r == if s@.len() == 0 { + None + } else { + Some(&s@.last()) + }, +; + +pub assume_specification[ <[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]>::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]>::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( + 0, + mid as int, + ), +; + +pub assume_specification[ <[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; N]]>::as_flattened ](s: &[[T; N]]) -> (r: &[T]) + ensures + r@ =~= Seq::new(s@.len() as nat, |i: int| s@[i]@).flatten(), +; + impl TrustedSpecSealed for [T; N] { } From f9addc018a07683bc81359ce049bc2b67edc0650 Mon Sep 17 00:00:00 2001 From: Hiroki Date: Mon, 24 Nov 2025 12:55:41 -0500 Subject: [PATCH 4/6] Move `unreachable_unchecked` to `control_flow` --- source/vstd/std_specs/control_flow.rs | 5 +++++ source/vstd/std_specs/slice.rs | 5 ----- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/source/vstd/std_specs/control_flow.rs b/source/vstd/std_specs/control_flow.rs index 30c707f764..d46717f1de 100644 --- a/source/vstd/std_specs/control_flow.rs +++ b/source/vstd/std_specs/control_flow.rs @@ -15,6 +15,11 @@ pub struct ExControlFlow(ControlFlow); #[verifier::external_body] pub struct ExInfallible(Infallible); +pub assume_specification[ core::hint::unreachable_unchecked ]() -> ! + requires + false, +; + pub assume_specification[ Result::::branch ](result: Result) -> (cf: ControlFlow< as Try>::Residual, as Try>::Output, diff --git a/source/vstd/std_specs/slice.rs b/source/vstd/std_specs/slice.rs index 0fa1604746..0a44502d09 100644 --- a/source/vstd/std_specs/slice.rs +++ b/source/vstd/std_specs/slice.rs @@ -289,11 +289,6 @@ impl IndexSetTrustedSpec for [T] { } } -pub assume_specification[ core::hint::unreachable_unchecked ]() -> ! - requires - false, -; - // The `iter` method of a `` returns an iterator of type `Iter<'_, T>`, // so we specify that type here. #[verifier::external_type_specification] From 2fc656e29523940c5434cecdc697e74192c1c9da Mon Sep 17 00:00:00 2001 From: Hiroki Date: Mon, 24 Nov 2025 13:10:28 -0500 Subject: [PATCH 5/6] Fix a type --- source/vstd/std_specs/slice.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/source/vstd/std_specs/slice.rs b/source/vstd/std_specs/slice.rs index 0a44502d09..0b5c6e409c 100644 --- a/source/vstd/std_specs/slice.rs +++ b/source/vstd/std_specs/slice.rs @@ -116,7 +116,7 @@ pub assume_specification[ <[T]>::binary_search ](s: &[T], x: &T) -> (r: pub assume_specification<'a, T, F: FnMut(&'a T) -> Ordering>[ <[T]>::binary_search_by ]( s: &'a [T], f: F, -) -> (r: Result) where +) -> (r: Result) ensures is_sorted_by_pivot_spec(s@, f) ==> match r { Ok(index) => { From e90c9da25e8ab5670702d7690e52b2cbce9aa16a Mon Sep 17 00:00:00 2001 From: Hiroki Date: Mon, 24 Nov 2025 13:42:03 -0500 Subject: [PATCH 6/6] Fix rustdoc --- source/vstd/std_specs/slice.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/source/vstd/std_specs/slice.rs b/source/vstd/std_specs/slice.rs index 0b5c6e409c..dfc5d8c838 100644 --- a/source/vstd/std_specs/slice.rs +++ b/source/vstd/std_specs/slice.rs @@ -83,7 +83,7 @@ pub assume_specification<'a, T, F: FnMut(&'a T) -> K, K: PartialOrd>[ <[T]>::is_ /// Please be extra careful that if the slice is not properly sorted, the result is /// unspecified and meaningless. /// -/// See https://doc.rust-lang.org/stable/core/primitive.slice.html#method.binary_search +/// See [here](https://doc.rust-lang.org/stable/core/primitive.slice.html#method.binary_search). pub assume_specification[ <[T]>::binary_search ](s: &[T], x: &T) -> (r: Result< usize, usize,