Skip to main content

seg_obligations_minted

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

Function seg_obligations_minted 

Source 
pub open spec fn seg_obligations_minted(
    pre: MetaRegionOwners,
    post: MetaRegionOwners,
    range_start: usize,
    n: int,
) -> bool
Expand description
{
    &&& forall |i: int| {
        0 <= i < n
            ==> post
                .frame_obligations
                .count(frame_to_index((range_start + i * PAGE_SIZE) as usize))
                >= pre
                    .frame_obligations
                    .count(frame_to_index((range_start + i * PAGE_SIZE) as usize)) + 1
    }
    &&& forall |jdx: usize| {
        (forall |i: int| {
            0 <= i < n ==> jdx != frame_to_index((range_start + i * PAGE_SIZE) as usize)
        }) ==> post.frame_obligations.count(jdx) == pre.frame_obligations.count(jdx)
    }

}

The exact frame_obligations effect of recording one forgotten reference per frame for the first n frames of a segment starting at range_start:

  • every segment frame’s count grows by at least one (its recorded reference), and
  • the frame condition: every slot that is NOT a segment frame is left untouched.

The frame condition is the load-bearing part — it pins the support of the change to the segment’s slots, so a caller’s ledger accounting telescopes (it can conclude this only touched the segment’s slots). Shared by tracked_mint_seg_obligations (which establishes it) and Segment::from_unused (which advertises it).