Other Examples

The code directory on GitHub contains a few additional examples not mentioned so far. These remaining examples don’t cover significant new material, but help fill in some extra use cases that are similar, but not identical to those already covered.

Java Equivalence Checking

The previous examples showed comparison between two different LLVM implementations, and cross-language comparisons between Cryptol, Java, and LLVM. The script in ffs_java.saw compares two different Java implementations, instead.

print "Extracting reference term";
j <- java_load_class "FFS";
ffs_ref <- jvm_extract j "ffs_ref";

print "Extracting implementation term";
ffs_imp <- jvm_extract j "ffs_imp";

print "Proving equivalence";
let thm1 = {{ \x -> ffs_ref x == ffs_imp x }};
prove_print abc thm1;
print "Done.";

As with previous Java examples, this one needs to be run with the -b flag to tell the interpreter where to find Java:

$ saw -b <path to directory where Java lives> ffs_java.saw

AIG Export and Import

Most of the previous examples have used the abc tactic to discharge theorems. This tactic works by translating the given term to And-Inverter Graph (AIG) format, transforming the graph in various ways, and then using a SAT solver to complete the proof.

Alternatively, the write_aig command can be used to write an AIG directly to a file, in AIGER format, for later processing by external tools, as shown in code/ffs_gen_aig.saw.

cls <- java_load_class "FFS";
bc <- llvm_load_module "ffs.bc";
java_ffs_ref <- jvm_extract cls "ffs_ref";
java_ffs_imp <- jvm_extract cls "ffs_imp";
c_ffs_ref <- llvm_extract bc "ffs_ref";
c_ffs_imp <- llvm_extract bc "ffs_imp";
write_aig "java_ffs_ref.aig" java_ffs_ref;
write_aig "java_ffs_imp.aig" java_ffs_imp;
write_aig "c_ffs_ref.aig" c_ffs_ref;
write_aig "c_ffs_imp.aig" c_ffs_imp;
print "Done.";

Conversely, the read_aig command can construct an internal term from an existing AIG file, as shown in ffs_compare_aig.saw.

java_ffs_ref <- read_aig "java_ffs_ref.aig";
java_ffs_imp <- read_aig "java_ffs_imp.aig";
c_ffs_ref <- read_aig "c_ffs_ref.aig";
c_ffs_imp <- read_aig "c_ffs_imp.aig";

let thm1 = {{ \x -> java_ffs_ref x == java_ffs_imp x }};
prove_print abc thm1;

let thm2 = {{ \x -> c_ffs_ref x == c_ffs_imp x }};
prove_print abc thm2;

print "Done.";

We can use external AIGs to verify the equivalence as follows, generating the AIGs with the first script and comparing them with the second:

$ saw -b <path to directory where Java lives> ffs_gen_aig.saw
$ saw ffs_compare_aig.saw

Files in AIGER format can be produced and processed by several external tools, including ABC, Cryptol version 1, and various hardware synthesis and verification systems.