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

1/// Tree-predicate lifting, tree entry level constraints, and tree membership
2/// lemmas for `CursorContinuation` and `CursorOwner`.
3///
4/// Themes moved here from `owners.rs`:
5/// - **Theme 5**: Tree predicate lifting (`map_children_lift`, `map_children_implies`, etc.)
6/// - **Theme 11**: Tree entry level constraints (`cur_entry_node_implies_level_gt_1`, etc.)
7/// - **Theme 12**: Tree membership & tracking (`absent_not_in_tree`)
8use vstd::prelude::*;
9
10use vstd_extra::ghost_tree::*;
11use vstd_extra::ownership::*;
12
13use crate::mm::page_table::*;
14use crate::mm::page_prop::PageProperty;
15use crate::mm::{Paddr, PagingLevel, Vaddr};
16use crate::specs::arch::mm::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE};
17use crate::mm::frame::meta::mapping::frame_to_index;
18use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
19use crate::specs::mm::page_table::cursor::owners::{CursorContinuation, CursorOwner};
20use crate::specs::mm::page_table::node::entry_owners::EntryOwner;
21use crate::specs::mm::page_table::node::GuardPerm;
22use crate::specs::mm::page_table::owners::*;
23use crate::specs::mm::page_table::AbstractVaddr;
24use crate::specs::mm::page_table::Mapping;
25
26use core::ops::Range;
27
28verus! {
29
30// ─── Tree predicate lifting (CursorContinuation) ───────────────────
31
32impl<'rcu, C: PageTableConfig> CursorContinuation<'rcu, C> {
33
34    /// Lift map_children(f) to map_children(g) when implies(f, g).
35    pub proof fn map_children_lift(
36        self,
37        f: spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool,
38        g: spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool,
39    )
40        requires
41            self.inv(),
42            self.map_children(f),
43            OwnerSubtree::implies(f, g),
44        ensures
45            self.map_children(g),
46    {
47        assert forall|j: int|
48            #![auto]
49            0 <= j < self.children.len()
50                && self.children[j] is Some implies
51                self.children[j].unwrap().tree_predicate_map(
52                    self.path().push_tail(j as usize), g)
53        by {
54            self.inv_children_unroll(j);
55            OwnerSubtree::map_implies(
56                self.children[j].unwrap(),
57                self.path().push_tail(j as usize),
58                f, g,
59            );
60        };
61    }
62
63    /// Lift map_children from f to g when siblings (j != idx) come from
64    /// cont0 which had map_children(f), and the child at idx (if present)
65    /// already satisfies g.
66    pub proof fn map_children_lift_skip_idx(
67        self,
68        cont0: Self,
69        idx: int,
70        f: spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool,
71        g: spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool,
72    )
73        requires
74            0 <= idx < NR_ENTRIES,
75            OwnerSubtree::implies(f, g),
76            cont0.inv(),
77            cont0.map_children(f),
78            self.path() == cont0.path(),
79            self.children.len() == cont0.children.len(),
80            forall|j: int| #![auto]
81                0 <= j < NR_ENTRIES && j != idx ==>
82                self.children[j] == cont0.children[j],
83            self.children[idx] is Some ==>
84                self.children[idx].unwrap().tree_predicate_map(
85                    self.path().push_tail(idx as usize), g),
86        ensures
87            self.map_children(g),
88    {
89        assert forall|j: int|
90            #![auto]
91            0 <= j < self.children.len()
92                && self.children[j] is Some implies
93                self.children[j].unwrap().tree_predicate_map(
94                    self.path().push_tail(j as usize), g)
95        by {
96            if j != idx {
97                cont0.inv_children_unroll(j);
98                OwnerSubtree::map_implies(
99                    cont0.children[j].unwrap(),
100                    cont0.path().push_tail(j as usize), f, g);
101            }
102        };
103    }
104
105    pub proof fn as_subtree_restore(self, child: Self)
106        requires
107            self.inv(),
108            child.inv(),
109            self.all_but_index_some(),
110            child.all_some(),
111        ensures
112            self.restore_spec(child).0.as_subtree() ==
113            self.put_child_spec(child.as_subtree()).as_subtree(),
114    {
115        assert(self.put_child_spec(child.as_subtree()).children ==
116        self.children.update(self.idx as int, Some(child.as_subtree())));
117    }
118}
119
120// ─── Tree predicate lifting (CursorOwner) ──────────────────────────
121
122impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
123
124    pub proof fn map_children_implies(
125        self,
126        f: spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool,
127        g: spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool,
128    )
129    requires
130        self.inv(),
131        OwnerSubtree::implies(f, g),
132        forall|i: int|
133            #![trigger self.continuations[i]]
134                self.level - 1 <= i < NR_LEVELS ==>
135                    self.continuations[i].map_children(f),
136    ensures
137        forall|i: int|
138            #![trigger self.continuations[i]]
139            self.level - 1 <= i < NR_LEVELS ==>
140                self.continuations[i].map_children(g),
141    {
142        assert forall|i: int|
143            #![trigger self.continuations[i]]
144            self.level - 1 <= i < NR_LEVELS implies self.continuations[i].map_children(g) by {
145                let cont = self.continuations[i];
146                reveal(CursorContinuation::inv_children);
147                assert forall|j: int|
148                    #![trigger cont.children[j]]
149                    0 <= j < cont.children.len() && cont.children[j] is Some
150                        implies cont.children[j].unwrap().tree_predicate_map(cont.path().push_tail(j as usize), g) by {
151                            cont.inv_children_unroll(j);
152                            OwnerSubtree::map_implies(cont.children[j].unwrap(), cont.path().push_tail(j as usize), f, g);
153                    }
154            }
155    }
156
157    // ─── Tree entry level constraints ──────────────────────────
158
159    pub proof fn cur_entry_node_implies_level_gt_1(self)
160        requires
161            self.inv(),
162            self.cur_entry_owner().is_node(),
163        ensures
164            self.level > 1,
165    {
166        self.cur_subtree_inv();
167        let cont = self.continuations[self.level - 1];
168        let child = self.cur_subtree();
169        assert(child.level < INC_LEVELS - 1);
170        assert(cont.level() == self.level) by {
171            if self.level == 1 {} else if self.level == 2 {} else if self.level == 3 {} else {}
172        };
173    }
174
175    /// A frame entry at the cursor's current level that doesn't fit the aligned range
176    /// `[cur_va, end)` must be at level > 1.
177    /// Justification: At level 1, `page_size(1) == BASE_PAGE_SIZE`. Since the cursor VA
178    /// and `end` are BASE_PAGE_SIZE-aligned and `cur_va < end`, we have
179    /// `cur_va + page_size(1) <= end`, so a level-1 frame always fits. Therefore
180    /// `!cur_entry_fits_range` implies `level > 1`.
181    pub proof fn frame_not_fits_implies_level_gt_1(
182        self,
183        cur_entry_fits_range: bool,
184        cur_va: Vaddr,
185        end: Vaddr,
186    )
187        requires
188            self.inv(),
189            self.cur_entry_owner().is_frame(),
190            !cur_entry_fits_range,
191            cur_va < end,
192            // cur_va is the cursor's current VA (from the call site: cur_va == self.va).
193            cur_va == self.cur_va(),
194            // Definition: cur_entry_fits_range iff cur_va is at start of entry AND entry end <= end.
195            cur_entry_fits_range == (
196                cur_va == self.cur_va_range().start.to_vaddr()
197                && self.cur_va_range().end.to_vaddr() <= end),
198            // cur_va and end are PAGE_SIZE-aligned
199            cur_va as nat % PAGE_SIZE as nat == 0,
200            end as nat % PAGE_SIZE as nat == 0,
201        ensures
202            self.level > 1
203    {
204        // At level 1, page_size(1) == PAGE_SIZE. cursor inv gives va.offset == 0,
205        // so align_down(va, PAGE_SIZE) == va. The range is [va, va + PAGE_SIZE).
206        // cur_va == va (precondition) and cur_va + PAGE_SIZE <= end (from alignment
207        // and cur_va < end). Hence cur_entry_fits_range == true, contradicting
208        // !cur_entry_fits_range.
209        if self.level == 1 {
210            crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_page_size_spec_level1();
211            self.va.align_down_concrete(1);
212            self.va.align_up_concrete(1);
213            self.va.align_diff(1);
214        }
215    }
216
217    // ─── Tree membership & tracking ────────────────────────────
218
219    pub open spec fn not_in_tree(self, owner: EntryOwner<C>) -> bool {
220        self.map_full_tree(|owner0: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
221            owner0.meta_slot_paddr_neq(owner))
222    }
223
224    pub proof fn absent_not_in_tree(self, owner: EntryOwner<C>)
225        requires
226            self.inv(),
227            owner.inv(),
228            owner.is_absent(),
229        ensures
230            self.not_in_tree(owner),
231    {
232        let g = |e: EntryOwner<C>, p: TreePath<NR_ENTRIES>| e.meta_slot_paddr_neq(owner);
233        let nsp = PageTableOwner::<C>::not_in_scope_pred();
234        assert(OwnerSubtree::implies(nsp, g)) by {
235            assert forall |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
236                entry.inv() && !entry.in_scope implies #[trigger] g(entry, path) by {};
237        };
238        assert forall |i: int| #![trigger self.continuations[i]]
239            self.level - 1 <= i < NR_LEVELS implies self.continuations[i].map_children(g)
240        by {
241            let cont = self.continuations[i];
242            reveal(CursorContinuation::inv_children);
243            assert forall |j: int| 0 <= j < NR_ENTRIES
244                && #[trigger] cont.children[j] is Some implies
245                cont.children[j].unwrap().tree_predicate_map(cont.path().push_tail(j as usize), g)
246            by {
247                cont.inv_children_unroll(j);
248                PageTableOwner::tree_not_in_scope(cont.children[j].unwrap(), cont.path().push_tail(j as usize));
249                cont.children[j].unwrap().map_implies(cont.path().push_tail(j as usize), nsp, g);
250            };
251        };
252    }
253
254}
255
256} // verus!
ostd/specs/mm/page_table/cursor/tree_lemmas.rs

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