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

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

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