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    /// Discharge the debt in the proof of
49    /// `lemma_from_raw_manuallydrop_general`, where the state observed is
50    /// the immediate post-`from_raw` state (`raw_count == 0`). The lemma
51    /// itself proves that the subsequent `ManuallyDrop::new` restores the
52    /// bookkeeping, so consuming the debt here is sound.
53    pub proof fn discharge_in_lemma(tracked self, regions: &MetaRegionOwners)
54        requires
55            regions.slot_owners.contains_key(self.frame_index),
56            regions.slot_owners[self.frame_index].raw_count == 0,
57    {}
58}
59
60impl<'a, M: AnyFrameMeta> Frame<M> {
61    // ── from_raw precondition predicates ──
62
63    /// **Safety**: The frame exists and is addressable.  This is sufficient to
64    /// call `from_raw` provided the caller will immediately wrap the result in
65    /// `ManuallyDrop::new` (i.e., the borrow pattern).
66    pub open spec fn from_raw_requires_safety(regions: MetaRegionOwners, paddr: Paddr) -> bool {
67        &&& regions.slot_owners.contains_key(frame_to_index(paddr))
68        &&& regions.slot_owners[frame_to_index(paddr)].self_addr == frame_to_meta(paddr)
69        &&& has_safe_slot(paddr) // TODO: this should actually imply the first condition
70        &&& regions.inv()
71    }
72
73    /// **Bookkeeping**: Exactly one forgotten copy exists (`raw_count == 1`).
74    /// When this holds, the `Frame` returned by `from_raw` may be dropped
75    /// normally (its `drop_requires` is satisfied after `ManuallyDrop::new`
76    /// increments `raw_count`).  When this does *not* hold, the caller must
77    /// wrap the result in `ManuallyDrop::new` to prevent the `Frame` from
78    /// being dropped (`drop_requires` needs `raw_count > 0`).
79    pub open spec fn from_raw_requires_bookkeeping(regions: MetaRegionOwners, paddr: Paddr) -> bool {
80        regions.slot_owners[frame_to_index(paddr)].raw_count == 1
81    }
82
83    /// Full precondition (safety + bookkeeping).  Retained for backward
84    /// compatibility with callers that restore a previously-forgotten frame.
85    pub open spec fn from_raw_requires(regions: MetaRegionOwners, paddr: Paddr) -> bool {
86        &&& Self::from_raw_requires_safety(regions, paddr)
87        &&& Self::from_raw_requires_bookkeeping(regions, paddr)
88    }
89
90    pub open spec fn from_raw_ensures(
91        old_regions: MetaRegionOwners,
92        new_regions: MetaRegionOwners,
93        paddr: Paddr,
94        r: Self,
95    ) -> bool {
96        &&& new_regions.inv()
97        &&& new_regions.slots.contains_key(frame_to_index(paddr))
98        &&& new_regions.slot_owners[frame_to_index(paddr)].raw_count == 0
99        &&& new_regions.slot_owners[frame_to_index(paddr)].inner_perms ==
100            old_regions.slot_owners[frame_to_index(paddr)].inner_perms
101        &&& new_regions.slot_owners[frame_to_index(paddr)].usage ==
102            old_regions.slot_owners[frame_to_index(paddr)].usage
103        &&& new_regions.slot_owners[frame_to_index(paddr)].paths_in_pt ==
104            old_regions.slot_owners[frame_to_index(paddr)].paths_in_pt
105        &&& new_regions.slot_owners[frame_to_index(paddr)].self_addr == r.ptr.addr()
106        &&& forall|i: usize|
107            #![trigger new_regions.slot_owners[i], old_regions.slot_owners[i]]
108            i != frame_to_index(paddr) ==> new_regions.slot_owners[i] == old_regions.slot_owners[i]
109        &&& forall|i: usize|
110            i != frame_to_index(paddr) ==>
111            new_regions.slots.contains_key(i) == old_regions.slots.contains_key(i)
112        &&& r.ptr.addr() == frame_to_meta(paddr)
113        &&& r.paddr() == paddr
114    }
115
116
117    // ── into_raw precondition predicates ──
118
119    /// **Safety Invariant**: The frame's structural invariant must hold.
120    pub open spec fn into_raw_pre_frame_inv(self) -> bool {
121        self.inv()
122    }
123
124    /// **Bookkeeping**: The frame must be in use (not unused).
125    pub open spec fn into_raw_pre_not_unused(self, regions: MetaRegionOwners) -> bool {
126        regions.slot_owners[self.index()].inner_perms.ref_count.value() != REF_COUNT_UNUSED
127    }
128
129    // ── into_raw postcondition predicates ──
130
131    /// **Correctness**: The frame's raw count is incremented.
132    pub open spec fn into_raw_post_raw_count_incremented(
133        self,
134        old_regions: MetaRegionOwners,
135        new_regions: MetaRegionOwners,
136    ) -> bool {
137        &&& new_regions.slot_owners.contains_key(self.index())
138        &&& new_regions.slot_owners[self.index()].raw_count
139            == (old_regions.slot_owners[self.index()].raw_count + 1) as usize
140    }
141
142    /// **Safety**: Frames other than this one are not affected by the call.
143    pub open spec fn into_raw_post_noninterference(
144        self,
145        old_regions: MetaRegionOwners,
146        new_regions: MetaRegionOwners,
147    ) -> bool {
148        &&& forall|i: usize|
149            #![trigger new_regions.slots[i], old_regions.slots[i]]
150            i != self.index() && old_regions.slots.contains_key(i)
151                ==> new_regions.slots.contains_key(i)
152                    && new_regions.slots[i] == old_regions.slots[i]
153        &&& forall|i: usize|
154            #![trigger new_regions.slot_owners[i], old_regions.slot_owners[i]]
155            i != self.index() ==> new_regions.slot_owners[i] == old_regions.slot_owners[i]
156        &&& new_regions.slot_owners.dom() =~= old_regions.slot_owners.dom()
157    }
158}
159
160} // verus!
ostd/specs/mm/frame/frame_specs.rs

ostd/specs/mm/frame/
frame_specs.rs
