ostd/specs/mm/frame/
unique.rs

1use vstd::prelude::*;
2use vstd_extra::{cast_ptr::*, ownership::*, prelude::*};
3
4use crate::specs::{
5    arch::{MAX_NR_PAGES, valid_frame_paddr},
6    mm::{
7        Paddr,
8        frame::{
9            mapping::{frame_to_index, index_to_meta, max_meta_slots, meta_to_index},
10            meta_region_owners::MetaRegionOwners,
11        },
12    },
13};
14
15use super::meta_owners::*;
16use crate::mm::{
17    frame::{
18        meta::{
19            META_SLOT_SIZE, REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED,
20            mapping::{frame_to_meta, meta_to_frame},
21        },
22        *,
23    },
24    kspace::FRAME_METADATA_RANGE,
25};
26
27verus! {
28
29impl<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage> + OwnerOf> UniqueFrame<M> {
30    pub open spec fn start_paddr_spec(self) -> Paddr {
31        meta_to_frame(self.ptr.addr())
32    }
33
34    pub open spec fn index(self) -> int {
35        frame_to_index(self.start_paddr_spec())
36    }
37
38    /// The complete metadata permission carried by this unique handle.
39    #[verifier::inline]
40    pub open spec fn metadata_perm(self) -> MetadataPerm {
41        self.tracked_metadata_perm@->0
42    }
43
44    /// The metadata-slot permission carried by this unique handle.
45    pub open spec fn slot_perm(self) -> vstd::simple_pptr::PointsTo<MetaSlot> {
46        *self.tracked_slot_perm@
47    }
48
49    #[verifier::inline]
50    pub open spec fn ptr_inv(self) -> bool {
51        &&& valid_frame_paddr(self.start_paddr_spec())
52        &&& self.ptr.addr() % META_SLOT_SIZE == 0
53        &&& FRAME_METADATA_RANGE.start <= self.ptr.addr() < FRAME_METADATA_RANGE.start
54            + MAX_NR_PAGES * META_SLOT_SIZE
55        &&& self.slot_perm().pptr() == self.ptr
56        &&& self.slot_perm().is_init()
57    }
58}
59
60impl<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage> + OwnerOf> Inv for UniqueFrame<M> {
61    open spec fn inv(self) -> bool {
62        &&& self.ptr_inv()
63        &&& self.tracked_metadata_perm@ is Some
64        &&& MetaSlot::perms_related(self.slot_perm(), self.metadata_perm())
65    }
66}
67
68//FIXME: why do we need a index here?
69pub tracked struct UniqueFrameOwner<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage> + OwnerOf> {
70    pub meta_own: M::Owner,
71    pub repr_perm: Option<M::ReprPerm>,
72    pub ghost slot_index: int,
73}
74
75impl<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage> + OwnerOf> Inv for UniqueFrameOwner<M> {
76    open spec fn inv(self) -> bool {
77        &&& 0 <= self.slot_index < MAX_NR_PAGES
78        &&& self.slot_index < max_meta_slots()
79        &&& self.repr_perm is Some
80    }
81}
82
83impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> OwnerOf for UniqueFrame<M> {
84    type Owner = UniqueFrameOwner<M>;
85
86    open spec fn wf(self, owner: Self::Owner) -> bool {
87        &&& self.ptr.addr() == index_to_meta(owner.slot_index)
88    }
89}
90
91impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> UniqueFrame<M> {
92    pub open spec fn meta_wf(self, owner: UniqueFrameOwner<M>) -> bool {
93        typed_meta_wf::<M>(self.slot_perm(), self.metadata_perm(), owner.repr_perm->0)
94    }
95
96    pub open spec fn meta_value(self, owner: UniqueFrameOwner<M>) -> M {
97        typed_meta_value::<M>(self.metadata_perm(), owner.repr_perm->0)
98    }
99
100    /// Cross-object validity of a live UNIQUE handle against the region map —
101    /// the [`UniqueFrame`] analog of [`Frame::wf_with_region`] (which covers
102    /// the SHARED state).
103    pub open spec fn wf_with_region(self, owner: UniqueFrameOwner<M>, s: MetaRegionOwners) -> bool {
104        let idx = owner.slot_index;
105        let so = s.slot_owners[idx];
106        &&& self.wf(owner)
107        &&& s.contains(idx)
108        &&& self.tracked_slot_perm@ == s.slots[idx]
109        &&& self.meta_wf(owner)
110        &&& self.meta_value(owner).wf(owner.meta_own)
111        &&& so.metadata_perm.is_resource_vacant()
112        &&& so.ref_count() == REF_COUNT_UNIQUE
113        &&& so.usage is Frame
114        &&& so.paths_in_pt.is_empty()
115    }
116}
117
118impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> UniqueFrameOwner<M> {
119    pub open spec fn meta_wf(self, regions: MetaRegionOwners) -> bool {
120        typed_meta_wf::<M>(
121            *regions.slots[self.slot_index],
122            regions.slot_owners[self.slot_index].metadata_perm.resource(),
123            self.repr_perm->0,
124        )
125    }
126
127    pub open spec fn meta_value(self, regions: MetaRegionOwners) -> M {
128        typed_meta_value::<M>(
129            regions.slot_owners[self.slot_index].metadata_perm.resource(),
130            self.repr_perm->0,
131        )
132    }
133
134    pub open spec fn global_inv(self, regions: MetaRegionOwners) -> bool {
135        &&& regions.contains(self.slot_index)
136        &&& self.meta_wf(regions)
137        &&& regions.slots[self.slot_index].addr() == index_to_meta(self.slot_index)
138        &&& self.meta_value(regions).wf(self.meta_own)
139        &&& regions.slot_owners[self.slot_index].metadata_perm.is_resource_vacant()
140        &&& regions.slot_owners[self.slot_index].metadata_perm.resource().storage_perm.id()
141            == regions.slots[self.slot_index].value().storage.id()
142        &&& regions.slot_owners[self.slot_index].metadata_perm.resource().vtable_ptr_perm.pptr()
143            == regions.slots[self.slot_index].value().vtable_ptr
144        &&& regions.slot_owners[self.slot_index].metadata_perm.resource().vtable_ptr_perm.is_init()
145        &&& regions.slot_owners[self.slot_index].slot_vaddr == index_to_meta(self.slot_index)
146        &&& regions.ref_count(self.slot_index) == REF_COUNT_UNIQUE
147        &&& regions.slot_owners[self.slot_index].usage is Frame
148    }
149
150    pub open spec fn from_unused_owner(
151        meta_own: M::Owner,
152        repr_perm: M::ReprPerm,
153        slot_index: int,
154    ) -> Self {
155        Self { meta_own, repr_perm: Some(repr_perm), slot_index }
156    }
157
158    pub proof fn tracked_from_unused_owner(
159        tracked meta_own: M::Owner,
160        tracked repr_perm: M::ReprPerm,
161        slot_index: int,
162    ) -> (tracked res: Self)
163        returns
164            Self::from_unused_owner(meta_own, repr_perm, slot_index),
165    {
166        Self { meta_own, repr_perm: Some(repr_perm), slot_index }
167    }
168
169    pub proof fn tracked_borrow_repr_perm(tracked &self) -> tracked &M::ReprPerm
170        requires
171            self.repr_perm is Some,
172        returns
173            self.repr_perm->0,
174    {
175        self.repr_perm.tracked_borrow()
176    }
177
178    pub proof fn tracked_borrow_mut_repr_perm(tracked &mut self) -> (tracked res: &mut M::ReprPerm)
179        requires
180            old(self).inv(),
181        ensures
182            *res == old(self).repr_perm->0,
183            final(self).meta_own == old(self).meta_own,
184            final(self).slot_index == old(self).slot_index,
185            final(self).repr_perm is Some,
186            final(self).repr_perm->0 == *final(res),
187            final(self).inv(),
188    {
189        self.repr_perm.tracked_borrow_mut()
190    }
191}
192
193} // verus!
ostd/specs/mm/frame/unique.rs

ostd/specs/mm/frame/
unique.rs
