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

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

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