Trait UniqueValueToken 

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

Interface for VerusSync tokens created for a field marked with the variable or option strategies.

See the super-trait ValueToken for more information.

Required Methods

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

ensures

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

*final(self) == *old(self),

The token for a given instance must be unique; in other words, if we have two tokens, they must be for distinct instances. 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

impl<K, V, Pred: InvariantPredicate<K, V>> UniqueValueToken<()> for pending_writer<K, V, Pred>

impl<K, V, Pred: InvariantPredicate<K, V>> UniqueValueToken<()> for writer<K, V, Pred>

impl<K, V, Pred: InvariantPredicate<K, V>> UniqueValueToken<bool> for flag_exc<K, V, Pred>

impl<K, V, Pred: InvariantPredicate<K, V>> UniqueValueToken<nat> for flag_rc<K, V, Pred>