Out of scope, this work is purely about semantic correctness.

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)