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`).
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 concrete VA to the page table view range.
10/// - Specifications and proofs for repositioning the cursor inside its current node.
11use vstd::prelude::*;
12use vstd_extra::{arithmetic::nat_align_down, ghost_tree::*, ownership::*};
13
14use crate::specs::{
15    arch::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE},
16    mm::page_table::{
17        Mapping,
18        cursor::{
19            owners::{CursorContinuation, CursorOwner},
20            page_size_lemmas::{
21                lemma_page_size_divides, lemma_page_size_ge_base, lemma_page_size_spec_values,
22            },
23        },
24        lemma_align_down_indices, lemma_inc_slot_indices, lemma_pte_index_bound,
25        lemma_same_node_pte_indices_match,
26        owners::*,
27        pte_index_spec, vaddr_replace_pte_index_spec, vaddr_upper_bits_spec,
28    },
29};
30
31use crate::arch::mm::PagingConsts;
32use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr, page_size, page_table::*};
33use crate::specs::task::InAtomicMode;
34use core::ops::Range;
35
36verus! {
37
38broadcast use group_ghost_tree_lemmas;
39
40impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
41    pub open spec fn zero_below_level(self) -> Self
42        recommends
43            1 <= self.level <= C::NR_LEVELS(),
44    {
45        Self {
46            va: nat_align_down(self.va as nat, page_size::<C>(self.level) as nat) as Vaddr,
47            ..self
48        }
49    }
50
51    pub open spec fn cur_va(self) -> Vaddr {
52        self.va
53    }
54
55    pub open spec fn prefix_vaddr(self) -> Vaddr {
56        self.prefix
57    }
58
59    pub open spec fn cur_va_range(self) -> Range<Vaddr> {
60        let size = page_size::<PagingConsts>(self.level);
61        let start = nat_align_down(self.cur_va() as nat, size as nat) as Vaddr;
62        Range { start, end: (start + size) as Vaddr }
63    }
64
65    pub open spec fn set_va_in_node(self, new_va: Vaddr) -> Self {
66        let old_cont = self.continuations[self.level - 1];
67        Self {
68            va: new_va,
69            continuations: self.continuations.insert(
70                self.level - 1,
71                CursorContinuation { idx: pte_index_spec::<C>(new_va, self.level), ..old_cont },
72            ),
73            // Repositioning to a concrete in-range VA clears the
74            // transient `popped_too_high` state.
75            popped_too_high: false,
76            ..self
77        }
78    }
79
80    pub proof fn do_zero_below_level(tracked &mut self)
81        requires
82            old(self).inv(),
83            old(self).level <= old(self).guard_level,
84        ensures
85            *final(self) == old(self).zero_below_level(),
86            final(self).inv(),
87    {
88        let ghost old_self = *self;
89        C::lemma_paging_consts_properties();
90        lemma_align_down_indices::<C>(old_self.va, old_self.level);
91        self.va = old_self.zero_below_level().va;
92
93        old_self.lemma_locked_range_span();
94        lemma_page_size_ge_base::<PagingConsts>(old_self.level as PagingLevel);
95        lemma_page_size_ge_base::<PagingConsts>(old_self.guard_level as PagingLevel);
96        lemma_page_size_divides::<PagingConsts>(
97            old_self.level as PagingLevel,
98            old_self.guard_level as PagingLevel,
99        );
100        let ghost old_va_val = old_self.va as nat;
101        let ghost prefix_va_val = old_self.prefix as nat;
102        let ghost ps = page_size::<PagingConsts>(old_self.level as PagingLevel) as nat;
103        let ghost guard_ps = page_size::<PagingConsts>(old_self.guard_level as PagingLevel) as nat;
104        let ghost start = old_self.locked_range().start as nat;
105
106        vstd_extra::arithmetic::lemma_nat_align_down_monotone(prefix_va_val, ps, guard_ps);
107        vstd_extra::arithmetic::lemma_mod_0_add(start as int, guard_ps as int, ps as int);
108
109        vstd_extra::arithmetic::lemma_nat_align_down_sound(old_va_val, ps);
110        if !self.popped_too_high && (self.in_locked_range() || self.level < self.guard_level) {
111            if self.level == self.guard_level {
112                let new_va_val = self.va as nat;
113                let diff = (new_va_val - start) as nat;
114                vstd::arithmetic::div_mod::lemma_mod_equivalence(
115                    new_va_val as int,
116                    start as int,
117                    ps as int,
118                );
119                vstd::arithmetic::div_mod::lemma_small_mod(diff, ps);
120            }
121        }
122    }
123
124    pub proof fn zero_preserves_all_but_va(self)
125        ensures
126            self.zero_below_level().level == self.level,
127            self.zero_below_level().continuations == self.continuations,
128            self.zero_below_level().guard_level == self.guard_level,
129            self.zero_below_level().prefix == self.prefix,
130            self.zero_below_level().popped_too_high == self.popped_too_high,
131    {
132    }
133
134    /// Incrementing the selected nonterminal entry advances by one slot without overflow.
135    pub proof fn lemma_inc_index_va(self)
136        requires
137            self.inv(),
138            self.in_locked_range(),
139            self.index() + 1 < NR_ENTRIES,
140        ensures
141            self.inc_index().va == self.va + page_size::<C>(self.level),
142    {
143        C::lemma_paging_consts_properties();
144        self.lemma_cur_pte_index();
145        lemma_inc_slot_indices::<C>(self.va, self.level);
146        reveal(vaddr_replace_pte_index_spec);
147        vstd::arithmetic::mul::lemma_mul_basics(page_size::<C>(self.level) as int);
148    }
149
150    /// Incrementing a nonterminal index and aligning down reaches the next slot boundary.
151    pub proof fn inc_and_zero_increases_va(self)
152        requires
153            self.inv(),
154            self.in_locked_range(),
155            self.index() + 1 < NR_ENTRIES,
156        ensures
157            self.inc_index().zero_below_level().va > self.va,
158            self.inc_index().zero_below_level().va == self@.align_up_spec(
159                page_size::<PagingConsts>(self.level),
160            ),
161    {
162        C::lemma_paging_consts_properties();
163        self.lemma_inc_index_va();
164        lemma_page_size_ge_base::<PagingConsts>(self.level);
165        let ps = page_size::<PagingConsts>(self.level) as nat;
166        let va = self.va as nat;
167        vstd_extra::arithmetic::lemma_nat_align_down_sound(va, ps);
168        vstd::arithmetic::div_mod::lemma_mod_add_multiples_vanish(va as int, ps as int);
169        vstd::arithmetic::div_mod::lemma_fundamental_div_mod(va as int, ps as int);
170    }
171
172    /// The current subtree starts at the cursor's aligned slot boundary and contains its VA.
173    pub proof fn cur_va_in_subtree_range(self)
174        requires
175            self.inv(),
176            self.in_locked_range(),
177        ensures
178            vaddr_of::<C>(self.cur_subtree().value().path) <= self.cur_va() < vaddr_of::<C>(
179                self.cur_subtree().value().path,
180            ) + page_size::<PagingConsts>(self.level),
181            vaddr_of::<C>(self.cur_subtree().value().path) == nat_align_down(
182                self.cur_va() as nat,
183                page_size::<PagingConsts>(self.level) as nat,
184            ),
185    {
186        self.cur_va_in_cont_child_range(self.level - 1);
187    }
188
189    /// Addresses in the locked block share the guard-level and higher indices.
190    pub proof fn lemma_locked_range_vaddr_prefix_match(self, new_va: Vaddr)
191        requires
192            self.inv(),
193            new_va % C::BASE_PAGE_SIZE() == 0,
194            vaddr_upper_bits_spec::<C>(new_va) == vaddr_upper_bits_spec::<C>(self.prefix_vaddr()),
195            self.locked_range().start <= new_va < self.locked_range().end,
196        ensures
197            pte_index_spec::<C>(new_va, self.guard_level) == pte_index_spec::<C>(
198                self.prefix,
199                self.guard_level,
200            ),
201            forall|i: int|
202                self.guard_level - 1 <= i < C::NR_LEVELS() ==> (#[trigger] pte_index_spec::<C>(
203                    new_va,
204                    (i + 1) as PagingLevel,
205                )) == pte_index_spec::<C>(self.prefix_vaddr(), (i + 1) as PagingLevel),
206    {
207        C::lemma_paging_consts_properties();
208        self.lemma_locked_range_span();
209        let gl = self.guard_level;
210        if gl == 1 {
211            lemma_page_size_spec_values();
212            let ps = C::BASE_PAGE_SIZE() as int;
213            let diff = new_va - self.prefix;
214            vstd::arithmetic::div_mod::lemma_mod_equivalence(new_va as int, self.prefix as int, ps);
215            vstd::arithmetic::div_mod::lemma_small_mod(diff as nat, ps as nat);
216            assert(new_va == self.prefix);
217        } else {
218            lemma_same_node_pte_indices_match::<C>(
219                new_va,
220                self.prefix,
221                self.prefix,
222                (gl - 1) as PagingLevel,
223            );
224        }
225    }
226
227    /// The entry selected by the cursor's concrete VA is the entry owned by its current
228    /// continuation. This is the architecture-parameterized replacement for exposing the
229    /// decomposed address stored in `CursorOwner`.
230    pub proof fn lemma_cur_pte_index(self)
231        requires
232            self.inv(),
233            self.in_locked_range(),
234        ensures
235            1 <= self.level <= C::NR_LEVELS(),
236            pte_index_spec::<C>(self.cur_va(), self.level) == self.continuations[self.level
237                - 1].idx,
238            pte_index_spec::<C>(self.cur_va(), self.level) < NR_ENTRIES,
239    {
240        C::lemma_paging_consts_properties();
241        lemma_pte_index_bound::<C>(self.cur_va(), self.level);
242    }
243
244    /// Architecture-parameterized entry point for repositioning a cursor inside its current
245    /// page-table node.
246    pub proof fn tracked_set_vaddr_in_node(tracked &mut self, new_va: Vaddr)
247        requires
248            old(self).inv(),
249            new_va % C::BASE_PAGE_SIZE() == 0,
250            vaddr_upper_bits_spec::<C>(new_va) == vaddr_upper_bits_spec::<C>(old(self).cur_va()),
251            forall|i: int|
252                old(self).level <= i < C::NR_LEVELS() ==> (#[trigger] pte_index_spec::<C>(
253                    new_va,
254                    (i + 1) as PagingLevel,
255                )) == pte_index_spec::<C>(old(self).cur_va(), (i + 1) as PagingLevel),
256            old(self).locked_range().start <= new_va < old(self).locked_range().end,
257            old(self).level <= old(self).guard_level,
258        ensures
259            *final(self) == old(self).set_va_in_node(new_va),
260            final(self).inv(),
261    {
262        let ghost old_self = *self;
263        C::lemma_paging_consts_properties();
264        lemma_pte_index_bound::<C>(new_va, old_self.level);
265        let tracked mut cont = self.continuations.tracked_remove(self.level - 1);
266        cont.idx = pte_index_spec::<C>(new_va, old_self.level);
267        self.continuations.tracked_insert(self.level - 1, cont);
268        self.va = new_va;
269        self.popped_too_high = false;
270        assert(self.continuations == old_self.continuations.insert(old_self.level - 1, cont));
271        old_self.lemma_locked_range_vaddr_prefix_match(new_va);
272        if old_self.level < old_self.guard_level {
273            old_self.lemma_prefix_in_locked_range();
274        }
275    }
276}
277
278impl<'rcu, C: PageTableConfig, A: InAtomicMode> Cursor<'rcu, C, A> {
279    /// Connects the executable cursor address to the architecture-parameterized index owned by
280    /// its ghost continuation, without exposing the owner's decomposed address representation.
281    pub proof fn lemma_pte_index_matches_owner(self, owner: CursorOwner<'rcu, C>)
282        requires
283            self.wf(owner),
284            owner.inv(),
285            owner.in_locked_range(),
286        ensures
287            1 <= self.level <= C::NR_LEVELS(),
288            pte_index_spec::<C>(self.va, self.level) == owner.continuations[owner.level - 1].idx,
289            pte_index_spec::<C>(self.va, self.level) < NR_ENTRIES,
290    {
291        owner.lemma_cur_pte_index();
292    }
293}
294
295} // verus!
ostd/specs/mm/page_table/cursor/va_lemmas.rs

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