pub struct Resource<P> { /* private fields */ }Expand description
Interface for ghost state that is consistent with the common presentations of partially commutative monoids (PCMs) / resource algebras.
For applications, the general advice is to use the
tokenized_state_machine! system,
which lets you focus on updates and invariants rather than composition.
However, the PCM interface you’ll find here may be more familiar to people.
Implementations§
source§impl<P: PCM> Resource<P>
impl<P: PCM> Resource<P>
sourcepub proof fn alloc(value: P) -> tracked Self
pub proof fn alloc(value: P) -> tracked Self
requires
value.valid(),out.value() == value,sourcepub proof fn join(tracked self, tracked other: Self) -> tracked Self
pub proof fn join(tracked self, tracked other: Self) -> tracked Self
requires
self.loc() == other.loc(),out.loc() == self.loc(),out.value() == P::op(self.value(), other.value()),sourcepub proof fn split(tracked self, left: P, right: P) -> (Self, Self)
pub proof fn split(tracked self, left: P, right: P) -> (Self, Self)
requires
self.value() == P::op(left, right),out.0.loc() == self.loc(),out.1.loc() == self.loc(),out.0.value() == left,out.1.value() == right,sourcepub proof fn create_unit(loc: Loc) -> tracked Self
pub proof fn create_unit(loc: Loc) -> tracked Self
ensures
out.value() == P::unit(),out.loc() == loc,sourcepub proof fn update(tracked self, new_value: P) -> tracked Self
pub proof fn update(tracked self, new_value: P) -> tracked Self
requires
frame_preserving_update(self.value(), new_value),out.loc() == self.loc(),out.value() == new_value,sourcepub proof fn update_nondeterministic(tracked self, new_values: Set<P>) -> tracked Self
pub proof fn update_nondeterministic(tracked self, new_values: Set<P>) -> tracked Self
requires
frame_preserving_update_nondeterministic(self.value(), new_values),out.loc() == self.loc(),new_values.contains(out.value()),requires
self.loc() == other.loc(),out.loc() == self.loc(),incl(self.value(), out.value()),incl(other.value(), out.value()),requires
self.loc() == other.loc(),conjunct_shared(self.value(), other.value(), target),out.loc() == self.loc(),out.value() == target,sourcepub proof fn weaken<'a>(tracked &'a self, target: P) -> &'a Self
pub proof fn weaken<'a>(tracked &'a self, target: P) -> &'a Self
requires
incl(target, self.value()),out.loc() == self.loc(),out.value() == target,sourcepub proof fn validate_2(tracked &mut self, tracked other: &Self)
pub proof fn validate_2(tracked &mut self, tracked other: &Self)
requires
old(self).loc() == other.loc(),*self == *old(self),P::op(self.value(), other.value()).valid(),requires
self.loc() == other.loc(),frame_preserving_update(
P::op(self.value(), other.value()),
P::op(new_value, other.value()),
),out.loc() == self.loc(),out.value() == new_value,requires
self.loc() == other.loc(),frame_preserving_update_nondeterministic(
P::op(self.value(), other.value()),
set_op(new_values, other.value()),
),out.loc() == self.loc(),new_values.contains(out.value()),Auto Trait Implementations§
impl<P> RefUnwindSafe for Resource<P>where
P: RefUnwindSafe,
impl<P> Send for Resource<P>where
P: Send,
impl<P> Sync for Resource<P>where
P: Sync,
impl<P> Unpin for Resource<P>where
P: Unpin,
impl<P> UnwindSafe for Resource<P>where
P: UnwindSafe,
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more