Formalize Cryptol semantics

[brianhuffman]

This ticket combines the previously separate tickets #42, #43, #45, #46, #55, and #56.

We should write a formal semantics for Cryptol, preferably mechanized in an interactive theorem prover. Ideally this would include operational and denotational semantics. We should also formalize Cryptol's typing rules.

[brianhuffman]

From #45: We have some notes about cryptol semantics on the wiki: CryptolSemantics

[brianhuffman]

From #46, @atomb says:

To some degree, the following two repositories, together, achieve some of this, by providing a direct translation from Cryptol to Coq.

• https://github.com/GaloisInc/cryptol-verifier
• https://github.com/galoisinc/saw-core-coq

[brianhuffman]

A formalized semantics would be particularly useful if we wanted to implement any semantics-preserving program transformations.