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 crate::mm::page_table::*;
16use crate::mm::{PagingLevel, Vaddr, page_size};
17use crate::specs::arch::*;
18use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
19use crate::specs::mm::page_table::AbstractVaddr;
20use crate::specs::mm::page_table::Mapping;
21use crate::specs::mm::page_table::cursor::owners::{CursorContinuation, CursorOwner};
22
23use crate::specs::mm::page_table::nat_align_down;
24use crate::specs::mm::page_table::owners::*;
25
26use core::ops::Range;
27
28verus! {
29
30impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
31    pub proof fn protect_preserves_cursor_inv_metaregion(
32        self,
33        other: Self,
34        regions: MetaRegionOwners,
35    )
36        requires
37            self.inv(),
38            self.in_locked_range(),
39            !self.popped_too_high,
40            self.metaregion_sound(regions),
41            self.cur_entry_owner().is_frame(),
42            other.cur_entry_owner().is_frame(),
43            other.cur_entry_owner().inv(),
44            // protect preserves PA, path, parent_level
45            other.cur_entry_owner().frame().mapped_pa == self.cur_entry_owner().frame().mapped_pa,
46            other.cur_entry_owner().path == self.cur_entry_owner().path,
47            other.cur_entry_owner().parent_level == self.cur_entry_owner().parent_level,
48            // cursor level and structural fields unchanged
49            self.level == other.level,
50            self.guard_level == other.guard_level,
51            self.va == other.va,
52            self.prefix == other.prefix,
53            self.popped_too_high == other.popped_too_high,
54            // higher-level continuations unchanged
55            forall|i: int|
56                self.level <= i < NR_LEVELS ==> #[trigger] self.continuations[i]
57                    == other.continuations[i],
58            // bottom continuation well-formed after protect
59            other.continuations[self.level - 1].inv(),
60            other.continuations[self.level - 1].all_some(),
61            other.continuations[self.level - 1].idx == self.continuations[self.level - 1].idx,
62            other.continuations[self.level - 1].entry_own.parent_level
63                == self.continuations[self.level - 1].entry_own.parent_level,
64            other.continuations[self.level - 1].guard.inner.inner@.ptr.addr()
65                == self.continuations[self.level - 1].guard.inner.inner@.ptr.addr(),
66            other.continuations[self.level - 1].path() == self.continuations[self.level - 1].path(),
67            other.continuations.dom() =~= self.continuations.dom(),
68            forall|j: int|
69                0 <= j < NR_ENTRIES && j != self.continuations[self.level - 1].idx
70                    ==> #[trigger] other.continuations[self.level - 1].children[j]
71                    == self.continuations[self.level - 1].children[j],
72            ({
73                let new_child = other.continuations[self.level
74                    - 1].children[other.continuations[self.level - 1].idx as int]->0;
75                let new_path = other.continuations[self.level - 1].path().push_tail(
76                    other.continuations[self.level - 1].idx as usize,
77                );
78                new_child.tree_predicate_map(
79                    new_path,
80                    PageTableOwner::<C>::metaregion_sound_pred(regions),
81                )
82            }),
83            other.continuations[self.level - 1].entry_own.metaregion_sound(regions),
84        ensures
85            other.inv(),
86            other.metaregion_sound(regions),
87    {
88        other.map_branch_none_inv_holds(self);
89
90        let f = PageTableOwner::<C>::metaregion_sound_pred(regions);
91        let L = self.level as int;
92        let idx = self.continuations[L - 1].idx as int;
93
94        assert forall|i: int|
95            #![trigger other.continuations[i]]
96            other.level - 1 <= i < NR_LEVELS implies other.continuations[i].map_children(f) by {
97            if i > L - 1 {
98                assert(other.continuations[i] == self.continuations[i]);
99                assert(self.continuations[i].map_children(f));
100            } else {
101                assert(i == L - 1);
102                let o_cont = other.continuations[L - 1];
103                let s_cont = self.continuations[L - 1];
104                reveal(CursorContinuation::inv_children);
105                assert forall|j: int|
106                    #![trigger o_cont.children[j]]
107                    0 <= j < o_cont.children.len()
108                        && o_cont.children[j] is Some implies o_cont.children[j].unwrap().tree_predicate_map(
109                o_cont.path().push_tail(j as usize), f) by {
110                    if j != idx {
111                        assert(o_cont.children[j] == s_cont.children[j]);
112                        s_cont.inv_children_unroll(j);
113                    }
114                };
115            }
116        };
117
118        assert forall|i: int|
119            #![trigger other.continuations[i]]
120            other.level - 1 <= i
121                < NR_LEVELS implies other.continuations[i].entry_own.metaregion_sound(regions) by {
122            if i > L - 1 {
123                assert(other.continuations[i] == self.continuations[i]);
124                self.inv_continuation(i);
125            }
126        };
127    }
128
129    pub proof fn map_branch_none_inv_holds(self, owner0: Self)
130        requires
131            owner0.inv(),
132            // The map happens in the locked range and changes only the current
133            // continuation's slot at `idx` (a real, in-range slot). With this +
134            // "higher continuations unchanged", the root continuation's
135            // isolation clauses are preserved.
136            self.in_locked_range(),
137            !self.popped_too_high,
138            forall|j: int|
139                0 <= j < NR_ENTRIES && j != owner0.continuations[owner0.level - 1].idx ==> (
140                #[trigger] self.continuations[self.level - 1].children[j])
141                    == owner0.continuations[owner0.level - 1].children[j],
142            self.level == owner0.level,
143            self.va == owner0.va,
144            self.guard_level == owner0.guard_level,
145            self.prefix == owner0.prefix,
146            self.popped_too_high == owner0.popped_too_high,
147            // Higher-level continuations unchanged
148            forall|i: int|
149                self.level <= i < NR_LEVELS ==> #[trigger] self.continuations[i]
150                    == owner0.continuations[i],
151            // Bottom continuation is well-formed
152            self.continuations[self.level - 1].inv(),
153            self.continuations[self.level - 1].all_some(),
154            self.continuations[self.level - 1].idx == owner0.continuations[owner0.level - 1].idx,
155            self.continuations[self.level - 1].entry_own.parent_level
156                == owner0.continuations[owner0.level - 1].entry_own.parent_level,
157            // Guard address preserved (from parent_perms_preserved).
158            self.continuations[self.level - 1].guard.inner.inner@.ptr.addr()
159                == owner0.continuations[owner0.level - 1].guard.inner.inner@.ptr.addr(),
160            self.continuations[self.level - 1].path() == owner0.continuations[owner0.level
161                - 1].path(),
162            self.va.index[self.level - 1] == self.continuations[self.level - 1].idx,
163            // Domain preserved: same keys as owner0.
164            self.continuations.dom() =~= owner0.continuations.dom(),
165        ensures
166            self.inv(),
167    {
168        let L = self.level as int;
169        assert(self.continuations[L - 1].level() == self.level);
170        assert(self.continuations.contains_key(L - 1));
171        // Isolation clauses for the root continuation (NR_LEVELS-1).
172        if self.level < NR_LEVELS {
173            // Root is above the current level ⟹ unchanged (higher-unchanged), so
174            // both clauses carry verbatim from `owner0.inv()`.
175            assert(self.continuations[NR_LEVELS - 1] == owner0.continuations[NR_LEVELS - 1]);
176        } else {
177            // Root IS the current continuation. The idx clause is vacuous
178            // (level == NR_LEVELS). For the outside-(borrowed||absent) clause:
179            // the map changed only the in-range slot `idx`, so every outside
180            // child keeps `owner0`'s value; `idx` is in-range (top index in
181            // [start, end), and `in_locked_range` rules out the sentinel).
182            owner0.in_locked_range_top_index_lt_top_end();
183            assert(self.continuations[NR_LEVELS - 1].idx == self.va.index[NR_LEVELS - 1]);
184            assert(self.continuations[NR_LEVELS - 1].idx == owner0.continuations[owner0.level
185                - 1].idx);
186            assert(C::TOP_LEVEL_INDEX_RANGE_spec().start <= owner0.continuations[owner0.level
187                - 1].idx < C::TOP_LEVEL_INDEX_RANGE_spec().end);
188            assert(forall|j: int|
189                0 <= j < NR_ENTRIES && !(C::TOP_LEVEL_INDEX_RANGE_spec().start <= j
190                    < C::TOP_LEVEL_INDEX_RANGE_spec().end) ==> (
191                #[trigger] self.continuations[NR_LEVELS - 1].children[j]) is Some ==> (
192                self.continuations[NR_LEVELS - 1].children[j].unwrap().value.is_borrowed()
193                    || self.continuations[NR_LEVELS - 1].children[j].unwrap().value.is_absent()));
194        }
195    }
196
197    /// After alloc_if_none (absent->node), `view_mappings` is unchanged (both contribute zero mappings).
198    pub proof fn map_branch_none_no_new_mappings(self, owner0: Self)
199        requires
200            owner0.inv(),
201            owner0.in_locked_range(),
202            self.inv(),
203            self.in_locked_range(),
204            self.level == owner0.level,
205            self.va == owner0.va,
206            forall|i: int|
207                self.level <= i < NR_LEVELS ==> #[trigger] self.continuations[i]
208                    == owner0.continuations[i],
209            // child at idx changed from absent to empty node
210            owner0.continuations[owner0.level - 1].children[owner0.continuations[owner0.level
211                - 1].idx as int] is Some,
212            owner0.continuations[owner0.level - 1].children[owner0.continuations[owner0.level
213                - 1].idx as int]->0.value.is_absent(),
214            self.continuations[self.level - 1].children[self.continuations[self.level
215                - 1].idx as int] is Some,
216            self.continuations[self.level - 1].children[self.continuations[self.level
217                - 1].idx as int]->0.value.is_node(),
218            // Non-idx children and path preserved
219            self.continuations[self.level - 1].path() == owner0.continuations[owner0.level
220                - 1].path(),
221            forall|j: int|
222                0 <= j < NR_ENTRIES && j != owner0.continuations[owner0.level - 1].idx as int
223                    ==> #[trigger] self.continuations[self.level - 1].children[j]
224                    == owner0.continuations[owner0.level - 1].children[j],
225            // The new node's subtree has empty view_rec (from alloc_if_none postcondition)
226            PageTableOwner(
227                self.continuations[self.level - 1].children[self.continuations[self.level
228                    - 1].idx as int]->0,
229            ).view_rec(
230                self.continuations[self.level - 1].path().push_tail(
231                    self.continuations[self.level - 1].idx as usize,
232                ),
233            ) =~= Set::<Mapping>::empty(),
234        ensures
235            self.view_mappings() == owner0.view_mappings(),
236    {
237        broadcast use {CursorContinuation::group_lemmas, CursorOwner::group_lemmas};
238
239        let L = self.level as int;
240        let cont = self.continuations[L - 1];
241        let cont0 = owner0.continuations[L - 1];
242        let idx = cont0.idx as int;
243
244        assert(cont.view_mappings() == cont0.view_mappings()) by {
245            cont0.inv_children_unroll(idx);
246            PageTableOwner(cont0.children[idx].unwrap()).view_rec_absent_empty(
247                cont0.path().push_tail(idx as usize),
248            );
249            assert forall|m: Mapping|
250                cont.view_mappings().contains(m) implies cont0.view_mappings().contains(m) by {
251                let j = choose|j: int|
252                    0 <= j < cont.children.len() && #[trigger] cont.children[j] is Some
253                        && PageTableOwner(cont.children[j].unwrap()).view_rec(
254                        cont.path().push_tail(j as usize),
255                    ).contains(m);
256                if j == idx {
257                    // cont.children[idx]'s view_rec == empty (from precondition)
258                    assert(false);
259                } else {
260                    assert(cont.children[j] == cont0.children[j]);
261                }
262            };
263            assert forall|m: Mapping|
264                cont0.view_mappings().contains(m) implies cont.view_mappings().contains(m) by {
265                let j = choose|j: int|
266                    0 <= j < cont0.children.len() && #[trigger] cont0.children[j] is Some
267                        && PageTableOwner(cont0.children[j].unwrap()).view_rec(
268                        cont0.path().push_tail(j as usize),
269                    ).contains(m);
270                if j == idx {
271                    // cont0.children[idx] is absent, view_rec is empty
272                    assert(false);
273                } else {
274                    assert(cont0.children[j] == cont.children[j]);
275                }
276            };
277        };
278        // Lift cont == cont0 to self.view_mappings() == owner0.view_mappings()
279        assert(self.view_mappings() == owner0.view_mappings()) by {
280            assert forall|m: Mapping|
281                self.view_mappings().contains(m) implies owner0.view_mappings().contains(m) by {
282                let i = choose|i: int|
283                    self.level - 1 <= i < NR_LEVELS
284                        && #[trigger] self.continuations[i].view_mappings().contains(m);
285                if i == L - 1 {
286                    assert(cont0.view_mappings().contains(m));
287                } else {
288                    assert(owner0.continuations[i] == self.continuations[i]);
289                }
290            };
291            assert forall|m: Mapping|
292                owner0.view_mappings().contains(m) implies self.view_mappings().contains(m) by {
293                let i = choose|i: int|
294                    owner0.level - 1 <= i < NR_LEVELS
295                        && #[trigger] owner0.continuations[i].view_mappings().contains(m);
296                if i == L - 1 {
297                    assert(cont.view_mappings().contains(m));
298                } else {
299                    assert(self.continuations[i] == owner0.continuations[i]);
300                }
301            };
302        };
303    }
304
305    /// After `map_branch_none` (alloc_if_none + push_level), the current entry is absent.
306    ///
307    /// Proof: `alloc_if_none` creates an empty PT node where all children are absent
308    /// (`allocated_empty_node_owner` line 172). `push_level` enters one of these children,
309    /// so `cur_entry_owner().is_absent()` holds.
310    pub proof fn map_branch_none_cur_entry_absent(self)
311        requires
312            self.inv(),
313            // All children of the current continuation are absent (from the empty node)
314            forall|i: int|
315                0 <= i < NR_ENTRIES ==> #[trigger] self.continuations[self.level
316                    - 1].children[i] is Some && self.continuations[self.level
317                    - 1].children[i]->0.value.is_absent(),
318        ensures
319            self.cur_entry_owner().is_absent(),
320    {
321    }
322
323    pub proof fn cursor_path_nesting(self, i: int, j: int)
324        requires
325            self.inv(),
326            self.level - 1 <= j < i,
327            i < NR_LEVELS,
328        ensures
329            self.continuations[j].path().len() as int > self.continuations[i].path().len(),
330            self.continuations[j].path().index(self.continuations[i].path().len() as int)
331                == self.continuations[i].idx,
332    {
333        if i == 3 && j == 2 {
334            self.continuations[3].path().push_tail_property_index(
335                self.continuations[3].idx as usize,
336            );
337            self.continuations[3].path().push_tail_property_len(self.continuations[3].idx as usize);
338        } else if i == 3 && j == 1 {
339            let p3 = self.continuations[3].path();
340            let p2 = self.continuations[2].path();
341            let idx3 = self.continuations[3].idx as usize;
342            let idx2 = self.continuations[2].idx as usize;
343            p3.push_tail_property_index(idx3);
344            p3.push_tail_property_len(idx3);
345            p2.push_tail_property_index(idx2);
346            p2.push_tail_property_len(idx2);
347            assert(p3.len() < p2.len());
348            assert(self.continuations[1].path() == p2.push_tail(idx2));
349            assert(p2.push_tail(idx2).index(p3.len() as int) == p2.index(p3.len() as int));
350        } else if i == 3 && j == 0 {
351            let p3 = self.continuations[3].path();
352            let p2 = self.continuations[2].path();
353            let p1 = self.continuations[1].path();
354            let idx3 = self.continuations[3].idx as usize;
355            let idx2 = self.continuations[2].idx as usize;
356            let idx1 = self.continuations[1].idx as usize;
357            p3.push_tail_property_index(idx3);
358            p3.push_tail_property_len(idx3);
359            p2.push_tail_property_index(idx2);
360            p2.push_tail_property_len(idx2);
361            p1.push_tail_property_index(idx1);
362            p1.push_tail_property_len(idx1);
363            assert(p3.len() < p2.len());
364            assert(p3.len() < p1.len());
365            assert(p1.push_tail(idx1).index(p3.len() as int) == p1.index(p3.len() as int));
366            assert(p2.push_tail(idx2).index(p3.len() as int) == p2.index(p3.len() as int));
367        } else if i == 2 && j == 1 {
368            self.continuations[2].path().push_tail_property_index(
369                self.continuations[2].idx as usize,
370            );
371            self.continuations[2].path().push_tail_property_len(self.continuations[2].idx as usize);
372        } else if i == 2 && j == 0 {
373            let p2 = self.continuations[2].path();
374            let p1 = self.continuations[1].path();
375            let idx2 = self.continuations[2].idx as usize;
376            let idx1 = self.continuations[1].idx as usize;
377            p2.push_tail_property_index(idx2);
378            p2.push_tail_property_len(idx2);
379            p1.push_tail_property_index(idx1);
380            p1.push_tail_property_len(idx1);
381            assert(p2.len() < p1.len());
382            assert(self.continuations[0].path() == p1.push_tail(idx1));
383            assert(p1.push_tail(idx1).index(p2.len() as int) == p1.index(p2.len() as int));
384            assert(p1 == p2.push_tail(idx2));
385            assert(p2.push_tail(idx2).index(p2.len() as int) == idx2);
386        } else if i == 1 && j == 0 {
387            self.continuations[1].path().push_tail_property_index(
388                self.continuations[1].idx as usize,
389            );
390            self.continuations[1].path().push_tail_property_len(self.continuations[1].idx as usize);
391        }
392    }
393
394    pub proof fn lemma_page_size_spec_5_eq_pow2_48()
395        ensures
396            page_size(5) == pow2(48nat) as usize,
397    {
398        crate::arch::mm::lemma_nr_subpage_per_huge_eq_nr_entries();
399        vstd_extra::external::ilog2::lemma_usize_ilog2_to32();
400        vstd::arithmetic::power2::lemma2_to64();
401        vstd::arithmetic::power2::lemma2_to64_rest();
402        vstd::arithmetic::power2::lemma_pow2_adds(12nat, 36nat);
403    }
404
405    pub proof fn jump_not_in_node_level_lt_guard_minus_one(
406        self,
407        level: PagingLevel,
408        va: Vaddr,
409        node_start: Vaddr,
410    )
411        requires
412            self.inv(),
413            self.locked_range().start <= va < self.locked_range().end,
414            1 <= level,
415            level + 1 <= self.guard_level,
416            self.locked_range().start <= node_start,
417            node_start + page_size((level + 1) as PagingLevel) <= self.locked_range().end,
418            !(node_start <= va && va < node_start + page_size((level + 1) as PagingLevel)),
419        ensures
420            level + 1 < self.guard_level,
421    {
422        if level + 1 == self.guard_level {
423            let pv = self.prefix.to_vaddr() as nat;
424            let ps = page_size(self.guard_level as PagingLevel) as nat;
425            self.prefix.align_down_concrete(self.guard_level as int);
426            self.prefix_aligned_to_guard_level();
427            self.prefix_plus_ps_no_overflow();
428            self.prefix.aligned_align_up_advances(self.guard_level as int);
429            AbstractVaddr::from_vaddr_to_vaddr_roundtrip(nat_align_down(pv, ps) as Vaddr);
430        }
431    }
432}
433
434} // verus!
ostd/specs/mm/page_table/cursor/cursor_fn_lemmas.rs

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