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    pub open spec fn get_from_unused_inner_perms_spec(
31        as_unique: bool,
32        perms: MetadataInnerPerms,
33    ) -> bool {
34        &&& perms.ref_count.value() == (if as_unique {
35            REF_COUNT_UNIQUE as u64
36        } else {
37            1u64
38        })
39        &&& perms.in_list.value() == 0
40        &&& perms.storage.is_init()
41        &&& perms.vtable_ptr.is_init()
42    }
43
44    pub open spec fn get_from_unused_spec(
45        paddr: Paddr,
46        as_unique: bool,
47        pre: MetaRegionOwners,
48        post: MetaRegionOwners,
49    ) -> bool
50        recommends
51            paddr % PAGE_SIZE == 0,
52            paddr < MAX_PADDR,
53            pre.inv(),
54    {
55        let idx = frame_to_index(paddr);
56        {
57            &&& post.slots =~= pre.slots.remove(idx)
58            &&& MetaSlot::get_from_unused_inner_perms_spec(
59                as_unique,
60                post.slot_owners[idx].inner_perms,
61            )
62            &&& post.slot_owners[idx].usage == PageUsage::Frame
63            &&& post.slot_owners[idx].raw_count == pre.slot_owners[idx].raw_count
64            &&& post.slot_owners[idx].self_addr == pre.slot_owners[idx].self_addr
65            &&& post.slot_owners[idx].path_if_in_pt == pre.slot_owners[idx].path_if_in_pt
66            &&& forall|i: usize| i != idx ==> (#[trigger] post.slot_owners[i] == pre.slot_owners[i])
67            &&& pre.slot_owners[idx].inner_perms.ref_count.value() == REF_COUNT_UNUSED
68        }
69    }
70
71    pub open spec fn get_from_unused_perm_spec<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
72        paddr: Paddr,
73        metadata: M,
74        as_unique: bool,
75        ptr: PPtr<MetaSlot>,
76        perm: PointsTo<MetaSlot, Metadata<M>>,
77    ) -> bool {
78        &&& ptr.addr() == frame_to_meta(paddr)
79        &&& perm.addr() == frame_to_meta(paddr)
80        &&& perm.is_init()
81        &&& perm.wf(&perm.inner_perms)
82        &&& MetaSlot::get_from_unused_inner_perms_spec(as_unique, perm.inner_perms)
83    }
84
85    pub open spec fn inc_ref_count_panic_cond(rc_perm: PermissionU64) -> bool {
86        rc_perm.value() >= REF_COUNT_MAX
87    }
88
89    pub open spec fn frame_paddr_safety_cond(perm: vstd::simple_pptr::PointsTo<MetaSlot>) -> bool {
90        &&& FRAME_METADATA_RANGE.start <= perm.addr() < FRAME_METADATA_RANGE.end
91        &&& perm.addr() % META_SLOT_SIZE == 0
92    }
93
94    pub open spec fn get_from_in_use_panic_cond(paddr: Paddr, regions: MetaRegionOwners) -> bool {
95        let idx = frame_to_index(paddr);
96        let pre_perms = regions.slot_owners[idx].inner_perms.ref_count.value();
97        pre_perms + 1 >= REF_COUNT_MAX
98    }
99
100    pub open spec fn get_from_in_use_success(
101        paddr: Paddr,
102        pre: MetaRegionOwners,
103        post: MetaRegionOwners,
104    ) -> bool
105        recommends
106            paddr % PAGE_SIZE == 0,
107            paddr < MAX_PADDR,
108            pre.inv(),
109    {
110        let idx = frame_to_index(paddr);
111        let pre_perms = pre.slot_owners[idx].inner_perms.ref_count.value();
112        {
113            &&& post.slot_owners[idx].inner_perms.ref_count.value() == pre_perms + 1
114            &&& post.slot_owners[idx].inner_perms.ref_count.id()
115                == pre.slot_owners[idx].inner_perms.ref_count.id()
116            &&& post.slot_owners[idx].inner_perms.storage
117                == pre.slot_owners[idx].inner_perms.storage
118            &&& post.slot_owners[idx].inner_perms.vtable_ptr
119                == pre.slot_owners[idx].inner_perms.vtable_ptr
120            &&& post.slot_owners[idx].inner_perms.in_list
121                == pre.slot_owners[idx].inner_perms.in_list
122            &&& post.slot_owners[idx].self_addr == pre.slot_owners[idx].self_addr
123            &&& post.slot_owners[idx].usage == pre.slot_owners[idx].usage
124            &&& post.slot_owners[idx].raw_count == pre.slot_owners[idx].raw_count
125            &&& post.slot_owners[idx].path_if_in_pt == pre.slot_owners[idx].path_if_in_pt
126            &&& forall|i: usize| i != idx ==> (#[trigger] post.slot_owners[i] == pre.slot_owners[i])
127        }
128    }
129
130    pub open spec fn drop_last_in_place_safety_cond(owner: MetaSlotOwner) -> bool {
131        &&& (owner.inner_perms.ref_count.value() == 0 || owner.inner_perms.ref_count.value()
132            == REF_COUNT_UNIQUE)
133        &&& owner.inner_perms.storage.is_init()
134        &&& owner.inner_perms.in_list.value() == 0
135        &&& owner.raw_count == 0
136    }
137
138    pub open spec fn inc_ref_count_spec(&self, pre: MetaSlotModel) -> (MetaSlotModel)
139        recommends
140            pre.inv(),
141            pre.status == MetaSlotStatus::SHARED,
142    {
143        MetaSlotModel { ref_count: (pre.ref_count + 1) as u64, ..pre }
144    }
145}
146
147impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Frame<M> {
148    pub open spec fn from_raw_spec(paddr: Paddr) -> Self {
149        Frame::<M> {
150            ptr: PPtr::<MetaSlot>(frame_to_meta(paddr), PhantomData),
151            _marker: PhantomData,
152        }
153    }
154}
155
156} // verus!
ostd/specs/mm/frame/meta_specs.rs

ostd/specs/mm/frame/
meta_specs.rs
