ostd/specs/mm/page_table/node/
entry.rs

1use vstd::prelude::*;
2
3use vstd_extra::ghost_tree::*;
4use vstd_extra::ownership::*;
5
6use crate::mm::frame::meta::mapping::frame_to_index;
7use crate::mm::page_table::*;
8use crate::specs::arch::mm::NR_ENTRIES;
9use crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED;
10use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
11use crate::specs::mm::page_table::*;
12
13verus! {
14
15impl<'rcu, C: PageTableConfig> Entry<'rcu, C> {
16    pub open spec fn invariants(self, owner: EntryOwner<C>, regions: MetaRegionOwners) -> bool {
17        &&& owner.inv()
18        &&& regions.inv()
19        &&& self.wf(owner)
20        &&& owner.relate_region(regions)
21    }
22
23    pub open spec fn node_matching(self, owner: EntryOwner<C>, parent_owner: NodeOwner<C>, guard_perm: GuardPerm<'rcu, C>) -> bool {
24        &&& parent_owner.level == owner.parent_level
25        &&& parent_owner.inv()
26        &&& guard_perm.addr() == self.node.addr()
27        &&& guard_perm.is_init()
28        &&& guard_perm.value().inner.inner@.ptr.addr() == parent_owner.meta_perm.addr()
29        &&& guard_perm.value().inner.inner@.ptr.addr() == parent_owner.meta_perm.points_to.addr()
30        &&& guard_perm.value().inner.inner@.wf(parent_owner)
31        &&& parent_owner.meta_perm.is_init()
32        &&& parent_owner.meta_perm.wf(&parent_owner.meta_perm.inner_perms)
33        &&& owner.match_pte(parent_owner.children_perm.value()[self.idx as int], owner.parent_level)
34    }
35
36    pub open spec fn relate_region_preserved(regions0: MetaRegionOwners, regions1: MetaRegionOwners) -> bool {
37        OwnerSubtree::implies(
38            |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| entry.relate_region(regions0),
39            |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| entry.relate_region(regions1),
40        )
41    }
42
43    pub open spec fn replace_panic_condition(
44        parent_owner: NodeOwner<C>,
45        new_owner: EntryOwner<C>,
46    ) -> bool {
47        if new_owner.is_node() {
48            parent_owner.level - 1 == new_owner.node.unwrap().level
49        } else if new_owner.is_frame() {
50            parent_owner.level == new_owner.parent_level
51        } else {
52            true
53        }
54    }
55
56    pub open spec fn relate_region_neq_preserved(
57        old_entry_owner: EntryOwner<C>,
58        new_entry_owner: EntryOwner<C>,
59        regions0: MetaRegionOwners,
60        regions1: MetaRegionOwners,
61    ) -> bool {
62        OwnerSubtree::implies(
63            |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
64                entry.meta_slot_paddr_neq(old_entry_owner)
65                && entry.meta_slot_paddr_neq(new_entry_owner)
66                && entry.relate_region(regions0),
67            |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
68                entry.relate_region(regions1),
69        )
70    }
71
72    pub open spec fn path_tracked_pred_preserved(regions0: MetaRegionOwners, regions1: MetaRegionOwners) -> bool {
73        OwnerSubtree::implies(
74            PageTableOwner::<C>::path_tracked_pred(regions0),
75            PageTableOwner::<C>::path_tracked_pred(regions1),
76        )
77    }
78
79    pub open spec fn new_owner_compatible(self,
80        new_child: Child<C>,
81        old_owner: EntryOwner<C>,
82        new_owner: EntryOwner<C>,
83        regions: MetaRegionOwners)
84    -> bool {
85        &&& old_owner.path == new_owner.path
86        &&& old_owner.parent_level == new_owner.parent_level
87        &&& old_owner.meta_slot_paddr_neq(new_owner)
88        &&& new_owner.in_scope
89        &&& new_owner.is_node() ==> {
90            &&& regions.slots.contains_key(frame_to_index(new_owner.meta_slot_paddr().unwrap()))
91            &&& regions.slot_owners[frame_to_index(new_owner.meta_slot_paddr().unwrap())].inner_perms.ref_count.value() !=
92                REF_COUNT_UNUSED
93        }
94    }
95
96    pub open spec fn parent_perms_preserved(self,
97        parent_owner0: NodeOwner<C>,
98        parent_owner1: NodeOwner<C>,
99        guard_perm0: GuardPerm<'rcu, C>,
100        guard_perm1: GuardPerm<'rcu, C>)
101    -> bool {
102        &&& guard_perm0.addr() == guard_perm1.addr()
103        &&& guard_perm0.value().inner.inner@.ptr.addr() == guard_perm1.value().inner.inner@.ptr.addr()
104        &&& forall|i: int| 0 <= i < NR_ENTRIES ==> i != self.idx ==>
105            parent_owner0.children_perm.value()[i] == parent_owner1.children_perm.value()[i]
106    }
107}
108
109} // verus!
ostd/specs/mm/page_table/node/entry.rs

ostd/specs/mm/page_table/node/
entry.rs
