Trait UniqueKeyValueToken 

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

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

See the super-trait KeyValueToken for more information.

Required Methods

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

ensures

final(self).instance_id() != other.instance_id() || final(self).key() != other.key(),

*final(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".

Implementors