Trait vstd::tokens::ValueToken

source · 
pub trait ValueToken<Value>: Sized {
    // Required methods
    spec fn instance_id(&self) -> InstanceId;
    spec fn value(&self) -> Value;
    proof fn agree(tracked &self, tracked other: &Self);
    proof fn arbitrary() -> tracked s : Self;
}
Expand description

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

VerusSync StrategyField typeToken trait
variableVUniqueValueToken<V>
optionOption<V>UniqueValueToken<V>
persistent_optionOption<V>ValueToken<V> + Copy

For the cases where the tokens are not Copy, then token is necessarily unique per-instance; the sub-trait, UniqueValueToken<V>, provides an additional lemma to prove uniqueness.

Required Methods§

source

spec fn instance_id(&self) -> InstanceId

source

spec fn value(&self) -> Value

source

proof fn agree(tracked &self, tracked other: &Self)

requires
self.instance_id() == other.instance_id(),
ensures
self.value() == other.value(),

All tokens (for the same instance) must agree on the value.

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>> ValueToken<bool> for flag_exc<K, V, Pred>

source§

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

source§

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

source§

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