Trait vstd::tokens::MonotonicCountToken

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 Strategy	Field type	Token trait
`persistent_count`	`nat`	`MonotonicCountToken + Copy`

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

Required Methods§

spec fn instance_id(&self) -> InstanceId

spec fn count(&self) -> nat

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

requires

count <= self.count(),

ensures

s.instance_id() == self.instance_id(),

s.count() == count,

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.

Object Safety§

This trait is not object safe.

Implementors§