chore: update to latest Verus snapshot

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

@@ -1,5 +1,6 @@
 #![allow(unused_imports)]
 use crate::seq::*;
+use crate::slice::SliceAdditionalSpecFns;
 use builtin::*;
 use builtin_macros::*;
 
@@ -65,4 +66,34 @@ pub open spec fn array_index<T, const N: usize>(ar: &[T; N], i: int) -> T {
     ar.view().index(i)
 }
 
+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])
+    ensures
+        (#[trigger] spec_array_as_slice(ar))@ == ar@,
+{
+}
+
+// Referenced by Verus' internal encoding for array -> slice coercion
+#[doc(hidden)]
+#[verifier(external_body)]
+#[verifier::when_used_as_spec(spec_array_as_slice)]
+#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "vstd::array::array_as_slice")]
+pub fn array_as_slice<T, const N: usize>(ar: &[T; N]) -> (out: &[T])
+    ensures
+        ar@ == out@,
+{
+    ar
+}
+
+#[verifier(external_fn_specification)]
+pub fn ex_array_as_slice<T, const N: usize>(ar: &[T; N]) -> (out: &[T])
+    ensures
+        ar@ == out@,
+{
+    ar.as_slice()
+}
+
 } // verus!

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/function.rs

@@ -31,15 +31,15 @@ pub proof fn fun_ext<A, B>(f1: spec_fn(A) -> B, f2: spec_fn(A) -> B)
 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)]
-      #[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
-      {}
-    }
+          /// DEPRECATED: use f1 =~= f2 or f1 =~~= f2 instead.
+          /// See [`fun_ext`]
+          #[verifier(external_body)]
+          #[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
+          {}
+        }
     };
 }
 

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

@@ -26,4 +26,3 @@ pub proof fn tracked_static_ref<V>(tracked v: V) -> (tracked res: &'static V)
 }
 
 } // verus!
-// verus

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

@@ -1,4 +1,5 @@
 use crate::prelude::*;
+use crate::set::*;
 
 verus! {
 
@@ -68,6 +69,16 @@ pub open spec fn frame_preserving_update<P: PCM>(a: P, b: P) -> bool {
     forall|c| #![trigger P::op(a, c), P::op(b, c)] P::op(a, c).valid() ==> P::op(b, c).valid()
 }
 
+pub open spec fn frame_preserving_update_nondeterministic<P: PCM>(a: P, bs: Set<P>) -> bool {
+    forall|c|
+        #![trigger P::op(a, c)]
+        P::op(a, c).valid() ==> exists|b| #[trigger] bs.contains(b) && P::op(b, c).valid()
+}
+
+pub open spec fn set_op<P: PCM>(s: Set<P>, t: P) -> Set<P> {
+    Set::new(|v| exists|q| s.contains(q) && v == P::op(q, t))
+}
+
 impl<P: PCM> Resource<P> {
     pub open spec fn value(self) -> P;
 
@@ -135,6 +146,17 @@ impl<P: PCM> Resource<P> {
         unimplemented!();
     }
 
+    #[verifier::external_body]
+    pub proof fn update_nondeterministic(tracked self, new_values: Set<P>) -> (tracked out: Self)
+        requires
+            frame_preserving_update_nondeterministic(self.value(), new_values),
+        ensures
+            out.loc() == self.loc(),
+            new_values.contains(out.value()),
+    {
+        unimplemented!();
+    }
+
     // Operations with shared references
     #[verifier::external_body]
     pub proof fn join_shared<'a>(
@@ -192,6 +214,25 @@ impl<P: PCM> Resource<P> {
     {
         unimplemented!();
     }
+
+    #[verifier::external_body]
+    pub proof fn update_nondeterministic_with_shared(
+        tracked self,
+        tracked other: &Self,
+        new_values: Set<P>,
+    ) -> (tracked out: Self)
+        requires
+            self.loc() == other.loc(),
+            frame_preserving_update_nondeterministic(
+                P::op(self.value(), other.value()),
+                set_op(new_values, other.value()),
+            ),
+        ensures
+            out.loc() == self.loc(),
+            new_values.contains(out.value()),
+    {
+        unimplemented!();
+    }
 }
 
 } // verus!

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

@@ -10,7 +10,7 @@ use builtin_macros::*;
 verus! {
 
 /// `Seq<A>` is a sequence type for specifications.
-/// To use a "sequence" in compiled code, use an `exec` type like [`vec::Vec`](crate::vec::Vec)
+/// To use a "sequence" in compiled code, use an `exec` type like `vec::Vec`
 /// that has `Seq<A>` as its specification type.
 ///
 /// An object `seq: Seq<A>` has a length, given by [`seq.len()`](Seq::len),

examples/verus-snapshot/source/vstd/source/vstd/std_specs/clone.rs

@@ -0,0 +1,64 @@
+use crate::prelude::*;
+use core::clone::Clone;
+
+verus! {
+
+// external_fn_specification doesn't generally support specifying generic functions
+// like this; it is special-cased for Clone for now
+#[verifier(external_fn_specification)]
+pub fn ex_clone_clone<T: Clone>(a: &T) -> T {
+    a.clone()
+}
+
+/*
+#[verifier(external_fn_specification)]
+pub fn ex_clone_clone_from<T: Clone>(a: &mut T, b: &T)
+{
+    a.clone_from(b)
+}
+*/
+
+#[verifier::external_fn_specification]
+pub fn ex_bool_clone(b: &bool) -> (res: bool)
+    ensures
+        res == b,
+{
+    b.clone()
+}
+
+#[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)
+    ensures
+        res == b,
+{
+    b.clone()
+}
+
+/*
+#[verifier::external_fn_specification]
+pub fn ex_bool_clone_from(dest: &mut bool, source: &bool)
+    ensures *dest == source,
+{
+    dest.clone_from(source)
+}
+*/
+
+// Cloning a Tracked copies the underlying ghost T
+#[verifier::external_fn_specification]
+pub fn ex_tracked_clone<T: Copy>(b: &Tracked<T>) -> (res: Tracked<T>)
+    ensures
+        res == b,
+{
+    b.clone()
+}
+
+#[verifier::external_fn_specification]
+pub fn ex_ghost_clone<T>(b: &Ghost<T>) -> (res: Ghost<T>)
+    ensures
+        res == b,
+{
+    b.clone()
+}
+
+} // verus!

examples/verus-snapshot/source/vstd/source/vstd/std_specs/mod.rs

@@ -1,5 +1,6 @@
 pub mod atomic;
 pub mod bits;
+pub mod clone;
 pub mod control_flow;
 pub mod core;
 pub mod num;

examples/verus-snapshot/source/vstd/source/vstd/std_specs/num.rs

@@ -14,6 +14,13 @@ 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 open spec fn wrapping_add(x: $uN, y: $uN) -> $uN {
                 if x + y > <$uN>::MAX {
                     (x + y - $range) as $uN
@@ -70,6 +77,13 @@ 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 open spec fn wrapping_add(x: $iN, y: $iN) -> $iN {
                 if x + y > <$iN>::MAX {
                     (x + y - $range) as $iN
@@ -151,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! {
 

examples/verus-snapshot/source/vstd/source/vstd/std_specs/vec.rs

@@ -3,9 +3,9 @@ use builtin::*;
 
 use alloc::vec::Vec;
 use core::alloc::Allocator;
+use core::clone::Clone;
 use core::option::Option;
 use core::option::Option::None;
-use core::option::Option::Some;
 
 verus! {
 
@@ -35,6 +35,14 @@ impl<T, A: Allocator> View for Vec<T, A> {
     spec fn view(&self) -> Seq<T>;
 }
 
+impl<T: DeepView, A: Allocator> DeepView for Vec<T, A> {
+    type V = Seq<T::V>;
+
+    open spec fn deep_view(&self) -> Seq<T::V> {
+        Seq::new(self.view().len(), |i: int| self[i].deep_view())
+    }
+}
+
 impl<T, A: Allocator> VecAdditionalSpecFns<T> for Vec<T, A> {
     #[verifier(inline)]
     open spec fn spec_len(&self) -> nat {
@@ -207,6 +215,37 @@ pub fn ex_vec_split_off<T, A: Allocator + core::clone::Clone>(
     vec.split_off(at)
 }
 
+pub open spec fn vec_clone_trigger<T, A: Allocator>(v1: Vec<T, A>, v2: Vec<T, A>) -> bool {
+    true
+}
+
+#[verifier::external_fn_specification]
+pub fn ex_vec_clone<T: Clone, A: Allocator + Clone>(vec: &Vec<T, A>) -> (res: Vec<T, A>)
+    ensures
+        res.len() == vec.len(),
+        forall|i|
+            #![all_triggers]
+            0 <= i < vec.len() ==> call_ensures(T::clone, (&vec[i],), res[i]),
+        vec_clone_trigger(*vec, res),
+        vec@ =~= res@ ==> vec@ == res@,
+{
+    vec.clone()
+}
+
+/*
+//TODO: improve pruning so that this is pruned away unless vec_clone_trigger is used
+#[verifier::external_body]
+#[verifier::broadcast_forall]
+pub proof fn vec_clone_deep_view_proof<T: DeepView, A: Allocator>(v1: Vec<T, A>, v2: Vec<T, A>)
+    requires
+        #[trigger] vec_clone_trigger(v1, v2),
+        v1.deep_view() =~= v2.deep_view(),
+    ensures
+        v1.deep_view() == v2.deep_view(),
+{
+}
+*/
+
 #[verifier::external_fn_specification]
 pub fn ex_vec_truncate<T, A: Allocator>(vec: &mut Vec<T, A>, len: usize)
     ensures