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::{get_slot_spec, 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_owners::{MetaPerm, MetaSlotStorage};
11use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
12
13use core::marker::PhantomData;
14
15verus! {
16
17impl<'a, M: AnyFrameMeta> Frame<M> {
18    /// # Internal Safety Spec
19    /// This is a condition that supports unsafe Rust encapsulation. It should never be exposed to
20    /// the API client.
21    pub open spec fn from_raw_requires(regions: MetaRegionOwners, paddr: Paddr) -> bool {
22        &&& regions.slot_owners.contains_key(frame_to_index(paddr))
23        &&& regions.slot_owners[frame_to_index(paddr)].raw_count == 1
24        &&& regions.slot_owners[frame_to_index(paddr)].self_addr == frame_to_meta(paddr)
25        &&& has_safe_slot(paddr) // TODO: this should actually imply the first condition
26        &&& regions.inv()
27    }
28
29    pub open spec fn from_raw_ensures(
30        old_regions: MetaRegionOwners,
31        new_regions: MetaRegionOwners,
32        paddr: Paddr,
33        r: Self,
34    ) -> bool {
35        &&& new_regions.inv()
36        &&& new_regions.slots.contains_key(frame_to_index(paddr))
37        &&& new_regions.slot_owners[frame_to_index(paddr)].raw_count == 0
38        &&& new_regions.slot_owners[frame_to_index(paddr)].inner_perms ==
39            old_regions.slot_owners[frame_to_index(paddr)].inner_perms
40        &&& new_regions.slot_owners[frame_to_index(paddr)].usage ==
41            old_regions.slot_owners[frame_to_index(paddr)].usage
42        &&& new_regions.slot_owners[frame_to_index(paddr)].path_if_in_pt ==
43            old_regions.slot_owners[frame_to_index(paddr)].path_if_in_pt
44        &&& new_regions.slot_owners[frame_to_index(paddr)].self_addr == r.ptr.addr()
45        &&& forall|i: usize|
46            #![trigger new_regions.slot_owners[i], old_regions.slot_owners[i]]
47            i != frame_to_index(paddr) ==> new_regions.slot_owners[i] == old_regions.slot_owners[i]
48        &&& forall|i: usize|
49            i != frame_to_index(paddr) ==>
50            new_regions.slots.contains_key(i) == old_regions.slots.contains_key(i)
51        &&& r.ptr.addr() == frame_to_meta(paddr)
52        &&& r.paddr() == paddr
53    }
54
55
56    // ── into_raw precondition predicates ──
57
58    /// **Safety Invariant**: The frame's structural invariant must hold.
59    pub open spec fn into_raw_pre_frame_inv(self) -> bool {
60        self.inv()
61    }
62
63    /// **Bookkeeping**: The frame must be in use (not unused).
64    pub open spec fn into_raw_pre_not_unused(self, regions: MetaRegionOwners) -> bool {
65        regions.slot_owners[self.index()].inner_perms.ref_count.value() != REF_COUNT_UNUSED
66    }
67
68    // ── into_raw postcondition predicates ──
69
70    /// **Correctness**: The frame's raw count is incremented.
71    pub open spec fn into_raw_post_raw_count_incremented(
72        self,
73        old_regions: MetaRegionOwners,
74        new_regions: MetaRegionOwners,
75    ) -> bool {
76        &&& new_regions.slot_owners.contains_key(self.index())
77        &&& new_regions.slot_owners[self.index()].raw_count
78            == (old_regions.slot_owners[self.index()].raw_count + 1) as usize
79    }
80
81    /// **Safety**: Frames other than this one are not affected by the call.
82    pub open spec fn into_raw_post_noninterference(
83        self,
84        old_regions: MetaRegionOwners,
85        new_regions: MetaRegionOwners,
86    ) -> bool {
87        &&& forall|i: usize|
88            #![trigger new_regions.slots[i], old_regions.slots[i]]
89            i != self.index() && old_regions.slots.contains_key(i)
90                ==> new_regions.slots.contains_key(i)
91                    && new_regions.slots[i] == old_regions.slots[i]
92        &&& forall|i: usize|
93            #![trigger new_regions.slot_owners[i], old_regions.slot_owners[i]]
94            i != self.index() ==> new_regions.slot_owners[i] == old_regions.slot_owners[i]
95        &&& new_regions.slot_owners.dom() =~= old_regions.slot_owners.dom()
96    }
97}
98
99} // verus!
ostd/specs/mm/frame/frame_specs.rs

ostd/specs/mm/frame/
frame_specs.rs
