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        }
494        // Construct a segment early to recycle previously forgotten frames if
495        // the subsequent operations fails in the middle.
496        let mut segment = Self {
497            range: range.start..range.start,
498            _marker: core::marker::PhantomData,
499        };
500
501        let mut i = 0;
502        let addr_len = (range.end - range.start) / PAGE_SIZE;
503
504        #[verus_spec(
505            invariant
506                i <= addr_len,
507                i as int == addrs.len(),
508                range.start % PAGE_SIZE == 0,
509                range.end % PAGE_SIZE == 0,
510                range.start <= range.start + i * PAGE_SIZE <= range.end,
511                range.end == range.start + addr_len * PAGE_SIZE,
512                addr_len == (range.end - range.start) / PAGE_SIZE as int,
513                i <= addr_len,
514                forall|paddr_in: Paddr|
515                    (range.start <= paddr_in < range.end && paddr_in % PAGE_SIZE == 0) ==> {
516                        &&& metadata_fn.requires((paddr_in,))
517                    },
518                forall|paddr_in: Paddr, paddr_out: Paddr, m: M|
519                    metadata_fn.ensures((paddr_in,), (paddr_out, m)) ==> {
520                        &&& paddr_out < MAX_PADDR
521                        &&& paddr_out % PAGE_SIZE == 0
522                        &&& paddr_in == paddr_out
523                        &&& regions.slots.contains_key(frame_to_index(paddr_out))
524                        &&& regions.slot_owners[frame_to_index(paddr_out)].usage is Unused
525                        &&& regions.slot_owners[frame_to_index(paddr_out)].inner_perms.in_list.points_to(0)
526                    },
527                forall|j: int|
528                    0 <= j < addrs.len() as int ==> {
529                        &&& regions.slots.contains_key(frame_to_index_spec(addrs[j]))
530                        &&& addrs[j] % PAGE_SIZE == 0
531                        &&& addrs[j] == range.start + (j as u64) * PAGE_SIZE
532                    },
533                forall|paddr: Paddr| #[trigger]
534                    old(regions).slots.contains_key(frame_to_index(paddr))
535                        ==> regions.slots.contains_key(frame_to_index(paddr)),
536                regions.inv(),
537                segment.range.start == range.start,
538                segment.range.end == range.start + i * PAGE_SIZE,
539            decreases addr_len - i,
540        )]
541        while i < addr_len {
542            let paddr = range.start + i * PAGE_SIZE;
543            let (paddr, meta) = metadata_fn(paddr);
544
545            proof_decl! {
546                let tracked mut perm : Option<PointsTo<MetaSlot, Metadata<M>>>;
547            }
548
549            let frame = match #[verus_spec(with Tracked(regions) => perm)]
550            Frame::<M>::from_unused(paddr, meta) {
551                Ok(f) => f,
552                Err(e) => {
553                    return {
554                        proof_with!(|= Tracked(owner));
555                        Err(e)
556                    };
557                },
558            };
559
560            proof {
561                assert(forall|paddr_in: Paddr, paddr_out: Paddr, m: M|
562                    metadata_fn.ensures((paddr_in,), (paddr_out, m)) ==> {
563                        &&& regions.slot_owners[frame_to_index(paddr_out)].usage is Unused
564                        &&& regions.slot_owners[frame_to_index(
565                            paddr_out,
566                        )].inner_perms.in_list.points_to(0)
567                    }) by {
568                    admit();
569                }
570                assert(frame.constructor_requires(*old(regions))) by { admit() };
571            }
572
573            let _ = ManuallyDrop::new(frame, Tracked(regions));
574            segment.range.end = paddr + PAGE_SIZE;
575            proof {
576                addrs.tracked_push(paddr);
577                admit();
578            }
579
580            i += 1;
581        }
582
583        proof {
584            broadcast use vstd_extra::map_extra::lemma_map_remove_keys_finite;
585            broadcast use vstd_extra::seq_extra::lemma_seq_to_set_map_contains;
586            broadcast use vstd::map::group_map_axioms;
587            broadcast use vstd::map_lib::group_map_extra;
588
589            let tracked owner_seq = seq_tracked_map_values(
590                addrs,
591                |addr: usize|
592                    {
593                        let perm = regions.slots[frame_to_index(addr)];
594                        MetaPerm {
595                            addr: meta_addr(frame_to_index(addr)),
596                            points_to: perm,
597                            inner_perms: regions.slot_owners[frame_to_index(addr)].inner_perms,
598                            _T: core::marker::PhantomData,
599                        }
600                    },
601            );
602            owner = Some(SegmentOwner { perms: owner_seq });
603
604            let index = addrs.map_values(|addr: Paddr| frame_to_index(addr)).to_set();
605            regions.slots.tracked_remove_keys(index);
606
607            assert forall|addr: usize|
608                #![trigger frame_to_index_spec(addr)]
609                range.start <= addr < range.end && addr % PAGE_SIZE == 0 implies {
610                &&& !regions.slots.contains_key(frame_to_index_spec(addr))
611            } by {
612                // proof by contradiction
613                assert(addrs.contains(addr)) by {
614                    if !addrs.contains(addr) {
615                        let j = (addr - range.start) / PAGE_SIZE as int;
616                        assert(0 <= j < addrs.len() as usize) by {
617                            assert(addr >= range.start);
618                            assert(addr < range.end);
619                            assert(addr % PAGE_SIZE == 0);
620                        };
621                        assert(addrs[j as int] == addr);
622                    }
623                }
624            }
625        }
626
627        proof_with!(|= Tracked(owner));
628        Ok(segment)
629    }
630
631    /// Splits the frames into two at the given byte offset from the start.
632    ///
633    /// The resulting frames cannot be empty. So the offset cannot be neither
634    /// zero nor the length of the frames.
635    ///
636    /// # Verified Properties
637    /// ## Preconditions
638    /// See [`Self::split_requires`].
639    ///
640    /// ## Postconditions
641    /// See [`Self::split_ensures`].
642    #[verus_spec(r =>
643        with
644            Tracked(owner): Tracked<SegmentOwner<M>>,
645            Tracked(regions): Tracked<&mut MetaRegionOwners>,
646                -> frame_perms: (Tracked<SegmentOwner<M>>, Tracked<SegmentOwner<M>>),
647        requires
648            Self::split_requires(self, owner, offset),
649        ensures
650            Self::split_ensures(self, offset, r.0, r.1, owner, frame_perms.0@, frame_perms.1@),
651    )]
652    pub fn split(self, offset: usize) -> (Self, Self) {
653        let at = self.range.start + offset;
654        let idx = offset / PAGE_SIZE;
655        let res = (
656            Self { range: self.range.start..at, _marker: core::marker::PhantomData },
657            Self { range: at..self.range.end, _marker: core::marker::PhantomData },
658        );
659
660        let _ = ManuallyDrop::new(self, Tracked(regions));
661
662        let tracked frame_perms1 = SegmentOwner {
663            perms: seq_tracked_subrange(owner.perms, 0, idx as int),
664        };
665        let tracked frame_perms2 = SegmentOwner {
666            perms: seq_tracked_subrange(owner.perms, idx as int, owner.perms.len() as int),
667        };
668
669        proof {
670            owner.perms.lemma_split_at(idx as int);
671        }
672
673        proof_with!(|= (Tracked(frame_perms1), Tracked(frame_perms2)));
674        res
675    }
676
677    /// Forgets the [`Segment`] and gets a raw range of physical addresses.
678    ///
679    /// The segment's permissions are returned to the caller via `frame_perms`.
680    /// The caller is responsible for holding onto the permissions and providing
681    /// them back when restoring the segment with [`Self::from_raw`].
682    #[verus_spec(r =>
683        with
684            Tracked(regions): Tracked<&mut MetaRegionOwners>,
685            Tracked(owner): Tracked<SegmentOwner<M>>,
686                -> frame_perms: Tracked<SegmentOwner<M>>,
687        requires
688            Self::into_raw_requires(self, *old(regions), owner),
689        ensures
690            Self::into_raw_ensures(self, *old(regions), *regions, r),
691            frame_perms@ == owner,
692    )]
693    pub(crate) fn into_raw(self) -> Range<Paddr> {
694        let range = self.range.clone();
695        let _ = ManuallyDrop::new(self, Tracked(regions));
696
697        proof_with!(|= Tracked(owner));
698        range
699    }
700
701    /// Restores the [`Segment`] from the raw physical address range.
702    ///
703    /// # Verified Properties
704    /// ## Preconditions
705    /// See [`Self::from_raw_requires`].
706    ///
707    /// ## Postconditions
708    /// See [`Self::from_raw_ensures`].
709    ///
710    /// # Safety
711    ///
712    /// The range must be a forgotten [`Segment`] that matches the type `M`.
713    /// The caller must provide the permissions that were returned by [`Self::into_raw`].
714    #[verus_spec(r =>
715        with
716            Tracked(regions): Tracked<&mut MetaRegionOwners>,
717            Tracked(owner): Tracked<SegmentOwner<M>>,
718        requires
719            Self::from_raw_requires(*old(regions), range, owner),
720        ensures
721            Self::from_raw_ensures(r, *old(regions), *regions, owner, range),
722    )]
723    pub(crate) unsafe fn from_raw(range: Range<Paddr>) -> Self {
724        Self { range, _marker: core::marker::PhantomData }
725    }
726
727    /// Gets an extra handle to the frames in the byte offset range.
728    ///
729    /// The sliced byte offset range in indexed by the offset from the start of
730    /// the contiguous frames. The resulting frames holds extra reference counts.
731    ///
732    /// # Verified Properties
733    ///
734    /// # Verified Properties
735    ///
736    /// ## Preconditions
737    /// See [`Self::slice_requires`].
738    ///
739    /// ## Postconditions
740    /// See [`Self::slice_ensures`].
741    #[verus_spec(r =>
742        with
743            Tracked(owner): Tracked<&SegmentOwner<M>>,
744        requires
745            Self::slice_requires(*self, *owner, *range),
746        ensures
747            Self::slice_ensures(*self, *owner, *range, r),
748    )]
749    pub fn slice(&self, range: &Range<Paddr>) -> Self {
750        let start = self.range.start + range.start;
751        let end = self.range.start + range.end;
752
753        let mut i = 0;
754        let addr_len = (end - start) / PAGE_SIZE;
755        while i < addr_len
756            invariant
757                start % PAGE_SIZE == 0,
758                end % PAGE_SIZE == 0,
759                start + i * PAGE_SIZE <= end,
760                i <= addr_len,
761                addr_len == (end - start) / PAGE_SIZE as int,
762            decreases addr_len - i,
763        {
764            let paddr = start + i * PAGE_SIZE;
765            // SAFETY: We already have reference counts for the frames since
766            // for each frame there would be a forgotten handle when creating
767            // the `Segment` object.
768            // unsafe { inc_frame_ref_count(paddr); }
769            i += 1;
770        }
771
772        Self { range: start..end, _marker: core::marker::PhantomData }
773    }
774
775    /// Gets the next frame in the segment (raw), if any.
776    ///
777    /// Since the segments here must be "non-active" where
778    /// there is no extra Verus-tracked permission [`SegmentOwner`]
779    /// associated with it; [`Segment`] becomes a kind of "zombie"
780    /// container through which we can only iterate the frames and
781    /// get the frame out of the `regions` instead.
782    ///
783    /// # Note
784    ///
785    /// We chose to make `next` the member function of [`Segment`] rather than a trait method
786    /// because the current Verus standard library has limited support for [`core::iter::Iterator`]
787    /// and associated types, and we want to avoid the complexity of defining a custom iterator trait
788    /// and implementing it for `Segment`.
789    ///
790    /// # Verified Properties
791    /// ## Preconditions
792    /// See [`Self::next_requires`].
793    ///
794    /// ## Postconditions
795    /// See [`Self::next_ensures`].
796    #[verus_spec(res =>
797        with
798            Tracked(regions): Tracked<&mut MetaRegionOwners>,
799            Tracked(owner): Tracked<&mut SegmentOwner<M>>
800        requires
801            Self::next_requires(*old(self), *old(regions), *old(owner)),
802        ensures
803            Self::next_ensures(*old(self), *self, *old(regions), *regions, res),
804    )]
805    pub fn next(&mut self) -> Option<Frame<M>> {
806        if self.range.start < self.range.end {
807            let tracked perm = owner.perms.tracked_remove(0);
808            let frame = unsafe {
809                #[verus_spec(with Tracked(regions), Tracked(&perm))]
810                Frame::<M>::from_raw(self.range.start)
811            };
812
813            self.range.start = self.range.start + PAGE_SIZE;
814            Some(frame)
815        } else {
816            None
817        }
818    }
819}
820
821} // verus!
ostd/mm/frame/segment.rs

ostd/mm/frame/
segment.rs
