Merge branch 'main' into optional-updater

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!

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;

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!

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;