ostd/specs/mm/frame/
meta_region_owners.rs

1use vstd::{
2    atomic::*,
3    prelude::*,
4    simple_pptr::{self, *},
5};
6use vstd_extra::{cast_ptr::Repr, ownership::*};
7
8use crate::specs::{
9    arch::{MAX_PADDR, PAGE_SIZE, valid_frame_paddr},
10    mm::frame::mapping::{frame_to_index, index_to_meta, max_meta_slots},
11};
12
13use super::{meta_owners::MetaSlotOwner, *};
14use crate::mm::{
15    Paddr,
16    frame::{
17        Link,
18        meta::{AnyFrameMeta, META_SLOT_SIZE, MetaSlot, REF_COUNT_MAX, mapping::frame_to_meta},
19    },
20    kspace::FRAME_METADATA_RANGE,
21};
22use core::ops::Range;
23
24verus! {
25
26/// Represents the ownership of the meta-frame memory region.
27/// # Verification Design
28/// ## Slot owners and permissions
29/// Every metadata slot has its owner ([`MetaSlotOwner`]) tracked by the `slot_owners` map at all times.
30/// Likewise, every slot has an permission stored in `slots`.
31#[verifier::ext_equal]
32pub tracked struct MetaRegionOwners {
33    pub slots: Map<int, &'static simple_pptr::PointsTo<MetaSlot>>,
34    pub slot_owners: Map<int, MetaSlotOwner>,
35}
36
37impl Inv for MetaRegionOwners {
38    open spec fn inv(self) -> bool {
39        &&& {
40            // Keep the map-membership trigger: callers frequently expose a
41            // slot-owner lookup without mentioning the `contains` wrapper.
42            forall|i: int|
43                0 <= i < max_meta_slots() <==> #[trigger] self.slot_owners.contains_key(i)
44        }
45        &&& {
46            forall|i: int| #[trigger]
47                self.slot_owners.contains_key(i) ==> self.slots.contains_key(i)
48        }
49        &&& { forall|i: int| #[trigger] self.slots.contains_key(i) ==> 0 <= i < max_meta_slots() }
50        &&& {
51            forall|i: int| #[trigger]
52                self.slots.contains_key(i) ==> {
53                    &&& self.slot_owners[i].inv()
54                    &&& self.slots[i].is_init()
55                    &&& self.slots[i].addr() == index_to_meta(i)
56                    &&& self.slots[i].value().wf(self.slot_owners[i])
57                    &&& self.slot_owners[i].slot_vaddr == self.slots[i].addr()
58                }
59        }
60    }
61}
62
63impl MetaRegionOwners {
64    /// Returns whether the slot permission and its corresponding owner are both present.
65    pub open spec fn contains(self, index: int) -> bool {
66        &&& self.slot_owners.contains_key(index)
67        &&& self.slots.contains_key(index)
68    }
69
70    pub open spec fn insert_slot_owner(self, paddr: Paddr, owner: MetaSlotOwner) -> Self {
71        let index = frame_to_index(paddr);
72        Self { slot_owners: self.slot_owners.insert(index, owner), ..self }
73    }
74
75    pub open spec fn ref_count(self, i: int) -> (res: u64)
76        recommends
77            0 <= i < max_meta_slots(),
78    {
79        self.slot_owners[i].ref_count()
80    }
81
82    pub open spec fn paddr_range_not_mapped(self, range: Range<Paddr>) -> bool
83        recommends
84            range.start < range.end < MAX_PADDR,
85    {
86        forall|paddr: Paddr|
87            #![trigger frame_to_index(paddr)]
88            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0) ==> self.slot_owner(
89                paddr,
90            ).paths_in_pt.is_empty()
91    }
92
93    pub proof fn lemma_contains_valid_frame_paddr(self, paddr: usize)
94        requires
95            valid_frame_paddr(paddr),
96            self.inv(),
97        ensures
98            self.contains(frame_to_index(paddr)),
99    {
100    }
101
102    /// Rertuns the `MetaSlotOwner`, indexed by frame paddr.
103    pub open spec fn slot_owner(self, paddr: Paddr) -> MetaSlotOwner {
104        self.slot_owners[frame_to_index(paddr)]
105    }
106
107    /// Borrows the metadata slot permission, indexed by frame paddr.
108    pub proof fn tracked_borrow_slot(
109        tracked &self,
110        paddr: Paddr,
111    ) -> tracked &'static simple_pptr::PointsTo<MetaSlot>
112        requires
113            valid_frame_paddr(paddr),
114            self.inv(),
115        returns
116            self.slots[frame_to_index(paddr)],
117    {
118        self.lemma_contains_valid_frame_paddr(paddr);
119        *self.slots.tracked_borrow(frame_to_index(paddr))
120    }
121
122    /// Borrows the `MetaSlotOwner`, indexed by frame paddr.
123    pub proof fn tracked_borrow_slot_owner(tracked &self, paddr: Paddr) -> tracked &MetaSlotOwner
124        requires
125            valid_frame_paddr(paddr),
126            self.inv(),
127        returns
128            self.slot_owner(paddr),
129    {
130        self.lemma_contains_valid_frame_paddr(paddr);
131        self.slot_owners.tracked_borrow(frame_to_index(paddr))
132    }
133
134    /// Mutably borrows the `MetaSlotOwner`, indexed by frame paddr.
135    pub proof fn tracked_borrow_mut_slot_owner(tracked &mut self, paddr: Paddr) -> (tracked ret:
136        &mut MetaSlotOwner)
137        requires
138            valid_frame_paddr(paddr),
139            self.inv(),
140        ensures
141            *ret == old(self).slot_owner(paddr),
142            *final(self) == old(self).insert_slot_owner(paddr, *final(ret)),
143    {
144        self.lemma_contains_valid_frame_paddr(paddr);
145        self.slot_owners.tracked_borrow_mut(frame_to_index(paddr))
146    }
147
148    /// The metadata region transition of claiming a currently shared slot.
149    pub open spec fn inc_frame_reference_region_spec(self, paddr: Paddr, post: Self) -> bool {
150        let idx = frame_to_index(paddr);
151        let pre_owner = self.slot_owners[idx];
152        let post_owner = post.slot_owners[idx];
153        {
154            &&& post.ref_count(idx) == self.ref_count(idx) + 1
155            &&& post_owner.ref_count_perm.id() == pre_owner.ref_count_perm.id()
156            &&& post_owner.metadata_perm.id() == pre_owner.metadata_perm.id()
157            &&& post_owner.metadata_perm.frac() + 1 == pre_owner.metadata_perm.frac()
158            &&& post_owner.metadata_perm@ == pre_owner.metadata_perm@
159            &&& post_owner.in_list_perm == pre_owner.in_list_perm
160            &&& post_owner.slot_vaddr == pre_owner.slot_vaddr
161            &&& post_owner.usage == pre_owner.usage
162            &&& post_owner.paths_in_pt == pre_owner.paths_in_pt
163            &&& post =~= self.insert_slot_owner(paddr, post_owner)
164        }
165    }
166}
167
168} // verus!
ostd/specs/mm/frame/meta_region_owners.rs

ostd/specs/mm/frame/
meta_region_owners.rs
