Skip to main content

Segment

ostd::mm::frame::segment

Struct Segment 

Source 
#[repr(transparent)]
pub struct Segment<M: AnyFrameMeta + ?Sized> {
    pub range: Range<Paddr>,
    pub _marker: PhantomData<M>,
}
Expand description

A contiguous range of homogeneous physical memory frames.

This is a handle to multiple contiguous frames. It will be more lightweight than owning an array of frame handles.

The ownership is achieved by the reference counting mechanism of frames. When constructing a Segment, the frame handles are created then forgotten, leaving the reference count. When dropping a it, the frame handles are restored and dropped, decrementing the reference count.

All the metadata of the frames are homogeneous, i.e., they are of the same type.

Fields§

§range: Range<Paddr>

The physical address range of the segment.

§_marker: PhantomData<M>

Implementations§

Source§

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Segment<M>

Source

pub exec fn from_unused( range: Range<Paddr>, metadata_fn: impl Fn(Paddr) -> (Paddr, M), ) -> res : Result<Self, GetFrameError>

with
Tracked(regions): Tracked<&mut MetaRegionOwners>,
requires
old(regions).inv(),
forall |paddr_in: Paddr| {
    (range.start <= paddr_in < range.end && paddr_in % PAGE_SIZE == 0)
        ==> {
            &&& metadata_fn.requires((paddr_in,))

        }
},
forall |paddr_in: Paddr, paddr_out: Paddr, m: M| {
    metadata_fn.ensures((paddr_in,), (paddr_out, m)) ==> paddr_in == paddr_out
},
!(range.end <= MAX_PADDR ==> range.start < range.end) ==> may_panic(),
ensures
final(regions).inv(),
r is Err ==> final(regions).frame_obligations == old(regions).frame_obligations,
(range.start % PAGE_SIZE != 0 || range.end % PAGE_SIZE != 0)
    ==> r == Err::<Self, _>(GetFrameError::NotAligned),
(range.start % PAGE_SIZE == 0 && range.end % PAGE_SIZE == 0 && range.end > MAX_PADDR)
    ==> r == Err::<Self, _>(GetFrameError::OutOfBound),
r matches Ok(
    seg,
) ==> {
    &&& seg.start_paddr() == range.start
    &&& seg.end_paddr() == range.end
    &&& seg.start_paddr() < seg.end_paddr()
    &&& seg.invariants(*final(regions))
    &&& crate::specs::mm::frame::segment::seg_obligations_minted(
        *old(regions),
        *final(regions),
        range.start,
        crate::specs::mm::frame::segment::seg_nframes(range),
    )
    &&& forall |paddr: Paddr| {
        (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
            ==> final(regions).slots.contains_key(frame_to_index(paddr))
    }
    &&& range.start < range.end <= MAX_PADDR

},

Creates a new Segment from unused frames.

The caller must provide a closure to initialize metadata for all the frames. The closure receives the physical address of the frame and returns the metadata, which is similar to core::array::from_fn.

It returns an error if:

  • the physical address is invalid or not aligned;
  • any of the frames cannot be created with a specific reason.
§Panics

It panics if the range is empty.

§Verified Properties
§Preconditions
  • the metadata function must be well-formed and valid for all frames in the range;
  • the metadata function must ensure that the frames can be created and owned by the segment;
  • for any frame created via the closure metadata_fn, the corresponding slot in regions must be unused and not dropped in the owner (MetaRegionOwners).

Range constraints (alignment, range.end <= MAX_PADDR, non-emptiness) are runtime-checked in the body — see the postconditions below for the corresponding error variants.

§Postconditions
  • if the result is Ok, the returned segment satisfies its invariant, relates to the updated metadata region, and has the same physical address range as the input;
  • if the input range is misaligned, the result is Err(NotAligned);
  • if the input range exceeds MAX_PADDR, the result is Err(OutOfBound);
  • if the input is aligned and within MAX_PADDR and the function terminated, then range.start < range.end (the runtime assert! would otherwise diverge).
Source§

impl<M: AnyFrameMeta + ?Sized> Segment<M>

Source

pub exec fn start_paddr(&self) -> Paddr

returns
self.start_paddr(),

Gets the start physical address of the contiguous frames.

Source

pub fn __VERUS_SPEC_start_paddr(&self) -> Paddr

Source

pub exec fn end_paddr(&self) -> Paddr

returns
self.end_paddr(),

Gets the end physical address of the contiguous frames.

Source

pub fn __VERUS_SPEC_end_paddr(&self) -> Paddr

Source

pub exec fn size(&self) -> r : usize

requires
self.inv(),
ensures
r == self.end_paddr() - self.start_paddr(),
returns
self.size(),

Gets the length in bytes of the contiguous frames.

Source

pub fn __VERUS_SPEC_size(&self) -> usize

Source

pub open spec fn range(&self) -> Range<Paddr>

{ self.start_paddr()..self.end_paddr() }
Source§

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Segment<M>

Source

pub exec fn split(self, offset: usize) -> r : (Self, Self)

with
Tracked(regions): Tracked<&mut MetaRegionOwners>,
requires
self.invariants(*old(regions)),
offset % PAGE_SIZE != 0 ==> may_panic(),
!(0 < offset && offset < self.size()) ==> may_panic(),
ensures
final(regions).slots == old(regions).slots,
final(regions).slot_owners == old(regions).slot_owners,
final(regions).frame_obligations == old(regions).frame_obligations,
(r.0, r.1) == self.split_spec(offset),
r.0.invariants(*final(regions)),
r.1.invariants(*final(regions)),

Splits the frames into two at the given byte offset from the start.

The resulting frames cannot be empty. So the offset cannot be neither zero nor the length of the frames.

§Verified Properties
§Preconditions
  • the segment must satisfy its bundled invariant against the metadata region;
  • the offset must be aligned and within bounds;
§Postconditions
  • the resulting segments satisfy their bundled invariants;
  • they match Self::split_spec;
  • both halves continue to relate correctly to regions (which is unchanged).
Source

pub open spec fn page_in_range_saturated( self, range: &Range<usize>, regions: MetaRegionOwners, ) -> bool

{
    exists |j: int| {
        (range.start as int) / (PAGE_SIZE as int) <= j
            < (range.end as int) / (PAGE_SIZE as int)
            && regions
                .slot_owners[frame_to_index(
                    (self.start_paddr() + j * PAGE_SIZE) as usize,
                )]
                .inner_perms
                .ref_count
                .value() >= REF_COUNT_MAX
    }
}

Precise panic condition for Self::slice. slice diverges iff:

  • the slice range is misaligned, reversed, or out of the segment’s bounds (the diverging assert!s at the top of slice), or
  • the specific per-frame slot that slice bumps is already saturated (inc_ref_count would overflow). Unlike query which clones one item, slice bumps one refcount per page in the slice range, so the saturation disjunct is an exists over those specific paddrs self.range.start + j * PAGE_SIZE for j ∈ [range.start/PAGE_SIZE, range.end/PAGE_SIZE).
Source

pub exec fn slice(&self, range: &Range<usize>) -> r : Self

with
Tracked(regions): Tracked<&mut MetaRegionOwners>,
requires
self.invariants(*old(regions)),
range.start % PAGE_SIZE != 0 ==> may_panic(),
range.end % PAGE_SIZE != 0 ==> may_panic(),
range.start > range.end ==> may_panic(),
range.end > self.size() ==> may_panic(),
self.page_in_range_saturated(range, *old(regions)) ==> may_panic(),
ensures
range.start % PAGE_SIZE == 0,
range.end % PAGE_SIZE == 0,
range.start <= range.end,
self.range.start + range.end <= self.range.end,
!self.page_in_range_saturated(range, *old(regions)),
r.inv(),
r.start_paddr() == self.start_paddr() + range.start,
r.end_paddr() == self.start_paddr() + range.end,
r.end_paddr() <= self.end_paddr(),
final(regions).inv(),
final(regions).slots == old(regions).slots,
final(regions).slot_owners.dom() == old(regions).slot_owners.dom(),
final(regions).frame_obligations == old(regions).frame_obligations,

Gets an extra handle to the frames in the byte offset range.

The sliced byte offset range in indexed by the offset from the start of the contiguous frames. The resulting frames holds extra reference counts.

§Verified Properties
§Postconditions
  • the resulting slice’s range matches the slicing range and is in-bounds (the in-bounds check follows from the diverging assert! in the body);
  • regions preserves invariants and key domains. Per-frame state for a hypothetical sub-segment relation is not exposed; threading that through the per-frame ref-count bump loop would require a much heavier proof. Mirrors Segment::clone.

See also [vstd::seq::Seq::subrange].

Source

pub open spec fn nrpage_spec(&self) -> usize

recommends
self.inv(),
{ self.size() / PAGE_SIZE }

Returns the number of pages of the contiguous frames.

Source

pub closed spec fn split_spec(self, offset: usize) -> (Self, Self)

recommends
self.inv(),
offset % PAGE_SIZE == 0,
0 < offset < self.size(),

Splits the contiguous frames into two at the given byte offset from the start in spec mode.

Source§

impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> Segment<M>

Source

pub exec fn drop(self)

with
Tracked(regions): Tracked<&mut MetaRegionOwners>,
requires
self.invariants(*old(regions)),
forall |i: int| {
    0 <= i < crate::specs::mm::frame::segment::seg_nframes(self.range)
        ==> {
            let idx = frame_to_index((self.range.start + i * PAGE_SIZE) as usize);
            old(regions).slot_owners[idx].inner_perms.ref_count.value() == 1
                ==> {
                    &&& old(regions).slot_owners[idx].inner_perms.storage.is_init()
                    &&& old(regions).slot_owners[idx].inner_perms.in_list.value() == 0

                }
        }
},
ensures
final(regions).inv(),

Verified drop: iterates over each frame in the segment, decrements its reference count, and (when last ref) tears down the metadata.

Per-frame linear-drop: before the teardown loop, this redeems the one frame_obligations entry the segment retained per frame (minted by Segment::from_unused). Failing to drop the segment leaves those per-frame counts outstanding and breaks MetaRegionOwners::clean_inv at the enclosing function’s exit.

Source§

impl<M: AnyUFrameMeta + OwnerOf> Segment<M>

Source

pub exec fn reader(&self) -> r : VmReader<'_, Infallible>

with
->
owner: Tracked<VmIoOwner>,
requires
self.inv(),
ensures
r.inv(),
owner@.inv(),
r.wf(owner@),
r.cursor.vaddr == paddr_to_vaddr_spec(self.start_paddr()),
r.remain_spec() == self.size(),
owner@.is_kernel,
Source

pub exec fn writer(&self) -> r : VmWriter<'_, Infallible>

with
->
owner: Tracked<VmIoOwner>,
requires
self.inv(),
ensures
r.inv(),
owner@.inv(),
r.wf(owner@),
r.cursor.vaddr == paddr_to_vaddr_spec(self.start_paddr()),
r.avail_spec() == self.size(),
owner@.is_kernel,
!owner@.is_fallible,
Source§

impl<M: AnyFrameMeta + ?Sized> Segment<M>

Source

pub open spec fn relate_regions(&self, regions: MetaRegionOwners) -> bool

{
    &&& forall |i: int| {
        0 <= i < seg_nframes(self.range)
            ==> {
                let idx = frame_to_index((self.range.start + i * PAGE_SIZE) as usize);
                &&& regions.frame_obligations.count(idx) >= 1
                &&& regions.slot_owners.contains_key(idx)
                &&& regions.slots.contains_key(idx)
                &&& regions.slot_owners[idx].slot_vaddr == index_to_meta(idx)
                &&& regions.slot_owners[idx].inner_perms.ref_count.value() > 0
                &&& regions.slot_owners[idx].inner_perms.ref_count.value()
                    <= crate::mm::frame::meta::REF_COUNT_MAX
                &&& regions.slot_owners[idx].paths_in_pt.is_empty()
                &&& regions.slot_owners[idx].usage is Frame

            }
    }
    &&& forall |i: int, j: int| {
        0 <= i < j < seg_nframes(self.range)
            ==> frame_to_index((self.range.start + i * PAGE_SIZE) as usize)
                != frame_to_index((self.range.start + j * PAGE_SIZE) as usize)
    }

}

The cross-object relation between a Segment and the global MetaRegionOwners.

For every frame i in the segment, this asserts:

  • the slot owner and canonical slot permission are present in regions,
  • the slot’s slot_vaddr is consistent with its index,
  • the slot has a live, non-UNUSED reference count,
  • the slot has a pending frame_obligations entry for this segment,
  • the slot is a data-frame slot with no page-table paths,
  • distinct frames in the segment map to distinct slot indices.

This is an invariant preserved by operations that transform a Segment together with MetaRegionOwners. The segment’s own range is the only identity source; there is no separate segment owner token.

Source

pub proof fn relate_regions_at(&self, regions: MetaRegionOwners, i: int)

requires
self.relate_regions(regions),
0 <= i < seg_nframes(self.range),
ensures
({
    let idx = frame_to_index((self.range.start + i * PAGE_SIZE) as usize);
    &&& regions.frame_obligations.count(idx) >= 1
    &&& regions.slot_owners.contains_key(idx)
    &&& regions.slots.contains_key(idx)
    &&& regions.slot_owners[idx].slot_vaddr == index_to_meta(idx)
    &&& regions.slot_owners[idx].inner_perms.ref_count.value() > 0
    &&& regions.slot_owners[idx].inner_perms.ref_count.value()
        <= crate::mm::frame::meta::REF_COUNT_MAX
    &&& regions.slot_owners[idx].paths_in_pt.is_empty()
    &&& regions.slot_owners[idx].usage is Frame

}),

Manually instantiates the [relate_regions] forall at a specific index. Use this to extract per-frame facts without fighting trigger inference.

Source

pub proof fn relate_regions_distinct(&self, regions: MetaRegionOwners, i: int, j: int)

requires
self.relate_regions(regions),
0 <= i < j < seg_nframes(self.range),
ensures
frame_to_index((self.range.start + i * PAGE_SIZE) as usize)
    != frame_to_index((self.range.start + j * PAGE_SIZE) as usize),

Manually instantiates the [relate_regions] distinctness forall at a specific index pair: distinct in-range frames map to distinct slot indices. Reusable lever for from_unused/split/slice proofs.

Source

pub open spec fn invariants(&self, regions: MetaRegionOwners) -> bool

{
    &&& self.inv()
    &&& regions.inv()
    &&& self.relate_regions(regions)

}

The bundled invariant for Segment operations that thread the global regions: the segment’s own invariant, the region invariant, and the cross-object relation tying this segment’s range to regions.

Mirrors the invariants bundles used throughout the page-table / cursor code — it collapses the clauses repeated across split, slice, into_raw, next, and drop into one predicate.

Source

pub open spec fn kernel_mem_view_covers(&self, view: &MemView) -> bool

{
    &&& self.inv()
    &&& view.mappings_are_disjoint()
    &&& forall |vaddr: Vaddr| {
        paddr_to_vaddr(self.start_paddr()) <= vaddr
            < paddr_to_vaddr(self.start_paddr()) + self.end_paddr() - self.start_paddr()
            ==> {
                &&& view.addr_transl(vaddr) is Some
                &&& view.memory.contains_key((view.addr_transl(vaddr)->0).0)
                &&& view.memory[(view.addr_transl(vaddr)->0).0].inv()
                &&& view
                    .memory[(view.addr_transl(vaddr)->0).0]
                    .contents[(view.addr_transl(vaddr)->0).1 as int] is Init

            }
    }
    &&& forall |paddr: Paddr| {
        self.start_paddr() <= paddr < self.end_paddr()
            ==> {
                let vaddr = paddr_to_vaddr(paddr);
                &&& view.addr_transl(vaddr) is Some
                &&& (view.addr_transl(vaddr)->0).0 <= paddr
                &&& paddr
                    < (view.addr_transl(vaddr)->0).0
                        + view.memory[(view.addr_transl(vaddr)->0).0].size@
                &&& (view.addr_transl(vaddr)->0).1
                    == paddr - (view.addr_transl(vaddr)->0).0
                &&& view.memory.contains_key((view.addr_transl(vaddr)->0).0)
                &&& view.memory[(view.addr_transl(vaddr)->0).0].inv()
                &&& view
                    .memory[(view.addr_transl(vaddr)->0).0]
                    .contents[(view.addr_transl(vaddr)->0).1 as int] is Init

            }
    }

}

Whether a MemView covers the segment through the kernel direct mapping.

This predicate only describes the virtual-to-physical relation and the presence of initialized backing frame contents.

Trait Implementations§

Source§

impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> From<Frame<M>> for Segment<M>

Source§

exec fn from(frame: Frame<M>) -> Self

Converts a single Frame into a one-page Segment by forgetting the frame and recording its paddr range. Symmetric to vostd’s From<Frame<M>> for Segment<M>.

Source§

impl<M: AnyFrameMeta + ?Sized> Inv for Segment<M>

Source§

open spec fn inv(self) -> bool

{
    &&& self.start_paddr() % PAGE_SIZE == 0
    &&& self.end_paddr() % PAGE_SIZE == 0
    &&& self.start_paddr() <= self.end_paddr() <= MAX_PADDR

}

The invariant of a Segment:

  • the physical addresses of the frames are aligned and within bounds.
  • the range is well-formed, i.e., the start is less than or equal to the end.
Source§

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Iterator for Segment<M>

Source§

exec fn next(&mut self) -> Option<Self::Item>

Gets the next frame in the segment.

Source§

type Item = Frame<M>

The type of the elements being iterated over.
Source§

fn next_chunk<const N: usize>( &mut self, ) -> Result<[Self::Item; N], IntoIter<Self::Item, N>>
where Self: Sized,

🔬This is a nightly-only experimental API. (iter_next_chunk)
Advances the iterator and returns an array containing the next N values. Read more
1.0.0 · Source§

fn size_hint(&self) -> (usize, Option<usize>)

Returns the bounds on the remaining length of the iterator. Read more
1.0.0 · Source§

fn count(self) -> usize
where Self: Sized,

Consumes the iterator, counting the number of iterations and returning it. Read more
1.0.0 · Source§

fn last(self) -> Option<Self::Item>
where Self: Sized,

Consumes the iterator, returning the last element. Read more
Source§

fn advance_by(&mut self, n: usize) -> Result<(), NonZero<usize>>

🔬This is a nightly-only experimental API. (iter_advance_by)
Advances the iterator by n elements. Read more
1.0.0 · Source§

fn nth(&mut self, n: usize) -> Option<Self::Item>

Returns the nth element of the iterator. Read more
1.28.0 · Source§

fn step_by(self, step: usize) -> StepBy<Self>
where Self: Sized,

Creates an iterator starting at the same point, but stepping by the given amount at each iteration. Read more
1.0.0 · Source§

fn chain<U>(self, other: U) -> Chain<Self, <U as IntoIterator>::IntoIter>
where Self: Sized, U: IntoIterator<Item = Self::Item>,

Takes two iterators and creates a new iterator over both in sequence. Read more
1.0.0 · Source§

fn zip<U>(self, other: U) -> Zip<Self, <U as IntoIterator>::IntoIter>
where Self: Sized, U: IntoIterator,

‘Zips up’ two iterators into a single iterator of pairs. Read more
Source§

fn intersperse_with<G>(self, separator: G) -> IntersperseWith<Self, G>
where Self: Sized, G: FnMut() -> Self::Item,

🔬This is a nightly-only experimental API. (iter_intersperse)
Creates a new iterator which places an item generated by separator between items of the original iterator. Read more
1.0.0 · Source§

fn map<B, F>(self, f: F) -> Map<Self, F>
where Self: Sized, F: FnMut(Self::Item) -> B,

Takes a closure and creates an iterator which calls that closure on each element. Read more
1.21.0 · Source§

fn for_each<F>(self, f: F)
where Self: Sized, F: FnMut(Self::Item),

Calls a closure on each element of an iterator. Read more
1.0.0 · Source§

fn filter<P>(self, predicate: P) -> Filter<Self, P>
where Self: Sized, P: FnMut(&Self::Item) -> bool,

Creates an iterator which uses a closure to determine if an element should be yielded. Read more
1.0.0 · Source§

fn filter_map<B, F>(self, f: F) -> FilterMap<Self, F>
where Self: Sized, F: FnMut(Self::Item) -> Option<B>,

Creates an iterator that both filters and maps. Read more
1.0.0 · Source§

fn enumerate(self) -> Enumerate<Self>
where Self: Sized,

Creates an iterator which gives the current iteration count as well as the next value. Read more
1.0.0 · Source§

fn peekable(self) -> Peekable<Self>
where Self: Sized,

Creates an iterator which can use the peek and peek_mut methods to look at the next element of the iterator without consuming it. See their documentation for more information. Read more
1.0.0 · Source§

fn skip_while<P>(self, predicate: P) -> SkipWhile<Self, P>
where Self: Sized, P: FnMut(&Self::Item) -> bool,

Creates an iterator that skips elements based on a predicate. Read more
1.0.0 · Source§

fn take_while<P>(self, predicate: P) -> TakeWhile<Self, P>
where Self: Sized, P: FnMut(&Self::Item) -> bool,

Creates an iterator that yields elements based on a predicate. Read more
1.57.0 · Source§

fn map_while<B, P>(self, predicate: P) -> MapWhile<Self, P>
where Self: Sized, P: FnMut(Self::Item) -> Option<B>,

Creates an iterator that both yields elements based on a predicate and maps. Read more
1.0.0 · Source§

fn skip(self, n: usize) -> Skip<Self>
where Self: Sized,

Creates an iterator that skips the first n elements. Read more
1.0.0 · Source§

fn take(self, n: usize) -> Take<Self>
where Self: Sized,

Creates an iterator that yields the first n elements, or fewer if the underlying iterator ends sooner. Read more
1.0.0 · Source§

fn scan<St, B, F>(self, initial_state: St, f: F) -> Scan<Self, St, F>
where Self: Sized, F: FnMut(&mut St, Self::Item) -> Option<B>,

An iterator adapter which, like fold, holds internal state, but unlike fold, produces a new iterator. Read more
1.0.0 · Source§

fn flat_map<U, F>(self, f: F) -> FlatMap<Self, U, F>
where Self: Sized, U: IntoIterator, F: FnMut(Self::Item) -> U,

Creates an iterator that works like map, but flattens nested structure. Read more
Source§

fn map_windows<F, R, const N: usize>(self, f: F) -> MapWindows<Self, F, N>
where Self: Sized, F: FnMut(&[Self::Item; N]) -> R,

🔬This is a nightly-only experimental API. (iter_map_windows)
Calls the given function f for each contiguous window of size N over self and returns an iterator over the outputs of f. Like slice::windows(), the windows during mapping overlap as well. Read more
1.0.0 · Source§

fn fuse(self) -> Fuse<Self>
where Self: Sized,

Creates an iterator which ends after the first None. Read more
1.0.0 · Source§

fn inspect<F>(self, f: F) -> Inspect<Self, F>
where Self: Sized, F: FnMut(&Self::Item),

Does something with each element of an iterator, passing the value on. Read more
1.0.0 · Source§

fn by_ref(&mut self) -> &mut Self
where Self: Sized,

Creates a “by reference” adapter for this instance of Iterator. Read more
1.0.0 · Source§

fn collect<B>(self) -> B
where B: FromIterator<Self::Item>, Self: Sized,

Transforms an iterator into a collection. Read more
Source§

fn collect_into<E>(self, collection: &mut E) -> &mut E
where E: Extend<Self::Item>, Self: Sized,

🔬This is a nightly-only experimental API. (iter_collect_into)
Collects all the items from an iterator into a collection. Read more
1.0.0 · Source§

fn partition<B, F>(self, f: F) -> (B, B)
where Self: Sized, B: Default + Extend<Self::Item>, F: FnMut(&Self::Item) -> bool,

Consumes an iterator, creating two collections from it. Read more
Source§

fn is_partitioned<P>(self, predicate: P) -> bool
where Self: Sized, P: FnMut(Self::Item) -> bool,

🔬This is a nightly-only experimental API. (iter_is_partitioned)
Checks if the elements of this iterator are partitioned according to the given predicate, such that all those that return true precede all those that return false. Read more
1.27.0 · Source§

fn try_fold<B, F, R>(&mut self, init: B, f: F) -> R
where Self: Sized, F: FnMut(B, Self::Item) -> R, R: Try<Output = B>,

An iterator method that applies a function as long as it returns successfully, producing a single, final value. Read more
1.27.0 · Source§

fn try_for_each<F, R>(&mut self, f: F) -> R
where Self: Sized, F: FnMut(Self::Item) -> R, R: Try<Output = ()>,

An iterator method that applies a fallible function to each item in the iterator, stopping at the first error and returning that error. Read more
1.0.0 · Source§

fn fold<B, F>(self, init: B, f: F) -> B
where Self: Sized, F: FnMut(B, Self::Item) -> B,

Folds every element into an accumulator by applying an operation, returning the final result. Read more
1.51.0 · Source§

fn reduce<F>(self, f: F) -> Option<Self::Item>
where Self: Sized, F: FnMut(Self::Item, Self::Item) -> Self::Item,

Reduces the elements to a single one, by repeatedly applying a reducing operation. Read more
Source§

fn try_reduce<R>( &mut self, f: impl FnMut(Self::Item, Self::Item) -> R, ) -> <<R as Try>::Residual as Residual<Option<<R as Try>::Output>>>::TryType
where Self: Sized, R: Try<Output = Self::Item>, <R as Try>::Residual: Residual<Option<Self::Item>>,

🔬This is a nightly-only experimental API. (iterator_try_reduce)
Reduces the elements to a single one by repeatedly applying a reducing operation. If the closure returns a failure, the failure is propagated back to the caller immediately. Read more
1.0.0 · Source§

fn all<F>(&mut self, f: F) -> bool
where Self: Sized, F: FnMut(Self::Item) -> bool,

Tests if every element of the iterator matches a predicate. Read more
1.0.0 · Source§

fn any<F>(&mut self, f: F) -> bool
where Self: Sized, F: FnMut(Self::Item) -> bool,

Tests if any element of the iterator matches a predicate. Read more
1.0.0 · Source§

fn find<P>(&mut self, predicate: P) -> Option<Self::Item>
where Self: Sized, P: FnMut(&Self::Item) -> bool,

Searches for an element of an iterator that satisfies a predicate. Read more
1.30.0 · Source§

fn find_map<B, F>(&mut self, f: F) -> Option<B>
where Self: Sized, F: FnMut(Self::Item) -> Option<B>,

Applies function to the elements of iterator and returns the first non-none result. Read more
Source§

fn try_find<R>( &mut self, f: impl FnMut(&Self::Item) -> R, ) -> <<R as Try>::Residual as Residual<Option<Self::Item>>>::TryType
where Self: Sized, R: Try<Output = bool>, <R as Try>::Residual: Residual<Option<Self::Item>>,

🔬This is a nightly-only experimental API. (try_find)
Applies function to the elements of iterator and returns the first true result or the first error. Read more
1.0.0 · Source§

fn position<P>(&mut self, predicate: P) -> Option<usize>
where Self: Sized, P: FnMut(Self::Item) -> bool,

Searches for an element in an iterator, returning its index. Read more
1.6.0 · Source§

fn max_by_key<B, F>(self, f: F) -> Option<Self::Item>
where B: Ord, Self: Sized, F: FnMut(&Self::Item) -> B,

Returns the element that gives the maximum value from the specified function. Read more
1.15.0 · Source§

fn max_by<F>(self, compare: F) -> Option<Self::Item>
where Self: Sized, F: FnMut(&Self::Item, &Self::Item) -> Ordering,

Returns the element that gives the maximum value with respect to the specified comparison function. Read more
1.6.0 · Source§

fn min_by_key<B, F>(self, f: F) -> Option<Self::Item>
where B: Ord, Self: Sized, F: FnMut(&Self::Item) -> B,

Returns the element that gives the minimum value from the specified function. Read more
1.15.0 · Source§

fn min_by<F>(self, compare: F) -> Option<Self::Item>
where Self: Sized, F: FnMut(&Self::Item, &Self::Item) -> Ordering,

Returns the element that gives the minimum value with respect to the specified comparison function. Read more
1.0.0 · Source§

fn unzip<A, B, FromA, FromB>(self) -> (FromA, FromB)
where FromA: Default + Extend<A>, FromB: Default + Extend<B>, Self: Sized + Iterator<Item = (A, B)>,

Converts an iterator of pairs into a pair of containers. Read more
1.36.0 · Source§

fn copied<'a, T>(self) -> Copied<Self>
where T: Copy + 'a, Self: Sized + Iterator<Item = &'a T>,

Creates an iterator which copies all of its elements. Read more
1.0.0 · Source§

fn cloned<'a, T>(self) -> Cloned<Self>
where T: Clone + 'a, Self: Sized + Iterator<Item = &'a T>,

Creates an iterator which clones all of its elements. Read more
Source§

fn array_chunks<const N: usize>(self) -> ArrayChunks<Self, N>
where Self: Sized,

🔬This is a nightly-only experimental API. (iter_array_chunks)
Returns an iterator over N elements of the iterator at a time. Read more
1.11.0 · Source§

fn sum<S>(self) -> S
where Self: Sized, S: Sum<Self::Item>,

Sums the elements of an iterator. Read more
1.11.0 · Source§

fn product<P>(self) -> P
where Self: Sized, P: Product<Self::Item>,

Iterates over the entire iterator, multiplying all the elements Read more
Source§

fn cmp_by<I, F>(self, other: I, cmp: F) -> Ordering
where Self: Sized, I: IntoIterator, F: FnMut(Self::Item, <I as IntoIterator>::Item) -> Ordering,

🔬This is a nightly-only experimental API. (iter_order_by)
Lexicographically compares the elements of this Iterator with those of another with respect to the specified comparison function. Read more
1.5.0 · Source§

fn partial_cmp<I>(self, other: I) -> Option<Ordering>
where I: IntoIterator, Self::Item: PartialOrd<<I as IntoIterator>::Item>, Self: Sized,

Lexicographically compares the PartialOrd elements of this Iterator with those of another. The comparison works like short-circuit evaluation, returning a result without comparing the remaining elements. As soon as an order can be determined, the evaluation stops and a result is returned. Read more
Source§

fn partial_cmp_by<I, F>(self, other: I, partial_cmp: F) -> Option<Ordering>
where Self: Sized, I: IntoIterator, F: FnMut(Self::Item, <I as IntoIterator>::Item) -> Option<Ordering>,

🔬This is a nightly-only experimental API. (iter_order_by)
Lexicographically compares the elements of this Iterator with those of another with respect to the specified comparison function. Read more
1.5.0 · Source§

fn eq<I>(self, other: I) -> bool
where I: IntoIterator, Self::Item: PartialEq<<I as IntoIterator>::Item>, Self: Sized,

Determines if the elements of this Iterator are equal to those of another. Read more
Source§

fn eq_by<I, F>(self, other: I, eq: F) -> bool
where Self: Sized, I: IntoIterator, F: FnMut(Self::Item, <I as IntoIterator>::Item) -> bool,

🔬This is a nightly-only experimental API. (iter_order_by)
Determines if the elements of this Iterator are equal to those of another with respect to the specified equality function. Read more
1.5.0 · Source§

fn ne<I>(self, other: I) -> bool
where I: IntoIterator, Self::Item: PartialEq<<I as IntoIterator>::Item>, Self: Sized,

Determines if the elements of this Iterator are not equal to those of another. Read more
1.5.0 · Source§

fn lt<I>(self, other: I) -> bool
where I: IntoIterator, Self::Item: PartialOrd<<I as IntoIterator>::Item>, Self: Sized,

Determines if the elements of this Iterator are lexicographically less than those of another. Read more
1.5.0 · Source§

fn le<I>(self, other: I) -> bool
where I: IntoIterator, Self::Item: PartialOrd<<I as IntoIterator>::Item>, Self: Sized,

Determines if the elements of this Iterator are lexicographically less or equal to those of another. Read more
1.5.0 · Source§

fn gt<I>(self, other: I) -> bool
where I: IntoIterator, Self::Item: PartialOrd<<I as IntoIterator>::Item>, Self: Sized,

Determines if the elements of this Iterator are lexicographically greater than those of another. Read more
1.5.0 · Source§

fn ge<I>(self, other: I) -> bool
where I: IntoIterator, Self::Item: PartialOrd<<I as IntoIterator>::Item>, Self: Sized,

Determines if the elements of this Iterator are lexicographically greater than or equal to those of another. Read more
1.82.0 · Source§

fn is_sorted_by<F>(self, compare: F) -> bool
where Self: Sized, F: FnMut(&Self::Item, &Self::Item) -> bool,

Checks if the elements of this iterator are sorted using the given comparator function. Read more
1.82.0 · Source§

fn is_sorted_by_key<F, K>(self, f: F) -> bool
where Self: Sized, F: FnMut(Self::Item) -> K, K: PartialOrd,

Checks if the elements of this iterator are sorted using the given key extraction function. Read more
Source§

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> RCClone for Segment<M>

Source§

open spec fn clone_requires(self, perm: MetaRegionOwners) -> bool

{
    &&& self.inv()
    &&& perm.inv()
    &&& forall |pa: Paddr| {
        (self.start_paddr() <= pa < self.end_paddr() && pa % PAGE_SIZE == 0)
            ==> {
                let idx = frame_to_index(pa);
                &&& perm.slots.contains_key(idx)
                &&& valid_frame_paddr(pa)
                &&& perm.slot_owners[idx].inner_perms.ref_count.value() > 0
                &&& perm.slot_owners[idx].inner_perms.ref_count.value() + 1
                    < super::meta::REF_COUNT_MAX
                &&& !MetaSlot::inc_ref_count_panic_cond(
                    perm.slot_owners[idx].inner_perms.ref_count,
                )

            }
    }

}
Source§

open spec fn clone_ensures( self, old_perm: MetaRegionOwners, new_perm: MetaRegionOwners, res: Self, ) -> bool

{
    &&& res.range() == self.range()
    &&& res.inv()
    &&& new_perm.inv()
    &&& new_perm.frame_obligations =~= old_perm.frame_obligations

}
Source§

exec fn clone(&self, Tracked(perm): Tracked<&mut MetaRegionOwners>) -> res : Self

Source§

impl<M: AnyFrameMeta + ?Sized> TrackDrop for Segment<M>

Source§

type State = MetaRegionOwners

The tracked state for ManuallyDrop purposes is the global MetaRegionOwners. The real per-segment obligation is represented by one entry per frame in MetaRegionOwners::frame_obligations, not by this TrackDrop impl. That keeps ManuallyDrop::new(self) callable in places like Segment::split / Segment::into_raw where the segment is “temporarily forgotten” without an actual ledger event.

Source§

type Obligation = DropObligation<Range<usize>>

Real segment-range key. The token produced by constructor_spec carries self.range as identity. The mint here does NOT insert into obligations — the real per-segment entry is added by Segment::from_unused and removed by Segment::drop directly. Carrying Range<Paddr> on the token still strengthens the discipline: a token forged for one segment can’t masquerade as belonging to another (the consume_requires/drop_requires checks would refuse the mismatched key).

Source§

open spec fn tracked_redeem_requires(self, s: Self::State) -> bool

{ true }
Source§

open spec fn tracked_redeem_ensures( self, s0: Self::State, s1: Self::State, obl: Self::Obligation, ) -> bool

{
    &&& s0 =~= s1
    &&& obl.value() == self.range

}
Source§

proof fn tracked_redeem(self, tracked s: &mut Self::State) -> tracked obl : Self::Obligation

Source§

open spec fn drop_requires(self, s: Self::State, obl: Self::Obligation) -> bool

{
    &&& s.inv()
    &&& obl.value() == self.range

}
Source§

open spec fn drop_ensures( self, s0: Self::State, s1: Self::State, obl: Self::Obligation, ) -> bool

{ true }

Auto Trait Implementations§

§

impl<M> Freeze for Segment<M>
where M: ?Sized,

§

impl<M> RefUnwindSafe for Segment<M>
where M: RefUnwindSafe + ?Sized,

§

impl<M> Send for Segment<M>
where M: ?Sized,

§

impl<M> Sync for Segment<M>
where M: ?Sized,

§

impl<M> Unpin for Segment<M>
where M: Unpin + ?Sized,

§

impl<M> UnsafeUnpin for Segment<M>
where M: ?Sized,

§

impl<M> UnwindSafe for Segment<M>
where M: UnwindSafe + ?Sized,

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

§

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

§

fn obeys_from_spec() -> bool

§

fn from_spec(v: T) -> VERUS_SPEC__A

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

Source§

impl<I> IntoIterator for I
where I: Iterator,

Source§

type Item = <I as Iterator>::Item

The type of the elements being iterated over.
Source§

type IntoIter = I

Which kind of iterator are we turning this into?
Source§

fn into_iter(self) -> I

Creates an iterator from a value. Read more
§

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> T

§

impl<T, U> IntoSpecImpl<U> for T
where U: From<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> U

§

impl<VERUS_SPEC__A> IteratorSpec for VERUS_SPEC__A
where VERUS_SPEC__A: Iterator + ?Sized,

§

fn obeys_prophetic_iter_laws(&self) -> bool

This iterator obeys the specifications below on next, expressed in terms of prophetic spec functions. Only iterators that terminate (i.e., eventually return None and then continue to return None) should use this interface.
§

fn remaining(&self) -> Seq<<VERUS_SPEC__A as Iterator>::Item>

Sequence of items that will (eventually) be returned
§

fn will_return_none(&self) -> bool

Does this iterator complete with a None after the above sequence? (As opposed to hanging indefinitely on a next() call) Trivially true for most iterators but important for iterators that apply an exec closure that may not terminate.
§

fn decrease(&self) -> Option<nat>

Value used by default for the decreases clause when no explicit decreases clause is provided (the user can override this with an explicit decreases clause). If there’s no appropriate metric to decrease, this can return None, and the user will have to provide an explicit decreases clause.
§

fn initial_value_relation(&self, init: &VERUS_SPEC__A) -> bool

Invariant relating the iterator to the initial expression that created it (e.g., my_vec.iter()). This allows for more ergonomic/intuitive invariants. When the analysis can infer a spec initial value (by discovering a when_used_as_spec annotation), the analysis places the value in init.
§

fn peek(&self, index: int) -> Option<<VERUS_SPEC__A as Iterator>::Item>

Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

§

fn obeys_try_from_spec() -> bool

§

fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

§

impl<T, U> TryIntoSpecImpl<U> for T
where U: TryFrom<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>

§

impl<A> SpecEq<&A> for A
where A: ?Sized,

§

impl<A> SpecEq<&mut A> for A
where A: ?Sized,

§

impl<A> SpecEq<A> for A
where A: ?Sized,

§

impl<A> SpecEq<Ghost<A>> for A

§

impl<A> SpecEq<Tracked<A>> for A