This is a Cryptol specification of the SIMON and SPECK lightweight block ciphers, based on the June 19, 2013 Report.

This specification is proven correct using Cryptol's :prove command. See my blog post for more information:

https://galois.com/blog/2013/06/simon-and-speck-in-cryptol/