ostd/specs/mm/page_table/
mod.rs

1#![allow(hidden_glob_reexports)]
2
3pub mod cursor;
4pub mod mapping_set_lemmas;
5pub mod node;
6mod owners;
7pub mod vaddr_range_proofs;
8mod view;
9
10use vstd::{
11    arithmetic::{
12        div_mod::{
13            lemma_div_denominator, lemma_fundamental_div_mod, lemma_fundamental_div_mod_converse,
14        },
15        mul::lemma_mul_inequality,
16        power2::{lemma_pow2_pos, pow2},
17    },
18    bits::{lemma_usize_low_bits_mask_is_mod, lemma_usize_shr_is_div},
19    prelude::*,
20    std_specs::range::RangeInclusiveView,
21};
22use vstd_extra::{
23    arithmetic::*, external::ilog2::lemma_usize_is_pow2_is_ilog2_pow2, ownership::*, prelude::*,
24};
25
26use crate::specs::arch::*;
27
28use crate::mm::{
29    PagingConsts, PagingConstsTrait, PagingLevel, Vaddr, kspace::KernelPtConfig,
30    nr_subpage_per_huge, page_size, page_table::PageTableConfig, vm_space::UserPtConfig,
31};
32use align_ext::AlignExt;
33use core::ops::Range;
34pub use cursor::*;
35pub use node::*;
36pub use owners::*;
37pub use view::*;
38
39verus! {
40
41#[verifier::inline]
42pub open spec fn nr_pte_index_bits_spec<C: PagingConstsTrait>() -> usize {
43    nr_subpage_per_huge::<C>().ilog2() as usize
44}
45
46#[verifier::inline]
47pub open spec fn pte_index_bit_offset_spec<C: PagingConstsTrait>(level: PagingLevel) -> usize {
48    (C::BASE_PAGE_SIZE().ilog2() + nr_pte_index_bits_spec::<C>() * (level - 1)) as usize
49}
50
51/// Page-table index selected by `va` at `level`.
52#[verifier::inline]
53pub open spec fn pte_index_spec<C: PagingConstsTrait>(va: Vaddr, level: PagingLevel) -> usize {
54    (va >> pte_index_bit_offset_spec::<C>(level)) & ((nr_subpage_per_huge::<C>() - 1) as usize)
55}
56
57/// Selecting an index is division by the slot size followed by reduction modulo the fanout.
58pub proof fn lemma_pte_index_spec_is_div_mod<C: PagingConstsTrait>(va: Vaddr, level: PagingLevel)
59    requires
60        1 <= level <= C::NR_LEVELS(),
61    ensures
62        pte_index_spec::<C>(va, level) == (va / page_size::<C>(level)) % nr_subpage_per_huge::<C>(),
63{
64    C::lemma_paging_consts_properties();
65    lemma_page_size_is_pow2_pte_index_bit_offset::<C>(level);
66    let bits = nr_pte_index_bits_spec::<C>();
67    lemma_mul_inequality(1, C::NR_LEVELS() as int, bits as int);
68    lemma_usize_is_pow2_is_ilog2_pow2(nr_subpage_per_huge::<C>());
69    lemma_usize_shr_is_div(va, pte_index_bit_offset_spec::<C>(level));
70    lemma_usize_low_bits_mask_is_mod(va >> pte_index_bit_offset_spec::<C>(level), bits as nat);
71}
72
73/// Every extracted index is in the configured fanout.
74pub proof fn lemma_pte_index_bound<C: PagingConstsTrait>(va: Vaddr, level: PagingLevel)
75    requires
76        1 <= level <= C::NR_LEVELS(),
77    ensures
78        pte_index_spec::<C>(va, level) < nr_subpage_per_huge::<C>(),
79{
80    lemma_pte_index_spec_is_div_mod::<C>(va, level);
81    C::lemma_paging_consts_properties();
82    vstd::arithmetic::div_mod::lemma_mod_bound(
83        va as int / page_size::<C>(level) as int,
84        nr_subpage_per_huge::<C>() as int,
85    );
86}
87
88/// Zero lower indices together with base-page alignment imply slot alignment.
89pub proof fn lemma_lower_indices_aligned<C: PagingConstsTrait>(va: Vaddr, level: PagingLevel)
90    requires
91        1 <= level <= C::NR_LEVELS() + 1,
92        va % C::BASE_PAGE_SIZE() == 0,
93        forall|i: int| 1 <= i < level ==> #[trigger] pte_index_spec::<C>(va, i as PagingLevel) == 0,
94    ensures
95        va % page_size::<C>(level) == 0,
96    decreases level,
97{
98    C::lemma_paging_consts_properties();
99    lemma_page_size_base::<C>();
100    if level > 1 {
101        let lower = (level - 1) as PagingLevel;
102        lemma_lower_indices_aligned::<C>(va, lower);
103        lemma_page_size_next::<C>(lower);
104        lemma_pte_index_spec_is_div_mod::<C>(va, lower);
105        assert(pte_index_spec::<C>(va, lower) == 0);
106        vstd::arithmetic::div_mod::lemma_mod_breakdown(
107            va as int,
108            page_size::<C>(lower) as int,
109            nr_subpage_per_huge::<C>() as int,
110        );
111        vstd::arithmetic::mul::lemma_mul_basics(page_size::<C>(lower) as int);
112        assert(va % page_size::<C>(level) == 0);
113    } else {
114        assert(page_size::<C>(level) == C::BASE_PAGE_SIZE());
115    }
116}
117
118/// Slot alignment makes every lower PTE index zero.
119pub proof fn lemma_aligned_indices_zero<C: PagingConstsTrait>(va: Vaddr, level: PagingLevel)
120    requires
121        1 <= level <= C::NR_LEVELS() + 1,
122        va % page_size::<C>(level) == 0,
123    ensures
124        va % C::BASE_PAGE_SIZE() == 0,
125        forall|i: int| 1 <= i < level ==> #[trigger] pte_index_spec::<C>(va, i as PagingLevel) == 0,
126    decreases level,
127{
128    C::lemma_paging_consts_properties();
129    lemma_page_size_base::<C>();
130    if level > 1 {
131        let lower = (level - 1) as PagingLevel;
132        lemma_page_size_next::<C>(lower);
133        let size = page_size::<C>(lower) as int;
134        let fanout = nr_subpage_per_huge::<C>() as int;
135        vstd::arithmetic::div_mod::lemma_mod_mod(va as int, size, fanout);
136        lemma_pte_index_spec_is_div_mod::<C>(va, lower);
137        vstd::arithmetic::div_mod::lemma_mod_breakdown(va as int, size, fanout);
138        vstd::arithmetic::div_mod::lemma_mod_bound(va as int / size, fanout);
139        assert(pte_index_spec::<C>(va, lower) == 0) by (nonlinear_arith)
140            requires
141                size > 0,
142                0 <= va as int / size % fanout,
143                size * (va as int / size % fanout) == 0,
144                pte_index_spec::<C>(va, lower) == va as int / size % fanout,
145        ;
146        lemma_aligned_indices_zero::<C>(va, lower);
147    } else {
148        assert(page_size::<C>(level) == C::BASE_PAGE_SIZE());
149    }
150}
151
152/// A power-of-two-aligned address leaves one complete slot before machine-word wrap.
153pub proof fn lemma_aligned_vaddr_slack<C: PagingConstsTrait>(va: Vaddr, level: PagingLevel)
154    requires
155        1 <= level <= C::NR_LEVELS() + 1,
156        va % page_size::<C>(level) == 0,
157    ensures
158        va + page_size::<C>(level) <= usize::MAX + 1,
159{
160    lemma_page_size_is_pow2_pte_index_bit_offset::<C>(level);
161    let size = page_size::<C>(level);
162    vstd::bits::lemma_usize_low_bits_mask_is_mod(
163        usize::MAX,
164        pte_index_bit_offset_spec::<C>(level) as nat,
165    );
166    vstd::bits::lemma_low_bits_mask_values();
167    assert(usize::MAX & ((size - 1) as usize) == (size - 1) as usize) by (bit_vector);
168    assert(usize::MAX % size == size - 1);
169    lemma_fundamental_div_mod(va as int, size as int);
170    lemma_fundamental_div_mod(usize::MAX as int, size as int);
171    vstd::arithmetic::div_mod::lemma_div_is_ordered(va as int, usize::MAX as int, size as int);
172    vstd::arithmetic::mul::lemma_mul_inequality(
173        va as int / size as int,
174        usize::MAX as int / size as int,
175        size as int,
176    );
177    assert(va + size <= usize::MAX + 1) by (nonlinear_arith)
178        requires
179            va == (size as int) * (va as int / size as int),
180            usize::MAX == (size as int) * (usize::MAX as int / size as int) + size - 1,
181            0 < size,
182            va as int / size as int <= usize::MAX as int / size as int,
183    ;
184}
185
186/// At the next aligned boundary, a terminal index carries into the parent slot.
187pub proof fn lemma_next_slot_pte_index<C: PagingConstsTrait>(
188    va: Vaddr,
189    next: Vaddr,
190    level: PagingLevel,
191)
192    requires
193        1 <= level <= C::NR_LEVELS(),
194        va < next <= va + page_size::<C>(level),
195        next % page_size::<C>(level) == 0,
196    ensures
197        next == (nat_align_down(va as nat, page_size::<C>(level) as nat) + page_size::<C>(
198            level,
199        )) as Vaddr,
200        pte_index_spec::<C>(next, level) == 0 ==> {
201            &&& pte_index_spec::<C>(va, level) + 1 == nr_subpage_per_huge::<C>()
202            &&& next % page_size::<C>((level + 1) as PagingLevel) == 0
203        },
204        pte_index_spec::<C>(next, level) != 0 ==> pte_index_spec::<C>(va, level) + 1
205            < nr_subpage_per_huge::<C>(),
206{
207    C::lemma_paging_consts_properties();
208    lemma_pte_index_spec_is_div_mod::<C>(va, level);
209    lemma_pte_index_spec_is_div_mod::<C>(next, level);
210    lemma_page_size_next::<C>(level);
211    let size = page_size::<C>(level) as int;
212    let fanout = nr_subpage_per_huge::<C>() as int;
213    let quotient = next as int / size;
214    let diff = next - va;
215    lemma_fundamental_div_mod(next as int, size);
216    vstd::arithmetic::mul::lemma_mul_basics(size);
217    vstd::arithmetic::mul::lemma_mul_is_distributive_sub_other_way(size, quotient, 1);
218    lemma_fundamental_div_mod_converse(va as int, size, quotient - 1, size - diff);
219    vstd::arithmetic::div_mod::lemma_mod_bound(va as int / size, fanout);
220    vstd::arithmetic::div_mod::lemma_add_mod_noop_right(1, va as int / size, fanout);
221    let index = pte_index_spec::<C>(va, level) as int;
222    if index + 1 < fanout {
223        vstd::arithmetic::div_mod::lemma_small_mod((index + 1) as nat, fanout as nat);
224    } else {
225        vstd::arithmetic::div_mod::lemma_mod_self_0(fanout);
226    }
227    if pte_index_spec::<C>(next, level) == 0 {
228        vstd::arithmetic::div_mod::lemma_mod_breakdown(next as int, size, fanout);
229        vstd::arithmetic::mul::lemma_mul_basics(size);
230    }
231}
232
233/// Replace one page-table index while leaving the other address components unchanged.
234pub open spec fn vaddr_replace_pte_index_spec<C: PagingConstsTrait>(
235    va: Vaddr,
236    level: PagingLevel,
237    index: int,
238) -> Vaddr {
239    (va as int + (index - pte_index_spec::<C>(va, level)) * page_size::<C>(level)) as Vaddr
240}
241
242/// Number of bits occupied by all configured page-table indices and the in-page offset.
243/// This need not equal the architecture's effective virtual-address width.
244#[verifier::inline]
245pub open spec fn page_table_vaddr_bits_spec<C: PagingConstsTrait>() -> usize {
246    pte_index_bit_offset_spec::<C>((C::NR_LEVELS() + 1) as PagingLevel)
247}
248
249/// Bits of `va` above the complete configured page-table coverage.
250#[verifier::inline]
251pub open spec fn vaddr_upper_bits_spec<C: PagingConstsTrait>(va: Vaddr) -> usize {
252    va >> page_table_vaddr_bits_spec::<C>()
253}
254
255/// Contribution of the uninterpreted upper virtual-address bits to the concrete address.
256/// Unlike the legacy fixed `leading_bits * 2^48` expression, the boundary is derived from `C`.
257#[verifier::inline]
258pub open spec fn vaddr_upper_part_spec<C: PagingConstsTrait>(va: Vaddr) -> int {
259    vaddr_upper_bits_spec::<C>(va) as int * pow2(page_table_vaddr_bits_spec::<C>() as nat) as int
260}
261
262#[verifier::inline]
263pub open spec fn top_level_index_width_spec<C: PageTableConfig>() -> usize {
264    (C::ADDRESS_WIDTH_spec() - pte_index_bit_offset_spec::<C>(C::NR_LEVELS())) as usize
265}
266
267/// Canonical bounds of the VA range managed by a page-table config,
268///
269/// Derived from `LEADING_BITS_spec` and `TOP_LEVEL_INDEX_RANGE`. For
270/// `UserPtConfig` `(LEADING_BITS=0, idx=0..256)` this is `(0, 2^47 - 1)`;
271/// for `KernelPtConfig` `(LEADING_BITS=0xffff, idx=256..512)` this is
272/// `(0xffff_8000_0000_0000, 0xffff_ffff_ffff_ffff)`.
273#[verusfmt::skip]
274pub open spec fn vaddr_range_spec<C: PageTableConfig>() -> RangeInclusiveView<Vaddr> {
275    let off = pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat;
276    let lb = C::LEADING_BITS_spec() as int;
277    let base = lb * 0x1_0000_0000_0000int;
278    let start = (base + (C::TOP_LEVEL_INDEX_RANGE().start) * pow2(off)) as usize;
279    let end = (base + (C::TOP_LEVEL_INDEX_RANGE().end) * pow2(off) - 1) as usize;
280    RangeInclusiveView { start, end, exhausted: false }
281}
282
283pub open spec fn is_valid_range_spec<C: PageTableConfig>(r: Range<Vaddr>) -> bool {
284    let va_range = vaddr_range_spec::<C>();
285    (r.start == 0 && r.end == 0) || (va_range.start <= r.start && r.end - 1 <= va_range.end)
286}
287
288/// Sanity-check: for x86_64 user PT, the bounds are
289/// `(0, 0x0000_7FFF_FFFF_FFFF)`, i.e. the low-half 47-bit user VA space.
290pub(crate) proof fn lemma_vaddr_range_spec_user()
291    ensures
292        vaddr_range_spec::<UserPtConfig>().start == 0,
293        vaddr_range_spec::<UserPtConfig>().end == 0x0000_7FFF_FFFF_FFFF,
294{
295    lemma_arch_specific_consts_properties::<PagingConsts>();
296}
297
298/// Sanity-check: for x86_64 kernel PT, the bounds are the canonical
299/// upper half `(0xFFFF_8000_0000_0000, 0xFFFF_FFFF_FFFF_FFFF)`.
300pub(crate) proof fn lemma_vaddr_range_spec_kernel()
301    ensures
302        vaddr_range_spec::<KernelPtConfig>().start == 0xFFFF_8000_0000_0000,
303        vaddr_range_spec::<KernelPtConfig>().end == 0xFFFF_FFFF_FFFF_FFFF,
304{
305    lemma_arch_specific_consts_properties::<PagingConsts>();
306}
307
308/// Addresses in one aligned node select the same entries at that node and above.
309pub proof fn lemma_same_node_pte_indices_match<C: PagingConstsTrait>(
310    va1: Vaddr,
311    va2: Vaddr,
312    node_start: Vaddr,
313    level: PagingLevel,
314)
315    requires
316        level < C::NR_LEVELS(),
317        node_start <= va1,
318        va1 < node_start + page_size::<C>((level + 1) as PagingLevel),
319        node_start <= va2,
320        va2 < node_start + page_size::<C>((level + 1) as PagingLevel),
321        node_start as nat % page_size::<C>((level + 1) as PagingLevel) as nat == 0,
322    ensures
323        pte_index_spec::<C>(va1, (level + 1) as PagingLevel) == pte_index_spec::<C>(
324            va2,
325            (level + 1) as PagingLevel,
326        ),
327        forall|i: int|
328            level <= i < C::NR_LEVELS() ==> (#[trigger] pte_index_spec::<C>(
329                va1,
330                (i + 1) as PagingLevel,
331            )) == pte_index_spec::<C>(va2, (i + 1) as PagingLevel),
332{
333    C::lemma_paging_consts_properties();
334    let small_level = (level + 1) as PagingLevel;
335    lemma_page_size_is_pow2_pte_index_bit_offset::<C>(small_level);
336    let small = page_size::<C>(small_level) as int;
337    let quotient = node_start as int / small;
338    lemma_fundamental_div_mod(node_start as int, small);
339    lemma_fundamental_div_mod_converse(va1 as int, small, quotient, va1 - node_start);
340    lemma_fundamental_div_mod_converse(va2 as int, small, quotient, va2 - node_start);
341    lemma_pte_index_spec_is_div_mod::<C>(va1, small_level);
342    lemma_pte_index_spec_is_div_mod::<C>(va2, small_level);
343
344    assert forall|i: int| level <= i < C::NR_LEVELS() implies (#[trigger] pte_index_spec::<C>(
345        va1,
346        (i + 1) as PagingLevel,
347    )) == pte_index_spec::<C>(va2, (i + 1) as PagingLevel) by {
348        let large_level = (i + 1) as PagingLevel;
349        lemma_page_size_ratio::<C>(small_level, large_level);
350        lemma_page_size_is_pow2_pte_index_bit_offset::<C>(large_level);
351        let delta = (nr_pte_index_bits_spec::<C>() * (i - level)) as nat;
352        lemma_pow2_pos(delta);
353        let ratio = pow2(delta) as int;
354        lemma_div_denominator(va1 as int, small, ratio);
355        lemma_div_denominator(va2 as int, small, ratio);
356        lemma_pte_index_spec_is_div_mod::<C>(va1, large_level);
357        lemma_pte_index_spec_is_div_mod::<C>(va2, large_level);
358    };
359}
360
361/// Architecture-parameterized view of the uninterpreted upper bits preserved by moving within
362/// one page-table node.
363pub proof fn lemma_same_node_vaddr_upper_bits_match<C: PagingConstsTrait>(
364    va1: Vaddr,
365    va2: Vaddr,
366    node_start: Vaddr,
367    level: PagingLevel,
368)
369    requires
370        level <= C::NR_LEVELS(),
371        node_start <= va1,
372        va1 - node_start < page_size::<C>((level + 1) as PagingLevel),
373        node_start <= va2,
374        va2 - node_start < page_size::<C>((level + 1) as PagingLevel),
375        node_start as nat % page_size::<C>((level + 1) as PagingLevel) as nat == 0,
376    ensures
377        vaddr_upper_bits_spec::<C>(va1) == vaddr_upper_bits_spec::<C>(va2),
378{
379    C::lemma_paging_consts_properties();
380    let small_level = (level + 1) as PagingLevel;
381    let body_level = (C::NR_LEVELS() + 1) as PagingLevel;
382    lemma_page_size_is_pow2_pte_index_bit_offset::<C>(small_level);
383    lemma_page_size_is_pow2_pte_index_bit_offset::<C>(body_level);
384    let small = page_size::<C>(small_level) as int;
385    let quotient = node_start as int / small;
386    lemma_fundamental_div_mod(node_start as int, small);
387    lemma_fundamental_div_mod_converse(va1 as int, small, quotient, va1 - node_start);
388    lemma_fundamental_div_mod_converse(va2 as int, small, quotient, va2 - node_start);
389    let delta = (nr_pte_index_bits_spec::<C>() * (C::NR_LEVELS() - level)) as nat;
390    lemma_page_size_ratio::<C>(small_level, body_level);
391    lemma_pow2_pos(delta);
392    let ratio = pow2(delta) as int;
393    lemma_div_denominator(va1 as int, small, ratio);
394    lemma_div_denominator(va2 as int, small, ratio);
395    lemma_usize_shr_is_div(va1, page_table_vaddr_bits_spec::<C>());
396    lemma_usize_shr_is_div(va2, page_table_vaddr_bits_spec::<C>());
397}
398
399/// Upper address bits contribute the aligned base of the complete paging body.
400pub proof fn lemma_vaddr_upper_part_is_align_down<C: PagingConstsTrait>(va: Vaddr)
401    ensures
402        vaddr_upper_part_spec::<C>(va) == nat_align_down(
403            va as nat,
404            page_size::<C>((C::NR_LEVELS() + 1) as PagingLevel) as nat,
405        ),
406{
407    C::lemma_paging_consts_properties();
408    let level = (C::NR_LEVELS() + 1) as PagingLevel;
409    lemma_page_size_is_pow2_pte_index_bit_offset::<C>(level);
410    lemma_usize_shr_is_div(va, page_table_vaddr_bits_spec::<C>());
411    lemma_fundamental_div_mod(va as int, page_size::<C>(level) as int);
412    vstd::arithmetic::mul::lemma_mul_is_commutative(
413        page_size::<C>(level) as int,
414        vaddr_upper_bits_spec::<C>(va) as int,
415    );
416}
417
418/// Aligning down preserves all indices at and above the slot and the upper address bits.
419pub proof fn lemma_align_down_indices<C: PagingConstsTrait>(va: Vaddr, level: PagingLevel)
420    requires
421        1 <= level <= C::NR_LEVELS(),
422    ensures
423        ({
424            let aligned = nat_align_down(va as nat, page_size::<C>(level) as nat) as Vaddr;
425            &&& aligned % C::BASE_PAGE_SIZE() == 0
426            &&& vaddr_upper_bits_spec::<C>(aligned) == vaddr_upper_bits_spec::<C>(va)
427            &&& forall|i: int|
428                1 <= i <= C::NR_LEVELS() ==> #[trigger] pte_index_spec::<C>(
429                    aligned,
430                    i as PagingLevel,
431                ) == if i < level {
432                    0
433                } else {
434                    pte_index_spec::<C>(va, i as PagingLevel)
435                }
436        }),
437{
438    lemma_page_size_is_pow2_pte_index_bit_offset::<C>(level);
439    let size = page_size::<C>(level) as nat;
440    lemma_nat_align_down_sound(va as nat, size);
441    let aligned = nat_align_down(va as nat, size) as Vaddr;
442    lemma_aligned_indices_zero::<C>(aligned, level);
443    lemma_same_node_pte_indices_match::<C>(va, aligned, aligned, (level - 1) as PagingLevel);
444    lemma_same_node_vaddr_upper_bits_match::<C>(va, aligned, aligned, (level - 1) as PagingLevel);
445    assert forall|i: int| 1 <= i <= C::NR_LEVELS() implies #[trigger] pte_index_spec::<C>(
446        aligned,
447        i as PagingLevel,
448    ) == if i < level {
449        0
450    } else {
451        pte_index_spec::<C>(va, i as PagingLevel)
452    } by {
453        if i >= level {
454            assert((level - 1) < i);
455            assert(pte_index_spec::<C>(va, ((i - 1) + 1) as PagingLevel) == pte_index_spec::<C>(
456                aligned,
457                ((i - 1) + 1) as PagingLevel,
458            ));
459        }
460    };
461}
462
463/// Advancing a nonterminal slot preserves every other index and cannot wrap the machine word.
464pub proof fn lemma_inc_slot_indices<C: PagingConstsTrait>(va: Vaddr, level: PagingLevel)
465    requires
466        1 <= level <= C::NR_LEVELS(),
467        pte_index_spec::<C>(va, level) + 1 < nr_subpage_per_huge::<C>(),
468    ensures
469        va + page_size::<C>(level) <= usize::MAX,
470        ({
471            let next = (va + page_size::<C>(level)) as Vaddr;
472            &&& next % C::BASE_PAGE_SIZE() == va % C::BASE_PAGE_SIZE()
473            &&& vaddr_upper_bits_spec::<C>(next) == vaddr_upper_bits_spec::<C>(va)
474            &&& forall|i: int|
475                1 <= i <= C::NR_LEVELS() ==> #[trigger] pte_index_spec::<C>(next, i as PagingLevel)
476                    == pte_index_spec::<C>(va, i as PagingLevel) + if i == level {
477                    1int
478                } else {
479                    0int
480                }
481        }),
482{
483    C::lemma_paging_consts_properties();
484    lemma_page_size_next::<C>(level);
485    lemma_pte_index_spec_is_div_mod::<C>(va, level);
486    let size = page_size::<C>(level) as int;
487    let parent_size = page_size::<C>((level + 1) as PagingLevel) as int;
488    let fanout = nr_subpage_per_huge::<C>() as int;
489    let index = pte_index_spec::<C>(va, level) as int;
490    lemma_nat_align_down_sound(va as nat, parent_size as nat);
491    let start = nat_align_down(va as nat, parent_size as nat) as Vaddr;
492    lemma_aligned_vaddr_slack::<C>(start, (level + 1) as PagingLevel);
493    vstd::arithmetic::div_mod::lemma_mod_breakdown(va as int, size, fanout);
494    vstd::arithmetic::div_mod::lemma_mod_bound(va as int, size);
495    assert(index == va as int / size % fanout);
496    assert(va as int % parent_size == size * index + va as int % size);
497    vstd::arithmetic::div_mod::lemma_mod_bound(va as int, parent_size);
498    vstd::arithmetic::div_mod::lemma_div_pos_is_pos(va as int, parent_size);
499    lemma_fundamental_div_mod(va as int, parent_size);
500    assert(va - start == va as int % parent_size);
501    assert(va - start + size < parent_size) by (nonlinear_arith)
502        requires
503            va - start == size * index + va as int % size,
504            0 <= va as int % size < size,
505            index + 1 < fanout,
506            parent_size == size * fanout,
507    ;
508    let next = (va + size) as Vaddr;
509    lemma_fundamental_div_mod(va as int, size);
510    vstd::arithmetic::mul::lemma_mul_is_distributive_add_other_way(size, va as int / size, 1);
511    lemma_fundamental_div_mod_converse(next as int, size, va as int / size + 1, va as int % size);
512    lemma_pte_index_spec_is_div_mod::<C>(next, level);
513    vstd::arithmetic::div_mod::lemma_add_mod_noop_right(1, va as int / size, fanout);
514    vstd::arithmetic::div_mod::lemma_small_mod((index + 1) as nat, fanout as nat);
515    assert(pte_index_spec::<C>(next, level) == index + 1);
516    if level < C::NR_LEVELS() {
517        lemma_same_node_pte_indices_match::<C>(va, next, start, level);
518    }
519    lemma_same_node_vaddr_upper_bits_match::<C>(va, next, start, level);
520    lemma_page_size_divides::<C>(1, level);
521    lemma_page_size_base::<C>();
522    vstd::arithmetic::div_mod::lemma_add_mod_noop(va as int, size, C::BASE_PAGE_SIZE() as int);
523    vstd::arithmetic::div_mod::lemma_mod_twice(va as int, C::BASE_PAGE_SIZE() as int);
524    assert(next % C::BASE_PAGE_SIZE() == va % C::BASE_PAGE_SIZE());
525    assert forall|i: int| 1 <= i < level implies #[trigger] pte_index_spec::<C>(
526        next,
527        i as PagingLevel,
528    ) == pte_index_spec::<C>(va, i as PagingLevel) by {
529        let lower = i as PagingLevel;
530        let parent = (i + 1) as PagingLevel;
531        lemma_page_size_divides::<C>(parent, level);
532        lemma_page_size_next::<C>(lower);
533        let small = page_size::<C>(lower) as int;
534        let block = page_size::<C>(parent) as int;
535        vstd::arithmetic::div_mod::lemma_add_mod_noop(va as int, size, block);
536        vstd::arithmetic::div_mod::lemma_mod_twice(va as int, block);
537        assert(next as int % block == va as int % block);
538        vstd::arithmetic::div_mod::lemma_mod_mod(va as int, small, fanout);
539        vstd::arithmetic::div_mod::lemma_mod_mod(next as int, small, fanout);
540        vstd::arithmetic::div_mod::lemma_mod_breakdown(va as int, small, fanout);
541        vstd::arithmetic::div_mod::lemma_mod_breakdown(next as int, small, fanout);
542        lemma_pte_index_spec_is_div_mod::<C>(va, lower);
543        lemma_pte_index_spec_is_div_mod::<C>(next, lower);
544        assert(next as int % small == va as int % small);
545        assert(small * pte_index_spec::<C>(next, lower) == small * pte_index_spec::<C>(va, lower));
546        assert(pte_index_spec::<C>(next, lower) == pte_index_spec::<C>(va, lower))
547            by (nonlinear_arith)
548            requires
549                small > 0,
550                small * pte_index_spec::<C>(next, lower) == small * pte_index_spec::<C>(va, lower),
551        ;
552    };
553    assert forall|i: int| 1 <= i <= C::NR_LEVELS() implies #[trigger] pte_index_spec::<C>(
554        next,
555        i as PagingLevel,
556    ) == pte_index_spec::<C>(va, i as PagingLevel) + if i == level {
557        1int
558    } else {
559        0int
560    } by {
561        if i > level {
562            assert(level < C::NR_LEVELS());
563            assert(pte_index_spec::<C>(va, ((i - 1) + 1) as PagingLevel) == pte_index_spec::<C>(
564                next,
565                ((i - 1) + 1) as PagingLevel,
566            ));
567        }
568    };
569}
570
571} // verus!
ostd/specs/mm/page_table/mod.rs

ostd/specs/mm/page_table/
mod.rs
