ostd::specs::mm::page_table::cursor::owners

Struct CursorView

pub struct CursorView<C: PageTableConfig> {
    pub cur_va: Vaddr,
    pub mappings: Set<Mapping>,
    pub phantom: PhantomData<C>,
}

Fields§

§cur_va: Vaddr§mappings: Set<Mapping>§phantom: PhantomData<C>

Implementations§

Source §

impl<C: PageTableConfig> CursorView<C>

Source

pub open spec fn non_overlapping(self) -> bool

{
    forall |m: Mapping, n: Mapping| {
        self.mappings.contains(m)
            ==> (self.mappings.contains(n)
                ==> (m != n
                    ==> m.va_range.end <= n.va_range.start
                        || n.va_range.end <= m.va_range.start))
    }
}

Mappings in the view are non-overlapping. This is a consequence of the page table tree structure: distinct paths map to disjoint VA ranges.

Source §

impl<C: PageTableConfig> CursorView<C>

A CursorView is not aware that the underlying structure of the page table is a tree. It treats the page table as an array of mappings of various sizes, and the cursor itself as the current virtual address, moving from low to high addresses. These functions specify its behavior and provide a simple interface for reasoning about its behavior.

Source

pub open spec fn item_into_mapping(va: Vaddr, item: C::Item) -> Mapping

{
    let (paddr, level, prop) = C::item_into_raw_spec(item);
    let size = page_size(level);
    Mapping {
        va_range: va as int..va as int + size as int,
        pa_range: paddr..(paddr + size) as Paddr,
        page_size: size,
        property: prop,
    }
}

Source

pub open spec fn present(self) -> bool

{
    self
        .mappings
        .filter(|m: Mapping| m.va_range.start <= self.cur_va < m.va_range.end)
        .len() > 0
}

This function checks if the current virtual address is mapped. It does not correspond to a cursor method itself, but defines what it means for an entry to present: there is a mapping whose virtual address range contains the current virtual address.

Source

pub open spec fn query_mapping(self) -> Mapping

recommends

self.present(),

{
    self.mappings
        .filter(|m: Mapping| m.va_range.start <= self.cur_va < m.va_range.end)
        .choose()
}

Source

pub open spec fn query(self, paddr: Paddr, size: usize, prop: PageProperty) -> bool

{
    let m = self.query_mapping();
    m.pa_range.start == paddr && m.page_size == size && m.property == prop
}

Source

pub open spec fn query_range(self) -> Range<int>

{ self.query_mapping().va_range }

Source

pub open spec fn cur_slot_range(self, size: usize) -> Range<int>

{
    let start = nat_align_down(self.cur_va as nat, size as nat) as int;
    start..start + size as int
}

The VA range of the current slot when mapping a page of the given size. Works for both present and absent mappings: when present, equals query_range() for a mapping of that size; when absent, returns the aligned range that would be mapped.

Source

pub open spec fn query_item_spec(self, item: C::Item) -> Option<Range<Vaddr>>

recommends

self.present(),

{
    let (paddr, level, prop) = C::item_into_raw_spec(item);
    let size = page_size(level);
    if self.query(paddr, size, prop) {
        let r = self.query_range();
        Some(r.start as Vaddr..r.end as Vaddr)
    } else {
        None
    }
}

This predicate specifies the behavior of the query method. It states that the current item in the page table matches the given item, mapped at the resulting virtual address range.

Source

pub open spec fn find_next_impl_spec( self, len: usize, find_unmap_subtree: bool, split_huge: bool, ) -> (Self, Option<Mapping>)

{
    let mappings_in_range = self
        .mappings
        .filter(|m: Mapping| {
            self.cur_va as int <= m.va_range.start < self.cur_va as int + len as int
        });
    if mappings_in_range.len() > 0 {
        let mapping = mappings_in_range
            .find_unique_minimal(|m: Mapping, n: Mapping| {
                m.va_range.start < n.va_range.start
            });
        let view = CursorView {
            cur_va: mapping.va_range.end as Vaddr,
            ..self
        };
        (view, Some(mapping))
    } else {
        let view = CursorView {
            cur_va: (self.cur_va + len) as Vaddr,
            ..self
        };
        (view, None)
    }
}

The specification for the internal function, find_next_impl. It finds the next mapped virtual address that is at most len bytes away from the current virtual address. TODO: add the specifications for find_unmap_subtree and split_huge, which are used by other functions that call this one. This returns a mapping rather than the address because that is useful when it’s called as a subroutine.

Source

pub open spec fn find_next_spec(self, len: usize) -> (Self, Option<Vaddr>)

{
    let (cursor, mapping) = self.find_next_impl_spec(len, false, false);
    if mapping is Some {
        (cursor, Some(mapping.unwrap().va_range.start as Vaddr))
    } else {
        (cursor, None)
    }
}

Actual specification for find_next. The cursor finds the next mapped virtual address that is at most len bytes away from the current virtual address, returns it, and then moves the cursor forward to the next end of its range.

Source

pub open spec fn jump_spec(self, va: usize) -> Self

{
    CursorView {
        cur_va: va as Vaddr,
        ..self
    }
}

Jump just sets the current virtual address to the given address.

Source

pub open spec fn align_up_spec(self, size: usize) -> Vaddr

{ nat_align_up(self.cur_va as nat, size as nat) as Vaddr }

Source

pub open spec fn split_index(m: Mapping, new_size: usize, n: usize) -> Mapping

{
    Mapping {
        va_range: m.va_range.start
            + n as int
                * new_size as int..m.va_range.start + (n + 1) as int * new_size as int,
        pa_range: (m.pa_range.start + n * new_size)
            as usize..(m.pa_range.start + (n + 1) * new_size) as usize,
        page_size: new_size,
        property: m.property,
    }
}

Source

pub open spec fn split_if_mapped_huge_spec(self, new_size: usize) -> Self

{
    let m = self.query_mapping();
    let size = m.page_size;
    let new_mappings = Set::<int>::new(|n: int| 0 <= n < size / new_size)
        .map(|n: int| Self::split_index(m, new_size, n as usize));
    CursorView {
        cur_va: self.cur_va,
        mappings: self.mappings - set![m] + new_mappings,
        ..self
    }
}

Source

pub open spec fn split_while_huge(self, size: usize) -> Self

{
    if self.present() {
        let m = self.query_mapping();
        if m.page_size > size {
            let new_size = m.page_size / NR_ENTRIES;
            let new_self = self.split_if_mapped_huge_spec(new_size);
            new_self.split_while_huge(size)
        } else {
            self
        }
    } else {
        self
    }
}

Source

pub open spec fn remove_subtree(self, size: usize) -> Set<Mapping>

{
    let start = nat_align_down(self.cur_va as nat, size as nat) as Vaddr;
    let subtree = self
        .mappings
        .filter(|m: Mapping| start <= m.va_range.start < start + size);
    self.mappings - subtree
}

Source

pub open spec fn map_spec(self, paddr: Paddr, size: usize, prop: PageProperty) -> Self

{
    let new = Mapping {
        va_range: self.cur_slot_range(size),
        pa_range: paddr..(paddr + size) as usize,
        page_size: size,
        property: prop,
    };
    let split_self = self.split_while_huge(size);
    CursorView {
        cur_va: split_self.align_up_spec(size),
        mappings: split_self.remove_subtree(size) + set![new],
        ..split_self
    }
}

Inserts a mapping into the cursor. If there were previously mappings there, they are removed. Note that multiple mappings might be removed if they overlap with a new large mapping.

Source

pub open spec fn map_simple(self, paddr: Paddr, size: usize, prop: PageProperty) -> Self

{
    let new = Mapping {
        va_range: self.cur_slot_range(size),
        pa_range: paddr..(paddr + size) as usize,
        page_size: size,
        property: prop,
    };
    CursorView {
        cur_va: self.cur_va,
        mappings: self.mappings + set![new],
        ..self
    }
}

Source

pub open spec fn unmap_spec(self, len: usize, new_view: Self, num_unmapped: usize) -> bool

{
    let start = self.cur_va;
    let end = (self.cur_va + len) as Vaddr;
    &&& new_view.cur_va >= end
    &&& forall |m: Mapping| {
        #[trigger] self.mappings.contains(m)
            && (m.va_range.end <= start || m.va_range.start >= end)
            ==> new_view.mappings.contains(m)
    }
    &&& forall |m: Mapping| {
        new_view.mappings.contains(m) && start <= m.va_range.start < end
            ==> exists |parent: Mapping| {
                #[trigger] self.mappings.contains(parent)
                    && parent.va_range.start < start
                    && parent.va_range.start <= m.va_range.start
                    && m.va_range.end <= parent.va_range.end
                    && m.pa_range.start
                        == (parent.pa_range.start
                            + (m.va_range.start - parent.va_range.start)) as Paddr
                    && m.property == parent.property
            }
    }
    &&& forall |m: Mapping| {
        #[trigger] new_view.mappings.contains(m)
            ==> self.mappings.contains(m)
                || exists |parent: Mapping| {
                    #[trigger] self.mappings.contains(parent)
                        && parent.va_range.start <= m.va_range.start
                        && m.va_range.end <= parent.va_range.end
                        && m.pa_range.start
                            == (parent.pa_range.start
                                + (m.va_range.start - parent.va_range.start)) as Paddr
                        && m.property == parent.property
                }
    }

}

Unmaps a range of virtual addresses from the current address up to len bytes. It returns the number of mappings that were removed.

Because the implementation may split huge pages that straddle the range boundaries, the spec first applies split_while_huge at both cur_va and cur_va + len to obtain a “base” set of mappings where all boundary entries are at the finest granularity. Mappings whose va_range.start falls in [cur_va, cur_va + len) are then removed from this base.

Source

pub open spec fn protect_spec( self, len: usize, op: FnSpec<(PageProperty,), PageProperty>, target_page_size: usize, ) -> (Self, Option<Range<Vaddr>>)

{
    let (find_cursor, next) = self.find_next_impl_spec(len, false, true);
    if next is Some {
        let found = next.unwrap();
        let at_found = CursorView {
            cur_va: found.va_range.start as Vaddr,
            ..self
        };
        let split_view = at_found.split_while_huge(target_page_size);
        let split_mapping = split_view.query_mapping();
        let new_mapping = Mapping {
            property: op(split_mapping.property),
            ..split_mapping
        };
        let new_cursor = CursorView {
            cur_va: split_mapping.va_range.end as Vaddr,
            mappings: split_view.mappings - set![split_mapping] + set![new_mapping],
            ..self
        };
        (
            new_cursor,
            Some(
                split_mapping.va_range.start
                    as Vaddr..split_mapping.va_range.end as Vaddr,
            ),
        )
    } else {
        (find_cursor, None)
    }
}

Models protect_next: find the next mapping in range, split it to target_page_size if it is a huge page, then update its property via op.

target_page_size corresponds to the cursor level after find_next_impl with split_huge = true — this is determined by the page table structure and cannot be derived from the abstract view alone.

Source §

impl<C: PageTableConfig> CursorView<C>

Source

pub proof fn split_if_mapped_huge_spec_preserves_present(v: Self, new_size: usize)

requires

v.inv(),

v.present(),

new_size > 0,

v.query_mapping().page_size > 0,

v.query_mapping().page_size % new_size == 0,

ensures

v.split_if_mapped_huge_spec(new_size).present(),

After split_if_mapped_huge_spec(new_size), a sub-mapping at cur_va still exists. The witness is split_index(m, new_size, k) where k = (cur_va - m.va_range.start) / new_size.

Source

pub proof fn split_if_mapped_huge_spec_decreases_page_size(v: Self, new_size: usize)

requires

v.inv(),

v.present(),

new_size > 0,

v.query_mapping().page_size > new_size,

v.query_mapping().page_size % new_size == 0,

ensures

v.split_if_mapped_huge_spec(new_size).present(),

v.split_if_mapped_huge_spec(new_size).query_mapping().page_size
    < v.query_mapping().page_size,

After split_if_mapped_huge_spec(new_size) on a valid view, the mapping at cur_va has page_size == new_size < m.page_size.

The sub-mapping split_index(m, new_size, k) has page_size = new_size. No other mapping from the original view covers cur_va (non-overlapping), so query_mapping() must return a sub-mapping with page_size = new_size.

Source

pub proof fn split_if_mapped_huge_spec_preserves_inv(v: Self, new_size: usize)

requires

v.inv(),

v.present(),

new_size > 0,

v.query_mapping().page_size > new_size,

v.query_mapping().page_size % new_size == 0,

set![4096usize, 2097152, 1073741824].contains(new_size),

ensures

v.split_if_mapped_huge_spec(new_size).inv(),

split_if_mapped_huge_spec preserves CursorView::inv().

Requires: v.inv(), v.present(), the mapping at cur_va has page_size > new_size, page_size % new_size == 0, and new_size is itself a valid page size.

Source

pub broadcast proof fn lemma_split_while_huge_preserves_cur_va(self, size: usize)

requires

self.inv(),

size >= PAGE_SIZE,

ensures

#[trigger] self.split_while_huge(size).cur_va == self.cur_va,

split_while_huge only modifies mappings, not cur_va.

Source

pub proof fn lemma_split_while_huge_preserves_inv(self, size: usize)

requires

self.inv(),

size >= PAGE_SIZE,

ensures

self.split_while_huge(size).inv(),

split_while_huge preserves CursorView::inv().

Source

pub proof fn split_while_huge_compose(self, s1: usize, s2: usize)

requires

self.inv(),

s1 >= PAGE_SIZE,

s2 <= s1,

ensures

self.split_while_huge(s2) == self.split_while_huge(s1).split_while_huge(s2),

Composition law for split_while_huge: splitting to a finer target s2 <= s1 is the same as first splitting to s1 and then further splitting to s2.

Source

pub proof fn split_while_huge_idempotent(self, size: usize)

requires

self.inv(),

size >= PAGE_SIZE,

ensures

self.split_while_huge(size).split_while_huge(size) == self.split_while_huge(size),

When the current entry is absent or maps at page_size <= size, split_while_huge(size) is a no-op. Applying a second call with the same size therefore returns the same value.

Source

pub proof fn split_while_huge_noop_implies_page_size_le(self, size: usize)

requires

self.inv(),

size >= PAGE_SIZE,

self.split_while_huge(size) == self,

self.present(),

ensures

self.query_mapping().page_size <= size,

When split_while_huge(size) is a no-op and the view is present(), the mapping at cur_va already has page_size <= size.

Source

pub proof fn split_while_huge_one_step(self, size: usize)

requires

self.inv(),

self.present(),

self.query_mapping().page_size > size,

self.query_mapping().page_size / NR_ENTRIES == size,

self.query_mapping().page_size % size == 0,

set![4096usize, 2097152, 1073741824].contains(size),

ensures

self.split_while_huge(size).mappings =~= self.split_if_mapped_huge_spec(size).mappings,

When the mapping at cur_va is exactly one split-step above size (i.e. query_mapping().page_size / NR_ENTRIES == size), one step of split_while_huge equals split_if_mapped_huge_spec:

self.split_while_huge(size) == self.split_if_mapped_huge_spec(size)

This is because split_while_huge takes one step split_if_mapped_huge_spec(m.page_size / NR_ENTRIES) = split_if_mapped_huge_spec(size), then the sub-mapping at cur_va has page_size == size <= size, so it stops.

Source

pub proof fn split_if_mapped_huge_spec_locality(self, new_size: usize, m2: Mapping)

requires

self.inv(),

self.present(),

new_size > 0,

self.query_mapping().page_size % new_size == 0,

Mapping::disjoint_vaddrs(m2, self.query_mapping()),

ensures

self.split_if_mapped_huge_spec(new_size).mappings.contains(m2)
    == self.mappings.contains(m2),

Locality of split_if_mapped_huge_spec: a mapping m2 whose VA range is disjoint from the mapping at cur_va is preserved.

Source

pub proof fn split_while_huge_locality(self, size: usize, m2: Mapping)

requires

self.inv(),

size >= PAGE_SIZE,

self.mappings.contains(m2),

!(m2.va_range.start <= self.cur_va < m2.va_range.end),

ensures

self.split_while_huge(size).mappings.contains(m2),

Locality of split_while_huge: a mapping m2 that is in self.mappings and whose VA range does not contain cur_va is preserved.

This is stronger than split_if_mapped_huge_spec_locality because it handles the recursive case: each step only splits the mapping at cur_va, and m2 is disjoint from that mapping (by non-overlap invariant).

Source

pub proof fn split_while_huge_locality_absent(self, size: usize, m2: Mapping)

requires

self.inv(),

size >= PAGE_SIZE,

!self.mappings.contains(m2),

self.present() ==> Mapping::disjoint_vaddrs(m2, self.query_mapping()),

ensures

!self.split_while_huge(size).mappings.contains(m2),

Converse locality: a mapping NOT in self.mappings and whose VA range does not overlap any mapping in self.mappings that contains cur_va is also NOT in self.split_while_huge(size).mappings.

More precisely: if m2 ∉ self.mappings and m2.va_range is disjoint from the range [start, end) of the mapping at cur_va (if present), then m2 ∉ self.split_while_huge(size).mappings.

Source

pub proof fn split_if_mapped_huge_spec_refinement(self, new_size: usize, e: Mapping)

requires

self.inv(),

self.present(),

new_size > 0,

self.query_mapping().page_size > new_size,

self.query_mapping().page_size % new_size == 0,

self.split_if_mapped_huge_spec(new_size).mappings.contains(e),

ensures

self.mappings.contains(e)
    || {
        let parent = self.query_mapping();
        &&& self.mappings.contains(parent)
        &&& parent.va_range.start <= e.va_range.start
        &&& e.va_range.end <= parent.va_range.end
        &&& e.pa_range.start
            == (parent.pa_range.start + (e.va_range.start - parent.va_range.start))
                as Paddr
        &&& e.property == parent.property

    },

Refinement: every mapping in split_while_huge(size).mappings is either from self.mappings or a sub-mapping of an entry in self.mappings. Base lemma: every mapping in split_if_mapped_huge_spec(new_size).mappings is either from the original mappings or a sub-mapping of query_mapping().

Source

pub proof fn split_while_huge_refinement(self, size: usize, m: Mapping)

requires

self.inv(),

size >= PAGE_SIZE,

self.split_while_huge(size).mappings.contains(m),

ensures

self.mappings.contains(m)
    || exists |parent: Mapping| {
        #[trigger] self.mappings.contains(parent)
            && parent.va_range.start <= m.va_range.start
            && m.va_range.end <= parent.va_range.end
            && m.pa_range.start
                == (parent.pa_range.start + (m.va_range.start - parent.va_range.start))
                    as Paddr && m.property == parent.property
    },

Source

pub proof fn split_while_huge_disjoint(self, size: usize, other: Set<Mapping>)

requires

self.inv(),

self.mappings.disjoint(other),

ensures

self.split_while_huge(size).mappings.disjoint(other),

split_while_huge produces a set disjoint from any set that was already disjoint from self.mappings.

Proof sketch: split_while_huge only adds sub-mappings of the entry at cur_va and preserves all other entries from self.mappings. If other is disjoint from self.mappings, then entries preserved from self.mappings aren’t in other, and sub-mappings (with va_range ⊂ query_mapping().va_range) can’t equal any entry in other because other has no entry overlapping the query mapping (which is in self.mappings).

Trait Implementations§

Source §

impl<C: PageTableConfig> Inv for CursorView<C>

Source §

open spec fn inv(self) -> bool

{
    &&& self.mappings.finite()
    &&& forall |m: Mapping| self.mappings.contains(m) ==> m.inv()
    &&& forall |m: Mapping| {
        self.mappings.contains(m)
            ==> {
                &&& vaddr_range_bounds_spec::<C>().0 <= m.va_range.start
                &&& m.va_range.end <= vaddr_range_bounds_spec::<C>().1 + 1

            }
    }
    &&& self.non_overlapping()

}

Source §

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

Performs the conversion.

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

Performs the conversion.

Struct CursorView Copy item path

Fields§

Implementations§

impl<C: PageTableConfig> CursorView<C>

pub open spec fn non_overlapping(self) -> bool

impl<C: PageTableConfig> CursorView<C>

pub open spec fn item_into_mapping(va: Vaddr, item: C::Item) -> Mapping

pub open spec fn present(self) -> bool

pub open spec fn query_mapping(self) -> Mapping

pub open spec fn query(self, paddr: Paddr, size: usize, prop: PageProperty) -> bool

pub open spec fn query_range(self) -> Range<int>

pub open spec fn cur_slot_range(self, size: usize) -> Range<int>

pub open spec fn query_item_spec(self, item: C::Item) -> Option<Range<Vaddr>>

pub open spec fn find_next_impl_spec( self, len: usize, find_unmap_subtree: bool, split_huge: bool, ) -> (Self, Option<Mapping>)

pub open spec fn find_next_spec(self, len: usize) -> (Self, Option<Vaddr>)

pub open spec fn jump_spec(self, va: usize) -> Self

pub open spec fn align_up_spec(self, size: usize) -> Vaddr

pub open spec fn split_index(m: Mapping, new_size: usize, n: usize) -> Mapping

pub open spec fn split_if_mapped_huge_spec(self, new_size: usize) -> Self

pub open spec fn split_while_huge(self, size: usize) -> Self

pub open spec fn remove_subtree(self, size: usize) -> Set<Mapping>

pub open spec fn map_spec(self, paddr: Paddr, size: usize, prop: PageProperty) -> Self

pub open spec fn map_simple(self, paddr: Paddr, size: usize, prop: PageProperty) -> Self

pub open spec fn unmap_spec(self, len: usize, new_view: Self, num_unmapped: usize) -> bool

pub open spec fn protect_spec( self, len: usize, op: FnSpec<(PageProperty,), PageProperty>, target_page_size: usize, ) -> (Self, Option<Range<Vaddr>>)

impl<C: PageTableConfig> CursorView<C>

pub proof fn split_if_mapped_huge_spec_preserves_present(v: Self, new_size: usize)

pub proof fn split_if_mapped_huge_spec_decreases_page_size(v: Self, new_size: usize)

pub proof fn split_if_mapped_huge_spec_preserves_inv(v: Self, new_size: usize)

pub broadcast proof fn lemma_split_while_huge_preserves_cur_va(self, size: usize)

pub proof fn lemma_split_while_huge_preserves_inv(self, size: usize)

pub proof fn split_while_huge_compose(self, s1: usize, s2: usize)

pub proof fn split_while_huge_idempotent(self, size: usize)

pub proof fn split_while_huge_noop_implies_page_size_le(self, size: usize)

pub proof fn split_while_huge_one_step(self, size: usize)

pub proof fn split_if_mapped_huge_spec_locality(self, new_size: usize, m2: Mapping)

pub proof fn split_while_huge_locality(self, size: usize, m2: Mapping)

pub proof fn split_while_huge_locality_absent(self, size: usize, m2: Mapping)

pub proof fn split_if_mapped_huge_spec_refinement(self, new_size: usize, e: Mapping)

pub proof fn split_while_huge_refinement(self, size: usize, m: Mapping)

pub proof fn split_while_huge_disjoint(self, size: usize, other: Set<Mapping>)

Trait Implementations§

impl<C: PageTableConfig> Inv for CursorView<C>

open spec fn inv(self) -> bool

Auto Trait Implementations§

impl<C> Freeze for CursorView<C>

impl<C> RefUnwindSafe for CursorView<C>where C: RefUnwindSafe,

impl<C> Send for CursorView<C>

impl<C> Sync for CursorView<C>

impl<C> Unpin for CursorView<C>where C: Unpin,

impl<C> UnsafeUnpin for CursorView<C>

impl<C> UnwindSafe for CursorView<C>where C: UnwindSafe,

Blanket Implementations§

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

fn type_id(&self) -> TypeId

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

fn borrow(&self) -> &T

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

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

impl<T> From<T> for T

fn from(t: T) -> T

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

fn obeys_from_spec() -> bool

fn from_spec(v: T) -> VERUS_SPEC__A

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

fn into(self) -> U

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

fn obeys_into_spec() -> bool

fn into_spec(self) -> T

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

fn obeys_into_spec() -> bool

fn into_spec(self) -> U

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

type Error = Infallible

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

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__Awhere 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>

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

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

Struct CursorView

impl<C> RefUnwindSafe for CursorView<C>
where C: RefUnwindSafe,

impl<C> Unpin for CursorView<C>
where C: Unpin,

impl<C> UnwindSafe for CursorView<C>
where C: UnwindSafe,

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

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

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

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

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

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

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

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

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

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

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

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