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

1use vstd::{
2    arithmetic::{
3        div_mod::lemma_fundamental_div_mod,
4        mul::{lemma_mul_inequality, lemma_mul_is_distributive_sub},
5        power2::{lemma_pow2_adds, lemma_pow2_pos, pow2},
6    },
7    bits::lemma_usize_pow2_no_overflow,
8    prelude::*,
9};
10use vstd_extra::{external::ilog2::lemma_usize_is_pow2_is_ilog2_pow2, prelude::*};
11
12use crate::specs::arch::*;
13use crate::specs::mm::page_table::{nr_pte_index_bits_spec, pte_index_bit_offset_spec};
14
15use crate::arch::mm::PagingConsts;
16use crate::mm::{
17    KERNEL_VADDR_RANGE, Paddr, PagingConstsTrait, PagingLevel, Vaddr, nr_subpage_per_huge,
18    page_size,
19};
20
21verus! {
22
23/// A page size is the power of two at that level's `pte_index_bit_offset_spec`.
24pub proof fn lemma_page_size_is_pow2_pte_index_bit_offset<C: PagingConstsTrait>(level: PagingLevel)
25    requires
26        1 <= level <= C::NR_LEVELS() + 1,
27    ensures
28        pte_index_bit_offset_spec::<C>(level) < usize::BITS,
29        pte_index_bit_offset_spec::<C>(level) == C::BASE_PAGE_SIZE().ilog2()
30            + nr_pte_index_bits_spec::<C>() * (level - 1),
31        0 < page_size::<C>(level) == pow2(pte_index_bit_offset_spec::<C>(level) as nat),
32{
33    C::lemma_paging_consts_properties();
34    let bits = nr_pte_index_bits_spec::<C>();
35    lemma_usize_is_pow2_is_ilog2_pow2(C::BASE_PAGE_SIZE());
36    lemma_usize_is_pow2_is_ilog2_pow2(nr_subpage_per_huge::<C>());
37    lemma_mul_inequality(level - 1, C::NR_LEVELS() as int, bits as int);
38    lemma_pow2_adds(C::BASE_PAGE_SIZE().ilog2() as nat, (bits * (level - 1)) as nat);
39    lemma_usize_pow2_no_overflow(pte_index_bit_offset_spec::<C>(level) as nat);
40}
41
42/// Two levels that differ by `n` differ in offset by `n` index widths, which
43/// multiplies the page size by the matching power of two.
44pub proof fn lemma_page_size_ratio<C: PagingConstsTrait>(small: PagingLevel, large: PagingLevel)
45    requires
46        1 <= small <= large <= C::NR_LEVELS() + 1,
47    ensures
48        pte_index_bit_offset_spec::<C>(large) == pte_index_bit_offset_spec::<C>(small)
49            + nr_pte_index_bits_spec::<C>() * (large - small),
50        page_size::<C>(large) == page_size::<C>(small) * pow2(
51            (nr_pte_index_bits_spec::<C>() * (large - small)) as nat,
52        ),
53{
54    C::lemma_paging_consts_properties();
55    lemma_page_size_is_pow2_pte_index_bit_offset::<C>(small);
56    lemma_page_size_is_pow2_pte_index_bit_offset::<C>(large);
57    let bits = nr_pte_index_bits_spec::<C>();
58    let delta = (bits * (large - small)) as nat;
59    lemma_mul_is_distributive_sub(bits as int, large as int, small as int);
60    lemma_mul_is_distributive_sub(bits as int, large as int, 1);
61    lemma_mul_is_distributive_sub(bits as int, small as int, 1);
62    lemma_pow2_adds(pte_index_bit_offset_spec::<C>(small) as nat, delta);
63    lemma_pow2_pos(delta);
64}
65
66/// A parent page contains `nr_subpage_per_huge` of pages at the next level.
67pub proof fn lemma_page_size_next<C: PagingConstsTrait>(level: PagingLevel)
68    requires
69        1 <= level <= C::NR_LEVELS(),
70    ensures
71        page_size::<C>((level + 1) as PagingLevel) == page_size::<C>(level) * nr_subpage_per_huge::<
72            C,
73        >(),
74        0 < page_size::<C>(level) <= page_size::<C>((level + 1) as PagingLevel),
75{
76    C::lemma_paging_consts_properties();
77    lemma_page_size_is_pow2_pte_index_bit_offset::<C>(level);
78    lemma_page_size_is_pow2_pte_index_bit_offset::<C>((level + 1) as PagingLevel);
79    let bits = nr_pte_index_bits_spec::<C>();
80    lemma_usize_is_pow2_is_ilog2_pow2(nr_subpage_per_huge::<C>());
81    lemma_mul_is_distributive_sub(bits as int, level as int, 1);
82    lemma_pow2_adds(pte_index_bit_offset_spec::<C>(level) as nat, bits as nat);
83    vstd::arithmetic::mul::lemma_mul_left_inequality(
84        page_size::<C>(level) as int,
85        1,
86        nr_subpage_per_huge::<C>() as int,
87    );
88    vstd::arithmetic::mul::lemma_mul_basics(page_size::<C>(level) as int);
89}
90
91/// High-level page size divides the sizes of low-level pages.
92pub proof fn lemma_page_size_divides<C: PagingConstsTrait>(small: PagingLevel, large: PagingLevel)
93    requires
94        1 <= small <= large <= C::NR_LEVELS() + 1,
95    ensures
96        0 < page_size::<C>(small) <= page_size::<C>(large),
97        page_size::<C>(large) % page_size::<C>(small) == 0,
98{
99    C::lemma_paging_consts_properties();
100    lemma_page_size_is_pow2_pte_index_bit_offset::<C>(small);
101    lemma_page_size_is_pow2_pte_index_bit_offset::<C>(large);
102    lemma_page_size_ratio::<C>(small, large);
103    let delta = (nr_pte_index_bits_spec::<C>() * (large - small)) as nat;
104    lemma_pow2_pos(delta);
105    let a = page_size::<C>(small) as int;
106    let ratio = pow2(delta) as int;
107    vstd::arithmetic::div_mod::lemma_mod_multiples_basic(ratio, a);
108    vstd::arithmetic::mul::lemma_mul_is_commutative(a, ratio);
109    vstd::arithmetic::mul::lemma_mul_left_inequality(a, 1, ratio);
110    vstd::arithmetic::mul::lemma_mul_basics(a);
111}
112
113/// `page_size(1)` is `BASE_PAGE_SIZE`.
114pub proof fn lemma_page_size_base<C: PagingConstsTrait>()
115    ensures
116        page_size::<C>(1) == C::BASE_PAGE_SIZE(),
117{
118    reveal(vstd::arithmetic::power::pow);
119    vstd::arithmetic::power2::lemma_pow2(0);
120    assert(pow2(0) == 1);
121    vstd::arithmetic::mul::lemma_mul_basics(nr_pte_index_bits_spec::<C>() as int);
122    vstd::arithmetic::mul::lemma_mul_basics(C::BASE_PAGE_SIZE() as int);
123}
124
125/// Every page size is at least `BASE_PAGE_SIZE`.
126pub proof fn lemma_page_size_ge_base<C: PagingConstsTrait>(level: PagingLevel)
127    requires
128        1 <= level <= C::NR_LEVELS() + 1,
129    ensures
130        C::BASE_PAGE_SIZE() <= page_size::<C>(level),
131{
132    lemma_page_size_base::<C>();
133    lemma_page_size_divides::<C>(1, level);
134}
135
136/// `page_size` is monotone in the level.
137pub proof fn lemma_page_size_monotone<C: PagingConstsTrait>(l1: PagingLevel, l2: PagingLevel)
138    requires
139        1 <= l1 <= l2 <= C::NR_LEVELS() + 1,
140    ensures
141        page_size::<C>(l1) <= page_size::<C>(l2),
142{
143    lemma_page_size_divides::<C>(l1, l2);
144}
145
146/// A level's page size divided by the base page size multiplies back exactly.
147pub proof fn lemma_page_size_div_mul_eq<C: PagingConstsTrait>(level: PagingLevel)
148    requires
149        1 <= level <= C::NR_LEVELS() + 1,
150    ensures
151        (page_size::<C>(level) / C::BASE_PAGE_SIZE()) * C::BASE_PAGE_SIZE() == page_size::<C>(
152            level,
153        ),
154{
155    lemma_page_size_base::<C>();
156    lemma_page_size_divides::<C>(1, level);
157    lemma_fundamental_div_mod(page_size::<C>(level) as int, page_size::<C>(1) as int);
158}
159
160/// When `va` is aligned to `page_size(large_level)` and `level <= large_level`, then
161/// `va` is aligned to `page_size(level)`.
162pub proof fn lemma_va_align_page_size<C: PagingConstsTrait>(va: Vaddr, level: PagingLevel)
163    requires
164        1 <= level <= C::NR_LEVELS() + 1,
165        va % C::BASE_PAGE_SIZE() == 0,
166        exists|large_level: PagingLevel|
167            1 <= large_level <= C::NR_LEVELS() + 1 && level <= large_level && va % page_size::<C>(
168                large_level,
169            ) == 0,
170    ensures
171        va % page_size::<C>(level) == 0,
172{
173    let large_level: PagingLevel = choose|l: PagingLevel|
174        1 <= l <= C::NR_LEVELS() + 1 && level <= l && va % page_size::<C>(l) == 0;
175    if level == 1nat {
176        lemma_page_size_base::<C>();
177    } else {
178        let ps_l = page_size::<C>(level) as int;
179        let ps_ll = page_size::<C>(large_level) as int;
180        lemma_page_size_divides::<C>(level, large_level);
181        let k = ps_ll / ps_l;
182        vstd::arithmetic::div_mod::lemma_div_non_zero(ps_ll, ps_l);
183        lemma_fundamental_div_mod(ps_ll, ps_l);
184        vstd::arithmetic::div_mod::lemma_mod_mod(va as int, ps_l, k);
185        assert(va as int % ps_l == 0);
186    }
187}
188
189/// When `va` is aligned to `BASE_PAGE_SIZE`, then `va` is aligned to `page_size(1)`.
190pub proof fn lemma_va_align_page_size_level_1<C: PagingConstsTrait>(va: Vaddr)
191    requires
192        va % C::BASE_PAGE_SIZE() == 0,
193    ensures
194        va % page_size::<C>(1) == 0,
195{
196    lemma_page_size_base::<C>();
197}
198
199/// Concrete page sizes for the x86_64 `PagingConsts`, kept for numeric automation.
200pub proof fn lemma_page_size_spec_values()
201    ensures
202        page_size::<PagingConsts>(1) == 4096,
203        page_size::<PagingConsts>(2) == 2097152,
204        page_size::<PagingConsts>(3) == 1073741824,
205        page_size::<PagingConsts>(4) == 549755813888,
206        page_size::<PagingConsts>(5) == 281474976710656,
207{
208    lemma_page_size_base::<PagingConsts>();
209    vstd_extra::external::ilog2::lemma_usize_ilog2_to32();
210    vstd::arithmetic::power2::lemma2_to64();
211    vstd::arithmetic::power2::lemma2_to64_rest();
212    vstd::bits::lemma_usize_pow2_no_overflow(48);
213}
214
215/// Used by `Entry::split_if_mapped_huge` to instantiate the 4KB sub-page forall
216/// invariant at the `i`-th sub-frame's slot.
217pub proof fn lemma_split_sub_page_big_j(pa: Paddr, level: PagingLevel, i: usize) -> (big_j: usize)
218    requires
219        2 <= level <= NR_LEVELS,
220        0 < i < NR_ENTRIES,
221    ensures
222        0 < big_j < page_size::<PagingConsts>(level) / PAGE_SIZE,
223        pa + i * page_size::<PagingConsts>((level - 1) as PagingLevel) == pa + big_j * PAGE_SIZE,
224        big_j == i * (page_size::<PagingConsts>((level - 1) as PagingLevel) / PAGE_SIZE),
225{
226    PagingConsts::lemma_paging_consts_properties();
227    let sub_pages_per_entry: int = (page_size::<PagingConsts>((level - 1) as PagingLevel)
228        / PAGE_SIZE) as int;
229    let big_j_int: int = i * sub_pages_per_entry;
230    lemma_page_size_spec_values();
231    lemma_page_size_div_mul_eq::<PagingConsts>((level - 1) as PagingLevel);
232    lemma_page_size_div_mul_eq::<PagingConsts>(level);
233    lemma_page_size_next::<PagingConsts>((level - 1) as PagingLevel);
234    crate::arch::mm::lemma_nr_subpage_per_huge_eq_nr_entries();
235    vstd::arithmetic::mul::lemma_mul_strictly_positive(i as int, sub_pages_per_entry);
236    vstd::arithmetic::mul::lemma_mul_strict_inequality(
237        i as int,
238        NR_ENTRIES as int,
239        sub_pages_per_entry,
240    );
241    vstd::arithmetic::mul::lemma_mul_is_associative(
242        NR_ENTRIES as int,
243        sub_pages_per_entry,
244        PAGE_SIZE as int,
245    );
246    vstd::arithmetic::div_mod::lemma_div_by_multiple(
247        NR_ENTRIES as int * sub_pages_per_entry,
248        PAGE_SIZE as int,
249    );
250    vstd::arithmetic::mul::lemma_mul_is_associative(
251        i as int,
252        sub_pages_per_entry,
253        PAGE_SIZE as int,
254    );
255    big_j_int as usize
256}
257
258/// For any VA within the kernel virtual address range and any page level,
259/// `va + len` does not overflow usize.
260pub proof fn lemma_va_plus_page_size_no_overflow(va: Vaddr, len: usize)
261    requires
262        va + len <= KERNEL_VADDR_RANGE.end,
263    ensures
264        va + len <= usize::MAX,
265{
266    assert(KERNEL_VADDR_RANGE.end == 0xffff_ffff_ffff_0000usize) by (compute_only);
267}
268
269} // verus!
ostd/specs/mm/page_table/cursor/page_size_lemmas.rs

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