Trait ValueToken 

pub trait ValueToken<Value>: Sized {
    // Required methods
    fn instance_id(&self) -> Loc;
    fn value(&self) -> Value;
    fn agree(&self, other: &Self);
    fn arbitrary() -> 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

fn instance_id(&self) -> Loc

fn value(&self) -> Value

fn agree(&self, other: &Self)

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

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

where Pred: InvariantPredicate<K, V>,

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

where Pred: InvariantPredicate<K, V>,

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

where Pred: InvariantPredicate<K, V>,

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

where Pred: InvariantPredicate<K, V>,