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.

logic

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, Fragment<R>)

Create a new authority/fragment pair from a raw Auth resource.

terminates

ghost

requires

r@.auth() != None

ensures

result.0.id() == r.id() && result.1.id() == r.id()

ensures

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

ensures

result.1@ == r@.frag()

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 add_fragment(&mut self, frag: Snapshot<R>) -> Fragment<R>

Add a piece to the authority, and return a new fragment corresponding to this piece.

This is a specialization of Self::update with OpLocalUpdate.

terminates

ghost

requires

self@.op(*frag) != None

ensures

(^self)@ == self@.op(*frag).unwrap_logic()

ensures

result@ == *frag

ensures

result.id() == self.id() && (^self).id() == self.id()

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

logic

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

fn view(self) -> R

Get the authoritative value.

logic

type ViewTy = R