Getting Started

For your very first proof, after installing SAW, start the saw executable. At the REPL (the sawscript> prompt) type the following:

prove_print z3 {{ 2 < 3 }};

This asks SAW to prove, using the Z3 solver, that 2 is less than 3. This in turn is not a very difficult proof, so SAW will in response immediately print something like the following:

Theorem (EqTrue
  (ecLt Integer PCmpInteger
     (ecNumber (TCNum 2) Integer PLiteralInteger)
     (ecNumber (TCNum 3) Integer PLiteralInteger)))

The word Theorem indicates what you got. The rest is a rendering of the theorem statement 2 < 3 into SAW’s internal interchange language called SAWCore.

Note that you do not need to be able to read the SAWCore version of the theorem statement except for certain very advanced uses of SAW. (Nonetheless we hope to make it more readable in the future…)

Let’s take a closer look at exactly what this operation does. The prove_print command asks SAW to prove some proposition (the second argument) using some solver or proof script (the first argument) and print the result.

For the proof script we use the builtin tactic z3 that runs the Z3 solver. The proposition {{ 2 < 3 }} is a Cryptol code block containing a simple Cryptol expression. Cryptol expressions can be embedded in double curly braces like this.

Now try asking for something that isn’t true:

prove_print z3 {{ 3 < 2 }};

This will fail, print a stack trace showing you were in z3 (which is not super helpful in this context, but can be important in a large proof development), as well as prove: 1 unsolved subgoals, meaning that it couldn’t prove {{ 3 < 2 }}, plus also Invalid: [], which means that the overall proof attempt failed.

The empty list in the Invalid result is, in general, a counterexample for which the proposition isn’t true. In this case because everything is a constant, the counterexample is empty.

That isn’t very interesting, so let’s try something else not true:

prove_print z3 {{ \(x: [8]) (y: [8]) -> x < y }};

The proposition should be read as “for all x and y that are 8-bit unsigned bitvectors, x < y.” That is obviously not true, so we get a failure, and a counterexample with values of x and y for which it’s not true: Invalid: [x = 0, y = 0]. (You will probably get zero as the counterexample, but you might not; solvers are not very deterministic and might pick any of the 32,896 possible counterexamples.)

The [8] clauses are, as suggested above, type annotations to specify that x and y should be treated as 8-bit bitvectors. If you leave this off, the type is ambiguous and SAW rejects the proof. Unfortunately, as of the current writing, it does so with the following mysterious and almost entirely unhelpful complaint:

prove_print z3 {{ \x y -> x < y }};

produces

sequentToSATQuery: expected first order type or assertion:
isort 0

See issue #1418.

Proofs In Files

For all but the simplest experiments you’ll want to put things in a file and not type them at the REPL over and over again.

Put the example from above in a file called myproof.saw:

prove_print z3 {{ 2 < 3 }};

and then run

saw myproof.saw

This will print:

Loading file "myproof.saw"

Note that it does not print the Theorem value that the proof produces; only the REPL does that. If you want your files to print things as they run, you can use print. Put the following in myproof2.saw:

prove_print z3 {{ 2 < 3 }};
print "Two is less than three!";
prove_print z3 {{ 3 < 4 }};
print "Three is less than four!";

Running that with saw myproof2.saw will produce

Loading file "myproof2.saw"
Two is less than three!
Three is less than four!

Now see what happens attempting to prove something false. Put this in myproof3.saw:

prove_print z3 {{ 3 < 2 }};
print "Three is less than two!";

Running with saw myproof3.saw produces:

Loading file "myproof3.saw"
Stack trace:
   (builtin) in z3
   myproof3.saw:1:13-1:15 in (callback)
   (builtin) in prove_print
   myproof3.saw:1:1-1:27 (at top level)
prove: 1 unsolved subgoal(s)
Invalid: []

Note that it does not print “Three is less than two!”; it bails out instead. The stack trace tells you the line number it failed on, so if you have multiple proofs in the file you can tell which one didn’t work.

If you have your shell configured to report exit status you’ll see that it exits with nonzero status to show failure. This allows managing larger SAW developments with make.

Proofs About Code

While proving arbitrary Cryptol propositions is an important use case, SAW is perhaps most commonly used to do proofs about code. These proofs have a somewhat different form.

Proofs about code in SAW are generally done via symbolic execution. SAW uses the Crucible symbolic execution engine to run the code against arbitrary (“symbolic”) inputs, and checks that this execution matches a specification written in terms of preconditions and postconditions.

In SAW these specifications are assembled programmatically; then one fires off the proof itself as a separate step.

For a simple example, place the following C code in a file called example.c:

int clamp(int x) {
   return x > 100 ? 100 : x;
}

Then compile it as follows:

clang -emit-llvm -c example.c -o example.bc

This produces an LLVM bitcode file that SAW can read.

Now place the following in a file example.saw:

bc <- llvm_load_module "example.bc";

let clamp_spec = do {
   x <- llvm_fresh_var "x" (llvm_int 32);
   llvm_execute_func [llvm_term x];
   let x' = {{ if x >$ 100 then 100 else x }};
   llvm_return (llvm_term x');
};

llvm_verify bc "clamp" [] true clamp_spec z3;

Now run saw on the script file:

saw example.saw

It should print Verifying clamp..., then Simulating clamp... (this is the symbolic execution stage), then Checking proof obligations clamp... (this is checking the conditions identified by the symbolic execution that are needed for success), then Proof succeeded! clamp.

To see what it does if the code doesn’t match the specification, change the x >$ 100 in example.saw to x >$ 101. The proof will fail, and provide you with a counterexample: the specification and the code do not match when x is 100.

Now, let’s unpack what this example does. The C code contains a simple function clamp that takes an integer argument, and returns the argument value, clamping it to no greater than 100.

The first step in the SAW file loads the LLVM bitcode we generated with clang. This is done with the command llvm_load_module; that returns a handle that we remember as bc for “bitcode”.

The next part is the LLVM-level specification:

let clamp_spec = do {
   x <- llvm_fresh_var "x" (llvm_int 32);
   llvm_execute_func [llvm_term x];
   let x' = {{ if x >$ 100 then 100 else x }};
   llvm_return (llvm_term x');
};

The name clamp_spec is arbitrary, although it’s usually helpful to name specifications after the code they specify. The do block is a series of actions that we’re going to attach to this name. This does not perform these actions right away; rather, it collects them up to be executed later. You will notice that some of the steps (both in the spec and at the top level of our proof development) bind variables with let and some use <- instead. The short explanation is that <- executes do-blocks and let doesn’t. We’ll return to this point in more detail later. There is a quick discussion in the introduction to SAWScript. More about <- can be found in Programming in SAWScript.

Now, the spec in the do block contains four steps. First, we call llvm_fresh_var to allocate a variable for use in the specification. Variables allocated with llvm_fresh_var like this become inputs to the verification. They are forall-quantified in the resultant theorem. Here we pass it the string "x" as a name for SAW to use when talking to us; x is arbitrary but as with the specification name it’s usually helpful to name specification objects after their corresponding code objects. Meanwhile, the unquoted x on the left is the proof-level metavariable we store the result in. The argument llvm_int 32 is the LLVM-level type for the variable, in this case a 32-bit bitvector. This corresponds to the C type int used in the C code.

The second step is that we set up the calling sequence for the function we’re verifying. This specifies the arguments in terms of the specification variables we created. In this case we have one argument, llvm_term x. The use of llvm_term promotes x, which is a Cryptol-level value, to an LLVM-level value. See Languages for Specifications.

The third step is to figure the return value we want to specify. We bind it to the name x'.

The final step of the specification is to specify the return value for the C function. Again we use llvm_term to lift the Cryptol-level value to an LLVM-level value.

Having written the specification, we now can now use it by verifying the function clamp in the bitcode module bc.

llvm_verify bc “clamp” [] true clamp_spec z3;

Here `bc` is the LLVM bitcode module and `"clamp"` is the function
within it we want to verify.
The empty list `[]` is a list of other previously verified functions
we want to use as lemmas for verifying this function.
Our simple example function does not call any other functions, so
we provide nothing here.
In more complex verifications there will often be entries here.
See
[Overrides and Compositional Verification](overrides-and-compositional-verification).

The `true` enables _path satisfiability checking_.
In general you should leave this set to `true`, though in some cases
turning it off with `false` can improve proof performance.
<!--
   XXX: when we have a discussion of this in some advanced topics chapter
   that doesn't currently exist, make a forward reference to it.
-->

<!--- XXX move this text
This prevents SAW from exploring certain cases of impossible execution.
In simple code like this, it has no effect; in other cases it avoids
spurious verification failures.
In some cases with complex code path satisfiability checking can
become combinatorially expensive, and in some of those cases disabling
it avoids the consequent performance problems and still successfully
verifies the code without generating spurious failures.
In general best practice is to enable path satisfiability checking,
and only turn it off if complications ensue.
-->

Finally, the last argument is a proof script or solver to use to
solve the proof goals that result from symbolic execution.
(Solver usage will be discussed further later on; see
[Using Solvers](#using-solvers).)

## Further Examples

For further worked examples, please consult one or both of the
SAW tutorials:
_LLVM/Java Verification with SAW_
and
_Rust Verification with SAW_
that you can find alongside this manual.

There is also a collection of examples in the `examples` subtree of the
source repository.

<!--
XXX: Go through this and sprinkle forward references, certainly
XXX: all the XXX ones but probably quite a few more.
XXX: I'm putting this off because a lot of the references we ought
XXX: to have don't have targets yet, or the targets are misnamed or
XXX: in the wrong place.
-->

<!--
XXX: Also, some people are going to not really want to read any more
XXX: than this and would rather just jump in, and what they'll want at
XXX: this point is a quick overview of how to discover things (:h, :t,
XXX: :search etc.) But as things stand, I don't think that's going to
XXX: be very successful; at a minimum they'll need to read about
XXX: memory allocation, but in general the system is still too tetchy
XXX: and too opaque for that approach to work very well. We ought to
XXX: try to figure out how to cater to this kind of reader better; I
XXX: think we should revisit the question once we've condensed the next
XXX: few chapters by moving stuff inappropriate for the user guide to
XXX: the reference manual. At that point it should be a lot clearer
XXX: (and reading on a bit will likely look more appealing, too...)
-->