vstd::tokens

Trait MonotonicCountToken

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

Interface for VerusSync tokens created for a field marked with the persistent_count strategy.

VerusSync StrategyField typeToken trait
persistent_countnatMonotonicCountToken + Copy

A token represents a “lower bound” on the field value, which increases monotonically.

Required Methods§

Source

spec fn instance_id(&self) -> InstanceId

Source

spec fn count(&self) -> nat

Source

proof fn weaken(tracked &self, count: nat) -> tracked s : Self

requires
count <= self.count(),
ensures
s.instance_id() == self.instance_id(),
s.count() == count,
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§