Skip to main content

tracked_mint_seg_obligations

ostd::specs::mm::frame::segment

Function tracked_mint_seg_obligations 

Source 
pub proof fn tracked_mint_seg_obligations(tracked 
    regions: &mut MetaRegionOwners,
    range_start: usize,
    n: int,
)
Expand description
requires
0 <= n,
old(regions).inv(),
ensures
final(regions).inv(),
final(regions).slots =~= old(regions).slots,
final(regions).slot_owners =~= old(regions).slot_owners,
forall |idx: usize| (
    final(regions).frame_obligations.count(idx)
        >= old(regions).frame_obligations.count(idx)
),
seg_obligations_minted(*old(regions), *final(regions), range_start, n),

Mints one per-frame frame_obligations entry for each of the first n frames of a segment starting at range_start. Used by Segment::from_unused to record the segment’s forgotten per-frame references after the construction loop (which is net-zero on the ledger: each frame’s Frame::from_unused mint is cancelled by its ManuallyDrop).

Per-frame obligations replace the old single range-keyed obligations ledger entry. Because frame_obligations is a multiset and minting only ever increases counts, no distinctness hypothesis on the frame indices is needed.

EXACT accounting (Tier A): the ensures pin the support of the change — every segment frame’s count grows by at least one, and every other slot is untouched. This frame condition is what lets a caller’s accounting telescope (it can conclude this call touched only the segment’s slots). Each mint targets a segment index, so a non-segment slot is simply never a mint target — hence the frame condition needs no injectivity argument.