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 IMap<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.