Trait vstd::tokens::ElementToken

source · 
pub trait ElementToken<Element>: Sized {
    // Required methods
    spec fn instance_id(&self) -> InstanceId;
    spec fn element(&self) -> Element;
    proof fn arbitrary() -> tracked s : Self;
}
Expand description

Interface for VerusSync tokens created for a field marked with the set, persistent_set or multiset strategies.

VerusSync StrategyField typeToken trait
setSet<V>UniqueElementToken<V>
persistent_setSet<V>ElementToken<V> + Copy
multisetMultiset<V>ElementToken<V>

Each token represents a single element of the set or multiset.

  • For the set strategy, the token for any given element is unique.
  • For the persistent_set strategy, the token for any given element is not unique, but is Copy.
  • For the multiset strategy, the tokens are neither unique nor Copy, as the specific multiplicity of each element must be exact.

To work with a collection of ElementTokens, use SetToken or MultisetToken.

Required Methods§

source

spec fn instance_id(&self) -> InstanceId

source

spec fn element(&self) -> Element

source

proof fn arbitrary() -> tracked s : Self

Return an arbitrary token. It’s not possible to do anything interesting with this token because it doesn’t have a specified instance.

Object Safety§

This trait is not object safe.

Implementors§

source§

impl<K, V, Pred: InvariantPredicate<K, V>> ElementToken<()> for pending_reader<K, V, Pred>

source§

impl<K, V, Pred: InvariantPredicate<K, V>> ElementToken<V> for reader<K, V, Pred>