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    // Expansion for ADDRESS_WIDTH
65    #[verifier::inline]
66    open spec fn ADDRESS_WIDTH_spec() -> usize {
67        48
68    }
69
70    #[inline(always)]
71    fn ADDRESS_WIDTH() -> (res: usize)
72        ensures
73            res == Self::ADDRESS_WIDTH_spec(),
74    {
75        48
76    }
77
78    // Expansion for HIGHEST_TRANSLATION_LEVEL
79    #[verifier::inline]
80    open spec fn HIGHEST_TRANSLATION_LEVEL_spec() -> PagingLevel {
81        2
82    }
83
84    #[inline(always)]
85    fn HIGHEST_TRANSLATION_LEVEL() -> (res: PagingLevel)
86        ensures
87            res == Self::HIGHEST_TRANSLATION_LEVEL_spec(),
88    {
89        2
90    }
91
92    #[verifier::inline]
93    open spec fn VA_SIGN_EXT_spec() -> bool {
94        true
95    }
96
97    #[inline(always)]
98    fn VA_SIGN_EXT() -> bool {
99        true
100    }
101
102    // Expansion for PTE_SIZE
103    #[verifier::inline]
104    open spec fn PTE_SIZE_spec() -> usize {
105        8
106    }
107
108    proof fn lemma_PTE_SIZE_properties()
109        ensures
110            0 < Self::PTE_SIZE_spec() <= Self::BASE_PAGE_SIZE(),
111            is_pow2(Self::PTE_SIZE_spec() as int),
112    {
113        lemma_pow2_is_pow2_to64();
114    }
115
116    #[inline(always)]
117    fn PTE_SIZE() -> (res: usize)
118        ensures
119            res == Self::PTE_SIZE_spec(),
120    {
121        proof {
122            Self::lemma_PTE_SIZE_properties();
123        }
124        8
125    }
126}
127
128} // verus!
ostd/specs/arch/x86_64/paging_consts.rs

ostd/specs/arch/x86_64/
paging_consts.rs
