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<'a, 'rcu, C: PageTableConfig> Entry<'a, '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(
24        self,
25        owner: EntryOwner<C>,
26        parent_owner: NodeOwner<C>,
27        guard: PageTableGuard<'rcu, C>,
28    ) -> bool {
29        &&& parent_owner.level == owner.parent_level
30        &&& parent_owner.inv()
31        &&& guard.inner.inner@.ptr.addr() == parent_owner.meta_addr_self()
32        &&& guard.inner.inner@.wf(parent_owner)
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(
37        regions0: MetaRegionOwners,
38        regions1: MetaRegionOwners,
39    ) -> bool {
40        OwnerSubtree::implies(
41            |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| entry.metaregion_sound(regions0),
42            |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| entry.metaregion_sound(regions1),
43        )
44    }
45
46    pub open spec fn replace_nonpanic_condition(
47        parent_owner: NodeOwner<C>,
48        new_owner: EntryOwner<C>,
49    ) -> bool {
50        if new_owner.is_node() {
51            parent_owner.level - 1 == new_owner.node.unwrap().level
52        } else if new_owner.is_frame() {
53            parent_owner.level == new_owner.parent_level
54        } else {
55            true
56        }
57    }
58
59    pub open spec fn metaregion_sound_neq_preserved(
60        old_entry_owner: EntryOwner<C>,
61        new_entry_owner: EntryOwner<C>,
62        regions0: MetaRegionOwners,
63        regions1: MetaRegionOwners,
64    ) -> bool {
65        OwnerSubtree::implies(
66            |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
67                entry.meta_slot_paddr_neq(old_entry_owner) && entry.meta_slot_paddr_neq(
68                    new_entry_owner,
69                ) && entry.metaregion_sound(regions0),
70            |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| entry.metaregion_sound(regions1),
71        )
72    }
73
74    /// When the new child is NOT a node, `into_pte` doesn't modify `raw_count`.
75    /// Only `paths_in_pt` changes at `new_idx`, which `metaregion_sound` doesn't inspect.
76    /// So entries with `paddr_neq(old_child)` preserve `metaregion_sound` — no
77    /// `paddr_neq(new_child)` needed.
78    pub open spec fn metaregion_sound_neq_old_preserved(
79        old_entry_owner: EntryOwner<C>,
80        regions0: MetaRegionOwners,
81        regions1: MetaRegionOwners,
82    ) -> bool {
83        OwnerSubtree::implies(
84            |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
85                entry.meta_slot_paddr_neq(old_entry_owner) && entry.metaregion_sound(regions0),
86            |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>| 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(
108                new_child.meta_slot_paddr().unwrap(),
109            )].inner_perms.ref_count.value() == REF_COUNT_UNUSED,
110            // Allocator-pool / MMIO disjointness: the freshly-allocated node's
111            // paddr is non-MMIO. Rules out an MMIO-frame entry sitting at the
112            // same idx as the new node (delivered by `PageTableNode::alloc`).
113            !crate::specs::mm::frame::meta_owners::is_mmio_paddr(
114                new_child.meta_slot_paddr().unwrap(),
115            ),
116            Self::metaregion_sound_neq_preserved(old_child, new_child, regions0, regions1),
117        ensures
118            Self::metaregion_sound_preserved(regions0, regions1),
119    {
120        broadcast use crate::specs::mm::frame::meta_owners::axiom_mmio_usage_iff_mmio_paddr;
121
122        let new_idx = frame_to_index(new_child.meta_slot_paddr().unwrap());
123        let f = PageTableOwner::<C>::metaregion_sound_pred(regions0);
124        let g = PageTableOwner::<C>::metaregion_sound_pred(regions1);
125
126        assert(old_child.meta_slot_paddr() is None);
127
128        assert forall|entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
129            entry.inv() && f(entry, path) implies #[trigger] g(entry, path) by {
130            if entry.meta_slot_paddr() is Some && entry.is_node() {
131                EntryOwner::<C>::active_entry_not_in_free_pool(entry, regions0, new_idx);
132            }
133            // Frame entries colliding at new_idx are ruled out: either the
134            // slot's `usage != MMIO` (then `metaregion_sound` requires
135            // `rc != UNUSED`, contradicting the precondition), or the slot's
136            // `usage == MMIO` (then by axiom the paddr is MMIO, contradicting
137            // the allocator's non-MMIO guarantee).
138
139        };
140    }
141
142    pub open spec fn path_tracked_pred_preserved(
143        regions0: MetaRegionOwners,
144        regions1: MetaRegionOwners,
145    ) -> bool {
146        OwnerSubtree::implies(
147            PageTableOwner::<C>::path_tracked_pred(regions0),
148            PageTableOwner::<C>::path_tracked_pred(regions1),
149        )
150    }
151
152    pub open spec fn new_owner_compatible(
153        self,
154        new_child: Child<C>,
155        old_owner: EntryOwner<C>,
156        new_owner: EntryOwner<C>,
157        regions: MetaRegionOwners,
158    ) -> bool {
159        &&& old_owner.path == new_owner.path
160        &&& old_owner.parent_level == new_owner.parent_level
161        &&& new_owner.in_scope
162        &&& new_owner.is_node() ==> {
163            &&& regions.slots.contains_key(frame_to_index(new_owner.meta_slot_paddr().unwrap()))
164            &&& regions.slot_owners[frame_to_index(
165                new_owner.meta_slot_paddr().unwrap(),
166            )].inner_perms.ref_count.value() != REF_COUNT_UNUSED
167        }
168    }
169
170    pub open spec fn parent_perms_preserved(
171        self,
172        parent_owner0: NodeOwner<C>,
173        parent_owner1: NodeOwner<C>,
174    ) -> bool {
175        &&& forall|i: int|
176            0 <= i < NR_ENTRIES ==> i != self.idx ==> parent_owner0.children_perm.value()[i]
177                == parent_owner1.children_perm.value()[i]
178        &&& parent_owner1.slot_index == parent_owner0.slot_index
179        &&& parent_owner1.level == parent_owner0.level
180        &&& parent_owner1.tree_level == parent_owner0.tree_level
181        &&& parent_owner1.meta_own.nr_children.id() == parent_owner0.meta_own.nr_children.id()
182        &&& parent_owner1.meta_own.stray == parent_owner0.meta_own.stray
183    }
184}
185
186} // verus!
ostd/specs/mm/page_table/node/entry.rs

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