Verus snapshot update (#77)

Automated verus snapshot update by GitHub Actions.
verus-lang · Jul 1, 2024 · 1fab825 · 1fab825
2 parents ea64a79 + f97903f
commit 1fab825
Show file tree

Hide file tree

Showing 7 changed files with 189 additions and 138 deletions.
diff --git a/examples/verus-snapshot/source/vstd/source/vstd/atomic.rs b/examples/verus-snapshot/source/vstd/source/vstd/atomic.rs
@@ -117,12 +117,24 @@ macro_rules! atomic_types {
             pub open spec fn points_to(&self, v: $value_ty) -> bool {
                 self.view().value == v
             }
+
+            #[verifier::inline]
+            pub open spec fn value(&self) -> $value_ty {
+                self.view().value
+            }
+
+            #[verifier::inline]
+            pub open spec fn id(&self) -> AtomicCellId {
+                self.view().patomic
+            }
         }
 
         }
     };
 }
 
+pub type AtomicCellId = int;
+
 macro_rules! atomic_common_methods {
     ($at_ident:ident, $p_ident:ident, $p_data_ident:ident, $rust_ty: ty, $value_ty: ty) => {
         verus!{

diff --git a/examples/verus-snapshot/source/vstd/source/vstd/pcm.rs b/examples/verus-snapshot/source/vstd/source/vstd/pcm.rs
@@ -157,7 +157,20 @@ impl<P: PCM> Resource<P> {
 
     // Operations with shared references
     #[verifier::external_body]
-    pub proof fn join_shared<'a>(
+    pub proof fn join_shared<'a>(tracked &'a self, tracked other: &'a Self) -> (tracked out:
+        &'a Self)
+        requires
+            self.loc() == other.loc(),
+        ensures
+            out.loc() == self.loc(),
+            incl(self.value(), out.value()),
+            incl(other.value(), out.value()),
+    {
+        unimplemented!();
+    }
+
+    #[verifier::external_body]
+    pub proof fn join_shared_to_target<'a>(
         tracked &'a self,
         tracked other: &'a Self,
         target: P,
@@ -169,7 +182,7 @@ impl<P: PCM> Resource<P> {
             out.loc() == self.loc(),
             out.value() == target,
     {
-        unimplemented!();
+        self.join_shared(other).weaken(target)
     }
 
     #[verifier::external_body]

diff --git a/examples/verus-snapshot/source/vstd/source/vstd/seq.rs b/examples/verus-snapshot/source/vstd/source/vstd/seq.rs
@@ -66,12 +66,14 @@ impl<A> Seq<A> {
 
     /// Appends the value `a` to the end of the sequence.
     /// This always increases the length of the sequence by 1.
+    /// This often requires annotating the type of the element literal in the sequence,
+    /// e.g., `10int`.
     ///
     /// ## Example
     ///
     /// ```rust
     /// proof fn push_test() {
-    ///     assert(seq![10, 11, 12].push(13) =~= seq![10, 11, 12, 13]);
+    ///     assert(seq![10int, 11, 12].push(13) =~= seq![10, 11, 12, 13]);
     /// }
     /// ```
     #[rustc_diagnostic_item = "verus::vstd::seq::Seq::push"]
@@ -117,9 +119,9 @@ impl<A> Seq<A> {
     ///
     /// ```rust
     /// proof fn subrange_test() {
-    ///     let s = seq![10, 11, 12, 13, 14];
-    ///     //                  ^-------^
-    ///     //          0   1   2   3   4   5
+    ///     let s = seq![10int, 11, 12, 13, 14];
+    ///     //                      ^-------^
+    ///     //           0      1   2   3   4   5
     ///     let sub = s.subrange(2, 4);
     ///     assert(sub =~= seq![12, 13]);
     /// }
@@ -359,15 +361,23 @@ macro_rules! seq_internal {
     [$($elem:expr),* $(,)?] => {
         $crate::vstd::seq::Seq::empty()
             $(.push($elem))*
-    }
+    };
+    [$elem:expr; $n:expr] => {
+        $crate::vstd::seq::Seq::new(
+            $n,
+            $crate::vstd::prelude::closure_to_fn_spec(
+                |_x: _| $elem
+            ),
+        )
+    };
 }
 
 /// Creates a [`Seq`] containing the given elements.
 ///
 /// ## Example
 ///
 /// ```rust
-/// let s = seq![11, 12, 13];
+/// let s = seq![11int, 12, 13];
 ///
 /// assert(s.len() == 3);
 /// assert(s[0] == 11);

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
@@ -19,21 +19,6 @@ pub struct ExVec<T, A: Allocator>(Vec<T, A>);
 #[verifier::external_body]
 pub struct ExGlobal(alloc::alloc::Global);
 
-impl<T, A: Allocator> View for Vec<T, A> {
-    type V = Seq<T>;
-
-    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> {
-        let v = self.view();
-        Seq::new(v.len(), |i: int| v[i].deep_view())
-    }
-}
-
 pub trait VecAdditionalSpecFns<T>: View<V = Seq<T>> {
     spec fn spec_index(&self, i: int) -> T
         recommends