Trait KeyValueToken 

pub trait KeyValueToken<Key, Value>: Sized {
    // Required methods
    fn instance_id(&self) -> Loc;
    fn key(&self) -> Key;
    fn value(&self) -> Value;
    fn agree(&self, other: &Self);
    fn arbitrary() -> Self;
}

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

VerusSync Strategy	Field type	Token trait
map	Map<K, V>	UniqueKeyValueToken<K, V>
imap	IMap<K, V>	UniqueKeyValueToken<K, V>
persistent_map	Map<K, V>	KeyValueToken<V> + Copy
persistent_imap	IMap<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

fn instance_id(&self) -> Loc

fn key(&self) -> Key

fn value(&self) -> Value

fn agree(&self, other: &Self)

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

fn arbitrary() -> 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".

Implementors