  We present an approach for implementing a formally certified loop-invariant
code motion optimization by composing an unrolling pass and a formally
certified yet efficient global subexpression elimination.This approach is
lightweight: each pass comes with a simple and independent proof of
correctness.Experiments show the approach significantly narrows the performance
gap between the CompCert certified compiler and state-of-the-art optimizing
compilers.Our static analysis employs an efficient yet verified hashed set
structure, resulting in fast compilation.
