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

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