# SMTCoq artifact SMTCoq is a Coq tool that can be used to dispatch goals to external SAT and SMT solvers or simply to check proof witnesses produced by them. It currenly supports the quantifier free fragments of the SMT-LIB theories of fixed-sized bit-vectors (`QF_BV`), functional arrays (`QF_A`), linear integer arithmetic (`QF_LIA`), equality over uninterpreted functions (`QF_EUF`), and their combinations. This document describes the organization of the SMTCoq artifact submission for CAV 2017. ## How to download the artifact To get the artifact, please browse [here](https://drive.google.com/file/d/0BzDtBR99eKp9WVNNLTlBQy1Lc28/view) and download the `SMTCoq.ova` which is an image of an Ubuntu 16.04 LTS running virtual machine with approximately 3.6GB size (using 8GB memory, single processor which runs at the same frequency with the host processor, and approximately 63GB virtual disk space once imported). Then, please run [VirtualBox](https://www.virtualbox.org/wiki/VirtualBox); from the `File` top-down menu click on `Import Appliance...` and locate the `SMTCoq.ova` image. This will create you a virtual machine named `SMTCoq`. To run it, simply click on `Start`. The login (and super user) password is `123`. ## How to install the artifact Once logged into the virtual machine, you will find SMTCoq installed. If you want to install it on a separate machine, please check the SMTCoq [installation guide](https://github.com/lfsc/smtcoq/blob/master/INSTALL.md). ## How to run the artifact There are two use-cases of SMTCoq: - `within a Coq tactic`: we can give a Coq goal to an external solver and get a proof certificate for it. If the checker can validate the certificate, the soundness of the checker allow us to establish a proof of the initial goal (by `computational reflection`). In this use case, the trusted base consists only of Coq: if something else goes wrong (e.g., the checker cannot validate the certificate), the tactic will fail, but nothing unsound will be added to the system. - `correct-by-construction checker`: the idea is to check the validity of a proof witness, or proof certificate, produced by an external SMT solver for some input problem. In this use case, the trusted base is both Coq and the parser of the input problem. ### Within a Coq tactic Once logged into the virtual machine, open a terminal and go to `unit-tests` directory by typing `cd Desktop/smtcoq/unit-tests` from home. It contains a test file (`Tests_lfsc.v`) which makes use of the new SMTCoq tactics inside Coq, to discharge goals with the aid of various SMT solvers. #### Running everything with a single command You can run Coq in batch mode on our test file (once you are in the correct directory) by simply running the following command: ``` coqc Tests_lfsc.v ``` The return code should be 0 to indicate that Coq typed-checked everything correctly. The batch compiler `coqc` tries to compile `Tests_lfsc.v` file into `Test_lfsc.vo`. Please refer to [Coq reference manual](https://coq.inria.fr/refman/Reference-Manual008.html#compiled) for details. #### Interactive session through CoqIDE In the `unit-test` directory, open the test file by running ``` coqide Tests_lfsc.v ``` in the terminal. This will load in `CoqIDE` (the Coq interactive development environment) the file where we use SMTCoq within a Coq tactic called `smt`. Within the CoqIDE, use `Forward one command` button (downarrow on the top-left corner) to navigate through the source since `Go to end` button uses a parallelization strategy which is not yet supported by SMTCoq. If the background becomes green after going one command forward, this means that Coq has accepted the statement. At the end of the session the whole file should be green. If Coq fails to accept any statement, you will see a brief reason of the failure in the bottom-right rectangle within the `Errors` tab. #### Understanding the test file ```coq Require Import SMTCoq. ``` loads the SMTCoq module. It might be interesting to check out the implementation details (with pointers to source codes) of the module [here](https://github.com/lfsc/smtcoq/blob/master/doc/sources.md). Similarly, ```coq Require Import Bool PArray Int63 List ZArith Logic. ``` loads above-mentioned modules from the Coq standard library. ```coq Infix "-->" := implb (at level 60, right associativity) : bool_scope. ``` introduces a new notation `-->` for the boolean implication. Using ```coq Section BV. ``` we open a new section to prove theorems from the theory of fixed-size bitvectors. ```coq Import BVList.BITVECTOR_LIST. Local Open Scope bv_scope. ``` are to load our own [bitvector module](https://github.com/lfsc/smtcoq/blob/master/src/bva/BVList.v) (called BITVECTOR_LIST in BVList.v file) to be able to use theorems proven and notations introduced there. Note that to end a section `XX` you need to type ```coq End XX. ``` Now, we can state goals and prove them automatically. For instance, the goal ```coq Goal forall (a b c: bitvector 4), (c = (bv_and a b)) -> ((bv_and (bv_and c a) b) = c). ``` is proven by the `smt` tactic which subsumes the powers of the tactics `cvc4` and `verit`: ```coq Proof. smt. Qed. ``` Here are some more detailed explanation of the tactics: - `verit` -> applies to Coq goals of type `Prop`: it first calls `prop2bool` on the goal, converting the goal to a term of type `bool`, it then calls the reification tactic `verit_bool` (which applies only to Boolean goals), and it finally converts the goals back to `Prop`, by calling `bool2prop`, if it is not solved. - `cvc4` -> applies to Coq goals of type `Prop`: it first calls `prop2bool` on the goal, converting the goal to a term of type `bool`, it then calls the reification tactic `cvc4_bool` (which applies only to Boolean goals), and it finally converts any unsolved subgoals returned by CVC4 back to `Prop`, by calling `bool2prop`. - `smt` -> has the combined effect of the `cvc4` and `verit` tactics: it first calls `prop2bool` on the goal, it then calls either of the `cvc4_bool` and `verit_bool` tactics, and it finally converts any unsolved subgoals back to `Prop`, by calling `bool2prop`. The reification tactics `cvc4_bool` and `verit_bool`, implemented in OCaml, do most of the work: calling the external solvers (`CVC4` and `veriT` respectively), getting a proof certificate, and if SMTCoq's checker can validate the certificate, establishing the proof of the initial goal. The translation tactics `prop2bool` and `bool2prop` are implemented in Coq using the Ltac language. NB: all of the above tactics perform better on a "standard" machine compared to the VM. Another example of a goal in the theory of bit-vectors is the following: ```coq Goal forall (bv1 bv2 bv3: bitvector 4), bv1 = #b|0|0|0|0| /\ bv2 = #b|1|0|0|0| /\ bv3 = #b|1|1|0|0| -> bv_ultP bv1 bv2 /\ bv_ultP bv2 bv3. Proof. smt. Qed. ``` This goal uses three bit-vectors of size four: `bv1`, `bv2` and `bv3` then sets them to `0000`, `1000` and `1100` in the given order (`#b|1|0|...|` is the notation for bit-vector constants, where `0` stands for `false` and `1` is for `true`). Finally, it states that `bv1` is less than (unsigned less than over bit-vectors) `bv2` and (propositional) `bv2` is less than `bv3`. The tactic `smt` suffices to solve the goal. The following sections `Arrays`, `LIA`, `EUF`, `PR`and `A_BV_EUF_LIA_PR` in the Coq file include goals that can be proven by the `smt` tactic from the theories of functional arrays; linear integer arithmetic; uninterpreted functions; propositional reasoning and the combination of functional arrays, fixed-size bit-vectors, uninterpreted functions, linear integer arithmetic and propositional reasoning; respectively. The example that appears in the paper can be found in the section `A_BV_EUF_LIA_PR`: ```coq Goal forall (a b: farray Z Z) (v w x y: Z) (r s: bitvector 4) (f: Z -> Z) (g: farray Z Z -> Z) (h: bitvector 4 -> Z), a[x <- v] = b /\ a[y <- w] = b -> r = s /\ h r = v /\ h s = y -> v < x + 1 /\ v > x - 1 -> f (h r) = f (h s) \/ g a = g b. Proof. smt. (** "cvc4. verit." also solves the goal *) Qed. ``` It introduces two arrays `a` and `b` of type `farray Z Z` (the type of integer arrays with integer indices); four integers `v`, `w`, `x` and `y`; three uninterpreted fuctions `f`, `g` and `h`. Notice that `a[i]` is used to select the value stored in the `i^th^` index of the array `a` while `a[x <- v]` is used to store the value `v` in `a[x]`, `x^th^` index of array `a`. ### Correct-by-construction checker Using SMTCoq as a `correct-by-construction checker` means that it is possible to start with a problem in SMT-LIB standard, call an external solver (CVC4 or veriT) on it, get the unsatisfiability proof and certify it using the certified "small checkers" of SMTCoq. To test that, in a terminal go to `tests` directory (from home) by typing `cd Desktop/smtcoq/src/lfsc/tests`. Run the shell script `cvc4tocoq` providing an input file (i.e., `uf1.smt2`) by typing `./cvc4tocoq uf1.smt2`. This will call `CVC4`, get the proof in `LFSC` format, type check and convert it (using a converter written in OCaml) into SMTCoq format (which is very close to the proof format of `veriT`) and call the SMTCoq checker. If the checker returns `true` that means that SMTCoq indeed agreed that the proof of the input problem is correct. If it returns `false`, that means either that the proof is incorrect or that the OCaml converter is mistaken/incomplete. Note that you can replace `uf1.smt2` with any `.smt2` extended file under `tests` directory (`/home/Desktop/smtcoq/src/lfsc/tests`). Feel free to generate your own problem files but please recall that the input problems should be from the supported theories: `QF_A`, `QF_BV`, `QF_LIA`, `QF_EUF`, and their combinations. NB: The successful execution of the `./cvc4tocoq XX.smt2` script outputs some new files: - `XX.lfsc` -> the file includes the `LFSC` style unsatisfiability proof of the input problem `XX.smt2`. - `XX_lfsc.v` -> Coq source file that calls the Coq checkers to validate the proof`XX.lfsc`. - `XX_lfsc.glob` -> the file includes the globals of the source `XX_lfsc.v`. - `XX_lfsc.vo` -> compliled module file of the source `XX_lfsc.v`, it is used when to load the modules from the source `XX_lfsc.v`.