pub trait ResourceAlgebra: Sized {
// Required methods
spec fn valid(self) -> bool;
spec fn op(a: Self, b: Self) -> Self;
proof fn associative(a: Self, b: Self, c: Self);
proof fn commutative(a: Self, b: Self);
proof fn valid_op(a: Self, b: Self);
}Expand description
A Resource Algebra operating on a type T
This construction is based off the Iris from the Ground Up report.
A striking difference is that we do not need a core for elements (the core is interesting in Iris because of the persistent modality, which Verus does not have).
See Resource for more information.
Required Methods§
Sourcespec fn op(a: Self, b: Self) -> Self
spec fn op(a: Self, b: Self) -> Self
Compose two elements
Sometimes the notation a · b is used to represent RA::op(a, b)
Sourceproof fn associative(a: Self, b: Self, c: Self)
proof fn associative(a: Self, b: Self, c: Self)
ensures
Self::op(a, Self::op(b, c)) == Self::op(Self::op(a, b), c),The operation is associative
Sourceproof fn commutative(a: Self, b: Self)
proof fn commutative(a: Self, b: Self)
ensures
Self::op(a, b) == Self::op(b, a),The operation is commutative
Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.
Implementations on Foreign Types§
Source§impl<RA: ResourceAlgebra> ResourceAlgebra for Option<RA>
impl<RA: ResourceAlgebra> ResourceAlgebra for Option<RA>
Source§open spec fn valid(self) -> bool
open spec fn valid(self) -> bool
{
match self {
Some(v) => v.valid(),
None => true,
}
}Whether an element is valid
Source§open spec fn op(a: Self, b: Self) -> Self
open spec fn op(a: Self, b: Self) -> Self
{
match (a, b) {
(Some(a), Some(b)) => Some(RA::op(a, b)),
(None, _) => b,
(_, None) => a,
}
}Compose two elements
Source§proof fn associative(a: Self, b: Self, c: Self)
proof fn associative(a: Self, b: Self, c: Self)
The operation is associative
Source§proof fn commutative(a: Self, b: Self)
proof fn commutative(a: Self, b: Self)
The operation is commutative