What you want is a proof that microarchitectural timing differences (ie. the difference between a cache hit and cache miss) cannot possibly turn into architecturally-visible timing differences. If a program cannot reliably distinguish between two points in time, time is not a suitable channel for programs.
You could have an ISA where timing information is simply not presented to the programmer, but programmers like being able to profile their programs.
You could have an ISA where timing information is simply not presented to the programmer, but programmers like being able to profile their programs.