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

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