Trait ValueToken 

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;
}

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

VerusSync Strategy	Field type	Token trait
variable	V	UniqueValueToken<V>
option	Option<V>	UniqueValueToken<V>
persistent_option	Option<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

spec fn instance_id(&self) -> InstanceId

spec fn value(&self) -> Value

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.

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.

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>> ValueToken<()> for pending_writer<K, V, Pred>

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

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

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