vstd

Module storage_protocol

Source

Structs§

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

Traits§

Protocol
See StorageResource for more information.

Functions§

deposits
exchanges
exchanges_nondeterministic
guards
incl
set_op
updates
withdraws