Function lemma_frame_drop_pre_derivable

pub proof fn lemma_frame_drop_pre_derivable<'rcu>(s: VmStore<'rcu>, fid: FrameId)

Expand description

requires

s.inv(),

s.frames.contains_key(fid),

segment_cover_count(s.segments, s.frames[fid].paddr) == 0,

ensures

frame::drop_pre(s.regions, s.frames[fid].paddr),

s.regions.slot_owner(s.frames[fid].paddr).ref_count() == 1
    ==> handle_count(s.frames, frame_to_index(s.frames[fid].paddr)) == 1,

lemma_frame_drop_pre_derivable