pub fn fence_acquire(acq_view: Ghost<AcquireSyncView>) -> Ghost<SyncView>
ensures
acq_view@ == *result