ostd/specs/arch/x86_64/
page_table_flags.rs

1use vstd::prelude::*;
2
3verus! {
4
5pub struct PageTableFlags {}
6
7#[allow(non_snake_case)]
8impl PageTableFlags {
9    /// Specifies whether the mapped frame or page table is loaded in memory.
10    #[inline(always)]
11    #[vstd::contrib::auto_spec]
12    pub const fn PRESENT() -> (res: usize) {
13        0b00000001usize
14    }
15
16    /// Controls whether writes to the mapped frames are allowed.
17    #[inline(always)]
18    #[vstd::contrib::auto_spec]
19    pub const fn WRITABLE() -> (res: usize) {
20        0b00000010usize
21    }
22
23    /// Controls whether accesses from userspace (i.e. ring 3) are permitted.
24    #[inline(always)]
25    #[vstd::contrib::auto_spec]
26    pub const fn USER() -> (res: usize) {
27        0b00000100usize
28    }
29
30    /// If this bit is set, a “write-through” policy is used for the cache, else a “write-back” policy is used.
31    #[inline(always)]
32    #[vstd::contrib::auto_spec]
33    pub const fn WRITE_THROUGH() -> (res: usize) {
34        0b00001000usize
35    }
36
37    /// Disables caching for the pointed entry if cacheable.
38    #[inline(always)]
39    #[vstd::contrib::auto_spec]
40    pub const fn NO_CACHE() -> (res: usize) {
41        0b00010000usize
42    }
43
44    /// Whether this entry has been used for linear-address translation.
45    #[inline(always)]
46    #[vstd::contrib::auto_spec]
47    pub const fn ACCESSED() -> (res: usize) {
48        0b00100000usize
49    }
50
51    /// Whether the memory area represented by this entry is modified.
52    #[inline(always)]
53    #[vstd::contrib::auto_spec]
54    pub const fn DIRTY() -> (res: usize) {
55        0b01000000usize
56    }
57
58    /// Only in the non-starting and non-ending levels, indication of huge page.
59    #[inline(always)]
60    #[vstd::contrib::auto_spec]
61    pub const fn HUGE() -> (res: usize) {
62        0b10000000usize
63    }
64
65    /// Indicates that the mapping is present in all address spaces, so it isn't flushed from the TLB on an address space switch.
66    #[inline(always)]
67    #[vstd::contrib::auto_spec]
68    pub const fn GLOBAL() -> (res: usize) {
69        0b00000001_00000000usize
70    }
71
72    /// Forbid constute codes on the page. The NXE bits in EFER msr must be set.
73    #[inline(always)]
74    #[vstd::contrib::auto_spec]
75    pub const fn NO_EXECUTE() -> (res: usize) {
76        1usize << 63
77    }
78}
79
80} // verus!
ostd/specs/arch/x86_64/page_table_flags.rs

ostd/specs/arch/x86_64/
page_table_flags.rs
