Proofs about Cryptol Models

Cryptol is a modeling and specification language for cryptographic algorithms. It is integrated into SAW and used for a broad range of tasks. Use of SAW for essentially any purpose requires use of Cryptol. Thus, the Cryptol manual is an important additional resource for SAW users.

In this chapter we discuss how to import Cryptol models and prove properties about them.

Importing Cryptol

Cryptol modules can be imported with import. For example:

import "Foo.cry";

The name to import can be a filename in double quotes, or a Cryptol module name, possibly qualified with ::, without quotes. The environment variable CRYPTOLPATH is used to search for Cryptol modules. SAW uses the same code to do this as Cryptol itself, so the behavior should be the same, including in complicated cases.

There is a known problem with the interaction of pathnames in quotes with CRYPTOLPATH, which also happens on the Cryptol command line; see #2194. This can be avoided by using qualified module names instead of file paths.

For example, instead of

import "Foo/Bar.cry";

use

import Foo::Bar;

To import a submodule (Cryptol submodules are ML-style modules nested within source files), use the keyword submodule before the module path.

By default the contents of the imported module are placed in scope. If this isn’t what you want, you can use the keyword as to introduce a qualified name.

After

import Foo::Bar as Baz;

the contents of the module Foo::Bar are available under the name Baz; e.g. Foo::Bar::myfunc appears as Baz::myfunc.

It is also possible to restrict the set of symbols imported. A list of symbols in parentheses after the rest of the import restricts the import to the symbols named; others are hidden. Alternatively, a list with the keyword hiding hides the listed symbols and imports the rest.

For example,

import Foo::Bar as Baz hiding (myfunc);

prevents referring to Baz::myfunc.

Partial imports are often useful to reduce namespace pollution or avoid name conflicts.

There is an additional mechanism cryptol_load, which is almost but not quite equivalent to import ... as.

The syntax Baz <- cryptol_load "Foo/Bar.cry"; is comparable to import "Foo/Bar.cry" as Baz; with one important difference: the returned handle Baz is a first-class value and can be passed to SAWScript functions if doing complicated things. In the import form that does not work; it can be used as a module qualifier only. Eventually the import form will become equivalent, at which point cryptol_load will be deprecated.

Note that cryptol_load does not support qualified module names or partial imports. Also, if using it for complicated things, beware of issue #3167; currently if you pass a module handle function to a function defined before the module load, things get confused and the Cryptol importer panics.

Writing Cryptol Inline in SAWScript

Typically, complex or nontrivial models will be written as one or more external Cryptol modules and imported into SAW. However, it isn’t necessary to create a whole Cryptol module for a few simple definitions. The quasiquotation syntax {{ expr }} allows embedding a Cryptol expression directly into SAWScript. We have already seen this in the introductory examples.

If you want to refer to a Cryptol type, the syntax for that is {| Ty |}.

You can also use the syntax let {{ decls }}; anywhere the SAWScript let decl; form can appear, which lets you write a Cryptol-level declaration, or possibly several of them.

Semantics of Imports

All Cryptol imported, or introduced by quasiquotation, is translated into SAWCore. (Recall that SAWCore is SAW’s internal interchange and proof language.)

This is done at the point in SAWScript execution where the import or quasiquotation block occurs. Unless doing complex things in SAWScript (discussed later), the primary consequence of this is that type errors and even syntax errors in embedded Cryptol are not detected until “runtime”. This can be annoying. However, it allows, within certain restrictions, Cryptol numeric types to be chosen at “runtime” rather than being fully constant; this in turn allows constructing more flexible proofs than would otherwise be possible.

Semantics of Quasiquotation Blocks

Embedded Cryptol blocks can refer to elements from imported Cryptol modules (complete with module qualifiers where needed, etc.) However, they can also refer to the following other things from the surrounding SAWScript:

  • Values whose SAWScript type is Term, regardless of where they came from, as long as they have an underlying SAWCore type that can be represented in Cryptol; this includes e.g. values from non-Cryptol importers.

  • Values whose SAWScript type is Type, regardless of where they came from, as long as they have a kind (type of type) that can be represented in Cryptol. These appear as Cryptol types.

  • SAWScript integers. These appear as Cryptol numeric types. If you want to use one as a Cryptol numeric value, you can lower it with ` in your Cryptol expression, as usual in Cryptol.

  • SAWScript boolean and string values appear as Cryptol boolean and string values.

Currently because SAW strings are Unicode and Cryptol strings are bytes, the translation of strings is unsatisfactory. This will almost certainly change in the future.

Unfortunately, due to internal restrictions, when an element cannot be made available in the Cryptol environment because its type is unsuitable, its name just disappears and references to it fail without any direct explanation. If you think something should be visible from Cryptol and it isn’t, check its type.

Stating Proof Goals

A proof goal can be any well-typed Cryptol expression that produces a boolean. (It can, but need not be, something specifically declared as a property in Cryptol.) The convention in Cryptol is that quantified proof goals are expressed as lambdas (that is, functions) rather than having forall-quantified types in Cryptol syntax. The operator for implication is ==>. Thus, for example, to prove that addition of integers respects less-than, the proof goal would be

{{ \(x : Integer) -> \y -> x < y ==> x + 1 < y + 1 }}

or equivalently

{{ \(x : Integer) y -> x < y ==> x + 1 < y + 1 }}

Beware that if you don’t specify the types when writing such a goal, the resulting goal may be polymorphic (for example, in this case it will range over all types in Cryptol Num) and then solvers will refuse to handle it.

Also beware that if you misspell the type name, Cryptol will assume you intended to introduce a type variable, with the same result.

Proving Things

The basic mechanism for proving Cryptol proof goals is the SAWScript function prove_print:

prove_print z3 {{ \(x : Integer) -> \y -> x < y ==> x + 1 < y + 1 }};

It takes two arguments; the second is the goal, which will usually be a Cryptol expression in double-braces as shown here, and the first is a proof script.

Unless using the manual proof interface, which is still largely experimental and not really recommended for other than advanced users (see Interactive Proofs), the proof scripts you’ll be using will be solver invocations.

The prove_print function fails (returning to the REPL if interactive and exiting with failure if not) if the proof does not succeed. Beware: a SAWScript function prove also exists. It returns a success/failure value, rather than failing; accidental use of prove instead of prove_print can result in proofs failing more or less silently. (At some point prove will be deprecated to remove this footgun; in the meantime, be careful.)

Using Solvers

The basic proof scripts are just solver names. For example, the z3 proof script runs the Z3 theorem prover, the abc proof script runs the ABC prover, and the cvc5 script runs the CVC5 solver. All of these are reasonable choices.

Others supported by SAW include Bitwuzla (bitwuzla), Boolector (boolector, deprecated because it’s been replaced upstream by Bitwuzla), MathSAT (mathsat), and Yices (yices). There is also an internal solver/decision procedure called rme that uses Reed-Muller expansions.

The question of which solver to use is fundamentally unanswerable: they are all different internally, and handle different sets of things well, and it’s extremely difficult to characterize those sets from outside.

The best general guidance we can offer is: if one doesn’t work, or takes excessively long to run or runs out of memory, try another.

There are a couple specific points worth mentioning:

  • A lot of people reach for z3 by default, which is as much because it’s better known than for any particular other reason. At one point it had broader coverage of theories than others; that is not true so much any more. This does not make it a bad choice; but sometimes, others are faster.

  • Bitwuzla (and Boolector before it) are specialized to bitvectors and don’t support integers (integers in the “math integer” and Cryptol Integer type sense) or many other theories; however, proofs near code tend to involve a lot of bitvectors and sometimes this is what you want.

  • The internal rme solver is based on an algorithm that specifically handles chains of exclusive-or efficiently, rather than (as often happens) expanding it in terms of plain and/or. This makes it work particularly well on the Galois field operations that show up, for example, in AES.

Also be aware that different versions of the same solver often also perform differently on any given proof, and newer versions are not always better.

Ultimately, the reason SAW supports so many solvers is that the only real way to deal with the question of which solver to use is to punt it to the user.

Further Solver Scripts

There is also a collection of additional solver scripts that run the solvers in slightly different ways.

The general form of these is

[offline_][LIBRARY_][unint_]SOLVER[_VARIANT]

The LIBRARY part can be either sbv for the SBV solver interface library or w4 for the what4 solver interface library. Neither of these is better nor worse; they’re just different. Using one or the other can occasionally unstick a proof that otherwise runs forever, or avoid a particular idiom that causes one of the solvers to complain or fail. Note that the default interface library if not requested specifically can vary; check the help text for each function with the :h REPL command if in doubt.

The unint fragment, when present, indicates a proof script that takes an additional argument, which is a list of names to be treated as uninterpreted. See the next section for further discussion.

The offline fragment, when present, indicates a proof script that takes a filename as an additional argument. Instead of running the solver, SAW will dump the solver query out to the file. This can be used to inspect the solver query as well as to run the solver by hand; the latter can be useful if you want to experiment with solver options or different solver versions or other things SAW does not provide good direct access to. Note that while all solvers theoretically speak SMTlib, each has its own dialect, so the offline output for each solver will be slightly different. Also note that the offline solver tactics always succeed; they assume you will run the solver yourself and the proof will work.

Not all combinations exist; in particular the offline tactics use what4 and generally also include unint_.

Use :search ProofScript or :search (_ -> ProofScript ()) to find everything that exists. (The second form excludes things like prove_print that take proof scripts. Both forms will also show you interactive proof tactics, especially if you have enabled experimental features.)

If you find that a combination you want to use is missing, please file a bug report.

Uninterpreted Functions

The most common technique to make a solver proof go faster is to mark certain functions as uninterpreted. This hides the implementation of a function. In fact, it replaces it with an arbitrary function where the only thing we know about it is that it is a function in the math sense: given the same argument, it produces the same result. This prevents the solver from wasting time exploring the definition. Note that this is a generalization of the proof goal: it replaces a goal that asks for something to be true about a specific function with one that asks for it to be true about all functions. So it’s a safe transformation.

This is an extremely helpful thing to do in many cases when reasoning about an equivalence that has the same function appearing on both sides. It’s very common that the function will also have the same argument on both sides, and that if it doesn’t, it’s wrong. In this case, preventing the solver from looking inside the function can save a lot of time.

Even though, arguably, converting a function to uninterpreted should be its own interactive proof tactic separate from (and used prior to) running a solver, it is common enough, especially in proofs about cryptographic code, that these compound proof scripts have been set up.

Satisfiability

SAW can also do satisfiability queries as well as proofs. The command is sat_print; it is used essentially the same way as prove_print. (There is also a sat that is, like prove, generally best avoided.) On success it prints the satisfying assignment found.

For example:

sawscript> sat_print z3 {{ \(x : Integer) (y : Integer) -> x < y }}
Sat: [
x = 0
y = 1
]

In the case of prove_print the goal is read “for all x and y…”; here it’s read “exists x and y such that…”.

There is, alas, currently no good way to state goals that require quantifier alternation. Since solvers cannot in general handle them, this is not a huge limitation in practice.