vstd::tokens::frac

Struct GhostVarAuth

Source
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>

Source

pub closed spec fn id(self) -> int

Source

pub closed spec fn view(self) -> T

Source

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.

Source

pub proof fn agree(tracked &self, tracked v: &GhostVar<T>)

requires
self.id() == v.id(),
ensures
self@ == v@,

Ensure that both tokens agree on the value.

Source

pub proof fn update(tracked &mut self, tracked v: &mut GhostVar<T>, new_val: T)

requires
old(self).id() == old(v).id(),
ensures
self.id() == old(self).id(),
v.id() == old(v).id(),
old(self)@ == old(v)@,
self@ == new_val,
v@ == new_val,

Update the value on each token.

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> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.