Comment by mswphd

In general you don’t need things that fancy. Instead, you can take

1. Some known set of architectures, with

2. Some known set of (constant time/variable time) operations

And then prove things about programs written against those architectures. See for example

https://github.com/PLSysSec/FaCT

That being said, practically the operations that are variable time are known, and are mostly* the same on all modern architectures. In particular

1. Branching on a secret-dependent variable, or

2. Indexing an array with a secret-dependent index, or

3. Some architecture specific operations (typically things like division, occasionally things like multiplications/shifting).