Add more functions to the library

Author: rikosellic

ostd/src/sync/rwlock.rs

@@ -322,7 +322,7 @@ impl<T, G> RwLock<T, G> {
         proof {lemma_consts_properties();}
         let tracked frac_perm = RwFrac::<T>::new(perm);
         proof_decl!{
-            let tracked read_retract_token = TokenStorage::<V_MAX_READ_RETRACT_FRACS>::new(());
+            let tracked read_retract_token = TokenStorage::<V_MAX_READ_RETRACT_FRACS>::alloc(());
             let tracked upread_retract_token = UniqueTokenStorage::alloc(());
             let tracked upreader_guard_token = UniqueTokenStorage::alloc(());
         }

vstd_extra/src/resource/ghost_resource/csum.rs

@@ -1,13 +1,137 @@
 //！ Sum types for ghost resources.
 use vstd::prelude::*;
+use vstd::pcm::Loc;
+use vstd::storage_protocol::*;
+
+
+use crate::resource::storage_protocol::csum::*;
+use crate::sum::*;
+
 
 verus! {
 
-pub ghost enum CsumP<A, B> {
-    Unit,
-    Cinl(A),
-    Cinr(B),
-    CsumInvalid,
+/// `SumResourceStorage` is a storage resource that stores either an A or a B, but not both.
+pub tracked struct SumResourceStorage<A, B> {
+    tracked r: StorageResource<(), Sum<A, B>, CsumP<A, B>>,
+}
+
+impl<A,B> SumResourceStorage<A, B>
+{
+    pub closed spec fn id(self) -> Loc {
+        self.r.loc()
+    }
+
+    pub closed spec fn protocol_monoid(self) -> CsumP<A, B> {
+        self.r.value()
+    }
+
+    pub open spec fn is_empty(self) -> bool {
+        self.protocol_monoid() is Unit
+    }
+
+    pub open spec fn is_left(self) -> bool {
+        self.protocol_monoid() is Cinl
+    }
+
+    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(),
+    {
+        let tracked r = StorageResource::alloc(CsumP::Unit, Map::tracked_empty());
+        SumResourceStorage { 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,
+    {
+        let tracked mut m = Map::tracked_empty();
+        m.tracked_insert((), Sum::Left(a));
+        let tracked r = StorageResource::alloc(CsumP::Cinl(a), m);
+        SumResourceStorage { 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,
+    {
+        let tracked mut m = Map::tracked_empty();
+        m.tracked_insert((), Sum::Right(b));
+        let tracked r = StorageResource::alloc(CsumP::Cinr(b), m);
+        SumResourceStorage { r }
+    }
+
+    pub proof fn tracked_take(tracked self) -> (tracked res: Sum<A, B>)
+        requires
+            self.is_left() || self.is_right(),
+        ensures
+            res == self.resource(),
+    {
+        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()]);
+        m.tracked_remove(())
+    }
+
+    pub proof fn tracked_take_left(tracked self) -> (tracked res: A)
+        requires
+            self.is_left(),
+        ensures
+            res == self.resource()->Left_0,
+    {
+        let tracked sum = self.tracked_take();
+        sum.tracked_take_left()
+    }
+
+    pub proof fn tracked_take_right(tracked self) -> (tracked res: B)
+        requires
+            self.is_right(),
+        ensures
+            res == self.resource()->Right_0,
+    {
+        let tracked sum = self.tracked_take();
+        sum.tracked_take_right()
+    }
+
+    pub proof fn tracked_borrow(tracked &self) -> (tracked res: &Sum<A, B>)
+        requires
+            self.is_left() || self.is_right(),
+        ensures
+            *res == self.resource(),
+    {
+        StorageResource::guard(&self.r, map![() => self.resource()]).tracked_borrow(())
+    }
+
+    pub proof fn tracked_borrow_left(tracked &self) -> (tracked res: &A)
+        requires
+            self.is_left(),
+        ensures
+            *res == self.resource()->Left_0,
+    {
+        self.tracked_borrow().tracked_borrow_left()
+    }
+
+    pub proof fn tracked_borrow_right(tracked &self) -> (tracked res: &B)
+        requires
+            self.is_right(),
+        ensures
+            *res == self.resource()->Right_0,
+    {
+        self.tracked_borrow().tracked_borrow_right()  
+    }
+
 }
 
 } // verus!

vstd_extra/src/resource/ghost_resource/frac.rs

@@ -52,7 +52,7 @@ impl<T> FracStorage<T> {
     }
 
     /// Allocate a new fractional storage resource with full permission.
-    pub proof fn new(tracked v: T) -> (tracked res: Self)
+    pub proof fn alloc(tracked v: T) -> (tracked res: Self)
         ensures
             res.has_full_frac(),
     {

vstd_extra/src/resource/ghost_resource/tokens.rs

@@ -64,7 +64,7 @@ impl<T, const TOTAL: u64> FracGhostStorage<T, TOTAL> {
         self.id
     }
 
-    pub proof fn new(value: T) -> (tracked res: Self)
+    pub proof fn alloc(value: T) -> (tracked res: Self)
         requires
             TOTAL > 0,
         ensures

vstd_extra/src/resource/storage_protocol/csum.rs

@@ -8,14 +8,74 @@ use crate::sum::*;
 
 verus!{
 
-/// The Csum storage protocol.
+/// The Csum protocol monoid.
 pub ghost enum CsumP<A, B> {
     Unit,
     Cinl(A),
     Cinr(B),
     CsumInvalid,
 }
 
+/// 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> {
+    open spec fn op(self, other: Self) -> Self {
+        match (self, other) {
+            (CsumP::Unit, x) => x,
+            (x, CsumP::Unit) => x,
+            _ => CsumP::CsumInvalid,
+        }
+    }
 
+    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),
+            _ => false,
+        }
+    }
+
+    open spec fn unit() -> Self {
+        CsumP::Unit
+    }
+
+    proof fn commutative(a: Self, b: Self) {
+    }
+
+    proof fn associative(a: Self, b: Self, c: Self) {
+    }
+
+    proof fn op_unit(a: Self) {
+    }
+}
+
+
+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 {
+            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));
+        }
+}
+}
 
 }