Struct Fragment 

pub struct Fragment<R: UnitRA>(pub Resource<Auth<R>>);

Wrapper around a Resource, that contains a fragment.

See Authority.

Tuple Fields

0: Resource<Auth<R>>

Implementations

impl<R: UnitRA> Fragment<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 new_unit(id: Id) -> Fragment<R>

Create a fragment containing a unit resource

terminates

ghost

ensures

result@ == R::unit() && result.id() == id

pub fn core(&self) -> Self

Duplicate the duplicable core of a fragment

terminates

ghost

requires

self@.core() != None

ensures

result.id() == self.id()

ensures

Some(result@) == self@.core()

pub fn split(self, a: Snapshot<R>, b: Snapshot<R>) -> (Self, Self)

Split a fragment into two parts, described by a and b.

See also [Self::split_mut] and Self::split_off.

terminates

ghost

requires

R::incl_eq_op(*a, *b, self@)

ensures

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

ensures

result.0@ == *a

ensures

result.1@ == *b

pub fn split_off(&mut self, r: Snapshot<R>, s: Snapshot<R>) -> Self

Remove r from self and return it, leaving s in self.

terminates

ghost

requires

R::incl_eq_op(*r, *s, self@)

ensures

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

ensures

(^self)@ == *s

ensures

result@ == *r

pub fn join(self, other: Self) -> Self

Join two owned framents together.

See also Self::join_in and [Self::join_shared].

terminates

ghost

requires

self.id() == other.id()

ensures

result.id() == self.id()

ensures

Some(result@) == self@.op(other@)

pub fn join_in(&mut self, other: Self)

Same as Self::join, but put the result into self.

terminates

ghost

requires

self.id() == other.id()

ensures

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

ensures

Some((^self)@) == self@.op(other@)

pub fn weaken(&mut self, target: Snapshot<R>)

Transforms self into target, given that target is included in self.

terminates

ghost

requires

target.incl(self@)

ensures

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

ensures

(^self)@ == *target

pub fn valid_op_lemma(&mut self, other: &Self)

Validate the composition of self and other.

terminates

ghost

requires

self.id() == other.id()

ensures

^self == *self

ensures

self@.op(other@) != None

Trait Implementations

impl<R: UnitRA> From<Resource<View<AuthViewRel<R>>>> for Fragment<R>

fn from(value: Resource<Auth<R>>) -> Self

terminates

ghost

ensures

result@ == value@.frag()

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

fn view(self) -> R

Get the fragment value.

(open)

pearlite! { self.0@.frag() }

type ViewTy = R