ostd/mm/frame/

linked_list.rs

// SPDX-License-Identifier: MPL-2.0
//! Enabling linked lists of frames without heap allocation.
//!
//! This module leverages the customizability of the metadata system (see
//! [super::meta]) to allow any type of frame to be used in a linked list.
use vstd::prelude::*;

use vstd::seq_lib::*;
use vstd::simple_pptr::*;

use vstd_extra::cast_ptr::*;
use vstd_extra::drop_tracking::{Drop, DropObligation, TrackDrop};
use vstd_extra::ownership::*;

use crate::mm::frame::meta::{
    META_SLOT_SIZE, REF_COUNT_UNIQUE,
    mapping::{frame_to_meta, meta_to_frame},
};
use crate::mm::kspace::FRAME_METADATA_RANGE;
use crate::specs::arch::*;
use crate::specs::mm::frame::{
    linked_list::linked_list_owners::*,
    mapping::{frame_to_index, group_page_meta, index_to_meta, meta_to_index},
    meta_owners::{
        MetaSlotOwner, MetaSlotStorage, borrow_meta, borrow_meta_mut, typed_meta_value,
        typed_meta_wf,
    },
    meta_region_owners::MetaRegionOwners,
    unique::UniqueFrameOwner,
};

use super::{
    MetaSlot, mapping,
    meta::{AnyFrameMeta, get_slot},
    unique::UniqueFrame,
};
use crate::{
    arch::mm::PagingConsts,
    mm::{Paddr, Vaddr},
    //panic::abort,
};
use core::{
    ops::{Deref, DerefMut},
    ptr::NonNull,
    sync::atomic::{AtomicU64, Ordering},
};

verus! {

/// A linked list of frames.
///
/// Two key features that [`LinkedList`] is different from
/// [`alloc::collections::LinkedList`] is that:
///  1. It is intrusive, meaning that the links are part of the frame metadata.
///     This allows the linked list to be used without heap allocation. But it
///     disallows a frame to be in multiple linked lists at the same time.
///  2. The linked list exclusively own the frames, meaning that it takes
///     unique pointers [`UniqueFrame`]. And other bodies cannot
///     [`from_in_use`] a frame that is inside a linked list.
///  3. We also allow creating cursors at a specific frame, allowing $O(1)$
///     removal without iterating through the list at a cost of some checks.
///
/// # Example
///
/// To create metadata types that allows linked list links, wrap the metadata
/// type in [`Link`]:
///
/// ```rust
/// use ostd::{
///     mm::{frame::{linked_list::{Link, LinkedList}, Frame}, FrameAllocOptions},
///     impl_untyped_frame_meta_for,
/// };
///
/// #[derive(Debug)]
/// struct MyMeta { mark: usize }
///
/// type MyFrame = Frame<Link<MyMeta>>;
///
/// impl_untyped_frame_meta_for!(MyMeta);
///
/// let alloc_options = FrameAllocOptions::new();
/// let frame1 = alloc_options.alloc_frame_with(Link::new(MyMeta { mark: 1 })).unwrap();
/// let frame2 = alloc_options.alloc_frame_with(Link::new(MyMeta { mark: 2 })).unwrap();
///
/// let mut list = LinkedList::new();
/// list.push_front(frame1.try_into().unwrap());
/// list.push_front(frame2.try_into().unwrap());
///
/// let mut cursor = list.cursor_front_mut();
/// assert_eq!(cursor.current_meta().unwrap().mark, 2);
/// cursor.move_next();
/// assert_eq!(cursor.current_meta().unwrap().mark, 1);
/// ```
///
/// [`from_in_use`]: super::Frame::from_in_use
///
/// # Verified Properties
/// ## Verification Design
/// The linked list is abstractly represented by a [`LinkedListOwner`]:
/// ```rust
/// tracked struct LinkedListOwner<M: AnyFrameMeta + Repr<MetaSlotStorage>> {
///     pub list: Seq<LinkOwner>,
///     pub list_id: u64,
/// }
/// ```
/// The raw slot and storage permissions for each link are parked in the global
/// [`MetaRegionOwners`], while [`LinkedListOwner`] owns the corresponding
/// type-specific `Link<M>::ReprPerm`. Cursor accessors borrow these independent
/// components together when projecting a `Link<M>`.
/// ## Invariant
/// The linked list uniquely owns the raw frames that it contains, so they cannot be used by other
/// data structures. The frame metadata field `in_list` is equal to `list_id` for all links in the list.
/// The per-link well-formedness against the region (pointer/permission wiring,
/// `next`/`prev` pointer chain) is captured by
/// [`LinkedListOwner::relate_region`] (opaque, with per-position
/// [`LinkedListOwner::relate_region_at`]). The cursor exposes this via
/// [`CursorOwner::wf_with_region`] and [`CursorMut::wf_region`].
/// ## Safety
/// A given linked list can only have one cursor at a time, so there are no data races.
/// The `prev` and `next` fields of the metadata for each link always points to valid
/// links in the list, so the structure is memory safe (will not read or write invalid memory).
pub struct LinkedList<M: AnyFrameMeta + Repr<MetaSlotSmall>> {
    pub front: Option<ReprPtr<MetaSlotStorage, Link<M>>>,
    pub back: Option<ReprPtr<MetaSlotStorage, Link<M>>>,
    /// The number of frames in the list.
    pub size: usize,
    /// A lazily initialized ID, used to check whether a frame is in the list.
    /// 0 means uninitialized.
    pub list_id: u64,
}

/// 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.
pub struct CursorMut<'a, M: AnyFrameMeta + Repr<MetaSlotSmall>> {
    pub list: &'a mut LinkedList<M>,
    pub current: Option<ReprPtr<MetaSlotStorage, Link<M>>>,
}

#[verifier::spinoff_prover]
proof fn lemma_meta_region_inv_at(regions: MetaRegionOwners, i: int)
    requires
        regions.inv(),
        regions.contains(i),
    ensures
        regions.slot_owners[i].inv(),
        regions.slots[i].is_init(),
        regions.slots[i].addr() == index_to_meta(i),
        regions.slots[i].value().wf(regions.slot_owners[i]),
        regions.slot_owners[i].slot_vaddr == regions.slots[i].addr(),
{
}

/// Localizes the "no existing slot aliases the inserted frame" universal fact
/// into its own prover query, so the `MetaRegionOwners::inv` and map-insert
/// quantifiers do not get over-instantiated inside `insert_before`'s body.
#[verifier::spinoff_prover]
proof fn lemma_insert_before_slot_distinct<M: AnyFrameMeta + Repr<MetaSlotSmall>>(
    owner0: LinkedListOwner<M>,
    regions0: MetaRegionOwners,
    frame_idx: int,
    nn: int,
)
    requires
        owner0.relate_region(regions0),
        regions0.inv(),
        regions0.contains(frame_idx),
        regions0.slot_owners[frame_idx].in_list_perm.value() == 0,
        0 <= nn <= owner0.list.len() as int,
    ensures
        forall|p: int|
            #![trigger regions0.slot_owners[meta_to_index(owner0.list[p].paddr)]]
            (0 <= p < owner0.list.len() as int) ==> frame_idx != meta_to_index(
                owner0.list[p].paddr,
            ),
{
    assert forall|p: int|
        #![trigger regions0.slot_owners[meta_to_index(owner0.list[p].paddr)]]
        0 <= p < owner0.list.len() as int implies frame_idx != meta_to_index(
        owner0.list[p].paddr,
    ) by {
        owner0.relate_region_at_facts(regions0, p);
        if frame_idx == meta_to_index(owner0.list[p].paddr) {
            assert(regions0.slot_owners[meta_to_index(owner0.list[p].paddr)].in_list_perm.value()
                == owner0.list_id);
        }
    }
}

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedList<M> {
    /// Creates a new linked list.
    pub const fn new() -> Self {
        Self { front: None, back: None, size: 0, list_id: 0 }
    }
}

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Default for LinkedList<M> {
    fn default() -> Self {
        Self::new()
    }
}

#[verus_verify]
impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedList<M> {
    /// Gets the number of frames in the linked list.
    #[verus_spec(s =>
        with
            Tracked(owner): Tracked<LinkedListOwner<M>>,
        requires
            self.wf(owner),
            owner.inv(),
        ensures
            s == owner@.list.len(),
    )]
    pub fn size(&self) -> usize {
        proof {
            LinkedListOwner::<M>::view_preserves_len(owner.list);
        }
        self.size
    }

    /// Tells if the linked list is empty.
    #[verus_spec(b =>
        with
            Tracked(owner): Tracked<LinkedListOwner<M>>,
        requires
            self.wf(owner),
            owner.inv(),
        ensures
            b ==> self.size == 0 && self.front is None && self.back is None,
            !b ==> self.size > 0 && self.front is Some && self.back is Some,
    )]
    pub fn is_empty(&self) -> bool {
        let is_empty = self.size == 0;
        is_empty
    }

    /// Pushes a frame to the front of the linked list.
    /// # Verified Properties
    /// ## Preconditions
    /// The list 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 inside of `insert_before`.
    /// ## Postconditions
    /// The new frame is inserted at the front of the list, and the cursor is moved to the new frame.
    /// The list invariants are preserved.
    /// ## Safety
    /// See [`insert_before`] for the safety guarantees.
    #[verus_spec(
        with
            Tracked(regions): Tracked<&mut MetaRegionOwners>,
            Tracked(owner): Tracked<&mut LinkedListOwner<M>>,
            Tracked(frame_own): Tracked<&mut UniqueFrameOwner<Link<M>>>,
        requires
            old(self).wf_region(*old(owner), *old(regions)),
            old(owner).relate_region(*old(regions)),
            old(frame_own).inv(),
            old(frame_own).global_inv(*old(regions)),
            frame.wf(*old(frame_own)),
            old(frame_own).frame_link_inv(*old(regions)),
            old(regions).inv(),
        ensures
            final(owner).relate_region(*final(regions)),
            final(regions).inv(),
            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,
            final(frame_own).meta_own.paddr == old(frame_own).meta_own.paddr,
            final(frame_own).meta_own.in_list == final(owner).list_id,
    )]
    pub fn push_front(&mut self, frame: UniqueFrame<Link<M>>) {
        let current = self.front;
        let tracked owner0 = LinkedListOwner::tracked_take(owner);
        let tracked mut cursor_own = CursorOwner::tracked_front_owner(owner0);
        let mut cursor = CursorMut { list: self, current };

        #[verus_spec(with Tracked(regions), Tracked(&mut cursor_own), Tracked(frame_own))]
        cursor.insert_before(frame);

        proof {
            *owner = cursor_own.list_own;
        }
    }

    /// Pops a frame from the front of the linked list.
    /// # Verified Properties
    /// ## Preconditions
    /// The list 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 front frame is removed from the list, and the cursor is moved to the next frame.
    /// The list invariants are preserved.
    /// ## Safety
    /// See [`take_current`] for the safety guarantees.
    #[verus_spec(r =>
        with
            Tracked(regions): Tracked<&mut MetaRegionOwners>,
            Tracked(owner): Tracked<LinkedListOwner<M>>,
            Tracked(frame_own): Tracked<UniqueFrameOwner<Link<M>>>,
        requires
            old(regions).inv(),
            old(self).wf_region(owner, *old(regions)),
            owner.relate_region(*old(regions)),
        ensures
            owner.list.len() == 0 ==> r.is_none(),
            r.is_some() ==> (r->0).1@@.meta == owner.list[0]@,
            r.is_some() ==> (r->0).1@.frame_link_inv(*final(regions)),
    )]
    pub fn pop_front(&mut self) -> Option<
        (UniqueFrame<Link<M>>, Tracked<UniqueFrameOwner<Link<M>>>),
    > {
        let tracked mut cursor_own = CursorOwner::tracked_front_owner(owner);
        let current = self.front;
        let mut cursor = CursorMut { list: self, current };

        proof {
            if owner.list.len() > 0 {
                owner.relate_region_at_facts(*regions, 0);
            }
        }

        #[verus_spec(with Tracked(regions), Tracked(&mut cursor_own))]
        cursor.take_current()
    }

    /// Pushes a frame to the back of the linked list.
    /// # Verified Properties
    /// ## Preconditions
    /// The list 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 inside of `insert_before`.
    /// ## Postconditions
    /// - The new frame is inserted at the back of the list, and the cursor is moved to the new frame.
    /// - The list invariants are preserved.
    /// ## Safety
    /// See [`insert_before`] for the safety guarantees.
    #[verus_spec(
        with
            Tracked(regions): Tracked<&mut MetaRegionOwners>,
            Tracked(owner): Tracked<&mut LinkedListOwner<M>>,
            Tracked(frame_own): Tracked<&mut UniqueFrameOwner<Link<M>>>,
        requires
            old(self).wf_region(*old(owner), *old(regions)),
            old(owner).relate_region(*old(regions)),
            old(frame_own).inv(),
            old(frame_own).global_inv(*old(regions)),
            frame.wf(*old(frame_own)),
            old(frame_own).frame_link_inv(*old(regions)),
            old(regions).inv(),
        ensures
            final(owner).relate_region(*final(regions)),
            final(regions).inv(),
            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),
            // Id preserved when already minted; a fresh (empty) list adopts a
            // non-zero id.
            old(owner).list_id != 0 ==> final(owner).list_id == old(owner).list_id,
            final(owner).list_id != 0,
            final(frame_own).meta_own.paddr == old(frame_own).meta_own.paddr,
            final(frame_own).meta_own.in_list == final(owner).list_id,
    )]
    pub fn push_back(&mut self, frame: UniqueFrame<Link<M>>) {
        let current = self.back;
        let tracked owner0 = LinkedListOwner::tracked_take(owner);
        let tracked mut cursor_own = CursorOwner::tracked_back_owner(owner0);
        let mut cursor = CursorMut { list: self, current };

        #[verus_spec(with Tracked(regions), Tracked(&mut cursor_own), Tracked(frame_own))]
        cursor.insert_before(frame);

        proof {
            *owner = cursor_own.list_own;
        }
    }

    /// Pops a frame from the back of the linked list.
    /// # Verified Properties
    /// ## Preconditions
    /// - The list 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 back frame is removed from the list, and the cursor is moved to the "ghost" non-element.
    /// - The list invariants are preserved.
    /// ## Safety
    /// See [`take_current`] for the safety guarantees.
    #[verus_spec(r =>
        with
            Tracked(regions): Tracked<&mut MetaRegionOwners>,
            Tracked(owner): Tracked<LinkedListOwner<M>>,
            Tracked(frame_own): Tracked<UniqueFrameOwner<Link<M>>>,
        requires
            old(regions).inv(),
            old(self).wf_region(owner, *old(regions)),
            owner.relate_region(*old(regions)),
        ensures
            owner.list.len() == 0 ==> r.is_none(),
            r.is_some() ==> (r->0).1@@.meta == owner.list[owner.list.len() - 1]@,
            r.is_some() ==> (r->0).1@.frame_link_inv(*final(regions)),
    )]
    pub fn pop_back(&mut self) -> Option<
        (UniqueFrame<Link<M>>, Tracked<UniqueFrameOwner<Link<M>>>),
    > {
        let current = self.back;
        let tracked mut cursor_own = CursorOwner::tracked_back_owner(owner);
        let mut cursor = CursorMut { list: self, current };

        proof {
            if owner.list.len() > 0 {
                owner.relate_region_at_facts(*regions, owner.list.len() - 1);
            }
        }

        #[verus_spec(with Tracked(regions), Tracked(&mut cursor_own))]
        cursor.take_current()
    }

    /// Tells if a frame is in the list.
    /// # Verified Properties
    /// ## Preconditions
    /// - The list must be well-formed, with the pointers to its links' metadata slots
    /// matching the tracked permission objects.
    /// - The frame must be a valid, active frame.
    /// ## Postconditions
    /// The function returns `true` if the frame is in the list, `false` otherwise.
    /// ## Safety
    /// - `lazy_get_id` uses atomic memory accesses, so there are no data races.
    /// - We assume that the ID allocator has an available ID if the list previously didn't have one,
    /// but the consequence if that is not the case is a failsafe panic.
    /// - Everything else conforms to the safe interface.
    #[verus_spec(r =>
        with
            Tracked(regions): Tracked<&mut MetaRegionOwners>,
            Tracked(slot_own): Tracked<&MetaSlotOwner>,
            Tracked(owner): Tracked<&mut LinkedListOwner<M>>,
        requires
            slot_own.inv(),
            old(regions).inv(),
        ensures
            old(owner).list_id != 0 ==> *final(owner) == *old(owner),
    )]
    pub fn contains(&mut self, frame: Paddr) -> bool {
        proof_decl! {
        let ghost idx = frame_to_index(frame);
            if valid_frame_paddr(frame) {
                regions.lemma_contains_valid_frame_paddr(frame);
            }
        let tracked slot_perm = if valid_frame_paddr(frame) {
            Some(*regions.slots.tracked_borrow(idx))
        } else {
            None
        };
        }
        let Ok(slot) = (#[verus_spec(with Tracked(slot_perm))]
        crate::mm::frame::meta::get_slot(frame)) else {
            return false;
        };

        let tracked mut slot_own = regions.slot_owners.tracked_borrow_mut(idx);

        slot.in_list.load(Tracked(&mut slot_own.in_list_perm)) == #[verus_spec(with Tracked(owner))]
        self.lazy_get_id()
    }

    /// Gets a cursor at the specified frame if the frame is in the list.
    ///
    /// This method fails if the frame is not in the list.
    /// # Verified Properties
    /// ## Preconditions
    /// - The list must be well-formed, with the pointers to its links' metadata slots
    /// matching the tracked permission objects.
    /// - The frame should be raw (because it is owned by the list)
    /// ## Postconditions
    /// - This functions post-conditions are incomplete due to refactoring of the permission model.
    /// When complete, it will guarantee that the cursor is well-formed and points to the matching
    /// element in the list.
    /// ## Safety
    /// - `lazy_get_id` uses atomic memory accesses, so there are no data races.
    /// - We assume that the ID allocator has an available ID if the list previously didn't have one,
    /// but the consequence if that is not the case is a failsafe panic.
    /// - Everything else conforms to the safe interface.
    #[verus_spec(r =>
        with
            Tracked(regions): Tracked<&mut MetaRegionOwners>,
            Tracked(owner): Tracked<LinkedListOwner<M>>,
            -> cursor_owner: Tracked<Option<CursorOwner<M>>>,
        requires
            old(regions).inv(),
        ensures
            !valid_frame_paddr(frame) ==> r is None,
            final(regions).inv(),
            final(regions).slots == old(regions).slots,
            final(regions).slot_owners.dom() == old(regions).slot_owners.dom(),
    )]
    pub fn cursor_mut_at(&mut self, frame: Paddr) -> Option<CursorMut<'_, M>> {
        proof_decl! {
            let ghost idx = frame_to_index(frame);
            if valid_frame_paddr(frame) {
                regions.lemma_contains_valid_frame_paddr(frame);
            }

            let tracked slot_perm = if valid_frame_paddr(frame) {
                Some(*regions.slots.tracked_borrow(idx))
            } else {
                None
            };
        }
        let Ok(slot) = (#[verus_spec(with Tracked(slot_perm))]
        crate::mm::frame::meta::get_slot(frame)) else {
            return {
                proof_with!(|= Tracked(None));
                None
            };
        };

        let tracked mut slot_own = regions.slot_owners.tracked_borrow_mut(idx);
        let contains = slot.in_list.load(Tracked(&mut slot_own.in_list_perm))
            == #[verus_spec(with Tracked(&owner))]
        self.lazy_get_id();

        if contains {
            proof_decl!{
                let ghost link = owner.list.filter(|link: LinkOwner| link.paddr == frame).first();
                let ghost index = owner.list.index_of(link);
                let tracked cursor_owner = CursorOwner::tracked_cursor_mut_at_owner(owner, index);
            }

            let meta_ptr = ReprPtr::<MetaSlotStorage, Link<M>>::from_pptr(
                PPtr::<MetaSlotStorage>::from_addr(frame_to_meta(frame)),
            );
            proof_with!(|= Tracked(Some(cursor_owner)));
            Some(CursorMut { list: self, current: Some(meta_ptr) })
        } else {
            proof_with!(|= Tracked(None));
            None
        }
    }

    /// Gets a cursor at the front that can mutate the linked list links.
    ///
    /// If the list is empty, the cursor points to the "ghost" non-element.
    /// # Verified Properties
    /// ## Preconditions
    /// - The list must be well-formed, with the pointers to its links' metadata slots
    /// matching the tracked permission objects.
    /// ## Postconditions
    /// - The cursor is well-formed, with the pointers to its links' metadata slots
    /// matching the tracked permission objects. The list invariants are preserved.
    /// - See [`CursorOwner::front_owner`] for the precise specification.
    /// ## Safety
    /// - This function only uses the list permission, so there are no illegal memory accesses.
    /// - No data races are possible.
    #[verus_spec(r =>
        with
            Tracked(owner): Tracked<LinkedListOwner<M>>,
        requires
            old(self).wf(owner),
            owner.inv(),
        ensures
            r.0.wf(r.1@),
            r.1@.inv(),
            r.1@ == CursorOwner::front_owner(owner),
    )]
    pub fn cursor_front_mut(&mut self) -> (CursorMut<'_, M>, Tracked<CursorOwner<M>>) {
        let current = self.front;

        (CursorMut { list: self, current }, Tracked(CursorOwner::tracked_front_owner(owner)))
    }

    /// Gets a cursor at the back that can mutate the linked list links.
    ///
    /// If the list is empty, the cursor points to the "ghost" non-element.
    /// # Verified Properties
    /// ## Preconditions
    /// - The list must be well-formed, with the pointers to its links' metadata slots
    /// matching the tracked permission objects.
    /// ## Postconditions
    /// - The cursor is well-formed, with the pointers to its links' metadata slots
    /// matching the tracked permission objects. The list invariants are preserved.
    /// See [`CursorOwner::back_owner`] for the precise specification.
    /// ## Safety
    /// - This function only uses the list permission, so there are no illegal memory accesses.
    /// - No data races are possible.
    #[verus_spec(
        with
            Tracked(owner): Tracked<LinkedListOwner<M>>,
    )]
    pub fn cursor_back_mut(&mut self) -> (res: (CursorMut<'_, M>, Tracked<CursorOwner<M>>))
        requires
            old(self).wf(owner),
            owner.inv(),
        ensures
            res.0.wf(res.1@),
            res.1@.inv(),
            res.1@ == CursorOwner::back_owner(owner),
    {
        let current = self.back;

        (CursorMut { list: self, current }, Tracked(CursorOwner::tracked_back_owner(owner)))
    }

    /// Gets a cursor at the "ghost" non-element that can mutate the linked list links.
    #[verus_spec(
        with Tracked(owner): Tracked<&mut LinkedListOwner<M>>
    )]
    fn cursor_at_ghost_mut(&mut self) -> CursorMut<'_, M> {
        CursorMut { list: self, current: None }
    }

    /// # Verification Assumption
    /// We assume that there is an available ID for `lazy_get_id` to return.
    /// This is safe because it will panic if the ID allocator is exhausted.
    #[verifier::external_body]
    #[verus_spec(
        with Tracked(owner): Tracked<& LinkedListOwner<M>>
    )]
    fn lazy_get_id(&mut self) -> (id: u64)
        ensures
            owner.list_id != 0 ==> id == owner.list_id,
            final(self).size == old(self).size,
            final(self).front == old(self).front,
            final(self).back == old(self).back,
            old(self).list_id != 0 ==> final(self).list_id == old(self).list_id,
            id != 0,
            final(self).list_id == id,
    {
        unimplemented!()/*        // FIXME: Self-incrementing IDs may overflow, while `core::pin::Pin`
        // is not compatible with locks. Think about a better solution.
        static LIST_ID_ALLOCATOR: AtomicU64 = AtomicU64::new(1);
        const MAX_LIST_ID: u64 = i64::MAX as u64;

        if self.list_id == 0 {
            let id = LIST_ID_ALLOCATOR.fetch_add(1, Ordering::Relaxed);
            if id >= MAX_LIST_ID {
//                log::error!("The frame list ID allocator has exhausted.");
//                abort();
                unimplemented!()
            }
            self.list_id = id;
            id
        } else {
            self.list_id
        }*/

    }
}

impl<'a, M: AnyFrameMeta + Repr<MetaSlotSmall>> CursorMut<'a, M> {
    /// 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.
    #[verus_spec(
        with Tracked(owner): Tracked<CursorOwner<M>>,
            Tracked(regions): Tracked<&MetaRegionOwners>,
    )]
    pub fn move_next(&mut self)
        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),
    {
        proof {
            if self.current is Some {
                owner.list_own.relate_region_at_facts(*regions, owner.index);
            }
            if owner.index < owner.length() - 1 {
                owner.list_own.relate_region_at_facts(*regions, owner.index + 1);
            }
        }

        self.current = match self.current {
            // SAFETY: The cursor is pointing to a valid element.
            Some(current) => {
                proof_decl!{
                    let ghost idx = meta_to_index(current.addr());
                    let tracked points_to = regions.slots.tracked_borrow(idx);
                    let tracked slot_owner = regions.slot_owners.tracked_borrow(idx);
                    let tracked repr_perm = owner.list_own.repr_perms.tracked_borrow(owner.index);
                }
                proof {
                    assert(regions.contains(idx));
                }
                let link = borrow_meta(
                    current,
                    Tracked(points_to),
                    Tracked(&slot_owner.metadata_perm),
                    Tracked(repr_perm),
                );
                link.next
            },
            None => self.list.front,
        };

        proof {
            LinkedListOwner::<M>::view_preserves_len(owner.list_own.list);
            assert(owner.move_next_owner_spec()@.fore == owner@.move_next_spec().fore);
            assert(owner.move_next_owner_spec()@.rear == owner@.move_next_spec().rear);
        }
    }

    /// 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.
    #[verus_spec(
        with Tracked(owner): Tracked<CursorOwner<M>>,
            Tracked(regions): Tracked<&MetaRegionOwners>,
    )]
    pub fn move_prev(&mut self)
        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),
    {
        proof {
            if self.current is Some {
                owner.list_own.relate_region_at_facts(*regions, owner.index);
            }
            if 0 < owner.index {
                owner.list_own.relate_region_at_facts(*regions, owner.index - 1);
            }
        }

        self.current = match self.current {
            // SAFETY: The cursor is pointing to a valid element.
            Some(current) => {
                proof_decl!{
                    let ghost idx = meta_to_index(current.addr());
                    let tracked points_to = regions.slots.tracked_borrow(idx);
                    let tracked slot_owner = regions.slot_owners.tracked_borrow(idx);
                    let tracked repr_perm = owner.list_own.repr_perms.tracked_borrow(owner.index);
                }
                proof {
                    assert(regions.contains(idx));
                }

                let link = borrow_meta(
                    current,
                    Tracked(points_to),
                    Tracked(&slot_owner.metadata_perm),
                    Tracked(repr_perm),
                );
                link.prev
            },
            None => self.list.back,
        };

        proof {
            LinkedListOwner::<M>::view_preserves_len(owner.list_own.list);

            if owner@.list_model.list.len() > 0 {
                if owner@.fore.len() > 0 {
                    assert(owner.move_prev_owner_spec()@.fore == owner@.move_prev_spec().fore);
                    assert(owner.move_prev_owner_spec()@.rear == owner@.move_prev_spec().rear);
                    if owner@.rear.len() > 0 {
                        owner.list_own.relate_region_at_facts(*regions, owner.index);
                    }
                } else {
                    owner.list_own.relate_region_at_facts(*regions, owner.index);
                    assert(owner.move_prev_owner_spec()@.rear == owner@.move_prev_spec().rear);
                    assert(owner@.rear == owner@.list_model.list);
                }
            }
        }
    }

    /// 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.
    #[verus_spec(
        with Tracked(owner): Tracked<&'b mut CursorOwner<M>>,
            Tracked(regions): Tracked<&'b mut MetaRegionOwners>,
    )]
    pub fn current_meta<'b>(&'b mut self) -> (res: Option<&'b mut M>)
        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(),
    {
        // Verus does not support option.map very well.
        // self.current.map(|current| {
        //     let link_mut = unsafe { &mut *(current.ptr.addr() as *mut Link<M>) };
        //     &mut link_mut.meta
        // })
        match self.current {
            Some(current) => {
                proof {
                    owner.list_own.relate_region_at_facts(*regions, owner.index);
                }
                let ghost idx = meta_to_index(current.addr());
                proof {
                    assert(regions.contains(idx));
                }
                let tracked points_to = regions.slots.tracked_borrow(idx);
                let tracked slot_owner = regions.slot_owners.tracked_borrow_mut(idx);
                let tracked repr_perm = owner.list_own.repr_perms.tracked_borrow_mut(owner.index);
                Some(
                    &mut borrow_meta_mut(
                        current,
                        Tracked(points_to),
                        Tracked(slot_owner),
                        Tracked(repr_perm),
                    ).meta,
                )
            },
            None => None,
        }
    }

    /// 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.
    #[verus_spec(
        with Tracked(regions) : Tracked<&mut MetaRegionOwners>,
            Tracked(owner) : Tracked<&mut CursorOwner<M>>
    )]
    #[verifier::spinoff_prover]
    #[verifier::rlimit(200)]
    pub fn take_current(&mut self) -> (res: Option<
        (UniqueFrame<Link<M>>, Tracked<UniqueFrameOwner<Link<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 == old(owner).list_own.list[old(owner).index]@,
            res.is_some() ==> final(owner)@ == old(owner)@.remove(),
            res.is_some() ==> (res->0).1@.frame_link_inv(*final(regions)),
            // Invariant preservation
            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(),
            // Structural: remove_owner_spec
            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).slot_owners[idx].ref_count() == REF_COUNT_UNIQUE
                &&& final(regions).slot_owners[idx].in_list_perm.value() == 0
                &&& final(regions).slot_owners[idx].storage_perm().is_init()
                &&& final(regions).slot_owners[idx].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|
                #![trigger final(regions).slot_owners[j]]
                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),
            // Properties of the returned frame needed for UniqueFrame::drop
            res.is_some() ==> (res->0).0.wf((res->0).1@),
            res.is_some() ==> (res->0).1@.inv(),
            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(),
            res.is_some() ==> final(regions).frame_obligations == old(
                regions,
            ).frame_obligations.insert(meta_to_index(old(self).current->0.addr())),
    {
        let ghost owner0 = *owner;
        let ghost regions0 = *regions;

        let current = self.current?;

        proof {
            owner.list_own.relate_region_at_facts(*regions, owner.index);
            if owner.index > 0 {
                owner.list_own.relate_region_at_facts(*regions, owner.index - 1);
            }
            if owner.index < owner.list_own.list.len() - 1 {
                owner.list_own.relate_region_at_facts(*regions, owner.index + 1);
            }
        }

        let meta_ptr = current.addr();
        let paddr = meta_to_frame(meta_ptr);
        let ghost idx = frame_to_index(paddr);

        let tracked mut cur_own = owner.list_own.list.tracked_remove(owner.index);
        let tracked cur_repr_perm = owner.list_own.repr_perms.tracked_remove(owner.index);

        let (mut frame, Tracked(mut frame_own)) = unsafe {
            // SAFETY: The frame was forgotten when inserted into the linked list.
            #[verus_spec(with Tracked(regions), Tracked(cur_own), Tracked(cur_repr_perm))]
            UniqueFrame::<Link<M>>::from_raw(paddr)
        };

        proof {
            assert(regions.slots.dom() == regions0.slots.dom());
            assert forall|j: int| #![trigger regions0.slot_owners[j]] j != idx implies {
                &&& regions.slot_owners[j].usage == regions0.slot_owners[j].usage
                &&& regions.slot_owners[j].slot_vaddr == regions0.slot_owners[j].slot_vaddr
                &&& regions.slot_owners[j].paths_in_pt == regions0.slot_owners[j].paths_in_pt
            } by {}
        }

        let next_ptr = (#[verus_spec(with Tracked(&frame_own), Tracked(&*regions))]
        frame.meta()).next;
        let prev_ptr = (#[verus_spec(with Tracked(&frame_own), Tracked(&*regions))]
        frame.meta()).prev;

        if let Some(prev) = prev_ptr {
            let ghost prev_idx = meta_to_index(owner.list_own.list[owner.index - 1].paddr);
            let tracked prev_points_to = regions.slots.tracked_borrow(prev_idx);
            let tracked prev_slot_owner = regions.slot_owners.tracked_borrow_mut(prev_idx);
            let tracked prev_repr_perm = owner.list_own.repr_perms.tracked_borrow_mut(
                owner.index - 1,
            );
            let prev_meta = borrow_meta_mut(
                prev,
                Tracked(prev_points_to),
                Tracked(prev_slot_owner),
                Tracked(prev_repr_perm),
            );
            prev_meta.next = next_ptr;

            proof {
                assert(regions.inv());
                assert(regions.slots.dom() == regions0.slots.dom());
                assert forall|j: int| #![trigger regions0.slot_owners[j]] j != idx implies {
                    &&& regions.slot_owners[j].usage == regions0.slot_owners[j].usage
                    &&& regions.slot_owners[j].slot_vaddr == regions0.slot_owners[j].slot_vaddr
                    &&& regions.slot_owners[j].paths_in_pt == regions0.slot_owners[j].paths_in_pt
                } by {
                    if j == meta_to_index(prev.addr()) {
                    }
                }
            }

        } else {
            self.list.front = next_ptr;
            proof {
                assert(regions.slots.dom() == regions0.slots.dom());
                assert forall|j: int| #![trigger regions0.slot_owners[j]] j != idx implies {
                    &&& regions.slot_owners[j].usage == regions0.slot_owners[j].usage
                    &&& regions.slot_owners[j].slot_vaddr == regions0.slot_owners[j].slot_vaddr
                    &&& regions.slot_owners[j].paths_in_pt == regions0.slot_owners[j].paths_in_pt
                } by {}
            }
        }

        if let Some(next) = next_ptr {
            let ghost next_idx = meta_to_index(owner.list_own.list[owner.index].paddr);
            let tracked next_points_to = regions.slots.tracked_borrow(next_idx);
            let tracked next_slot_owner = regions.slot_owners.tracked_borrow_mut(next_idx);
            let tracked next_repr_perm = owner.list_own.repr_perms.tracked_borrow_mut(owner.index);
            let next_meta = borrow_meta_mut(
                next,
                Tracked(next_points_to),
                Tracked(next_slot_owner),
                Tracked(next_repr_perm),
            );
            next_meta.prev = prev_ptr;

            proof {
                assert(regions.inv());
                assert(regions.slots.dom() == regions0.slots.dom());
                assert forall|j: int| #![trigger regions0.slot_owners[j]] j != idx implies {
                    &&& regions.slot_owners[j].usage == regions0.slot_owners[j].usage
                    &&& regions.slot_owners[j].slot_vaddr == regions0.slot_owners[j].slot_vaddr
                    &&& regions.slot_owners[j].paths_in_pt == regions0.slot_owners[j].paths_in_pt
                } by {
                    if j == meta_to_index(next.addr()) {
                    }
                }
            }

            self.current = Some(next);
        } else {
            self.list.back = prev_ptr;

            self.current = None;
            proof {
                assert(regions.slots.dom() == regions0.slots.dom());
                assert forall|j: int| #![trigger regions0.slot_owners[j]] j != idx implies {
                    &&& regions.slot_owners[j].usage == regions0.slot_owners[j].usage
                    &&& regions.slot_owners[j].slot_vaddr == regions0.slot_owners[j].slot_vaddr
                    &&& regions.slot_owners[j].paths_in_pt == regions0.slot_owners[j].paths_in_pt
                } by {}
            }
        }

        (#[verus_spec(with Tracked(&mut frame_own), Tracked(regions))]
        frame.meta_mut()).next = None;
        (#[verus_spec(with Tracked(&mut frame_own), Tracked(regions))]
        frame.meta_mut()).prev = None;

        let tracked frame_outer = regions.slots.tracked_borrow(idx);
        let tracked mut frame_so = regions.slot_owners.tracked_borrow_mut(idx);
        #[verus_spec(with Tracked(&frame_outer))]
        let slot = frame.slot();
        slot.in_list.store(Tracked(&mut frame_so.in_list_perm), 0);
        proof {
            assert(regions.inv());
            assert(regions.slots.dom() == regions0.slots.dom());
            assert(regions.slot_owners[idx].paths_in_pt == regions0.slot_owners[idx].paths_in_pt);
            assert forall|j: int| #![trigger regions0.slot_owners[j]] j != idx implies {
                &&& regions.slot_owners[j].usage == regions0.slot_owners[j].usage
                &&& regions.slot_owners[j].slot_vaddr == regions0.slot_owners[j].slot_vaddr
                &&& regions.slot_owners[j].paths_in_pt == regions0.slot_owners[j].paths_in_pt
            } by {}
        }

        self.list.size = self.list.size - 1;

        proof {
            owner0.remove_owner_spec_implies_model_spec(*owner);
            let ghost oldl = owner0.list_own;
            let ghost nn = owner0.index as int;
            assert forall|p: int|
                #![trigger meta_to_index(oldl.list[p].paddr)]
                (0 <= p < oldl.list.len() && p != nn) implies ({
                let i = meta_to_index(oldl.list[p].paddr);
                let np = if p < nn {
                    p
                } else {
                    p - 1
                };
                let fp = owner.list_own.meta_value_at(*regions, np);
                &&& regions.contains(i)
                &&& regions.slots[i].addr() == oldl.list[p].paddr
                &&& regions.slots[i].pptr() == regions0.slots[i].pptr()
                &&& regions.slot_owners[i].ref_count() == REF_COUNT_UNIQUE
                &&& regions.slot_owners[i].usage is Frame
                &&& regions.slot_owners[i].in_list_perm.value() == owner.list_own.list_id
                &&& owner.list_own.meta_wf_at(*regions, np)
                &&& regions.slots[i].addr() % META_SLOT_SIZE == 0
                &&& FRAME_METADATA_RANGE.start <= regions.slots[i].addr()
                    < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
                &&& (p == nn - 1 ==> fp.next == oldl.meta_value_at(regions0, nn).next)
                &&& (p != nn - 1 ==> fp.next == oldl.meta_value_at(regions0, p).next)
                &&& (p == nn + 1 ==> fp.prev == oldl.meta_value_at(regions0, nn).prev)
                &&& (p != nn + 1 ==> fp.prev == oldl.meta_value_at(regions0, p).prev)
            }) by {
                let i = meta_to_index(oldl.list[p].paddr);
                let np = if p < nn {
                    p
                } else {
                    p - 1
                };
                let fp = owner.list_own.meta_value_at(*regions, np);
                oldl.relate_region_at_facts(regions0, p);
                oldl.relate_region_at_facts(regions0, nn);
                assert(regions.contains(i));
            }
            LinkedListOwner::pop_preserves_relate_region(
                oldl,
                regions0,
                owner.list_own,
                *regions,
                nn,
            );
        }
        Some((frame, Tracked(frame_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.)
    #[verus_spec(
        with Tracked(regions): Tracked<&mut MetaRegionOwners>,
            Tracked(owner): Tracked<&mut CursorOwner<M>>,
            Tracked(frame_own): Tracked<&mut UniqueFrameOwner<Link<M>>>
    )]
    #[verifier::spinoff_prover]
    #[verifier::rlimit(200)]
    pub fn insert_before(&mut self, mut frame: UniqueFrame<Link<M>>)
        requires
            old(self).wf_region(*old(owner), *old(regions)),
            old(owner).wf_with_region(*old(regions)),
            old(regions).inv(),
            old(frame_own).inv(),
            old(frame_own).global_inv(*old(regions)),
            frame.wf(*old(frame_own)),
            old(frame_own).frame_link_inv(*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,
            ),
            // The id is preserved when it was already minted; a `list_id == 0`
            // (necessarily empty) list adopts a freshly-minted non-zero id.
            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@),
    {
        hide(LinkedListOwner::relate_region);
        hide(<MetaRegionOwners as Inv>::inv);
        let ghost owner0 = *owner;
        let ghost regions0 = *regions;
        let ghost nn = owner.index as int;

        proof {
            assert(owner0.list_own.repr_perms.len() == owner0.list_own.list.len()) by {
                reveal(LinkedListOwner::relate_region);
            };
            assert(owner0.list_own.list.len() > 0 ==> owner0.list_own.list_id != 0) by {
                reveal(LinkedListOwner::relate_region);
            };
            assert(regions0.contains(frame_own.slot_index));
            lemma_meta_region_inv_at(regions0, frame_own.slot_index);
            owner0.list_own.length_lt_usize_max(regions0);
            if nn > 0 {
                assert(owner0.list_own.relate_region_at(regions0, nn - 1)) by {
                    reveal(LinkedListOwner::relate_region);
                };
                owner.list_own.relate_region_at_facts(*regions, nn - 1);
                lemma_meta_region_inv_at(
                    regions0,
                    meta_to_index(owner0.list_own.list[nn - 1].paddr),
                );
            }
            if nn < owner.list_own.list.len() {
                assert(owner0.list_own.relate_region_at(regions0, nn)) by {
                    reveal(LinkedListOwner::relate_region);
                };
                owner.list_own.relate_region_at_facts(*regions, nn);
                lemma_meta_region_inv_at(regions0, meta_to_index(owner0.list_own.list[nn].paddr));
            }
            assert forall|p: int|
                #![trigger
                    regions0.slot_owners[meta_to_index(owner0.list_own.list[p].paddr)]]
                0 <= p < owner0.list_own.list.len() implies frame_own.slot_index != meta_to_index(
                owner0.list_own.list[p].paddr,
            ) by {
                lemma_insert_before_slot_distinct(
                    owner0.list_own,
                    regions0,
                    frame_own.slot_index,
                    nn,
                );
            }
        }

        let frame_ptr = ReprPtr::<MetaSlotStorage, Link<M>>::from_pptr(
            PPtr::<MetaSlotStorage>::from_addr(frame.ptr.addr()),
        );

        if let Some(current) = self.current {
            proof_decl!{
                let ghost idx = meta_to_index(current.addr());
                let tracked points_to = regions.slots.tracked_borrow(idx);
                let tracked slot_owner = regions.slot_owners.tracked_borrow(idx);
                let tracked repr_perm = owner.list_own.repr_perms.tracked_borrow(owner.index);
            }

            // Read current's prev pointer.
            let opt_prev_link: Option<ReprPtr<MetaSlotStorage, Link<M>>> = borrow_meta(
                current,
                Tracked(points_to),
                Tracked(&slot_owner.metadata_perm),
                Tracked(repr_perm),
            ).prev;

            if let Some(prev_link) = opt_prev_link {
                let prev = prev_link;

                (#[verus_spec(with Tracked(frame_own), Tracked(regions))]
                frame.meta_mut()).prev = Some(prev_link);
                (#[verus_spec(with Tracked(frame_own), Tracked(regions))]
                frame.meta_mut()).next = Some(current);

                let ghost prev_idx = meta_to_index(owner.list_own.list[nn - 1].paddr);
                proof {
                    assert(prev_idx != idx) by {
                        reveal(LinkedListOwner::relate_region);
                    };
                }
                let tracked prev_points_to = regions.slots.tracked_borrow(prev_idx);
                let tracked prev_slot_owner = regions.slot_owners.tracked_borrow_mut(prev_idx);
                let tracked prev_repr_perm = owner.list_own.repr_perms.tracked_borrow_mut(nn - 1);
                let prev_meta = borrow_meta_mut(
                    prev,
                    Tracked(prev_points_to),
                    Tracked(prev_slot_owner),
                    Tracked(prev_repr_perm),
                );
                prev_meta.next = Some(frame_ptr);

                let ghost current_idx = meta_to_index(owner.list_own.list[nn].paddr);
                let tracked current_points_to = regions.slots.tracked_borrow(current_idx);
                let tracked current_slot_owner = regions.slot_owners.tracked_borrow_mut(
                    current_idx,
                );
                let tracked current_repr_perm = owner.list_own.repr_perms.tracked_borrow_mut(nn);
                let current_meta = borrow_meta_mut(
                    current,
                    Tracked(current_points_to),
                    Tracked(current_slot_owner),
                    Tracked(current_repr_perm),
                );
                current_meta.prev = Some(frame_ptr);
            } else {
                (#[verus_spec(with Tracked(frame_own), Tracked(regions))]
                frame.meta_mut()).next = Some(current);

                let ghost current_idx = meta_to_index(owner.list_own.list[nn].paddr);
                let tracked current_points_to = regions.slots.tracked_borrow(current_idx);
                let tracked current_slot_owner = regions.slot_owners.tracked_borrow_mut(
                    current_idx,
                );
                let tracked current_repr_perm = owner.list_own.repr_perms.tracked_borrow_mut(nn);
                let current_meta = borrow_meta_mut(
                    current,
                    Tracked(current_points_to),
                    Tracked(current_slot_owner),
                    Tracked(current_repr_perm),
                );
                current_meta.prev = Some(frame_ptr);
                self.list.front = Some(frame_ptr);
            }
        } else {
            if let Some(back) = self.list.back {
                (#[verus_spec(with Tracked(frame_own), Tracked(regions))]
                frame.meta_mut()).prev = Some(back);

                let ghost back_idx = meta_to_index(owner.list_own.list[nn - 1].paddr);
                proof {
                    assert(0 <= nn - 1 < owner.list_own.repr_perms.len());
                }
                let tracked back_points_to = regions.slots.tracked_borrow(back_idx);
                let tracked back_slot_owner = regions.slot_owners.tracked_borrow_mut(back_idx);
                let tracked back_repr_perm = owner.list_own.repr_perms.tracked_borrow_mut(nn - 1);
                let back_meta = borrow_meta_mut(
                    back,
                    Tracked(back_points_to),
                    Tracked(back_slot_owner),
                    Tracked(back_repr_perm),
                );
                back_meta.next = Some(frame_ptr);
                self.list.back = Some(frame_ptr);
            } else {
                // EMPTY list: just point both ends at the inserted frame.
                self.list.front = Some(frame_ptr);
                self.list.back = Some(frame_ptr);
            }
        }

        #[verus_spec(with Tracked(&owner.list_own))]
        let list_id = self.list.lazy_get_id();

        proof {
            assert(owner0.list_own.list.len() > 0 ==> list_id == owner0.list_own.list_id);
        }
        let tracked frame_outer = regions.slots.tracked_borrow_mut(frame_own.slot_index);
        let tracked mut frame_so = regions.slot_owners.tracked_borrow_mut(frame_own.slot_index);
        #[verus_spec(with Tracked(frame_outer))]
        let slot = frame.slot();
        slot.in_list.store(Tracked(&mut frame_so.in_list_perm), list_id);
        proof {
            assert(regions.inv()) by {
                reveal(<MetaRegionOwners as Inv>::inv);
            };
        }

        #[verus_spec(with Tracked(&*frame_own), Tracked(regions))]
        let _ = frame.into_raw();

        self.list.size = self.list.size + 1;

        proof {
            let tracked frame_repr_perm = frame_own.repr_perm.tracked_take();
            CursorOwner::<M>::tracked_list_insert(
                owner,
                &mut frame_own.meta_own,
                frame_repr_perm,
                list_id,
            );

            let oldl = owner0.list_own;
            let nn = owner0.index as int;
            let flink = frame_own.meta_own;
            let ins = frame_own.slot_index;

            assert(owner.list_own.relate_region(*regions)) by {
                assert forall|p: int|
                    #![trigger
                        owner.list_own.insert_old_slot_post_at(
                            *regions,
                            oldl,
                            regions0,
                            nn,
                            flink,
                            p,
                        )]
                    (0 <= p < oldl.list.len()) implies owner.list_own.insert_old_slot_post_at(
                    *regions,
                    oldl,
                    regions0,
                    nn,
                    flink,
                    p,
                ) by {
                    reveal(LinkedListOwner::insert_old_slot_post_at);
                    assert(oldl.relate_region_at(regions0, p)) by {
                        reveal(LinkedListOwner::relate_region);
                    };
                    oldl.relate_region_at_facts(regions0, p);
                    if nn - 1 >= 0 && nn - 1 < oldl.list.len() && p != nn - 1 {
                        assert(meta_to_index(oldl.list[p].paddr) != meta_to_index(
                            oldl.list[nn - 1].paddr,
                        )) by {
                            reveal(LinkedListOwner::relate_region);
                        };
                    }
                    if nn >= 0 && nn < oldl.list.len() && p != nn {
                        assert(meta_to_index(oldl.list[p].paddr) != meta_to_index(
                            oldl.list[nn].paddr,
                        )) by {
                            reveal(LinkedListOwner::relate_region);
                        };
                    }
                }

                LinkedListOwner::insert_preserves_relate_region(
                    oldl,
                    regions0,
                    owner.list_own,
                    *regions,
                    nn,
                    flink,
                );
            };

            owner0.insert_owner_spec_implies_model_spec(flink, *owner);
        }
    }

    /// Provides a reference to the linked list.
    pub fn as_list(&self) -> &LinkedList<M> {
        self.list
    }
}

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> TrackDrop for LinkedList<M> {
    type State = (LinkedListOwner<M>, MetaRegionOwners);

    /// Real key: the list's `list_id`. The token carries the identity of
    /// the list it belongs to, so a token forged for one list can't be
    /// used to discharge another (the `consume_requires` key match
    /// refuses the mismatch). A multiset ledger over `list_id` is not
    /// added because every live `LinkedList` already has a unique
    /// `LinkedListOwner` in scope — the per-instance discipline is
    /// state-side, not ledger-side.
    type Obligation = DropObligation<u64>;

    open spec fn tracked_redeem_requires(self, s: Self::State) -> bool {
        true
    }

    open spec fn tracked_redeem_ensures(
        self,
        s0: Self::State,
        s1: Self::State,
        obl: Self::Obligation,
    ) -> bool {
        &&& s0 =~= s1
        &&& obl.value() == self.list_id
    }

    proof fn tracked_redeem(self, tracked s: &mut Self::State) -> (tracked obl: Self::Obligation) {
        DropObligation::tracked_mint(self.list_id)
    }

    open spec fn drop_requires(self, s: Self::State, obl: Self::Obligation) -> bool {
        &&& self.wf(s.0)
        &&& s.0.inv()
        &&& s.1.inv()
        &&& forall|i: int|
            #![trigger s.0.list[i]]
            0 <= i < s.0.list.len() ==> s.1.contains(meta_to_index(s.0.list[i].paddr))
        &&& forall|i: int|
            #![trigger s.0.list[i]]
            0 <= i < s.0.list.len() ==> {
                let idx = meta_to_index(s.0.list[i].paddr);
                s.1.contains(idx)
            }
        &&& forall|i: int|
            #![trigger s.0.list[i]]
            0 <= i < s.0.list.len() ==> {
                let idx = meta_to_index(s.0.list[i].paddr);
                s.1.slot_owners[idx].ref_count() == REF_COUNT_UNIQUE
            }
        &&& forall|i: int|
            #![trigger s.0.list[i]]
            0 <= i < s.0.list.len() ==> {
                let idx = meta_to_index(s.0.list[i].paddr);
                s.1.frame_obligations.count(idx) == 0
            }
        &&& forall|i: int|
            #![trigger s.0.list[i]]
            0 <= i < s.0.list.len() ==> {
                let idx = meta_to_index(s.0.list[i].paddr);
                s.1.slot_owners[idx].paths_in_pt.is_empty()
            }
        &&& forall|i: int, j: int|
            #![trigger s.0.list[i], s.0.list[j]]
            0 <= i < j < s.0.list.len() ==> meta_to_index(s.0.list[i].paddr) != meta_to_index(
                s.0.list[j].paddr,
            )
        &&& s.0.relate_region(s.1)
        &&& obl.value() == self.list_id
    }

    open spec fn drop_ensures(
        self,
        s0: Self::State,
        s1: Self::State,
        obl: Self::Obligation,
    ) -> bool {
        &&& s1.0.list.len() == 0
        &&& forall|i: int|
            #![trigger s0.0.list[i]]
            0 <= i < s0.0.list.len() ==> {
                let idx = meta_to_index(s0.0.list[i].paddr);
                s1.1.frame_obligations.count(idx) == s0.1.frame_obligations.count(idx)
            }
        &&& forall|idx: int|
            #![trigger s1.1.slot_owners[idx]]
            (forall|i: int|
                #![trigger s0.0.list[i]]
                0 <= i < s0.0.list.len() ==> idx != meta_to_index(s0.0.list[i].paddr)) ==> {
                &&& s1.1.frame_obligations.count(idx) == s0.1.frame_obligations.count(idx)
                &&& s1.1.slot_owners[idx].usage == s0.1.slot_owners[idx].usage
                &&& s1.1.slot_owners[idx].slot_vaddr == s0.1.slot_owners[idx].slot_vaddr
                &&& s1.1.slot_owners[idx].paths_in_pt == s0.1.slot_owners[idx].paths_in_pt
            }
        &&& s1.1.slots.dom() =~= s0.1.slots.dom()
        &&& s1.1.inv()
    }
}

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Drop for LinkedList<M> {
    #[verifier::spinoff_prover]
    fn drop(
        self,
        Tracked(s): Tracked<&mut Self::State>,
        Tracked(obl): Tracked<DropObligation<u64>>,
    ) {
        proof_decl! {
            let tracked mut list_own: LinkedListOwner<M>;
        }
        let ghost original_list = s.0.list;
        let ghost original_list_id = s.0.list_id;
        let ghost n = original_list.len();
        let ghost original_regions = s.1;
        proof {
            list_own = LinkedListOwner::<M>::tracked_take(&mut s.0);
        }
        let tracked regions: &mut MetaRegionOwners = &mut s.1;
        let mut this = self;

        #[verus_spec(with Tracked(list_own))]
        let cursor_pair = this.cursor_front_mut();
        let (mut cursor, Tracked(mut cursor_own)) = cursor_pair;

        proof {
            if n > 0 {
                cursor_own.list_own.relate_region_at_facts(*regions, 0);
                cursor_own.list_own.relate_region_at_facts(*regions, n - 1);
            }
        }

        let ghost mut k: int = 0;

        loop
            invariant_except_break
                cursor.wf_region(cursor_own, *regions),
                cursor.current.is_some() <==> k < n,
            invariant
                cursor_own.wf_with_region(*regions),
                cursor_own.list_own.list_id == original_list_id,
                cursor_own.index == 0,
                regions.inv(),
                cursor_own.list_own.list.len() == n - k,
                0 <= k <= n,
                // The remaining list is a suffix of the original
                forall|j: int|
                    #![trigger cursor_own.list_own.list[j]]
                    0 <= j < n - k ==> cursor_own.list_own.list[j] == original_list[j + k],
                // Elements already taken have their in-list obligation redeemed (count 0)
                forall|j: int|
                    #![trigger original_list[j]]
                    0 <= j < k ==> {
                        let idx = meta_to_index(original_list[j].paddr);
                        regions.frame_obligations.count(idx) == 0
                    },
                // slots values inside the original_list.
                forall|idx: int|
                    #![trigger regions.slot_owners[idx]]
                    (forall|j: int|
                        #![trigger original_list[j]]
                        0 <= j < n ==> idx != meta_to_index(original_list[j].paddr)) ==> {
                        &&& regions.frame_obligations.count(idx)
                            == original_regions.frame_obligations.count(idx)
                        &&& regions.slot_owners[idx].usage
                            == original_regions.slot_owners[idx].usage
                        &&& regions.slot_owners[idx].slot_vaddr
                            == original_regions.slot_owners[idx].slot_vaddr
                        &&& regions.slot_owners[idx].paths_in_pt
                            == original_regions.slot_owners[idx].paths_in_pt
                    },
                regions.slots.dom() == original_regions.slots.dom(),
                // `paths_in_pt.is_empty()` precondition).
                forall|j: int|
                    #![trigger original_list[j]]
                    k <= j < n ==> {
                        let idx = meta_to_index(original_list[j].paddr);
                        &&& regions.frame_obligations.count(idx)
                            == original_regions.frame_obligations.count(idx)
                        &&& regions.slot_owners[idx].paths_in_pt
                            == original_regions.slot_owners[idx].paths_in_pt
                    },
                // Each remaining element's slot is in slot_owners
                forall|j: int|
                    #![trigger original_list[j]]
                    k <= j < n ==> regions.contains(meta_to_index(original_list[j].paddr)),
                // Distinct slot indices in original list (from drop_requires)
                forall|i: int, j: int|
                    #![trigger original_list[i], original_list[j]]
                    0 <= i < j < n ==> meta_to_index(original_list[i].paddr) != meta_to_index(
                        original_list[j].paddr,
                    ),
                forall|j: int|
                    #![trigger original_list[j]]
                    0 <= j < n ==> {
                        let idx = meta_to_index(original_list[j].paddr);
                        &&& original_regions.contains(idx)
                        &&& original_regions.frame_obligations.count(idx) == 0
                        &&& original_regions.slot_owners[idx].paths_in_pt.is_empty()
                        &&& original_regions.slot_owners[idx].ref_count() == REF_COUNT_UNIQUE
                    },
            ensures
                k == n,
                cursor_own.list_own.list.len() == 0,
            decreases n - k,
        {
            #[verus_spec(with Tracked(regions), Tracked(&mut cursor_own))]
            let entry = cursor.take_current();

            if let Some(current) = entry {
                let (mut frame, frame_own_tracked) = current;
                let tracked frame_own = frame_own_tracked.get();
                let ghost regions_pre_drop = *regions;

                // Drop the frame, returning its slot to regions
                #[verus_spec(with Tracked(frame_own), Tracked(regions))]
                frame.drop();

                proof {
                    assert forall|i: int|
                        #![trigger cursor_own.list_own.list[i]]
                        0 <= i < cursor_own.list_own.list.len() implies ({
                        let idx = meta_to_index(cursor_own.list_own.list[i].paddr);
                        &&& regions.contains(idx)
                        &&& regions.slot_owners[idx] == regions_pre_drop.slot_owners[idx]
                        &&& regions.frame_obligations.count(idx)
                            == regions_pre_drop.frame_obligations.count(idx)
                    }) by {
                        let idx = meta_to_index(cursor_own.list_own.list[i].paddr);
                        let ghost _trig_k = original_list[k as int];
                        let ghost _trig_ik = original_list[i + k + 1];
                        assert(cursor_own.list_own.list[i] == original_list[i + k + 1]);

                        cursor_own.list_own.relate_region_at_facts(regions_pre_drop, i);
                    };
                    cursor_own.list_own.relate_region_preserved_external_change(
                        regions_pre_drop,
                        *regions,
                    );

                    assert forall|j: int|
                        #![trigger cursor_own.list_own.list[j]]
                        0 <= j < n - k - 1 implies cursor_own.list_own.list[j] == original_list[j
                        + k + 1] by {};

                    assert forall|j: int| #![trigger original_list[j]] 0 <= j < k implies ({
                        let idx = meta_to_index(original_list[j].paddr);
                        regions.frame_obligations.count(idx) == 0
                    }) by {
                        let ghost _a = original_list[j as int];
                        let ghost _b = original_list[k as int];
                    };

                    k = k + 1;
                }
            } else {
                break;
            }
        }

        // `s.1` is already updated in place via the re-borrow `regions`;
        // restore `s.0` to the cursor's final (empty) `list_own`.
        proof {
            let tracked mut final_list_own = cursor_own.list_own;
            vstd::modes::tracked_swap(&mut s.0, &mut final_list_own);
            final_list_own.tracked_destroy_empty();
        }
    }
}

// SAFETY: `Link<M>` is `Send` and `Sync` if `M` is `Send` and `Sync` because
// we only access these unsafe cells when the frame is not shared. This is
// enforced by `UniqueFrame`.
// #[verifier::external]
// unsafe impl<M> Send for LinkedList<M> where Link<M>: AnyFrameMeta {}
// #[verifier::external]
// unsafe impl<M> Sync for LinkedList<M> where Link<M>: AnyFrameMeta {}
/// A link in the linked list.
pub struct Link<M: AnyFrameMeta + Repr<MetaSlotSmall>> {
    pub next: Option<ReprPtr<MetaSlotStorage, Link<M>>>,
    pub prev: Option<ReprPtr<MetaSlotStorage, Link<M>>>,
    pub meta: M,
}

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Deref for Link<M> {
    type Target = M;

    fn deref(&self) -> &Self::Target {
        &self.meta
    }
}

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> DerefMut for Link<M> {
    fn deref_mut(&mut self) -> &mut Self::Target {
        &mut self.meta
    }
}

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Link<M> {
    /// Creates a new linked list metadata.
    pub const fn new(meta: M) -> Self {
        Self { next: None, prev: None, meta }
    }
}

// SAFETY: If `M::on_drop` reads the page using the provided `VmReader`,
// the safety is upheld by the one who implements `AnyFrameMeta` for `M`.
unsafe impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> AnyFrameMeta for Link<M> {
    open spec fn on_drop_pre(
        &self,
        reader: crate::mm::VmReader<'_, crate::mm::Infallible>,
        regions: crate::specs::mm::frame::meta_region_owners::MetaRegionOwners,
        vm_io_owner: crate::specs::mm::io::VmIoOwner,
    ) -> bool {
        self.meta.on_drop_pre(reader, regions, vm_io_owner)
    }

    fn on_drop(
        &mut self,
        reader: &mut crate::mm::VmReader<crate::mm::Infallible>,
        regions: Tracked<&mut crate::specs::mm::frame::meta_region_owners::MetaRegionOwners>,
        vm_io_owner: Tracked<&mut crate::specs::mm::io::VmIoOwner>,
    ) {
        self.meta.on_drop(reader, regions, vm_io_owner);
    }

    fn is_untyped(&self) -> bool {
        self.meta.is_untyped()
    }

    uninterp spec fn vtable_ptr(&self) -> usize;
}

} // verus!