pub broadcast proof fn axiom_cast_spec_eq<T: PointeeSized, U>(ptr: NonNull<T>)Expand description
ensures
(#[trigger] ptr.cast_spec::<U>()).view_ptr_mut() == ptr.view_ptr_mut() as *mut U,The semantic of casting a NonNull<T> should be the same as casting the underlying raw pointer
(including the address, metadata, and provenance).