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.metaregion_sound(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 metaregion_sound_preserved(regions0: MetaRegionOwners, regions1: MetaRegionOwners) -> bool {
37        OwnerSubtree::implies(
38            |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| entry.metaregion_sound(regions0),
39            |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| entry.metaregion_sound(regions1),
40        )
41    }
42
43    pub open spec fn replace_nonpanic_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 metaregion_sound_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.metaregion_sound(regions0),
67            |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
68                entry.metaregion_sound(regions1),
69        )
70    }
71
72    /// When the new child is NOT a node, `into_pte` doesn't modify `raw_count`.
73    /// Only `paths_in_pt` changes at `new_idx`, which `metaregion_sound` doesn't inspect.
74    /// So entries with `paddr_neq(old_child)` preserve `metaregion_sound` — no
75    /// `paddr_neq(new_child)` needed.
76    pub open spec fn metaregion_sound_neq_old_preserved(
77        old_entry_owner: EntryOwner<C>,
78        regions0: MetaRegionOwners,
79        regions1: MetaRegionOwners,
80    ) -> bool {
81        OwnerSubtree::implies(
82            |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
83                entry.meta_slot_paddr_neq(old_entry_owner)
84                && entry.metaregion_sound(regions0),
85            |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
86                entry.metaregion_sound(regions1),
87        )
88    }
89
90    /// When `alloc_if_none` allocates a new node from an absent slot, all existing entries'
91    /// `metaregion_sound` is preserved in the new regions.
92    ///
93    /// Justification: `metaregion_sound_neq_preserved` gives preservation for entries whose paddr
94    /// differs from both old_child and new_child. Old_child is absent (paddr_neq trivially true).
95    pub proof fn alloc_if_none_metaregion_sound_preserved(
96        old_child: EntryOwner<C>,
97        new_child: EntryOwner<C>,
98        regions0: MetaRegionOwners,
99        regions1: MetaRegionOwners,
100    )
101        requires
102            old_child.is_absent(),
103            old_child.inv(),
104            new_child.is_node(),
105            regions0.inv(),
106            regions0.slots.contains_key(frame_to_index(new_child.meta_slot_paddr().unwrap())),
107            regions0.slot_owners[frame_to_index(new_child.meta_slot_paddr().unwrap())]
108                .inner_perms.ref_count.value() == REF_COUNT_UNUSED,
109            Self::metaregion_sound_neq_preserved(old_child, new_child, regions0, regions1),
110        ensures
111            Self::metaregion_sound_preserved(regions0, regions1),
112    {
113        let new_idx = frame_to_index(new_child.meta_slot_paddr().unwrap());
114        let f = PageTableOwner::<C>::metaregion_sound_pred(regions0);
115        let g = PageTableOwner::<C>::metaregion_sound_pred(regions1);
116
117        assert(old_child.meta_slot_paddr() is None);
118
119        assert forall |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
120            entry.inv() && f(entry, path) implies #[trigger] g(entry, path)
121        by {
122            if entry.meta_slot_paddr() is Some && entry.is_node() {
123                EntryOwner::<C>::active_entry_not_in_free_pool(entry, regions0, new_idx);
124            }
125        };
126    }
127
128    pub open spec fn path_tracked_pred_preserved(regions0: MetaRegionOwners, regions1: MetaRegionOwners) -> bool {
129        OwnerSubtree::implies(
130            PageTableOwner::<C>::path_tracked_pred(regions0),
131            PageTableOwner::<C>::path_tracked_pred(regions1),
132        )
133    }
134
135    pub open spec fn new_owner_compatible(self,
136        new_child: Child<C>,
137        old_owner: EntryOwner<C>,
138        new_owner: EntryOwner<C>,
139        regions: MetaRegionOwners)
140    -> bool {
141        &&& old_owner.path == new_owner.path
142        &&& old_owner.parent_level == new_owner.parent_level
143        &&& new_owner.in_scope
144        &&& new_owner.is_node() ==> {
145            &&& regions.slots.contains_key(frame_to_index(new_owner.meta_slot_paddr().unwrap()))
146            &&& regions.slot_owners[frame_to_index(new_owner.meta_slot_paddr().unwrap())].inner_perms.ref_count.value() !=
147                REF_COUNT_UNUSED
148        }
149    }
150
151    pub open spec fn parent_perms_preserved(self,
152        parent_owner0: NodeOwner<C>,
153        parent_owner1: NodeOwner<C>,
154        guard_perm0: GuardPerm<'rcu, C>,
155        guard_perm1: GuardPerm<'rcu, C>)
156    -> bool {
157        &&& guard_perm0.addr() == guard_perm1.addr()
158        &&& guard_perm0.value().inner.inner@.ptr.addr() == guard_perm1.value().inner.inner@.ptr.addr()
159        &&& forall|i: int| 0 <= i < NR_ENTRIES ==> i != self.idx ==>
160            parent_owner0.children_perm.value()[i] == parent_owner1.children_perm.value()[i]
161        // meta_perm is unchanged: only children_perm and meta_own are modified by entry operations.
162        &&& parent_owner1.meta_perm.addr() == parent_owner0.meta_perm.addr()
163        &&& parent_owner1.meta_perm.points_to == parent_owner0.meta_perm.points_to
164        &&& parent_owner1.meta_perm.inner_perms == parent_owner0.meta_perm.inner_perms
165    }
166}
167
168} // verus!
ostd/specs/mm/page_table/node/entry.rs

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