Skip to main content

PCM

vstd::resource::pcm

Trait PCM

pub trait PCM: ResourceAlgebra {
    // Required methods
    spec fn unit() -> Self;
    proof fn op_unit(self);
    proof fn unit_valid();
}

Expand description

A Partial Commutative Monoid is a special type of ResourceAlgebra, where all elements have the same core (which belongs in the carrier), the unit. For this reason, they are also called unitary resource algebras¹.

This is slightly misleading. PCMs are partial in the sense that the operation is not defined for certain inputs. Because Verus does not support partial functions, we model that partiality with the validity predicate, which does make it a unitary resource algebra. ↩

Required Methods§

spec fn unit() -> Self

The unit of the monoid, i.e., the carrier value that composed with any other carrier value yields the identity function

proof fn op_unit(self)

ensures

Self::op(self, Self::unit()) == self,

The core of an element a is, by definition, some other element x such that a · x = a

proof fn unit_valid()

ensures

Self::unit().valid(),

The unit is always a valid element

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§

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

open spec fn unit() -> Self

{ None }

proof fn op_unit(self)

The core of an element a is, by definition, some other element x such that a op x = a

proof fn unit_valid()

The unit is always a valid element

Implementors§