Skip to main content

tracked_redeem_seg_obligations

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

Function tracked_redeem_seg_obligations 

Source 
pub proof fn tracked_redeem_seg_obligations(tracked 
    regions: &mut MetaRegionOwners,
    range_start: usize,
    n: int,
)
Expand description
requires
0 <= n,
old(regions).inv(),
forall |i: int| {
    0 <= i < n
        ==> old(regions)
            .frame_obligations
            .count(frame_to_index((range_start + i * PAGE_SIZE) as usize)) >= 1
},
forall |i: int, j: int| {
    0 <= i < j < n
        ==> frame_to_index((range_start + i * PAGE_SIZE) as usize)
            != frame_to_index((range_start + j * PAGE_SIZE) as usize)
},
ensures
final(regions).inv(),
final(regions).slots =~= old(regions).slots,
final(regions).slot_owners =~= old(regions).slot_owners,

Redeems the per-frame frame_obligations entry for each of the first n frames of a segment starting at range_start — the inverse of tracked_mint_seg_obligations. Used by Segment::drop to drain the segment’s retained per-frame references before the per-frame teardown loop, so that loop sees count == 0 (as it did before the migration) and its from_raw(+1)/frame.drop(-1) pair nets to zero unchanged.

Unlike minting, redeeming requires the frame indices be distinct (redeeming one frame must not drop another’s count below 1) and each count be >= 1 up front — both supplied by SegmentOwner::relate_regions. Leaves slots, slot_owners, and the (vestigial) range obligations ledger untouched.