Enum SumSP 

pub enum SumSP<A, B, const TOTAL: u64> {
    Unit,
    Left(Option<A>, int, bool),
    Right(Option<B>, int, bool),
    CsumInvalid,
}

A sum-type protocol monoid that stores a tracked object of either type A or type B.

The knowledge of the existence of a specific type of resource can be shared up to TOTAL pieces, but only one piece has the exclusive ownership of the resource, allowing arbitrary withdrawing, depositing, or updating.

Variants

Unit

The unit element, only for technical reasons, not intended to be used directly.

Left(Option<A>, int, bool)

The left side of the sum, with an optional resource, a fraction, and a boolean indicating whether it is the exclusive owner of the resource.

Right(Option<B>, int, bool)

The right side of the sum, with an optional resource, a fraction, and a boolean indicating whether it is the exclusive owner of the resource.

CsumInvalid

An invalid state, used to represent an invalid combination of resources.

Implementations

impl<A, B, const TOTAL: u64> SumSP<A, B, TOTAL>

pub fn arrow_2(self) -> bool

pub fn arrow_1(self) -> int

pub fn arrow_Left_0(self) -> Option<A>

pub fn arrow_Left_1(self) -> int

pub fn arrow_Left_2(self) -> bool

pub fn arrow_Right_0(self) -> Option<B>

pub fn arrow_Right_1(self) -> int

pub fn arrow_Right_2(self) -> bool

impl<A, B, const TOTAL: u64> SumSP<A, B, TOTAL>

pub open spec fn is_left(self) -> bool

{ self is Left }

Whether the protocol monoid is currently in the left state.

pub open spec fn is_right(self) -> bool

{ self is Right }

Whether the protocol monoid is currently in the right state.

pub open spec fn is_resource_owner(self) -> bool

{
    match self {
        SumSP::Left(_, _, b) | SumSP::Right(_, _, b) => b,
        _ => false,
    }
}

Whether the protocol monoid is an exclusive owner of a resource.

pub open spec fn has_resource(self) -> bool

{
    match self {
        SumSP::Left(ov, n, true) => ov is Some,
        SumSP::Right(ov, n, true) => ov is Some,
        _ => false,
    }
}

Whether the protocol monoid currently owns a resource, only meaningful when it is the exclusive owner.

pub open spec fn has_no_resource(self) -> bool

{
    match self {
        SumSP::Left(ov, n, true) => ov is None,
        SumSP::Right(ov, n, true) => ov is None,
        _ => false,
    }
}

Whether the protocol monoid has had its resource taken, only meaningful when it is the exclusive owner.

pub open spec fn resource(self) -> Sum<A, B>

{
    match self {
        SumSP::Left(Some(a), n, true) => Sum::Left(a),
        SumSP::Right(Some(b), n, true) => Sum::Right(b),
        _ => arbitrary(),
    }
}

The resource stored in the protocol monoid.

pub open spec fn frac(self) -> int

{
    match self {
        SumSP::Left(_, n, _) | SumSP::Right(_, n, _) => n,
        _ => 1,
    }
}

The fraction of the resource knowledge.

pub open spec fn is_valid(self) -> bool

{
    match self {
        SumSP::Unit => true,
        SumSP::Left(ov, n, b) => 0 < n <= TOTAL && (ov is Some ==> b),
        SumSP::Right(ov, n, b) => 0 < n <= TOTAL && (ov is Some ==> b),
        _ => false,
    }
}

The invariant of the protocol monoid.

pub proof fn lemma_withdraws_left(self)

requires

self.is_left(),

self.is_resource_owner(),

self.has_resource(),

self.is_valid(),

ensures

withdraws(self, SumSP::Left(None, self.frac(), true), imap![() => self.resource()]),

pub proof fn lemma_withdraws_right(self)

requires

self.is_resource_owner(),

self.is_right(),

self.has_resource(),

self.is_valid(),

ensures

withdraws(self, SumSP::Right(None, self.frac(), true), imap![() => self.resource()]),

pub proof fn lemma_deposit_left(self, a: A)

requires

self.is_resource_owner(),

self.is_left(),

self.has_no_resource(),

self.is_valid(),

ensures

deposits(self, imap![() => Sum::Left(a)], SumSP::Left(Some(a), self.frac(), true)),

pub proof fn lemma_deposit_right(self, b: B)

requires

self.is_resource_owner(),

self.is_right(),

self.has_no_resource(),

self.is_valid(),

ensures

deposits(self, imap![() => Sum::Right(b)], SumSP::Right(Some(b), self.frac(), true)),

pub proof fn lemma_updates_none(self)

requires

self.is_left() || self.is_right(),

self.frac() == TOTAL,

self.is_resource_owner(),

self.has_no_resource(),

ensures

updates(self, SumSP::Left(None, self.frac(), true)),

updates(self, SumSP::Right(None, self.frac(), true)),

Trait Implementations

impl<A, B, const TOTAL: u64> Protocol<(), Sum<A, B>> for SumSP<A, B, TOTAL>

open spec fn op(self, other: Self) -> Self

{
    match (self, other) {
        (SumSP::Unit, x) => x,
        (x, SumSP::Unit) => x,
        (SumSP::Left(ov1, n1, b1), SumSP::Left(ov2, n2, b2)) => {
            if !self.is_valid() || !other.is_valid() || n1 + n2 > TOTAL || b1 && b2
                || ov1 is Some && ov2 is Some
            {
                SumSP::CsumInvalid
            } else {
                SumSP::Left(if ov1 is Some { ov1 } else { ov2 }, n1 + n2, b1 || b2)
            }
        }
        (SumSP::Right(ov1, n1, b1), SumSP::Right(ov2, n2, b2)) => {
            if !self.is_valid() || !other.is_valid() || n1 + n2 > TOTAL || b1 && b2
                || ov1 is Some && ov2 is Some
            {
                SumSP::CsumInvalid
            } else {
                SumSP::Right(if ov1 is Some { ov1 } else { ov2 }, n1 + n2, b1 || b2)
            }
        }
        _ => SumSP::CsumInvalid,
    }
}

open spec fn rel(self, s: IMap<(), Sum<A, B>>) -> bool

{
    match self {
        SumSP::Unit => s.is_empty(),
        SumSP::Left(None, n, true) => 0 <= n <= TOTAL && s.is_empty(),
        SumSP::Left(Some(a), n, true) => {
            0 <= n <= TOTAL && s.contains_key(()) && s[()] == Sum::<A, B>::Left(a)
        }
        SumSP::Right(None, n, true) => 0 <= n <= TOTAL && s.is_empty(),
        SumSP::Right(Some(b), n, true) => {
            0 <= n <= TOTAL && s.contains_key(()) && s[()] == Sum::<A, B>::Right(b)
        }
        _ => false,
    }
}

open spec fn unit() -> Self

{ SumSP::Unit }

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

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

proof fn op_unit(a: Self)