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

ostd/specs/mm/page_table/
mod.rs
