[nanolith]

The formal methods nerd in me is happy to see HOL Light being used to formally verify this implementation. I'm curious to see how closely their abstract machine models follow specific machine implementations. OOO, speculation, and deep pipelining have non-trivial impacts on potential side channels, and these vary quite a bit by stepping and architecture.

[holowoodman]

Even worse: Each new CPU generation will need a new machine model and a reevaluation. Because OOO, speculation and all the timing behaviour are non-functional properties that frequently change due to new optimizations, different internal structuring, etc.