ostd/specs/mm/page_table/cursor/
invariant_preservation_lemmas.rs

1/// CursorOwner-level preservation lemmas for transient `MetaRegionOwners`
2/// updates that affect at most one slot. Written as preparation for Phase 3b
3/// of the `paths_in_pt` refactor, where map/unmap operations insert or remove
4/// a single tree path from a single frame slot and must show that the global
5/// `Cursor::invariants` survives the edit.
6///
7/// Each lemma here lifts [`EntryOwner`]-level preservation facts (from
8/// `entry_owners.rs`) over the full cursor tree.
9use vstd::prelude::*;
10
11use vstd_extra::ghost_tree::*;
12use vstd_extra::ownership::*;
13
14use crate::mm::frame::meta::mapping::frame_to_index;
15use crate::mm::page_table::*;
16use crate::specs::arch::mm::{NR_ENTRIES, NR_LEVELS};
17use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
18use crate::specs::mm::page_table::cursor::owners::{CursorContinuation, CursorOwner};
19use crate::specs::mm::page_table::node::entry_owners::EntryOwner;
20use crate::specs::mm::page_table::owners::{OwnerSubtree, PageTableOwner};
21
22verus! {
23
24impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
25
26    /// Tree-wide predicate: no page-table node in either the cursor's tree
27    /// children or its continuation path has metadata slot index `idx`.
28    /// Used as the "sanity" precondition of the path-insert preservation
29    /// lemma: the only kind of entry it can touch with the new path is a
30    /// frame. Callers satisfy it by observing that page-table node metadata
31    /// lives in `FRAME_METADATA_RANGE`, which is disjoint from any data-frame
32    /// paddr (where `paths_in_pt` inserts happen).
33    pub open spec fn no_node_at_idx(self, idx: usize) -> bool {
34        &&& self.map_full_tree(
35            |e: EntryOwner<C>, _p: TreePath<NR_ENTRIES>|
36                e.is_node() && e.meta_slot_paddr() is Some
37                    ==> frame_to_index(e.meta_slot_paddr().unwrap()) != idx)
38        &&& forall |i: int| #![trigger self.continuations[i]]
39            self.level - 1 <= i < NR_LEVELS ==> {
40                let e = self.continuations[i].entry_own;
41                e.is_node() && e.meta_slot_paddr() is Some
42                    ==> frame_to_index(e.meta_slot_paddr().unwrap()) != idx
43            }
44    }
45
46    /// Pointwise conjunction of two tree-wide predicates: if `self.map_full_tree(f)`
47    /// and `self.map_full_tree(guard)` hold, then `self.map_full_tree(f && guard)`
48    /// holds. A thin wrapper around `OwnerSubtree::map_implies_and` applied per
49    /// continuation + per child; extracted so callers don't have to re-derive
50    /// the same nested `assert forall ... by { map_implies_and(...) }` block.
51    pub proof fn and_map_full_tree(
52        self,
53        f: spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool,
54        guard: spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool,
55    )
56        requires
57            self.inv(),
58            self.map_full_tree(f),
59            self.map_full_tree(guard),
60        ensures
61            self.map_full_tree(
62                |e: EntryOwner<C>, p: TreePath<NR_ENTRIES>| f(e, p) && guard(e, p)),
63    {
64        let combined = |e: EntryOwner<C>, p: TreePath<NR_ENTRIES>|
65            f(e, p) && guard(e, p);
66        assert forall |i: int| #![trigger self.continuations[i]]
67            self.level - 1 <= i < NR_LEVELS
68        implies
69            self.continuations[i].map_children(combined)
70        by {
71            let cont = self.continuations[i];
72            reveal(CursorContinuation::inv_children);
73            assert forall |j: int| #![trigger cont.children[j]]
74                0 <= j < cont.children.len() && cont.children[j] is Some
75            implies
76                cont.children[j].unwrap()
77                    .tree_predicate_map(cont.path().push_tail(j as usize), combined)
78            by {
79                cont.inv_children_unroll(j);
80                OwnerSubtree::map_implies_and(
81                    cont.children[j].unwrap(),
82                    cont.path().push_tail(j as usize),
83                    f, guard, combined);
84            };
85        };
86    }
87
88    /// Discharge `no_node_at_idx(changed_idx)` from the observation that
89    /// `changed_idx` is the index of a slot currently sitting in the free
90    /// pool (`regions.slots.contains_key(changed_idx)`). The argument uses
91    /// `EntryOwner::active_entry_not_in_free_pool`: an active node's
92    /// metadata slot is never simultaneously in the free pool, so any node
93    /// in the cursor tree must have a different slot index than
94    /// `changed_idx`.
95    ///
96    /// Callers doing a `paths_in_pt.insert` at a frame's data-slot
97    /// (e.g., `map` and the huge-page split) use this helper to
98    /// satisfy the precondition of
99    /// [`Self::metaregion_preserved_under_path_insert`].
100    pub proof fn no_node_at_idx_from_slot_key(
101        self,
102        regions: MetaRegionOwners,
103        changed_idx: usize,
104    )
105        requires
106            self.inv(),
107            regions.inv(),
108            self.metaregion_sound(regions),
109            regions.slots.contains_key(changed_idx),
110        ensures
111            self.no_node_at_idx(changed_idx),
112    {
113        let msp = PageTableOwner::<C>::metaregion_sound_pred(regions);
114        let target = |e: EntryOwner<C>, _p: TreePath<NR_ENTRIES>|
115            e.is_node() && e.meta_slot_paddr() is Some
116                ==> frame_to_index(e.meta_slot_paddr().unwrap()) != changed_idx;
117
118        assert(OwnerSubtree::implies(msp, target)) by {
119            assert forall |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
120                entry.inv() && msp(entry, path)
121            implies #[trigger] target(entry, path) by {
122                if entry.is_node() && entry.meta_slot_paddr() is Some {
123                    EntryOwner::<C>::active_entry_not_in_free_pool(
124                        entry, regions, changed_idx);
125                }
126            };
127        };
128        self.map_children_implies(msp, target);
129
130        assert forall |i: int| #![trigger self.continuations[i]]
131            self.level - 1 <= i < NR_LEVELS
132        implies {
133            let e = self.continuations[i].entry_own;
134            e.is_node() && e.meta_slot_paddr() is Some
135                ==> frame_to_index(e.meta_slot_paddr().unwrap()) != changed_idx
136        } by {
137            let entry = self.continuations[i].entry_own;
138            if entry.is_node() && entry.meta_slot_paddr() is Some {
139                EntryOwner::<C>::active_entry_not_in_free_pool(
140                    entry, regions, changed_idx);
141            }
142        };
143    }
144
145    /// Preservation of the cursor-level metaregion invariants when the only
146    /// change to `regions` is the **insertion** of a new path into the
147    /// `paths_in_pt` set at a single slot.
148    pub proof fn metaregion_preserved_under_path_insert(
149        self,
150        regions0: MetaRegionOwners,
151        regions1: MetaRegionOwners,
152        changed_idx: usize,
153        new_path: TreePath<NR_ENTRIES>,
154    )
155        requires
156            self.inv(),
157            self.metaregion_sound(regions0),
158            regions0.inv(),
159            regions0.slot_owners.contains_key(changed_idx),
160            regions1.slots == regions0.slots,
161            regions1.slot_owners.dom() =~= regions0.slot_owners.dom(),
162            forall |i: usize| #![trigger regions1.slot_owners[i]]
163                i != changed_idx ==> regions0.slot_owners[i] == regions1.slot_owners[i],
164            regions1.slot_owners[changed_idx].inner_perms
165                == regions0.slot_owners[changed_idx].inner_perms,
166            regions1.slot_owners[changed_idx].self_addr
167                == regions0.slot_owners[changed_idx].self_addr,
168            regions1.slot_owners[changed_idx].raw_count
169                == regions0.slot_owners[changed_idx].raw_count,
170            regions1.slot_owners[changed_idx].usage
171                == regions0.slot_owners[changed_idx].usage,
172            regions1.slot_owners[changed_idx].paths_in_pt
173                == regions0.slot_owners[changed_idx].paths_in_pt.insert(new_path),
174            self.no_node_at_idx(changed_idx),
175        ensures
176            self.metaregion_sound(regions1),
177    {
178        let f = PageTableOwner::<C>::metaregion_sound_pred(regions0);
179        let g = PageTableOwner::<C>::metaregion_sound_pred(regions1);
180        let guard = |entry: EntryOwner<C>, _p: TreePath<NR_ENTRIES>|
181            entry.is_node() && entry.meta_slot_paddr() is Some
182                ==> frame_to_index(entry.meta_slot_paddr().unwrap()) != changed_idx;
183        let f_strong = |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
184            f(entry, path) && guard(entry, path);
185
186        assert(OwnerSubtree::implies(f_strong, g)) by {
187            assert forall |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
188                entry.inv() && f_strong(entry, path)
189            implies #[trigger] g(entry, path) by {
190                if entry.meta_slot_paddr() is Some {
191                    let eidx = frame_to_index(entry.meta_slot_paddr().unwrap());
192                    if eidx != changed_idx {
193                        entry.metaregion_sound_one_slot_changed(
194                            regions0, regions1, changed_idx);
195                    } else {
196                        assert(!entry.is_node());
197                        assert(entry.is_frame());
198                        if entry.parent_level > 1 {
199                            assert(entry.frame_sub_pages_valid(regions1));
200                        }
201                    }
202                }
203            };
204        };
205
206        self.and_map_full_tree(f, guard);
207        self.map_children_implies(f_strong, g);
208
209        assert forall |i: int| #![trigger self.continuations[i]]
210            self.level - 1 <= i < NR_LEVELS
211        implies
212            self.continuations[i].entry_own.metaregion_sound(regions1)
213        by {
214            let cont_entry = self.continuations[i].entry_own;
215            if cont_entry.meta_slot_paddr() is Some {
216                cont_entry.metaregion_sound_one_slot_changed(
217                    regions0, regions1, changed_idx);
218            }
219        };
220    }
221}
222
223} // verus!
ostd/specs/mm/page_table/cursor/invariant_preservation_lemmas.rs

ostd/specs/mm/page_table/cursor/
invariant_preservation_lemmas.rs
