ostd/specs/mm/frame/
meta_specs.rs

1use core::marker::PhantomData;
2
3use vstd::prelude::*;
4
5use vstd::{
6    atomic::*,
7    simple_pptr::{self, PPtr},
8};
9use vstd_extra::{cast_ptr::*, ownership::*};
10
11use crate::specs::{
12    arch::*,
13    mm::frame::{
14        mapping::{frame_to_index, index_to_meta},
15        meta_owners::MetadataInnerPerms,
16        meta_region_owners::MetaRegionOwners,
17    },
18};
19
20use crate::mm::{
21    Paddr, PagingLevel, Vaddr,
22    frame::{
23        meta::{
24            META_SLOT_SIZE, REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED,
25            mapping::{frame_to_meta, meta_to_frame},
26        },
27        *,
28    },
29    kspace::FRAME_METADATA_RANGE,
30};
31
32use super::meta_owners::{
33    MetaSlotModel, MetaSlotOwner, MetaSlotStatus, MetaSlotStorage, Metadata, PageUsage,
34};
35
36verus! {
37
38global layout MetaSlot is size == 64, align == 8;
39
40impl MetaSlot {
41    pub proof fn lemma_layout()
42        ensures
43            core::mem::size_of::<MetaSlot>() == META_SLOT_SIZE,
44            vstd::layout::size_of::<MetaSlot>() == META_SLOT_SIZE,
45    {
46        broadcast use VERUS_layout_of_MetaSlot;
47
48    }
49
50    /// A helper function that casts a `MetaSlot` pointer to a `Metadata` pointer of type `M`.
51    #[verus_spec(res =>
52        with
53            Tracked(perm): Tracked<&vstd::simple_pptr::PointsTo<MetaSlot>>,
54        requires
55            perm.value() == self,
56            addr == perm.addr(),
57        ensures
58            res.ptr.addr() == addr,
59            res.addr() == addr,
60    )]
61    pub fn cast_slot<M: AnyFrameMeta + Repr<MetaSlotStorage>>(&self, addr: usize) -> ReprPtr<
62        MetaSlot,
63        Metadata<M>,
64    > {
65        ReprPtr::<MetaSlot, Metadata<M>> { ptr: PPtr::from_addr(addr), _T: PhantomData }
66    }
67
68    pub open spec fn get_from_unused_inner_perms_spec(
69        as_unique: bool,
70        perms: MetadataInnerPerms,
71    ) -> bool {
72        &&& perms.ref_count.value() == (if as_unique {
73            REF_COUNT_UNIQUE as u64
74        } else {
75            1u64
76        })
77        &&& perms.in_list.value() == 0
78        &&& perms.storage.is_init()
79        &&& perms.vtable_ptr.is_init()
80    }
81
82    /// The `slot_owners`/`obligations` transition of claiming an unused slot.
83    pub open spec fn get_from_unused_spec(
84        paddr: Paddr,
85        as_unique: bool,
86        pre: MetaRegionOwners,
87        post: MetaRegionOwners,
88    ) -> bool
89        recommends
90            valid_frame_paddr(paddr),
91            pre.inv(),
92    {
93        let idx = frame_to_index(paddr);
94        let pre_owner = pre.slot_owners[idx];
95        let post_owner = post.slot_owners[idx];
96        {
97            &&& pre_owner.inner_perms.ref_count.value() == REF_COUNT_UNUSED
98            &&& MetaSlot::get_from_unused_inner_perms_spec(as_unique, post_owner.inner_perms)
99            &&& post_owner.usage is Frame
100            &&& post_owner.slot_vaddr == pre_owner.slot_vaddr
101            &&& post_owner.paths_in_pt == pre_owner.paths_in_pt
102            &&& post =~= pre.insert_slot_owner(paddr, post_owner)
103        }
104    }
105
106    /// Variant of [`get_from_unused_spec`] for allocating a page-table *node*
107    /// (always non-unique). Identical except the claimed slot becomes
108    /// `PageUsage::PageTable` rather than `PageUsage::Frame`: a page-table
109    /// node is tracked with `PageTable` usage, which gives a clean
110    /// usage-based discriminator between node slots and data-frame slots
111    /// (the latter are `Frame`/MMIO). Used by the node allocators
112    /// (`PageTableNode::alloc`, `PageTable::empty_with_owner`).
113    pub open spec fn get_node_from_unused_spec(
114        paddr: Paddr,
115        pre: MetaRegionOwners,
116        post: MetaRegionOwners,
117    ) -> bool
118        recommends
119            valid_frame_paddr(paddr),
120            pre.inv(),
121    {
122        let idx = frame_to_index(paddr);
123        {
124            &&& post.slot_owners.dom() =~= pre.slot_owners.dom()
125            &&& MetaSlot::get_from_unused_inner_perms_spec(false, post.slot_owners[idx].inner_perms)
126            &&& post.slot_owners[idx].usage is PageTable
127            &&& post.slot_owners[idx].slot_vaddr == pre.slot_owners[idx].slot_vaddr
128            &&& post.slot_owners[idx].paths_in_pt == pre.slot_owners[idx].paths_in_pt
129            &&& forall|i: int| i != idx ==> (#[trigger] post.slot_owners[i] == pre.slot_owners[i])
130            &&& pre.slot_owners[idx].inner_perms.ref_count.value() == REF_COUNT_UNUSED
131        }
132    }
133
134    /// Permission-location clause: the extracted slot perm was *re-parked* into
135    /// `regions.slots`, so the domain is preserved and every other slot's perm
136    /// is untouched. Callers that re-park (see
137    /// [`crate::mm::frame::Frame::from_unused`] — it hands the perm back via the
138    /// `perm` out-param and re-inserts it) pair this with [`get_from_unused_spec`]
139    /// (the `slot_owners` transition) to fully describe the Design-B post-state.
140    pub open spec fn slot_perm_reparked_spec(
141        paddr: Paddr,
142        pre: MetaRegionOwners,
143        post: MetaRegionOwners,
144    ) -> bool {
145        let idx = frame_to_index(paddr);
146        &&& post.slots.dom() =~= pre.slots.dom()
147        &&& forall|k: int|
148            #![trigger post.slots[k]]
149            k != idx && pre.slots.contains_key(k) ==> post.slots[k] == pre.slots[k]
150    }
151
152    /// Obligation-ledger effect of producing a fresh live `Frame` handle on
153    /// success (e.g. [`crate::mm::frame::Frame::from_unused`] or
154    /// [`crate::mm::frame::Frame::from_in_use`]): the segment `obligations`
155    /// ledger is untouched, and the new handle mints its pending-Drop entry in
156    /// `frame_obligations` at `paddr`.
157    pub open spec fn live_frame_obligations_ok_spec(
158        paddr: Paddr,
159        pre: MetaRegionOwners,
160        post: MetaRegionOwners,
161    ) -> bool {
162        &&& post.frame_obligations =~= pre.frame_obligations.insert(frame_to_index(paddr))
163    }
164
165    /// Obligation-ledger effect on failure: both the segment and frame ledgers
166    /// are left untouched.
167    pub open spec fn live_frame_obligations_err_spec(
168        pre: MetaRegionOwners,
169        post: MetaRegionOwners,
170    ) -> bool {
171        &&& post.frame_obligations =~= pre.frame_obligations
172    }
173
174    pub open spec fn get_from_unused_perm_spec<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
175        paddr: Paddr,
176        metadata: M,
177        as_unique: bool,
178        ptr: PPtr<MetaSlot>,
179        perm: simple_pptr::PointsTo<MetaSlot>,
180    ) -> bool {
181        &&& ptr.addr() == frame_to_meta(paddr)
182        &&& perm.addr() == frame_to_meta(paddr)
183        &&& perm.is_init()
184        &&& perm.pptr() == ptr
185    }
186
187    pub open spec fn inc_ref_count_panic_cond(rc_perm: PermissionU64) -> bool {
188        rc_perm.value() >= REF_COUNT_MAX
189    }
190
191    pub open spec fn frame_paddr_safety_cond(perm: vstd::simple_pptr::PointsTo<MetaSlot>) -> bool {
192        &&& FRAME_METADATA_RANGE.start <= perm.addr() < FRAME_METADATA_RANGE.end
193        &&& perm.addr() % META_SLOT_SIZE == 0
194    }
195
196    pub open spec fn get_from_in_use_success(
197        paddr: Paddr,
198        pre: MetaRegionOwners,
199        post: MetaRegionOwners,
200    ) -> bool
201        recommends
202            valid_frame_paddr(paddr),
203            pre.inv(),
204    {
205        let idx = frame_to_index(paddr);
206        let pre_perms = pre.slot_owners[idx].inner_perms.ref_count.value();
207        {
208            &&& post.slot_owners[idx].inner_perms.ref_count.value() == pre_perms + 1
209            &&& post.slot_owners[idx].inner_perms.ref_count.id()
210                == pre.slot_owners[idx].inner_perms.ref_count.id()
211            &&& post.slot_owners[idx].inner_perms.storage
212                == pre.slot_owners[idx].inner_perms.storage
213            &&& post.slot_owners[idx].inner_perms.vtable_ptr
214                == pre.slot_owners[idx].inner_perms.vtable_ptr
215            &&& post.slot_owners[idx].inner_perms.in_list
216                == pre.slot_owners[idx].inner_perms.in_list
217            &&& post.slot_owners[idx].slot_vaddr == pre.slot_owners[idx].slot_vaddr
218            &&& post.slot_owners[idx].usage == pre.slot_owners[idx].usage
219            &&& post.slot_owners[idx].paths_in_pt == pre.slot_owners[idx].paths_in_pt
220            &&& forall|i: int| i != idx ==> (#[trigger] post.slot_owners[i] == pre.slot_owners[i])
221        }
222    }
223
224    pub open spec fn drop_last_in_place_safety_cond(owner: MetaSlotOwner) -> bool {
225        &&& (owner.inner_perms.ref_count.value() == 0 || owner.inner_perms.ref_count.value()
226            == REF_COUNT_UNIQUE)
227        &&& owner.inner_perms.storage.is_init()
228        &&& owner.inner_perms.in_list.value()
229            == 0
230        // The slot is torn down to `REF_COUNT_UNUSED`; the strengthened
231        // `MetaSlotOwner::inv` UNUSED branch requires an empty
232        // `paths_in_pt`, and `drop_last_in_place` does not touch
233        // `paths_in_pt`, so it must already be empty. Sound: a slot at
234        // the teardown point has no live PTE mapping (a mapping is a
235        // reference — it would keep the count above the teardown
236        // threshold).
237        &&& owner.paths_in_pt.is_empty()
238    }
239
240    pub open spec fn inc_ref_count_spec(&self, pre: MetaSlotModel) -> (MetaSlotModel)
241        recommends
242            pre.inv(),
243            pre.status == MetaSlotStatus::SHARED,
244    {
245        MetaSlotModel { ref_count: (pre.ref_count + 1) as u64, ..pre }
246    }
247}
248
249impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Frame<M> {
250    pub open spec fn from_raw_spec(paddr: Paddr) -> Self {
251        Frame::<M> {
252            ptr: PPtr::<MetaSlot>(frame_to_meta(paddr), PhantomData),
253            _marker: PhantomData,
254        }
255    }
256}
257
258} // verus!
ostd/specs/mm/frame/meta_specs.rs

ostd/specs/mm/frame/
meta_specs.rs
