chore: update to latest Verus snapshot

examples/verus-snapshot/source/vstd/source/vstd/array.rs

@@ -52,8 +52,7 @@ pub exec fn array_index_get<T, const N: usize>(ar: &[T; N], i: usize) -> (out: &
 }
 
 #[verifier(external_body)]
-#[verifier(broadcast_forall)]
-pub proof fn array_len_matches_n<T, const N: usize>(ar: &[T; N])
+pub broadcast proof fn array_len_matches_n<T, const N: usize>(ar: &[T; N])
     ensures
         (#[trigger] ar@.len()) == N,
 {
@@ -69,8 +68,7 @@ pub open spec fn array_index<T, const N: usize>(ar: &[T; N], i: int) -> T {
 pub open spec fn spec_array_as_slice<T, const N: usize>(ar: &[T; N]) -> (out: &[T]);
 
 #[verifier(external_body)]
-#[verifier(broadcast_forall)]
-pub proof fn axiom_spec_array_as_slice<T, const N: usize>(ar: &[T; N])
+pub broadcast proof fn axiom_spec_array_as_slice<T, const N: usize>(ar: &[T; N])
     ensures
         (#[trigger] spec_array_as_slice(ar))@ == ar@,
 {

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,

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.

examples/verus-snapshot/source/vstd/source/vstd/map.rs

@@ -189,8 +189,7 @@ impl<K, V> Map<K, V> {
 // 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<K, V>(m: Map<K, V>, key: K)
+pub broadcast proof fn axiom_map_index_decreases<K, V>(m: Map<K, V>, key: K)
     requires
         m.dom().contains(key),
     ensures
@@ -200,8 +199,7 @@ pub proof fn axiom_map_index_decreases<K, V>(m: Map<K, V>, key: K)
 */
 
 #[verifier(external_body)]
-#[verifier(broadcast_forall)]
-pub proof fn axiom_map_index_decreases_finite<K, V>(m: Map<K, V>, key: K)
+pub broadcast proof fn axiom_map_index_decreases_finite<K, V>(m: Map<K, V>, key: K)
     requires
         m.dom().finite(),
         m.dom().contains(key),
@@ -213,8 +211,7 @@ pub proof fn axiom_map_index_decreases_finite<K, V>(m: Map<K, V>, 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<K, V>(m: Map<K, V>, key: K)
+pub broadcast proof fn axiom_map_index_decreases_infinite<K, V>(m: Map<K, V>, key: K)
     requires
         m.dom().contains(key),
     ensures
@@ -224,8 +221,7 @@ pub proof fn axiom_map_index_decreases_infinite<K, V>(m: Map<K, V>, key: K)
 
 /// The domain of the empty map is the empty set
 #[verifier(external_body)]
-#[verifier(broadcast_forall)]
-pub proof fn axiom_map_empty<K, V>()
+pub broadcast proof fn axiom_map_empty<K, V>()
     ensures
         #[trigger] Map::<K, V>::empty().dom() == Set::<K>::empty(),
 {
@@ -234,26 +230,23 @@ pub proof fn axiom_map_empty<K, V>()
 /// 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<K, V>(m: Map<K, V>, key: K, value: V)
+pub broadcast proof fn axiom_map_insert_domain<K, V>(m: Map<K, V>, key: K, value: V)
     ensures
         #[trigger] m.insert(key, value).dom() == m.dom().insert(key),
 {
 }
 
 /// 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<K, V>(m: Map<K, V>, key: K, value: V)
+pub broadcast proof fn axiom_map_insert_same<K, V>(m: Map<K, V>, key: K, value: V)
     ensures
         #[trigger] m.insert(key, value)[key] == value,
 {
 }
 
 /// 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<K, V>(m: Map<K, V>, key1: K, key2: K, value: V)
+pub broadcast proof fn axiom_map_insert_different<K, V>(m: Map<K, V>, key1: K, key2: K, value: V)
     requires
         m.dom().contains(key1),
         key1 != key2,
@@ -265,8 +258,7 @@ pub proof fn axiom_map_insert_different<K, V>(m: Map<K, V>, 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<K, V>(m: Map<K, V>, key: K)
+pub broadcast proof fn axiom_map_remove_domain<K, V>(m: Map<K, V>, key: K)
     ensures
         #[trigger] m.remove(key).dom() == m.dom().remove(key),
 {
@@ -275,8 +267,7 @@ pub proof fn axiom_map_remove_domain<K, V>(m: Map<K, V>, 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<K, V>(m: Map<K, V>, key1: K, key2: K)
+pub broadcast proof fn axiom_map_remove_different<K, V>(m: Map<K, V>, key1: K, key2: K)
     requires
         m.dom().contains(key1),
         key1 != key2,
@@ -287,8 +278,7 @@ pub proof fn axiom_map_remove_different<K, V>(m: Map<K, V>, 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<K, V>(m1: Map<K, V>, m2: Map<K, V>)
+pub broadcast proof fn axiom_map_ext_equal<K, V>(m1: Map<K, V>, m2: Map<K, V>)
     ensures
         #[trigger] (m1 =~= m2) <==> {
             &&& m1.dom() =~= m2.dom()
@@ -298,8 +288,7 @@ pub proof fn axiom_map_ext_equal<K, V>(m1: Map<K, V>, m2: Map<K, V>)
 }
 
 #[verifier(external_body)]
-#[verifier(broadcast_forall)]
-pub proof fn axiom_map_ext_equal_deep<K, V>(m1: Map<K, V>, m2: Map<K, V>)
+pub broadcast proof fn axiom_map_ext_equal_deep<K, V>(m1: Map<K, V>, m2: Map<K, V>)
     ensures
         #[trigger] (m1 =~~= m2) <==> {
             &&& m1.dom() =~~= m2.dom()

examples/verus-snapshot/source/vstd/source/vstd/multiset.rs

@@ -204,8 +204,7 @@ impl<V> Multiset<V> {
 // 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: V)
+pub broadcast proof fn axiom_multiset_empty<V>(v: V)
     ensures
         Multiset::empty().count(v) == 0,
 {
@@ -226,8 +225,7 @@ pub proof fn lemma_multiset_empty_len<V>(m: Multiset<V>)
 /// 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<V>(m: Map<V, nat>, v: V)
+pub broadcast proof fn axiom_multiset_contained<V>(m: Map<V, nat>, v: V)
     requires
         m.dom().finite(),
         m.dom().contains(v),
@@ -239,8 +237,7 @@ pub proof fn axiom_multiset_contained<V>(m: Map<V, nat>, 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<V>(m: Map<V, nat>, v: V)
+pub broadcast proof fn axiom_multiset_new_not_contained<V>(m: Map<V, nat>, v: V)
     requires
         m.dom().finite(),
         !m.dom().contains(v),
@@ -253,8 +250,7 @@ pub proof fn axiom_multiset_new_not_contained<V>(m: Map<V, nat>, 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: V)
+pub broadcast proof fn axiom_multiset_singleton<V>(v: V)
     ensures
         (#[trigger] Multiset::singleton(v)).count(v) == 1,
 {
@@ -263,8 +259,7 @@ pub proof fn axiom_multiset_singleton<V>(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: V, w: V)
+pub broadcast proof fn axiom_multiset_singleton_different<V>(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: 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<V>(m1: Multiset<V>, m2: Multiset<V>, v: V)
+pub broadcast proof fn axiom_multiset_add<V>(m1: Multiset<V>, m2: Multiset<V>, v: V)
     ensures
         m1.add(m2).count(v) == m1.count(v) + m2.count(v),
 {
@@ -286,8 +280,7 @@ pub proof fn axiom_multiset_add<V>(m1: Multiset<V>, m2: Multiset<V>, 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<V>(m1: Multiset<V>, m2: Multiset<V>, v: V)
+pub broadcast proof fn axiom_multiset_sub<V>(m1: Multiset<V>, m2: Multiset<V>, 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<V>(m1: Multiset<V>, m2: Multiset<V>, 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<V>(m1: Multiset<V>, m2: Multiset<V>)
+pub broadcast proof fn axiom_multiset_ext_equal<V>(m1: Multiset<V>, m2: Multiset<V>)
     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<V>(m1: Multiset<V>, m2: Multiset<V>)
+pub broadcast proof fn axiom_multiset_ext_equal_deep<V>(m1: Multiset<V>, m2: Multiset<V>)
     ensures
         #[trigger] (m1 =~~= m2) <==> m1 =~= m2,
 {
@@ -318,26 +309,23 @@ pub proof fn axiom_multiset_ext_equal_deep<V>(m1: Multiset<V>, m2: Multiset<V>)
 // Specification of `len`
 /// The length of the empty multiset is 0.
 #[verifier(external_body)]
-#[verifier(broadcast_forall)]
-pub proof fn axiom_len_empty<V>()
+pub broadcast proof fn axiom_len_empty<V>()
     ensures
         (#[trigger] Multiset::<V>::empty().len()) == 0,
 {
 }
 
 /// The length of a singleton multiset is 1.
 #[verifier(external_body)]
-#[verifier(broadcast_forall)]
-pub proof fn axiom_len_singleton<V>(v: V)
+pub broadcast proof fn axiom_len_singleton<V>(v: V)
     ensures
         (#[trigger] Multiset::<V>::singleton(v).len()) == 1,
 {
 }
 
 /// 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<V>(m1: Multiset<V>, m2: Multiset<V>)
+pub broadcast proof fn axiom_len_add<V>(m1: Multiset<V>, m2: Multiset<V>)
     ensures
         (#[trigger] m1.add(m2).len()) == m1.len() + m2.len(),
 {
@@ -346,8 +334,7 @@ pub proof fn axiom_len_add<V>(m1: Multiset<V>, m2: Multiset<V>)
 // 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<V>(m1: Multiset<V>, m2: Multiset<V>)
+pub broadcast proof fn axiom_len_sub<V>(m1: Multiset<V>, m2: Multiset<V>)
     requires
         m2.subset_of(m1),
     ensures
@@ -357,8 +344,7 @@ pub proof fn axiom_len_sub<V>(m1: Multiset<V>, m2: Multiset<V>)
 
 /// 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<V>(m: Multiset<V>, v: V)
+pub broadcast proof fn axiom_count_le_len<V>(m: Multiset<V>, v: V)
     ensures
         #[trigger] m.count(v) <= #[trigger] m.len(),
 {
@@ -368,8 +354,7 @@ pub proof fn axiom_count_le_len<V>(m: Multiset<V>, 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<V>(m: Multiset<V>, f: spec_fn(V) -> bool, v: V)
+pub broadcast proof fn axiom_filter_count<V>(m: Multiset<V>, 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<V>(m: Multiset<V>, 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<V>(m: Multiset<V>)
+pub broadcast proof fn axiom_choose_count<V>(m: Multiset<V>)
     requires
         #[trigger] m.len() != 0,
     ensures
@@ -397,8 +381,7 @@ pub proof fn axiom_choose_count<V>(m: Multiset<V>)
 // 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<V>(m: Multiset<V>)
+pub broadcast proof fn axiom_multiset_always_finite<V>(m: Multiset<V>)
     ensures
         #[trigger] m.dom().finite(),
 {

examples/verus-snapshot/source/vstd/source/vstd/ptr.rs

@@ -175,9 +175,8 @@ pub ghost struct PointsToData<V> {
 }
 
 // TODO add similiar height axioms for other ghost objects
-#[verifier(broadcast_forall)]
-#[verifier(external_body)]
-pub proof fn points_to_height_axiom<V>(points_to: PointsTo<V>)
+#[verifier::external_body]
+pub broadcast proof fn points_to_height_axiom<V>(points_to: PointsTo<V>)
     ensures
         #[trigger] is_smaller_than(points_to@, points_to),
 {