ostd/specs/arch/x86_64/
paging_consts.rs

1use vstd::arithmetic::power2::*;
2use vstd::prelude::*;
3
4use vstd_extra::prelude::*;
5
6use crate::mm::*;
7
8use super::*;
9
10verus! {
11
12#[derive(Debug, Default)]
13pub struct PagingConsts {}
14
15impl Clone for PagingConsts {
16    fn clone(&self) -> (res: Self)
17        returns
18            *self,
19    {
20        PagingConsts {  }
21    }
22}
23
24impl PagingConstsTrait for PagingConsts {
25    // Expansion for BASE_PAGE_SIZE
26    #[verifier::inline]
27    open spec fn BASE_PAGE_SIZE_spec() -> usize {
28        4096
29    }
30
31    proof fn lemma_BASE_PAGE_SIZE_properties()
32        ensures
33            0 < Self::BASE_PAGE_SIZE_spec(),
34            is_pow2(Self::BASE_PAGE_SIZE_spec() as int),
35    {
36        lemma_pow2_is_pow2_to64();
37    }
38
39    #[inline(always)]
40    fn BASE_PAGE_SIZE() -> (res: usize)
41        ensures
42            res == Self::BASE_PAGE_SIZE_spec(),
43    {
44        proof {
45            Self::lemma_BASE_PAGE_SIZE_properties();
46        }
47        4096
48    }
49
50    // Expansion for NR_LEVELS
51    #[verifier::inline]
52    open spec fn NR_LEVELS_spec() -> PagingLevel {
53        4
54    }
55
56    #[inline(always)]
57    fn NR_LEVELS() -> (res: PagingLevel)
58        ensures
59            res == Self::NR_LEVELS_spec(),
60    {
61        4
62    }
63
64    proof fn lemma_NR_LEVELS_eq()
65        ensures
66            Self::NR_LEVELS_spec() as int == NR_LEVELS as int,
67    {
68        // Both sides are concretely 4 for x86_64.
69    }
70
71    // Expansion for ADDRESS_WIDTH
72    #[verifier::inline]
73    open spec fn ADDRESS_WIDTH_spec() -> usize {
74        48
75    }
76
77    #[inline(always)]
78    fn ADDRESS_WIDTH() -> (res: usize)
79        ensures
80            res == Self::ADDRESS_WIDTH_spec(),
81    {
82        48
83    }
84
85    // Expansion for HIGHEST_TRANSLATION_LEVEL
86    #[verifier::inline]
87    open spec fn HIGHEST_TRANSLATION_LEVEL_spec() -> PagingLevel {
88        2
89    }
90
91    #[inline(always)]
92    fn HIGHEST_TRANSLATION_LEVEL() -> (res: PagingLevel)
93        ensures
94            res == Self::HIGHEST_TRANSLATION_LEVEL_spec(),
95    {
96        2
97    }
98
99    #[verifier::inline]
100    open spec fn VA_SIGN_EXT_spec() -> bool {
101        true
102    }
103
104    #[inline(always)]
105    fn VA_SIGN_EXT() -> bool {
106        true
107    }
108
109    // Expansion for PTE_SIZE
110    #[verifier::inline]
111    open spec fn PTE_SIZE_spec() -> usize {
112        8
113    }
114
115    proof fn lemma_PTE_SIZE_properties()
116        ensures
117            0 < Self::PTE_SIZE_spec() <= Self::BASE_PAGE_SIZE(),
118            is_pow2(Self::PTE_SIZE_spec() as int),
119    {
120        lemma_pow2_is_pow2_to64();
121    }
122
123    #[inline(always)]
124    fn PTE_SIZE() -> (res: usize)
125        ensures
126            res == Self::PTE_SIZE_spec(),
127    {
128        proof {
129            Self::lemma_PTE_SIZE_properties();
130        }
131        8
132    }
133}
134
135pub proof fn lemma_nr_subpage_per_huge_eq_nr_entries()
136    ensures
137        crate::mm::nr_subpage_per_huge::<PagingConsts>() == NR_ENTRIES,
138{
139    assert(crate::mm::nr_subpage_per_huge::<PagingConsts>() == 4096usize / 8usize);
140    assert(NR_ENTRIES == 512usize);
141}
142
143} // verus!
ostd/specs/arch/x86_64/paging_consts.rs

ostd/specs/arch/x86_64/
paging_consts.rs
