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`.
8
9use vstd::arithmetic::power2::{lemma_pow2_adds, lemma_pow2_pos, pow2};
10use vstd::prelude::*;
11
12use crate::mm::page_table::{
13    axiom_top_level_index_range_bounds, pte_index_bit_offset_spec, PageTableConfig,
14};
15use crate::mm::{PagingConstsTrait, Vaddr};
16
17verus! {
18
19/// Two-in-one: `start = idx.start * 2^off < 2^ADDRESS_WIDTH` and
20/// `end = (idx.end * 2^off - 1) % 2^64 < 2^ADDRESS_WIDTH`.
21///
22/// The first follows from `idx.start < 2^(ADDRESS_WIDTH - off)`. The
23/// second from `idx.end <= 2^(ADDRESS_WIDTH - off)` plus the no-wrap
24/// condition: `idx.end * 2^off <= 2^ADDRESS_WIDTH ≤ 2^64`, so the `% 2^64`
25/// is a no-op when the value is positive.
26pub proof fn lemma_idx_times_pow2_bound<C: PageTableConfig>(start: Vaddr, end: Vaddr)
27    requires
28        start as int == (C::TOP_LEVEL_INDEX_RANGE_spec().start as int)
29            * (pow2(pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()) as nat) as int),
30        end as int == ((C::TOP_LEVEL_INDEX_RANGE_spec().end as int)
31            * (pow2(pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()) as nat) as int)
32            - 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)
38            * (pow2(pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()) as nat) as int)
39            - 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    // end pre-wrap value.
66    let e_pre = i_end * p_off;
67    assert(i_end <= p_top);
68    assert(e_pre <= p_top * p_off) by (nonlinear_arith)
69        requires
70            e_pre == i_end * p_off,
71            i_end <= p_top,
72            p_off > 0;
73    // i_end > 0 — from `axiom_top_level_index_range_bounds`'s
74    // `idx.start < idx.end` plus `idx.start >= 0` (usize).
75    assert(i_end > 0);
76    assert(e_pre > 0) by (nonlinear_arith)
77        requires
78            e_pre == i_end * p_off,
79            i_end > 0,
80            p_off > 0;
81    assert(e_pre <= p_aw);
82    // p_aw <= 2^64 — from `ADDRESS_WIDTH <= 64` plus monotonicity of pow2.
83    if aw < 64 {
84        vstd::arithmetic::power2::lemma_pow2_strictly_increases(aw, 64);
85    }
86    assert(pow2(64) == 0x1_0000_0000_0000_0000nat) by {
87        vstd::arithmetic::power2::lemma2_to64();
88    };
89    assert(p_aw <= 0x1_0000_0000_0000_0000int);
90    // No-wrap: 0 < e_pre <= 2^64, so (e_pre - 1) % 2^64 = e_pre - 1.
91    assert(0 <= e_pre - 1);
92    assert((e_pre - 1) < 0x1_0000_0000_0000_0000int);
93    assert((e_pre - 1) % 0x1_0000_0000_0000_0000int == e_pre - 1) by (nonlinear_arith)
94        requires 0 <= (e_pre - 1), (e_pre - 1) < 0x1_0000_0000_0000_0000int;
95}
96
97} // verus!
ostd/specs/mm/page_table/vaddr_range_proofs.rs

ostd/specs/mm/page_table/
vaddr_range_proofs.rs
