ostd/specs/mm/frame/
meta_specs.rs

1use vstd::cell;
2use vstd::prelude::*;
3use vstd::simple_pptr::{self, PPtr};
4
5use vstd_extra::cast_ptr::*;
6use vstd_extra::ownership::*;
7
8use super::meta_owners::{MetaSlotModel, MetaSlotStatus, PageUsage};
9use crate::mm::frame::meta::{
10    get_slot_spec,
11    mapping::{frame_to_index, frame_to_meta},
12    REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED,
13};
14use crate::mm::frame::*;
15use crate::mm::{Paddr, PagingLevel, Vaddr};
16use crate::specs::arch::mm::{MAX_NR_PAGES, MAX_PADDR, PAGE_SIZE};
17use crate::specs::mm::frame::meta_region_owners::{MetaRegionModel, MetaRegionOwners};
18
19use core::marker::PhantomData;
20
21verus! {
22
23impl MetaSlot {
24    #[rustc_allow_incoherent_impl]
25    pub open spec fn from_unused_slot_spec<M: AnyFrameMeta>(
26        paddr: Paddr,
27        metadata: M,
28        as_unique_ptr: bool,
29    ) -> MetaSlotModel {
30        let (rc, status) = if as_unique_ptr {
31            (REF_COUNT_UNIQUE, MetaSlotStatus::UNIQUE)
32        } else {
33            (1, MetaSlotStatus::SHARED)
34        };
35        MetaSlotModel {
36            status,
37            storage: cell::MemContents::Uninit,  //TODO: fix this cell::MemContents::Init(metadata.to_repr()),
38            ref_count: rc,
39            vtable_ptr: simple_pptr::MemContents::Init(metadata.vtable_ptr()),
40            in_list: 0,
41            self_addr: frame_to_meta(paddr),
42            usage: PageUsage::Frame,
43        }
44    }
45
46    #[rustc_allow_incoherent_impl]
47    pub open spec fn get_from_unused_spec<M: AnyFrameMeta>(
48        paddr: Paddr,
49        metadata: M,
50        as_unique_ptr: bool,
51        // -- ghost parameters --
52        pre: MetaRegionModel,
53    ) -> (PPtr<MetaSlot>, MetaRegionModel)
54        recommends
55            paddr % 4096 == 0,
56            paddr < MAX_PADDR(),
57            pre.inv(),
58            pre.slots[frame_to_index(paddr)].ref_count == REF_COUNT_UNUSED,
59    {
60        let ptr = get_slot_spec(paddr);
61        let idx = frame_to_index(paddr);
62
63        let post = MetaRegionModel {
64            slots: pre.slots.insert(
65                idx,
66                Self::from_unused_slot_spec(paddr, metadata, as_unique_ptr),
67            ),
68        };
69        (ptr, post)
70    }
71
72    /// All other slots remain unchanged.
73    #[rustc_allow_incoherent_impl]
74    pub open spec fn update_index_tracked(
75        idx: usize,
76        pre: MetaRegionOwners,
77        post: MetaRegionOwners,
78    ) -> bool
79        recommends
80            pre.slots.contains_key(idx),
81    {
82        &&& pre.slots.dom() == post.slots.dom()
83        &&& pre.dropped_slots.dom() == post.dropped_slots.dom()
84        &&& pre.slot_owners.dom() == post.slot_owners.dom()
85        &&& forall|i: usize| #[trigger]
86            pre.slots.contains_key(i) && i != idx ==> pre.slots[i] == post.slots[i]
87        &&& forall|i: usize| #[trigger]
88            pre.dropped_slots.contains_key(i) && i != idx ==> pre.dropped_slots[i]
89                == post.dropped_slots[i]
90        &&& forall|i: usize| #[trigger]
91            pre.slot_owners.contains_key(i) && i != idx ==> pre.slot_owners[i]
92                == post.slot_owners[i]
93    }
94
95    #[rustc_allow_incoherent_impl]
96    pub open spec fn get_from_unused_tracked<M: AnyFrameMeta>(
97        paddr: Paddr,
98        metadata: M,
99        as_unique_ptr: bool,
100        // -- ghost parameters --
101        pre: MetaRegionOwners,
102        post: MetaRegionOwners,
103    ) -> bool
104        recommends
105            paddr % 4096 == 0,
106            paddr < MAX_PADDR(),
107            pre.inv(),
108            pre.view().slots[paddr / 4096].ref_count == REF_COUNT_UNUSED,
109    {
110        let idx = paddr / 4096;
111        {
112            &&& Self::update_index_tracked(idx, pre, post)
113            &&& Self::get_from_unused_spec(paddr, metadata, as_unique_ptr, pre.view()).1
114                == post.view()
115        }
116    }
117
118    #[rustc_allow_incoherent_impl]
119    pub open spec fn get_from_in_use_spec(paddr: Paddr, pre: MetaRegionModel) -> (
120        PPtr<MetaSlot>,
121        MetaRegionModel,
122    )
123        recommends
124            paddr % 4096 == 0,
125            paddr < MAX_PADDR(),
126            pre.inv(),
127            0 <= pre.slots[paddr / 4096].ref_count < REF_COUNT_MAX,
128    {
129        let ptr = get_slot_spec(paddr);
130        let idx = paddr / 4096;
131        let pre_slot = pre.slots[idx];
132        let post = MetaRegionModel {
133            slots: pre.slots.insert(
134                idx,
135                MetaSlotModel { ref_count: (pre_slot.ref_count + 1) as u64, ..pre_slot },
136            ),
137        };
138        (ptr, post)
139    }
140
141    #[rustc_allow_incoherent_impl]
142    pub open spec fn get_from_in_use_tracked(
143        paddr: Paddr,
144        // -- ghost parameters --
145        pre: MetaRegionOwners,
146        post: MetaRegionOwners,
147    ) -> bool
148        recommends
149            paddr % 4096 == 0,
150            paddr < MAX_PADDR(),
151            pre.inv(),
152            0 <= pre.view().slots[paddr / 4096].ref_count < REF_COUNT_MAX,
153    {
154        let idx = paddr / 4096;
155        {
156            &&& Self::update_index_tracked(idx, pre, post)
157            &&& Self::get_from_in_use_spec(paddr, pre.view()).1 == post.view()
158        }
159    }
160
161    #[rustc_allow_incoherent_impl]
162    pub open spec fn inc_ref_count_spec(&self, pre: MetaSlotModel) -> (MetaSlotModel)
163        recommends
164            pre.inv(),
165            pre.status == MetaSlotStatus::SHARED,
166    {
167        MetaSlotModel { ref_count: (pre.ref_count + 1) as u64, ..pre }
168    }
169}
170
171impl<M: AnyFrameMeta + Repr<MetaSlot> + OwnerOf> Frame<M> {
172    #[rustc_allow_incoherent_impl]
173    pub open spec fn from_raw_spec(paddr: Paddr) -> Self {
174        Frame::<M> {
175            ptr: PPtr::<MetaSlot>(frame_to_meta(paddr), PhantomData),
176            _marker: PhantomData,
177        }
178    }
179}
180
181} // verus!
ostd/specs/mm/frame/meta_specs.rs

ostd/specs/mm/frame/
meta_specs.rs
