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::{
9    arithmetic::{
10        div_mod::{lemma_mod_bound, lemma_mod_breakdown, lemma_mod_decreases},
11        power2::{lemma_pow2_adds, lemma_pow2_pos, lemma_pow2_strictly_increases, pow2},
12    },
13    prelude::*,
14};
15use vstd_extra::arithmetic::nat_align_down;
16
17use crate::specs::mm::page_table::*;
18
19use crate::mm::{
20    PagingConstsTrait, PagingLevel, Vaddr, nr_subpage_per_huge, page_size,
21    page_table::PageTableConfig,
22};
23
24verus! {
25
26/// Derives the sign-extension mask and its width from the paging constants.
27pub proof fn lemma_leading_bits_properties<C: PageTableConfig>()
28    ensures
29        page_table_coverage_start_spec::<C>() == leading_bits_spec::<C>() * pow2(
30            nr_page_table_coverage_bits_spec::<C>() as nat,
31        ),
32        page_table_coverage_start_spec::<C>() + pow2(nr_page_table_coverage_bits_spec::<C>() as nat)
33            <= pow2(usize::BITS as nat),
34        C::VA_SIGN_EXT() && (C::TOP_LEVEL_INDEX_RANGE().start * pow2(
35            pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat,
36        ) / pow2((C::ADDRESS_WIDTH() - 1) as nat) as int) % 2 == 1
37            ==> page_table_coverage_start_spec::<C>() == pow2(usize::BITS as nat) - pow2(
38            C::ADDRESS_WIDTH() as nat,
39        ),
40        leading_bits_spec::<C>() < pow2(
41            (usize::BITS - nr_page_table_coverage_bits_spec::<C>()) as nat,
42        ),
43{
44    C::lemma_paging_consts_properties();
45    let bits = nr_page_table_coverage_bits_spec::<C>() as nat;
46    let width = C::ADDRESS_WIDTH() as nat;
47    lemma_pow2_adds((usize::BITS - bits) as nat, bits);
48    lemma_pow2_adds((width - bits) as nat, bits);
49    lemma_pow2_pos((width - bits) as nat);
50    vstd::arithmetic::power2::lemma_pow2_strictly_increases(
51        (width - bits) as nat,
52        (usize::BITS - bits) as nat,
53    );
54    vstd::layout::unsigned_int_max_values();
55    if bits < usize::BITS {
56        if bits > 0 {
57            vstd::arithmetic::power2::lemma_pow2_strictly_increases(
58                (usize::BITS - bits) as nat,
59                usize::BITS as nat,
60            );
61        }
62    }
63    assert((pow2((usize::BITS - bits) as nat) - pow2((width - bits) as nat)) * pow2(bits) == pow2(
64        usize::BITS as nat,
65    ) - pow2(width)) by (nonlinear_arith)
66        requires
67            pow2((usize::BITS - bits) as nat) * pow2(bits) == pow2(usize::BITS as nat),
68            pow2((width - bits) as nat) * pow2(bits) == pow2(width),
69    ;
70    assert(leading_bits_spec::<C>() * pow2(bits) + pow2(bits) <= pow2(usize::BITS as nat))
71        by (nonlinear_arith)
72        requires
73            leading_bits_spec::<C>() < pow2((usize::BITS - bits) as nat),
74            pow2(bits) > 0,
75            pow2((usize::BITS - bits) as nat) * pow2(bits) == pow2(usize::BITS as nat),
76    ;
77}
78
79/// Managed bounds preserve their mathematical values and match the inclusive range model.
80pub proof fn lemma_page_table_managed_bounds<C: PageTableConfig>()
81    ensures
82        page_table_managed_start_spec::<C>() == page_table_coverage_start_spec::<C>()
83            + C::TOP_LEVEL_INDEX_RANGE().start * page_size::<C>(C::NR_LEVELS()),
84        page_table_managed_start_spec::<C>() < page_table_managed_end_spec::<C>() <= usize::MAX + 1,
85        vaddr_range_spec::<C>().end + 1 == page_table_managed_end_spec::<C>(),
86{
87    C::lemma_paging_consts_properties();
88    C::lemma_page_table_config_constant_properties();
89    lemma_leading_bits_properties::<C>();
90    lemma_page_size_is_pow2_pte_index_bit_offset::<C>(C::NR_LEVELS());
91    let off = pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat;
92    let aw = C::ADDRESS_WIDTH() as nat;
93    lemma_pow2_adds((aw - off) as nat, off);
94    lemma_pow2_strictly_increases(aw, usize::BITS as nat);
95    vstd::layout::unsigned_int_max_values();
96    let base = page_table_coverage_start_spec::<C>() as int;
97    let size = page_size::<C>(C::NR_LEVELS()) as int;
98    let start = base + C::TOP_LEVEL_INDEX_RANGE().start * size;
99    let end = page_table_managed_end_spec::<C>();
100    assert(0 <= start < end <= usize::MAX + 1) by (nonlinear_arith)
101        requires
102            0 <= base,
103            base == 0 || base == pow2(usize::BITS as nat) - pow2(aw),
104            pow2(aw) < pow2(usize::BITS as nat),
105            pow2(usize::BITS as nat) == usize::MAX + 1,
106            0 < size,
107            size == pow2(off),
108            pow2((aw - off) as nat) * pow2(off) == pow2(aw),
109            0 <= C::TOP_LEVEL_INDEX_RANGE().start < C::TOP_LEVEL_INDEX_RANGE().end <= pow2(
110                (aw - off) as nat,
111            ),
112            start == base + C::TOP_LEVEL_INDEX_RANGE().start * size,
113            end == base + C::TOP_LEVEL_INDEX_RANGE().end * size,
114    ;
115}
116
117/// Managed address bounds are equivalent to root-index bounds when the upper address bits match.
118/// The current root slot ends within the managed range whenever the address is inside it.
119pub proof fn lemma_page_table_managed_index_bounds<C: PageTableConfig>(va: Vaddr)
120    requires
121        vaddr_leading_part_spec::<C>(va) == page_table_coverage_start_spec::<C>(),
122    ensures
123        (page_table_managed_start_spec::<C>() <= va) == (C::TOP_LEVEL_INDEX_RANGE().start
124            <= pte_index_spec::<C>(va, C::NR_LEVELS())),
125        (va < page_table_managed_end_spec::<C>()) == (pte_index_spec::<C>(va, C::NR_LEVELS())
126            < C::TOP_LEVEL_INDEX_RANGE().end),
127        va < page_table_managed_end_spec::<C>() ==> nat_align_down(
128            va as nat,
129            page_size::<C>(C::NR_LEVELS()) as nat,
130        ) + page_size::<C>(C::NR_LEVELS()) <= page_table_managed_end_spec::<C>(),
131{
132    C::lemma_paging_consts_properties();
133    lemma_page_table_managed_bounds::<C>();
134    let top = C::NR_LEVELS();
135    lemma_page_size_next::<C>(top);
136    lemma_vaddr_leading_part_is_align_down::<C>(va);
137    lemma_pte_index_spec_is_div_mod::<C>(va, top);
138    let size = page_size::<C>(top) as int;
139    let body = page_size::<C>((top + 1) as PagingLevel) as int;
140    let fanout = nr_subpage_per_huge::<C>() as int;
141    lemma_mod_decreases(va as nat, body as nat);
142    lemma_mod_breakdown(va as int, size, fanout);
143    let base = page_table_coverage_start_spec::<C>() as int;
144    let index = pte_index_spec::<C>(va, top) as int;
145    assert({
146        &&& base + index * size == va - va as int % size
147        &&& base + index * size <= va < base + (index + 1) * size
148    }) by (nonlinear_arith)
149        requires
150            base == va - va as int % body,
151            va as int % body == size * index + va as int % size,
152            0 <= va as int % size < size,
153    ;
154    assert({
155        &&& (page_table_managed_start_spec::<C>() <= va) == (C::TOP_LEVEL_INDEX_RANGE().start
156            <= index)
157        &&& (va < page_table_managed_end_spec::<C>()) == (index < C::TOP_LEVEL_INDEX_RANGE().end)
158        &&& (va < page_table_managed_end_spec::<C>() ==> base + index * size + size
159            <= page_table_managed_end_spec::<C>())
160    }) by (nonlinear_arith)
161        requires
162            size > 0,
163            base + index * size <= va < base + (index + 1) * size,
164            page_table_managed_start_spec::<C>() == base + C::TOP_LEVEL_INDEX_RANGE().start * size,
165            page_table_managed_end_spec::<C>() == base + C::TOP_LEVEL_INDEX_RANGE().end * size,
166    ;
167}
168
169/// Facts needed to turn `idx.start << offset` into
170/// `idx.start * 2^offset` for `pt_va_range_start`.
171pub proof fn lemma_pt_va_range_start_shift_facts<C: PageTableConfig>(
172    idx_start: usize,
173    offset: usize,
174)
175    requires
176        idx_start == C::TOP_LEVEL_INDEX_RANGE().start,
177        offset == pte_index_bit_offset_spec::<C>(C::NR_LEVELS()),
178    ensures
179        offset < usize::BITS,
180        idx_start * pow2(offset as nat) <= usize::MAX,
181        offset == pte_index_bit_offset_spec::<C>(C::NR_LEVELS()),
182{
183    C::lemma_paging_consts_properties();
184    C::lemma_page_table_config_constant_properties();
185    vstd::layout::unsigned_int_max_values();
186
187    let off = pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat;
188    let aw = C::ADDRESS_WIDTH() as nat;
189    let top_w = (aw - off) as nat;
190    lemma_pow2_adds(top_w, off);
191    lemma_pow2_pos(off);
192
193    let i_start = C::TOP_LEVEL_INDEX_RANGE().start as int;
194    let p_off = pow2(off) as int;
195    let p_top = pow2(top_w) as int;
196
197    assert(i_start * p_off < p_top * p_off) by (nonlinear_arith)
198        requires
199            i_start < p_top,
200            p_off > 0,
201    ;
202
203    if aw < 64 {
204        vstd::arithmetic::power2::lemma_pow2_strictly_increases(aw, 64);
205    }
206}
207
208/// Facts needed to turn `idx.end << offset` into
209/// `idx.end * 2^offset` for `pt_va_range_end`.
210pub proof fn lemma_pt_va_range_end_shift_facts<C: PageTableConfig>(idx_end: usize, offset: usize)
211    requires
212        idx_end == C::TOP_LEVEL_INDEX_RANGE().end,
213        offset == pte_index_bit_offset_spec::<C>(C::NR_LEVELS()),
214    ensures
215        offset < usize::BITS,
216        idx_end * pow2(offset as nat) <= usize::MAX,
217        0 < idx_end * pow2(offset as nat),
218        offset == pte_index_bit_offset_spec::<C>(C::NR_LEVELS()),
219{
220    C::lemma_paging_consts_properties();
221    C::lemma_page_table_config_constant_properties();
222    lemma_pow2_pos(offset as nat);
223
224    let i_end = C::TOP_LEVEL_INDEX_RANGE().end as int;
225    let p_off = pow2(offset as nat) as int;
226    assert(i_end * p_off > 0) by (nonlinear_arith)
227        requires
228            i_end > 0,
229            p_off > 0,
230    ;
231}
232
233/// Two-in-one: `start = idx.start * 2^off < 2^ADDRESS_WIDTH` and
234/// `end = (idx.end * 2^off - 1) % 2^64 < 2^ADDRESS_WIDTH`.
235///
236/// The first follows from `idx.start < 2^(ADDRESS_WIDTH - off)`. The
237/// second from `idx.end <= 2^(ADDRESS_WIDTH - off)` plus the no-wrap
238/// condition: `idx.end * 2^off <= 2^ADDRESS_WIDTH ≤ 2^64`, so the `% 2^64`
239/// is a no-op when the value is positive.
240pub proof fn lemma_idx_times_pow2_bound<C: PageTableConfig>(start: Vaddr, end: Vaddr)
241    requires
242        start == C::TOP_LEVEL_INDEX_RANGE().start * (pow2(
243            pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat,
244        ) as int),
245        end == (C::TOP_LEVEL_INDEX_RANGE().end * (pow2(
246            pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat,
247        ) as int) - 1) % 0x1_0000_0000_0000_0000int,
248    ensures
249        start < pow2(C::ADDRESS_WIDTH() as nat),
250        end < pow2(C::ADDRESS_WIDTH() as nat),
251        // For the end-of-range arithmetic ensures of `vaddr_range`:
252        end == C::TOP_LEVEL_INDEX_RANGE().end * pow2(
253            pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat,
254        ) - 1,
255{
256    C::lemma_paging_consts_properties();
257    C::lemma_page_table_config_constant_properties();
258    let off = pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat;
259    let aw = C::ADDRESS_WIDTH() as nat;
260    let top_w = (aw - off) as nat;
261    lemma_pow2_adds(top_w, off);
262    lemma_pow2_pos(off);
263    // Constants for clarity.
264    let i_start = C::TOP_LEVEL_INDEX_RANGE().start as int;
265    let i_end = C::TOP_LEVEL_INDEX_RANGE().end as int;
266    let p_off = pow2(off) as int;
267    let p_top = pow2(top_w) as int;
268    let p_aw = pow2(aw) as int;
269    // start < p_top * p_off = p_aw.
270    assert(start < (p_top * p_off)) by (nonlinear_arith)
271        requires
272            start == i_start * p_off,
273            i_start < p_top,
274            p_off > 0,
275    ;
276    // end pre-wrap value.
277    let e_pre = i_end * p_off;
278    assert(e_pre <= p_top * p_off) by (nonlinear_arith)
279        requires
280            e_pre == i_end * p_off,
281            i_end <= p_top,
282            p_off > 0,
283    ;
284    // i_end > 0 — from `lemma_page_table_config_constant_properties`'s
285    // `idx.start < idx.end` plus `idx.start >= 0` (usize).
286    assert(e_pre > 0) by (nonlinear_arith)
287        requires
288            e_pre == i_end * p_off,
289            i_end > 0,
290            p_off > 0,
291    ;
292}
293
294} // verus!
ostd/specs/mm/page_table/vaddr_range_proofs.rs

ostd/specs/mm/page_table/
vaddr_range_proofs.rs
