Struct Budget 

pub struct Budget {
    pub capacity: u64,
    pub allocated: u64,
    pub reserved: u64,
    pub pending_eviction: u64,
}

A budget: a capacity ceiling against three claimants — allocated (committed), reserved (held but not committed), and pending_eviction (being reclaimed).

Fields

capacity: u64

Fixed capacity ceiling.

allocated: u64

Capacity committed to live allocation.

reserved: u64

Capacity held for later commitment.

pending_eviction: u64

Allocated capacity marked for eviction completion.

Implementations

impl Budget

pub fn new(capacity: u64) -> Budget

Construct an empty budget with the given capacity. Realises Init.

pub fn available(&self) -> u64

Headroom = capacity - used, computed overflow-safely (used <= capacity by the invariant, so the subtraction never underflows). Exposed for callers and the try-operations.

pub fn try_allocate(&mut self, amount: u64) -> bool

Try to commit amount: succeeds iff it fits under the ceiling. The returned bool is exactly the TLA+ IF condition allocated + reserved + pending_eviction + amount <= capacity.

pub fn reserve(&mut self, amount: u64) -> bool

Try to reserve amount (held, not yet committed). Same ceiling test as TryAllocate; on success grows reserved.

pub fn commit_reservation(&mut self, amount: u64)

Commit amount of the reservation: moves it from reserved to allocated. Enabling condition: amount <= reserved. The total used is unchanged, so SafetyInvariant is trivially preserved.

pub fn release(&mut self, amount: u64)

Release amount of committed allocation. Enabling condition: amount <= allocated. Decreases used, so SafetyInvariant is preserved.

pub fn mark_eviction(&mut self, amount: u64)

Mark amount of committed allocation for eviction: moves it from allocated to pending_eviction. Enabling condition: amount <= allocated. used is unchanged, so SafetyInvariant is preserved.

pub fn complete_eviction(&mut self, amount: u64)

Complete eviction of amount: removes it from pending_eviction. Enabling condition: amount <= pending_eviction. Decreases used, so SafetyInvariant is preserved.

Trait Implementations

impl Clone for Budget

fn clone(&self) -> Budget

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Copy for Budget