ostd/mm/frame/
segment.rs

1// SPDX-License-Identifier: MPL-2.0
2//! A contiguous range of frames.
3use vstd::prelude::*;
4use vstd_extra::seq_extra::{seq_tracked_map_values, seq_tracked_subrange};
5
6use core::{fmt::Debug, ops::Range};
7
8use crate::mm::frame::{inc_frame_ref_count, untyped::AnyUFrameMeta, Frame};
9
10use vstd_extra::cast_ptr::*;
11use vstd_extra::cast_ptr::*;
12use vstd_extra::ownership::*;
13
14use super::meta::mapping::{frame_to_index, frame_to_index_spec, frame_to_meta, meta_addr};
15use super::{AnyFrameMeta, GetFrameError, MetaPerm, MetaSlot};
16use crate::mm::{Paddr, PagingLevel, Vaddr};
17use crate::specs::arch::mm::{MAX_NR_PAGES, MAX_PADDR, PAGE_SIZE};
18use crate::specs::mm::frame::meta_owners::*;
19use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
20use vstd_extra::drop_tracking::*;
21
22verus! {
23
24/// A contiguous range of homogeneous physical memory frames.
25///
26/// This is a handle to multiple contiguous frames. It will be more lightweight
27/// than owning an array of frame handles.
28///
29/// The ownership is achieved by the reference counting mechanism of frames.
30/// When constructing a [`Segment`], the frame handles are created then
31/// forgotten, leaving the reference count. When dropping a it, the frame
32/// handles are restored and dropped, decrementing the reference count.
33///
34/// All the metadata of the frames are homogeneous, i.e., they are of the same
35/// type.
36#[repr(transparent)]
37pub struct Segment<M: AnyFrameMeta + ?Sized> {
38    /// The physical address range of the segment.
39    pub range: Range<Paddr>,
40    /// Marker for the metadata type.
41    pub _marker: core::marker::PhantomData<M>,
42}
43
44// TODO: treat `manually_drop` as equivalent to `into_raw`
45impl<M: AnyFrameMeta + ?Sized> TrackDrop for Segment<M> {
46    type State = MetaRegionOwners;
47
48    open spec fn constructor_requires(self, s: Self::State) -> bool {
49        true
50    }
51
52    open spec fn constructor_ensures(self, s0: Self::State, s1: Self::State) -> bool {
53        s0 =~= s1
54    }
55
56    proof fn constructor_spec(self, tracked s: &mut Self::State) {
57        admit()
58    }
59
60    open spec fn drop_requires(self, s: Self::State) -> bool {
61        true
62    }
63
64    open spec fn drop_ensures(self, s0: Self::State, s1: Self::State) -> bool {
65        s0 =~= s1
66    }
67
68    proof fn drop_spec(self, tracked s: &mut Self::State) {
69        admit()
70    }
71}
72
73/// A [`SegmentOwner<M>`] holds the permission tokens for all frames in the
74/// [`Segment<M>`] for verification purposes.
75pub tracked struct SegmentOwner<M: AnyFrameMeta + ?Sized> {
76    /// The permissions for all frames in the segment, which must be well-formed and valid.
77    pub perms: Seq<MetaPerm<M>>,
78}
79
80impl<M: AnyFrameMeta + ?Sized> Inv for Segment<M> {
81    /// The invariant of a [`Segment`]:
82    ///
83    /// - the physical addresses of the frames are aligned and within bounds.
84    /// - the range is well-formed, i.e., the start is less than or equal to the end.
85    open spec fn inv(self) -> bool {
86        &&& self.range.start % PAGE_SIZE == 0
87        &&& self.range.end % PAGE_SIZE == 0
88        &&& self.range.start <= self.range.end < MAX_PADDR
89    }
90}
91
92impl<M: AnyFrameMeta + ?Sized> Inv for SegmentOwner<M> {
93    /// The invariant of a [`Segment`]:
94    ///
95    /// - the permissions are well-formed and valid;
96    /// - the physical addresses of the permissions are aligned and within bounds.
97    open spec fn inv(self) -> bool {
98        &&& forall|i: int|
99            #![trigger self.perms[i]]
100            0 <= i < self.perms.len() as int ==> {
101                &&& self.perms[i].addr() % PAGE_SIZE == 0
102                &&& self.perms[i].addr() < MAX_PADDR
103                &&& self.perms[i].wf(&self.perms[i].inner_perms)
104                &&& self.perms[i].is_init()
105            }
106    }
107}
108
109impl<M: AnyFrameMeta + ?Sized> Segment<M> {
110    /// The invariant of a [`Segment`] with a specific owner, such that besides [`Self::inv`]:
111    ///
112    /// - the number of permissions in the owner matches the number of frames in the segment;
113    /// - the physical address of each permission matches the corresponding frame in the segment.
114    ///
115    /// Interested readers are encouraged to see [`frame_to_index`] and [`meta_addr`] for how
116    /// we convert between physical addresses and meta region indices.
117    pub open spec fn inv_with(&self, owner: &SegmentOwner<M>) -> bool {
118        &&& self.inv()
119        &&& owner.perms.len() * PAGE_SIZE == self.range.end - self.range.start
120        &&& forall|i: int|
121            #![trigger owner.perms[i]]
122            0 <= i < owner.perms.len() as int ==> owner.perms[i].addr() == meta_addr(
123                frame_to_index((self.range.start + i * PAGE_SIZE) as usize),
124            )
125    }
126}
127
128/// A contiguous range of homogeneous untyped physical memory frames that have any metadata.
129///
130/// In other words, the metadata of the frames are of the same type, and they
131/// are untyped, but the type of metadata is not known at compile time. An
132/// [`USegment`] as a parameter accepts any untyped segments.
133///
134/// The usage of this frame will not be changed while this object is alive.
135pub type USegment = Segment<dyn AnyUFrameMeta>;
136
137#[verus_verify]
138impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Segment<M> {
139    /// Returns the starting physical address of the contiguous frames.
140    #[verifier::inline]
141    pub open spec fn start_paddr_spec(&self) -> Paddr
142        recommends
143            self.inv(),
144    {
145        self.range.start
146    }
147
148    /// Returns the ending physical address of the contiguous frames.
149    #[verifier::inline]
150    pub open spec fn end_paddr_spec(&self) -> Paddr
151        recommends
152            self.inv(),
153    {
154        self.range.end
155    }
156
157    /// Returns the length in bytes of the contiguous frames.
158    #[verifier::inline]
159    pub open spec fn size_spec(&self) -> usize
160        recommends
161            self.inv(),
162    {
163        (self.range.end - self.range.start) as usize
164    }
165
166    /// Returns the number of pages of the contiguous frames.
167    #[verifier::inline]
168    pub open spec fn nrpage_spec(&self) -> usize
169        recommends
170            self.inv(),
171    {
172        self.size_spec() / PAGE_SIZE
173    }
174
175    /// Splits the contiguous frames into two at the given byte offset from the start in spec mode.
176    pub open spec fn split_spec(self, offset: usize) -> (Self, Self)
177        recommends
178            self.inv(),
179            offset % PAGE_SIZE == 0,
180            0 < offset < self.size_spec(),
181    {
182        let at = (self.range.start + offset) as usize;
183        let idx = at / PAGE_SIZE;
184        (
185            Self { range: self.range.start..at, _marker: core::marker::PhantomData },
186            Self { range: at..self.range.end, _marker: core::marker::PhantomData },
187        )
188    }
189
190    /// Gets the start physical address of the contiguous frames.
191    #[inline(always)]
192    #[verifier::when_used_as_spec(start_paddr_spec)]
193    pub fn start_paddr(&self) -> (res: Paddr)
194        requires
195            self.inv(),
196        returns
197            self.start_paddr_spec(),
198    {
199        self.range.start
200    }
201
202    /// Gets the end physical address of the contiguous frames.
203    #[inline(always)]
204    #[verifier::when_used_as_spec(end_paddr_spec)]
205    pub fn end_paddr(&self) -> (res: Paddr)
206        requires
207            self.inv(),
208        returns
209            self.end_paddr_spec(),
210    {
211        self.range.end
212    }
213
214    /// Gets the length in bytes of the contiguous frames.
215    #[inline(always)]
216    #[verifier::when_used_as_spec(size_spec)]
217    pub fn size(&self) -> (res: usize)
218        requires
219            self.inv(),
220        returns
221            self.size_spec(),
222    {
223        self.range.end - self.range.start
224    }
225
226    /// The wrapper for the precondition for [`Self::from_unused`]:
227    ///
228    /// - the metadata function must be well-formed and valid for all frames in the range;
229    /// - the metadata function must ensure that the frames can be created and owned by the segment.
230    /// - for any frame created via the closure `metadata_fn`, the corresponding slot in `regions`
231    ///   must be unused and not dropped in the owner ([`MetaRegionOwners`]).
232    pub open spec fn from_unused_requires(
233        regions: MetaRegionOwners,
234        range: Range<Paddr>,
235        metadata_fn: impl Fn(Paddr) -> (Paddr, M),
236    ) -> bool {
237        &&& regions.inv()
238        &&& range.start % PAGE_SIZE == 0
239        &&& range.end % PAGE_SIZE == 0
240        &&& range.start <= range.end < MAX_PADDR
241        &&& forall|paddr_in: Paddr|
242            (range.start <= paddr_in < range.end && paddr_in % PAGE_SIZE == 0) ==> {
243                &&& metadata_fn.requires((paddr_in,))
244            }
245        &&& forall|paddr_in: Paddr, paddr_out: Paddr, m: M|
246            metadata_fn.ensures((paddr_in,), (paddr_out, m)) ==> {
247                &&& paddr_out < MAX_PADDR
248                &&& paddr_out % PAGE_SIZE == 0
249                &&& paddr_in == paddr_out
250                &&& regions.slots.contains_key(frame_to_index(paddr_out))
251                &&& regions.slot_owners[frame_to_index(paddr_out)].usage is Unused
252                &&& regions.slot_owners[frame_to_index(paddr_out)].inner_perms.in_list.points_to(0)
253            }
254    }
255
256    /// The wrapper for the postcondition for [`Self::from_unused`]:
257    ///
258    /// - if the result is `Ok`, then the returned segment must satisfy the invariant with the owner;
259    /// - the returned segment must have the same physical address range as the input;
260    /// - the returned owner must be `Some` if the result is `Ok`, and the owner must satisfy the invariant;
261    pub open spec fn from_unused_ensures(
262        old_regions: MetaRegionOwners,
263        new_regions: MetaRegionOwners,
264        owner: Option<SegmentOwner<M>>,
265        range: Range<Paddr>,
266        metadata_fn: impl Fn(Paddr) -> (Paddr, M),
267        r: Result<Self, GetFrameError>,
268    ) -> bool {
269        &&& r matches Ok(r) ==> {
270            &&& new_regions.inv()
271            &&& r.range.start == range.start
272            &&& r.range.end == range.end
273            &&& owner matches Some(owner) && {
274                &&& r.inv_with(&owner)
275                &&& forall|i: int|
276                    #![trigger owner.perms[i]]
277                    0 <= i < owner.perms.len() as int ==> {
278                        &&& owner.perms[i].addr() == meta_addr(
279                            frame_to_index_spec((range.start + i * PAGE_SIZE) as usize),
280                        )
281                    }
282                &&& forall|paddr: Paddr|
283                    #![trigger frame_to_index_spec(paddr)]
284                    (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
285                        ==> !new_regions.slots.contains_key(frame_to_index_spec(paddr))
286            }
287        }
288    }
289
290    /// The wrapper for the precondition for [`Self::split`]:
291    ///
292    /// - the segment must satisfy the invariant with the owner ([`Self::inv_with`])
293    /// - the offset must be aligned and within bounds.
294    pub open spec fn split_requires(self, owner: SegmentOwner<M>, offset: usize) -> bool {
295        &&& self.inv_with(&owner)
296        &&& offset % PAGE_SIZE == 0
297        &&& 0 < offset < self.size()
298    }
299
300    /// The wrapper for the postcondition for [`Self::split`]:
301    ///
302    /// - the resulting segments must satisfy the invariant with the corresponding owners;
303    /// - the resulting segments must be the same as the result of [`Self::split_spec`];
304    /// - the permissions in the original owner must be split into the resulting owners.
305    pub open spec fn split_ensures(
306        self,
307        offset: usize,
308        lhs: Self,
309        rhs: Self,
310        ori_owner: SegmentOwner<M>,
311        lhs_owner: SegmentOwner<M>,
312        rhs_owner: SegmentOwner<M>,
313    ) -> bool {
314        &&& lhs.inv_with(&lhs_owner)
315        &&& rhs.inv_with(&rhs_owner)
316        &&& (lhs, rhs) == self.split_spec(offset)
317        &&& ori_owner.perms =~= (lhs_owner.perms + rhs_owner.perms)
318    }
319
320    /// The wrapper for the precondition for [`Self::into_raw`]:
321    ///
322    /// - the segment must satisfy the invariant with the owner;
323    /// - the meta region in `regions` must satisfy the invariant.
324    pub open spec fn into_raw_requires(
325        self,
326        regions: MetaRegionOwners,
327        owner: SegmentOwner<M>,
328    ) -> bool {
329        &&& self.inv_with(&owner)
330        &&& regions.inv()
331        &&& owner.inv()
332    }
333
334    /// The wrapper for the postcondition for [`Self::into_raw`]:
335    ///
336    /// - the returned physical address range must be the same as the segment's range;
337    /// - the meta region is unchanged.
338    pub open spec fn into_raw_ensures(
339        self,
340        old_regions: MetaRegionOwners,
341        regions: MetaRegionOwners,
342        r: Range<Paddr>,
343    ) -> bool {
344        &&& r == self.range
345        &&& regions.inv()
346        &&& regions =~= old_regions
347    }
348
349    /// The wrapper for the precondition for [`Self::from_raw`]:
350    ///
351    /// - the range must be a forgotten [`Segment`] that matches the type `M`;
352    /// - the caller must provide the owner with valid permissions;
353    /// - the range must be aligned and within bounds.
354    pub open spec fn from_raw_requires(
355        regions: MetaRegionOwners,
356        range: Range<Paddr>,
357        owner: SegmentOwner<M>,
358    ) -> bool {
359        &&& regions.inv()
360        &&& range.start % PAGE_SIZE == 0
361        &&& range.end % PAGE_SIZE == 0
362        &&& range.start < range.end < MAX_PADDR
363    }
364
365    /// The wrapper for the postcondition for [`Self::from_raw`]:
366    ///
367    /// - the returned segment must have the same physical address range as the input;
368    /// - the meta region is unchanged.
369    pub open spec fn from_raw_ensures(
370        self,
371        old_regions: MetaRegionOwners,
372        new_regions: MetaRegionOwners,
373        owner: SegmentOwner<M>,
374        range: Range<Paddr>,
375    ) -> bool {
376        &&& self.range == range
377        &&& new_regions.inv()
378        &&& new_regions =~= old_regions
379    }
380
381    /// The wrapper for the precondition for slicing a segment with a given range:
382    ///
383    /// - the segment must satisfy the invariant with the owner ([`Self::inv_with`])
384    /// - the slicing range must be aligned and within bounds of the segment.
385    pub open spec fn slice_requires(self, owner: SegmentOwner<M>, range: Range<Paddr>) -> bool {
386        &&& self.inv_with(&owner)
387        &&& range.start % PAGE_SIZE == 0
388        &&& range.end % PAGE_SIZE == 0
389        &&& self.range.start + range.start <= self.range.start + range.end <= self.range.end
390    }
391
392    /// The wrapper for the postcondition for slicing a segment with a given range:
393    ///
394    /// - the resulting slice must satisfy the invariant with the owner;
395    /// - the resulting slice must have the same physical address range as the slicing range.
396    ///
397    /// See also [`vstd::seq::Seq::subrange`].
398    pub open spec fn slice_ensures(
399        self,
400        owner: SegmentOwner<M>,
401        range: Range<Paddr>,
402        res: Self,
403    ) -> bool {
404        &&& res.inv_with(
405            &SegmentOwner {
406                perms: owner.perms.subrange(
407                    (range.start / PAGE_SIZE) as int,
408                    (range.end / PAGE_SIZE) as int,
409                ),
410            },
411        )
412    }
413
414    /// Checks if the current segment can be iterated to get the next frame:
415    ///
416    /// - the segment and meta regions must satisfy their respective invariants;
417    /// - the frame's slot must not be in `regions.slots` (the owner holds the permission);
418    /// - the frame's raw_count must be 1 (it was forgotten once).
419    pub open spec fn next_requires(
420        self,
421        regions: MetaRegionOwners,
422        owner: SegmentOwner<M>,
423    ) -> bool {
424        &&& self.inv()
425        &&& regions.inv()
426        &&& owner.perms.len() > 0
427        &&& !regions.slots.contains_key(frame_to_index(self.range.start))
428        &&& regions.slot_owners.contains_key(frame_to_index(self.range.start))
429        &&& regions.slot_owners[frame_to_index(self.range.start)].raw_count == 1
430        &&& regions.slot_owners[frame_to_index(self.range.start)].self_addr == frame_to_meta(
431            self.range.start,
432        )
433        &&& owner.perms[0].points_to.is_init()
434        &&& owner.perms[0].points_to.addr() == frame_to_meta(self.range.start)
435        &&& owner.perms[0].points_to.value().wf(
436            regions.slot_owners[frame_to_index(self.range.start)],
437        )
438    }
439
440    /// The wrapper for the postcondition for iterating to the next frame:
441    ///
442    /// - if the result is [`None`], then the segment has been exhausted;
443    /// - if the result is [`Some`], then the segment is advanced by one frame and
444    ///   the returned frame is the next frame, with its slot restored to `regions`.
445    pub open spec fn next_ensures(
446        old_self: Self,
447        new_self: Self,
448        old_regions: MetaRegionOwners,
449        new_regions: MetaRegionOwners,
450        res: Option<Frame<M>>,
451    ) -> bool {
452        &&& new_regions.inv()
453        &&& new_self.inv()
454        &&& match res {
455            None => { &&& new_self.range.start == old_self.range.end },
456            Some(f) => {
457                &&& new_self.range.start == old_self.range.start + PAGE_SIZE
458                &&& f.paddr() == old_self.range.start
459                &&& new_regions.slots.contains_key(frame_to_index(f.paddr()))
460                &&& new_regions.slot_owners[frame_to_index(f.paddr())].raw_count == 0
461            },
462        }
463    }
464
465    /// Creates a new [`Segment`] from unused frames.
466    ///
467    /// The caller must provide a closure to initialize metadata for all the frames.
468    /// The closure receives the physical address of the frame and returns the
469    /// metadata, which is similar to [`core::array::from_fn`].
470    ///
471    /// It returns an error if:
472    ///  - any of the frames cannot be created with a specific reason.
473    ///
474    /// # Verified Properties
475    /// ## Preconditions
476    /// See [`Self::from_unused_requires`].
477    /// ## Postconditions
478    /// See [`Self::from_unused_ensures`].
479    #[verus_spec(r =>
480        with
481            Tracked(regions): Tracked<&mut MetaRegionOwners>,
482                -> owner: Tracked<Option<SegmentOwner<M>>>,
483        requires
484            Self::from_unused_requires(*old(regions), range, metadata_fn),
485        ensures
486            Self::from_unused_ensures(*old(regions), *regions, owner@, range, metadata_fn, r),
487    )]
488    pub fn from_unused(range: Range<Paddr>, metadata_fn: impl Fn(Paddr) -> (Paddr, M)) -> (res:
489        Result<Self, GetFrameError>) {
490        proof_decl! {
491            let tracked mut owner: Option<SegmentOwner<M>> = None;
492            let tracked mut addrs = Seq::<usize>::tracked_empty();
493            let tracked mut perms = Seq::<MetaPerm<M>>::tracked_empty();
494        }
495        // Construct a segment early to recycle previously forgotten frames if
496        // the subsequent operations fails in the middle.
497        let mut segment = Self {
498            range: range.start..range.start,
499            _marker: core::marker::PhantomData,
500        };
501
502        let mut i = 0;
503        let addr_len = (range.end - range.start) / PAGE_SIZE;
504
505        #[verus_spec(
506            invariant
507                i <= addr_len,
508                i as int == addrs.len(),
509                i as int == perms.len(),
510                range.start % PAGE_SIZE == 0,
511                range.end % PAGE_SIZE == 0,
512                range.start <= range.start + i * PAGE_SIZE <= range.end,
513                range.end == range.start + addr_len * PAGE_SIZE,
514                addr_len == (range.end - range.start) / PAGE_SIZE as int,
515                i <= addr_len,
516                forall|paddr_in: Paddr|
517                    (range.start + i * PAGE_SIZE <= paddr_in < range.end && paddr_in % PAGE_SIZE == 0) ==> {
518                        &&& metadata_fn.requires((paddr_in,))
519                    },
520                forall|paddr_in: Paddr, paddr_out: Paddr, m: M|
521                    range.start + i * PAGE_SIZE <= paddr_in < range.end
522                        && paddr_in % PAGE_SIZE == 0
523                        && metadata_fn.ensures((paddr_in,), (paddr_out, m)) ==> {
524                        &&& paddr_out < MAX_PADDR
525                        &&& paddr_out % PAGE_SIZE == 0
526                        &&& paddr_in == paddr_out
527                        &&& regions.slots.contains_key(frame_to_index(paddr_out))
528                        &&& regions.slot_owners[frame_to_index(paddr_out)].usage is Unused
529                        &&& regions.slot_owners[frame_to_index(paddr_out)].inner_perms.in_list.points_to(0)
530                    },
531                forall|j: int|
532                    0 <= j < addrs.len() as int ==> {
533                        &&& !regions.slots.contains_key(frame_to_index_spec(addrs[j]))
534                        &&& addrs[j] % PAGE_SIZE == 0
535                        &&& addrs[j] < MAX_PADDR
536                        &&& addrs[j] == range.start + (j as u64) * PAGE_SIZE
537                    },
538                forall|j: int|
539                    #![trigger perms[j]]
540                    0 <= j < perms.len() as int ==> {
541                        &&& perms[j].addr() == frame_to_meta(addrs[j])
542                        &&& perms[j].wf(&perms[j].inner_perms)
543                        &&& perms[j].is_init()
544                    },
545                regions.inv(),
546                segment.range.start == range.start,
547                segment.range.end == range.start + i * PAGE_SIZE,
548            decreases addr_len - i,
549        )]
550        while i < addr_len {
551            let paddr_in = range.start + i * PAGE_SIZE;
552            let (paddr, meta) = metadata_fn(paddr_in);
553
554            let (frame, Tracked(frame_perm)) = match #[verus_spec(with Tracked(regions))]
555            MetaSlot::get_from_unused(paddr, meta, false) {
556                Ok(res) => {
557                    let (ptr, Tracked(frame_perm)) = res;
558                    (Frame { ptr, _marker: core::marker::PhantomData::<M> }, Tracked(frame_perm))
559                },
560                Err(e) => {
561                    return {
562                        proof_with!(|= Tracked(owner));
563                        Err(e)
564                    };
565                },
566            };
567
568            proof {
569                assert(metadata_fn.ensures((paddr_in,), (paddr, meta)));
570                assert(frame_perm.addr() == frame_to_meta(paddr));
571                assert(frame_perm.wf(&frame_perm.inner_perms));
572                assert(frame_perm.is_init());
573                assert(frame.constructor_requires(*regions)) by {};
574                perms.tracked_push(frame_perm);
575            }
576
577            let _ = ManuallyDrop::new(frame, Tracked(regions));
578            segment.range.end = paddr + PAGE_SIZE;
579            proof {
580                addrs.tracked_push(paddr);
581            }
582
583            i += 1;
584        }
585
586        proof {
587            broadcast use vstd_extra::seq_extra::lemma_seq_to_set_map_contains;
588
589            owner = Some(SegmentOwner { perms });
590
591            assert forall|addr: usize|
592                #![trigger frame_to_index_spec(addr)]
593                range.start <= addr < range.end && addr % PAGE_SIZE == 0 implies {
594                &&& !regions.slots.contains_key(frame_to_index_spec(addr))
595            } by {
596                // proof by contradiction
597                assert(addrs.contains(addr)) by {
598                    if !addrs.contains(addr) {
599                        let j = (addr - range.start) / PAGE_SIZE as int;
600                        assert(0 <= j < addrs.len() as usize) by {
601                            assert(addr >= range.start);
602                            assert(addr < range.end);
603                            assert(addr % PAGE_SIZE == 0);
604                        };
605                        assert(addrs[j as int] == addr);
606                    }
607                }
608            }
609        }
610
611        proof_with!(|= Tracked(owner));
612        Ok(segment)
613    }
614
615    /// Splits the frames into two at the given byte offset from the start.
616    ///
617    /// The resulting frames cannot be empty. So the offset cannot be neither
618    /// zero nor the length of the frames.
619    ///
620    /// # Verified Properties
621    /// ## Preconditions
622    /// See [`Self::split_requires`].
623    ///
624    /// ## Postconditions
625    /// See [`Self::split_ensures`].
626    #[verus_spec(r =>
627        with
628            Tracked(owner): Tracked<SegmentOwner<M>>,
629            Tracked(regions): Tracked<&mut MetaRegionOwners>,
630                -> frame_perms: (Tracked<SegmentOwner<M>>, Tracked<SegmentOwner<M>>),
631        requires
632            Self::split_requires(self, owner, offset),
633        ensures
634            Self::split_ensures(self, offset, r.0, r.1, owner, frame_perms.0@, frame_perms.1@),
635    )]
636    pub fn split(self, offset: usize) -> (Self, Self) {
637        let at = self.range.start + offset;
638        let idx = offset / PAGE_SIZE;
639        let res = (
640            Self { range: self.range.start..at, _marker: core::marker::PhantomData },
641            Self { range: at..self.range.end, _marker: core::marker::PhantomData },
642        );
643
644        let _ = ManuallyDrop::new(self, Tracked(regions));
645
646        let tracked frame_perms1 = SegmentOwner {
647            perms: seq_tracked_subrange(owner.perms, 0, idx as int),
648        };
649        let tracked frame_perms2 = SegmentOwner {
650            perms: seq_tracked_subrange(owner.perms, idx as int, owner.perms.len() as int),
651        };
652
653        proof {
654            owner.perms.lemma_split_at(idx as int);
655        }
656
657        proof_with!(|= (Tracked(frame_perms1), Tracked(frame_perms2)));
658        res
659    }
660
661    /// Forgets the [`Segment`] and gets a raw range of physical addresses.
662    ///
663    /// The segment's permissions are returned to the caller via `frame_perms`.
664    /// The caller is responsible for holding onto the permissions and providing
665    /// them back when restoring the segment with [`Self::from_raw`].
666    #[verus_spec(r =>
667        with
668            Tracked(regions): Tracked<&mut MetaRegionOwners>,
669            Tracked(owner): Tracked<SegmentOwner<M>>,
670                -> frame_perms: Tracked<SegmentOwner<M>>,
671        requires
672            Self::into_raw_requires(self, *old(regions), owner),
673        ensures
674            Self::into_raw_ensures(self, *old(regions), *regions, r),
675            frame_perms@ == owner,
676    )]
677    pub(crate) fn into_raw(self) -> Range<Paddr> {
678        let range = self.range.clone();
679        let _ = ManuallyDrop::new(self, Tracked(regions));
680
681        proof_with!(|= Tracked(owner));
682        range
683    }
684
685    /// Restores the [`Segment`] from the raw physical address range.
686    ///
687    /// # Verified Properties
688    /// ## Preconditions
689    /// See [`Self::from_raw_requires`].
690    ///
691    /// ## Postconditions
692    /// See [`Self::from_raw_ensures`].
693    ///
694    /// # Safety
695    ///
696    /// The range must be a forgotten [`Segment`] that matches the type `M`.
697    /// The caller must provide the permissions that were returned by [`Self::into_raw`].
698    #[verus_spec(r =>
699        with
700            Tracked(regions): Tracked<&mut MetaRegionOwners>,
701            Tracked(owner): Tracked<SegmentOwner<M>>,
702        requires
703            Self::from_raw_requires(*old(regions), range, owner),
704        ensures
705            Self::from_raw_ensures(r, *old(regions), *regions, owner, range),
706    )]
707    pub(crate) unsafe fn from_raw(range: Range<Paddr>) -> Self {
708        Self { range, _marker: core::marker::PhantomData }
709    }
710
711    /// Gets an extra handle to the frames in the byte offset range.
712    ///
713    /// The sliced byte offset range in indexed by the offset from the start of
714    /// the contiguous frames. The resulting frames holds extra reference counts.
715    ///
716    /// # Verified Properties
717    ///
718    /// # Verified Properties
719    ///
720    /// ## Preconditions
721    /// See [`Self::slice_requires`].
722    ///
723    /// ## Postconditions
724    /// See [`Self::slice_ensures`].
725    #[verus_spec(r =>
726        with
727            Tracked(owner): Tracked<&SegmentOwner<M>>,
728        requires
729            Self::slice_requires(*self, *owner, *range),
730        ensures
731            Self::slice_ensures(*self, *owner, *range, r),
732    )]
733    pub fn slice(&self, range: &Range<Paddr>) -> Self {
734        let start = self.range.start + range.start;
735        let end = self.range.start + range.end;
736
737        let mut i = 0;
738        let addr_len = (end - start) / PAGE_SIZE;
739        while i < addr_len
740            invariant
741                start % PAGE_SIZE == 0,
742                end % PAGE_SIZE == 0,
743                start + i * PAGE_SIZE <= end,
744                i <= addr_len,
745                addr_len == (end - start) / PAGE_SIZE as int,
746            decreases addr_len - i,
747        {
748            let paddr = start + i * PAGE_SIZE;
749            // SAFETY: We already have reference counts for the frames since
750            // for each frame there would be a forgotten handle when creating
751            // the `Segment` object.
752            // unsafe { inc_frame_ref_count(paddr); }
753            i += 1;
754        }
755
756        Self { range: start..end, _marker: core::marker::PhantomData }
757    }
758
759    /// Gets the next frame in the segment (raw), if any.
760    ///
761    /// Since the segments here must be "non-active" where
762    /// there is no extra Verus-tracked permission [`SegmentOwner`]
763    /// associated with it; [`Segment`] becomes a kind of "zombie"
764    /// container through which we can only iterate the frames and
765    /// get the frame out of the `regions` instead.
766    ///
767    /// # Note
768    ///
769    /// We chose to make `next` the member function of [`Segment`] rather than a trait method
770    /// because the current Verus standard library has limited support for [`core::iter::Iterator`]
771    /// and associated types, and we want to avoid the complexity of defining a custom iterator trait
772    /// and implementing it for `Segment`.
773    ///
774    /// # Verified Properties
775    /// ## Preconditions
776    /// See [`Self::next_requires`].
777    ///
778    /// ## Postconditions
779    /// See [`Self::next_ensures`].
780    #[verus_spec(res =>
781        with
782            Tracked(regions): Tracked<&mut MetaRegionOwners>,
783            Tracked(owner): Tracked<&mut SegmentOwner<M>>
784        requires
785            Self::next_requires(*old(self), *old(regions), *old(owner)),
786        ensures
787            Self::next_ensures(*old(self), *self, *old(regions), *regions, res),
788    )]
789    pub fn next(&mut self) -> Option<Frame<M>> {
790        if self.range.start < self.range.end {
791            let tracked perm = owner.perms.tracked_remove(0);
792
793            proof_decl! {
794                let tracked from_raw_debt: crate::specs::mm::frame::frame_specs::BorrowDebt;
795            }
796
797            let frame = unsafe {
798                #[verus_spec(with Tracked(regions), Tracked(&perm) => Tracked(from_raw_debt))]
799                Frame::<M>::from_raw(self.range.start)
800            };
801
802            proof {
803                // raw_count was 1 (segment was forgotten via into_raw), so discharge trivially.
804                from_raw_debt.discharge_bookkeeping();
805            }
806
807            self.range.start = self.range.start + PAGE_SIZE;
808            Some(frame)
809        } else {
810            None
811        }
812    }
813}
814
815} // verus!
ostd/mm/frame/segment.rs

ostd/mm/frame/
segment.rs
