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);
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>);
}Expand description
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
Sourcetype RefPermission: Inv
type RefPermission: Inv
A verification-only permission type that represents the reading permission of the memory managed by the pointer.
Required Methods§
Sourcespec fn ref_perm_view_permission(perm: Self::RefPermission) -> Self::Permission
spec fn ref_perm_view_permission(perm: Self::RefPermission) -> Self::Permission
The RefPermission must be able to be viewed as the owned Permission.
Sourcespec fn ref_rel_perm(r: Self::Ref, perm: Self::RefPermission) -> bool
spec fn ref_rel_perm(r: Self::Ref, perm: Self::RefPermission) -> bool
A specification function that relates the Ref type and the RefPermission.
Sourceproof fn lemma_ref_perm_inv_impl_perm_inv(perm: Self::RefPermission)
proof fn lemma_ref_perm_inv_impl_perm_inv(perm: Self::RefPermission)
perm.inv(),Self::ref_perm_view_permission(perm).inv(),The RefPermission must present the invariant of the Permission.
Sourceunsafe exec fn raw_as_ref(
raw: NonNull<Self::Target>,
perm: Tracked<Self::RefPermission>,
) -> ret : Self::Ref
unsafe exec fn raw_as_ref( raw: NonNull<Self::Target>, perm: Tracked<Self::RefPermission>, ) -> ret : Self::Ref
Self::ptr_perm_match(raw, Self::ref_perm_view_permission(perm@)),perm@.inv(),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.
Sourceexec fn ref_as_raw(
ptr_ref: Self::Ref,
) -> (NonNull<Self::Target>, Tracked<Self::RefPermission>)
exec fn ref_as_raw( ptr_ref: Self::Ref, ) -> (NonNull<Self::Target>, Tracked<Self::RefPermission>)
Self::ref_rel_perm(ptr_ref, perm@),Self::ptr_perm_match(res_ptr, 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", so this trait is not object safe.
Implementations on Foreign Types§
Source§impl<'a, T: 'static> NonNullPtrRef<'a> for Box<T>
impl<'a, T: 'static> NonNullPtrRef<'a> for Box<T>
Source§open spec fn ref_perm_view_permission(perm: Self::RefPermission) -> Self::Permission
open spec fn ref_perm_view_permission(perm: Self::RefPermission) -> Self::Permission
{ perm@ }Source§open spec fn ref_rel_perm(r: Self::Ref, perm: Self::RefPermission) -> bool
open spec fn ref_rel_perm(r: Self::Ref, perm: Self::RefPermission) -> bool
{
&&& r.value() == perm@.value()
&&& r.ptr() == perm@.ptr()
}Source§proof fn lemma_ref_perm_inv_impl_perm_inv(perm: Self::RefPermission)
proof fn lemma_ref_perm_inv_impl_perm_inv(perm: Self::RefPermission)
Source§unsafe exec fn raw_as_ref(
raw: NonNull<Self::Target>,
perm: Tracked<Self::RefPermission>,
) -> Self::Ref
unsafe exec fn raw_as_ref( raw: NonNull<Self::Target>, perm: Tracked<Self::RefPermission>, ) -> Self::Ref
Source§exec fn ref_as_raw(
ptr_ref: Self::Ref,
) -> (NonNull<Self::Target>, Tracked<Self::RefPermission>)
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>
Source§impl<'a, T: 'static> NonNullPtrRef<'a> for Arc<T>
impl<'a, T: 'static> NonNullPtrRef<'a> for Arc<T>
Source§open spec fn ref_perm_view_permission(perm: Self::RefPermission) -> Self::Permission
open spec fn ref_perm_view_permission(perm: Self::RefPermission) -> Self::Permission
{ perm }Source§open spec fn ref_rel_perm(r: Self::Ref, perm: Self::RefPermission) -> bool
open spec fn ref_rel_perm(r: Self::Ref, perm: Self::RefPermission) -> bool
{ perm.view_target() == r@ }