Struct Segment 

pub struct Segment<M: AnyFrameMeta + ?Sized> { /* private fields */ }

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.

Implementations

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

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>,
Tracked(repr_perm): Tracked<&mut M::ReprPerm>,

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(),

(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.inv()
    &&& seg.start_paddr() == range.start
    &&& seg.end_paddr() == range.end
    &&& seg.start_paddr() < seg.end_paddr()
    &&& seg.relate_regions(*final(regions))
    &&& forall |paddr: Paddr| {
        (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
            ==> final(regions).contains(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). FIXME: this implementation does not match source code.

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

pub exec fn start_paddr(&self) -> Paddr

returns

self.start_paddr(),

Gets the start physical address of the contiguous frames.

pub fn __VERUS_SPEC_start_paddr(&self) -> Paddr

pub exec fn end_paddr(&self) -> Paddr

returns

self.end_paddr(),

Gets the end physical address of the contiguous frames.

pub fn __VERUS_SPEC_end_paddr(&self) -> Paddr

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.

pub fn __VERUS_SPEC_size(&self) -> usize

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

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

pub open spec fn len(&self) -> int

{ (self.size() / PAGE_SIZE) as int }

Returns the number of pages of the contiguous frames.

pub closed spec fn raw_perms(&self) -> Seq<FrameRawPerms>

pub open spec fn metadata_perms(&self) -> Seq<FracMetadataPerm>

{ self.raw_perms().map_values(|perm: FrameRawPerms| perm.metadata_perm) }

pub closed spec fn inner_perm_inv(&self) -> bool

pub open spec fn slot_perms(&self) -> Seq<&'static PointsTo<MetaSlot>>

{ self.raw_perms().map_values(|perm: FrameRawPerms| perm.slot_perm) }

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

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

requires

self.inv(),

offset % PAGE_SIZE != 0 ==> may_panic(),

!(0 < offset && offset < self.size()) ==> may_panic(),

ensures

(r.0, r.1) == self.split_spec(offset),

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;
• the offset must be aligned and within bounds;

Postconditions

• the resulting segments satisfy their invariants;
• they match Self::split_spec.

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_owner((self.start_paddr() + j * PAGE_SIZE) as usize)
                .ref_count() >= 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).

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

with

Tracked(regions): Tracked<&mut MetaRegionOwners>,

requires

self.inv(),

old(regions).inv(),

self.relate_regions(*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.start_paddr() + range.end <= self.end_paddr(),

!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(),

r.relate_regions(*final(regions)),

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].

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

recommends

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.

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

pub exec fn drop(self)

with

Tracked(regions): Tracked<&mut MetaRegionOwners>,

requires

old(regions).inv(),

self.inv(),

self.relate_regions(*old(regions)),

forall |i: int| {
    0 <= i < self.len()
        ==> {
            let idx = frame_to_index((self.start_paddr() + i * PAGE_SIZE) as usize);
            &&& old(regions).slot_owners[idx].storage_perm().is_init()
            &&& old(regions).ref_count(idx) == 1
                ==> {
                    &&& old(regions).slot_owners[idx].in_list_perm.value() == 0

                }

        }
},

ensures

final(regions).inv(),

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

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(self.start_paddr()),

r.remain_spec() == self.size(),

owner@.is_kernel,

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(self.start_paddr()),

r.avail_spec() == self.size(),

owner@.is_kernel,

!owner@.is_fallible,

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

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

{
    &&& forall |i: int| {
        0 <= i < self.len()
            ==> {
                let idx = frame_to_index((self.range().start + i * PAGE_SIZE) as usize);
                &&& self.raw_perms()[i].slot_perm == regions.slots[idx]
                &&& self.raw_perms()[i].inv()
                &&& self.raw_perms()[i].metadata_perm.id()
                    == regions.slot_owners[idx].metadata_perm.id()
                &&& regions.contains(idx)
                &&& regions.slot_owners[idx].slot_vaddr == index_to_meta(idx)
                &&& 0 < regions.slot_owners[idx].ref_count()
                    <= 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 < self.len()
            ==> 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.

Trait Implementations

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

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

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

open spec fn obeys_from_spec() -> bool

{ true }

closed spec fn from_spec(frame: Frame<M>) -> Self

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

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
    &&& self.inner_perm_inv()
    &&& self.raw_perms().len() == self.len()
    &&& forall |i: int| {
        0 <= i < self.raw_perms().len()
            ==> {
                let paddr = (self.range().start + i * PAGE_SIZE) as usize;
                &&& self.raw_perms()[i].slot_vaddr() == frame_to_meta(paddr)
                &&& self.raw_perms()[i].inv()

            }
    }

}

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.

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

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

type Item = Frame<M>

The type of the elements being iterated over.

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.

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

Returns the bounds on the remaining length of the iterator.

fn count(self) -> usize

where Self: Sized,

Consumes the iterator, counting the number of iterations and returning it.

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

where Self: Sized,

Consumes the iterator, returning the last element.

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.

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

Returns the nth element of the iterator.

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.

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.

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.

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.

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.

fn for_each<F>(self, f: F)

where Self: Sized, F: FnMut(Self::Item),

Calls a closure on each element of an iterator.

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.

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.

fn enumerate(self) -> Enumerate<Self>

where Self: Sized,

Creates an iterator which gives the current iteration count as well as the next value.

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.

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.

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.

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.

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

where Self: Sized,

Creates an iterator that skips the first n elements.

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.

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.

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.

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.

fn fuse(self) -> Fuse<Self>

where Self: Sized,

Creates an iterator which ends after the first None.

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.

fn by_ref(&mut self) -> &mut Self

where Self: Sized,

Creates a “by reference” adapter for this instance of Iterator.

fn collect<B>(self) -> B

where B: FromIterator<Self::Item>, Self: Sized,

Transforms an iterator into a collection.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

fn sum<S>(self) -> S

where Self: Sized, S: Sum<Self::Item>,

Sums the elements of an iterator.

fn product<P>(self) -> P

where Self: Sized, P: Product<Self::Item>,

Iterates over the entire iterator, multiplying all the elements.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

closed spec fn remaining(&self) -> Seq<Self::Item>

closed spec fn will_return_none(&self) -> bool

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

open spec fn peek(&self, index: int) -> Option<Self::Item>

{
    if 0 <= index < self.metadata_perms().len() {
        Some(
            Frame::<
                M,
            >::from_raw_spec(
                (self.range().start + index * PAGE_SIZE) as usize,
                self.slot_perms()[index],
                Some(self.metadata_perms()[index]),
            ),
        )
    } else {
        None
    }
}

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

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

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

            }
    }

}

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

{
    &&& res.range() == self.range()
    &&& res.inv()
    &&& new_perm.inv()
    &&& res.relate_regions(new_perm)

}

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