ostd/specs/arch/x86_64/
page_table_entry.rs

1use vstd::prelude::*;
2use vstd::raw_ptr::*;
3
4use core::fmt::Debug;
5
6use vstd_extra::prelude::*;
7
8use super::*;
9use crate::mm::{
10    page_prop::{CachePolicy, PageFlags, PageProperty, PrivilegedPageFlags},
11    page_table::*,
12    Paddr, PagingLevel,
13};
14
15decl_bms_const!(
16    PAGE_FLAG_MAPPING,
17    PAGE_FLAG_MAPPING_SPEC,
18    u8,
19    usize,
20    4,
21    [
22        (PageFlags::R().value(), PageTableFlags::PRESENT()),
23        (PageFlags::W().value(), PageTableFlags::WRITABLE()),
24        (PageFlags::ACCESSED().value(), PageTableFlags::ACCESSED()),
25        (PageFlags::DIRTY().value(), PageTableFlags::DIRTY())
26    ]
27);
28
29decl_bms_const!(
30    PAGE_PRIV_MAPPING,
31    PAGE_PRIV_MAPPING_SPEC,
32    u8,
33    usize,
34    2,
35    [
36        (PrivilegedPageFlags::USER().value(), PageTableFlags::USER()),
37        (
38            PrivilegedPageFlags::GLOBAL().value(),
39            PageTableFlags::GLOBAL()
40        )
41    ]
42);
43
44decl_bms_const!(
45    PAGE_INVERTED_FLAG_MAPPING,
46    PAGE_INVERTED_FLAG_MAPPING_SPEC,
47    u8,
48    usize,
49    1,
50    [(PageFlags::X().value(), PageTableFlags::NO_EXECUTE())]
51);
52
53verus! {
54
55#[repr(transparent)]
56#[derive(Copy, Debug, PartialEq)]
57pub struct PageTableEntry(pub usize);
58
59global layout PageTableEntry is size == 8, align == 8;
60
61extern_const!(
62/// Masks of the physical address.
63pub PHYS_ADDR_MASK
64    [PHYS_ADDR_MASK_SPEC, CONST_PHYS_ADDR_MASK]: usize =
65    0xffff_ffff_ffff_f000);
66
67impl Clone for PageTableEntry {
68    fn clone(&self) -> Self {
69        Self { 0: self.0 }
70    }
71}
72
73#[allow(non_snake_case)]
74impl PageTableEntry {
75
76    #[inline(always)]
77    #[vstd::contrib::auto_spec]
78    pub const fn PROP_MASK() -> (res: usize)
79    {
80        !PHYS_ADDR_MASK() & !(PageTableFlags::HUGE())
81    }
82
83    #[verifier::inline]
84    pub open spec fn prop_assign_spec(self, flags: usize) -> Self {
85        Self((self.0 & !Self::PROP_MASK()) | flags as usize)
86    }
87
88    #[inline(always)]
89    pub fn prop_assign(&mut self, flags: usize)
90        ensures self.0 == old(self).prop_assign_spec(flags).0
91    {
92        self.0 = (self.0 & !Self::PROP_MASK()) | flags as usize;
93    }
94
95    #[vstd::contrib::auto_spec]
96    pub fn encode_cache(cache: CachePolicy) -> (res: usize)
97    {
98        match cache {
99            CachePolicy::Uncacheable => PageTableFlags::NO_CACHE(),
100            CachePolicy::Writethrough => PageTableFlags::WRITE_THROUGH(),
101            _ => 0,
102        }
103    }
104
105    pub open spec fn format_flags_spec(prop: PageProperty) -> usize {
106        let flags: u8 = prop.flags.value();
107        let priv_flags: u8 = prop.priv_flags.value();
108        PageTableFlags::PRESENT()
109            | flags.map_forward(&PAGE_FLAG_MAPPING)
110            | flags.map_invert_forward(&PAGE_INVERTED_FLAG_MAPPING)
111            | priv_flags.map_forward(&PAGE_PRIV_MAPPING)
112            | Self::encode_cache(prop.cache)
113    }
114
115    #[verifier::external_body]
116    #[verifier::when_used_as_spec(format_flags_spec)]
117    pub fn format_flags(prop: PageProperty) -> (res: usize)
118        ensures res == Self::format_flags_spec(prop)
119    {
120        let flags: u8 = prop.flags.value();
121        let priv_flags: u8 = prop.priv_flags.value();
122        PageTableFlags::PRESENT()
123            | flags.map_forward(&PAGE_FLAG_MAPPING)
124            | flags.map_invert_forward(&PAGE_INVERTED_FLAG_MAPPING)
125            | priv_flags.map_forward(&PAGE_PRIV_MAPPING)
126            | Self::encode_cache(prop.cache)
127    }
128
129    #[vstd::contrib::auto_spec]
130    pub fn format_cache(flags: usize) -> (res: CachePolicy)
131    {
132        if flags & PageTableFlags::NO_CACHE() != 0 {
133            CachePolicy::Uncacheable
134        } else if flags & PageTableFlags::WRITE_THROUGH() != 0 {
135            CachePolicy::Writethrough
136        } else {
137            CachePolicy::Writeback
138        }
139    }
140
141    pub open spec fn format_property_spec(entry: usize) -> PageProperty {
142        let flags: u8 = entry.map_backward(&PAGE_FLAG_MAPPING)
143                      | entry.map_invert_backward(&PAGE_INVERTED_FLAG_MAPPING);
144        let priv_flags: u8 = entry.map_backward(&PAGE_PRIV_MAPPING);
145        let cache = Self::format_cache(entry);
146        PageProperty {
147            flags: PageFlags::from_bits(flags),
148            cache,
149            priv_flags: PrivilegedPageFlags::from_bits(priv_flags),
150        }
151    }
152
153    #[verifier::external_body]
154    #[verifier::when_used_as_spec(format_property_spec)]
155    pub fn format_property(entry: usize) -> (res: PageProperty)
156        ensures res == Self::format_property_spec(entry)
157    {
158        let flags = entry.map_backward(&PAGE_FLAG_MAPPING)
159                  | entry.map_invert_backward(&PAGE_INVERTED_FLAG_MAPPING);
160        let priv_flags: u8 = entry.map_backward(&PAGE_PRIV_MAPPING);
161        let cache = Self::format_cache(entry);
162        PageProperty {
163            flags: PageFlags::from_bits(flags),
164            cache,
165            priv_flags: PrivilegedPageFlags::from_bits(priv_flags),
166        }
167    }
168
169    #[inline(always)]
170    #[vstd::contrib::auto_spec]
171    pub fn format_huge_page(level: PagingLevel) -> (res: u64)
172    {
173        if level == 1 {
174            0
175        } else {
176            PageTableFlags::HUGE() as u64
177        }
178    }
179
180}
181
182}
183
184verus! {
185
186impl PageTableEntryTrait for PageTableEntry {
187
188    #[verifier::inline]
189    open spec fn default_spec() -> Self
190    {
191        Self { 0: 0 }
192    }
193
194    #[inline(always)]
195    fn default() -> (res: Self)
196        ensures res == Self::default_spec()
197    {
198        Self { 0: 0 }
199    }
200
201    #[verifier::inline]
202    open spec fn new_absent_spec() -> Self {
203        Self::default_spec()
204    }
205
206    #[inline(always)]
207    #[verifier::external_body]
208    fn new_absent() -> (res: Self)
209    {
210        Self::default()
211    }
212
213    #[verifier::inline]
214    open spec fn as_usize_spec(self) -> usize {
215        self.0 as usize
216    }
217
218    #[inline(always)]
219    fn as_usize(self) -> (res: usize)
220            ensures res == self.as_usize_spec()
221    {
222        self.0 as usize
223    }
224
225    #[verifier::inline]
226    open spec fn is_present_spec(&self) -> bool {
227        self.0 & PageTableFlags::PRESENT() != 0
228    }
229
230    #[inline(always)]
231    fn is_present(&self) -> (res: bool)
232        ensures res == self.is_present_spec()
233    {
234        self.0 & PageTableFlags::PRESENT() != 0
235    }
236
237    open spec fn set_prop_spec(&self, prop: PageProperty) -> Self {
238        let flags = Self::format_flags(prop);
239        self.prop_assign_spec(flags)
240    }
241
242    fn set_prop(&mut self, prop: PageProperty)
243        ensures *self == old(self).set_prop_spec(prop)
244    {
245        let flags = Self::format_flags(prop);
246        self.prop_assign(flags)
247    }
248
249    open spec fn new_page_spec(paddr: Paddr, level: PagingLevel, prop: PageProperty) -> Self {
250        let addr = paddr & PHYS_ADDR_MASK();
251        let hp = Self::format_huge_page(level) as usize;
252        let flags = Self::format_flags(prop) as usize;
253        Self(addr | hp | flags)
254    }
255
256    #[verifier::external_body]
257    fn new_page(paddr: Paddr, level: PagingLevel, prop: PageProperty) -> (res: Self)
258    {
259        let addr = paddr & PHYS_ADDR_MASK();
260        let hp = Self::format_huge_page(level) as usize;
261        let flags = Self::format_flags(prop) as usize;
262        Self(addr | hp | flags)
263    }
264
265    open spec fn new_pt_spec(paddr: Paddr) -> Self {
266        let addr = paddr & PHYS_ADDR_MASK();
267        Self(addr | PageTableFlags::PRESENT() | PageTableFlags::WRITABLE() | PageTableFlags::USER())
268    }
269
270    #[verifier::external_body]
271    fn new_pt(paddr: Paddr) -> (res: Self)
272    {
273        let addr = paddr & PHYS_ADDR_MASK();
274        Self(addr | PageTableFlags::PRESENT() | PageTableFlags::WRITABLE() | PageTableFlags::USER())
275    }
276
277    #[verifier::inline]
278    open spec fn paddr_spec(&self) -> Paddr {
279        self.0 & PHYS_ADDR_MASK()
280    }
281
282    #[inline(always)]
283    fn paddr(&self) -> (res: Paddr)
284        ensures res == self.paddr_spec()
285    {
286        self.0 & PHYS_ADDR_MASK()
287    }
288
289    #[verifier::inline]
290    open spec fn prop_spec(&self) -> PageProperty {
291        Self::format_property(self.0)
292    }
293
294    #[inline(always)]
295    fn prop(&self) -> (res: PageProperty)
296        ensures res == self.prop_spec()
297    {
298        Self::format_property(self.0)
299    }
300
301    #[verifier::inline]
302    open spec fn is_last_spec(&self, level: PagingLevel) -> bool {
303        level == 1 || (self.0 & PageTableFlags::HUGE() != 0)
304    }
305
306    #[inline(always)]
307    fn is_last(&self, level: PagingLevel) -> (res: bool)
308        ensures res == self.is_last_spec(level)
309    {
310        level == 1 || (self.0 & PageTableFlags::HUGE() != 0)
311    }
312
313    proof fn set_prop_properties(self, prop: PageProperty)
314    {
315        admit();
316    }
317
318    proof fn new_properties()
319    {
320        admit();
321    }
322
323}
324
325}
ostd/specs/arch/x86_64/page_table_entry.rs

ostd/specs/arch/x86_64/
page_table_entry.rs
