From 6b720caf35b953811dc736a71ecb29ad0e532744 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
 <41898282+github-actions[bot]@users.noreply.github.com>
Date: Sun, 1 Dec 2024 03:46:30 +0000
Subject: [PATCH] Verus snapshot update (#108)

Automated verus snapshot update by GitHub Actions.
---
 .../verus-snapshot/source/vstd/compute.rs     |  40 ++
 .../verus-snapshot/source/vstd/prelude.rs     |  16 +
 .../verus-snapshot/source/vstd/raw_ptr.rs     |  87 +++
 examples/verus-snapshot/source/vstd/rwlock.rs |  35 +-
 .../verus-snapshot/source/vstd/seq_lib.rs     | 131 +++-
 .../source/vstd/std_specs/core.rs             |   2 +
 .../source/vstd/std_specs/hash.rs             |   2 +-
 .../source/vstd/std_specs/option.rs           |   9 +
 .../source/vstd/std_specs/smart_ptrs.rs       |   8 +
 examples/verus-snapshot/source/vstd/tokens.rs | 630 ++++++++++++++++++
 examples/verus-snapshot/source/vstd/vstd.rs   |   5 +
 11 files changed, 942 insertions(+), 23 deletions(-)
 create mode 100644 examples/verus-snapshot/source/vstd/compute.rs
 create mode 100644 examples/verus-snapshot/source/vstd/tokens.rs

diff --git a/examples/verus-snapshot/source/vstd/compute.rs b/examples/verus-snapshot/source/vstd/compute.rs
new file mode 100644
index 0000000..5e639d0
--- /dev/null
+++ b/examples/verus-snapshot/source/vstd/compute.rs
@@ -0,0 +1,40 @@
+use super::prelude::*;
+use core::ops::Range;
+
+verus! {
+
+/// Simplify proofs-by-computation for ranges of values
+pub trait RangeAll where Self: Sized {
+    /// Checks whether `p` holds for all values in this range.
+    /// See the [Verus tutorial](https://verus-lang.github.io/verus/guide/assert_by_compute.html) for example usage.
+    spec fn all_spec(self, p: spec_fn(int) -> bool) -> bool;
+}
+
+pub open spec fn range_all_spec_rec(r: Range<int>, p: spec_fn(int) -> bool) -> bool
+    decreases r.end - r.start,
+{
+    if r.start >= r.end {
+        true
+    } else {
+        p(r.start) && range_all_spec_rec(r.start + 1..r.end, p)
+    }
+}
+
+impl RangeAll for Range<int> {
+    open spec fn all_spec(self, p: spec_fn(int) -> bool) -> bool {
+        range_all_spec_rec(self, p)
+    }
+}
+
+pub broadcast proof fn all_spec_implies(r: Range<int>, p: spec_fn(int) -> bool)
+    ensures
+        #[trigger] r.all_spec(p) ==> (forall|i| r.start <= i < r.end ==> #[trigger] p(i)),
+    decreases r.end - r.start,
+{
+    if r.start >= r.end {
+    } else {
+        all_spec_implies(r.start + 1..r.end, p);
+    }
+}
+
+} // verus!
diff --git a/examples/verus-snapshot/source/vstd/prelude.rs b/examples/verus-snapshot/source/vstd/prelude.rs
index 438effb..9828d1d 100644
--- a/examples/verus-snapshot/source/vstd/prelude.rs
+++ b/examples/verus-snapshot/source/vstd/prelude.rs
@@ -39,3 +39,19 @@ pub use super::string::StrSliceExecFns;
 pub use super::string::StringExecFns;
 #[cfg(feature = "alloc")]
 pub use super::string::StringExecFnsIsAscii;
+
+#[cfg(verus_keep_ghost)]
+pub use super::tokens::CountToken;
+#[cfg(verus_keep_ghost)]
+pub use super::tokens::ElementToken;
+#[cfg(verus_keep_ghost)]
+pub use super::tokens::KeyValueToken;
+#[cfg(verus_keep_ghost)]
+pub use super::tokens::MonotonicCountToken;
+#[cfg(verus_keep_ghost)]
+pub use super::tokens::SimpleToken;
+#[cfg(verus_keep_ghost)]
+pub use super::tokens::ValueToken;
+
+#[cfg(verus_keep_ghost)]
+pub use super::tokens::InstanceId;
diff --git a/examples/verus-snapshot/source/vstd/raw_ptr.rs b/examples/verus-snapshot/source/vstd/raw_ptr.rs
index 3dd190e..bd0a6e6 100644
--- a/examples/verus-snapshot/source/vstd/raw_ptr.rs
+++ b/examples/verus-snapshot/source/vstd/raw_ptr.rs
@@ -757,4 +757,91 @@ pub fn deallocate(
     }
 }
 
+/// This is meant to be a replacement for `&'a T` that allows Verus to keep track of
+/// not just the `T` value but the pointer as well.
+/// It would be better to get rid of this and use normal reference types `&'a T`,
+/// but there are a lot of unsolved implementation questions.
+/// The existence of `SharedReference<'a, T>` is a stop-gap.
+#[verifier::external_body]
+#[verifier::accept_recursive_types(T)]
+pub struct SharedReference<'a, T>(&'a T);
+
+impl<'a, T> Clone for SharedReference<'a, T> {
+    #[verifier::external_body]
+    fn clone(&self) -> (ret: Self)
+        ensures
+            ret == *self,
+    {
+        SharedReference(self.0)
+    }
+}
+
+impl<'a, T> Copy for SharedReference<'a, T> {
+
+}
+
+impl<'a, T> SharedReference<'a, T> {
+    pub spec fn value(self) -> T;
+
+    pub spec fn ptr(self) -> *const T;
+
+    #[verifier::external_body]
+    fn new(t: &'a T) -> (s: Self)
+        ensures
+            s.value() == t,
+    {
+        SharedReference(t)
+    }
+
+    #[verifier::external_body]
+    fn as_ref(self) -> (t: &'a T)
+        ensures
+            t == self.value(),
+    {
+        self.0
+    }
+
+    #[verifier::external_body]
+    fn as_ptr(self) -> (ptr: *const T)
+        ensures
+            ptr == self.ptr(),
+    {
+        &*self.0
+    }
+
+    #[verifier::external_body]
+    proof fn points_to(tracked self) -> (tracked pt: &'a PointsTo<T>)
+        ensures
+            pt.ptr() == self.ptr(),
+            pt.is_init(),
+            pt.value() == self.value(),
+    {
+        unimplemented!();
+    }
+}
+
+/// Like [`ptr_ref`] but returns a `SharedReference` so it keeps track of the relationship
+/// between the pointers.
+/// Note the resulting reference's pointers does NOT have the same provenance.
+/// This is because in Rust models like Stacked Borrows / Tree Borrows, the pointer
+/// gets a new tag.
+#[inline(always)]
+#[verifier::external_body]
+pub fn ptr_ref2<'a, T>(ptr: *const T, Tracked(perm): Tracked<&PointsTo<T>>) -> (v: SharedReference<
+    'a,
+    T,
+>)
+    requires
+        perm.ptr() == ptr,
+        perm.is_init(),
+    ensures
+        v.value() == perm.value(),
+        v.ptr().addr() == ptr.addr(),
+        v.ptr()@.metadata == ptr@.metadata,
+    opens_invariants none
+    no_unwind
+{
+    SharedReference(unsafe { &*ptr })
+}
+
 } // verus!
diff --git a/examples/verus-snapshot/source/vstd/rwlock.rs b/examples/verus-snapshot/source/vstd/rwlock.rs
index baf6a09..fa2b673 100644
--- a/examples/verus-snapshot/source/vstd/rwlock.rs
+++ b/examples/verus-snapshot/source/vstd/rwlock.rs
@@ -348,13 +348,13 @@ struct_with_invariants_vstd!{
     #[verifier::type_invariant]
     spec fn wf(&self) -> bool {
         invariant on exc with (inst) is (v: bool, g: RwLockToks::flag_exc<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>) {
-            g@.instance == inst@
-                && g@.value == v
+            g.instance_id() == inst@.id()
+                && g.value() == v
         }
 
         invariant on rc with (inst) is (v: u64, g: RwLockToks::flag_rc<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>) {
-            g@.instance == inst@
-                && g@.value == v
+            g.instance_id() == inst@.id()
+                && g.value() == v
         }
 
         predicate {
@@ -392,7 +392,7 @@ impl<'a, V, Pred: RwLockPredicate<V>> WriteHandle<'a, V, Pred> {
     #[verifier::type_invariant]
     spec fn wf_write_handle(self) -> bool {
         equal(self.perm@.view().pcell, self.rwlock.cell.id()) && self.perm@.view().value.is_None()
-            && equal(self.handle@.view().instance, self.rwlock.inst@) && self.rwlock.wf()
+            && equal(self.handle@.instance_id(), self.rwlock.inst@.id()) && self.rwlock.wf()
     }
 
     pub closed spec fn rwlock(self) -> RwLock<V, Pred> {
@@ -421,15 +421,15 @@ impl<'a, V, Pred: RwLockPredicate<V>> WriteHandle<'a, V, Pred> {
 impl<'a, V, Pred: RwLockPredicate<V>> ReadHandle<'a, V, Pred> {
     #[verifier::type_invariant]
     spec fn wf_read_handle(self) -> bool {
-        equal(self.handle@.view().instance, self.rwlock.inst@)
-            && self.handle@.view().key.view().value.is_Some() && equal(
-            self.handle@.view().key.view().pcell,
+        equal(self.handle@.instance_id(), self.rwlock.inst@.id())
+            && self.handle@.element().view().value.is_Some() && equal(
+            self.handle@.element().view().pcell,
             self.rwlock.cell.id(),
-        ) && self.handle@.view().count == 1 && self.rwlock.wf()
+        ) && self.rwlock.wf()
     }
 
     pub closed spec fn view(self) -> V {
-        self.handle@.view().key.view().value.unwrap()
+        self.handle@.element().view().value.unwrap()
     }
 
     pub closed spec fn rwlock(self) -> RwLock<V, Pred> {
@@ -445,7 +445,7 @@ impl<'a, V, Pred: RwLockPredicate<V>> ReadHandle<'a, V, Pred> {
             use_type_invariant(self);
         }
         let tracked perm = self.rwlock.inst.borrow().read_guard(
-            self.handle@.view().key,
+            self.handle@.element(),
             self.handle.borrow(),
         );
         self.rwlock.cell.borrow(Tracked(&perm))
@@ -463,8 +463,8 @@ impl<'a, V, Pred: RwLockPredicate<V>> ReadHandle<'a, V, Pred> {
         use_type_invariant(read_handle1);
         use_type_invariant(read_handle2);
         read_handle1.rwlock.inst.borrow().read_match(
-            read_handle1.handle@.view().key,
-            read_handle2.handle@.view().key,
+            read_handle1.handle@.element(),
+            read_handle2.handle@.element(),
             &read_handle1.handle.borrow(),
             &read_handle2.handle.borrow(),
         );
@@ -481,7 +481,7 @@ impl<'a, V, Pred: RwLockPredicate<V>> ReadHandle<'a, V, Pred> {
             &rwlock.rc => fetch_sub(1);
             ghost g =>
         {
-            rwlock.inst.borrow().release_shared(handle.view().key, &mut g, handle);
+            rwlock.inst.borrow().release_shared(handle.element(), &mut g, handle);
         });
     }
 }
@@ -542,7 +542,10 @@ impl<V, Pred: RwLockPredicate<V>> RwLock<V, Pred> {
         > = Option::None;
         while !done
             invariant
-                done ==> token.is_Some() && equal(token.get_Some_0().view().instance, self.inst@),
+                done ==> token.is_Some() && equal(
+                    token.get_Some_0().instance_id(),
+                    self.inst@.id(),
+                ),
                 self.wf(),
         {
             let result =
@@ -564,7 +567,7 @@ impl<V, Pred: RwLockPredicate<V>> RwLock<V, Pred> {
         }
         loop
             invariant
-                token.is_Some() && equal(token.get_Some_0().view().instance, self.inst@),
+                token.is_Some() && equal(token.get_Some_0().instance_id(), self.inst@.id()),
                 self.wf(),
         {
             let tracked mut perm_opt: Option<PointsTo<V>> = None;
diff --git a/examples/verus-snapshot/source/vstd/seq_lib.rs b/examples/verus-snapshot/source/vstd/seq_lib.rs
index 6bfc056..f047487 100644
--- a/examples/verus-snapshot/source/vstd/seq_lib.rs
+++ b/examples/verus-snapshot/source/vstd/seq_lib.rs
@@ -446,6 +446,9 @@ impl<A> Seq<A> {
     pub proof fn to_multiset_ensures(self)
         ensures
             forall|a: A| #[trigger] (self.push(a).to_multiset()) =~= self.to_multiset().insert(a),
+            forall|i: int|
+                0 <= i < self.len() ==> #[trigger] (self.remove(i).to_multiset())
+                    =~= self.to_multiset().remove(self[i]),
             self.len() == self.to_multiset().len(),
             forall|a: A| self.contains(a) <==> #[trigger] self.to_multiset().count(a) > 0,
     {
@@ -453,6 +456,10 @@ impl<A> Seq<A> {
             (self.push(a).to_multiset()) =~= self.to_multiset().insert(a) by {
             to_multiset_build(self, a);
         }
+        assert forall|i: int| 0 <= i < self.len() implies #[trigger] (self.remove(i).to_multiset())
+            =~= self.to_multiset().remove(self[i]) by {
+            to_multiset_remove(self, i);
+        }
         to_multiset_len(self);
         assert forall|a: A| self.contains(a) <==> #[trigger] self.to_multiset().count(a) > 0 by {
             to_multiset_contains(self, a);
@@ -646,20 +653,22 @@ impl<A> Seq<A> {
         }
     }
 
-    /// An auxiliary lemma for proving [`Self::lemma_fold_right_alt`].
-    proof fn aux_lemma_fold_right_alt<B>(self, f: spec_fn(A, B) -> B, b: B, k: int)
+    /// A lemma that proves how [`Self::fold_right`] distributes over splitting a sequence.
+    pub proof fn lemma_fold_right_split<B>(self, f: spec_fn(A, B) -> B, b: B, k: int)
         requires
-            0 <= k < self.len(),
+            0 <= k <= self.len(),
         ensures
             self.subrange(0, k).fold_right(f, self.subrange(k, self.len() as int).fold_right(f, b))
                 == self.fold_right(f, b),
         decreases self.len(),
     {
         reveal_with_fuel(Seq::fold_right, 2);
-        if k == self.len() - 1 {
+        if k == self.len() {
+            assert(self.subrange(0, k) == self);
+        } else if k == self.len() - 1 {
             // trivial base case
         } else {
-            self.subrange(0, self.len() - 1).aux_lemma_fold_right_alt(f, f(self.last(), b), k);
+            self.subrange(0, self.len() - 1).lemma_fold_right_split(f, f(self.last(), b), k);
             assert_seqs_equal!(
                 self.subrange(0, self.len() - 1).subrange(0, k) ==
                 self.subrange(0, k)
@@ -675,6 +684,19 @@ impl<A> Seq<A> {
         }
     }
 
+    // Lemma that proves it's possible to commute a commutative operator across fold_right.
+    pub proof fn lemma_fold_right_commute_one<B>(self, a: A, f: spec_fn(A, B) -> B, v: B)
+        requires
+            commutative_foldr(f),
+        ensures
+            self.fold_right(f, f(a, v)) == f(a, self.fold_right(f, v)),
+        decreases self.len(),
+    {
+        if self.len() > 0 {
+            self.drop_last().lemma_fold_right_commute_one(a, f, f(self.last(), v));
+        }
+    }
+
     /// [`Self::fold_right`] and [`Self::fold_right_alt`] are equivalent.
     pub proof fn lemma_fold_right_alt<B>(self, f: spec_fn(A, B) -> B, b: B)
         ensures
@@ -687,7 +709,7 @@ impl<A> Seq<A> {
             // trivial base cases
         } else {
             self.subrange(1, self.len() as int).lemma_fold_right_alt(f, b);
-            self.aux_lemma_fold_right_alt(f, b, 1);
+            self.lemma_fold_right_split(f, b, 1);
         }
     }
 
@@ -713,6 +735,43 @@ impl<A> Seq<A> {
         }
     }
 
+    /// If, in a sequence's conversion to a multiset, each element occurs only once,
+    /// the sequence has no duplicates.
+    pub proof fn lemma_multiset_has_no_duplicates_conv(self)
+        requires
+            forall|x: A| self.to_multiset().contains(x) ==> self.to_multiset().count(x) == 1,
+        ensures
+            self.no_duplicates(),
+    {
+        broadcast use super::multiset::group_multiset_axioms;
+
+        assert forall|i, j| (0 <= i < self.len() && 0 <= j < self.len() && i != j) implies self[i]
+            != self[j] by {
+            let mut a = if (i < j) {
+                i
+            } else {
+                j
+            };
+            let mut b = if (i < j) {
+                j
+            } else {
+                i
+            };
+
+            if (self[a] == self[b]) {
+                let s0 = self.subrange(0, b);
+                let s1 = self.subrange(b, self.len() as int);
+                assert(self == s0 + s1);
+
+                s0.to_multiset_ensures();
+                s1.to_multiset_ensures();
+
+                lemma_multiset_commutative(s0, s1);
+                assert(self.to_multiset().count(self[a]) >= 2);
+            }
+        }
+    }
+
     /// The concatenation of two subsequences derived from a non-empty sequence,
     /// the first obtained from skipping the last element, the second consisting only
     /// of the last element, is the original sequence.
@@ -1320,6 +1379,23 @@ proof fn to_multiset_build<A>(s: Seq<A>, a: A)
     }
 }
 
+proof fn to_multiset_remove<A>(s: Seq<A>, i: int)
+    requires
+        0 <= i < s.len(),
+    ensures
+        s.remove(i).to_multiset() =~= s.to_multiset().remove(s[i]),
+{
+    broadcast use super::multiset::group_multiset_axioms;
+
+    let s0 = s.subrange(0, i);
+    let s1 = s.subrange(i, s.len() as int);
+    let s2 = s.subrange(i + 1, s.len() as int);
+    lemma_seq_union_to_multiset_commutative(s0, s2);
+    lemma_seq_union_to_multiset_commutative(s0, s1);
+    assert(s == s0 + s1);
+    assert(s2 + s0 == (s1 + s0).drop_first());
+}
+
 /// to_multiset() preserves length
 proof fn to_multiset_len<A>(s: Seq<A>)
     ensures
@@ -1669,6 +1745,49 @@ pub proof fn lemma_seq_subrange_elements<A>(s: Seq<A>, start: int, stop: int, x:
     }
 }
 
+// Definition of a commutative fold_right operator.
+pub open spec fn commutative_foldr<A, B>(f: spec_fn(A, B) -> B) -> bool {
+    forall|x: A, y: A, v: B| #[trigger] f(x, f(y, v)) == f(y, f(x, v))
+}
+
+// For a commutative fold_right operator, any folding order
+// (i.e., any permutation) produces the same result.
+pub proof fn lemma_fold_right_permutation<A, B>(l1: Seq<A>, l2: Seq<A>, f: spec_fn(A, B) -> B, v: B)
+    requires
+        commutative_foldr(f),
+        l1.to_multiset() == l2.to_multiset(),
+    ensures
+        l1.fold_right(f, v) == l2.fold_right(f, v),
+    decreases l1.len(),
+{
+    l1.to_multiset_ensures();
+    l2.to_multiset_ensures();
+
+    if l1.len() > 0 {
+        let a = l1.last();
+        let i = l2.index_of(a);
+        let l2r = l2.subrange(i + 1, l2.len() as int).fold_right(f, v);
+
+        assert(l1.to_multiset().count(a) > 0);
+        l1.drop_last().lemma_fold_right_commute_one(a, f, v);
+        l2.subrange(0, i).lemma_fold_right_commute_one(a, f, l2r);
+
+        l2.lemma_fold_right_split(f, v, i + 1);
+        l2.remove(i).lemma_fold_right_split(f, v, i);
+
+        assert(l2.subrange(0, i + 1).drop_last() == l2.subrange(0, i));
+        assert(l1.drop_last() == l1.remove(l1.len() - 1));
+
+        assert(l2.remove(i).subrange(0, i) == l2.subrange(0, i));
+        assert(l2.remove(i).subrange(i, l2.remove(i).len() as int) == l2.subrange(
+            i + 1,
+            l2.len() as int,
+        ));
+
+        lemma_fold_right_permutation(l1.drop_last(), l2.remove(i), f, v);
+    }
+}
+
 /************************** Lemmas about Take/Skip ***************************/
 
 // This verified lemma used to be an axiom in the Dafny prelude
diff --git a/examples/verus-snapshot/source/vstd/std_specs/core.rs b/examples/verus-snapshot/source/vstd/std_specs/core.rs
index 82ed862..1a3f3a1 100644
--- a/examples/verus-snapshot/source/vstd/std_specs/core.rs
+++ b/examples/verus-snapshot/source/vstd/std_specs/core.rs
@@ -95,6 +95,8 @@ pub fn ex_swap<T>(a: &mut T, b: &mut T)
     ensures
         *a == *old(b),
         *b == *old(a),
+    opens_invariants none
+    no_unwind
 {
     core::mem::swap(a, b)
 }
diff --git a/examples/verus-snapshot/source/vstd/std_specs/hash.rs b/examples/verus-snapshot/source/vstd/std_specs/hash.rs
index 90f5724..45200d1 100644
--- a/examples/verus-snapshot/source/vstd/std_specs/hash.rs
+++ b/examples/verus-snapshot/source/vstd/std_specs/hash.rs
@@ -73,7 +73,7 @@ pub fn ex_default_hasher_new() -> (result: DefaultHasher)
 #[verifier::external_fn_specification]
 pub fn ex_default_hasher_write(state: &mut DefaultHasher, bytes: &[u8])
     ensures
-        state@ == old::<&mut _>(state)@.push(bytes@),
+        state@ == old(state)@.push(bytes@),
 {
     state.write(bytes)
 }
diff --git a/examples/verus-snapshot/source/vstd/std_specs/option.rs b/examples/verus-snapshot/source/vstd/std_specs/option.rs
index c4aa050..ca21775 100644
--- a/examples/verus-snapshot/source/vstd/std_specs/option.rs
+++ b/examples/verus-snapshot/source/vstd/std_specs/option.rs
@@ -179,4 +179,13 @@ pub fn ex_map<T, U, F: FnOnce(T) -> U>(a: Option<T>, f: F) -> (ret: Option<U>)
     a.map(f)
 }
 
+#[verifier::external_fn_specification]
+pub fn ex_option_clone<T: Clone>(opt: &Option<T>) -> (res: Option<T>)
+    ensures
+        opt.is_none() ==> res.is_none(),
+        opt.is_some() ==> res.is_some() && call_ensures(T::clone, (&opt.unwrap(),), res.unwrap()),
+{
+    opt.clone()
+}
+
 } // verus!
diff --git a/examples/verus-snapshot/source/vstd/std_specs/smart_ptrs.rs b/examples/verus-snapshot/source/vstd/std_specs/smart_ptrs.rs
index b33d7c1..c21edd4 100644
--- a/examples/verus-snapshot/source/vstd/std_specs/smart_ptrs.rs
+++ b/examples/verus-snapshot/source/vstd/std_specs/smart_ptrs.rs
@@ -40,4 +40,12 @@ pub fn arc_new<T>(t: T) -> (v: Arc<T>)
     Arc::new(t)
 }
 
+#[verifier::external_fn_specification]
+pub fn box_clone<T: Clone, A: Allocator + Clone>(b: &Box<T, A>) -> (res: Box<T, A>)
+    ensures
+        call_ensures(T::clone, (&**b,), *res),
+{
+    b.clone()
+}
+
 } // verus!
diff --git a/examples/verus-snapshot/source/vstd/tokens.rs b/examples/verus-snapshot/source/vstd/tokens.rs
new file mode 100644
index 0000000..55ab4ad
--- /dev/null
+++ b/examples/verus-snapshot/source/vstd/tokens.rs
@@ -0,0 +1,630 @@
+use super::multiset::*;
+use super::prelude::*;
+use core::marker::PhantomData;
+
+use verus as verus_;
+verus_! {
+
+// Note that the tokenized_state_machine! macro creates trusted implementations
+// of all these traits. Therefore all the proof functions in here are trusted.
+// The 'collection types', (MapToken, SetToken, MultisetToken) are verified, but the properties
+// of these types is still assumed by the Verus macro, so they're still mostly trusted.
+
+#[verusfmt::skip]
+broadcast use
+    super::set_lib::group_set_lib_axioms,
+    super::set::group_set_axioms,
+    super::map::group_map_axioms;
+
+/// Unique identifier for every VerusSync instance.
+/// Every "Token" and "Instance" object has an `InstanceId`. These ID values must agree
+/// to perform any token operation.
+pub ghost struct InstanceId(pub int);
+
+/// Interface for VerusSync tokens created for a field marked with the
+/// `variable`, `option` or `persistent_option` strategies.
+///
+/// | VerusSync Strategy  | Field type  | Token trait            |
+/// |---------------------|-------------|------------------------|
+/// | `variable`          | `V`         | [`UniqueValueToken<V>`](`UniqueValueToken`)        |
+/// | `option`            | `Option<V>` | [`UniqueValueToken<V>`](`UniqueValueToken`)        |
+/// | `persistent_option` | `Option<V>` | `ValueToken<V> + Copy` |
+///
+/// For the cases where the tokens are not `Copy`, then token is necessarily _unique_
+/// per-instance; the sub-trait, [`UniqueValueToken<V>`](`UniqueValueToken`), provides
+/// an additional lemma to prove uniqueness.
+
+pub trait ValueToken<Value> : Sized {
+    spec fn instance_id(&self) -> InstanceId;
+    spec fn value(&self) -> Value;
+
+    /// All tokens (for the same instance) must agree on the value.
+    proof fn agree(tracked &self, tracked other: &Self)
+        requires self.instance_id() == other.instance_id(),
+        ensures self.value() == other.value();
+
+    /// Return an arbitrary token. It's not possible to do anything interesting
+    /// with this token because it doesn't have a specified instance.
+    proof fn arbitrary() -> (tracked s: Self);
+}
+
+/// Interface for VerusSync tokens created for a field marked with the `variable` or `option` strategies.
+///
+/// See the super-trait [`ValueToken`](ValueToken) for more information.
+pub trait UniqueValueToken<Value> : ValueToken<Value> {
+    /// The token for a given instance must be unique; in other words, if we have two
+    /// tokens, they must be for distinct instances.
+    /// Though the first argument is mutable, the value is not really mutated;
+    /// this is only used to ensure unique ownership of the argument.
+    proof fn unique(tracked &mut self, tracked other: &Self)
+        ensures
+            self.instance_id() != other.instance_id(),
+            *self == *old(self);
+}
+
+/// Interface for VerusSync tokens created for a field marked with the
+/// `map` or `persistent_map` strategies.
+///
+/// | VerusSync Strategy  | Field type  | Token trait            |
+/// |---------------------|-------------|------------------------|
+/// | `map`               | `Map<K, V>` | [`UniqueKeyValueToken<K, V>`](`UniqueKeyValueToken`) |
+/// | `persistent_map`    | `Map<K, V>` | `KeyValueToken<V> + Copy` |
+///
+/// For the cases where the tokens are not `Copy`, then token is necessarily _unique_
+/// per-instance, per-key; the sub-trait, [`UniqueKeyValueToken<V>`](`UniqueKeyValueToken`), provides
+/// an additional lemma to prove uniqueness.
+///
+/// Each token represents a _single_ key-value pair.
+/// To work with a collection of `KeyValueToken`s, use [`MapToken`].
+
+pub trait KeyValueToken<Key, Value> : Sized {
+    spec fn instance_id(&self) -> InstanceId;
+    spec fn key(&self) -> Key;
+    spec fn value(&self) -> Value;
+
+    /// All tokens, for the same instance and _key_, must agree on the value.
+    proof fn agree(tracked &self, tracked other: &Self)
+        requires self.instance_id() == other.instance_id(),
+                 self.key() == other.key(),
+        ensures self.value() == other.value();
+
+    /// Return an arbitrary token. It's not possible to do anything interesting
+    /// with this token because it doesn't have a specified instance.
+    proof fn arbitrary() -> (tracked s: Self);
+}
+
+/// Interface for VerusSync tokens created for a field marked with the `map` strategy.
+///
+/// See the super-trait [`KeyValueToken`](KeyValueToken) for more information.
+pub trait UniqueKeyValueToken<Key, Value> : KeyValueToken<Key, Value> {
+    /// The token for a given instance and key must be unique; in other words, if we have two
+    /// tokens, they must be for distinct instances or keys.
+    /// Though the first argument is mutable, the value is not really mutated;
+    /// this is only used to ensure unique ownership of the argument.
+    proof fn unique(tracked &mut self, tracked other: &Self)
+        ensures
+            self.instance_id() != other.instance_id() || self.key() != other.key(),
+            *self == *old(self);
+}
+
+/// Interface for VerusSync tokens created for a field marked with the `count` strategy.
+///
+/// | VerusSync Strategy  | Field type  | Token trait            |
+/// |---------------------|-------------|------------------------|
+/// | `count`             | `nat`       | `CountToken`           |
+///
+/// These tokens are "fungible" in the sense that they can be combined and split, numbers
+/// combining additively.
+///
+/// (For the `persistent_count` strategy, see [`MonotonicCountToken`].)
+pub trait CountToken : Sized {
+    spec fn instance_id(&self) -> InstanceId;
+    spec fn count(&self) -> nat;
+
+    proof fn join(tracked &mut self, tracked other: Self)
+        requires
+            old(self).instance_id() == other.instance_id(),
+        ensures
+            self.instance_id() == old(self).instance_id(),
+            self.count() == old(self).count() + other.count();
+
+    proof fn split(tracked &mut self, count: nat) -> (tracked token: Self)
+        requires
+            count <= old(self).count()
+        ensures
+            self.instance_id() == old(self).instance_id(),
+            self.count() == old(self).count() - count,
+            token.instance_id() == old(self).instance_id(),
+            token.count() == count;
+
+    proof fn weaken_shared(tracked &self, count: nat) -> (tracked s: &Self)
+        requires count <= self.count(),
+        ensures s.instance_id() == self.instance_id(),
+            s.count() == count;
+
+    /// Return an arbitrary token. It's not possible to do anything interesting
+    /// with this token because it doesn't have a specified instance.
+    proof fn arbitrary() -> (tracked s: Self);
+}
+
+/// Interface for VerusSync tokens created for a field marked with the `persistent_count` strategy.
+///
+/// | VerusSync Strategy  | Field type  | Token trait                   |
+/// |---------------------|-------------|-------------------------------|
+/// | `persistent_count`  | `nat`       | `MonotonicCountToken + Copy`  |
+///
+/// A token represents a "lower bound" on the field value, which increases monotonically.
+
+pub trait MonotonicCountToken : Sized {
+    spec fn instance_id(&self) -> InstanceId;
+    spec fn count(&self) -> nat;
+
+    proof fn weaken(tracked &self, count: nat) -> (tracked s: Self)
+        requires count <= self.count(),
+        ensures s.instance_id() == self.instance_id(),
+            s.count() == count;
+
+    /// Return an arbitrary token. It's not possible to do anything interesting
+    /// with this token because it doesn't have a specified instance.
+    proof fn arbitrary() -> (tracked s: Self);
+}
+
+/// Interface for VerusSync tokens created for a field marked with the
+/// `set`, `persistent_set` or `multiset` strategies.
+///
+/// | VerusSync Strategy  | Field type  | Token trait            |
+/// |---------------------|-------------|------------------------|
+/// | `set`               | `Set<V>`    | [`UniqueElementToken<V>`](`UniqueElementToken`) |
+/// | `persistent_set`    | `Set<V>`    | `ElementToken<V> + Copy` |
+/// | `multiset`          | `Multiset<V>` | `ElementToken<V>`      |
+///
+/// Each token represents a single element of the set or multiset.
+///
+///  * For the `set` strategy, the token for any given element is unique.
+///  * For the `persistent_set` strategy, the token for any given element is not unique, but is `Copy`.
+///  * For the `multiset` strategy, the tokens are neither unique nor `Copy`, as the specific
+///    multiplicity of each element must be exact.
+///
+/// To work with a collection of `ElementToken`s, use [`SetToken`] or [`MultisetToken`].
+
+pub trait ElementToken<Element> : Sized {
+    spec fn instance_id(&self) -> InstanceId;
+    spec fn element(&self) -> Element;
+
+    /// Return an arbitrary token. It's not possible to do anything interesting
+    /// with this token because it doesn't have a specified instance.
+    proof fn arbitrary() -> (tracked s: Self);
+}
+
+/// Interface for VerusSync tokens created for a field marked with the `set` strategy.
+///
+/// See the super-trait [`ElementToken`](ElementToken) for more information.
+pub trait UniqueElementToken<Element> : ElementToken<Element> {
+    /// The token for a given instance and element must be unique; in other words, if we have two
+    /// tokens, they must be for distinct instances or elements.
+    /// Though the first argument is mutable, the value is not really mutated;
+    /// this is only used to ensure unique ownership of the argument.
+    proof fn unique(tracked &mut self, tracked other: &Self)
+        ensures
+            self.instance_id() == other.instance_id() ==> self.element() != other.element(),
+            *self == *old(self);
+}
+
+/// Interface for VerusSync tokens created for a field marked with the `bool` or
+/// `persistent_bool` strategy.
+///
+/// | VerusSync Strategy  | Field type  | Token trait            |
+/// |---------------------|-------------|------------------------|
+/// | `bool`              | `bool`      | [`UniqueSimpleToken<V>`](`UniqueSimpleToken`) |
+/// | `persistent_bool`   | `bool`      | `SimpleToken<V> + Copy` |
+///
+/// The token contains no additional data; its presence indicates that the boolean field
+/// is `true`.
+pub trait SimpleToken : Sized {
+    spec fn instance_id(&self) -> InstanceId;
+
+    /// Return an arbitrary token. It's not possible to do anything interesting
+    /// with this token because it doesn't have a specified instance.
+    proof fn arbitrary() -> (tracked s: Self);
+}
+
+/// Interface for VerusSync tokens created for a field marked with the `bool` strategy.
+///
+/// See the super-trait [`SimpleToken`](SimpleToken) for more information.
+pub trait UniqueSimpleToken : SimpleToken {
+    /// The token for a given instance must be unique; in other words, if we have two
+    /// tokens, they must be for distinct instances.
+    /// Though the first argument is mutable, the value is not really mutated;
+    /// this is only used to ensure unique ownership of the argument.
+    proof fn unique(tracked &mut self, tracked other: &Self)
+        ensures
+            self.instance_id() != other.instance_id(),
+            *self == *old(self);
+}
+
+#[verifier::reject_recursive_types(Key)]
+pub tracked struct MapToken<Key, Value, Token>
+    where Token: KeyValueToken<Key, Value>
+{
+    ghost _v: PhantomData<Value>,
+    ghost inst: InstanceId,
+    tracked m: Map<Key, Token>,
+}
+
+impl<Key, Value, Token> MapToken<Key, Value, Token>
+    where Token: KeyValueToken<Key, Value>
+{
+    #[verifier::type_invariant]
+    spec fn wf(self) -> bool {
+        forall |k| #[trigger] self.m.dom().contains(k) ==> self.m[k].key() == k
+            && self.m[k].instance_id() == self.inst
+    }
+
+    pub closed spec fn instance_id(self) -> InstanceId {
+        self.inst
+    }
+
+    pub closed spec fn map(self) -> Map<Key, Value> {
+        Map::new(
+            |k: Key| self.m.dom().contains(k),
+            |k: Key| self.m[k].value(),
+        )
+    }
+
+    #[verifier::inline]
+    pub open spec fn dom(self) -> Set<Key> {
+        self.map().dom()
+    }
+
+    #[verifier::inline]
+    pub open spec fn spec_index(self, k: Key) -> Value {
+        self.map()[k]
+    }
+
+    #[verifier::inline]
+    pub open spec fn index(self, k: Key) -> Value {
+        self.map()[k]
+    }
+
+    pub proof fn empty(instance_id: InstanceId) -> (tracked s: Self)
+        ensures
+            s.instance_id() == instance_id,
+            s.map() === Map::empty(),
+    {
+        let tracked s = Self { inst: instance_id, m: Map::tracked_empty(), _v: PhantomData };
+        assert(s.map() =~= Map::empty());
+        return s;
+    }
+
+    pub proof fn insert(tracked &mut self, tracked token: Token)
+        requires
+            old(self).instance_id() == token.instance_id(),
+        ensures
+            self.instance_id() == old(self).instance_id(),
+            self.map() == old(self).map().insert(token.key(), token.value()),
+    {
+        use_type_invariant(&*self);
+        self.m.tracked_insert(token.key(), token);
+        assert(self.map() =~= old(self).map().insert(token.key(), token.value()));
+    }
+
+    pub proof fn remove(tracked &mut self, key: Key) -> (tracked token: Token)
+        requires
+            old(self).map().dom().contains(key)
+        ensures
+            self.instance_id() == old(self).instance_id(),
+            self.map() == old(self).map().remove(key),
+            token.instance_id() == self.instance_id(),
+            token.key() == key,
+            token.value() == old(self).map()[key]
+    {
+        use_type_invariant(&*self);
+        let tracked t = self.m.tracked_remove(key);
+        assert(self.map() =~= old(self).map().remove(key));
+        t
+    }
+
+    pub proof fn into_map(tracked self) -> (tracked map: Map<Key, Token>)
+        ensures
+            map.dom() == self.map().dom(),
+            forall |key|
+                #![trigger(map.dom().contains(key))]
+                #![trigger(map.index(key))]
+              map.dom().contains(key)
+                ==> map[key].instance_id() == self.instance_id()
+                 && map[key].key() == key
+                 && map[key].value() == self.map()[key]
+    {
+        use_type_invariant(&self);
+        let tracked MapToken { inst, m, _v } = self;
+        assert(m.dom() =~= self.map().dom());
+        return m;
+    }
+
+    pub proof fn from_map(instance_id: InstanceId, tracked map: Map<Key, Token>) -> (tracked s: Self)
+        requires
+            forall |key| #[trigger] map.dom().contains(key) ==> map[key].instance_id() == instance_id,
+            forall |key| #[trigger] map.dom().contains(key) ==> map[key].key() == key,
+        ensures
+            s.instance_id() == instance_id,
+            s.map().dom() == map.dom(),
+            forall |key| #[trigger] map.dom().contains(key)
+                ==> s.map()[key] == map[key].value()
+    {
+        let tracked s = MapToken { inst: instance_id, m: map, _v: PhantomData };
+        assert(map.dom() == s.map().dom());
+        s
+    }
+}
+
+#[verifier::reject_recursive_types(Element)]
+pub tracked struct SetToken<Element, Token>
+    where Token: ElementToken<Element>
+{
+    ghost inst: InstanceId,
+    tracked m: Map<Element, Token>,
+}
+
+impl<Element, Token> SetToken<Element, Token>
+    where Token: ElementToken<Element>
+{
+    #[verifier::type_invariant]
+    spec fn wf(self) -> bool {
+        forall |k| #[trigger] self.m.dom().contains(k) ==> self.m[k].element() == k
+            && self.m[k].instance_id() == self.inst
+    }
+
+    pub closed spec fn instance_id(self) -> InstanceId {
+        self.inst
+    }
+
+    pub closed spec fn set(self) -> Set<Element> {
+        Set::new(
+            |e: Element| self.m.dom().contains(e),
+        )
+    }
+
+    #[verifier::inline]
+    pub open spec fn contains(self, element: Element) -> bool {
+        self.set().contains(element)
+    }
+
+    pub proof fn empty(instance_id: InstanceId) -> (tracked s: Self)
+        ensures
+            s.instance_id() == instance_id,
+            s.set() === Set::empty(),
+    {
+        let tracked s = Self { inst: instance_id, m: Map::tracked_empty() };
+        assert(s.set() =~= Set::empty());
+        return s;
+    }
+
+    pub proof fn insert(tracked &mut self, tracked token: Token)
+        requires
+            old(self).instance_id() == token.instance_id(),
+        ensures
+            self.instance_id() == old(self).instance_id(),
+            self.set() == old(self).set().insert(token.element()),
+    {
+        use_type_invariant(&*self);
+        self.m.tracked_insert(token.element(), token);
+        assert(self.set() =~= old(self).set().insert(token.element()));
+    }
+
+    pub proof fn remove(tracked &mut self, element: Element) -> (tracked token: Token)
+        requires
+            old(self).set().contains(element)
+        ensures
+            self.instance_id() == old(self).instance_id(),
+            self.set() == old(self).set().remove(element),
+            token.instance_id() == self.instance_id(),
+            token.element() == element,
+    {
+        use_type_invariant(&*self);
+        let tracked t = self.m.tracked_remove(element);
+        assert(self.set() =~= old(self).set().remove(element));
+        t
+    }
+
+    pub proof fn into_map(tracked self) -> (tracked map: Map<Element, Token>)
+        ensures
+            map.dom() == self.set(),
+            forall |key|
+                #![trigger(map.dom().contains(key))]
+                #![trigger(map.index(key))]
+                map.dom().contains(key)
+                    ==> map[key].instance_id() == self.instance_id()
+                     && map[key].element() == key
+    {
+        use_type_invariant(&self);
+        let tracked SetToken { inst, m } = self;
+        assert(m.dom() =~= self.set());
+        return m;
+    }
+
+    pub proof fn from_map(instance_id: InstanceId, tracked map: Map<Element, Token>) -> (tracked s: Self)
+        requires
+            forall |key| #[trigger] map.dom().contains(key) ==> map[key].instance_id() == instance_id,
+            forall |key| #[trigger] map.dom().contains(key) ==> map[key].element() == key,
+        ensures
+            s.instance_id() == instance_id,
+            s.set() == map.dom(),
+    {
+        let tracked s = SetToken { inst: instance_id, m: map };
+        assert(s.set() =~= map.dom());
+        s
+    }
+}
+
+pub tracked struct MultisetToken<Element, Token>
+    where Token: ElementToken<Element>
+{
+    ghost _v: PhantomData<Element>,
+    ghost inst: InstanceId,
+    tracked m: Map<int, Token>,
+}
+
+spec fn map_values<K, V>(m: Map<K, V>) -> Multiset<V> {
+    m.dom().fold(Multiset::empty(), |multiset: Multiset<V>, k: K| multiset.insert(m[k]))
+}
+
+proof fn map_values_insert_not_in<K, V>(m: Map<K, V>, k: K, v: V)
+    requires
+        !m.dom().contains(k)
+    ensures
+        map_values(m.insert(k, v)) == map_values(m).insert(v)
+{
+    assume(false);
+}
+
+proof fn map_values_remove<K, V>(m: Map<K, V>, k: K)
+    requires
+        m.dom().contains(k)
+    ensures
+        map_values(m.remove(k)) == map_values(m).remove(m[k])
+{
+    assume(false);
+}
+
+//proof fn map_values_empty_empty<K, V>()
+//    ensures map_values(Map::<K, V>::empty()) == Multiset::empty(),
+
+spec fn fresh(m: Set<int>) -> int {
+    m.find_unique_maximal(|a: int, b: int| a <= b) + 1
+}
+
+proof fn fresh_is_fresh(s: Set<int>)
+    requires s.finite(),
+    ensures !s.contains(fresh(s))
+{
+    assume(false);
+}
+
+proof fn get_key_for_value<K, V>(m: Map<K, V>, value: V) -> (k: K)
+    requires map_values(m).contains(value), m.dom().finite(),
+    ensures m.dom().contains(k), m[k] == value,
+{
+    assume(false);
+    arbitrary()
+}
+
+impl<Element, Token> MultisetToken<Element, Token>
+    where Token: ElementToken<Element>
+{
+    #[verifier::type_invariant]
+    spec fn wf(self) -> bool {
+        self.m.dom().finite() &&
+        forall |k| #[trigger] self.m.dom().contains(k)
+            ==> self.m[k].instance_id() == self.inst
+    }
+
+    pub closed spec fn instance_id(self) -> InstanceId {
+        self.inst
+    }
+
+    spec fn map_elems(m: Map<int, Token>) -> Map<int, Element> {
+        m.map_values(|t: Token| t.element())
+    }
+
+    pub closed spec fn multiset(self) -> Multiset<Element> {
+        map_values(Self::map_elems(self.m))
+    }
+
+    pub proof fn empty(instance_id: InstanceId) -> (tracked s: Self)
+        ensures
+            s.instance_id() == instance_id,
+            s.multiset() === Multiset::empty(),
+    {
+        let tracked s = Self { inst: instance_id, m: Map::tracked_empty(), _v: PhantomData, };
+        assert(Self::map_elems(Map::empty()) =~= Map::empty());
+        return s;
+    }
+
+    pub proof fn insert(tracked &mut self, tracked token: Token)
+        requires
+            old(self).instance_id() == token.instance_id(),
+        ensures
+            self.instance_id() == old(self).instance_id(),
+            self.multiset() == old(self).multiset().insert(token.element()),
+    {
+        use_type_invariant(&*self);
+        let f = fresh(self.m.dom());
+        fresh_is_fresh(self.m.dom());
+        map_values_insert_not_in(
+            Self::map_elems(self.m),
+            f,
+            token.element());
+        self.m.tracked_insert(f, token);
+        assert(Self::map_elems(self.m) =~= Self::map_elems(old(self).m).insert(
+            f, token.element()));
+        assert(self.multiset() =~= old(self).multiset().insert(token.element()));
+    }
+
+    pub proof fn remove(tracked &mut self, element: Element) -> (tracked token: Token)
+        requires
+            old(self).multiset().contains(element)
+        ensures
+            self.instance_id() == old(self).instance_id(),
+            self.multiset() == old(self).multiset().remove(element),
+            token.instance_id() == self.instance_id(),
+            token.element() == element,
+    {
+        use_type_invariant(&*self);
+        assert(Self::map_elems(self.m).dom() =~= self.m.dom());
+        let k = get_key_for_value(Self::map_elems(self.m), element);
+        map_values_remove(Self::map_elems(self.m), k);
+        let tracked t = self.m.tracked_remove(k);
+        assert(Self::map_elems(self.m) =~= Self::map_elems(old(self).m).remove(k));
+        assert(self.multiset() =~= old(self).multiset().remove(element));
+        t
+    }
+}
+
+pub open spec fn option_value_eq_option_token<Value, Token: ValueToken<Value>>(
+    opt_value: Option<Value>,
+    opt_token: Option<Token>,
+    instance_id: InstanceId,
+) -> bool {
+    match opt_value {
+        Some(val) => opt_token.is_some()
+            && opt_token.unwrap().value() == val
+            && opt_token.unwrap().instance_id() == instance_id,
+        None => opt_token.is_none(),
+    }
+}
+
+pub open spec fn option_value_le_option_token<Value, Token: ValueToken<Value>>(
+    opt_value: Option<Value>,
+    opt_token: Option<Token>,
+    instance_id: InstanceId,
+) -> bool {
+    match opt_value {
+        Some(val) => opt_token.is_some()
+            && opt_token.unwrap().value() == val
+            && opt_token.unwrap().instance_id() == instance_id,
+        None => true,
+    }
+}
+
+pub open spec fn bool_value_eq_option_token<Token: SimpleToken>(
+    b: bool,
+    opt_token: Option<Token>,
+    instance_id: InstanceId,
+) -> bool {
+    if b {
+        opt_token.is_some() && opt_token.unwrap().instance_id() == instance_id
+    } else {
+        opt_token.is_none()
+    }
+}
+
+pub open spec fn bool_value_le_option_token<Token: SimpleToken>(
+    b: bool,
+    opt_token: Option<Token>,
+    instance_id: InstanceId,
+) -> bool {
+    b ==>
+        opt_token.is_some() && opt_token.unwrap().instance_id() == instance_id
+}
+
+}
diff --git a/examples/verus-snapshot/source/vstd/vstd.rs b/examples/verus-snapshot/source/vstd/vstd.rs
index d6f32be..684ad1d 100644
--- a/examples/verus-snapshot/source/vstd/vstd.rs
+++ b/examples/verus-snapshot/source/vstd/vstd.rs
@@ -27,6 +27,7 @@ pub mod bits;
 pub mod bytes;
 pub mod calc_macro;
 pub mod cell;
+pub mod compute;
 pub mod function;
 #[cfg(all(feature = "alloc", feature = "std"))]
 pub mod hash_map;
@@ -74,6 +75,8 @@ pub mod std_specs;
 // Re-exports all vstd types, traits, and functions that are commonly used or replace
 // regular `core` or `std` definitions.
 pub mod prelude;
+#[cfg(verus_keep_ghost)]
+pub mod tokens;
 
 use prelude::*;
 
@@ -96,6 +99,7 @@ pub broadcast group group_vstd_default {
     string::group_string_axioms,
     std_specs::range::group_range_axioms,
     raw_ptr::group_raw_ptr_axioms,
+    compute::all_spec_implies,
 }
 
 #[cfg(not(feature = "alloc"))]
@@ -114,6 +118,7 @@ pub broadcast group group_vstd_default {
     string::group_string_axioms,
     std_specs::range::group_range_axioms,
     raw_ptr::group_raw_ptr_axioms,
+    compute::all_spec_implies,
 }
 
 } // verus!