Verifying Constant-Time Implementations in a Verified Compilation Toolchain. (Vérification d'implémentations constant-time dans une chaîne de compilation vérifiée).