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

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

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