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::{PageTableEntryTrait, PageTableGuard};
20
21use crate::specs::arch::*;
22use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
23use crate::specs::mm::page_table::*;
24
25use core::ops::Deref;
26
27verus! {
28
29#[verifier::inline]
30pub open spec fn vaddr_shift_bits<const L: usize>(idx: int) -> nat
31    recommends
32        0 < L,
33        idx < L,
34{
35    (12 + 9 * (L - 1 - idx)) as nat
36}
37
38#[verifier::inline]
39pub open spec fn vaddr_shift<const L: usize>(idx: int) -> usize
40    recommends
41        0 < L,
42        idx < L,
43{
44    pow2(vaddr_shift_bits::<L>(idx)) as usize
45}
46
47#[verifier::inline]
48pub open spec fn vaddr_make<const L: usize>(idx: int, offset: usize) -> usize
49    recommends
50        0 < L,
51        idx < L,
52        0 <= offset < 512,
53{
54    (vaddr_shift::<L>(idx) * offset) as usize
55}
56
57pub open spec fn rec_vaddr(
58    path: TreePath<NR_ENTRIES>,
59    idx: int,
60) -> usize/*        recommends
61        0 < NR_LEVELS,
62        path.len() <= NR_LEVELS,
63        0 <= idx <= path.len(),*/
64
65    decreases path.len() - idx,
66    when 0 <= idx <= path.len()
67{
68    if idx == path.len() {
69        0
70    } else {
71        let offset: usize = path.index(idx);
72        (vaddr_make::<NR_LEVELS>(idx, offset) + rec_vaddr(path, idx + 1)) as usize
73    }
74}
75
76pub open spec fn vaddr(path: TreePath<NR_ENTRIES>) -> usize {
77    rec_vaddr(path, 0)
78}
79
80/// Sibling paths (same prefix, different last index) have disjoint VA ranges.
81/// This is a fundamental property of page table virtual address layout:
82/// each entry at a given level covers a distinct, non-overlapping range.
83pub proof fn sibling_paths_disjoint(
84    prefix: TreePath<NR_ENTRIES>,
85    j: usize,
86    k: usize,
87    size: usize,
88)
89    requires
90        j < NR_ENTRIES,
91        k < NR_ENTRIES,
92        j != k,
93        size == page_size((prefix.len() + 1) as PagingLevel),
94    ensures
95        vaddr(prefix.push_tail(j)) + size <= vaddr(prefix.push_tail(k))
96        || vaddr(prefix.push_tail(k)) + size <= vaddr(prefix.push_tail(j)),
97{
98    admit()
99}
100
101impl<C: PageTableConfig, const L: usize> TreeNodeValue<L> for EntryOwner<C> {
102    open spec fn default(lv: nat) -> Self {
103        Self {
104            in_scope: false,
105            path: TreePath::new(Seq::empty()),
106            parent_level: (INC_LEVELS - lv + 1) as PagingLevel,
107            node: None,
108            frame: None,
109            locked: None,
110            absent: true,
111        }
112    }
113
114    proof fn default_preserves_inv() {
115    }
116
117    open spec fn la_inv(self, lv: nat) -> bool {
118        self.is_node() ==> lv < L - 1
119    }
120
121    proof fn default_preserves_la_inv() {
122    }
123
124    open spec fn rel_children(self, i: int, child: Option<Self>) -> bool {
125        if self.is_node() {
126            &&& child is Some
127            &&& child.unwrap().path.len() == self.node.unwrap().tree_level + 1
128            &&& child.unwrap().match_pte(self.node.unwrap().children_perm.value()[i], self.node.unwrap().level)
129            &&& child.unwrap().path == self.path.push_tail(i as usize)
130        } else {
131            &&& child is None
132        }
133    }
134
135    proof fn default_preserves_rel_children(self, lv: nat) {
136        admit()
137    }
138}
139
140pub const INC_LEVELS: usize = NR_LEVELS + 1;
141
142/// `OwnerSubtree` is a tree `Node` (from `vstd_extra::ghost_tree`) containing `EntryOwner`s.
143/// 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
144/// 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.
145///
146/// Level correspondences: tree level 0 ==> path length 0 ==> level 4 page table
147///                        tree level 1 ==> path length 1 ==> level 3 page table (the level 4 page table does not map frames directly)
148///                        tree level 2 ==> path length 2 ==> level 2 page table or frame mapped by level 3 table
149///                        tree level 3 ==> path length 3 ==> level 1 page table or frame mapped by level 2 table
150///                        tree level 4 ==> path length 4 ==> frame mapped by level 1 table
151pub type OwnerSubtree<C> = Node<EntryOwner<C>, NR_ENTRIES, INC_LEVELS>;
152
153/// Specifies that `owner` is the ghost owner of a newly allocated empty page table node at the given level.
154/// Captures the structural post-conditions of `PageTableNode::alloc`.
155pub open spec fn allocated_empty_node_owner<C: PageTableConfig>(
156    owner: OwnerSubtree<C>,
157    level: PagingLevel,
158) -> bool {
159    &&& owner.inv()
160    &&& owner.value.is_node()
161    &&& owner.value.path == TreePath::<NR_ENTRIES>::new(Seq::empty())
162    &&& owner.value.parent_level == level
163    &&& owner.value.node.unwrap().level == level - 1
164    &&& owner.value.node.unwrap().inv()
165    &&& forall |i: int| #![auto] 0 <= i < NR_ENTRIES ==>
166        !owner.value.node.unwrap().children_perm.value()[i].is_present()
167    &&& forall |i: int| #![auto] 0 <= i < NR_ENTRIES ==> {
168        &&& owner.children[i] is Some
169        &&& owner.children[i].unwrap().value.is_absent()
170        &&& !owner.children[i].unwrap().value.in_scope
171        &&& owner.children[i].unwrap().value.inv()
172        &&& owner.children[i].unwrap().value.path == owner.value.path.push_tail(i as usize)
173    }
174    &&& forall |i: int| #![auto] 0 <= i < NR_ENTRIES ==>
175        owner.children[i].unwrap().value.match_pte(
176            owner.value.node.unwrap().children_perm.value()[i],
177            owner.children[i].unwrap().value.parent_level,
178        )
179    &&& forall |i: int| #![auto] 0 <= i < NR_ENTRIES ==>
180        owner.children[i].unwrap().value.parent_level == owner.value.node.unwrap().level
181}
182
183pub struct PageTableOwner<C: PageTableConfig>(pub OwnerSubtree<C>);
184
185impl<C: PageTableConfig> PageTableOwner<C> {
186
187    pub open spec fn view_rec(self, path: TreePath<NR_ENTRIES>) -> Set<Mapping>
188        decreases INC_LEVELS - path.len() when self.0.inv() && path.len() <= INC_LEVELS - 1
189    {
190        if self.0.value.is_frame() {
191            let vaddr = vaddr(path);
192            let pt_level = INC_LEVELS - path.len();
193            let page_size = page_size(pt_level as PagingLevel);
194
195            set![Mapping {
196                va_range: Range { start: vaddr, end: (vaddr + page_size) as Vaddr },
197                pa_range: Range {
198                    start: self.0.value.frame.unwrap().mapped_pa,
199                    end: (self.0.value.frame.unwrap().mapped_pa + page_size) as Paddr,
200                },
201                page_size: page_size,
202                property: self.0.value.frame.unwrap().prop,
203            }]
204        } else if self.0.value.is_node() && path.len() < INC_LEVELS - 1 {
205            Set::new(
206                |m: Mapping| exists|i:int|
207                #![trigger self.0.children[i]]
208                0 <= i < self.0.children.len() &&
209                    self.0.children[i] is Some &&
210                    PageTableOwner(self.0.children[i].unwrap()).view_rec(path.push_tail(i as usize)).contains(m)
211            )
212        } else {
213            set![]
214        }
215    }
216
217    pub proof fn view_rec_contains(self, path: TreePath<NR_ENTRIES>, m: Mapping)
218        requires
219            self.0.inv(),
220            path.len() < INC_LEVELS - 1,
221            path.len() == self.0.level,
222            self.view_rec(path).contains(m),
223            self.0.value.is_node()
224        ensures
225            exists|i:int| #![auto] 0 <= i < self.0.children.len() &&
226            self.0.children[i] is Some &&
227            PageTableOwner(self.0.children[i].unwrap()).view_rec(path.push_tail(i as usize)).contains(m)
228    { }
229
230    pub proof fn view_rec_contains_choose(self, path: TreePath<NR_ENTRIES>, m: Mapping) -> (i: int)
231        requires
232            self.0.inv(),
233            path.len() < INC_LEVELS - 1,
234            path.len() == self.0.level,
235            self.view_rec(path).contains(m),
236            self.0.value.is_node(),
237        ensures
238            0 <= i < self.0.children.len() &&
239            self.0.children[i] is Some &&
240            PageTableOwner(self.0.children[i].unwrap()).view_rec(path.push_tail(i as usize)).contains(m)
241    {
242        choose|i:int| #![auto] 0 <= i < self.0.children.len() &&
243            self.0.children[i] is Some &&
244            PageTableOwner(self.0.children[i].unwrap()).view_rec(path.push_tail(i as usize)).contains(m)
245    }
246
247    pub proof fn view_rec_vaddr_range(self, path: TreePath<NR_ENTRIES>, m: Mapping)
248        requires
249            self.0.inv(),
250            path.len() <= INC_LEVELS - 1,
251            path.len() == self.0.level,
252            self.view_rec(path).contains(m),
253        ensures
254            vaddr(path) <= m.va_range.start < m.va_range.end <= vaddr(path) + page_size(path.len() as PagingLevel),
255    {
256        admit();
257    }
258
259    pub proof fn view_rec_disjoint_vaddrs(self, path: TreePath<NR_ENTRIES>, m1: Mapping, m2: Mapping)
260        requires
261            self.0.inv(),
262            path.len() <= INC_LEVELS - 1,
263            path.len() == self.0.level,
264            self.view_rec(path).contains(m1),
265            self.view_rec(path).contains(m2),
266            m1 != m2,
267        ensures
268            m1.va_range.end <= m2.va_range.start || m2.va_range.end <= m1.va_range.start
269        decreases INC_LEVELS - path.len()
270    {
271        broadcast use group_set_properties;
272
273        if self.0.value.is_frame() {
274            assert(self.view_rec(path).is_singleton());
275        } else if self.0.value.is_node() {
276            self.view_rec_contains(path, m1);
277            self.view_rec_contains(path, m2);
278
279            let i1 = self.view_rec_contains_choose(path, m1);
280            let i2 = self.view_rec_contains_choose(path, m2);
281
282            if i1 == i2 {
283                PageTableOwner(self.0.children[i1].unwrap()).view_rec_disjoint_vaddrs(path.push_tail(i1 as usize), m1, m2);
284            } else if i1 < i2 {
285                let page_size = page_size((path.len() + 1) as PagingLevel);
286                // TODO: connect TreePath to AbstractVaddr
287                assert(vaddr(path.push_tail(i1 as usize)) + page_size <= vaddr(path.push_tail(i2 as usize))) by { admit(); };
288                PageTableOwner(self.0.children[i1].unwrap()).view_rec_vaddr_range(path.push_tail(i1 as usize), m1);
289                PageTableOwner(self.0.children[i2].unwrap()).view_rec_vaddr_range(path.push_tail(i2 as usize), m2);
290            } else {
291                let page_size = page_size((path.len() + 1) as PagingLevel);
292                assert(vaddr(path.push_tail(i2 as usize)) + page_size <= vaddr(path.push_tail(i1 as usize))) by { admit(); };
293                PageTableOwner(self.0.children[i2].unwrap()).view_rec_vaddr_range(path.push_tail(i2 as usize), m2);
294                PageTableOwner(self.0.children[i1].unwrap()).view_rec_vaddr_range(path.push_tail(i1 as usize), m1);
295            }
296        }
297    }
298
299    /// An absent entry contributes no mappings - view_rec returns the empty set.
300    pub proof fn view_rec_absent_empty(self, path: TreePath<NR_ENTRIES>)
301        requires
302            self.0.inv(),
303            self.0.value.is_absent(),
304            path.len() <= INC_LEVELS - 1,
305        ensures
306            self.view_rec(path) =~= set![],
307    { }
308
309    pub open spec fn relate_region_pred(regions: MetaRegionOwners)
310        -> (spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool) {
311        |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| entry.relate_region(regions)
312    }
313
314    pub open spec fn relate_region(self, regions: MetaRegionOwners) -> bool
315        decreases INC_LEVELS - self.0.level when self.0.inv()
316    {
317        self.0.tree_predicate_map(self.0.value.path, Self::relate_region_pred(regions))
318    }
319
320    /// Predicate: all nodes in the tree have their paths tracked in regions
321    pub open spec fn path_tracked_pred(regions: MetaRegionOwners)
322        -> spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool
323    {
324        |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| {
325            entry.meta_slot_paddr() is Some ==> {
326                &&& regions.slot_owners.contains_key(frame_to_index(entry.meta_slot_paddr().unwrap()))
327                &&& regions.slot_owners[frame_to_index(entry.meta_slot_paddr().unwrap())].path_if_in_pt is Some
328            }
329        }
330    }
331
332    pub open spec fn relate_region_tracked_pred(regions: MetaRegionOwners)
333        -> spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool
334    {
335        |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| {
336            &&& entry.meta_slot_paddr() is Some
337            &&& regions.slot_owners.contains_key(frame_to_index(entry.meta_slot_paddr().unwrap()))
338            &&& regions.slot_owners[frame_to_index(entry.meta_slot_paddr().unwrap())].path_if_in_pt is Some
339            &&& regions.slot_owners[frame_to_index(entry.meta_slot_paddr().unwrap())].path_if_in_pt.unwrap() == path
340        }
341    }
342
343    pub open spec fn path_correct_pred()
344        -> spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool
345    {
346        |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| {
347            entry.path == path
348        }
349    }
350
351    /// Spec function: path1 is a prefix of path2
352    pub open spec fn is_prefix_of<const N: usize>(
353        prefix: TreePath<N>,
354        path: TreePath<N>,
355    ) -> bool {
356        &&& prefix.len() <= path.len()
357        &&& forall |i: int| 0 <= i < prefix.len() ==> prefix.index(i) == path.index(i)
358    }
359
360    /// Transitivity of is_prefix_of
361    pub proof fn prefix_transitive<const N: usize>(
362        p1: TreePath<N>,
363        p2: TreePath<N>,
364        p3: TreePath<N>,
365    )
366        requires
367            Self::is_prefix_of(p1, p2),
368            Self::is_prefix_of(p2, p3),
369        ensures
370            Self::is_prefix_of(p1, p3),
371    {
372        assert(p1.len() <= p3.len());
373        assert forall |i: int| 0 <= i < p1.len() implies p1.index(i) == p3.index(i) by {
374            assert(p1.index(i) == p2.index(i));
375            assert(p2.index(i) == p3.index(i));
376        };
377    }
378
379    pub proof fn prefix_push_different_indices(
380        prefix: TreePath<NR_ENTRIES>,
381        path: TreePath<NR_ENTRIES>,
382        i: usize,
383        j: usize,
384    )
385        requires
386            prefix.inv(),
387            path.inv(),
388            i != j,
389            Self::is_prefix_of(prefix.push_tail(i), path),
390        ensures
391            !Self::is_prefix_of(prefix.push_tail(j), path),
392    {
393        assert(path.index(prefix.len() as int) == i);
394    }
395
396    pub open spec fn is_at_pred(entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>)
397        -> spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool
398    {
399        |entry0: EntryOwner<C>, path0: TreePath<NR_ENTRIES>| {
400            path0 == path ==> entry0 == entry
401        }
402    }
403
404    pub open spec fn path_in_tree_pred(path: TreePath<NR_ENTRIES>)
405        -> spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool
406    {
407        |entry: EntryOwner<C>, path0: TreePath<NR_ENTRIES>|
408            Self::is_prefix_of(path0, path) ==>
409            !entry.is_node() ==>
410            path == path0
411    }
412
413    pub proof fn is_at_pred_eq(path: TreePath<NR_ENTRIES>, entry1: EntryOwner<C>, entry2: EntryOwner<C>)
414        requires
415            entry1.inv(),
416            OwnerSubtree::implies(Self::is_at_pred(entry1, path), Self::is_at_pred(entry2, path)),
417        ensures
418            entry1 == entry2,
419    {
420        assert(Self::is_at_pred(entry1, path)(entry1, path) ==>
421               Self::is_at_pred(entry2, path)(entry1, path));
422    }
423
424    pub proof fn is_at_holds_when_on_wrong_path(
425        subtree: OwnerSubtree<C>,
426        root_path: TreePath<NR_ENTRIES>,
427        dest_path: TreePath<NR_ENTRIES>,
428        entry: EntryOwner<C>,
429    )
430        requires
431            subtree.inv(),
432            dest_path.inv(),
433            !Self::is_prefix_of(root_path, dest_path),
434            root_path.len() <= INC_LEVELS - 1,
435            root_path.len() == subtree.level,
436        ensures
437            subtree.tree_predicate_map(root_path, Self::is_at_pred(entry, dest_path)),
438        decreases INC_LEVELS - root_path.len()
439    {
440        if subtree.value.is_node() {
441            assert forall |i: int| 0 <= i < NR_ENTRIES implies
442                (#[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 {
443                    Self::is_at_holds_when_on_wrong_path(subtree.children[i as int].unwrap(),
444                        root_path.push_tail(i as usize), dest_path, entry);
445                };
446        }
447    }
448
449    /// Counterintuitive: the predicate is vacuously true when the path is not a prefix of the target path,
450    /// because it is actually a liveness property: if we keep following the path, we will eventually reach it.
451    /// This covers when we are not following it.
452    pub proof fn path_in_tree_holds_when_on_wrong_path(
453        subtree: OwnerSubtree<C>,
454        root_path: TreePath<NR_ENTRIES>,
455        dest_path: TreePath<NR_ENTRIES>,
456    )
457        requires
458            subtree.inv(),
459            dest_path.inv(),
460            !Self::is_prefix_of(root_path, dest_path),
461            root_path.len() <= INC_LEVELS - 1,
462            root_path.len() == subtree.level,
463        ensures
464            subtree.tree_predicate_map(root_path, Self::path_in_tree_pred(dest_path)),
465        decreases INC_LEVELS - root_path.len()
466    {
467        if subtree.value.is_node() {
468            assert forall |i: int| 0 <= i < NR_ENTRIES implies
469                (#[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 {
470                    Self::path_in_tree_holds_when_on_wrong_path(subtree.children[i as int].unwrap(),
471                        root_path.push_tail(i as usize), dest_path);
472                };
473        }
474    }
475
476    pub proof fn is_at_eq_rec(
477        subtree: OwnerSubtree<C>,
478        root_path: TreePath<NR_ENTRIES>,
479        dest_path: TreePath<NR_ENTRIES>,
480        entry1: EntryOwner<C>,
481        entry2: EntryOwner<C>
482    )
483        requires
484            subtree.inv(),
485            dest_path.inv(),
486            root_path.inv(),
487            Self::is_prefix_of(root_path, dest_path),
488            root_path.len() <= INC_LEVELS - 1,
489            root_path.len() == subtree.level,
490            subtree.tree_predicate_map(root_path, Self::path_in_tree_pred(dest_path)),
491            subtree.tree_predicate_map(root_path, Self::is_at_pred(entry1, dest_path)),
492            subtree.tree_predicate_map(root_path, Self::is_at_pred(entry2, dest_path)),
493        ensures
494            entry1 == entry2,
495        decreases INC_LEVELS - root_path.len()
496    {
497        if root_path == dest_path {
498            assert(subtree.value == entry1);
499            assert(subtree.value == entry2);
500            assert(entry1 == entry2);
501        } else if subtree.level == INC_LEVELS - 1 || !subtree.value.is_node() {
502            proof_from_false()
503        } else {
504            assert(root_path.len() < dest_path.len()) by { admit() };
505            let i = dest_path.index(root_path.len() as int);
506            assert(0 <= i < NR_ENTRIES);
507            assert(subtree.children[i as int] is Some);
508            assert(Self::is_prefix_of(root_path.push_tail(i), dest_path));
509            Self::is_at_eq_rec(subtree.children[i as int].unwrap(), root_path.push_tail(i as usize),
510                dest_path, entry1, entry2);
511        }
512    }
513
514    pub proof fn view_rec_inversion(self,
515        path: TreePath<NR_ENTRIES>,
516        regions: MetaRegionOwners,
517        m: Mapping,
518    ) -> (entry: EntryOwner<C>)
519        requires
520            self.0.inv(),
521            path.len() == self.0.level,
522            self.view_rec(path).contains(m),
523            self.0.tree_predicate_map(path, Self::path_correct_pred()),
524            self.0.tree_predicate_map(path, Self::relate_region_tracked_pred(regions)),
525        ensures
526            Self::is_prefix_of(path, entry.path),
527            regions.slot_owners[frame_to_index(m.pa_range.start)].path_if_in_pt == Some(entry.path),
528            m.va_range.start == vaddr(entry.path),
529            m.page_size == page_size((INC_LEVELS - entry.path.len()) as PagingLevel),
530            entry.is_frame(),
531            m.property == entry.frame.unwrap().prop,
532            self.0.tree_predicate_map(path, Self::is_at_pred(entry, entry.path)),
533            self.0.tree_predicate_map(path, Self::path_in_tree_pred(entry.path)),
534            entry.inv(),
535        decreases INC_LEVELS - path.len()
536    {
537        if self.0.value.is_frame() {
538            assert(Self::is_prefix_of(path, self.0.value.path));
539            assert(self.0.tree_predicate_map(path, Self::is_at_pred(self.0.value, self.0.value.path)));
540            assert(self.0.tree_predicate_map(path, Self::path_in_tree_pred(self.0.value.path)));
541            self.0.value
542        } else if self.0.value.is_node() {
543            self.view_rec_contains(path, m);
544            let i = self.view_rec_contains_choose(path, m);
545            let entry = PageTableOwner(self.0.children[i].unwrap()).view_rec_inversion(path.push_tail(i as usize), regions, m);
546            Self::prefix_transitive(path, path.push_tail(i as usize), entry.path);
547            assert(self.0.tree_predicate_map(path, Self::is_at_pred(entry, entry.path))) by {
548                assert forall |j: int| 0 <= j < NR_ENTRIES && #[trigger] self.0.children[j] is Some implies
549                    self.0.children[j].unwrap().tree_predicate_map(path.push_tail(j as usize),
550                        Self::is_at_pred(entry, entry.path))
551                by {
552                    if j != i {
553                        assert(!Self::is_prefix_of(path.push_tail(j as usize), entry.path)) by {
554                            Self::prefix_push_different_indices(path, entry.path, i as usize, j as usize);
555                        }
556                        Self::is_at_holds_when_on_wrong_path(self.0.children[j].unwrap(),
557                            path.push_tail(j as usize), entry.path, entry);
558                    }
559                };
560            };
561            assert(self.0.tree_predicate_map(path, Self::path_in_tree_pred(entry.path))) by {
562                assert forall |j: int| 0 <= j < NR_ENTRIES && #[trigger] self.0.children[j] is Some implies
563                    self.0.children[j].unwrap().tree_predicate_map(path.push_tail(j as usize),
564                        Self::path_in_tree_pred(entry.path))
565                by {
566                    if j != i {
567                        assert(!Self::is_prefix_of(path.push_tail(j as usize), entry.path)) by {
568                            Self::prefix_push_different_indices(path, entry.path, i as usize, j as usize);
569                        }
570                        Self::path_in_tree_holds_when_on_wrong_path(self.0.children[j].unwrap(),
571                            path.push_tail(j as usize), entry.path);
572                    }
573                };
574            };
575            entry
576        } else {
577            proof_from_false()
578        }
579    }
580
581    pub proof fn view_rec_inversion_unique(self,
582        path: TreePath<NR_ENTRIES>,
583        regions: MetaRegionOwners,
584        m1: Mapping,
585        m2: Mapping,
586    )
587        requires
588            self.0.inv(),
589            path.len() <= INC_LEVELS - 1,
590            path.len() == self.0.level,
591            self.view_rec(path).contains(m1),
592            self.view_rec(path).contains(m2),
593            m1.pa_range.start == m2.pa_range.start,
594            m1.inv(),
595            m2.inv(),
596            self.0.tree_predicate_map(path, Self::path_tracked_pred(regions)),
597            self.0.tree_predicate_map(path, Self::path_correct_pred()),
598            self.0.tree_predicate_map(path, Self::relate_region_tracked_pred(regions)),
599        ensures
600            m1 == m2,
601    {
602        let entry1 = self.view_rec_inversion(path, regions, m1);
603        let entry2 = self.view_rec_inversion(path, regions, m2);
604
605        assert(self.0.tree_predicate_map(path, Self::is_at_pred(entry1, entry1.path)));
606        assert(self.0.tree_predicate_map(path, Self::is_at_pred(entry2, entry2.path)));
607
608        Self::is_at_eq_rec(self.0, path, entry1.path, entry1, entry2);
609    }
610
611}
612
613impl<C: PageTableConfig> Inv for PageTableOwner<C> {
614    open spec fn inv(self) -> bool {
615        &&& self.0.inv()
616        &&& self.0.value.path.len() <= INC_LEVELS - 1
617        &&& self.0.value.path.inv()
618        &&& self.0.value.path.len() == self.0.level
619        &&& self.0.tree_predicate_map(self.0.value.path, Self::path_correct_pred())
620    }
621}
622
623impl<C: PageTableConfig> View for PageTableOwner<C> {
624    type V = PageTableView;
625
626    open spec fn view(&self) -> <Self as View>::V {
627        let mappings = self.view_rec(self.0.value.path);
628        PageTableView {
629            mappings
630        }
631    }
632}
633
634} // verus!
ostd/specs/mm/page_table/owners.rs

ostd/specs/mm/page_table/
owners.rs
