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

1use vstd::arithmetic::power2::pow2;
2use vstd::prelude::*;
3
4use crate::mm::PagingLevel;
5use crate::mm::page_table::{page_size, page_size_spec};
6use crate::mm::{MAX_PADDR, Paddr, Vaddr, nr_subpage_per_huge};
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
25    vstd::arithmetic::power::lemma_pow0(2int);
26}
27
28// ─── VA alignment ────────────────────────────────────────────────────────────
29/// When `va` is aligned to `page_size(large_level)` and `level <= large_level` (so
30/// page_size(level) divides page_size(large_level)), then `va` is aligned to page_size(level).
31/// Note: page_size(level) for level >= 1 is always a multiple of PAGE_SIZE.
32pub proof fn lemma_va_align_page_size(va: Vaddr, level: PagingLevel)
33    requires
34        1 <= level <= NR_LEVELS + 1,
35        va % PAGE_SIZE == 0,
36        exists|large_level: PagingLevel|
37            1 <= large_level <= NR_LEVELS + 1 && level <= large_level && va % page_size_spec(
38                large_level,
39            ) == 0,
40    ensures
41        va % page_size_spec(level) == 0,
42{
43    let large_level: PagingLevel = choose|l: PagingLevel|
44        1 <= l <= NR_LEVELS + 1 && level <= l && va % page_size_spec(l) == 0;
45    if level == 1nat {
46        lemma_page_size_spec_level1();
47    } else {
48        let ps_l = page_size_spec(level) as int;
49        let ps_ll = page_size_spec(large_level) as int;
50        lemma_page_size_ge_page_size(level);
51        lemma_page_size_ge_page_size(large_level);
52        lemma_page_size_divides(level, large_level);
53        assert(ps_ll >= ps_l) by {
54            if ps_ll < ps_l {
55                vstd::arithmetic::div_mod::lemma_small_mod(ps_ll as nat, ps_l as nat);
56            }
57        };
58        let k = ps_ll / ps_l;
59        vstd::arithmetic::div_mod::lemma_div_non_zero(ps_ll, ps_l);
60        vstd::arithmetic::div_mod::lemma_fundamental_div_mod(ps_ll, ps_l);
61        vstd::arithmetic::div_mod::lemma_mod_mod(va as int, ps_l, k);
62        assert(va as int % ps_l == 0);
63    }
64}
65
66/// Special case for level 1: page_size_spec(1) == PAGE_SIZE, so va % PAGE_SIZE == 0 implies
67/// va % page_size_spec(1) == 0.
68pub proof fn lemma_va_align_page_size_level_1(va: Vaddr)
69    requires
70        va % PAGE_SIZE == 0,
71    ensures
72        va % page_size_spec(1) == 0,
73{
74    lemma_page_size_spec_level1();
75}
76
77/// For any level in [1, NR_LEVELS], page_size(level) is a multiple of PAGE_SIZE.
78pub proof fn lemma_page_size_multiple_of_page_size(level: PagingLevel)
79    requires
80        1 <= level <= NR_LEVELS,
81    ensures
82        page_size_spec(level) % PAGE_SIZE == 0,
83{
84    lemma_page_size_spec_values();
85}
86
87/// For any level in [1, NR_LEVELS+1], the page size is at least PAGE_SIZE.
88/// This follows from page_size(level) = PAGE_SIZE * pow2((ilog2 * (level-1)) as nat)
89/// with pow2(k) >= 1 for all k >= 0.
90#[verifier::spinoff_prover]
91pub proof fn lemma_page_size_ge_page_size(level: PagingLevel)
92    requires
93        1 <= level <= NR_LEVELS + 1,
94    ensures
95        page_size(level) >= PAGE_SIZE,
96{
97    lemma_page_size_spec_values();
98}
99
100/// `page_size` is monotone in the level: a higher level has a larger or equal page size.
101/// This follows from page_size(level) = PAGE_SIZE * 512^(level-1); incrementing level multiplies
102/// by 512, so page_size(l+1) = 512 * page_size(l) > page_size(l).
103pub proof fn lemma_page_size_monotone(l1: PagingLevel, l2: PagingLevel)
104    requires
105        1 <= l1 <= NR_LEVELS + 1,
106        1 <= l2 <= NR_LEVELS + 1,
107        l1 <= l2,
108    ensures
109        page_size(l1) <= page_size(l2),
110{
111    if l1 != l2 {
112        let ps1 = page_size(l1);
113        let ps2 = page_size(l2);
114
115        lemma_page_size_ge_page_size(l1);
116        lemma_page_size_ge_page_size(l2);
117        lemma_page_size_divides(l1, l2);
118
119        assert(ps1 <= ps2) by {
120            if ps2 < ps1 {
121                vstd::arithmetic::div_mod::lemma_small_mod(ps2 as nat, ps1 as nat);
122            }
123        };
124    }
125}
126
127pub proof fn lemma_page_size_spec_values()
128    ensures
129        page_size_spec(1) == 4096,
130        page_size_spec(2) == 2097152,
131        page_size_spec(3) == 1073741824,
132        page_size_spec(4) == 549755813888,
133        page_size_spec(5) == 281474976710656,
134{
135    lemma_page_size_spec_level1();
136    vstd_extra::external::ilog2::lemma_usize_ilog2_to32();
137    vstd::arithmetic::power2::lemma2_to64();
138    vstd::arithmetic::power2::lemma2_to64_rest();
139    vstd::bits::lemma_usize_pow2_no_overflow(48);
140}
141
142/// `(page_size(level) / PAGE_SIZE) * PAGE_SIZE == page_size(level)` for level in [1, NR_LEVELS+1].
143/// page_size(level) is divisible by PAGE_SIZE so the integer division is exact.
144pub proof fn lemma_page_size_div_mul_eq(level: PagingLevel)
145    requires
146        1 <= level <= NR_LEVELS + 1,
147    ensures
148        (page_size_spec(level) / PAGE_SIZE) * PAGE_SIZE == page_size_spec(level),
149{
150    lemma_page_size_spec_values();
151}
152
153/// `NR_ENTRIES * page_size(level - 1) == page_size(level)` for level in [2, NR_LEVELS + 1].
154/// A huge page at `level` consists of NR_ENTRIES sub-pages each of size `page_size(level - 1)`.
155pub proof fn lemma_nr_entries_times_sub_page_size(level: PagingLevel)
156    requires
157        2 <= level <= NR_LEVELS + 1,
158    ensures
159        crate::specs::arch::mm::NR_ENTRIES as int * page_size_spec(
160            (level - 1) as PagingLevel,
161        ) as int == page_size_spec(level) as int,
162{
163    lemma_page_size_spec_values();
164    crate::specs::arch::paging_consts::lemma_nr_subpage_per_huge_eq_nr_entries();
165}
166
167/// Used by `Entry::split_if_mapped_huge` to instantiate the 4KB sub-page
168/// forall invariant at the `i`-th sub-frame's slot.
169///
170/// For a huge frame at paddr `pa` with level `level > 1`, the `i`-th sub-frame
171/// lives at `small_pa = pa + i * page_size(level - 1)`. In units of 4KB sub-pages
172/// that's `big_j = i * (page_size(level - 1) / PAGE_SIZE)`. This lemma discharges
173/// the arithmetic facts needed at the call site:
174///   * `0 < big_j < page_size(level) / PAGE_SIZE` so the sub-page forall
175///     (quantified over `j ∈ (0, page_size(level) / PAGE_SIZE)`) fires.
176///   * `small_pa == pa + big_j * PAGE_SIZE` so the forall trigger matches.
177pub proof fn lemma_split_sub_page_big_j(pa: Paddr, level: PagingLevel, i: usize) -> (big_j: usize)
178    requires
179        2 <= level <= NR_LEVELS,
180        0 < i < crate::specs::arch::mm::NR_ENTRIES,
181    ensures
182        0 < big_j < page_size_spec(level) / PAGE_SIZE,
183        (pa + i * page_size_spec((level - 1) as PagingLevel)) as int == pa as int + big_j as int
184            * PAGE_SIZE as int,
185        big_j as int == i as int * (page_size_spec((level - 1) as PagingLevel) / PAGE_SIZE) as int,
186{
187    let sub_pages_per_entry: int = (page_size_spec((level - 1) as PagingLevel) / PAGE_SIZE) as int;
188    let big_j_int: int = i as int * sub_pages_per_entry;
189    lemma_page_size_spec_values();
190    lemma_page_size_div_mul_eq((level - 1) as PagingLevel);
191    lemma_page_size_div_mul_eq(level);
192    lemma_nr_entries_times_sub_page_size(level);
193    vstd::arithmetic::mul::lemma_mul_strictly_positive(i as int, sub_pages_per_entry);
194    vstd::arithmetic::mul::lemma_mul_strict_inequality(
195        i as int,
196        crate::specs::arch::mm::NR_ENTRIES as int,
197        sub_pages_per_entry,
198    );
199    vstd::arithmetic::mul::lemma_mul_is_associative(
200        crate::specs::arch::mm::NR_ENTRIES as int,
201        sub_pages_per_entry,
202        PAGE_SIZE as int,
203    );
204    vstd::arithmetic::div_mod::lemma_div_by_multiple(
205        crate::specs::arch::mm::NR_ENTRIES as int * sub_pages_per_entry,
206        PAGE_SIZE as int,
207    );
208    vstd::arithmetic::mul::lemma_mul_is_associative(
209        i as int,
210        sub_pages_per_entry,
211        PAGE_SIZE as int,
212    );
213    big_j_int as usize
214}
215
216/// page_size(l2) is divisible by page_size(l1) when l1 <= l2.
217/// This holds because page_size(l) = PAGE_SIZE * 512^(l-1), so
218/// page_size(l2) / page_size(l1) = 512^(l2-l1), which is a positive integer.
219pub proof fn lemma_page_size_divides(l1: PagingLevel, l2: PagingLevel)
220    requires
221        1 <= l1 <= l2 <= NR_LEVELS + 1,
222    ensures
223        page_size_spec(l2) % page_size_spec(l1) == 0,
224{
225    lemma_page_size_spec_values();
226    // Enumerate pairs to keep SMT context narrow.
227    if l1 == 1 {
228    } else if l1 == 2 {
229    } else if l1 == 3 {
230    } else if l1 == 4 {
231    } else {
232        assert(l1 == 5);
233    }
234}
235
236/// For any valid physical address `pa < MAX_PADDR` and page level, pa + page_size(level)
237/// does not overflow usize. This holds because MAX_PADDR = 2^31 and page sizes are at
238/// most 2^39 (NR_LEVELS = 4), so pa + size < 2^40 << usize::MAX = 2^64.
239pub proof fn lemma_pa_plus_page_size_no_overflow(pa: Paddr, level: PagingLevel)
240    requires
241        1 <= level <= NR_LEVELS,
242        pa < MAX_PADDR,
243    ensures
244        pa + page_size(level) < usize::MAX,
245{
246    lemma_page_size_spec_values();
247}
248
249/// For any VA within the kernel virtual address range and any page level,
250/// va + page_size(level) does not overflow usize.
251/// KERNEL_VADDR_RANGE.end = 0xffff_ffff_ffff_0000 and max page_size (level 4) = 512GB = 0x80_0000_0000.
252/// The sum is at most 0x1_0000_7fff_ffff_0000 which overflows 64-bit usize.
253/// However, at the levels actually used (1-3), page_size <= 1GB = 0x4000_0000, and
254/// 0xffff_ffff_ffff_0000 + 0x4000_0000 = 0x1_0000_0000_3fff_0000 — still overflows.
255/// So this lemma requires va + page_size(level) <= barrier_va.end <= KERNEL_VADDR_RANGE.end,
256/// which is guaranteed by !map_panic_conditions / !find_next_panic_condition.
257pub proof fn lemma_va_plus_page_size_no_overflow(va: Vaddr, len: usize)
258    requires
259        va + len <= KERNEL_VADDR_RANGE.end,
260    ensures
261        va + len <= usize::MAX,
262{
263    assert(KERNEL_VADDR_RANGE.end == 0xffff_ffff_ffff_0000usize) by (compute_only);
264    assert(va + len <= 0xffff_ffff_ffff_0000usize);
265}
266
267/// The number of base pages in the address space fits in usize.
268/// max pages = MAX_PADDR / PAGE_SIZE = 0x8000_0000 / 0x1000 = 0x8_0000 = 524288.
269pub proof fn lemma_max_mappings_fit_usize()
270    ensures
271        MAX_PADDR / PAGE_SIZE < usize::MAX,
272{
273    assert(MAX_PADDR / PAGE_SIZE < usize::MAX) by (compute_only);
274}
275
276} // verus!
ostd/specs/mm/page_table/cursor/page_size_lemmas.rs

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