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        &&& res.meta_perm.value().metadata == metadata
105        &&& regions.slots == old_regions.slots.remove(frame_to_index(paddr))
106        &&& regions.slot_owners[frame_to_index(paddr)].raw_count == old_regions.slot_owners[frame_to_index(paddr)].raw_count
107        &&& regions.slot_owners[frame_to_index(paddr)].usage == old_regions.slot_owners[frame_to_index(paddr)].usage
108        &&& regions.slot_owners[frame_to_index(paddr)].paths_in_pt == old_regions.slot_owners[frame_to_index(paddr)].paths_in_pt
109        &&& forall|i: usize| i != frame_to_index(paddr) ==> regions.slot_owners[i] == old_regions.slot_owners[i]
110        &&& regions.inv()
111    }
112
113    pub axiom fn from_unused_owner(
114        tracked regions: &mut MetaRegionOwners,
115        paddr: Paddr,
116        meta_perm: PointsTo<MetaSlot, Metadata<M>>,
117    ) -> (tracked res: Self)
118    ensures
119        Self::from_unused_owner_spec(*old(regions), paddr, meta_perm.value().metadata, res, *final(regions));
120    /* {
121        let tracked perm = regions.slots.tracked_remove(frame_to_index(paddr));
122        UniqueFrameOwner::<M> {
123            meta_own: regions.slot_owners[frame_to_index(paddr)],
124            meta_perm: perm,
125            slot_index: frame_to_index(paddr)
126        }
127    }*/
128}
129
130impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> TrackDrop for UniqueFrame<M> {
131    type State = MetaRegionOwners;
132
133    open spec fn constructor_requires(self, s: Self::State) -> bool {
134        &&& s.slot_owners.contains_key(frame_to_index(meta_to_frame(self.ptr.addr())))
135        &&& s.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].raw_count == 0
136        &&& s.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].inner_perms.ref_count.value() != REF_COUNT_UNUSED
137        &&& s.inv()
138    }
139
140    open spec fn constructor_ensures(self, s0: Self::State, s1: Self::State) -> bool {
141        &&& s1.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].raw_count == 1
142        &&& forall|i: usize| #![trigger s1.slot_owners[i]]
143            i != frame_to_index(meta_to_frame(self.ptr.addr())) ==> s1.slot_owners[i] == s0.slot_owners[i]
144        &&& s1.slots =~= s0.slots
145        &&& s1.inv()
146    }
147
148    proof fn constructor_spec(self, tracked s: &mut Self::State) {
149        let index = frame_to_index(meta_to_frame(self.ptr.addr()));
150        let tracked mut slot_own = s.slot_owners.tracked_remove(index);
151        slot_own.raw_count = 1;
152        s.slot_owners.tracked_insert(index, slot_own);
153    }
154
155    open spec fn drop_requires(self, s: Self::State) -> bool {
156        &&& s.slot_owners.contains_key(frame_to_index(meta_to_frame(self.ptr.addr())))
157        &&& s.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].raw_count > 0
158        &&& s.inv()
159    }
160
161    open spec fn drop_ensures(self, s0: Self::State, s1: Self::State) -> bool {
162        &&& s1.slot_owners[frame_to_index(meta_to_frame(self.ptr.addr()))].raw_count == 0
163        &&& forall|i: usize| #![trigger s1.slot_owners[i]]
164            i != frame_to_index(meta_to_frame(self.ptr.addr())) ==> s1.slot_owners[i] == s0.slot_owners[i]
165        &&& s1.slots =~= s0.slots
166        &&& s1.inv()
167    }
168
169    proof fn drop_tracked(self, tracked s: &mut Self::State) {
170        let index = frame_to_index(meta_to_frame(self.ptr.addr()));
171        let tracked mut slot_own = s.slot_owners.tracked_remove(index);
172        slot_own.raw_count = 0;
173        s.slot_owners.tracked_insert(index, slot_own);
174    }
175}
176
177}
ostd/specs/mm/frame/unique.rs

ostd/specs/mm/frame/
unique.rs
