Verus snapshot update

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

@@ -309,7 +309,8 @@ pub struct InvCell<T> {
 }
 
 impl<T> InvCell<T> {
-    pub closed spec fn wf(&self) -> bool {
+    #[verifier::type_invariant]
+    closed spec fn wf(&self) -> bool {
         &&& [email protected]() === (self.possible_values@, self.pcell)
     }
 
@@ -321,7 +322,7 @@ impl<T> InvCell<T> {
         requires
             f(val),
         ensures
-            cell.wf() && forall|v| f(v) <==> cell.inv(v),
+            forall|v| f(v) <==> cell.inv(v),
     {
         let (pcell, Tracked(perm)) = PCell::new(val);
         let ghost possible_values = Set::new(f);
@@ -333,10 +334,13 @@ impl<T> InvCell<T> {
 impl<T> InvCell<T> {
     pub fn replace(&self, val: T) -> (old_val: T)
         requires
-            self.wf() && self.inv(val),
+            self.inv(val),
         ensures
             self.inv(old_val),
     {
+        proof {
+            use_type_invariant(self);
+        }
         let r;
         open_local_invariant!(self.perm_inv.borrow() => perm => {
             r = self.pcell.replace(Tracked(&mut perm), val);
@@ -347,11 +351,12 @@ impl<T> InvCell<T> {
 
 impl<T: Copy> InvCell<T> {
     pub fn get(&self) -> (val: T)
-        requires
-            self.wf(),
         ensures
             self.inv(val),
     {
+        proof {
+            use_type_invariant(self);
+        }
         let r;
         open_local_invariant!(self.perm_inv.borrow() => perm => {
             r = *self.pcell.borrow(Tracked(&perm));

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

@@ -0,0 +1,228 @@
+// altered from HashMap
+use core::marker;
+use std::borrow::Borrow;
+
+#[allow(unused_imports)]
+use super::pervasive::*;
+use super::prelude::*;
+#[allow(unused_imports)]
+use super::set::*;
+#[cfg(verus_keep_ghost)]
+use super::std_specs::hash::obeys_key_model;
+#[allow(unused_imports)]
+use core::hash::Hash;
+use std::collections::HashSet;
+
+verus! {
+
+#[verifier::ext_equal]
+#[verifier::reject_recursive_types(Key)]
+pub struct HashSetWithView<Key> where Key: View + Eq + Hash {
+    m: HashSet<Key>,
+}
+
+impl<Key> View for HashSetWithView<Key> where Key: View + Eq + Hash {
+    type V = Set<<Key as View>::V>;
+
+    closed spec fn view(&self) -> Self::V;
+}
+
+impl<Key> HashSetWithView<Key> where Key: View + Eq + Hash {
+    #[verifier::external_body]
+    pub fn new() -> (result: Self)
+        requires
+            obeys_key_model::<Key>(),
+            forall|k1: Key, k2: Key| k1@ == k2@ ==> k1 == k2,
+        ensures
+            result@ == Set::<<Key as View>::V>::empty(),
+    {
+        Self { m: HashSet::new() }
+    }
+
+    #[verifier::external_body]
+    pub fn with_capacity(capacity: usize) -> (result: Self)
+        requires
+            obeys_key_model::<Key>(),
+            forall|k1: Key, k2: Key| k1@ == k2@ ==> k1 == k2,
+        ensures
+            result@ == Set::<<Key as View>::V>::empty(),
+    {
+        Self { m: HashSet::with_capacity(capacity) }
+    }
+
+    #[verifier::external_body]
+    pub fn reserve(&mut self, additional: usize)
+        ensures
+            self@ == old(self)@,
+    {
+        self.m.reserve(additional);
+    }
+
+    pub open spec fn spec_len(&self) -> usize;
+
+    #[verifier::external_body]
+    #[verifier::when_used_as_spec(spec_len)]
+    pub fn len(&self) -> (result: usize)
+        ensures
+            result == [email protected](),
+    {
+        self.m.len()
+    }
+
+    #[verifier::external_body]
+    pub fn insert(&mut self, k: Key) -> (result: bool)
+        ensures
+            self@ == old(self)@.insert(k@) && result == !old(self)@.contains(k@),
+    {
+        self.m.insert(k)
+    }
+
+    #[verifier::external_body]
+    pub fn remove(&mut self, k: &Key) -> (result: bool)
+        ensures
+            self@ == old(self)@.remove(k@) && result == old(self)@.contains(k@),
+    {
+        self.m.remove(k)
+    }
+
+    #[verifier::external_body]
+    pub fn contains(&self, k: &Key) -> (result: bool)
+        ensures
+            result == [email protected](k@),
+    {
+        self.m.contains(k)
+    }
+
+    #[verifier::external_body]
+    pub fn get<'a>(&'a self, k: &Key) -> (result: Option<&'a Key>)
+        ensures
+            match result {
+                Some(v) => [email protected](k@) && v == &k,
+                None => [email protected](k@),
+            },
+    {
+        self.m.get(k)
+    }
+
+    #[verifier::external_body]
+    pub fn clear(&mut self)
+        ensures
+            self@ == Set::<<Key as View>::V>::empty(),
+    {
+        self.m.clear()
+    }
+}
+
+pub broadcast proof fn axiom_hash_set_with_view_spec_len<Key>(m: &HashSetWithView<Key>) where
+    Key: View + Eq + Hash,
+
+    ensures
+        #[trigger] m.spec_len() == [email protected](),
+{
+    admit();
+}
+
+#[verifier::ext_equal]
+pub struct StringHashSet {
+    m: HashSet<String>,
+}
+
+impl View for StringHashSet {
+    type V = Set<Seq<char>>;
+
+    closed spec fn view(&self) -> Self::V;
+}
+
+impl StringHashSet {
+    #[verifier::external_body]
+    pub fn new() -> (result: Self)
+        ensures
+            result@ == Set::<Seq<char>>::empty(),
+    {
+        Self { m: HashSet::new() }
+    }
+
+    #[verifier::external_body]
+    pub fn with_capacity(capacity: usize) -> (result: Self)
+        ensures
+            result@ == Set::<Seq<char>>::empty(),
+    {
+        Self { m: HashSet::with_capacity(capacity) }
+    }
+
+    #[verifier::external_body]
+    pub fn reserve(&mut self, additional: usize)
+        ensures
+            self@ == old(self)@,
+    {
+        self.m.reserve(additional);
+    }
+
+    pub open spec fn spec_len(&self) -> usize;
+
+    #[verifier::external_body]
+    #[verifier::when_used_as_spec(spec_len)]
+    pub fn len(&self) -> (result: usize)
+        ensures
+            result == [email protected](),
+    {
+        self.m.len()
+    }
+
+    #[verifier::external_body]
+    pub fn insert(&mut self, k: String) -> (result: bool)
+        ensures
+            self@ == old(self)@.insert(k@) && result == !old(self)@.contains(k@),
+    {
+        self.m.insert(k)
+    }
+
+    #[verifier::external_body]
+    pub fn remove(&mut self, k: &str) -> (result: bool)
+        ensures
+            self@ == old(self)@.remove(k@) && result == old(self)@.contains(k@),
+    {
+        self.m.remove(k)
+    }
+
+    #[verifier::external_body]
+    pub fn contains(&self, k: &str) -> (result: bool)
+        ensures
+            result == [email protected](k@),
+    {
+        self.m.contains(k)
+    }
+
+    #[verifier::external_body]
+    pub fn get<'a>(&'a self, k: &str) -> (result: Option<&'a String>)
+        ensures
+            match result {
+                Some(v) => [email protected](k@) && v@ == k@,
+                None => [email protected](k@),
+            },
+    {
+        self.m.get(k)
+    }
+
+    #[verifier::external_body]
+    pub fn clear(&mut self)
+        ensures
+            self@ == Set::<Seq<char>>::empty(),
+    {
+        self.m.clear()
+    }
+}
+
+pub broadcast proof fn axiom_string_hash_set_spec_len(m: &StringHashSet)
+    ensures
+        #[trigger] m.spec_len() == [email protected](),
+{
+    admit();
+}
+
+pub broadcast group group_hash_set_axioms {
+    axiom_hash_set_with_view_spec_len,
+    axiom_string_hash_set_spec_len,
+}
+
+} // verus!

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

@@ -528,11 +528,7 @@ pub use open_atomic_invariant_internal;
 /// boundaries, every `proof` and `exec` function has, as part of its specification,
 /// the set of invariant namespaces that it might open.
 ///
-/// UNDER CONSTRUCTION: right now the forms of these specifications are somewhat limited
-/// and we expect to expand them.
-///
-/// The invariant set of a function can be specified by putting either
-/// `opens_invariants none` or `opens_invariants any` in the function signature.
+/// The invariant set of a function can be specified via the [`opens_invariants` clause](https://verus-lang.github.io/verus/guide/reference-opens-invariants.html).
 /// The default for an `exec`-mode function is to open any, while the default
 /// for a `proof`-mode function is to open none.
 ///

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

@@ -14,6 +14,10 @@ pub proof fn tracked_swap<V>(tracked a: &mut V, tracked b: &mut V)
     unimplemented!();
 }
 
+/// Make any tracked object permanently shared and get a reference to it.
+///
+/// Tip: If you try to use this and run into problems relating to the introduction
+/// of a lifetime variable, you want to try [`Shared`](crate::shared::Shared) instead.
 #[verifier::external_body]
 pub proof fn tracked_static_ref<V>(tracked v: V) -> (tracked res: &'static V)
     ensures

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

@@ -124,7 +124,9 @@ pub tracked struct PointsTo<T> {
 // variant names like Uninit/Init.)
 #[verifier::accept_recursive_types(T)]
 pub ghost enum MemContents<T> {
+    /// Represents uninitialized memory
     Uninit,
+    /// Represents initialized memory with the given value
     Init(T),
 }
 
@@ -169,20 +171,25 @@ impl<T> PointsTo<T> {
     }
 
     #[verifier::inline]
+    #[doc(verus_show_body)]
     pub open spec fn is_init(&self) -> bool {
         self.opt_value().is_init()
     }
 
     #[verifier::inline]
+    #[doc(verus_show_body)]
     pub open spec fn is_uninit(&self) -> bool {
         self.opt_value().is_uninit()
     }
 
     #[verifier::inline]
+    #[doc(verus_show_body)]
     pub open spec fn value(&self) -> T {
         self.opt_value().value()
     }
 
+    /// Guarantee that the `PointsTo` for any non-zero-sized type points to a non-null address.
+    ///
     // ZST pointers *are* allowed to be null, so we need a precondition that size != 0.
     // See https://doc.rust-lang.org/std/ptr/#safety
     #[verifier::external_body]
@@ -195,8 +202,11 @@ impl<T> PointsTo<T> {
         unimplemented!();
     }
 
-    /// "De-initialize" the memory by setting it to MemContents::Uninit
-    /// This is actually a pure no-op; we're just forgetting that the contents are there.
+    /// "Forgets" about the value stored behind the pointer.
+    /// Updates the `PointsTo` value to [`MemContents::Uninit`](MemContents::Uninit).
+    /// Note that this is a `proof` function, i.e.,
+    /// it is operationally a no-op in executable code, even on the Rust Abstract Machine.
+    /// Only the proof-code representation changes.
     #[verifier::external_body]
     pub proof fn leak_contents(tracked &mut self)
         ensures