Proofs about Terms

The goal of SAW is to facilitate proofs about the behavior of programs. It may be useful to prove some small fact to use as a rewrite rule in later proofs, but ultimately these rewrite rules come together into a proof of some higher-level property about a software system.

Whether proving small lemmas (in the form of rewrite rules) or a top-level theorem, the process builds on the idea of a proof script that is run by one of the top level proof commands.

prove_print : ProofScript () -> Term -> TopLevel Theorem takes a proof script (which we’ll describe next) and a Term. The Term should be of function type with a return value of Bool (Bit at the Cryptol level). It will then use the proof script to attempt to show that the Term returns True for all possible inputs. If it is successful, it will print Valid and return a Theorem. If not, it will abort.
sat_print : ProofScript () -> Term -> TopLevel () is similar except that it looks for a single value for which the Term evaluates to True and prints out that value, returning nothing.
prove_core : ProofScript () -> String -> TopLevel Theorem proves and returns a Theorem from a string in SAWCore syntax.

Automated Tactics

The simplest proof scripts just specify the automated prover to use. The ProofScript values abc and z3 select the ABC and Z3 theorem provers, respectively, and are typically good choices.

For example, combining prove_print with abc:

sawscript> t <- prove_print abc {{ \(x:[8]) -> x+x == x*2 }}
Valid
sawscript> t
Theorem (let { x@1 = Prelude.Vec 8 Prelude.Bool
      x@2 = Cryptol.TCNum 8
      x@3 = Cryptol.PArithSeqBool x@2
    }
 in (x : x@1)
-> Prelude.EqTrue
     (Cryptol.ecEq x@1 (Cryptol.PCmpSeqBool x@2)
        (Cryptol.ecPlus x@1 x@3 x x)
        (Cryptol.ecMul x@1 x@3 x
           (Cryptol.ecNumber (Cryptol.TCNum 2) x@1
              (Cryptol.PLiteralSeqBool x@2)))))

Similarly, sat_print will show that the function returns True for one specific input (which it should, since we already know it returns True for all inputs):

sawscript> sat_print abc {{ \(x:[8]) -> x+x == x*2 }}
Sat: [x = 0]

In addition to these, the bitwuzla, boolector, cvc4, cvc5, mathsat, and yices provers are available. The internal decision procedure rme, short for Reed-Muller Expansion, is an automated prover that works particularly well on the Galois field operations that show up, for example, in AES.

In more complex cases, some pre-processing can be helpful or necessary before handing the problem off to an automated prover. The pre-processing can involve rewriting, beta reduction, unfolding, the use of provers that require slightly more configuration, or the use of provers that do very little real work.

Proof Script Diagnostics

During development of a proof, it can be useful to print various information about the current goal. The following tactics are useful in that context.

print_goal : ProofScript () prints the entire goal in SAWCore syntax.
print_goal_consts : ProofScript () prints a list of unfoldable constants in the current goal.
print_goal_depth : Int -> ProofScript () takes an integer argument, n, and prints the goal up to depth n. Any elided subterms are printed with a ... notation.
print_goal_size : ProofScript () prints the number of nodes in the DAG representation of the goal.

Rewriting in Proof Scripts

One of the key techniques available for completing proofs in SAWScript is the use of rewriting or transformation. The following commands support this approach.

simplify : Simpset -> ProofScript () works just like rewrite, except that it works in a ProofScript context and implicitly transforms the current (unnamed) goal rather than taking a Term as a parameter.
goal_eval : ProofScript () will evaluate the current proof goal to a first-order combination of primitives.
goal_eval_unint : [String] -> ProofScript () works like goal_eval but avoids expanding or simplifying the given names.

Other Transformations

Some useful transformations are not easily specified using equality statements, and instead have special tactics.

beta_reduce_goal : ProofScript () works like beta_reduce_term but on the current goal. It takes any sub-expression of the form (\x -> t) v and replaces it with a transformed version of t in which all instances of x are replaced by v.
unfolding : [String] -> ProofScript () works like unfold_term but on the current goal.

Using unfolding is mostly valuable for proofs based entirely on rewriting, since the default behavior for automated provers is to unfold everything before sending a goal to a prover. However, with some provers it is possible to indicate that specific named subterms should be represented as uninterpreted functions.

unint_bitwuzla : [String] -> ProofScript ()
unint_cvc4 : [String] -> ProofScript ()
unint_cvc5 : [String] -> ProofScript ()
unint_yices : [String] -> ProofScript ()
unint_z3 : [String] -> ProofScript ()

The list of String arguments in these cases indicates the names of the subterms to leave folded, and therefore present as uninterpreted functions to the prover. To determine which folded constants appear in a goal, use the print_goal_consts function described above.

Ultimately, we plan to implement a more generic tactic that leaves certain constants uninterpreted in whatever prover is ultimately used (provided that uninterpreted functions are expressible in the prover).

Note that each of the unint_* tactics have variants that are prefixed with sbv_ and w4_. The sbv_-prefixed tactics make use of the SBV library to represent and solve SMT queries:

sbv_unint_bitwuzla : [String] -> ProofScript ()
sbv_unint_cvc4 : [String] -> ProofScript ()
sbv_unint_cvc5 : [String] -> ProofScript ()
sbv_unint_yices : [String] -> ProofScript ()
sbv_unint_z3 : [String] -> ProofScript ()

The w4_-prefixed tactics make use of the What4 library instead of SBV:

w4_unint_bitwuzla : [String] -> ProofScript ()
w4_unint_cvc4 : [String] -> ProofScript ()
w4_unint_cvc5 : [String] -> ProofScript ()
w4_unint_yices : [String] -> ProofScript ()
w4_unint_z3 : [String] -> ProofScript ()

In most specifications, the choice of SBV versus What4 is not important, as both libraries are broadly compatible in terms of functionality. There are some situations where one library may outpeform the other, however, due to differences in how each library represents certain SMT queries. There are also some experimental features that are only supported with What4 at the moment, such as enable_lax_loads_and_stores.

Caching Solver Results

SAW has the capability to cache the results of tactics which call out to automated provers. This can save a considerable amount of time in cases such as proof development and CI, where the same proof scripts are often run repeatedly without changes.

This caching is available for all tactics which call out to automated provers at runtime: abc, boolector, cvc4, cvc5, mathsat, yices, z3, rme, and the family of unint tactics described in the previous section.

When solver caching is enabled and one of the tactics mentioned above is encountered, if there is already an entry in the cache corresponding to the call then the cached result is used, otherwise the appropriate solver is queried, and the result saved to the cache. Entries are indexed by a SHA256 hash of the exact query to the solver (ignoring variable names), any options passed to the solver, and the names and full version strings of all the solver backends involved (e.g. ABC and SBV for the abc tactic). This ensures cached results are only used when they would be identical to the result of actually running the tactic.

The simplest way to enable solver caching is to set the environment variable SAW_SOLVER_CACHE_PATH. With this environment variable set, saw and saw-remote-api will automatically keep an LMDB database at the given path containing the solver result cache. Setting this environment variable globally therefore creates a global, concurrency-safe solver result cache used by all newly created saw or saw-remote-api processes. Note that when this environment variable is set, SAW does not create a cache at the specified path until it is actually needed.

There are also a number of SAW commands related to solver caching.

set_solver_cache_path is like setting SAW_SOLVER_CACHE_PATH for the remainder of the current session, but opens an LMDB database at the specified path immediately. If a cache is already in use in the current session (i.e. through a prior call to set_solver_cache_path or through SAW_SOLVER_CACHE_PATH being set and the cache being used at least once) then all entries in the cache already in use will be copied to the new cache being opened.
clean_mismatched_versions_solver_cache will remove all entries in the solver result cache which were created using solver backend versions which do not match the versions in the current environment. This can be run after an update to clear out any old, unusable entries from the solver cache. This command can also be run directly from the command line through the --clean-mismatched-versions-solver-cache command-line option.
print_solver_cache prints to the console all entries in the cache whose SHA256 hash keys start with the given hex string. Providing an empty string results in all entries in the cache being printed.
print_solver_cache_stats prints to the console statistics including the size of the solver cache, where on disk it is stored, and some counts of how often it has been used during the current session.

For performing more complicated database operations on the set of cached results, the file solver_cache.py is provided with the Python bindings of the SAW Remote API. This file implements a general-purpose Python interface for interacting with the LMDB databases kept by SAW for solver caching.

Below is an example of using solver caching with saw -v Debug. Only the relevant output is shown, the rest abbreviated with “…”.

sawscript> set_solver_cache_path "example.cache"
sawscript> prove_print z3 {{ \(x:[8]) -> x+x == x*2 }}
[22:13:00.832] Caching result: d1f5a76e7a0b7c01 (SBV 9.2, Z3 4.8.7 - 64 bit)
...
sawscript> prove_print z3 {{ \(new:[8]) -> new+new == new*2 }}
[22:13:04.122] Using cached result: d1f5a76e7a0b7c01 (SBV 9.2, Z3 4.8.7 - 64 bit)
...
sawscript> prove_print (w4_unint_z3_using "qfnia" []) \
                                  {{ \(x:[8]) -> x+x == x*2 }}
[22:13:09.484] Caching result: 4ee451f8429c2dfe (What4 v1.3-29-g6c462cd using qfnia, Z3 4.8.7 - 64 bit)
...
sawscript> print_solver_cache "d1f5a76e7a0b7c01"
[22:13:13.250] SHA: d1f5a76e7a0b7c01bdfe7d0e1be82b4f233a805ae85a287d45933ed12a54d3eb
[22:13:13.250] - Result: unsat
[22:13:13.250] - Solver: "SBV->Z3"
[22:13:13.250] - Versions: SBV 9.2, Z3 4.8.7 - 64 bit
[22:13:13.250] - Last used: 2023-07-25 22:13:04.120351 UTC

sawscript> print_solver_cache "4ee451f8429c2dfe"
[22:13:16.727] SHA: 4ee451f8429c2dfefecb6216162bd33cf053f8e66a3b41833193529449ef5752
[22:13:16.727] - Result: unsat
[22:13:16.727] - Solver: "W4 ->z3"
[22:13:16.727] - Versions: What4 v1.3-29-g6c462cd using qfnia, Z3 4.8.7 - 64 bit
[22:13:16.727] - Last used: 2023-07-25 22:13:09.484464 UTC

sawscript> print_solver_cache_stats
[22:13:20.585] == Solver result cache statistics ==
[22:13:20.585] - 2 results cached in example.cache
[22:13:20.585] - 2 insertions into the cache so far this run (0 failed attempts)
[22:13:20.585] - 1 usage of cached results so far this run (0 failed attempts)

Other External Provers

In addition to the built-in automated provers already discussed, SAW supports more generic interfaces to other arbitrary theorem provers supporting specific interfaces.

external_aig_solver : String -> [String] -> ProofScript () supports theorem provers that can take input as a single-output AIGER file. The first argument is the name of the executable to run. The second argument is the list of command-line parameters to pass to that executable. Any element of this list equal to "%f" will be replaced with the name of the temporary AIGER file generated for the proof goal. The output from the solver is expected to be in DIMACS solution format.
external_cnf_solver : String -> [String] -> ProofScript () works similarly but for SAT solvers that take input in DIMACS CNF format and produce output in DIMACS solution format.

Offline Provers

For provers that must be invoked in more complex ways, or to defer proof until a later time, there are functions to write the current goal to a file in various formats, and then assume that the goal is valid through the rest of the script.

offline_aig : String -> ProofScript ()
offline_cnf : String -> ProofScript ()
offline_extcore : String -> ProofScript ()
offline_smtlib2 : String -> ProofScript ()
offline_unint_smtlib2 : [String] -> String -> ProofScript ()

These support the AIGER, DIMACS CNF, shared SAWCore, and SMT-Lib v2 formats, respectively. The shared representation for SAWCore is described in the saw-script repository. The offline_unint_smtlib2 command represents the folded subterms listed in its first argument as uninterpreted functions.

Finishing Proofs without External Solvers

Some proofs can be completed using unsound placeholders, or using techniques that do not require significant computation.

assume_unsat : ProofScript () indicates that the current goal should be assumed to be unsatisfiable. This is an alias for assume_valid. Users should prefer to use admit instead.
assume_valid : ProofScript () indicates that the current goal should be assumed to be valid. Users should prefer to use admit instead
admit : String -> ProofScript () indicates that the current goal should be assumed to be valid without proof. The given string should be used to record why the user has decided to assume this proof goal.
quickcheck : Int -> ProofScript () runs the goal on the given number of random inputs, and succeeds if the result of evaluation is always True. This is unsound, but can be helpful during proof development, or as a way to provide some evidence for the validity of a specification believed to be true but difficult or infeasible to prove.
trivial : ProofScript () states that the current goal should be trivially true. This tactic recognizes instances of equality that can be demonstrated by conversion alone. In particular it is able to prove EqTrue x goals where x reduces to the constant value True. It fails if this is not the case.

Multiple Goals

The proof scripts shown so far all have a single implicit goal. As in many other interactive provers, however, SAWScript proofs can have multiple goals. The following commands can introduce or work with multiple goals. These are experimental and can be used only after enable_experimental has been called.

goal_apply : Theorem -> ProofScript () will apply a given introduction rule to the current goal. This will result in zero or more new subgoals.
goal_assume : ProofScript Theorem will convert the first hypothesis in the current proof goal into a local Theorem
goal_insert : Theorem -> ProofScript () will insert a given Theorem as a new hypothesis in the current proof goal.
goal_intro : String -> ProofScript Term will introduce a quantified variable in the current proof goal, returning the variable as a Term.
goal_when : String -> ProofScript () -> ProofScript () will run the given proof script only when the goal name contains the given string.
goal_exact : Term -> ProofScript () will attempt to use the given term as an exact proof for the current goal. This tactic will succeed whever the type of the given term exactly matches the current goal, and will fail otherwise.
split_goal : ProofScript () will split a goal of the form Prelude.and prop1 prop2 into two separate goals prop1 and prop2.

Proof Failure and Satisfying Assignments

The prove_print and sat_print commands print out their essential results (potentially returning a Theorem in the case of prove_print). In some cases, though, one may want to act programmatically on the result of a proof rather than displaying it.

The prove and sat commands allow this sort of programmatic analysis of proof results. To allow this, they use two types we haven’t mentioned yet: ProofResult and SatResult. These are different from the other types in SAWScript because they encode the possibility of two outcomes. In the case of ProofResult, a statement may be valid or there may be a counter-example. In the case of SatResult, there may be a satisfying assignment or the statement may be unsatisfiable.

prove : ProofScript SatResult -> Term -> TopLevel ProofResult
sat : ProofScript SatResult -> Term -> TopLevel SatResult

To operate on these new types, SAWScript includes a pair of functions:

caseProofResult : {b} ProofResult -> b -> (Term -> b) -> b takes a ProofResult, a value to return in the case that the statement is valid, and a function to run on the counter-example, if there is one.
caseSatResult : {b} SatResult -> b -> (Term -> b) -> b has the same shape: it returns its first argument if the result represents an unsatisfiable statement, or its second argument applied to a satisfying assignment if it finds one.

AIG Values and Proofs

Most SAWScript programs operate on Term values, and in most cases this is the appropriate representation. It is possible, however, to represent the same function that a Term may represent using a different data structure: an And-Inverter-Graph (AIG). An AIG is a representation of a Boolean function as a circuit composed entirely of AND gates and inverters. Hardware synthesis and verification tools, including the ABC tool that SAW has built in, can do efficient verification and particularly equivalence checking on AIGs.

To take advantage of this capability, a handful of built-in commands can operate on AIGs.

bitblast : Term -> TopLevel AIG represents a Term as an AIG by “blasting” all of its primitive operations (things like bit-vector addition) down to the level of individual bits.
load_aig : String -> TopLevel AIG loads an AIG from an external AIGER file.
save_aig : String -> AIG -> TopLevel () saves an AIG to an external AIGER file.
save_aig_as_cnf : String -> AIG -> TopLevel () writes an AIG out in CNF format for input into a standard SAT solver.