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

ostd/mm/frame/
linked_list.rs
