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.