We address the problem of preserving non-interference across compiler transformations under speculative semantics. We develop a proof method that ensures the preservation uni- formly across all source programs. The basis of our proof method is a new form of simulation relation. It operates over directives that model the attacker’s control over the micro-architectural state, and it accounts for the fact that the compiler transforma- tion may change the influence of the micro-architectural state on the execution (and hence the di- rectives). Using our proof method, we show the correctness of dead code elimination. When we tried to prove register allocation correct, we identified a previously unknown weak- ness that introduces violations to non-interference. We have confirmed the weakness for a mainstream compiler on code from the libsodium cryptographic library. To reclaim security once more, we develop a novel static analysis that operates on a product of source program and register-allocated pro- gram. Using the analysis, we present an automated fix to existing register allocation implementations. We prove the correctness of the fixed register allocations with our proof method.