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        assert(start % ps == 0);
149        vstd::arithmetic::div_mod::lemma_add_mod_noop(start as int, guard_ps as int, ps as int);
150
151        vstd_extra::arithmetic::lemma_nat_align_down_sound(old_va_val, ps);
152    }
153
154    pub proof fn zero_rec_preserves_all_but_va(self, level: PagingLevel)
155        ensures
156            self.zero_below_level_rec(level).level == self.level,
157            self.zero_below_level_rec(level).continuations == self.continuations,
158            self.zero_below_level_rec(level).guard_level == self.guard_level,
159            self.zero_below_level_rec(level).prefix == self.prefix,
160            self.zero_below_level_rec(level).popped_too_high == self.popped_too_high,
161        decreases self.level - level,
162    {
163        if self.level > level {
164            self.zero_rec_preserves_all_but_va((level + 1) as u8);
165        }
166    }
167
168    pub proof fn zero_preserves_all_but_va(self)
169        ensures
170            self.zero_below_level().level == self.level,
171            self.zero_below_level().continuations == self.continuations,
172            self.zero_below_level().guard_level == self.guard_level,
173            self.zero_below_level().prefix == self.prefix,
174            self.zero_below_level().popped_too_high == self.popped_too_high,
175    {
176        self.zero_rec_preserves_all_but_va(1u8);
177    }
178
179    // ─── Proofs: inc + zero ──────────────────────────────────────────────
180    pub proof fn inc_and_zero_increases_va(self)
181        requires
182            self.inv(),
183            self.in_locked_range(),
184            self.index() + 1 < NR_ENTRIES,
185        ensures
186            self.inc_index().zero_below_level().va.to_vaddr() > self.va.to_vaddr(),
187    {
188        // inc_index increments va.index[level-1] by 1. zero_below_level zeroes
189        // indices below level (= align_down). The result is align_up(va, ps).
190        let inc = self.inc_index();
191        inc.zero_preserves_all_but_va();
192        inc.zero_below_level_va();
193        assert(inc.va.inv());
194
195        let ps = page_size(self.level as PagingLevel) as nat;
196        let self_va = self.va.to_vaddr() as nat;
197        lemma_page_size_ge_page_size(self.level as PagingLevel);
198
199        // Step 1: inc_index adds page_size to the vaddr.
200        self.va.index_increment_adds_page_size(self.level as int);
201        let inc_va = inc.va.to_vaddr() as nat;
202
203        // Step 2: zero_below_level().va == inc.va.align_down(level).
204        // align_down_concrete gives .reflect(nat_align_down(inc_va, ps)).
205        inc.va.align_down_concrete(self.level as int);
206        let new_va = vstd_extra::arithmetic::nat_align_down(inc_va, ps);
207        AbstractVaddr::from_vaddr_to_vaddr_roundtrip(new_va as Vaddr);
208        // Now inc.zero_below_level().va.to_vaddr() == new_va.
209
210        // Step 3: align_down(self_va + ps, ps) = align_down(self_va, ps) + ps.
211        // Because (self_va + ps) % ps == self_va % ps, adding a full ps doesn't
212        // change the remainder.
213        vstd::arithmetic::div_mod::lemma_mod_add_multiples_vanish(self_va as int, ps as int);
214
215        // Step 4: align_down(self_va, ps) + ps > self_va.
216        // Because align_down(self_va, ps) = self_va - self_va % ps,
217        // and self_va % ps < ps.
218        vstd::arithmetic::div_mod::lemma_fundamental_div_mod(self_va as int, ps as int);
219        vstd::arithmetic::div_mod::lemma_mod_bound(self_va as int, ps as int);
220    }
221
222    // ─── Proofs: VA range / view ─────────────────────────────────────────
223    #[verifier::spinoff_prover]
224    pub proof fn cur_va_range_reflects_view(self)
225        requires
226            self.inv(),
227            self.in_locked_range(),
228            !self.popped_too_high,
229            self.cur_entry_owner().is_frame(),
230        ensures
231            self.cur_va_range().start.reflect(self@.query_range().start as Vaddr),
232            self.cur_va_range().end.reflect(self@.query_range().end as Vaddr),
233    {
234        broadcast use CursorContinuation::group_lemmas;
235
236        self.cur_subtree_inv();
237        self.cur_va_in_subtree_range();
238        self.view_preserves_inv();
239        self.cur_entry_frame_present();
240        let subtree = self.cur_subtree();
241        let path = subtree.value().path;
242        let frame = self.cur_entry_owner().frame();
243
244        let ps = page_size(self.level as PagingLevel);
245        let m = Mapping {
246            va_range: Range { start: vaddr_of::<C>(path) as int, end: vaddr_of::<C>(path) + ps },
247            pa_range: Range { start: frame.mapped_pa, end: (frame.mapped_pa + ps) as Paddr },
248            page_size: ps,
249            property: frame.prop,
250        };
251
252        assert(PageTableOwner(subtree).view_rec(path).contains(m));
253        self.lemma_view_mappings_intro(m, (self.level - 1) as int);
254        assert(m.inv());
255
256        self.cur_va_in_subtree_range();
257        crate::specs::mm::page_table::owners::lemma_vaddr_of_eq_int::<C>(path);
258
259        let filtered = self@.mappings.filter(
260            |m2: Mapping| m2.va_range.start <= self@.cur_va < m2.va_range.end,
261        );
262        vstd::set::lemma_set_choose_len(filtered);
263
264        let cur_va = self.va.to_vaddr() as nat;
265        let ps_nat = ps as nat;
266        self.va.align_down_concrete(self.level as int);
267        lemma_page_size_ge_page_size(self.level as PagingLevel);
268        vstd_extra::arithmetic::lemma_nat_align_down_sound(cur_va, ps_nat);
269
270        // Bridge: `cur_va == vaddr_of::<C>(path)` for paths aligned with the
271        // cursor (offset is 0, the `to_vaddr_indices(0)` positional sum
272        // equals `vaddr(path)`, and the `leading_bits * 2^48` is the same
273        // `LEADING_BITS * 2^48` that `vaddr_of` adds).
274
275        assert(nat_align_down(cur_va, ps_nat) == vaddr_of::<C>(path) as nat) by {
276            vstd::arithmetic::div_mod::lemma_fundamental_div_mod(cur_va as int, ps as int);
277            vstd::arithmetic::div_mod::lemma_fundamental_div_mod(
278                vaddr_of::<C>(path) as int,
279                ps as int,
280            );
281            assert(vaddr_of::<C>(path) as int % ps as int == 0);
282            vstd::arithmetic::div_mod::lemma_indistinguishable_quotients(
283                vaddr_of::<C>(path) as int,
284                cur_va as int,
285                ps as int,
286            );
287        };
288
289        self.locked_range_page_aligned();
290        self.va.to_vaddr_bounded();
291        self.in_locked_range_level_le_guard_level();
292        self.va_plus_page_size_no_overflow(self.level as PagingLevel);
293        self.va.align_up_advances_general(self.level as int);
294
295        AbstractVaddr::from_vaddr_to_vaddr_roundtrip(nat_align_down(cur_va, ps_nat) as Vaddr);
296        AbstractVaddr::from_vaddr_to_vaddr_roundtrip((vaddr_of::<C>(path) + ps) as Vaddr);
297
298        self.va.align_up(self.level as int).reflect_to_vaddr();
299    }
300
301    /// The current virtual address falls within the VA range of the
302    /// current subtree's path, in canonical form (positional vaddr plus
303    /// the `leading_bits * 2^48` shift).
304    pub proof fn cur_va_in_subtree_range(self)
305        requires
306            self.inv(),
307            self.in_locked_range(),
308        ensures
309            vaddr(self.cur_subtree().value().path) + self.va.leading_bits * 0x1_0000_0000_0000int
310                <= self.cur_va(),
311            self.cur_va() < vaddr(self.cur_subtree().value().path) + self.va.leading_bits
312                * 0x1_0000_0000_0000int + page_size(self.level as PagingLevel),
313    {
314        let L = self.level as int;
315        let cont = self.continuations[L - 1];
316        let subtree_path = cont.path().push_tail(cont.idx as int);
317        let va_path = self.va.to_path(L - 1);
318
319        self.va.to_path_len(L - 1);
320
321        assert forall|i: int| 0 <= i < subtree_path.len() implies subtree_path[i] == va_path[i] by {
322            self.va.to_path_index(L - 1, i);
323        };
324
325        self.va.to_path_inv(L - 1);
326        self.cur_subtree_inv();
327        AbstractVaddr::rec_vaddr_eq_if_indices_eq(subtree_path, va_path, 0);
328        self.va.vaddr_range_from_path(L - 1);
329    }
330
331    pub proof fn lemma_locked_range_vaddr_prefix_match(self, new_va: AbstractVaddr)
332        requires
333            self.inv(),
334            new_va.inv(),
335            new_va.offset == 0,
336            new_va.leading_bits == self.prefix.leading_bits,
337            self.locked_range().start <= new_va.to_vaddr() < self.locked_range().end,
338        ensures
339            forall|i: int|
340                #![trigger new_va.index[i]]
341                self.guard_level - 1 <= i < NR_LEVELS ==> new_va.index[i] == self.prefix.index[i],
342    {
343        let gl = self.guard_level;
344        let start = self.locked_range().start;
345        let ps = page_size(gl as PagingLevel);
346        let new_val = new_va.to_vaddr();
347        let prefix_val = self.prefix.to_vaddr();
348
349        self.locked_range_span();
350        self.prefix_aligned_to_guard_level();
351        self.prefix_plus_ps_no_overflow();
352        self.prefix.aligned_align_down_is_self(gl as int);
353        self.prefix.aligned_align_up_advances(gl as int);
354
355        lemma_page_size_spec_values();
356        if gl == 1 {
357            new_va.reflect_to_vaddr();
358
359            AbstractVaddr::same_page_aligned_vaddrs_equal(new_val, prefix_val, start);
360            AbstractVaddr::to_vaddr_from_vaddr_roundtrip(new_va);
361            AbstractVaddr::to_vaddr_from_vaddr_roundtrip(self.prefix);
362        } else {
363            AbstractVaddr::to_vaddr_from_vaddr_roundtrip(new_va);
364            AbstractVaddr::to_vaddr_from_vaddr_roundtrip(self.prefix);
365            AbstractVaddr::same_node_indices_match(
366                new_val,
367                prefix_val,
368                start,
369                (gl - 1) as PagingLevel,
370            );
371        }
372    }
373
374    // ─── Axioms: VA mutation ─────────────────────────────────────────────
375    /// When jumping within the same page-table node, only indices at levels
376    /// >= level are guaranteed to match. The entry-within-node index (level - 1)
377    /// may change, so we update continuations[level-1].idx along with va.
378    pub proof fn tracked_set_va_in_node(tracked &mut self, new_va: AbstractVaddr)
379        requires
380            old(self).inv(),
381            new_va.inv(),
382            new_va.offset == 0,
383            new_va.leading_bits == old(self).prefix.leading_bits,
384            forall|i: int|
385                #![auto]
386                old(self).level <= i < NR_LEVELS ==> new_va.index[i] == old(self).va.index[i],
387            old(self).locked_range().start <= new_va.to_vaddr() < old(self).locked_range().end,
388            // Needed for soundness of the asserted `final(self).inv()`:
389            // we clear `popped_too_high`, so `CursorOwner::inv`'s
390            // `!popped_too_high ==> level <= guard_level || above_locked_range`
391            // clause must hold; the new VA is in-range (not above), so
392            // we require `level <= guard_level`.
393            old(self).level <= old(self).guard_level,
394        ensures
395            *final(self) == old(self).set_va_in_node(new_va),
396            final(self).inv(),
397    {
398        let ghost old_self = *self;
399        let tracked mut cont = self.continuations.tracked_remove(self.level - 1);
400
401        assert(new_va.index.contains_key(old_self.level - 1));
402
403        cont.idx = new_va.index[old_self.level - 1] as usize;
404
405        self.continuations.tracked_insert(self.level - 1, cont);
406        self.va = new_va;
407        self.popped_too_high = false;
408
409        assert(self.continuations == old_self.continuations.insert(old_self.level - 1, cont));
410
411        old_self.lemma_locked_range_vaddr_prefix_match(new_va);
412
413        if old_self.level < old_self.guard_level {
414            old_self.prefix_in_locked_range();
415        }
416    }
417}
418
419} // verus!
ostd/specs/mm/page_table/cursor/va_lemmas.rs

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