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::simple_pptr::*;
6
7use vstd::std_specs::convert::FromSpecImpl;
8use vstd_extra::cast_ptr::{Repr, ReprPtr};
9use vstd_extra::ownership::*;
10
11use core::marker::PhantomData;
12
13use super::*;
14use crate::mm::frame::{AnyFrameMeta, CursorMut, Link, LinkedList, MetaSlot};
15use crate::mm::Paddr;
16use crate::specs::arch::kspace::FRAME_METADATA_RANGE;
17use crate::specs::arch::mm::MAX_NR_PAGES;
18use crate::specs::mm::frame::mapping::META_SLOT_SIZE;
19use crate::specs::mm::frame::meta_owners::*;
20use crate::specs::mm::frame::meta_owners::*;
21use crate::specs::mm::frame::unique::UniqueFrameOwner;
22
23verus! {
24
25pub struct MetaSlotSmall;
26
27/// Representation of a link as stored in the metadata slot.
28pub struct StoredLink {
29    pub next: Option<Paddr>,
30    pub prev: Option<Paddr>,
31    pub slot: MetaSlotSmall,
32}
33
34pub struct LinkInnerPerms {
35    pub storage: cell::PointsTo<MetaSlotSmall>,
36}
37
38impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> AnyFrameMeta for Link<M> {
39    fn on_drop(&mut self) {
40    }
41
42    fn is_untyped(&self) -> bool {
43        false
44    }
45
46    uninterp spec fn vtable_ptr(&self) -> usize;
47}
48
49impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Repr<MetaSlotStorage> for Link<M> {
50    type Perm = LinkInnerPerms;
51
52    uninterp spec fn wf(r: MetaSlotStorage, perm: LinkInnerPerms) -> bool;
53
54    uninterp spec fn to_repr_spec(self, perm: LinkInnerPerms) -> (MetaSlotStorage, LinkInnerPerms);
55
56    #[verifier::external_body]
57    fn to_repr(self, Tracked(perm): Tracked<&mut LinkInnerPerms>) -> MetaSlotStorage {
58        unimplemented!()
59    }
60
61    uninterp spec fn from_repr_spec(r: MetaSlotStorage, perm: LinkInnerPerms) -> Self;
62
63    #[verifier::external_body]
64    fn from_repr(r: MetaSlotStorage, Tracked(perm): Tracked<&LinkInnerPerms>) -> Self {
65        unimplemented!()
66    }
67
68    #[verifier::external_body]
69    fn from_borrowed<'a>(r: &'a MetaSlotStorage, Tracked(perm): Tracked<&'a LinkInnerPerms>) -> &'a Self {
70        unimplemented!()
71    }
72
73    proof fn from_to_repr(self, perm: LinkInnerPerms) {
74        admit();
75    }
76
77    proof fn to_from_repr(r: MetaSlotStorage, perm: LinkInnerPerms) {
78        admit();
79    }
80
81    proof fn to_repr_wf(self, perm: LinkInnerPerms) {
82        admit();
83    }
84}
85
86pub ghost struct LinkModel {
87    pub paddr: Paddr,
88}
89
90impl Inv for LinkModel {
91    open spec fn inv(self) -> bool {
92        true
93    }
94}
95
96pub tracked struct LinkOwner {
97    pub paddr: Paddr,
98    pub in_list: u64,
99}
100
101impl Inv for LinkOwner {
102    open spec fn inv(self) -> bool {
103        true
104    }
105}
106
107impl View for LinkOwner {
108    type V = LinkModel;
109
110    open spec fn view(&self) -> Self::V {
111        LinkModel { paddr: self.paddr }
112    }
113}
114
115impl InvView for LinkOwner {
116    proof fn view_preserves_inv(self) {
117    }
118}
119
120impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> OwnerOf for Link<M> {
121    type Owner = LinkOwner;
122
123    open spec fn wf(self, owner: Self::Owner) -> bool {
124        true
125        //        &&& owner.self_perm@.mem_contents().value() == self
126        //        &&& owner.next == self.next
127        //        &&& owner.prev == self.prev
128
129    }
130}
131
132impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> ModelOf for Link<M> {
133
134}
135
136pub ghost struct LinkedListModel {
137    pub list: Seq<LinkModel>,
138}
139
140impl LinkedListModel {
141    pub open spec fn front(self) -> Option<LinkModel> {
142        if self.list.len() > 0 {
143            Some(self.list[0])
144        } else {
145            None
146        }
147    }
148
149    pub open spec fn back(self) -> Option<LinkModel> {
150        if self.list.len() > 0 {
151            Some(self.list[self.list.len() - 1])
152        } else {
153            None
154        }
155    }
156}
157
158impl Inv for LinkedListModel {
159    open spec fn inv(self) -> bool {
160        true
161    }
162}
163
164pub tracked struct LinkedListOwner<M: AnyFrameMeta + Repr<MetaSlotSmall>> {
165    pub list: Seq<LinkOwner>,
166    pub perms: Map<int, vstd_extra::cast_ptr::PointsTo<MetaSlot, Metadata<Link<M>>>>,
167    pub list_id: u64,
168}
169
170impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Inv for LinkedListOwner<M> {
171    open spec fn inv(self) -> bool {
172        forall|i: int| 0 <= i < self.list.len() ==> self.inv_at(i)
173    }
174}
175
176impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedListOwner<M> {
177    pub open spec fn inv_at(self, i: int) -> bool {
178        &&& self.perms.contains_key(i)
179        &&& self.perms[i].addr() == self.list[i].paddr
180        &&& self.perms[i].points_to.addr() == self.list[i].paddr
181        &&& self.perms[i].wf(&self.perms[i].inner_perms)
182        &&& self.perms[i].addr() % META_SLOT_SIZE == 0
183        &&& FRAME_METADATA_RANGE.start <= self.perms[i].addr() < FRAME_METADATA_RANGE.start
184            + MAX_NR_PAGES * META_SLOT_SIZE
185        &&& self.perms[i].is_init()
186        &&& self.perms[i].value().metadata.wf(self.list[i])
187        &&& i == 0 <==> self.perms[i].value().metadata.prev is None
188        &&& i == self.list.len() - 1 <==> self.perms[i].value().metadata.next is None
189        &&& 0 < i ==> {
190            &&& self.perms[i].value().metadata.prev is Some
191            &&& self.perms[i].value().metadata.prev.unwrap().addr() == self.perms[i - 1].addr()
192            &&& self.perms[i].value().metadata.prev.unwrap().ptr == self.perms[i - 1].points_to.pptr()
193        }
194        &&& i < self.list.len() - 1 ==> {
195            &&& self.perms[i].value().metadata.next is Some
196            &&& self.perms[i].value().metadata.next.unwrap().addr() == self.perms[i + 1].addr()
197            &&& self.perms[i].value().metadata.next.unwrap().ptr == self.perms[i + 1].points_to.pptr()
198        }
199        &&& self.list[i].inv()
200        &&& self.list[i].in_list == self.list_id
201    }
202
203    pub open spec fn view_helper(owners: Seq<LinkOwner>) -> Seq<LinkModel>
204        decreases owners.len(),
205    {
206        if owners.len() == 0 {
207            Seq::<LinkModel>::empty()
208        } else {
209            seq![owners[0].view()].add(Self::view_helper(owners.remove(0)))
210        }
211    }
212
213    pub proof fn view_preserves_len(owners: Seq<LinkOwner>)
214        ensures
215            Self::view_helper(owners).len() == owners.len(),
216        decreases owners.len(),
217    {
218        if owners.len() == 0 {
219        } else {
220            Self::view_preserves_len(owners.remove(0))
221        }
222    }
223
224    /// Proves that view_helper preserves indexing: view_helper(s)[i] == s[i].view()
225    pub proof fn view_helper_index(owners: Seq<LinkOwner>, i: int)
226        requires
227            0 <= i < owners.len(),
228        ensures
229            Self::view_helper(owners)[i] == owners[i].view(),
230        decreases owners.len(),
231    {
232        Self::view_preserves_len(owners);
233        if i > 0 {
234            Self::view_helper_index(owners.remove(0), i - 1);
235        }
236    }
237
238    /// Proves that view_helper commutes with remove:
239    /// view_helper(s.remove(i)) =~= view_helper(s).remove(i)
240    pub proof fn view_helper_remove(owners: Seq<LinkOwner>, i: int)
241        requires
242            0 <= i < owners.len(),
243        ensures
244            Self::view_helper(owners.remove(i)) =~= Self::view_helper(owners).remove(i),
245    {
246        Self::view_preserves_len(owners);
247        Self::view_preserves_len(owners.remove(i));
248        assert forall |j: int| 0 <= j < Self::view_helper(owners.remove(i)).len() implies
249            Self::view_helper(owners.remove(i))[j] == Self::view_helper(owners).remove(i)[j]
250        by {
251            Self::view_helper_index(owners.remove(i), j);
252            if j < i {
253                Self::view_helper_index(owners, j);
254            } else {
255                Self::view_helper_index(owners, j + 1);
256            }
257        };
258    }
259
260    /// Proves that view_helper commutes with insert:
261    /// view_helper(s.insert(i, v)) =~= view_helper(s).insert(i, v.view())
262    pub proof fn view_helper_insert(owners: Seq<LinkOwner>, i: int, v: LinkOwner)
263        requires
264            0 <= i <= owners.len(),
265        ensures
266            Self::view_helper(owners.insert(i, v)) =~= Self::view_helper(owners).insert(i, v.view()),
267    {
268        Self::view_preserves_len(owners);
269        Self::view_preserves_len(owners.insert(i, v));
270        assert forall |j: int| 0 <= j < Self::view_helper(owners.insert(i, v)).len() implies
271            #[trigger] Self::view_helper(owners.insert(i, v))[j] == Self::view_helper(owners).insert(i, v.view())[j]
272        by {
273            Self::view_helper_index(owners.insert(i, v), j);
274            if j < i {
275                Self::view_helper_index(owners, j);
276            } else if j == i {
277                // owners.insert(i, v)[i] == v, and view_helper(owners).insert(i, v@)[i] == v@
278            } else {
279                Self::view_helper_index(owners, j - 1);
280            }
281        };
282    }
283}
284
285impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> View for LinkedListOwner<M> {
286    type V = LinkedListModel;
287
288    open spec fn view(&self) -> Self::V {
289        LinkedListModel { list: Self::view_helper(self.list) }
290    }
291}
292
293impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> InvView for LinkedListOwner<M> {
294    proof fn view_preserves_inv(self) {
295    }
296}
297
298impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> OwnerOf for LinkedList<M> {
299    type Owner = LinkedListOwner<M>;
300
301    open spec fn wf(self, owner: Self::Owner) -> bool {
302        &&& self.front is None <==> owner.list.len() == 0
303        &&& self.back is None <==> owner.list.len() == 0
304        &&& owner.list.len() > 0 ==> self.front is Some && self.front.unwrap().addr()
305            == owner.list[0].paddr && owner.perms[0].pptr().addr() == self.front.unwrap().addr()
306            && self.front.unwrap().ptr == owner.perms[0].points_to.pptr()
307            && self.back is Some && self.back.unwrap().addr() == owner.list[owner.list.len()
308            - 1].paddr && owner.perms[owner.list.len() - 1].pptr().addr() == self.back.unwrap().addr()
309            && self.back.unwrap().ptr == owner.perms[owner.list.len() - 1].points_to.pptr()
310        &&& self.size == owner.list.len()
311        &&& self.list_id == owner.list_id
312    }
313}
314
315impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> ModelOf for LinkedList<M> {
316
317}
318
319pub ghost struct CursorModel {
320    pub ghost fore: Seq<LinkModel>,
321    pub ghost rear: Seq<LinkModel>,
322    pub ghost list_model: LinkedListModel,
323}
324
325impl Inv for CursorModel {
326    open spec fn inv(self) -> bool {
327        self.list_model.inv()
328    }
329}
330
331pub tracked struct CursorOwner<M: AnyFrameMeta + Repr<MetaSlotSmall>> {
332    pub list_own: LinkedListOwner<M>,
333    pub list_perm: PointsTo<LinkedList<M>>,
334    pub index: int,
335}
336
337impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Inv for CursorOwner<M> {
338    open spec fn inv(self) -> bool {
339        &&& 0 <= self.index <= self.length()
340        &&& self.list_own.inv()
341    }
342}
343
344impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> View for CursorOwner<M> {
345    type V = CursorModel;
346
347    open spec fn view(&self) -> Self::V {
348        let list = self.list_own.view();
349        CursorModel {
350            fore: list.list.take(self.index),
351            rear: list.list.skip(self.index),
352            list_model: list,
353        }
354    }
355}
356
357impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> InvView for CursorOwner<M> {
358    proof fn view_preserves_inv(self) {
359    }
360}
361
362impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> OwnerOf for CursorMut<M> {
363    type Owner = CursorOwner<M>;
364
365    open spec fn wf(self, owner: Self::Owner) -> bool {
366        &&& 0 <= owner.index < owner.length() ==> self.current.is_some()
367            && self.current.unwrap().addr() == owner.list_own.list[owner.index].paddr
368            && owner.list_own.perms[owner.index].pptr().addr() == self.current.unwrap().addr()
369            && self.current.unwrap().ptr == owner.list_own.perms[owner.index].points_to.pptr()
370        &&& owner.index == owner.list_own.list.len() ==> self.current.is_none()
371        &&& owner.list_perm.pptr() == self.list
372        &&& owner.list_perm.is_init()
373        &&& owner.list_perm.mem_contents().value().wf(owner.list_own)
374    }
375}
376
377impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> ModelOf for CursorMut<M> {
378
379}
380
381impl CursorModel {
382    pub open spec fn current(self) -> Option<LinkModel> {
383        if self.rear.len() > 0 {
384            Some(self.rear[0])
385        } else {
386            None
387        }
388    }
389}
390
391impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> CursorOwner<M> {
392    pub open spec fn length(self) -> int {
393        self.list_own.list.len() as int
394    }
395
396    pub open spec fn current(self) -> Option<LinkOwner> {
397        if 0 <= self.index < self.length() {
398            Some(self.list_own.list[self.index])
399        } else {
400            None
401        }
402    }
403
404    pub axiom fn list_insert(
405        tracked cursor: &mut Self,
406        tracked link: &mut LinkOwner,
407        tracked perm: &vstd_extra::cast_ptr::PointsTo<MetaSlot, Metadata<Link<M>>>,
408    )
409        ensures
410            link.paddr == old(link).paddr,
411            link.in_list == cursor.list_own.list_id,
412            cursor.list_own.list == old(cursor).list_own.list.insert(old(cursor).index, *link),
413            cursor.list_own.list_id == old(cursor).list_own.list_id,
414            forall|idx: int| 0 <= idx < cursor.length() ==> cursor.list_own.perms.contains_key(idx),
415            forall|idx: int|
416                0 <= idx < cursor.index ==> cursor.list_own.perms[idx] == old(
417                    cursor,
418                ).list_own.perms[idx],
419            forall|idx: int|
420                old(cursor).index < idx <= old(cursor).length() ==> cursor.list_own.perms[idx]
421                    == old(cursor).list_own.perms[idx - 1],
422            cursor.list_own.perms[old(cursor).index] == perm,
423            cursor.index == old(cursor).index + 1,
424            cursor.list_perm == old(cursor).list_perm;
425
426    pub open spec fn front_owner_spec(
427        list_own: LinkedListOwner<M>,
428        list_perm: PointsTo<LinkedList<M>>,
429    ) -> Self {
430        CursorOwner::<M> { list_own: list_own, list_perm: list_perm, index: 0 }
431    }
432
433    pub open spec fn cursor_mut_at_owner_spec(
434        list_own: LinkedListOwner<M>,
435        list_perm: PointsTo<LinkedList<M>>,
436        index: int,
437    ) -> Self {
438        CursorOwner::<M> { list_own: list_own, list_perm: list_perm, index: index }
439    }
440
441    #[verifier::returns(proof)]
442    pub axiom fn cursor_mut_at_owner(list_own: LinkedListOwner<M>, list_perm: PointsTo<LinkedList<M>>, index: int) -> Self
443        returns Self::cursor_mut_at_owner_spec(list_own, list_perm, index);
444
445    #[verifier::returns(proof)]
446    pub axiom fn front_owner(
447        list_own: LinkedListOwner<M>,
448        list_perm: PointsTo<LinkedList<M>>,
449    ) -> (res: Self)
450        ensures
451            res == Self::front_owner_spec(list_own, list_perm);
452    pub open spec fn back_owner_spec(
453        list_own: LinkedListOwner<M>,
454        list_perm: PointsTo<LinkedList<M>>,
455    ) -> Self {
456        CursorOwner::<M> {
457            list_own: list_own,
458            list_perm: list_perm,
459            index: if list_own.list.len() > 0 {
460                list_own.list.len() as int - 1
461            } else {
462                0
463            },
464        }
465    }
466
467    #[verifier::returns(proof)]
468    #[verifier::external_body]
469    pub proof fn back_owner(
470        list_own: LinkedListOwner<M>,
471        list_perm: PointsTo<LinkedList<M>>,
472    ) -> (res: Self)
473        ensures
474            res == Self::back_owner_spec(list_own, list_perm),
475    {
476        CursorOwner::<M> {
477            list_own: list_own,
478            list_perm: list_perm,
479            index: if list_own.list.len() > 0 {
480                list_own.list.len() as int - 1
481            } else {
482                0
483            },
484        }
485    }
486
487    pub open spec fn ghost_owner_spec(
488        list_own: LinkedListOwner<M>,
489        list_perm: PointsTo<LinkedList<M>>,
490    ) -> Self {
491        CursorOwner::<M> {
492            list_own: list_own,
493            list_perm: list_perm,
494            index: list_own.list.len() as int,
495        }
496    }
497
498    #[verifier::returns(proof)]
499    #[verifier::external_body]
500    pub proof fn ghost_owner(
501        list_own: LinkedListOwner<M>,
502        list_perm: PointsTo<LinkedList<M>>,
503    ) -> (res: Self)
504        ensures
505            res == Self::ghost_owner_spec(list_own, list_perm),
506    {
507        CursorOwner::<M> {
508            list_own: list_own,
509            list_perm: list_perm,
510            index: list_own.list.len() as int,
511        }
512    }
513}
514
515impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> UniqueFrameOwner<Link<M>> {
516    pub open spec fn frame_link_inv(&self) -> bool {
517        &&& self.meta_perm.value().metadata.prev is None
518        &&& self.meta_perm.value().metadata.next is None
519        &&& self.meta_own.paddr == self.meta_perm.addr()
520    }
521}
522
523pub struct MetadataAsLink<M: AnyFrameMeta> {
524    pub metadata: M,
525    pub next: Option<PPtr<MetaSlot>>,
526    pub prev: Option<PPtr<MetaSlot>>,
527    pub ref_count: u64,
528    pub vtable_ptr: MemContents<usize>,
529    pub in_list: u64,
530}
531
532impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Repr<MetaSlot> for MetadataAsLink<M> {
533    type Perm = MetadataInnerPerms;
534
535    uninterp spec fn wf(r: MetaSlot, perm: MetadataInnerPerms) -> bool;
536
537    uninterp spec fn to_repr_spec(self, perm: MetadataInnerPerms) -> (MetaSlot, MetadataInnerPerms);
538    #[verifier::external_body]
539    fn to_repr(self, Tracked(perm): Tracked<&mut MetadataInnerPerms>) -> MetaSlot {
540        unimplemented!()
541    }
542
543    uninterp spec fn from_repr_spec(r: MetaSlot, perm: MetadataInnerPerms) -> Self;
544
545    #[verifier::external_body]
546    fn from_repr(r: MetaSlot, Tracked(perm): Tracked<&MetadataInnerPerms>) -> Self {
547        unimplemented!()
548    }
549
550    #[verifier::external_body]
551    fn from_borrowed<'a>(r: &'a MetaSlot, Tracked(perm): Tracked<&'a MetadataInnerPerms>) -> &'a Self {
552        unimplemented!()
553    }
554
555    proof fn from_to_repr(self, perm: MetadataInnerPerms) {
556        admit();
557    }
558
559    proof fn to_from_repr(r: MetaSlot, perm: MetadataInnerPerms) {
560        admit();
561    }
562
563    proof fn to_repr_wf(self, perm: MetadataInnerPerms) {
564        admit();
565    }
566
567}
568
569impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> FromSpecImpl<Metadata<Link<M>>> for MetadataAsLink<M> {
570    open spec fn obeys_from_spec() -> bool {
571        true
572    }
573
574    open spec fn from_spec(m: Metadata<Link<M>>) -> MetadataAsLink<M> {
575        MetadataAsLink {
576            metadata: m.metadata.meta,
577            next: match m.metadata.next {
578                Some(repr_ptr) => Some(repr_ptr.ptr),
579                None => None,
580            },
581            prev: match m.metadata.prev {
582                Some(repr_ptr) => Some(repr_ptr.ptr),
583                None => None,
584            },
585            ref_count: m.ref_count,
586            vtable_ptr: m.vtable_ptr,
587            in_list: m.in_list,
588        }
589    }
590}
591
592impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> From<Metadata<Link<M>>> for MetadataAsLink<M> {
593    fn from(m: Metadata<Link<M>>) -> Self {
594        let next = match m.metadata.next {
595            Some(repr_ptr) => Some(repr_ptr.ptr),
596            None => None,
597        };
598        let prev = match m.metadata.prev {
599            Some(repr_ptr) => Some(repr_ptr.ptr),
600            None => None,
601        };
602        MetadataAsLink {
603            metadata: m.metadata.meta,
604            next,
605            prev,
606            ref_count: m.ref_count,
607            vtable_ptr: m.vtable_ptr,
608            in_list: m.in_list,
609        }
610    }
611}
612
613impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> FromSpecImpl<MetadataAsLink<M>> for Metadata<Link<M>> {
614    open spec fn obeys_from_spec() -> bool {
615        true
616    }
617
618    open spec fn from_spec(m: MetadataAsLink<M>) -> Metadata<Link<M>> {
619        Metadata {
620            metadata: Link {
621                next: match m.next {
622                    Some(pptr) => Some(ReprPtr::new_spec(pptr)),
623                    None => None,
624                },
625                prev: match m.prev {
626                    Some(pptr) => Some(ReprPtr::new_spec(pptr)),
627                    None => None,
628                },
629                meta: m.metadata,
630            },
631            ref_count: m.ref_count,
632            vtable_ptr: m.vtable_ptr,
633            in_list: m.in_list,
634        }
635    }
636}
637
638impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> From<MetadataAsLink<M>> for Metadata<Link<M>> {
639    fn from(m: MetadataAsLink<M>) -> Self {
640        let next = match m.next {
641            Some(pptr) => Some(ReprPtr::from_pptr(pptr)),
642            None => None,
643        };
644        let prev = match m.prev {
645            Some(pptr) => Some(ReprPtr::from_pptr(pptr)),
646            None => None,
647        };
648        Metadata {
649            metadata: Link { next, prev, meta: m.metadata },
650            ref_count: m.ref_count,
651            vtable_ptr: m.vtable_ptr,
652            in_list: m.in_list,
653        }
654    }
655}
656
657impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> MetadataAsLink<M> {
658    pub fn cast_to_metadata(ptr: ReprPtr<MetaSlot, Self>) -> (res: ReprPtr<MetaSlot, Metadata<Link<M>>>)
659        ensures
660            res.addr() == ptr.addr(),
661            res.ptr == ptr.ptr,
662    {
663        ReprPtr { addr: ptr.addr, ptr: ptr.ptr, _T: PhantomData }
664    }
665
666    pub fn cast_from_metadata(ptr: ReprPtr<MetaSlot, Metadata<Link<M>>>) -> (res: ReprPtr<MetaSlot, Self>)
667        ensures
668            res.addr() == ptr.addr(),
669            res.ptr == ptr.ptr,
670    {
671        ReprPtr { addr: ptr.addr, ptr: ptr.ptr, _T: PhantomData }
672    }
673
674    #[verifier::external_body]
675    pub proof fn cast_points_to_metadata(tracked perm: vstd_extra::cast_ptr::PointsTo<MetaSlot, MetadataAsLink<M>>) -> (tracked result: vstd_extra::cast_ptr::PointsTo<MetaSlot, Metadata<Link<M>>>)
676        ensures
677            result.addr() == perm.addr(),
678            result.is_init() == perm.is_init(),
679            result.points_to.pptr() == perm.points_to.pptr(),
680    {
681        unimplemented!()
682    }
683
684    #[verifier::external_body]
685    pub proof fn cast_points_to_as_link(tracked perm: vstd_extra::cast_ptr::PointsTo<MetaSlot, Metadata<Link<M>>>) -> (tracked result: vstd_extra::cast_ptr::PointsTo<MetaSlot, MetadataAsLink<M>>)
686        ensures
687            result.addr() == perm.addr(),
688            result.is_init() == perm.is_init(),
689            result.points_to.pptr() == perm.points_to.pptr(),
690    {
691        unimplemented!()
692    }
693}
694
695} // verus!
ostd/specs/mm/frame/linked_list/linked_list_owners.rs

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