Trait ResourceAlgebra 

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);
}

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

spec fn valid(self) -> bool

Whether an element is valid

spec fn op(a: Self, b: Self) -> Self

Compose two elements

Sometimes the notation a · b is used to represent RA::op(a, b)

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

proof fn commutative(a: Self, b: Self)

ensures

Self::op(a, b) == Self::op(b, a),

The operation is commutative

proof fn valid_op(a: Self, b: Self)

requires

Self::op(a, b).valid(),

ensures

a.valid(),

The operation is closed under inclusion (i.e., if the result of the operation is valid then its parts are also valid)

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementations on Foreign Types

impl<RA: ResourceAlgebra> ResourceAlgebra for Option<RA>

open spec fn valid(self) -> bool

{
    match self {
        Some(v) => v.valid(),
        None => true,
    }
}

Whether an element is valid

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

proof fn associative(a: Self, b: Self, c: Self)

The operation is associative

proof fn commutative(a: Self, b: Self)

The operation is commutative

proof fn valid_op(a: Self, b: Self)

The operation is closed under inclusion (i.e., if the result of the operation is valid then its parts are also valid)

Implementors

impl ResourceAlgebra for FractionRA

impl<RA1: ResourceAlgebra, RA2: ResourceAlgebra> ResourceAlgebra for ProductRA<RA1, RA2>

impl<RA1: ResourceAlgebra, RA2: ResourceAlgebra> ResourceAlgebra for SumRA<RA1, RA2>

impl<RA: ResourceAlgebra> ResourceAlgebra for AuthRA<RA>

impl<T> ResourceAlgebra for AgreementRA<T>

impl<T> ResourceAlgebra for ExclusiveRA<T>