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

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