Struct GhostVarAuth Copy item path

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);
}