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

1use vstd::prelude::*;
2use vstd_extra::{ghost_tree::*, ownership::*};
3
4use crate::specs::{
5    arch::NR_ENTRIES,
6    mm::{
7        frame::{mapping::frame_to_index, meta_region_owners::MetaRegionOwners},
8        page_table::*,
9    },
10};
11
12use crate::mm::{frame::meta::REF_COUNT_UNUSED, page_table::*};
13
14verus! {
15
16impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
17    /// Claiming one unused slot preserves entries that refer to other slots.
18    pub proof fn lemma_allocated_node_preserves_disjoint_entries(
19        old_child: EntryOwner<C>,
20        new_child: EntryOwner<C>,
21        r0: MetaRegionOwners,
22        r1: MetaRegionOwners,
23    )
24        requires
25            old_child.is_absent(),
26            new_child.is_node(),
27            new_child.inv(),
28            r0.inv(),
29            r1.inv(),
30            r0.slots == r1.slots,
31            forall|i: int|
32                #![trigger r1.slot_owners[i]]
33                i != frame_to_index(new_child.meta_slot_paddr()->0) ==> {
34                    &&& r1.slot_owners[i].same_permissions(r0.slot_owners[i])
35                    &&& r1.slot_owners[i].usage == r0.slot_owners[i].usage
36                    &&& r1.slot_owners[i].slot_vaddr == r0.slot_owners[i].slot_vaddr
37                    &&& r0.slot_owners[i].paths_in_pt.subset_of(r1.slot_owners[i].paths_in_pt)
38                    &&& r0.slot_owners[i].usage is PageTable ==> r1.slot_owners[i].paths_in_pt
39                        == r0.slot_owners[i].paths_in_pt
40                },
41            r1.contains(frame_to_index(new_child.meta_slot_paddr()->0)),
42            0 < r1.ref_count(frame_to_index(new_child.meta_slot_paddr()->0))
43                <= crate::mm::frame::meta::REF_COUNT_MAX,
44        ensures
45            Self::metaregion_sound_neq_preserved(old_child, new_child, r0, r1),
46    {
47        broadcast use crate::specs::mm::frame::mapping::lemma_frame_to_index_injective;
48
49        let idx = frame_to_index(new_child.meta_slot_paddr()->0);
50        assert forall|entry: EntryOwner<C>|
51            entry.inv() && entry.meta_slot_paddr_neq(new_child) && entry.metaregion_sound(
52                r0,
53            ) implies #[trigger] entry.metaregion_sound(r1) by {
54            let intermediate = r0.insert_slot_owner(
55                new_child.meta_slot_paddr()->0,
56                r1.slot_owners[idx],
57            );
58            assert(intermediate.inv());
59            entry.lemma_metaregion_sound_one_slot_changed(r0, intermediate, idx);
60            entry.lemma_metaregion_sound_frame_paths_changed(intermediate, r1);
61        };
62    }
63
64    pub open spec fn invariants(self, owner: EntryOwner<C>, regions: MetaRegionOwners) -> bool {
65        &&& owner.inv()
66        &&& regions.inv()
67        &&& self.wf(owner)
68        &&& owner.metaregion_sound(regions)
69    }
70
71    pub open spec fn node_matching(
72        self,
73        owner: EntryOwner<C>,
74        parent_owner: NodeOwner<C>,
75        guard: PageTableGuard<'rcu, C>,
76    ) -> bool {
77        &&& parent_owner.level() == owner.parent_level
78        &&& parent_owner.inv()
79        &&& parent_owner.relate_guard(guard)
80        &&& owner.match_pte(parent_owner.children_perm.value()[self.idx as int], owner.parent_level)
81    }
82
83    pub open spec fn metaregion_sound_preserved(
84        regions0: MetaRegionOwners,
85        regions1: MetaRegionOwners,
86    ) -> bool {
87        OwnerSubtree::implies(
88            |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| entry.metaregion_sound(regions0),
89            |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| entry.metaregion_sound(regions1),
90        )
91    }
92
93    pub open spec fn replace_nonpanic_condition(
94        parent_owner: NodeOwner<C>,
95        new_owner: EntryOwner<C>,
96    ) -> bool {
97        if new_owner.is_node() {
98            parent_owner.level() - 1 == new_owner.node().level()
99        } else if new_owner.is_frame() {
100            parent_owner.level() == new_owner.parent_level
101        } else {
102            true
103        }
104    }
105
106    pub open spec fn metaregion_sound_neq_preserved(
107        old_entry_owner: EntryOwner<C>,
108        new_entry_owner: EntryOwner<C>,
109        regions0: MetaRegionOwners,
110        regions1: MetaRegionOwners,
111    ) -> bool {
112        OwnerSubtree::implies(
113            |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
114                entry.meta_slot_paddr_neq(old_entry_owner) && entry.meta_slot_paddr_neq(
115                    new_entry_owner,
116                ) && entry.metaregion_sound(regions0),
117            |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| entry.metaregion_sound(regions1),
118        )
119    }
120
121    /// Preservation for entries whose counted slot is disjoint from the old entry.
122    /// Untracked physical aliases impose no counted-metadata exclusion.
123    pub open spec fn metaregion_sound_neq_old_preserved(
124        old_entry_owner: EntryOwner<C>,
125        regions0: MetaRegionOwners,
126        regions1: MetaRegionOwners,
127    ) -> bool {
128        OwnerSubtree::implies(
129            |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
130                entry.meta_slot_paddr_neq(old_entry_owner) && entry.metaregion_sound(regions0),
131            |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| entry.metaregion_sound(regions1),
132        )
133    }
134
135    /// When `alloc_if_none` allocates a new node from an absent slot, all existing entries'
136    /// `metaregion_sound` is preserved in the new regions.
137    pub proof fn alloc_if_none_metaregion_sound_preserved(
138        old_child: EntryOwner<C>,
139        new_child: EntryOwner<C>,
140        regions0: MetaRegionOwners,
141        regions1: MetaRegionOwners,
142    )
143        requires
144            old_child.is_absent(),
145            old_child.inv(),
146            new_child.is_node(),
147            regions0.inv(),
148            regions0.contains(frame_to_index(new_child.meta_slot_paddr()->0)),
149            regions0.slot_owner(new_child.meta_slot_paddr()->0).ref_count() == REF_COUNT_UNUSED,
150            Self::metaregion_sound_neq_preserved(old_child, new_child, regions0, regions1),
151        ensures
152            Self::metaregion_sound_preserved(regions0, regions1),
153    {
154        let new_idx = frame_to_index(new_child.meta_slot_paddr().unwrap());
155        let f = PageTableOwner::<C>::metaregion_sound_pred(regions0);
156        let g = PageTableOwner::<C>::metaregion_sound_pred(regions1);
157
158        assert(old_child.meta_slot_paddr() is None);
159
160        assert forall|entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
161            entry.inv() && f(entry, path) implies #[trigger] g(entry, path) by {
162            if entry.meta_slot_paddr() is Some && entry.is_node() {
163                EntryOwner::<C>::lemma_active_entry_not_in_free_pool(entry, regions0, new_idx);
164            }
165        };
166    }
167
168    pub open spec fn path_tracked_pred_preserved(
169        regions0: MetaRegionOwners,
170        regions1: MetaRegionOwners,
171    ) -> bool {
172        OwnerSubtree::implies(
173            PageTableOwner::<C>::path_tracked_pred(regions0),
174            PageTableOwner::<C>::path_tracked_pred(regions1),
175        )
176    }
177
178    pub open spec fn new_owner_compatible(
179        self,
180        new_child: Child<C>,
181        old_owner: EntryOwner<C>,
182        new_owner: EntryOwner<C>,
183        regions: MetaRegionOwners,
184    ) -> bool {
185        &&& old_owner.path == new_owner.path
186        &&& old_owner.parent_level == new_owner.parent_level
187        &&& new_owner.is_node() ==> {
188            &&& regions.contains(frame_to_index(new_owner.meta_slot_paddr()->0))
189            &&& regions.slot_owner(new_owner.meta_slot_paddr()->0).ref_count() != REF_COUNT_UNUSED
190        }
191    }
192
193    pub open spec fn parent_perms_preserved(
194        self,
195        parent_owner0: NodeOwner<C>,
196        parent_owner1: NodeOwner<C>,
197    ) -> bool {
198        &&& forall|i: int|
199            0 <= i < NR_ENTRIES ==> i != self.idx ==> parent_owner0.children_perm.value()[i]
200                == parent_owner1.children_perm.value()[i]
201        &&& parent_owner1.slot_index == parent_owner0.slot_index
202        &&& parent_owner1.level() == parent_owner0.level()
203        &&& parent_owner1.tree_level == parent_owner0.tree_level
204        &&& parent_owner1.meta_own.nr_children.id() == parent_owner0.meta_own.nr_children.id()
205        &&& parent_owner1.meta_own.stray == parent_owner0.meta_own.stray
206    }
207}
208
209} // verus!
ostd/specs/mm/page_table/node/entry.rs

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