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    Paddr,
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<Paddr>,
35    pub prev: Option<Paddr>,
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 paddr: Paddr,
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 paddr: Paddr,
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 { paddr: self.paddr }
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].paddr)].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].paddr)].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].paddr);
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].paddr);
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].paddr);
290        let value = self.meta_value_at(regions, i);
291        &&& regions.contains(idx)
292        &&& regions.slots[idx].addr() == self.list[i].paddr
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].paddr)]` 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].paddr), meta_to_index(self.list[j].paddr)]
332            0 <= i < self.list.len() && 0 <= j < self.list.len() && i != j ==> meta_to_index(
333                self.list[i].paddr,
334            ) != meta_to_index(self.list[j].paddr)
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    /// Extracts the region relation at one list position without leaving the
351    /// list-wide quantifiers visible in the caller.
352    pub proof fn lemma_relate_region_at_index(self, regions: MetaRegionOwners, i: int)
353        requires
354            self.relate_region(regions),
355            0 <= i < self.list.len(),
356        ensures
357            self.relate_region_at(regions, i),
358    {
359        reveal(LinkedListOwner::relate_region);
360        let _ = self.list[i];
361    }
362
363    /// Extracts injectivity for one pair of list positions.
364    pub proof fn lemma_relate_region_indices_distinct(
365        self,
366        regions: MetaRegionOwners,
367        i: int,
368        j: int,
369    )
370        requires
371            self.relate_region(regions),
372            0 <= i < self.list.len(),
373            0 <= j < self.list.len(),
374            i != j,
375        ensures
376            meta_to_index(self.list[i].paddr) != meta_to_index(self.list[j].paddr),
377    {
378        reveal(LinkedListOwner::relate_region);
379        let _ = meta_to_index(self.list[i].paddr);
380        let _ = meta_to_index(self.list[j].paddr);
381    }
382
383    /// Pigeonhole bound: the list is no longer than the number of meta slots.
384    /// Each link occupies a region slot (`relate_region_at` ⟹
385    /// `slots.contains_key(meta_to_index(self.list[i].paddr))`, and `regions.inv()` ⟹
386    /// `meta_to_index(self.list[i].paddr) < max_meta_slots()`), and distinct positions occupy
387    /// distinct slots (`relate_region`'s injectivity). So the positions inject
388    /// into `[0, max_meta_slots())` and the length is capped by it.
389    pub proof fn lemma_length_le_max_meta_slots(self, regions: MetaRegionOwners)
390        requires
391            self.relate_region(regions),
392            regions.inv(),
393        ensures
394            self.list.len() <= max_meta_slots(),
395    {
396        reveal(LinkedListOwner::relate_region);
397        let idxs = Seq::new(self.list.len(), |i: int| meta_to_index(self.list[i].paddr));
398
399        idxs.unique_seq_to_set();
400
401        let bound = set_int_range(0, max_meta_slots());
402        assert(idxs.to_set().subset_of(bound)) by {
403            assert forall|x: int|
404                #![trigger idxs.to_set().contains(x)]
405                idxs.to_set().contains(x) implies bound.contains(x) by {
406                let i = choose|i: int| 0 <= i < idxs.len() && idxs[i] == x;
407                self.lemma_relate_region_at_facts(regions, i);
408                // `regions.inv()`: the contained slot index is `< max_meta_slots()`.
409            }
410        }
411        lemma_int_range(0, max_meta_slots());
412        lemma_len_subset(idxs.to_set(), bound);
413    }
414
415    /// The list counter can never saturate: its length is capped by
416    /// `max_meta_slots()` (see [`Self::lemma_length_le_max_meta_slots`]), which is far
417    /// below `usize::MAX`. Lets `insert_before` discharge the `size + 1`
418    /// overflow check without a caller-supplied non-fullness precondition.
419    pub proof fn lemma_length_lt_usize_max(self, regions: MetaRegionOwners)
420        requires
421            self.relate_region(regions),
422            regions.inv(),
423        ensures
424            self.list.len() < usize::MAX,
425    {
426        self.lemma_length_le_max_meta_slots(regions);
427    }
428
429    /// Unfolds the opaque `relate_region_at` ONCE and exposes its clauses.
430    /// `relate_region_at` is opaque to avoid quantifier explosion at use sites;
431    /// this lemma localizes the reveal so callers get
432    /// the facts at a single index without re-exploding the SMT context.
433    pub proof fn lemma_relate_region_at_facts(self, regions: MetaRegionOwners, i: int)
434        requires
435            self.relate_region_at(regions, i),
436        ensures
437            ({
438                let idx = meta_to_index(self.list[i].paddr);
439                let value = self.meta_value_at(regions, i);
440                &&& regions.contains(idx)
441                &&& regions.slots[idx].addr() == self.list[i].paddr
442                &&& regions.ref_count(idx) == REF_COUNT_UNIQUE
443                &&& regions.slot_owners[idx].metadata_perm.is_resource_vacant()
444                &&& self.metadata_perms[i].storage_perm.id()
445                    == regions.slots[idx].value().storage.id()
446                &&& self.metadata_perms[i].vtable_ptr_perm.pptr()
447                    == regions.slots[idx].value().vtable_ptr
448                &&& self.metadata_perms[i].vtable_ptr_perm.is_init()
449                &&& regions.slot_owners[idx].usage is Frame
450                &&& regions.slot_owners[idx].in_list_perm.value() == self.list_id
451                &&& self.meta_wf_at(regions, i)
452                &&& regions.slots[idx].addr() % META_SLOT_SIZE == 0
453                &&& FRAME_METADATA_RANGE.start <= regions.slots[idx].addr()
454                    < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
455                &&& value.wf(self.list[i])
456                &&& (i == 0 <==> value.prev is None)
457                &&& (i == self.list.len() - 1 <==> value.next is None)
458                &&& (0 < i ==> {
459                    &&& value.prev is Some
460                    &&& value.prev->0.addr() == self.meta_addr_at(regions, i - 1)
461                })
462                &&& (i < self.list.len() - 1 ==> {
463                    &&& value.next is Some
464                    &&& value.next->0.addr() == self.meta_addr_at(regions, i + 1)
465                })
466                &&& self.list[i].inv()
467                &&& self.list[i].in_list == self.list_id
468            }),
469    {
470        reveal(LinkedListOwner::relate_region_at);
471    }
472
473    /// Constructor (inverse of [`lemma_relate_region_at_facts`]): establishes the
474    /// opaque `relate_region_at` from its unfolded clauses. Used by the pop/
475    /// insert "surgery" proofs, which assemble each clause for the new list and
476    /// then fold them back into the opaque predicate.
477    pub proof fn lemma_relate_region_at_from_clauses(self, regions: MetaRegionOwners, i: int)
478        requires
479            ({
480                let idx = meta_to_index(self.list[i].paddr);
481                let value = self.meta_value_at(regions, i);
482                &&& regions.contains(idx)
483                &&& self.repr_perms.len() == self.list.len()
484                &&& self.metadata_perms.len() == self.list.len()
485                &&& regions.slots[idx].addr() == self.list[i].paddr
486                &&& regions.ref_count(idx) == REF_COUNT_UNIQUE
487                &&& regions.slot_owners[idx].metadata_perm.is_resource_vacant()
488                &&& self.metadata_perms[i].storage_perm.id()
489                    == regions.slots[idx].value().storage.id()
490                &&& self.metadata_perms[i].vtable_ptr_perm.pptr()
491                    == regions.slots[idx].value().vtable_ptr
492                &&& self.metadata_perms[i].vtable_ptr_perm.is_init()
493                &&& regions.slot_owners[idx].usage is Frame
494                &&& regions.slot_owners[idx].in_list_perm.value() == self.list_id
495                &&& self.meta_wf_at(regions, i)
496                &&& regions.slots[idx].addr() % META_SLOT_SIZE == 0
497                &&& FRAME_METADATA_RANGE.start <= regions.slots[idx].addr()
498                    < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
499                &&& value.wf(self.list[i])
500                &&& (i == 0 <==> value.prev is None)
501                &&& (i == self.list.len() - 1 <==> value.next is None)
502                &&& (0 < i ==> {
503                    &&& value.prev is Some
504                    &&& value.prev->0.addr() == self.meta_addr_at(regions, i - 1)
505                })
506                &&& (i < self.list.len() - 1 ==> {
507                    &&& value.next is Some
508                    &&& value.next->0.addr() == self.meta_addr_at(regions, i + 1)
509                })
510                &&& self.list[i].inv()
511                &&& self.list[i].in_list == self.list_id
512            }),
513        ensures
514            self.relate_region_at(regions, i),
515    {
516        reveal(LinkedListOwner::relate_region_at);
517    }
518
519    /// `relate_region` is preserved under a region change that doesn't touch
520    /// any of the list's slots. Used by `LinkedList::drop`'s loop body: after
521    /// `take_current` pops position 0, the popped slot is dropped via
522    /// `frame.drop`, which only modifies `regions.slot_owners[cur_idx]` and
523    /// leaves `regions.slots` fully untouched. Since the cursor's remaining
524    /// list never contains `cur_idx` (distinctness on the original list),
525    /// `relate_region` carries through.
526    pub proof fn lemma_relate_region_preserved_external_change(
527        self,
528        regions1: MetaRegionOwners,
529        regions2: MetaRegionOwners,
530    )
531        requires
532            self.relate_region(regions1),
533            regions2.slots == regions1.slots,
534            forall|i: int|
535                #![trigger self.list[i]]
536                0 <= i < self.list.len() ==> {
537                    let idx = meta_to_index(self.list[i].paddr);
538                    &&& regions2.contains(idx)
539                    &&& regions2.slot_owners[idx] == regions1.slot_owners[idx]
540                },
541        ensures
542            self.relate_region(regions2),
543    {
544        reveal(LinkedListOwner::relate_region);
545        let llen = self.list.len() as int;
546        assert forall|k: int|
547            #![trigger self.relate_region_at(regions2, k)]
548            0 <= k < llen implies self.relate_region_at(regions2, k) by {
549            let _ = self.list[k];
550            self.lemma_relate_region_at_facts(regions1, k);
551            self.lemma_relate_region_at_from_clauses(regions2, k);
552        }
553    }
554
555    /// The list-rewiring "surgery" for popping the element at index `n`: given
556    /// the entry invariant `old.relate_region(r0)` and a characterization of the
557    /// post-pop region `fr` (every surviving slot keeps its local facts and
558    /// pointers, except the two neighbors whose `next`/`prev` were rewired to
559    /// bridge the gap), the shrunk list `new` satisfies `relate_region(fr)`.
560    ///
561    /// New position `k` maps to old position `p = (k < n ? k : k+1)`; the
562    /// neighbor of `k` maps to `p ± 1` except across the cut (new position `n-1`
563    /// reaches old `n+1`, new position `n` reaches old `n-1`), which is exactly
564    /// where the body rewired the link pointers.
565    #[verifier::spinoff_prover]
566    #[verifier::rlimit(60)]
567    pub proof fn lemma_pop_preserves_relate_region(
568        old: LinkedListOwner<M>,
569        r0: MetaRegionOwners,
570        new: LinkedListOwner<M>,
571        fr: MetaRegionOwners,
572        n: int,
573    )
574        requires
575            0 <= n < old.list.len(),
576            old.relate_region(r0),
577            new.list == old.list.remove(n),
578            new.repr_perms.len() == new.list.len(),
579            new.metadata_perms.len() == new.list.len(),
580            new.list_id == old.list_id,
581            forall|p: int|
582                #![trigger meta_to_index(old.list[p].paddr)]
583                (0 <= p < old.list.len() && p != n) ==> ({
584                    let i = meta_to_index(old.list[p].paddr);
585                    let np = if p < n {
586                        p
587                    } else {
588                        p - 1
589                    };
590                    let fp = typed_meta_value::<Link<M>>(
591                        new.metadata_perms[np],
592                        new.repr_perms[np],
593                    );
594                    &&& fr.contains(i)
595                    &&& fr.slots[i].addr() == old.list[p].paddr
596                    &&& fr.slots[i].pptr() == r0.slots[i].pptr()
597                    &&& fr.ref_count(i) == REF_COUNT_UNIQUE
598                    &&& fr.slot_owners[i].metadata_perm.is_resource_vacant()
599                    &&& new.metadata_perms[np].storage_perm.id() == fr.slots[i].value().storage.id()
600                    &&& new.metadata_perms[np].vtable_ptr_perm.pptr()
601                        == fr.slots[i].value().vtable_ptr
602                    &&& new.metadata_perms[np].vtable_ptr_perm.is_init()
603                    &&& fr.slot_owners[i].usage is Frame
604                    &&& fr.slot_owners[i].in_list_perm.value() == new.list_id
605                    &&& typed_meta_wf::<Link<M>>(
606                        *fr.slots[i],
607                        new.metadata_perms[np],
608                        new.repr_perms[np],
609                    )
610                    &&& fr.slots[i].addr() % META_SLOT_SIZE == 0
611                    &&& FRAME_METADATA_RANGE.start <= fr.slots[i].addr()
612                        < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
613                    &&& (p == n - 1 ==> fp.next == old.meta_value_at(r0, n).next)
614                    &&& (p != n - 1 ==> fp.next == old.meta_value_at(r0, p).next)
615                    &&& (p == n + 1 ==> fp.prev == old.meta_value_at(r0, n).prev)
616                    &&& (p != n + 1 ==> fp.prev == old.meta_value_at(r0, p).prev)
617                }),
618        ensures
619            new.relate_region(fr),
620    {
621        reveal(LinkedListOwner::relate_region);
622        let nlen = new.list.len() as int;
623
624        assert forall|k: int| #![trigger meta_to_index(new.list[k].paddr)] 0 <= k < nlen implies {
625            let p = if k < n {
626                k
627            } else {
628                k + 1
629            };
630            &&& new.list[k] == old.list[p]
631            &&& meta_to_index(new.list[k].paddr) == meta_to_index(old.list[p].paddr)
632        } by {}
633
634        assert forall|a: int, b: int|
635            #![trigger meta_to_index(new.list[a].paddr), meta_to_index(new.list[b].paddr)]
636            0 <= a < nlen && 0 <= b < nlen && a != b implies meta_to_index(new.list[a].paddr)
637            != meta_to_index(new.list[b].paddr) by {
638            let pa = if a < n {
639                a
640            } else {
641                a + 1
642            };
643            let pb = if b < n {
644                b
645            } else {
646                b + 1
647            };
648        }
649
650        assert forall|m: int| #![trigger new.meta_addr_at(fr, m)] 0 <= m < nlen implies {
651            let pm = if m < n {
652                m
653            } else {
654                m + 1
655            };
656            &&& new.meta_addr_at(fr, m) == old.meta_addr_at(r0, pm)
657            &&& new.meta_pptr_at(fr, m) == old.meta_pptr_at(r0, pm)
658        } by {
659            let pm = if m < n {
660                m
661            } else {
662                m + 1
663            };
664            let _ = old.list[pm];
665            old.lemma_relate_region_at_facts(r0, pm);
666        }
667
668        assert forall|k: int|
669            #![trigger new.relate_region_at(fr, k)]
670            0 <= k < nlen implies new.relate_region_at(fr, k) by {
671            let p = if k < n {
672                k
673            } else {
674                k + 1
675            };
676            let _ = old.list[p];
677            old.lemma_relate_region_at_facts(r0, p);
678            let _ = old.list[n];
679            old.lemma_relate_region_at_facts(r0, n);
680            if p - 1 >= 0 {
681                let _ = old.list[p - 1];
682                old.lemma_relate_region_at_facts(r0, p - 1);
683            }
684            if p + 1 < old.list.len() {
685                let _ = old.list[p + 1];
686                old.lemma_relate_region_at_facts(r0, p + 1);
687            }
688            if n - 1 >= 0 {
689                let _ = old.list[n - 1];
690                old.lemma_relate_region_at_facts(r0, n - 1);
691            }
692            if n + 1 < old.list.len() {
693                old.lemma_relate_region_at_facts(r0, n + 1);
694            }
695            new.lemma_relate_region_at_from_clauses(fr, k);
696        }
697
698    }
699
700    /// The list-rewiring "surgery" for inserting `link` before index `n`
701    /// (`0 <= n <= old.list.len()`): given the entry `relate_region` and a
702    /// per-slot characterization of the post-insert region `fr`, the longer list
703    /// `new = old.list.insert(n, link)` satisfies `relate_region(fr)`.
704    ///
705    /// New position `k` maps to old position `k` (k<n), is the inserted link
706    /// (k==n), or maps to old `k-1` (k>n). The inserted link sits at slot
707    /// `ins = meta_to_index(new.list[n].paddr)`; its `prev`/`next` point to old `n-1`/`n`
708    /// (or `None` at the endsP), and old `n-1`'s `next` / old `n`'s `prev` are
709    /// rewired to point at the inserted link. Mirror of
710    /// [`lemma_pop_preserves_relate_region`].
711    pub open spec fn insert_old_slot_post_clauses(
712        self,
713        fr: MetaRegionOwners,
714        old: LinkedListOwner<M>,
715        r0: MetaRegionOwners,
716        n: int,
717        link: LinkOwner,
718        p: int,
719    ) -> bool {
720        let i = meta_to_index(old.list[p].paddr);
721        let ins = meta_to_index(self.list[n].paddr);
722        let np = if p < n {
723            p
724        } else {
725            p + 1
726        };
727        let fp = typed_meta_value::<Link<M>>(self.metadata_perms[np], self.repr_perms[np]);
728        &&& fr.contains(i)
729        &&& fr.slots[i].is_init()
730        &&& fr.slots[i].addr() == old.list[p].paddr
731        &&& fr.slots[i].pptr() == r0.slots[i].pptr()
732        &&& fr.ref_count(i) == REF_COUNT_UNIQUE
733        &&& fr.slot_owners[i].metadata_perm.is_resource_vacant()
734        &&& self.metadata_perms[np].storage_perm.id() == fr.slots[i].value().storage.id()
735        &&& self.metadata_perms[np].vtable_ptr_perm.pptr() == fr.slots[i].value().vtable_ptr
736        &&& self.metadata_perms[np].vtable_ptr_perm.is_init()
737        &&& fr.slot_owners[i].usage is Frame
738        &&& fr.slot_owners[i].in_list_perm.value() == self.list_id
739        &&& self.meta_wf_at(fr, np)
740        &&& fr.slots[i].addr() % META_SLOT_SIZE == 0
741        &&& FRAME_METADATA_RANGE.start <= fr.slots[i].addr() < FRAME_METADATA_RANGE.start
742            + MAX_NR_PAGES * META_SLOT_SIZE
743        &&& (p == n - 1 ==> {
744            &&& fp.next is Some
745            &&& fp.next->0.addr() == link.paddr
746            &&& fp.next->0.ptr.addr() == fr.slots[ins].pptr().addr()
747        })
748        &&& (p != n - 1 ==> fp.next == old.meta_value_at(r0, p).next)
749        &&& (p == n ==> {
750            &&& fp.prev is Some
751            &&& fp.prev->0.addr() == link.paddr
752            &&& fp.prev->0.ptr.addr() == fr.slots[ins].pptr().addr()
753        })
754        &&& (p != n ==> fp.prev == old.meta_value_at(r0, p).prev)
755    }
756
757    #[verifier::opaque]
758    pub open spec fn insert_old_slot_post_at(
759        self,
760        fr: MetaRegionOwners,
761        old: LinkedListOwner<M>,
762        r0: MetaRegionOwners,
763        n: int,
764        link: LinkOwner,
765        p: int,
766    ) -> bool {
767        self.insert_old_slot_post_clauses(fr, old, r0, n, link, p)
768    }
769
770    pub proof fn lemma_insert_old_slot_post_at_facts(
771        self,
772        fr: MetaRegionOwners,
773        old: LinkedListOwner<M>,
774        r0: MetaRegionOwners,
775        n: int,
776        link: LinkOwner,
777        p: int,
778    )
779        requires
780            self.insert_old_slot_post_at(fr, old, r0, n, link, p),
781        ensures
782            self.insert_old_slot_post_clauses(fr, old, r0, n, link, p),
783    {
784        reveal(LinkedListOwner::insert_old_slot_post_at);
785    }
786
787    #[verifier::spinoff_prover]
788    #[verifier::rlimit(120)]
789    pub proof fn lemma_insert_preserves_relate_region(
790        old: LinkedListOwner<M>,
791        r0: MetaRegionOwners,
792        new: LinkedListOwner<M>,
793        fr: MetaRegionOwners,
794        n: int,
795        link: LinkOwner,
796    )
797        requires
798            0 <= n <= old.list.len(),
799            old.relate_region(r0),
800            new.list == old.list.insert(n, link),
801            new.repr_perms.len() == new.list.len(),
802            new.metadata_perms.len() == new.list.len(),
803            new.list_id != 0,
804            old.list.len() > 0 ==> new.list_id == old.list_id,
805            link.inv(),
806            link.in_list == new.list_id,
807            forall|p: int|
808                #![trigger meta_to_index(old.list[p].paddr)]
809                (0 <= p < old.list.len()) ==> meta_to_index(old.list[p].paddr) != meta_to_index(
810                    new.list[n].paddr,
811                ),
812            ({
813                let ins = meta_to_index(new.list[n].paddr);
814                let fpn = new.meta_value_at(fr, n);
815                &&& fr.contains(ins)
816                &&& fr.slots[ins].is_init()
817                &&& fr.slots[ins].addr() == link.paddr
818                &&& fr.ref_count(ins) == REF_COUNT_UNIQUE
819                &&& fr.slot_owners[ins].metadata_perm.is_resource_vacant()
820                &&& new.metadata_perms[n].storage_perm.id() == fr.slots[ins].value().storage.id()
821                &&& new.metadata_perms[n].vtable_ptr_perm.pptr() == fr.slots[ins].value().vtable_ptr
822                &&& new.metadata_perms[n].vtable_ptr_perm.is_init()
823                &&& fr.slot_owners[ins].usage is Frame
824                &&& fr.slot_owners[ins].in_list_perm.value() == new.list_id
825                &&& new.meta_wf_at(fr, n)
826                &&& fr.slots[ins].addr() % META_SLOT_SIZE == 0
827                &&& FRAME_METADATA_RANGE.start <= fr.slots[ins].addr() < FRAME_METADATA_RANGE.start
828                    + MAX_NR_PAGES * META_SLOT_SIZE
829                &&& (n == 0 <==> fpn.prev is None)
830                &&& (n == old.list.len() <==> fpn.next is None)
831                &&& (n > 0 ==> {
832                    &&& fpn.prev is Some
833                    &&& fpn.prev->0.addr() == old.list[n - 1].paddr
834                    &&& fpn.prev->0.ptr.addr() == old.meta_pptr_at(r0, n - 1).addr()
835                })
836                &&& (n < old.list.len() ==> {
837                    &&& fpn.next is Some
838                    &&& fpn.next->0.addr() == old.list[n].paddr
839                    &&& fpn.next->0.ptr.addr() == old.meta_pptr_at(r0, n).addr()
840                })
841            }),
842            forall|p: int|
843                #![trigger new.insert_old_slot_post_at(fr, old, r0, n, link, p)]
844                (0 <= p < old.list.len()) ==> new.insert_old_slot_post_at(fr, old, r0, n, link, p),
845        ensures
846            new.relate_region(fr),
847    {
848        reveal(LinkedListOwner::relate_region);
849        let nlen = new.list.len() as int;
850        let ins = meta_to_index(new.list[n].paddr);
851
852        assert forall|k: int| #![trigger meta_to_index(new.list[k].paddr)] 0 <= k < nlen implies ({
853            &&& (k < n ==> new.list[k] == old.list[k] && meta_to_index(new.list[k].paddr)
854                == meta_to_index(old.list[k].paddr))
855            &&& (k == n ==> new.list[k] == link && meta_to_index(new.list[k].paddr) == ins)
856            &&& (k > n ==> new.list[k] == old.list[k - 1] && meta_to_index(new.list[k].paddr)
857                == meta_to_index(old.list[k - 1].paddr))
858        }) by {}
859
860        assert forall|a: int, b: int|
861            #![trigger meta_to_index(new.list[a].paddr), meta_to_index(new.list[b].paddr)]
862            0 <= a < nlen && 0 <= b < nlen && a != b implies meta_to_index(new.list[a].paddr)
863            != meta_to_index(new.list[b].paddr) by {}
864
865        assert forall|m: int| #![trigger new.meta_addr_at(fr, m)] 0 <= m < nlen implies ({
866            &&& (m < n ==> new.meta_addr_at(fr, m) == old.meta_addr_at(r0, m) && new.meta_pptr_at(
867                fr,
868                m,
869            ) == old.meta_pptr_at(r0, m))
870            &&& (m > n ==> new.meta_addr_at(fr, m) == old.meta_addr_at(r0, m - 1)
871                && new.meta_pptr_at(fr, m) == old.meta_pptr_at(r0, m - 1))
872        }) by {
873            if m < n {
874                let _ = old.list[m];
875                old.lemma_relate_region_at_facts(r0, m);
876                new.lemma_insert_old_slot_post_at_facts(fr, old, r0, n, link, m);
877            }
878            if m > n {
879                let _ = old.list[m - 1];
880                old.lemma_relate_region_at_facts(r0, m - 1);
881                new.lemma_insert_old_slot_post_at_facts(fr, old, r0, n, link, m - 1);
882            }
883        }
884
885        assert forall|k: int|
886            #![trigger new.relate_region_at(fr, k)]
887            0 <= k < nlen implies new.relate_region_at(fr, k) by {
888            if k < n {
889                let _ = old.list[k];
890                old.lemma_relate_region_at_facts(r0, k);
891                new.lemma_insert_old_slot_post_at_facts(fr, old, r0, n, link, k);
892            }
893            if k > n {
894                let _ = old.list[k - 1];
895                old.lemma_relate_region_at_facts(r0, k - 1);
896                new.lemma_insert_old_slot_post_at_facts(fr, old, r0, n, link, k - 1);
897            }
898            if n - 1 >= 0 && n - 1 < old.list.len() {
899                let _ = old.list[n - 1];
900                old.lemma_relate_region_at_facts(r0, n - 1);
901            }
902            if n >= 0 && n < old.list.len() {
903                let _ = old.list[n];
904                old.lemma_relate_region_at_facts(r0, n);
905            }
906            new.lemma_relate_region_at_from_clauses(fr, k);
907        }
908    }
909
910    pub open spec fn view_helper(owners: Seq<LinkOwner>) -> Seq<LinkModel>
911        decreases owners.len(),
912    {
913        if owners.len() == 0 {
914            Seq::<LinkModel>::empty()
915        } else {
916            seq![owners[0].view()].add(Self::view_helper(owners.remove(0)))
917        }
918    }
919
920    pub proof fn lemma_view_preserves_len(owners: Seq<LinkOwner>)
921        ensures
922            Self::view_helper(owners).len() == owners.len(),
923        decreases owners.len(),
924    {
925        if owners.len() > 0 {
926            Self::lemma_view_preserves_len(owners.remove(0))
927        }
928    }
929
930    /// Proves that view_helper preserves indexing: view_helper(s)[i] == s[i].view()
931    pub proof fn lemma_view_helper_index(owners: Seq<LinkOwner>, i: int)
932        requires
933            0 <= i < owners.len(),
934        ensures
935            Self::view_helper(owners)[i] == owners[i].view(),
936        decreases owners.len(),
937    {
938        Self::lemma_view_preserves_len(owners);
939        if i > 0 {
940            Self::lemma_view_helper_index(owners.remove(0), i - 1);
941        }
942    }
943
944    /// Proves that view_helper commutes with insert:
945    /// view_helper(s.insert(i, v)) == view_helper(s).insert(i, v.view())
946    pub proof fn lemma_view_helper_insert(owners: Seq<LinkOwner>, i: int, v: LinkOwner)
947        requires
948            0 <= i <= owners.len(),
949        ensures
950            Self::view_helper(owners.insert(i, v)) == Self::view_helper(owners).insert(i, v.view()),
951    {
952        Self::lemma_view_preserves_len(owners);
953        Self::lemma_view_preserves_len(owners.insert(i, v));
954        assert forall|j: int|
955            0 <= j < Self::view_helper(
956                owners.insert(i, v),
957            ).len() implies #[trigger] Self::view_helper(owners.insert(i, v))[j]
958            == Self::view_helper(owners).insert(i, v.view())[j] by {
959            Self::lemma_view_helper_index(owners.insert(i, v), j);
960            if j < i {
961                Self::lemma_view_helper_index(owners, j);
962            } else if j == i {
963                // owners.insert(i, v)[i] == v, and view_helper(owners).insert(i, v@)[i] == v@
964            } else {
965                Self::lemma_view_helper_index(owners, j - 1);
966            }
967        };
968    }
969}
970
971impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> View for LinkedListOwner<M> {
972    type V = LinkedListModel;
973
974    open spec fn view(&self) -> Self::V {
975        LinkedListModel { list: Self::view_helper(self.list) }
976    }
977}
978
979impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> InvView for LinkedListOwner<M> {
980    proof fn view_preserves_inv(self) {
981    }
982}
983
984impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedListOwner<M> {
985    /// Take ownership of `*owner` by swapping it with a fresh empty
986    /// `LinkedListOwner`. The resulting "leftover" `*owner` has an empty
987    /// `list`, so its `inv()` holds vacuously. Used by drop-style call sites
988    /// that need to feed an owned `LinkedListOwner` to a downstream API while
989    /// themselves only having a `&mut` to it.
990    pub proof fn tracked_take(tracked owner: &mut Self) -> (tracked res: Self)
991        ensures
992            res == *old(owner),
993            final(owner).list == Seq::<LinkOwner>::empty(),
994            final(owner).repr_perms == Seq::<LinkInnerPerms<M>>::empty(),
995            final(owner).metadata_perms == Seq::<MetadataPerm>::empty(),
996            final(owner).inv(),
997    {
998        let tracked mut tmp = crate::specs::mm::embedding::list_store::tracked_empty_list_owner::<
999            M,
1000        >();
1001        tracked_swap(owner, &mut tmp);
1002        tmp
1003    }
1004
1005    /// Discard a logically-empty `LinkedListOwner`. Sound because such an
1006    /// owner has an empty `list` and claims no external permissions (the
1007    /// borrow model parks all permissions in `MetaRegionOwners`).
1008    #[verifier::external_body]
1009    pub proof fn tracked_destroy_empty(tracked self)
1010        requires
1011            self.list =~= Seq::<LinkOwner>::empty(),
1012            self.repr_perms =~= Seq::<LinkInnerPerms<M>>::empty(),
1013            self.metadata_perms =~= Seq::<MetadataPerm>::empty(),
1014    {
1015        unimplemented!()
1016    }
1017}
1018
1019impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> OwnerOf for LinkedList<M> {
1020    type Owner = LinkedListOwner<M>;
1021
1022    /// Structural well-formedness of the LinkedList against its owner: size,
1023    /// list_id, and front/back addresses match. The per-link pointer-permission
1024    /// facts (pptr/ptr equality against the front/back) live in `wf_region`,
1025    /// which sources them from `MetaRegionOwners`.
1026    open spec fn wf(self, owner: Self::Owner) -> bool {
1027        &&& self.front is None <==> owner.list.len() == 0
1028        &&& self.back is None <==> owner.list.len() == 0
1029        &&& owner.list.len() > 0 ==> self.front is Some && self.front->0.addr()
1030            == owner.list[0].paddr && self.back is Some && self.back->0.addr()
1031            == owner.list[owner.list.len() - 1].paddr
1032        &&& self.size == owner.list.len()
1033        &&& self.list_id == owner.list_id
1034    }
1035}
1036
1037pub ghost struct CursorModel {
1038    pub ghost fore: Seq<LinkModel>,
1039    pub ghost rear: Seq<LinkModel>,
1040    pub ghost list_model: LinkedListModel,
1041}
1042
1043impl Inv for CursorModel {
1044    open spec fn inv(self) -> bool {
1045        self.list_model.inv()
1046    }
1047}
1048
1049pub tracked struct CursorOwner<M: AnyFrameMeta + Repr<MetaSlotSmall>> {
1050    pub list_own: LinkedListOwner<M>,
1051    pub ghost index: int,
1052}
1053
1054impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Inv for CursorOwner<M> {
1055    open spec fn inv(self) -> bool {
1056        &&& 0 <= self.index <= self.length()
1057        &&& self.list_own.inv()
1058    }
1059}
1060
1061impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> View for CursorOwner<M> {
1062    type V = CursorModel;
1063
1064    open spec fn view(&self) -> Self::V {
1065        let list = self.list_own.view();
1066        CursorModel {
1067            fore: list.list[..self.index],
1068            rear: list.list[self.index..],
1069            list_model: list,
1070        }
1071    }
1072}
1073
1074impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> InvView for CursorOwner<M> {
1075    proof fn view_preserves_inv(self) {
1076    }
1077}
1078
1079impl<'a, M: AnyFrameMeta + Repr<MetaSlotSmall>> OwnerOf for CursorMut<'a, M> {
1080    type Owner = CursorOwner<M>;
1081
1082    /// Structural well-formedness: `current` matches the link at `index`'s
1083    /// address. Pointer-permission facts (pptr/ptr equality) are stated in
1084    /// `wf_region` over the region-owned slot pointers.
1085    open spec fn wf(self, owner: Self::Owner) -> bool {
1086        &&& 0 <= owner.index < owner.length() ==> self.current.is_some() && self.current->0.addr()
1087            == owner.list_own.list[owner.index].paddr
1088        &&& owner.index == owner.list_own.list.len() ==> self.current.is_none()
1089        &&& (*self.list).wf(owner.list_own)
1090    }
1091}
1092
1093impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedList<M> {
1094    /// Region-based analog of [`LinkedList::wf`]: the front/back pointer facts
1095    /// are stated directly over the region-owned slot pointers.
1096    pub open spec fn wf_region(self, owner: LinkedListOwner<M>, regions: MetaRegionOwners) -> bool {
1097        &&& self.front is None <==> owner.list.len() == 0
1098        &&& self.back is None <==> owner.list.len() == 0
1099        &&& owner.list.len() > 0 ==> self.front is Some && self.front->0.addr()
1100            == owner.list[0].paddr && owner.meta_pptr_at(regions, 0).addr() == self.front->0.addr()
1101            && self.back is Some && self.back->0.addr() == owner.list[owner.list.len() - 1].paddr
1102            && owner.meta_pptr_at(regions, owner.list.len() - 1).addr() == self.back->0.addr()
1103        &&& self.size == owner.list.len()
1104        &&& self.list_id == owner.list_id
1105    }
1106}
1107
1108impl<'a, M: AnyFrameMeta + Repr<MetaSlotSmall>> CursorMut<'a, M> {
1109    /// Region-based analog of [`CursorMut::wf`]: the current-link pointer facts
1110    /// are stated over the corresponding region-owned slot pointer.
1111    pub open spec fn wf_region(self, owner: CursorOwner<M>, regions: MetaRegionOwners) -> bool {
1112        &&& 0 <= owner.index < owner.length() ==> self.current.is_some() && self.current->0.addr()
1113            == owner.list_own.list[owner.index].paddr && owner.list_own.meta_pptr_at(
1114            regions,
1115            owner.index,
1116        ).addr() == self.current->0.addr()
1117        &&& owner.index == owner.list_own.list.len() ==> self.current.is_none()
1118        &&& (*self.list).wf_region(owner.list_own, regions)
1119    }
1120}
1121
1122impl CursorModel {
1123    pub open spec fn current(self) -> Option<LinkModel> {
1124        if self.rear.len() > 0 {
1125            Some(self.rear[0])
1126        } else {
1127            None
1128        }
1129    }
1130}
1131
1132impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> CursorOwner<M> {
1133    pub open spec fn length(self) -> int {
1134        self.list_own.list.len() as int
1135    }
1136
1137    /// Region-based analog of [`CursorOwner::inv`]: replaces `list_own.inv()`
1138    /// (over the owned `perms`) with `list_own.relate_region(regions)` (over
1139    /// the region permissions).
1140    pub open spec fn wf_with_region(self, regions: MetaRegionOwners) -> bool {
1141        &&& 0 <= self.index <= self.length()
1142        &&& self.list_own.relate_region(regions)
1143    }
1144
1145    pub open spec fn current(self) -> Option<LinkOwner> {
1146        if 0 <= self.index < self.length() {
1147            Some(self.list_own.list[self.index])
1148        } else {
1149            None
1150        }
1151    }
1152
1153    pub open spec fn list_insert(
1154        cursor: Self,
1155        link: LinkOwner,
1156        repr_perm: LinkInnerPerms<M>,
1157        metadata_perms: MetadataPerm,
1158        list_id: u64,
1159    ) -> (Self, LinkOwner) {
1160        let link = LinkOwner { paddr: link.paddr, in_list: list_id };
1161        (
1162            Self {
1163                list_own: LinkedListOwner::<M> {
1164                    list: cursor.list_own.list.insert(cursor.index, link),
1165                    repr_perms: cursor.list_own.repr_perms.insert(cursor.index, repr_perm),
1166                    metadata_perms: cursor.list_own.metadata_perms.insert(
1167                        cursor.index,
1168                        metadata_perms,
1169                    ),
1170                    list_id,
1171                    _marker: PhantomData,
1172                },
1173                index: cursor.index + 1,
1174            },
1175            link,
1176        )
1177    }
1178
1179    /// Tracked update to the cursor's owner state when a new link is inserted
1180    /// before the current position. The inserted `link`'s `paddr` is unchanged
1181    /// and its `in_list` is stamped with `list_id` — the (non-zero) id the
1182    /// concrete `lazy_get_id` resolved. The cursor's list gains `link` at
1183    /// `old.index`, adopts `list_id` (which equals the old id when that was
1184    /// already non-zero), and `index` advances by one. In the borrow model, the
1185    /// link's tracked permission remains parked in `MetaRegionOwners.slots`;
1186    /// this axiom doesn't need to take or carry a perm.
1187    pub proof fn tracked_list_insert(
1188        tracked cursor: &mut Self,
1189        tracked link: &mut LinkOwner,
1190        tracked repr_perm: LinkInnerPerms<M>,
1191        tracked metadata_perms: MetadataPerm,
1192        list_id: u64,
1193    )
1194        requires
1195            list_id != 0,
1196            0 <= old(cursor).index <= old(cursor).list_own.list.len(),
1197            old(cursor).list_own.repr_perms.len() == old(cursor).list_own.list.len(),
1198            old(cursor).list_own.metadata_perms.len() == old(cursor).list_own.list.len(),
1199            old(cursor).list_own.list.len() > 0 ==> list_id == old(cursor).list_own.list_id,
1200            old(cursor).list_own.list_id != 0 ==> list_id == old(cursor).list_own.list_id,
1201        ensures
1202            ({
1203                let res = Self::list_insert(
1204                    *old(cursor),
1205                    *old(link),
1206                    repr_perm,
1207                    metadata_perms,
1208                    list_id,
1209                );
1210
1211                res.0 == *final(cursor) && res.1 == *final(link)
1212            }),
1213    {
1214        let ghost idx = cursor.index;
1215        let ghost link_paddr = link.paddr;
1216        let tracked list_entry = LinkOwner { paddr: link_paddr, in_list: list_id };
1217
1218        cursor.list_own.list.tracked_insert(idx, list_entry);
1219        cursor.list_own.repr_perms.tracked_insert(idx, repr_perm);
1220        cursor.list_own.metadata_perms.tracked_insert(idx, metadata_perms);
1221        cursor.list_own.list_id = list_id;
1222        cursor.index = idx + 1;
1223        *link = LinkOwner { paddr: link_paddr, in_list: list_id };
1224    }
1225
1226    pub open spec fn front_owner(list_own: LinkedListOwner<M>) -> Self {
1227        CursorOwner::<M> { list_own: list_own, index: 0 }
1228    }
1229
1230    pub open spec fn cursor_mut_at_owner(list_own: LinkedListOwner<M>, index: int) -> Self {
1231        CursorOwner::<M> { list_own: list_own, index: index }
1232    }
1233
1234    pub proof fn tracked_cursor_mut_at_owner(
1235        tracked list_own: LinkedListOwner<M>,
1236        index: int,
1237    ) -> tracked Self
1238        returns
1239            Self::cursor_mut_at_owner(list_own, index),
1240    {
1241        let tracked res = CursorOwner::<M> { list_own, index };
1242        res
1243    }
1244
1245    pub proof fn tracked_front_owner(tracked list_own: LinkedListOwner<M>) -> tracked Self
1246        returns
1247            Self::front_owner(list_own),
1248    {
1249        let tracked res = CursorOwner::<M> { list_own, index: 0 };
1250        res
1251    }
1252
1253    pub open spec fn back_owner(list_own: LinkedListOwner<M>) -> Self {
1254        CursorOwner::<M> {
1255            list_own: list_own,
1256            index: if list_own.list.len() > 0 {
1257                list_own.list.len() - 1
1258            } else {
1259                0
1260            },
1261        }
1262    }
1263
1264    pub proof fn tracked_back_owner(tracked list_own: LinkedListOwner<M>) -> (tracked res: Self)
1265        ensures
1266            res == Self::back_owner(list_own),
1267    {
1268        CursorOwner::<M> {
1269            list_own: list_own,
1270            index: if list_own.list.len() > 0 {
1271                list_own.list.len() - 1
1272            } else {
1273                0
1274            },
1275        }
1276    }
1277}
1278
1279impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> UniqueFrameOwner<Link<M>> {
1280    pub open spec fn frame_link_inv(&self, regions: MetaRegionOwners) -> bool {
1281        &&& self.meta_value(regions).prev is None
1282        &&& self.meta_value(regions).next is None
1283        &&& self.meta_own.paddr == regions.slots[self.slot_index].addr()
1284        &&& regions.slot_owners[self.slot_index].in_list_perm.value() == 0
1285    }
1286}
1287
1288impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> UniqueFrame<Link<M>> {
1289    pub open spec fn frame_link_inv(
1290        self,
1291        owner: UniqueFrameOwner<Link<M>>,
1292        regions: MetaRegionOwners,
1293    ) -> bool {
1294        &&& self.meta_value(owner).prev is None
1295        &&& self.meta_value(owner).next is None
1296        &&& owner.meta_own.paddr == regions.slots[owner.slot_index].addr()
1297        &&& regions.slot_owners[owner.slot_index].in_list_perm.value() == 0
1298    }
1299}
1300
1301} // verus!
ostd/specs/mm/frame/linked_list/linked_list_owners.rs

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