ostd::specs::mm::frame::linked_list::linked_list_owners

Struct LinkedListOwner

pub struct LinkedListOwner<M: AnyFrameMeta + Repr<MetaSlotSmall>> {
    pub list: Seq<LinkOwner>,
    pub list_id: u64,
    pub _marker: PhantomData<M>,
}

Fields§

§list: Seq<LinkOwner>§list_id: u64§_marker: PhantomData<M>

Implementations§

Source §

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedListOwner<M>

Source

pub open spec fn inv_at(self, i: int) -> bool

{
    &&& self.list[i].inv()
    &&& self.list[i].in_list == self.list_id

}

Per-link structural invariant: the link’s own inv() holds and its in_list tag matches the list’s list_id. The per-link metadata facts (perm wf/is_init/pointer wiring) are tracked via relate_region_at against the global MetaRegionOwners, NOT through this predicate.

Source

pub open spec fn slot_index_at(self, i: int) -> usize

{ frame_to_index(meta_to_frame_spec(self.list[i].paddr)) }

The region slot index keyed by the i-th link’s meta-slot address.

Source

pub open spec fn meta_perm_of( self, regions: MetaRegionOwners, i: int, ) -> PointsTo<MetaSlot, Metadata<Link<M>>>

{
    let idx = self.slot_index_at(i);
    vstd_extra::cast_ptr::PointsTo::new_spec(
        regions.slots[idx],
        regions.slot_owners[idx].inner_perms,
    )
}

The typed permission for the i-th link, reconstructed from the region: the outer pointer-perm regions.slots[idx] paired with the inner perms regions.slot_owners[idx].inner_perms.

Source

pub open spec fn relate_region_at(self, regions: MetaRegionOwners, i: int) -> bool

{
    let idx = self.slot_index_at(i);
    let perm = self.meta_perm_of(regions, i);
    &&& regions.slots.contains_key(idx)
    &&& regions.slot_owners.contains_key(idx)
    &&& perm.addr() == self.list[i].paddr
    &&& perm.points_to.addr() == self.list[i].paddr
    &&& perm.inner_perms.ref_count.value() == REF_COUNT_UNIQUE
    &&& perm.wf(&perm.inner_perms)
    &&& perm.addr() % META_SLOT_SIZE == 0
    &&& FRAME_METADATA_RANGE.start <= perm.addr()
        < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
    &&& perm.is_init()
    &&& perm.value().metadata.wf(self.list[i])
    &&& i == 0 <==> perm.value().metadata.prev is None
    &&& i == self.list.len() - 1 <==> perm.value().metadata.next is None
    &&& 0 < i
        ==> {
            &&& perm.value().metadata.prev is Some
            &&& perm.value().metadata.prev.unwrap().addr()
                == self.meta_perm_of(regions, i - 1).addr()
            &&& perm.value().metadata.prev.unwrap().ptr
                == self.meta_perm_of(regions, i - 1).points_to.pptr()

        }
    &&& i < self.list.len() - 1
        ==> {
            &&& perm.value().metadata.next is Some
            &&& perm.value().metadata.next.unwrap().addr()
                == self.meta_perm_of(regions, i + 1).addr()
            &&& perm.value().metadata.next.unwrap().ptr
                == self.meta_perm_of(regions, i + 1).points_to.pptr()

        }
    &&& self.list[i].inv()
    &&& self.list[i].in_list == self.list_id

}

The per-link invariant expressed over the region permission (meta_perm_of) rather than the list’s owned perms[i]. This is the inv_at analog that connects each list element to its region slot, so accessors can reason about the link’s metadata without bringing the list’s perms[i] into scope (which would conflict — two permissions at the same address).

Source

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

{
    &&& forall |i: int| 0 <= i < self.list.len() ==> self.relate_region_at(regions, i)
    &&& forall |i: int, j: int| {
        0 <= i < self.list.len() && 0 <= j < self.list.len() && i != j
            ==> self.slot_index_at(i) != self.slot_index_at(j)
    }
    &&& self.list.len() > 0 ==> self.list_id != 0

}

The list-wide region relation: every link satisfies relate_region_at, and distinct list positions map to distinct region slot indices (so a frame appears at most once — required by the borrow model, where link edits mutate regions.slots[slot_index_at(i)] and must not alias).

Source

pub proof fn length_le_max_meta_slots(self, regions: MetaRegionOwners)

requires

self.relate_region(regions),

regions.inv(),

ensures

self.list.len() <= max_meta_slots(),

Pigeonhole bound: the list is no longer than the number of meta slots. Each link occupies a region slot (relate_region_at ⟹ slots.contains_key(slot_index_at(i)), and regions.inv() ⟹ slot_index_at(i) < max_meta_slots()), and distinct positions occupy distinct slots (relate_region’s injectivity). So the positions inject into [0, max_meta_slots()) and the length is capped by it.

Source

pub proof fn length_lt_usize_max(self, regions: MetaRegionOwners)

requires

self.relate_region(regions),

regions.inv(),

ensures

self.list.len() < usize::MAX,

The list counter can never saturate: its length is capped by max_meta_slots() (see Self::length_le_max_meta_slots), which is far below usize::MAX. Lets insert_before discharge the size + 1 overflow check without a caller-supplied non-fullness precondition.

Source

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

requires

self.relate_region_at(regions, i),

ensures

({
    let idx = self.slot_index_at(i);
    let perm = self.meta_perm_of(regions, i);
    &&& regions.slots.contains_key(idx)
    &&& regions.slot_owners.contains_key(idx)
    &&& perm.addr() == self.list[i].paddr
    &&& perm.points_to.addr() == self.list[i].paddr
    &&& perm.inner_perms.ref_count.value() == REF_COUNT_UNIQUE
    &&& perm.wf(&perm.inner_perms)
    &&& perm.addr() % META_SLOT_SIZE == 0
    &&& FRAME_METADATA_RANGE.start <= perm.addr()
        < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
    &&& perm.is_init()
    &&& perm.value().metadata.wf(self.list[i])
    &&& (i == 0 <==> perm.value().metadata.prev is None)
    &&& (i == self.list.len() - 1 <==> perm.value().metadata.next is None)
    &&& (0 < i
        ==> {
            &&& perm.value().metadata.prev is Some
            &&& perm.value().metadata.prev.unwrap().addr()
                == self.meta_perm_of(regions, i - 1).addr()
            &&& perm.value().metadata.prev.unwrap().ptr
                == self.meta_perm_of(regions, i - 1).points_to.pptr()

        })
    &&& (i < self.list.len() - 1
        ==> {
            &&& perm.value().metadata.next is Some
            &&& perm.value().metadata.next.unwrap().addr()
                == self.meta_perm_of(regions, i + 1).addr()
            &&& perm.value().metadata.next.unwrap().ptr
                == self.meta_perm_of(regions, i + 1).points_to.pptr()

        })
    &&& self.list[i].inv()
    &&& self.list[i].in_list == self.list_id

}),

Unfolds the opaque relate_region_at ONCE and exposes its clauses. relate_region_at is opaque to avoid meta_perm_of quantifier explosion at use sites; this lemma localizes the reveal so callers get the facts at a single index without re-exploding the SMT context.

Source

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

requires

({
    let idx = self.slot_index_at(i);
    let perm = self.meta_perm_of(regions, i);
    &&& regions.slots.contains_key(idx)
    &&& regions.slot_owners.contains_key(idx)
    &&& perm.addr() == self.list[i].paddr
    &&& perm.points_to.addr() == self.list[i].paddr
    &&& perm.inner_perms.ref_count.value() == REF_COUNT_UNIQUE
    &&& perm.wf(&perm.inner_perms)
    &&& perm.addr() % META_SLOT_SIZE == 0
    &&& FRAME_METADATA_RANGE.start <= perm.addr()
        < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
    &&& perm.is_init()
    &&& perm.value().metadata.wf(self.list[i])
    &&& (i == 0 <==> perm.value().metadata.prev is None)
    &&& (i == self.list.len() - 1 <==> perm.value().metadata.next is None)
    &&& (0 < i
        ==> {
            &&& perm.value().metadata.prev is Some
            &&& perm.value().metadata.prev.unwrap().addr()
                == self.meta_perm_of(regions, i - 1).addr()
            &&& perm.value().metadata.prev.unwrap().ptr
                == self.meta_perm_of(regions, i - 1).points_to.pptr()

        })
    &&& (i < self.list.len() - 1
        ==> {
            &&& perm.value().metadata.next is Some
            &&& perm.value().metadata.next.unwrap().addr()
                == self.meta_perm_of(regions, i + 1).addr()
            &&& perm.value().metadata.next.unwrap().ptr
                == self.meta_perm_of(regions, i + 1).points_to.pptr()

        })
    &&& self.list[i].inv()
    &&& self.list[i].in_list == self.list_id

}),

ensures

self.relate_region_at(regions, i),

Constructor (inverse of [relate_region_at_facts]): establishes the opaque relate_region_at from its unfolded clauses. Used by the pop/ insert “surgery” proofs, which assemble each clause for the new list and then fold them back into the opaque predicate.

Source

pub proof fn relate_region_preserved_external_change( self, regions1: MetaRegionOwners, regions2: MetaRegionOwners, )

requires

self.relate_region(regions1),

regions2.slots == regions1.slots,

forall |i: int| {
    0 <= i < self.list.len()
        ==> {
            let idx = self.slot_index_at(i);
            &&& regions2.slot_owners.contains_key(idx)
            &&& regions2.slot_owners[idx] == regions1.slot_owners[idx]

        }
},

ensures

self.relate_region(regions2),

relate_region is preserved under a region change that doesn’t touch any of the list’s slots. Used by LinkedList::drop’s loop body: after take_current pops position 0, the popped slot is dropped via frame.drop, which only modifies regions.slot_owners[cur_idx] and leaves regions.slots fully untouched. Since the cursor’s remaining list never contains cur_idx (distinctness on the original list), relate_region carries through.

Source

pub proof fn pop_preserves_relate_region( old: LinkedListOwner<M>, r0: MetaRegionOwners, new: LinkedListOwner<M>, fr: MetaRegionOwners, n: int, )

requires

0 <= n < old.list.len(),

old.relate_region(r0),

new.list == old.list.remove(n),

new.list_id == old.list_id,

forall |p: int| {
    (0 <= p < old.list.len() && p != n)
        ==> ({
            let i = old.slot_index_at(p);
            let fp = vstd_extra::cast_ptr::PointsTo::<
                MetaSlot,
                Metadata<Link<M>>,
            >::new_spec(fr.slots[i], fr.slot_owners[i].inner_perms);
            &&& fr.slots.contains_key(i)
            &&& fr.slot_owners.contains_key(i)
            &&& fp.addr() == old.list[p].paddr
            &&& fp.points_to.addr() == old.list[p].paddr
            &&& fp.points_to.pptr() == r0.slots[i].pptr()
            &&& fp.inner_perms.ref_count.value() == REF_COUNT_UNIQUE
            &&& fp.wf(&fp.inner_perms)
            &&& fp.addr() % META_SLOT_SIZE == 0
            &&& FRAME_METADATA_RANGE.start <= fp.addr()
                < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
            &&& fp.is_init()
            &&& (p == n - 1
                ==> fp.value().metadata.next
                    == old.meta_perm_of(r0, n).value().metadata.next)
            &&& (p != n - 1
                ==> fp.value().metadata.next
                    == old.meta_perm_of(r0, p).value().metadata.next)
            &&& (p == n + 1
                ==> fp.value().metadata.prev
                    == old.meta_perm_of(r0, n).value().metadata.prev)
            &&& (p != n + 1
                ==> fp.value().metadata.prev
                    == old.meta_perm_of(r0, p).value().metadata.prev)

        })
},

ensures

new.relate_region(fr),

The list-rewiring “surgery” for popping the element at index n: given the entry invariant old.relate_region(r0) and a characterization of the post-pop region fr (every surviving slot keeps its local facts and pointers, except the two neighbors whose next/prev were rewired to bridge the gap), the shrunk list new satisfies relate_region(fr).

New position k maps to old position p = (k < n ? k : k+1); the neighbor of k maps to p ± 1 except across the cut (new position n-1 reaches old n+1, new position n reaches old n-1), which is exactly where the body rewired the link pointers.

Source

pub proof fn insert_preserves_relate_region( old: LinkedListOwner<M>, r0: MetaRegionOwners, new: LinkedListOwner<M>, fr: MetaRegionOwners, n: int, link: LinkOwner, )

requires

0 <= n <= old.list.len(),

old.relate_region(r0),

new.list == old.list.insert(n, link),

new.list_id != 0,

old.list.len() > 0 ==> new.list_id == old.list_id,

link.in_list == new.list_id,

forall |p: int| {
    (0 <= p < old.list.len()) ==> old.slot_index_at(p) != new.slot_index_at(n)
},

({
    let ins = new.slot_index_at(n);
    let fpn = vstd_extra::cast_ptr::PointsTo::<
        MetaSlot,
        Metadata<Link<M>>,
    >::new_spec(fr.slots[ins], fr.slot_owners[ins].inner_perms);
    &&& fr.slots.contains_key(ins)
    &&& fr.slot_owners.contains_key(ins)
    &&& fpn.addr() == link.paddr
    &&& fpn.points_to.addr() == link.paddr
    &&& fpn.inner_perms.ref_count.value() == REF_COUNT_UNIQUE
    &&& fpn.wf(&fpn.inner_perms)
    &&& fpn.addr() % META_SLOT_SIZE == 0
    &&& FRAME_METADATA_RANGE.start <= fpn.addr()
        < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
    &&& fpn.is_init()
    &&& (n == 0 <==> fpn.value().metadata.prev is None)
    &&& (n == old.list.len() <==> fpn.value().metadata.next is None)
    &&& (n > 0
        ==> {
            &&& fpn.value().metadata.prev is Some
            &&& fpn.value().metadata.prev.unwrap().addr() == old.list[n - 1].paddr
            &&& fpn.value().metadata.prev.unwrap().ptr
                == r0.slots[old.slot_index_at(n - 1)].pptr()

        })
    &&& (n < old.list.len()
        ==> {
            &&& fpn.value().metadata.next is Some
            &&& fpn.value().metadata.next.unwrap().addr() == old.list[n].paddr
            &&& fpn.value().metadata.next.unwrap().ptr
                == r0.slots[old.slot_index_at(n)].pptr()

        })

}),

forall |p: int| {
    (0 <= p < old.list.len())
        ==> ({
            let i = old.slot_index_at(p);
            let ins = new.slot_index_at(n);
            let fp = vstd_extra::cast_ptr::PointsTo::<
                MetaSlot,
                Metadata<Link<M>>,
            >::new_spec(fr.slots[i], fr.slot_owners[i].inner_perms);
            &&& fr.slots.contains_key(i)
            &&& fr.slot_owners.contains_key(i)
            &&& fp.addr() == old.list[p].paddr
            &&& fp.points_to.addr() == old.list[p].paddr
            &&& fp.points_to.pptr() == r0.slots[i].pptr()
            &&& fp.inner_perms.ref_count.value() == REF_COUNT_UNIQUE
            &&& fp.wf(&fp.inner_perms)
            &&& fp.addr() % META_SLOT_SIZE == 0
            &&& FRAME_METADATA_RANGE.start <= fp.addr()
                < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE
            &&& fp.is_init()
            &&& (p == n - 1
                ==> {
                    &&& fp.value().metadata.next is Some
                    &&& fp.value().metadata.next.unwrap().addr() == link.paddr
                    &&& fp.value().metadata.next.unwrap().ptr == fr.slots[ins].pptr()

                })
            &&& (p != n - 1
                ==> fp.value().metadata.next
                    == old.meta_perm_of(r0, p).value().metadata.next)
            &&& (p == n
                ==> {
                    &&& fp.value().metadata.prev is Some
                    &&& fp.value().metadata.prev.unwrap().addr() == link.paddr
                    &&& fp.value().metadata.prev.unwrap().ptr == fr.slots[ins].pptr()

                })
            &&& (p != n
                ==> fp.value().metadata.prev
                    == old.meta_perm_of(r0, p).value().metadata.prev)

        })
},

ensures

new.relate_region(fr),

The list-rewiring “surgery” for inserting link before index n (0 <= n <= old.list.len()): given the entry relate_region and a per-slot characterization of the post-insert region fr, the longer list new = old.list.insert(n, link) satisfies relate_region(fr).

New position k maps to old position k (k<n), is the inserted link (k==n), or maps to old k-1 (k>n). The inserted link sits at slot ins = new.slot_index_at(n); its prev/next point to old n-1/n (or None at the ends), and old n-1’s next / old n’s prev are rewired to point at the inserted link. Mirror of [pop_preserves_relate_region].

Source

pub open spec fn view_helper(owners: Seq<LinkOwner>) -> Seq<LinkModel>

{
    if owners.len() == 0 {
        Seq::<LinkModel>::empty()
    } else {
        seq![owners[0].view()].add(Self::view_helper(owners.remove(0)))
    }
}

Source

pub proof fn view_preserves_len(owners: Seq<LinkOwner>)

ensures

Self::view_helper(owners).len() == owners.len(),

Source

pub proof fn view_helper_index(owners: Seq<LinkOwner>, i: int)

requires

0 <= i < owners.len(),

ensures

Self::view_helper(owners)[i] == owners[i].view(),

Proves that view_helper preserves indexing: view_helper(s)[i] == s[i].view()

Source

pub proof fn view_helper_remove(owners: Seq<LinkOwner>, i: int)

requires

0 <= i < owners.len(),

ensures

Self::view_helper(owners.remove(i)) =~= Self::view_helper(owners).remove(i),

Proves that view_helper commutes with remove: view_helper(s.remove(i)) =~= view_helper(s).remove(i)

Source

pub proof fn view_helper_insert(owners: Seq<LinkOwner>, i: int, v: LinkOwner)

requires

0 <= i <= owners.len(),

ensures

Self::view_helper(owners.insert(i, v)) =~= Self::view_helper(owners).insert(i, v.view()),

Proves that view_helper commutes with insert: view_helper(s.insert(i, v)) =~= view_helper(s).insert(i, v.view())

Source §

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedListOwner<M>

Source

pub proof fn tracked_take(tracked owner: &mut Self) -> tracked res : Self

ensures

res == *old(owner),

final(owner).list =~= Seq::<LinkOwner>::empty(),

final(owner).inv(),

Take ownership of *owner by swapping it with a fresh empty LinkedListOwner. The resulting “leftover” *owner has an empty list, so its inv() holds vacuously. Used by drop-style call sites that need to feed an owned LinkedListOwner to a downstream API while themselves only having a &mut to it.

Source

pub proof fn tracked_destroy_empty(tracked self)

requires

self.list =~= Seq::<LinkOwner>::empty(),

Discard a logically-empty LinkedListOwner. Sound because such an owner has an empty list and claims no external permissions (the borrow model parks all permissions in MetaRegionOwners).

Trait Implementations§

Source §

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Inv for LinkedListOwner<M>

Source §

open spec fn inv(self) -> bool

{
    &&& self.list_id != 0
    &&& forall |i: int| 0 <= i < self.list.len() ==> self.inv_at(i)

}

Source §

open spec fn view(&self) -> Self::V

{
    LinkedListModel {
        list: Self::view_helper(self.list),
    }
}

Source §

type V = LinkedListModel

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 LinkedListOwner Copy item path

Fields§

Implementations§

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedListOwner<M>

pub open spec fn inv_at(self, i: int) -> bool

pub open spec fn slot_index_at(self, i: int) -> usize

pub open spec fn meta_perm_of( self, regions: MetaRegionOwners, i: int, ) -> PointsTo<MetaSlot, Metadata<Link<M>>>

pub open spec fn relate_region_at(self, regions: MetaRegionOwners, i: int) -> bool

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

pub proof fn length_le_max_meta_slots(self, regions: MetaRegionOwners)

pub proof fn length_lt_usize_max(self, regions: MetaRegionOwners)

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

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

pub proof fn relate_region_preserved_external_change( self, regions1: MetaRegionOwners, regions2: MetaRegionOwners, )

pub proof fn pop_preserves_relate_region( old: LinkedListOwner<M>, r0: MetaRegionOwners, new: LinkedListOwner<M>, fr: MetaRegionOwners, n: int, )

pub proof fn insert_preserves_relate_region( old: LinkedListOwner<M>, r0: MetaRegionOwners, new: LinkedListOwner<M>, fr: MetaRegionOwners, n: int, link: LinkOwner, )

pub open spec fn view_helper(owners: Seq<LinkOwner>) -> Seq<LinkModel>

pub proof fn view_preserves_len(owners: Seq<LinkOwner>)

pub proof fn view_helper_index(owners: Seq<LinkOwner>, i: int)

pub proof fn view_helper_remove(owners: Seq<LinkOwner>, i: int)

pub proof fn view_helper_insert(owners: Seq<LinkOwner>, i: int, v: LinkOwner)

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedListOwner<M>

pub proof fn tracked_take(tracked owner: &mut Self) -> tracked res : Self

pub proof fn tracked_destroy_empty(tracked self)

Trait Implementations§

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Inv for LinkedListOwner<M>

open spec fn inv(self) -> bool

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> InvView for LinkedListOwner<M>

proof fn view_preserves_inv(self)

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> View for LinkedListOwner<M>

open spec fn view(&self) -> Self::V

type V = LinkedListModel

Auto Trait Implementations§

impl<M> Freeze for LinkedListOwner<M>

impl<M> RefUnwindSafe for LinkedListOwner<M>where M: RefUnwindSafe,

impl<M> Send for LinkedListOwner<M>where M: Send,

impl<M> Sync for LinkedListOwner<M>where M: Sync,

impl<M> Unpin for LinkedListOwner<M>where M: Unpin,

impl<M> UnsafeUnpin for LinkedListOwner<M>

impl<M> UnwindSafe for LinkedListOwner<M>where M: 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

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

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__Awhere 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 Twhere 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 Awhere A: ?Sized,

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

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

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

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

Struct LinkedListOwner

impl<M> RefUnwindSafe for LinkedListOwner<M>
where M: RefUnwindSafe,

impl<M> Send for LinkedListOwner<M>
where M: Send,

impl<M> Sync for LinkedListOwner<M>
where M: Sync,

impl<M> Unpin for LinkedListOwner<M>
where M: Unpin,

impl<M> UnwindSafe for LinkedListOwner<M>
where M: 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>,

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,