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 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§
Sourcespec fn instance_id(&self) -> InstanceId
spec fn instance_id(&self) -> InstanceId
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.