ostd/specs/mm/frame/
frame_specs.rs

1use vstd::prelude::*;
2
3use vstd_extra::cast_ptr::*;
4use vstd_extra::ownership::*;
5
6use crate::mm::frame::meta::{mapping::frame_to_index, REF_COUNT_UNUSED};
7use crate::mm::frame::*;
8use crate::mm::{Paddr, PagingLevel, Vaddr};
9use crate::specs::arch::mm::{MAX_NR_PAGES, MAX_PADDR, PAGE_SIZE};
10use crate::specs::mm::frame::meta_region_owners::MetaRegionModel;
11
12use core::marker::PhantomData;
13
14verus! {
15
16impl<M: AnyFrameMeta + Repr<MetaSlot> + OwnerOf> UniqueFrame<M> {
17
18    pub open spec fn from_unused_spec(paddr: Paddr, metadata: M, pre: MetaRegionModel)
19        -> (Self, MetaRegionModel)
20        recommends
21            paddr % PAGE_SIZE() == 0,
22            paddr < MAX_PADDR(),
23            pre.inv(),
24            pre.slots[frame_to_index(paddr)].ref_count == REF_COUNT_UNUSED,
25    {
26        let (ptr, post) = MetaSlot::get_from_unused_spec(paddr, metadata, true, pre);
27        (UniqueFrame { ptr, _marker: PhantomData }, post)
28    }
29
30    pub proof fn from_unused_properties(paddr: Paddr, metadata: M, pre: MetaRegionModel)
31        requires
32            paddr % 4096 == 0,
33            paddr < MAX_PADDR(),
34            pre.inv(),
35            pre.slots[paddr / 4096].ref_count == REF_COUNT_UNUSED,
36        ensures
37            UniqueFrame::from_unused_spec(paddr, metadata, pre).1.inv(),
38    { }
39}
40
41} // verus!
ostd/specs/mm/frame/frame_specs.rs

ostd/specs/mm/frame/
frame_specs.rs
