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 claim_unused_slot_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.slot_vaddr == pre_owner.slot_vaddr
87            &&& post =~= pre.insert_slot_owner(paddr, post_owner)
88        }
89    }
90
91    /// The metadata region transition of claiming an unused slot for a frame.
92    pub open spec fn get_from_unused_region_spec(
93        paddr: Paddr,
94        as_unique: bool,
95        usage: PageUsage,
96        pre: MetaRegionOwners,
97        post: MetaRegionOwners,
98    ) -> bool {
99        let idx = frame_to_index(paddr);
100        &&& Self::claim_unused_slot_region_spec(paddr, as_unique, pre, post)
101        &&& post.slot_owners[idx].usage == usage
102        &&& post.slot_owners[idx].paths_in_pt == pre.slot_owners[idx].paths_in_pt
103    }
104
105    /// The complete successful result of claiming an unused slot, including
106    /// the fraction returned to the new frame handle.
107    pub open spec fn get_from_unused_spec<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
108        paddr: Paddr,
109        metadata: M,
110        as_unique: bool,
111        pre: MetaRegionOwners,
112        post: MetaRegionOwners,
113        repr_perm: M::ReprPerm,
114        permission: Sum<FracMetadataPerm, MetadataPerm>,
115    ) -> bool {
116        let idx = frame_to_index(paddr);
117        let metadata_perms = match permission {
118            Sum::Left(permission) => permission.resource(),
119            Sum::Right(permission) => permission,
120        };
121        &&& Self::get_from_unused_region_spec(paddr, as_unique, metadata_perms.usage(), pre, post)
122        &&& as_unique ==> permission is Right
123        &&& !as_unique ==> {
124            &&& permission is Left
125            &&& permission->Left_0.frac() == 1
126            &&& permission->Left_0.id() == post.slot_owners[idx].metadata_perm.id()
127        }
128        &&& Self::perms_related(*post.slots[idx], metadata_perms)
129        &&& <M as Repr<MetaSlotStorage>>::wf(metadata_perms.storage_perm.value(), repr_perm)
130        &&& M::from_repr_spec(metadata_perms.storage_perm.value(), repr_perm) == metadata
131    }
132
133    pub open spec fn inc_ref_count_panic_cond(rc_perm: PermissionU64) -> bool {
134        rc_perm.value() >= REF_COUNT_MAX
135    }
136
137    pub open spec fn frame_paddr_safety_cond(perm: PointsTo<MetaSlot>) -> bool {
138        &&& FRAME_METADATA_RANGE.start <= perm.addr() < FRAME_METADATA_RANGE.end
139        &&& perm.addr() % META_SLOT_SIZE == 0
140    }
141
142    pub open spec fn get_from_in_use_success_spec(
143        paddr: Paddr,
144        pre: MetaRegionOwners,
145        post: MetaRegionOwners,
146        metadata_perm: FracMetadataPerm,
147    ) -> bool {
148        let idx = frame_to_index(paddr);
149        {
150            &&& pre.inc_frame_reference_region_spec(paddr, post)
151            &&& metadata_perm.frac() == 1
152            &&& metadata_perm.id() == post.slot_owners[idx].metadata_perm.id()
153            &&& Self::perms_related(*post.slots[idx], metadata_perm.resource())
154        }
155    }
156
157    pub open spec fn drop_last_in_place_safety_cond(owner: MetaSlotOwner) -> bool {
158        &&& (owner.ref_count() == 0 || owner.ref_count() == REF_COUNT_UNIQUE)
159        &&& owner.metadata_perm.is_full()
160        &&& owner.storage_perm().is_init()
161        &&& owner.vtable_ptr_perm().is_init()
162        &&& owner.in_list_perm.value() == 0
163        &&& owner.paths_in_pt.is_empty()
164    }
165}
166
167} // verus!
ostd/specs/mm/frame/meta_specs.rs

ostd/specs/mm/frame/
meta_specs.rs
