ostd/specs/mm/frame/
meta_specs.rs

1use vstd::atomic::*;
2use vstd::atomic::*;
3use vstd::cell;
4use vstd::prelude::*;
5use vstd::simple_pptr::{self, PPtr};
6
7use vstd_extra::cast_ptr::*;
8use vstd_extra::ownership::*;
9
10use super::meta_owners::{
11    MetaSlotModel, MetaSlotOwner, MetaSlotStatus, MetaSlotStorage, Metadata, PageUsage,
12};
13use crate::mm::frame::meta::{
14    get_slot_spec,
15    mapping::{frame_to_index, frame_to_meta},
16    REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED,
17};
18use crate::mm::frame::*;
19use crate::mm::{Paddr, PagingLevel, Vaddr};
20use crate::specs::arch::kspace::FRAME_METADATA_RANGE;
21use crate::specs::arch::mm::{MAX_NR_PAGES, MAX_PADDR, PAGE_SIZE};
22use crate::specs::mm::frame::meta_owners::MetadataInnerPerms;
23use crate::specs::mm::frame::meta_region_owners::{MetaRegionModel, MetaRegionOwners};
24
25use core::marker::PhantomData;
26
27verus! {
28
29impl MetaSlot {
30
31    pub open spec fn get_from_unused_inner_perms_spec(as_unique: bool, perms: MetadataInnerPerms) -> bool
32    {
33        &&& perms.ref_count.value() == (if as_unique { REF_COUNT_UNIQUE as u64 } else { 1u64 })
34        &&& perms.in_list.value() == 0
35        &&& perms.storage.is_init()
36        &&& perms.vtable_ptr.is_init()
37    }
38
39    pub open spec fn get_from_unused_spec(
40        paddr: Paddr,
41        as_unique: bool,
42        pre: MetaRegionOwners,
43        post: MetaRegionOwners,
44    ) -> bool
45        recommends
46            paddr % PAGE_SIZE == 0,
47            paddr < MAX_PADDR,
48            pre.inv(),
49    {
50        let idx = frame_to_index(paddr);
51        {
52            &&& post.slots =~= pre.slots.remove(idx)
53            &&& MetaSlot::get_from_unused_inner_perms_spec(as_unique, post.slot_owners[idx].inner_perms)
54            &&& post.slot_owners[idx].usage == PageUsage::Frame
55            &&& post.slot_owners[idx].raw_count == pre.slot_owners[idx].raw_count
56            &&& post.slot_owners[idx].self_addr == pre.slot_owners[idx].self_addr
57            &&& post.slot_owners[idx].path_if_in_pt == pre.slot_owners[idx].path_if_in_pt
58            &&& forall|i: usize| i != idx ==> (#[trigger] post.slot_owners[i] == pre.slot_owners[i])
59        }
60    }
61
62    pub open spec fn get_from_unused_perm_spec<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
63        paddr: Paddr,
64        metadata: M,
65        as_unique: bool,
66        ptr: PPtr<MetaSlot>,
67        perm: PointsTo<MetaSlot, Metadata<M>>,
68    ) -> bool {
69        &&& ptr.addr() == frame_to_meta(paddr)
70        &&& perm.addr() == frame_to_meta(paddr)
71        &&& MetaSlot::get_from_unused_inner_perms_spec(as_unique, perm.inner_perms)
72    }
73
74    pub open spec fn inc_ref_count_panic_cond(rc_perm: PermissionU64) -> bool {
75        rc_perm.value() >= REF_COUNT_MAX
76    }
77
78    pub open spec fn frame_paddr_safety_cond(perm: vstd::simple_pptr::PointsTo<MetaSlot>) -> bool {
79        &&& FRAME_METADATA_RANGE.start <= perm.addr() < FRAME_METADATA_RANGE.end
80        &&& perm.addr() % META_SLOT_SIZE == 0
81    }
82
83    pub open spec fn get_from_in_use_panic_cond(paddr: Paddr, regions: MetaRegionOwners) -> bool {
84        let idx = frame_to_index(paddr);
85        let pre_perms = regions.slot_owners[idx].inner_perms.ref_count.value();
86        pre_perms + 1 >= REF_COUNT_MAX
87    }
88
89    pub open spec fn get_from_in_use_success(paddr: Paddr, pre: MetaRegionOwners, post: MetaRegionOwners) -> bool
90        recommends
91            paddr % PAGE_SIZE == 0,
92            paddr < MAX_PADDR,
93            pre.inv(),
94    {
95        let idx = frame_to_index(paddr);
96        let pre_perms = pre.slot_owners[idx].inner_perms.ref_count.value();
97        {
98            &&& post.slot_owners[idx].inner_perms.ref_count.value() == pre_perms + 1
99            &&& post.slot_owners[idx].inner_perms.ref_count.id() == pre.slot_owners[idx].inner_perms.ref_count.id()
100            &&& post.slot_owners[idx].inner_perms.storage == pre.slot_owners[idx].inner_perms.storage
101            &&& post.slot_owners[idx].inner_perms.vtable_ptr == pre.slot_owners[idx].inner_perms.vtable_ptr
102            &&& post.slot_owners[idx].inner_perms.in_list == pre.slot_owners[idx].inner_perms.in_list
103            &&& post.slot_owners[idx].self_addr == pre.slot_owners[idx].self_addr
104            &&& post.slot_owners[idx].usage == pre.slot_owners[idx].usage
105            &&& post.slot_owners[idx].raw_count == pre.slot_owners[idx].raw_count
106            &&& post.slot_owners[idx].path_if_in_pt == pre.slot_owners[idx].path_if_in_pt
107            &&& forall|i: usize| i != idx ==> (#[trigger] post.slot_owners[i] == pre.slot_owners[i])
108        }
109    }
110
111    pub open spec fn drop_last_in_place_safety_cond(owner: MetaSlotOwner) -> bool {
112        &&& (owner.inner_perms.ref_count.value() == 0
113            || owner.inner_perms.ref_count.value() == REF_COUNT_UNIQUE)
114        &&& owner.inner_perms.storage.is_init()
115        &&& owner.inner_perms.in_list.value() == 0
116        &&& owner.raw_count == 0
117    }
118
119    pub open spec fn inc_ref_count_spec(&self, pre: MetaSlotModel) -> (MetaSlotModel)
120        recommends
121            pre.inv(),
122            pre.status == MetaSlotStatus::SHARED,
123    {
124        MetaSlotModel { ref_count: (pre.ref_count + 1) as u64, ..pre }
125    }
126}
127
128impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Frame<M> {
129    pub open spec fn from_raw_spec(paddr: Paddr) -> Self {
130        Frame::<M> {
131            ptr: PPtr::<MetaSlot>(frame_to_meta(paddr), PhantomData),
132            _marker: PhantomData,
133        }
134    }
135}
136
137} // verus!
ostd/specs/mm/frame/meta_specs.rs

ostd/specs/mm/frame/
meta_specs.rs
