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

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

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