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().bits(), PageTableFlags::PRESENT()),
23        (PageFlags::W().bits(), PageTableFlags::WRITABLE()),
24        (PageFlags::ACCESSED().bits(), PageTableFlags::ACCESSED()),
25        (PageFlags::DIRTY().bits(), 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().bits(), PageTableFlags::USER()),
37        (
38            PrivilegedPageFlags::GLOBAL().bits(),
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().bits(), 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
61unsafe impl crate::Pod for PageTableEntry {}
62
63impl crate::mm::io::PodOnce for PageTableEntry {}
64
65/// Masks of the physical address.
66pub const PHYS_ADDR_MASK: usize = 0xffff_ffff_ffff_f000;
67
68impl Clone for PageTableEntry {
69    fn clone(&self) -> Self {
70        Self { 0: self.0 }
71    }
72}
73
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 final(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.bits();
107        let priv_flags: u8 = prop.priv_flags.bits();
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) -> usize
118        returns Self::format_flags_spec(prop)
119    {
120        let flags: u8 = prop.flags.bits();
121        let priv_flags: u8 = prop.priv_flags.bits();
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).unwrap(),
148            cache,
149            priv_flags: PrivilegedPageFlags::from_bits(priv_flags).unwrap(),
150        }
151    }
152
153    #[verifier::external_body]
154    #[verifier::when_used_as_spec(format_property_spec)]
155    pub fn format_property(entry: usize) -> PageProperty
156        returns 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).unwrap(),
164            cache,
165            priv_flags: PrivilegedPageFlags::from_bits(priv_flags).unwrap(),
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() -> Self
196        returns 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) -> usize
220        returns 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) -> bool
232        returns 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 *final(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) -> Paddr
284        returns 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) -> PageProperty
296        returns 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) -> bool
308        returns 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    proof fn axiom_present_paddr_aligned(&self)
324    {
325        admit();
326    }
327
328}
329
330impl PageTableEntry {
331    /// Absent (zero) PTE has well-formed paddr for match_pte.
332    pub axiom fn absent_pte_paddr_ok()
333        ensures
334            Self::new_absent_spec().paddr_spec() % crate::specs::arch::mm::PAGE_SIZE == 0,
335            Self::new_absent_spec().paddr_spec() < crate::specs::arch::mm::MAX_PADDR;
336}
337
338}
ostd/specs/arch/x86_64/page_table_entry.rs

ostd/specs/arch/x86_64/
page_table_entry.rs
