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

ostd/specs/mm/frame/
meta_specs.rs
