Skip to main content

push_back_embedded

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

Function push_back_embedded 

Source 
pub proof fn push_back_embedded<M: AnyFrameMeta + Repr<MetaSlotSmall>>(tracked 
    regions: &mut MetaRegionOwners,
tracked     owner: &mut LinkedListOwner<M>,
tracked     frame_own: &mut UniqueFrameOwner<Link<M>>,
    used_ids: Set<u64>,
)
Expand description
requires
old(regions).inv(),
old(owner).inv(),
old(owner).relate_region(*old(regions)),
old(frame_own).inv(),
old(frame_own).global_inv(*old(regions)),
old(frame_own).frame_link_inv(*old(regions)),
old(regions).slot_owners[old(frame_own).slot_index].inner_perms.in_list.value() == 0,
ensures
final(regions).inv(),
final(owner).inv(),
final(owner).relate_region(*final(regions)),
old(owner).list.len() > 0
    ==> final(owner).list
        == old(owner).list.insert(old(owner).list.len() - 1, final(frame_own).meta_own),
old(owner).list.len() == 0
    ==> final(owner).list == old(owner).list.insert(0, final(frame_own).meta_own),
old(owner).list_id != 0 ==> final(owner).list_id == old(owner).list_id,
final(owner).list_id != 0,
old(owner).list_id == 0 ==> !used_ids.contains(final(owner).list_id),
final(frame_own).meta_own.paddr == old(frame_own).meta_own.paddr,
final(frame_own).meta_own.in_list == final(owner).list_id,
final(regions).frame_obligations
    =~= old(regions).frame_obligations.remove(old(frame_own).slot_index),
forall |k: usize| {
    k != old(frame_own).slot_index
        && (old(owner).list.len() > 1
            ==> k != old(owner).slot_index_at(old(owner).list.len() - 2))
        && (old(owner).list.len() > 0
            ==> k != old(owner).slot_index_at(old(owner).list.len() - 1))
        ==> final(regions).slots[k] == old(regions).slots[k]
            && final(regions).slot_owners[k] == old(regions).slot_owners[k]
},
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.slot_index != old(frame_own).slot_index
        ==> fo.global_inv(*final(regions)) && fo.frame_link_inv(*final(regions))
            && final(regions).slot_owners[fo.slot_index].inner_perms.in_list.value() == 0
},

Trusted reflection of the (verified) crate::mm::frame::LinkedList::push_back. Identical to push_front_embedded except the frame is spliced in at the tail (touching the back neighbours instead of the front).