ostd/specs/mm/page_table/cursor/
page_size_lemmas.rs

1use vstd::arithmetic::power2::pow2;
2use vstd::prelude::*;
3
4use crate::mm::page_table::{page_size, page_size_spec};
5use crate::mm::PagingLevel;
6use crate::mm::{nr_subpage_per_huge, Paddr, Vaddr, MAX_PADDR};
7use crate::specs::arch::mm::{NR_LEVELS, PAGE_SIZE};
8use crate::specs::arch::paging_consts::PagingConsts;
9
10verus! {
11
12// ─── page_size_spec(1) ──────────────────────────────────────────────────────
13/// page_size_spec(1) == PAGE_SIZE.
14/// Both sides equal PAGE_SIZE * pow2(0) = PAGE_SIZE * 1 = PAGE_SIZE,
15/// because the exponent ilog2 * (1 - 1) = ilog2 * 0 = 0.
16pub proof fn lemma_page_size_spec_level1()
17    ensures
18        page_size_spec(1) == PAGE_SIZE,
19{
20    vstd::arithmetic::mul::lemma_mul_by_zero_is_zero(
21        nr_subpage_per_huge::<PagingConsts>().ilog2() as int,
22    );
23    broadcast use vstd::arithmetic::power2::lemma_pow2;
24    vstd::arithmetic::power::lemma_pow0(2int);
25}
26
27// ─── VA alignment ────────────────────────────────────────────────────────────
28/// When `va` is aligned to `page_size(large_level)` and `level <= large_level` (so
29/// page_size(level) divides page_size(large_level)), then `va` is aligned to page_size(level).
30/// Note: page_size(level) for level >= 1 is always a multiple of PAGE_SIZE.
31pub proof fn lemma_va_align_page_size(va: Vaddr, level: PagingLevel)
32    requires
33        1 <= level <= NR_LEVELS + 1,
34        va % PAGE_SIZE == 0,
35        exists|large_level: PagingLevel|
36            1 <= large_level <= NR_LEVELS + 1 && level <= large_level && va % page_size_spec(
37                large_level,
38            ) == 0,
39    ensures
40        va % page_size_spec(level) == 0,
41{
42    let large_level: PagingLevel = choose|l: PagingLevel|
43        1 <= l <= NR_LEVELS + 1 && level <= l && va % page_size_spec(l) == 0;
44    if level == 1nat {
45        lemma_page_size_spec_level1();
46    } else {
47        let ps_l = page_size_spec(level) as int;
48        let ps_ll = page_size_spec(large_level) as int;
49        lemma_page_size_ge_page_size(level);
50        lemma_page_size_ge_page_size(large_level);
51        lemma_page_size_divides(level, large_level);
52        assert(ps_ll >= ps_l) by {
53            if ps_ll < ps_l {
54                vstd::arithmetic::div_mod::lemma_small_mod(ps_ll as nat, ps_l as nat);
55            }
56        };
57        let k = ps_ll / ps_l;
58        vstd::arithmetic::div_mod::lemma_div_non_zero(ps_ll, ps_l);
59        vstd::arithmetic::div_mod::lemma_fundamental_div_mod(ps_ll, ps_l);
60        vstd::arithmetic::div_mod::lemma_mod_mod(va as int, ps_l, k);
61        assert(va as int % ps_l == 0);
62    }
63}
64
65/// Special case for level 1: page_size_spec(1) == PAGE_SIZE, so va % PAGE_SIZE == 0 implies
66/// va % page_size_spec(1) == 0.
67pub proof fn lemma_va_align_page_size_level_1(va: Vaddr)
68    requires
69        va % PAGE_SIZE == 0,
70    ensures
71        va % page_size_spec(1) == 0,
72{
73    lemma_page_size_spec_level1();
74}
75
76/// For any level in [1, NR_LEVELS], page_size(level) is a multiple of PAGE_SIZE.
77pub proof fn lemma_page_size_multiple_of_page_size(level: PagingLevel)
78    requires
79        1 <= level <= NR_LEVELS,
80    ensures
81        page_size_spec(level) % PAGE_SIZE == 0,
82{
83    lemma_page_size_spec_values();
84}
85
86/// For any level in [1, NR_LEVELS+1], the page size is at least PAGE_SIZE.
87/// This follows from page_size(level) = PAGE_SIZE * pow2((ilog2 * (level-1)) as nat)
88/// with pow2(k) >= 1 for all k >= 0.
89pub proof fn lemma_page_size_ge_page_size(level: PagingLevel)
90    requires
91        1 <= level <= NR_LEVELS + 1,
92    ensures
93        page_size(level) >= PAGE_SIZE,
94{
95    lemma_page_size_spec_values();
96    // FIXME: why the following empty if-else is needed to make the proof go through?
97    // It seems that the proof fails without it, even though the lemma_page_size_spec_values()
98    // should already give us the needed information about page_size_spec(level).
99    if level == 1 {
100    } else if level == 2 {
101    } else if level == 3 {
102    } else if level == 4 {
103    } else {
104    }
105}
106
107/// `page_size` is monotone in the level: a higher level has a larger or equal page size.
108/// This follows from page_size(level) = PAGE_SIZE * 512^(level-1); incrementing level multiplies
109/// by 512, so page_size(l+1) = 512 * page_size(l) > page_size(l).
110pub proof fn lemma_page_size_monotone(l1: PagingLevel, l2: PagingLevel)
111    requires
112        1 <= l1 <= NR_LEVELS + 1,
113        1 <= l2 <= NR_LEVELS + 1,
114        l1 <= l2,
115    ensures
116        page_size(l1) <= page_size(l2),
117{
118    if l1 != l2 {
119        let ps1 = page_size(l1);
120        let ps2 = page_size(l2);
121
122        lemma_page_size_ge_page_size(l1);
123        lemma_page_size_ge_page_size(l2);
124        lemma_page_size_divides(l1, l2);
125
126        assert(ps1 <= ps2) by {
127            if ps2 < ps1 {
128                vstd::arithmetic::div_mod::lemma_small_mod(ps2 as nat, ps1 as nat);
129            }
130        };
131    }
132}
133
134proof fn lemma_page_size_spec_values()
135    ensures
136        page_size_spec(1) == 4096,
137        page_size_spec(2) == 2097152,
138        page_size_spec(3) == 1073741824,
139        page_size_spec(4) == 549755813888,
140        page_size_spec(5) == 281474976710656,
141{
142    lemma_page_size_spec_level1();
143    vstd_extra::external::ilog2::lemma_usize_ilog2_to32();
144    vstd::arithmetic::power2::lemma2_to64();
145    vstd::arithmetic::power2::lemma2_to64_rest();
146    vstd::bits::lemma_usize_pow2_no_overflow(48);
147}
148
149/// page_size(l2) is divisible by page_size(l1) when l1 <= l2.
150/// This holds because page_size(l) = PAGE_SIZE * 512^(l-1), so
151/// page_size(l2) / page_size(l1) = 512^(l2-l1), which is a positive integer.
152pub proof fn lemma_page_size_divides(l1: PagingLevel, l2: PagingLevel)
153    requires
154        1 <= l1 <= l2 <= NR_LEVELS + 1,
155    ensures
156        page_size_spec(l2) % page_size_spec(l1) == 0,
157{
158    lemma_page_size_spec_values();
159}
160
161/// For any valid physical address `pa < MAX_PADDR` and page level, pa + page_size(level)
162/// does not overflow usize. This holds because MAX_PADDR = 2^31 and page sizes are at
163/// most 2^39 (NR_LEVELS = 4), so pa + size < 2^40 << usize::MAX = 2^64.
164pub proof fn lemma_pa_plus_page_size_no_overflow(pa: Paddr, level: PagingLevel)
165    requires
166        1 <= level <= NR_LEVELS,
167        pa < MAX_PADDR,
168    ensures
169        pa + page_size(level) < usize::MAX,
170{
171    lemma_page_size_spec_values();
172}
173
174} // verus!
ostd/specs/mm/page_table/cursor/page_size_lemmas.rs

ostd/specs/mm/page_table/cursor/
page_size_lemmas.rs
