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

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