SumResource

vstd_extra::resource::ghost_resource::csum

Struct SumResource 

Source 
pub struct SumResource<A, B, const TOTAL: u64 = 2> { /* private fields */ }
Expand description

SumResource is a token that maintains access to a resource of either type A or type B. It can be split into up to TOTAL fractions, one of which have the exclusive right to access the resource, and others shares the knowledge of the resource’s existence and type, but not the ability to access it.

Implementations§

Source§

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

Source

pub closed spec fn id(self) -> Loc

Returns the unique identifier.

Source

pub closed spec fn protocol_monoid(self) -> CsumP<A, B, TOTAL>

The underlying protocol monoid value for this resource.

Source

pub open spec fn is_resource_owner(self) -> bool

{ self.protocol_monoid().is_resource_owner() }

Whether this token has the right to access the underlying resource.

Source

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

{ self.protocol_monoid().resource() }

The resource value, only meaningful if is_resource_owner is true.

Source

pub open spec fn resource_left(self) -> A

{ self.resource()->Left_0 }

The resource value if this token is in the left variant, only meaningful if is_resource_owner is true.

Source

pub open spec fn resource_right(self) -> B

{ self.resource()->Right_0 }

The resource value if this token is in the right variant, only meaningful if is_resource_owner is true.

Source

pub open spec fn is_left(self) -> bool

{ self.protocol_monoid().is_left() }

Whether this token is a Left variant.

Source

pub open spec fn is_right(self) -> bool

{ self.protocol_monoid().is_right() }

Whether this token is a Right variant.

Source

pub open spec fn has_resource(self) -> bool

{
    let p = self.protocol_monoid();
    p.is_resource_owner() && p.has_resource()
}

Whether the resource is currently stored, returns false if this token is not the resource owner.

Source

pub open spec fn has_no_resource(self) -> bool

{
    let p = self.protocol_monoid();
    p.is_resource_owner() && p.has_no_resource()
}

Whether the resource has been taken, returns false if this token is not the resource owner.

Source

pub open spec fn frac(self) -> int

{ self.protocol_monoid().frac() }

The fraction this token represents.

Source

pub open spec fn wf(self) -> bool

{
    &&& 1 <= self.frac() <= TOTAL
    &&& self.protocol_monoid().is_valid()
    &&& self.is_resource_owner() ==> (self.has_resource() <==> !self.has_no_resource())
    &&& (self.is_left() <==> !self.is_right())

}

Type invariant.

Source

pub proof fn alloc_left(tracked a: A) -> tracked res : Self

requires
TOTAL > 0,
ensures
res.is_left(),
res.is_resource_owner(),
res.has_resource(),
res.resource() == Sum::<A, B>::Left(a),
res.frac() == TOTAL,
res.wf(),

Allocates a new SumResource with the resource of type A.

Source

pub proof fn alloc_right(tracked b: B) -> tracked res : Self

requires
TOTAL > 0,
ensures
res.is_right(),
res.is_resource_owner(),
res.has_resource(),
res.resource() == Sum::<A, B>::Right(b),
res.frac() == TOTAL,
res.wf(),

Allocates a new SumResource with the resource of type B.

Source

pub proof fn validate(tracked &self)

ensures
self.wf(),

SumResource satisfies its type invariant.

Source

pub proof fn validate_with_other(tracked &mut self, tracked other: &Self)

requires
old(self).is_left() && old(self).is_right() || other.is_left() && other.is_right()
    || old(self).is_left() && other.is_left() && old(self).is_resource_owner()
        && other.is_resource_owner()
    || old(self).is_right() && other.is_right() && old(self).is_resource_owner()
        && other.is_resource_owner(),
ensures
*old(self) == *self,
self.id() != other.id(),
self.wf(),

Two SumResource tokens can not both be the resource owner unless they have different ids.

Source

pub proof fn validate_with_left(tracked &mut self, tracked other: &Left<A, B, TOTAL>)

requires
old(self).id() == other.id(),
ensures
*old(self) == *self,
self.is_left(),
!(self.is_resource_owner() && other.is_resource_owner()),
self.frac() + other.frac() <= TOTAL,
self.wf(),

The existence of a Left token with the same id ensures this token is also a Left token.

Source

pub proof fn validate_with_right(tracked &mut self, tracked other: &Right<A, B, TOTAL>)

requires
old(self).id() == other.id(),
ensures
*old(self) == *self,
self.is_right(),
!(self.is_resource_owner() && other.is_resource_owner()),
self.frac() + other.frac() <= TOTAL,
self.wf(),

The existence of a Right token with the same id ensures this token is also a Right token.

Source

pub proof fn validate_with_one_left_owner(tracked &mut self, tracked other: &OneLeftOwner<A, B, TOTAL>, )

requires
old(self).id() == other.id(),
ensures
*old(self) == *self,
self.is_left(),
!self.is_resource_owner(),
self.frac() + 1 <= TOTAL,
self.wf(),

The existence of a OneLeftOwner token with the same id ensures this token is a Left token that is not the resource owner.

Source

pub proof fn validate_with_one_right_owner(tracked &mut self, tracked other: &OneRightOwner<A, B, TOTAL>, )

requires
old(self).id() == other.id(),
ensures
*old(self) == *self,
self.is_right(),
!self.is_resource_owner(),
self.frac() + 1 <= TOTAL,
self.wf(),

The existence of a OneRightOwner token with the same id ensures this token is a Right token that is not the resource owner.

Source

pub proof fn validate_with_one_left_knowledge(tracked &mut self, tracked other: &OneLeftKnowledge<A, B, TOTAL>, )

requires
old(self).id() == other.id(),
ensures
*old(self) == *self,
self.is_left(),
self.frac() + 1 <= TOTAL,
self.wf(),

The existence of a OneLeftKnowledge token with the same id ensures this token is a Left token.

Source

pub proof fn validate_with_one_right_knowledge(tracked &mut self, tracked other: &OneRightKnowledge<A, B, TOTAL>, )

requires
old(self).id() == other.id(),
ensures
*old(self) == *self,
self.is_right(),
self.frac() + 1 <= TOTAL,
self.wf(),

The existence of a OneRightKnowledge token with the same id ensures this token is a Right token.

Source

pub proof fn tracked_borrow_left(tracked &self) -> tracked res : &A

requires
self.is_left(),
self.is_resource_owner(),
self.has_resource(),
ensures
*res == self.resource_left(),

Borrows the resource of type A.

Source

pub proof fn tracked_borrow_right(tracked &self) -> tracked res : &B

requires
self.is_right(),
self.is_resource_owner(),
self.has_resource(),
ensures
*res == self.resource()->Right_0,

Borrows the resource of type B.

Source

pub proof fn split_left_with_resource(tracked &mut self, n: int) -> tracked res : Left<A, B, TOTAL>

requires
old(self).is_left(),
0 < n < old(self).frac(),
ensures
self.id() == old(self).id(),
self.frac() == old(self).frac() - n,
res.id() == old(self).id(),
res.frac() == n,
!self.is_resource_owner(),
res.is_resource_owner() <==> old(self).is_resource_owner(),
res.is_resource_owner() ==> (res.has_resource() <==> old(self).has_resource()),
res.has_resource() ==> res.resource() == old(self).resource_left(),
self.wf(),
res.wf(),

Splits a Left token with the given fraction n, and gives the resource to that Left token if available.

Source

pub proof fn split_left_without_resource(tracked &mut self, n: int) -> tracked res : Left<A, B, TOTAL>

requires
old(self).is_left(),
0 < n < old(self).frac(),
ensures
self.id() == old(self).id(),
self.frac() == old(self).frac() - n,
res.id() == old(self).id(),
res.frac() == n,
!res.is_resource_owner(),
self.is_resource_owner() <==> old(self).is_resource_owner(),
self.is_resource_owner() ==> (self.has_resource() <==> old(self).has_resource()),
self.has_resource() ==> self.resource() == old(self).resource(),
self.wf(),
res.wf(),

Splits a Left token with the given fraction n, without giving the resource to the Left token.

Source

pub proof fn split_right_with_resource(tracked &mut self, n: int) -> tracked res : Right<A, B, TOTAL>

requires
old(self).is_right(),
0 < n < old(self).frac(),
ensures
self.id() == old(self).id(),
self.frac() == old(self).frac() - n,
res.id() == old(self).id(),
res.frac() == n,
!self.is_resource_owner(),
res.is_resource_owner() <==> old(self).is_resource_owner(),
res.is_resource_owner() ==> (res.has_resource() <==> old(self).has_resource()),
res.has_resource() ==> res.resource() == old(self).resource_right(),
self.wf(),
res.wf(),

Splits a Right token with the given fraction n, and gives the resource to that Right token if available.

Source

pub proof fn split_right_without_resource(tracked &mut self, n: int) -> tracked res : Right<A, B, TOTAL>

requires
old(self).is_right(),
0 < n < old(self).frac(),
ensures
self.id() == old(self).id(),
self.frac() == old(self).frac() - n,
res.id() == old(self).id(),
res.frac() == n,
!res.is_resource_owner(),
self.is_resource_owner() <==> old(self).is_resource_owner(),
self.is_resource_owner() ==> (self.has_resource() <==> old(self).has_resource()),
self.has_resource() ==> self.resource() == old(self).resource(),
self.wf(),
res.wf(),

Splits a Right token with the given fraction n, without giving the resource to the Right token.

Source

pub proof fn split_one_left_owner(tracked &mut self) -> tracked res : OneLeftOwner<A, B, TOTAL>

requires
old(self).is_left(),
old(self).is_resource_owner(),
old(self).frac() > 1,
ensures
self.wf(),
self.id() == old(self).id(),
self.is_left(),
self.frac() + 1 == old(self).frac(),
!self.is_resource_owner(),
res.id() == old(self).id(),
res.wf(),
res.has_resource() == old(self).has_resource(),
res.has_resource() ==> res.resource() == old(self).resource_left(),

Splits a OneLeftOwner, giving it the resource.

Source

pub proof fn split_one_right_owner(tracked &mut self) -> tracked res : OneRightOwner<A, B, TOTAL>

requires
old(self).is_right(),
old(self).is_resource_owner(),
old(self).frac() > 1,
ensures
self.wf(),
self.id() == old(self).id(),
self.is_right(),
self.frac() + 1 == old(self).frac(),
!self.is_resource_owner(),
res.id() == old(self).id(),
res.wf(),
res.has_resource() == old(self).has_resource(),
res.has_resource() ==> res.resource() == old(self).resource_right(),

Splits a OneRightOwner, giving it the resource.

Source

pub proof fn split_one_left_knowledge(tracked &mut self) -> tracked res : OneLeftKnowledge<A, B, TOTAL>

requires
old(self).is_left(),
old(self).frac() > 1,
ensures
self.wf(),
self.id() == old(self).id(),
self.is_left(),
self.frac() + 1 == old(self).frac(),
self.is_resource_owner() == old(self).is_resource_owner(),
self.has_resource() == old(self).has_resource(),
self.has_resource() ==> self.resource() == old(self).resource(),
res.id() == old(self).id(),
res.wf(),

Splits a OneLeftKnowledge, without giving it the resource.

Source

pub proof fn split_one_right_knowledge(tracked &mut self) -> tracked res : OneRightKnowledge<A, B, TOTAL>

requires
old(self).is_right(),
old(self).frac() > 1,
ensures
self.wf(),
self.id() == old(self).id(),
self.is_right(),
self.frac() + 1 == old(self).frac(),
self.is_resource_owner() == old(self).is_resource_owner(),
self.has_resource() == old(self).has_resource(),
self.has_resource() ==> self.resource() == old(self).resource(),
res.id() == old(self).id(),
res.wf(),

Splits a OneRightKnowledge, without giving it the resource.

Source

pub proof fn take_resource_left(tracked &mut self) -> tracked res : A

requires
old(self).is_left(),
old(self).is_resource_owner(),
old(self).has_resource(),
ensures
self.is_left(),
res == old(self).resource_left(),
self.id() == old(self).id(),
self.is_resource_owner(),
self.has_no_resource(),
self.frac() == old(self).frac(),
self.wf(),

Takes the resource out of the token if it is in the left variant.

Source

pub proof fn take_resource_right(tracked &mut self) -> tracked res : B

requires
old(self).is_right(),
old(self).is_resource_owner(),
old(self).has_resource(),
ensures
self.is_right(),
res == old(self).resource_right(),
self.id() == old(self).id(),
self.is_resource_owner(),
self.has_no_resource(),
self.frac() == old(self).frac(),
self.wf(),

Takes the resource out of the token if it is in the right variant.

Source

pub proof fn put_resource_left(tracked &mut self, tracked a: A)

requires
old(self).is_left(),
old(self).is_resource_owner(),
old(self).has_no_resource(),
ensures
self.is_left(),
self.has_resource(),
self.is_resource_owner(),
self.resource_left() == a,
self.id() == old(self).id(),
self.frac() == old(self).frac(),
self.wf(),

Puts a resource of type A back to the token.

Source

pub proof fn put_resource_right(tracked &mut self, tracked b: B)

requires
old(self).is_right(),
old(self).is_resource_owner(),
old(self).has_no_resource(),
ensures
self.is_right(),
self.is_resource_owner(),
self.has_resource(),
self.resource_right() == b,
self.id() == old(self).id(),
self.frac() == old(self).frac(),
self.wf(),

Puts a resource of type B back to the token.

Source

pub proof fn update_left(tracked &mut self, tracked a: A) -> tracked res : Option<A>

requires
old(self).is_left(),
old(self).is_resource_owner(),
old(self).has_resource(),
ensures
self.is_left(),
self.is_resource_owner(),
self.has_resource(),
self.resource_left() == a,
self.id() == old(self).id(),
self.frac() == old(self).frac(),
res == Some(old(self).resource_left()),
self.wf(),

Updates the resource of type A in the token, when the token is in the left variant and is a resource owner. Returns the old resource if available.

Source

pub proof fn update_right(tracked &mut self, tracked b: B) -> tracked res : Option<B>

requires
old(self).is_right(),
old(self).is_resource_owner(),
old(self).has_resource(),
ensures
self.is_right(),
self.is_resource_owner(),
self.has_resource(),
self.resource_right() == b,
self.id() == old(self).id(),
self.frac() == old(self).frac(),
res == Some(old(self).resource_right()),
self.wf(),

Updates the resource of type B in the token, when the token is in the right variant and is a resource owner. Returns the old resource if available.

Source

pub proof fn change_to_left(tracked &mut self, tracked a: A) -> tracked res : Option<Sum<A, B>>

requires
old(self).is_resource_owner(),
old(self).frac() == TOTAL,
ensures
self.id() == old(self).id(),
self.protocol_monoid() == CsumP::<A, B, TOTAL>::Cinl(Some(a), old(self).frac(), true),
self.frac() == old(self).frac(),
self.is_left(),
self.is_resource_owner(),
self.has_resource(),
self.resource_left() == a,
old(self).has_resource() ==> res == Some(old(self).resource()),
old(self).has_no_resource() ==> res == None::<Sum<A, B>>,
self.wf(),

Changes the token to the left invariant with a new resource of type A, and returns the old resource if available.

NOTE: Unlike Self::update_left, this operation can only be done with the full fraction, because there should be no Right tokens to witness the existence of the old resource after the update.

Source

pub proof fn change_to_right(tracked &mut self, tracked b: B) -> tracked res : Option<Sum<A, B>>

requires
old(self).is_resource_owner(),
old(self).frac() == TOTAL,
ensures
self.id() == old(self).id(),
self.protocol_monoid() == CsumP::<A, B, TOTAL>::Cinr(Some(b), old(self).frac(), true),
self.frac() == old(self).frac(),
self.is_right(),
self.is_resource_owner(),
self.has_resource(),
self.resource_right() == b,
old(self).has_resource() ==> res == Some(old(self).resource()),
old(self).has_no_resource() ==> res == None::<Sum<A, B>>,
self.wf(),

Changes the token to the right invariant with a new resource of type B, and returns the old resource if available.

NOTE: Unlike Self::update_right, this operation can only be done with the full fraction, because there should be no Left tokens to witness the existence of the old resource after the update.

Source

pub proof fn join_left(tracked &mut self, tracked other: Left<A, B, TOTAL>)

requires
old(self).id() == other.id(),
ensures
self.id() == old(self).id(),
self.is_left(),
self.is_resource_owner() == (old(self).is_resource_owner() || other.is_resource_owner()),
self.has_resource() == (old(self).has_resource() || other.has_resource()),
self.has_resource()
    ==> self.resource()
        == if old(self).is_resource_owner() {
            old(self).resource()
        } else {
            Sum::Left(other.resource())
        },
self.frac() == old(self).frac() + other.frac(),
self.wf(),

Joins this token with another Left token with the same id.

Source

pub proof fn join_right(tracked &mut self, tracked other: Right<A, B, TOTAL>)

requires
old(self).id() == other.id(),
ensures
self.id() == old(self).id(),
self.is_right(),
self.is_resource_owner() == (old(self).is_resource_owner() || other.is_resource_owner()),
self.has_resource() == (old(self).has_resource() || other.has_resource()),
self.has_resource()
    ==> self.resource()
        == if old(self).is_resource_owner() {
            old(self).resource()
        } else {
            Sum::Right(other.resource())
        },
self.frac() == old(self).frac() + other.frac(),
self.wf(),

Joins this token with another Right token with the same id.

Source

pub proof fn join_one_left_owner(tracked &mut self, tracked other: OneLeftOwner<A, B, TOTAL>)

requires
old(self).id() == other.id(),
ensures
self.id() == old(self).id(),
self.is_left(),
self.is_resource_owner(),
self.has_resource() == other.has_resource(),
self.has_resource() ==> self.resource_left() == other.resource(),
self.frac() == old(self).frac() + 1,
self.wf(),

Joins a OneLeftOwner token.

Source

pub proof fn join_one_right_owner(tracked &mut self, tracked other: OneRightOwner<A, B, TOTAL>)

requires
old(self).id() == other.id(),
ensures
self.id() == old(self).id(),
self.is_right(),
self.is_resource_owner(),
self.has_resource() == other.has_resource(),
self.has_resource() ==> self.resource_right() == other.resource(),
self.frac() == old(self).frac() + 1,
self.wf(),

Joins a OneRightOwner token.

Source

pub proof fn join_one_left_knowledge(tracked &mut self, tracked other: OneLeftKnowledge<A, B, TOTAL>)

requires
old(self).id() == other.id(),
ensures
self.id() == old(self).id(),
self.is_left(),
self.is_resource_owner() == old(self).is_resource_owner(),
self.has_resource() == old(self).has_resource(),
self.has_resource() ==> self.resource() == old(self).resource(),
self.frac() == old(self).frac() + 1,
self.wf(),

Joins a OneLeftKnowledge token.

Source

pub proof fn join_one_right_knowledge(tracked &mut self, tracked other: OneRightKnowledge<A, B, TOTAL>, )

requires
old(self).id() == other.id(),
ensures
self.id() == old(self).id(),
self.is_right(),
self.is_resource_owner() == old(self).is_resource_owner(),
self.has_resource() == old(self).has_resource(),
self.has_resource() ==> self.resource() == old(self).resource(),
self.frac() == old(self).frac() + 1,
self.wf(),

Joins a OneRightKnowledge token.

Auto Trait Implementations§

§

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

§

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

§

impl<A, B, const TOTAL: u64> Send for SumResource<A, B, TOTAL>
where A: Send + Sync, B: Send + Sync,

§

impl<A, B, const TOTAL: u64> Sync for SumResource<A, B, TOTAL>
where A: Sync + Send, B: Sync + Send,

§

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

§

impl<A, B, const TOTAL: u64> UnwindSafe for SumResource<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>