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::{KERNEL_VADDR_RANGE, 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
134pub proof 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(level) / PAGE_SIZE) * PAGE_SIZE == page_size(level)` for level in [1, NR_LEVELS+1].
150/// page_size(level) is divisible by PAGE_SIZE so the integer division is exact.
151pub proof fn lemma_page_size_div_mul_eq(level: PagingLevel)
152    requires
153        1 <= level <= NR_LEVELS + 1,
154    ensures
155        (page_size_spec(level) / PAGE_SIZE) * PAGE_SIZE == page_size_spec(level),
156{
157    lemma_page_size_spec_values();
158}
159
160/// `NR_ENTRIES * page_size(level - 1) == page_size(level)` for level in [2, NR_LEVELS + 1].
161/// A huge page at `level` consists of NR_ENTRIES sub-pages each of size `page_size(level - 1)`.
162pub proof fn lemma_nr_entries_times_sub_page_size(level: PagingLevel)
163    requires
164        2 <= level <= NR_LEVELS + 1,
165    ensures
166        crate::specs::arch::mm::NR_ENTRIES as int * page_size_spec((level - 1) as PagingLevel) as int
167            == page_size_spec(level) as int,
168{
169    lemma_page_size_spec_values();
170    crate::specs::arch::paging_consts::lemma_nr_subpage_per_huge_eq_nr_entries();
171}
172
173/// Used by `Entry::split_if_mapped_huge` to instantiate the 4KB sub-page
174/// forall invariant at the `i`-th sub-frame's slot.
175///
176/// For a huge frame at paddr `pa` with level `level > 1`, the `i`-th sub-frame
177/// lives at `small_pa = pa + i * page_size(level - 1)`. In units of 4KB sub-pages
178/// that's `big_j = i * (page_size(level - 1) / PAGE_SIZE)`. This lemma discharges
179/// the arithmetic facts needed at the call site:
180///   * `0 < big_j < page_size(level) / PAGE_SIZE` so the sub-page forall
181///     (quantified over `j ∈ (0, page_size(level) / PAGE_SIZE)`) fires.
182///   * `small_pa == pa + big_j * PAGE_SIZE` so the forall trigger matches.
183pub proof fn lemma_split_sub_page_big_j(
184    pa: Paddr,
185    level: PagingLevel,
186    i: usize,
187) -> (big_j: usize)
188    requires
189        2 <= level <= NR_LEVELS,
190        0 < i < crate::specs::arch::mm::NR_ENTRIES,
191    ensures
192        0 < big_j < page_size_spec(level) / PAGE_SIZE,
193        (pa + i * page_size_spec((level - 1) as PagingLevel)) as int
194            == pa as int + big_j as int * PAGE_SIZE as int,
195        big_j as int == i as int * (page_size_spec((level - 1) as PagingLevel) / PAGE_SIZE) as int,
196{
197    let sub_pages_per_entry: int =
198        (page_size_spec((level - 1) as PagingLevel) / PAGE_SIZE) as int;
199    let big_j_int: int = i as int * sub_pages_per_entry;
200    lemma_page_size_spec_values();
201    lemma_page_size_div_mul_eq((level - 1) as PagingLevel);
202    lemma_page_size_div_mul_eq(level);
203    lemma_nr_entries_times_sub_page_size(level);
204    vstd::arithmetic::mul::lemma_mul_strictly_positive(
205        i as int, sub_pages_per_entry);
206    vstd::arithmetic::mul::lemma_mul_strict_inequality(
207        i as int, crate::specs::arch::mm::NR_ENTRIES as int, sub_pages_per_entry);
208    vstd::arithmetic::mul::lemma_mul_is_associative(
209        crate::specs::arch::mm::NR_ENTRIES as int, sub_pages_per_entry, PAGE_SIZE as int);
210    vstd::arithmetic::div_mod::lemma_div_by_multiple(
211        crate::specs::arch::mm::NR_ENTRIES as int * sub_pages_per_entry, PAGE_SIZE as int);
212    vstd::arithmetic::mul::lemma_mul_is_associative(
213        i as int, sub_pages_per_entry, PAGE_SIZE as int);
214    big_j_int as usize
215}
216
217/// page_size(l2) is divisible by page_size(l1) when l1 <= l2.
218/// This holds because page_size(l) = PAGE_SIZE * 512^(l-1), so
219/// page_size(l2) / page_size(l1) = 512^(l2-l1), which is a positive integer.
220pub proof fn lemma_page_size_divides(l1: PagingLevel, l2: PagingLevel)
221    requires
222        1 <= l1 <= l2 <= NR_LEVELS + 1,
223    ensures
224        page_size_spec(l2) % page_size_spec(l1) == 0,
225{
226    lemma_page_size_spec_values();
227}
228
229/// For any valid physical address `pa < MAX_PADDR` and page level, pa + page_size(level)
230/// does not overflow usize. This holds because MAX_PADDR = 2^31 and page sizes are at
231/// most 2^39 (NR_LEVELS = 4), so pa + size < 2^40 << usize::MAX = 2^64.
232pub proof fn lemma_pa_plus_page_size_no_overflow(pa: Paddr, level: PagingLevel)
233    requires
234        1 <= level <= NR_LEVELS,
235        pa < MAX_PADDR,
236    ensures
237        pa + page_size(level) < usize::MAX,
238{
239    lemma_page_size_spec_values();
240}
241
242/// For any VA within the kernel virtual address range and any page level,
243/// va + page_size(level) does not overflow usize.
244/// KERNEL_VADDR_RANGE.end = 0xffff_ffff_ffff_0000 and max page_size (level 4) = 512GB = 0x80_0000_0000.
245/// The sum is at most 0x1_0000_7fff_ffff_0000 which overflows 64-bit usize.
246/// However, at the levels actually used (1-3), page_size <= 1GB = 0x4000_0000, and
247/// 0xffff_ffff_ffff_0000 + 0x4000_0000 = 0x1_0000_0000_3fff_0000 — still overflows.
248/// So this lemma requires va + page_size(level) <= barrier_va.end <= KERNEL_VADDR_RANGE.end,
249/// which is guaranteed by !map_panic_conditions / !find_next_panic_condition.
250pub proof fn lemma_va_plus_page_size_no_overflow(
251    va: Vaddr,
252    len: usize,
253)
254    requires
255        va + len <= KERNEL_VADDR_RANGE.end,
256    ensures
257        va + len <= usize::MAX,
258{
259    assert(KERNEL_VADDR_RANGE.end == 0xffff_ffff_ffff_0000usize) by (compute_only);
260    assert(va + len <= 0xffff_ffff_ffff_0000usize);
261}
262
263/// The number of base pages in the address space fits in usize.
264/// max pages = MAX_PADDR / PAGE_SIZE = 0x8000_0000 / 0x1000 = 0x8_0000 = 524288.
265pub proof fn lemma_max_mappings_fit_usize()
266    ensures
267        MAX_PADDR / PAGE_SIZE < usize::MAX,
268{
269    assert(MAX_PADDR / PAGE_SIZE < usize::MAX) by (compute_only);
270}
271
272} // verus!
ostd/specs/mm/page_table/cursor/page_size_lemmas.rs

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