Struct Count 

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

Implementations

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

pub closed spec fn id(self) -> Loc

Returns the unique identifier.

pub closed spec fn resource(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 unique authority for taking/updating the resource.

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

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

}

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

requires

TOTAL > 0,

ensures

result.frac() == TOTAL,

result.resource() == v,

result.has_authority(),

Allocates a new Count with the full fraction and the given resource value.

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

requires

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

ensures

self.resource() == other.resource(),

Two Counts 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).resource() == old(self).resource(),

result.resource() == old(self).resource(),

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

result.frac() == n,

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

!result.has_authority(),

Splits another fraction n from this Count, returning a new Count 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).resource() == old(self).resource(),

final(self).resource() == other.resource(),

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

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

Combines another Count into this one, consuming the other Count.

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 tracked_borrow(tracked &self) -> tracked ret : &T

returns

self.resource(),

Borrows the resource value.

pub proof fn take_resource(tracked self) -> tracked (T, EmptyCount<T, TOTAL>)

requires

self.frac() == TOTAL,

self.has_authority(),

ensures

resource == self.resource(),

empty.id() == self.id(),

Consumes the Count and returns the resource value and an EmptyCount with the same id.

pub proof fn into_resource(tracked self) -> tracked res : T

requires

self.frac() == TOTAL,

self.has_authority(),

returns

self.resource(),

Consumes the Count and returns the resource value, the id is lost because the EmptyCount is not returned.