vstd::tokens

Trait UniqueKeyValueToken

Source 
pub trait UniqueKeyValueToken<Key, Value>: KeyValueToken<Key, Value> {
    // Required method
    proof fn unique(tracked &mut self, tracked other: &Self);
}
Expand description

Interface for VerusSync tokens created for a field marked with the map strategy.

See the super-trait KeyValueToken for more information.

Required Methods§

Source

proof fn unique(tracked &mut self, tracked other: &Self)

ensures
self.instance_id() != other.instance_id() || self.key() != other.key(),
*self == *old(self),

The token for a given instance and key must be unique; in other words, if we have two tokens, they must be for distinct instances or keys. Though the first argument is mutable, the value is not really mutated; this is only used to ensure unique ownership of the argument.

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§