pub struct GhostVarAuth<T> { /* private fields */ }
Expand description
GhostVarAuth<T>
is one half of a pair of tokens—the other being GhostVar<T>
.
These tokens each track a value, and they can only be allocated or updated together.
Thus, the pair of tokens always agree on the value, but they can be owned separately.
One possible application is to have a library which
keeps GhostVarAuth<T>
and maintains an invariant relating the implementation’s
abstract state to the value of GhostVarAuth<T>
. Both GhostVarAuth<T>
and GhostVar<T>
are needed together to update the value, but either one alone
allows reasoning about the current state.
These tokens can be implemented using fractional permissions, e.g., FracGhost
.
§Example
fn example() {
let tracked (mut gauth, mut gvar) = GhostVarAuth::<u64>::new(1);
assert(gauth@ == 1);
assert(gvar@ == 1);
proof {
gauth.update(&mut gvar, 2);
}
assert(gauth@ == 2);
assert(gvar@ == 2);
}
Implementations§
Source§impl<T> GhostVarAuth<T>
impl<T> GhostVarAuth<T>
Sourcepub proof fn new(v: T) -> tracked result : (GhostVarAuth<T>, GhostVar<T>)
pub proof fn new(v: T) -> tracked result : (GhostVarAuth<T>, GhostVar<T>)
ensures
result.0.id() == result.1.id(),
result.0@ == v,
result.1@ == v,
Allocate a new pair of tokens, each initialized to the given value.
Auto Trait Implementations§
impl<T> Freeze for GhostVarAuth<T>
impl<T> RefUnwindSafe for GhostVarAuth<T>where
T: RefUnwindSafe,
impl<T> Send for GhostVarAuth<T>where
T: Send,
impl<T> Sync for GhostVarAuth<T>where
T: Sync,
impl<T> Unpin for GhostVarAuth<T>where
T: Unpin,
impl<T> UnwindSafe for GhostVarAuth<T>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