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 for the static `MetaSlot` permissions.
105    /// Only the slot at `paddr` is changed.
106    pub open spec fn slot_perm_reparked_spec(
107        paddr: Paddr,
108        pre: MetaRegionOwners,
109        post: MetaRegionOwners,
110    ) -> bool {
111        let idx = frame_to_index(paddr);
112        &&& post.slots.dom() =~= pre.slots.dom()
113        &&& forall|k: int|
114            #![trigger post.slots[k]]
115            k != idx && pre.contains(k) ==> post.slots[k] == pre.slots[k]
116    }
117
118    /// Obligation-ledger effect of producing a fresh live `Frame` handle on
119    /// success (e.g. [`crate::mm::frame::Frame::from_unused`] or
120    /// [`crate::mm::frame::Frame::from_in_use`]): the segment `obligations`
121    /// ledger is untouched, and the new handle mints its pending-Drop entry in
122    /// `frame_obligations` at `paddr`.
123    pub open spec fn live_frame_obligations_ok_spec(
124        paddr: Paddr,
125        pre: MetaRegionOwners,
126        post: MetaRegionOwners,
127    ) -> bool {
128        &&& post.frame_obligations =~= pre.frame_obligations.insert(frame_to_index(paddr))
129    }
130
131    /// Obligation-ledger effect on failure: both the segment and frame ledgers
132    /// are left untouched.
133    pub open spec fn live_frame_obligations_err_spec(
134        pre: MetaRegionOwners,
135        post: MetaRegionOwners,
136    ) -> bool {
137        &&& post.frame_obligations =~= pre.frame_obligations
138    }
139
140    pub open spec fn get_from_unused_perm_spec<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
141        paddr: Paddr,
142        metadata: M,
143        as_unique: bool,
144        ptr: PPtr<MetaSlot>,
145        perm: simple_pptr::PointsTo<MetaSlot>,
146    ) -> bool {
147        &&& ptr.addr() == frame_to_meta(paddr)
148        &&& perm.addr() == frame_to_meta(paddr)
149        &&& perm.is_init()
150        &&& perm.pptr() == ptr
151    }
152
153    pub open spec fn inc_ref_count_panic_cond(rc_perm: PermissionU64) -> bool {
154        rc_perm.value() >= REF_COUNT_MAX
155    }
156
157    pub open spec fn frame_paddr_safety_cond(perm: vstd::simple_pptr::PointsTo<MetaSlot>) -> bool {
158        &&& FRAME_METADATA_RANGE.start <= perm.addr() < FRAME_METADATA_RANGE.end
159        &&& perm.addr() % META_SLOT_SIZE == 0
160    }
161
162    pub open spec fn get_from_in_use_success(
163        paddr: Paddr,
164        pre: MetaRegionOwners,
165        post: MetaRegionOwners,
166    ) -> bool {
167        let idx = frame_to_index(paddr);
168        let pre_perms = pre.slot_owners[idx].ref_count();
169        {
170            &&& post.slot_owners[idx].ref_count() == pre_perms + 1
171            &&& post.slot_owners[idx].ref_count_perm.id()
172                == pre.slot_owners[idx].ref_count_perm.id()
173            &&& post.slot_owners[idx].storage_perm() == pre.slot_owners[idx].storage_perm()
174            &&& post.slot_owners[idx].vtable_ptr_perm() == pre.slot_owners[idx].vtable_ptr_perm()
175            &&& post.slot_owners[idx].in_list_perm == pre.slot_owners[idx].in_list_perm
176            &&& post.slot_owners[idx].slot_vaddr == pre.slot_owners[idx].slot_vaddr
177            &&& post.slot_owners[idx].usage == pre.slot_owners[idx].usage
178            &&& post.slot_owners[idx].paths_in_pt == pre.slot_owners[idx].paths_in_pt
179            &&& forall|i: int| i != idx ==> (#[trigger] post.slot_owners[i] == pre.slot_owners[i])
180        }
181    }
182
183    pub open spec fn drop_last_in_place_safety_cond(owner: MetaSlotOwner) -> bool {
184        &&& (owner.ref_count() == 0 || owner.ref_count() == REF_COUNT_UNIQUE)
185        &&& owner.storage_perm().is_init()
186        &&& owner.in_list_perm.value() == 0
187        &&& owner.paths_in_pt.is_empty()
188    }
189
190    pub open spec fn inc_ref_count_spec(&self, pre: MetaSlotModel) -> (MetaSlotModel)
191        recommends
192            pre.status == MetaSlotStatus::SHARED,
193    {
194        MetaSlotModel { ref_count: (pre.ref_count + 1) as u64, ..pre }
195    }
196}
197
198impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Frame<M> {
199    pub open spec fn from_raw_spec(paddr: Paddr) -> Self {
200        Frame::<M> {
201            ptr: PPtr::<MetaSlot>(frame_to_meta(paddr), PhantomData),
202            _marker: PhantomData,
203        }
204    }
205}
206
207} // verus!
ostd/specs/mm/frame/meta_specs.rs

ostd/specs/mm/frame/
meta_specs.rs
