ostd/specs/mm/frame/
meta_specs.rs

1use vstd::{atomic::*, prelude::*, simple_pptr::PointsTo};
2use vstd_extra::{cast_ptr::*, ownership::*, sum::Sum};
3
4use crate::specs::{
5    arch::*,
6    mm::frame::{
7        frame_specs::*,
8        mapping::{frame_to_index, index_to_meta},
9        meta_region_owners::MetaRegionOwners,
10    },
11};
12
13use super::meta_owners::{
14    FracMetadataPerm, MetaSlotOwner, MetaSlotStatus, MetaSlotStorage, MetadataPerm, PageUsage,
15};
16use crate::mm::{
17    Paddr, PagingLevel, Vaddr,
18    frame::{
19        meta::{
20            META_SLOT_SIZE, REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED,
21            mapping::{frame_to_meta, meta_to_frame},
22        },
23        *,
24    },
25    kspace::FRAME_METADATA_RANGE,
26};
27
28verus! {
29
30global layout MetaSlot is size == 64, align == 8;
31
32impl MetaSlot {
33    /// The relation between the [`MetaSlot`] permission and a metadata permission fraction.
34    #[verifier::inline]
35    pub open spec fn perms_related(
36        slot_perm: PointsTo<MetaSlot>,
37        metadata_perm: MetadataPerm,
38    ) -> bool {
39        &&& metadata_perm.storage_perm.is_init()
40        &&& metadata_perm.vtable_ptr_perm.is_init()
41        &&& slot_perm.value().storage.id() == metadata_perm.storage_perm.id()
42        &&& slot_perm.value().vtable_ptr == metadata_perm.vtable_ptr_perm.pptr()
43    }
44
45    pub proof fn lemma_layout()
46        ensures
47            core::mem::size_of::<MetaSlot>() == META_SLOT_SIZE,
48            vstd::layout::size_of::<MetaSlot>() == META_SLOT_SIZE,
49    {
50        broadcast use VERUS_layout_of_MetaSlot;
51
52    }
53
54    pub open spec fn get_from_unused_owner_spec(as_unique: bool, owner: MetaSlotOwner) -> bool {
55        &&& owner.ref_count() == (if as_unique {
56            REF_COUNT_UNIQUE as u64
57        } else {
58            1u64
59        })
60        &&& owner.in_list_perm.value() == 0
61        &&& owner.metadata_perm.frac() == (if as_unique {
62            0int
63        } else {
64            REF_COUNT_MAX - 1
65        })
66        &&& as_unique ==> owner.metadata_perm.is_resource_vacant()
67        &&& !as_unique ==> {
68            &&& owner.storage_perm().is_init()
69            &&& owner.vtable_ptr_perm().is_init()
70        }
71    }
72
73    /// The metadata region transition of claiming an unused slot.
74    pub open spec fn get_from_unused_region_spec(
75        paddr: Paddr,
76        as_unique: bool,
77        pre: MetaRegionOwners,
78        post: MetaRegionOwners,
79    ) -> bool {
80        let idx = frame_to_index(paddr);
81        let pre_owner = pre.slot_owners[idx];
82        let post_owner = post.slot_owners[idx];
83        {
84            &&& pre_owner.ref_count() == REF_COUNT_UNUSED
85            &&& MetaSlot::get_from_unused_owner_spec(as_unique, post_owner)
86            &&& post_owner.usage is Frame
87            &&& post_owner.slot_vaddr == pre_owner.slot_vaddr
88            &&& post_owner.paths_in_pt == pre_owner.paths_in_pt
89            &&& post =~= pre.insert_slot_owner(paddr, post_owner)
90        }
91    }
92
93    /// The complete successful result of claiming an unused slot, including
94    /// the fraction returned to the new frame handle.
95    pub open spec fn get_from_unused_spec<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
96        paddr: Paddr,
97        metadata: M,
98        as_unique: bool,
99        pre: MetaRegionOwners,
100        post: MetaRegionOwners,
101        repr_perm: M::ReprPerm,
102        permission: Sum<FracMetadataPerm, MetadataPerm>,
103    ) -> bool {
104        let idx = frame_to_index(paddr);
105        let metadata_perms = match permission {
106            Sum::Left(permission) => permission.resource(),
107            Sum::Right(permission) => permission,
108        };
109        &&& Self::get_from_unused_region_spec(paddr, as_unique, pre, post)
110        &&& as_unique ==> permission is Right
111        &&& !as_unique ==> {
112            &&& permission is Left
113            &&& permission->Left_0.frac() == 1
114            &&& permission->Left_0.id() == post.slot_owners[idx].metadata_perm.id()
115        }
116        &&& Self::perms_related(*post.slots[idx], metadata_perms)
117        &&& <M as Repr<MetaSlotStorage>>::wf(metadata_perms.storage_perm.value(), repr_perm)
118        &&& M::from_repr_spec(metadata_perms.storage_perm.value(), repr_perm) == metadata
119    }
120
121    /// Variant of [`get_from_unused_region_spec`] for allocating a page-table *node*
122    /// (always non-unique). Identical except the claimed slot becomes
123    /// `PageUsage::PageTable` rather than `PageUsage::Frame`.
124    pub open spec fn get_node_from_unused_spec(
125        paddr: Paddr,
126        pre: MetaRegionOwners,
127        post: MetaRegionOwners,
128    ) -> bool {
129        let idx = frame_to_index(paddr);
130        {
131            &&& post.slot_owners.dom() =~= pre.slot_owners.dom()
132            &&& MetaSlot::get_from_unused_owner_spec(false, post.slot_owners[idx])
133            &&& post.slot_owners[idx].usage is PageTable
134            &&& post.slot_owners[idx].slot_vaddr == pre.slot_owners[idx].slot_vaddr
135            &&& post.slot_owners[idx].paths_in_pt == pre.slot_owners[idx].paths_in_pt
136            &&& forall|i: int| i != idx ==> (#[trigger] post.slot_owners[i] == pre.slot_owners[i])
137            &&& pre.slot_owners[idx].ref_count() == REF_COUNT_UNUSED
138        }
139    }
140
141    /// Permission-location clause for the static `MetaSlot` permissions.
142    /// Only the slot at `paddr` is changed.
143    pub open spec fn slot_perm_reparked_spec(
144        paddr: Paddr,
145        pre: MetaRegionOwners,
146        post: MetaRegionOwners,
147    ) -> bool {
148        let idx = frame_to_index(paddr);
149        &&& post.slots.dom() =~= pre.slots.dom()
150        &&& forall|k: int|
151            #![trigger post.slots[k]]
152            k != idx && pre.contains(k) ==> post.slots[k] == pre.slots[k]
153    }
154
155    pub open spec fn inc_ref_count_panic_cond(rc_perm: PermissionU64) -> bool {
156        rc_perm.value() >= REF_COUNT_MAX
157    }
158
159    pub open spec fn frame_paddr_safety_cond(perm: PointsTo<MetaSlot>) -> bool {
160        &&& FRAME_METADATA_RANGE.start <= perm.addr() < FRAME_METADATA_RANGE.end
161        &&& perm.addr() % META_SLOT_SIZE == 0
162    }
163
164    pub open spec fn get_from_in_use_success_spec(
165        paddr: Paddr,
166        pre: MetaRegionOwners,
167        post: MetaRegionOwners,
168        metadata_perm: FracMetadataPerm,
169    ) -> bool {
170        let idx = frame_to_index(paddr);
171        {
172            &&& pre.inc_frame_reference_region_spec(paddr, post)
173            &&& metadata_perm.frac() == 1
174            &&& metadata_perm.id() == post.slot_owners[idx].metadata_perm.id()
175            &&& Self::perms_related(*post.slots[idx], metadata_perm.resource())
176        }
177    }
178
179    pub open spec fn drop_last_in_place_safety_cond(owner: MetaSlotOwner) -> bool {
180        &&& (owner.ref_count() == 0 || owner.ref_count() == REF_COUNT_UNIQUE)
181        &&& owner.metadata_perm.is_full()
182        &&& owner.storage_perm().is_init()
183        &&& owner.vtable_ptr_perm().is_init()
184        &&& owner.in_list_perm.value() == 0
185        &&& owner.paths_in_pt.is_empty()
186    }
187}
188
189} // verus!
ostd/specs/mm/frame/meta_specs.rs

ostd/specs/mm/frame/
meta_specs.rs
