ostd/specs/mm/frame/
unique.rs

1use vstd::prelude::*;
2use vstd_extra::cast_ptr::*;
3use vstd_extra::drop_tracking::*;
4use vstd_extra::ownership::*;
5
6use super::meta_owners::*;
7use crate::mm::frame::*;
8use crate::specs::arch::kspace::FRAME_METADATA_RANGE;
9use crate::specs::arch::mm::{MAX_NR_PAGES, MAX_PADDR, PAGE_SIZE};
10use crate::specs::mm::frame::mapping::{
11    frame_to_index, frame_to_meta, max_meta_slots, meta_addr, meta_to_frame,
12};
13use crate::specs::mm::frame::meta_region_owners::{MetaRegionModel, MetaRegionOwners};
14use crate::specs::mm::Paddr;
15
16verus! {
17
18pub tracked struct UniqueFrameOwner<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> {
19    pub meta_own: M::Owner,
20    pub meta_perm: PointsTo<MetaSlot, Metadata<M>>,
21    pub ghost slot_index: usize,
22}
23
24pub ghost struct UniqueFrameModel<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> {
25    pub meta: <M::Owner as View>::V,
26}
27
28impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Inv for UniqueFrameOwner<M> {
29    open spec fn inv(self) -> bool {
30        &&& self.meta_perm.is_init()
31        &&& self.meta_perm.wf(&self.meta_perm.inner_perms)
32        &&& self.slot_index == frame_to_index(meta_to_frame(self.meta_perm.addr()))
33        &&& self.slot_index < max_meta_slots()
34        &&& (self.slot_index - FRAME_METADATA_RANGE.start) as usize % META_SLOT_SIZE == 0
35        &&& self.meta_perm.addr() < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
36        &&& self.meta_perm.addr() == meta_addr(self.slot_index)
37        &&& self.meta_perm.addr() == self.meta_perm.points_to.addr()
38        &&& self.meta_perm.value().metadata.wf(self.meta_own)
39    }
40}
41
42impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Inv for UniqueFrameModel<M> {
43    open spec fn inv(self) -> bool {
44        true
45    }
46}
47
48impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> View for UniqueFrameOwner<M> {
49    type V = UniqueFrameModel<M>;
50
51    open spec fn view(&self) -> Self::V {
52        UniqueFrameModel { meta: self.meta_own@ }
53    }
54}
55
56impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> InvView for UniqueFrameOwner<M> {
57    proof fn view_preserves_inv(self) {
58    }
59}
60
61impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> OwnerOf for UniqueFrame<M> {
62    type Owner = UniqueFrameOwner<M>;
63
64    open spec fn wf(self, owner: Self::Owner) -> bool {
65        &&& self.ptr.addr() == owner.meta_perm.addr()
66    }
67}
68
69impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> ModelOf for UniqueFrame<M> {
70
71}
72
73impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> UniqueFrameOwner<M> {
74
75    pub open spec fn perm_inv(self, perm: vstd::simple_pptr::PointsTo<MetaSlot>) -> bool {
76        &&& perm.is_init()
77        &&& perm.addr() == self.meta_perm.addr()
78    }
79
80    pub open spec fn global_inv(self, regions: MetaRegionOwners) -> bool {
81        &&& !regions.slots.contains_key(self.slot_index)
82        &&& regions.slot_owners.contains_key(self.slot_index)
83        &&& regions.slot_owners[self.slot_index].inner_perms == self.meta_perm.inner_perms
84        &&& self.meta_perm.addr() == regions.slot_owners[self.slot_index].self_addr
85    }
86
87    pub proof fn from_raw_owner(
88        owner: M::Owner,
89        index: Ghost<usize>,
90        perm: PointsTo<MetaSlot, Metadata<M>>,
91    ) -> Self {
92        UniqueFrameOwner::<M> { meta_own: owner, meta_perm: perm, slot_index: index@ }
93    }
94
95    pub open spec fn from_unused_owner_spec(
96        old_regions: MetaRegionOwners,
97        paddr: Paddr,
98        metadata: M,
99        res: Self,
100        regions: MetaRegionOwners,
101    ) -> bool {
102        &&& <M as OwnerOf>::wf(metadata, res.meta_own)
103        &&& res.meta_perm.addr() == frame_to_meta(paddr)
104        &&& regions.slots == old_regions.slots.remove(frame_to_index(paddr))
105        &&& regions.slot_owners[frame_to_index(paddr)].raw_count == old_regions.slot_owners[frame_to_index(paddr)].raw_count
106        &&& regions.slot_owners[frame_to_index(paddr)].usage == old_regions.slot_owners[frame_to_index(paddr)].usage
107        &&& regions.slot_owners[frame_to_index(paddr)].path_if_in_pt == old_regions.slot_owners[frame_to_index(paddr)].path_if_in_pt
108        &&& forall|i: usize| i != frame_to_index(paddr) ==> regions.slot_owners[i] == old_regions.slot_owners[i]
109        &&& regions.inv()
110    }
111
112    pub axiom fn from_unused_owner(
113        tracked regions: &mut MetaRegionOwners,
114        paddr: Paddr,
115        meta_perm: PointsTo<MetaSlot, Metadata<M>>,
116    ) -> (tracked res: Self)
117    ensures
118        Self::from_unused_owner_spec(*old(regions), paddr, meta_perm.value().metadata, res, *regions);
119    /* {
120        let tracked perm = regions.slots.tracked_remove(frame_to_index(paddr));
121        UniqueFrameOwner::<M> {
122            meta_own: regions.slot_owners[frame_to_index(paddr)],
123            meta_perm: perm,
124            slot_index: frame_to_index(paddr)
125        }
126    }*/
127}
128
129impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> TrackDrop for UniqueFrame<M> {
130    type State = MetaRegionOwners;
131
132    open spec fn constructor_requires(self, s: Self::State) -> bool {
133        &&& s.slot_owners.contains_key(frame_to_index(meta_to_frame(self.ptr.addr())))
134        &&& s.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].raw_count == 0
135        &&& s.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].inner_perms.ref_count.value() != REF_COUNT_UNUSED
136        &&& s.inv()
137    }
138
139    open spec fn constructor_ensures(self, s0: Self::State, s1: Self::State) -> bool {
140        &&& s1.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].raw_count == 1
141        &&& forall|i: usize| #![trigger s1.slot_owners[i]]
142            i != frame_to_index(meta_to_frame(self.ptr.addr())) ==> s1.slot_owners[i] == s0.slot_owners[i]
143        &&& s1.slots =~= s0.slots
144        &&& s1.inv()
145    }
146
147    proof fn constructor_spec(self, tracked s: &mut Self::State) {
148        let index = frame_to_index(meta_to_frame(self.ptr.addr()));
149        let tracked mut slot_own = s.slot_owners.tracked_remove(index);
150        slot_own.raw_count = 1;
151        s.slot_owners.tracked_insert(index, slot_own);
152    }
153
154    open spec fn drop_requires(self, s: Self::State) -> bool {
155        &&& s.slot_owners.contains_key(frame_to_index(meta_to_frame(self.ptr.addr())))
156        &&& s.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].raw_count > 0
157        &&& s.inv()
158    }
159
160    open spec fn drop_ensures(self, s0: Self::State, s1: Self::State) -> bool {
161        &&& s1.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].raw_count == 0
162        &&& forall|i: usize| #![trigger s1.slot_owners[i]]
163            i != frame_to_index(meta_to_frame(self.ptr.addr())) ==> s1.slot_owners[i] == s0.slot_owners[i]
164        &&& s1.slots =~= s0.slots
165        &&& s1.inv()
166    }
167
168    proof fn drop_spec(self, tracked s: &mut Self::State) {
169        let index = frame_to_index(meta_to_frame(self.ptr.addr()));
170        let tracked mut slot_own = s.slot_owners.tracked_remove(index);
171        slot_own.raw_count = 0;
172        s.slot_owners.tracked_insert(index, slot_own);
173    }
174}
175
176}
ostd/specs/mm/frame/unique.rs

ostd/specs/mm/frame/
unique.rs
