mutable reference support in raw pointer

[zpzigi754]

In source/vstd/raw_ptr.rs, there is a code snippet for ptr_mut_ref<T>(), which is commented out like the below.

/* coming soon
/// Equivalent to &mut *X, passing in a permission `perm` to ensure safety.
/// The memory pointed to by `ptr` must be initialized.
#[inline(always)]
#[verifier::external_body]
pub fn ptr_mut_ref<T>(ptr: *mut T, Tracked(perm): Tracked<&mut PointsTo<T>>) -> (v: &mut T)
    requires
        old(perm).ptr() == ptr,
        old(perm).is_init()
    ensures
        perm.ptr() == ptr,
        perm.is_init(),

        old(perm).value() == *old(v),
        new(perm).value() == *new(v),
    unsafe { &*ptr }
}
*/

Is there any issue which blocks supporting the mutable reference of raw pointer now?