Struct Authority 

pub struct Authority<R: UnitRA>(/* private fields */);

Wrapper around a Resource, that contains an authoritative value.

This type is a specialization of Resource for the common case where you want an authoritative resource. Authority and Fragment respectively contain the authoritative part and the fragment part of the ressource, and come with handy ghost functions to use them (provers have some trouble authomatically deriving when the context is full of other hypotheses).

Implementations

impl<R: UnitRA> Authority<R>

pub fn id(self) -> Id

Id of the underlying Resource.

pub fn id_ghost(&self) -> Id

Get the id for this resource.

This is the same as Self::id, but for ghost code.

terminates

ghost

ensures

result == self.id()

pub fn alloc() -> Ghost<Self>

Create a new, empty authority.

terminates

ghost

ensures

result@ == R::unit()

pub fn from_resource(r: Resource<Auth<R>>) -> Self

Create a new, empty authority.

terminates

ghost

requires

r@.auth() != None

ensures

result@ == r@.auth().unwrap_logic()

ensures

result.id() == r.id()

pub fn update<U: LocalUpdate<R>>(&mut self, frag: &mut Fragment<R>, upd: U)

Perform a local update on an authority, fragment pair

terminates

ghost

requires

self.id() == frag.id()

requires

upd.premise(self@, frag@)

ensures

self.id() == (^self).id()

ensures

frag.id() == (^frag).id()

ensures

frag@.incl(self@)

ensures

((^self)@, (^frag)@) == upd.update(self@, frag@)

pub fn frag_lemma(&self, frag: &Fragment<R>)

Asserts that the fragment represented by frag is contained in self.

terminates

ghost

requires

self.id() == frag.id()

ensures

frag@.incl(self@)

Trait Implementations

impl<R: UnitRA> Invariant for Authority<R>

fn invariant(self) -> bool

impl<R: UnitRA> View for Authority<R>

fn view(self) -> R

Get the authoritative value.

type ViewTy = R