[DoctorOetker]

in theory a provable lack of timing side channels might be possible to formalize, but it would be a tremendous amount of work (from which we will benefit enormously once we do)