Announcing Isabelle support for SAW

Summary

We’re excited to announce that SAW now supports generating Isabelle theories from Cryptol specifications – a new capability developed by Galois in collaboration with Apple. Cryptol and SAW offer a simple, usable, semi-automated path towards creating, analyzing, and verifying cryptographic protocols, but with limitations on what can be automatically proven. Interactive theorem provers (ITPs) like Isabelle are far more expressive, but are complex and have a steep learning curve. SAW’s new ability to generate Isabelle theories from Cryptol offers the best of both worlds: combining SAW and Cryptol’s usability with Isabelle’s expressivity [1].You can see these new capabilities in action with Apple’s recent release, or check out the GitHub release page.Included in the latest development version is:a new SAW command: write_isabelle_cryptol_modules (requires enable_experimental)a new SAW tactic: offline_isabelle (requires enable_experimental)a separate cryptol-to-isabelle executable for independently translating Cryptol modules into Isabellea prelude Isabelle theory, implementing the Cryptol primitivescode generator and quickcheck support for Cryptol primitivesa library of supporting Isabelle theories for reasoning about Cryptol specificationsWhat is supported:all Cryptol built-in operations, types and classes, excluding infinite streamstype signature constraints, deferring complex constraints as proof obligations Cryptol records, represented as Isabelle recordsmutually-recursive Cryptol functions via user-supplied termination proofstype-level arithmetic, with implicit coercion between values of logically-equivalent typesWhat is not (yet) supported:arbitrary SAWCore terms – the source must be either a Cryptol module or a simple SAWCore term comprising defined Cryptol functions and primitivesinf type – all bitvectors must have concrete length, or constrained to be finitenewtypes are translated into type aliases, rather than distinct typessubmodulesforeign function callsExamp...