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(),
ensuresout.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(),
ensuresout.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),
ensuresout.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),
ensuresout.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),
ensuresout.loc() == self.loc(),
new_values.contains(out.value()),
requires
self.loc() == other.loc(),
ensuresout.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),
ensuresout.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()),
ensuresout.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(),
ensures*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()),
),
ensuresout.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()),
),
ensuresout.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