vstd::tokens

Trait SimpleToken

Source 
pub trait SimpleToken: Sized {
    // Required methods
    spec fn instance_id(&self) -> InstanceId;
    proof fn arbitrary() -> tracked s : Self;
}
Expand description

Interface for VerusSync tokens created for a field marked with the bool or persistent_bool strategy.

VerusSync StrategyField typeToken trait
boolboolUniqueSimpleToken<V>
persistent_boolboolSimpleToken<V> + Copy

The token contains no additional data; its presence indicates that the boolean field is true.

Required Methods§

Source

spec fn instance_id(&self) -> InstanceId

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.

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§