Struct LifetimeToken 

pub struct LifetimeToken(/* private fields */);

A token signaling that the corresponding lifetime is still active.

This token is not duplicable, but it may be split into multiple other tokens. Each token has an associated fraction; if it is 1, the lifetime may be killed to end borrows made at this lifetime.

This type is purely ghost, and all operations on its values compile to no-ops.

Implementations

impl LifetimeToken

pub fn frac(self) -> PositiveReal

The fraction owned by this particular token.

If the token owns the full fraction (1), it can be used to end the lifetime.

logic

pub fn lft(self) -> Lifetime

The lifetime identifier associated with this particular token.

Only tokens with the same lifetime can be combined.

logic

pub fn new() -> Self

Get a full lifetime token for a fresh lifetime.

terminates

ghost

ensures

result.frac() == PositiveReal::from_int(1)

pub fn split(self) -> (Self, Self)

Split a lifetime token into two tokens, by dividing its fraction by 2.

terminates

ghost

ensures

result.0.lft() == self.lft() && result.1.lft() == self.lft()

ensures

result.0.frac() + result.1.frac() == self.frac()

ensures

result.0.frac() == self.frac() / PositiveReal::from_int(2)
       && result.1.frac() == self.frac() / PositiveReal::from_int(2)

pub fn split_off(&mut self) -> Self

Split a lifetime token from this token, by removing half of the token’s fraction and giving it to the result.

terminates

ghost

ensures

result.lft() == self.lft() && (^self).lft() == (*self).lft()

ensures

result.frac() + (^self).frac() == self.frac()

ensures

result.frac() == self.frac() / PositiveReal::from_int(2) && (^self).frac() == self.frac() / PositiveReal::from_int(2)

pub fn join(self, other: Self) -> Self

Combine two lifetime tokens together, adding their fractions.

terminates

ghost

requires

self.lft() == other.lft()

ensures

result.lft() == self.lft()

ensures

result.frac() == self.frac() + other.frac()

pub fn join_in(&mut self, other: Self)

Same as Self::join, but with a mutable borrow.

terminates

ghost

requires

self.lft() == other.lft()

ensures

(^self).lft() == self.lft()

ensures

(^self).frac() == self.frac() + other.frac()

pub fn end(self) -> LifetimeDead

Terminates the lifetime, giving back a ‘dead’ token.

terminates

ghost

requires

self.frac() == PositiveReal::from_int(1)

ensures

result.lft() == self.lft()

Trait Implementations

impl Default for LifetimeToken

fn default() -> Self

terminates

ghost

ensures

result.frac() == PositiveReal::from_int(1)