Formal Replay of Translation Validation for Highly Optimised C

In previous work [6] we have implemented a translation validation mechanism for checking that a C compiler is adhering to the expected semantics of a veried program. We used this apparatus to check the compilation of the seL4 veried operating system kernel [2] by GCC 4.5.1, with some optimisations disabled. We obtained this result by carefully choosing a problem representation that worked well with certain highly optimised SMT solvers. This raises a question of correctness. While we are condent the result is correct, we still aim to replay this result with the most dependable tools available. In this work we present a formalisation of the proof rules needed to replay the translation check within the theorem prover Isabelle/HOL. This is part of an ongoing eort to bring the entire translation validation result within a single trusted proof engine and derive a single correctness theorem. For the moment such a single correctness theorem is our gold standard of trustworthiness. We had hoped to present the formal rule set in action through a worked example. Unfortunately while we have all the theory we need, the mechanisms for selecting and applying the rules and discharging the resulting proof obligations remain a work in progress, and our example proof is incomplete.