pub fn fence_acqrel(acq_view: Ghost<AcquireSyncView>) -> Ghost<ReleaseSyncView>
ensures
acq_view@ == result@