pub struct FracResource<T, const TOTAL: u64> { /* private fields */ }Expand description
A struct that stores and dispatches Frac<T>.
Unlike Frac, it provides an empty state.
Implementations§
Source§impl<T, const TOTAL: u64> FracResource<T, TOTAL>
impl<T, const TOTAL: u64> FracResource<T, TOTAL>
Sourcepub closed spec fn storage(self) -> Frac<T, TOTAL>
pub closed spec fn storage(self) -> Frac<T, TOTAL>
Returns the Frac<T,TOTAL> stored in this FracResource.
Sourcepub open spec fn wf(self) -> bool
pub open spec fn wf(self) -> bool
{
&&& TOTAL > 0
&&& 0 <= self.frac() <= TOTAL
&&& self.type_inv()
}Type invariant.
Sourcepub open spec fn is_empty(self) -> bool
pub open spec fn is_empty(self) -> bool
{ self.frac() == 0 }Whether this FracResource is empty, i.e., has no fraction.
Sourcepub open spec fn not_empty(self) -> bool
pub open spec fn not_empty(self) -> bool
{ !self.is_empty() }Whether the fraction stored in this FracResource is less than TOTAL.
Sourcepub open spec fn is_full(self) -> bool
pub open spec fn is_full(self) -> bool
{ self.frac() == TOTAL }Whether this FracResource has the full fraction, i.e., TOTAL.
Sourcepub closed spec fn resource(self) -> T
pub closed spec fn resource(self) -> T
Returns the value of type T stored in this FracResource.
Sourcepub open spec fn view(self) -> T
pub open spec fn view(self) -> T
{ self.resource() }Returns the value of type T stored in this FracResource. It is an alias of Self::resource.
Sourcepub proof fn arbitrary() -> tracked res : Self
pub proof fn arbitrary() -> tracked res : Self
requires
TOTAL > 0,Create an arbitrary FracResource. Useful as a placeholder.
Sourcepub proof fn alloc(tracked value: T) -> tracked res : Self
pub proof fn alloc(tracked value: T) -> tracked res : Self
requires
TOTAL > 0,res.not_empty(),res.is_full(),res@ == value,res.wf(),Allocates a new FracResource with the given tracked object.
Sourcepub proof fn alloc_from_empty(tracked empty: Empty<T, TOTAL>, tracked value: T) -> tracked res : Self
pub proof fn alloc_from_empty(tracked empty: Empty<T, TOTAL>, tracked value: T) -> tracked res : Self
requires
TOTAL > 0,res.is_full(),res.id() == empty.id(),res.view() == value,res.wf(),Allocates a new FracResource from an Empty<T,TOTAL> with the given tracked object.
Sourcepub proof fn split_one(tracked &mut self) -> tracked res : Frac<T, TOTAL>
pub proof fn split_one(tracked &mut self) -> tracked res : Frac<T, TOTAL>
requires
old(self).not_empty(),self.id() == old(self).id(),self.frac() + 1 == old(self).frac(),old(self).frac() > 1 ==> self@ == old(self)@,res.frac() == 1,res.id() == self.id(),res.resource() == old(self)@,old(self).frac() == 1 ==> self.is_empty(),self.wf(),Splits a Frac with fraction 1.
Sourcepub proof fn split(tracked &mut self, n: int) -> tracked res : Frac<T, TOTAL>
pub proof fn split(tracked &mut self, n: int) -> tracked res : Frac<T, TOTAL>
requires
1 <= n <= old(self).frac(),self.id() == old(self).id(),self.frac() + n == old(self).frac(),old(self).frac() > n ==> self@ == old(self)@,res.frac() == n,res.id() == self.id(),res.resource() == old(self)@,old(self).frac() == n ==> self.is_empty(),self.wf(),Splits a Frac with the given fraction.
Sourcepub proof fn combine(tracked &mut self, tracked other: Frac<T, TOTAL>)
pub proof fn combine(tracked &mut self, tracked other: Frac<T, TOTAL>)
requires
old(self).id() == other.id(),old(self).frac() + other.frac() > TOTAL ==> false,old(self).frac() + other.frac() <= TOTAL
==> {
&&& self.id() == old(self).id()
&&& self.resource() == other.resource()
&&& self.frac() == old(self).frac() + other.frac()
&&& self.wf()
&&& old(self).frac() > 0 ==> self@ == old(self)@
},Combines a Frac.
Sourcepub proof fn validate(tracked &self)
pub proof fn validate(tracked &self)
ensures
self.wf(),FracResource satisfies the type invariant.
Sourcepub proof fn validate_full(tracked &self)
pub proof fn validate_full(tracked &self)
requires
self.is_full(),self.not_empty(),self.frac() == TOTAL,self.wf(),Sourcepub proof fn validate_with_frac(tracked &self, tracked frac: &Frac<T, TOTAL>)
pub proof fn validate_with_frac(tracked &self, tracked frac: &Frac<T, TOTAL>)
requires
self.id() == frac.id(),self.frac() > 0,self.resource() == frac.resource(),Sourcepub proof fn take_resource(tracked self) -> tracked (T, Empty<T, TOTAL>)
pub proof fn take_resource(tracked self) -> tracked (T, Empty<T, TOTAL>)
requires
self.is_full(),res == self@,empty.id() == self.id(),Consumes the token and takes out the resource.
Sourcepub proof fn update(tracked &mut self, tracked value: T) -> tracked res : T
pub proof fn update(tracked &mut self, tracked value: T) -> tracked res : T
requires
old(self).is_full(),self.is_full(),res == old(self)@,self.id() == old(self).id(),self.wf(),Updates the resource stored in this FracResource and retunrs the old resource if it exists.
The fraction must be full before the update.
Auto Trait Implementations§
impl<T, const TOTAL: u64> Freeze for FracResource<T, TOTAL>
impl<T, const TOTAL: u64> RefUnwindSafe for FracResource<T, TOTAL>where
T: RefUnwindSafe,
impl<T, const TOTAL: u64> Send for FracResource<T, TOTAL>
impl<T, const TOTAL: u64> Sync for FracResource<T, TOTAL>
impl<T, const TOTAL: u64> Unpin for FracResource<T, TOTAL>where
T: Unpin,
impl<T, const TOTAL: u64> UnwindSafe for FracResource<T, TOTAL>where
T: UnwindSafe,
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more