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

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