Skip to main content

pop_back_embedded

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

Function pop_back_embedded 

Source 
pub proof fn pop_back_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(old(owner).list.len() - 1),
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(old(owner).list.len() - 1),
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(old(owner).list.len() - 1)),
forall |j: usize| {
    j != old(owner).slot_index_at(old(owner).list.len() - 1)
        && (old(owner).list.len() > 1
            ==> j != old(owner).slot_index_at(old(owner).list.len() - 2))
        ==> 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(old(owner).list.len() - 1)
},

Trusted reflection of the (verified) crate::mm::frame::LinkedList::pop_back. Identical to pop_front_embedded except the last link is popped (touching the back neighbour at slot_index_at(len - 2)).