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,
6    mm::{
7        Paddr, Vaddr,
8        frame::{frame_specs::valid_slot_vaddr, mapping::*, meta_region_owners::MetaRegionOwners},
9    },
10};
11
12use super::meta_owners::*;
13use crate::mm::frame::{
14    meta::{
15        REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED,
16        mapping::{frame_to_meta, meta_to_frame},
17    },
18    *,
19};
20
21verus! {
22
23impl<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage> + OwnerOf> UniqueFrame<M> {
24    #[verifier::inline]
25    pub open spec fn slot_vaddr(self) -> Vaddr {
26        self.ptr.addr()
27    }
28
29    #[verifier::inline]
30    pub open spec fn start_paddr_spec(self) -> Paddr {
31        meta_to_frame(self.slot_vaddr())
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_slot_vaddr(self.slot_vaddr())
52        &&& self.slot_perm().pptr() == self.ptr
53        &&& self.slot_perm().is_init()
54    }
55}
56
57impl<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage> + OwnerOf> Inv for UniqueFrame<M> {
58    open spec fn inv(self) -> bool {
59        &&& self.ptr_inv()
60        &&& self.tracked_metadata_perm@ is Some
61        &&& MetaSlot::perms_related(self.slot_perm(), self.metadata_perm())
62    }
63}
64
65//FIXME: why do we need a index here?
66pub tracked struct UniqueFrameOwner<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage> + OwnerOf> {
67    pub meta_own: M::Owner,
68    pub repr_perm: Option<M::ReprPerm>,
69    pub ghost slot_index: int,
70}
71
72impl<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage> + OwnerOf> Inv for UniqueFrameOwner<M> {
73    open spec fn inv(self) -> bool {
74        &&& 0 <= self.slot_index < MAX_NR_PAGES
75        &&& self.slot_index < max_meta_slots()
76        &&& self.repr_perm is Some
77    }
78}
79
80impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> OwnerOf for UniqueFrame<M> {
81    type Owner = UniqueFrameOwner<M>;
82
83    open spec fn wf(self, owner: Self::Owner) -> bool {
84        &&& self.slot_vaddr() == index_to_meta(owner.slot_index)
85    }
86}
87
88impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> UniqueFrame<M> {
89    pub open spec fn meta_wf(self, owner: UniqueFrameOwner<M>) -> bool {
90        typed_meta_wf::<M>(self.slot_perm(), self.metadata_perm(), owner.repr_perm->0)
91    }
92
93    pub open spec fn meta_value(self, owner: UniqueFrameOwner<M>) -> M {
94        typed_meta_value::<M>(self.metadata_perm(), owner.repr_perm->0)
95    }
96
97    /// Cross-object validity of a live UNIQUE handle against the region map —
98    /// the [`UniqueFrame`] analog of [`Frame::wf_with_region`] (which covers
99    /// the SHARED state).
100    pub open spec fn wf_with_region(self, owner: UniqueFrameOwner<M>, s: MetaRegionOwners) -> bool {
101        let idx = owner.slot_index;
102        let so = s.slot_owners[idx];
103        &&& self.wf(owner)
104        &&& s.contains(idx)
105        &&& self.tracked_slot_perm@ == s.slots[idx]
106        &&& self.meta_wf(owner)
107        &&& self.meta_value(owner).wf(owner.meta_own)
108        &&& so.metadata_perm.is_resource_vacant()
109        &&& so.ref_count() == REF_COUNT_UNIQUE
110        &&& so.usage == self.metadata_perm().usage()
111        &&& so.paths_in_pt.is_empty()
112    }
113}
114
115impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> UniqueFrameOwner<M> {
116    pub open spec fn meta_wf(self, regions: MetaRegionOwners) -> bool {
117        typed_meta_wf::<M>(
118            *regions.slots[self.slot_index],
119            regions.slot_owners[self.slot_index].metadata_perm.resource(),
120            self.repr_perm->0,
121        )
122    }
123
124    pub open spec fn meta_value(self, regions: MetaRegionOwners) -> M {
125        typed_meta_value::<M>(
126            regions.slot_owners[self.slot_index].metadata_perm.resource(),
127            self.repr_perm->0,
128        )
129    }
130
131    pub open spec fn global_inv(self, regions: MetaRegionOwners) -> bool {
132        &&& regions.contains(self.slot_index)
133        &&& self.meta_wf(regions)
134        &&& regions.slots[self.slot_index].addr() == index_to_meta(self.slot_index)
135        &&& self.meta_value(regions).wf(self.meta_own)
136        &&& regions.slot_owners[self.slot_index].metadata_perm.is_resource_vacant()
137        &&& regions.slot_owners[self.slot_index].metadata_perm.resource().storage_perm.id()
138            == regions.slots[self.slot_index].value().storage.id()
139        &&& regions.slot_owners[self.slot_index].metadata_perm.resource().vtable_ptr_perm.pptr()
140            == regions.slots[self.slot_index].value().vtable_ptr
141        &&& regions.slot_owners[self.slot_index].metadata_perm.resource().vtable_ptr_perm.is_init()
142        &&& regions.slot_owners[self.slot_index].slot_vaddr == index_to_meta(self.slot_index)
143        &&& regions.ref_count(self.slot_index) == REF_COUNT_UNIQUE
144        &&& regions.slot_owners[self.slot_index].usage
145            == regions.slot_owners[self.slot_index].metadata_perm().usage()
146    }
147
148    pub proof fn tracked_borrow_repr_perm(tracked &self) -> tracked &M::ReprPerm
149        requires
150            self.repr_perm is Some,
151        returns
152            self.repr_perm->0,
153    {
154        self.repr_perm.tracked_borrow()
155    }
156
157    pub proof fn tracked_borrow_mut_repr_perm(tracked &mut self) -> (tracked res: &mut M::ReprPerm)
158        requires
159            old(self).inv(),
160        ensures
161            *res == old(self).repr_perm->0,
162            final(self).meta_own == old(self).meta_own,
163            final(self).slot_index == old(self).slot_index,
164            final(self).repr_perm is Some,
165            final(self).repr_perm->0 == *final(res),
166            final(self).inv(),
167    {
168        self.repr_perm.tracked_borrow_mut()
169    }
170}
171
172} // verus!
ostd/specs/mm/frame/unique.rs

ostd/specs/mm/frame/
unique.rs
