pub struct FracGhost<T, const TOTAL: u64 = 2> { /* private fields */ }Expand description
An implementation of a resource for fractional ownership of a ghost variable.
While most presentations of fractional permissions use the fractional total of 1,
with fractions being arbitrary rational numbers, this library represents fractional
permissions as integers, totalling to some compile-time constant TOTAL.
Thus, you can have any fractions from 1 up to TOTAL, and if you
have TOTAL, you can update the ghost variable.
If you just want to split the permission in half, you can also use the
GhostVar<T> and GhostVarAuth<T> library.
§Example
fn example_use() {
let tracked mut r = FracGhost::<u64, 3>::new(123);
assert(r@ == 123);
assert(r.frac() == 3);
let tracked r2 = r.split(2);
assert(r@ == 123);
assert(r2@ == 123);
assert(r.frac() == 1);
assert(r2.frac() == 2);
proof {
r.combine(r2);
r.update(456);
}
assert(r@ == 456);
assert(r.frac() == 3);
let tracked mut a = FracGhost::<u32>::new(5);
assert(a@ == 5);
assert(a.frac() == 2);
let tracked mut b = a.split(1);
assert(a.frac() == 1);
assert(b.frac() == 1);
proof {
a.update_with(&mut b, 123);
}
assert(a@ == 123);
proof {
a.combine(b);
a.update(6);
}
assert(a@ == 6);
}Implementations§
source§impl<T, const TOTAL: u64> FracGhost<T, TOTAL>
impl<T, const TOTAL: u64> FracGhost<T, TOTAL>
sourcepub closed spec fn frac(self) -> int
pub closed spec fn frac(self) -> int
The fractional quantity of this permission. The “fraction” is represented as an integer,
out of 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(v: T) -> tracked result : Self
pub proof fn new(v: T) -> tracked result : Self
TOTAL > 0,result.frac() == TOTAL as int,result@ == v,Allocate a new token with the given value. The returned token represents
the TOTAL quantity.
sourcepub proof fn agree(tracked &self, tracked other: &Self)
pub proof fn agree(tracked &self, tracked other: &Self)
self.id() == other.id(),self@ == other@,Two tokens agree on their values.
sourcepub proof fn take(tracked &mut self) -> tracked result : Self
pub proof fn take(tracked &mut self) -> tracked result : Self
result == *old(self),Take a token out of a mutable reference, leaving a meaningless token behind.
sourcepub proof fn split(tracked &mut self, n: int) -> tracked result : Self
pub proof fn split(tracked &mut self, n: int) -> tracked result : Self
0 < n < old(self).frac(),result.id() == self.id() == old(self).id(),self@ == old(self)@,result@ == old(self)@,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)
old(self).id() == other.id(),self.id() == old(self).id(),self@ == old(self)@,self@ == other@,self.frac() == old(self).frac() + other.frac(),Combine two tokens, summing their quantities.
sourcepub proof fn update(tracked &mut self, v: T)
pub proof fn update(tracked &mut self, v: T)
old(self).frac() == TOTAL,self.id() == old(self).id(),self@ == v,self.frac() == old(self).frac(),Update the value of the token. This requires having ALL the permissions,
i.e., a quantity total of TOTAL.
sourcepub proof fn update_with(tracked &mut self, tracked other: &mut Self, v: T)
pub proof fn update_with(tracked &mut self, tracked other: &mut Self, v: T)
old(self).id() == old(other).id(),old(self).frac() + old(other).frac() == TOTAL,self.id() == old(self).id(),other.id() == old(other).id(),self.frac() == old(self).frac(),other.frac() == old(other).frac(),old(self)@ == old(other)@,self@ == v,other@ == v,Update the value of the token. This requires having ALL the permissions,
i.e., the tokens together must have a quantity total of TOTAL.