pub enum Either<L, R> {
Left(L),
Right(R),
}Variants§
Implementations§
Source§impl<L, R> Either<L, R>
impl<L, R> Either<L, R>
pub fn __VERUS_SPEC_left(self) -> Option<L>
pub fn __VERUS_SPEC_right(self) -> Option<R>
pub fn __VERUS_SPEC_is_left(&self) -> bool
pub fn __VERUS_SPEC_is_right(&self) -> bool
Trait Implementations§
Source§impl<L: NonNullPtr, R: NonNullPtr> NonNullPtr for Either<L, R>
impl<L: NonNullPtr, R: NonNullPtr> NonNullPtr for Either<L, R>
Source§unsafe exec fn from_raw(
ptr: NonNull<Self::Target>,
verus_tmp_perm: Tracked<Self::Permission>,
) -> Self
unsafe exec fn from_raw( ptr: NonNull<Self::Target>, verus_tmp_perm: Tracked<Self::Permission>, ) -> Self
Source§open spec fn ptr_perm_match(ptr: NonNull<Self::Target>, perm: Self::Permission) -> bool
open spec fn ptr_perm_match(ptr: NonNull<Self::Target>, perm: Self::Permission) -> bool
{
let tag = 1usize << Self::ALIGN_BITS;
match perm {
Sum::Left(left) => (
&&& ptr.view_ptr_mut().addr() & tag == 0
&&& L::ptr_perm_match(ptr.cast(), left)
),
Sum::Right(right) => {
let untagged_ptr = ptr
.view_ptr_mut()
.with_addr((ptr.view_ptr_mut().addr() & !tag));
let right_nonnull = nonnull_from_ptr_mut_spec(untagged_ptr);
&&& ptr.view_ptr_mut().addr() & tag == tag
&&& (ptr.view_ptr_mut().addr() & !tag) != 0
&&& R::ptr_perm_match(right_nonnull.cast(), right)
}
}
}Source§open spec fn rel_perm(self, perm: Self::Permission) -> bool
open spec fn rel_perm(self, perm: Self::Permission) -> bool
{
match (self, perm) {
(Either::Left(left), Sum::Left(left_perm)) => left.rel_perm(left_perm),
(Either::Right(right), Sum::Right(right_perm)) => right.rel_perm(right_perm),
_ => false,
}
}Source§proof fn lemma_align_bits_range()
proof fn lemma_align_bits_range()
ensures
Self::ALIGN_BITS
== if L::ALIGN_BITS < R::ALIGN_BITS { L::ALIGN_BITS - 1 } else { R::ALIGN_BITS - 1 },Source§const ALIGN_BITS: u32
const ALIGN_BITS: u32
The power of two of the pointer alignment.
Source§type Target = PhantomData<Either<L, R>>
type Target = PhantomData<Either<L, R>>
The target type that this pointer refers to.
Source§type Permission = Sum<<L as NonNullPtr>::Permission, <R as NonNullPtr>::Permission>
type Permission = Sum<<L as NonNullPtr>::Permission, <R as NonNullPtr>::Permission>
A verification-only permission type that represents the ownership of the memory managed by the pointer.
Source§impl<'a, L: NonNullPtrRef<'a>, R: NonNullPtrRef<'a>> NonNullPtrRef<'a> for Either<L, R>
impl<'a, L: NonNullPtrRef<'a>, R: NonNullPtrRef<'a>> NonNullPtrRef<'a> for Either<L, R>
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
{
match perm {
Sum::Left(left) => Sum::Left(L::ref_perm_view_permission(left)),
Sum::Right(right) => Sum::Right(R::ref_perm_view_permission(right)),
}
}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
{ true }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>,
verus_tmp_perm: Tracked<Self::RefPermission>,
) -> Self::Ref
unsafe exec fn raw_as_ref( raw: NonNull<Self::Target>, verus_tmp_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 = Either<<L as NonNullPtrRef<'a>>::Ref, <R as NonNullPtrRef<'a>>::Ref>
Source§type RefPermission = Sum<<L as NonNullPtrRef<'a>>::RefPermission, <R as NonNullPtrRef<'a>>::RefPermission>
type RefPermission = Sum<<L as NonNullPtrRef<'a>>::RefPermission, <R as NonNullPtrRef<'a>>::RefPermission>
A verification-only permission type that represents the reading permission of the memory managed by the pointer.
impl<L: Copy, R: Copy> Copy for Either<L, R>
impl<L: Eq, R: Eq> Eq for Either<L, R>
impl<L, R> StructuralPartialEq for Either<L, R>
Auto Trait Implementations§
impl<L, R> Freeze for Either<L, R>
impl<L, R> RefUnwindSafe for Either<L, R>where
L: RefUnwindSafe,
R: RefUnwindSafe,
impl<L, R> Send for Either<L, R>
impl<L, R> Sync for Either<L, R>
impl<L, R> Unpin for Either<L, R>
impl<L, R> UnsafeUnpin for Either<L, R>where
L: UnsafeUnpin,
R: UnsafeUnpin,
impl<L, R> UnwindSafe for Either<L, R>where
L: UnwindSafe,
R: UnwindSafe,
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more