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

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