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

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

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