ostd/specs/arch/x86_64/
page_table_flags.rs

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

ostd/specs/arch/x86_64/
page_table_flags.rs
