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

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