[GregarianChild]

Yes, so you want to say something like: the CPU doesn't allow additional timing attacks that already exist in software. Making such a relational property formal in a way that is usable in practise is a hard problem.