Announcing Isabelle support for SAW

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 Isabelle
• a prelude Isabelle theory, implementing the Cryptol primitives
• code generator and quickcheck support for Cryptol primitives
• a library of supporting Isabelle theories for reasoning about Cryptol specifications

What is supported:

• all Cryptol built-in operations, types and classes, excluding infinite streams
• type signature constraints, deferring complex constraints as proof obligations 
• Cryptol records, represented as Isabelle records
• mutually-recursive Cryptol functions via user-supplied termination proofs
• type-level arithmetic, with implicit coercion between values of logically-equivalent types

What 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 primitives
• inf type – all bitvectors must have concrete length, or constrained to be finite
• newtypes are translated into type aliases, rather than distinct types
• submodules
• foreign function calls

Example Output

cryptol_definition toInt :: "{'n} ((fin 'n) =?> ((['n]) ⇒ Integer))" where
  "toInt x ≡ foldr`{'n,Bit,Integer} (λ(y :: Bit) (b :: Integer). ((if y then 1 else 0 :: Integer) +`{Integer} ((2 :: Integer) *`{Integer} b))) (0 :: Integer) (reverse`{'n,Bit} x)"

‍

Background

Cryptol

Cryptol is a programming language developed by Galois for creating, analyzing, and verifying complex cryptographic algorithms. It provides a simple interface that allows users to easily describe algorithms in the language of mathematics, and to specify and prove properties about them. Cryptol proofs are automated, based on SMT solvers such as Z3, which provides simplicity and usability at the cost of limitations on what can be proven.

Example 

module toInt where

toInt : {n} (fin n) => [n] -> Int
toInt x = foldr (\y b -> (if y then 1 else 0) + 2 * b) 0 (reverse x)

toInt_valid : {n} (fin n) => [n] -> Bit
property toInt_valid x = toInt x == toInteger x

‍

In this example, toInt is a function for converting a fixed-width bitvector of any length into an equivalent integer. The property toInt_valid states that toInt should always give the same result as the Cryptol primitive toInteger.

We can easily prove that this property holds for any concrete bitvector width directly from the Cryptol REPL.

cryptol> :l toInt.cry
toInt> :prove toInt_valid`{16}
Q.E.D.

‍

SAW

SAW, also developed by Galois, is a multi-tool for proving properties about software, supporting multiple input languages and integrating multiple solutions for specifying and proving properties. A key component of SAW is its deep integration with Cryptol, which acts as the SAW’s main specification language. Similar to Cryptol, SAW is primarily focused on automating proofs using SMT solvers, but supports user-guided proof strategies via its scripting language: SAWScript. 

Example

We can import the toInt Cryptol module into SAW and similarly prove that it holds for concrete bitvector widths:

sawscript> import "toInt.cry"
sawscript> prove z3 {{ toInt_valid`{16} }}
Valid

‍

Interactive Theorem Provers (ITPs)

In contrast to SAW and Cryptol, interactive theorem provers, such as Isabelle or Rocq, are general-purpose tools for any kind of formal reasoning. The core focus of an ITP is (most often) to provide a framework for a mix of automated reasoning and manual proofs, while ensuring that, regardless of the approach, only sound proofs are admitted. This makes them suitable for both formalized mathematics, as well as software verification. 

The flexibility of ITPs comes at the cost of a steep learning curve, users must first master writing formal proofs in general before they can attempt any software verification. Proofs in ITPs can become extremely large, making them difficult to update and maintain. Often, however, ITPs are the only tools expressive enough to handle a given verification problem.

Example

In our example, both Cryptol and SAW were able to prove toInt_valid for specific bitvector widths, but neither supports automatically proving that it holds for all bitvector lengths.

cryptol> :l toInt.cry
toInt> :prove toInt_valid
Not a monomorphic type:
  {n} (fin n) => [n] -> Bi
sawscript> prove z3 {{ toInt_valid }}
...
sequentToSATQuery: expected first order type or assertion:
Num

‍

Proving this property generally is simply out of scope for the bitvector theory of SMT solvers. This kind of abstract reasoning typically requires an ITP.

From Cryptol to Isabelle

With this update, SAWScript now includes two new commands: write_isabelle_cryptol_modules and offline_isabelle, where both require first executing enable_experimental to access. The first command takes a list of CryptolModule values as input and a target directory. It translates the provided modules (and any dependencies) into Isabelle and emits them as a collection of Isabelle theories.

Example

sawscript> toInt_m <- cryptol_load "toInt.cry"
sawscript> write_isabelle_cryptol_modules [toInt_m] "./"
Successfully wrote './toInt.thy'

‍

The resulting toInt.thy file then contains definitions for all of the functions and properties from the corresponding Cryptol module:

theory "toInt"
imports "Cryptol.Cryptol"
begin

context includes cryptol_translation_syntax begin
cryptol_definition toInt :: "{'n} ((fin 'n) =?> ((['n]) ⇒ Integer))" where
  "toInt x ≡ foldr`{'n,Bit,Integer} (λ(y :: Bit) (b :: Integer). ((if y then 1 else 0 :: Integer) +`{Integer} ((2 :: Integer) *`{Integer} b))) (0 :: Integer) (reverse`{'n,Bit} x)"

cryptol_definition toInt_valid :: "{'n} ((fin 'n) =?> ((['n]) ⇒ Bit))" where
  "toInt_valid x ≡ (toInt`{'n} x) ==`{Integer} (toInteger`{['n]} x)"
end
end

‍

We can then import this into a separate Isabelle theory in order to prove our desired property.

theory toInt_valid 
imports "toInt"
...
lemma "toInt_valid`{'n} x" sorry (* TODO *)
...

‍

The second command,  offline_isabelle, is a proof script command (or tactic) that can only be called as part of a call to “prove”. In SAW, an offline tactic takes the current proof state and translates it into input for another verification tool. Unlike the SMT-based tactics, SAW does not actually execute this external tool in order to validate the proof, instead it trusts that the user will perform this validation themselves.

Example

sawscript> import "toInt.cry"
sawscript> prove (offline_isabelle "toInt") {{ toInt_valid }}
Successfully wrote './toInt.thy'
Successfully wrote './toInt_prove0.thy'
Valid

‍

As before,  the toInt Cryptol module is translated into an Isabelle theory, but an additional theory toInt_prove0 has been generated from the proof goal:

theory "toInt_prove0"
...
cryptol_definition goal :: "{'n} ((fin 'n) =?> Bit)" where
  "goal  ≡ (∀(i_U :: ['n]). (toInt.toInt_valid`{'n} (i_U :: ['n])))"
...

‍

Although SAW has accepted the proof as “Valid”, it assumes that the user will independently prove that this generated goal is true. To accomplish this, we need to prove that the predicate “goal” is “True” for any instantiation of ‘n. With the supporting Cryptol theories, and Isabelle’s finite machine word library, this proof is straightforward:

lemma "goal`{'n}"  
  unfolding goal_def toInt_valid_def toInt_def
  by (simp add: horner_sum_foldr seq_to_list bl_to_bin_eq of_bool_def)

‍

Design Goals

The goal of this project is to provide the ability to automatically translate a Cryptol specification (i.e. a collection of Cryptol modules) into a corresponding set of Isabelle theories, preserving the original meaning (semantics) and as much of the original structure as possible.

Properties that can be proven in Cryptol should remain provable in Isabelle. In particular, functions should always produce the same concrete result, given the same concrete inputs.

In cases where Cryptol leaves behavior undefined (such as out-of-bounds indexing), the translated Isabelle definition may or may not be defined, but will be internally consistent.

The translation aims to preserve the original “shape” of the Cryptol source, with Cryptol concepts mapping to equivalent Isabelle concepts wherever possible. Cryptol modules are converted into Isabelle theories, functions into Isabelle functions, types into Isabelle types, and classes into Isabelle classes. This is not always possible: for example, the types [n + m] and [m + n] are considered equivalent in Cryptol, but not in Isabelle. Rather than complicating the translation itself, these issues are addressed by custom Isabelle tools, such as the cryptol_definition command.

Prelude

While the translation itself is relatively direct, most of the complexity lives in the provided prelude that allows the generated theories to be processed by Isabelle. This library, provided as Crypol.thy, defines syntax for Cryptol concepts (e.g., type-application, sequence type syntax, etc.), implements a custom seq type that is used as the translation target for Cryptol sequences, provides a library of lemmas for reasoning about these structures, and defines type constructors and classes for Cryptol’s corresponding type-level functions and classes.

Why Isabelle?

Isabelle brings a well-established ecosystem of proof tactics and theories. Most significantly, the Finite Machine Word library (originally developed as part of the l4.verified proofs) has a robust collection of results about word operations, including lemmas for converting between different representations, definitions and lemmas for arithmetic and bit-shifting, as well as code generator support. These can be adapted to proofs about Cryptol functions, using the included prelude theories.

Isabelle also includes a powerful and extensible library of proof tactics such as simp, auto, and induct, along with tools like Sledgehammer that use SMT solvers to generate interactive proofs and highly extensible term syntax. Its standard library covers a wide range of common structures, including lists, sets, integers, and type classes for abstract algebra.

Crucially, Cryptol specifications map (fairly) naturally into Isabelle’s higher-order logic and type system. First-order types like bitvectors and lists, higher-order functions, and type classes such as Ring or Integral all have close analogues in Isabelle. This makes it possible to translate Cryptol programs into Isabelle in a way that preserves their original structure and meaning, without introducing cumbersome translation artifacts from intermediate representations.

Limitations and Future Work

As with any translation between systems, there are limitations. Most notably, the semantic equivalence between Cryptol and Isabelle has not been formally proven. Cryptol itself does not have a fully formalized semantics; its behavior depends on a combination of the implementation of its expression evaluation, SMT translation, and underlying solver theory. Thus, testing that specifications agree on concrete inputs remains an important step. In the future, we may develop more standardized testing harnesses for validating semantic equivalence.

There is also currently no support for infinite sequences, as the provided “seq” type is only defined for finite lengths. In addition, parameterized module structure is flattened during translation, meaning each instantiation becomes its own independent theory. 

Despite these limitations, the ability to translate from Cryptol to Isabelle within SAW represents a remarkable leap forward - significantly expanding the scope of the possible in software verification. The classic usability–efficacy tradeoff in formal methods has long been taken as a given. That assumption is starting to crack. Stay tuned as we help close the gap.

‍

‍

[1] This is in addition to SAW’s existing Cryptol to Rocq translation capability.