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    /// When `alloc_if_none` allocates a new node from an absent slot, all existing entries'
73    /// `relate_region` is preserved in the new regions.
74    ///
75    /// Justification: `relate_region_neq_preserved` gives preservation for entries whose paddr
76    /// differs from both old_child and new_child. Old_child is absent (paddr_neq trivially true).
77    /// New_child was freshly allocated from `regions0.slots` (a free slot). By PointsTo
78    /// uniqueness (`active_entry_not_in_free_pool`), no existing entry can share its slot index.
79    /// With both `paddr_neq` conditions, `relate_region_neq_preserved` yields the result.
80    pub proof fn alloc_if_none_relate_region_preserved(
81        old_child: EntryOwner<C>,
82        new_child: EntryOwner<C>,
83        regions0: MetaRegionOwners,
84        regions1: MetaRegionOwners,
85    )
86        requires
87            old_child.is_absent(),
88            old_child.inv(),
89            new_child.is_node(),
90            regions0.inv(),
91            regions0.slots.contains_key(frame_to_index(new_child.meta_slot_paddr().unwrap())),
92            Self::relate_region_neq_preserved(old_child, new_child, regions0, regions1),
93        ensures
94            Self::relate_region_preserved(regions0, regions1),
95    {
96        let new_idx = frame_to_index(new_child.meta_slot_paddr().unwrap());
97        // Use relate_region_pred to get spec_fn values whose application covers both variables,
98        // satisfying Verus's trigger-coverage requirement.
99        let f = PageTableOwner::<C>::relate_region_pred(regions0);
100        let g = PageTableOwner::<C>::relate_region_pred(regions1);
101        assert(Self::relate_region_preserved(regions0, regions1)) by {
102            assert(OwnerSubtree::implies(f, g)) by {
103                assert forall |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
104                    entry.inv() && f(entry, path) implies
105                    #[trigger] g(entry, path)
106                by {
107                    // Part 1: meta_slot_paddr_neq(old_child) — trivial since old_child is absent.
108                    // old_child.inv() + is_absent() ==> node is None && frame is None ==> meta_slot_paddr() is None.
109                    assert(old_child.meta_slot_paddr() is None) by {
110                        assert(!old_child.is_node());
111                        assert(!old_child.is_frame());
112                    };
113                    assert(entry.meta_slot_paddr_neq(old_child));
114
115                    // Part 2: meta_slot_paddr_neq(new_child) — by PointsTo uniqueness.
116                    // If this entry has a paddr, it can't be the same as new_child's free-pool slot.
117                    assert(entry.meta_slot_paddr_neq(new_child)) by {
118                        if entry.meta_slot_paddr() is Some {
119                            // PointsTo uniqueness: a slot in the free pool can't also be active.
120                            EntryOwner::<C>::active_entry_not_in_free_pool(entry, regions0, new_idx);
121                            assert(frame_to_index(entry.meta_slot_paddr().unwrap()) != new_idx);
122                            // frame_to_index is a function: same paddr gives same index,
123                            // so different index implies different paddr.
124                            if entry.meta_slot_paddr().unwrap() == new_child.meta_slot_paddr().unwrap() {
125                                assert(frame_to_index(entry.meta_slot_paddr().unwrap())
126                                    == frame_to_index(new_child.meta_slot_paddr().unwrap()));
127                                assert(false);
128                            }
129                        }
130                    };
131
132                    // Part 3: apply relate_region_neq_preserved.
133                    // The antecedent f(entry, path) = paddr_neq(old) && paddr_neq(new) && relate(r0)
134                    // is fully established; the conclusion g(entry, path) = relate(r1) follows.
135                    assert(entry.meta_slot_paddr_neq(old_child)
136                        && entry.meta_slot_paddr_neq(new_child)
137                        && entry.relate_region(regions0));
138                };
139            };
140        };
141    }
142
143    pub open spec fn path_tracked_pred_preserved(regions0: MetaRegionOwners, regions1: MetaRegionOwners) -> bool {
144        OwnerSubtree::implies(
145            PageTableOwner::<C>::path_tracked_pred(regions0),
146            PageTableOwner::<C>::path_tracked_pred(regions1),
147        )
148    }
149
150    pub open spec fn new_owner_compatible(self,
151        new_child: Child<C>,
152        old_owner: EntryOwner<C>,
153        new_owner: EntryOwner<C>,
154        regions: MetaRegionOwners)
155    -> bool {
156        &&& old_owner.path == new_owner.path
157        &&& old_owner.parent_level == new_owner.parent_level
158        &&& old_owner.meta_slot_paddr_neq(new_owner)
159        &&& new_owner.in_scope
160        &&& new_owner.is_node() ==> {
161            &&& regions.slots.contains_key(frame_to_index(new_owner.meta_slot_paddr().unwrap()))
162            &&& regions.slot_owners[frame_to_index(new_owner.meta_slot_paddr().unwrap())].inner_perms.ref_count.value() !=
163                REF_COUNT_UNUSED
164        }
165    }
166
167    pub open spec fn parent_perms_preserved(self,
168        parent_owner0: NodeOwner<C>,
169        parent_owner1: NodeOwner<C>,
170        guard_perm0: GuardPerm<'rcu, C>,
171        guard_perm1: GuardPerm<'rcu, C>)
172    -> bool {
173        &&& guard_perm0.addr() == guard_perm1.addr()
174        &&& guard_perm0.value().inner.inner@.ptr.addr() == guard_perm1.value().inner.inner@.ptr.addr()
175        &&& forall|i: int| 0 <= i < NR_ENTRIES ==> i != self.idx ==>
176            parent_owner0.children_perm.value()[i] == parent_owner1.children_perm.value()[i]
177    }
178}
179
180} // verus!
ostd/specs/mm/page_table/node/entry.rs

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