ostd/specs/mm/page_table/cursor/
va_lemmas.rs

1/// Virtual-address manipulation specs and lemmas for `CursorOwner`.
2///
3/// This module contains:
4/// - Spec functions for zeroing VA indices below the cursor's level
5///   (`zero_below_level_rec`, `zero_below_level`).
6/// - Lemmas about how zeroing preserves fields other than VA.
7/// - Spec functions for the cursor's current VA and VA range
8///   (`cur_va`, `cur_va_range`).
9/// - Lemmas relating the abstract VA to the page table view range.
10/// - Axiom functions for updating the cursor VA (`set_va`, `set_va_in_node`).
11use core::ops::Range;
12
13use vstd::prelude::*;
14
15use vstd_extra::{arithmetic::nat_align_down, ghost_tree::*, ownership::*};
16
17use crate::specs::{
18    arch::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE},
19    mm::page_table::{
20        AbstractVaddr, Mapping,
21        cursor::{
22            owners::{CursorContinuation, CursorOwner},
23            page_size_lemmas::{
24                lemma_page_size_divides, lemma_page_size_ge_page_size, lemma_page_size_spec_values,
25            },
26        },
27        owners::*,
28    },
29};
30
31use crate::mm::{Paddr, PagingLevel, Vaddr, page_size, page_table::*};
32
33verus! {
34
35broadcast use group_ghost_tree_lemmas;
36
37impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
38    // ─── Spec helpers ────────────────────────────────────────────────────
39    pub open spec fn zero_below_level_rec(self, level: PagingLevel) -> Self
40        decreases self.level - level,
41    {
42        if self.level <= level {
43            self
44        } else {
45            Self {
46                va: AbstractVaddr { index: self.va.index.insert(level - 1, 0), ..self.va },
47                ..self.zero_below_level_rec((level + 1) as u8)
48            }
49        }
50    }
51
52    pub open spec fn zero_below_level(self) -> Self
53        recommends
54            1 <= self.level <= NR_LEVELS,
55    {
56        Self { va: self.va.align_down(self.level as int), ..self }
57    }
58
59    pub open spec fn cur_va(self) -> Vaddr {
60        self.va.to_vaddr()
61    }
62
63    pub open spec fn cur_va_range(self) -> Range<AbstractVaddr> {
64        let start = self.va.align_down(self.level as int);
65        let end = self.va.align_up(self.level as int);
66        Range { start, end }
67    }
68
69    pub open spec fn set_va(self, new_va: AbstractVaddr) -> Self {
70        Self { va: new_va, ..self }
71    }
72
73    pub open spec fn set_va_in_node(self, new_va: AbstractVaddr) -> Self {
74        let old_cont = self.continuations[self.level - 1];
75        Self {
76            va: new_va,
77            continuations: self.continuations.insert(
78                self.level - 1,
79                CursorContinuation { idx: new_va.index[self.level - 1] as usize, ..old_cont },
80            ),
81            // Repositioning to a concrete in-range VA clears the
82            // transient `popped_too_high` state.
83            popped_too_high: false,
84            ..self
85        }
86    }
87
88    // ─── Proofs: zero preserves structure ────────────────────────────────
89    pub proof fn zero_below_level_rec_preserves_above(self, level: PagingLevel)
90        ensures
91            forall|lv: int|
92                lv >= self.level ==> self.zero_below_level_rec(level).va.index[lv]
93                    == #[trigger] self.va.index[lv],
94        decreases self.level - level,
95    {
96        if self.level > level {
97            self.zero_below_level_rec_preserves_above((level + 1) as u8);
98        }
99    }
100
101    /// Unfolds zero_below_level to expose the VA as align_down(level).
102    pub proof fn zero_below_level_va(self)
103        requires
104            1 <= self.level <= NR_LEVELS,
105        ensures
106            self.zero_below_level().va == self.va.align_down(self.level as int),
107    {
108    }
109
110    pub proof fn zero_preserves_above(self)
111        requires
112            self.va.inv(),
113            1 <= self.level <= NR_LEVELS,
114        ensures
115            forall|lv: int|
116                self.level <= lv < NR_LEVELS ==> self.zero_below_level().va.index[lv]
117                    == #[trigger] self.va.index[lv],
118    {
119        self.va.align_down_shape(self.level as int);
120    }
121
122    pub proof fn do_zero_below_level(tracked &mut self)
123        requires
124            old(self).inv(),
125            old(self).level <= old(self).guard_level,
126        ensures
127            *final(self) == old(self).zero_below_level(),
128            final(self).inv(),
129    {
130        let ghost old_self = *self;
131        old_self.va.align_down_shape(old_self.level as int);
132        old_self.va.align_down_leading_bits(old_self.level as int);
133        self.va = old_self.va.align_down(old_self.level as int);
134
135        old_self.locked_range_span();
136        lemma_page_size_ge_page_size(old_self.level as PagingLevel);
137        lemma_page_size_ge_page_size(old_self.guard_level as PagingLevel);
138        lemma_page_size_divides(old_self.level as PagingLevel, old_self.guard_level as PagingLevel);
139        old_self.va.align_down_to_vaddr_nat_align_down(old_self.level as int);
140
141        let ghost old_va_val = old_self.va.to_vaddr() as nat;
142        let ghost prefix_va_val = old_self.prefix.to_vaddr() as nat;
143        let ghost ps = page_size(old_self.level as PagingLevel) as nat;
144        let ghost guard_ps = page_size(old_self.guard_level as PagingLevel) as nat;
145        let ghost start = old_self.locked_range().start as nat;
146
147        vstd_extra::arithmetic::lemma_nat_align_down_monotone(prefix_va_val, ps, guard_ps);
148        vstd_extra::arithmetic::lemma_mod_0_add(start as int, guard_ps as int, ps as int);
149
150        vstd_extra::arithmetic::lemma_nat_align_down_sound(old_va_val, ps);
151        if !self.popped_too_high && (self.in_locked_range() || self.level < self.guard_level) {
152            if self.level == self.guard_level {
153                let new_va_val = self.va.to_vaddr() as nat;
154                let diff = (new_va_val - start) as nat;
155                vstd::arithmetic::div_mod::lemma_mod_equivalence(
156                    new_va_val as int,
157                    start as int,
158                    ps as int,
159                );
160                vstd::arithmetic::div_mod::lemma_small_mod(diff, ps);
161            }
162        }
163    }
164
165    pub proof fn zero_rec_preserves_all_but_va(self, level: PagingLevel)
166        ensures
167            self.zero_below_level_rec(level).level == self.level,
168            self.zero_below_level_rec(level).continuations == self.continuations,
169            self.zero_below_level_rec(level).guard_level == self.guard_level,
170            self.zero_below_level_rec(level).prefix == self.prefix,
171            self.zero_below_level_rec(level).popped_too_high == self.popped_too_high,
172        decreases self.level - level,
173    {
174        if self.level > level {
175            self.zero_rec_preserves_all_but_va((level + 1) as u8);
176        }
177    }
178
179    pub proof fn zero_preserves_all_but_va(self)
180        ensures
181            self.zero_below_level().level == self.level,
182            self.zero_below_level().continuations == self.continuations,
183            self.zero_below_level().guard_level == self.guard_level,
184            self.zero_below_level().prefix == self.prefix,
185            self.zero_below_level().popped_too_high == self.popped_too_high,
186    {
187        self.zero_rec_preserves_all_but_va(1u8);
188    }
189
190    // ─── Proofs: inc + zero ──────────────────────────────────────────────
191    pub proof fn inc_and_zero_increases_va(self)
192        requires
193            self.inv(),
194            self.in_locked_range(),
195            self.index() + 1 < NR_ENTRIES,
196        ensures
197            self.inc_index().zero_below_level().va.to_vaddr() > self.va.to_vaddr(),
198    {
199        // inc_index increments va.index[level-1] by 1. zero_below_level zeroes
200        // indices below level (= align_down). The result is align_up(va, ps).
201        self.lemma_inc_index_va_inv();
202        let inc = self.inc_index();
203        inc.zero_preserves_all_but_va();
204        inc.zero_below_level_va();
205        assert(inc.va.inv());
206
207        let ps = page_size(self.level as PagingLevel) as nat;
208        let self_va = self.va.to_vaddr() as nat;
209        lemma_page_size_ge_page_size(self.level as PagingLevel);
210
211        // Step 1: inc_index adds page_size to the vaddr.
212        self.va.index_increment_adds_page_size(self.level as int);
213        let inc_va = inc.va.to_vaddr() as nat;
214
215        // Step 2: zero_below_level().va == inc.va.align_down(level).
216        // align_down_concrete gives .reflect(nat_align_down(inc_va, ps)).
217        inc.va.align_down_concrete(self.level as int);
218        let new_va = vstd_extra::arithmetic::nat_align_down(inc_va, ps);
219        AbstractVaddr::from_vaddr_to_vaddr_roundtrip(new_va as Vaddr);
220        // Now inc.zero_below_level().va.to_vaddr() == new_va.
221
222        // Step 3: align_down(self_va + ps, ps) = align_down(self_va, ps) + ps.
223        // Because (self_va + ps) % ps == self_va % ps, adding a full ps doesn't
224        // change the remainder.
225        vstd::arithmetic::div_mod::lemma_mod_add_multiples_vanish(self_va as int, ps as int);
226
227        // Step 4: align_down(self_va, ps) + ps > self_va.
228        // Because align_down(self_va, ps) = self_va - self_va % ps,
229        // and self_va % ps < ps.
230        vstd::arithmetic::div_mod::lemma_fundamental_div_mod(self_va as int, ps as int);
231        vstd::arithmetic::div_mod::lemma_mod_bound(self_va as int, ps as int);
232    }
233
234    // ─── Proofs: VA range / view ─────────────────────────────────────────
235    #[verifier::spinoff_prover]
236    pub proof fn cur_va_range_reflects_view(self)
237        requires
238            self.inv(),
239            self.in_locked_range(),
240            !self.popped_too_high,
241            self.cur_entry_owner().is_frame(),
242        ensures
243            self.cur_va_range().start.reflect(self@.query_range().start as Vaddr),
244            self.cur_va_range().end.reflect(self@.query_range().end as Vaddr),
245    {
246        broadcast use CursorContinuation::group_lemmas;
247
248        self.cur_subtree_inv();
249        self.cur_va_in_subtree_range();
250        self.view_preserves_inv();
251        self.cur_entry_frame_present();
252        let subtree = self.cur_subtree();
253        let path = subtree.value().path;
254        let frame = self.cur_entry_owner().frame();
255
256        let ps = page_size(self.level as PagingLevel);
257        let m = Mapping {
258            va_range: Range { start: vaddr_of::<C>(path) as int, end: vaddr_of::<C>(path) + ps },
259            pa_range: Range { start: frame.mapped_pa, end: (frame.mapped_pa + ps) as Paddr },
260            page_size: ps,
261            property: frame.prop,
262        };
263
264        assert(PageTableOwner(subtree).view_rec(path).contains(m));
265        self.lemma_view_mappings_intro(m, (self.level - 1) as int);
266        assert(m.inv());
267
268        self.cur_va_in_subtree_range();
269        crate::specs::mm::page_table::owners::lemma_vaddr_of_eq_int::<C>(path);
270
271        let filtered = self@.mappings.filter(
272            |m2: Mapping| m2.va_range.start <= self@.cur_va < m2.va_range.end,
273        );
274        vstd::set::lemma_set_choose_len(filtered);
275
276        let cur_va = self.va.to_vaddr() as nat;
277        let ps_nat = ps as nat;
278        self.va.align_down_concrete(self.level as int);
279        lemma_page_size_ge_page_size(self.level as PagingLevel);
280        vstd_extra::arithmetic::lemma_nat_align_down_sound(cur_va, ps_nat);
281
282        // Bridge: `cur_va == vaddr_of::<C>(path)` for paths aligned with the
283        // cursor (offset is 0, the `to_vaddr_indices(0)` positional sum
284        // equals `vaddr(path)`, and the `leading_bits * 2^48` is the same
285        // `LEADING_BITS * 2^48` that `vaddr_of` adds).
286
287        assert(nat_align_down(cur_va, ps_nat) == vaddr_of::<C>(path) as nat) by {
288            vstd::arithmetic::div_mod::lemma_fundamental_div_mod(cur_va as int, ps as int);
289            vstd::arithmetic::div_mod::lemma_fundamental_div_mod(
290                vaddr_of::<C>(path) as int,
291                ps as int,
292            );
293            assert(vaddr_of::<C>(path) as int % ps as int == 0);
294            vstd::arithmetic::div_mod::lemma_indistinguishable_quotients(
295                vaddr_of::<C>(path) as int,
296                cur_va as int,
297                ps as int,
298            );
299        };
300
301        self.locked_range_page_aligned();
302        self.va.to_vaddr_bounded();
303        self.in_locked_range_level_le_guard_level();
304        self.va_plus_page_size_no_overflow(self.level as PagingLevel);
305        self.va.align_up_advances_general(self.level as int);
306
307        AbstractVaddr::from_vaddr_to_vaddr_roundtrip(nat_align_down(cur_va, ps_nat) as Vaddr);
308        AbstractVaddr::from_vaddr_to_vaddr_roundtrip((vaddr_of::<C>(path) + ps) as Vaddr);
309
310        self.va.align_up(self.level as int).reflect_to_vaddr();
311    }
312
313    /// The current virtual address falls within the VA range of the
314    /// current subtree's path, in canonical form (positional vaddr plus
315    /// the `leading_bits * 2^48` shift).
316    pub proof fn cur_va_in_subtree_range(self)
317        requires
318            self.inv(),
319            self.in_locked_range(),
320        ensures
321            vaddr(self.cur_subtree().value().path) + self.va.leading_bits * 0x1_0000_0000_0000int
322                <= self.cur_va(),
323            self.cur_va() < vaddr(self.cur_subtree().value().path) + self.va.leading_bits
324                * 0x1_0000_0000_0000int + page_size(self.level as PagingLevel),
325    {
326        let L = self.level as int;
327        let cont = self.continuations[L - 1];
328        let subtree_path = cont.path().push_tail(cont.idx as int);
329        let va_path = self.va.to_path(L - 1);
330
331        self.va.to_path_len(L - 1);
332
333        assert forall|i: int| 0 <= i < subtree_path.len() implies subtree_path[i] == va_path[i] by {
334            self.va.to_path_index(L - 1, i);
335        };
336
337        self.va.to_path_inv(L - 1);
338        self.cur_subtree_inv();
339        AbstractVaddr::rec_vaddr_eq_if_indices_eq(subtree_path, va_path, 0);
340        self.va.vaddr_range_from_path(L - 1);
341    }
342
343    pub proof fn lemma_locked_range_vaddr_prefix_match(self, new_va: AbstractVaddr)
344        requires
345            self.inv(),
346            new_va.inv(),
347            new_va.offset == 0,
348            new_va.leading_bits == self.prefix.leading_bits,
349            self.locked_range().start <= new_va.to_vaddr() < self.locked_range().end,
350        ensures
351            forall|i: int|
352                #![trigger new_va.index[i]]
353                self.guard_level - 1 <= i < NR_LEVELS ==> new_va.index[i] == self.prefix.index[i],
354    {
355        let gl = self.guard_level;
356        let start = self.locked_range().start;
357        let ps = page_size(gl as PagingLevel);
358        let new_val = new_va.to_vaddr();
359        let prefix_val = self.prefix.to_vaddr();
360
361        self.locked_range_span();
362        self.prefix_aligned_to_guard_level();
363        self.prefix_plus_ps_no_overflow();
364        self.prefix.aligned_align_down_is_self(gl as int);
365        self.prefix.aligned_align_up_advances(gl as int);
366
367        lemma_page_size_spec_values();
368        if gl == 1 {
369            new_va.reflect_to_vaddr();
370
371            AbstractVaddr::same_page_aligned_vaddrs_equal(new_val, prefix_val, start);
372            AbstractVaddr::to_vaddr_from_vaddr_roundtrip(new_va);
373            AbstractVaddr::to_vaddr_from_vaddr_roundtrip(self.prefix);
374        } else {
375            AbstractVaddr::to_vaddr_from_vaddr_roundtrip(new_va);
376            AbstractVaddr::to_vaddr_from_vaddr_roundtrip(self.prefix);
377            AbstractVaddr::same_node_indices_match(
378                new_val,
379                prefix_val,
380                start,
381                (gl - 1) as PagingLevel,
382            );
383        }
384    }
385
386    // ─── Axioms: VA mutation ─────────────────────────────────────────────
387    /// When jumping within the same page-table node, only indices at levels
388    /// >= level are guaranteed to match. The entry-within-node index (level - 1)
389    /// may change, so we update continuations[level-1].idx along with va.
390    pub proof fn tracked_set_va_in_node(tracked &mut self, new_va: AbstractVaddr)
391        requires
392            old(self).inv(),
393            new_va.inv(),
394            new_va.offset == 0,
395            new_va.leading_bits == old(self).prefix.leading_bits,
396            forall|i: int|
397                #![auto]
398                old(self).level <= i < NR_LEVELS ==> new_va.index[i] == old(self).va.index[i],
399            old(self).locked_range().start <= new_va.to_vaddr() < old(self).locked_range().end,
400            // Needed for soundness of the asserted `final(self).inv()`:
401            // we clear `popped_too_high`, so `CursorOwner::inv`'s
402            // `!popped_too_high ==> level <= guard_level || above_locked_range`
403            // clause must hold; the new VA is in-range (not above), so
404            // we require `level <= guard_level`.
405            old(self).level <= old(self).guard_level,
406        ensures
407            *final(self) == old(self).set_va_in_node(new_va),
408            final(self).inv(),
409    {
410        let ghost old_self = *self;
411        let tracked mut cont = self.continuations.tracked_remove(self.level - 1);
412
413        assert(new_va.index.contains_key(old_self.level - 1));
414
415        cont.idx = new_va.index[old_self.level - 1] as usize;
416
417        self.continuations.tracked_insert(self.level - 1, cont);
418        self.va = new_va;
419        self.popped_too_high = false;
420
421        assert(self.continuations == old_self.continuations.insert(old_self.level - 1, cont));
422
423        old_self.lemma_locked_range_vaddr_prefix_match(new_va);
424
425        if old_self.level < old_self.guard_level {
426            old_self.prefix_in_locked_range();
427        }
428    }
429}
430
431} // verus!
ostd/specs/mm/page_table/cursor/va_lemmas.rs

ostd/specs/mm/page_table/cursor/
va_lemmas.rs
