Enum Sum 

pub enum Sum<T, U> {
    Left(T),
    Right(U),
}

The ‘sum’ (or ‘either’) Resource Algebra.

This represents a resource that is in two possible states. Combining a Left with a Right is invalid.

Variants

Left(T)

Right(U)

Trait Implementations

impl<R1: RA, R2: RA, U: LocalUpdate<R1>> LocalUpdate<Sum<R1, R2>> for SumLocalUpdateL<U>

fn premise(self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>) -> bool

(open)

match (from_auth, from_frag) {
    (Sum::Left(from_auth), Sum::Left(from_frag)) => self.0.premise(from_auth, from_frag),
    (Sum::Right(_), Sum::Right(_)) => false,
    _ => true,
}

fn update( self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>, ) -> (Sum<R1, R2>, Sum<R1, R2>)

(open)

match (from_auth, from_frag) {
    (Sum::Left(from_auth), Sum::Left(from_frag)) => {
        let (to_auth, to_frag) = self.0.update(from_auth, from_frag);
        (Sum::Left(to_auth), Sum::Left(to_frag))
    }
    _ => such_that(|_| true),
}

fn frame_preserving( self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>, frame: Option<Sum<R1, R2>>, )

requires

self.premise(from_auth, from_frag)

requires

Some(from_frag).op(frame) == Some(Some(from_auth))

ensures

let (to_auth, to_frag) = self.update(from_auth, from_frag);
Some(to_frag).op(frame) == Some(Some(to_auth))

impl<R1: RA, R2: RA, U: LocalUpdate<R2>> LocalUpdate<Sum<R1, R2>> for SumLocalUpdateR<U>

fn premise(self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>) -> bool

(open)

match (from_auth, from_frag) {
    (Sum::Right(from_auth), Sum::Right(from_frag)) => self.0.premise(from_auth, from_frag),
    (Sum::Left(_), Sum::Left(_)) => false,
    _ => true,
}

fn update( self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>, ) -> (Sum<R1, R2>, Sum<R1, R2>)

(open)

match (from_auth, from_frag) {
    (Sum::Right(from_auth), Sum::Right(from_frag)) => {
        let (to_auth, to_frag) = self.0.update(from_auth, from_frag);
        (Sum::Right(to_auth), Sum::Right(to_frag))
    }
    _ => such_that(|_| true),
}

fn frame_preserving( self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>, frame: Option<Sum<R1, R2>>, )

requires

self.premise(from_auth, from_frag)

requires

Some(from_frag).op(frame) == Some(Some(from_auth))

ensures

let (to_auth, to_frag) = self.update(from_auth, from_frag);
Some(to_frag).op(frame) == Some(Some(to_auth))

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

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

(open)

match (self, other) {
    (Self::Left(x), Self::Left(y)) => x.op(y).map_logic(|l| Self::Left(l)),
    (Self::Right(x), Self::Right(y)) => x.op(y).map_logic(|r| Self::Right(r)),
    _ => None,
}

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

(open)

match (self, factor) {
    (Self::Left(x), Self::Left(y)) => x.factor(y).map_logic(|l| Self::Left(l)),
    (Self::Right(x), Self::Right(y)) => x.factor(y).map_logic(|r| Self::Right(r)),
    _ => 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 {
    Self::Left(x) => x.core().map_logic(|l| Self::Left(l)),
    Self::Right(x) => x.core().map_logic(|r| Self::Right(r)),
}

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,
    }

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

Inclusion of RA.

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

(law, sealed)

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

(open, sealed)

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

(open, sealed)

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

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

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

This is used in Resource::update_nondet.

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

RA::incl is transitive.

impl<R1: RA, R2: RA, U: Update<R1>> Update<Sum<R1, R2>> for SumUpdateL<U>

fn premise(self, from: Sum<R1, R2>) -> bool

(open)

match from {
    Sum::Left(from) => self.0.premise(from),
    Sum::Right(_) => false,
}

fn update(self, from: Sum<R1, R2>, ch: U::Choice) -> Sum<R1, R2>

(open)

match from {
    Sum::Left(from) => Sum::Left(self.0.update(from, ch)),
    x => x, /* Dummy */
}

requires

self.premise(from)

fn frame_preserving(self, from: Sum<R1, R2>, frame: Sum<R1, R2>) -> U::Choice

requires

self.premise(from)

requires

from.op(frame) != None

ensures

self.update(from, result).op(frame) != None

type Choice = <U as Update<R1>>::Choice

impl<R: RA, U: Update<R>, V: RA> Update<Sum<V, R>> for SumUpdateR<U>

fn premise(self, from: Sum<V, R>) -> bool

(open)

match from {
    Sum::Right(from) => self.0.premise(from),
    Sum::Left(_) => false,
}

fn update(self, from: Sum<V, R>, ch: U::Choice) -> Sum<V, R>

(open)

match from {
    Sum::Right(from) => Sum::Right(self.0.update(from, ch)),
    x => x, /* Dummy */
}

requires

self.premise(from)

fn frame_preserving(self, from: Sum<V, R>, frame: Sum<V, R>) -> U::Choice

requires

self.premise(from)

requires

from.op(frame) != None

ensures

self.update(from, result).op(frame) != None

type Choice = <U as Update<R>>::Choice