pub struct Frac<T, const TOTAL: u64 = 2> { /* private fields */ }
Expand description
Token that maintains fractional access to some resource.
This allows multiple clients to obtain shared references to some resource
via borrow
.
Implementations§
Source§impl<T, const TOTAL: u64> Frac<T, TOTAL>
impl<T, const TOTAL: u64> Frac<T, TOTAL>
Sourcepub open spec fn valid(self, id: Loc, frac: int) -> bool
pub open spec fn valid(self, id: Loc, frac: int) -> bool
{
&&& self.id() == id
&&& self.frac() == frac
}
Sourcepub proof fn new(tracked v: T) -> tracked result : Self
pub proof fn new(tracked v: T) -> tracked result : Self
requires
TOTAL > 0,
ensuresresult.frac() == TOTAL as int,
result.resource() == v,
Create a fractional token that maintains shared access to the input resource.
Sourcepub proof fn agree(tracked &self, tracked other: &Self)
pub proof fn agree(tracked &self, tracked other: &Self)
requires
self.id() == other.id(),
ensuresself.resource() == other.resource(),
Two tokens agree on values of the underlying resource.
Sourcepub proof fn split(tracked &mut self, n: int) -> tracked result : Self
pub proof fn split(tracked &mut self, n: int) -> tracked result : Self
requires
0 < n < old(self).frac(),
ensuresresult.id() == self.id() == old(self).id(),
self.resource() == old(self).resource(),
result.resource() == old(self).resource(),
self.frac() + result.frac() == old(self).frac(),
result.frac() == n,
Split one token into two tokens whose quantities sum to the original.
The returned token has quantity n
; the new value of the input token has
quantity old(self).frac() - n
.
Sourcepub proof fn combine(tracked &mut self, tracked other: Self)
pub proof fn combine(tracked &mut self, tracked other: Self)
requires
old(self).id() == other.id(),
ensuresself.id() == old(self).id(),
self.resource() == old(self).resource(),
self.resource() == other.resource(),
self.frac() == old(self).frac() + other.frac(),
Combine two tokens, summing their quantities.
Sourcepub proof fn bounded(tracked &self)
pub proof fn bounded(tracked &self)
ensures
0 < self.frac() <= TOTAL,
Allowed values for a token’s quantity.
Sourcepub proof fn borrow(tracked &self) -> tracked ret : &T
pub proof fn borrow(tracked &self) -> tracked ret : &T
ensures
ret == self.resource(),
Obtain shared access to the underlying resource.
Sourcepub proof fn take_resource(tracked self) -> tracked pair : (T, Empty<T, TOTAL>)
pub proof fn take_resource(tracked self) -> tracked pair : (T, Empty<T, TOTAL>)
requires
self.frac() == TOTAL,
ensurespair.0 == self.resource(),
pair.1.id() == self.id(),
Reclaim full ownership of the underlying resource.
Auto Trait Implementations§
impl<T, const TOTAL: u64> Freeze for Frac<T, TOTAL>
impl<T, const TOTAL: u64> RefUnwindSafe for Frac<T, TOTAL>where
T: RefUnwindSafe,
impl<T, const TOTAL: u64> Send for Frac<T, TOTAL>
impl<T, const TOTAL: u64> Sync for Frac<T, TOTAL>
impl<T, const TOTAL: u64> Unpin for Frac<T, TOTAL>where
T: Unpin,
impl<T, const TOTAL: u64> UnwindSafe for Frac<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