Struct CursorMut 

pub struct CursorMut<'a, M: AnyFrameMeta + Repr<MetaSlotSmall>> {
    pub list: &'a mut LinkedList<M>,
    pub current: Option<ReprPtr<MetaSlotStorage, Link<M>>>,
}

A cursor that can mutate the linked list links.

The cursor points to either a frame or the “ghost” non-element. It points to the “ghost” non-element when the cursor surpasses the back of the list.

Fields

list: &'a mut LinkedList<M>

current: Option<ReprPtr<MetaSlotStorage, Link<M>>>

Implementations

impl<'a, M: AnyFrameMeta + Repr<MetaSlotSmall>> CursorMut<'a, M>

pub exec fn move_next(&mut self)

with

Tracked(owner): Tracked<CursorOwner<M>>,
Tracked(regions): Tracked<&MetaRegionOwners>,

requires

owner.wf_with_region(*regions),

old(self).wf_region(owner, *regions),

ensures

owner.move_next_owner_spec()@ == owner@.move_next_spec(),

owner.move_next_owner_spec().wf_with_region(*regions),

final(self).wf_region(owner.move_next_owner_spec(), *regions),

Moves the cursor to the next frame towards the back.

If the cursor is pointing to the “ghost” non-element then this will move it to the first element of the LinkedList. If it is pointing to the last element of the LinkedList then this will move it to the “ghost” non-element.

pub exec fn move_prev(&mut self)

with

Tracked(owner): Tracked<CursorOwner<M>>,
Tracked(regions): Tracked<&MetaRegionOwners>,

requires

owner.wf_with_region(*regions),

old(self).wf_region(owner, *regions),

ensures

owner.move_prev_owner_spec()@ == owner@.move_prev_spec(),

owner.move_prev_owner_spec().wf_with_region(*regions),

final(self).wf_region(owner.move_prev_owner_spec(), *regions),

Moves the cursor to the previous frame towards the front.

If the cursor is pointing to the “ghost” non-element then this will move it to the last element of the LinkedList. If it is pointing to the first element of the LinkedList then this will move it to the “ghost” non-element.

pub exec fn current_meta<'b>(&'b mut self) -> res : Option<&'b mut M>

with

Tracked(owner): Tracked<&'b mut CursorOwner<M>>,
Tracked(regions): Tracked<&'b mut MetaRegionOwners>,

requires

old(self).wf_region(*old(owner), *old(regions)),

old(owner).wf_with_region(*old(regions)),

old(regions).inv(),

ensures

final(owner).index == old(owner).index,

final(owner).list_own.list == old(owner).list_own.list,

final(owner).list_own.list_id == old(owner).list_own.list_id,

*final(self) == *old(self),

res.is_some() == (0 <= final(owner).index < final(owner).length()),

final(regions).slots.dom() == old(regions).slots.dom(),

final(regions).slot_owners.dom() == old(regions).slot_owners.dom(),

Gets the mutable reference to the current frame’s metadata.

Verified Properties

Preconditions

The cursor must be well-formed with respect to the tracked CursorOwner.

Postconditions

If the cursor is on an element, returns Some(&mut meta) borrowing the current link’s metadata. The cursor state and list shape are otherwise unchanged; the current metadata permission remains borrowed while the returned reference is live.

Safety

The &mut self guarantees exclusive access to the cursor; the tracked CursorOwner guarantees the perm for the current link is live.

pub exec fn take_current( &mut self, ) -> res : Option<(UniqueFrame<Link<M>>, Tracked<UniqueFrameOwner<Link<M>>>)>

with

Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(owner): Tracked<&mut CursorOwner<M>>,

requires

old(self).wf_region(*old(owner), *old(regions)),

old(owner).wf_with_region(*old(regions)),

old(regions).inv(),

ensures

old(owner).length() == 0 ==> res.is_none(),

old(self).current.is_some() ==> res.is_some(),

res.is_some() ==> (res->0).1@.meta_own@ == old(owner).list_own.list[old(owner).index]@,

res.is_some() ==> final(owner)@ == old(owner)@.remove(),

res.is_some() ==> (res->0).0.frame_link_inv((res->0).1@, *final(regions)),

res.is_some() ==> final(owner).wf_with_region(*final(regions)),

res.is_some() ==> final(self).wf_region(*final(owner), *final(regions)),

res.is_none() ==> *final(owner) == *old(owner),

final(regions).inv(),

res.is_some() ==> final(owner).index == old(owner).index,

res.is_some()
    ==> final(owner).list_own.list == old(owner).list_own.list.remove(old(owner).index),

final(owner).list_own.list_id == old(owner).list_own.list_id,

res.is_some()
    ==> {
        let paddr = old(self).current->0.addr();
        let idx = meta_to_index(paddr);
        &&& final(regions).slots.dom() == old(regions).slots.dom()
        &&& final(regions).ref_count(idx) == REF_COUNT_UNIQUE
        &&& final(regions).slot_owners[idx].in_list_perm.value() == 0
        &&& (res->0).0.tracked_metadata_perm@->0.storage_perm.is_init()
        &&& (res->0).0.tracked_metadata_perm@->0.vtable_ptr_perm.is_init()
        &&& final(regions).slot_owners[idx].slot_vaddr == index_to_meta(idx)
        &&& final(regions).slot_owners[idx].paths_in_pt
            == old(regions).slot_owners[idx].paths_in_pt

    },

res.is_some()
    ==> forall |j: int| {
        j != meta_to_index(old(self).current->0.addr())
            ==> {
                &&& final(regions).slot_owners[j].usage
                    == old(regions).slot_owners[j].usage
                &&& final(regions).slot_owners[j].slot_vaddr
                    == old(regions).slot_owners[j].slot_vaddr
                &&& final(regions).slot_owners[j].paths_in_pt
                    == old(regions).slot_owners[j].paths_in_pt

            }
    },

res.is_none() ==> *final(regions) == *old(regions),

res.is_some() ==> (res->0).0.inv(),

res.is_some() ==> (res->0).0.wf((res->0).1@),

res.is_some() ==> (res->0).1@.inv(),

res.is_some() ==> (res->0).0.wf_with_region((res->0).1@, *final(regions)),

res.is_some() ==> (res->0).1@.slot_index == meta_to_index(old(self).current->0.addr()),

res.is_some() ==> (res->0).0.ptr.addr() == old(self).current->0.addr(),

Takes the current pointing frame out of the linked list.

If successful, the frame is returned and the cursor is moved to the next frame. If the cursor is pointing to the back of the list then it is moved to the “ghost” non-element.

Verified Properties

Preconditions

The cursor must be well-formed, with the pointers to its links’ metadata slots matching the tracked permission objects. The list must be non-empty, so that the current frame is valid.

Postconditions

The current frame is removed from the list, and the cursor is moved to the next frame. The list invariants are preserved.

Safety

This function calls from_raw on the frame, but we guarantee that the frame is forgotten if it is in the list. So, double-free will not occur. All loads and stores are through track tracked permissions, so there are no illegal memory accesses. No data races are possible.

pub exec fn insert_before(&mut self, frame: UniqueFrame<Link<M>>)

with

Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(owner): Tracked<&mut CursorOwner<M>>,
Tracked(frame_own): Tracked<&mut UniqueFrameOwner<Link<M>>>,

requires

old(self).wf_region(*old(owner), *old(regions)),

old(owner).wf_with_region(*old(regions)),

old(regions).inv(),

frame.inv(),

old(frame_own).inv(),

frame.wf_with_region(*old(frame_own), *old(regions)),

frame.frame_link_inv(*old(frame_own), *old(regions)),

ensures

final(owner).wf_with_region(*final(regions)),

final(self).wf_region(*final(owner), *final(regions)),

final(regions).inv(),

final(owner).list_own.list
    == old(owner).list_own.list.insert(old(owner).index, final(frame_own).meta_own),

old(owner).list_own.list_id != 0
    ==> final(owner).list_own.list_id == old(owner).list_own.list_id,

final(owner).list_own.list_id != 0,

final(owner).index == old(owner).index + 1,

final(frame_own).meta_own.paddr == old(frame_own).meta_own.paddr,

final(frame_own).meta_own.in_list == final(owner).list_own.list_id,

final(owner)@ == old(owner)@.insert(final(frame_own).meta_own@),

Inserts a frame before the current frame.

If the cursor is pointing at the “ghost” non-element then the new element is inserted at the back of the LinkedList.

Verified Properties

Preconditions

The cursor must be well-formed, with the pointers to its links’ metadata slots matching the tracked permission objects.

• The new frame must be active, so that it is valid to call into_raw on it.

Postconditions

• The new frame is inserted into the list, immediately before the current index.
• The list invariants are preserved.

Safety

• This function calls into_raw on the frame, so the caller must ensure that the frame is active and has not been forgotten already to avoid a memory leak. If the caller attempts to insert a forgotten frame, the invariant around into_raw and from_raw will be violated. But, it is the safe failure case in that it will not cause a double-free. (Note: we should be able to move this requirement into the UniqueFrame invariants.)

pub exec fn as_list(&self) -> &LinkedList<M>

Provides a reference to the linked list.

impl<'a, M: AnyFrameMeta + Repr<MetaSlotSmall>> CursorMut<'a, M>

pub open spec fn wf_region(self, owner: CursorOwner<M>, regions: MetaRegionOwners) -> bool

{
    &&& 0 <= owner.index < owner.length()
        ==> self.current.is_some()
            && self.current->0.addr() == owner.list_own.list[owner.index].paddr
            && owner.list_own.meta_pptr_at(regions, owner.index).addr()
                == self.current->0.addr()
    &&& owner.index == owner.list_own.list.len() ==> self.current.is_none()
    &&& (*self.list).wf_region(owner.list_own, regions)

}

Region-based analog of CursorMut::wf: the current-link pointer facts are stated over the corresponding region-owned slot pointer.

Trait Implementations

impl<'a, M: AnyFrameMeta + Repr<MetaSlotSmall>> OwnerOf for CursorMut<'a, M>

open spec fn wf(self, owner: Self::Owner) -> bool

{
    &&& 0 <= owner.index < owner.length()
        ==> self.current.is_some()
            && self.current->0.addr() == owner.list_own.list[owner.index].paddr
    &&& owner.index == owner.list_own.list.len() ==> self.current.is_none()
    &&& (*self.list).wf(owner.list_own)

}

Structural well-formedness: current matches the link at index’s address. Pointer-permission facts (pptr/ptr equality) are stated in wf_region over the region-owned slot pointers.

type Owner = CursorOwner<M>

The owner of the concrete type. The Owner must implement Inv, indicating that it must has a consistent state.