Struct vstd::storage_protocol::StorageResource
source · pub struct StorageResource<K, V, P> { /* private fields */ }Expand description
Interface for “storage protocol” ghost state.
This is an extension-slash-variant on the more well-known concept
of “PCM” ghost state, which we also have an interface for here.
The unique feature of a storage protocol is the ability to use guard
to manipulate shared references of ghost state.
Storage protocols are based on Leaf: Modularity for Temporary Sharing in Separation Logic.
The reference for the laws and operations we’re embedding here can be found at: https://github.com/secure-foundations/leaf/blob/9d72b880feb6af0a7e752b2b2a43806a0812ad56/src/guarding/protocol_relational.v
The reference version requires two monoids, the “protocol monoid” and the “base monoid”.
In this interface, we fix the base monoid to be of the form Map<K, V>.
(with composition of overlapping maps being undefined), which has all the necessary properties.
Note that there’s no create_unit (it’s not sound to do this for an arbitrary location unless you
already know a protocol was initialized at that location).
For applications, I generally advise using the
tokenized_state_machine! system,
rather than using this interface directly.
Implementations§
source§impl<K, V, P: Protocol<K, V>> StorageResource<K, V, P>
impl<K, V, P: Protocol<K, V>> StorageResource<K, V, P>
sourcepub proof fn alloc(p: P, tracked s: Map<K, V>) -> tracked out : Self
pub proof fn alloc(p: P, tracked s: Map<K, V>) -> tracked out : Self
P::rel(p, s),out.value() == p,sourcepub proof fn join(tracked a: Self, tracked b: Self) -> tracked out : Self
pub proof fn join(tracked a: Self, tracked b: Self) -> tracked out : Self
a.loc() == b.loc(),out.loc() == a.loc(),out.value() == P::op(a.value(), b.value()),sourcepub proof fn split(tracked self, a_value: P, b_value: P) -> tracked out : (Self, Self)
pub proof fn split(tracked self, a_value: P, b_value: P) -> tracked out : (Self, Self)
self.value() == P::op(a_value, b_value),out.0.loc() == self.loc(),out.1.loc() == self.loc(),out.0.value() == a_value,out.1.value() == b_value,sourcepub proof fn validate(tracked a: &Self) -> out : (P, Map<K, V>)
pub proof fn validate(tracked a: &Self) -> out : (P, Map<K, V>)
({
let (q, t) = out;
P::rel(P::op(a.value(), q), t)
}),Since inv isn’t closed under inclusion, validity for an element
is defined as the inclusion-closure of invariant, i.e., an element
is valid if there exists another element x that, added to it,
meets the invariant.
sourcepub proof fn exchange(tracked
p: Self,
tracked s: Map<K, V>,
new_p_value: P,
new_s_value: Map<K, V>
) -> tracked out : (Self, Map<K, V>)
pub proof fn exchange(tracked p: Self, tracked s: Map<K, V>, new_p_value: P, new_s_value: Map<K, V> ) -> tracked out : (Self, Map<K, V>)
exchanges(p.value(), s, new_p_value, new_s_value),({
let (new_p, new_s) = out;
new_p.loc() == p.loc() && new_p.value() == new_p_value && new_s == new_s_value
}),Most general kind of update, potentially depositing and withdrawing
sourcepub proof fn deposit(tracked self, tracked base: Map<K, V>, new_value: P) -> tracked out : Self
pub proof fn deposit(tracked self, tracked base: Map<K, V>, new_value: P) -> tracked out : Self
deposits(self.value(), base, new_value),out.loc() == self.loc(),out.value() == new_value,sourcepub proof fn withdraw(tracked self, new_value: P, new_base: Map<K, V>) -> tracked out : (Self, Map<K, V>)
pub proof fn withdraw(tracked self, new_value: P, new_base: Map<K, V>) -> tracked out : (Self, Map<K, V>)
withdraws(self.value(), new_value, new_base),out.0.loc() == self.loc(),out.0.value() == new_value,out.1 == new_base,sourcepub proof fn update(tracked self, new_value: P) -> tracked out : Self
pub proof fn update(tracked self, new_value: P) -> tracked out : Self
updates(self.value(), new_value),out.loc() == self.loc(),out.value() == new_value,“Normal” update, no depositing or withdrawing
sourcepub proof fn exchange_nondeterministic(tracked
p: Self,
tracked s: Map<K, V>,
new_values: Set<(P, Map<K, V>)>
) -> tracked out : (Self, Map<K, V>)
pub proof fn exchange_nondeterministic(tracked p: Self, tracked s: Map<K, V>, new_values: Set<(P, Map<K, V>)> ) -> tracked out : (Self, Map<K, V>)
exchanges_nondeterministic(p.value(), s, new_values),({
let (new_p, new_s) = out;
new_p.loc() == p.loc() && new_values.contains((new_p.value(), new_s))
}),sourcepub proof fn guard(tracked p: &Self, s_value: Map<K, V>) -> tracked s : &Map<K, V>
pub proof fn guard(tracked p: &Self, s_value: Map<K, V>) -> tracked s : &Map<K, V>
guards(p.value(), s_value),s == s_value,self.loc() == other.loc(),out.loc() == self.loc(),incl(self.value(), out.value()),incl(other.value(), out.value()),sourcepub proof fn weaken<'a>(tracked &'a self, target: P) -> tracked out : &'a Self
pub proof fn weaken<'a>(tracked &'a self, target: P) -> tracked out : &'a Self
incl(target, self.value()),out.loc() == self.loc(),out.value() == target,old(p).loc() == x.loc(),*p == *old(p),({
let (q, t) = res;
{ P::rel(P::op(P::op(p.value(), x.value()), q), t) }
}),p.loc() == x.loc(),exchanges(P::op(p.value(), x.value()), s, P::op(new_p_value, x.value()), new_s_value),out.0.loc() == p.loc(),out.0.value() == new_p_value,out.1 == new_s_value,p.loc() == x.loc(),exchanges_nondeterministic(P::op(p.value(), x.value()), s, set_op(new_values, x.value())),({
let (new_p, new_s) = out;
new_p.loc() == p.loc() && new_values.contains((new_p.value(), new_s))
}),Most general kind of update, potentially depositing and withdrawing