Trait vstd::tokens::CountToken

source · 
pub trait CountToken: Sized {
    // Required methods
    spec fn instance_id(&self) -> InstanceId;
    spec fn count(&self) -> nat;
    proof fn join(tracked &mut self, tracked other: Self);
    proof fn split(tracked &mut self, count: nat) -> tracked token : Self;
    proof fn weaken_shared(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 count strategy.

VerusSync StrategyField typeToken trait
countnatCountToken

These tokens are “fungible” in the sense that they can be combined and split, numbers combining additively.

(For the persistent_count strategy, see MonotonicCountToken.)

Required Methods§

source

spec fn instance_id(&self) -> InstanceId

source

spec fn count(&self) -> nat

source

proof fn join(tracked &mut self, tracked other: Self)

requires
old(self).instance_id() == other.instance_id(),
ensures
self.instance_id() == old(self).instance_id(),
self.count() == old(self).count() + other.count(),
source

proof fn split(tracked &mut self, count: nat) -> tracked token : Self

requires
count <= old(self).count(),
ensures
self.instance_id() == old(self).instance_id(),
self.count() == old(self).count() - count,
token.instance_id() == old(self).instance_id(),
token.count() == count,
source

proof fn weaken_shared(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.

Object Safety§

This trait is not object safe.

Implementors§