verify the Cryptol interpreter against the mechanized formal semantics

GaloisInc / cryptol

Cryptol: The Language of Cryptography

https://galoisinc.github.io/cryptol/master/RefMan.html

BSD 3-Clause "New" or "Revised" License

1.14k stars 123 forks source link

verify the Cryptol interpreter against the mechanized formal semantics #44

Open kiniry opened 10 years ago

kiniry commented 10 years ago

See #43 and #42.

brianhuffman commented 4 years ago

Formal verification of the Cryptol interpreter would require a theorem prover for Haskell, which doesn't exist. This is probably not going to happen.

A more attainable goal would be to have some test suites that compare the output of the Cryptol interpreter with an executable version of our Cryptol semantics on a bunch of examples.

atomb commented 3 years ago

The most easily attainable thing to do here would be to set it up so that we could run the test suite thorough both the normal interpreter and the reference interpreter.