ostd/specs/mm/frame/
meta_owners.rs

1//! The model of a metadata slot. It includes:
2//! - The model of the metadata slot: `MetaSlotModel`.
3//! - The invariants for both MetaSlot and MetaSlotModel.
4//! - The primitives for MetaSlot.
5use vstd::atomic::*;
6use vstd::cell;
7use vstd::prelude::*;
8use vstd::simple_pptr::*;
9
10use vstd_extra::cast_ptr::{self, Repr};
11use vstd_extra::ownership::*;
12use vstd_extra::ghost_tree::TreePath;
13
14use super::*;
15use crate::mm::frame::meta::{MetaSlot, MetaSlotStorage};
16use crate::specs::arch::kspace::FRAME_METADATA_RANGE;
17use crate::specs::mm::frame::mapping::META_SLOT_SIZE;
18use crate::specs::arch::mm::CONST_NR_ENTRIES;
19
20use core::marker::PhantomData;
21
22verus! {
23
24#[allow(non_camel_case_types)]
25pub enum MetaSlotStatus {
26    UNUSED,
27    UNIQUE,
28    SHARED,
29    OVERFLOW,
30    UNDER_CONSTRUCTION,
31}
32
33pub enum PageState {
34    Unused,
35    Typed,
36    Untyped,
37}
38
39#[repr(u8)]
40#[derive(Debug, PartialEq, Clone, Copy)]
41#[rustc_has_incoherent_inherent_impls]
42pub enum PageUsage {
43    // The zero variant is reserved for the unused type. Only an unused page
44    // can be designated for one of the other purposes.
45    #[allow(dead_code)]
46    Unused,
47    /// The page is reserved or unusable. The kernel should not touch it.
48    #[allow(dead_code)]
49    Reserved,
50    /// The page is used as a frame, i.e., a page of untyped memory.
51    Frame,
52    /// The page is used by a page table.
53    PageTable,
54    /// The page stores metadata of other pages.
55    Meta,
56    /// The page stores the kernel such as kernel code, data, etc.
57    Kernel,
58}
59
60impl PageUsage {
61    pub open spec fn as_u8_spec(&self) -> u8 {
62        match self {
63            PageUsage::Unused => 0,
64            PageUsage::Reserved => 1,
65            PageUsage::Frame => 32,
66            PageUsage::PageTable => 64,
67            PageUsage::Meta => 65,
68            PageUsage::Kernel => 66,
69        }
70    }
71
72    #[verifier::external_body]
73    #[verifier::when_used_as_spec(as_u8_spec)]
74    pub fn as_u8(&self) -> (res: u8)
75        ensures
76            res == self.as_u8_spec(),
77    {
78        *self as u8
79    }
80
81    #[vstd::contrib::auto_spec]
82    pub fn as_state(&self) -> (res: PageState) {
83        match &self {
84            PageUsage::Unused => PageState::Unused,
85            PageUsage::Frame => PageState::Untyped,
86            _ => PageState::Typed,
87        }
88    }
89}
90
91pub const REF_COUNT_UNUSED: u64 = u64::MAX;
92
93pub const REF_COUNT_UNIQUE: u64 = u64::MAX - 1;
94
95pub const REF_COUNT_MAX: u64 = i64::MAX as u64;
96
97} // verus!
98verus! {
99
100pub tracked struct MetaSlotOwner {
101    pub storage: PointsTo<MetaSlotStorage>,
102    pub ref_count: PermissionU64,
103    pub vtable_ptr: PointsTo<usize>,
104    pub in_list: PermissionU64,
105    pub self_addr: usize,
106    pub usage: PageUsage,
107    pub path_if_in_pt: Option<TreePath<CONST_NR_ENTRIES>>,
108}
109
110impl Inv for MetaSlotOwner {
111    open spec fn inv(self) -> bool {
112        &&& self.ref_count.value() == REF_COUNT_UNUSED ==> {
113            &&& self.vtable_ptr.is_uninit()
114            &&& self.in_list.value() == 0
115        }
116        &&& self.ref_count.value() == REF_COUNT_UNIQUE ==> {
117            &&& self.vtable_ptr.is_init()
118        }
119        &&& 0 < self.ref_count.value() < REF_COUNT_MAX ==> {
120            &&& self.vtable_ptr.is_init()
121        }
122        &&& REF_COUNT_MAX <= self.ref_count.value() < REF_COUNT_UNUSED ==> { false }
123        &&& self.ref_count.value() == 0 ==> {
124            &&& self.vtable_ptr.is_uninit()
125            &&& self.in_list.value() == 0
126        }
127        &&& FRAME_METADATA_RANGE().start <= self.self_addr < FRAME_METADATA_RANGE().end
128        &&& self.self_addr % META_SLOT_SIZE() == 0
129    }
130}
131
132pub ghost struct MetaSlotModel {
133    pub status: MetaSlotStatus,
134    pub storage: MemContents<MetaSlotStorage>,
135    pub ref_count: u64,
136    pub vtable_ptr: MemContents<usize>,
137    pub in_list: u64,
138    pub self_addr: usize,
139    pub usage: PageUsage,
140}
141
142impl Inv for MetaSlotModel {
143    open spec fn inv(self) -> bool {
144        match self.ref_count {
145            REF_COUNT_UNUSED => {
146                &&& self.vtable_ptr.is_uninit()
147                &&& self.in_list == 0
148            },
149            REF_COUNT_UNIQUE => { &&& self.vtable_ptr.is_init() },
150            0 => {
151                &&& self.vtable_ptr.is_uninit()
152                &&& self.in_list == 0
153            },
154            _ if self.ref_count < REF_COUNT_MAX => { &&& self.vtable_ptr.is_init() },
155            _ => { false },
156        }
157    }
158}
159
160impl View for MetaSlotOwner {
161    type V = MetaSlotModel;
162
163    open spec fn view(&self) -> Self::V {
164        let storage = self.storage.mem_contents();
165        let ref_count = self.ref_count.value();
166        let vtable_ptr = self.vtable_ptr.mem_contents();
167        let in_list = self.in_list.value();
168        let self_addr = self.self_addr;
169        let usage = self.usage;
170        let status = match ref_count {
171            REF_COUNT_UNUSED => MetaSlotStatus::UNUSED,
172            REF_COUNT_UNIQUE => MetaSlotStatus::UNIQUE,
173            0 => MetaSlotStatus::UNDER_CONSTRUCTION,
174            _ if ref_count < REF_COUNT_MAX => MetaSlotStatus::SHARED,
175            _ => MetaSlotStatus::OVERFLOW,
176        };
177        MetaSlotModel { status, storage, ref_count, vtable_ptr, in_list, self_addr, usage }
178    }
179}
180
181impl InvView for MetaSlotOwner {
182    proof fn view_preserves_inv(self) {
183    }
184}
185
186impl OwnerOf for MetaSlot {
187    type Owner = MetaSlotOwner;
188
189    open spec fn wf(self, owner: Self::Owner) -> bool {
190        &&& self.storage == owner.storage.pptr()
191        &&& self.ref_count.id() == owner.ref_count.id()
192        &&& self.vtable_ptr == owner.vtable_ptr.pptr()
193        &&& self.in_list.id() == owner.in_list.id()
194    }
195}
196
197impl ModelOf for MetaSlot {
198
199}
200
201} // verus!
ostd/specs/mm/frame/meta_owners.rs

ostd/specs/mm/frame/
meta_owners.rs
