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

1/// Cursor function-specific lemmas for `CursorOwner`.
2///
3/// Themes moved here from `owners.rs`:
4/// - **Theme 7**: PTE & entry modification invariant preservation
5///   (`protect_preserves_cursor_inv_metaregion`, `map_branch_none_*`)
6/// - **Theme 14**: Cursor path structure & jump utilities
7///   (`cursor_path_nesting`, `jump_above_locked_range_va_in_node`,
8///    `jump_not_in_node_level_lt_guard_minus_one`, `lemma_page_size_spec_5_eq_pow2_48`)
9use vstd::arithmetic::power2::pow2;
10use vstd::prelude::*;
11
12use vstd_extra::ghost_tree::*;
13use vstd_extra::ownership::*;
14
15use vstd_extra::arithmetic::{
16    lemma_nat_align_down_monotone, lemma_nat_align_down_sound, lemma_nat_align_down_within_block,
17    lemma_nat_align_up_sound,
18};
19
20use crate::mm::page_table::*;
21use crate::mm::{PagingLevel, Vaddr};
22use crate::specs::arch::mm::{NR_ENTRIES, NR_LEVELS};
23use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
24use crate::specs::mm::page_table::cursor::owners::{CursorOwner, CursorContinuation};
25use crate::specs::mm::page_table::cursor::page_size_lemmas::{
26    lemma_page_size_divides, lemma_page_size_ge_page_size,
27};
28use crate::specs::mm::page_table::owners::*;
29use crate::specs::mm::page_table::AbstractVaddr;
30use crate::specs::mm::page_table::Mapping;
31use crate::specs::mm::page_table::{nat_align_down, nat_align_up};
32
33use core::ops::Range;
34
35verus! {
36
37impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
38
39    // ─── Theme 7: PTE & entry modification invariant preservation ────────
40
41    pub proof fn protect_preserves_cursor_inv_metaregion(
42        self,
43        other: Self,
44        regions: MetaRegionOwners,
45    )
46        requires
47            self.inv(),
48            self.metaregion_sound(regions),
49            self.cur_entry_owner().is_frame(),
50            other.cur_entry_owner().is_frame(),
51            other.cur_entry_owner().inv(),
52            // protect preserves PA, path, parent_level
53            other.cur_entry_owner().frame.unwrap().mapped_pa == self.cur_entry_owner().frame.unwrap().mapped_pa,
54            other.cur_entry_owner().path == self.cur_entry_owner().path,
55            other.cur_entry_owner().parent_level == self.cur_entry_owner().parent_level,
56            // cursor level and structural fields unchanged
57            self.level == other.level,
58            self.guard_level == other.guard_level,
59            self.va == other.va,
60            self.prefix == other.prefix,
61            self.popped_too_high == other.popped_too_high,
62            // higher-level continuations unchanged
63            forall|i: int| self.level <= i < NR_LEVELS ==>
64                #[trigger] self.continuations[i] == other.continuations[i],
65            // bottom continuation well-formed after protect
66            other.continuations[self.level - 1].inv(),
67            other.continuations[self.level - 1].all_some(),
68            other.continuations[self.level - 1].idx == self.continuations[self.level - 1].idx,
69            other.continuations[self.level - 1].entry_own.parent_level
70                == self.continuations[self.level - 1].entry_own.parent_level,
71            other.continuations[self.level - 1].guard_perm.value().inner.inner@.ptr.addr()
72                == self.continuations[self.level - 1].guard_perm.value().inner.inner@.ptr.addr(),
73            other.continuations[self.level - 1].path()
74                == self.continuations[self.level - 1].path(),
75            other.continuations.dom() =~= self.continuations.dom(),
76            forall |j: int| 0 <= j < NR_ENTRIES
77                && j != self.continuations[self.level - 1].idx as int ==>
78                #[trigger] other.continuations[self.level - 1].children[j]
79                    == self.continuations[self.level - 1].children[j],
80            ({
81                let new_child = other.continuations[self.level - 1].children[
82                    other.continuations[self.level - 1].idx as int].unwrap();
83                let new_path = other.continuations[self.level - 1].path()
84                    .push_tail(other.continuations[self.level - 1].idx as usize);
85                new_child.tree_predicate_map(new_path,
86                    PageTableOwner::<C>::metaregion_sound_pred(regions))
87            }),
88            other.continuations[self.level - 1].entry_own.metaregion_sound(regions),
89        ensures
90            other.inv(),
91            other.metaregion_sound(regions),
92    {
93        other.map_branch_none_inv_holds(self);
94
95        let f = PageTableOwner::<C>::metaregion_sound_pred(regions);
96        let L = self.level as int;
97        let idx = self.continuations[L - 1].idx as int;
98
99        assert forall |i: int| #![trigger other.continuations[i]]
100            other.level - 1 <= i < NR_LEVELS
101        implies
102            other.continuations[i].map_children(f)
103        by {
104            if i > L - 1 {
105                assert(other.continuations[i] == self.continuations[i]);
106                assert(self.continuations[i].map_children(f));
107            } else {
108                assert(i == L - 1);
109                let o_cont = other.continuations[L - 1];
110                let s_cont = self.continuations[L - 1];
111                reveal(CursorContinuation::inv_children);
112                assert forall |j: int| #![trigger o_cont.children[j]]
113                    0 <= j < o_cont.children.len() && o_cont.children[j] is Some
114                implies
115                    o_cont.children[j].unwrap()
116                        .tree_predicate_map(o_cont.path().push_tail(j as usize), f)
117                by {
118                    if j != idx {
119                        assert(o_cont.children[j] == s_cont.children[j]);
120                        s_cont.inv_children_unroll(j);
121                    }
122                };
123            }
124        };
125
126        assert forall |i: int| #![trigger other.continuations[i]]
127            other.level - 1 <= i < NR_LEVELS
128        implies
129            other.continuations[i].entry_own.metaregion_sound(regions)
130        by {
131            if i > L - 1 {
132                assert(other.continuations[i] == self.continuations[i]);
133                self.inv_continuation(i);
134            }
135        };
136    }
137
138    pub proof fn map_branch_none_inv_holds(self, owner0: Self)
139        requires
140            owner0.inv(),
141            self.level == owner0.level,
142            self.va == owner0.va,
143            self.guard_level == owner0.guard_level,
144            self.prefix == owner0.prefix,
145            self.popped_too_high == owner0.popped_too_high,
146            // Higher-level continuations unchanged
147            forall|i: int| self.level <= i < NR_LEVELS ==>
148                #[trigger] self.continuations[i] == owner0.continuations[i],
149            // Bottom continuation is well-formed
150            self.continuations[self.level - 1].inv(),
151            self.continuations[self.level - 1].all_some(),
152            self.continuations[self.level - 1].idx == owner0.continuations[owner0.level - 1].idx,
153            self.continuations[self.level - 1].entry_own.parent_level
154                == owner0.continuations[owner0.level - 1].entry_own.parent_level,
155            // Guard address preserved (from parent_perms_preserved).
156            self.continuations[self.level - 1].guard_perm.value().inner.inner@.ptr.addr()
157                == owner0.continuations[owner0.level - 1].guard_perm.value().inner.inner@.ptr.addr(),
158            self.continuations[self.level - 1].path()
159                == owner0.continuations[owner0.level - 1].path(),
160            self.va.index[self.level - 1] == self.continuations[self.level - 1].idx,
161            // Domain preserved: same keys as owner0.
162            self.continuations.dom() =~= owner0.continuations.dom(),
163        ensures
164            self.inv()
165    {
166        let L = self.level as int;
167        assert(self.continuations[L - 1].level() == self.level) by {
168            assert(self.continuations[L - 1].path() == owner0.continuations[L - 1].path());
169            if L == 1 {} else if L == 2 {} else if L == 3 {} else {}
170        };
171        assert(self.continuations.contains_key(L - 1)) by {
172            if L == 1 {} else if L == 2 {} else if L == 3 {} else {}
173        };
174    }
175
176    /// After alloc_if_none (absent->node), `view_mappings` is unchanged (both contribute zero mappings).
177    pub proof fn map_branch_none_no_new_mappings(self, owner0: Self)
178        requires
179            owner0.inv(),
180            self.inv(),
181            self.level == owner0.level,
182            self.va == owner0.va,
183            forall|i: int| self.level <= i < NR_LEVELS ==>
184                #[trigger] self.continuations[i] == owner0.continuations[i],
185            // child at idx changed from absent to empty node
186            owner0.continuations[owner0.level - 1].children[
187                owner0.continuations[owner0.level - 1].idx as int] is Some,
188            owner0.continuations[owner0.level - 1].children[
189                owner0.continuations[owner0.level - 1].idx as int].unwrap().value.is_absent(),
190            self.continuations[self.level - 1].children[
191                self.continuations[self.level - 1].idx as int] is Some,
192            self.continuations[self.level - 1].children[
193                self.continuations[self.level - 1].idx as int].unwrap().value.is_node(),
194            // Non-idx children and path preserved
195            self.continuations[self.level - 1].path()
196                == owner0.continuations[owner0.level - 1].path(),
197            forall|j: int| 0 <= j < NR_ENTRIES
198                && j != owner0.continuations[owner0.level - 1].idx as int ==>
199                #[trigger] self.continuations[self.level - 1].children[j]
200                    == owner0.continuations[owner0.level - 1].children[j],
201            // The new node's subtree has empty view_rec (from alloc_if_none postcondition)
202            PageTableOwner(self.continuations[self.level - 1].children[
203                self.continuations[self.level - 1].idx as int].unwrap())
204                .view_rec(self.continuations[self.level - 1].path()
205                    .push_tail(self.continuations[self.level - 1].idx as usize))
206                =~= Set::<Mapping>::empty(),
207        ensures
208            self.view_mappings() =~= owner0.view_mappings()
209    {
210        let L = self.level as int;
211        let cont = self.continuations[L - 1];
212        let cont0 = owner0.continuations[L - 1];
213        let idx = cont0.idx as int;
214
215        assert(cont.view_mappings() =~= cont0.view_mappings()) by {
216            cont0.inv_children_unroll(idx);
217            PageTableOwner(cont0.children[idx].unwrap())
218                .view_rec_absent_empty(cont0.path().push_tail(idx as usize));
219            assert forall |m: Mapping| cont.view_mappings().contains(m)
220                implies cont0.view_mappings().contains(m) by {
221                let j = choose|j:int| 0 <= j < cont.children.len()
222                    && #[trigger] cont.children[j] is Some
223                    && PageTableOwner(cont.children[j].unwrap())
224                        .view_rec(cont.path().push_tail(j as usize)).contains(m);
225                if j != idx { assert(cont.children[j] == cont0.children[j]); }
226            };
227            assert forall |m: Mapping| cont0.view_mappings().contains(m)
228                implies cont.view_mappings().contains(m) by {
229                let j = choose|j:int| 0 <= j < cont0.children.len()
230                    && #[trigger] cont0.children[j] is Some
231                    && PageTableOwner(cont0.children[j].unwrap())
232                        .view_rec(cont0.path().push_tail(j as usize)).contains(m);
233                if j != idx { assert(cont0.children[j] == cont.children[j]); }
234            };
235        };
236    }
237
238    /// After `map_branch_none` (alloc_if_none + push_level), the current entry is absent.
239    ///
240    /// Proof: `alloc_if_none` creates an empty PT node where all children are absent
241    /// (`allocated_empty_node_owner` line 172). `push_level` enters one of these children,
242    /// so `cur_entry_owner().is_absent()` holds.
243    pub proof fn map_branch_none_cur_entry_absent(self)
244        requires
245            self.inv(),
246            // All children of the current continuation are absent (from the empty node)
247            forall|i: int| 0 <= i < NR_ENTRIES ==>
248                #[trigger] self.continuations[self.level - 1].children[i] is Some &&
249                self.continuations[self.level - 1].children[i].unwrap().value.is_absent(),
250        ensures
251            self.cur_entry_owner().is_absent(),
252    {
253    }
254
255    pub proof fn cursor_path_nesting(self, i: int, j: int)
256        requires
257            self.inv(),
258            self.level - 1 <= j < i,
259            i < NR_LEVELS,
260        ensures
261            self.continuations[j].path().len() as int > self.continuations[i].path().len() as int,
262            self.continuations[j].path().index(self.continuations[i].path().len() as int)
263                == self.continuations[i].idx,
264    {
265        if i == 3 && j == 2 {
266            self.continuations[3].path().push_tail_property_index(self.continuations[3].idx as usize);
267            self.continuations[3].path().push_tail_property_len(self.continuations[3].idx as usize);
268        } else if i == 3 && j == 1 {
269            let p3 = self.continuations[3].path();
270            let p2 = self.continuations[2].path();
271            let idx3 = self.continuations[3].idx as usize;
272            let idx2 = self.continuations[2].idx as usize;
273            p3.push_tail_property_index(idx3);
274            p3.push_tail_property_len(idx3);
275            p2.push_tail_property_index(idx2);
276            p2.push_tail_property_len(idx2);
277            assert(p3.len() < p2.len());
278            assert(self.continuations[1].path() == p2.push_tail(idx2));
279            assert(p2.push_tail(idx2).index(p3.len() as int) == p2.index(p3.len() as int));
280        } else if i == 3 && j == 0 {
281            let p3 = self.continuations[3].path();
282            let p2 = self.continuations[2].path();
283            let p1 = self.continuations[1].path();
284            let idx3 = self.continuations[3].idx as usize;
285            let idx2 = self.continuations[2].idx as usize;
286            let idx1 = self.continuations[1].idx as usize;
287            p3.push_tail_property_index(idx3);
288            p3.push_tail_property_len(idx3);
289            p2.push_tail_property_index(idx2);
290            p2.push_tail_property_len(idx2);
291            p1.push_tail_property_index(idx1);
292            p1.push_tail_property_len(idx1);
293            assert(p3.len() < p2.len());
294            assert(p3.len() < p1.len());
295            assert(p1.push_tail(idx1).index(p3.len() as int) == p1.index(p3.len() as int));
296            assert(p2.push_tail(idx2).index(p3.len() as int) == p2.index(p3.len() as int));
297        } else if i == 2 && j == 1 {
298            self.continuations[2].path().push_tail_property_index(self.continuations[2].idx as usize);
299            self.continuations[2].path().push_tail_property_len(self.continuations[2].idx as usize);
300        } else if i == 2 && j == 0 {
301            let p2 = self.continuations[2].path();
302            let p1 = self.continuations[1].path();
303            let idx2 = self.continuations[2].idx as usize;
304            let idx1 = self.continuations[1].idx as usize;
305            p2.push_tail_property_index(idx2);
306            p2.push_tail_property_len(idx2);
307            p1.push_tail_property_index(idx1);
308            p1.push_tail_property_len(idx1);
309            assert(p2.len() < p1.len());
310            assert(self.continuations[0].path() == p1.push_tail(idx1));
311            assert(p1.push_tail(idx1).index(p2.len() as int) == p1.index(p2.len() as int));
312            assert(p1 == p2.push_tail(idx2));
313            assert(p2.push_tail(idx2).index(p2.len() as int) == idx2);
314        } else if i == 1 && j == 0 {
315            self.continuations[1].path().push_tail_property_index(self.continuations[1].idx as usize);
316            self.continuations[1].path().push_tail_property_len(self.continuations[1].idx as usize);
317        }
318    }
319
320    pub proof fn lemma_page_size_spec_5_eq_pow2_48()
321        ensures
322            page_size_spec(5) == pow2(48nat) as usize,
323    {
324        crate::specs::arch::paging_consts::lemma_nr_subpage_per_huge_eq_nr_entries();
325        vstd_extra::external::ilog2::lemma_usize_ilog2_to32();
326        vstd::arithmetic::power2::lemma2_to64();
327        vstd::arithmetic::power2::lemma2_to64_rest();
328        vstd::arithmetic::power2::lemma_pow2_adds(12nat, 36nat);
329    }
330
331    pub proof fn jump_not_in_node_level_lt_guard_minus_one(
332        self,
333        level: PagingLevel,
334        va: Vaddr,
335        node_start: Vaddr,
336    )
337        requires
338            self.inv(),
339            self.locked_range().start <= va < self.locked_range().end,
340            1 <= level,
341            level + 1 <= self.guard_level,
342            self.locked_range().start <= node_start,
343            node_start + page_size((level + 1) as PagingLevel) <= self.locked_range().end,
344            !(node_start <= va && va < node_start + page_size((level + 1) as PagingLevel)),
345        ensures
346            level + 1 < self.guard_level,
347    {
348        if level + 1 == self.guard_level {
349            let pv = self.prefix.to_vaddr() as nat;
350            let ps = page_size(self.guard_level as PagingLevel) as nat;
351            self.prefix.align_down_concrete(self.guard_level as int);
352            self.prefix.align_up_concrete(self.guard_level as int);
353            self.prefix.align_diff(self.guard_level as int);
354            AbstractVaddr::from_vaddr_to_vaddr_roundtrip(nat_align_down(pv, ps) as Vaddr);
355            AbstractVaddr::from_vaddr_to_vaddr_roundtrip(nat_align_up(pv, ps) as Vaddr);
356        }
357    }
358}
359
360} // verus!
ostd/specs/mm/page_table/cursor/cursor_fn_lemmas.rs

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