Skip to main content

push_front_embedded

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

Function push_front_embedded 

Source 
pub proof fn push_front_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)),
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() > 0 ==> k != old(owner).slot_index_at(0))
        ==> 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 crate::mm::frame::LinkedList::push_front’s effect on (regions, owner, frame_own). The first block of ensures mirrors the now-verified exec push_front ensures verbatim (relate_region of the pushed owner, the list / id / in_list effects, s consumption, and the outside-the-list slot-preservation frame). The last two add facts that follow from them — sound, hence safe to assert here:

  • fresh minted id (old.list_id == 0 ==> final.list_id ∉ used_ids): the exec mints the id from a global counter, so it is fresh w.r.t. any finite in-use set; the caller passes the other lists’ ids, keeping cross-list id uniqueness.
  • other lists preserved: any well-formed list l with a different id keeps its relate_region. The only slots the surgery touches are the loose frame’s (in_list == 0, required below) and the old front’s (in_list == new id); both are disjoint from l’s slots (which carry in_list == l.list_id), so by the slot-preservation frame l is untouched.