A safety and liveness theory for total reversibility