Skip to main content

ostd/mm/frame/
linked_list.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Enabling linked lists of frames without heap allocation.
3//!
4//! This module leverages the customizability of the metadata system (see
5//! [super::meta]) to allow any type of frame to be used in a linked list.
6use vstd::{prelude::*, seq_lib::*, simple_pptr::*};
7use vstd_extra::{cast_ptr::*, ownership::*};
8
9use crate::specs::{
10    arch::*,
11    mm::embedding::list_store::list_registry_ok,
12    mm::frame::{
13        linked_list::linked_list_owners::*, mapping::*, meta_owners::*,
14        meta_region_owners::MetaRegionOwners, unique::UniqueFrameOwner,
15    },
16};
17
18use super::{MetaSlot, mapping, meta::AnyFrameMeta, unique::UniqueFrame};
19use crate::mm::frame::meta::{
20    META_SLOT_SIZE, REF_COUNT_UNIQUE,
21    mapping::{frame_to_meta, meta_to_frame},
22};
23use crate::mm::kspace::FRAME_METADATA_RANGE;
24use crate::{
25    arch::mm::PagingConsts,
26    mm::{Paddr, Vaddr},
27    //panic::abort,
28};
29use core::{
30    ops::{Deref, DerefMut},
31    ptr::NonNull,
32    sync::atomic::{AtomicU64, Ordering},
33};
34
35verus! {
36
37/// A linked list of frames.
38///
39/// Two key features that [`LinkedList`] is different from
40/// [`alloc::collections::LinkedList`] is that:
41///  1. It is intrusive, meaning that the links are part of the frame metadata.
42///     This allows the linked list to be used without heap allocation. But it
43///     disallows a frame to be in multiple linked lists at the same time.
44///  2. The linked list exclusively own the frames, meaning that it takes
45///     unique pointers [`UniqueFrame`]. And other bodies cannot
46///     [`from_in_use`] a frame that is inside a linked list.
47///  3. We also allow creating cursors at a specific frame, allowing $O(1)$
48///     removal without iterating through the list at a cost of some checks.
49///
50/// # Example
51///
52/// To create metadata types that allows linked list links, wrap the metadata
53/// type in [`Link`]:
54///
55/// ```rust
56/// use ostd::{
57///     mm::{frame::{linked_list::{Link, LinkedList}, Frame}, FrameAllocOptions},
58///     impl_untyped_frame_meta_for,
59/// };
60///
61/// #[derive(Debug)]
62/// struct MyMeta { mark: usize }
63///
64/// type MyFrame = Frame<Link<MyMeta>>;
65///
66/// impl_untyped_frame_meta_for!(MyMeta);
67///
68/// let alloc_options = FrameAllocOptions::new();
69/// let frame1 = alloc_options.alloc_frame_with(Link::new(MyMeta { mark: 1 })).unwrap();
70/// let frame2 = alloc_options.alloc_frame_with(Link::new(MyMeta { mark: 2 })).unwrap();
71///
72/// let mut list = LinkedList::new();
73/// list.push_front(frame1.try_into().unwrap());
74/// list.push_front(frame2.try_into().unwrap());
75///
76/// let mut cursor = list.cursor_front_mut();
77/// assert_eq!(cursor.current_meta().unwrap().mark, 2);
78/// cursor.move_next();
79/// assert_eq!(cursor.current_meta().unwrap().mark, 1);
80/// ```
81///
82/// [`from_in_use`]: super::Frame::from_in_use
83///
84/// # Verified Properties
85/// ## Verification Design
86/// The linked list is abstractly represented by a [`LinkedListOwner`]:
87/// ```rust
88/// tracked struct LinkedListOwner<M: AnyFrameMeta + Repr<MetaSlotStorage>> {
89///     pub list: Seq<LinkOwner>,
90///     pub list_id: u64,
91/// }
92/// ```
93/// The raw slot and storage permissions for each link are parked in the global
94/// [`MetaRegionOwners`], while [`LinkedListOwner`] owns the corresponding
95/// type-specific `Link<M>::ReprPerm`. Cursor accessors borrow these independent
96/// components together when projecting a `Link<M>`.
97/// ## Invariant
98/// The linked list uniquely owns the raw frames that it contains, so they cannot be used by other
99/// data structures. The frame metadata field `in_list` is equal to `list_id` for all links in the list.
100/// The per-link well-formedness against the region (pointer/permission wiring,
101/// `next`/`prev` pointer chain) is captured by
102/// [`LinkedListOwner::relate_region`] (opaque, with per-position
103/// [`LinkedListOwner::relate_region_at`]). The cursor exposes this via
104/// [`CursorOwner::wf_with_region`] and [`CursorMut::wf_region`].
105/// ## Safety
106/// A given linked list can only have one cursor at a time, so there are no data races.
107/// The `prev` and `next` fields of the metadata for each link always points to valid
108/// links in the list, so the structure is memory safe (will not read or write invalid memory).
109pub struct LinkedList<M: AnyFrameMeta + Repr<MetaSlotSmall>> {
110    pub front: Option<ReprPtr<MetaSlotStorage, Link<M>>>,
111    pub back: Option<ReprPtr<MetaSlotStorage, Link<M>>>,
112    /// The number of frames in the list.
113    pub size: usize,
114    /// A lazily initialized ID, used to check whether a frame is in the list.
115    /// 0 means uninitialized.
116    pub list_id: u64,
117}
118
119/// A cursor that can mutate the linked list links.
120///
121/// The cursor points to either a frame or the "ghost" non-element. It points
122/// to the "ghost" non-element when the cursor surpasses the back of the list.
123pub struct CursorMut<'a, M: AnyFrameMeta + Repr<MetaSlotSmall>> {
124    pub list: &'a mut LinkedList<M>,
125    pub current: Option<ReprPtr<MetaSlotStorage, Link<M>>>,
126}
127
128#[verifier::spinoff_prover]
129proof fn lemma_meta_region_inv_at(regions: MetaRegionOwners, i: int)
130    requires
131        regions.inv(),
132        regions.contains(i),
133    ensures
134        regions.slot_owners[i].inv(),
135        regions.slots[i].is_init(),
136        regions.slots[i].addr() == index_to_meta(i),
137        regions.slots[i].value().wf(regions.slot_owners[i]),
138        regions.slot_owners[i].slot_vaddr == regions.slots[i].addr(),
139{
140}
141
142/// Localizes the "no existing slot aliases the inserted frame" universal fact
143/// into its own prover query, so the `MetaRegionOwners::inv` and map-insert
144/// quantifiers do not get over-instantiated inside `insert_before`'s body.
145#[verifier::spinoff_prover]
146proof fn lemma_insert_before_slot_distinct<M: AnyFrameMeta + Repr<MetaSlotSmall>>(
147    owner0: LinkedListOwner<M>,
148    regions0: MetaRegionOwners,
149    frame_idx: int,
150    nn: int,
151)
152    requires
153        owner0.relate_region(regions0),
154        regions0.inv(),
155        regions0.contains(frame_idx),
156        regions0.slot_owners[frame_idx].in_list_perm.value() == 0,
157        0 <= nn <= owner0.list.len() as int,
158    ensures
159        forall|p: int|
160            #![trigger regions0.slot_owners[meta_to_index(owner0.list[p].slot_vaddr)]]
161            (0 <= p < owner0.list.len() as int) ==> frame_idx != meta_to_index(
162                owner0.list[p].slot_vaddr,
163            ),
164{
165    owner0.lemma_relate_region_shape(regions0);
166    assert forall|p: int|
167        #![trigger regions0.slot_owners[meta_to_index(owner0.list[p].slot_vaddr)]]
168        0 <= p < owner0.list.len() as int implies frame_idx != meta_to_index(
169        owner0.list[p].slot_vaddr,
170    ) by {
171        owner0.lemma_relate_region_at_index(regions0, p);
172        owner0.lemma_relate_region_at_facts(regions0, p);
173        if frame_idx == meta_to_index(owner0.list[p].slot_vaddr) {
174            assert(regions0.slot_owners[meta_to_index(
175                owner0.list[p].slot_vaddr,
176            )].in_list_perm.value() == owner0.list_id);
177        }
178    }
179}
180
181impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedList<M> {
182    /// Creates a new linked list.
183    pub const fn new() -> Self {
184        Self { front: None, back: None, size: 0, list_id: 0 }
185    }
186}
187
188impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Default for LinkedList<M> {
189    fn default() -> Self {
190        Self::new()
191    }
192}
193
194#[verus_verify]
195impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedList<M> {
196    /// Gets the number of frames in the linked list.
197    #[verus_spec(s =>
198        with
199            Tracked(owner): Tracked<LinkedListOwner<M>>,
200        requires
201            self.wf(owner),
202            owner.inv(),
203        ensures
204            s == owner@.list.len(),
205    )]
206    pub fn size(&self) -> usize {
207        self.size
208    }
209
210    /// Tells if the linked list is empty.
211    #[verus_spec(b =>
212        with
213            Tracked(owner): Tracked<LinkedListOwner<M>>,
214        requires
215            self.wf(owner),
216            owner.inv(),
217        ensures
218            b ==> self.size == 0 && self.front is None && self.back is None,
219            !b ==> self.size > 0 && self.front is Some && self.back is Some,
220    )]
221    pub fn is_empty(&self) -> bool {
222        let is_empty = self.size == 0;
223        is_empty
224    }
225
226    /// Pushes a frame to the front of the linked list.
227    /// # Verified Properties
228    /// ## Preconditions
229    /// The list must be well-formed, with the pointers to its links' metadata slots
230    /// matching the tracked permission objects. The new frame must be active, so that it is
231    /// valid to call `into_raw` on it inside of `insert_before`.
232    /// ## Postconditions
233    /// The new frame is inserted at the front of the list.
234    /// The list invariants are preserved.
235    /// ## Safety
236    /// See [`insert_before`] for the safety guarantees.
237    #[verus_spec(
238        with
239            Tracked(regions): Tracked<&mut MetaRegionOwners>,
240            Tracked(owner): Tracked<&mut LinkedListOwner<M>>,
241            Tracked(frame_own): Tracked<&mut UniqueFrameOwner<Link<M>>>,
242        requires
243            old(self).wf_region(*old(owner), *old(regions)),
244            old(owner).relate_region(*old(regions)),
245            frame.inv(),
246            old(frame_own).inv(),
247            frame.wf_with_region(*old(frame_own), *old(regions)),
248            frame.frame_link_inv(*old(frame_own), *old(regions)),
249            old(regions).inv(),
250        ensures
251            final(self).wf_region(*final(owner), *final(regions)),
252            final(owner).inv(),
253            final(owner).relate_region(*final(regions)),
254            final(regions).inv(),
255            final(owner).list == old(owner).list.insert(0, final(frame_own).meta_own),
256            old(owner).list_id != 0 ==> final(owner).list_id == old(owner).list_id,
257            final(owner).list_id != 0,
258            final(frame_own).meta_own.slot_vaddr == old(frame_own).meta_own.slot_vaddr,
259            final(frame_own).meta_own.in_list == final(owner).list_id,
260    )]
261    pub fn push_front(&mut self, frame: UniqueFrame<Link<M>>) {
262        let current = self.front;
263        let tracked owner0 = LinkedListOwner::tracked_take(owner);
264        let tracked mut cursor_own = CursorOwner::tracked_front_owner(owner0);
265        let mut cursor = CursorMut { list: self, current };
266
267        #[verus_spec(with Tracked(regions), Tracked(&mut cursor_own), Tracked(frame_own))]
268        cursor.insert_before(frame);
269
270        proof {
271            *owner = cursor_own.list_own;
272            owner.lemma_relate_region_implies_inv(*regions);
273        }
274    }
275
276    /// Pops a frame from the front of the linked list.
277    /// # Verified Properties
278    /// ## Preconditions
279    /// The list must be well-formed, with the pointers to its links' metadata slots
280    /// matching the tracked permission objects.
281    /// ## Postconditions
282    /// - The list invariants are preserved.
283    /// - Returns the front frame and its owner, or `None` if the list is empty.
284    /// ## Safety
285    /// See [`take_current`] for the safety guarantees.
286    #[verus_spec(r =>
287        with
288            Tracked(regions): Tracked<&mut MetaRegionOwners>,
289            Tracked(owner): Tracked<&mut LinkedListOwner<M>>,
290            -> frame_owner: Tracked<Option<UniqueFrameOwner<Link<M>>>>,
291        requires
292            old(regions).inv(),
293            old(self).wf_region(*old(owner), *old(regions)),
294            old(owner).relate_region(*old(regions)),
295        ensures
296            final(regions).inv(),
297            final(owner).inv(),
298            final(owner).relate_region(*final(regions)),
299            final(self).wf_region(*final(owner), *final(regions)),
300            final(owner).list_id == old(owner).list_id,
301            r is Some == (old(owner).list.len() > 0),
302            r is Some == frame_owner@ is Some,
303            r matches Some(frame) ==> (frame_owner@ matches Some(fo) ==> {
304                &&& final(owner).list == old(owner).list.remove(0)
305                &&& fo.meta_own@ == old(owner).list[0]@
306                &&& frame.inv()
307                &&& fo.inv()
308                &&& frame.wf(fo)
309                &&& frame.wf_with_region(fo, *final(regions))
310                &&& frame.frame_link_inv(fo, *final(regions))
311            }),
312            r is None ==> *final(owner) == *old(owner)
313                && *final(self) == *old(self) && *final(regions) == *old(regions),
314    )]
315    pub fn pop_front(&mut self) -> Option<UniqueFrame<Link<M>>> {
316        let tracked owner0 = LinkedListOwner::tracked_take(owner);
317        let tracked mut cursor_own = CursorOwner::tracked_front_owner(owner0);
318        let tracked mut returned_owner: Option<UniqueFrameOwner<Link<M>>>;
319
320        /* Restore the tracked list owner after the cursor call.
321         * Origin Rust: self.cursor_front_mut().take_current()
322         */
323        #[verus_spec(with Tracked(regions), Tracked(&mut cursor_own) => Tracked(returned_owner))]
324        let frame = self.cursor_front_mut().take_current();
325        proof! {
326            *owner = cursor_own.list_own;
327            owner.lemma_relate_region_implies_inv(*regions);
328        }
329        proof_with!(|= Tracked(returned_owner));
330        frame
331    }
332
333    /// Pushes a frame to the back of the linked list.
334    /// # Verified Properties
335    /// ## Preconditions
336    /// The list must be well-formed, with the pointers to its links' metadata slots
337    /// matching the tracked permission objects. The new frame must be active, so that it is
338    /// valid to call `into_raw` on it inside of `insert_before`.
339    /// ## Postconditions
340    /// - The new frame is inserted at the back of the list.
341    /// - The list invariants are preserved.
342    /// ## Safety
343    /// See [`insert_before`] for the safety guarantees.
344    #[verus_spec(
345        with
346            Tracked(regions): Tracked<&mut MetaRegionOwners>,
347            Tracked(owner): Tracked<&mut LinkedListOwner<M>>,
348            Tracked(frame_own): Tracked<&mut UniqueFrameOwner<Link<M>>>,
349        requires
350            old(self).wf_region(*old(owner), *old(regions)),
351            old(owner).relate_region(*old(regions)),
352            frame.inv(),
353            old(frame_own).inv(),
354            frame.wf_with_region(*old(frame_own), *old(regions)),
355            frame.frame_link_inv(*old(frame_own), *old(regions)),
356            old(regions).inv(),
357        ensures
358            final(self).wf_region(*final(owner), *final(regions)),
359            final(owner).inv(),
360            final(owner).relate_region(*final(regions)),
361            final(regions).inv(),
362            final(owner).list == old(owner).list.insert(
363                old(owner).list.len() as int, final(frame_own).meta_own),
364            // Id preserved when already minted; a fresh (empty) list adopts a
365            // non-zero id.
366            old(owner).list_id != 0 ==> final(owner).list_id == old(owner).list_id,
367            final(owner).list_id != 0,
368            final(frame_own).meta_own.slot_vaddr == old(frame_own).meta_own.slot_vaddr,
369            final(frame_own).meta_own.in_list == final(owner).list_id,
370    )]
371    pub fn push_back(&mut self, frame: UniqueFrame<Link<M>>) {
372        let tracked owner0 = LinkedListOwner::tracked_take(owner);
373        let tracked mut cursor_own = CursorOwner::tracked_cursor_mut_at_owner(
374            owner0,
375            owner0.list.len() as int,
376        );
377
378        #[verus_spec(with Tracked(regions), Tracked(&mut cursor_own), Tracked(frame_own))]
379        self.cursor_at_ghost_mut().insert_before(frame);
380
381        proof {
382            *owner = cursor_own.list_own;
383            owner.lemma_relate_region_implies_inv(*regions);
384            assert(self.wf_region(*owner, *regions));
385        }
386    }
387
388    /// Pops a frame from the back of the linked list.
389    /// # Verified Properties
390    /// ## Preconditions
391    /// - The list must be well-formed, with the pointers to its links' metadata slots
392    /// matching the tracked permission objects.
393    /// ## Postconditions
394    /// - Returns the back frame and its owner, or `None` if the list is empty.
395    /// - The list invariants are preserved.
396    /// ## Safety
397    /// See [`take_current`] for the safety guarantees.
398    #[verus_spec(r =>
399        with
400            Tracked(regions): Tracked<&mut MetaRegionOwners>,
401            Tracked(owner): Tracked<&mut LinkedListOwner<M>>,
402            -> frame_owner: Tracked<Option<UniqueFrameOwner<Link<M>>>>,
403        requires
404            old(regions).inv(),
405            old(self).wf_region(*old(owner), *old(regions)),
406            old(owner).relate_region(*old(regions)),
407        ensures
408            final(regions).inv(),
409            final(owner).inv(),
410            final(owner).relate_region(*final(regions)),
411            final(self).wf_region(*final(owner), *final(regions)),
412            final(owner).list_id == old(owner).list_id,
413            (r is Some) == (old(owner).list.len() > 0),
414            (r is Some) == (frame_owner@ is Some),
415            r matches Some(frame) ==> (frame_owner@ matches Some(fo) ==> {
416                &&& final(owner).list == old(owner).list.remove(old(owner).list.len() - 1)
417                &&& fo.meta_own@ == old(owner).list[old(owner).list.len() - 1]@
418                &&& frame.inv()
419                &&& fo.inv()
420                &&& frame.wf(fo)
421                &&& frame.wf_with_region(fo, *final(regions))
422                &&& frame.frame_link_inv(fo, *final(regions))
423            }),
424            r is None ==> *final(owner) == *old(owner)
425                && *final(self) == *old(self) && *final(regions) == *old(regions),
426    )]
427    pub fn pop_back(&mut self) -> Option<UniqueFrame<Link<M>>> {
428        let tracked owner0 = LinkedListOwner::tracked_take(owner);
429        let tracked mut cursor_own = CursorOwner::tracked_back_owner(owner0);
430        let tracked mut returned_owner: Option<UniqueFrameOwner<Link<M>>>;
431
432        /* Restore the tracked list owner after the cursor call.
433         * Origin Rust: self.cursor_back_mut().take_current()
434         */
435        #[verus_spec(with Tracked(regions), Tracked(&mut cursor_own) => Tracked(returned_owner))]
436        let frame = self.cursor_back_mut().take_current();
437        proof! {
438            *owner = cursor_own.list_own;
439            owner.lemma_relate_region_implies_inv(*regions);
440        }
441        proof_with!(|= Tracked(returned_owner));
442        frame
443    }
444
445    /// Tells if a frame is in the list.
446    /// # Verified Properties
447    /// ## Preconditions
448    /// - The list must be well-formed, with the pointers to its links' metadata slots
449    /// matching the tracked permission objects.
450    /// - The list owner must relate its links to the region permissions.
451    /// ## Postconditions
452    /// - The result is `true` exactly when the frame address is valid and its
453    /// region-owned `in_list` tag equals the list's ID after lazy initialization.
454    /// - A valid frame in the owner's list always returns `true`.
455    /// ## Safety
456    /// - `lazy_get_id` uses atomic memory accesses, so there are no data races.
457    /// - We assume that the ID allocator has an available ID if the list previously didn't have one,
458    /// but the consequence if that is not the case is a failsafe panic.
459    /// - Everything else conforms to the safe interface.
460    #[verus_spec(r =>
461        with
462            Tracked(regions): Tracked<&MetaRegionOwners>,
463            Tracked(owner): Tracked<&LinkedListOwner<M>>,
464        requires
465            regions.inv(),
466            old(self).wf(*owner),
467            owner.relate_region(*regions),
468        ensures
469            (valid_frame_paddr(frame) && exists|i: int| 0 <= i < owner.list.len()
470                && #[trigger] meta_to_index(owner.list[i].slot_vaddr) == frame_to_index(frame))
471                ==> r,
472        returns
473            valid_frame_paddr(frame)
474                && regions.slot_owners[frame_to_index(frame)].in_list_perm.value()
475                    == final(self).list_id,
476    )]
477    pub fn contains(&mut self, frame: Paddr) -> bool {
478        proof_decl! {
479        let ghost idx = frame_to_index(frame);
480            if valid_frame_paddr(frame) {
481                regions.lemma_contains_valid_frame_paddr(frame);
482                if exists|i: int| 0 <= i < owner.list.len()
483                    && #[trigger] meta_to_index(owner.list[i].slot_vaddr) == idx {
484                    let i = choose|i: int| 0 <= i < owner.list.len()
485                        && #[trigger] meta_to_index(owner.list[i].slot_vaddr) == idx;
486                    owner.lemma_relate_region_shape(*regions);
487                    owner.lemma_relate_region_at_index(*regions, i);
488                    owner.lemma_relate_region_at_facts(*regions, i);
489                }
490            }
491        let tracked slot_perm = if valid_frame_paddr(frame) {
492            Some(*regions.slots.tracked_borrow(idx))
493        } else {
494            None
495        };
496        }
497        let Ok(slot) = (#[verus_spec(with Tracked(slot_perm))]
498        crate::mm::frame::meta::get_slot(frame)) else {
499            return false;
500        };
501
502        let tracked slot_own = regions.slot_owners.tracked_borrow(idx);
503
504        slot.in_list.load(Tracked(&slot_own.in_list_perm)) == #[verus_spec(with Tracked(owner))]
505        self.lazy_get_id()
506    }
507
508    /// Gets a cursor at the specified frame if the frame is in the list.
509    ///
510    /// This method fails if the frame is not in the list.
511    /// # Verified Properties
512    /// ## Preconditions
513    /// - The list must be well-formed, with the pointers to its links' metadata slots
514    /// matching the tracked permission objects.
515    /// - The list owner must match the list and region permissions, and its
516    /// membership registry must be consistent with the region's `in_list` tags.
517    /// - The list must already have a non-zero ID: `lazy_get_id` does not yet
518    /// model freshness against the region's `in_list` tags for a fresh list.
519    /// ## Postconditions
520    /// - A cursor is returned exactly when the valid frame belongs to the list.
521    /// Its owner has an in-range index matching the frame, and the cursor is
522    /// well-formed with the region permissions.
523    /// - The returned cursor and its tracked owner are either both present or both absent.
524    /// ## Safety
525    /// - `lazy_get_id` uses atomic memory accesses, so there are no data races.
526    #[verus_spec(r =>
527        with
528            Tracked(regions): Tracked<&MetaRegionOwners>,
529            Tracked(owner): Tracked<&mut LinkedListOwner<M>>,
530            -> cursor_owner: Tracked<Option<CursorOwner<M>>>,
531        requires
532            regions.inv(),
533            old(self).wf_region(*old(owner), *regions),
534            old(owner).relate_region(*regions),
535            list_registry_ok(*regions, *old(owner)),
536            old(owner).list_id != 0,
537        ensures
538            !valid_frame_paddr(frame) ==> r is None,
539            r is Some == cursor_owner@ is Some,
540            (r is Some) == (valid_frame_paddr(frame)
541                && exists|i: int| 0 <= i < old(owner).list.len()
542                    && #[trigger] meta_to_index(old(owner).list[i].slot_vaddr) == frame_to_index(frame)),
543            r is None ==> {
544                &&& *final(owner) == *old(owner)
545                &&& *final(self) == *old(self)
546                &&& final(self).wf_region(*final(owner), *regions)
547                &&& final(owner).inv()
548            },
549            r matches Some(cursor) ==> (cursor_owner@ matches Some(co) ==> {
550                &&& co.list_own == *old(owner)
551                &&& 0 <= co.index < co.list_own.list.len()
552                &&& meta_to_index(co.list_own.list[co.index].slot_vaddr) == frame_to_index(frame)
553                &&& cursor.wf_region(co, *regions)
554                &&& co.wf_with_region(*regions)
555                &&& cursor.wf(co)
556                &&& co.inv()
557                &&& *cursor.list == *old(self)
558                &&& *final(self) == *final(cursor.list)
559            }),
560    )]
561    pub fn cursor_mut_at(&mut self, frame: Paddr) -> Option<CursorMut<'_, M>> {
562        proof_decl! {
563            owner.lemma_relate_region_implies_inv(*regions);
564            let ghost idx = frame_to_index(frame);
565            if valid_frame_paddr(frame) {
566                regions.lemma_contains_valid_frame_paddr(frame);
567            }
568
569            let tracked slot_perm = if valid_frame_paddr(frame) {
570                Some(*regions.slots.tracked_borrow(idx))
571            } else {
572                None
573            };
574        }
575        let Ok(slot) = (#[verus_spec(with Tracked(slot_perm))]
576        crate::mm::frame::meta::get_slot(frame)) else {
577            return {
578                proof_with!(|= Tracked(None));
579                None
580            };
581        };
582
583        let tracked slot_own = regions.slot_owners.tracked_borrow(idx);
584
585        let contains = slot.in_list.load(Tracked(&slot_own.in_list_perm))
586            == #[verus_spec(with Tracked(&*owner))]
587        self.lazy_get_id();
588
589        if contains {
590            proof_decl!{
591                let ghost index = choose|i: int| 0 <= i < owner.list.len()
592                    && #[trigger] meta_to_index(owner.list[i].slot_vaddr) == frame_to_index(frame);
593                owner.lemma_relate_region_at_index(*regions, index);
594                owner.lemma_relate_region_at_facts(*regions, index);
595                lemma_meta_region_inv_at(*regions, idx);
596                let tracked list_owner = LinkedListOwner::tracked_take(owner);
597                let tracked cursor_owner = CursorOwner::tracked_cursor_mut_at_owner(list_owner, index);
598            }
599
600            let meta_ptr = ReprPtr::<MetaSlotStorage, Link<M>>::from_pptr(
601                PPtr::<MetaSlotStorage>::from_addr(frame_to_meta(frame)),
602            );
603            proof_with!(|= Tracked(Some(cursor_owner)));
604            Some(CursorMut { list: self, current: Some(meta_ptr) })
605        } else {
606            proof_with!(|= Tracked(None));
607            None
608        }
609    }
610
611    /// Gets a cursor at the front that can mutate the linked list links.
612    ///
613    /// If the list is empty, the cursor points to the "ghost" non-element.
614    /// # Verified Properties
615    /// ## Safety
616    /// This function is written in safe Rust and there is no undefined behavior.
617    #[verus_spec(r =>
618        ensures
619            r.current == old(self).front,
620            *r.list == *old(self),
621            *final(self) == *final(r.list),
622    )]
623    pub fn cursor_front_mut(&mut self) -> CursorMut<'_, M> {
624        let current = self.front;
625        CursorMut { list: self, current }
626    }
627
628    /// Gets a cursor at the back that can mutate the linked list links.
629    ///
630    /// If the list is empty, the cursor points to the "ghost" non-element.
631    /// # Verified Properties
632    /// ## Safety
633    /// This function is written in safe Rust and there is no undefined behavior.
634    #[verus_spec(r =>
635        ensures
636            r.current == old(self).back,
637            *r.list == *old(self),
638            *final(self) == *final(r.list),
639    )]
640    pub fn cursor_back_mut(&mut self) -> CursorMut<'_, M> {
641        let current = self.back;
642        CursorMut { list: self, current }
643    }
644
645    /// Gets a cursor at the "ghost" non-element that can mutate the linked list links.
646    /// # Verified Properties
647    /// ## Safety
648    /// This function is written in safe Rust and there is no undefined behavior.
649    #[verus_spec(r =>
650        ensures
651            r.current.is_none(),
652            *r.list == *old(self),
653            *final(self) == *final(r.list),
654    )]
655    fn cursor_at_ghost_mut(&mut self) -> CursorMut<'_, M> {
656        CursorMut { list: self, current: None }
657    }
658
659    /// # Verification Assumption
660    /// We assume that there is an available ID for `lazy_get_id` to return.
661    /// This is safe because it will panic if the ID allocator is exhausted.
662    #[verifier::external_body]
663    #[verus_spec(
664        with Tracked(owner): Tracked<& LinkedListOwner<M>>
665    )]
666    fn lazy_get_id(&mut self) -> (id: u64)
667        ensures
668            owner.list_id != 0 ==> id == owner.list_id,
669            final(self).size == old(self).size,
670            final(self).front == old(self).front,
671            final(self).back == old(self).back,
672            old(self).list_id != 0 ==> final(self).list_id == old(self).list_id,
673            id != 0,
674            final(self).list_id == id,
675    {
676        unimplemented!()/*        // FIXME: Self-incrementing IDs may overflow, while `core::pin::Pin`
677        // is not compatible with locks. Think about a better solution.
678        static LIST_ID_ALLOCATOR: AtomicU64 = AtomicU64::new(1);
679        const MAX_LIST_ID: u64 = i64::MAX as u64;
680
681        if self.list_id == 0 {
682            let id = LIST_ID_ALLOCATOR.fetch_add(1, Ordering::Relaxed);
683            if id >= MAX_LIST_ID {
684//                log::error!("The frame list ID allocator has exhausted.");
685//                abort();
686                unimplemented!()
687            }
688            self.list_id = id;
689            id
690        } else {
691            self.list_id
692        }*/
693
694    }
695}
696
697impl<'a, M: AnyFrameMeta + Repr<MetaSlotSmall>> CursorMut<'a, M> {
698    /// Moves the cursor to the next frame towards the back.
699    ///
700    /// If the cursor is pointing to the "ghost" non-element then this will
701    /// move it to the first element of the [`LinkedList`]. If it is pointing
702    /// to the last element of the LinkedList then this will move it to the
703    /// "ghost" non-element.
704    #[verus_spec(
705        with Tracked(owner): Tracked<CursorOwner<M>>,
706            Tracked(regions): Tracked<&MetaRegionOwners>,
707    )]
708    pub fn move_next(&mut self)
709        requires
710            owner.wf_with_region(*regions),
711            old(self).wf_region(owner, *regions),
712        ensures
713            owner.move_next_owner_spec()@ == owner@.move_next_spec(),
714            owner.move_next_owner_spec().wf_with_region(*regions),
715            final(self).wf_region(owner.move_next_owner_spec(), *regions),
716    {
717        proof {
718            owner.list_own.lemma_relate_region_shape(*regions);
719            if self.current is Some {
720                owner.list_own.lemma_relate_region_at_index(*regions, owner.index);
721                owner.list_own.lemma_relate_region_at_facts(*regions, owner.index);
722            }
723            if owner.index < owner.length() - 1 {
724                owner.list_own.lemma_relate_region_at_index(*regions, owner.index + 1);
725                owner.list_own.lemma_relate_region_at_facts(*regions, owner.index + 1);
726            }
727        }
728
729        self.current = match self.current {
730            // SAFETY: The cursor is pointing to a valid element.
731            Some(current) => {
732                proof_decl!{
733                    let ghost idx = meta_to_index(current.addr());
734                    let tracked points_to = regions.slots.tracked_borrow(idx);
735                    let tracked metadata_perms =
736                        owner.list_own.metadata_perms.tracked_borrow(owner.index);
737                    let tracked repr_perm = owner.list_own.repr_perms.tracked_borrow(owner.index);
738                }
739                proof {
740                    assert(regions.contains(idx));
741                }
742                let link = borrow_meta(
743                    current,
744                    Tracked(points_to),
745                    Tracked(metadata_perms),
746                    Tracked(repr_perm),
747                );
748                link.next
749            },
750            None => self.list.front,
751        };
752
753        proof {
754            assert(owner.move_next_owner_spec()@.fore == owner@.move_next_spec().fore);
755            assert(owner.move_next_owner_spec()@.rear == owner@.move_next_spec().rear);
756        }
757    }
758
759    /// Moves the cursor to the previous frame towards the front.
760    ///
761    /// If the cursor is pointing to the "ghost" non-element then this will
762    /// move it to the last element of the [`LinkedList`]. If it is pointing
763    /// to the first element of the LinkedList then this will move it to the
764    /// "ghost" non-element.
765    #[verus_spec(
766        with Tracked(owner): Tracked<CursorOwner<M>>,
767            Tracked(regions): Tracked<&MetaRegionOwners>,
768    )]
769    pub fn move_prev(&mut self)
770        requires
771            owner.wf_with_region(*regions),
772            old(self).wf_region(owner, *regions),
773        ensures
774            owner.move_prev_owner_spec()@ == owner@.move_prev_spec(),
775            owner.move_prev_owner_spec().wf_with_region(*regions),
776            final(self).wf_region(owner.move_prev_owner_spec(), *regions),
777    {
778        proof {
779            owner.list_own.lemma_relate_region_shape(*regions);
780            if self.current is Some {
781                owner.list_own.lemma_relate_region_at_index(*regions, owner.index);
782                owner.list_own.lemma_relate_region_at_facts(*regions, owner.index);
783            }
784            if 0 < owner.index {
785                owner.list_own.lemma_relate_region_at_index(*regions, owner.index - 1);
786                owner.list_own.lemma_relate_region_at_facts(*regions, owner.index - 1);
787            }
788        }
789
790        self.current = match self.current {
791            // SAFETY: The cursor is pointing to a valid element.
792            Some(current) => {
793                proof_decl!{
794                    let ghost idx = meta_to_index(current.addr());
795                    let tracked points_to = regions.slots.tracked_borrow(idx);
796                    let tracked metadata_perms =
797                        owner.list_own.metadata_perms.tracked_borrow(owner.index);
798                    let tracked repr_perm = owner.list_own.repr_perms.tracked_borrow(owner.index);
799                }
800                proof {
801                    assert(regions.contains(idx));
802                }
803
804                let link = borrow_meta(
805                    current,
806                    Tracked(points_to),
807                    Tracked(metadata_perms),
808                    Tracked(repr_perm),
809                );
810                link.prev
811            },
812            None => self.list.back,
813        };
814
815        proof {
816            if owner@.list_model.list.len() > 0 {
817                if owner@.fore.len() > 0 {
818                    assert(owner.move_prev_owner_spec()@.fore == owner@.move_prev_spec().fore);
819                    assert(owner.move_prev_owner_spec()@.rear == owner@.move_prev_spec().rear);
820                    if owner@.rear.len() > 0 {
821                        owner.list_own.lemma_relate_region_at_index(*regions, owner.index);
822                        owner.list_own.lemma_relate_region_at_facts(*regions, owner.index);
823                    }
824                } else {
825                    owner.list_own.lemma_relate_region_at_index(*regions, owner.index);
826                    owner.list_own.lemma_relate_region_at_facts(*regions, owner.index);
827                    assert(owner.move_prev_owner_spec()@.rear == owner@.move_prev_spec().rear);
828                    assert(owner@.rear == owner@.list_model.list);
829                }
830            }
831        }
832    }
833
834    /// Gets the mutable reference to the current frame's metadata.
835    ///
836    /// # Verified Properties
837    /// ## Preconditions
838    /// The cursor must be well-formed with respect to the tracked `CursorOwner`.
839    /// ## Postconditions
840    /// If the cursor is on an element, returns `Some(&mut meta)` borrowing the
841    /// current link's metadata. The cursor state and list shape are otherwise
842    /// unchanged; the current metadata permission remains borrowed while the
843    /// returned reference is live.
844    /// ## Safety
845    /// The `&mut self` guarantees exclusive access to the cursor; the tracked
846    /// `CursorOwner` guarantees the perm for the current link is live.
847    #[verus_spec(
848        with Tracked(owner): Tracked<&'b mut CursorOwner<M>>,
849            Tracked(regions): Tracked<&'b mut MetaRegionOwners>,
850    )]
851    pub fn current_meta<'b>(&'b mut self) -> (res: Option<&'b mut M>)
852        requires
853            old(self).wf_region(*old(owner), *old(regions)),
854            old(owner).wf_with_region(*old(regions)),
855            old(regions).inv(),
856        ensures
857            final(owner).index == old(owner).index,
858            final(owner).list_own.list == old(owner).list_own.list,
859            final(owner).list_own.list_id == old(owner).list_own.list_id,
860            *final(self) == *old(self),
861            res.is_some() == (0 <= final(owner).index < final(owner).length()),
862            final(regions).slots.dom() == old(regions).slots.dom(),
863            final(regions).slot_owners.dom() == old(regions).slot_owners.dom(),
864    {
865        // Verus does not support option.map very well.
866        // self.current.map(|current| {
867        //     let link_mut = unsafe { &mut *(current.ptr.addr() as *mut Link<M>) };
868        //     &mut link_mut.meta
869        // })
870        match self.current {
871            Some(current) => {
872                proof {
873                    owner.list_own.lemma_relate_region_shape(*regions);
874                    owner.list_own.lemma_relate_region_at_index(*regions, owner.index);
875                    owner.list_own.lemma_relate_region_at_facts(*regions, owner.index);
876                }
877                let ghost idx = meta_to_index(current.addr());
878                proof {
879                    assert(regions.contains(idx));
880                }
881                let tracked points_to = regions.slots.tracked_borrow(idx);
882                let tracked repr_perm = owner.list_own.repr_perms.tracked_borrow_mut(owner.index);
883                let tracked metadata_perms = owner.list_own.metadata_perms.tracked_borrow_mut(
884                    owner.index,
885                );
886                Some(
887                    &mut borrow_meta_mut(
888                        current,
889                        Tracked(points_to),
890                        Tracked(metadata_perms),
891                        Tracked(repr_perm),
892                    ).meta,
893                )
894            },
895            None => None,
896        }
897    }
898
899    /// Takes the current pointing frame out of the linked list.
900    ///
901    /// If successful, the frame is returned and the cursor is moved to the
902    /// next frame. If the cursor is pointing to the back of the list then it
903    /// is moved to the "ghost" non-element.
904    /// # Verified Properties
905    /// ## Preconditions
906    /// The cursor must be well-formed, with the pointers to its links' metadata slots
907    /// matching the tracked permission objects.
908    /// ## Postconditions
909    /// At an element, returns the frame, transfers its owner through the tracked output,
910    /// and moves the cursor to the next frame. At the ghost non-element, returns `None`
911    /// without changing the cursor, list owner, or region permissions.
912    /// ## Safety
913    /// This function calls `from_raw` on the frame, but we guarantee that the frame is forgotten
914    /// if it is in the list. So, double-free will not occur. All loads and stores are through track
915    /// tracked permissions, so there are no illegal memory accesses. No data races are possible.
916    #[verus_spec(res =>
917        with
918            Tracked(regions): Tracked<&mut MetaRegionOwners>,
919            Tracked(owner): Tracked<&mut CursorOwner<M>>,
920            -> returned_owner: Tracked<Option<UniqueFrameOwner<Link<M>>>>,
921
922        requires
923            old(self).wf_region(*old(owner), *old(regions)),
924            old(owner).wf_with_region(*old(regions)),
925            old(regions).inv(),
926        ensures
927            (res is Some) == (returned_owner@ is Some),
928            old(owner).length() == 0 ==> res.is_none(),
929            old(self).current.is_some() ==> res.is_some(),
930            final(owner).wf_with_region(*final(regions)),
931            final(self).wf_region(*final(owner), *final(regions)),
932            *final(final(self).list) == *final(old(self).list),
933            final(regions).inv(),
934            final(owner).list_own.list_id == old(owner).list_own.list_id,
935            res is None ==> {
936                &&& *final(self) == *old(self)
937                &&& *final(owner) == *old(owner)
938                &&& *final(regions) == *old(regions)
939            },
940            res matches Some(unique) ==> {
941                let paddr = meta_to_frame(old(self).current->0.addr());
942                let idx = frame_to_index(paddr);
943                let metadata_perm = unique.tracked_metadata_perm@->0;
944                &&& final(owner)@ == old(owner)@.remove()
945                &&& final(owner).index == old(owner).index
946                &&& final(owner).list_own.list == old(owner).list_own.list.remove(old(owner).index)
947                &&& final(regions).slots.dom() == old(regions).slots.dom()
948                &&& final(regions).ref_count(idx) == REF_COUNT_UNIQUE
949                &&& final(regions).slot_owners[idx].in_list_perm.value() == 0
950                &&& metadata_perm.storage_perm.is_init()
951                &&& metadata_perm.vtable_ptr_perm.is_init()
952                &&& final(regions).slot_owners[idx].slot_vaddr == index_to_meta(idx)
953                &&& final(regions).slot_owners[idx].paths_in_pt == old(regions).slot_owners[idx].paths_in_pt
954                &&& *final(regions) == old(regions).insert_slot_owner(
955                    paddr, final(regions).slot_owners[idx],
956                )
957                &&& unique.inv()
958                &&& unique.ptr.addr() == old(self).current->0.addr()
959                &&& returned_owner@ matches Some(unique_owner) ==> {
960                    &&& unique_owner.meta_own@ == old(owner).list_own.list[old(owner).index]@
961                    &&& unique.frame_link_inv(unique_owner, *final(regions))
962                    &&& unique.wf(unique_owner)
963                    &&& unique_owner.inv()
964                    &&& unique.wf_with_region(unique_owner, *final(regions))
965                    &&& unique_owner.slot_index == idx
966                }
967            },
968    )]
969    #[verifier::spinoff_prover]
970    #[verifier::rlimit(250)]
971    pub fn take_current(&mut self) -> Option<UniqueFrame<Link<M>>> {
972        hide(MetaSlotOwner::storage_perm);
973        hide(MetaSlotOwner::vtable_ptr_perm);
974        hide(<MetaRegionOwners as Inv>::inv);
975        let ghost owner0 = *owner;
976        let ghost regions0 = *regions;
977
978        /* Ghost returns need an explicit owner on the early-return path.
979         * Origin Rust: let current = self.current?;
980         */
981        let current = match self.current {
982            Some(current) => current,
983            None => return {
984                proof_with!(|= Tracked(None));
985                None
986            },
987        };
988
989        proof {
990            owner.list_own.lemma_relate_region_shape(*regions);
991            owner.list_own.lemma_relate_region_at_index(*regions, owner.index);
992            owner.list_own.lemma_relate_region_at_facts(*regions, owner.index);
993            if owner.index > 0 {
994                owner.list_own.lemma_relate_region_at_index(*regions, owner.index - 1);
995                owner.list_own.lemma_relate_region_at_facts(*regions, owner.index - 1);
996            }
997            if owner.index < owner.list_own.list.len() - 1 {
998                owner.list_own.lemma_relate_region_at_index(*regions, owner.index + 1);
999                owner.list_own.lemma_relate_region_at_facts(*regions, owner.index + 1);
1000            }
1001        }
1002
1003        let meta_ptr = current.addr();
1004        let paddr = meta_to_frame(meta_ptr);
1005        let ghost idx = frame_to_index(paddr);
1006
1007        proof {
1008            lemma_meta_region_inv_at(regions0, idx);
1009        }
1010
1011        let tracked mut cur_own = owner.list_own.list.tracked_remove(owner.index);
1012        let tracked cur_repr_perm = owner.list_own.repr_perms.tracked_remove(owner.index);
1013        let tracked cur_metadata_perm = owner.list_own.metadata_perms.tracked_remove(owner.index);
1014
1015        proof_decl! {
1016            let tracked mut frame_own: UniqueFrameOwner<Link<M>>;
1017        }
1018        let mut frame = unsafe {
1019            // SAFETY: The frame was forgotten when inserted into the linked list.
1020            #[verus_spec(with
1021                Tracked(regions.tracked_borrow_slot(paddr)),
1022                Tracked(cur_own),
1023                Tracked(cur_repr_perm),
1024                Tracked(cur_metadata_perm) => Tracked(frame_own)
1025            )]
1026            UniqueFrame::<Link<M>>::from_raw(paddr)
1027        };
1028
1029        proof {
1030            assert(regions.slots.dom() == regions0.slots.dom());
1031        }
1032
1033        let next_ptr = (#[verus_spec(with Tracked(&frame_own))]
1034        frame.meta()).next;
1035        let prev_ptr = (#[verus_spec(with Tracked(&frame_own))]
1036        frame.meta()).prev;
1037
1038        if let Some(prev) = prev_ptr {
1039            let ghost prev_idx = meta_to_index(owner.list_own.list[owner.index - 1].slot_vaddr);
1040            proof {
1041                lemma_meta_region_inv_at(*regions, prev_idx);
1042            }
1043            let tracked prev_points_to = regions.slots.tracked_borrow(prev_idx);
1044            let tracked prev_repr_perm = owner.list_own.repr_perms.tracked_borrow_mut(
1045                owner.index - 1,
1046            );
1047            let tracked prev_metadata_perm = owner.list_own.metadata_perms.tracked_borrow_mut(
1048                owner.index - 1,
1049            );
1050            let prev_meta = borrow_meta_mut(
1051                prev,
1052                Tracked(prev_points_to),
1053                Tracked(prev_metadata_perm),
1054                Tracked(prev_repr_perm),
1055            );
1056            prev_meta.next = next_ptr;
1057
1058        } else {
1059            self.list.front = next_ptr;
1060        }
1061
1062        if let Some(next) = next_ptr {
1063            let ghost next_idx = meta_to_index(owner.list_own.list[owner.index].slot_vaddr);
1064            proof {
1065                lemma_meta_region_inv_at(*regions, next_idx);
1066            }
1067            let tracked next_points_to = regions.slots.tracked_borrow(next_idx);
1068            let tracked next_repr_perm = owner.list_own.repr_perms.tracked_borrow_mut(owner.index);
1069            let tracked next_metadata_perm = owner.list_own.metadata_perms.tracked_borrow_mut(
1070                owner.index,
1071            );
1072            let next_meta = borrow_meta_mut(
1073                next,
1074                Tracked(next_points_to),
1075                Tracked(next_metadata_perm),
1076                Tracked(next_repr_perm),
1077            );
1078            next_meta.prev = prev_ptr;
1079
1080            self.current = Some(next);
1081        } else {
1082            self.list.back = prev_ptr;
1083
1084            self.current = None;
1085        }
1086
1087        (#[verus_spec(with Tracked(&mut frame_own))]
1088        frame.meta_mut()).next = None;
1089        (#[verus_spec(with Tracked(&mut frame_own))]
1090        frame.meta_mut()).prev = None;
1091
1092        let tracked mut frame_so = regions.slot_owners.tracked_borrow_mut(idx);
1093        let tracked mut fip = &mut frame_so;
1094        let slot = frame.slot();
1095        slot.in_list.store(Tracked(&mut fip.in_list_perm), 0);
1096        proof {
1097            assert(regions.inv()) by {
1098                reveal(MetaSlotOwner::storage_perm);
1099                reveal(MetaSlotOwner::vtable_ptr_perm);
1100                reveal(<MetaRegionOwners as Inv>::inv);
1101            };
1102            assert(regions.slots.dom() == regions0.slots.dom());
1103        }
1104
1105        self.list.size -= 1;
1106
1107        proof {
1108            owner0.remove_owner_spec_implies_model_spec(*owner);
1109            let ghost oldl = owner0.list_own;
1110            let ghost nn = owner0.index as int;
1111            assert forall|p: int|
1112                #![trigger meta_to_index(oldl.list[p].slot_vaddr)]
1113                (0 <= p < oldl.list.len() && p != nn) implies ({
1114                let i = meta_to_index(oldl.list[p].slot_vaddr);
1115                let np = if p < nn {
1116                    p
1117                } else {
1118                    p - 1
1119                };
1120                let fp = owner.list_own.meta_value_at(*regions, np);
1121                &&& regions.contains(i)
1122                &&& regions.slots[i].addr() == oldl.list[p].slot_vaddr
1123                &&& regions.slots[i].pptr() == regions0.slots[i].pptr()
1124                &&& regions.ref_count(i) == REF_COUNT_UNIQUE
1125                &&& regions.slot_owners[i].metadata_perm.is_resource_vacant()
1126                &&& owner.list_own.metadata_perms[np].storage_perm.id()
1127                    == regions.slots[i].value().storage.id()
1128                &&& owner.list_own.metadata_perms[np].vtable_ptr_perm.pptr()
1129                    == regions.slots[i].value().vtable_ptr
1130                &&& owner.list_own.metadata_perms[np].vtable_ptr_perm.is_init()
1131                &&& regions.slot_owners[i].usage is Frame
1132                &&& regions.slot_owners[i].in_list_perm.value() == owner.list_own.list_id
1133                &&& owner.list_own.meta_wf_at(*regions, np)
1134                &&& regions.slots[i].addr() % META_SLOT_SIZE == 0
1135                &&& FRAME_METADATA_RANGE.start <= regions.slots[i].addr()
1136                    < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
1137                &&& (p == nn - 1 ==> fp.next == oldl.meta_value_at(regions0, nn).next)
1138                &&& (p != nn - 1 ==> fp.next == oldl.meta_value_at(regions0, p).next)
1139                &&& (p == nn + 1 ==> fp.prev == oldl.meta_value_at(regions0, nn).prev)
1140                &&& (p != nn + 1 ==> fp.prev == oldl.meta_value_at(regions0, p).prev)
1141            }) by {
1142                let i = meta_to_index(oldl.list[p].slot_vaddr);
1143                let np = if p < nn {
1144                    p
1145                } else {
1146                    p - 1
1147                };
1148                let fp = owner.list_own.meta_value_at(*regions, np);
1149                oldl.lemma_relate_region_at_index(regions0, p);
1150                oldl.lemma_relate_region_at_index(regions0, nn);
1151                oldl.lemma_relate_region_indices_distinct(regions0, p, nn);
1152                oldl.lemma_relate_region_at_facts(regions0, p);
1153                oldl.lemma_relate_region_at_facts(regions0, nn);
1154                assert(regions.contains(i));
1155            }
1156            LinkedListOwner::lemma_pop_preserves_relate_region(
1157                oldl,
1158                regions0,
1159                owner.list_own,
1160                *regions,
1161                nn,
1162            );
1163        }
1164        proof_with!(|= Tracked(Some(frame_own)));
1165        Some(frame)
1166    }
1167
1168    /// Inserts a frame before the current frame.
1169    ///
1170    /// If the cursor is pointing at the "ghost" non-element then the new
1171    /// element is inserted at the back of the [`LinkedList`].
1172    /// # Verified Properties
1173    /// ## Preconditions
1174    /// The cursor must be well-formed, with the pointers to its links' metadata slots matching the tracked permission objects.
1175    /// - The new frame must be active, so that it is valid to call `into_raw` on it.
1176    /// ## Postconditions
1177    /// - The new frame is inserted into the list, immediately before the current index.
1178    /// - The list invariants are preserved.
1179    /// ## Safety
1180    /// - This function calls `into_raw` on the frame, so the caller must ensure that the frame is active and
1181    /// has not been forgotten already to avoid a memory leak. If the caller attempts to insert a forgotten frame,
1182    /// the invariant around `into_raw` and `from_raw` will be violated. But, it is the safe failure case in that
1183    /// it will not cause a double-free. (Note: we should be able to move this requirement into the `UniqueFrame` invariants.)
1184    #[verus_spec(
1185        with Tracked(regions): Tracked<&mut MetaRegionOwners>,
1186            Tracked(owner): Tracked<&mut CursorOwner<M>>,
1187            Tracked(frame_own): Tracked<&mut UniqueFrameOwner<Link<M>>>
1188    )]
1189    #[verifier::spinoff_prover]
1190    #[verifier::rlimit(200)]
1191    pub fn insert_before(&mut self, mut frame: UniqueFrame<Link<M>>)
1192        requires
1193            old(self).wf_region(*old(owner), *old(regions)),
1194            old(owner).wf_with_region(*old(regions)),
1195            old(regions).inv(),
1196            frame.inv(),
1197            old(frame_own).inv(),
1198            frame.wf_with_region(*old(frame_own), *old(regions)),
1199            frame.frame_link_inv(*old(frame_own), *old(regions)),
1200        ensures
1201            final(owner).wf_with_region(*final(regions)),
1202            final(self).wf_region(*final(owner), *final(regions)),
1203            *final(final(self).list) == *final(old(self).list),
1204            final(regions).inv(),
1205            final(owner).list_own.list == old(owner).list_own.list.insert(
1206                old(owner).index,
1207                final(frame_own).meta_own,
1208            ),
1209            // The id is preserved when it was already minted; a `list_id == 0`
1210            // (necessarily empty) list adopts a freshly-minted non-zero id.
1211            old(owner).list_own.list_id != 0 ==> final(owner).list_own.list_id == old(
1212                owner,
1213            ).list_own.list_id,
1214            final(owner).list_own.list_id != 0,
1215            final(owner).index == old(owner).index + 1,
1216            final(frame_own).meta_own.slot_vaddr == old(frame_own).meta_own.slot_vaddr,
1217            final(frame_own).meta_own.in_list == final(owner).list_own.list_id,
1218            final(owner)@ == old(owner)@.insert(final(frame_own).meta_own@),
1219    {
1220        hide(<MetaRegionOwners as Inv>::inv);
1221        let ghost owner0 = *owner;
1222        let ghost regions0 = *regions;
1223        let ghost nn = owner.index as int;
1224
1225        proof {
1226            assert(owner0.list_own.repr_perms.len() == owner0.list_own.list.len()) by {
1227                reveal(LinkedListOwner::relate_region);
1228            };
1229            assert(owner0.list_own.metadata_perms.len() == owner0.list_own.list.len()) by {
1230                reveal(LinkedListOwner::relate_region);
1231            };
1232            assert(owner0.list_own.list.len() > 0 ==> owner0.list_own.list_id != 0) by {
1233                reveal(LinkedListOwner::relate_region);
1234            };
1235            lemma_meta_region_inv_at(regions0, frame_own.slot_index);
1236            owner0.list_own.lemma_length_lt_usize_max(regions0);
1237            if nn > 0 {
1238                assert(owner0.list_own.relate_region_at(regions0, nn - 1)) by {
1239                    reveal(LinkedListOwner::relate_region);
1240                };
1241                owner.list_own.lemma_relate_region_at_facts(*regions, nn - 1);
1242                lemma_meta_region_inv_at(
1243                    regions0,
1244                    meta_to_index(owner0.list_own.list[nn - 1].slot_vaddr),
1245                );
1246            }
1247            if nn < owner.list_own.list.len() {
1248                assert(owner0.list_own.relate_region_at(regions0, nn)) by {
1249                    reveal(LinkedListOwner::relate_region);
1250                };
1251                owner.list_own.lemma_relate_region_at_facts(*regions, nn);
1252                lemma_meta_region_inv_at(
1253                    regions0,
1254                    meta_to_index(owner0.list_own.list[nn].slot_vaddr),
1255                );
1256            }
1257            assert forall|p: int|
1258                #![trigger
1259                    regions0.slot_owners[meta_to_index(owner0.list_own.list[p].slot_vaddr)]]
1260                0 <= p < owner0.list_own.list.len() implies frame_own.slot_index != meta_to_index(
1261                owner0.list_own.list[p].slot_vaddr,
1262            ) by {
1263                lemma_insert_before_slot_distinct(
1264                    owner0.list_own,
1265                    regions0,
1266                    frame_own.slot_index,
1267                    nn,
1268                );
1269            }
1270        }
1271
1272        let frame_ptr = ReprPtr::<MetaSlotStorage, Link<M>>::from_pptr(
1273            PPtr::<MetaSlotStorage>::from_addr(frame.ptr.addr()),
1274        );
1275
1276        if let Some(current) = self.current {
1277            proof_decl!{
1278                let ghost idx = meta_to_index(current.addr());
1279                let tracked points_to = regions.slots.tracked_borrow(idx);
1280                let tracked metadata_perms =
1281                    owner.list_own.metadata_perms.tracked_borrow(owner.index);
1282                let tracked repr_perm = owner.list_own.repr_perms.tracked_borrow(owner.index);
1283            }
1284
1285            // Read current's prev pointer.
1286            let opt_prev_link: Option<ReprPtr<MetaSlotStorage, Link<M>>> = borrow_meta(
1287                current,
1288                Tracked(points_to),
1289                Tracked(metadata_perms),
1290                Tracked(repr_perm),
1291            ).prev;
1292
1293            if let Some(prev_link) = opt_prev_link {
1294                let prev = prev_link;
1295
1296                (#[verus_spec(with Tracked(frame_own))]
1297                frame.meta_mut()).prev = Some(prev_link);
1298                (#[verus_spec(with Tracked(frame_own))]
1299                frame.meta_mut()).next = Some(current);
1300
1301                let ghost prev_idx = meta_to_index(owner.list_own.list[nn - 1].slot_vaddr);
1302                proof {
1303                    assert(prev_idx != idx) by {
1304                        reveal(LinkedListOwner::relate_region);
1305                    };
1306                }
1307                let tracked prev_points_to = regions.slots.tracked_borrow(prev_idx);
1308                let tracked prev_repr_perm = owner.list_own.repr_perms.tracked_borrow_mut(nn - 1);
1309                let tracked prev_metadata_perm = owner.list_own.metadata_perms.tracked_borrow_mut(
1310                    nn - 1,
1311                );
1312                let prev_meta = borrow_meta_mut(
1313                    prev,
1314                    Tracked(prev_points_to),
1315                    Tracked(prev_metadata_perm),
1316                    Tracked(prev_repr_perm),
1317                );
1318                prev_meta.next = Some(frame_ptr);
1319
1320                let ghost current_idx = meta_to_index(owner.list_own.list[nn].slot_vaddr);
1321                let tracked current_points_to = regions.slots.tracked_borrow(current_idx);
1322                let tracked current_repr_perm = owner.list_own.repr_perms.tracked_borrow_mut(nn);
1323                let tracked current_metadata_perm =
1324                    owner.list_own.metadata_perms.tracked_borrow_mut(nn);
1325                let current_meta = borrow_meta_mut(
1326                    current,
1327                    Tracked(current_points_to),
1328                    Tracked(current_metadata_perm),
1329                    Tracked(current_repr_perm),
1330                );
1331                current_meta.prev = Some(frame_ptr);
1332            } else {
1333                (#[verus_spec(with Tracked(frame_own))]
1334                frame.meta_mut()).next = Some(current);
1335
1336                let ghost current_idx = meta_to_index(owner.list_own.list[nn].slot_vaddr);
1337                let tracked current_points_to = regions.slots.tracked_borrow(current_idx);
1338                let tracked current_repr_perm = owner.list_own.repr_perms.tracked_borrow_mut(nn);
1339                let tracked current_metadata_perm =
1340                    owner.list_own.metadata_perms.tracked_borrow_mut(nn);
1341                let current_meta = borrow_meta_mut(
1342                    current,
1343                    Tracked(current_points_to),
1344                    Tracked(current_metadata_perm),
1345                    Tracked(current_repr_perm),
1346                );
1347                current_meta.prev = Some(frame_ptr);
1348                self.list.front = Some(frame_ptr);
1349            }
1350        } else {
1351            if let Some(back) = self.list.back {
1352                (#[verus_spec(with Tracked(frame_own))]
1353                frame.meta_mut()).prev = Some(back);
1354
1355                let ghost back_idx = meta_to_index(owner.list_own.list[nn - 1].slot_vaddr);
1356                proof {
1357                    assert(0 <= nn - 1 < owner.list_own.repr_perms.len());
1358                }
1359                let tracked back_points_to = regions.slots.tracked_borrow(back_idx);
1360                let tracked back_repr_perm = owner.list_own.repr_perms.tracked_borrow_mut(nn - 1);
1361                let tracked back_metadata_perm = owner.list_own.metadata_perms.tracked_borrow_mut(
1362                    nn - 1,
1363                );
1364                let back_meta = borrow_meta_mut(
1365                    back,
1366                    Tracked(back_points_to),
1367                    Tracked(back_metadata_perm),
1368                    Tracked(back_repr_perm),
1369                );
1370                back_meta.next = Some(frame_ptr);
1371                self.list.back = Some(frame_ptr);
1372            } else {
1373                // EMPTY list: just point both ends at the inserted frame.
1374                self.list.front = Some(frame_ptr);
1375                self.list.back = Some(frame_ptr);
1376            }
1377        }
1378
1379        #[verus_spec(with Tracked(&owner.list_own))]
1380        let list_id = self.list.lazy_get_id();
1381
1382        proof {
1383            assert(owner0.list_own.list.len() > 0 ==> list_id == owner0.list_own.list_id);
1384        }
1385        let tracked mut frame_so = regions.slot_owners.tracked_borrow_mut(frame_own.slot_index);
1386        let tracked mut fip = &mut frame_so;
1387        let slot = frame.slot();
1388        slot.in_list.store(Tracked(&mut fip.in_list_perm), list_id);
1389        proof {
1390            assert(regions.inv()) by {
1391                reveal(<MetaRegionOwners as Inv>::inv);
1392            };
1393            assert(frame.wf_with_region(*frame_own, *regions));
1394        }
1395
1396        #[verus_spec(with
1397            => Tracked(frame_metadata_perm)
1398        )]
1399        let _ = frame.into_raw();
1400
1401        self.list.size += 1;
1402
1403        proof {
1404            let tracked frame_repr_perm = frame_own.repr_perm.tracked_take();
1405            let ghost insert_index = owner.index;
1406            let ghost slot_vaddr = frame_own.meta_own.slot_vaddr;
1407            let tracked list_entry = LinkOwner { slot_vaddr, in_list: list_id };
1408            owner.list_own.list.tracked_insert(insert_index, list_entry);
1409            owner.list_own.repr_perms.tracked_insert(insert_index, frame_repr_perm);
1410            owner.list_own.metadata_perms.tracked_insert(insert_index, frame_metadata_perm);
1411            owner.list_own.list_id = list_id;
1412            owner.index = insert_index + 1;
1413            frame_own.meta_own = LinkOwner { slot_vaddr, in_list: list_id };
1414            let oldl = owner0.list_own;
1415            let nn = owner0.index as int;
1416            let flink = frame_own.meta_own;
1417            let ins = frame_own.slot_index;
1418
1419            assert(owner.list_own.relate_region(*regions)) by {
1420                assert forall|p: int|
1421                    #![trigger
1422                        owner.list_own.insert_old_slot_post_at(
1423                            *regions,
1424                            oldl,
1425                            regions0,
1426                            nn,
1427                            flink,
1428                            p,
1429                        )]
1430                    (0 <= p < oldl.list.len()) implies owner.list_own.insert_old_slot_post_at(
1431                    *regions,
1432                    oldl,
1433                    regions0,
1434                    nn,
1435                    flink,
1436                    p,
1437                ) by {
1438                    reveal(LinkedListOwner::insert_old_slot_post_at);
1439                    assert(oldl.relate_region_at(regions0, p)) by {
1440                        reveal(LinkedListOwner::relate_region);
1441                    };
1442                    oldl.lemma_relate_region_at_facts(regions0, p);
1443                    if nn - 1 >= 0 && nn - 1 < oldl.list.len() && p != nn - 1 {
1444                        assert(meta_to_index(oldl.list[p].slot_vaddr) != meta_to_index(
1445                            oldl.list[nn - 1].slot_vaddr,
1446                        )) by {
1447                            reveal(LinkedListOwner::relate_region);
1448                        };
1449                    }
1450                    if nn >= 0 && nn < oldl.list.len() && p != nn {
1451                        assert(meta_to_index(oldl.list[p].slot_vaddr) != meta_to_index(
1452                            oldl.list[nn].slot_vaddr,
1453                        )) by {
1454                            reveal(LinkedListOwner::relate_region);
1455                        };
1456                    }
1457                }
1458
1459                LinkedListOwner::lemma_insert_preserves_relate_region(
1460                    oldl,
1461                    regions0,
1462                    owner.list_own,
1463                    *regions,
1464                    nn,
1465                    flink,
1466                );
1467            };
1468
1469            owner0.insert_owner_spec_implies_model_spec(flink, *owner);
1470        }
1471    }
1472
1473    /// Provides a reference to the linked list.
1474    pub fn as_list(&self) -> &LinkedList<M> {
1475        self.list
1476    }
1477}
1478
1479impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedList<M> {
1480    /// Releases every frame owned by the list.
1481    ///
1482    /// # Verified Properties
1483    /// Requires matching list ownership and region permissions, with every list
1484    /// frame uniquely owned and absent from page tables.
1485    /// Empties the list owner, preserves the region invariant, and leaves unrelated
1486    /// frames' usage, metadata addresses, and page-table ownership unchanged.
1487    #[verifier::spinoff_prover]
1488    pub fn drop(
1489        mut self,
1490        Tracked(owner): Tracked<&mut LinkedListOwner<M>>,
1491        Tracked(regions): Tracked<&mut MetaRegionOwners>,
1492    )
1493        requires
1494            self.wf(*old(owner)),
1495            old(owner).inv(),
1496            old(regions).inv(),
1497            forall|i: int|
1498                #![trigger old(owner).list[i]]
1499                0 <= i < old(owner).list.len() ==> {
1500                    let idx = meta_to_index(old(owner).list[i].slot_vaddr);
1501                    &&& old(regions).contains(idx)
1502                    &&& old(regions).ref_count(idx) == REF_COUNT_UNIQUE
1503                    &&& old(regions).slot_owners[idx].paths_in_pt.is_empty()
1504                },
1505            forall|i: int, j: int|
1506                #![trigger old(owner).list[i], old(owner).list[j]]
1507                0 <= i < j < old(owner).list.len() ==> meta_to_index(old(owner).list[i].slot_vaddr)
1508                    != meta_to_index(old(owner).list[j].slot_vaddr),
1509            old(owner).relate_region(*old(regions)),
1510        ensures
1511            final(owner).list.len() == 0,
1512            forall|idx: int|
1513                #![trigger final(regions).slot_owners[idx]]
1514                (forall|i: int|
1515                    #![trigger old(owner).list[i]]
1516                    0 <= i < old(owner).list.len() ==> idx != meta_to_index(
1517                        old(owner).list[i].slot_vaddr,
1518                    )) ==> {
1519                    &&& final(regions).slot_owners[idx].usage == old(regions).slot_owners[idx].usage
1520                    &&& final(regions).slot_owners[idx].slot_vaddr == old(
1521                        regions,
1522                    ).slot_owners[idx].slot_vaddr
1523                    &&& final(regions).slot_owners[idx].paths_in_pt == old(
1524                        regions,
1525                    ).slot_owners[idx].paths_in_pt
1526                },
1527            final(regions).slots.dom() =~= old(regions).slots.dom(),
1528            final(regions).inv(),
1529    {
1530        proof_decl! {
1531            let tracked mut list_own: LinkedListOwner<M>;
1532        }
1533        let ghost original_list = owner.list;
1534        let ghost original_list_id = owner.list_id;
1535        let ghost n = original_list.len();
1536        let ghost original_regions = *regions;
1537        proof {
1538            list_own = LinkedListOwner::<M>::tracked_take(owner);
1539        }
1540
1541        let tracked mut cursor_own = CursorOwner::tracked_front_owner(list_own);
1542        let mut cursor = self.cursor_front_mut();
1543
1544        proof {
1545            if n > 0 {
1546                cursor_own.list_own.lemma_relate_region_at_index(*regions, 0);
1547                cursor_own.list_own.lemma_relate_region_at_index(*regions, n - 1);
1548                cursor_own.list_own.lemma_relate_region_at_facts(*regions, 0);
1549                cursor_own.list_own.lemma_relate_region_at_facts(*regions, n - 1);
1550            }
1551        }
1552
1553        let ghost mut k: int = 0;
1554
1555        loop
1556            invariant_except_break
1557                cursor.wf_region(cursor_own, *regions),
1558                cursor.current.is_some() <==> k < n,
1559            invariant
1560                cursor_own.wf_with_region(*regions),
1561                cursor_own.list_own.list_id == original_list_id,
1562                cursor_own.index == 0,
1563                regions.inv(),
1564                cursor_own.list_own.list.len() == n - k,
1565                0 <= k <= n,
1566                // The remaining list is a suffix of the original
1567                forall|j: int|
1568                    #![trigger cursor_own.list_own.list[j]]
1569                    0 <= j < n - k ==> cursor_own.list_own.list[j] == original_list[j + k],
1570                // slots values inside the original_list.
1571                forall|idx: int|
1572                    #![trigger regions.slot_owners[idx]]
1573                    (forall|j: int|
1574                        #![trigger original_list[j]]
1575                        0 <= j < n ==> idx != meta_to_index(original_list[j].slot_vaddr)) ==> {
1576                        &&& regions.slot_owners[idx].usage
1577                            == original_regions.slot_owners[idx].usage
1578                        &&& regions.slot_owners[idx].slot_vaddr
1579                            == original_regions.slot_owners[idx].slot_vaddr
1580                        &&& regions.slot_owners[idx].paths_in_pt
1581                            == original_regions.slot_owners[idx].paths_in_pt
1582                    },
1583                regions.slots.dom() == original_regions.slots.dom(),
1584                forall|j: int|
1585                    #![trigger original_list[j]]
1586                    k <= j < n ==> {
1587                        let idx = meta_to_index(original_list[j].slot_vaddr);
1588                        &&& regions.slot_owners[idx].paths_in_pt
1589                            == original_regions.slot_owners[idx].paths_in_pt
1590                    },
1591                // Each remaining element's slot is in slot_owners
1592                forall|j: int|
1593                    #![trigger original_list[j]]
1594                    k <= j < n ==> regions.contains(meta_to_index(original_list[j].slot_vaddr)),
1595                forall|i: int, j: int|
1596                    #![trigger original_list[i], original_list[j]]
1597                    0 <= i < j < n ==> meta_to_index(original_list[i].slot_vaddr) != meta_to_index(
1598                        original_list[j].slot_vaddr,
1599                    ),
1600                forall|j: int|
1601                    #![trigger original_list[j]]
1602                    0 <= j < n ==> {
1603                        let idx = meta_to_index(original_list[j].slot_vaddr);
1604                        &&& original_regions.contains(idx)
1605                        &&& original_regions.slot_owners[idx].paths_in_pt.is_empty()
1606                        &&& original_regions.ref_count(idx) == REF_COUNT_UNIQUE
1607                    },
1608            ensures
1609                k == n,
1610                cursor_own.list_own.list.len() == 0,
1611            decreases n - k,
1612        {
1613            #[verus_spec(with Tracked(regions), Tracked(&mut cursor_own) => Tracked(returned_owner))]
1614            let entry = cursor.take_current();
1615
1616            if let Some(current) = entry {
1617                let mut frame = current;
1618                let tracked frame_own = returned_owner.tracked_unwrap();
1619                let ghost regions_pre_drop = *regions;
1620
1621                // Drop the frame, returning its slot to regions
1622                #[verus_spec(with Tracked(frame_own), Tracked(regions))]
1623                frame.drop();
1624
1625                proof {
1626                    assert forall|i: int|
1627                        #![trigger cursor_own.list_own.list[i]]
1628                        0 <= i < cursor_own.list_own.list.len() implies ({
1629                        let idx = meta_to_index(cursor_own.list_own.list[i].slot_vaddr);
1630                        &&& regions.contains(idx)
1631                        &&& regions.slot_owners[idx] == regions_pre_drop.slot_owners[idx]
1632                    }) by {
1633                        let idx = meta_to_index(cursor_own.list_own.list[i].slot_vaddr);
1634                        assert(cursor_own.list_own.list[i] == original_list[i + k + 1]);
1635
1636                        cursor_own.list_own.lemma_relate_region_at_index(regions_pre_drop, i);
1637                        cursor_own.list_own.lemma_relate_region_at_facts(regions_pre_drop, i);
1638                    };
1639                    cursor_own.list_own.lemma_relate_region_preserved_external_change(
1640                        regions_pre_drop,
1641                        *regions,
1642                    );
1643
1644                    assert forall|j: int|
1645                        #![trigger cursor_own.list_own.list[j]]
1646                        0 <= j < n - k - 1 implies cursor_own.list_own.list[j] == original_list[j
1647                        + k + 1] by {};
1648
1649                    k = k + 1;
1650                }
1651            } else {
1652                break;
1653            }
1654        }
1655
1656        // Restore the list owner from the cursor's final (empty) list.
1657        proof {
1658            let tracked mut final_list_own = cursor_own.list_own;
1659            vstd::modes::tracked_swap(owner, &mut final_list_own);
1660            final_list_own.tracked_destroy_empty();
1661        }
1662    }
1663}
1664
1665// SAFETY: `Link<M>` is `Send` and `Sync` if `M` is `Send` and `Sync` because
1666// we only access these unsafe cells when the frame is not shared. This is
1667// enforced by `UniqueFrame`.
1668// #[verifier::external]
1669// unsafe impl<M> Send for LinkedList<M> where Link<M>: AnyFrameMeta {}
1670// #[verifier::external]
1671// unsafe impl<M> Sync for LinkedList<M> where Link<M>: AnyFrameMeta {}
1672/// A link in the linked list.
1673pub struct Link<M: AnyFrameMeta + Repr<MetaSlotSmall>> {
1674    pub next: Option<ReprPtr<MetaSlotStorage, Link<M>>>,
1675    pub prev: Option<ReprPtr<MetaSlotStorage, Link<M>>>,
1676    pub meta: M,
1677}
1678
1679impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Deref for Link<M> {
1680    type Target = M;
1681
1682    fn deref(&self) -> &Self::Target {
1683        &self.meta
1684    }
1685}
1686
1687impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> DerefMut for Link<M> {
1688    fn deref_mut(&mut self) -> &mut Self::Target {
1689        &mut self.meta
1690    }
1691}
1692
1693impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Link<M> {
1694    /// Creates a new linked list metadata.
1695    pub const fn new(meta: M) -> Self {
1696        Self { next: None, prev: None, meta }
1697    }
1698}
1699
1700// SAFETY: If `M::on_drop` reads the page using the provided `VmReader`,
1701// the safety is upheld by the one who implements `AnyFrameMeta` for `M`.
1702unsafe impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> AnyFrameMeta for Link<M> {
1703    open spec fn on_drop_pre(
1704        &self,
1705        reader: crate::mm::VmReader<'_, crate::mm::Infallible>,
1706        regions: MetaRegionOwners,
1707        vm_io_owner: crate::specs::mm::io::VmIoOwner,
1708    ) -> bool {
1709        self.meta.on_drop_pre(reader, regions, vm_io_owner)
1710    }
1711
1712    fn on_drop(
1713        &mut self,
1714        reader: &mut crate::mm::VmReader<crate::mm::Infallible>,
1715        regions: Tracked<&mut MetaRegionOwners>,
1716        vm_io_owner: Tracked<&mut crate::specs::mm::io::VmIoOwner>,
1717    ) {
1718        self.meta.on_drop(reader, regions, vm_io_owner);
1719    }
1720
1721    fn is_untyped(&self) -> bool {
1722        self.meta.is_untyped()
1723    }
1724
1725    uninterp spec fn vtable_ptr(&self) -> usize;
1726}
1727
1728} // verus!