vstd::tokens

Trait KeyValueToken

Source 
pub trait KeyValueToken<Key, Value>: Sized {
    // Required methods
    spec fn instance_id(&self) -> InstanceId;
    spec fn key(&self) -> Key;
    spec fn value(&self) -> Value;
    proof fn agree(tracked &self, tracked other: &Self);
    proof fn arbitrary() -> tracked s : Self;
}
Expand description

Interface for VerusSync tokens created for a field marked with the map or persistent_map strategies.

VerusSync StrategyField typeToken trait
mapMap<K, V>UniqueKeyValueToken<K, V>
persistent_mapMap<K, V>KeyValueToken<V> + Copy

For the cases where the tokens are not Copy, then token is necessarily unique per-instance, per-key; the sub-trait, UniqueKeyValueToken<V>, provides an additional lemma to prove uniqueness.

Each token represents a single key-value pair. To work with a collection of KeyValueTokens, use MapToken.

Required Methods§

Source

spec fn instance_id(&self) -> InstanceId

Source

spec fn key(&self) -> Key

Source

spec fn value(&self) -> Value

Source

proof fn agree(tracked &self, tracked other: &Self)

requires
self.instance_id() == other.instance_id(),
self.key() == other.key(),
ensures
self.value() == other.value(),

All tokens, for the same instance and key, must agree on the value.

Source

proof fn arbitrary() -> tracked s : Self

Return an arbitrary token. It’s not possible to do anything interesting with this token because it doesn’t have a specified instance.

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§