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::{PageTableConfig, pte_index_bit_offset_spec};
12use crate::mm::{PagingConstsTrait, Vaddr};
13
14verus! {
15
16/// Facts needed to turn `idx.start << offset` into
17/// `idx.start * 2^offset` for `pt_va_range_start`.
18pub proof fn lemma_pt_va_range_start_shift_facts<C: PageTableConfig>(
19    idx_start: usize,
20    offset: usize,
21)
22    requires
23        idx_start == C::TOP_LEVEL_INDEX_RANGE_spec().start,
24        offset == pte_index_bit_offset_spec::<C>(C::NR_LEVELS()),
25    ensures
26        offset < usize::BITS,
27        idx_start * pow2(offset as nat) <= usize::MAX,
28        offset == pte_index_bit_offset_spec::<C>(C::NR_LEVELS()),
29{
30    C::lemma_paging_consts_properties();
31    C::lemma_page_table_config_constant_properties();
32    vstd::layout::unsigned_int_max_values();
33
34    let off = pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat;
35    let aw = C::ADDRESS_WIDTH() as nat;
36    let top_w = (aw - off) as nat;
37    lemma_pow2_adds(top_w, off);
38    lemma_pow2_pos(off);
39    lemma_pow2_pos(top_w);
40    lemma_pow2_pos(aw);
41
42    let i_start = C::TOP_LEVEL_INDEX_RANGE_spec().start as int;
43    let p_off = pow2(off) as int;
44    let p_top = pow2(top_w) as int;
45
46    assert(i_start * p_off < p_top * p_off) by (nonlinear_arith)
47        requires
48            i_start < p_top,
49            p_off > 0,
50    ;
51
52    if aw < 64 {
53        vstd::arithmetic::power2::lemma_pow2_strictly_increases(aw, 64);
54    }
55}
56
57/// Facts needed to turn `idx.end << offset` into
58/// `idx.end * 2^offset` for `pt_va_range_end`.
59pub proof fn lemma_pt_va_range_end_shift_facts<C: PageTableConfig>(idx_end: usize, offset: usize)
60    requires
61        idx_end == C::TOP_LEVEL_INDEX_RANGE_spec().end,
62        offset == pte_index_bit_offset_spec::<C>(C::NR_LEVELS()),
63    ensures
64        offset < usize::BITS,
65        idx_end * pow2(offset as nat) <= usize::MAX,
66        0 < idx_end * pow2(offset as nat),
67        offset == pte_index_bit_offset_spec::<C>(C::NR_LEVELS()),
68{
69    C::lemma_paging_consts_properties();
70    C::lemma_page_table_config_constant_properties();
71    lemma_pow2_pos(offset as nat);
72
73    let i_end = C::TOP_LEVEL_INDEX_RANGE_spec().end as int;
74    let p_off = pow2(offset as nat) as int;
75    assert(i_end * p_off > 0) by (nonlinear_arith)
76        requires
77            i_end > 0,
78            p_off > 0,
79    ;
80}
81
82/// Connect `wrapping_sub(1)` to the modulo end-of-range spec after the
83/// shift result is known to be non-zero.
84pub proof fn lemma_pt_va_range_end_wrapping_sub<C: PageTableConfig>(
85    idx_end: usize,
86    offset: usize,
87    shifted: usize,
88    ret: usize,
89)
90    requires
91        idx_end == C::TOP_LEVEL_INDEX_RANGE_spec().end,
92        offset == pte_index_bit_offset_spec::<C>(C::NR_LEVELS()),
93        shifted == idx_end * pow2(offset as nat),
94        ret == vstd::wrapping::usize_specs::wrapping_sub(shifted, 1usize),
95    ensures
96        ret == (C::TOP_LEVEL_INDEX_RANGE_spec().end * pow2(
97            pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat,
98        ) - 1) % 0x1_0000_0000_0000_0000int,
99{
100    lemma_pt_va_range_end_shift_facts::<C>(idx_end, offset);
101    vstd::layout::unsigned_int_max_values();
102}
103
104/// Facts needed to connect `(va >> (ADDRESS_WIDTH - 1)) & 1` with the
105/// arithmetic bit-test specification.
106pub proof fn lemma_sign_bit_facts<C: PageTableConfig>(
107    va: Vaddr,
108    address_width: usize,
109    shift: usize,
110    shifted: usize,
111    bit: usize,
112)
113    requires
114        address_width == C::ADDRESS_WIDTH(),
115        shift == address_width - 1,
116        shifted == va >> shift,
117        bit == shifted & 1usize,
118    ensures
119        (bit != 0) == ((va as int / pow2((C::ADDRESS_WIDTH() - 1) as nat) as int) % 2 == 1),
120{
121    C::lemma_paging_consts_properties();
122    C::lemma_page_table_config_constant_properties();
123
124    vstd::bits::lemma_usize_shr_is_div(va, shift);
125    vstd::bits::lemma_usize_low_bits_mask_is_mod(shifted, 1);
126    vstd::bits::lemma_low_bits_mask_values();
127    vstd::arithmetic::power2::lemma2_to64();
128}
129
130/// Two-in-one: `start = idx.start * 2^off < 2^ADDRESS_WIDTH` and
131/// `end = (idx.end * 2^off - 1) % 2^64 < 2^ADDRESS_WIDTH`.
132///
133/// The first follows from `idx.start < 2^(ADDRESS_WIDTH - off)`. The
134/// second from `idx.end <= 2^(ADDRESS_WIDTH - off)` plus the no-wrap
135/// condition: `idx.end * 2^off <= 2^ADDRESS_WIDTH ≤ 2^64`, so the `% 2^64`
136/// is a no-op when the value is positive.
137pub proof fn lemma_idx_times_pow2_bound<C: PageTableConfig>(start: Vaddr, end: Vaddr)
138    requires
139        start == C::TOP_LEVEL_INDEX_RANGE_spec().start * (pow2(
140            pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat,
141        ) as int),
142        end == (C::TOP_LEVEL_INDEX_RANGE_spec().end * (pow2(
143            pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat,
144        ) as int) - 1) % 0x1_0000_0000_0000_0000int,
145    ensures
146        start < pow2(C::ADDRESS_WIDTH() as nat),
147        end < pow2(C::ADDRESS_WIDTH() as nat),
148        // For the end-of-range arithmetic ensures of `vaddr_range`:
149        end == C::TOP_LEVEL_INDEX_RANGE_spec().end * pow2(
150            pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat,
151        ) - 1,
152{
153    C::lemma_paging_consts_properties();
154    C::lemma_page_table_config_constant_properties();
155    let off = pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat;
156    let aw = C::ADDRESS_WIDTH() as nat;
157    let top_w = (aw - off) as nat;
158    lemma_pow2_adds(top_w, off);
159    lemma_pow2_pos(off);
160    lemma_pow2_pos(top_w);
161    lemma_pow2_pos(aw);
162    // Constants for clarity.
163    let i_start = C::TOP_LEVEL_INDEX_RANGE_spec().start as int;
164    let i_end = C::TOP_LEVEL_INDEX_RANGE_spec().end as int;
165    let p_off = pow2(off) as int;
166    let p_top = pow2(top_w) as int;
167    let p_aw = pow2(aw) as int;
168    // start < p_top * p_off = p_aw.
169    assert(start < (p_top * p_off)) by (nonlinear_arith)
170        requires
171            start == i_start * p_off,
172            i_start < p_top,
173            p_off > 0,
174    ;
175    // end pre-wrap value.
176    let e_pre = i_end * p_off;
177    assert(e_pre <= p_top * p_off) by (nonlinear_arith)
178        requires
179            e_pre == i_end * p_off,
180            i_end <= p_top,
181            p_off > 0,
182    ;
183    // i_end > 0 — from `lemma_page_table_config_constant_properties`'s
184    // `idx.start < idx.end` plus `idx.start >= 0` (usize).
185    assert(e_pre > 0) by (nonlinear_arith)
186        requires
187            e_pre == i_end * p_off,
188            i_end > 0,
189            p_off > 0,
190    ;
191}
192
193} // verus!
ostd/specs/mm/page_table/vaddr_range_proofs.rs

ostd/specs/mm/page_table/
vaddr_range_proofs.rs
