Update library

Author: rikosellic

vstd_extra/src/resource/ghost_resource/csum.rs

@@ -1,22 +1,19 @@
 //！ Sum types for ghost resources.
-use vstd::prelude::*;
 use vstd::pcm::Loc;
+use vstd::prelude::*;
 use vstd::storage_protocol::*;
 
-
 use crate::resource::storage_protocol::csum::*;
 use crate::sum::*;
 
-
 verus! {
 
-/// `SumResourceStorage` is a storage resource that stores either an A or a B, but not both.
-pub tracked struct SumResourceStorage<A, B> {
+/// `SumResource` is a storage resource that stores either an A or a B, but not both.
+pub tracked struct SumResource<A, B> {
     tracked r: StorageResource<(), Sum<A, B>, CsumP<A, B>>,
 }
 
-impl<A,B> SumResourceStorage<A, B>
-{
+impl<A, B> SumResource<A, B> {
     pub closed spec fn id(self) -> Loc {
         self.r.loc()
     }
@@ -36,41 +33,54 @@ impl<A,B> SumResourceStorage<A, B>
     pub open spec fn is_right(self) -> bool {
         self.protocol_monoid() is Cinr
     }
-    
+
     pub open spec fn resource(self) -> Sum<A, B> {
         self.protocol_monoid().to_sum()
     }
 
-    pub proof fn alloc_empty() -> (tracked res:Self)
-    ensures
-        res.is_empty(),
+    pub proof fn is_exclusive(tracked &mut self, tracked other: &Self)
+        requires
+            old(self).is_left() || old(self).is_right(),
+            other.is_left() || other.is_right(),
+        ensures
+            *self == *old(self),
+            self.id() != other.id(),
+    {
+        if (self.id() == other.id()) {
+            self.r.validate_with_shared(&other.r);
+        }
+    }
+
+    pub proof fn alloc_empty() -> (tracked res: Self)
+        ensures
+            res.is_empty(),
     {
         let tracked r = StorageResource::alloc(CsumP::Unit, Map::tracked_empty());
-        SumResourceStorage { r }
+        SumResource { r }
     }
 
     pub proof fn alloc_left(tracked a: A) -> (tracked res: Self)
-    ensures
-        res.is_left(),
-        res.resource() is Left,
-        res.resource()->Left_0 == a,
+        ensures
+            res.is_left(),
+            res.resource() is Left,
+            res.resource()->Left_0 == a,
     {
         let tracked mut m = Map::tracked_empty();
         m.tracked_insert((), Sum::Left(a));
         let tracked r = StorageResource::alloc(CsumP::Cinl(a), m);
-        SumResourceStorage { r }
+        SumResource { r }
     }
 
     pub proof fn alloc_right(tracked b: B) -> (tracked res: Self)
-    ensures
-        res.is_right(),
-        res.resource() is Right,
-        res.resource()->Right_0 == b,
+        ensures
+            res.is_right(),
+            res.resource() is Right,
+            res.resource()->Right_0 == b,
     {
         let tracked mut m = Map::tracked_empty();
         m.tracked_insert((), Sum::Right(b));
         let tracked r = StorageResource::alloc(CsumP::Cinr(b), m);
-        SumResourceStorage { r }
+        SumResource { r }
     }
 
     pub proof fn tracked_take(tracked self) -> (tracked res: Sum<A, B>)
@@ -81,7 +91,10 @@ impl<A,B> SumResourceStorage<A, B>
     {
         self.protocol_monoid().lemma_csum_withdraws();
         let tracked r = self.r;
-        let tracked (_,mut m) = r.withdraw(CsumP::Unit, map![() => self.protocol_monoid().to_sum()]);
+        let tracked (_, mut m) = r.withdraw(
+            CsumP::Unit,
+            map![() => self.protocol_monoid().to_sum()],
+        );
         m.tracked_remove(())
     }
 
@@ -105,6 +118,64 @@ impl<A,B> SumResourceStorage<A, B>
         sum.tracked_take_right()
     }
 
+    pub proof fn split_left(tracked self) -> (tracked res: (Self, Self))
+        requires
+            self.is_left(),
+        ensures
+            res.0.is_empty(),
+            res.1.is_left(),
+            res.0.id() == self.id(),
+            res.1.id() == self.id(),
+            res.1.protocol_monoid() == self.protocol_monoid(),
+            res.1.resource() == self.resource(),
+    {
+        self.protocol_monoid().lemma_csum_withdraws();
+        let tracked r = self.r;
+        let tracked (r1, r2) = r.split(CsumP::Unit, CsumP::Cinl(self.resource()->Left_0));
+        (SumResource { r: r1 }, SumResource { r: r2 })
+    }
+
+    pub proof fn split_right(tracked self) -> (tracked res: (Self, Self))
+        requires
+            self.is_right(),
+        ensures
+            res.0.is_empty(),
+            res.1.is_right(),
+            res.0.id() == self.id(),
+            res.1.id() == self.id(),
+            res.1.protocol_monoid() == self.protocol_monoid(),
+            res.1.resource() == self.resource(),
+    {
+        self.protocol_monoid().lemma_csum_withdraws();
+        let tracked r = self.r;
+        let tracked (r1, r2) = r.split(CsumP::Unit, CsumP::Cinr(self.resource()->Right_0));
+        (SumResource { r: r1 }, SumResource { r: r2 })
+    }
+
+    pub proof fn split_and_take_left(tracked self) -> (tracked res: (Self, A))
+        requires
+            self.is_left(),
+        ensures
+            res.0.is_empty(),
+            res.0.id() == self.id(),
+            res.1 == self.resource()->Left_0,
+    {
+        let tracked (r1, r2) = self.split_left();
+        (r1, r2.tracked_take_left())
+    }
+
+    pub proof fn split_and_take_right(tracked self) -> (tracked res: (Self, B))
+        requires
+            self.is_right(),
+        ensures
+            res.0.is_empty(),
+            res.0.id() == self.id(),
+            res.1 == self.resource()->Right_0,
+    {
+        let tracked (r1, r2) = self.split_right();
+        (r1, r2.tracked_take_right())
+    }
+
     pub proof fn tracked_borrow(tracked &self) -> (tracked res: &Sum<A, B>)
         requires
             self.is_left() || self.is_right(),
@@ -129,7 +200,7 @@ impl<A,B> SumResourceStorage<A, B>
         ensures
             *res == self.resource()->Right_0,
     {
-        self.tracked_borrow().tracked_borrow_right()  
+        self.tracked_borrow().tracked_borrow_right()
     }
 
 }

vstd_extra/src/resource/ghost_resource/mod.rs

@@ -1,5 +1,5 @@
 //！ Ghost resources availbe for use in proofs, based on previous resource algebras.
+pub mod csum;
 pub mod excl;
 pub mod frac;
-pub mod csum;
 pub mod tokens;

vstd_extra/src/resource/storage_protocol/csum.rs

@@ -1,12 +1,13 @@
 //! Csum storage protocol.
+use core::panic;
 
-use vstd::prelude::*;
+use crate::sum::*;
 use vstd::pcm::Loc;
 use vstd::prelude::*;
+use vstd::prelude::*;
 use vstd::storage_protocol::*;
-use crate::sum::*;
 
-verus!{
+verus! {
 
 /// The Csum protocol monoid.
 pub ghost enum CsumP<A, B> {
@@ -17,7 +18,7 @@ pub ghost enum CsumP<A, B> {
 }
 
 /// This protocol monoid allows exclusive ownership of either an A or a B, but not both. s
-impl<A,B> Protocol<(), Sum<A, B>> for CsumP<A, B> {
+impl<A, B> Protocol<(), Sum<A, B>> for CsumP<A, B> {
     open spec fn op(self, other: Self) -> Self {
         match (self, other) {
             (CsumP::Unit, x) => x,
@@ -29,8 +30,8 @@ impl<A,B> Protocol<(), Sum<A, B>> for CsumP<A, B> {
     open spec fn rel(self, s: Map<(), Sum<A, B>>) -> bool {
         match self {
             CsumP::Unit => s.is_empty(),
-            CsumP::Cinl(a) => s.contains_key(()) && s[()] == Sum::<A,B>::Left(a),
-            CsumP::Cinr(b) => s.contains_key(()) && s[()] == Sum::<A,B>::Right(b),
+            CsumP::Cinl(a) => s.contains_key(()) && s[()] == Sum::<A, B>::Left(a),
+            CsumP::Cinr(b) => s.contains_key(()) && s[()] == Sum::<A, B>::Right(b),
             _ => false,
         }
     }
@@ -49,33 +50,33 @@ impl<A,B> Protocol<(), Sum<A, B>> for CsumP<A, B> {
     }
 }
 
-
-impl<A,B> CsumP<A, B> {
-
-pub open spec fn to_sum(self) -> Sum<A, B> {
-    match self {
-        CsumP::Cinl(a) => Sum::Left(a),
-        CsumP::Cinr(b) => Sum::Right(b),
-        _ => arbitrary()
+impl<A, B> CsumP<A, B> {
+    pub open spec fn to_sum(self) -> Sum<A, B> {
+        match self {
+            CsumP::Cinl(a) => Sum::Left(a),
+            CsumP::Cinr(b) => Sum::Right(b),
+            _ => arbitrary(),
+        }
     }
-}
 
-pub proof fn lemma_csum_withdraws(self)
-requires
-    self is Cinl || self is Cinr,
-ensures
-    withdraws(self, CsumP::Unit, map![() => self.to_sum()]),
-{
-    let res_map = map![() => self.to_sum()];
-    
-    assert forall |q: Self, t1: Map<(), Sum<A, B>>| Self::rel(Self::op(self, q), t1) implies 
-        exists |t2: Map<(), Sum<A, B>>| #[trigger] Self::rel(Self::op(CsumP::Unit, q), t2) && 
-        t2.dom().disjoint(res_map.dom()) &&
-        t1 == t2.union_prefer_right(res_map) by {
+    pub proof fn lemma_csum_withdraws(self)
+        requires
+            self is Cinl || self is Cinr,
+        ensures
+            withdraws(self, CsumP::Unit, map![() => self.to_sum()]),
+    {
+        let res_map = map![() => self.to_sum()];
+
+        assert forall|q: Self, t1: Map<(), Sum<A, B>>|
+            Self::rel(Self::op(self, q), t1) implies exists|t2: Map<(), Sum<A, B>>| #[trigger]
+            Self::rel(Self::op(CsumP::Unit, q), t2) && t2.dom().disjoint(res_map.dom()) && t1
+                == t2.union_prefer_right(res_map) by {
             let empty_map = Map::<(), Sum<A, B>>::empty();
-            assert(Self::rel(Self::op(CsumP::Unit, q), empty_map) && empty_map.dom().disjoint(res_map.dom()) && Self::rel(Self::op(self, q), res_map));
+            assert(Self::rel(Self::op(CsumP::Unit, q), empty_map) && empty_map.dom().disjoint(
+                res_map.dom(),
+            ) && Self::rel(Self::op(self, q), res_map));
         }
-}
+    }
 }
 
-}
+} // verus!