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

ostd/specs/mm/frame/
meta_specs.rs
