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

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