pub fn fence_release(sync_view: Ghost<SyncView>) -> Ghost<ReleaseSyncView>
ensures
*sync_view == result@