Skip to main content

VmStore

ostd::specs::mm::embedding

Struct VmStore 

Source 
pub struct VmStore<'rcu> {
    pub regions: MetaRegionOwners,
    pub tlb_model: TlbModel,
    pub vm_spaces: Map<VmSpaceId, VmSpaceOwner>,
    pub cursors: Map<CursorId, CursorEntry<'rcu>>,
    pub vm_ios: Map<VmIoId, VmIoEntry>,
    pub frames: Map<FrameId, FrameEntry>,
    pub segments: Map<SegmentId, SegmentEntry>,
    pub unique_frames: Map<UniqueId, UniqueEntry>,
}
Expand description

Resource store: the abstract state visible to a caller of the VmSpace + VmReader/VmWriter API.

Fields§

§regions: MetaRegionOwners§tlb_model: TlbModel§vm_spaces: Map<VmSpaceId, VmSpaceOwner>§cursors: Map<CursorId, CursorEntry<'rcu>>§vm_ios: Map<VmIoId, VmIoEntry>§frames: Map<FrameId, FrameEntry>§segments: Map<SegmentId, SegmentEntry>§unique_frames: Map<UniqueId, UniqueEntry>

Implementations§

Source§

impl<'a, 'rcu> VmStore<'rcu>

Source

pub open spec fn inv(self) -> bool

{ self.structural_inv() && self.accounting_inv() && self.regions.inv() }

The store’s top-level invariant.

Source

pub open spec fn structural_inv(self) -> bool

{
    &&& forall |idx: int| {
        0 <= idx < max_meta_slots()
            ==> #[trigger] self.regions.slots.contains_key(idx)
                || (self.regions.slot_owners[idx].usage is PageTable
                    && self.regions.ref_count(idx) != REF_COUNT_UNUSED)
    }
    &&& forall |idx: int| {
        0 <= idx < max_meta_slots()
            ==> #[trigger] self.regions.slot_owners[idx].in_list_perm.value() == 0
    }
    &&& self.tlb_model.inv()
    &&& forall |id: VmSpaceId| {
        #[trigger] self.vm_spaces.contains_key(id) ==> self.vm_spaces[id].inv()
    }
    &&& forall |id: CursorId| {
        #[trigger] self.cursors.contains_key(id) ==> self.cursors[id].inv()
    }
    &&& forall |id: CursorId| {
        #[trigger] self.cursors.contains_key(id)
            ==> self.cursors[id].owner.metaregion_sound(self.regions)
    }
    &&& forall |id: CursorId| {
        #[trigger] self.cursors.contains_key(id)
            ==> self.vm_spaces.contains_key(self.cursors[id].vm_space)
    }
    &&& forall |id: VmIoId| {
        #[trigger] self.vm_ios.contains_key(id) ==> self.vm_ios[id].inv()
    }
    &&& forall |id: VmIoId| {
        #[trigger] self.vm_ios.contains_key(id)
            ==> (self
                .vm_ios[id]
                .vm_space matches Some(vs) ==> self.vm_spaces.contains_key(vs))
    }
    &&& forall |id: VmIoId| {
        #[trigger] self.vm_ios.contains_key(id)
            ==> (self.vm_ios[id].vm_space is Some
                ==> (self.vm_ios[id].vaddr as nat) + (self.vm_ios[id].len as nat)
                    <= MAX_USERSPACE_VADDR as nat)
    }
    &&& forall |fid: FrameId| {
        #[trigger] self.frames.contains_key(fid)
            ==> valid_frame_paddr(self.frames[fid].paddr)
    }
    &&& forall |fid: FrameId| {
        #[trigger] self.frames.contains_key(fid)
            ==> self.regions.slot_owner(self.frames[fid].paddr).usage is Frame
    }
    &&& forall |sid: SegmentId| {
        #[trigger] self.segments.contains_key(sid)
            ==> {
                let r = self.segments[sid].range;
                &&& r.start % PAGE_SIZE == 0
                &&& r.end % PAGE_SIZE == 0
                &&& r.start < r.end
                &&& r.end <= MAX_PADDR

            }
    }
    &&& forall |sid: SegmentId, paddr: Paddr| {
        self.segments.contains_key(sid)
            && self.segments[sid].range.start <= paddr < self.segments[sid].range.end
            && paddr % PAGE_SIZE == 0 ==> self.regions.slot_owner(paddr).usage is Frame
    }
    &&& forall |uid: UniqueId| {
        #[trigger] self.unique_frames.contains_key(uid)
            ==> valid_frame_paddr(self.unique_frames[uid].paddr)
    }
    &&& forall |uid: UniqueId| {
        #[trigger] self.unique_frames.contains_key(uid)
            ==> {
                let so = self.regions.slot_owner(self.unique_frames[uid].paddr);
                &&& so.usage is Frame
                &&& so.ref_count() == REF_COUNT_UNIQUE
                &&& so.in_list_perm.value() == 0
                &&& so.paths_in_pt.is_empty()

            }
    }
    &&& forall |uid1: UniqueId, uid2: UniqueId| {
        self.unique_frames.contains_key(uid1) && self.unique_frames.contains_key(uid2)
            && self.unique_frames[uid1].paddr == self.unique_frames[uid2].paddr
            ==> uid1 == uid2
    }

}

Everything in [inv] except the accounting equation. Preserved by any helper that touches at most one of frames / regions.slot_owners, since the accounting equation is the only clause that mentions both. Frame-only helpers ([tracked_extract_frame] / [lemma_insert_frame]) require / ensure this.

Source

pub open spec fn accounting_inv(self) -> bool

{
    &&& forall |idx: int| {
        0 <= idx < max_meta_slots() && self.regions.ref_count(idx) == REF_COUNT_UNUSED
            ==> handle_count(self.frames, idx) == 0
                && self.regions.slot_owners[idx].paths_in_pt.is_empty()
                && segment_cover_count(self.segments, index_to_frame(idx)) == 0
    }
    &&& forall |idx: int| {
        0 <= idx < max_meta_slots() && self.regions.slot_owners[idx].usage is Frame
            && self.regions.ref_count(idx) != REF_COUNT_UNUSED
            && self.regions.ref_count(idx) != REF_COUNT_UNIQUE
            ==> handle_count(self.frames, idx) > 0
                || self.regions.slot_owners[idx].paths_in_pt.len() > 0
                || segment_cover_count(self.segments, index_to_frame(idx)) > 0
    }
    &&& forall |idx: int| {
        0 <= idx < max_meta_slots() && self.regions.slot_owners[idx].usage is Frame
            && (handle_count(self.frames, idx) > 0
                || self.regions.slot_owners[idx].paths_in_pt.len() > 0
                || segment_cover_count(self.segments, index_to_frame(idx)) > 0)
            ==> {
                let so = self.regions.slot_owners[idx];
                let rc = so.ref_count();
                &&& rc != REF_COUNT_UNUSED
                &&& rc != REF_COUNT_UNIQUE
                &&& rc
                    == handle_count(self.frames, idx) + so.paths_in_pt.len()
                        + segment_cover_count(self.segments, index_to_frame(idx))

            }
    }

}
Source§

impl<'rcu> VmStore<'rcu>

Source

pub proof fn tracked_extract_vm_space(tracked &mut self, vs: VmSpaceId) -> tracked res : VmSpaceOwner

requires
old(self).inv(),
old(self).vm_spaces.contains_key(vs),
forall |c: CursorId| {
    #[trigger] old(self).cursors.contains_key(c) ==> old(self).cursors[c].vm_space != vs
},
forall |v: VmIoId| {
    #[trigger] old(self).vm_ios.contains_key(v)
        ==> old(self).vm_ios[v].vm_space != Some(vs)
},
ensures
final(self).regions == old(self).regions,
final(self).tlb_model == old(self).tlb_model,
final(self).vm_spaces == old(self).vm_spaces.remove(vs),
final(self).cursors == old(self).cursors,
final(self).vm_ios == old(self).vm_ios,
final(self).frames == old(self).frames,
final(self).segments == old(self).segments,
final(self).unique_frames == old(self).unique_frames,
res == old(self).vm_spaces[vs],
final(self).inv(),

Removes the VmSpaceOwner at vs from the store and returns it. Requires no cursor or VmIo refers to vs, and no activated ranges remain on vs (otherwise inv would break after the removal).

Source

pub proof fn lemma_insert_vm_space(tracked &mut self, vs: VmSpaceId, tracked owner: VmSpaceOwner)

requires
old(self).inv(),
!old(self).vm_spaces.contains_key(vs),
owner.inv(),
ensures
final(self).regions == old(self).regions,
final(self).tlb_model == old(self).tlb_model,
final(self).vm_spaces == old(self).vm_spaces.insert(vs, owner),
final(self).cursors == old(self).cursors,
final(self).vm_ios == old(self).vm_ios,
final(self).frames == old(self).frames,
final(self).segments == old(self).segments,
final(self).unique_frames == old(self).unique_frames,
final(self).inv(),

Inserts a VmSpaceOwner at the given fresh id. Requires the id is not already used and the owner satisfies its invariant.

Source

pub proof fn tracked_extract_cursor(tracked &mut self, c: CursorId) -> tracked res : CursorEntry<'rcu>

requires
old(self).inv(),
old(self).cursors.contains_key(c),
ensures
final(self).regions == old(self).regions,
final(self).tlb_model == old(self).tlb_model,
final(self).vm_spaces == old(self).vm_spaces,
final(self).cursors == old(self).cursors.remove(c),
final(self).vm_ios == old(self).vm_ios,
final(self).frames == old(self).frames,
final(self).segments == old(self).segments,
final(self).unique_frames == old(self).unique_frames,
res == old(self).cursors[c],
final(self).inv(),

Removes the cursor entry at c from the store and returns it.

Source

pub proof fn lemma_insert_cursor(tracked &mut self, c: CursorId, tracked entry: CursorEntry<'rcu>)

requires
old(self).inv(),
!old(self).cursors.contains_key(c),
entry.inv(),
entry.owner.metaregion_sound(old(self).regions),
old(self).vm_spaces.contains_key(entry.vm_space),
ensures
final(self).regions == old(self).regions,
final(self).tlb_model == old(self).tlb_model,
final(self).vm_spaces == old(self).vm_spaces,
final(self).cursors == old(self).cursors.insert(c, entry),
final(self).vm_ios == old(self).vm_ios,
final(self).frames == old(self).frames,
final(self).segments == old(self).segments,
final(self).unique_frames == old(self).unique_frames,
final(self).inv(),

Inserts a cursor entry at the given fresh id. Requires the id is not already used, the entry satisfies its inv, the entry’s vm_space is in the store, and the entry’s owner is sound w.r.t. the store’s regions.

Source

pub proof fn tracked_extract_vm_io(tracked &mut self, vio: VmIoId) -> tracked res : VmIoEntry

requires
old(self).inv(),
old(self).vm_ios.contains_key(vio),
ensures
final(self).regions == old(self).regions,
final(self).tlb_model == old(self).tlb_model,
final(self).vm_spaces == old(self).vm_spaces,
final(self).cursors == old(self).cursors,
final(self).vm_ios == old(self).vm_ios.remove(vio),
final(self).frames == old(self).frames,
final(self).segments == old(self).segments,
final(self).unique_frames == old(self).unique_frames,
res == old(self).vm_ios[vio],
final(self).inv(),

Removes the VmIo entry at vio from the store and returns it.

Source

pub proof fn lemma_insert_vm_io(tracked &mut self, vio: VmIoId, tracked entry: VmIoEntry)

requires
old(self).inv(),
!old(self).vm_ios.contains_key(vio),
entry.inv(),
entry.vm_space matches Some(vs) ==> old(self).vm_spaces.contains_key(vs),
entry.vm_space is Some
    ==> (entry.vaddr as nat) + (entry.len as nat) <= MAX_USERSPACE_VADDR as nat,
ensures
final(self).regions == old(self).regions,
final(self).tlb_model == old(self).tlb_model,
final(self).vm_spaces == old(self).vm_spaces,
final(self).cursors == old(self).cursors,
final(self).vm_ios == old(self).vm_ios.insert(vio, entry),
final(self).frames == old(self).frames,
final(self).segments == old(self).segments,
final(self).unique_frames == old(self).unique_frames,
final(self).inv(),

Inserts a VmIo entry at the given fresh id.

Source

pub proof fn tracked_extract_frame(tracked &mut self, fid: FrameId) -> tracked res : FrameEntry

requires
old(self).structural_inv(),
old(self).frames.contains_key(fid),
ensures
final(self).regions == old(self).regions,
final(self).tlb_model == old(self).tlb_model,
final(self).vm_spaces == old(self).vm_spaces,
final(self).cursors == old(self).cursors,
final(self).vm_ios == old(self).vm_ios,
final(self).frames == old(self).frames.remove(fid),
final(self).segments == old(self).segments,
final(self).unique_frames == old(self).unique_frames,
res == old(self).frames[fid],
final(self).structural_inv(),

Removes the FrameEntry at fid from the store.

Source

pub proof fn lemma_insert_frame(tracked &mut self, fid: FrameId, tracked entry: FrameEntry)

requires
old(self).structural_inv(),
!old(self).frames.contains_key(fid),
valid_frame_paddr(entry.paddr),
old(self).regions.slot_owner(entry.paddr).usage is Frame,
ensures
final(self).regions == old(self).regions,
final(self).tlb_model == old(self).tlb_model,
final(self).vm_spaces == old(self).vm_spaces,
final(self).cursors == old(self).cursors,
final(self).vm_ios == old(self).vm_ios,
final(self).frames == old(self).frames.insert(fid, entry),
final(self).segments == old(self).segments,
final(self).unique_frames == old(self).unique_frames,
final(self).structural_inv(),

Inserts a FrameEntry at the given fresh id.

Source

pub proof fn tracked_extract_unique(tracked &mut self, uid: UniqueId) -> tracked res : UniqueEntry

requires
old(self).unique_frames.contains_key(uid),
ensures
final(self).regions == old(self).regions,
final(self).tlb_model == old(self).tlb_model,
final(self).vm_spaces == old(self).vm_spaces,
final(self).cursors == old(self).cursors,
final(self).vm_ios == old(self).vm_ios,
final(self).frames == old(self).frames,
final(self).segments == old(self).segments,
final(self).unique_frames == old(self).unique_frames.remove(uid),
res == old(self).unique_frames[uid],

Removes the UniqueEntry at uid from the store.

Source

pub proof fn lemma_insert_unique(tracked &mut self, uid: UniqueId, tracked entry: UniqueEntry)

requires
!old(self).unique_frames.contains_key(uid),
ensures
final(self).regions == old(self).regions,
final(self).tlb_model == old(self).tlb_model,
final(self).vm_spaces == old(self).vm_spaces,
final(self).cursors == old(self).cursors,
final(self).vm_ios == old(self).vm_ios,
final(self).frames == old(self).frames,
final(self).segments == old(self).segments,
final(self).unique_frames == old(self).unique_frames.insert(uid, entry),

Inserts a UniqueEntry at a fresh id.

Source

pub proof fn tracked_extract_segment(tracked &mut self, sid: SegmentId) -> tracked res : SegmentEntry

requires
old(self).segments.contains_key(sid),
ensures
final(self).regions == old(self).regions,
final(self).tlb_model == old(self).tlb_model,
final(self).vm_spaces == old(self).vm_spaces,
final(self).cursors == old(self).cursors,
final(self).vm_ios == old(self).vm_ios,
final(self).frames == old(self).frames,
final(self).segments == old(self).segments.remove(sid),
final(self).unique_frames == old(self).unique_frames,
res == old(self).segments[sid],

Removes the SegmentEntry at sid from the store.

Source

pub proof fn lemma_insert_segment(tracked &mut self, sid: SegmentId, tracked entry: SegmentEntry)

requires
!old(self).segments.contains_key(sid),
ensures
final(self).regions == old(self).regions,
final(self).tlb_model == old(self).tlb_model,
final(self).vm_spaces == old(self).vm_spaces,
final(self).cursors == old(self).cursors,
final(self).vm_ios == old(self).vm_ios,
final(self).frames == old(self).frames,
final(self).segments == old(self).segments.insert(sid, entry),
final(self).unique_frames == old(self).unique_frames,

Inserts a SegmentEntry at a fresh id.

Auto Trait Implementations§

§

impl<'rcu> !RefUnwindSafe for VmStore<'rcu>

§

impl<'rcu> !UnwindSafe for VmStore<'rcu>

§

impl<'rcu> Freeze for VmStore<'rcu>

§

impl<'rcu> Send for VmStore<'rcu>

§

impl<'rcu> Sync for VmStore<'rcu>

§

impl<'rcu> Unpin for VmStore<'rcu>

§

impl<'rcu> UnsafeUnpin for VmStore<'rcu>

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
§

impl<T> Conv for T

§

fn conv<T>(self) -> T
where Self: Into<T>,

Converts self into T using Into<T>. Read more
§

impl<T> FmtForward for T

§

fn fmt_binary(self) -> FmtBinary<Self>
where Self: Binary,

Causes self to use its Binary implementation when Debug-formatted.
§

fn fmt_display(self) -> FmtDisplay<Self>
where Self: Display,

Causes self to use its Display implementation when Debug-formatted.
§

fn fmt_lower_exp(self) -> FmtLowerExp<Self>
where Self: LowerExp,

Causes self to use its LowerExp implementation when Debug-formatted.
§

fn fmt_lower_hex(self) -> FmtLowerHex<Self>
where Self: LowerHex,

Causes self to use its LowerHex implementation when Debug-formatted.
§

fn fmt_octal(self) -> FmtOctal<Self>
where Self: Octal,

Causes self to use its Octal implementation when Debug-formatted.
§

fn fmt_pointer(self) -> FmtPointer<Self>
where Self: Pointer,

Causes self to use its Pointer implementation when Debug-formatted.
§

fn fmt_upper_exp(self) -> FmtUpperExp<Self>
where Self: UpperExp,

Causes self to use its UpperExp implementation when Debug-formatted.
§

fn fmt_upper_hex(self) -> FmtUpperHex<Self>
where Self: UpperHex,

Causes self to use its UpperHex implementation when Debug-formatted.
§

fn fmt_list(self) -> FmtList<Self>
where &'a Self: for<'a> IntoIterator,

Formats each item in a sequence. 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

§

impl<T> FromSpecImpl<T> for T

§

fn obeys_from_spec() -> bool

§

fn from_spec(v: T) -> T

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.

§

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<T> Pipe for T
where T: ?Sized,

§

fn pipe<R>(self, func: impl FnOnce(Self) -> R) -> R
where Self: Sized,

Pipes by value. This is generally the method you want to use. Read more
§

fn pipe_ref<'a, R>(&'a self, func: impl FnOnce(&'a Self) -> R) -> R
where R: 'a,

Borrows self and passes that borrow into the pipe function. Read more
§

fn pipe_ref_mut<'a, R>(&'a mut self, func: impl FnOnce(&'a mut Self) -> R) -> R
where R: 'a,

Mutably borrows self and passes that borrow into the pipe function. Read more
§

fn pipe_borrow<'a, B, R>(&'a self, func: impl FnOnce(&'a B) -> R) -> R
where Self: Borrow<B>, B: 'a + ?Sized, R: 'a,

Borrows self, then passes self.borrow() into the pipe function. Read more
§

fn pipe_borrow_mut<'a, B, R>( &'a mut self, func: impl FnOnce(&'a mut B) -> R, ) -> R
where Self: BorrowMut<B>, B: 'a + ?Sized, R: 'a,

Mutably borrows self, then passes self.borrow_mut() into the pipe function. Read more
§

fn pipe_as_ref<'a, U, R>(&'a self, func: impl FnOnce(&'a U) -> R) -> R
where Self: AsRef<U>, U: 'a + ?Sized, R: 'a,

Borrows self, then passes self.as_ref() into the pipe function.
§

fn pipe_as_mut<'a, U, R>(&'a mut self, func: impl FnOnce(&'a mut U) -> R) -> R
where Self: AsMut<U>, U: 'a + ?Sized, R: 'a,

Mutably borrows self, then passes self.as_mut() into the pipe function.
§

fn pipe_deref<'a, T, R>(&'a self, func: impl FnOnce(&'a T) -> R) -> R
where Self: Deref<Target = T>, T: 'a + ?Sized, R: 'a,

Borrows self, then passes self.deref() into the pipe function.
§

fn pipe_deref_mut<'a, T, R>( &'a mut self, func: impl FnOnce(&'a mut T) -> R, ) -> R
where Self: DerefMut<Target = T> + Deref, T: 'a + ?Sized, R: 'a,

Mutably borrows self, then passes self.deref_mut() into the pipe function.
§

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

§

impl<T> Tap for T

§

fn tap(self, func: impl FnOnce(&Self)) -> Self

Immutable access to a value. Read more
§

fn tap_mut(self, func: impl FnOnce(&mut Self)) -> Self

Mutable access to a value. Read more
§

fn tap_borrow<B>(self, func: impl FnOnce(&B)) -> Self
where Self: Borrow<B>, B: ?Sized,

Immutable access to the Borrow<B> of a value. Read more
§

fn tap_borrow_mut<B>(self, func: impl FnOnce(&mut B)) -> Self
where Self: BorrowMut<B>, B: ?Sized,

Mutable access to the BorrowMut<B> of a value. Read more
§

fn tap_ref<R>(self, func: impl FnOnce(&R)) -> Self
where Self: AsRef<R>, R: ?Sized,

Immutable access to the AsRef<R> view of a value. Read more
§

fn tap_ref_mut<R>(self, func: impl FnOnce(&mut R)) -> Self
where Self: AsMut<R>, R: ?Sized,

Mutable access to the AsMut<R> view of a value. Read more
§

fn tap_deref<T>(self, func: impl FnOnce(&T)) -> Self
where Self: Deref<Target = T>, T: ?Sized,

Immutable access to the Deref::Target of a value. Read more
§

fn tap_deref_mut<T>(self, func: impl FnOnce(&mut T)) -> Self
where Self: DerefMut<Target = T> + Deref, T: ?Sized,

Mutable access to the Deref::Target of a value. Read more
§

fn tap_dbg(self, func: impl FnOnce(&Self)) -> Self

Calls .tap() only in debug builds, and is erased in release builds.
§

fn tap_mut_dbg(self, func: impl FnOnce(&mut Self)) -> Self

Calls .tap_mut() only in debug builds, and is erased in release builds.
§

fn tap_borrow_dbg<B>(self, func: impl FnOnce(&B)) -> Self
where Self: Borrow<B>, B: ?Sized,

Calls .tap_borrow() only in debug builds, and is erased in release builds.
§

fn tap_borrow_mut_dbg<B>(self, func: impl FnOnce(&mut B)) -> Self
where Self: BorrowMut<B>, B: ?Sized,

Calls .tap_borrow_mut() only in debug builds, and is erased in release builds.
§

fn tap_ref_dbg<R>(self, func: impl FnOnce(&R)) -> Self
where Self: AsRef<R>, R: ?Sized,

Calls .tap_ref() only in debug builds, and is erased in release builds.
§

fn tap_ref_mut_dbg<R>(self, func: impl FnOnce(&mut R)) -> Self
where Self: AsMut<R>, R: ?Sized,

Calls .tap_ref_mut() only in debug builds, and is erased in release builds.
§

fn tap_deref_dbg<T>(self, func: impl FnOnce(&T)) -> Self
where Self: Deref<Target = T>, T: ?Sized,

Calls .tap_deref() only in debug builds, and is erased in release builds.
§

fn tap_deref_mut_dbg<T>(self, func: impl FnOnce(&mut T)) -> Self
where Self: DerefMut<Target = T> + Deref, T: ?Sized,

Calls .tap_deref_mut() only in debug builds, and is erased in release builds.
§

impl<T> TryConv for T

§

fn try_conv<T>(self) -> Result<T, Self::Error>
where Self: TryInto<T>,

Attempts to convert self into T using TryInto<T>. Read more
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>