Trait RA 

pub trait RA: Sized {
    // Required methods
    fn op(self, other: Self) -> Option<Self>;
    fn factor(self, factor: Self) -> Option<Self>;
    fn commutative(a: Self, b: Self);
    fn associative(a: Self, b: Self, c: Self);
    fn core(self) -> Option<Self>;
    fn core_is_maximal_idemp(self, i: Self);

    // Provided methods
    fn incl(self, other: Self) -> bool { ... }
    fn incl_op(self, other: Self, comb: Self) { ... }
    fn incl_eq(self, other: Self) -> bool { ... }
    fn incl_eq_op(a: Self, b: Self, x: Self) -> bool { ... }
    fn update(self, x: Self) -> bool { ... }
    fn update_nondet(self, s: Set<Self>) -> bool { ... }
    fn incl_transitive(a: Self, b: Self, c: Self) { ... }
}

Define a Resource Algebra.

Resource algebras are a concept inspired by Iris. Used in conjunction with Resources, they unlock new reasonings.

Notes on the definition of resource algebras

Our definition of resource algebras differs from the one in Iris in that it does not require RAs to define a “core” function. Instead, we follow “Idempotent Resources in Separation Logic — The Heart of core in Iris” by Gratzer, Møller & Birkedal (GMB), and require RAs to satisfy a “maximal idempotent” axiom.

Required Methods

fn op(self, other: Self) -> Option<Self>

The operation of this resource algebra.

This is the core of the trait. This operation will be used to join and split resources.

It must be associative and commutative (among others).

fn factor(self, factor: Self) -> Option<Self>

Factorizing elements of the RA

Given a and c, this returns an element b such that a = b.c, or returns None if there does not exists such an element.

ensures

match result {
        Some(c) => factor.op(c) == Some(self),
        None => forall<c: Self> factor.op(c) != Some(self),
    }

fn commutative(a: Self, b: Self)

Self::op is commutative.

(law)

ensures

a.op(b) == b.op(a)

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

Self::op is associative.

(law)

ensures

a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc))

fn core(self) -> Option<Self>

The core of an element, when it exists, is included in that element, and idempotent. Note that the statement c.op(self) == Some(self) is equivalent to c.incl(self) for idempotent elements.

ensures

match result {
        Some(c) => c.op(c) == Some(c) && c.op(self) == Some(self),
        None => true
    }

fn core_is_maximal_idemp(self, i: Self)

The core maximal, if there exists an idempotent element included in self

requires

i.op(i) == Some(i)

requires

i.op(self) == Some(self)

ensures

match self.core() {
        Some(c) => i.incl(c),
        None => false,
    }

Provided Methods

fn incl(self, other: Self) -> bool

Inclusion of RA.

This asserts that other is, in a sense, ‘bigger’ than self.

Notes on reflexivity

Following Iris, our definition of incl is not reflexive. We could define it to be self == other || ..., but doing that loses the following desirable property for the product RA:

(x, y).incl((x', y')) == x.incl(x') && y.incl(y').

If you need the reflexive closure of the inclusion relation, then you can use Some(x).incl(Some(y)). Indeed, incl on the Option RA has the following property:

Some(x).incl(Some(y)) == (x == y || x.incl(y))

Note that the paper on the maximal idempotent axiom (GMB) uses the reflexive definition of incl on paper, but not in its accompanying Iris formalization, where it uses the non-reflexive definition (as we do here).

(open, sealed)

other.factor(self) != None

fn incl_op(self, other: Self, comb: Self)

(law, sealed)

requires

self.op(other) == Some(comb)

ensures

self.incl(comb)

fn incl_eq(self, other: Self) -> bool

(open, sealed)

self == other || self.incl(other)

fn incl_eq_op(a: Self, b: Self, x: Self) -> bool

(open, sealed)

match a.op(b) {
    None => false,
    Some(ab) => ab.incl_eq(x),
}

fn update(self, x: Self) -> bool

Ensures that we can go from self to x without making composition with the frame invalid.

This is used in Resource::update.

(open, sealed)

pearlite! {
    forall<y: Self> self.op(y) != None ==> x.op(y) != None
}

fn update_nondet(self, s: Set<Self>) -> bool

This is used in Resource::update_nondet.

(open, sealed)

pearlite! {
    forall<y: Self> self.op(y) != None ==>
        exists<x: Self> s.contains(x) && x.op(y) != None
}

fn incl_transitive(a: Self, b: Self, c: Self)

RA::incl is transitive.

(open(pub(self)), law, sealed)

requires

a.incl(b)

requires

b.incl(c)

ensures

a.incl(c)

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<T: RA> RA for Option<T>

fn op(self, other: Self) -> Option<Self>

(open)

match (self, other) {
    (None, _) => Some(other),
    (_, None) => Some(self),
    (Some(x), Some(y)) => x.op(y).map_logic(|z| Some(z)),
}

fn factor(self, factor: Self) -> Option<Self>

(open)

match (self, factor) {
    (x, None) => Some(x),
    (None, _) => None,
    (Some(x), Some(y)) => match x.factor(y) {
        Some(z) => Some(Some(z)),
        None => {
            if x == y {
                Some(None)
            } else {
                None
            }
        }
    },
}

ensures

match result {
        Some(c) => factor.op(c) == Some(self),
        None => forall<c: Self> factor.op(c) != Some(self),
    }

fn commutative(a: Self, b: Self)

(open(pub(self)), law)

ensures

a.op(b) == b.op(a)

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

(open(pub(self)), law)

ensures

a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc))

fn core(self) -> Option<Self>

(open)

Some(self.core_total())

ensures

match result {
        Some(c) => c.op(c) == Some(c) && c.op(self) == Some(self),
        None => true
    }

fn core_is_maximal_idemp(self, i: Self)

requires

i.op(i) == Some(i)

requires

i.op(self) == Some(self)

ensures

match self.core() {
        Some(c) => i.incl(c),
        None => false,
    }

impl<T: RA, U: RA> RA for (T, U)

fn op(self, other: Self) -> Option<Self>

(open)

self.0.op(other.0).and_then_logic(|x| self.1.op(other.1).map_logic(|y| (x, y)))

fn factor(self, factor: Self) -> Option<Self>

(open)

match (self.0.factor(factor.0), self.1.factor(factor.1)) {
    (Some(x), Some(y)) => Some((x, y)),
    _ => None,
}

ensures

match result {
        Some(c) => factor.op(c) == Some(self),
        None => forall<c: Self> factor.op(c) != Some(self),
    }

fn commutative(a: Self, b: Self)

(open(pub(self)), law)

ensures

a.op(b) == b.op(a)

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

(open(pub(self)), law)

ensures

a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc))

fn core(self) -> Option<Self>

(open)

match (self.0.core(), self.1.core()) {
    (Some(x), Some(y)) => Some((x, y)),
    _ => None,
}

ensures

match result {
        Some(c) => c.op(c) == Some(c) && c.op(self) == Some(self),
        None => true
    }

fn core_is_maximal_idemp(self, i: Self)

requires

i.op(i) == Some(i)

requires

i.op(self) == Some(self)

ensures

match self.core() {
        Some(c) => i.incl(c),
        None => false,
    }

Implementors

impl<K, V: RA> RA for FMap<K, V>

impl<R1: RA, R2: RA> RA for Sum<R1, R2>

impl<R: ViewRel> RA for View<R>

impl<T> RA for Ag<T>

impl<T> RA for Excl<T>