SMTCoq

SMTCoq is a Coq tool that checks proof witnesses coming from external SAT and SMT solvers.

It relies on a certified checker for such witnesses. On top of it, vernacular commands and tactics to interface with the SAT solver zChaff and the SMT solvers veriT and CVC4 are provided. It is designed in a modular way allowing to extend it easily to other solvers.

The current stable version is version 1.3.

Installation

See the INSTALL.md file for instructions.

License

SMTCoq is released under the CeCILL-C license; see LICENSE for more details.

Use

Examples are given in the file examples/Example.v. They are meant to be easily re-usable for your own usage.

Overview

After installation, the SMTCoq module can be used in Coq files via the Require Import SMTCoq. command. For each supported solver, it provides:

• a vernacular command to check answers: XXX_Checker "problem_file" "witness_file" returns true only if witness_file contains a proof of the unsatisfiability of the problem stated in problem_file;

• a vernacular command to safely import theorems: XXX_Theorem theo "problem_file" "witness_file" produces a Coq term theo whose type is the theorem stated in problem_file if witness_file is a proof of the unsatisfiability of it, and fails otherwise.

• safe tactics to try to solve a Coq goal using the chosen solver (or a combination of solvers).

We now give more details for each solver.

zChaff

Compile and install zChaff as explained in the installation instructions. In the following, we consider that the command zchaff is in your PATH environment variable.

Checking zChaff answers of unsatisfiability and importing theorems

To check the result given by zChaff on an unsatisfiable dimacs file file.cnf:

• Produce a zChaff proof witness: zchaff file.cnf. This command produces a proof witness file named resolve_trace.

• In a Coq file file.v, put:

Require Import SMTCoq.
Zchaff_Checker "file.cnf" "resolve_trace".

• Compile file.v: coqc file.v. If it returns true then zChaff indeed proved that the problem was unsatisfiable.

• You can also produce Coq theorems from zChaff proof witnesses: the commands

Require Import SMTCoq.
Zchaff_Theorem theo "file.cnf" "resolve_trace".

will produce a Coq term theo whose type is the theorem stated in file.cnf.

zChaff as a Coq decision procedure

The zchaff tactic can be used to solve any goal of the form:

forall l, b1 = b2

where l is a quantifier-free list of variables and b1 and b2 are expressions of type bool.

veriT

Compile and install veriT as explained in the installation instructions. In the following, we consider that the command veriT is in your PATH environment variable.

Checking veriT answers of unsatisfiability and importing theorems

To check the result given by veriT on an unsatisfiable SMT-LIB2 file file.smt2:

• Produce a veriT proof witness:

veriT --proof-prune --proof-merge --proof-with-sharing --cnf-definitional --disable-e --disable-ackermann --input=smtlib2 --proof=file.log file.smt2

This command produces a proof witness file named file.log.

• In a Coq file file.v, put:

Require Import SMTCoq.
Section File.
  Verit_Checker "file.smt2" "file.log".
End File.

• Compile file.v: coqc file.v. If it returns true then veriT indeed proved that the problem was unsatisfiable.

• You can also produce Coq theorems from veriT proof witnesses: the commands

Require Import SMTCoq.
Section File.
  Verit_Theorem theo "file.smt2" "file.log".
End File.

will produce a Coq term theo whose type is the theorem stated in file.smt2.

The theories that are currently supported by these commands are QF_UF (theory of equality), QF_LIA (linear integer arithmetic), QF_IDL (integer difference logic), and their combinations.

veriT as a Coq decision procedure

The verit_bool tactic can be used to solve any goal of the form:

forall l, b1 = b2

where l is a quantifier-free list of variables and b1 and b2 are expressions of type bool.

In addition, the verit tactic applies to Coq goals of sort Prop: it first converts the goal into a term of type bool (thanks to the reflect predicate of SSReflect), and then calls the previous tactic verit_bool.

The theories that are currently supported by these tactics are QF_UF (theory of equality), QF_LIA (linear integer arithmetic), QF_IDL (integer difference logic), and their combinations.

CVC4

Compile and install CVC4 as explained in the installation instructions. In the following, we consider that the command cvc4 is in your PATH environment variable.

Checking CVC4 answers of unsatisfiability and importing theorems

To check the result given by CVC4 on an unsatisfiable SMT-LIB2 file name.smt2:

• Produce a CVC4 proof witness:

cvc4 --dump-proof --no-simplification --fewer-preprocessing-holes --no-bv-eq --no-bv-ineq --no-bv-algebraic name.smt2 > name.lfsc

This set of commands produces a proof witness file named name.lfsc.

• In a Coq file name.v, put:

Require Import SMTCoq Bool List.
Import ListNotations BVList.BITVECTOR_LIST FArray.
Local Open Scope list_scope.
Local Open Scope farray_scope.
Local Open Scope bv_scope.

Section File.
  Lfsc_Checker "name.smt2" "name.lfsc".
End File.

• Compile name.v: coqc name.v. If it returns true then the problem is indeed unsatisfiable.

NB: Use cvc4tocoq script in src/lfsc/tests to automatize the above steps.

• Ex: ./cvc4tocoq name.smt2 returns true only if the problem name.smt2 has been proved unsatisfiable by CVC4.

The theories that are currently supported by these commands are QF_UF (theory of equality), QF_LIA (linear integer arithmetic), QF_IDL (integer difference logic), QF_BV (theory of fixed-size bit vectors), QF_A (theory of arrays), and their combinations.

CVC4 as a Coq decision procedure

The cvc4_bool tactic can be used to solve any goal of the form:

forall l, b1 = b2

where l is a quantifier-free list of variables and b1 and b2 are expressions of type bool.

In addition, the cvc4 tactic applies to Coq goals of sort Prop: it first converts the goal into a term of type bool (thanks to the reflect predicate of SSReflect), it then calls the previous tactic cvc4_bool, and it finally converts any unsolved subgoals returned by CVC4 back to Prop, thus offering to the user the possibility to solve these (usually simpler) subgoals.

The theories that are currently supported by these tactics are QF_UF (theory of equality), QF_LIA (linear integer arithmetic), QF_IDL (integer difference logic), QF_BV (theory of fixed-size bit vectors), QF_A (theory of arrays), and their combinations.

The smt tactic

The more powerful tactic smt combines all the previous tactics: it first converts the goal to a term of type bool (thanks to the reflect predicate of SSReflect), it then calls a combination of the cvc4_bool and verit_bool tactics, and it finally converts any unsolved subgoals back to Prop, thus offering to the user the possibility to solve these (usually simpler) subgoals.