ostd/specs/mm/frame/linked_list/
linked_list_owners.rs

1use vstd::{atomic::*, modes::tracked_swap, prelude::*, seq_lib::*, set_lib::*, simple_pptr::*};
2use vstd_extra::{
3    cast_ptr::{Repr, ReprPtr},
4    ownership::*,
5};
6
7use crate::specs::{
8    arch::MAX_NR_PAGES,
9    mm::frame::{
10        mapping::{max_meta_slots, meta_to_index},
11        meta_owners::*,
12        meta_region_owners::MetaRegionOwners,
13        unique::UniqueFrameOwner,
14    },
15};
16
17use super::*;
18use crate::mm::{
19    Vaddr,
20    frame::{
21        AnyFrameMeta, CursorMut, Link, LinkedList, MetaSlot, UniqueFrame,
22        meta::{META_SLOT_SIZE, REF_COUNT_UNIQUE},
23    },
24    kspace::FRAME_METADATA_RANGE,
25};
26use core::marker::PhantomData;
27
28verus! {
29
30pub struct MetaSlotSmall;
31
32/// Representation of a link as stored in the metadata slot.
33pub struct StoredLink {
34    pub next: Option<Vaddr>,
35    pub prev: Option<Vaddr>,
36    pub slot: MetaSlotSmall,
37}
38
39pub tracked struct LinkInnerPerms<M: AnyFrameMeta + Repr<MetaSlotSmall>> {
40    pub storage: <M as Repr<MetaSlotSmall>>::ReprPerm,
41    pub ghost next_ptr: Option<PPtr<MetaSlotStorage>>,
42    pub ghost prev_ptr: Option<PPtr<MetaSlotStorage>>,
43}
44
45impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Repr<MetaSlotStorage> for Link<M> {
46    type ReprPerm = LinkInnerPerms<M>;
47
48    open spec fn wf(r: MetaSlotStorage, perm: LinkInnerPerms<M>) -> bool {
49        match r {
50            MetaSlotStorage::FrameLink(link) => {
51                &&& M::wf(link.slot, perm.storage)
52                &&& (link.next is Some) == (perm.next_ptr is Some)
53                &&& (link.prev is Some) == (perm.prev_ptr is Some)
54                &&& link.next is Some ==> link.next->0 == perm.next_ptr->0.addr()
55                &&& link.prev is Some ==> link.prev->0 == perm.prev_ptr->0.addr()
56            },
57            _ => false,
58        }
59    }
60
61    open spec fn to_repr_spec(self, perm: LinkInnerPerms<M>) -> (
62        MetaSlotStorage,
63        LinkInnerPerms<M>,
64    ) {
65        let (slot, storage) = self.meta.to_repr_spec(perm.storage);
66        (
67            MetaSlotStorage::FrameLink(
68                StoredLink {
69                    next: match self.next {
70                        Some(ptr) => Some(ptr.ptr.addr()),
71                        None => None,
72                    },
73                    prev: match self.prev {
74                        Some(ptr) => Some(ptr.ptr.addr()),
75                        None => None,
76                    },
77                    slot,
78                },
79            ),
80            LinkInnerPerms {
81                storage,
82                next_ptr: match self.next {
83                    Some(ptr) => Some(ptr.ptr),
84                    None => None,
85                },
86                prev_ptr: match self.prev {
87                    Some(ptr) => Some(ptr.ptr),
88                    None => None,
89                },
90            },
91        )
92    }
93
94    #[verifier::external_body]
95    fn to_repr(self, Tracked(perm): Tracked<&mut LinkInnerPerms<M>>) -> MetaSlotStorage {
96        unimplemented!()
97    }
98
99    open spec fn from_repr_spec(r: MetaSlotStorage, perm: LinkInnerPerms<M>) -> Self {
100        match r {
101            MetaSlotStorage::FrameLink(link) => Link {
102                next: match link.next {
103                    Some(addr) => Some(ReprPtr { ptr: perm.next_ptr->0, _T: PhantomData }),
104                    None => None,
105                },
106                prev: match link.prev {
107                    Some(addr) => Some(ReprPtr { ptr: perm.prev_ptr->0, _T: PhantomData }),
108                    None => None,
109                },
110                meta: M::from_repr_spec(link.slot, perm.storage),
111            },
112            _ => Link {
113                next: None,
114                prev: None,
115                meta: M::from_repr_spec(MetaSlotSmall, perm.storage),
116            },
117        }
118    }
119
120    #[verifier::external_body]
121    fn from_repr(r: MetaSlotStorage, Tracked(perm): Tracked<&LinkInnerPerms<M>>) -> Self {
122        unimplemented!()
123    }
124
125    #[verifier::external_body]
126    fn from_borrowed<'a>(
127        r: &'a MetaSlotStorage,
128        Tracked(perm): Tracked<&'a LinkInnerPerms<M>>,
129    ) -> &'a Self {
130        unimplemented!()
131    }
132
133    #[verifier::external_body]
134    fn from_borrowed_mut<'a>(
135        r: &'a mut MetaSlotStorage,
136        Tracked(perm): Tracked<&'a mut LinkInnerPerms<M>>,
137    ) -> &'a mut Self {
138        unimplemented!()
139    }
140
141    proof fn from_to_repr(self, perm: LinkInnerPerms<M>) {
142        <M as Repr<MetaSlotSmall>>::from_to_repr(self.meta, perm.storage);
143    }
144
145    proof fn to_from_repr(r: MetaSlotStorage, perm: LinkInnerPerms<M>) {
146        match r {
147            MetaSlotStorage::FrameLink(link) => {
148                M::to_from_repr(link.slot, perm.storage);
149            },
150            _ => {
151                assert(false);
152            },
153        }
154    }
155
156    proof fn to_repr_wf(self, perm: LinkInnerPerms<M>) {
157        <M as Repr<MetaSlotSmall>>::to_repr_wf(self.meta, perm.storage);
158    }
159}
160
161pub ghost struct LinkModel {
162    pub slot_vaddr: Vaddr,
163}
164
165impl Inv for LinkModel {
166    open spec fn inv(self) -> bool {
167        true
168    }
169}
170
171pub tracked struct LinkOwner {
172    pub ghost slot_vaddr: Vaddr,
173    pub ghost in_list: u64,
174}
175
176impl Inv for LinkOwner {
177    open spec fn inv(self) -> bool {
178        true
179    }
180}
181
182impl View for LinkOwner {
183    type V = LinkModel;
184
185    open spec fn view(&self) -> Self::V {
186        LinkModel { slot_vaddr: self.slot_vaddr }
187    }
188}
189
190impl InvView for LinkOwner {
191    proof fn view_preserves_inv(self) {
192    }
193}
194
195impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> OwnerOf for Link<M> {
196    type Owner = LinkOwner;
197
198    open spec fn wf(self, owner: Self::Owner) -> bool {
199        true
200        //        &&& owner.self_perm@.mem_contents().value() == self
201        //        &&& owner.next == self.next
202        //        &&& owner.prev == self.prev
203
204    }
205}
206
207pub ghost struct LinkedListModel {
208    pub list: Seq<LinkModel>,
209}
210
211impl LinkedListModel {
212    pub open spec fn front(self) -> Option<LinkModel> {
213        if self.list.len() > 0 {
214            Some(self.list[0])
215        } else {
216            None
217        }
218    }
219
220    pub open spec fn back(self) -> Option<LinkModel> {
221        if self.list.len() > 0 {
222            Some(self.list[self.list.len() - 1])
223        } else {
224            None
225        }
226    }
227}
228
229impl Inv for LinkedListModel {
230    open spec fn inv(self) -> bool {
231        true
232    }
233}
234
235pub tracked struct LinkedListOwner<M: AnyFrameMeta + Repr<MetaSlotSmall>> {
236    pub list: Seq<LinkOwner>,
237    pub repr_perms: Seq<LinkInnerPerms<M>>,
238    /// Exclusive metadata permissions for the unique frames stored in the
239    /// list.
240    pub metadata_perms: Seq<MetadataPerm>,
241    pub ghost list_id: u64,
242    pub ghost _marker: core::marker::PhantomData<M>,
243}
244
245impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Inv for LinkedListOwner<M> {
246    open spec fn inv(self) -> bool {
247        // Weakened (our change): an EMPTY list may carry `list_id == 0` (the
248        // lazily-minted-id convention used by the list-store embedding); the
249        // id is only constrained non-zero once the list is non-empty.
250        &&& self.list.len() > 0 ==> self.list_id != 0
251        &&& self.repr_perms.len() == self.list.len()
252        &&& self.metadata_perms.len() == self.list.len()
253        &&& forall|i: int| 0 <= i < self.list.len() ==> self.inv_at(i)
254    }
255}
256
257impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedListOwner<M> {
258    pub open spec fn meta_addr_at(self, regions: MetaRegionOwners, i: int) -> usize {
259        regions.slots[meta_to_index(self.list[i].slot_vaddr)].addr()
260    }
261
262    pub open spec fn meta_pptr_at(self, regions: MetaRegionOwners, i: int) -> PPtr<MetaSlot> {
263        regions.slots[meta_to_index(self.list[i].slot_vaddr)].pptr()
264    }
265
266    /// Per-link structural invariant: the link's own `inv()` holds and its
267    /// `in_list` tag matches the list's `list_id`. The per-link metadata facts
268    /// (perm wf/is_init/pointer wiring) are tracked via `relate_region_at`
269    /// against the global `MetaRegionOwners`, NOT through this predicate.
270    pub open spec fn inv_at(self, i: int) -> bool {
271        &&& self.list[i].inv()
272        &&& self.list[i].in_list == self.list_id
273    }
274
275    pub open spec fn meta_wf_at(self, regions: MetaRegionOwners, i: int) -> bool {
276        let idx = meta_to_index(self.list[i].slot_vaddr);
277        typed_meta_wf::<Link<M>>(*regions.slots[idx], self.metadata_perms[i], self.repr_perms[i])
278    }
279
280    pub open spec fn meta_value_at(self, regions: MetaRegionOwners, i: int) -> Link<M> {
281        let idx = meta_to_index(self.list[i].slot_vaddr);
282        typed_meta_value::<Link<M>>(self.metadata_perms[i], self.repr_perms[i])
283    }
284
285    /// The per-link invariant expressed directly over the region-owned slot and
286    /// storage permissions plus the list-owned representation permission.
287    #[verifier::opaque]
288    pub open spec fn relate_region_at(self, regions: MetaRegionOwners, i: int) -> bool {
289        let idx = meta_to_index(self.list[i].slot_vaddr);
290        let value = self.meta_value_at(regions, i);
291        &&& regions.contains(idx)
292        &&& regions.slots[idx].addr() == self.list[i].slot_vaddr
293        &&& regions.ref_count(idx) == REF_COUNT_UNIQUE
294        &&& regions.slot_owners[idx].metadata_perm.is_resource_vacant()
295        &&& self.metadata_perms[i].storage_perm.id() == regions.slots[idx].value().storage.id()
296        &&& self.metadata_perms[i].vtable_ptr_perm.pptr() == regions.slots[idx].value().vtable_ptr
297        &&& self.metadata_perms[i].vtable_ptr_perm.is_init()
298        &&& regions.slot_owners[idx].usage is Frame
299        &&& regions.slot_owners[idx].in_list_perm.value() == self.list_id
300        &&& self.meta_wf_at(regions, i)
301        &&& regions.slots[idx].addr() % META_SLOT_SIZE == 0
302        &&& FRAME_METADATA_RANGE.start <= regions.slots[idx].addr() < FRAME_METADATA_RANGE.start
303            + MAX_NR_PAGES * META_SLOT_SIZE
304        &&& value.wf(self.list[i])
305        &&& i == 0 <==> value.prev is None
306        &&& i == self.list.len() - 1 <==> value.next is None
307        &&& 0 < i ==> {
308            &&& value.prev is Some
309            &&& value.prev->0.addr() == self.meta_addr_at(regions, i - 1)
310        }
311        &&& i < self.list.len() - 1 ==> {
312            &&& value.next is Some
313            &&& value.next->0.addr() == self.meta_addr_at(regions, i + 1)
314        }
315        &&& self.list[i].inv()
316        &&& self.list[i].in_list == self.list_id
317    }
318
319    /// The list-wide region relation: every link satisfies `relate_region_at`,
320    /// and distinct list positions map to distinct region slot indices (so a
321    /// frame appears at most once — required by the borrow model, where link
322    /// edits mutate `regions.slots[meta_to_index(self.list[i].slot_vaddr)]` and must not alias).
323    #[verifier::opaque]
324    pub open spec fn relate_region(self, regions: MetaRegionOwners) -> bool {
325        &&& self.repr_perms.len() == self.list.len()
326        &&& self.metadata_perms.len() == self.list.len()
327        &&& forall|i: int|
328            #![trigger self.list[i]]
329            0 <= i < self.list.len() ==> self.relate_region_at(regions, i)
330        &&& forall|i: int, j: int|
331            #![trigger meta_to_index(self.list[i].slot_vaddr), meta_to_index(self.list[j].slot_vaddr)]
332            0 <= i < self.list.len() && 0 <= j < self.list.len() && i != j ==> meta_to_index(
333                self.list[i].slot_vaddr,
334            ) != meta_to_index(self.list[j].slot_vaddr)
335        &&& self.list.len() > 0 ==> self.list_id != 0
336    }
337
338    /// Exposes only the non-quantified shape facts of `relate_region`.
339    pub proof fn lemma_relate_region_shape(self, regions: MetaRegionOwners)
340        requires
341            self.relate_region(regions),
342        ensures
343            self.repr_perms.len() == self.list.len(),
344            self.metadata_perms.len() == self.list.len(),
345            self.list.len() > 0 ==> self.list_id != 0,
346    {
347        reveal(LinkedListOwner::relate_region);
348    }
349
350    /// Derives the owner invariant from the list's region relation.
351    pub proof fn lemma_relate_region_implies_inv(self, regions: MetaRegionOwners)
352        requires
353            self.relate_region(regions),
354        ensures
355            self.inv(),
356    {
357        self.lemma_relate_region_shape(regions);
358        assert forall|i: int| 0 <= i < self.list.len() implies self.inv_at(i) by {
359            self.lemma_relate_region_at_index(regions, i);
360            self.lemma_relate_region_at_facts(regions, i);
361        }
362    }
363
364    /// Extracts the region relation at one list position without leaving the
365    /// list-wide quantifiers visible in the caller.
366    pub proof fn lemma_relate_region_at_index(self, regions: MetaRegionOwners, i: int)
367        requires
368            self.relate_region(regions),
369            0 <= i < self.list.len(),
370        ensures
371            self.relate_region_at(regions, i),
372    {
373        reveal(LinkedListOwner::relate_region);
374        let _ = self.list[i];
375    }
376
377    /// Extracts injectivity for one pair of list positions.
378    pub proof fn lemma_relate_region_indices_distinct(
379        self,
380        regions: MetaRegionOwners,
381        i: int,
382        j: int,
383    )
384        requires
385            self.relate_region(regions),
386            0 <= i < self.list.len(),
387            0 <= j < self.list.len(),
388            i != j,
389        ensures
390            meta_to_index(self.list[i].slot_vaddr) != meta_to_index(self.list[j].slot_vaddr),
391    {
392        reveal(LinkedListOwner::relate_region);
393        let _ = meta_to_index(self.list[i].slot_vaddr);
394        let _ = meta_to_index(self.list[j].slot_vaddr);
395    }
396
397    /// Pigeonhole bound: the list is no longer than the number of meta slots.
398    /// Each link occupies a region slot (`relate_region_at` ⟹
399    /// `slots.contains_key(meta_to_index(self.list[i].slot_vaddr))`, and `regions.inv()` ⟹
400    /// `meta_to_index(self.list[i].slot_vaddr) < max_meta_slots()`), and distinct positions occupy
401    /// distinct slots (`relate_region`'s injectivity). So the positions inject
402    /// into `[0, max_meta_slots())` and the length is capped by it.
403    pub proof fn lemma_length_le_max_meta_slots(self, regions: MetaRegionOwners)
404        requires
405            self.relate_region(regions),
406            regions.inv(),
407        ensures
408            self.list.len() <= max_meta_slots(),
409    {
410        reveal(LinkedListOwner::relate_region);
411        let idxs = Seq::new(self.list.len(), |i: int| meta_to_index(self.list[i].slot_vaddr));
412
413        idxs.unique_seq_to_set();
414
415        let bound = set_int_range(0, max_meta_slots());
416        assert(idxs.to_set().subset_of(bound)) by {
417            assert forall|x: int|
418                #![trigger idxs.to_set().contains(x)]
419                idxs.to_set().contains(x) implies bound.contains(x) by {
420                let i = choose|i: int| 0 <= i < idxs.len() && idxs[i] == x;
421                self.lemma_relate_region_at_facts(regions, i);
422                // `regions.inv()`: the contained slot index is `< max_meta_slots()`.
423            }
424        }
425        lemma_int_range(0, max_meta_slots());
426        lemma_len_subset(idxs.to_set(), bound);
427    }
428
429    /// The list counter can never saturate: its length is capped by
430    /// `max_meta_slots()` (see [`Self::lemma_length_le_max_meta_slots`]), which is far
431    /// below `usize::MAX`. Lets `insert_before` discharge the `size + 1`
432    /// overflow check without a caller-supplied non-fullness precondition.
433    pub proof fn lemma_length_lt_usize_max(self, regions: MetaRegionOwners)
434        requires
435            self.relate_region(regions),
436            regions.inv(),
437        ensures
438            self.list.len() < usize::MAX,
439    {
440        self.lemma_length_le_max_meta_slots(regions);
441    }
442
443    /// Unfolds the opaque `relate_region_at` ONCE and exposes its clauses.
444    pub proof fn lemma_relate_region_at_facts(self, regions: MetaRegionOwners, i: int)
445        requires
446            self.relate_region_at(regions, i),
447        ensures
448            ({
449                let idx = meta_to_index(self.list[i].slot_vaddr);
450                let value = self.meta_value_at(regions, i);
451                &&& regions.contains(idx)
452                &&& regions.slots[idx].addr() == self.list[i].slot_vaddr
453                &&& regions.ref_count(idx) == REF_COUNT_UNIQUE
454                &&& regions.slot_owners[idx].metadata_perm.is_resource_vacant()
455                &&& self.metadata_perms[i].storage_perm.id()
456                    == regions.slots[idx].value().storage.id()
457                &&& self.metadata_perms[i].vtable_ptr_perm.pptr()
458                    == regions.slots[idx].value().vtable_ptr
459                &&& self.metadata_perms[i].vtable_ptr_perm.is_init()
460                &&& regions.slot_owners[idx].usage is Frame
461                &&& regions.slot_owners[idx].in_list_perm.value() == self.list_id
462                &&& self.meta_wf_at(regions, i)
463                &&& regions.slots[idx].addr() % META_SLOT_SIZE == 0
464                &&& FRAME_METADATA_RANGE.start <= regions.slots[idx].addr()
465                    < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
466                &&& value.wf(self.list[i])
467                &&& (i == 0 <==> value.prev is None)
468                &&& (i == self.list.len() - 1 <==> value.next is None)
469                &&& (0 < i ==> {
470                    &&& value.prev is Some
471                    &&& value.prev->0.addr() == self.meta_addr_at(regions, i - 1)
472                })
473                &&& (i < self.list.len() - 1 ==> {
474                    &&& value.next is Some
475                    &&& value.next->0.addr() == self.meta_addr_at(regions, i + 1)
476                })
477                &&& self.list[i].inv()
478                &&& self.list[i].in_list == self.list_id
479            }),
480    {
481        reveal(LinkedListOwner::relate_region_at);
482    }
483
484    /// Constructor (inverse of [`lemma_relate_region_at_facts`]): establishes the
485    /// opaque `relate_region_at` from its unfolded clauses. Used by the pop/
486    /// insert "surgery" proofs, which assemble each clause for the new list and
487    /// then fold them back into the opaque predicate.
488    pub proof fn lemma_relate_region_at_from_clauses(self, regions: MetaRegionOwners, i: int)
489        requires
490            ({
491                let idx = meta_to_index(self.list[i].slot_vaddr);
492                let value = self.meta_value_at(regions, i);
493                &&& regions.contains(idx)
494                &&& self.repr_perms.len() == self.list.len()
495                &&& self.metadata_perms.len() == self.list.len()
496                &&& regions.slots[idx].addr() == self.list[i].slot_vaddr
497                &&& regions.ref_count(idx) == REF_COUNT_UNIQUE
498                &&& regions.slot_owners[idx].metadata_perm.is_resource_vacant()
499                &&& self.metadata_perms[i].storage_perm.id()
500                    == regions.slots[idx].value().storage.id()
501                &&& self.metadata_perms[i].vtable_ptr_perm.pptr()
502                    == regions.slots[idx].value().vtable_ptr
503                &&& self.metadata_perms[i].vtable_ptr_perm.is_init()
504                &&& regions.slot_owners[idx].usage is Frame
505                &&& regions.slot_owners[idx].in_list_perm.value() == self.list_id
506                &&& self.meta_wf_at(regions, i)
507                &&& regions.slots[idx].addr() % META_SLOT_SIZE == 0
508                &&& FRAME_METADATA_RANGE.start <= regions.slots[idx].addr()
509                    < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
510                &&& value.wf(self.list[i])
511                &&& (i == 0 <==> value.prev is None)
512                &&& (i == self.list.len() - 1 <==> value.next is None)
513                &&& (0 < i ==> {
514                    &&& value.prev is Some
515                    &&& value.prev->0.addr() == self.meta_addr_at(regions, i - 1)
516                })
517                &&& (i < self.list.len() - 1 ==> {
518                    &&& value.next is Some
519                    &&& value.next->0.addr() == self.meta_addr_at(regions, i + 1)
520                })
521                &&& self.list[i].inv()
522                &&& self.list[i].in_list == self.list_id
523            }),
524        ensures
525            self.relate_region_at(regions, i),
526    {
527        reveal(LinkedListOwner::relate_region_at);
528    }
529
530    /// `relate_region` is preserved under a region change that doesn't touch
531    /// any of the list's slots. Used by `LinkedList::drop`'s loop body: after
532    /// `take_current` pops position 0, the popped slot is dropped via
533    /// `frame.drop`, which only modifies `regions.slot_owners[cur_idx]` and
534    /// leaves `regions.slots` fully untouched. Since the cursor's remaining
535    /// list never contains `cur_idx` (distinctness on the original list),
536    /// `relate_region` carries through.
537    pub proof fn lemma_relate_region_preserved_external_change(
538        self,
539        regions1: MetaRegionOwners,
540        regions2: MetaRegionOwners,
541    )
542        requires
543            self.relate_region(regions1),
544            regions2.slots == regions1.slots,
545            forall|i: int|
546                #![trigger self.list[i]]
547                0 <= i < self.list.len() ==> {
548                    let idx = meta_to_index(self.list[i].slot_vaddr);
549                    &&& regions2.contains(idx)
550                    &&& regions2.slot_owners[idx] == regions1.slot_owners[idx]
551                },
552        ensures
553            self.relate_region(regions2),
554    {
555        reveal(LinkedListOwner::relate_region);
556        let llen = self.list.len() as int;
557        assert forall|k: int|
558            #![trigger self.relate_region_at(regions2, k)]
559            0 <= k < llen implies self.relate_region_at(regions2, k) by {
560            let _ = self.list[k];
561            self.lemma_relate_region_at_facts(regions1, k);
562            self.lemma_relate_region_at_from_clauses(regions2, k);
563        }
564    }
565
566    /// The list-rewiring "surgery" for popping the element at index `n`: given
567    /// the entry invariant `old.relate_region(r0)` and a characterization of the
568    /// post-pop region `fr` (every surviving slot keeps its local facts and
569    /// pointers, except the two neighbors whose `next`/`prev` were rewired to
570    /// bridge the gap), the shrunk list `new` satisfies `relate_region(fr)`.
571    ///
572    /// New position `k` maps to old position `p = (k < n ? k : k+1)`; the
573    /// neighbor of `k` maps to `p ± 1` except across the cut (new position `n-1`
574    /// reaches old `n+1`, new position `n` reaches old `n-1`), which is exactly
575    /// where the body rewired the link pointers.
576    #[verifier::spinoff_prover]
577    #[verifier::rlimit(60)]
578    pub proof fn lemma_pop_preserves_relate_region(
579        old: LinkedListOwner<M>,
580        r0: MetaRegionOwners,
581        new: LinkedListOwner<M>,
582        fr: MetaRegionOwners,
583        n: int,
584    )
585        requires
586            0 <= n < old.list.len(),
587            old.relate_region(r0),
588            new.list == old.list.remove(n),
589            new.repr_perms.len() == new.list.len(),
590            new.metadata_perms.len() == new.list.len(),
591            new.list_id == old.list_id,
592            forall|p: int|
593                #![trigger meta_to_index(old.list[p].slot_vaddr)]
594                (0 <= p < old.list.len() && p != n) ==> ({
595                    let i = meta_to_index(old.list[p].slot_vaddr);
596                    let np = if p < n {
597                        p
598                    } else {
599                        p - 1
600                    };
601                    let fp = typed_meta_value::<Link<M>>(
602                        new.metadata_perms[np],
603                        new.repr_perms[np],
604                    );
605                    &&& fr.contains(i)
606                    &&& fr.slots[i].addr() == old.list[p].slot_vaddr
607                    &&& fr.slots[i].pptr() == r0.slots[i].pptr()
608                    &&& fr.ref_count(i) == REF_COUNT_UNIQUE
609                    &&& fr.slot_owners[i].metadata_perm.is_resource_vacant()
610                    &&& new.metadata_perms[np].storage_perm.id() == fr.slots[i].value().storage.id()
611                    &&& new.metadata_perms[np].vtable_ptr_perm.pptr()
612                        == fr.slots[i].value().vtable_ptr
613                    &&& new.metadata_perms[np].vtable_ptr_perm.is_init()
614                    &&& fr.slot_owners[i].usage is Frame
615                    &&& fr.slot_owners[i].in_list_perm.value() == new.list_id
616                    &&& typed_meta_wf::<Link<M>>(
617                        *fr.slots[i],
618                        new.metadata_perms[np],
619                        new.repr_perms[np],
620                    )
621                    &&& fr.slots[i].addr() % META_SLOT_SIZE == 0
622                    &&& FRAME_METADATA_RANGE.start <= fr.slots[i].addr()
623                        < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
624                    &&& (p == n - 1 ==> fp.next == old.meta_value_at(r0, n).next)
625                    &&& (p != n - 1 ==> fp.next == old.meta_value_at(r0, p).next)
626                    &&& (p == n + 1 ==> fp.prev == old.meta_value_at(r0, n).prev)
627                    &&& (p != n + 1 ==> fp.prev == old.meta_value_at(r0, p).prev)
628                }),
629        ensures
630            new.relate_region(fr),
631    {
632        old.lemma_relate_region_shape(r0);
633        let nlen = new.list.len() as int;
634
635        assert forall|k: int|
636            #![trigger meta_to_index(new.list[k].slot_vaddr)]
637            0 <= k < nlen implies {
638            let p = if k < n {
639                k
640            } else {
641                k + 1
642            };
643            &&& new.list[k] == old.list[p]
644            &&& meta_to_index(new.list[k].slot_vaddr) == meta_to_index(old.list[p].slot_vaddr)
645        } by {}
646
647        assert forall|a: int, b: int|
648            #![trigger meta_to_index(new.list[a].slot_vaddr), meta_to_index(new.list[b].slot_vaddr)]
649            0 <= a < nlen && 0 <= b < nlen && a != b implies meta_to_index(new.list[a].slot_vaddr)
650            != meta_to_index(new.list[b].slot_vaddr) by {
651            let pa = if a < n {
652                a
653            } else {
654                a + 1
655            };
656            let pb = if b < n {
657                b
658            } else {
659                b + 1
660            };
661            old.lemma_relate_region_indices_distinct(r0, pa, pb);
662        }
663
664        assert forall|m: int| #![trigger new.meta_addr_at(fr, m)] 0 <= m < nlen implies {
665            let pm = if m < n {
666                m
667            } else {
668                m + 1
669            };
670            &&& new.meta_addr_at(fr, m) == old.meta_addr_at(r0, pm)
671            &&& new.meta_pptr_at(fr, m) == old.meta_pptr_at(r0, pm)
672        } by {
673            let pm = if m < n {
674                m
675            } else {
676                m + 1
677            };
678            let _ = old.list[pm];
679            old.lemma_relate_region_at_index(r0, pm);
680            old.lemma_relate_region_at_facts(r0, pm);
681        }
682
683        assert forall|k: int|
684            #![trigger new.relate_region_at(fr, k)]
685            0 <= k < nlen implies new.relate_region_at(fr, k) by {
686            let p = if k < n {
687                k
688            } else {
689                k + 1
690            };
691            let _ = old.list[p];
692            old.lemma_relate_region_at_index(r0, p);
693            old.lemma_relate_region_at_facts(r0, p);
694            let _ = old.list[n];
695            old.lemma_relate_region_at_index(r0, n);
696            old.lemma_relate_region_at_facts(r0, n);
697            if p - 1 >= 0 {
698                let _ = old.list[p - 1];
699                old.lemma_relate_region_at_index(r0, p - 1);
700                old.lemma_relate_region_at_facts(r0, p - 1);
701            }
702            if p + 1 < old.list.len() {
703                let _ = old.list[p + 1];
704                old.lemma_relate_region_at_index(r0, p + 1);
705                old.lemma_relate_region_at_facts(r0, p + 1);
706            }
707            if n - 1 >= 0 {
708                let _ = old.list[n - 1];
709                old.lemma_relate_region_at_index(r0, n - 1);
710                old.lemma_relate_region_at_facts(r0, n - 1);
711            }
712            if n + 1 < old.list.len() {
713                old.lemma_relate_region_at_index(r0, n + 1);
714                old.lemma_relate_region_at_facts(r0, n + 1);
715            }
716            new.lemma_relate_region_at_from_clauses(fr, k);
717        }
718
719        assert(new.relate_region(fr)) by {
720            reveal(LinkedListOwner::relate_region);
721        };
722    }
723
724    /// The list-rewiring "surgery" for inserting `link` before index `n`
725    /// (`0 <= n <= old.list.len()`): given the entry `relate_region` and a
726    /// per-slot characterization of the post-insert region `fr`, the longer list
727    /// `new = old.list.insert(n, link)` satisfies `relate_region(fr)`.
728    ///
729    /// New position `k` maps to old position `k` (k<n), is the inserted link
730    /// (k==n), or maps to old `k-1` (k>n). The inserted link sits at slot
731    /// `ins = meta_to_index(new.list[n].slot_vaddr)`; its `prev`/`next` point to old `n-1`/`n`
732    /// (or `None` at the endsP), and old `n-1`'s `next` / old `n`'s `prev` are
733    /// rewired to point at the inserted link. Mirror of
734    /// [`lemma_pop_preserves_relate_region`].
735    pub open spec fn insert_old_slot_post_clauses(
736        self,
737        fr: MetaRegionOwners,
738        old: LinkedListOwner<M>,
739        r0: MetaRegionOwners,
740        n: int,
741        link: LinkOwner,
742        p: int,
743    ) -> bool {
744        let i = meta_to_index(old.list[p].slot_vaddr);
745        let ins = meta_to_index(self.list[n].slot_vaddr);
746        let np = if p < n {
747            p
748        } else {
749            p + 1
750        };
751        let fp = typed_meta_value::<Link<M>>(self.metadata_perms[np], self.repr_perms[np]);
752        &&& fr.contains(i)
753        &&& fr.slots[i].is_init()
754        &&& fr.slots[i].addr() == old.list[p].slot_vaddr
755        &&& fr.slots[i].pptr() == r0.slots[i].pptr()
756        &&& fr.ref_count(i) == REF_COUNT_UNIQUE
757        &&& fr.slot_owners[i].metadata_perm.is_resource_vacant()
758        &&& self.metadata_perms[np].storage_perm.id() == fr.slots[i].value().storage.id()
759        &&& self.metadata_perms[np].vtable_ptr_perm.pptr() == fr.slots[i].value().vtable_ptr
760        &&& self.metadata_perms[np].vtable_ptr_perm.is_init()
761        &&& fr.slot_owners[i].usage is Frame
762        &&& fr.slot_owners[i].in_list_perm.value() == self.list_id
763        &&& self.meta_wf_at(fr, np)
764        &&& fr.slots[i].addr() % META_SLOT_SIZE == 0
765        &&& FRAME_METADATA_RANGE.start <= fr.slots[i].addr() < FRAME_METADATA_RANGE.start
766            + MAX_NR_PAGES * META_SLOT_SIZE
767        &&& (p == n - 1 ==> {
768            &&& fp.next is Some
769            &&& fp.next->0.addr() == link.slot_vaddr
770            &&& fp.next->0.ptr.addr() == fr.slots[ins].pptr().addr()
771        })
772        &&& (p != n - 1 ==> fp.next == old.meta_value_at(r0, p).next)
773        &&& (p == n ==> {
774            &&& fp.prev is Some
775            &&& fp.prev->0.addr() == link.slot_vaddr
776            &&& fp.prev->0.ptr.addr() == fr.slots[ins].pptr().addr()
777        })
778        &&& (p != n ==> fp.prev == old.meta_value_at(r0, p).prev)
779    }
780
781    #[verifier::opaque]
782    pub open spec fn insert_old_slot_post_at(
783        self,
784        fr: MetaRegionOwners,
785        old: LinkedListOwner<M>,
786        r0: MetaRegionOwners,
787        n: int,
788        link: LinkOwner,
789        p: int,
790    ) -> bool {
791        self.insert_old_slot_post_clauses(fr, old, r0, n, link, p)
792    }
793
794    pub proof fn lemma_insert_old_slot_post_at_facts(
795        self,
796        fr: MetaRegionOwners,
797        old: LinkedListOwner<M>,
798        r0: MetaRegionOwners,
799        n: int,
800        link: LinkOwner,
801        p: int,
802    )
803        requires
804            self.insert_old_slot_post_at(fr, old, r0, n, link, p),
805        ensures
806            self.insert_old_slot_post_clauses(fr, old, r0, n, link, p),
807    {
808        reveal(LinkedListOwner::insert_old_slot_post_at);
809    }
810
811    #[verifier::spinoff_prover]
812    #[verifier::rlimit(120)]
813    pub proof fn lemma_insert_preserves_relate_region(
814        old: LinkedListOwner<M>,
815        r0: MetaRegionOwners,
816        new: LinkedListOwner<M>,
817        fr: MetaRegionOwners,
818        n: int,
819        link: LinkOwner,
820    )
821        requires
822            0 <= n <= old.list.len(),
823            old.relate_region(r0),
824            new.list == old.list.insert(n, link),
825            new.repr_perms.len() == new.list.len(),
826            new.metadata_perms.len() == new.list.len(),
827            new.list_id != 0,
828            old.list.len() > 0 ==> new.list_id == old.list_id,
829            link.inv(),
830            link.in_list == new.list_id,
831            forall|p: int|
832                #![trigger meta_to_index(old.list[p].slot_vaddr)]
833                (0 <= p < old.list.len()) ==> meta_to_index(old.list[p].slot_vaddr)
834                    != meta_to_index(new.list[n].slot_vaddr),
835            ({
836                let ins = meta_to_index(new.list[n].slot_vaddr);
837                let fpn = new.meta_value_at(fr, n);
838                &&& fr.contains(ins)
839                &&& fr.slots[ins].is_init()
840                &&& fr.slots[ins].addr() == link.slot_vaddr
841                &&& fr.ref_count(ins) == REF_COUNT_UNIQUE
842                &&& fr.slot_owners[ins].metadata_perm.is_resource_vacant()
843                &&& new.metadata_perms[n].storage_perm.id() == fr.slots[ins].value().storage.id()
844                &&& new.metadata_perms[n].vtable_ptr_perm.pptr() == fr.slots[ins].value().vtable_ptr
845                &&& new.metadata_perms[n].vtable_ptr_perm.is_init()
846                &&& fr.slot_owners[ins].usage is Frame
847                &&& fr.slot_owners[ins].in_list_perm.value() == new.list_id
848                &&& new.meta_wf_at(fr, n)
849                &&& fr.slots[ins].addr() % META_SLOT_SIZE == 0
850                &&& FRAME_METADATA_RANGE.start <= fr.slots[ins].addr() < FRAME_METADATA_RANGE.start
851                    + MAX_NR_PAGES * META_SLOT_SIZE
852                &&& (n == 0 <==> fpn.prev is None)
853                &&& (n == old.list.len() <==> fpn.next is None)
854                &&& (n > 0 ==> {
855                    &&& fpn.prev is Some
856                    &&& fpn.prev->0.addr() == old.list[n - 1].slot_vaddr
857                    &&& fpn.prev->0.ptr.addr() == old.meta_pptr_at(r0, n - 1).addr()
858                })
859                &&& (n < old.list.len() ==> {
860                    &&& fpn.next is Some
861                    &&& fpn.next->0.addr() == old.list[n].slot_vaddr
862                    &&& fpn.next->0.ptr.addr() == old.meta_pptr_at(r0, n).addr()
863                })
864            }),
865            forall|p: int|
866                #![trigger new.insert_old_slot_post_at(fr, old, r0, n, link, p)]
867                (0 <= p < old.list.len()) ==> new.insert_old_slot_post_at(fr, old, r0, n, link, p),
868        ensures
869            new.relate_region(fr),
870    {
871        old.lemma_relate_region_shape(r0);
872        let nlen = new.list.len() as int;
873        let ins = meta_to_index(new.list[n].slot_vaddr);
874
875        assert forall|k: int|
876            #![trigger meta_to_index(new.list[k].slot_vaddr)]
877            0 <= k < nlen implies ({
878            &&& (k < n ==> new.list[k] == old.list[k] && meta_to_index(new.list[k].slot_vaddr)
879                == meta_to_index(old.list[k].slot_vaddr))
880            &&& (k == n ==> new.list[k] == link && meta_to_index(new.list[k].slot_vaddr) == ins)
881            &&& (k > n ==> new.list[k] == old.list[k - 1] && meta_to_index(new.list[k].slot_vaddr)
882                == meta_to_index(old.list[k - 1].slot_vaddr))
883        }) by {}
884
885        assert forall|a: int, b: int|
886            #![trigger meta_to_index(new.list[a].slot_vaddr), meta_to_index(new.list[b].slot_vaddr)]
887            0 <= a < nlen && 0 <= b < nlen && a != b implies meta_to_index(new.list[a].slot_vaddr)
888            != meta_to_index(new.list[b].slot_vaddr) by {
889            if a != n && b != n {
890                let pa = if a < n {
891                    a
892                } else {
893                    a - 1
894                };
895                let pb = if b < n {
896                    b
897                } else {
898                    b - 1
899                };
900                old.lemma_relate_region_indices_distinct(r0, pa, pb);
901            }
902        }
903
904        assert forall|m: int| #![trigger new.meta_addr_at(fr, m)] 0 <= m < nlen implies ({
905            &&& (m < n ==> new.meta_addr_at(fr, m) == old.meta_addr_at(r0, m) && new.meta_pptr_at(
906                fr,
907                m,
908            ) == old.meta_pptr_at(r0, m))
909            &&& (m > n ==> new.meta_addr_at(fr, m) == old.meta_addr_at(r0, m - 1)
910                && new.meta_pptr_at(fr, m) == old.meta_pptr_at(r0, m - 1))
911        }) by {
912            if m < n {
913                let _ = old.list[m];
914                old.lemma_relate_region_at_index(r0, m);
915                old.lemma_relate_region_at_facts(r0, m);
916                new.lemma_insert_old_slot_post_at_facts(fr, old, r0, n, link, m);
917            }
918            if m > n {
919                let _ = old.list[m - 1];
920                old.lemma_relate_region_at_index(r0, m - 1);
921                old.lemma_relate_region_at_facts(r0, m - 1);
922                new.lemma_insert_old_slot_post_at_facts(fr, old, r0, n, link, m - 1);
923            }
924        }
925
926        assert forall|k: int|
927            #![trigger new.relate_region_at(fr, k)]
928            0 <= k < nlen implies new.relate_region_at(fr, k) by {
929            if k < n {
930                let _ = old.list[k];
931                old.lemma_relate_region_at_index(r0, k);
932                old.lemma_relate_region_at_facts(r0, k);
933                new.lemma_insert_old_slot_post_at_facts(fr, old, r0, n, link, k);
934            }
935            if k > n {
936                let _ = old.list[k - 1];
937                old.lemma_relate_region_at_index(r0, k - 1);
938                old.lemma_relate_region_at_facts(r0, k - 1);
939                new.lemma_insert_old_slot_post_at_facts(fr, old, r0, n, link, k - 1);
940            }
941            if n - 1 >= 0 && n - 1 < old.list.len() {
942                let _ = old.list[n - 1];
943                old.lemma_relate_region_at_index(r0, n - 1);
944                old.lemma_relate_region_at_facts(r0, n - 1);
945            }
946            if n >= 0 && n < old.list.len() {
947                let _ = old.list[n];
948                old.lemma_relate_region_at_index(r0, n);
949                old.lemma_relate_region_at_facts(r0, n);
950            }
951            new.lemma_relate_region_at_from_clauses(fr, k);
952        }
953        assert(new.relate_region(fr)) by {
954            reveal(LinkedListOwner::relate_region);
955        };
956    }
957
958    pub open spec fn view_helper(owners: Seq<LinkOwner>) -> Seq<LinkModel> {
959        owners.map_values(|owner: LinkOwner| owner@)
960    }
961
962    /// Proves that view_helper commutes with insert:
963    /// view_helper(s.insert(i, v)) == view_helper(s).insert(i, v.view())
964    pub proof fn lemma_view_helper_insert(owners: Seq<LinkOwner>, i: int, v: LinkOwner)
965        requires
966            0 <= i <= owners.len(),
967        ensures
968            Self::view_helper(owners.insert(i, v)) == Self::view_helper(owners).insert(i, v.view()),
969    {
970        assert forall|j: int|
971            0 <= j < Self::view_helper(
972                owners.insert(i, v),
973            ).len() implies #[trigger] Self::view_helper(owners.insert(i, v))[j]
974            == Self::view_helper(owners).insert(i, v.view())[j] by {};
975    }
976}
977
978impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> View for LinkedListOwner<M> {
979    type V = LinkedListModel;
980
981    open spec fn view(&self) -> Self::V {
982        LinkedListModel { list: Self::view_helper(self.list) }
983    }
984}
985
986impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> InvView for LinkedListOwner<M> {
987    proof fn view_preserves_inv(self) {
988    }
989}
990
991impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedListOwner<M> {
992    /// Take ownership of `*owner` by swapping it with a fresh empty
993    /// `LinkedListOwner`. The resulting "leftover" `*owner` has an empty
994    /// `list`, so its `inv()` holds vacuously. Used by drop-style call sites
995    /// that need to feed an owned `LinkedListOwner` to a downstream API while
996    /// themselves only having a `&mut` to it.
997    pub proof fn tracked_take(tracked owner: &mut Self) -> (tracked res: Self)
998        ensures
999            res == *old(owner),
1000            final(owner).list == Seq::<LinkOwner>::empty(),
1001            final(owner).repr_perms == Seq::<LinkInnerPerms<M>>::empty(),
1002            final(owner).metadata_perms == Seq::<MetadataPerm>::empty(),
1003            final(owner).inv(),
1004    {
1005        let tracked mut tmp = crate::specs::mm::embedding::list_store::tracked_empty_list_owner::<
1006            M,
1007        >();
1008        tracked_swap(owner, &mut tmp);
1009        tmp
1010    }
1011
1012    /// Discard a logically-empty `LinkedListOwner`. Sound because such an
1013    /// owner has an empty `list` and claims no external permissions (the
1014    /// borrow model parks all permissions in `MetaRegionOwners`).
1015    #[verifier::external_body]
1016    pub proof fn tracked_destroy_empty(tracked self)
1017        requires
1018            self.list =~= Seq::<LinkOwner>::empty(),
1019            self.repr_perms =~= Seq::<LinkInnerPerms<M>>::empty(),
1020            self.metadata_perms =~= Seq::<MetadataPerm>::empty(),
1021    {
1022        unimplemented!()
1023    }
1024}
1025
1026impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> OwnerOf for LinkedList<M> {
1027    type Owner = LinkedListOwner<M>;
1028
1029    /// Structural well-formedness of the LinkedList against its owner: size,
1030    /// list_id, and front/back addresses match. The per-link pointer-permission
1031    /// facts (pptr/ptr equality against the front/back) live in `wf_region`,
1032    /// which sources them from `MetaRegionOwners`.
1033    open spec fn wf(self, owner: Self::Owner) -> bool {
1034        &&& self.front is None <==> owner.list.len() == 0
1035        &&& self.back is None <==> owner.list.len() == 0
1036        &&& owner.list.len() > 0 ==> self.front is Some && self.front->0.addr()
1037            == owner.list[0].slot_vaddr && self.back is Some && self.back->0.addr()
1038            == owner.list[owner.list.len() - 1].slot_vaddr
1039        &&& self.size == owner.list.len()
1040        &&& self.list_id == owner.list_id
1041    }
1042}
1043
1044pub ghost struct CursorModel {
1045    pub ghost fore: Seq<LinkModel>,
1046    pub ghost rear: Seq<LinkModel>,
1047    pub ghost list_model: LinkedListModel,
1048}
1049
1050impl Inv for CursorModel {
1051    open spec fn inv(self) -> bool {
1052        self.list_model.inv()
1053    }
1054}
1055
1056pub tracked struct CursorOwner<M: AnyFrameMeta + Repr<MetaSlotSmall>> {
1057    pub list_own: LinkedListOwner<M>,
1058    pub ghost index: int,
1059}
1060
1061impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Inv for CursorOwner<M> {
1062    open spec fn inv(self) -> bool {
1063        &&& 0 <= self.index <= self.length()
1064        &&& self.list_own.inv()
1065    }
1066}
1067
1068impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> View for CursorOwner<M> {
1069    type V = CursorModel;
1070
1071    open spec fn view(&self) -> Self::V {
1072        let list = self.list_own.view();
1073        CursorModel {
1074            fore: list.list[..self.index],
1075            rear: list.list[self.index..],
1076            list_model: list,
1077        }
1078    }
1079}
1080
1081impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> InvView for CursorOwner<M> {
1082    proof fn view_preserves_inv(self) {
1083    }
1084}
1085
1086impl<'a, M: AnyFrameMeta + Repr<MetaSlotSmall>> OwnerOf for CursorMut<'a, M> {
1087    type Owner = CursorOwner<M>;
1088
1089    /// Structural well-formedness: `current` matches the link at `index`'s
1090    /// address. Pointer-permission facts (pptr/ptr equality) are stated in
1091    /// `wf_region` over the region-owned slot pointers.
1092    open spec fn wf(self, owner: Self::Owner) -> bool {
1093        &&& 0 <= owner.index < owner.length() ==> self.current.is_some() && self.current->0.addr()
1094            == owner.list_own.list[owner.index].slot_vaddr
1095        &&& owner.index == owner.list_own.list.len() ==> self.current.is_none()
1096        &&& (*self.list).wf(owner.list_own)
1097    }
1098}
1099
1100impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedList<M> {
1101    /// Region-based analog of [`LinkedList::wf`]: the front/back pointer facts
1102    /// are stated directly over the region-owned slot pointers.
1103    pub open spec fn wf_region(self, owner: LinkedListOwner<M>, regions: MetaRegionOwners) -> bool {
1104        &&& self.front is None <==> owner.list.len() == 0
1105        &&& self.back is None <==> owner.list.len() == 0
1106        &&& owner.list.len() > 0 ==> self.front is Some && self.front->0.addr()
1107            == owner.list[0].slot_vaddr && owner.meta_pptr_at(regions, 0).addr()
1108            == self.front->0.addr() && self.back is Some && self.back->0.addr()
1109            == owner.list[owner.list.len() - 1].slot_vaddr && owner.meta_pptr_at(
1110            regions,
1111            owner.list.len() - 1,
1112        ).addr() == self.back->0.addr()
1113        &&& self.size == owner.list.len()
1114        &&& self.list_id == owner.list_id
1115    }
1116}
1117
1118impl<'a, M: AnyFrameMeta + Repr<MetaSlotSmall>> CursorMut<'a, M> {
1119    /// Region-based analog of [`CursorMut::wf`]: the current-link pointer facts
1120    /// are stated over the corresponding region-owned slot pointer.
1121    pub open spec fn wf_region(self, owner: CursorOwner<M>, regions: MetaRegionOwners) -> bool {
1122        &&& 0 <= owner.index < owner.length() ==> self.current.is_some() && self.current->0.addr()
1123            == owner.list_own.list[owner.index].slot_vaddr && owner.list_own.meta_pptr_at(
1124            regions,
1125            owner.index,
1126        ).addr() == self.current->0.addr()
1127        &&& owner.index == owner.list_own.list.len() ==> self.current.is_none()
1128        &&& (*self.list).wf_region(owner.list_own, regions)
1129    }
1130}
1131
1132impl CursorModel {
1133    pub open spec fn current(self) -> Option<LinkModel> {
1134        if self.rear.len() > 0 {
1135            Some(self.rear[0])
1136        } else {
1137            None
1138        }
1139    }
1140}
1141
1142impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> CursorOwner<M> {
1143    pub open spec fn length(self) -> int {
1144        self.list_own.list.len() as int
1145    }
1146
1147    /// Region-based analog of [`CursorOwner::inv`]: replaces `list_own.inv()`
1148    /// (over the owned `perms`) with `list_own.relate_region(regions)` (over
1149    /// the region permissions).
1150    pub open spec fn wf_with_region(self, regions: MetaRegionOwners) -> bool {
1151        &&& 0 <= self.index <= self.length()
1152        &&& self.list_own.relate_region(regions)
1153    }
1154
1155    pub open spec fn current(self) -> Option<LinkOwner> {
1156        if 0 <= self.index < self.length() {
1157            Some(self.list_own.list[self.index])
1158        } else {
1159            None
1160        }
1161    }
1162
1163    pub open spec fn front_owner(list_own: LinkedListOwner<M>) -> Self {
1164        CursorOwner::<M> { list_own: list_own, index: 0 }
1165    }
1166
1167    pub open spec fn cursor_mut_at_owner(list_own: LinkedListOwner<M>, index: int) -> Self {
1168        CursorOwner::<M> { list_own: list_own, index: index }
1169    }
1170
1171    pub proof fn tracked_cursor_mut_at_owner(
1172        tracked list_own: LinkedListOwner<M>,
1173        index: int,
1174    ) -> tracked Self
1175        returns
1176            Self::cursor_mut_at_owner(list_own, index),
1177    {
1178        let tracked res = CursorOwner::<M> { list_own, index };
1179        res
1180    }
1181
1182    pub proof fn tracked_front_owner(tracked list_own: LinkedListOwner<M>) -> tracked Self
1183        returns
1184            Self::front_owner(list_own),
1185    {
1186        let tracked res = CursorOwner::<M> { list_own, index: 0 };
1187        res
1188    }
1189
1190    pub open spec fn back_owner(list_own: LinkedListOwner<M>) -> Self {
1191        CursorOwner::<M> {
1192            list_own: list_own,
1193            index: if list_own.list.len() > 0 {
1194                list_own.list.len() - 1
1195            } else {
1196                0
1197            },
1198        }
1199    }
1200
1201    pub proof fn tracked_back_owner(tracked list_own: LinkedListOwner<M>) -> (tracked res: Self)
1202        ensures
1203            res == Self::back_owner(list_own),
1204    {
1205        CursorOwner::<M> {
1206            list_own: list_own,
1207            index: if list_own.list.len() > 0 {
1208                list_own.list.len() - 1
1209            } else {
1210                0
1211            },
1212        }
1213    }
1214}
1215
1216impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> UniqueFrameOwner<Link<M>> {
1217    pub open spec fn frame_link_inv(&self, regions: MetaRegionOwners) -> bool {
1218        &&& self.meta_value(regions).prev is None
1219        &&& self.meta_value(regions).next is None
1220        &&& self.meta_own.slot_vaddr == regions.slots[self.slot_index].addr()
1221        &&& regions.slot_owners[self.slot_index].in_list_perm.value() == 0
1222    }
1223}
1224
1225impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> UniqueFrame<Link<M>> {
1226    pub open spec fn frame_link_inv(
1227        self,
1228        owner: UniqueFrameOwner<Link<M>>,
1229        regions: MetaRegionOwners,
1230    ) -> bool {
1231        &&& self.meta_value(owner).prev is None
1232        &&& self.meta_value(owner).next is None
1233        &&& owner.meta_own.slot_vaddr == regions.slots[owner.slot_index].addr()
1234        &&& regions.slot_owners[owner.slot_index].in_list_perm.value() == 0
1235    }
1236}
1237
1238} // verus!
ostd/specs/mm/frame/linked_list/linked_list_owners.rs

ostd/specs/mm/frame/linked_list/
linked_list_owners.rs
