For anyone interested, here is another paper concerning similar topics:

`Verification of a Cryptographic Primitive: SHA-256',

https://www.cs.princeton.edu/~appel/papers/verif-sha.pdf.

And don't forget about `CompCert C compiler',

http://compcert.inria.fr/compcert-C.html.

Or the `Vellvm' project,

http://www.cis.upenn.edu/~stevez/vellvm/.