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

ostd/specs/mm/frame/
meta_region_owners.rs
