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>

Marker for the metadata type.

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>,
->
owner: Tracked<Option<SegmentOwner<M>>>,
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 is Ok ==> (range.end <= MAX_PADDR ==> range.start < range.end),
r matches Ok(
    seg,
) ==> {
    &&& seg.start_paddr() == range.start
    &&& seg.end_paddr() == range.end
    &&& seg.start_paddr() < seg.end_paddr()
    &&& crate::specs::mm::frame::segment::seg_obligations_minted(
        *old(regions),
        *final(regions),
        range.start,
        crate::specs::mm::frame::segment::seg_nframes(range),
    )
    &&& owner@ matches Some(
        owner,
    ) && {
        &&& seg.inv()
        &&& seg.wf(&owner)

    }
    &&& forall |paddr: Paddr| {
        (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
            ==> final(regions).slots.contains_key(frame_to_index(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:

  • any of the frames cannot be created with a specific reason.
§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 with the owner, has the same physical address range as the input, and the owner is Some;
  • 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(owner): Tracked<SegmentOwner<M>>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,
->
result_owners: (Tracked<SegmentOwner<M>>, Tracked<SegmentOwner<M>>),
requires
self.invariants(&owner, *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(&result_owners.0@, *final(regions)),
r.1.invariants(&result_owners.1@, *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 invariant (Self::inv) and the well-formedness relation with the owner (Self::wf);
  • the offset must be aligned and within bounds;
  • the meta region must be valid and the owner must relate to it.
§Postconditions
  • the resulting segments satisfy their invariants with the corresponding owners;
  • they match Self::split_spec;
  • the original owner’s permissions are split between the two new owners;
  • 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(owner): Tracked<&SegmentOwner<M>>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,
requires
self.invariants(owner, *old(regions)),
range.start % PAGE_SIZE != 0 ==> may_panic(),
range.end % PAGE_SIZE != 0 ==> may_panic(),
range.start > range.end ==> may_panic(),
self.range.start as int + range.end as int > self.range.end as int ==> 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 as int + range.end as int <= self.range.end as int,
!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 — e.g. that a hypothetical sub_owner.relate_regions(regions) would hold — 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 exec fn next(&mut self) -> res : Option<(Frame<M>, Tracked<DropObligation<usize>>)>

with
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(owner): Tracked<&mut SegmentOwner<M>>,
requires
old(self).invariants(old(owner), *old(regions)),
ensures
final(regions).inv(),
final(self).inv(),
final(owner).relate_regions(*final(regions)),
match res {
    None => final(self).start_paddr() == old(self).end_paddr(),
    Some(pair) => (
        &&& final(self).start_paddr() == old(self).start_paddr() + PAGE_SIZE
        &&& pair.0.paddr() == old(self).start_paddr()
        &&& final(regions).slots.contains_key(frame_to_index(pair.0.paddr()))
        &&& pair.1@.value() == frame_to_index(pair.0.paddr())
        &&& pair.0.inv_with_regions(*final(regions))
        &&& final(regions).frame_obligations.count(frame_to_index(pair.0.paddr())) >= 1

    ),
},

Gets the next frame in the segment.

This is the verified counterpart of Iterator::next for Segment<M>. The trait method is external_body because Verus’s core::iter::Iterator support can’t thread Tracked metadata through the trait method’s fixed signature.

§Verified Properties
§Preconditions
  • segment, owner, and meta regions must satisfy their respective invariants;
  • the segment is well-formed with the owner;
  • the owner relates correctly to regions (forgotten reference, slot present and consistent, etc. — see SegmentOwner::relate_regions).

All the per-frame coherence conditions previously listed inline are now consequences of owner.relate_regions(regions) instantiated at i = 0.

§Postconditions
  • if the result is None, then the segment has been exhausted;
  • if the result is Some, then the segment is advanced by one frame and the returned frame is the next frame, with its slot restored to regions;
  • the new owner continues to relate correctly to the new regions.
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(owner): Tracked<SegmentOwner<M>>,
Tracked(regions): Tracked<&mut MetaRegionOwners>,
requires
self.invariants(&owner, *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 wf(&self, owner: &SegmentOwner<M>) -> bool

{
    &&& self.range == owner.range

}

The well-formedness relation between a Segment and its owner:

  • the segment’s range matches the range tracked by the owner;
  • the number of permissions in the owner matches the number of frames in the segment;
  • the physical address of each permission matches the corresponding frame in the segment.

This is only the cross-object relation; callers are expected to also state self.inv() (and where relevant owner.inv()) alongside. With owner.inv() the perm-address and length conjuncts are consequences of self.range == owner.range, but they are kept here for trigger availability at sites that don’t invoke owner.inv().

Interested readers are encouraged to see frame_to_index and meta_addr for how we convert between physical addresses and meta region indices.

Source

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

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

}

The bundled invariant for Segment operations that thread an owner and the global regions: the segment’s own invariant, its well-formedness against the owner, the owner’s invariant, the region invariant, and the cross-object relation tying the owner to regions.

Mirrors the invariants bundles used throughout the page-table / cursor code — it collapses the five clauses repeated verbatim 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.finite()
    &&& 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).unwrap().0)
                &&& view.memory[view.addr_transl(vaddr).unwrap().0].inv()
                &&& view
                    .memory[view.addr_transl(vaddr).unwrap().0]
                    .contents[view.addr_transl(vaddr).unwrap().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).unwrap().0 <= paddr
                &&& paddr
                    < view.addr_transl(vaddr).unwrap().0
                        + view.memory[view.addr_transl(vaddr).unwrap().0].size@
                &&& view.addr_transl(vaddr).unwrap().1
                    == paddr - view.addr_transl(vaddr).unwrap().0
                &&& view.memory.contains_key(view.addr_transl(vaddr).unwrap().0)
                &&& view.memory[view.addr_transl(vaddr).unwrap().0].inv()
                &&& view
                    .memory[view.addr_transl(vaddr).unwrap().0]
                    .contents[view.addr_transl(vaddr).unwrap().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 adjacent 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)
                &&& has_safe_slot(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 SegmentOwner<M> is threaded in separately via verus_spec, and the real per-segment obligation (with the segment-range ledger entry) is held on SegmentOwner itself — not via this TrackDrop impl. That keeps ManuallyDrop::new(self, Tracked(regions)) callable in places like Segment::split / Segment::into_raw where the segment is “temporarily forgotten” without an actual ledger event.

Source§

type Key = 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 key(self) -> Self::Key

{ self.range }
Source§

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

{ true }
Source§

open spec fn constructor_ensures( self, s0: Self::State, s1: Self::State, obl_key: Self::Key, ) -> bool

{
    &&& s0 =~= s1
    &&& obl_key == self.range

}
Source§

proof fn constructor_spec(self, tracked s: &mut Self::State) -> tracked obl : DropObligation<Self::Key>

Source§

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

{ s.inv() }
Source§

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

{ true }
Source§

open spec fn consume_requires(self, s: Self::State, obl_key: Self::Key) -> bool

{ true }
Source§

open spec fn consume_ensures( self, s0: Self::State, s1: Self::State, obl_key: Self::Key, ) -> bool

{ s0 =~= s1 }
Source§

proof fn consume_obligation(self, tracked s: &mut Self::State, tracked obl: DropObligation<Self::Key>)

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: Send + ?Sized,

§

impl<M> Sync for Segment<M>
where M: Sync + ?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