Skip to main content

take_at_embedded

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

Function take_at_embedded 

Source 
pub proof fn take_at_embedded<M: AnyFrameMeta + Repr<MetaSlotSmall>>(tracked 
    regions: &mut MetaRegionOwners,
tracked     owner: &mut LinkedListOwner<M>,
    n: int,
) -> tracked frame_own : UniqueFrameOwner<Link<M>>
Expand description
requires
old(regions).inv(),
old(owner).inv(),
old(owner).relate_region(*old(regions)),
0 <= n < old(owner).list.len(),
ensures
final(regions).inv(),
final(owner).inv(),
final(owner).relate_region(*final(regions)),
final(owner).list == old(owner).list.remove(n),
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(n),
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(n)),
forall |j: usize| {
    j != old(owner).slot_index_at(n) && (n > 0 ==> j != old(owner).slot_index_at(n - 1))
        && (n < old(owner).list.len() - 1 ==> j != old(owner).slot_index_at(n + 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(n)
},

Trusted reflection of crate::mm::frame::CursorMut::take_current at an arbitrary index n over owner. The general form of pop_front_embedded (n == 0) / pop_back_embedded: removes the link at position n (0 <= n < len) back into a loose handle, touching n’s ≤2 bridged neighbours.