CsumP

vstd_extra::resource::storage_protocol::csum

Enum CsumP 

Source 
pub enum CsumP<A, B, const TOTAL: u64> {
    Unit,
    Cinl(Option<A>, int, bool),
    Cinr(Option<B>, int, bool),
    CsumInvalid,
}
Expand description

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.

§

Cinl(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.

§

Cinr(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§

Source§

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

Source

pub fn arrow_2(self) -> bool

Source

pub fn arrow_1(self) -> int

Source

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

Source

pub fn arrow_Cinl_1(self) -> int

Source

pub fn arrow_Cinl_2(self) -> bool

Source

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

Source

pub fn arrow_Cinr_1(self) -> int

Source

pub fn arrow_Cinr_2(self) -> bool

Source§

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

Source

pub open spec fn is_left(self) -> bool

{ self is Cinl }

Whether the protocol monoid is currently in the left state.

Source

pub open spec fn is_right(self) -> bool

{ self is Cinr }

Whether the protocol monoid is currently in the right state.

Source

pub open spec fn is_resource_owner(self) -> bool

{
    match self {
        CsumP::Cinl(_, _, b) | CsumP::Cinr(_, _, b) => b,
        _ => false,
    }
}

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

Source

pub open spec fn has_resource(self) -> bool

{
    match self {
        CsumP::Cinl(ov, n, true) => ov is Some,
        CsumP::Cinr(ov, n, true) => ov is Some,
        _ => false,
    }
}

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

Source

pub open spec fn has_no_resource(self) -> bool

{
    match self {
        CsumP::Cinl(ov, n, true) => ov is None,
        CsumP::Cinr(ov, n, true) => ov is None,
        _ => false,
    }
}

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

Source

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

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

The resource stored in the protocol monoid.

Source

pub open spec fn frac(self) -> int

{
    match self {
        CsumP::Cinl(_, n, _) | CsumP::Cinr(_, n, _) => n,
        _ => 1,
    }
}

The fraction of the resource knowledge.

Source

pub open spec fn is_valid(self) -> bool

{
    match self {
        CsumP::Unit => true,
        CsumP::Cinl(ov, n, b) => 0 < n <= TOTAL && (ov is Some ==> b),
        CsumP::Cinr(ov, n, b) => 0 < n <= TOTAL && (ov is Some ==> b),
        _ => false,
    }
}

The invariant of the protocol monoid.

Source

pub proof fn lemma_withdraws_left(self)

requires
self.is_left(),
self.is_resource_owner(),
self.has_resource(),
self.is_valid(),
ensures
withdraws(self, CsumP::Cinl(None, self.frac(), true), map![() => self.resource()]),
Source

pub proof fn lemma_withdraws_right(self)

requires
self.is_resource_owner(),
self.is_right(),
self.has_resource(),
self.is_valid(),
ensures
withdraws(self, CsumP::Cinr(None, self.frac(), true), map![() => self.resource()]),
Source

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, map![() => Sum::Left(a)], CsumP::Cinl(Some(a), self.frac(), true)),
Source

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, map![() => Sum::Right(b)], CsumP::Cinr(Some(b), self.frac(), true)),
Source

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, CsumP::Cinl(None, self.frac(), true)),
updates(self, CsumP::Cinr(None, self.frac(), true)),

Trait Implementations§

Source§

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

Source§

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

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

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

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

open spec fn unit() -> Self

{ CsumP::Unit }
Source§

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

Source§

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

Source§

proof fn op_unit(a: Self)

Auto Trait Implementations§

§

impl<A, B, const TOTAL: u64> Freeze for CsumP<A, B, TOTAL>
where A: Freeze, B: Freeze,

§

impl<A, B, const TOTAL: u64> RefUnwindSafe for CsumP<A, B, TOTAL>
where A: RefUnwindSafe, B: RefUnwindSafe,

§

impl<A, B, const TOTAL: u64> Send for CsumP<A, B, TOTAL>
where A: Send, B: Send,

§

impl<A, B, const TOTAL: u64> Sync for CsumP<A, B, TOTAL>
where A: Sync, B: Sync,

§

impl<A, B, const TOTAL: u64> Unpin for CsumP<A, B, TOTAL>
where A: Unpin, B: Unpin,

§

impl<A, B, const TOTAL: u64> UnwindSafe for CsumP<A, B, TOTAL>
where A: UnwindSafe, B: UnwindSafe,

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

§

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

§

fn obeys_from_spec() -> bool

§

fn from_spec(v: T) -> VERUS_SPEC__A

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

§

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> T

§

impl<T, U> IntoSpecImpl<U> for T
where U: From<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> U

Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

§

fn obeys_try_from_spec() -> bool

§

fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

§

impl<T, U> TryIntoSpecImpl<U> for T
where U: TryFrom<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>