diff --git a/examples/verus-snapshot/source/vstd/arithmetic/power2.rs b/examples/verus-snapshot/source/vstd/arithmetic/power2.rs index a164a8c..98b3be5 100644 --- a/examples/verus-snapshot/source/vstd/arithmetic/power2.rs +++ b/examples/verus-snapshot/source/vstd/arithmetic/power2.rs @@ -172,4 +172,81 @@ pub proof fn lemma2_to64() ) by(compute_only); } +/// Proof establishing the concrete values for all powers of 2 from 33 to 64. +/// This lemma is separated from `lemma2_to64()` to avoid a stack overflow issue +/// while executing ./tools/docs.sh. +pub proof fn lemma2_to64_rest() + ensures + pow2(33) == 0x200000000, + pow2(34) == 0x400000000, + pow2(35) == 0x800000000, + pow2(36) == 0x1000000000, + pow2(37) == 0x2000000000, + pow2(38) == 0x4000000000, + pow2(39) == 0x8000000000, + pow2(40) == 0x10000000000, + pow2(41) == 0x20000000000, + pow2(42) == 0x40000000000, + pow2(43) == 0x80000000000, + pow2(44) == 0x100000000000, + pow2(45) == 0x200000000000, + pow2(46) == 0x400000000000, + pow2(47) == 0x800000000000, + pow2(48) == 0x1000000000000, + pow2(49) == 0x2000000000000, + pow2(50) == 0x4000000000000, + pow2(51) == 0x8000000000000, + pow2(52) == 0x10000000000000, + pow2(53) == 0x20000000000000, + pow2(54) == 0x40000000000000, + pow2(55) == 0x80000000000000, + pow2(56) == 0x100000000000000, + pow2(57) == 0x200000000000000, + pow2(58) == 0x400000000000000, + pow2(59) == 0x800000000000000, + pow2(60) == 0x1000000000000000, + pow2(61) == 0x2000000000000000, + pow2(62) == 0x4000000000000000, + pow2(63) == 0x8000000000000000, + pow2(64) == 0x10000000000000000, +{ + reveal(pow2); + reveal(pow); + #[verusfmt::skip] + assert( + pow2(33) == 0x200000000 && + pow2(34) == 0x400000000 && + pow2(35) == 0x800000000 && + pow2(36) == 0x1000000000 && + pow2(37) == 0x2000000000 && + pow2(38) == 0x4000000000 && + pow2(39) == 0x8000000000 && + pow2(40) == 0x10000000000 && + pow2(41) == 0x20000000000 && + pow2(42) == 0x40000000000 && + pow2(43) == 0x80000000000 && + pow2(44) == 0x100000000000 && + pow2(45) == 0x200000000000 && + pow2(46) == 0x400000000000 && + pow2(47) == 0x800000000000 && + pow2(48) == 0x1000000000000 && + pow2(49) == 0x2000000000000 && + pow2(50) == 0x4000000000000 && + pow2(51) == 0x8000000000000 && + pow2(52) == 0x10000000000000 && + pow2(53) == 0x20000000000000 && + pow2(54) == 0x40000000000000 && + pow2(55) == 0x80000000000000 && + pow2(56) == 0x100000000000000 && + pow2(57) == 0x200000000000000 && + pow2(58) == 0x400000000000000 && + pow2(59) == 0x800000000000000 && + pow2(60) == 0x1000000000000000 && + pow2(61) == 0x2000000000000000 && + pow2(62) == 0x4000000000000000 && + pow2(63) == 0x8000000000000000 && + pow2(64) == 0x10000000000000000 + ) by(compute_only); +} + } // verus! diff --git a/examples/verus-snapshot/source/vstd/array.rs b/examples/verus-snapshot/source/vstd/array.rs index efc1c0f..4ea534f 100644 --- a/examples/verus-snapshot/source/vstd/array.rs +++ b/examples/verus-snapshot/source/vstd/array.rs @@ -107,13 +107,10 @@ pub fn array_as_slice(ar: &[T; N]) -> (out: &[T]) ar } -#[verifier::external_fn_specification] -pub fn ex_array_as_slice(ar: &[T; N]) -> (out: &[T]) +pub assume_specification[ <[T; N]>::as_slice ](ar: &[T; N]) -> (out: &[T]) ensures ar@ == out@, -{ - ar.as_slice() -} +; pub spec fn spec_array_fill_for_copy_type(t: T) -> (res: [T; N]); diff --git a/examples/verus-snapshot/source/vstd/function.rs b/examples/verus-snapshot/source/vstd/function.rs deleted file mode 100644 index 1603573..0000000 --- a/examples/verus-snapshot/source/vstd/function.rs +++ /dev/null @@ -1,48 +0,0 @@ -#[allow(unused_imports)] -use super::prelude::*; - -// TODO: get rid of fun_ext* - -verus! { - -/// General properties of spec functions. -/// -/// For now, this just contains an axiom of function extensionality for -/// spec_fn. -/// DEPRECATED: use f1 =~= f2 or f1 =~~= f2 instead. -/// Axiom of function extensionality: two functions are equal if they are -/// equal on all inputs. -#[verifier::external_body] -#[cfg_attr(not(verus_verify_core), deprecated = "use f1 =~= f2 or f1 =~~= f2 instead")] -pub proof fn fun_ext(f1: spec_fn(A) -> B, f2: spec_fn(A) -> B) - requires - forall|x: A| #![trigger f1(x)] f1(x) == f2(x), - ensures - f1 == f2, -{ -} - -} // verus! -/// A macro to conveniently generate similar functional extensionality axioms for functions that -/// take `n` arguments. -#[doc(hidden)] -macro_rules! gen_fun_ext_n { - ($fun_ext:ident, $O:ident, $($x:ident : $I:ident),*) => { - verus! { - /// DEPRECATED: use f1 =~= f2 or f1 =~~= f2 instead. - /// See [`fun_ext`] - #[verifier::external_body] - #[cfg_attr(not(verus_verify_core), deprecated = "use f1 =~= f2 or f1 =~~= f2 instead")] - pub proof fn $fun_ext<$($I),*, $O>(f1: spec_fn($($I),*,) -> $O, f2: spec_fn($($I),*,) -> $O) - requires forall |$($x: $I),*| #![trigger f1($($x),*)] f1($($x),*) == f2($($x),*) - ensures f1 == f2 - {} - } - }; -} - -// Note: We start at 1 just for consistency; it is exactly equivalent to `fun_ext` -gen_fun_ext_n! { fun_ext_1, B, x1: A1 } -gen_fun_ext_n! { fun_ext_2, B, x1: A1, x2: A2 } -gen_fun_ext_n! { fun_ext_3, B, x1: A1, x2: A2, x3: A3 } -gen_fun_ext_n! { fun_ext_4, B, x1: A1, x2: A2, x3: A3, x4: A4 } diff --git a/examples/verus-snapshot/source/vstd/invariant.rs b/examples/verus-snapshot/source/vstd/invariant.rs index f969f2b..430c8ee 100644 --- a/examples/verus-snapshot/source/vstd/invariant.rs +++ b/examples/verus-snapshot/source/vstd/invariant.rs @@ -509,9 +509,9 @@ pub use open_atomic_invariant_internal; /// ``` /// error: possible invariant collision /// | -/// | open_atomic_invariant!(&inv => id1 => { +/// | open_local_invariant!(&inv => id1 => { /// | ^ this invariant -/// | open_atomic_invariant!(&inv => id2 => { +/// | open_local_invariant!(&inv => id2 => { /// | ^ might be the same as this invariant /// ... /// | } diff --git a/examples/verus-snapshot/source/vstd/layout.rs b/examples/verus-snapshot/source/vstd/layout.rs index 9bda5bc..231be3b 100644 --- a/examples/verus-snapshot/source/vstd/layout.rs +++ b/examples/verus-snapshot/source/vstd/layout.rs @@ -69,29 +69,23 @@ pub open spec fn align_of_as_usize() -> usize align_of::() as usize } -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(size_of_as_usize)] -pub fn ex_size_of() -> (u: usize) +pub assume_specification[ core::mem::size_of:: ]() -> (u: usize) ensures is_sized::(), u as nat == size_of::(), opens_invariants none no_unwind -{ - core::mem::size_of::() -} +; -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(align_of_as_usize)] -pub fn ex_align_of() -> (u: usize) +pub assume_specification[ core::mem::align_of:: ]() -> (u: usize) ensures is_sized::(), u as nat == align_of::(), opens_invariants none no_unwind -{ - core::mem::align_of::() -} +; // This is marked as exec, again, in order to force `V` to be a real exec type. // Of course, it's still a no-op. diff --git a/examples/verus-snapshot/source/vstd/map.rs b/examples/verus-snapshot/source/vstd/map.rs index 7267da8..1ce1f0c 100644 --- a/examples/verus-snapshot/source/vstd/map.rs +++ b/examples/verus-snapshot/source/vstd/map.rs @@ -3,7 +3,6 @@ use super::pervasive::*; use super::prelude::*; use super::set::*; -use core::marker; verus! { @@ -27,17 +26,18 @@ verus! { /// * By manipulating an existing map with [`Map::insert`] or [`Map::remove`]. /// /// To prove that two maps are equal, it is usually easiest to use the extensionality operator `=~=`. -#[verifier::external_body] #[verifier::ext_equal] #[verifier::reject_recursive_types(K)] #[verifier::accept_recursive_types(V)] pub tracked struct Map { - dummy: marker::PhantomData<(K, V)>, + mapping: spec_fn(K) -> Option, } impl Map { /// An empty map. - pub spec fn empty() -> Map; + pub closed spec fn empty() -> Map { + Map { mapping: |k| None } + } /// Gives a `Map` whose domain contains every key, and maps each key /// to the value given by `fv`. @@ -52,14 +52,18 @@ impl Map { } /// The domain of the map as a set. - pub spec fn dom(self) -> Set; + pub closed spec fn dom(self) -> Set { + Set::new(|k| (self.mapping)(k) is Some) + } /// Gets the value that the given key `key` maps to. /// For keys not in the domain, the result is meaningless and arbitrary. - pub spec fn index(self, key: K) -> V + pub closed spec fn index(self, key: K) -> V recommends self.dom().contains(key), - ; + { + (self.mapping)(key)->Some_0 + } /// `[]` operator, synonymous with `index` #[verifier::inline] @@ -74,32 +78,36 @@ impl Map { /// /// If the key is already present from the map, then its existing value is overwritten /// by the new value. - pub spec fn insert(self, key: K, value: V) -> Map; + pub closed spec fn insert(self, key: K, value: V) -> Map { + Map { + mapping: |k| + if k == key { + Some(value) + } else { + (self.mapping)(k) + }, + } + } /// Removes the given key and its associated value from the map. /// /// If the key is already absent from the map, then the map is left unchanged. - pub spec fn remove(self, key: K) -> Map; + pub closed spec fn remove(self, key: K) -> Map { + Map { + mapping: |k| + if k == key { + None + } else { + (self.mapping)(k) + }, + } + } /// Returns the number of key-value pairs in the map pub open spec fn len(self) -> nat { self.dom().len() } - /// DEPRECATED: use =~= or =~~= instead. - /// Returns true if the two maps are pointwise equal, i.e., - /// they have the same domains and the corresponding values are equal - /// for each key. This is equivalent to the maps being actually equal - /// by [`axiom_map_ext_equal`]. - /// - /// To prove that two maps are equal via extensionality, it may be easier - /// to use the general-purpose `=~=` or `=~~=` or - /// to use the [`assert_maps_equal!`] macro, rather than using `.ext_equal` directly. - #[cfg_attr(not(verus_verify_core), deprecated = "use =~= or =~~= instead")] - pub open spec fn ext_equal(self, m2: Map) -> bool { - self =~= m2 - } - #[verifier::external_body] pub proof fn tracked_empty() -> (tracked out_v: Self) ensures @@ -222,7 +230,9 @@ pub broadcast proof fn axiom_map_empty() ensures #[trigger] Map::::empty().dom() == Set::::empty(), { - admit(); + broadcast use super::set::group_set_axioms; + + assert(Set::new(|k: K| (|k| None::)(k) is Some) == Set::::empty()); } /// The domain of a map after inserting a key-value pair is equivalent to inserting the key into @@ -231,7 +241,9 @@ pub broadcast proof fn axiom_map_insert_domain(m: Map, key: K, value ensures #[trigger] m.insert(key, value).dom() == m.dom().insert(key), { - admit(); + broadcast use super::set::group_set_axioms; + + assert(m.insert(key, value).dom() =~= m.dom().insert(key)); } /// Inserting `value` at `key` in `m` results in a map that maps `key` to `value` @@ -239,18 +251,15 @@ pub broadcast proof fn axiom_map_insert_same(m: Map, key: K, value: ensures #[trigger] m.insert(key, value)[key] == value, { - admit(); } /// Inserting `value` at `key2` does not change the value mapped to by any other keys in `m` pub broadcast proof fn axiom_map_insert_different(m: Map, key1: K, key2: K, value: V) requires - m.dom().contains(key1), key1 != key2, ensures #[trigger] m.insert(key2, value)[key1] == m[key1], { - admit(); } /// The domain of a map after removing a key-value pair is equivalent to removing the key from @@ -259,19 +268,19 @@ pub broadcast proof fn axiom_map_remove_domain(m: Map, key: K) ensures #[trigger] m.remove(key).dom() == m.dom().remove(key), { - admit(); + broadcast use super::set::group_set_axioms; + + assert(m.remove(key).dom() =~= m.dom().remove(key)); } /// Removing a key-value pair from a map does not change the value mapped to by /// any other keys in the map. pub broadcast proof fn axiom_map_remove_different(m: Map, key1: K, key2: K) requires - m.dom().contains(key1), key1 != key2, ensures #[trigger] m.remove(key2)[key1] == m[key1], { - admit(); } /// Two maps are equivalent if their domains are equivalent and every key in their domains map to the same value. @@ -282,7 +291,26 @@ pub broadcast proof fn axiom_map_ext_equal(m1: Map, m2: Map) &&& forall|k: K| #![auto] m1.dom().contains(k) ==> m1[k] == m2[k] }, { - admit(); + broadcast use super::set::group_set_axioms; + + if m1 =~= m2 { + assert(m1.dom() =~= m2.dom()); + assert(forall|k: K| #![auto] m1.dom().contains(k) ==> m1[k] == m2[k]); + } + if ({ + &&& m1.dom() =~= m2.dom() + &&& forall|k: K| #![auto] m1.dom().contains(k) ==> m1[k] == m2[k] + }) { + if m1.mapping != m2.mapping { + assert(exists|k| #[trigger] (m1.mapping)(k) != (m2.mapping)(k)); + let k = choose|k| #[trigger] (m1.mapping)(k) != (m2.mapping)(k); + if m1.dom().contains(k) { + assert(m1[k] == m2[k]); + } + assert(false); + } + assert(m1 =~= m2); + } } pub broadcast proof fn axiom_map_ext_equal_deep(m1: Map, m2: Map) @@ -292,7 +320,7 @@ pub broadcast proof fn axiom_map_ext_equal_deep(m1: Map, m2: Map m1[k] =~~= m2[k] }, { - admit(); + axiom_map_ext_equal(m1, m2); } pub broadcast group group_map_axioms { diff --git a/examples/verus-snapshot/source/vstd/map_lib.rs b/examples/verus-snapshot/source/vstd/map_lib.rs index c196ad7..bfa5183 100644 --- a/examples/verus-snapshot/source/vstd/map_lib.rs +++ b/examples/verus-snapshot/source/vstd/map_lib.rs @@ -74,13 +74,6 @@ impl Map { self.submap_of(m2) } - /// Deprecated synonym for `submap_of` - #[verifier::inline] - #[cfg_attr(not(verus_verify_core), deprecated = "use m1.submap_of(m2) or m1 <= m2 instead")] - pub open spec fn le(self, m2: Self) -> bool { - self.submap_of(m2) - } - /// Gives the union of two maps, defined as: /// * The domain is the union of the two input maps. /// * For a given key in _both_ input maps, it maps to the same value that it maps to in the _right_ map (`m2`). @@ -270,6 +263,20 @@ pub proof fn lemma_disjoint_union_size(m1: Map, m2: Map) } } +/// submap_of (<=) is transitive. +pub broadcast proof fn lemma_submap_of_trans(m1: Map, m2: Map, m3: Map) + requires + #[trigger] m1.submap_of(m2), + #[trigger] m2.submap_of(m3), + ensures + m1.submap_of(m3), +{ + assert forall|k| m1.dom().contains(k) implies #[trigger] m3.dom().contains(k) && m1[k] + == m3[k] by { + assert(m2.dom().contains(k)); + } +} + // This verified lemma used to be an axiom in the Dafny prelude /// The domain of a map constructed with `Map::new(fk, fv)` is equivalent to the set constructed with `Set::new(fk)`. pub proof fn lemma_map_new_domain(fk: spec_fn(K) -> bool, fv: spec_fn(K) -> V) diff --git a/examples/verus-snapshot/source/vstd/multiset.rs b/examples/verus-snapshot/source/vstd/multiset.rs index f12f1cb..45f4189 100644 --- a/examples/verus-snapshot/source/vstd/multiset.rs +++ b/examples/verus-snapshot/source/vstd/multiset.rs @@ -62,11 +62,6 @@ impl Multiset { /// must be finite, or else this multiset is arbitrary. pub open spec fn from_map(m: Map) -> Self; - #[cfg_attr(not(verus_verify_core), deprecated = "use from_map instead")] - pub open spec fn new(m: Map) -> Self { - Self::from_map(m) - } - pub open spec fn from_set(m: Set) -> Self { Self::from_map(Map::new(|k| m.contains(k), |v| 1)) } @@ -122,31 +117,11 @@ impl Multiset { forall|v: V| self.count(v) <= m2.count(v) } - #[verifier::inline] - #[cfg_attr(not(verus_verify_core), deprecated = "use m1.subset_of(m2) or m1 <= m2 instead")] - pub open spec fn le(self, m2: Self) -> bool { - self.subset_of(m2) - } - #[verifier::inline] pub open spec fn spec_le(self, m2: Self) -> bool { self.subset_of(m2) } - /// DEPRECATED: use =~= or =~~= instead. - /// Returns true if the two multisets are pointwise equal, i.e., - /// for every value `v: V`, the counts are the same in each multiset. - /// This is equivalent to the multisets actually being equal - /// by [`axiom_multiset_ext_equal`]. - /// - /// To prove that two maps are equal via extensionality, it may be easier - /// to use the general-purpose `=~=` or `=~~=` or - /// to use the [`assert_multisets_equal!`] macro, rather than using `ext_equal` directly. - #[cfg_attr(not(verus_verify_core), deprecated = "use =~= or =~~= instead")] - pub open spec fn ext_equal(self, m2: Self) -> bool { - self =~= m2 - } - // TODO define this in terms of a more general constructor? pub spec fn filter(self, f: impl Fn(V) -> bool) -> Self; diff --git a/examples/verus-snapshot/source/vstd/ptr.rs b/examples/verus-snapshot/source/vstd/ptr.rs deleted file mode 100644 index 3dfeb66..0000000 --- a/examples/verus-snapshot/source/vstd/ptr.rs +++ /dev/null @@ -1,824 +0,0 @@ -#![cfg_attr( - not(verus_verify_core), - deprecated = "The vstd::ptr version of PPtr is deprecated. Use either:\n -- `PPtr` in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)\n -- `*mut T` with vstd::raw_ptr (for more advanced use-cases)" -)] -#![allow(unused_imports)] -#![allow(deprecated)] - -use alloc::alloc::Layout; -use core::{marker, mem, mem::MaybeUninit}; - -use super::layout::*; -use super::modes::*; -use super::pervasive::*; -use super::prelude::*; -use super::*; -use builtin::*; -use builtin_macros::*; - -#[cfg(verus_keep_ghost)] -use super::set_lib::set_int_range; - -verus! { - -/// `PPtr` (which stands for "permissioned pointer") -/// is a wrapper around a raw pointer to `V` on the heap. -/// -/// Technically, it is a wrapper around `*mut mem::MaybeUninit`, that is, the object -/// it points to may be uninitialized. -/// -/// In order to access (read or write) the value behind the pointer, the user needs -/// a special _ghost permission token_, [`PointsTo`](PointsTo). This object is `tracked`, -/// which means that it is "only a proof construct" that does not appear in code, -/// but its uses _are_ checked by the borrow-checker. This ensures memory safety, -/// data-race-freedom, prohibits use-after-free, etc. -/// -/// ### PointsTo objects. -/// -/// The [`PointsTo`] object represents both the ability to access the data behind the -/// pointer _and_ the ability to free it (return it to the memory allocator). -/// -/// In particular: -/// * When the user owns a `PointsTo` object associated to a given pointer, -/// they can either read or write its contents, or deallocate ("free") it. -/// * When the user has a shared borrow, `&PointsTo`, they can read -/// the contents (i.e., obtained a shared borrow `&V`). -/// -/// The `perm: PointsTo` object tracks two pieces of data: -/// * `perm.pptr` is the pointer that the permission is associated to, -/// given by [`ptr.id()`](PPtr::id). -/// * `perm.value` tracks the data that is behind the pointer. Thereby: -/// * When the user uses the permission to _read_ a value, they always -/// read the value as given by the `perm.value`. -/// * When the user uses the permission to _write_ a value, the `perm.value` -/// data is updated. -/// -/// For those familiar with separation logic, the `PointsTo` object plays a role -/// similar to that of the "points-to" operator, _ptr_ ↦ _value_. -/// -/// ### Differences from `PCell`. -/// -/// `PPtr` is similar to [`cell::PCell`], but has a few key differences: -/// * In `PCell`, the type `T` is placed internally to the `PCell`, whereas with `PPtr`, -/// the type `T` is placed at some location on the heap. -/// * Since `PPtr` is just a pointer (represented by an integer), it can be `Copy`. -/// * The `ptr::PointsTo` token represents not just the permission to read/write -/// the contents, but also to deallocate. -/// -/// ### Example (TODO) -// Notes about pointer provenance: -// -// "Pointer provenance" is this complicated subject which is a necessary -// evil if you want to understand the abstract machine semantics of a language -// with pointers and what is or is not UB with int-to-pointer casts. -// -// See this series of blog posts for some introduction: -// https://www.ralfj.de/blog/2022/04/11/provenance-exposed.html -// -// Here in Verus, where code is forced to be verified, we want to tell -// a much simpler story, which is the following: -// -// ***** VERUS POINTER MODEL ***** -// "Provenance" comes from the `tracked ghost` PointsTo object. -// ******************************* -// -// Pretty simple, right? -// -// Of course, this trusted pointer library still needs to actually run and -// be sound in the Rust backend. -// Rust's abstract pointer model is unchanged, and it doesn't know anything -// about Verus's special ghost `PointsTo` object, which gets erased, anyway. -// -// Maybe someday the ghost PointsTo model will become a real -// memory model. That isn't true today. -// So we still need to know something about actual, real memory models that -// are used right now in order to implement this API soundly. -// -// Our goal is to allow the *user of Verus* to think in terms of the -// VERUS POINTER MODEL where provenance is tracked via the `PointsTo` object. -// The rest of this is just details for the trusted implementation of PPtr -// that will be sound in the Rust backend. -// -// In the "PNVI-ae-udi" model: -// * A ptr->int cast "exposes" a pointer (adding it some global list in the -// abstract machine) -// * An int->ptr cast acquires the provenance of that pointer only if it -// was previously exposed. -// -// The "tower of weakenings", however, -// (see https://gankra.github.io/blah/tower-of-weakenings/) -// proposes a stricter model called "Strict Provenance". -// This basically forbids exposing and requires provenance to always be tracked. -// -// If possible, it would be nice to stick to this stricter model, but it isn't necessary. -// -// Unfortunately, it's not possible. The Strict Provenance requires "provenance" to be -// tracked through non-ghost pointers. We can't use our ghost objects to track provenance -// in general while staying consistent with Strict Provenance. -// -// We have two options: -// -// 1. Just forbid int->ptr conversions -// 2. Always "expose" every PPtr when it's created, in order to definitely be safe -// under PNVI-ae-udi. -// -// However, int->ptr conversions ought to be allowed in the VERUS POINTER MODEL, -// so I'm going with (2) here. -// -// TODO reconsider: Is this plan actually good? Exposing all pointers has the potential -// to ruin optimizations. If the plan is bad, and we want to avoid the cost of -// "expose-everywhere", we may need to actually track provenance as part -// of the specification of PPtr. -// -// Perhaps what we could do is specify a low-level pointer library with -// strict provenance rules + exposed pointers, -// and then verify user libraries on top of that? -// TODO implement: borrow_mut; figure out Drop, see if we can avoid leaking? -// TODO just replace this with `*mut V` -#[repr(C)] -#[verifier::accept_recursive_types(V)] -pub struct PPtr { - pub uptr: *mut V, -} - -// PPtr is always safe to Send/Sync. It's the PointsTo object where Send/Sync matters. -// It doesn't matter if you send the pointer to another thread if you can't access it. -#[verifier::external] -unsafe impl Sync for PPtr { - -} - -#[verifier::external] -unsafe impl Send for PPtr { - -} - -// TODO some of functionality could have V: ?Sized -/// A `tracked` ghost object that gives the user permission to dereference a pointer -/// for reading or writing, or to free the memory at that pointer. -/// -/// The meaning of a `PointsTo` object is given by the data in its -/// `View` object, [`PointsToData`]. -/// -/// See the [`PPtr`] documentation for more details. -#[verifier::external_body] -#[verifier::reject_recursive_types_in_ground_variants(V)] -pub tracked struct PointsTo { - phantom: marker::PhantomData, - no_copy: NoCopy, -} - -/// Represents the meaning of a [`PointsTo`] object. -pub ghost struct PointsToData { - /// Indicates that this token is for a pointer `ptr: PPtr` - /// such that [`ptr.id()`](PPtr::id) equal to this value. - pub pptr: int, - /// Indicates that this token gives the ability to read a value `V` from memory. - /// When `None`, it indicates that the memory is uninitialized. - pub value: Option, -} - -// TODO add similiar height axioms for other ghost objects -pub broadcast proof fn points_to_height_axiom(points_to: PointsTo) - ensures - #[trigger] is_smaller_than(points_to@, points_to), -{ - admit(); -} - -pub broadcast group group_ptr_axioms { - points_to_height_axiom, -} - -/// Points to uninitialized memory. -#[verifier::external_body] -pub tracked struct PointsToRaw { - no_copy: NoCopy, -} - -#[verifier::external_body] -#[verifier::reject_recursive_types_in_ground_variants(V)] -pub tracked struct Dealloc { - phantom: marker::PhantomData, - no_copy: NoCopy, -} - -pub ghost struct DeallocData { - pub pptr: int, -} - -#[verifier::external_body] -pub tracked struct DeallocRaw { - no_copy: NoCopy, -} - -pub ghost struct DeallocRawData { - pub pptr: int, - pub size: nat, - pub align: nat, -} - -impl PointsTo { - pub spec fn view(self) -> PointsToData; - - /// Any dereferenceable pointer must be non-null. - /// (Note that null pointers _do_ exist and are representable by `PPtr`; - /// however, it is not possible to obtain a `PointsTo` token for - /// any such a pointer.) - #[verifier::external_body] - pub proof fn is_nonnull(tracked &self) - ensures - self@.pptr != 0, - { - unimplemented!(); - } - - #[verifier::external_body] - pub proof fn leak_contents(tracked &mut self) - ensures - self@.pptr == old(self)@.pptr && self@.value.is_None(), - { - unimplemented!(); - } -} - -impl PointsTo { - #[verifier::external_body] - pub proof fn into_raw(tracked self) -> (tracked points_to_raw: PointsToRaw) - requires - self@.value.is_None(), - ensures - points_to_raw.is_range(self@.pptr, size_of::() as int), - is_sized::(), - { - unimplemented!(); - } - - #[verifier::external_body] - pub proof fn borrow_raw(tracked &self) -> (tracked points_to_raw: &PointsToRaw) - requires - self@.value.is_None(), - ensures - points_to_raw.is_range(self@.pptr, size_of::() as int), - is_sized::(), - { - unimplemented!(); - } -} - -impl PointsToRaw { - pub spec fn view(self) -> Map; - - pub open spec fn contains_range(self, start: int, len: int) -> bool { - set_int_range(start, start + len).subset_of(self@.dom()) - } - - pub open spec fn is_range(self, start: int, len: int) -> bool { - set_int_range(start, start + len) =~= self@.dom() - } - - #[verifier::inline] - pub open spec fn spec_index(self, i: int) -> u8 { - self@[i] - } - - #[verifier::external_body] - pub proof fn is_nonnull(tracked &self) - ensures - !self@.dom().contains(0), - { - unimplemented!(); - } - - #[verifier::external_body] - pub proof fn is_in_bounds(tracked &self) - ensures - forall|i: int| self@.dom().contains(i) ==> 0 < i <= usize::MAX, - { - unimplemented!(); - } - - #[verifier::external_body] - pub proof fn empty() -> (tracked points_to_raw: Self) - ensures - points_to_raw@ == Map::::empty(), - { - unimplemented!(); - } - - #[verifier::external_body] - pub proof fn into_typed(tracked self, start: usize) -> (tracked points_to: PointsTo) - requires - is_sized::(), - start as int % align_of::() as int == 0, - self.is_range(start as int, size_of::() as int), - ensures - points_to@.pptr == start, - points_to@.value === None, - { - unimplemented!(); - } - - #[verifier::external_body] - pub proof fn borrow_typed(tracked &self, start: int) -> (tracked points_to: &PointsTo) - requires - is_sized::(), - start % align_of::() as int == 0, - self.contains_range(start, size_of::() as int), - ensures - points_to@.pptr === start, - points_to@.value === None, - { - unimplemented!(); - } - - #[verifier::external_body] - pub proof fn join(tracked self, tracked other: Self) -> (tracked joined: Self) - ensures - self@.dom().disjoint(other@.dom()), - joined@ == self@.union_prefer_right(other@), - { - unimplemented!(); - } - - pub proof fn insert(tracked &mut self, tracked other: Self) - ensures - old(self)@.dom().disjoint(other@.dom()), - self@ == old(self)@.union_prefer_right(other@), - { - let tracked mut tmp = Self::empty(); - tracked_swap(&mut tmp, self); - tmp = tmp.join(other); - tracked_swap(&mut tmp, self); - } - - #[verifier::external_body] - pub proof fn borrow_join<'a>(tracked &'a self, tracked other: &'a Self) -> (tracked joined: - &'a Self) - ensures - (forall|i| - #![trigger self@.dom().contains(i), other@.dom().contains(i)] - self@.dom().contains(i) && other@.dom().contains(i) ==> self@[i] == other@[i]), - joined@ == self@.union_prefer_right(other@), - { - unimplemented!(); - } - - #[verifier::external_body] - pub proof fn split(tracked self, range: Set) -> (tracked res: (Self, Self)) - requires - range.subset_of(self@.dom()), - ensures - res.0@ == self@.restrict(range), - res.1@ == self@.remove_keys(range), - { - unimplemented!(); - } - - pub proof fn take(tracked &mut self, range: Set) -> (tracked res: Self) - requires - range.subset_of(old(self)@.dom()), - ensures - res@ == old(self)@.restrict(range), - self@ == old(self)@.remove_keys(range), - { - let tracked mut tmp = Self::empty(); - tracked_swap(&mut tmp, self); - let tracked (l, mut r) = tmp.split(range); - tracked_swap(&mut r, self); - l - } - - #[verifier::external_body] - pub proof fn borrow_subset(tracked &self, range: Set) -> (tracked res: &Self) - requires - range.subset_of(self@.dom()), - ensures - res@ == self@.restrict(range), - { - unimplemented!(); - } -} - -impl Dealloc { - pub spec fn view(self) -> DeallocData; -} - -impl Dealloc { - #[verifier::external_body] - pub proof fn is_nonnull(tracked &self) - ensures - self@.pptr != 0, - { - unimplemented!(); - } - - #[verifier::external_body] - pub proof fn into_raw(tracked self) -> (tracked dealloc_raw: DeallocRaw) - ensures - dealloc_raw@.pptr === self@.pptr, - dealloc_raw@.size === size_of::(), - dealloc_raw@.align === align_of::(), - is_sized::(), - { - unimplemented!(); - } - - #[verifier::external_body] - pub proof fn borrow_raw(tracked &self) -> (tracked dealloc_raw: &DeallocRaw) - ensures - dealloc_raw@.pptr === self@.pptr, - dealloc_raw@.size === size_of::(), - dealloc_raw@.align === align_of::(), - is_sized::(), - { - unimplemented!(); - } -} - -impl DeallocRaw { - pub spec fn view(self) -> DeallocRawData; - - #[verifier::external_body] - pub proof fn is_nonnull(tracked &self) - ensures - self@.pptr != 0, - { - unimplemented!(); - } - - #[verifier::external_body] - pub proof fn into_typed(tracked self) -> (tracked dealloc: Dealloc) - requires - is_sized::(), - self@.size === size_of::(), - self@.align === align_of::(), - ensures - dealloc@.pptr === self@.pptr, - { - unimplemented!(); - } - - #[verifier::external_body] - pub proof fn borrow_typed(tracked &self) -> (tracked dealloc: &Dealloc) - requires - is_sized::(), - self@.size === size_of::(), - self@.align === align_of::(), - ensures - dealloc@.pptr === self@.pptr, - { - unimplemented!(); - } -} - -impl Clone for PPtr { - #[verifier::external_body] - fn clone(&self) -> (s: Self) - ensures - s == *self, - { - PPtr { uptr: self.uptr } - } -} - -impl Copy for PPtr { - -} - -impl PPtr { - /// Cast a pointer to an integer. - #[inline(always)] - #[verifier::external_body] - pub fn to_usize(&self) -> (u: usize) - ensures - u as int == self.id(), - { - self.uptr as usize - } - - /// integer address of the pointer - pub spec fn id(&self) -> int; - - /// Cast an integer to a pointer. - /// - /// Note that this does _not_ require or ensure that the pointer is valid. - /// Of course, if the user creates an invalid pointer, they would still not be able to - /// create a valid [`PointsTo`] token for it, and thus they would never - /// be able to access the data behind the pointer. - /// - /// This is analogous to normal Rust, where casting to a pointer is always possible, - /// but dereferencing a pointer is an `unsafe` operation. - /// In Verus, casting to a pointer is likewise always possible, - /// while dereferencing it is only allowed when the right preconditions are met. - #[inline(always)] - #[verifier::external_body] - pub fn from_usize(u: usize) -> (p: Self) - ensures - p.id() == u as int, - { - let uptr = u as *mut V; - PPtr { uptr } - } - - /// Allocates heap memory for type `V`, leaving it uninitialized. - #[inline(always)] - #[verifier::external_body] - pub fn empty() -> (pt: (PPtr, Tracked>, Tracked>)) - ensures - pt.1@@ === (PointsToData { pptr: pt.0.id(), value: None }), - pt.2@@ === (DeallocData { pptr: pt.0.id() }), - opens_invariants none - { - let layout = Layout::new::(); - let size = layout.size(); - let align = layout.align(); - let (p, _, _) = PPtr::::alloc(size, align); - (p, Tracked::assume_new(), Tracked::assume_new()) - } - - #[inline(always)] - #[verifier::external_body] - pub fn alloc(size: usize, align: usize) -> (pt: ( - PPtr, - Tracked, - Tracked, - )) - requires - valid_layout(size, align), - ensures - pt.1@.is_range(pt.0.id(), size as int), - pt.2@@ === (DeallocRawData { pptr: pt.0.id(), size: size as nat, align: align as nat }), - pt.0.id() % align as int == 0, - opens_invariants none - { - // Add padding (this is to prevent the user from being able to "combine" allocations) - // Constructing the layout object might fail if the allocation becomes too big. - // The 'add' can't overflow, since we already know (size, align) is a valid layout. - let layout = Layout::from_size_align(size + align, align).unwrap(); - let p = PPtr { uptr: unsafe { ::alloc::alloc::alloc(layout) as *mut V } }; - // See explanation about exposing pointers, above - let _exposed_addr = p.uptr as usize; - (p, Tracked::assume_new(), Tracked::assume_new()) - } - - /// Moves `v` into the location pointed to by the pointer `self`. - /// Requires the memory to be uninitialized, and leaves it initialized. - /// - /// In the ghost perspective, this updates `perm.value` - /// from `None` to `Some(v)`. - #[inline(always)] - #[verifier::external_body] - pub fn put(&self, Tracked(perm): Tracked<&mut PointsTo>, v: V) - requires - self.id() === old(perm)@.pptr, - old(perm)@.value === None, - ensures - perm@.pptr === old(perm)@.pptr, - perm@.value === Some(v), - opens_invariants none - no_unwind - { - // See explanation about exposing pointers, above - let ptr = self.uptr as usize as *mut V; - unsafe { - // We use `write` here because it does not attempt to "drop" the memory at `*ptr`. - core::ptr::write(ptr, v); - } - } - - /// Moves `v` out of the location pointed to by the pointer `self` - /// and returns it. - /// Requires the memory to be initialized, and leaves it uninitialized. - /// - /// In the ghost perspective, this updates `perm.value` - /// from `Some(v)` to `None`, - /// while returning the `v` as an `exec` value. - #[inline(always)] - #[verifier::external_body] - pub fn take(&self, Tracked(perm): Tracked<&mut PointsTo>) -> (v: V) - requires - self.id() === old(perm)@.pptr, - old(perm)@.value.is_Some(), - ensures - perm@.pptr === old(perm)@.pptr, - perm@.value === None, - v === old(perm)@.value.get_Some_0(), - opens_invariants none - no_unwind - { - // See explanation about exposing pointers, above - let ptr = self.uptr as usize as *mut V; - unsafe { core::ptr::read(ptr) } - } - - /// Swaps the `in_v: V` passed in as an argument with the value in memory. - /// Requires the memory to be initialized, and leaves it initialized with the new value. - #[inline(always)] - #[verifier::external_body] - pub fn replace(&self, Tracked(perm): Tracked<&mut PointsTo>, in_v: V) -> (out_v: V) - requires - self.id() === old(perm)@.pptr, - old(perm)@.value.is_Some(), - ensures - perm@.pptr === old(perm)@.pptr, - perm@.value === Some(in_v), - out_v === old(perm)@.value.get_Some_0(), - opens_invariants none - no_unwind - { - // See explanation about exposing pointers, above - let ptr = self.uptr as usize as *mut V; - unsafe { - let mut m = in_v; - mem::swap(&mut m, &mut *ptr); - m - } - } - - /// Given a shared borrow of the `PointsTo`, obtain a shared borrow of `V`. - // Note that `self` is just a pointer, so it doesn't need to outlive - // the returned borrow. - #[inline(always)] - #[verifier::external_body] - pub fn borrow<'a>(&self, Tracked(perm): Tracked<&'a PointsTo>) -> (v: &'a V) - requires - self.id() === perm@.pptr, - perm@.value.is_Some(), - ensures - *v === perm@.value.get_Some_0(), - opens_invariants none - no_unwind - { - // See explanation about exposing pointers, above - let ptr = self.uptr as usize as *mut V; - unsafe { &*ptr } - } - - /// Free the memory pointed to be `perm`. - /// Requires the memory to be uninitialized. - /// - /// This consumes `perm`, since it will no longer be safe to access - /// that memory location. - #[inline(always)] - #[verifier::external_body] - pub fn dispose( - &self, - Tracked(perm): Tracked>, - Tracked(dealloc): Tracked>, - ) - requires - self.id() === perm@.pptr, - perm@.value === None, - perm@.pptr == dealloc@.pptr, - opens_invariants none - { - unsafe { - let layout = alloc::alloc::Layout::for_value(&*self.uptr); - let size = layout.size(); - let align = layout.align(); - // Add the padding to match what we did in 'alloc' - let layout = Layout::from_size_align_unchecked(size + align, align); - ::alloc::alloc::dealloc(self.uptr as *mut u8, layout); - } - } - - #[inline(always)] - #[verifier::external_body] - pub fn dealloc( - &self, - size: usize, - align: usize, - Tracked(perm): Tracked, - Tracked(dealloc): Tracked, - ) - requires - perm.is_range(self.id(), size as int), - dealloc@.pptr === self.id(), - dealloc@.size === size as nat, - dealloc@.align === align as nat, - opens_invariants none - { - unsafe { - // Since we have the Dealloc object, we know this is a valid layout - // and that it's safe to call 'deallocate' - // Remember to add the padding, like in `alloc` - let layout = Layout::from_size_align_unchecked(size + align, align); - ::alloc::alloc::dealloc(self.uptr as *mut u8, layout); - } - } - - ////////////////////////////////// - // Verified library functions below here - /// Free the memory pointed to be `perm` and return the - /// value that was previously there. - /// Requires the memory to be initialized. - /// This consumes the [`PointsTo`] token, since the user is giving up - /// access to the memory by freeing it. - #[inline(always)] - pub fn into_inner( - self, - Tracked(perm): Tracked>, - Tracked(dealloc): Tracked>, - ) -> (v: V) - requires - self.id() === perm@.pptr, - perm@.pptr == dealloc@.pptr, - perm@.value.is_Some(), - ensures - v === perm@.value.get_Some_0(), - opens_invariants none - { - let tracked mut perm = perm; - let v = self.take(Tracked(&mut perm)); - self.dispose(Tracked(perm), Tracked(dealloc)); - v - } - - /// Allocates heap memory for type `V`, leaving it initialized - /// with the given value `v`. - #[inline(always)] - pub fn new(v: V) -> (pt: (PPtr, Tracked>, Tracked>)) - ensures - (pt.1@@ === PointsToData { pptr: pt.0.id(), value: Some(v) }), - (pt.2@@ === DeallocData { pptr: pt.0.id() }), - { - let (p, Tracked(mut t), Tracked(d)) = Self::empty(); - p.put(Tracked(&mut t), v); - (p, Tracked(t), Tracked(d)) - } -} - -impl PPtr { - #[inline(always)] - pub fn write(&self, Tracked(perm): Tracked<&mut PointsTo>, in_v: V) - requires - self.id() === old(perm)@.pptr, - ensures - perm@.pptr === old(perm)@.pptr, - perm@.value === Some(in_v), - opens_invariants none - no_unwind - { - proof { - perm.leak_contents(); - } - self.put(Tracked(&mut *perm), in_v); - } - - #[inline(always)] - pub fn read(&self, Tracked(perm): Tracked<&PointsTo>) -> (out_v: V) - requires - self.id() === perm@.pptr, - perm@.value.is_Some(), - ensures - perm@.value === Some(out_v), - opens_invariants none - no_unwind - { - *self.borrow(Tracked(&*perm)) - } -} - -// Manipulating the contents in a PointsToRaw -impl PPtr { - #[cfg_attr(not(verus_keep_ghost), allow(unused_variables))] - #[verifier::external_body] - fn copy_nonoverlapping( - &self, - dst: PPtr, - count: usize, - perm_src: &PointsToRaw, - perm_dst: &mut PointsToRaw, - ) - requires - perm_src.contains_range(self.id(), count as int), - old(perm_dst).contains_range(dst.id(), count as int), - ensures - perm_dst@ == old(perm_dst)@.union_prefer_right( - perm_src@.restrict(set_int_range(self.id(), self.id() + count)), - ), - { - unsafe { core::ptr::copy_nonoverlapping(self.uptr, dst.uptr, count) } - } - - #[cfg_attr(not(verus_keep_ghost), allow(unused_variables))] - #[verifier::external_body] - fn write_bytes(&self, val: u8, count: usize, perm: &mut PointsToRaw) - requires - old(perm).contains_range(self.id(), count as int), - ensures - perm@ == old(perm)@.union_prefer_right( - Map::new( - |addr| set_int_range(self.id(), self.id() + count).contains(addr), - |addr| val, - ), - ), - { - unsafe { - core::ptr::write_bytes::(self.uptr, val, count); - } - } -} - -} // verus! diff --git a/examples/verus-snapshot/source/vstd/raw_ptr.rs b/examples/verus-snapshot/source/vstd/raw_ptr.rs index bd0a6e6..e3cd5d0 100644 --- a/examples/verus-snapshot/source/vstd/raw_ptr.rs +++ b/examples/verus-snapshot/source/vstd/raw_ptr.rs @@ -283,16 +283,15 @@ pub open spec fn ptr_null>() -> *c } #[cfg(verus_keep_ghost)] -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(ptr_null)] -pub fn ex_ptr_null>() -> (res: *const T) +pub assume_specification< + T: ?Sized + core::ptr::Pointee, +>[ core::ptr::null ]() -> (res: *const T) ensures res == ptr_null::(), opens_invariants none no_unwind -{ - core::ptr::null() -} +; #[verifier::inline] pub open spec fn ptr_null_mut>() -> *mut T { @@ -300,16 +299,15 @@ pub open spec fn ptr_null_mut>() - } #[cfg(verus_keep_ghost)] -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(ptr_null_mut)] -pub fn ex_ptr_null_mut>() -> (res: *mut T) +pub assume_specification< + T: ?Sized + core::ptr::Pointee, +>[ core::ptr::null_mut ]() -> (res: *mut T) ensures res == ptr_null_mut::(), opens_invariants none no_unwind -{ - core::ptr::null_mut() -} +; ////////////////////////////////////// // Casting @@ -459,29 +457,21 @@ macro_rules! pointer_specs { #[verifier::inline] pub open spec fn spec_addr(p: *$mu T) -> usize { p@.addr } - #[verifier::external_fn_specification] #[verifier::when_used_as_spec(spec_addr)] - pub fn ex_addr(p: *$mu T) -> (addr: usize) + pub assume_specification[<*$mu T>::addr](p: *$mu T) -> (addr: usize) ensures addr == spec_addr(p) opens_invariants none - no_unwind - { - p.addr() - } + no_unwind; pub open spec fn spec_with_addr(p: *$mu T, addr: usize) -> *$mu T { $ptr_from_data(PtrData { addr: addr, .. p@ }) } - #[verifier::external_fn_specification] #[verifier::when_used_as_spec(spec_with_addr)] - pub fn ex_with_addr(p: *$mu T, addr: usize) -> (q: *$mu T) + pub assume_specification[<*$mu T>::with_addr](p: *$mu T, addr: usize) -> (q: *$mu T) ensures q == spec_with_addr(p, addr) opens_invariants none - no_unwind - { - p.with_addr(addr) - } + no_unwind; } } diff --git a/examples/verus-snapshot/source/vstd/seq.rs b/examples/verus-snapshot/source/vstd/seq.rs index d9ceda3..2251a09 100644 --- a/examples/verus-snapshot/source/vstd/seq.rs +++ b/examples/verus-snapshot/source/vstd/seq.rs @@ -97,22 +97,6 @@ impl Seq { 0 <= i < self.len(), ; - /// DEPRECATED: use =~= or =~~= instead. - /// Returns `true` if the two sequences are pointwise equal, i.e., - /// they have the same length and the corresponding values are equal - /// at each index. This is equivalent to the sequences being actually equal - /// by [`axiom_seq_ext_equal`]. - /// - /// To prove that two sequences are equal via extensionality, it may be easier - /// to use the general-purpose `=~=` or `=~~=` or - /// to use the [`assert_seqs_equal!`](crate::seq_lib::assert_seqs_equal) macro, - /// rather than using `.ext_equal` directly. - #[cfg_attr(not(verus_verify_core), deprecated = "use =~= or =~~= instead")] - #[rustc_diagnostic_item = "verus::vstd::seq::Seq::ext_equal"] - pub open spec fn ext_equal(self, s2: Seq) -> bool { - self =~= s2 - } - /// Returns a sequence for the given subrange. /// /// ## Example diff --git a/examples/verus-snapshot/source/vstd/set.rs b/examples/verus-snapshot/source/vstd/set.rs index f5f901b..2dec920 100644 --- a/examples/verus-snapshot/source/vstd/set.rs +++ b/examples/verus-snapshot/source/vstd/set.rs @@ -56,20 +56,6 @@ impl Set { self.contains(a) } - /// DEPRECATED: use =~= or =~~= instead. - /// Returns `true` if for every value `a: A`, it is either in both input sets or neither. - /// This is equivalent to the sets being actually equal - /// by [`axiom_set_ext_equal`]. - /// - /// To prove that two sets are equal via extensionality, it may be easier - /// to use the general-purpose `=~=` or `=~~=` or - /// to use the [`assert_sets_equal!`](crate::set_lib::assert_sets_equal) macro, - /// rather than using `.ext_equal` directly. - #[cfg_attr(not(verus_verify_core), deprecated = "use =~= or =~~= instead")] - pub open spec fn ext_equal(self, s2: Set) -> bool { - self =~= s2 - } - /// Returns `true` if the first argument is a subset of the second. pub open spec fn subset_of(self, s2: Set) -> bool { forall|a: A| self.contains(a) ==> s2.contains(a) @@ -202,7 +188,26 @@ pub broadcast proof fn axiom_set_remove_insert(s: Set, a: A) ensures (#[trigger] s.remove(a)).insert(a) == s, { - admit(); + assert forall|aa| #![all_triggers] s.remove(a).insert(a).contains(aa) implies s.contains( + aa, + ) by { + if a == aa { + } else { + axiom_set_remove_different(s, aa, a); + axiom_set_insert_different(s.remove(a), aa, a); + } + }; + assert forall|aa| #![all_triggers] s.contains(aa) implies s.remove(a).insert(a).contains( + aa, + ) by { + if a == aa { + axiom_set_insert_same(s.remove(a), a); + } else { + axiom_set_remove_different(s, aa, a); + axiom_set_insert_different(s.remove(a), aa, a); + } + }; + axiom_set_ext_equal(s.remove(a).insert(a), s); } /// If `a1` does not equal `a2`, then the result of removing element `a2` from set `s` diff --git a/examples/verus-snapshot/source/vstd/set_lib.rs b/examples/verus-snapshot/source/vstd/set_lib.rs index 72b7431..b8a6dbf 100644 --- a/examples/verus-snapshot/source/vstd/set_lib.rs +++ b/examples/verus-snapshot/source/vstd/set_lib.rs @@ -442,6 +442,73 @@ impl Set { } } +/// The result of inserting an element `a` into a set `s` is finite iff `s` is finite. +pub broadcast proof fn lemma_set_insert_finite_iff(s: Set, a: A) + ensures + #[trigger] s.insert(a).finite() <==> s.finite(), +{ + if s.insert(a).finite() { + if s.contains(a) { + assert(s == s.insert(a)); + } else { + assert(s == s.insert(a).remove(a)); + } + } + assert(s.insert(a).finite() ==> s.finite()); +} + +/// The result of removing an element `a` into a set `s` is finite iff `s` is finite. +pub broadcast proof fn lemma_set_remove_finite_iff(s: Set, a: A) + ensures + #[trigger] s.remove(a).finite() <==> s.finite(), +{ + if s.remove(a).finite() { + if s.contains(a) { + assert(s == s.remove(a).insert(a)); + } else { + assert(s == s.remove(a)); + } + } +} + +/// The union of two sets is finite iff both sets are finite. +pub broadcast proof fn lemma_set_union_finite_iff(s1: Set, s2: Set) + ensures + #[trigger] s1.union(s2).finite() <==> s1.finite() && s2.finite(), +{ + if s1.union(s2).finite() { + lemma_set_union_finite_implies_sets_finite(s1, s2); + } +} + +pub proof fn lemma_set_union_finite_implies_sets_finite(s1: Set, s2: Set) + requires + s1.union(s2).finite(), + ensures + s1.finite(), + s2.finite(), + decreases s1.union(s2).len(), +{ + if s1.union(s2) =~= set![] { + assert(s1 =~= set![]); + assert(s2 =~= set![]); + } else { + let a = s1.union(s2).choose(); + assert(s1.remove(a).union(s2.remove(a)) == s1.union(s2).remove(a)); + axiom_set_remove_len(s1.union(s2), a); + lemma_set_union_finite_implies_sets_finite(s1.remove(a), s2.remove(a)); + assert(forall|s: Set| + #![auto] + s.remove(a).insert(a) == if s.contains(a) { + s + } else { + s.insert(a) + }); + lemma_set_insert_finite_iff(s1, a); + lemma_set_insert_finite_iff(s2, a); + } +} + /// The size of a union of two sets is less than or equal to the size of /// both individual sets combined. pub proof fn lemma_len_union(s1: Set, s2: Set) diff --git a/examples/verus-snapshot/source/vstd/slice.rs b/examples/verus-snapshot/source/vstd/slice.rs index 5df0363..1538444 100644 --- a/examples/verus-snapshot/source/vstd/slice.rs +++ b/examples/verus-snapshot/source/vstd/slice.rs @@ -38,6 +38,23 @@ impl SliceAdditionalSpecFns for [T] { } } +#[verifier::external] +pub trait SliceAdditionalExecFns { + fn set(&mut self, idx: usize, t: T); +} + +impl SliceAdditionalExecFns for [T] { + #[verifier::external_body] + fn set(&mut self, idx: usize, t: T) + requires + 0 <= idx < old(self)@.len(), + ensures + self@ == old(self)@.update(idx as int, t), + { + self[idx] = t; + } +} + #[verifier::external_body] #[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::slice::slice_index_get")] pub exec fn slice_index_get(slice: &[T], i: usize) -> (out: &T) @@ -61,14 +78,11 @@ pub broadcast proof fn axiom_spec_len(slice: &[T]) admit(); } -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(spec_slice_len)] -pub fn slice_len(slice: &[T]) -> (len: usize) +pub assume_specification[ <[T]>::len ](slice: &[T]) -> (len: usize) ensures len == spec_slice_len(slice), -{ - slice.len() -} +; #[cfg(feature = "alloc")] #[verifier::external_body] diff --git a/examples/verus-snapshot/source/vstd/std_specs/atomic.rs b/examples/verus-snapshot/source/vstd/std_specs/atomic.rs index c13abab..6bf4e6a 100644 --- a/examples/verus-snapshot/source/vstd/std_specs/atomic.rs +++ b/examples/verus-snapshot/source/vstd/std_specs/atomic.rs @@ -15,90 +15,56 @@ macro_rules! atomic_specs_common { #[verifier::external_body] pub struct ExAtomic($at); - #[verifier::external_fn_specification] - pub fn ex_new(v: $ty) -> $at { - <$at>::new(v) - } + verus!{ + + pub assume_specification [ <$at>::new ](v: $ty) -> $at; - #[verifier::external_fn_specification] - pub fn ex_compare_exchange( + pub assume_specification [ <$at>::compare_exchange ]( atomic: &$at, current: $ty, new: $ty, success: Ordering, failure: Ordering, - ) -> Result<$ty, $ty> { - atomic.compare_exchange(current, new, success, failure) - } + ) -> Result<$ty, $ty>; - #[verifier::external_fn_specification] - pub fn ex_compare_exchange_weak( + pub assume_specification [ <$at>::compare_exchange_weak ]( atomic: &$at, current: $ty, new: $ty, success: Ordering, failure: Ordering, - ) -> Result<$ty, $ty> { - atomic.compare_exchange_weak(current, new, success, failure) - } + ) -> Result<$ty, $ty>; - #[verifier::external_fn_specification] - pub fn ex_fetch_and(atomic: &$at, val: $ty, order: Ordering) -> $ty { - atomic.fetch_and(val, order) - } + pub assume_specification [ <$at>::fetch_and ](atomic: &$at, val: $ty, order: Ordering) -> $ty; - #[verifier::external_fn_specification] - pub fn ex_fetch_nand(atomic: &$at, val: $ty, order: Ordering) -> $ty { - atomic.fetch_nand(val, order) - } + pub assume_specification [ <$at>::fetch_nand ](atomic: &$at, val: $ty, order: Ordering) -> $ty; - #[verifier::external_fn_specification] - pub fn ex_fetch_or(atomic: &$at, val: $ty, order: Ordering) -> $ty { - atomic.fetch_or(val, order) - } + pub assume_specification [ <$at>::fetch_or ](atomic: &$at, val: $ty, order: Ordering) -> $ty; - #[verifier::external_fn_specification] - pub fn ex_fetch_xor(atomic: &$at, val: $ty, order: Ordering) -> $ty { - atomic.fetch_xor(val, order) - } + pub assume_specification [ <$at>::fetch_xor ](atomic: &$at, val: $ty, order: Ordering) -> $ty; - #[verifier::external_fn_specification] - pub fn ex_load(atomic: &$at, order: Ordering) -> $ty { - atomic.load(order) - } + pub assume_specification [ <$at>::load ](atomic: &$at, order: Ordering) -> $ty; - #[verifier::external_fn_specification] - pub fn ex_store(atomic: &$at, val: $ty, order: Ordering) { - atomic.store(val, order) - } + pub assume_specification [ <$at>::store ](atomic: &$at, val: $ty, order: Ordering); + + pub assume_specification [ <$at>::swap ](atomic: &$at, val: $ty, order: Ordering) -> $ty; - #[verifier::external_fn_specification] - pub fn ex_swap(atomic: &$at, val: $ty, order: Ordering) -> $ty { - atomic.swap(val, order) } }; } macro_rules! atomic_specs_int_specific { ($at:ty, $ty:ty) => { - #[verifier::external_fn_specification] - pub fn ex_fetch_add(atomic: &$at, val: $ty, order: Ordering) -> $ty { - atomic.fetch_add(val, order) - } + verus!{ - #[verifier::external_fn_specification] - pub fn ex_fetch_sub(atomic: &$at, val: $ty, order: Ordering) -> $ty { - atomic.fetch_sub(val, order) - } + pub assume_specification [ <$at>::fetch_add ](atomic: &$at, val: $ty, order: Ordering) -> $ty; - #[verifier::external_fn_specification] - pub fn ex_fetch_min(atomic: &$at, val: $ty, order: Ordering) -> $ty { - atomic.fetch_min(val, order) - } + pub assume_specification [ <$at>::fetch_sub ](atomic: &$at, val: $ty, order: Ordering) -> $ty; + + pub assume_specification [ <$at>::fetch_min ](atomic: &$at, val: $ty, order: Ordering) -> $ty; + + pub assume_specification [ <$at>::fetch_max ](atomic: &$at, val: $ty, order: Ordering) -> $ty; - #[verifier::external_fn_specification] - pub fn ex_fetch_max(atomic: &$at, val: $ty, order: Ordering) -> $ty { - atomic.fetch_max(val, order) } }; } diff --git a/examples/verus-snapshot/source/vstd/std_specs/bits.rs b/examples/verus-snapshot/source/vstd/std_specs/bits.rs index 686d688..98ef81b 100644 --- a/examples/verus-snapshot/source/vstd/std_specs/bits.rs +++ b/examples/verus-snapshot/source/vstd/std_specs/bits.rs @@ -44,41 +44,29 @@ pub open spec fn u8_leading_ones(i: u8) -> u32 { u8_leading_zeros(!i) } -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(u8_trailing_zeros)] -pub fn ex_u8_trailing_zeros(i: u8) -> (r: u32) +pub assume_specification[ u8::trailing_zeros ](i: u8) -> (r: u32) ensures r == u8_trailing_zeros(i), -{ - i.trailing_zeros() -} +; -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(u8_trailing_ones)] -pub fn ex_u8_trailing_ones(i: u8) -> (r: u32) +pub assume_specification[ u8::trailing_ones ](i: u8) -> (r: u32) ensures r == u8_trailing_ones(i), -{ - i.trailing_ones() -} +; -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(u8_leading_zeros)] -pub fn ex_u8_leading_zeros(i: u8) -> (r: u32) +pub assume_specification[ u8::leading_zeros ](i: u8) -> (r: u32) ensures r == u8_leading_zeros(i), -{ - i.leading_zeros() -} +; -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(u8_leading_ones)] -pub fn ex_u8_leading_ones(i: u8) -> (r: u32) +pub assume_specification[ u8::leading_ones ](i: u8) -> (r: u32) ensures r == u8_leading_ones(i), -{ - i.leading_ones() -} +; pub broadcast proof fn axiom_u8_trailing_zeros(i: u8) ensures @@ -226,41 +214,29 @@ pub open spec fn u16_leading_ones(i: u16) -> u32 { u16_leading_zeros(!i) } -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(u16_trailing_zeros)] -pub fn ex_u16_trailing_zeros(i: u16) -> (r: u32) +pub assume_specification[ u16::trailing_zeros ](i: u16) -> (r: u32) ensures r == u16_trailing_zeros(i), -{ - i.trailing_zeros() -} +; -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(u16_trailing_ones)] -pub fn ex_u16_trailing_ones(i: u16) -> (r: u32) +pub assume_specification[ u16::trailing_ones ](i: u16) -> (r: u32) ensures r == u16_trailing_ones(i), -{ - i.trailing_ones() -} +; -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(u16_leading_zeros)] -pub fn ex_u16_leading_zeros(i: u16) -> (r: u32) +pub assume_specification[ u16::leading_zeros ](i: u16) -> (r: u32) ensures r == u16_leading_zeros(i), -{ - i.leading_zeros() -} +; -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(u16_leading_ones)] -pub fn ex_u16_leading_ones(i: u16) -> (r: u32) +pub assume_specification[ u16::leading_ones ](i: u16) -> (r: u32) ensures r == u16_leading_ones(i), -{ - i.leading_ones() -} +; pub broadcast proof fn axiom_u16_trailing_zeros(i: u16) ensures @@ -414,41 +390,29 @@ pub open spec fn u32_leading_ones(i: u32) -> u32 { u32_leading_zeros(!i) } -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(u32_trailing_zeros)] -pub fn ex_u32_trailing_zeros(i: u32) -> (r: u32) +pub assume_specification[ u32::trailing_zeros ](i: u32) -> (r: u32) ensures r == u32_trailing_zeros(i), -{ - i.trailing_zeros() -} +; -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(u32_trailing_ones)] -pub fn ex_u32_trailing_ones(i: u32) -> (r: u32) +pub assume_specification[ u32::trailing_ones ](i: u32) -> (r: u32) ensures r == u32_trailing_ones(i), -{ - i.trailing_ones() -} +; -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(u32_leading_zeros)] -pub fn ex_u32_leading_zeros(i: u32) -> (r: u32) +pub assume_specification[ u32::leading_zeros ](i: u32) -> (r: u32) ensures r == u32_leading_zeros(i), -{ - i.leading_zeros() -} +; -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(u32_leading_ones)] -pub fn ex_u32_leading_ones(i: u32) -> (r: u32) +pub assume_specification[ u32::leading_ones ](i: u32) -> (r: u32) ensures r == u32_leading_ones(i), -{ - i.leading_ones() -} +; pub broadcast proof fn axiom_u32_trailing_zeros(i: u32) ensures @@ -603,41 +567,29 @@ pub open spec fn u64_leading_ones(i: u64) -> u32 { u64_leading_zeros(!i) as u32 } -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(u64_trailing_zeros)] -pub fn ex_u64_trailing_zeros(i: u64) -> (r: u32) +pub assume_specification[ u64::trailing_zeros ](i: u64) -> (r: u32) ensures r == u64_trailing_zeros(i), -{ - i.trailing_zeros() -} +; -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(u64_trailing_ones)] -pub fn ex_u64_trailing_ones(i: u64) -> (r: u32) +pub assume_specification[ u64::trailing_ones ](i: u64) -> (r: u32) ensures r == u64_trailing_ones(i), -{ - i.trailing_ones() -} +; -#[verifier::external_fn_specification] //#[verifier::when_used_as_spec(u64_leading_zeros)] -pub fn ex_u64_leading_zeros(i: u64) -> (r: u32) +pub assume_specification[ u64::leading_zeros ](i: u64) -> (r: u32) ensures r as int == u64_leading_zeros(i), -{ - i.leading_zeros() -} +; -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(u64_leading_ones)] -pub fn ex_u64_leading_ones(i: u64) -> (r: u32) +pub assume_specification[ u64::leading_ones ](i: u64) -> (r: u32) ensures r == u64_leading_ones(i), -{ - i.leading_ones() -} +; pub broadcast proof fn axiom_u64_trailing_zeros(i: u64) ensures diff --git a/examples/verus-snapshot/source/vstd/std_specs/clone.rs b/examples/verus-snapshot/source/vstd/std_specs/clone.rs index 1c282bb..2481d4d 100644 --- a/examples/verus-snapshot/source/vstd/std_specs/clone.rs +++ b/examples/verus-snapshot/source/vstd/std_specs/clone.rs @@ -18,30 +18,21 @@ pub fn ex_clone_clone_from(a: &mut T, b: &T) } */ -#[verifier::external_fn_specification] -pub fn ex_bool_clone(b: &bool) -> (res: bool) - ensures - res == b, -{ - b.clone() -} +pub assume_specification[ ::clone ](b: &bool) -> (res: bool) + returns + b, +; -#[verifier::external_fn_specification] -pub fn ex_char_clone(c: &char) -> (res: char) - ensures - res == c, -{ - c.clone() -} +pub assume_specification[ ::clone ](c: &char) -> (res: char) + returns + c, +; #[allow(suspicious_double_ref_op)] -#[verifier::external_fn_specification] -pub fn ex_ref_clone<'b, T: ?Sized, 'a>(b: &'a &'b T) -> (res: &'b T) +pub assume_specification<'b, T: ?Sized, 'a>[ <&'b T as Clone>::clone ](b: &'a &'b T) -> (res: &'b T) ensures res == b, -{ - b.clone() -} +; /* #[verifier::external_fn_specification] @@ -53,20 +44,16 @@ pub fn ex_bool_clone_from(dest: &mut bool, source: &bool) */ // Cloning a Tracked copies the underlying ghost T -#[verifier::external_fn_specification] -pub fn ex_tracked_clone(b: &Tracked) -> (res: Tracked) +pub assume_specification[ as Clone>::clone ](b: &Tracked) -> (res: Tracked< + T, +>) ensures res == b, -{ - b.clone() -} +; -#[verifier::external_fn_specification] -pub fn ex_ghost_clone(b: &Ghost) -> (res: Ghost) +pub assume_specification[ as Clone>::clone ](b: &Ghost) -> (res: Ghost) ensures res == b, -{ - b.clone() -} +; } // verus! diff --git a/examples/verus-snapshot/source/vstd/std_specs/control_flow.rs b/examples/verus-snapshot/source/vstd/std_specs/control_flow.rs index f37c843..cd42e26 100644 --- a/examples/verus-snapshot/source/vstd/std_specs/control_flow.rs +++ b/examples/verus-snapshot/source/vstd/std_specs/control_flow.rs @@ -15,8 +15,7 @@ pub struct ExControlFlow(ControlFlow); #[verifier::external_body] pub struct ExInfallible(Infallible); -#[verifier::external_fn_specification] -pub fn ex_result_branch(result: Result) -> (cf: ControlFlow< +pub assume_specification[ Result::::branch ](result: Result) -> (cf: ControlFlow< as Try>::Residual, as Try>::Output, >) @@ -25,12 +24,9 @@ pub fn ex_result_branch(result: Result) -> (cf: ControlFlow< Ok(v) => ControlFlow::Continue(v), Err(e) => ControlFlow::Break(Err(e)), }, -{ - result.branch() -} +; -#[verifier::external_fn_specification] -pub fn ex_option_branch(option: Option) -> (cf: ControlFlow< +pub assume_specification[ Option::::branch ](option: Option) -> (cf: ControlFlow< as Try>::Residual, as Try>::Output, >) @@ -39,18 +35,14 @@ pub fn ex_option_branch(option: Option) -> (cf: ControlFlow< Some(v) => ControlFlow::Continue(v), None => ControlFlow::Break(None), }, -{ - option.branch() -} +; -#[verifier::external_fn_specification] -pub fn ex_option_from_residual(option: Option) -> (option2: Option) +pub assume_specification[ Option::::from_residual ](option: Option) -> (option2: + Option) ensures option.is_none(), option2.is_none(), -{ - Option::from_residual(option) -} +; pub spec fn spec_from(value: T, ret: S) -> bool; @@ -61,19 +53,15 @@ pub broadcast proof fn spec_from_blanket_identity(t: T, s: T) admit(); } -#[verifier::external_fn_specification] -pub fn ex_result_from_residual>(result: Result) -> (result2: Result< - T, - F, ->) +pub assume_specification>[ Result::::from_residual ]( + result: Result, +) -> (result2: Result) ensures match (result, result2) { (Err(e), Err(e2)) => spec_from::(e, e2), _ => false, }, -{ - Result::from_residual(result) -} +; pub broadcast group group_control_flow_axioms { spec_from_blanket_identity, diff --git a/examples/verus-snapshot/source/vstd/std_specs/core.rs b/examples/verus-snapshot/source/vstd/std_specs/core.rs index 1a3f3a1..1740e12 100644 --- a/examples/verus-snapshot/source/vstd/std_specs/core.rs +++ b/examples/verus-snapshot/source/vstd/std_specs/core.rs @@ -90,16 +90,13 @@ pub trait ExStructural { type ExternalTraitSpecificationFor: Structural; } -#[verifier::external_fn_specification] -pub fn ex_swap(a: &mut T, b: &mut T) +pub assume_specification[ core::mem::swap:: ](a: &mut T, b: &mut T) ensures *a == *old(b), *b == *old(a), opens_invariants none no_unwind -{ - core::mem::swap(a, b) -} +; #[verifier::external_type_specification] #[verifier::accept_recursive_types(V)] @@ -115,14 +112,11 @@ pub open spec fn iter_into_iter_spec(i: I) -> I { i } -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(iter_into_iter_spec)] -pub fn ex_iter_into_iter(i: I) -> (r: I) +pub assume_specification[ I::into_iter ](i: I) -> (r: I) ensures r == i, -{ - i.into_iter() -} +; // I don't really expect this to be particularly useful; // this is mostly here because I wanted an easy way to test @@ -136,21 +130,15 @@ pub struct ExDuration(core::time::Duration); #[verifier::accept_recursive_types(V)] pub struct ExPhantomData(core::marker::PhantomData); -#[verifier::external_fn_specification] -pub fn ex_intrinsics_likely(b: bool) -> (c: bool) +pub assume_specification[ core::intrinsics::likely ](b: bool) -> (c: bool) ensures c == b, -{ - core::intrinsics::likely(b) -} +; -#[verifier::external_fn_specification] -pub fn ex_intrinsics_unlikely(b: bool) -> (c: bool) +pub assume_specification[ core::intrinsics::unlikely ](b: bool) -> (c: bool) ensures c == b, -{ - core::intrinsics::unlikely(b) -} +; #[verifier::external_type_specification] #[verifier::external_body] diff --git a/examples/verus-snapshot/source/vstd/std_specs/hash.rs b/examples/verus-snapshot/source/vstd/std_specs/hash.rs index 45200d1..09254f8 100644 --- a/examples/verus-snapshot/source/vstd/std_specs/hash.rs +++ b/examples/verus-snapshot/source/vstd/std_specs/hash.rs @@ -30,7 +30,8 @@ use core::borrow::Borrow; use core::hash::{BuildHasher, Hash, Hasher}; use core::option::Option; use core::option::Option::None; -use std::collections::hash_map::{DefaultHasher, RandomState}; +use std::collections::hash_map::{DefaultHasher, Keys, RandomState}; +use std::collections::hash_set::Iter; use std::collections::{HashMap, HashSet}; verus! { @@ -61,31 +62,22 @@ impl DefaultHasherAdditionalSpecFns for DefaultHasher { } // This is the specification of behavior for `DefaultHasher::new()`. -#[verifier::external_fn_specification] -pub fn ex_default_hasher_new() -> (result: DefaultHasher) +pub assume_specification[ DefaultHasher::new ]() -> (result: DefaultHasher) ensures result@ == Seq::>::empty(), -{ - DefaultHasher::new() -} +; // This is the specification of behavior for `DefaultHasher::write(&[u8])`. -#[verifier::external_fn_specification] -pub fn ex_default_hasher_write(state: &mut DefaultHasher, bytes: &[u8]) +pub assume_specification[ DefaultHasher::write ](state: &mut DefaultHasher, bytes: &[u8]) ensures state@ == old(state)@.push(bytes@), -{ - state.write(bytes) -} +; // This is the specification of behavior for `DefaultHasher::finish()`. -#[verifier::external_fn_specification] -pub fn ex_default_hasher_finish(state: &DefaultHasher) -> (result: u64) +pub assume_specification[ DefaultHasher::finish ](state: &DefaultHasher) -> (result: u64) ensures result == DefaultHasher::spec_finish(state@), -{ - state.finish() -} +; // This function specifies whether a type obeys the requirements // to be a key in a hash table and have that hash table conform to our @@ -95,7 +87,7 @@ pub fn ex_default_hasher_finish(state: &DefaultHasher) -> (result: u64) // isn't satisfied by having `Key` implement `Hash`, since this trait // doesn't mandate determinism. #[verifier::external_body] -pub spec fn obeys_key_model() -> bool; +pub closed spec fn obeys_key_model() -> bool; // These axioms state that any primitive type, or `Box` thereof, // obeys the requirements to be a key in a hash table that @@ -143,6 +135,13 @@ pub broadcast proof fn axiom_u128_obeys_hash_table_key_model() admit(); } +pub broadcast proof fn axiom_usize_obeys_hash_table_key_model() + ensures + #[trigger] obeys_key_model::(), +{ + admit(); +} + pub broadcast proof fn axiom_i8_obeys_hash_table_key_model() ensures #[trigger] obeys_key_model::(), @@ -178,6 +177,13 @@ pub broadcast proof fn axiom_i128_obeys_hash_table_key_model() admit(); } +pub broadcast proof fn axiom_isize_obeys_hash_table_key_model() + ensures + #[trigger] obeys_key_model::(), +{ + admit(); +} + pub broadcast proof fn axiom_box_bool_obeys_hash_table_key_model() ensures #[trigger] obeys_key_model::>(), @@ -215,7 +221,7 @@ pub trait ExBuildHasher { } #[verifier::external_body] -pub spec fn builds_valid_hashers() -> bool; +pub closed spec fn builds_valid_hashers() -> bool; // A commonly used type of trait `BuildHasher` is `RandomState`. We // model that type here. In particular, we have an axiom that @@ -231,11 +237,120 @@ pub broadcast proof fn axiom_random_state_builds_valid_hashers() admit(); } +// The `keys` method of a `HashMap` returns an iterator of type `Keys`, +// so we specify that type here. +#[verifier::external_type_specification] +#[verifier::external_body] +#[verifier::accept_recursive_types(Key)] +#[verifier::accept_recursive_types(Value)] +pub struct ExKeys<'a, Key: 'a, Value: 'a>(Keys<'a, Key, Value>); + +pub trait KeysAdditionalSpecFns<'a, Key: 'a, Value: 'a> { + spec fn view(self: &Self) -> (int, Seq); +} + +impl<'a, Key: 'a, Value: 'a> KeysAdditionalSpecFns<'a, Key, Value> for Keys<'a, Key, Value> { + spec fn view(self: &Keys<'a, Key, Value>) -> (int, Seq); +} + +pub assume_specification<'a, Key, Value>[ Keys::<'a, Key, Value>::next ]( + keys: &mut Keys<'a, Key, Value>, +) -> (r: Option<&'a Key>) + ensures + ({ + let (old_index, old_seq) = old(keys)@; + match r { + None => { + &&& keys@ == old(keys)@ + &&& old_index >= old_seq.len() + }, + Some(k) => { + let (new_index, new_seq) = keys@; + &&& 0 <= old_index < old_seq.len() + &&& new_seq == old_seq + &&& new_index == old_index + 1 + &&& k == old_seq[old_index] + }, + } + }), +; + +pub struct KeysGhostIterator<'a, Key, Value> { + pub pos: int, + pub keys: Seq, + pub phantom: Option<&'a Value>, +} + +impl<'a, Key, Value> super::super::pervasive::ForLoopGhostIteratorNew for Keys<'a, Key, Value> { + type GhostIter = KeysGhostIterator<'a, Key, Value>; + + open spec fn ghost_iter(&self) -> KeysGhostIterator<'a, Key, Value> { + KeysGhostIterator { pos: self@.0, keys: self@.1, phantom: None } + } +} + +impl<'a, Key: 'a, Value: 'a> super::super::pervasive::ForLoopGhostIterator for KeysGhostIterator< + 'a, + Key, + Value, +> { + type ExecIter = Keys<'a, Key, Value>; + + type Item = Key; + + type Decrease = int; + + open spec fn exec_invariant(&self, exec_iter: &Keys<'a, Key, Value>) -> bool { + &&& self.pos == exec_iter@.0 + &&& self.keys == exec_iter@.1 + } + + open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool { + init matches Some(init) ==> { + &&& init.pos == 0 + &&& init.keys == self.keys + &&& 0 <= self.pos <= self.keys.len() + } + } + + open spec fn ghost_ensures(&self) -> bool { + self.pos == self.keys.len() + } + + open spec fn ghost_decrease(&self) -> Option { + Some(self.keys.len() - self.pos) + } + + open spec fn ghost_peek_next(&self) -> Option { + if 0 <= self.pos < self.keys.len() { + Some(self.keys[self.pos]) + } else { + None + } + } + + open spec fn ghost_advance(&self, _exec_iter: &Keys<'a, Key, Value>) -> KeysGhostIterator< + 'a, + Key, + Value, + > { + Self { pos: self.pos + 1, ..*self } + } +} + +impl<'a, Key, Value> View for KeysGhostIterator<'a, Key, Value> { + type V = Seq; + + open spec fn view(&self) -> Seq { + self.keys.take(self.pos) + } +} + // We now specify the behavior of `HashMap`. #[verifier::external_type_specification] #[verifier::external_body] -#[verifier::reject_recursive_types(Key)] -#[verifier::reject_recursive_types(Value)] +#[verifier::accept_recursive_types(Key)] +#[verifier::accept_recursive_types(Value)] #[verifier::reject_recursive_types(S)] pub struct ExHashMap(HashMap); @@ -270,52 +385,43 @@ pub broadcast proof fn axiom_spec_hash_map_len(m: &HashMap(m: &HashMap) -> (len: usize) +pub assume_specification[ HashMap::::len ]( + m: &HashMap, +) -> (len: usize) ensures len == spec_hash_map_len(m), -{ - m.len() -} +; -#[verifier::external_fn_specification] -pub fn ex_hash_map_new() -> (m: HashMap) - ensures - m@ == Map::::empty(), -{ - HashMap::::new() -} - -#[verifier::external_fn_specification] -pub fn ex_hash_map_with_capacity(capacity: usize) -> (m: HashMap< +pub assume_specification[ HashMap::::new ]() -> (m: HashMap< Key, Value, RandomState, >) ensures m@ == Map::::empty(), -{ - HashMap::::with_capacity(capacity) -} +; -#[verifier::external_fn_specification] -pub fn ex_hash_map_reserve(m: &mut HashMap, additional: usize) where - Key: Eq + Hash, - S: BuildHasher, +pub assume_specification[ HashMap::::with_capacity ](capacity: usize) -> (m: + HashMap) + ensures + m@ == Map::::empty(), +; +pub assume_specification[ HashMap::< + Key, + Value, + S, +>::reserve ](m: &mut HashMap, additional: usize) ensures m@ == old(m)@, -{ - m.reserve(additional) -} +; -#[verifier::external_fn_specification] -pub fn ex_hash_map_insert( +pub assume_specification[ HashMap::::insert ]( m: &mut HashMap, k: Key, v: Value, -) -> (result: Option) where Key: Eq + Hash, S: BuildHasher +) -> (result: Option) ensures obeys_key_model::() && builds_valid_hashers::() ==> { &&& m@ == old(m)@.insert(k, v) @@ -324,9 +430,7 @@ pub fn ex_hash_map_insert( None => !old(m)@.contains_key(k), } }, -{ - m.insert(k, v) -} +; // The specification for `contains_key` has a parameter `key: &Q` // where you'd expect to find `key: &Key`. This allows for the case @@ -360,17 +464,19 @@ pub broadcast proof fn axiom_contains_box(m: Map, Value>, k: &Q admit(); } -#[verifier::external_fn_specification] -pub fn ex_hash_contains_key(m: &HashMap, k: &Q) -> (result: - bool) where Key: Borrow + Hash + Eq, Q: Hash + Eq + ?Sized, S: BuildHasher +pub assume_specification< + Key: Borrow + Hash + Eq, + Value, + S: BuildHasher, + Q: Hash + Eq + ?Sized, +>[ HashMap::::contains_key:: ](m: &HashMap, k: &Q) -> (result: + bool) ensures obeys_key_model::() && builds_valid_hashers::() ==> result == contains_borrowed_key( m@, k, ), -{ - m.contains_key(k) -} +; // The specification for `get` has a parameter `key: &Q` where you'd // expect to find `key: &Key`. This allows for the case that `Key` can @@ -413,17 +519,21 @@ pub broadcast proof fn axiom_maps_box_key_to_value(m: Map, Valu admit(); } -#[verifier::external_fn_specification] -pub fn ex_hash_map_get<'a, Key, Value, S, Q>(m: &'a HashMap, k: &Q) -> (result: - Option<&'a Value>) where Key: Borrow + Hash + Eq, Q: Hash + Eq + ?Sized, S: BuildHasher +pub assume_specification< + 'a, + Key: Borrow + Hash + Eq, + Value, + S: BuildHasher, + Q: Hash + Eq + ?Sized, +>[ HashMap::::get:: ](m: &'a HashMap, k: &Q) -> (result: Option< + &'a Value, +>) ensures obeys_key_model::() && builds_valid_hashers::() ==> match result { Some(v) => maps_borrowed_key_to_value(m@, k, *v), None => !contains_borrowed_key(m@, k), }, -{ - m.get(k) -} +; // The specification for `remove` has a parameter `key: &Q` where // you'd expect to find `key: &Key`. This allows for the case that @@ -471,9 +581,13 @@ pub broadcast proof fn axiom_box_key_removed( admit(); } -#[verifier::external_fn_specification] -pub fn ex_hash_map_remove(m: &mut HashMap, k: &Q) -> (result: - Option) where Key: Borrow + Hash + Eq, Q: Hash + Eq + ?Sized, S: BuildHasher +pub assume_specification< + Key: Borrow + Hash + Eq, + Value, + S: BuildHasher, + Q: Hash + Eq + ?Sized, +>[ HashMap::::remove:: ](m: &mut HashMap, k: &Q) -> (result: + Option) ensures obeys_key_model::() && builds_valid_hashers::() ==> { &&& borrowed_key_removed(old(m)@, m@, k) @@ -482,22 +596,130 @@ pub fn ex_hash_map_remove(m: &mut HashMap, k: & None => !contains_borrowed_key(old(m)@, k), } }, -{ - m.remove(k) -} +; -#[verifier::external_fn_specification] -pub fn ex_hash_map_clear(m: &mut HashMap) +pub assume_specification[ HashMap::::clear ]( + m: &mut HashMap, +) ensures m@ == Map::::empty(), -{ - m.clear() +; + +pub assume_specification<'a, Key, Value, S>[ HashMap::::keys ]( + m: &'a HashMap, +) -> (keys: Keys<'a, Key, Value>) + ensures + obeys_key_model::() && builds_valid_hashers::() ==> { + let (index, s) = keys@; + &&& index == 0 + &&& s.to_set() == m@.dom() + &&& s.no_duplicates() + }, +; + +// The `iter` method of a `HashSet` returns an iterator of type `Iter`, +// so we specify that type here. +#[verifier::external_type_specification] +#[verifier::external_body] +#[verifier::accept_recursive_types(Key)] +pub struct ExIter<'a, Key: 'a>(Iter<'a, Key>); + +pub trait IterAdditionalSpecFns<'a, Key: 'a> { + spec fn view(self: &Self) -> (int, Seq); +} + +impl<'a, Key: 'a> IterAdditionalSpecFns<'a, Key> for Iter<'a, Key> { + spec fn view(self: &Iter<'a, Key>) -> (int, Seq); +} + +pub assume_specification<'a, Key>[ Iter::<'a, Key>::next ](elements: &mut Iter<'a, Key>) -> (r: + Option<&'a Key>) + ensures + ({ + let (old_index, old_seq) = old(elements)@; + match r { + None => { + &&& elements@ == old(elements)@ + &&& old_index >= old_seq.len() + }, + Some(element) => { + let (new_index, new_seq) = elements@; + &&& 0 <= old_index < old_seq.len() + &&& new_seq == old_seq + &&& new_index == old_index + 1 + &&& element == old_seq[old_index] + }, + } + }), +; + +pub struct IterGhostIterator<'a, Key> { + pub pos: int, + pub elements: Seq, + pub phantom: Option<&'a Key>, +} + +impl<'a, Key> super::super::pervasive::ForLoopGhostIteratorNew for Iter<'a, Key> { + type GhostIter = IterGhostIterator<'a, Key>; + + open spec fn ghost_iter(&self) -> IterGhostIterator<'a, Key> { + IterGhostIterator { pos: self@.0, elements: self@.1, phantom: None } + } +} + +impl<'a, Key: 'a> super::super::pervasive::ForLoopGhostIterator for IterGhostIterator<'a, Key> { + type ExecIter = Iter<'a, Key>; + + type Item = Key; + + type Decrease = int; + + open spec fn exec_invariant(&self, exec_iter: &Iter<'a, Key>) -> bool { + &&& self.pos == exec_iter@.0 + &&& self.elements == exec_iter@.1 + } + + open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool { + init matches Some(init) ==> { + &&& init.pos == 0 + &&& init.elements == self.elements + &&& 0 <= self.pos <= self.elements.len() + } + } + + open spec fn ghost_ensures(&self) -> bool { + self.pos == self.elements.len() + } + + open spec fn ghost_decrease(&self) -> Option { + Some(self.elements.len() - self.pos) + } + + open spec fn ghost_peek_next(&self) -> Option { + if 0 <= self.pos < self.elements.len() { + Some(self.elements[self.pos]) + } else { + None + } + } + + open spec fn ghost_advance(&self, _exec_iter: &Iter<'a, Key>) -> IterGhostIterator<'a, Key> { + Self { pos: self.pos + 1, ..*self } + } +} + +impl<'a, Key> View for IterGhostIterator<'a, Key> { + type V = Seq; + + open spec fn view(&self) -> Seq { + self.elements.take(self.pos) + } } // We now specify the behavior of `HashSet`. #[verifier::external_type_specification] #[verifier::external_body] -#[verifier::reject_recursive_types(Key)] +#[verifier::accept_recursive_types(Key)] #[verifier::reject_recursive_types(S)] pub struct ExHashSet(HashSet); @@ -518,55 +740,43 @@ pub broadcast proof fn axiom_spec_hash_set_len(m: &HashSet) admit(); } -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(spec_hash_set_len)] -pub fn ex_hash_set_len(m: &HashSet) -> (len: usize) +pub assume_specification[ HashSet::::len ](m: &HashSet) -> (len: usize) ensures len == spec_hash_set_len(m), -{ - m.len() -} +; -#[verifier::external_fn_specification] -pub fn ex_hash_set_new() -> (m: HashSet) +pub assume_specification[ HashSet::::new ]() -> (m: HashSet) ensures m@ == Set::::empty(), -{ - HashSet::::new() -} +; -#[verifier::external_fn_specification] -pub fn ex_hash_set_with_capacity(capacity: usize) -> (m: HashSet) +pub assume_specification[ HashSet::::with_capacity ](capacity: usize) -> (m: HashSet< + Key, + RandomState, +>) ensures m@ == Set::::empty(), -{ - HashSet::::with_capacity(capacity) -} - -#[verifier::external_fn_specification] -pub fn ex_hash_set_reserve(m: &mut HashSet, additional: usize) where - Key: Eq + Hash, - S: BuildHasher, +; +pub assume_specification[ HashSet::::reserve ]( + m: &mut HashSet, + additional: usize, +) ensures m@ == old(m)@, -{ - m.reserve(additional) -} - -#[verifier::external_fn_specification] -pub fn ex_hash_set_insert(m: &mut HashSet, k: Key) -> (result: bool) where - Key: Eq + Hash, - S: BuildHasher, +; +pub assume_specification[ HashSet::::insert ]( + m: &mut HashSet, + k: Key, +) -> (result: bool) ensures obeys_key_model::() && builds_valid_hashers::() ==> { &&& m@ == old(m)@.insert(k) &&& result == !old(m)@.contains(k) }, -{ - m.insert(k) -} +; // The specification for `contains` has a parameter `key: &Q` // where you'd expect to find `key: &Key`. This allows for the case @@ -598,18 +808,15 @@ pub broadcast proof fn axiom_set_contains_box(m: Set>, k: &Q) admit(); } -#[verifier::external_fn_specification] -pub fn ex_hash_set_contains(m: &HashSet, k: &Q) -> (result: bool) where +pub assume_specification< Key: Borrow + Hash + Eq, - Q: Hash + Eq + ?Sized, S: BuildHasher, - + Q: Hash + Eq + ?Sized, +>[ HashSet::::contains ](m: &HashSet, k: &Q) -> (result: bool) ensures obeys_key_model::() && builds_valid_hashers::() ==> result == set_contains_borrowed_key(m@, k), -{ - m.contains(k) -} +; // The specification for `get` has a parameter `key: &Q` where you'd // expect to find `key: &Key`. This allows for the case that `Key` can @@ -645,18 +852,18 @@ pub broadcast proof fn axiom_set_box_key_to_value(m: Set>, q: &Q, v: & admit(); } -#[verifier::external_fn_specification] -pub fn ex_hash_set_get<'a, Key, S, Q>(m: &'a HashSet, k: &Q) -> (result: Option< - &'a Key, ->) where Key: Borrow + Hash + Eq, Q: Hash + Eq + ?Sized, S: BuildHasher +pub assume_specification< + 'a, + Key: Borrow + Hash + Eq, + S: BuildHasher, + Q: Hash + Eq + ?Sized, +>[ HashSet::::get:: ](m: &'a HashSet, k: &Q) -> (result: Option<&'a Key>) ensures obeys_key_model::() && builds_valid_hashers::() ==> match result { Some(v) => sets_borrowed_key_to_key(m@, k, v), None => !set_contains_borrowed_key(m@, k), }, -{ - m.get(k) -} +; // The specification for `remove` has a parameter `key: &Q` where // you'd expect to find `key: &Key`. This allows for the case that @@ -695,28 +902,35 @@ pub broadcast proof fn axiom_set_box_key_removed(old_m: Set>, new_m: S admit(); } -#[verifier::external_fn_specification] -pub fn ex_hash_set_remove(m: &mut HashSet, k: &Q) -> (result: bool) where +pub assume_specification< Key: Borrow + Hash + Eq, - Q: Hash + Eq + ?Sized, S: BuildHasher, - + Q: Hash + Eq + ?Sized, +>[ HashSet::::remove:: ](m: &mut HashSet, k: &Q) -> (result: bool) ensures obeys_key_model::() && builds_valid_hashers::() ==> { &&& sets_differ_by_borrowed_key(old(m)@, m@, k) &&& result == set_contains_borrowed_key(old(m)@, k) }, -{ - m.remove(k) -} +; -#[verifier::external_fn_specification] -pub fn ex_hash_set_clear(m: &mut HashSet) +pub assume_specification[ HashSet::::clear ](m: &mut HashSet) ensures m@ == Set::::empty(), -{ - m.clear() -} +; + +pub assume_specification<'a, Key, S>[ HashSet::::iter ](m: &'a HashSet) -> (r: Iter< + 'a, + Key, +>) + ensures + obeys_key_model::() && builds_valid_hashers::() ==> { + let (index, s) = r@; + &&& index == 0 + &&& s.to_set() == m@ + &&& s.no_duplicates() + }, +; pub broadcast group group_hash_axioms { axiom_box_key_removed, @@ -731,11 +945,13 @@ pub broadcast group group_hash_axioms { axiom_u32_obeys_hash_table_key_model, axiom_u64_obeys_hash_table_key_model, axiom_u128_obeys_hash_table_key_model, + axiom_usize_obeys_hash_table_key_model, axiom_i8_obeys_hash_table_key_model, axiom_i16_obeys_hash_table_key_model, axiom_i32_obeys_hash_table_key_model, axiom_i164_obeys_hash_table_key_model, axiom_i128_obeys_hash_table_key_model, + axiom_isize_obeys_hash_table_key_model, axiom_box_bool_obeys_hash_table_key_model, axiom_box_integer_type_obeys_hash_table_key_model, axiom_random_state_builds_valid_hashers, diff --git a/examples/verus-snapshot/source/vstd/std_specs/mod.rs b/examples/verus-snapshot/source/vstd/std_specs/mod.rs index bc3a84f..c61cbe5 100644 --- a/examples/verus-snapshot/source/vstd/std_specs/mod.rs +++ b/examples/verus-snapshot/source/vstd/std_specs/mod.rs @@ -17,3 +17,7 @@ pub mod vec; #[cfg(feature = "alloc")] pub mod smart_ptrs; + +// This struct is a hack that exists purely to create +// a rustdoc page dedicated to 'assume_specification' specs +pub struct VstdSpecsForRustStdLib; diff --git a/examples/verus-snapshot/source/vstd/std_specs/num.rs b/examples/verus-snapshot/source/vstd/std_specs/num.rs index 9398176..9163803 100644 --- a/examples/verus-snapshot/source/vstd/std_specs/num.rs +++ b/examples/verus-snapshot/source/vstd/std_specs/num.rs @@ -12,12 +12,8 @@ macro_rules! num_specs { mod $modname_u { use super::*; - #[verifier::external_fn_specification] - pub fn ex_num_clone(x: &$uN) -> (res: $uN) - ensures res == x, - { - x.clone() - } + pub assume_specification[<$uN as Clone>::clone](x: &$uN) -> (res: $uN) + ensures res == x; pub open spec fn wrapping_add(x: $uN, y: $uN) -> $uN { if x + y > <$uN>::MAX { @@ -27,13 +23,9 @@ macro_rules! num_specs { } } - #[verifier::external_fn_specification] #[verifier::when_used_as_spec(wrapping_add)] - pub fn ex_wrapping_add(x: $uN, y: $uN) -> (res: $uN) - ensures res == wrapping_add(x, y) - { - x.wrapping_add(y) - } + pub assume_specification[<$uN>::wrapping_add](x: $uN, y: $uN) -> (res: $uN) + ensures res == wrapping_add(x, y); pub open spec fn wrapping_add_signed(x: $uN, y: $iN) -> $uN { if x + y > <$uN>::MAX { @@ -45,13 +37,9 @@ macro_rules! num_specs { } } - #[verifier::external_fn_specification] #[verifier::when_used_as_spec(wrapping_add_signed)] - pub fn ex_wrapping_add_signed(x: $uN, y: $iN) -> (res: $uN) - ensures res == wrapping_add_signed(x, y) - { - x.wrapping_add_signed(y) - } + pub assume_specification[<$uN>::wrapping_add_signed](x: $uN, y: $iN) -> (res: $uN) + ensures res == wrapping_add_signed(x, y); pub open spec fn wrapping_sub(x: $uN, y: $uN) -> $uN { if x - y < 0 { @@ -61,13 +49,9 @@ macro_rules! num_specs { } } - #[verifier::external_fn_specification] #[verifier::when_used_as_spec(wrapping_sub)] - pub fn ex_wrapping_sub(x: $uN, y: $uN) -> (res: $uN) - ensures res == wrapping_sub(x, y) - { - x.wrapping_sub(y) - } + pub assume_specification[<$uN>::wrapping_sub](x: $uN, y: $uN) -> (res: $uN) + ensures res == wrapping_sub(x, y); pub open spec fn checked_add(x: $uN, y: $uN) -> Option<$uN> { if x + y > <$uN>::MAX { @@ -77,13 +61,9 @@ macro_rules! num_specs { } } - #[verifier::external_fn_specification] #[verifier::when_used_as_spec(checked_add)] - pub fn ex_checked_add(x: $uN, y: $uN) -> (res: Option<$uN>) - ensures res == checked_add(x, y) - { - x.checked_add(y) - } + pub assume_specification[<$uN>::checked_add](x: $uN, y: $uN) -> (res: Option<$uN>) + ensures res == checked_add(x, y); pub open spec fn checked_add_signed(x: $uN, y: $iN) -> Option<$uN> { if x + y > <$uN>::MAX || x + y < 0 { @@ -93,13 +73,9 @@ macro_rules! num_specs { } } - #[verifier::external_fn_specification] #[verifier::when_used_as_spec(checked_add_signed)] - pub fn ex_checked_add_signed(x: $uN, y: $iN) -> (res: Option<$uN>) - ensures res == checked_add_signed(x, y) - { - x.checked_add_signed(y) - } + pub assume_specification[<$uN>::checked_add_signed](x: $uN, y: $iN) -> (res: Option<$uN>) + ensures res == checked_add_signed(x, y); pub open spec fn checked_sub(x: $uN, y: $uN) -> Option<$uN> { if x - y < 0 { @@ -109,13 +85,9 @@ macro_rules! num_specs { } } - #[verifier::external_fn_specification] #[verifier::when_used_as_spec(checked_sub)] - pub fn ex_checked_sub(x: $uN, y: $uN) -> (res: Option<$uN>) - ensures res == checked_sub(x, y) - { - x.checked_sub(y) - } + pub assume_specification[<$uN>::checked_sub](x: $uN, y: $uN) -> (res: Option<$uN>) + ensures res == checked_sub(x, y); pub open spec fn checked_mul(x: $uN, y: $uN) -> Option<$uN> { if x * y > <$uN>::MAX { @@ -125,14 +97,10 @@ macro_rules! num_specs { } } - #[verifier::external_fn_specification] #[verifier::when_used_as_spec(checked_mul)] - pub fn ex_checked_mul(lhs: $uN, rhs: $uN) -> (result: Option<$uN>) + pub assume_specification[<$uN>::checked_mul](lhs: $uN, rhs: $uN) -> (result: Option<$uN>) ensures - result == checked_mul(lhs, rhs) - { - lhs.checked_mul(rhs) - } + result == checked_mul(lhs, rhs); pub open spec fn checked_div(x: $uN, y: $uN) -> Option<$uN> { if y == 0 { @@ -142,26 +110,16 @@ macro_rules! num_specs { } } - #[verifier::external_fn_specification] #[verifier::when_used_as_spec(checked_div)] - pub fn ex_checked_div(lhs: $uN, rhs: $uN) -> (result: Option<$uN>) + pub assume_specification[<$uN>::checked_div](lhs: $uN, rhs: $uN) -> (result: Option<$uN>) ensures - result == checked_div(lhs, rhs) - { - lhs.checked_div(rhs) - } + result == checked_div(lhs, rhs); - #[verifier::external_fn_specification] #[verifier::when_used_as_spec(checked_div)] - pub fn ex_checked_div_euclid(lhs: $uN, rhs: $uN) -> (result: Option<$uN>) + pub assume_specification[<$uN>::checked_div_euclid](lhs: $uN, rhs: $uN) -> (result: Option<$uN>) ensures // checked_div is the same as checked_div_euclid for unsigned ints - result == checked_div(lhs, rhs) - { - lhs.checked_div_euclid(rhs) - } - - + result == checked_div(lhs, rhs); } // Signed ints (i8, i16, etc.) @@ -169,12 +127,8 @@ macro_rules! num_specs { mod $modname_i { use super::*; - #[verifier::external_fn_specification] - pub fn ex_num_clone(x: &$iN) -> (res: $iN) - ensures res == x, - { - x.clone() - } + pub assume_specification[<$iN as Clone>::clone](x: &$iN) -> (res: $iN) + ensures res == x; pub open spec fn wrapping_add(x: $iN, y: $iN) -> $iN { if x + y > <$iN>::MAX { @@ -186,13 +140,9 @@ macro_rules! num_specs { } } - #[verifier::external_fn_specification] #[verifier::when_used_as_spec(wrapping_add)] - pub fn ex_wrapping_add(x: $iN, y: $iN) -> (res: $iN) - ensures res == wrapping_add(x, y) - { - x.wrapping_add(y) - } + pub assume_specification[<$iN>::wrapping_add](x: $iN, y: $iN) -> (res: $iN) + ensures res == wrapping_add(x, y); pub open spec fn wrapping_add_unsigned(x: $iN, y: $uN) -> $iN { if x + y > <$iN>::MAX { @@ -202,13 +152,9 @@ macro_rules! num_specs { } } - #[verifier::external_fn_specification] #[verifier::when_used_as_spec(wrapping_add_unsigned)] - pub fn ex_wrapping_add_unsigned(x: $iN, y: $uN) -> (res: $iN) - ensures res == wrapping_add_unsigned(x, y) - { - x.wrapping_add_unsigned(y) - } + pub assume_specification[<$iN>::wrapping_add_unsigned](x: $iN, y: $uN) -> (res: $iN) + ensures res == wrapping_add_unsigned(x, y); pub open spec fn wrapping_sub(x: $iN, y: $iN) -> $iN { if x - y > <$iN>::MAX { @@ -220,13 +166,9 @@ macro_rules! num_specs { } } - #[verifier::external_fn_specification] #[verifier::when_used_as_spec(wrapping_sub)] - pub fn ex_wrapping_sub(x: $iN, y: $iN) -> (res: $iN) - ensures res == wrapping_sub(x, y) - { - x.wrapping_sub(y) - } + pub assume_specification[<$iN>::wrapping_sub](x: $iN, y: $iN) -> (res: $iN) + ensures res == wrapping_sub(x, y); pub open spec fn signed_crop(x: int) -> $iN { if (x % ($range as int)) > (<$iN>::MAX as int) { @@ -240,13 +182,9 @@ macro_rules! num_specs { signed_crop(x * y) } - #[verifier::external_fn_specification] #[verifier::when_used_as_spec(wrapping_mul)] - pub fn ex_wrapping_mul(x: $iN, y: $iN) -> (res: $iN) - ensures res == wrapping_mul(x, y) - { - x.wrapping_mul(y) - } + pub assume_specification[<$iN>::wrapping_mul](x: $iN, y: $iN) -> (res: $iN) + ensures res == wrapping_mul(x, y); pub open spec fn checked_add(x: $iN, y: $iN) -> Option<$iN> { if x + y > <$iN>::MAX || x + y < <$iN>::MIN { @@ -256,13 +194,9 @@ macro_rules! num_specs { } } - #[verifier::external_fn_specification] #[verifier::when_used_as_spec(checked_add)] - pub fn ex_checked_add(x: $iN, y: $iN) -> (res: Option<$iN>) - ensures res == checked_add(x, y) - { - x.checked_add(y) - } + pub assume_specification[<$iN>::checked_add](x: $iN, y: $iN) -> (res: Option<$iN>) + ensures res == checked_add(x, y); pub open spec fn checked_add_unsigned(x: $iN, y: $uN) -> Option<$iN> { if x + y > <$iN>::MAX { @@ -272,13 +206,9 @@ macro_rules! num_specs { } } - #[verifier::external_fn_specification] #[verifier::when_used_as_spec(checked_add_unsigned)] - pub fn ex_checked_add_unsigned(x: $iN, y: $uN) -> (res: Option<$iN>) - ensures res == checked_add_unsigned(x, y) - { - x.checked_add_unsigned(y) - } + pub assume_specification[<$iN>::checked_add_unsigned](x: $iN, y: $uN) -> (res: Option<$iN>) + ensures res == checked_add_unsigned(x, y); pub open spec fn saturating_add(x: $uN, y: $uN) -> $uN { if x + y > <$uN>::MAX { @@ -288,13 +218,9 @@ macro_rules! num_specs { } } - #[verifier::external_fn_specification] #[verifier::when_used_as_spec(saturating_add)] - pub fn ex_saturating_add(x: $uN, y: $uN) -> (res: $uN) - ensures res == saturating_add(x, y) - { - x.saturating_add(y) - } + pub assume_specification[<$uN>::saturating_add](x: $uN, y: $uN) -> (res: $uN) + ensures res == saturating_add(x, y); pub open spec fn checked_sub(x: $iN, y: $iN) -> Option<$iN> { if x - y > <$iN>::MAX || x - y < <$iN>::MIN { @@ -304,13 +230,9 @@ macro_rules! num_specs { } } - #[verifier::external_fn_specification] #[verifier::when_used_as_spec(checked_sub)] - pub fn ex_checked_sub(x: $iN, y: $iN) -> (res: Option<$iN>) - ensures res == checked_sub(x, y) - { - x.checked_sub(y) - } + pub assume_specification[<$iN>::checked_sub](x: $iN, y: $iN) -> (res: Option<$iN>) + ensures res == checked_sub(x, y); pub open spec fn checked_sub_unsigned(x: $iN, y: $uN) -> Option<$iN> { if x - y < <$iN>::MIN { @@ -320,13 +242,9 @@ macro_rules! num_specs { } } - #[verifier::external_fn_specification] #[verifier::when_used_as_spec(checked_sub_unsigned)] - pub fn ex_checked_sub_unsigned(x: $iN, y: $uN) -> (res: Option<$iN>) - ensures res == checked_sub_unsigned(x, y) - { - x.checked_sub_unsigned(y) - } + pub assume_specification[<$iN>::checked_sub_unsigned](x: $iN, y: $uN) -> (res: Option<$iN>) + ensures res == checked_sub_unsigned(x, y); pub open spec fn checked_mul(x: $iN, y: $iN) -> Option<$iN> { if x * y > <$iN>::MAX || x * y < <$iN>::MIN { @@ -336,13 +254,9 @@ macro_rules! num_specs { } } - #[verifier::external_fn_specification] #[verifier::when_used_as_spec(checked_mul)] - pub fn ex_checked_mul(x: $iN, y: $iN) -> (res: Option<$iN>) - ensures res == checked_mul(x, y) - { - x.checked_mul(y) - } + pub assume_specification[<$iN>::checked_mul](x: $iN, y: $iN) -> (res: Option<$iN>) + ensures res == checked_mul(x, y); } } @@ -360,27 +274,20 @@ verus! { // TODO move all these into the num_specs! macro to handle them for other integer widths // == u32 methods == -#[verifier::external_fn_specification] -pub fn ex_u32_checked_rem(lhs: u32, rhs: u32) -> (result: Option) +pub assume_specification[ u32::checked_rem ](lhs: u32, rhs: u32) -> (result: Option) ensures rhs == 0 ==> result.is_None(), rhs != 0 ==> result == Some((lhs % rhs) as u32), -{ - lhs.checked_rem(rhs) -} +; -#[verifier::external_fn_specification] -pub fn ex_u32_checked_rem_euclid(lhs: u32, rhs: u32) -> (result: Option) +pub assume_specification[ u32::checked_rem_euclid ](lhs: u32, rhs: u32) -> (result: Option) ensures rhs == 0 ==> result.is_None(), rhs != 0 ==> result == Some((lhs % rhs) as u32), -{ - lhs.checked_rem_euclid(rhs) -} +; // == i32 methods == -#[verifier::external_fn_specification] -pub fn ex_i32_checked_div(lhs: i32, rhs: i32) -> (result: Option) +pub assume_specification[ i32::checked_div ](lhs: i32, rhs: i32) -> (result: Option) ensures rhs == 0 ==> result.is_None(), ({ @@ -403,22 +310,16 @@ pub fn ex_i32_checked_div(lhs: i32, rhs: i32) -> (result: Option) result == Some(output as i32) } }), -{ - lhs.checked_div(rhs) -} +; -#[verifier::external_fn_specification] -pub fn ex_i32_checked_div_euclid(lhs: i32, rhs: i32) -> (result: Option) +pub assume_specification[ i32::checked_div_euclid ](lhs: i32, rhs: i32) -> (result: Option) ensures rhs == 0 ==> result.is_None(), lhs / rhs < i32::MIN || lhs / rhs > i32::MAX ==> result.is_None(), i32::MIN <= lhs / rhs <= i32::MAX ==> result == Some((lhs / rhs) as i32), -{ - lhs.checked_div_euclid(rhs) -} +; -#[verifier::external_fn_specification] -pub fn ex_i32_checked_rem(lhs: i32, rhs: i32) -> (result: Option) +pub assume_specification[ i32::checked_rem ](lhs: i32, rhs: i32) -> (result: Option) ensures rhs == 0 ==> result.is_None(), ({ @@ -441,18 +342,13 @@ pub fn ex_i32_checked_rem(lhs: i32, rhs: i32) -> (result: Option) result == Some(output as i32) } }), -{ - lhs.checked_rem(rhs) -} +; -#[verifier::external_fn_specification] -pub fn ex_i32_checked_rem_euclid(lhs: i32, rhs: i32) -> (result: Option) +pub assume_specification[ i32::checked_rem_euclid ](lhs: i32, rhs: i32) -> (result: Option) ensures rhs == 0 ==> result.is_None(), lhs % rhs < i32::MIN || lhs % rhs > i32::MAX ==> result.is_None(), i32::MIN <= lhs % rhs <= i32::MAX ==> result == Some((lhs % rhs) as i32), -{ - lhs.checked_rem_euclid(rhs) -} +; } // verus! diff --git a/examples/verus-snapshot/source/vstd/std_specs/option.rs b/examples/verus-snapshot/source/vstd/std_specs/option.rs index c7d3f9d..2744dcf 100644 --- a/examples/verus-snapshot/source/vstd/std_specs/option.rs +++ b/examples/verus-snapshot/source/vstd/std_specs/option.rs @@ -7,6 +7,25 @@ use core::option::Option::Some; verus! { +impl View for Option { + type V = Option; + + open spec fn view(&self) -> Option { + *self + } +} + +impl DeepView for Option { + type V = Option; + + open spec fn deep_view(&self) -> Option { + match self { + Some(t) => Some(t.deep_view()), + None => None, + } + } +} + ////// Add is_variant-style spec functions pub trait OptionAdditionalFns: Sized { #[allow(non_snake_case)] @@ -87,14 +106,11 @@ pub open spec fn is_some(option: &Option) -> bool { is_variant(option, "Some") } -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(is_some)] -pub fn ex_option_is_some(option: &Option) -> (b: bool) +pub assume_specification[ Option::::is_some ](option: &Option) -> (b: bool) ensures b == is_some(option), -{ - option.is_some() -} +; // is_none #[verifier::inline] @@ -102,24 +118,18 @@ pub open spec fn is_none(option: &Option) -> bool { is_variant(option, "None") } -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(is_none)] -pub fn ex_option_is_none(option: &Option) -> (b: bool) +pub assume_specification[ Option::::is_none ](option: &Option) -> (b: bool) ensures b == is_none(option), -{ - option.is_none() -} +; // as_ref -#[verifier::external_fn_specification] -pub fn as_ref(option: &Option) -> (a: Option<&T>) +pub assume_specification[ Option::::as_ref ](option: &Option) -> (a: Option<&T>) ensures a.is_Some() <==> option.is_Some(), a.is_Some() ==> option.get_Some_0() == a.get_Some_0(), -{ - option.as_ref() -} +; // unwrap #[verifier::inline] @@ -131,15 +141,12 @@ pub open spec fn spec_unwrap(option: Option) -> T } #[verifier::when_used_as_spec(spec_unwrap)] -#[verifier::external_fn_specification] -pub fn unwrap(option: Option) -> (t: T) +pub assume_specification[ Option::::unwrap ](option: Option) -> (t: T) requires option.is_Some(), ensures t == spec_unwrap(option), -{ - option.unwrap() -} +; // unwrap_or #[verifier::inline] @@ -151,42 +158,33 @@ pub open spec fn spec_unwrap_or(option: Option, default: T) -> T { } #[verifier::when_used_as_spec(spec_unwrap_or)] -#[verifier::external_fn_specification] -pub fn unwrap_or(option: Option, default: T) -> (t: T) +pub assume_specification[ Option::::unwrap_or ](option: Option, default: T) -> (t: T) ensures t == spec_unwrap_or(option, default), -{ - option.unwrap_or(default) -} +; -#[verifier::external_fn_specification] -pub fn take(option: &mut Option) -> (t: Option) +pub assume_specification[ Option::::take ](option: &mut Option) -> (t: Option) ensures t == old(option), *option is None, -{ - option.take() -} +; -#[verifier::external_fn_specification] -pub fn ex_map U>(a: Option, f: F) -> (ret: Option) +pub assume_specification U>[ Option::::map ](a: Option, f: F) -> (ret: + Option) requires a.is_some() ==> f.requires((a.unwrap(),)), ensures ret.is_some() == a.is_some(), ret.is_some() ==> f.ensures((a.unwrap(),), ret.unwrap()), -{ - a.map(f) -} +; -#[verifier::external_fn_specification] -pub fn ex_option_clone(opt: &Option) -> (res: Option) +pub assume_specification[ as Clone>::clone ](opt: &Option) -> (res: Option< + T, +>) ensures opt.is_none() ==> res.is_none(), opt.is_some() ==> res.is_some() && call_ensures(T::clone, (&opt.unwrap(),), res.unwrap()), -{ - opt.clone() -} +; // ok_or #[verifier::inline] @@ -197,13 +195,10 @@ pub open spec fn spec_ok_or(option: Option, err: E) -> Result { } } -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(spec_ok_or)] -pub fn ex_ok_or(option: Option, err: E) -> (res: Result) +pub assume_specification[ Option::ok_or ](option: Option, err: E) -> (res: Result) ensures res == spec_ok_or(option, err), -{ - option.ok_or(err) -} +; } // verus! diff --git a/examples/verus-snapshot/source/vstd/std_specs/range.rs b/examples/verus-snapshot/source/vstd/std_specs/range.rs index d65f037..f859d30 100644 --- a/examples/verus-snapshot/source/vstd/std_specs/range.rs +++ b/examples/verus-snapshot/source/vstd/std_specs/range.rs @@ -27,13 +27,11 @@ pub trait StepSpec where Self: Sized { pub spec fn spec_range_next(a: Range) -> (Range, Option); -#[verifier::external_fn_specification] -pub fn ex_range_next(range: &mut Range) -> (r: Option) +pub assume_specification[ Range::::next ](range: &mut Range) -> (r: + Option) ensures (*range, r) == spec_range_next(*old(range)), -{ - range.next() -} +; pub struct RangeGhostIterator { pub start: A, diff --git a/examples/verus-snapshot/source/vstd/std_specs/result.rs b/examples/verus-snapshot/source/vstd/std_specs/result.rs index 7f980bd..ee8d865 100644 --- a/examples/verus-snapshot/source/vstd/std_specs/result.rs +++ b/examples/verus-snapshot/source/vstd/std_specs/result.rs @@ -55,14 +55,11 @@ pub open spec fn is_ok(result: &Result) -> bool { is_variant(result, "Ok") } -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(is_ok)] -pub fn ex_result_is_ok(result: &Result) -> (b: bool) +pub assume_specification[ Result::::is_ok ](r: &Result) -> (b: bool) ensures - b == is_ok(result), -{ - result.is_ok() -} + b == is_ok(r), +; // is_err #[verifier::inline] @@ -70,26 +67,23 @@ pub open spec fn is_err(result: &Result) -> bool { is_variant(result, "Err") } -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(is_err)] -pub fn ex_result_is_err(result: &Result) -> (b: bool) +pub assume_specification[ Result::::is_err ](r: &Result) -> (b: bool) ensures - b == is_err(result), -{ - result.is_err() -} + b == is_err(r), +; // as_ref -#[verifier::external_fn_specification] -pub fn as_ref(result: &Result) -> (r: Result<&T, &E>) +pub assume_specification[ Result::::as_ref ](result: &Result) -> (r: Result< + &T, + &E, +>) ensures r.is_Ok() <==> result.is_Ok(), r.is_Ok() ==> result.get_Ok_0() == r.get_Ok_0(), r.is_Err() <==> result.is_Err(), r.is_Err() ==> result.get_Err_0() == r.get_Err_0(), -{ - result.as_ref() -} +; // unwrap #[verifier::inline] @@ -101,15 +95,14 @@ pub open spec fn spec_unwrap(result: Result) -> T } #[verifier::when_used_as_spec(spec_unwrap)] -#[verifier::external_fn_specification] -pub fn unwrap(result: Result) -> (t: T) +pub assume_specification[ Result::::unwrap ]( + result: Result, +) -> (t: T) requires result.is_Ok(), ensures t == result.get_Ok_0(), -{ - result.unwrap() -} +; // unwrap_err #[verifier::inline] @@ -121,19 +114,20 @@ pub open spec fn spec_unwrap_err(result: Result) - } #[verifier::when_used_as_spec(spec_unwrap_err)] -#[verifier::external_fn_specification] -pub fn unwrap_err(result: Result) -> (e: E) +pub assume_specification[ Result::::unwrap_err ]( + result: Result, +) -> (e: E) requires result.is_Err(), ensures e == result.get_Err_0(), -{ - result.unwrap_err() -} +; // map -#[verifier::external_fn_specification] -pub fn map U>(result: Result, op: F) -> (mapped_result: Result) +pub assume_specification U>[ Result::::map ]( + result: Result, + op: F, +) -> (mapped_result: Result) requires result.is_ok() ==> op.requires((result.get_Ok_0(),)), ensures @@ -142,9 +136,19 @@ pub fn map U>(result: Result, op: F) -> (mapped_r mapped_result.get_Ok_0(), ), result.is_err() ==> mapped_result == Result::::Err(result.get_Err_0()), -{ - result.map(op) -} +; + +// map_err +#[verusfmt::skip] +pub assume_specification F>[Result::::map_err](result: Result, op: O) -> (mapped_result: Result) + requires + result.is_err() ==> op.requires((result.get_Err_0(),)), + ensures + result.is_err() ==> mapped_result.is_err() && op.ensures( + (result.get_Err_0(),), + mapped_result.get_Err_0(), + ), + result.is_ok() ==> mapped_result == Result::::Ok(result.get_Ok_0()); // ok #[verifier::inline] @@ -155,14 +159,11 @@ pub open spec fn ok(result: Result) -> Option { } } -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(ok)] -pub fn ex_result_ok(result: Result) -> (opt: Option) +pub assume_specification[ Result::::ok ](result: Result) -> (opt: Option) ensures opt == ok(result), -{ - result.ok() -} +; // err #[verifier::inline] @@ -173,13 +174,10 @@ pub open spec fn err(result: Result) -> Option { } } -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(err)] -pub fn ex_result_err(result: Result) -> (opt: Option) +pub assume_specification[ Result::::err ](result: Result) -> (opt: Option) ensures opt == err(result), -{ - result.err() -} +; } // verus! diff --git a/examples/verus-snapshot/source/vstd/std_specs/smart_ptrs.rs b/examples/verus-snapshot/source/vstd/std_specs/smart_ptrs.rs index c21edd4..0de817a 100644 --- a/examples/verus-snapshot/source/vstd/std_specs/smart_ptrs.rs +++ b/examples/verus-snapshot/source/vstd/std_specs/smart_ptrs.rs @@ -8,44 +8,50 @@ use core::alloc::Allocator; verus! { -#[verifier::external_fn_specification] -pub fn box_into_vec(b: Box<[T], A>) -> (v: Vec) +// TODO +pub assume_specification[ <[T]>::into_vec ](b: Box<[T], A>) -> (v: Vec) ensures v@ == b@, -{ - b.into_vec() -} +; -#[verifier::external_fn_specification] -pub fn box_new(t: T) -> (v: Box) +pub assume_specification[ Box::::new ](t: T) -> (v: Box) ensures v == t, -{ - Box::new(t) -} +; -#[verifier::external_fn_specification] -pub fn rc_new(t: T) -> (v: Rc) +pub assume_specification[ Rc::::new ](t: T) -> (v: Rc) ensures v == t, -{ - Rc::new(t) -} +; -#[verifier::external_fn_specification] -pub fn arc_new(t: T) -> (v: Arc) +pub assume_specification[ Arc::::new ](t: T) -> (v: Arc) ensures v == t, -{ - Arc::new(t) -} +; -#[verifier::external_fn_specification] -pub fn box_clone(b: &Box) -> (res: Box) +pub assume_specification[ as Clone>::clone ]( + b: &Box, +) -> (res: Box) ensures call_ensures(T::clone, (&**b,), *res), -{ - b.clone() -} +; + +pub assume_specification[ Rc::::try_unwrap ](v: Rc) -> (result: Result< + T, + Rc, +>) + ensures + match result { + Ok(t) => t == v, + Err(e) => e == v, + }, +; + +pub assume_specification[ Rc::::into_inner ](v: Rc) -> (result: Option< + T, +>) + ensures + result matches Some(t) ==> t == v, +; } // verus! diff --git a/examples/verus-snapshot/source/vstd/std_specs/vec.rs b/examples/verus-snapshot/source/vstd/std_specs/vec.rs index 4eaec56..701b417 100644 --- a/examples/verus-snapshot/source/vstd/std_specs/vec.rs +++ b/examples/verus-snapshot/source/vstd/std_specs/vec.rs @@ -35,7 +35,7 @@ impl VecAdditionalSpecFns for Vec { } } -// TODO this should really be a 'external_fn_specification' function +// TODO this should really be an 'assume_specification' function // but it's difficult to handle vec.index right now because // it uses more trait polymorphism than we can handle right now. // @@ -68,124 +68,99 @@ pub broadcast proof fn axiom_spec_len(v: &Vec) admit(); } -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(spec_vec_len)] -pub fn ex_vec_len(vec: &Vec) -> (len: usize) +pub assume_specification[ Vec::::len ](vec: &Vec) -> (len: usize) ensures len == spec_vec_len(vec), -{ - vec.len() -} +; ////// Other functions -#[verifier::external_fn_specification] -pub fn ex_vec_new() -> (v: Vec) +pub assume_specification[ Vec::::new ]() -> (v: Vec) ensures v@ == Seq::::empty(), -{ - Vec::::new() -} +; -#[verifier::external_fn_specification] -pub fn ex_vec_with_capacity(capacity: usize) -> (v: Vec) +pub assume_specification[ Vec::::with_capacity ](capacity: usize) -> (v: Vec) ensures v@ == Seq::::empty(), -{ - Vec::::with_capacity(capacity) -} +; -#[verifier::external_fn_specification] -pub fn ex_vec_reserve(vec: &mut Vec, additional: usize) +pub assume_specification[ Vec::::reserve ]( + vec: &mut Vec, + additional: usize, +) ensures vec@ == old(vec)@, -{ - vec.reserve(additional) -} +; -#[verifier::external_fn_specification] -pub fn ex_vec_push(vec: &mut Vec, value: T) +pub assume_specification[ Vec::::push ](vec: &mut Vec, value: T) ensures vec@ == old(vec)@.push(value), -{ - vec.push(value) -} +; -#[verifier::external_fn_specification] -pub fn ex_vec_pop(vec: &mut Vec) -> (value: Option) +pub assume_specification[ Vec::::pop ](vec: &mut Vec) -> (value: + Option) ensures old(vec)@.len() > 0 ==> value == Some(old(vec)@[old(vec)@.len() - 1]) && vec@ == old( vec, )@.subrange(0, old(vec)@.len() - 1), old(vec)@.len() == 0 ==> value == None:: && vec@ == old(vec)@, -{ - vec.pop() -} +; -#[verifier::external_fn_specification] -pub fn ex_vec_append(vec: &mut Vec, other: &mut Vec) +pub assume_specification[ Vec::::append ]( + vec: &mut Vec, + other: &mut Vec, +) ensures vec@ == old(vec)@ + old(other)@, other@ == Seq::::empty(), -{ - vec.append(other) -} +; /* // TODO find a way to support this // This is difficult because of the SliceIndex trait use std::ops::Index; -#[verifier::external_fn_specification] -pub fn index(vec: &Vec, i: usize) -> (r: &T) +pub assume_specification[Vec::::index](vec: &Vec, i: usize) -> (r: &T) requires i < vec.len(), ensures - *r == vec[i as int], -{ - - vec.index(i) -} + *r == vec[i as int]; */ -#[verifier::external_fn_specification] -pub fn ex_vec_insert(vec: &mut Vec, i: usize, element: T) +pub assume_specification[ Vec::::insert ]( + vec: &mut Vec, + i: usize, + element: T, +) requires i <= old(vec).len(), ensures vec@ == old(vec)@.insert(i as int, element), -{ - vec.insert(i, element) -} +; -#[verifier::external_fn_specification] -pub fn ex_vec_remove(vec: &mut Vec, i: usize) -> (element: T) +pub assume_specification[ Vec::::remove ]( + vec: &mut Vec, + i: usize, +) -> (element: T) requires i < old(vec).len(), ensures element == old(vec)[i as int], vec@ == old(vec)@.remove(i as int), -{ - vec.remove(i) -} +; -#[verifier::external_fn_specification] -pub fn ex_vec_clear(vec: &mut Vec) +pub assume_specification[ Vec::::clear ](vec: &mut Vec) ensures vec.view() == Seq::::empty(), -{ - vec.clear() -} +; -#[verifier::external_fn_specification] -pub fn ex_vec_as_slice(vec: &Vec) -> (slice: &[T]) +pub assume_specification[ Vec::::as_slice ](vec: &Vec) -> (slice: &[T]) ensures slice@ == vec@, -{ - vec.as_slice() -} +; -#[verifier::external_fn_specification] -pub fn ex_vec_split_off( +pub assume_specification[ Vec::::split_off ]( vec: &mut Vec, at: usize, ) -> (return_value: Vec) @@ -194,16 +169,15 @@ pub fn ex_vec_split_off( ensures vec@ == old(vec)@.subrange(0, at as int), return_value@ == old(vec)@.subrange(at as int, old(vec)@.len() as int), -{ - vec.split_off(at) -} +; pub open spec fn vec_clone_trigger(v1: Vec, v2: Vec) -> bool { true } -#[verifier::external_fn_specification] -pub fn ex_vec_clone(vec: &Vec) -> (res: Vec) +pub assume_specification[ as Clone>::clone ]( + vec: &Vec, +) -> (res: Vec) ensures res.len() == vec.len(), forall|i| @@ -211,9 +185,7 @@ pub fn ex_vec_clone(vec: &Vec) -> (res: Ve 0 <= i < vec.len() ==> call_ensures(T::clone, (&vec[i],), res[i]), vec_clone_trigger(*vec, res), vec@ =~= res@ ==> vec@ == res@, -{ - vec.clone() -} +; pub broadcast proof fn vec_clone_deep_view_proof( v1: Vec, @@ -227,14 +199,28 @@ pub broadcast proof fn vec_clone_deep_view_proof( { } -#[verifier::external_fn_specification] -pub fn ex_vec_truncate(vec: &mut Vec, len: usize) +pub assume_specification[ Vec::::truncate ](vec: &mut Vec, len: usize) ensures - len <= vec.len() ==> vec@ == old(vec)@.subrange(0, len as int), - len > vec.len() ==> vec@ == old(vec)@, -{ - vec.truncate(len) -} + len <= old(vec).len() ==> vec@ == old(vec)@.subrange(0, len as int), + len > old(vec).len() ==> vec@ == old(vec)@, +; + +pub assume_specification[ Vec::::resize ]( + vec: &mut Vec, + len: usize, + value: T, +) + ensures + len <= old(vec).len() ==> vec@ == old(vec)@.subrange(0, len as int), + len > old(vec).len() ==> { + &&& vec@.len() == len + &&& vec@.subrange(0, old(vec).len() as int) == old(vec)@ + &&& forall|i| + #![all_triggers] + old(vec).len() <= i < len ==> call_ensures(T::clone, (&value,), vec@[i]) || value + == vec@[i] + }, +; pub broadcast proof fn axiom_vec_index_decreases(v: Vec, i: int) requires diff --git a/examples/verus-snapshot/source/vstd/string.rs b/examples/verus-snapshot/source/vstd/string.rs index 322e954..92d2e98 100644 --- a/examples/verus-snapshot/source/vstd/string.rs +++ b/examples/verus-snapshot/source/vstd/string.rs @@ -18,40 +18,22 @@ impl View for str { pub spec fn str_slice_is_ascii(s: &str) -> bool; -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(str_slice_is_ascii)] -pub fn ex_str_slice_is_ascii(s: &str) -> (b: bool) +pub assume_specification[ str::is_ascii ](s: &str) -> (b: bool) ensures b == str_slice_is_ascii(s), -{ - s.is_ascii() -} - -#[deprecated = "Use `&str` instead"] -pub type StrSlice<'a> = &'a str; +; pub open spec fn new_strlit_spec(s: &str) -> &str { s } -#[deprecated = "new_strlit is no longer necessary"] -#[verifier::when_used_as_spec(new_strlit_spec)] -pub fn new_strlit(s: &str) -> (t: &str) - ensures - t == s, -{ - s -} - #[cfg(feature = "alloc")] -#[verifier::external_fn_specification] -pub fn ex_str_to_string(s: &str) -> (res: String) +pub assume_specification[ str::to_string ](s: &str) -> (res: String) ensures s@ == res@, s.is_ascii() == res.is_ascii(), -{ - s.to_string() -} +; #[verifier::external] pub trait StrSliceExecFns { @@ -67,12 +49,6 @@ pub trait StrSliceExecFns { #[cfg(feature = "alloc")] fn as_bytes_vec(&self) -> alloc::vec::Vec; - - #[deprecated = "from_rust_str is no longer necessary"] - fn from_rust_str<'a>(&'a self) -> &'a str; - - #[deprecated = "into_rust_str is no longer necessary"] - fn into_rust_str<'a>(&'a self) -> &'a str; } impl StrSliceExecFns for str { @@ -174,14 +150,6 @@ impl StrSliceExecFns for str { } v } - - fn from_rust_str<'a>(&'a self) -> &'a str { - self - } - - fn into_rust_str<'a>(&'a self) -> &'a str { - self - } } pub broadcast proof fn axiom_str_literal_is_ascii<'a>(s: &'a str) @@ -227,42 +195,30 @@ pub struct ExString(String); pub spec fn string_is_ascii(s: &String) -> bool; #[cfg(feature = "alloc")] -#[verifier::external_fn_specification] #[verifier::when_used_as_spec(string_is_ascii)] -pub fn ex_string_is_ascii(s: &String) -> (b: bool) +pub assume_specification[ String::is_ascii ](s: &String) -> (b: bool) ensures b == string_is_ascii(s), -{ - s.is_ascii() -} +; #[cfg(feature = "alloc")] -#[verifier::external_fn_specification] -pub fn ex_string_as_str<'a>(s: &'a String) -> (res: &'a str) +pub assume_specification<'a>[ String::as_str ](s: &'a String) -> (res: &'a str) ensures res@ == s@, s.is_ascii() == res.is_ascii(), -{ - s.as_str() -} +; #[cfg(feature = "alloc")] -#[verifier::external_fn_specification] -pub fn ex_string_clone(s: &String) -> (res: String) +pub assume_specification[ ::clone ](s: &String) -> (res: String) ensures res == s, -{ - s.clone() -} +; #[cfg(feature = "alloc")] -#[verifier::external_fn_specification] -pub fn ex_string_eq(s: &String, other: &String) -> (res: bool) +pub assume_specification[ ::eq ](s: &String, other: &String) -> (res: bool) ensures res == (s@ == other@), -{ - s.eq(other) -} +; #[cfg(feature = "alloc")] #[verifier::external] @@ -287,15 +243,6 @@ pub trait StringExecFns: Sized { fn append<'a, 'b>(&'a mut self, other: &'b str); fn concat<'b>(self, other: &'b str) -> String; - - #[deprecated = "from_rust_string is no longer necessary"] - fn from_rust_string(self) -> String; - - #[deprecated = "into_rust_string is no longer necessary"] - fn into_rust_string(self) -> String; - - #[deprecated = "as_rust_string_ref is no longer necessary"] - fn as_rust_string_ref(&self) -> &String; } #[cfg(feature = "alloc")] @@ -326,18 +273,6 @@ impl StringExecFns for String { { self + other } - - fn from_rust_string(self) -> String { - self - } - - fn into_rust_string(self) -> String { - self - } - - fn as_rust_string_ref(&self) -> &String { - self - } } pub use super::view::View; diff --git a/examples/verus-snapshot/source/vstd/vstd.rs b/examples/verus-snapshot/source/vstd/vstd.rs index 684ad1d..6c24229 100644 --- a/examples/verus-snapshot/source/vstd/vstd.rs +++ b/examples/verus-snapshot/source/vstd/vstd.rs @@ -28,7 +28,6 @@ pub mod bytes; pub mod calc_macro; pub mod cell; pub mod compute; -pub mod function; #[cfg(all(feature = "alloc", feature = "std"))] pub mod hash_map; #[cfg(all(feature = "alloc", feature = "std"))] @@ -45,8 +44,6 @@ pub mod pcm; pub mod pcm_lib; pub mod pervasive; pub mod proph; -#[cfg(feature = "alloc")] -pub mod ptr; pub mod raw_ptr; // TODO this should be permitted even in not(verus_keep_ghost)