ostd/specs/mm/frame/
meta_specs.rs

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

ostd/specs/mm/frame/
meta_specs.rs
