Verus snapshot update

examples/verus-snapshot/source/rust_verify/example/syntax.rs

@@ -1,4 +1,5 @@
 #![allow(unused_imports)]
+
 use builtin::*;
 use builtin_macros::*;
 use vstd::{modes::*, prelude::*, seq::*, *};
@@ -572,19 +573,15 @@ proof fn uses_arrow_matches_2(t: ThisOrThat)
     assert(t is That && t->v == 3);
 }
 
-#[verifier::external_body]
-struct Collection {}
-
-impl Collection {
-    pub spec fn spec_has(&self, v: nat) -> bool;
-}
-
-proof fn uses_spec_has(c: Collection)
+proof fn uses_spec_has(s: Set<int>, ms: vstd::multiset::Multiset<int>)
     requires
-        c has 3,
+        s has 3,
+        ms has 4,
 {
-    assert(c has 3);
-    assert(c has 3 == c has 3);
+    assert(s has 3);
+    assert(s has 3 == s has 3);
+    assert(ms has 4);
+    assert(ms has 4 == ms has 4);
 }
 
 } // verus!

examples/verus-snapshot/source/vstd/arithmetic/internals/div_internals.rs

@@ -87,7 +87,7 @@ pub proof fn lemma_div_basics(n: int)
     lemma_mod_basics(n);
     div_internals_nonlinear::lemma_small_div();
     div_internals_nonlinear::lemma_div_by_self(n);
-    assert forall|x: int| 0 <= x < n <== #[trigger] (x / n) == 0 by {
+    assert forall|x: int| #[trigger] (x / n) == 0 implies 0 <= x < n by {
         mod_internals_nonlinear::lemma_fundamental_div_mod(x, n);
     }
 }
@@ -172,7 +172,7 @@ proof fn lemma_div_auto_plus(n: int)
             assert(((i - n) + j) / n == ((i + j) - n) / n);
             assert((i + (j - n)) / n == ((i + j) - n) / n);
         }
-        assert forall|i: int, j: int| 0 <= i < n && 0 <= j < n ==> #[trigger] f(i, j) by {
+        assert forall|i: int, j: int| 0 <= i < n && 0 <= j < n implies #[trigger] f(i, j) by {
             assert(((i + n) + j) / n == ((i + j) + n) / n);
             assert((i + (j + n)) / n == ((i + j) + n) / n);
             assert(((i - n) + j) / n == ((i + j) - n) / n);

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

@@ -70,6 +70,8 @@ macro_rules! declare_atomic_type {
                 let (patomic, Tracked(perm)) = $patomic_ty::new(u);
 
                 let tracked pair = (perm, g);
+                assert(Pred::atomic_inv(k, u, g));
+                assert(perm.view().patomic == patomic.id());
                 let tracked atomic_inv = AtomicInvariant::new(
                     (k, patomic.id()), pair, 0);
 

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

@@ -110,6 +110,14 @@ impl<Key, Value> HashMapWithView<Key, Value> where Key: View + Eq + Hash {
     {
         self.m.clear()
     }
+
+    #[verifier::external_body]
+    pub fn union_prefer_right(&mut self, other: Self)
+        ensures
+            self@ == old(self)@.union_prefer_right(other@),
+    {
+        self.m.extend(other.m)
+    }
 }
 
 pub broadcast proof fn axiom_hash_map_with_view_spec_len<Key, Value>(
@@ -211,6 +219,14 @@ impl<Value> StringHashMap<Value> {
     {
         self.m.clear()
     }
+
+    #[verifier::external_body]
+    pub fn union_prefer_right(&mut self, other: Self)
+        ensures
+            self@ == old(self)@.union_prefer_right(other@),
+    {
+        self.m.extend(other.m)
+    }
 }
 
 pub broadcast proof fn axiom_string_hash_map_spec_len<Value>(m: &StringHashMap<Value>)

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

@@ -272,8 +272,7 @@ pub struct OpenInvariantCredit {}
 
 // It's intentional that `create_open_invariant_credit` uses `exec` mode. This prevents
 // creation of an infinite number of credits to open invariants infinitely often.
-#[cfg(verus_keep_ghost)]
-#[rustc_diagnostic_item = "verus::vstd::invariant::create_open_invariant_credit"]
+#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::invariant::create_open_invariant_credit")]
 #[verifier::external_body]
 #[inline(always)]
 pub fn create_open_invariant_credit() -> Tracked<OpenInvariantCredit>
@@ -290,11 +289,13 @@ pub fn create_open_invariant_credit() -> Tracked<OpenInvariantCredit>
 pub proof fn spend_open_invariant_credit_in_proof(tracked credit: OpenInvariantCredit) {
 }
 
-#[cfg(verus_keep_ghost)]
-#[rustc_diagnostic_item = "verus::vstd::invariant::spend_open_invariant_credit"]
+#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::invariant::spend_open_invariant_credit")]
 #[doc(hidden)]
 #[inline(always)]
-pub fn spend_open_invariant_credit(credit: Tracked<OpenInvariantCredit>)
+pub fn spend_open_invariant_credit(
+    #[allow(unused_variables)]
+    credit: Tracked<OpenInvariantCredit>,
+)
     opens_invariants none
     no_unwind
 {

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

@@ -165,6 +165,12 @@ impl<V> Multiset<V> {
         self.count(v) > 0
     }
 
+    /// Predicate indicating if the set contains the given element: supports `self has a` syntax.
+    #[verifier::inline]
+    pub open spec fn spec_has(self, v: V) -> bool {
+        self.contains(v)
+    }
+
     /// Returns a multiset containing the lower count of a given element
     /// between the two sets. In other words, returns a multiset with only
     /// the elements that "overlap".

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

@@ -0,0 +1,68 @@
+#[allow(unused_imports)]
+use super::multiset::Multiset;
+#[allow(unused_imports)]
+use super::prelude::*;
+
+verus! {
+
+broadcast use super::multiset::group_multiset_axioms;
+
+impl<A> Multiset<A> {
+    /// Is `true` if called by an "empty" multiset, i.e., a set containing no elements and has length 0
+    pub open spec fn is_empty(self) -> (b: bool) {
+        self.len() == 0
+    }
+
+    /// A singleton multiset has at least one element with multiplicity 1 and any two elements are equal.
+    pub open spec fn is_singleton(self) -> bool {
+        &&& self.len() > 0
+        &&& (forall|x: A| self.contains(x) ==> self.count(x) == 1)
+        &&& (forall|x: A, y: A| self.contains(x) && self.contains(y) ==> x == y)
+    }
+
+    /// A singleton multiset that contains an alement is equivalent to the singleton multiset with that element.
+    pub proof fn lemma_is_singleton_contains_elem_equal_singleton(self, x: A)
+        requires
+            self.is_singleton(),
+            self.contains(x),
+        ensures
+            self =~= Multiset::singleton(x),
+    {
+        assert forall|y: A| #[trigger] Multiset::singleton(x).count(y) == self.count(y) by {
+            if self.contains(y) {
+            } else {
+            }
+        };
+    }
+
+    /// A singleton multiset has length 1.
+    pub proof fn lemma_singleton_size(self)
+        requires
+            self.is_singleton(),
+        ensures
+            self.len() == 1,
+    {
+        self.lemma_is_singleton_contains_elem_equal_singleton(self.choose());
+    }
+
+    /// A multiset has exactly one element, if and only if, it has at least one element with multiplicity 1 and any two elements are equal.
+    pub proof fn lemma_is_singleton(s: Multiset<A>)
+        ensures
+            s.is_singleton() <==> (s.len() == 1),
+    {
+        if s.is_singleton() {
+            s.lemma_singleton_size();
+        }
+        if s.len() == 1 {
+            assert forall|x: A, y: A| s.contains(x) && s.contains(y) implies x == y by {
+                assert(s.remove(x).len() == 0);
+                if x != y {
+                    assert(s.remove(x).count(y) == 0);
+                    assert(s.remove(x).insert(x) =~= s);
+                }
+            }
+        }
+    }
+}
+
+} // verus!

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

@@ -0,0 +1,51 @@
+#![allow(unused_variables)]
+
+use super::prelude::*;
+
+// This file implements prophecy variables.
+//
+// A prophecy variable is represented by a Prophecy<T>, and predicts some value
+// of type T.
+//
+// A prophecy can be allocated by calling Prophecy::<T>::alloc() in exec mode.
+// The result is a prophecy variable whose view is an arbitrary value of type T.
+//
+// A prophecy can be resolved by calling Prophecy::<T>::resolve() in exec mode.
+// This call ensures that the view of the prophecy variable is equal to the value
+// passed to resolve().  This call (and in particular, its argument v) must be
+// exec-mode to avoid circular dependency on the value of the prophecy variable.
+//
+// An informal soundness argument (following the Future-is-ours paper) is that,
+// for any execution of the program, there is some sequence of calls to resolve(),
+// whose values do not depend on spec- or proof-mode values.  Those values can be
+// plugged into the arbitrary ghost values chosen by alloc(), for the corresponding
+// prophecy variables, to justify the proof accompanying the program.  Since both
+// alloc() and resolve() are exec-mode, there is no ambiguity about which alloc()
+// call corresponds to a particular resolve() value.
+
+verus! {
+
+pub struct Prophecy<T> {
+    v: Ghost<T>,
+}
+
+impl<T> Prophecy<T> where T: Structural {
+    pub closed spec fn view(self) -> T {
+        self.v@
+    }
+
+    #[inline(always)]
+    pub exec fn new() -> (result: Self) {
+        Prophecy::<T> { v: Ghost(arbitrary()) }
+    }
+
+    #[inline(always)]
+    #[verifier::external_body]
+    pub exec fn resolve(self, v: &T)
+        ensures
+            self@ == v,
+    {
+    }
+}
+
+} // verus!

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

@@ -171,19 +171,16 @@ 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()
     }
@@ -701,7 +698,7 @@ impl Dealloc {
 
 /// Allocate with the global allocator.
 /// Precondition should be consistent with the [documented safety conditions on `alloc`](https://doc.rust-lang.org/alloc/alloc/trait.GlobalAlloc.html#tymethod.alloc).
-#[cfg(feature = "alloc")]
+#[cfg(feature = "std")]
 #[verifier::external_body]
 pub fn allocate(size: usize, align: usize) -> (pt: (
     *mut u8,
@@ -728,6 +725,9 @@ pub fn allocate(size: usize, align: usize) -> (pt: (
     let layout = unsafe { alloc::alloc::Layout::from_size_align_unchecked(size, align) };
     // SAFETY: size != 0
     let p = unsafe { ::alloc::alloc::alloc(layout) };
+    if p == core::ptr::null_mut() {
+        std::process::abort();
+    }
     (p, Tracked::assume_new(), Tracked::assume_new())
 }