Trait vstd::tokens::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.

Object Safety§

This trait is not object safe.

Implementors§