Skip to main content

pop_front_embedded

ostd::specs::mm::embedding::list_store

Function pop_front_embedded 

Source 
pub proof fn pop_front_embedded<M: AnyFrameMeta + Repr<MetaSlotSmall>>(tracked 
    regions: &mut MetaRegionOwners,
tracked     owner: &mut LinkedListOwner<M>,
) -> tracked frame_own : UniqueFrameOwner<Link<M>>
Expand description
requires
old(regions).inv(),
old(owner).inv(),
old(owner).relate_region(*old(regions)),
old(owner).list.len() > 0,
ensures
final(regions).inv(),
final(owner).inv(),
final(owner).relate_region(*final(regions)),
final(owner).list == old(owner).list.remove(0),
final(owner).list_id == old(owner).list_id,
frame_own.inv(),
frame_own.global_inv(*final(regions)),
frame_own.frame_link_inv(*final(regions)),
frame_own.slot_index == old(owner).slot_index_at(0),
final(regions).slot_owners[frame_own.slot_index].inner_perms.in_list.value() == 0,
final(regions).frame_obligations
    =~= old(regions).frame_obligations.insert(old(owner).slot_index_at(0)),
forall |j: usize| {
    j != old(owner).slot_index_at(0)
        && (old(owner).list.len() > 1 ==> j != old(owner).slot_index_at(1))
        ==> final(regions).slots[j] == old(regions).slots[j]
            && final(regions).slot_owners[j] == old(regions).slot_owners[j]
},
forall |l: LinkedListOwner<M>| {
    l.inv() && l.relate_region(*old(regions)) && l.list_id != final(owner).list_id
        ==> l.relate_region(*final(regions))
},
list_registry_ok(*final(regions), *final(owner)),
forall |l: LinkedListOwner<M>| {
    l.inv() && l.relate_region(*old(regions)) && list_registry_ok(*old(regions), l)
        && l.list_id != final(owner).list_id ==> list_registry_ok(*final(regions), l)
},
forall |fo: UniqueFrameOwner<Link<M>>| {
    fo.global_inv(*old(regions)) && fo.frame_link_inv(*old(regions))
        && old(regions).slot_owners[fo.slot_index].inner_perms.in_list.value() == 0
        ==> fo.global_inv(*final(regions)) && fo.frame_link_inv(*final(regions))
            && final(regions).slot_owners[fo.slot_index].inner_perms.in_list.value() == 0
            && fo.slot_index != old(owner).slot_index_at(0)
},

Trusted reflection of the (now properly &mut owner-threaded and fully verified) crate::mm::frame::LinkedList::pop_front. Pops the front link off owner, restoring it to a loose UniqueFrame<Link<M>> (its drop-obligation re-minted by from_raw, in_list reset to 0, prev/next cleared). The list shrinks by one from the front with list_id preserved.

The first block of ensures mirrors the verified exec pop_front verbatim. The last two are the sound companion facts (cf. push_front_embedded): other lists and other loose frames are untouched, and — additionally — the popped slot is distinct from every loose slot (it was a list link, in_list == list_id != 0), which keeps loose-slot disjointness when the popped frame joins loose.