ostd/specs/mm/page_table/
vaddr_range_proofs.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Bounded-arithmetic proofs for `vaddr_range`'s body.
3//!
4//! Factored into a leaf module because the `nonlinear_arith` tactic
5//! triggers a Verus internal panic when used in `page_table/mod.rs`
6//! alongside `largest_pages` (which has an `impl Iterator` return type).
7//! Same workaround pattern as the older `vaddr_range_bv_lemmas`.
8use vstd::arithmetic::power2::{lemma_pow2_adds, lemma_pow2_pos, pow2};
9use vstd::prelude::*;
10
11use crate::mm::page_table::{
12    PageTableConfig, axiom_top_level_index_range_bounds, pte_index_bit_offset_spec,
13};
14use crate::mm::{PagingConstsTrait, Vaddr};
15
16verus! {
17
18/// Two-in-one: `start = idx.start * 2^off < 2^ADDRESS_WIDTH` and
19/// `end = (idx.end * 2^off - 1) % 2^64 < 2^ADDRESS_WIDTH`.
20///
21/// The first follows from `idx.start < 2^(ADDRESS_WIDTH - off)`. The
22/// second from `idx.end <= 2^(ADDRESS_WIDTH - off)` plus the no-wrap
23/// condition: `idx.end * 2^off <= 2^ADDRESS_WIDTH ≤ 2^64`, so the `% 2^64`
24/// is a no-op when the value is positive.
25pub proof fn lemma_idx_times_pow2_bound<C: PageTableConfig>(start: Vaddr, end: Vaddr)
26    requires
27        start as int == (C::TOP_LEVEL_INDEX_RANGE_spec().start as int) * (pow2(
28            pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()) as nat,
29        ) as int),
30        end as int == ((C::TOP_LEVEL_INDEX_RANGE_spec().end as int) * (pow2(
31            pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()) as nat,
32        ) as int) - 1) % 0x1_0000_0000_0000_0000int,
33    ensures
34        (start as int) < (pow2(C::ADDRESS_WIDTH() as nat) as int),
35        (end as int) < (pow2(C::ADDRESS_WIDTH() as nat) as int),
36        // For the end-of-range arithmetic ensures of `vaddr_range`:
37        end as int == (C::TOP_LEVEL_INDEX_RANGE_spec().end as int) * (pow2(
38            pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()) as nat,
39        ) as int) - 1,
40{
41    axiom_top_level_index_range_bounds::<C>();
42    let off = pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()) as nat;
43    let aw = C::ADDRESS_WIDTH() as nat;
44    let top_w = (aw as int - off as int) as nat;
45    lemma_pow2_adds(top_w, off);
46    lemma_pow2_pos(off);
47    lemma_pow2_pos(top_w);
48    lemma_pow2_pos(aw);
49    // Constants for clarity.
50    let i_start = C::TOP_LEVEL_INDEX_RANGE_spec().start as int;
51    let i_end = C::TOP_LEVEL_INDEX_RANGE_spec().end as int;
52    let p_off = pow2(off) as int;
53    let p_top = pow2(top_w) as int;
54    let p_aw = pow2(aw) as int;
55    assert(p_top * p_off == p_aw);
56    assert(start as int == i_start * p_off);
57    assert(i_start < p_top);
58    assert(p_off > 0);
59    // start < p_top * p_off = p_aw.
60    assert((start as int) < (p_top * p_off)) by (nonlinear_arith)
61        requires
62            start as int == i_start * p_off,
63            i_start < p_top,
64            p_off > 0,
65    ;
66    // end pre-wrap value.
67    let e_pre = i_end * p_off;
68    assert(i_end <= p_top);
69    assert(e_pre <= p_top * p_off) by (nonlinear_arith)
70        requires
71            e_pre == i_end * p_off,
72            i_end <= p_top,
73            p_off > 0,
74    ;
75    // i_end > 0 — from `axiom_top_level_index_range_bounds`'s
76    // `idx.start < idx.end` plus `idx.start >= 0` (usize).
77    assert(i_end > 0);
78    assert(e_pre > 0) by (nonlinear_arith)
79        requires
80            e_pre == i_end * p_off,
81            i_end > 0,
82            p_off > 0,
83    ;
84    assert(e_pre <= p_aw);
85    // p_aw <= 2^64 — from `ADDRESS_WIDTH <= 64` plus monotonicity of pow2.
86    if aw < 64 {
87        vstd::arithmetic::power2::lemma_pow2_strictly_increases(aw, 64);
88    }
89    assert(pow2(64) == 0x1_0000_0000_0000_0000nat) by {
90        vstd::arithmetic::power2::lemma2_to64();
91    };
92    assert(p_aw <= 0x1_0000_0000_0000_0000int);
93    // No-wrap: 0 < e_pre <= 2^64, so (e_pre - 1) % 2^64 = e_pre - 1.
94    assert(0 <= e_pre - 1);
95    assert((e_pre - 1) < 0x1_0000_0000_0000_0000int);
96    assert((e_pre - 1) % 0x1_0000_0000_0000_0000int == e_pre - 1) by (nonlinear_arith)
97        requires
98            0 <= (e_pre - 1),
99            (e_pre - 1) < 0x1_0000_0000_0000_0000int,
100    ;
101}
102
103} // verus!
ostd/specs/mm/page_table/vaddr_range_proofs.rs

ostd/specs/mm/page_table/
vaddr_range_proofs.rs
