Provably secure compilation of side-channel countermeasures

Source of the Coq development is here