Struct CountGhost 

pub struct CountGhost<T, const TOTAL: usize = 2> { /* private fields */ }

Implementations

impl<T, const TOTAL: usize> CountGhost<T, TOTAL>

pub closed spec fn id(self) -> Loc

Returns the unique identifier.

pub closed spec fn view(self) -> T

Returns the stored resource value.

pub closed spec fn frac(self) -> int

Returns the fraction of the resource.

pub closed spec fn has_authority(self) -> bool

Whether this token carries the authority for updating the resource value.

pub open spec fn valid(self, id: Loc, frac: int) -> bool

{
    &&& self.id() == id
    &&& self.frac() == frac

}

pub proof fn alloc(v: T) -> tracked result : Self

requires

TOTAL > 0,

ensures

result.frac() == TOTAL,

result@ == v,

result.has_authority(),

Allocates a new CountGhost with the full fraction, the given value, and the authority.

pub proof fn agree(tracked &self, tracked other: &Self)

requires

self.id() == other.id(),

ensures

self@ == other@,

Two CountGhosts with the same id must have the same resource value.

pub proof fn split(tracked &mut self, n: int) -> tracked result : Self

requires

0 < n < old(self).frac(),

ensures

result.id() == final(self).id(),

final(self).id() == old(self).id(),

final(self)@ == old(self)@,

result@ == old(self)@,

final(self).frac() + result.frac() == old(self).frac(),

result.frac() == n,

!result.has_authority(),

final(self).has_authority() == old(self).has_authority(),

Splits another fraction n from this CountGhost, returning a new CountGhost with that fraction.

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

requires

old(self).id() == other.id(),

ensures

final(self).id() == old(self).id(),

final(self)@ == old(self)@,

final(self)@ == other@,

final(self).frac() == old(self).frac() + other.frac(),

final(self).has_authority() == (old(self).has_authority() || other.has_authority()),

Combines a CountGhost.

pub proof fn update(tracked &mut self, v: T)

requires

old(self).has_authority(),

old(self).frac() == TOTAL,

ensures

final(self).id() == old(self).id(),

final(self)@ == v,

final(self).frac() == old(self).frac(),

final(self).has_authority(),

Updates the value stored in this CountGhost. The token must be the authority and hold the full fraction.

pub proof fn update_with(tracked &mut self, tracked other: &mut Self, v: T)

requires

old(self).id() == old(other).id(),

old(self).frac() + old(other).frac() == TOTAL,

old(self).has_authority() || old(other).has_authority(),

ensures

final(self).id() == old(self).id(),

final(other).id() == old(other).id(),

final(self).frac() == old(self).frac(),

final(other).frac() == old(other).frac(),

old(self)@ == old(other)@,

final(self)@ == v,

final(other)@ == v,

Updates the value stored in both CountGhosts.

pub proof fn bounded(tracked &self)

ensures

0 < self.frac() <= TOTAL,

The fraction of the resource must be positive and at most TOTAL.

pub proof fn dummy() -> tracked result : Self

requires

TOTAL > 0,