From 210a29ce589580683adf866981c13c36c497d446 Mon Sep 17 00:00:00 2001 From: jaybosamiya <5683582+jaybosamiya@users.noreply.github.com> Date: Mon, 1 Apr 2024 00:38:54 +0000 Subject: [PATCH] chore: update to latest Verus snapshot --- .../source/vstd/source/vstd/array.rs | 6 +- .../source/vstd/source/vstd/atomic.rs | 8 +- .../source/vstd/source/vstd/atomic_ghost.rs | 26 +--- .../source/vstd/source/vstd/invariant.rs | 124 ++++++++++++++++-- .../source/vstd/source/vstd/map.rs | 33 ++--- .../source/vstd/source/vstd/multiset.rs | 51 +++---- .../source/vstd/source/vstd/ptr.rs | 5 +- .../source/vstd/source/vstd/seq.rs | 51 +++---- .../source/vstd/source/vstd/seq_lib.rs | 27 ++-- .../source/vstd/source/vstd/set.rs | 81 ++++-------- .../source/vstd/source/vstd/set_lib.rs | 3 +- .../source/vstd/source/vstd/std_specs/bits.rs | 48 +++---- .../source/vstd/std_specs/control_flow.rs | 3 +- .../source/vstd/source/vstd/std_specs/num.rs | 16 +-- .../vstd/source/vstd/std_specs/range.rs | 3 +- .../source/vstd/source/vstd/std_specs/vec.rs | 3 +- .../source/vstd/source/vstd/string.rs | 9 +- 17 files changed, 233 insertions(+), 264 deletions(-) diff --git a/examples/verus-snapshot/source/vstd/source/vstd/array.rs b/examples/verus-snapshot/source/vstd/source/vstd/array.rs index 1cdacf0..b00f396 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/array.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/array.rs @@ -52,8 +52,7 @@ pub exec fn array_index_get(ar: &[T; N], i: usize) -> (out: & } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn array_len_matches_n(ar: &[T; N]) +pub broadcast proof fn array_len_matches_n(ar: &[T; N]) ensures (#[trigger] ar@.len()) == N, { @@ -69,8 +68,7 @@ pub open spec fn array_index(ar: &[T; N], i: int) -> T { pub open spec fn spec_array_as_slice(ar: &[T; N]) -> (out: &[T]); #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_spec_array_as_slice(ar: &[T; N]) +pub broadcast proof fn axiom_spec_array_as_slice(ar: &[T; N]) ensures (#[trigger] spec_array_as_slice(ar))@ == ar@, { diff --git a/examples/verus-snapshot/source/vstd/source/vstd/atomic.rs b/examples/verus-snapshot/source/vstd/source/vstd/atomic.rs index 561c6df..906cff9 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/atomic.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/atomic.rs @@ -471,13 +471,7 @@ macro_rules! atomic_bool_methods { }; } -make_bool_atomic!( - PAtomicBool, - PermissionBool, - PermissionDataBool, - AtomicBool, - bool -); +make_bool_atomic!(PAtomicBool, PermissionBool, PermissionDataBool, AtomicBool, bool); make_unsigned_integer_atomic!( PAtomicU8, diff --git a/examples/verus-snapshot/source/vstd/source/vstd/atomic_ghost.rs b/examples/verus-snapshot/source/vstd/source/vstd/atomic_ghost.rs index 1da04c3..4dee0b0 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/atomic_ghost.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/atomic_ghost.rs @@ -114,33 +114,15 @@ declare_atomic_type!(AtomicU64, PAtomicU64, PermissionU64, u64, AtomicPredU64); declare_atomic_type!(AtomicU32, PAtomicU32, PermissionU32, u32, AtomicPredU32); declare_atomic_type!(AtomicU16, PAtomicU16, PermissionU16, u16, AtomicPredU16); declare_atomic_type!(AtomicU8, PAtomicU8, PermissionU8, u8, AtomicPredU8); -declare_atomic_type!( - AtomicUsize, - PAtomicUsize, - PermissionUsize, - usize, - AtomicPredUsize -); +declare_atomic_type!(AtomicUsize, PAtomicUsize, PermissionUsize, usize, AtomicPredUsize); declare_atomic_type!(AtomicI64, PAtomicI64, PermissionI64, i64, AtomicPredI64); declare_atomic_type!(AtomicI32, PAtomicI32, PermissionI32, i32, AtomicPredI32); declare_atomic_type!(AtomicI16, PAtomicI16, PermissionI16, i16, AtomicPredI16); declare_atomic_type!(AtomicI8, PAtomicI8, PermissionI8, i8, AtomicPredI8); -declare_atomic_type!( - AtomicIsize, - PAtomicIsize, - PermissionIsize, - isize, - AtomicPredIsize -); - -declare_atomic_type!( - AtomicBool, - PAtomicBool, - PermissionBool, - bool, - AtomicPredBool -); +declare_atomic_type!(AtomicIsize, PAtomicIsize, PermissionIsize, isize, AtomicPredIsize); + +declare_atomic_type!(AtomicBool, PAtomicBool, PermissionBool, bool, AtomicPredBool); /// Performs a given atomic operation on a given atomic /// while providing access to its ghost state. diff --git a/examples/verus-snapshot/source/vstd/source/vstd/invariant.rs b/examples/verus-snapshot/source/vstd/source/vstd/invariant.rs index aff0155..2ef73ad 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/invariant.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/invariant.rs @@ -233,6 +233,57 @@ declare_invariant_impl!(LocalInvariant); #[cfg_attr(verus_keep_ghost, verifier::proof)] pub struct InvariantBlockGuard; +// In the "Logical Paradoxes" section of the Iris 4.1 Reference +// (`https://plv.mpi-sws.org/iris/appendix-4.1.pdf`), they show that +// opening invariants carries the risk of unsoundness. One solution to +// this, described in the paper "Later Credits: Resourceful Reasoning +// for the Later Modality" by Spies et al. (available at +// `https://plv.mpi-sws.org/later-credits/paper-later-credits.pdf`) is +// to use "later credits". That is, require the expenditure of a later +// credit, only obtainable in exec mode, when opening an invariant. So +// we require the relinquishment of a tracked +// `OpenInvariantCredit` to open an invariant, and we provide an +// exec-mode function `create_open_invariant_credit` to obtain one. + +verus! { + +#[doc(hidden)] +#[cfg_attr(verus_keep_ghost, verifier::proof)] +#[verifier::external_body] +pub struct OpenInvariantCredit {} + +// It's intentional that `create_open_invariant_credit` uses `exec` mode. This prevents +// creation of an infinite number of credits to open invariants infinitely often. +#[cfg(verus_keep_ghost)] +#[rustc_diagnostic_item = "verus::vstd::invariant::create_open_invariant_credit"] +#[verifier::external_body] +#[inline(always)] +pub fn create_open_invariant_credit() -> Tracked + opens_invariants none +{ + Tracked::::assume_new() +} + +#[cfg(verus_keep_ghost)] +#[rustc_diagnostic_item = "verus::vstd::invariant::spend_open_invariant_credit_in_proof"] +#[doc(hidden)] +#[inline(always)] +pub proof fn spend_open_invariant_credit_in_proof(tracked credit: OpenInvariantCredit) { +} + +#[cfg(verus_keep_ghost)] +#[rustc_diagnostic_item = "verus::vstd::invariant::spend_open_invariant_credit"] +#[doc(hidden)] +#[inline(always)] +pub fn spend_open_invariant_credit(credit: Tracked) + opens_invariants none +{ + proof { + spend_open_invariant_credit_in_proof(credit.get()); + } +} + +} // verus! // NOTE: These 3 methods are removed in the conversion to VIR; they are only used // for encoding and borrow-checking. // In the VIR these are all replaced by the OpenInvariant block. @@ -250,7 +301,6 @@ pub struct InvariantBlockGuard; // // The purpose of the `guard` object, used below, is to ensure the borrow on `i` will // last the entire block. - #[cfg(verus_keep_ghost)] #[rustc_diagnostic_item = "verus::vstd::invariant::open_atomic_invariant_begin"] #[doc(hidden)] @@ -317,32 +367,60 @@ pub fn open_invariant_end(_guard: &InvariantBlockGuard, _v: V) { /// **Note:** Rather than using `open_atomic_invariant!` directly, we generally recommend /// using the [`atomic_ghost` APIs](crate::atomic_ghost). /// +/// It's not legal to use `open_atomic_invariant!` in proof mode. In proof mode, you need +/// to use `open_atomic_invariant_in_proof!` instead. This takes one extra parameter, +/// an open-invariant credit, which you can get by calling +/// `create_open_invariant_credit()` before you enter proof mode. + /// ### Example /// /// TODO fill this in -// TODO the first argument here should be macro'ed in ghost context, not exec +// TODO the `$eexpr` argument here should be macro'ed in ghost context, not exec #[macro_export] macro_rules! open_atomic_invariant { [$($tail:tt)*] => { - ::builtin_macros::verus_exec_inv_macro_exprs!($crate::invariant::open_atomic_invariant_internal!($($tail)*)) + #[cfg(verus_keep_ghost_body)] + let credit = $crate::invariant::create_open_invariant_credit(); + ::builtin_macros::verus_exec_inv_macro_exprs!( + $crate::invariant::open_atomic_invariant_internal!(credit => $($tail)*) + ) }; } #[macro_export] macro_rules! open_atomic_invariant_in_proof { [$($tail:tt)*] => { - ::builtin_macros::verus_ghost_inv_macro_exprs!($crate::invariant::open_atomic_invariant_internal!($($tail)*)) + ::builtin_macros::verus_ghost_inv_macro_exprs!($crate::invariant::open_atomic_invariant_in_proof_internal!($($tail)*)) }; } #[macro_export] macro_rules! open_atomic_invariant_internal { - ($eexpr:expr => $iident:ident => $bblock:block) => { + ($credit_expr:expr => $eexpr:expr => $iident:ident => $bblock:block) => { + #[cfg_attr(verus_keep_ghost, verifier::invariant_block)] /* vattr */ { + #[cfg(verus_keep_ghost_body)] + $crate::invariant::spend_open_invariant_credit($credit_expr); + #[cfg(verus_keep_ghost_body)] + #[allow(unused_mut)] let (guard, mut $iident) = + $crate::invariant::open_atomic_invariant_begin($eexpr); + $bblock + #[cfg(verus_keep_ghost_body)] + $crate::invariant::open_invariant_end(guard, $iident); + } + } +} + +#[macro_export] +macro_rules! open_atomic_invariant_in_proof_internal { + ($credit_expr:expr => $eexpr:expr => $iident:ident => $bblock:block) => { #[cfg_attr(verus_keep_ghost, verifier::invariant_block)] /* vattr */ { #[cfg(verus_keep_ghost_body)] - #[allow(unused_mut)] let (guard, mut $iident) = $crate::invariant::open_atomic_invariant_begin($eexpr); + $crate::invariant::spend_open_invariant_credit_in_proof($credit_expr); + #[cfg(verus_keep_ghost_body)] + #[allow(unused_mut)] let (guard, mut $iident) = + $crate::invariant::open_atomic_invariant_begin($eexpr); $bblock #[cfg(verus_keep_ghost_body)] $crate::invariant::open_invariant_end(guard, $iident); @@ -353,6 +431,8 @@ macro_rules! open_atomic_invariant_internal { pub use open_atomic_invariant; pub use open_atomic_invariant_in_proof; #[doc(hidden)] +pub use open_atomic_invariant_in_proof_internal; +#[doc(hidden)] pub use open_atomic_invariant_internal; /// Macro used to temporarily "open" a [`LocalInvariant`] object, obtaining the stored @@ -439,6 +519,11 @@ pub use open_atomic_invariant_internal; /// The default for an `exec`-mode function is to open any, while the default /// for a `proof`-mode function is to open none. /// +/// It's not legal to use `open_local_invariant!` in proof mode. In proof mode, you need +/// to use `open_local_invariant_in_proof!` instead. This takes one extra parameter, +/// an open-invariant credit, which you can get by calling +/// `create_open_invariant_credit()` before you enter proof mode. +/// /// ### Example /// /// TODO fill this in @@ -450,22 +535,41 @@ pub use open_atomic_invariant_internal; #[macro_export] macro_rules! open_local_invariant { [$($tail:tt)*] => { + #[cfg(verus_keep_ghost_body)] + let credit = $crate::invariant::create_open_invariant_credit(); ::builtin_macros::verus_exec_inv_macro_exprs!( - $crate::invariant::open_local_invariant_internal!($($tail)*)) + $crate::invariant::open_local_invariant_internal!(credit => $($tail)*)) }; } #[macro_export] macro_rules! open_local_invariant_in_proof { [$($tail:tt)*] => { - ::builtin_macros::verus_ghost_inv_macro_exprs!($crate::invariant::open_local_invariant_internal!($($tail)*)) + ::builtin_macros::verus_ghost_inv_macro_exprs!($crate::invariant::open_local_invariant_in_proof_internal!($($tail)*)) }; } #[macro_export] macro_rules! open_local_invariant_internal { - ($eexpr:expr => $iident:ident => $bblock:block) => { + ($credit_expr:expr => $eexpr:expr => $iident:ident => $bblock:block) => { #[cfg_attr(verus_keep_ghost, verifier::invariant_block)] /* vattr */ { + #[cfg(verus_keep_ghost_body)] + $crate::invariant::spend_open_invariant_credit($credit_expr); + #[cfg(verus_keep_ghost_body)] + #[allow(unused_mut)] let (guard, mut $iident) = $crate::invariant::open_local_invariant_begin($eexpr); + $bblock + #[cfg(verus_keep_ghost_body)] + $crate::invariant::open_invariant_end(guard, $iident); + } + } +} + +#[macro_export] +macro_rules! open_local_invariant_in_proof_internal { + ($credit_expr:expr => $eexpr:expr => $iident:ident => $bblock:block) => { + #[cfg_attr(verus_keep_ghost, verifier::invariant_block)] /* vattr */ { + #[cfg(verus_keep_ghost_body)] + $crate::invariant::spend_open_invariant_credit_in_proof($credit_expr); #[cfg(verus_keep_ghost_body)] #[allow(unused_mut)] let (guard, mut $iident) = $crate::invariant::open_local_invariant_begin($eexpr); $bblock @@ -478,4 +582,6 @@ macro_rules! open_local_invariant_internal { pub use open_local_invariant; pub use open_local_invariant_in_proof; #[doc(hidden)] +pub use open_local_invariant_in_proof_internal; +#[doc(hidden)] pub use open_local_invariant_internal; diff --git a/examples/verus-snapshot/source/vstd/source/vstd/map.rs b/examples/verus-snapshot/source/vstd/source/vstd/map.rs index 2d0bd60..bd06335 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/map.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/map.rs @@ -189,8 +189,7 @@ impl Map { // Trusted axioms /* REVIEW: this is simpler than the two separate axioms below -- would this be ok? #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_map_index_decreases(m: Map, key: K) +pub broadcast proof fn axiom_map_index_decreases(m: Map, key: K) requires m.dom().contains(key), ensures @@ -200,8 +199,7 @@ pub proof fn axiom_map_index_decreases(m: Map, key: K) */ #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_map_index_decreases_finite(m: Map, key: K) +pub broadcast proof fn axiom_map_index_decreases_finite(m: Map, key: K) requires m.dom().finite(), m.dom().contains(key), @@ -213,8 +211,7 @@ pub proof fn axiom_map_index_decreases_finite(m: Map, key: K) // REVIEW: this is currently a special case that is hard-wired into the verifier // It implements a version of https://github.com/FStarLang/FStar/pull/2954 . #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_map_index_decreases_infinite(m: Map, key: K) +pub broadcast proof fn axiom_map_index_decreases_infinite(m: Map, key: K) requires m.dom().contains(key), ensures @@ -224,8 +221,7 @@ pub proof fn axiom_map_index_decreases_infinite(m: Map, key: K) /// The domain of the empty map is the empty set #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_map_empty() +pub broadcast proof fn axiom_map_empty() ensures #[trigger] Map::::empty().dom() == Set::::empty(), { @@ -234,8 +230,7 @@ pub proof fn axiom_map_empty() /// The domain of a map after inserting a key-value pair is equivalent to inserting the key into /// the original map's domain set. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_map_insert_domain(m: Map, key: K, value: V) +pub broadcast proof fn axiom_map_insert_domain(m: Map, key: K, value: V) ensures #[trigger] m.insert(key, value).dom() == m.dom().insert(key), { @@ -243,8 +238,7 @@ pub proof fn axiom_map_insert_domain(m: Map, key: K, value: V) /// Inserting `value` at `key` in `m` results in a map that maps `key` to `value` #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_map_insert_same(m: Map, key: K, value: V) +pub broadcast proof fn axiom_map_insert_same(m: Map, key: K, value: V) ensures #[trigger] m.insert(key, value)[key] == value, { @@ -252,8 +246,7 @@ pub proof fn axiom_map_insert_same(m: Map, key: K, value: V) /// Inserting `value` at `key2` does not change the value mapped to by any other keys in `m` #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_map_insert_different(m: Map, key1: K, key2: K, value: V) +pub broadcast proof fn axiom_map_insert_different(m: Map, key1: K, key2: K, value: V) requires m.dom().contains(key1), key1 != key2, @@ -265,8 +258,7 @@ pub proof fn axiom_map_insert_different(m: Map, key1: K, key2: K, va /// The domain of a map after removing a key-value pair is equivalent to removing the key from /// the original map's domain set. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_map_remove_domain(m: Map, key: K) +pub broadcast proof fn axiom_map_remove_domain(m: Map, key: K) ensures #[trigger] m.remove(key).dom() == m.dom().remove(key), { @@ -275,8 +267,7 @@ pub proof fn axiom_map_remove_domain(m: Map, key: K) /// Removing a key-value pair from a map does not change the value mapped to by /// any other keys in the map. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_map_remove_different(m: Map, key1: K, key2: K) +pub broadcast proof fn axiom_map_remove_different(m: Map, key1: K, key2: K) requires m.dom().contains(key1), key1 != key2, @@ -287,8 +278,7 @@ pub proof fn axiom_map_remove_different(m: Map, key1: K, key2: K) /// Two maps are equivalent if their domains are equivalent and every key in their domains map to the same value. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_map_ext_equal(m1: Map, m2: Map) +pub broadcast proof fn axiom_map_ext_equal(m1: Map, m2: Map) ensures #[trigger] (m1 =~= m2) <==> { &&& m1.dom() =~= m2.dom() @@ -298,8 +288,7 @@ pub proof fn axiom_map_ext_equal(m1: Map, m2: Map) } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_map_ext_equal_deep(m1: Map, m2: Map) +pub broadcast proof fn axiom_map_ext_equal_deep(m1: Map, m2: Map) ensures #[trigger] (m1 =~~= m2) <==> { &&& m1.dom() =~~= m2.dom() diff --git a/examples/verus-snapshot/source/vstd/source/vstd/multiset.rs b/examples/verus-snapshot/source/vstd/source/vstd/multiset.rs index 71c84bf..4b47ad9 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/multiset.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/multiset.rs @@ -204,8 +204,7 @@ impl Multiset { // Specification of `empty` /// The empty multiset maps every element to multiplicity 0 #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_multiset_empty(v: V) +pub broadcast proof fn axiom_multiset_empty(v: V) ensures Multiset::empty().count(v) == 0, { @@ -226,8 +225,7 @@ pub proof fn lemma_multiset_empty_len(m: Multiset) /// A call to Multiset::new with input map `m` will return a multiset that maps /// value `v` to multiplicity `m[v]` if `v` is in the domain of `m`. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_multiset_contained(m: Map, v: V) +pub broadcast proof fn axiom_multiset_contained(m: Map, v: V) requires m.dom().finite(), m.dom().contains(v), @@ -239,8 +237,7 @@ pub proof fn axiom_multiset_contained(m: Map, v: V) /// A call to Multiset::new with input map `m` will return a multiset that maps /// value `v` to multiplicity 0 if `v` is not in the domain of `m`. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_multiset_new_not_contained(m: Map, v: V) +pub broadcast proof fn axiom_multiset_new_not_contained(m: Map, v: V) requires m.dom().finite(), !m.dom().contains(v), @@ -253,8 +250,7 @@ pub proof fn axiom_multiset_new_not_contained(m: Map, v: V) /// A call to Multiset::singleton with input value `v` will return a multiset that maps /// value `v` to multiplicity 1. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_multiset_singleton(v: V) +pub broadcast proof fn axiom_multiset_singleton(v: V) ensures (#[trigger] Multiset::singleton(v)).count(v) == 1, { @@ -263,8 +259,7 @@ pub proof fn axiom_multiset_singleton(v: V) /// A call to Multiset::singleton with input value `v` will return a multiset that maps /// any value other than `v` to 0 #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_multiset_singleton_different(v: V, w: V) +pub broadcast proof fn axiom_multiset_singleton_different(v: V, w: V) ensures v != w ==> Multiset::singleton(v).count(w) == 0, { @@ -274,8 +269,7 @@ pub proof fn axiom_multiset_singleton_different(v: V, w: V) /// The count of value `v` in the multiset `m1.add(m2)` is equal to the sum of the /// counts of `v` in `m1` and `m2` individually. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_multiset_add(m1: Multiset, m2: Multiset, v: V) +pub broadcast proof fn axiom_multiset_add(m1: Multiset, m2: Multiset, v: V) ensures m1.add(m2).count(v) == m1.count(v) + m2.count(v), { @@ -286,8 +280,7 @@ pub proof fn axiom_multiset_add(m1: Multiset, m2: Multiset, v: V) /// count of `v` in `m1` and `m2` individually. However, the difference is cut off at 0 and /// cannot be negative. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_multiset_sub(m1: Multiset, m2: Multiset, v: V) +pub broadcast proof fn axiom_multiset_sub(m1: Multiset, m2: Multiset, v: V) ensures m1.sub(m2).count(v) == if m1.count(v) >= m2.count(v) { m1.count(v) - m2.count(v) @@ -300,16 +293,14 @@ pub proof fn axiom_multiset_sub(m1: Multiset, m2: Multiset, v: V) // Extensional equality /// Two multisets are equivalent if and only if they have the same count for every value. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_multiset_ext_equal(m1: Multiset, m2: Multiset) +pub broadcast proof fn axiom_multiset_ext_equal(m1: Multiset, m2: Multiset) ensures #[trigger] (m1 =~= m2) <==> (forall|v: V| m1.count(v) == m2.count(v)), { } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_multiset_ext_equal_deep(m1: Multiset, m2: Multiset) +pub broadcast proof fn axiom_multiset_ext_equal_deep(m1: Multiset, m2: Multiset) ensures #[trigger] (m1 =~~= m2) <==> m1 =~= m2, { @@ -318,8 +309,7 @@ pub proof fn axiom_multiset_ext_equal_deep(m1: Multiset, m2: Multiset) // Specification of `len` /// The length of the empty multiset is 0. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_len_empty() +pub broadcast proof fn axiom_len_empty() ensures (#[trigger] Multiset::::empty().len()) == 0, { @@ -327,8 +317,7 @@ pub proof fn axiom_len_empty() /// The length of a singleton multiset is 1. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_len_singleton(v: V) +pub broadcast proof fn axiom_len_singleton(v: V) ensures (#[trigger] Multiset::::singleton(v).len()) == 1, { @@ -336,8 +325,7 @@ pub proof fn axiom_len_singleton(v: V) /// The length of the addition of two multisets is equal to the sum of the lengths of each individual multiset. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_len_add(m1: Multiset, m2: Multiset) +pub broadcast proof fn axiom_len_add(m1: Multiset, m2: Multiset) ensures (#[trigger] m1.add(m2).len()) == m1.len() + m2.len(), { @@ -346,8 +334,7 @@ pub proof fn axiom_len_add(m1: Multiset, m2: Multiset) // TODO could probably prove this theorem. /// The length of the subtraction of two multisets is equal to the difference between the lengths of each individual multiset. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_len_sub(m1: Multiset, m2: Multiset) +pub broadcast proof fn axiom_len_sub(m1: Multiset, m2: Multiset) requires m2.subset_of(m1), ensures @@ -357,8 +344,7 @@ pub proof fn axiom_len_sub(m1: Multiset, m2: Multiset) /// The count for any given value `v` in a multiset `m` must be less than or equal to the length of `m`. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_count_le_len(m: Multiset, v: V) +pub broadcast proof fn axiom_count_le_len(m: Multiset, v: V) ensures #[trigger] m.count(v) <= #[trigger] m.len(), { @@ -368,8 +354,7 @@ pub proof fn axiom_count_le_len(m: Multiset, v: V) /// For a given value `v` and boolean predicate `f`, if `f(v)` is true, then the count of `v` in /// `m.filter(f)` is the same as the count of `v` in `m`. Otherwise, the count of `v` in `m.filter(f)` is 0. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_filter_count(m: Multiset, f: spec_fn(V) -> bool, v: V) +pub broadcast proof fn axiom_filter_count(m: Multiset, f: spec_fn(V) -> bool, v: V) ensures (#[trigger] m.filter(f).count(v)) == if f(v) { m.count(v) @@ -383,8 +368,7 @@ pub proof fn axiom_filter_count(m: Multiset, f: spec_fn(V) -> bool, v: V) /// In a nonempty multiset `m`, the `choose` function will return a value that maps to a multiplicity /// greater than 0 in `m`. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_choose_count(m: Multiset) +pub broadcast proof fn axiom_choose_count(m: Multiset) requires #[trigger] m.len() != 0, ensures @@ -397,8 +381,7 @@ pub proof fn axiom_choose_count(m: Multiset) // NB this axiom's soundness depends on the inability to learn anything about the entirety of // Multiset::from_map.dom(). #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_multiset_always_finite(m: Multiset) +pub broadcast proof fn axiom_multiset_always_finite(m: Multiset) ensures #[trigger] m.dom().finite(), { diff --git a/examples/verus-snapshot/source/vstd/source/vstd/ptr.rs b/examples/verus-snapshot/source/vstd/source/vstd/ptr.rs index 7512502..f84f506 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/ptr.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/ptr.rs @@ -175,9 +175,8 @@ pub ghost struct PointsToData { } // TODO add similiar height axioms for other ghost objects -#[verifier(broadcast_forall)] -#[verifier(external_body)] -pub proof fn points_to_height_axiom(points_to: PointsTo) +#[verifier::external_body] +pub broadcast proof fn points_to_height_axiom(points_to: PointsTo) ensures #[trigger] is_smaller_than(points_to@, points_to), { diff --git a/examples/verus-snapshot/source/vstd/source/vstd/seq.rs b/examples/verus-snapshot/source/vstd/source/vstd/seq.rs index ecdbdd3..b6298d2 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/seq.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/seq.rs @@ -184,8 +184,7 @@ impl Seq { // Trusted axioms #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_seq_index_decreases(s: Seq, i: int) +pub broadcast proof fn axiom_seq_index_decreases(s: Seq, i: int) requires 0 <= i < s.len(), ensures @@ -194,24 +193,21 @@ pub proof fn axiom_seq_index_decreases(s: Seq, i: int) } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_seq_empty() +pub broadcast proof fn axiom_seq_empty() ensures #[trigger] Seq::::empty().len() == 0, { } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_seq_new_len(len: nat, f: spec_fn(int) -> A) +pub broadcast proof fn axiom_seq_new_len(len: nat, f: spec_fn(int) -> A) ensures #[trigger] Seq::new(len, f).len() == len, { } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_seq_new_index(len: nat, f: spec_fn(int) -> A, i: int) +pub broadcast proof fn axiom_seq_new_index(len: nat, f: spec_fn(int) -> A, i: int) requires 0 <= i < len, ensures @@ -220,16 +216,14 @@ pub proof fn axiom_seq_new_index(len: nat, f: spec_fn(int) -> A, i: int) } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_seq_push_len(s: Seq, a: A) +pub broadcast proof fn axiom_seq_push_len(s: Seq, a: A) ensures #[trigger] s.push(a).len() == s.len() + 1, { } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_seq_push_index_same(s: Seq, a: A, i: int) +pub broadcast proof fn axiom_seq_push_index_same(s: Seq, a: A, i: int) requires i == s.len(), ensures @@ -238,8 +232,7 @@ pub proof fn axiom_seq_push_index_same(s: Seq, a: A, i: int) } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_seq_push_index_different(s: Seq, a: A, i: int) +pub broadcast proof fn axiom_seq_push_index_different(s: Seq, a: A, i: int) requires 0 <= i < s.len(), ensures @@ -248,8 +241,7 @@ pub proof fn axiom_seq_push_index_different(s: Seq, a: A, i: int) } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_seq_update_len(s: Seq, i: int, a: A) +pub broadcast proof fn axiom_seq_update_len(s: Seq, i: int, a: A) requires 0 <= i < s.len(), ensures @@ -258,8 +250,7 @@ pub proof fn axiom_seq_update_len(s: Seq, i: int, a: A) } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_seq_update_same(s: Seq, i: int, a: A) +pub broadcast proof fn axiom_seq_update_same(s: Seq, i: int, a: A) requires 0 <= i < s.len(), ensures @@ -268,8 +259,7 @@ pub proof fn axiom_seq_update_same(s: Seq, i: int, a: A) } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_seq_update_different(s: Seq, i1: int, i2: int, a: A) +pub broadcast proof fn axiom_seq_update_different(s: Seq, i1: int, i2: int, a: A) requires 0 <= i1 < s.len(), 0 <= i2 < s.len(), @@ -280,8 +270,7 @@ pub proof fn axiom_seq_update_different(s: Seq, i1: int, i2: int, a: A) } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_seq_ext_equal(s1: Seq, s2: Seq) +pub broadcast proof fn axiom_seq_ext_equal(s1: Seq, s2: Seq) ensures #[trigger] (s1 =~= s2) <==> { &&& s1.len() == s2.len() @@ -291,8 +280,7 @@ pub proof fn axiom_seq_ext_equal(s1: Seq, s2: Seq) } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_seq_ext_equal_deep(s1: Seq, s2: Seq) +pub broadcast proof fn axiom_seq_ext_equal_deep(s1: Seq, s2: Seq) ensures #[trigger] (s1 =~~= s2) <==> { &&& s1.len() == s2.len() @@ -302,8 +290,7 @@ pub proof fn axiom_seq_ext_equal_deep(s1: Seq, s2: Seq) } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_seq_subrange_len(s: Seq, j: int, k: int) +pub broadcast proof fn axiom_seq_subrange_len(s: Seq, j: int, k: int) requires 0 <= j <= k <= s.len(), ensures @@ -312,8 +299,7 @@ pub proof fn axiom_seq_subrange_len(s: Seq, j: int, k: int) } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_seq_subrange_index(s: Seq, j: int, k: int, i: int) +pub broadcast proof fn axiom_seq_subrange_index(s: Seq, j: int, k: int, i: int) requires 0 <= j <= k <= s.len(), 0 <= i < k - j, @@ -323,16 +309,14 @@ pub proof fn axiom_seq_subrange_index(s: Seq, j: int, k: int, i: int) } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_seq_add_len(s1: Seq, s2: Seq) +pub broadcast proof fn axiom_seq_add_len(s1: Seq, s2: Seq) ensures #[trigger] s1.add(s2).len() == s1.len() + s2.len(), { } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_seq_add_index1(s1: Seq, s2: Seq, i: int) +pub broadcast proof fn axiom_seq_add_index1(s1: Seq, s2: Seq, i: int) requires 0 <= i < s1.len(), ensures @@ -341,8 +325,7 @@ pub proof fn axiom_seq_add_index1(s1: Seq, s2: Seq, i: int) } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_seq_add_index2(s1: Seq, s2: Seq, i: int) +pub broadcast proof fn axiom_seq_add_index2(s1: Seq, s2: Seq, i: int) requires s1.len() <= i < s1.len() + s2.len(), ensures diff --git a/examples/verus-snapshot/source/vstd/source/vstd/seq_lib.rs b/examples/verus-snapshot/source/vstd/source/vstd/seq_lib.rs index 3c7b8fe..4e3529b 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/seq_lib.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/seq_lib.rs @@ -195,8 +195,7 @@ impl Seq { } #[verifier(external_body)] - #[verifier(broadcast_forall)] - pub proof fn filter_lemma_broadcast(self, pred: spec_fn(A) -> bool) + pub broadcast proof fn filter_lemma_broadcast(self, pred: spec_fn(A) -> bool) ensures forall|i: int| 0 <= i < self.filter(pred).len() ==> pred(#[trigger] self.filter(pred)[i]) @@ -230,8 +229,7 @@ impl Seq { } } - #[verifier(broadcast_forall)] - pub proof fn add_empty_left(a: Self, b: Self) + pub broadcast proof fn add_empty_left(a: Self, b: Self) requires a.len() == 0, ensures @@ -240,8 +238,7 @@ impl Seq { assert(a + b =~= b); } - #[verifier(broadcast_forall)] - pub proof fn add_empty_right(a: Self, b: Self) + pub broadcast proof fn add_empty_right(a: Self, b: Self) requires b.len() == 0, ensures @@ -250,8 +247,7 @@ impl Seq { assert(a + b =~= a); } - #[verifier(broadcast_forall)] - pub proof fn push_distributes_over_add(a: Self, b: Self, elt: A) + pub broadcast proof fn push_distributes_over_add(a: Self, b: Self, elt: A) ensures (a + b).push(elt) == a + b.push(elt), { @@ -259,8 +255,11 @@ impl Seq { } #[verifier(external_body)] - #[verifier(broadcast_forall)] - pub proof fn filter_distributes_over_add_broacast(a: Self, b: Self, pred: spec_fn(A) -> bool) + pub broadcast proof fn filter_distributes_over_add_broacast( + a: Self, + b: Self, + pred: spec_fn(A) -> bool, + ) ensures #[trigger] (a + b).filter(pred) == a.filter(pred) + b.filter(pred), { @@ -971,7 +970,7 @@ impl Seq> { ensures self.len() == 1 ==> self.flatten() == self.first(), { - reveal(Seq::add_empty_right); + broadcast use Seq::add_empty_right; if self.len() == 1 { assert(self.flatten() =~= self.first().add(self.drop_first().flatten())); } @@ -1022,8 +1021,7 @@ impl Seq> { self.flatten() == self.flatten_alt(), decreases self.len(), { - reveal(Seq::add_empty_right); - reveal(Seq::push_distributes_over_add); + broadcast use Seq::add_empty_right, Seq::push_distributes_over_add; if self.len() != 0 { self.drop_last().lemma_flatten_and_flatten_alt_are_equivalent(); seq![self.last()].lemma_flatten_one_element(); @@ -1472,8 +1470,7 @@ pub proof fn seq_to_set_is_finite(seq: Seq) } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn seq_to_set_is_finite_broadcast(seq: Seq) +pub broadcast proof fn seq_to_set_is_finite_broadcast(seq: Seq) ensures #[trigger] seq.to_set().finite(), { diff --git a/examples/verus-snapshot/source/vstd/source/vstd/set.rs b/examples/verus-snapshot/source/vstd/source/vstd/set.rs index baaa4be..a2d95d3 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/set.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/set.rs @@ -149,8 +149,7 @@ impl Set { // Trusted axioms /// The empty set contains no elements #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_empty(a: A) +pub broadcast proof fn axiom_set_empty(a: A) ensures !(#[trigger] Set::empty().contains(a)), { @@ -158,8 +157,7 @@ pub proof fn axiom_set_empty(a: A) /// A call to `Set::new` with the predicate `f` contains `a` if and only if `f(a)` is true. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_new(f: spec_fn(A) -> bool, a: A) +pub broadcast proof fn axiom_set_new(f: spec_fn(A) -> bool, a: A) ensures Set::new(f).contains(a) == f(a), { @@ -167,8 +165,7 @@ pub proof fn axiom_set_new(f: spec_fn(A) -> bool, a: A) /// The result of inserting element `a` into set `s` must contains `a`. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_insert_same(s: Set, a: A) +pub broadcast proof fn axiom_set_insert_same(s: Set, a: A) ensures #[trigger] s.insert(a).contains(a), { @@ -177,8 +174,7 @@ pub proof fn axiom_set_insert_same(s: Set, a: A) /// If `a1` does not equal `a2`, then the result of inserting element `a2` into set `s` /// must contain `a1` if and only if the set contained `a1` before the insertion of `a2`. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_insert_different(s: Set, a1: A, a2: A) +pub broadcast proof fn axiom_set_insert_different(s: Set, a1: A, a2: A) requires a1 != a2, ensures @@ -188,8 +184,7 @@ pub proof fn axiom_set_insert_different(s: Set, a1: A, a2: A) /// The result of removing element `a` from set `s` must not contain `a`. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_remove_same(s: Set, a: A) +pub broadcast proof fn axiom_set_remove_same(s: Set, a: A) ensures !(#[trigger] s.remove(a).contains(a)), { @@ -198,8 +193,7 @@ pub proof fn axiom_set_remove_same(s: Set, a: A) /// Removing an element `a` from a set `s` and then inserting `a` back into the set` /// is equivalent to the original set `s`. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_remove_insert(s: Set, a: A) +pub broadcast proof fn axiom_set_remove_insert(s: Set, a: A) requires s.contains(a), ensures @@ -210,8 +204,7 @@ pub proof fn axiom_set_remove_insert(s: Set, a: A) /// If `a1` does not equal `a2`, then the result of removing element `a2` from set `s` /// must contain `a1` if and only if the set contained `a1` before the removal of `a2`. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_remove_different(s: Set, a1: A, a2: A) +pub broadcast proof fn axiom_set_remove_different(s: Set, a1: A, a2: A) requires a1 != a2, ensures @@ -222,8 +215,7 @@ pub proof fn axiom_set_remove_different(s: Set, a1: A, a2: A) /// The union of sets `s1` and `s2` contains element `a` if and only if /// `s1` contains `a` and/or `s2` contains `a`. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_union(s1: Set, s2: Set, a: A) +pub broadcast proof fn axiom_set_union(s1: Set, s2: Set, a: A) ensures s1.union(s2).contains(a) == (s1.contains(a) || s2.contains(a)), { @@ -232,8 +224,7 @@ pub proof fn axiom_set_union(s1: Set, s2: Set, a: A) /// The intersection of sets `s1` and `s2` contains element `a` if and only if /// both `s1` and `s2` contain `a`. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_intersect(s1: Set, s2: Set, a: A) +pub broadcast proof fn axiom_set_intersect(s1: Set, s2: Set, a: A) ensures s1.intersect(s2).contains(a) == (s1.contains(a) && s2.contains(a)), { @@ -242,8 +233,7 @@ pub proof fn axiom_set_intersect(s1: Set, s2: Set, a: A) /// The set difference between `s1` and `s2` contains element `a` if and only if /// `s1` contains `a` and `s2` does not contain `a`. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_difference(s1: Set, s2: Set, a: A) +pub broadcast proof fn axiom_set_difference(s1: Set, s2: Set, a: A) ensures s1.difference(s2).contains(a) == (s1.contains(a) && !s2.contains(a)), { @@ -251,8 +241,7 @@ pub proof fn axiom_set_difference(s1: Set, s2: Set, a: A) /// The complement of set `s` contains element `a` if and only if `s` does not contain `a`. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_complement(s: Set, a: A) +pub broadcast proof fn axiom_set_complement(s: Set, a: A) ensures s.complement().contains(a) == !s.contains(a), { @@ -260,32 +249,28 @@ pub proof fn axiom_set_complement(s: Set, a: A) /// Sets `s1` and `s2` are equal if and only if they contain all of the same elements. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_ext_equal(s1: Set, s2: Set) +pub broadcast proof fn axiom_set_ext_equal(s1: Set, s2: Set) ensures #[trigger] (s1 =~= s2) <==> (forall|a: A| s1.contains(a) == s2.contains(a)), { } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_ext_equal_deep(s1: Set, s2: Set) +pub broadcast proof fn axiom_set_ext_equal_deep(s1: Set, s2: Set) ensures #[trigger] (s1 =~~= s2) <==> s1 =~= s2, { } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_mk_map_domain(s: Set, f: spec_fn(K) -> V) +pub broadcast proof fn axiom_mk_map_domain(s: Set, f: spec_fn(K) -> V) ensures #[trigger] s.mk_map(f).dom() == s, { } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_mk_map_index(s: Set, f: spec_fn(K) -> V, key: K) +pub broadcast proof fn axiom_mk_map_index(s: Set, f: spec_fn(K) -> V, key: K) requires s.contains(key), ensures @@ -296,8 +281,7 @@ pub proof fn axiom_mk_map_index(s: Set, f: spec_fn(K) -> V, key: K) // Trusted axioms about finite /// The empty set is finite. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_empty_finite() +pub broadcast proof fn axiom_set_empty_finite() ensures #[trigger] Set::::empty().finite(), { @@ -305,8 +289,7 @@ pub proof fn axiom_set_empty_finite() /// The result of inserting an element `a` into a finite set `s` is also finite. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_insert_finite(s: Set, a: A) +pub broadcast proof fn axiom_set_insert_finite(s: Set, a: A) requires s.finite(), ensures @@ -316,8 +299,7 @@ pub proof fn axiom_set_insert_finite(s: Set, a: A) /// The result of removing an element `a` from a finite set `s` is also finite. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_remove_finite(s: Set, a: A) +pub broadcast proof fn axiom_set_remove_finite(s: Set, a: A) requires s.finite(), ensures @@ -327,8 +309,7 @@ pub proof fn axiom_set_remove_finite(s: Set, a: A) /// The union of two finite sets is finite. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_union_finite(s1: Set, s2: Set) +pub broadcast proof fn axiom_set_union_finite(s1: Set, s2: Set) requires s1.finite(), s2.finite(), @@ -339,8 +320,7 @@ pub proof fn axiom_set_union_finite(s1: Set, s2: Set) /// The intersection of two finite sets is finite. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_intersect_finite(s1: Set, s2: Set) +pub broadcast proof fn axiom_set_intersect_finite(s1: Set, s2: Set) requires s1.finite() || s2.finite(), ensures @@ -350,8 +330,7 @@ pub proof fn axiom_set_intersect_finite(s1: Set, s2: Set) /// The set difference between two finite sets is finite. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_difference_finite(s1: Set, s2: Set) +pub broadcast proof fn axiom_set_difference_finite(s1: Set, s2: Set) requires s1.finite(), ensures @@ -361,8 +340,7 @@ pub proof fn axiom_set_difference_finite(s1: Set, s2: Set) /// An infinite set `s` contains the element `s.choose()`. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_choose_finite(s: Set) +pub broadcast proof fn axiom_set_choose_finite(s: Set) requires !s.finite(), ensures @@ -375,8 +353,7 @@ pub proof fn axiom_set_choose_finite(s: Set) // The following, with axiom_set_ext_equal, are enough to build libraries about len. /// The empty set has length 0. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_empty_len() +pub broadcast proof fn axiom_set_empty_len() ensures #[trigger] Set::::empty().len() == 0, { @@ -385,8 +362,7 @@ pub proof fn axiom_set_empty_len() /// The result of inserting an element `a` into a finite set `s` has length /// `s.len() + 1` if `a` is not already in `s` and length `s.len()` otherwise. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_insert_len(s: Set, a: A) +pub broadcast proof fn axiom_set_insert_len(s: Set, a: A) requires s.finite(), ensures @@ -401,8 +377,7 @@ pub proof fn axiom_set_insert_len(s: Set, a: A) /// The result of removing an element `a` from a finite set `s` has length /// `s.len() - 1` if `a` is in `s` and length `s.len()` otherwise. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_remove_len(s: Set, a: A) +pub broadcast proof fn axiom_set_remove_len(s: Set, a: A) requires s.finite(), ensures @@ -416,8 +391,7 @@ pub proof fn axiom_set_remove_len(s: Set, a: A) /// If a finite set `s` contains any element, it has length greater than 0. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_contains_len(s: Set, a: A) +pub broadcast proof fn axiom_set_contains_len(s: Set, a: A) requires s.finite(), #[trigger] s.contains(a), @@ -428,8 +402,7 @@ pub proof fn axiom_set_contains_len(s: Set, a: A) /// A finite set `s` contains the element `s.choose()` if it has length greater than 0. #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_set_choose_len(s: Set) +pub broadcast proof fn axiom_set_choose_len(s: Set) requires s.finite(), #[trigger] s.len() != 0, diff --git a/examples/verus-snapshot/source/vstd/source/vstd/set_lib.rs b/examples/verus-snapshot/source/vstd/source/vstd/set_lib.rs index 19615ff..b928d04 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/set_lib.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/set_lib.rs @@ -847,8 +847,7 @@ pub proof fn lemma_set_properties() } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_is_empty(s: Set) +pub broadcast proof fn axiom_is_empty(s: Set) requires s.finite(), !(#[trigger] s.is_empty()), diff --git a/examples/verus-snapshot/source/vstd/source/vstd/std_specs/bits.rs b/examples/verus-snapshot/source/vstd/source/vstd/std_specs/bits.rs index e49e24a..88f6d8d 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/std_specs/bits.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/std_specs/bits.rs @@ -80,9 +80,8 @@ pub fn ex_u8_leading_ones(i: u8) -> (r: u32) i.leading_ones() } -#[verifier::broadcast_forall] #[verifier::external_body] -pub proof fn axiom_u8_trailing_zeros(i: u8) +pub broadcast proof fn axiom_u8_trailing_zeros(i: u8) ensures 0 <= #[trigger] u8_trailing_zeros(i) <= 8, i == 0 <==> u8_trailing_zeros(i) == 8, @@ -114,9 +113,8 @@ pub proof fn axiom_u8_trailing_zeros(i: u8) } } -#[verifier::broadcast_forall] #[verifier::external_body] -pub proof fn axiom_u8_trailing_ones(i: u8) +pub broadcast proof fn axiom_u8_trailing_ones(i: u8) ensures 0 <= #[trigger] u8_trailing_ones(i) <= 8, i == 0xffu8 <==> u8_trailing_ones(i) == 8, @@ -138,9 +136,8 @@ pub proof fn axiom_u8_trailing_ones(i: u8) } } -#[verifier::broadcast_forall] #[verifier::external_body] -pub proof fn axiom_u8_leading_zeros(i: u8) +pub broadcast proof fn axiom_u8_leading_zeros(i: u8) ensures 0 <= #[trigger] u8_leading_zeros(i) <= 8, i == 0 <==> u8_leading_zeros(i) == 8, @@ -170,9 +167,8 @@ pub proof fn axiom_u8_leading_zeros(i: u8) } } -#[verifier::broadcast_forall] #[verifier::external_body] -pub proof fn axiom_u8_leading_ones(i: u8) +pub broadcast proof fn axiom_u8_leading_ones(i: u8) ensures 0 <= #[trigger] u8_leading_ones(i) <= 8, i == 0xffu8 <==> u8_leading_ones(i) == 8, @@ -270,9 +266,8 @@ pub fn ex_u16_leading_ones(i: u16) -> (r: u32) i.leading_ones() } -#[verifier::broadcast_forall] #[verifier::external_body] -pub proof fn axiom_u16_trailing_zeros(i: u16) +pub broadcast proof fn axiom_u16_trailing_zeros(i: u16) ensures 0 <= #[trigger] u16_trailing_zeros(i) <= 16, i == 0 <==> u16_trailing_zeros(i) == 16, @@ -305,9 +300,8 @@ pub proof fn axiom_u16_trailing_zeros(i: u16) } } -#[verifier::broadcast_forall] #[verifier::external_body] -pub proof fn axiom_u16_trailing_ones(i: u16) +pub broadcast proof fn axiom_u16_trailing_ones(i: u16) ensures 0 <= #[trigger] u16_trailing_ones(i) <= 16, i == 0xffffu16 <==> u16_trailing_ones(i) == 16, @@ -330,9 +324,8 @@ pub proof fn axiom_u16_trailing_ones(i: u16) } } -#[verifier::broadcast_forall] #[verifier::external_body] -pub proof fn axiom_u16_leading_zeros(i: u16) +pub broadcast proof fn axiom_u16_leading_zeros(i: u16) ensures 0 <= #[trigger] u16_leading_zeros(i) <= 16, i == 0 <==> u16_leading_zeros(i) == 16, @@ -364,9 +357,8 @@ pub proof fn axiom_u16_leading_zeros(i: u16) } } -#[verifier::broadcast_forall] #[verifier::external_body] -pub proof fn axiom_u16_leading_ones(i: u16) +pub broadcast proof fn axiom_u16_leading_ones(i: u16) ensures 0 <= #[trigger] u16_leading_ones(i) <= 16, i == 0xffffu16 <==> u16_leading_ones(i) == 16, @@ -466,9 +458,8 @@ pub fn ex_u32_leading_ones(i: u32) -> (r: u32) i.leading_ones() } -#[verifier::broadcast_forall] #[verifier::external_body] -pub proof fn axiom_u32_trailing_zeros(i: u32) +pub broadcast proof fn axiom_u32_trailing_zeros(i: u32) ensures 0 <= #[trigger] u32_trailing_zeros(i) <= 32, i == 0 <==> u32_trailing_zeros(i) == 32, @@ -501,9 +492,8 @@ pub proof fn axiom_u32_trailing_zeros(i: u32) } } -#[verifier::broadcast_forall] #[verifier::external_body] -pub proof fn axiom_u32_trailing_ones(i: u32) +pub broadcast proof fn axiom_u32_trailing_ones(i: u32) ensures 0 <= #[trigger] u32_trailing_ones(i) <= 32, i == 0xffff_ffffu32 <==> u32_trailing_ones(i) == 32, @@ -526,9 +516,8 @@ pub proof fn axiom_u32_trailing_ones(i: u32) } } -#[verifier::broadcast_forall] #[verifier::external_body] -pub proof fn axiom_u32_leading_zeros(i: u32) +pub broadcast proof fn axiom_u32_leading_zeros(i: u32) ensures 0 <= #[trigger] u32_leading_zeros(i) <= 32, i == 0 <==> u32_leading_zeros(i) == 32, @@ -560,9 +549,8 @@ pub proof fn axiom_u32_leading_zeros(i: u32) } } -#[verifier::broadcast_forall] #[verifier::external_body] -pub proof fn axiom_u32_leading_ones(i: u32) +pub broadcast proof fn axiom_u32_leading_ones(i: u32) ensures 0 <= #[trigger] u32_leading_ones(i) <= 32, i == 0xffff_ffffu32 <==> u32_leading_ones(i) == 32, @@ -663,9 +651,8 @@ pub fn ex_u64_leading_ones(i: u64) -> (r: u32) i.leading_ones() } -#[verifier::broadcast_forall] #[verifier::external_body] -pub proof fn axiom_u64_trailing_zeros(i: u64) +pub broadcast proof fn axiom_u64_trailing_zeros(i: u64) ensures 0 <= #[trigger] u64_trailing_zeros(i) <= 64, i == 0 <==> u64_trailing_zeros(i) == 64, @@ -698,9 +685,8 @@ pub proof fn axiom_u64_trailing_zeros(i: u64) } } -#[verifier::broadcast_forall] #[verifier::external_body] -pub proof fn axiom_u64_trailing_ones(i: u64) +pub broadcast proof fn axiom_u64_trailing_ones(i: u64) ensures 0 <= #[trigger] u64_trailing_ones(i) <= 64, i == 0xffff_ffff_ffff_ffffu64 <==> u64_trailing_ones(i) == 64, @@ -723,9 +709,8 @@ pub proof fn axiom_u64_trailing_ones(i: u64) } } -#[verifier::broadcast_forall] #[verifier::external_body] -pub proof fn axiom_u64_leading_zeros(i: u64) +pub broadcast proof fn axiom_u64_leading_zeros(i: u64) ensures 0 <= #[trigger] u64_leading_zeros(i) <= 64, i == 0 <==> u64_leading_zeros(i) == 64, @@ -757,9 +742,8 @@ pub proof fn axiom_u64_leading_zeros(i: u64) } } -#[verifier::broadcast_forall] #[verifier::external_body] -pub proof fn axiom_u64_leading_ones(i: u64) +pub broadcast proof fn axiom_u64_leading_ones(i: u64) ensures 0 <= #[trigger] u64_leading_ones(i) <= 64, i == 0xffff_ffff_ffff_ffffu64 <==> u64_leading_ones(i) == 64, diff --git a/examples/verus-snapshot/source/vstd/source/vstd/std_specs/control_flow.rs b/examples/verus-snapshot/source/vstd/source/vstd/std_specs/control_flow.rs index 4eb91d1..5b622b7 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/std_specs/control_flow.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/std_specs/control_flow.rs @@ -54,9 +54,8 @@ pub fn ex_option_from_residual(option: Option) -> (option2: Optio pub spec fn spec_from(value: T, ret: S) -> bool; -#[verifier::broadcast_forall] #[verifier::external_body] -pub proof fn spec_from_blanket_identity(t: T, s: T) +pub broadcast proof fn spec_from_blanket_identity(t: T, s: T) ensures spec_from::(t, s) ==> t == s, { diff --git a/examples/verus-snapshot/source/vstd/source/vstd/std_specs/num.rs b/examples/verus-snapshot/source/vstd/source/vstd/std_specs/num.rs index 0fee85b..63edbb6 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/std_specs/num.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/std_specs/num.rs @@ -165,20 +165,8 @@ num_specs!(u8, i8, u8_specs, i8_specs, 0x100); num_specs!(u16, i16, u16_specs, i16_specs, 0x1_0000); num_specs!(u32, i32, u32_specs, i32_specs, 0x1_0000_0000); num_specs!(u64, i64, u64_specs, i64_specs, 0x1_0000_0000_0000_0000); -num_specs!( - u128, - i128, - u128_specs, - i128_specs, - 0x1_0000_0000_0000_0000_0000_0000_0000_0000 -); -num_specs!( - usize, - isize, - usize_specs, - isize_specs, - (usize::MAX - usize::MIN + 1) -); +num_specs!(u128, i128, u128_specs, i128_specs, 0x1_0000_0000_0000_0000_0000_0000_0000_0000); +num_specs!(usize, isize, usize_specs, isize_specs, (usize::MAX - usize::MIN + 1)); verus! { diff --git a/examples/verus-snapshot/source/vstd/source/vstd/std_specs/range.rs b/examples/verus-snapshot/source/vstd/source/vstd/std_specs/range.rs index b7b9cad..4f2bedc 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/std_specs/range.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/std_specs/range.rs @@ -149,8 +149,7 @@ macro_rules! step_specs { // TODO: we might be able to make this generic over A: StepSpec // once we settle on a way to connect std traits like Step with spec traits like StepSpec. #[verifier::external_body] - #[verifier::broadcast_forall] - pub proof fn $axiom(range: Range<$t>) + pub broadcast proof fn $axiom(range: Range<$t>) ensures range.start.spec_is_lt(range.end) ==> // TODO (not important): use new "matches ==>" syntax here diff --git a/examples/verus-snapshot/source/vstd/source/vstd/std_specs/vec.rs b/examples/verus-snapshot/source/vstd/source/vstd/std_specs/vec.rs index 409f4ce..430b976 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/std_specs/vec.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/std_specs/vec.rs @@ -81,8 +81,7 @@ pub open spec fn spec_vec_len(v: &Vec) -> usize; // This axiom is slightly better than defining spec_vec_len to just be `v@.len() as usize` // (the axiom also shows that v@.len() is in-bounds for usize) #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_spec_len(v: &Vec) +pub broadcast proof fn axiom_spec_len(v: &Vec) ensures #[trigger] spec_vec_len(v) == v@.len(), { diff --git a/examples/verus-snapshot/source/vstd/source/vstd/string.rs b/examples/verus-snapshot/source/vstd/source/vstd/string.rs index 6cdce90..5772687 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/string.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/string.rs @@ -155,24 +155,21 @@ impl<'a> StrSlice<'a> { } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_str_literal_is_ascii<'a>(s: StrSlice<'a>) +pub broadcast proof fn axiom_str_literal_is_ascii<'a>(s: StrSlice<'a>) ensures #[trigger] s.is_ascii() == builtin::strslice_is_ascii(s), { } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_str_literal_len<'a>(s: StrSlice<'a>) +pub broadcast proof fn axiom_str_literal_len<'a>(s: StrSlice<'a>) ensures #[trigger] s@.len() == builtin::strslice_len(s), { } #[verifier(external_body)] -#[verifier(broadcast_forall)] -pub proof fn axiom_str_literal_get_char<'a>(s: StrSlice<'a>, i: int) +pub broadcast proof fn axiom_str_literal_get_char<'a>(s: StrSlice<'a>, i: int) ensures #[trigger] s@.index(i) == builtin::strslice_get_char(s, i), {