ostd/specs/mm/page_table/
owners.rs

1use vstd::prelude::*;
2
3use core::ops::Range;
4
5use vstd::arithmetic::power2::pow2;
6use vstd::seq::*;
7use vstd::seq_lib::*;
8use vstd::set_lib::*;
9use vstd_extra::array_ptr;
10use vstd_extra::cast_ptr::Repr;
11use vstd_extra::drop_tracking::*;
12use vstd_extra::ghost_tree::*;
13use vstd_extra::ownership::*;
14use vstd_extra::prelude::TreeNodeValue;
15
16use crate::mm::{page_table::EntryOwner, Paddr, PagingLevel, Vaddr, MAX_NR_LEVELS};
17
18use crate::mm::frame::frame_to_index;
19use crate::mm::page_table::{page_size_spec, PageTableEntryTrait, PageTableGuard};
20
21use crate::specs::arch::*;
22use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
23use crate::specs::mm::page_table::*;
24use crate::specs::mm::page_table::cursor::page_size_lemmas::{
25    lemma_page_size_divides, lemma_page_size_ge_page_size,
26};
27
28use core::ops::Deref;
29
30verus! {
31
32#[verifier::inline]
33pub open spec fn vaddr_shift_bits<const L: usize>(idx: int) -> nat
34    recommends
35        0 < L,
36        idx < L,
37{
38    (12 + 9 * (L - 1 - idx)) as nat
39}
40
41#[verifier::inline]
42pub open spec fn vaddr_shift<const L: usize>(idx: int) -> usize
43    recommends
44        0 < L,
45        idx < L,
46{
47    pow2(vaddr_shift_bits::<L>(idx)) as usize
48}
49
50#[verifier::inline]
51pub open spec fn vaddr_make<const L: usize>(idx: int, offset: usize) -> usize
52    recommends
53        0 < L,
54        idx < L,
55        0 <= offset < 512,
56{
57    (vaddr_shift::<L>(idx) * offset) as usize
58}
59
60pub open spec fn rec_vaddr(
61    path: TreePath<NR_ENTRIES>,
62    idx: int,
63) -> usize/*        recommends
64        0 < NR_LEVELS,
65        path.len() <= NR_LEVELS,
66        0 <= idx <= path.len(),*/
67
68    decreases path.len() - idx,
69    when 0 <= idx <= path.len()
70{
71    if idx == path.len() {
72        0
73    } else {
74        let offset: usize = path.index(idx);
75        (vaddr_make::<NR_LEVELS>(idx, offset) + rec_vaddr(path, idx + 1)) as usize
76    }
77}
78
79pub open spec fn vaddr(path: TreePath<NR_ENTRIES>) -> usize {
80    rec_vaddr(path, 0)
81}
82
83/// page_size is monotonically increasing in its argument.
84pub proof fn page_size_monotonic(a: PagingLevel, b: PagingLevel)
85    requires
86        1 <= a <= NR_LEVELS + 1,
87        1 <= b <= NR_LEVELS + 1,
88        a <= b,
89    ensures
90        page_size(a) <= page_size(b),
91{
92    if a == b {
93    } else {
94        let ps_a = page_size(a);
95        let ps_b = page_size(b);
96
97        assert(ps_a == page_size_spec(a));
98        assert(ps_b == page_size_spec(b));
99
100        lemma_page_size_ge_page_size(a);
101        lemma_page_size_ge_page_size(b);
102        assert(ps_a > 0);
103        assert(ps_b > 0);
104
105        lemma_page_size_divides(a, b);
106        assert(ps_b % ps_a == 0);
107
108        assert(ps_a <= ps_b) by {
109            if ps_b < ps_a {
110                vstd::arithmetic::div_mod::lemma_small_mod(ps_b as nat, ps_a as nat);
111                assert(ps_b % ps_a == ps_b);
112                assert(ps_b % ps_a == 0);
113                assert(false);
114            }
115        }
116    }
117}
118
119/// Sibling paths (same prefix, different last index) have disjoint VA ranges.
120/// This is a fundamental property of page table virtual address layout:
121/// each entry at a given level covers a distinct, non-overlapping range.
122pub proof fn sibling_paths_disjoint(
123    prefix: TreePath<NR_ENTRIES>,
124    j: usize,
125    k: usize,
126    size: usize,
127)
128    requires
129        j < NR_ENTRIES,
130        k < NR_ENTRIES,
131        j != k,
132        size == page_size((INC_LEVELS - prefix.len()) as PagingLevel),
133    ensures
134        vaddr(prefix.push_tail(j)) + size <= vaddr(prefix.push_tail(k))
135        || vaddr(prefix.push_tail(k)) + size <= vaddr(prefix.push_tail(j)),
136{
137    admit()
138}
139
140impl<C: PageTableConfig, const L: usize> TreeNodeValue<L> for EntryOwner<C> {
141    open spec fn default(lv: nat) -> Self {
142        Self {
143            in_scope: false,
144            path: TreePath::new(Seq::empty()),
145            parent_level: (INC_LEVELS - lv) as PagingLevel,
146            node: None,
147            frame: None,
148            locked: None,
149            absent: true,
150        }
151    }
152
153    proof fn default_preserves_inv() {
154    }
155
156    open spec fn la_inv(self, lv: nat) -> bool {
157        self.is_node() ==> lv < L - 1
158    }
159
160    proof fn default_preserves_la_inv() {
161    }
162
163    open spec fn rel_children(self, i: int, child: Option<Self>) -> bool {
164        if self.is_node() {
165            &&& child is Some
166            &&& child.unwrap().path.len() == self.node.unwrap().tree_level + 1
167            &&& child.unwrap().match_pte(self.node.unwrap().children_perm.value()[i], self.node.unwrap().level)
168            &&& child.unwrap().path == self.path.push_tail(i as usize)
169        } else {
170            &&& child is None
171        }
172    }
173
174    proof fn default_preserves_rel_children(self, lv: nat) {
175        admit()
176    }
177}
178
179pub const INC_LEVELS: usize = NR_LEVELS + 1;
180
181/// `OwnerSubtree` is a tree `Node` (from `vstd_extra::ghost_tree`) containing `EntryOwner`s.
182/// It lives in a tree of maximum depth 5. Page table nodes can be at levels 0-3, and their entries are their children at the next
183/// level down. This means that level 4, the lowest level, can only contain frame entries as it consists of the entries of level 1 page tables.
184///
185/// Level correspondences: tree level 0 ==> path length 0 ==> level 4 page table
186///                        tree level 1 ==> path length 1 ==> level 3 page table (the level 4 page table does not map frames directly)
187///                        tree level 2 ==> path length 2 ==> level 2 page table or frame mapped by level 3 table
188///                        tree level 3 ==> path length 3 ==> level 1 page table or frame mapped by level 2 table
189///                        tree level 4 ==> path length 4 ==> frame mapped by level 1 table
190pub type OwnerSubtree<C> = Node<EntryOwner<C>, NR_ENTRIES, INC_LEVELS>;
191
192/// Specifies that `owner` is the ghost owner of a newly allocated empty page table node at the given level.
193/// Captures the structural post-conditions of `PageTableNode::alloc`.
194pub open spec fn allocated_empty_node_owner<C: PageTableConfig>(owner: OwnerSubtree<C>, level: PagingLevel) -> bool {
195    &&& owner.inv()
196    &&& owner.value.is_node()
197    &&& owner.value.path == TreePath::<NR_ENTRIES>::new(Seq::empty())
198    &&& owner.value.parent_level == level
199    &&& owner.value.node.unwrap().level == level - 1
200    &&& owner.value.node.unwrap().inv()
201    &&& !owner.value.node.unwrap().children_perm.value().all(|child: C::E| child.is_present())
202    &&& forall |i: int| #![auto] 0 <= i < NR_ENTRIES ==> {
203        &&& owner.children[i] is Some
204        &&& owner.children[i].unwrap().value.is_absent()
205        &&& !owner.children[i].unwrap().value.in_scope
206        &&& owner.children[i].unwrap().value.inv()
207        &&& owner.children[i].unwrap().value.path == owner.value.path.push_tail(i as usize)
208    }
209    &&& forall |i: int| #![auto] 0 <= i < NR_ENTRIES ==>
210        owner.children[i].unwrap().value.match_pte(
211            owner.value.node.unwrap().children_perm.value()[i],
212            owner.children[i].unwrap().value.parent_level,
213        )
214    &&& forall |i: int| #![auto] 0 <= i < NR_ENTRIES ==>
215        owner.children[i].unwrap().value.parent_level == owner.value.node.unwrap().level
216}
217
218pub struct PageTableOwner<C: PageTableConfig>(pub OwnerSubtree<C>);
219
220impl<C: PageTableConfig> PageTableOwner<C> {
221
222    /// For a top-level (root) page table, entries at indices outside of
223    /// `C::TOP_LEVEL_INDEX_RANGE_spec()` are absent. This ensures that
224    /// UserPtConfig and KernelPtConfig page tables manage disjoint portions
225    /// of the virtual address space.
226    pub open spec fn top_level_indices_absent(self) -> bool {
227        let range = C::TOP_LEVEL_INDEX_RANGE_spec();
228        self.0.value.is_node() ==>
229        forall|i: int|
230            #![trigger self.0.children[i]]
231            0 <= i < NR_ENTRIES
232            && !(range.start <= i < range.end)
233            ==> self.0.children[i] is Some
234                && self.0.children[i].unwrap().value.is_absent()
235    }
236
237    pub open spec fn view_rec(self, path: TreePath<NR_ENTRIES>) -> Set<Mapping>
238        decreases INC_LEVELS - path.len() when self.0.inv() && path.len() <= INC_LEVELS - 1
239    {
240        if self.0.value.is_frame() {
241            let vaddr = vaddr(path);
242            let pt_level = INC_LEVELS - path.len();
243            let page_size = page_size(pt_level as PagingLevel);
244
245            set![Mapping {
246                va_range: Range { start: vaddr, end: (vaddr + page_size) as Vaddr },
247                pa_range: Range {
248                    start: self.0.value.frame.unwrap().mapped_pa,
249                    end: (self.0.value.frame.unwrap().mapped_pa + page_size) as Paddr,
250                },
251                page_size: page_size,
252                property: self.0.value.frame.unwrap().prop,
253            }]
254        } else if self.0.value.is_node() && path.len() < INC_LEVELS - 1 {
255            Set::new(
256                |m: Mapping| exists|i:int|
257                #![trigger self.0.children[i]]
258                0 <= i < self.0.children.len() &&
259                    self.0.children[i] is Some &&
260                    PageTableOwner(self.0.children[i].unwrap()).view_rec(path.push_tail(i as usize)).contains(m)
261            )
262        } else {
263            set![]
264        }
265    }
266
267    pub proof fn view_rec_contains(self, path: TreePath<NR_ENTRIES>, m: Mapping)
268        requires
269            self.0.inv(),
270            path.len() < INC_LEVELS - 1,
271            path.len() == self.0.level,
272            self.view_rec(path).contains(m),
273            self.0.value.is_node()
274        ensures
275            exists|i:int| #![auto] 0 <= i < self.0.children.len() &&
276            self.0.children[i] is Some &&
277            PageTableOwner(self.0.children[i].unwrap()).view_rec(path.push_tail(i as usize)).contains(m)
278    { }
279
280    pub proof fn view_rec_contains_choose(self, path: TreePath<NR_ENTRIES>, m: Mapping) -> (i: int)
281        requires
282            self.0.inv(),
283            path.len() < INC_LEVELS - 1,
284            path.len() == self.0.level,
285            self.view_rec(path).contains(m),
286            self.0.value.is_node(),
287        ensures
288            0 <= i < self.0.children.len() &&
289            self.0.children[i] is Some &&
290            PageTableOwner(self.0.children[i].unwrap()).view_rec(path.push_tail(i as usize)).contains(m)
291    {
292        choose|i:int| #![auto] 0 <= i < self.0.children.len() &&
293            self.0.children[i] is Some &&
294            PageTableOwner(self.0.children[i].unwrap()).view_rec(path.push_tail(i as usize)).contains(m)
295    }
296
297    pub proof fn view_rec_vaddr_range(self, path: TreePath<NR_ENTRIES>, m: Mapping)
298        requires
299            self.0.inv(),
300            path.len() <= INC_LEVELS - 1,
301            path.len() == self.0.level,
302            self.view_rec(path).contains(m),
303        ensures
304            vaddr(path) <= m.va_range.start < m.va_range.end <= vaddr(path) + page_size((INC_LEVELS - path.len()) as PagingLevel),
305    {
306        admit();
307    }
308
309    pub proof fn view_rec_disjoint_vaddrs(self, path: TreePath<NR_ENTRIES>, m1: Mapping, m2: Mapping)
310        requires
311            self.0.inv(),
312            path.len() <= INC_LEVELS - 1,
313            path.len() == self.0.level,
314            self.view_rec(path).contains(m1),
315            self.view_rec(path).contains(m2),
316            m1 != m2,
317        ensures
318            m1.va_range.end <= m2.va_range.start || m2.va_range.end <= m1.va_range.start
319        decreases INC_LEVELS - path.len()
320    {
321        broadcast use group_set_properties;
322
323        if self.0.value.is_frame() {
324            assert(self.view_rec(path).is_singleton());
325        } else if self.0.value.is_node() {
326            self.view_rec_contains(path, m1);
327            self.view_rec_contains(path, m2);
328
329            let i1 = self.view_rec_contains_choose(path, m1);
330            let i2 = self.view_rec_contains_choose(path, m2);
331
332            if i1 == i2 {
333                PageTableOwner(self.0.children[i1].unwrap()).view_rec_disjoint_vaddrs(path.push_tail(i1 as usize), m1, m2);
334            } else if i1 < i2 {
335                let parent_page_size = page_size((INC_LEVELS - path.len()) as PagingLevel);
336                let child_page_size = page_size((INC_LEVELS - path.len() - 1) as PagingLevel);
337                PageTableOwner(self.0.children[i1].unwrap()).view_rec_vaddr_range(path.push_tail(i1 as usize), m1);
338                PageTableOwner(self.0.children[i2].unwrap()).view_rec_vaddr_range(path.push_tail(i2 as usize), m2);
339                page_size_monotonic((INC_LEVELS - path.len() - 1) as PagingLevel, (INC_LEVELS - path.len()) as PagingLevel);
340                assert(child_page_size <= parent_page_size);
341                sibling_paths_disjoint(path, i1 as usize, i2 as usize, parent_page_size);
342                if vaddr(path.push_tail(i1 as usize)) + parent_page_size <= vaddr(path.push_tail(i2 as usize)) {
343                    let start1: usize = vaddr(path.push_tail(i1 as usize));
344                    let start2: usize = vaddr(path.push_tail(i2 as usize));
345                    let m1_end: usize = m1.va_range.end;
346                    let m2_start: usize = m2.va_range.start;
347                    assert(m1_end <= start1 + child_page_size);
348                    assert(start1 + child_page_size <= start1 + parent_page_size) by (nonlinear_arith)
349                        requires
350                            child_page_size <= parent_page_size,
351                    ;
352                    assert(m1_end <= start1 + parent_page_size) by (nonlinear_arith)
353                        requires
354                            m1_end <= start1 + child_page_size,
355                            start1 + child_page_size <= start1 + parent_page_size,
356                    ;
357                    assert(start2 <= m2_start);
358                    assert(m1_end <= m2_start) by (nonlinear_arith)
359                        requires
360                            m1_end <= start1 + parent_page_size,
361                            start1 + parent_page_size <= start2,
362                            start2 <= m2_start,
363                    ;
364                } else {
365                    let start2: usize = vaddr(path.push_tail(i2 as usize));
366                    let start1: usize = vaddr(path.push_tail(i1 as usize));
367                    let m2_end: usize = m2.va_range.end;
368                    let m1_start: usize = m1.va_range.start;
369                    assert(start2 + parent_page_size <= start1);
370                    assert(m2_end <= start2 + child_page_size);
371                    assert(start2 + child_page_size <= start2 + parent_page_size) by (nonlinear_arith)
372                        requires
373                            child_page_size <= parent_page_size,
374                    ;
375                    assert(m2_end <= start2 + parent_page_size) by (nonlinear_arith)
376                        requires
377                            m2_end <= start2 + child_page_size,
378                            start2 + child_page_size <= start2 + parent_page_size,
379                    ;
380                    assert(start1 <= m1_start);
381                    assert(m2_end <= m1_start) by (nonlinear_arith)
382                        requires
383                            m2_end <= start2 + parent_page_size,
384                            start2 + parent_page_size <= start1,
385                            start1 <= m1_start,
386                    ;
387                }
388            } else {
389                let parent_page_size = page_size((INC_LEVELS - path.len()) as PagingLevel);
390                let child_page_size = page_size((INC_LEVELS - path.len() - 1) as PagingLevel);
391                PageTableOwner(self.0.children[i2].unwrap()).view_rec_vaddr_range(path.push_tail(i2 as usize), m2);
392                PageTableOwner(self.0.children[i1].unwrap()).view_rec_vaddr_range(path.push_tail(i1 as usize), m1);
393                page_size_monotonic((INC_LEVELS - path.len() - 1) as PagingLevel, (INC_LEVELS - path.len()) as PagingLevel);
394                assert(child_page_size <= parent_page_size);
395                sibling_paths_disjoint(path, i2 as usize, i1 as usize, parent_page_size);
396                if vaddr(path.push_tail(i2 as usize)) + parent_page_size <= vaddr(path.push_tail(i1 as usize)) {
397                    let start2: usize = vaddr(path.push_tail(i2 as usize));
398                    let start1: usize = vaddr(path.push_tail(i1 as usize));
399                    let m2_end: usize = m2.va_range.end;
400                    let m1_start: usize = m1.va_range.start;
401                    assert(m2_end <= start2 + child_page_size);
402                    assert(start2 + child_page_size <= start2 + parent_page_size) by (nonlinear_arith)
403                        requires
404                            child_page_size <= parent_page_size,
405                    ;
406                    assert(m2_end <= start2 + parent_page_size) by (nonlinear_arith)
407                        requires
408                            m2_end <= start2 + child_page_size,
409                            start2 + child_page_size <= start2 + parent_page_size,
410                    ;
411                    assert(start1 <= m1_start);
412                    assert(m2_end <= m1_start) by (nonlinear_arith)
413                        requires
414                            m2_end <= start2 + parent_page_size,
415                            start2 + parent_page_size <= start1,
416                            start1 <= m1_start,
417                    ;
418                } else {
419                    let start1: usize = vaddr(path.push_tail(i1 as usize));
420                    let start2: usize = vaddr(path.push_tail(i2 as usize));
421                    let m1_end: usize = m1.va_range.end;
422                    let m2_start: usize = m2.va_range.start;
423                    assert(start1 + parent_page_size <= start2);
424                    assert(m1_end <= start1 + child_page_size);
425                    assert(start1 + child_page_size <= start1 + parent_page_size) by (nonlinear_arith)
426                        requires
427                            child_page_size <= parent_page_size,
428                    ;
429                    assert(m1_end <= start1 + parent_page_size) by (nonlinear_arith)
430                        requires
431                            m1_end <= start1 + child_page_size,
432                            start1 + child_page_size <= start1 + parent_page_size,
433                    ;
434                    assert(start2 <= m2_start);
435                    assert(m1_end <= m2_start) by (nonlinear_arith)
436                        requires
437                            m1_end <= start1 + parent_page_size,
438                            start1 + parent_page_size <= start2,
439                            start2 <= m2_start,
440                    ;
441                }
442            }
443        }
444    }
445
446    /// An absent entry contributes no mappings - view_rec returns the empty set.
447    pub proof fn view_rec_absent_empty(self, path: TreePath<NR_ENTRIES>)
448        requires
449            self.0.inv(),
450            self.0.value.is_absent(),
451            path.len() <= INC_LEVELS - 1,
452        ensures
453            self.view_rec(path) =~= set![],
454    { }
455
456    /// A node with nr_children == 0 has no present PTEs, so all children are absent
457    /// and the subtree contributes no mappings.
458    ///
459    /// Axiom: the link between `nr_children` and the count of present PTEs is maintained
460    /// by `Entry::replace` / `Entry::new` but not yet formalised as a `NodeOwner` invariant.
461    pub axiom fn view_rec_nr_children_zero_empty(self, path: TreePath<NR_ENTRIES>)
462        requires
463            self.0.inv(),
464            self.0.value.is_node(),
465            self.0.value.node.unwrap().meta_own.nr_children.value() == 0,
466            path.len() <= INC_LEVELS - 1,
467            path.len() == self.0.level,
468        ensures
469            self.view_rec(path) =~= set![];
470
471    pub open spec fn relate_region_pred(regions: MetaRegionOwners)
472        -> (spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool) {
473        |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| entry.relate_region(regions)
474    }
475
476    pub open spec fn relate_region(self, regions: MetaRegionOwners) -> bool
477        decreases INC_LEVELS - self.0.level when self.0.inv()
478    {
479        self.0.tree_predicate_map(self.0.value.path, Self::relate_region_pred(regions))
480    }
481
482    /// Predicate: all nodes in the tree have their paths tracked in regions
483    pub open spec fn path_tracked_pred(regions: MetaRegionOwners)
484        -> spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool
485    {
486        |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| {
487            entry.meta_slot_paddr() is Some ==> {
488                &&& regions.slot_owners.contains_key(frame_to_index(entry.meta_slot_paddr().unwrap()))
489                &&& regions.slot_owners[frame_to_index(entry.meta_slot_paddr().unwrap())].path_if_in_pt is Some
490            }
491        }
492    }
493
494    pub open spec fn relate_region_tracked_pred(regions: MetaRegionOwners)
495        -> spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool
496    {
497        |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| {
498            &&& entry.meta_slot_paddr() is Some
499            &&& regions.slot_owners.contains_key(frame_to_index(entry.meta_slot_paddr().unwrap()))
500            &&& regions.slot_owners[frame_to_index(entry.meta_slot_paddr().unwrap())].path_if_in_pt is Some
501            &&& regions.slot_owners[frame_to_index(entry.meta_slot_paddr().unwrap())].path_if_in_pt.unwrap() == path
502        }
503    }
504
505    pub open spec fn path_correct_pred()
506        -> spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool
507    {
508        |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| {
509            entry.path == path
510        }
511    }
512
513    pub open spec fn not_in_scope_pred()
514        -> spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool
515    {
516        |entry: EntryOwner<C>, _path: TreePath<NR_ENTRIES>| !entry.in_scope
517    }
518
519    /// Every entry in an OwnerSubtree has `!in_scope`.
520    /// Follows from `EntryOwner::inv()` including `!in_scope`, propagated through the tree.
521    pub proof fn tree_not_in_scope(subtree: OwnerSubtree<C>, path: TreePath<NR_ENTRIES>)
522        requires
523            subtree.inv(),
524        ensures
525            subtree.tree_predicate_map(path, Self::not_in_scope_pred()),
526        decreases INC_LEVELS - subtree.level,
527    {
528        // subtree.inv() => inv_node() => value.inv() => !value.in_scope
529        if subtree.level < INC_LEVELS - 1 {
530            assert forall |i: int|
531                0 <= i < subtree.children.len()
532                && (#[trigger] subtree.children[i]) is Some implies
533                subtree.children[i].unwrap().tree_predicate_map(
534                    path.push_tail(i as usize), Self::not_in_scope_pred())
535            by {
536                Self::tree_not_in_scope(
537                    subtree.children[i].unwrap(), path.push_tail(i as usize));
538            };
539        }
540    }
541
542    /// All mappings in a subtree's `view_rec` have `page_size <= page_size(pt_level)`
543    /// where `pt_level = INC_LEVELS - path.len()` (the paging level of the subtree root).
544    ///
545    /// For frames: the mapping has exactly `page_size(pt_level)`.
546    /// For nodes: children have longer paths, so their mappings have strictly smaller page sizes.
547    pub proof fn view_rec_page_size_bound(self, path: TreePath<NR_ENTRIES>, m: Mapping)
548        requires
549            self.0.inv(),
550            path.len() <= INC_LEVELS - 1,
551            self.view_rec(path).contains(m),
552        ensures
553            m.page_size <= page_size((INC_LEVELS - path.len()) as PagingLevel),
554        decreases INC_LEVELS - path.len(),
555    {
556        admit()
557    }
558
559    /// For a node subtree, all mappings have `page_size < page_size(pt_level)`, i.e.,
560    /// `page_size <= page_size(pt_level - 1)`.  This is because node mappings come from
561    /// children whose paths are one level deeper.
562    pub proof fn view_rec_node_page_size_bound(self, path: TreePath<NR_ENTRIES>, m: Mapping)
563        requires
564            self.0.inv(),
565            self.0.value.is_node(),
566            path.len() < INC_LEVELS - 1,
567            self.view_rec(path).contains(m),
568        ensures
569            m.page_size <= page_size(((INC_LEVELS - path.len()) - 1) as PagingLevel),
570        decreases INC_LEVELS - path.len(),
571    {
572        admit()
573    }
574
575    /// Spec function: path1 is a prefix of path2
576    pub open spec fn is_prefix_of<const N: usize>(
577        prefix: TreePath<N>,
578        path: TreePath<N>,
579    ) -> bool {
580        &&& prefix.len() <= path.len()
581        &&& forall |i: int| 0 <= i < prefix.len() ==> prefix.index(i) == path.index(i)
582    }
583
584    /// Transitivity of is_prefix_of
585    pub proof fn prefix_transitive<const N: usize>(
586        p1: TreePath<N>,
587        p2: TreePath<N>,
588        p3: TreePath<N>,
589    )
590        requires
591            Self::is_prefix_of(p1, p2),
592            Self::is_prefix_of(p2, p3),
593        ensures
594            Self::is_prefix_of(p1, p3),
595    {
596        assert(p1.len() <= p3.len());
597        assert forall |i: int| 0 <= i < p1.len() implies p1.index(i) == p3.index(i) by {
598            assert(p1.index(i) == p2.index(i));
599            assert(p2.index(i) == p3.index(i));
600        };
601    }
602
603    pub proof fn prefix_push_different_indices(
604        prefix: TreePath<NR_ENTRIES>,
605        path: TreePath<NR_ENTRIES>,
606        i: usize,
607        j: usize,
608    )
609        requires
610            prefix.inv(),
611            path.inv(),
612            i != j,
613            Self::is_prefix_of(prefix.push_tail(i), path),
614        ensures
615            !Self::is_prefix_of(prefix.push_tail(j), path),
616    {
617        assert(path.index(prefix.len() as int) == i);
618    }
619
620    pub open spec fn is_at_pred(entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>)
621        -> spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool
622    {
623        |entry0: EntryOwner<C>, path0: TreePath<NR_ENTRIES>| {
624            path0 == path ==> entry0 == entry
625        }
626    }
627
628    pub open spec fn path_in_tree_pred(path: TreePath<NR_ENTRIES>)
629        -> spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool
630    {
631        |entry: EntryOwner<C>, path0: TreePath<NR_ENTRIES>|
632            Self::is_prefix_of(path0, path) ==>
633            !entry.is_node() ==>
634            path == path0
635    }
636
637    pub proof fn is_at_pred_eq(path: TreePath<NR_ENTRIES>, entry1: EntryOwner<C>, entry2: EntryOwner<C>)
638        requires
639            entry1.inv(),
640            OwnerSubtree::implies(Self::is_at_pred(entry1, path), Self::is_at_pred(entry2, path)),
641        ensures
642            entry1 == entry2,
643    {
644        assert(Self::is_at_pred(entry1, path)(entry1, path) ==>
645               Self::is_at_pred(entry2, path)(entry1, path));
646    }
647
648    pub proof fn is_at_holds_when_on_wrong_path(
649        subtree: OwnerSubtree<C>,
650        root_path: TreePath<NR_ENTRIES>,
651        dest_path: TreePath<NR_ENTRIES>,
652        entry: EntryOwner<C>,
653    )
654        requires
655            subtree.inv(),
656            dest_path.inv(),
657            !Self::is_prefix_of(root_path, dest_path),
658            root_path.len() <= INC_LEVELS - 1,
659            root_path.len() == subtree.level,
660        ensures
661            subtree.tree_predicate_map(root_path, Self::is_at_pred(entry, dest_path)),
662        decreases INC_LEVELS - root_path.len()
663    {
664        if subtree.value.is_node() {
665            assert forall |i: int| 0 <= i < NR_ENTRIES implies
666                (#[trigger] subtree.children[i as int]).unwrap().tree_predicate_map(root_path.push_tail(i as usize), Self::is_at_pred(entry, dest_path)) by {
667                    Self::is_at_holds_when_on_wrong_path(subtree.children[i as int].unwrap(),
668                        root_path.push_tail(i as usize), dest_path, entry);
669                };
670        }
671    }
672
673    /// Counterintuitive: the predicate is vacuously true when the path is not a prefix of the target path,
674    /// because it is actually a liveness property: if we keep following the path, we will eventually reach it.
675    /// This covers when we are not following it.
676    pub proof fn path_in_tree_holds_when_on_wrong_path(
677        subtree: OwnerSubtree<C>,
678        root_path: TreePath<NR_ENTRIES>,
679        dest_path: TreePath<NR_ENTRIES>,
680    )
681        requires
682            subtree.inv(),
683            dest_path.inv(),
684            !Self::is_prefix_of(root_path, dest_path),
685            root_path.len() <= INC_LEVELS - 1,
686            root_path.len() == subtree.level,
687        ensures
688            subtree.tree_predicate_map(root_path, Self::path_in_tree_pred(dest_path)),
689        decreases INC_LEVELS - root_path.len()
690    {
691        if subtree.value.is_node() {
692            assert forall |i: int| 0 <= i < NR_ENTRIES implies
693                (#[trigger] subtree.children[i as int]).unwrap().tree_predicate_map(root_path.push_tail(i as usize), Self::path_in_tree_pred(dest_path)) by {
694                    Self::path_in_tree_holds_when_on_wrong_path(subtree.children[i as int].unwrap(),
695                        root_path.push_tail(i as usize), dest_path);
696                };
697        }
698    }
699
700    /// If a subtree satisfies `inv()` and the root entry's `path` field equals the structural root
701    /// path, then the subtree satisfies `tree_predicate_map(path, path_correct_pred())`.
702    /// This is proved by induction using `rel_children` (which stores `child.path == parent.path.push_tail(i)`)
703    /// from `Node::inv_children()`.
704    pub proof fn inv_implies_path_correct(
705        subtree: OwnerSubtree<C>,
706        path: TreePath<NR_ENTRIES>,
707    )
708        requires
709            subtree.inv(),
710            path.inv(),
711            path.len() <= INC_LEVELS - 1,
712            path.len() == subtree.level,
713            subtree.value.path == path,
714        ensures
715            subtree.tree_predicate_map(path, Self::path_correct_pred()),
716        decreases INC_LEVELS - path.len()
717    {
718        if subtree.level < INC_LEVELS - 1 {
719            assert forall|i: int| #![auto]
720                0 <= i < NR_ENTRIES && subtree.children[i] is Some implies
721                subtree.children[i].unwrap().tree_predicate_map(
722                    path.push_tail(i as usize),
723                    Self::path_correct_pred(),
724                ) by {
725                let child = subtree.children[i].unwrap();
726                // From Node::inv_children + rel_children: child.value.path == path.push_tail(i)
727                assert(child.value.path == path.push_tail(i as usize)) by {
728                    assert(<EntryOwner<C> as TreeNodeValue<INC_LEVELS>>::rel_children(subtree.value, i, Some(child.value)));
729                    if subtree.value.is_node() {
730                        assert(child.value.path == subtree.value.path.push_tail(i as usize));
731                    } else {
732                        // rel_children with is_not_node() requires child is None → contradiction
733                        assert(false);
734                    }
735                };
736                assert(child.inv());
737                assert(child.level == subtree.level + 1);
738                assert((path.push_tail(i as usize)).len() == child.level) by {
739                    path.push_tail_property_len(i as usize);
740                };
741                Self::inv_implies_path_correct(child, path.push_tail(i as usize));
742            };
743        }
744    }
745
746    /// For entries in a subtree rooted at `path_j` whose `path_j` is not a prefix of
747    /// `old_entry.path`, no entry in the subtree shares a physical address with `old_entry`.
748    ///
749    /// Proof sketch: by `inv_implies_path_correct`, every entry `e` at structural position `p`
750    /// has `e.path == p`.  Since `!is_prefix_of(path_j, old_entry.path)`, no structural position
751    /// in the subtree equals `old_entry.path`.  Combined with `relate_region` + `path_tracked_pred`
752    /// uniqueness (via `same_paddr_implies_same_path`), same paddr would force same path — contradiction.
753    pub axiom fn neq_old_from_path_disjoint(
754        subtree: OwnerSubtree<C>,
755        path_j: TreePath<NR_ENTRIES>,
756        old_entry: EntryOwner<C>,
757        regions: MetaRegionOwners,
758    )
759        requires
760            subtree.inv(),
761            subtree.value.path == path_j,
762            path_j.len() == subtree.level,
763            path_j.inv(),
764            path_j.len() <= INC_LEVELS - 1,
765            subtree.tree_predicate_map(path_j, Self::relate_region_pred(regions)),
766            subtree.tree_predicate_map(path_j, Self::path_tracked_pred(regions)),
767            old_entry.meta_slot_paddr() is Some,
768            old_entry.relate_region(regions),
769            regions.slot_owners[
770                frame_to_index(old_entry.meta_slot_paddr().unwrap())
771            ].path_if_in_pt is Some,
772            !Self::is_prefix_of(path_j, old_entry.path),
773        ensures
774            subtree.tree_predicate_map(
775                path_j,
776                |e: EntryOwner<C>, p: TreePath<NR_ENTRIES>| e.meta_slot_paddr_neq(old_entry),
777            );
778
779    pub proof fn is_at_eq_rec(
780        subtree: OwnerSubtree<C>,
781        root_path: TreePath<NR_ENTRIES>,
782        dest_path: TreePath<NR_ENTRIES>,
783        entry1: EntryOwner<C>,
784        entry2: EntryOwner<C>
785    )
786        requires
787            subtree.inv(),
788            dest_path.inv(),
789            root_path.inv(),
790            Self::is_prefix_of(root_path, dest_path),
791            root_path.len() <= INC_LEVELS - 1,
792            root_path.len() == subtree.level,
793            subtree.tree_predicate_map(root_path, Self::path_in_tree_pred(dest_path)),
794            subtree.tree_predicate_map(root_path, Self::is_at_pred(entry1, dest_path)),
795            subtree.tree_predicate_map(root_path, Self::is_at_pred(entry2, dest_path)),
796        ensures
797            entry1 == entry2,
798        decreases INC_LEVELS - root_path.len()
799    {
800        if root_path == dest_path {
801            assert(subtree.value == entry1);
802            assert(subtree.value == entry2);
803            assert(entry1 == entry2);
804        } else if subtree.level == INC_LEVELS - 1 || !subtree.value.is_node() {
805            proof_from_false()
806        } else {
807            assert(root_path.len() < dest_path.len()) by {
808                assert(root_path.len() <= dest_path.len());
809                if root_path.len() == dest_path.len() {
810                    assert(root_path =~= dest_path) by {
811                        assert(root_path.0.len() == dest_path.0.len());
812                        assert forall |i: int| 0 <= i < root_path.0.len() implies #[trigger] root_path.0[i] == dest_path.0[i] by {
813                            assert(root_path.index(i) == dest_path.index(i));
814                        };
815                    };
816                    assert(root_path == dest_path);
817                    assert(false);
818                }
819            };
820            let i = dest_path.index(root_path.len() as int);
821            assert(0 <= i < NR_ENTRIES);
822            assert(subtree.children[i as int] is Some);
823            assert(Self::is_prefix_of(root_path.push_tail(i), dest_path));
824            Self::is_at_eq_rec(subtree.children[i as int].unwrap(), root_path.push_tail(i as usize),
825                dest_path, entry1, entry2);
826        }
827    }
828
829    pub proof fn view_rec_inversion(self,
830        path: TreePath<NR_ENTRIES>,
831        regions: MetaRegionOwners,
832        m: Mapping,
833    ) -> (entry: EntryOwner<C>)
834        requires
835            self.0.inv(),
836            path.len() == self.0.level,
837            self.view_rec(path).contains(m),
838            self.0.tree_predicate_map(path, Self::path_correct_pred()),
839            self.0.tree_predicate_map(path, Self::relate_region_tracked_pred(regions)),
840        ensures
841            Self::is_prefix_of(path, entry.path),
842            regions.slot_owners[frame_to_index(m.pa_range.start)].path_if_in_pt == Some(entry.path),
843            m.va_range.start == vaddr(entry.path),
844            m.page_size == page_size((INC_LEVELS - entry.path.len()) as PagingLevel),
845            entry.is_frame(),
846            m.property == entry.frame.unwrap().prop,
847            self.0.tree_predicate_map(path, Self::is_at_pred(entry, entry.path)),
848            self.0.tree_predicate_map(path, Self::path_in_tree_pred(entry.path)),
849            entry.inv(),
850        decreases INC_LEVELS - path.len()
851    {
852        if self.0.value.is_frame() {
853            assert(Self::is_prefix_of(path, self.0.value.path));
854            assert(self.0.tree_predicate_map(path, Self::is_at_pred(self.0.value, self.0.value.path)));
855            assert(self.0.tree_predicate_map(path, Self::path_in_tree_pred(self.0.value.path)));
856            self.0.value
857        } else if self.0.value.is_node() {
858            self.view_rec_contains(path, m);
859            let i = self.view_rec_contains_choose(path, m);
860            let entry = PageTableOwner(self.0.children[i].unwrap()).view_rec_inversion(path.push_tail(i as usize), regions, m);
861            Self::prefix_transitive(path, path.push_tail(i as usize), entry.path);
862            assert(self.0.tree_predicate_map(path, Self::is_at_pred(entry, entry.path))) by {
863                assert forall |j: int| 0 <= j < NR_ENTRIES && #[trigger] self.0.children[j] is Some implies
864                    self.0.children[j].unwrap().tree_predicate_map(path.push_tail(j as usize),
865                        Self::is_at_pred(entry, entry.path))
866                by {
867                    if j != i {
868                        assert(!Self::is_prefix_of(path.push_tail(j as usize), entry.path)) by {
869                            Self::prefix_push_different_indices(path, entry.path, i as usize, j as usize);
870                        }
871                        Self::is_at_holds_when_on_wrong_path(self.0.children[j].unwrap(),
872                            path.push_tail(j as usize), entry.path, entry);
873                    }
874                };
875            };
876            assert(self.0.tree_predicate_map(path, Self::path_in_tree_pred(entry.path))) by {
877                assert forall |j: int| 0 <= j < NR_ENTRIES && #[trigger] self.0.children[j] is Some implies
878                    self.0.children[j].unwrap().tree_predicate_map(path.push_tail(j as usize),
879                        Self::path_in_tree_pred(entry.path))
880                by {
881                    if j != i {
882                        assert(!Self::is_prefix_of(path.push_tail(j as usize), entry.path)) by {
883                            Self::prefix_push_different_indices(path, entry.path, i as usize, j as usize);
884                        }
885                        Self::path_in_tree_holds_when_on_wrong_path(self.0.children[j].unwrap(),
886                            path.push_tail(j as usize), entry.path);
887                    }
888                };
889            };
890            entry
891        } else {
892            proof_from_false()
893        }
894    }
895
896    pub proof fn view_rec_inversion_unique(self,
897        path: TreePath<NR_ENTRIES>,
898        regions: MetaRegionOwners,
899        m1: Mapping,
900        m2: Mapping,
901    )
902        requires
903            self.0.inv(),
904            path.len() <= INC_LEVELS - 1,
905            path.len() == self.0.level,
906            self.view_rec(path).contains(m1),
907            self.view_rec(path).contains(m2),
908            m1.pa_range.start == m2.pa_range.start,
909            m1.inv(),
910            m2.inv(),
911            self.0.tree_predicate_map(path, Self::path_tracked_pred(regions)),
912            self.0.tree_predicate_map(path, Self::path_correct_pred()),
913            self.0.tree_predicate_map(path, Self::relate_region_tracked_pred(regions)),
914        ensures
915            m1 == m2,
916    {
917        let entry1 = self.view_rec_inversion(path, regions, m1);
918        let entry2 = self.view_rec_inversion(path, regions, m2);
919
920        assert(self.0.tree_predicate_map(path, Self::is_at_pred(entry1, entry1.path)));
921        assert(self.0.tree_predicate_map(path, Self::is_at_pred(entry2, entry2.path)));
922
923        Self::is_at_eq_rec(self.0, path, entry1.path, entry1, entry2);
924    }
925
926}
927
928impl<C: PageTableConfig> Inv for PageTableOwner<C> {
929    open spec fn inv(self) -> bool {
930        &&& self.0.inv()
931        &&& self.0.value.is_node()
932        &&& self.0.value.path.len() <= INC_LEVELS - 1
933        &&& self.0.value.path.inv()
934        &&& self.0.value.path.len() == self.0.level
935        &&& self.0.tree_predicate_map(self.0.value.path, Self::path_correct_pred())
936    }
937}
938
939impl<C: PageTableConfig> View for PageTableOwner<C> {
940    type V = PageTableView;
941
942    open spec fn view(&self) -> <Self as View>::V {
943        let mappings = self.view_rec(self.0.value.path);
944        PageTableView {
945            mappings
946        }
947    }
948}
949
950} // verus!
ostd/specs/mm/page_table/owners.rs

ostd/specs/mm/page_table/
owners.rs
