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
61/// Masks of the physical address.
62pub const PHYS_ADDR_MASK: usize = 0xffff_ffff_ffff_f000;
63
64impl Clone for PageTableEntry {
65    fn clone(&self) -> Self {
66        Self { 0: self.0 }
67    }
68}
69
70#[allow(non_snake_case)]
71impl PageTableEntry {
72
73    #[inline(always)]
74    #[vstd::contrib::auto_spec]
75    pub const fn PROP_MASK() -> (res: usize)
76    {
77        !PHYS_ADDR_MASK & !(PageTableFlags::HUGE())
78    }
79
80    #[verifier::inline]
81    pub open spec fn prop_assign_spec(self, flags: usize) -> Self {
82        Self((self.0 & !Self::PROP_MASK()) | flags as usize)
83    }
84
85    #[inline(always)]
86    pub fn prop_assign(&mut self, flags: usize)
87        ensures self.0 == old(self).prop_assign_spec(flags).0
88    {
89        self.0 = (self.0 & !Self::PROP_MASK()) | flags as usize;
90    }
91
92    #[vstd::contrib::auto_spec]
93    pub fn encode_cache(cache: CachePolicy) -> (res: usize)
94    {
95        match cache {
96            CachePolicy::Uncacheable => PageTableFlags::NO_CACHE(),
97            CachePolicy::Writethrough => PageTableFlags::WRITE_THROUGH(),
98            _ => 0,
99        }
100    }
101
102    pub open spec fn format_flags_spec(prop: PageProperty) -> usize {
103        let flags: u8 = prop.flags.value();
104        let priv_flags: u8 = prop.priv_flags.value();
105        PageTableFlags::PRESENT()
106            | flags.map_forward(&PAGE_FLAG_MAPPING)
107            | flags.map_invert_forward(&PAGE_INVERTED_FLAG_MAPPING)
108            | priv_flags.map_forward(&PAGE_PRIV_MAPPING)
109            | Self::encode_cache(prop.cache)
110    }
111
112    #[verifier::external_body]
113    #[verifier::when_used_as_spec(format_flags_spec)]
114    pub fn format_flags(prop: PageProperty) -> usize
115        returns Self::format_flags_spec(prop)
116    {
117        let flags: u8 = prop.flags.value();
118        let priv_flags: u8 = prop.priv_flags.value();
119        PageTableFlags::PRESENT()
120            | flags.map_forward(&PAGE_FLAG_MAPPING)
121            | flags.map_invert_forward(&PAGE_INVERTED_FLAG_MAPPING)
122            | priv_flags.map_forward(&PAGE_PRIV_MAPPING)
123            | Self::encode_cache(prop.cache)
124    }
125
126    #[vstd::contrib::auto_spec]
127    pub fn format_cache(flags: usize) -> (res: CachePolicy)
128    {
129        if flags & PageTableFlags::NO_CACHE() != 0 {
130            CachePolicy::Uncacheable
131        } else if flags & PageTableFlags::WRITE_THROUGH() != 0 {
132            CachePolicy::Writethrough
133        } else {
134            CachePolicy::Writeback
135        }
136    }
137
138    pub open spec fn format_property_spec(entry: usize) -> PageProperty {
139        let flags: u8 = entry.map_backward(&PAGE_FLAG_MAPPING)
140                      | entry.map_invert_backward(&PAGE_INVERTED_FLAG_MAPPING);
141        let priv_flags: u8 = entry.map_backward(&PAGE_PRIV_MAPPING);
142        let cache = Self::format_cache(entry);
143        PageProperty {
144            flags: PageFlags::from_bits(flags),
145            cache,
146            priv_flags: PrivilegedPageFlags::from_bits(priv_flags),
147        }
148    }
149
150    #[verifier::external_body]
151    #[verifier::when_used_as_spec(format_property_spec)]
152    pub fn format_property(entry: usize) -> PageProperty
153        returns Self::format_property_spec(entry)
154    {
155        let flags = entry.map_backward(&PAGE_FLAG_MAPPING)
156                  | entry.map_invert_backward(&PAGE_INVERTED_FLAG_MAPPING);
157        let priv_flags: u8 = entry.map_backward(&PAGE_PRIV_MAPPING);
158        let cache = Self::format_cache(entry);
159        PageProperty {
160            flags: PageFlags::from_bits(flags),
161            cache,
162            priv_flags: PrivilegedPageFlags::from_bits(priv_flags),
163        }
164    }
165
166    #[inline(always)]
167    #[vstd::contrib::auto_spec]
168    pub fn format_huge_page(level: PagingLevel) -> (res: u64)
169    {
170        if level == 1 {
171            0
172        } else {
173            PageTableFlags::HUGE() as u64
174        }
175    }
176
177}
178
179}
180
181verus! {
182
183impl PageTableEntryTrait for PageTableEntry {
184
185    #[verifier::inline]
186    open spec fn default_spec() -> Self
187    {
188        Self { 0: 0 }
189    }
190
191    #[inline(always)]
192    fn default() -> Self
193        returns Self::default_spec()
194    {
195        Self { 0: 0 }
196    }
197
198    #[verifier::inline]
199    open spec fn new_absent_spec() -> Self {
200        Self::default_spec()
201    }
202
203    #[inline(always)]
204    #[verifier::external_body]
205    fn new_absent() -> (res: Self)
206    {
207        Self::default()
208    }
209
210    #[verifier::inline]
211    open spec fn as_usize_spec(self) -> usize {
212        self.0 as usize
213    }
214
215    #[inline(always)]
216    fn as_usize(self) -> usize
217        returns self.as_usize_spec()
218    {
219        self.0 as usize
220    }
221
222    #[verifier::inline]
223    open spec fn is_present_spec(&self) -> bool {
224        self.0 & PageTableFlags::PRESENT() != 0
225    }
226
227    #[inline(always)]
228    fn is_present(&self) -> bool
229        returns self.is_present_spec()
230    {
231        self.0 & PageTableFlags::PRESENT() != 0
232    }
233
234    open spec fn set_prop_spec(&self, prop: PageProperty) -> Self {
235        let flags = Self::format_flags(prop);
236        self.prop_assign_spec(flags)
237    }
238
239    fn set_prop(&mut self, prop: PageProperty)
240        ensures *self == old(self).set_prop_spec(prop)
241    {
242        let flags = Self::format_flags(prop);
243        self.prop_assign(flags)
244    }
245
246    open spec fn new_page_spec(paddr: Paddr, level: PagingLevel, prop: PageProperty) -> Self {
247        let addr = paddr & PHYS_ADDR_MASK;
248        let hp = Self::format_huge_page(level) as usize;
249        let flags = Self::format_flags(prop) as usize;
250        Self(addr | hp | flags)
251    }
252
253    #[verifier::external_body]
254    fn new_page(paddr: Paddr, level: PagingLevel, prop: PageProperty) -> (res: Self)
255    {
256        let addr = paddr & PHYS_ADDR_MASK;
257        let hp = Self::format_huge_page(level) as usize;
258        let flags = Self::format_flags(prop) as usize;
259        Self(addr | hp | flags)
260    }
261
262    open spec fn new_pt_spec(paddr: Paddr) -> Self {
263        let addr = paddr & PHYS_ADDR_MASK;
264        Self(addr | PageTableFlags::PRESENT() | PageTableFlags::WRITABLE() | PageTableFlags::USER())
265    }
266
267    #[verifier::external_body]
268    fn new_pt(paddr: Paddr) -> (res: Self)
269    {
270        let addr = paddr & PHYS_ADDR_MASK;
271        Self(addr | PageTableFlags::PRESENT() | PageTableFlags::WRITABLE() | PageTableFlags::USER())
272    }
273
274    #[verifier::inline]
275    open spec fn paddr_spec(&self) -> Paddr {
276        self.0 & PHYS_ADDR_MASK
277    }
278
279    #[inline(always)]
280    fn paddr(&self) -> Paddr
281        returns self.paddr_spec()
282    {
283        self.0 & PHYS_ADDR_MASK
284    }
285
286    #[verifier::inline]
287    open spec fn prop_spec(&self) -> PageProperty {
288        Self::format_property(self.0)
289    }
290
291    #[inline(always)]
292    fn prop(&self) -> PageProperty
293        returns self.prop_spec()
294    {
295        Self::format_property(self.0)
296    }
297
298    #[verifier::inline]
299    open spec fn is_last_spec(&self, level: PagingLevel) -> bool {
300        level == 1 || (self.0 & PageTableFlags::HUGE() != 0)
301    }
302
303    #[inline(always)]
304    fn is_last(&self, level: PagingLevel) -> bool
305        returns self.is_last_spec(level)
306    {
307        level == 1 || (self.0 & PageTableFlags::HUGE() != 0)
308    }
309
310    proof fn set_prop_properties(self, prop: PageProperty)
311    {
312        admit();
313    }
314
315    proof fn new_properties()
316    {
317        admit();
318    }
319
320}
321
322impl PageTableEntry {
323    /// Absent (zero) PTE has well-formed paddr for match_pte.
324    pub axiom fn absent_pte_paddr_ok()
325        ensures
326            Self::new_absent_spec().paddr_spec() % crate::specs::arch::mm::PAGE_SIZE == 0,
327            Self::new_absent_spec().paddr_spec() < crate::specs::arch::mm::MAX_PADDR;
328}
329
330}
ostd/specs/arch/x86_64/page_table_entry.rs

ostd/specs/arch/x86_64/
page_table_entry.rs
