Trait vstd::tokens::UniqueValueToken

source · 
pub trait UniqueValueToken<Value>: ValueToken<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 variable or option strategies.

See the super-trait ValueToken for more information.

Required Methods§

source

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

ensures
self.instance_id() != other.instance_id(),
*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.

Object Safety§

This trait is not object safe.

Implementors§

source§

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

source§

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

source§

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

source§

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