ostd/specs/mm/frame/
frame_specs.rs

1use vstd::prelude::*;
2
3use vstd_extra::cast_ptr::*;
4use vstd_extra::ownership::*;
5
6use crate::mm::frame::meta::{get_slot_spec, mapping::frame_to_index, REF_COUNT_UNUSED};
7use crate::mm::frame::*;
8use crate::mm::{Paddr, PagingLevel, Vaddr};
9use crate::specs::arch::mm::{MAX_NR_PAGES, MAX_PADDR, PAGE_SIZE};
10use crate::specs::mm::frame::meta_owners::{MetaPerm, MetaSlotStorage};
11use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
12
13use core::marker::PhantomData;
14
15verus! {
16
17/// A tracked obligation token issued when `from_raw` is called without the
18/// bookkeeping precondition (`raw_count == 1`).  The holder must ensure that
19/// the resulting `Frame` is wrapped in `ManuallyDrop::new` (which increments
20/// `raw_count` to 1) before the `Frame` could be dropped.
21///
22/// The token is linear: Verus requires every tracked value to be consumed,
23/// so the caller is forced to account for it.
24pub tracked struct BorrowDebt {
25    /// Index of the frame slot this debt applies to.
26    pub ghost frame_index: usize,
27    /// The `raw_count` that was observed when `from_raw` was called.
28    pub ghost raw_count_at_issue: usize,
29}
30
31impl BorrowDebt {
32    /// Discharge the debt when the bookkeeping precondition was already met
33    /// (`raw_count` was 1 at the time of `from_raw`).  This is the zero-cost
34    /// path for normal `from_raw` callers.
35    pub proof fn discharge_bookkeeping(tracked self)
36        requires self.raw_count_at_issue == 1,
37    {}
38
39    /// Discharge the debt after the `Frame` has been wrapped in
40    /// `ManuallyDrop::new`, which increments `raw_count` to 1.
41    /// This is the path used by `borrow_paddr`.
42    pub proof fn discharge_with_manual_drop(tracked self, regions: &MetaRegionOwners)
43        requires
44            regions.slot_owners.contains_key(self.frame_index),
45            regions.slot_owners[self.frame_index].raw_count == 1,
46    {}
47}
48
49impl<'a, M: AnyFrameMeta> Frame<M> {
50    // ── from_raw precondition predicates ──
51
52    /// **Safety**: The frame exists and is addressable.  This is sufficient to
53    /// call `from_raw` provided the caller will immediately wrap the result in
54    /// `ManuallyDrop::new` (i.e., the borrow pattern).
55    pub open spec fn from_raw_requires_safety(regions: MetaRegionOwners, paddr: Paddr) -> bool {
56        &&& regions.slot_owners.contains_key(frame_to_index(paddr))
57        &&& regions.slot_owners[frame_to_index(paddr)].self_addr == frame_to_meta(paddr)
58        &&& has_safe_slot(paddr) // TODO: this should actually imply the first condition
59        &&& regions.inv()
60    }
61
62    /// **Bookkeeping**: Exactly one forgotten copy exists (`raw_count == 1`).
63    /// When this holds, the `Frame` returned by `from_raw` may be dropped
64    /// normally (its `drop_requires` is satisfied after `ManuallyDrop::new`
65    /// increments `raw_count`).  When this does *not* hold, the caller must
66    /// wrap the result in `ManuallyDrop::new` to prevent the `Frame` from
67    /// being dropped (`drop_requires` needs `raw_count > 0`).
68    pub open spec fn from_raw_requires_bookkeeping(regions: MetaRegionOwners, paddr: Paddr) -> bool {
69        regions.slot_owners[frame_to_index(paddr)].raw_count == 1
70    }
71
72    /// Full precondition (safety + bookkeeping).  Retained for backward
73    /// compatibility with callers that restore a previously-forgotten frame.
74    pub open spec fn from_raw_requires(regions: MetaRegionOwners, paddr: Paddr) -> bool {
75        &&& Self::from_raw_requires_safety(regions, paddr)
76        &&& Self::from_raw_requires_bookkeeping(regions, paddr)
77    }
78
79    pub open spec fn from_raw_ensures(
80        old_regions: MetaRegionOwners,
81        new_regions: MetaRegionOwners,
82        paddr: Paddr,
83        r: Self,
84    ) -> bool {
85        &&& new_regions.inv()
86        &&& new_regions.slots.contains_key(frame_to_index(paddr))
87        &&& new_regions.slot_owners[frame_to_index(paddr)].raw_count == 0
88        &&& new_regions.slot_owners[frame_to_index(paddr)].inner_perms ==
89            old_regions.slot_owners[frame_to_index(paddr)].inner_perms
90        &&& new_regions.slot_owners[frame_to_index(paddr)].usage ==
91            old_regions.slot_owners[frame_to_index(paddr)].usage
92        &&& new_regions.slot_owners[frame_to_index(paddr)].path_if_in_pt ==
93            old_regions.slot_owners[frame_to_index(paddr)].path_if_in_pt
94        &&& new_regions.slot_owners[frame_to_index(paddr)].self_addr == r.ptr.addr()
95        &&& forall|i: usize|
96            #![trigger new_regions.slot_owners[i], old_regions.slot_owners[i]]
97            i != frame_to_index(paddr) ==> new_regions.slot_owners[i] == old_regions.slot_owners[i]
98        &&& forall|i: usize|
99            i != frame_to_index(paddr) ==>
100            new_regions.slots.contains_key(i) == old_regions.slots.contains_key(i)
101        &&& r.ptr.addr() == frame_to_meta(paddr)
102        &&& r.paddr() == paddr
103    }
104
105
106    // ── into_raw precondition predicates ──
107
108    /// **Safety Invariant**: The frame's structural invariant must hold.
109    pub open spec fn into_raw_pre_frame_inv(self) -> bool {
110        self.inv()
111    }
112
113    /// **Bookkeeping**: The frame must be in use (not unused).
114    pub open spec fn into_raw_pre_not_unused(self, regions: MetaRegionOwners) -> bool {
115        regions.slot_owners[self.index()].inner_perms.ref_count.value() != REF_COUNT_UNUSED
116    }
117
118    // ── into_raw postcondition predicates ──
119
120    /// **Correctness**: The frame's raw count is incremented.
121    pub open spec fn into_raw_post_raw_count_incremented(
122        self,
123        old_regions: MetaRegionOwners,
124        new_regions: MetaRegionOwners,
125    ) -> bool {
126        &&& new_regions.slot_owners.contains_key(self.index())
127        &&& new_regions.slot_owners[self.index()].raw_count
128            == (old_regions.slot_owners[self.index()].raw_count + 1) as usize
129    }
130
131    /// **Safety**: Frames other than this one are not affected by the call.
132    pub open spec fn into_raw_post_noninterference(
133        self,
134        old_regions: MetaRegionOwners,
135        new_regions: MetaRegionOwners,
136    ) -> bool {
137        &&& forall|i: usize|
138            #![trigger new_regions.slots[i], old_regions.slots[i]]
139            i != self.index() && old_regions.slots.contains_key(i)
140                ==> new_regions.slots.contains_key(i)
141                    && new_regions.slots[i] == old_regions.slots[i]
142        &&& forall|i: usize|
143            #![trigger new_regions.slot_owners[i], old_regions.slot_owners[i]]
144            i != self.index() ==> new_regions.slot_owners[i] == old_regions.slot_owners[i]
145        &&& new_regions.slot_owners.dom() =~= old_regions.slot_owners.dom()
146    }
147}
148
149} // verus!
ostd/specs/mm/frame/frame_specs.rs

ostd/specs/mm/frame/
frame_specs.rs
