resource: add ResourceAlgebra trait

This is done by partitioning the previous PCM trait (while keeping that
axiomatization of the pcm::Resource API intact and unchanged).

Then the algebra::Resouce API is verified agains the pcm::Resource API,
using an Option combinator (which lifts any RA into a PCM).

Author: bsdinis

examples/pcm/agreement.rs

@@ -35,6 +35,7 @@ use verus_builtin::*;
 use verus_builtin_macros::*;
 use vstd::prelude::*;
 use vstd::resource;
+use vstd::resource::algebra::ResourceAlgebra;
 use vstd::resource::pcm::Resource;
 use vstd::resource::pcm::PCM;
 use vstd::resource::Loc;
@@ -53,7 +54,7 @@ impl<T> AgreementResourceValue<T> {
     }
 }
 
-impl<T> PCM for AgreementResourceValue<T> {
+impl<T> ResourceAlgebra for AgreementResourceValue<T> {
     open spec fn valid(self) -> bool {
         !(self is Invalid)
     }
@@ -75,10 +76,6 @@ impl<T> PCM for AgreementResourceValue<T> {
         }
     }
 
-    open spec fn unit() -> Self {
-        AgreementResourceValue::<T>::Empty {  }
-    }
-
     proof fn valid_op(a: Self, b: Self) {
     }
 
@@ -87,6 +84,13 @@ impl<T> PCM for AgreementResourceValue<T> {
 
     proof fn associative(a: Self, b: Self, c: Self) {
     }
+}
+
+
+impl<T> PCM for AgreementResourceValue<T> {
+    open spec fn unit() -> Self {
+        AgreementResourceValue::<T>::Empty {  }
+    }
 
     proof fn op_unit(self) {
     }

examples/pcm/log.rs

@@ -48,6 +48,7 @@ use std::result::*;
 use verus_builtin::*;
 use verus_builtin_macros::*;
 use vstd::prelude::*;
+use vstd::resource::algebra::ResourceAlgebra;
 use vstd::resource::copy_duplicable_part;
 use vstd::resource::pcm::Resource;
 use vstd::resource::pcm::PCM;
@@ -69,7 +70,7 @@ pub open spec fn is_prefix<T>(s1: Seq<T>, s2: Seq<T>) -> bool {
     &&& forall|i| 0 <= i < s1.len() ==> s1[i] == s2[i]
 }
 
-impl<T> PCM for LogResourceValue<T> {
+impl<T> ResourceAlgebra for LogResourceValue<T> {
     open spec fn valid(self) -> bool {
         &&& !(self is Invalid)
     }
@@ -130,10 +131,6 @@ impl<T> PCM for LogResourceValue<T> {
         }
     }
 
-    open spec fn unit() -> Self {
-        Self::PrefixKnowledge { prefix: Seq::<T>::empty() }
-    }
-
     proof fn valid_op(a: Self, b: Self) {
     }
 
@@ -147,6 +144,11 @@ impl<T> PCM for LogResourceValue<T> {
             is_prefix(log1, log2) && is_prefix(log2, log1) <==> log1 =~= log2);
         assert(forall|log| is_prefix(log, Seq::<T>::empty()) ==> log =~= Seq::<T>::empty());
     }
+}
+impl<T> PCM for LogResourceValue<T> {
+    open spec fn unit() -> Self {
+        Self::PrefixKnowledge { prefix: Seq::<T>::empty() }
+    }
 
     proof fn op_unit(self) {
         assert(forall|log| is_prefix(log, Seq::<T>::empty()) ==> log =~= Seq::<T>::empty());

examples/pcm/monotonic_counter.rs

@@ -55,6 +55,7 @@ use std::result::*;
 use verus_builtin::*;
 use verus_builtin_macros::*;
 use vstd::prelude::*;
+use vstd::resource::algebra::ResourceAlgebra;
 use vstd::resource::copy_duplicable_part;
 use vstd::resource::pcm::Resource;
 use vstd::resource::pcm::PCM;
@@ -86,7 +87,7 @@ pub enum MonotonicCounterResourceValue {
 
 // To use `MonotonicCounterResourceValue` as a resource, we have to implement
 // `PCM`, showing how to use it in a resource algebra.
-impl PCM for MonotonicCounterResourceValue {
+impl ResourceAlgebra for MonotonicCounterResourceValue {
     open spec fn valid(self) -> bool {
         !(self is Invalid)
     }
@@ -160,10 +161,6 @@ impl PCM for MonotonicCounterResourceValue {
         }
     }
 
-    open spec fn unit() -> Self {
-        MonotonicCounterResourceValue::LowerBound { lower_bound: 0 }
-    }
-
     proof fn valid_op(a: Self, b: Self) {
     }
 
@@ -172,6 +169,11 @@ impl PCM for MonotonicCounterResourceValue {
 
     proof fn associative(a: Self, b: Self, c: Self) {
     }
+}
+impl PCM for MonotonicCounterResourceValue {
+    open spec fn unit() -> Self {
+        MonotonicCounterResourceValue::LowerBound { lower_bound: 0 }
+    }
 
     proof fn op_unit(self) {
     }

examples/pcm/oneshot.rs

@@ -69,6 +69,7 @@ use verus_builtin::*;
 use verus_builtin_macros::*;
 use vstd::prelude::*;
 use vstd::resource;
+use vstd::resource::algebra::ResourceAlgebra;
 use vstd::resource::pcm::Resource;
 use vstd::resource::pcm::PCM;
 use vstd::resource::update_and_redistribute;
@@ -98,7 +99,7 @@ pub enum OneShotResourceValue {
 
 // To use `OneShotResourceValue` as a resource, we have to implement
 // `PCM`, showing how to use it in a resource algebra.
-impl PCM for OneShotResourceValue {
+impl ResourceAlgebra for OneShotResourceValue {
     open spec fn valid(self) -> bool {
         !(self is Invalid)
     }
@@ -119,10 +120,6 @@ impl PCM for OneShotResourceValue {
         }
     }
 
-    open spec fn unit() -> Self {
-        OneShotResourceValue::Empty {  }
-    }
-
     proof fn valid_op(a: Self, b: Self) {
     }
 
@@ -131,6 +128,11 @@ impl PCM for OneShotResourceValue {
 
     proof fn associative(a: Self, b: Self, c: Self) {
     }
+}
+impl PCM for OneShotResourceValue {
+    open spec fn unit() -> Self {
+        OneShotResourceValue::Empty {  }
+    }
 
     proof fn op_unit(self) {
     }