From 18d55e02c86cebdd5870120ea432cb3d7faf1a0d Mon Sep 17 00:00:00 2001
From: jaybosamiya <5683582+jaybosamiya@users.noreply.github.com>
Date: Mon, 25 Mar 2024 18:34:49 +0000
Subject: [PATCH] chore: update to latest Verus snapshot

---
 .../source/rust_verify/example/syntax.rs      | 143 ++++++++----------
 .../source/vstd/source/vstd/array.rs          |  31 ++++
 .../source/vstd/source/vstd/atomic.rs         |   8 +-
 .../source/vstd/source/vstd/atomic_ghost.rs   |  26 +---
 .../source/vstd/source/vstd/function.rs       |  18 +--
 .../source/vstd/source/vstd/modes.rs          |   1 -
 .../source/vstd/source/vstd/pcm.rs            |  41 +++++
 .../source/vstd/source/vstd/seq.rs            |   2 +-
 .../vstd/source/vstd/std_specs/clone.rs       |  64 ++++++++
 .../source/vstd/source/vstd/std_specs/mod.rs  |   1 +
 .../source/vstd/source/vstd/std_specs/num.rs  |  30 ++--
 .../source/vstd/source/vstd/std_specs/vec.rs  |  41 ++++-
 .../vstd/source/vstd/storage_protocol.rs      |  97 ++++++++++--
 .../source/vstd/source/vstd/view.rs           |  69 +++++++++
 14 files changed, 432 insertions(+), 140 deletions(-)
 create mode 100644 examples/verus-snapshot/source/vstd/source/vstd/std_specs/clone.rs

diff --git a/examples/verus-snapshot/source/rust_verify/example/syntax.rs b/examples/verus-snapshot/source/rust_verify/example/syntax.rs
index 33a479f..91c1237 100644
--- a/examples/verus-snapshot/source/rust_verify/example/syntax.rs
+++ b/examples/verus-snapshot/source/rust_verify/example/syntax.rs
@@ -1,10 +1,11 @@
 #![allow(unused_imports)]
-use builtin::*;
 use builtin_macros::*;
-use vstd::{modes::*, prelude::*, seq::*, *};
+use builtin::*;
+use vstd::{*, prelude::*, seq::*, modes::*};
 
 #[verifier::external]
-fn main() {}
+fn main() {
+}
 
 verus! {
 
@@ -54,8 +55,8 @@ fn test_my_funs(x: u32, y: u32)
     // my_proof_fun(x, y); // not allowed in exec code
     // let u = my_spec_fun(x, y); // not allowed exec code
     proof {
-        let u = my_spec_fun(x as int, y as int);  // allowed in proof code
-        my_proof_fun(u / 2, y as int);  // allowed in proof code
+        let u = my_spec_fun(x as int, y as int); // allowed in proof code
+        my_proof_fun(u / 2, y as int); // allowed in proof code
     }
 }
 
@@ -65,14 +66,12 @@ pub open spec fn my_pub_spec_fun1(x: int, y: int) -> int {
     // function and body visible to all
     x / 2 + y / 2
 }
-
 /* TODO
 pub open(crate) spec fn my_pub_spec_fun2(x: u32, y: u32) -> u32 {
     // function visible to all, body visible to crate
     x / 2 + y / 2
 }
 */
-
 // TODO(main_new) pub(crate) is not being handled correctly
 // pub(crate) open spec fn my_pub_spec_fun3(x: int, y: int) -> int {
 //     // function and body visible to crate
@@ -82,7 +81,6 @@ pub closed spec fn my_pub_spec_fun4(x: int, y: int) -> int {
     // function visible to all, body visible to module
     x / 2 + y / 2
 }
-
 pub(crate) closed spec fn my_pub_spec_fun5(x: int, y: int) -> int {
     // function visible to crate, body visible to module
     x / 2 + y / 2
@@ -94,7 +92,7 @@ fn test_rec(x: u64, y: u64)
     requires
         0 < x < 100,
         y < 100 - x,
-    decreases x,
+    decreases x
 {
     if x > 1 {
         test_rec(x - 1, y + 1);
@@ -104,7 +102,7 @@ fn test_rec(x: u64, y: u64)
 /// Multiple decreases clauses are ordered lexicographically, so that later clauses may
 /// increase when earlier clauses decrease.
 spec fn test_rec2(x: int, y: int) -> int
-    decreases x, y,
+    decreases x, y
 {
     if y > 0 {
         1 + test_rec2(x, y - 1)
@@ -122,15 +120,14 @@ spec fn test_rec2(x: int, y: int) -> int
 ///   - recommends .. "when" specifies a proof function that proves the
 ///     recommendations of the functions invoked in the body
 spec fn add0(a: nat, b: nat) -> nat
-    recommends
-        a > 0,
+    recommends a > 0
     via add0_recommends
 {
     a + b
 }
 
 spec fn dec0(a: int) -> int
-    decreases a,
+    decreases a
     when a > 0
     via dec0_decreases
 {
@@ -161,17 +158,17 @@ proof fn dec0_decreases(a: int) {
 ///   - variables in spec code are always ghost
 /// For example:
 fn test_my_funs2(
-    a: u32,  // exec variable
-    b: u32,  // exec variable
+    a: u32, // exec variable
+    b: u32, // exec variable
 )
     requires
         a < 100,
         b < 100,
 {
-    let s = a + b;  // s is an exec variable
+    let s = a + b; // s is an exec variable
     proof {
-        let u = a + b;  // u is a ghost variable
-        my_proof_fun(u / 2, b as int);  // my_proof_fun(x, y) takes ghost parameters x and y
+        let u = a + b; // u is a ghost variable
+        my_proof_fun(u / 2, b as int); // my_proof_fun(x, y) takes ghost parameters x and y
     }
 }
 
@@ -184,31 +181,27 @@ spec fn f1(i: int) -> int {
 
 fn assert_by_test() {
     assert(f1(3) > 3) by {
-        reveal(f1);  // reveal f1's definition just inside this block
+        reveal(f1); // reveal f1's definition just inside this block
     }
     assert(f1(3) > 3);
 }
 
 /// "assert by" can also invoke specialized provers for bit-vector reasoning or nonlinear arithmetic.
 fn assert_by_provers(x: u32) {
-    assert(x ^ x == 0u32) by (bit_vector);
-    assert(2 <= x && x < 10 ==> x * x > x) by (nonlinear_arith);
+    assert(x ^ x == 0u32) by(bit_vector);
+    assert(2 <= x && x < 10 ==> x * x > x) by(nonlinear_arith);
 }
 
 /// "assert by" provers can also appear on function signatures to select a specific prover
 /// for the function body.
 proof fn lemma_mul_upper_bound(x: int, x_bound: int, y: int, y_bound: int)
     by (nonlinear_arith)
-    requires
-        x <= x_bound,
-        y <= y_bound,
-        0 <= x,
-        0 <= y,
-    ensures
-        x * y <= x_bound * y_bound,
+    requires x <= x_bound, y <= y_bound, 0 <= x, 0 <= y,
+    ensures x * y <= x_bound * y_bound,
 {
 }
 
+
 /// "assert by" can use nonlinear_arith with proof code,
 /// where "requires" clauses selectively make facts available to the proof code.
 proof fn test5_bound_checking(x: u32, y: u32, z: u32)
@@ -217,7 +210,7 @@ proof fn test5_bound_checking(x: u32, y: u32, z: u32)
         y <= 0xffff,
         z <= 0xffff,
 {
-    assert(x * z == mul(x, z)) by (nonlinear_arith)
+    assert(x * z == mul(x, z)) by(nonlinear_arith)
         requires
             x <= 0xffff,
             z <= 0xffff,
@@ -241,6 +234,7 @@ fn test_assert_forall_by() {
     }
     assert(f1(1) + f1(2) == 5);
     assert(f1(3) + f1(4) == 9);
+
     // to prove forall|...| P ==> Q, write assert forall|...| P implies Q by {...}
     assert forall|x: int| x < 10 implies f1(x) < 11 by {
         assert(x < 10);
@@ -257,6 +251,7 @@ fn test_choose() {
         let x_witness = choose|x: int| f1(x) == 10;
         assert(f1(x_witness) == 10);
     }
+
     assume(exists|x: int, y: int| f1(x) + f1(y) == 30);
     proof {
         let (x_witness, y_witness): (int, int) = choose|x: int, y: int| f1(x) + f1(y) == 30;
@@ -270,11 +265,11 @@ fn test_single_trigger1() {
     // Use [my_spec_fun(x, y)] as the trigger
     assume(forall|x: int, y: int| f1(x) < 100 && f1(y) < 100 ==> #[trigger] my_spec_fun(x, y) >= x);
 }
-
 fn test_single_trigger2() {
     // Use [f1(x), f1(y)] as the trigger
-    assume(forall|x: int, y: int| #[trigger]
-        f1(x) < 100 && #[trigger] f1(y) < 100 ==> my_spec_fun(x, y) >= x);
+    assume(forall|x: int, y: int|
+        #[trigger] f1(x) < 100 && #[trigger] f1(y) < 100 ==> my_spec_fun(x, y) >= x
+    );
 }
 
 /// To manually specify multiple triggers, use #![trigger]:
@@ -283,7 +278,8 @@ fn test_multiple_triggers() {
     assume(forall|x: int, y: int|
         #![trigger my_spec_fun(x, y)]
         #![trigger f1(x), f1(y)]
-        f1(x) < 100 && f1(y) < 100 ==> my_spec_fun(x, y) >= x);
+        f1(x) < 100 && f1(y) < 100 ==> my_spec_fun(x, y) >= x
+    );
 }
 
 /// Verus can often automatically choose a trigger if no manual trigger is given.
@@ -311,17 +307,16 @@ spec fn simple_conjuncts(x: int, y: int) -> bool {
     &&& x < 100
     &&& y < 100
 }
-
 spec fn complex_conjuncts(x: int, y: int) -> bool {
     let b = x < y;
     &&& b
     &&& if false {
-        &&& b ==> b
-        &&& !b ==> !b
-    } else {
-        ||| b ==> b
-        ||| !b
-    }
+            &&& b ==> b
+            &&& !b ==> !b
+        } else {
+            ||| b ==> b
+            ||| !b
+        }
     &&& false ==> true
 }
 
@@ -333,14 +328,17 @@ pub(crate) proof fn binary_ops<A>(a: A, x: int) {
     assert(false ==> true);
     assert(true && false ==> false && false);
     assert(!(true && (false ==> false) && false));
+
     assert(false ==> false ==> false);
     assert(false ==> (false ==> false));
     assert(!((false ==> false) ==> false));
+
     assert(false <== false <== false);
     assert(!(false <== (false <== false)));
     assert((false <== false) <== false);
     assert(2 + 2 !== 3);
     assert(a == a);
+
     assert(false <==> true && false);
 }
 
@@ -363,7 +361,7 @@ fn test_views() {
     v.push(10);
     v.push(20);
     proof {
-        let s: Seq<u8> = v@;  // v@ is equivalent to v.view()
+        let s: Seq<u8> = v@; // v@ is equivalent to v.view()
         assert(s[0] == 10);
         assert(s[1] == 20);
     }
@@ -371,7 +369,10 @@ fn test_views() {
 
 /// struct and enum declarations may be declared exec (default), tracked, or ghost,
 /// and fields may be declared exec (default), tracked or ghost.
-tracked struct TrackedAndGhost<T, G>(tracked T, ghost G);
+tracked struct TrackedAndGhost<T, G>(
+    tracked T,
+    ghost G,
+);
 
 /// Proof code may manipulate tracked variables directly.
 /// Declarations of tracked variables must be explicitly marked as "tracked".
@@ -382,7 +383,7 @@ proof fn test_tracked(
     tracked w: int,
     tracked x: int,
     tracked y: int,
-    z: int,
+    z: int
 ) -> tracked TrackedAndGhost<(int, int), int> {
     consume(w);
     let tracked tag: TrackedAndGhost<(int, int), int> = TrackedAndGhost((x, y), z);
@@ -400,7 +401,7 @@ fn test_ghost(x: u32, y: u32)
     let ghost mut v = u + 1;
     assert(v == x + y + 1);
     proof {
-        v = v + 1;  // proof code may assign to ghost mut variables
+        v = v + 1; // proof code may assign to ghost mut variables
     }
     let ghost w = {
         let temp = v + 1;
@@ -426,21 +427,18 @@ fn test_ghost_wrappers(x: u32, y: Ghost<u32>)
     let mut v: Ghost<int> = Ghost(u@ + 1);
     assert(v@ == x + y@ + 1);
     proof {
-        v@ = v@ + 1;  // proof code may assign to the view of exec variables of type Ghost/Tracked
+        v@ = v@ + 1; // proof code may assign to the view of exec variables of type Ghost/Tracked
     }
-    let w: Ghost<int> = Ghost(
-        {
-            // proof block that returns a ghost value
-            let temp = v@ + 1;
-            temp + 1
-        },
-    );
+    let w: Ghost<int> = Ghost({
+        // proof block that returns a ghost value
+        let temp = v@ + 1;
+        temp + 1
+    });
     assert(w@ == x + y@ + 4);
 }
 
 fn test_consume(t: Tracked<int>)
-    requires
-        t@ <= 7,
+    requires t@ <= 7
 {
     proof {
         let tracked x = t.get();
@@ -450,10 +448,7 @@ fn test_consume(t: Tracked<int>)
 }
 
 /// Ghost(...) and Tracked(...) patterns can unwrap Ghost<...> and Tracked<...> values:
-fn test_ghost_unwrap(
-    x: u32,
-    Ghost(y): Ghost<u32>,
-)  // unwrap so that y has typ u32, not Ghost<u32>
+fn test_ghost_unwrap(x: u32, Ghost(y): Ghost<u32>) // unwrap so that y has typ u32, not Ghost<u32>
     requires
         x < 100,
         y < 100,
@@ -463,15 +458,13 @@ fn test_ghost_unwrap(
     let Ghost(mut v): Ghost<int> = Ghost(u + 1);
     assert(v == x + y + 1);
     proof {
-        v = v + 1;  // assign directly to ghost mut v
+        v = v + 1; // assign directly to ghost mut v
     }
-    let Ghost(w): Ghost<int> = Ghost(
-        {
-            // proof block that returns a ghost value
-            let temp = v + 1;
-            temp + 1
-        },
-    );
+    let Ghost(w): Ghost<int> = Ghost({
+        // proof block that returns a ghost value
+        let temp = v + 1;
+        temp + 1
+    });
     assert(w == x + y + 4);
 }
 
@@ -483,8 +476,10 @@ struct S {}
 fn test_ghost_tuple_match(t: (Tracked<S>, Tracked<S>, Ghost<int>, Ghost<int>)) -> Tracked<S> {
     let ghost g: (int, int) = (10, 20);
     assert(g.0 + g.1 == 30);
+
     let ghost (g1, g2) = g;
     assert(g1 + g2 == 30);
+
     // b1, b2: Tracked<S> and g3, g4: Ghost<int>
     let (Tracked(b1), Tracked(b2), Ghost(g3), Ghost(g4)) = t;
     Tracked(b2)
@@ -529,8 +524,7 @@ spec fn my_uninterpreted_fun1(i: int, j: int) -> int;
 spec fn my_uninterpreted_fun2(i: int, j: int) -> int
     recommends
         0 <= i < 10,
-        0 <= j < 10,
-;
+        0 <= j < 10;
 
 /// Trait functions may have specifications
 trait T {
@@ -540,8 +534,7 @@ trait T {
             0 <= j < 10,
         ensures
             i <= r,
-            j <= r,
-    ;
+            j <= r;
 }
 
 enum ThisOrThat {
@@ -552,7 +545,7 @@ enum ThisOrThat {
 proof fn uses_is(t: ThisOrThat) {
     match t {
         ThisOrThat::This(..) => assert(t is This),
-        ThisOrThat::That { .. } => assert(t is That),
+        ThisOrThat::That {..} => assert(t is That),
     }
 }
 
@@ -566,22 +559,20 @@ proof fn uses_arrow_matches_1(t: ThisOrThat)
 }
 
 proof fn uses_arrow_matches_2(t: ThisOrThat)
-    requires
-        t matches ThisOrThat::That { v: a } && a == 3,
+    requires t matches ThisOrThat::That { v: a } && a == 3,
 {
     assert(t is That && t->v == 3);
 }
 
 #[verifier::external_body]
-struct Collection {}
+struct Collection { }
 
 impl Collection {
     pub spec fn spec_has(&self, v: nat) -> bool;
 }
 
 proof fn uses_spec_has(c: Collection)
-    requires
-        c has 3,
+    requires c has 3,
 {
     assert(c has 3);
     assert(c has 3 == c has 3);
diff --git a/examples/verus-snapshot/source/vstd/source/vstd/array.rs b/examples/verus-snapshot/source/vstd/source/vstd/array.rs
index e5796ce..1cdacf0 100644
--- a/examples/verus-snapshot/source/vstd/source/vstd/array.rs
+++ b/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!
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/function.rs b/examples/verus-snapshot/source/vstd/source/vstd/function.rs
index f15cc50..4324d56 100644
--- a/examples/verus-snapshot/source/vstd/source/vstd/function.rs
+++ b/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
+          {}
+        }
     };
 }
 
diff --git a/examples/verus-snapshot/source/vstd/source/vstd/modes.rs b/examples/verus-snapshot/source/vstd/source/vstd/modes.rs
index 8be2930..ed0e708 100644
--- a/examples/verus-snapshot/source/vstd/source/vstd/modes.rs
+++ b/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
diff --git a/examples/verus-snapshot/source/vstd/source/vstd/pcm.rs b/examples/verus-snapshot/source/vstd/source/vstd/pcm.rs
index 418a46c..12f5cec 100644
--- a/examples/verus-snapshot/source/vstd/source/vstd/pcm.rs
+++ b/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!
diff --git a/examples/verus-snapshot/source/vstd/source/vstd/seq.rs b/examples/verus-snapshot/source/vstd/source/vstd/seq.rs
index 21d6669..ecdbdd3 100644
--- a/examples/verus-snapshot/source/vstd/source/vstd/seq.rs
+++ b/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),
diff --git a/examples/verus-snapshot/source/vstd/source/vstd/std_specs/clone.rs b/examples/verus-snapshot/source/vstd/source/vstd/std_specs/clone.rs
new file mode 100644
index 0000000..ed338bb
--- /dev/null
+++ b/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!
diff --git a/examples/verus-snapshot/source/vstd/source/vstd/std_specs/mod.rs b/examples/verus-snapshot/source/vstd/source/vstd/std_specs/mod.rs
index 103547a..ce2690e 100644
--- a/examples/verus-snapshot/source/vstd/source/vstd/std_specs/mod.rs
+++ b/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;
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 cebabdb..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
@@ -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! {
 
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 199de54..409f4ce 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
@@ -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
diff --git a/examples/verus-snapshot/source/vstd/source/vstd/storage_protocol.rs b/examples/verus-snapshot/source/vstd/source/vstd/storage_protocol.rs
index f5e246f..559cf24 100644
--- a/examples/verus-snapshot/source/vstd/source/vstd/storage_protocol.rs
+++ b/examples/verus-snapshot/source/vstd/source/vstd/storage_protocol.rs
@@ -13,19 +13,24 @@ verus! {
 /// [_Leaf: Modularity for Temporary Sharing in Separation Logic_](https://dl.acm.org/doi/10.1145/3622798).
 ///
 /// The reference for the laws and operations we're embedding here can be found at:
-/// <https://github.com/secure-foundations/leaf/blob/70c391162fa4c0198b0581ae274e68cc97204388/src/guarding/protocol.v#L31>
+/// <https://github.com/secure-foundations/leaf/blob/a51725deedecc88294057ac1502a7c7ff2104a69/src/guarding/protocol.v#L31>
 ///
 /// The reference version requires two monoids, the "protocol monoid" and the "base monoid".
 /// In this interface, we fix the base monoid to be of the form [`Map<K, V>`](crate::map::Map).
 /// (with composition of overlapping maps being undefined), which has all the necessary properties.
 /// Note that there's no `create_unit` (it's not sound to do this for an arbitrary location unless you
 /// already know a protocol was initialized at that location).
+///
+/// For applications, I generally advise using the
+/// [`tokenized_state_machine!` system](https://verus-lang.github.io/verus/state_machines/),
+/// rather than using this interface directly.
 #[verifier::external_body]
 #[verifier::accept_recursive_types(K)]
 #[verifier::accept_recursive_types(P)]
 #[verifier::accept_recursive_types(V)]
 pub tracked struct StorageResource<K, V, P> {
-    p: core::marker::PhantomData<(K, V, P)>,
+    _p: core::marker::PhantomData<(K, V, P)>,
+    _send_sync: crate::state_machine_internal::SyncSendIfSyncSend<Map<K, V>>,
 }
 
 /// See [`StorageResource`] for more information.
@@ -88,6 +93,25 @@ pub open spec fn exchanges<K, V, P: Protocol<K, V>>(
         ).interp().union_prefer_right(b1) =~= P::op(p2, q).interp().union_prefer_right(b2)
 }
 
+pub open spec fn exchanges_nondeterministic<K, V, P: Protocol<K, V>>(
+    p1: P,
+    b1: Map<K, V>,
+    new_values: Set<(P, Map<K, V>)>,
+) -> bool {
+    forall|q: P|
+        #![all_triggers]
+        P::op(p1, q).inv() ==> exists|p2, b2|
+            #![all_triggers]
+            new_values.contains((p2, b2)) && P::op(p2, q).inv() && P::op(
+                p1,
+                q,
+            ).interp().dom().disjoint(b1.dom()) && P::op(p2, q).interp().dom().disjoint(b2.dom())
+                && P::op(p1, q).interp().union_prefer_right(b1) =~= P::op(
+                p2,
+                q,
+            ).interp().union_prefer_right(b2)
+}
+
 pub open spec fn deposits<K, V, P: Protocol<K, V>>(p1: P, b1: Map<K, V>, p2: P) -> bool {
     forall|q: P|
         #![all_triggers]
@@ -108,6 +132,12 @@ pub open spec fn updates<K, V, P: Protocol<K, V>>(p1: P, p2: P) -> bool {
         P::op(p1, q).inv() ==> P::op(p2, q).inv() && P::op(p1, q).interp() =~= P::op(p2, q).interp()
 }
 
+pub open spec fn set_op<K, V, P: Protocol<K, V>>(s: Set<(P, Map<K, V>)>, t: P) -> Set<
+    (P, Map<K, V>),
+> {
+    Set::new(|v: (P, Map<K, V>)| exists|q| s.contains((q, v.1)) && v.0 == #[trigger] P::op(q, t))
+}
+
 impl<K, V, P: Protocol<K, V>> StorageResource<K, V, P> {
     pub open spec fn value(self) -> P;
 
@@ -161,7 +191,6 @@ impl<K, V, P: Protocol<K, V>> StorageResource<K, V, P> {
 
     // Updates and guards
     /// Most general kind of update, potentially depositing and withdrawing
-    #[verifier::external_body]
     pub proof fn exchange(
         tracked self,
         tracked base: Map<K, V>,
@@ -175,10 +204,10 @@ impl<K, V, P: Protocol<K, V>> StorageResource<K, V, P> {
             out.0.value() == new_value,
             out.1 == new_base,
     {
-        unimplemented!();
+        let s = set![(new_value, new_base)];
+        self.exchange_nondeterministic(base, s)
     }
 
-    #[verifier::external_body]
     pub proof fn deposit(tracked self, tracked base: Map<K, V>, new_value: P) -> (tracked out: Self)
         requires
             deposits(self.value(), base, new_value),
@@ -189,7 +218,6 @@ impl<K, V, P: Protocol<K, V>> StorageResource<K, V, P> {
         self.exchange(base, new_value, Map::empty()).0
     }
 
-    #[verifier::external_body]
     pub proof fn withdraw(tracked self, new_value: P, new_base: Map<K, V>) -> (tracked out: (
         Self,
         Map<K, V>,
@@ -205,7 +233,6 @@ impl<K, V, P: Protocol<K, V>> StorageResource<K, V, P> {
     }
 
     /// "Normal" update, no depositing or withdrawing
-    #[verifier::external_body]
     pub proof fn update(tracked self, new_value: P) -> (tracked out: Self)
         requires
             updates(self.value(), new_value),
@@ -216,6 +243,34 @@ impl<K, V, P: Protocol<K, V>> StorageResource<K, V, P> {
         self.exchange(Map::tracked_empty(), new_value, Map::empty()).0
     }
 
+    pub proof fn exchange_nondeterministic(
+        tracked self,
+        tracked base: Map<K, V>,
+        new_values: Set<(P, Map<K, V>)>,
+    ) -> (tracked out: (Self, Map<K, V>))
+        requires
+            exchanges_nondeterministic(self.value(), base, new_values),
+        ensures
+            out.0.loc() == self.loc(),
+            new_values.contains((out.0.value(), out.1)),
+    {
+        P::op_unit(self.value());
+        let tracked (selff, unit) = self.split(self.value(), P::unit());
+        let new_values0 = set_op(new_values, P::unit());
+        crate::set_lib::assert_sets_equal!(new_values0, new_values, v => {
+            P::op_unit(v.0);
+            if new_values.contains(v) {
+                assert(new_values0.contains(v));
+            }
+            if new_values0.contains(v) {
+                let q = choose |q| new_values.contains((q, v.1)) && v.0 == #[trigger] P::op(q, P::unit());
+                P::op_unit(q);
+                assert(new_values.contains(v));
+            }
+        });
+        selff.exchange_nondeterministic_with_shared(&unit, base, new_values)
+    }
+
     #[verifier::external_body]
     pub proof fn guard(tracked &self, b: Map<K, V>) -> (tracked out: &Map<K, V>)
         requires
@@ -266,8 +321,7 @@ impl<K, V, P: Protocol<K, V>> StorageResource<K, V, P> {
     }
 
     // See `logic_exchange_with_extra_guard`
-    // https://github.com/secure-foundations/leaf/blob/70c391162fa4c0198b0581ae274e68cc97204388/src/guarding/protocol.v#L503
-    #[verifier::external_body]
+    // https://github.com/secure-foundations/leaf/blob/a51725deedecc88294057ac1502a7c7ff2104a69/src/guarding/protocol.v#L720
     pub proof fn exchange_with_shared(
         tracked self,
         tracked other: &Self,
@@ -287,6 +341,31 @@ impl<K, V, P: Protocol<K, V>> StorageResource<K, V, P> {
             out.0.loc() == self.loc(),
             out.0.value() == new_value,
             out.1 == new_base,
+    {
+        let s = set![(new_value, new_base)];
+        self.exchange_nondeterministic_with_shared(other, base, s)
+    }
+
+    // See `logic_exchange_with_extra_guard_nondeterministic`
+    // https://github.com/secure-foundations/leaf/blob/a51725deedecc88294057ac1502a7c7ff2104a69/src/guarding/protocol.v#L834
+    /// Most general kind of update, potentially depositing and withdrawing
+    #[verifier::external_body]
+    pub proof fn exchange_nondeterministic_with_shared(
+        tracked self,
+        tracked other: &Self,
+        tracked base: Map<K, V>,
+        new_values: Set<(P, Map<K, V>)>,
+    ) -> (tracked out: (Self, Map<K, V>))
+        requires
+            self.loc() == other.loc(),
+            exchanges_nondeterministic(
+                P::op(self.value(), other.value()),
+                base,
+                set_op(new_values, other.value()),
+            ),
+        ensures
+            out.0.loc() == self.loc(),
+            new_values.contains((out.0.value(), out.1)),
     {
         unimplemented!();
     }
diff --git a/examples/verus-snapshot/source/vstd/source/vstd/view.rs b/examples/verus-snapshot/source/vstd/source/vstd/view.rs
index feaada6..16a2ad8 100644
--- a/examples/verus-snapshot/source/vstd/source/vstd/view.rs
+++ b/examples/verus-snapshot/source/vstd/source/vstd/view.rs
@@ -16,6 +16,12 @@ pub trait View {
     spec fn view(&self) -> Self::V;
 }
 
+pub trait DeepView {
+    type V;
+
+    spec fn deep_view(&self) -> Self::V;
+}
+
 impl<A: View> View for &A {
     type V = A::V;
 
@@ -25,6 +31,15 @@ impl<A: View> View for &A {
     }
 }
 
+impl<A: DeepView> DeepView for &A {
+    type V = A::V;
+
+    #[verifier::inline]
+    open spec fn deep_view(&self) -> A::V {
+        (**self).deep_view()
+    }
+}
+
 #[cfg(feature = "alloc")]
 impl<A: View> View for alloc::boxed::Box<A> {
     type V = A::V;
@@ -35,6 +50,16 @@ impl<A: View> View for alloc::boxed::Box<A> {
     }
 }
 
+#[cfg(feature = "alloc")]
+impl<A: DeepView> DeepView for alloc::boxed::Box<A> {
+    type V = A::V;
+
+    #[verifier::inline]
+    open spec fn deep_view(&self) -> A::V {
+        (**self).deep_view()
+    }
+}
+
 #[cfg(feature = "alloc")]
 impl<A: View> View for alloc::rc::Rc<A> {
     type V = A::V;
@@ -45,6 +70,16 @@ impl<A: View> View for alloc::rc::Rc<A> {
     }
 }
 
+#[cfg(feature = "alloc")]
+impl<A: DeepView> DeepView for alloc::rc::Rc<A> {
+    type V = A::V;
+
+    #[verifier::inline]
+    open spec fn deep_view(&self) -> A::V {
+        (**self).deep_view()
+    }
+}
+
 #[cfg(feature = "alloc")]
 impl<A: View> View for alloc::sync::Arc<A> {
     type V = A::V;
@@ -55,6 +90,16 @@ impl<A: View> View for alloc::sync::Arc<A> {
     }
 }
 
+#[cfg(feature = "alloc")]
+impl<A: DeepView> DeepView for alloc::sync::Arc<A> {
+    type V = A::V;
+
+    #[verifier::inline]
+    open spec fn deep_view(&self) -> A::V {
+        (**self).deep_view()
+    }
+}
+
 macro_rules! declare_identity_view {
     ($t:ty) => {
         #[cfg_attr(verus_keep_ghost, verifier::verify)]
@@ -69,6 +114,19 @@ macro_rules! declare_identity_view {
                 *self
             }
         }
+
+        #[cfg_attr(verus_keep_ghost, verifier::verify)]
+        impl DeepView for $t {
+            type V = $t;
+
+            #[cfg(verus_keep_ghost)]
+            #[verus::internal(spec)]
+            #[verus::internal(open)]
+            #[verifier::inline]
+            fn deep_view(&self) -> $t {
+                *self
+            }
+        }
     }
 }
 
@@ -112,6 +170,17 @@ macro_rules! declare_tuple_view {
                 ($(self.$n.view(), )*)
             }
         }
+
+        #[cfg_attr(verus_keep_ghost, verifier::verify)]
+        impl<$($a: DeepView, )*> DeepView for ($($a, )*) {
+            type V = ($($a::V, )*);
+            #[cfg(verus_keep_ghost)]
+            #[verus::internal(spec)]
+            #[verus::internal(open)]
+            fn deep_view(&self) -> ($($a::V, )*) {
+                ($(self.$n.deep_view(), )*)
+            }
+        }
     }
 }