Trait NonNullPtrRef 

pub unsafe trait NonNullPtrRef<'a>: NonNullPtr {
    type Ref: 'a;
    type RefPermission: Inv;

    // Required methods
    spec fn ref_perm_view_permission(perm: Self::RefPermission) -> Self::Permission;
    spec fn ref_rel_perm(r: Self::Ref, perm: Self::RefPermission) -> bool;
    proof fn lemma_ref_perm_inv_impl_perm_inv(perm: Self::RefPermission);
    proof fn borrow_ref_perm(tracked perm: &Self::RefPermission) -> tracked ret : Self::RefPermission;
    proof fn borrow_perm_as_ref_perm(
        tracked perm: &'a Self::Permission,
    ) -> tracked ret : Self::RefPermission;
    unsafe fn raw_as_ref(
        raw: NonNull<Self::Target>,
        perm: Tracked<Self::RefPermission>,
    ) -> Self::Ref;
    exec fn ref_as_raw(
        ptr_ref: Self::Ref,
    ) -> (NonNull<Self::Target>, Tracked<Self::RefPermission>);
}

The trait for the associated Ref type of NonNullPtr, which is separated from the NonNullPtr trait. FIXME: This is a workaround for the lack of GAT with lifetime in Verus. We can merge this trait back to NonNullPtr once it is supported.

Required Associated Types

type Ref: 'a

type RefPermission: Inv

A verification-only permission type that represents the reading permission of the memory managed by the pointer.

Required Methods

spec fn ref_perm_view_permission(perm: Self::RefPermission) -> Self::Permission

The RefPermission must be able to be viewed as the owned Permission.

spec fn ref_rel_perm(r: Self::Ref, perm: Self::RefPermission) -> bool

A specification function that relates the Ref type and the RefPermission.

proof fn lemma_ref_perm_inv_impl_perm_inv(perm: Self::RefPermission)

requires

perm.inv(),

ensures

Self::ref_perm_view_permission(perm).inv(),

The RefPermission must present the invariant of the Permission.

proof fn borrow_ref_perm(tracked perm: &Self::RefPermission) -> tracked ret : Self::RefPermission

requires

perm.inv(),

ensures

ret.inv(),

Self::ref_perm_view_permission(ret) == Self::ref_perm_view_permission(*perm),

Borrows a reusable reading permission from an existing reading permission.

proof fn borrow_perm_as_ref_perm(tracked perm: &'a Self::Permission) -> tracked ret : Self::RefPermission

requires

perm.inv(),

ensures

ret.inv(),

Self::ref_perm_view_permission(ret) == *perm,

Borrows a reusable reading permission from the owned permission.

unsafe exec fn raw_as_ref( raw: NonNull<Self::Target>, perm: Tracked<Self::RefPermission>, ) -> ret : Self::Ref

requires

Self::ptr_perm_match(raw.view_ptr_mut(), Self::ref_perm_view_permission(perm@)),

perm@.inv(),

ensures

Self::ref_rel_perm(ret, perm@),

Obtains a shared reference to the original pointer.

Safety

The original pointer must outlive the lifetime parameter 'a, and during 'a no mutable references to the pointer will exist.

exec fn ref_as_raw( ptr_ref: Self::Ref, ) -> (NonNull<Self::Target>, Tracked<Self::RefPermission>)

ensures

Self::ref_rel_perm(ptr_ref, perm@),

Self::ptr_perm_match(res_ptr.view_ptr_mut(), Self::ref_perm_view_permission(perm@)),

perm@.inv(),

res_ptr.view_ptr_mut().addr() % (1usize << Self::ALIGN_BITS) == 0,

Converts a shared reference to a raw pointer.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementations on Foreign Types

impl<'a, T: 'static> NonNullPtrRef<'a> for Arc<T>

open spec fn ref_perm_view_permission(perm: Self::RefPermission) -> Self::Permission

{ perm }

open spec fn ref_rel_perm(r: Self::Ref, perm: Self::RefPermission) -> bool

{ perm.view_target() == *r@ }

proof fn lemma_ref_perm_inv_impl_perm_inv(perm: Self::RefPermission)

proof fn borrow_ref_perm(tracked perm: &Self::RefPermission) -> tracked ret : Self::RefPermission

proof fn borrow_perm_as_ref_perm(tracked perm: &'a Self::Permission) -> tracked ret : Self::RefPermission

unsafe exec fn raw_as_ref( raw: NonNull<Self::Target>, perm: Tracked<Self::RefPermission>, ) -> Self::Ref

exec fn ref_as_raw( ptr_ref: Self::Ref, ) -> (NonNull<Self::Target>, Tracked<Self::RefPermission>)

type Ref = ArcRef<'a, T>

type RefPermission = ArcPointsTo<T>

impl<'a, T: 'static> NonNullPtrRef<'a> for Box<T>

open spec fn ref_perm_view_permission(perm: Self::RefPermission) -> Self::Permission

{ perm@ }

open spec fn ref_rel_perm(r: Self::Ref, perm: Self::RefPermission) -> bool

{
    &&& r.value() == perm@.value()
    &&& r.ptr() == perm@.ptr()

}

proof fn lemma_ref_perm_inv_impl_perm_inv(perm: Self::RefPermission)

proof fn borrow_ref_perm(tracked perm: &Self::RefPermission) -> tracked ret : Self::RefPermission

proof fn borrow_perm_as_ref_perm(tracked perm: &'a Self::Permission) -> tracked ret : Self::RefPermission

unsafe exec fn raw_as_ref( raw: NonNull<Self::Target>, perm: Tracked<Self::RefPermission>, ) -> Self::Ref

exec fn ref_as_raw( ptr_ref: Self::Ref, ) -> (NonNull<Self::Target>, Tracked<Self::RefPermission>)

type Ref = BoxRef<'a, T>

type RefPermission = BoxPointsToRef<'a, T>

Implementors

impl<'a, L: NonNullPtrRef<'a>, R: NonNullPtrRef<'a>> NonNullPtrRef<'a> for Either<L, R>

type Ref = Either<<L as NonNullPtrRef<'a>>::Ref, <R as NonNullPtrRef<'a>>::Ref>

type RefPermission = Sum<<L as NonNullPtrRef<'a>>::RefPermission, <R as NonNullPtrRef<'a>>::RefPermission>