path: root/doc/sources.md

# SMTCoq sources

This document describes the organization of the SMTCoq repository and locations
of source code and modules.

Sources are contained in the directory [src](../src) which can be found at
top-level. The directories [examples](../examples) and
[unit-tests](../unit-tests) contain respectively example files of usage for
SMTCoq and regression tests for the different tactics and vernacular commands
that the plugin provides.

The rest of the document describes the organization of `src`.


## Top-level architecture of SMTCoq

SMTCoq sources are contained in this directory. A few Coq files can be found at
top-level.

### [SMTCoq.v](../src/SMTCoq.v)

This is the main SMTCoq entry point, it is meant to be imported by users that
want to use SMTCoq in their Coq developments. It provides (exports) the other
SMTCoq modules as well as declares the OCaml plugin for adding the new
vernacular commands and tactics.

### [Trace.v](../src/Trace.v)

This file defines the types of certificates and steps (atomic certificate
pieces) as well as the *main checkers*.

The first section `trace` gives a generic definition of a main checker
parameterized by the type of individual steps and a function to check
individual steps `check_step` (small checkers). Correctness of the main checker
is proved under the assumption that the small checker is correct.

These generic definitions are applied to construct main checkers for resolution
(module `Sat_Checker`), CNF conversion (module `Cnf_Checker`) and
satisfiability modulo theories (module `Euf_Checker`). They each define an
inductive type `step` to represent certificate steps. For instance, in the case
of the resolution checker, the only possible step is to apply the resolution
rule so steps are defined as:

```coq
Inductive step :=
   | Res (_:int) (_:resolution).
```

The main theorems for these modules are named `checker_*correct`. For instance
the main result for the SMT checker (`Euf_Checker`) is formulated as follows:

```coq
Lemma checker_correct : forall d used_roots c,
    checker d used_roots c = true ->
    ~ valid t_func t_atom t_form d.
```

which means that if the checker returns true on the formula `d` and the
certificate `c` then `d` is not valid (*i.e.* `c` is a refutation proof
certificate for `d`).



### [State.v](../src/State.v)

This module is used to define representations for the global state of the
checker. 

A state is an array of clauses:

```coq
Module S.
  Definition t := array C.t.
...
End S.
```

on which we define resolution chain operations `set_resolve` that modify the
state.

Variables, literals and clauses are defined respectively in modules `Var`,
`Lit` and `C`. Binary resolution is defined between two clauses in `C.resolve`.



### [SMT_terms.v](../src/SMT_terms.v)

This Coq module defines reification types for formulas (`Form.form`), types
(`Typ.type`) and atoms/terms (`Atom.atom`). Formulas are given an
interpretation in Coq's Booleans, types are interpreted in Coq types (for
instance, type `TZ` is interpreted as Coq's mathematical integers `Z`) and
atoms are interpreted as Coq terms of type the interpretation of their type
(for instance an atom whose type is `TZ` is interpreted as an integer of `Z`).


**Some important lemmas:**

A function `cast` allows to change the encoded type of a term of type
`Typ.type` when we know two types are equal (the inductive `cast_result`
provides the conversion function).

```coq
Fixpoint cast_refl A:
      cast A A = Cast (fun P (H : P A) => H).
```

This is the lemma to use to remove cast constructions during the proofs.



```coq
Lemma i_eqb_spec : forall t x y, i_eqb t x y <-> x = y.
```

This other lemma says that Boolean equality over interpretation of types is the
equivalent to Leibniz equality. This is useful to allow rewriting.


Atom (as well as formulas) are encoded by integers, and mapping is preserved by
an array `t_atom`. Another array maintains interpretations of encodings. The
following lemma states that these two relates:

```coq
Lemma t_interp_wf : forall i,
   t_interp.[i] = interp_aux (PArray.get t_interp) (t_atom.[i]).
```




### [Misc.v](../src/Misc.v)

This module contains miscellaneous general lemmas that are used in several
places throughout the development of SMTCoq.




### [spl](../src/spl)

This directory contains everything related to simplifications of input
formulas as well as the Coq machinery to handle step checkers that use
assumptions (and generate sub-goals).

- [Arithmetic.v](../src/spl/Arithmetic.v): Arithmetic simplifications
- [Operators.v](../src/spl/Operators.v): Simplifications of SMT-LIB 2 operators
  (atomic disequalities and distinct operators)
- [Syntactic.v](../src/spl/Syntactic.v): Flattening and normalization of
  propositional structures
- [Assumptions.v](../src/spl/Assumptions.v): Small checker for assumptions



### [extraction](../src/extraction)

This is the extracted version of the SMTCoq checker, that can be run outside
Coq. It still needs to be fixed for the new additions and extensions.



### [classes](../src/classes)


The definitions of interpretations of terms and types of SMTCoq requires some
additional constraints that are encoded as Coq type-classes. This directory
contains definitions and properties of these classes
[SMT_classes.v](../src/classes/SMT_classes.v) as well as predefined useful
instances of these classes
[SMT_classes_instances.v](../src/classes/SMT_classes_instances.v).

These classes are:

- `EqbType`: types with a Boolean equality that reflects in Leibniz equality
- `DecType`: types with a decidable equality
- `OrdType`: class of types with a partial order 
- `Comparable`: augmentation of class of partial order with a compare function
  to obtain a total order
- `Inhabited`: class of inhabited types (used to obtain default values for
  types)
- `CompDec`: a class that merges all previous classes



## Small checkers

Small Coq checkers are organized in sub-directories that reflect the theories
they handle. Small checkers for propositional logic, equality over
uninterpreted functions and linear integer arithmetic all use preexisting
standard Coq libraries (Bool, Arith, Z, BinPos, ...) to formalize the
underlying interpretation of these theories. The theories of fixed-width
bit-vectors and functional unbounded arrays are formalized in new custom Coq
libraries (that are distributed with SMTCoq).


Computational small checkers have the following signature:

```coq
Definition checker (s : S.t) (p1 ... pn : int) (l1 ... lm : lit) : C.t := ...
```

where `s` is the state of the main checker, `p1`, ..., `pn` are positions
(there can be none) of deduced clauses that appear in the state `s` and `l1`,
..., `lm` are literals. The function `checker` returns a clause that is
`deducible` from the already deduced clauses in the state `s`.

Correctness of checkers are specified (and proven) through lemmas of the form:

```coq
Lemma valid_checker : forall s rho p1 ... pm l1 ... lm,
                      C.valid rho (checker s p1 ... pm l1 ... lm).
```

It states that the clause returned by `checker` is valid. In most cases for the
small checkers, when they fail they return a trivially true clause (`C._true`).


### [cnf](../src/cnf)

Small checkers for CNF (conjunctive normal form) are defined in the module
[Cnf.v](../src/cnf/Cnf.v). In essence they implement a Tseitin conversion.

For instance, the checker `check_BuildDef` returns a tautology in clausal form
(the validity of the clause is not dependent on the validity of the state) and
the checker `check_ImmBuildDef` is a generic encoding of conversion rules that
have a premise (which appears in the state).



### [euf](../src/euf)

The checkers for EUF (equality over uninterpreted functions) are defined in the
module [Euf.v](../src/euf/Euf.v).

The first one checks application of the rule of transitivity. `check_trans`
takes as argument the result of the rule application as well as list of
equalities of the form `a = b`, `b = c`, ..., `x = y`, `y = z`.

The other checker takes care of applications of the congruence rule. Functions
in SMT-LIB have a given arity and they are interpreted as Coq functions. The
checker for congruence can check rule applications with a number of equalities
corresponding to the arity of the function.


### [lia](../src/lia)

Checking linear arithmetic lemmas that come from the SMT solver is performed
using the already existing `Micromega` solver of Coq. The corresponding
checker is implemented in module [Lia.v](../src/lia/Lia.v).





### [bva](../src/bva)

The small checkers for bit-vector operations can be found in module
[Bva_checker.v](../src/bva/Bva_checker.v). They implement the rules for
bit-blasting operators of the theory of fixed width bit-vector.

There are small checkers for:

- bit-wise operators (`bvand`, `bvor`, `bvxor`, `bvnot`)
- equality
- variables
- constants
- extraction
- concatenation
- arithmetic operations (addition, negation, multiplication)
- comparison predicates (signed/unsigned)
- extensions (zero/signed)


The theory of fixed width is realized by an implementation provided in
[BVList.v](../src/bva/BVList.v). There, bit-vectors are interpreted by lists of
Booleans. The type of bit-vectors is a dependent type:

```coq
Parameter bitvector : N -> Type.
```

In the implementation, a bit-vector is a record that contains a list of
Booleans `bv`, *i.e.* the lists of its bits, as well as a proof of well
formedness `wf`, *i.e.* a proof that the size of the list `bv` is the parameter
`n` of the type.

```coq
Record bitvector_ (n:N) : Type :=
    MkBitvector
      { bv :> M.bitvector;
        wf : M.size bv = n
      }.
```



### [array](../src/array)

The theory of unbounded functional arrays with extensionality is realized in
Coq by a custom type that can be found in [FArray.v](../src/array/FArray.v).

```coq
Definition farray (key elt : Type) _ _  :=
```

The type `farray` is parameterized by the type of keys (or indexes) of the
array and the type of the elements. `key` must be a type equipped with a
partial order and `elt` must be inhabited. 


```coq
Record slist :=
  {this :> Raw.farray key elt;
   sorted : sort (Raw.ltk key_ord) this;
   nodefault : NoDefault this
   }.
   
Definition farray := slist.
```

An array is represented internally by an association list for its mappings with
additional constraints that encode the fact that the list is sorted and that
there are no mapping to the default value.

Computable equality and comparison functions require additional constraints on
the types `key` and `elt` (for instance they need to have a total order,
*etc.*).

This library also provides useful properties on these arrays. Notably
extensionality which is required by the theory of arrays in SMT solvers:

```coq
Lemma extensionnality : forall a b, (forall i, select a i = select b i) -> a = b.
```

The extensionality rule that is used by the checker is a bit different and
requires classical axioms to be proven. This is done in section
```Classical_extensionnality``` which provides an alternative version without
contaminating uses of the library.

There are three small checkers for arrays. They check application of the axioms
(in the theory sense) of the theory of arrays, two for *read over write* and
one for *extensionality*


## OCaml implementation of the plugin

Part of SMTCoq is implemented in OCaml. These concern functionality which are
not certified such as the reification mechanism, the parsers, pre-processors
and the definitions of tactics.

This part communicates directly with Coq by using the OCaml Coq API.


### [trace](../src/trace)

This directory contain the implementation of certificates and the
representation of SMT-LIB formulas in SMTCoq.

[coqTerms.ml](../src/trace/coqTerms.ml) contains imports from Coq of terms to
be used directly in OCaml. These include usual Coq terms but also ones specific
to SMTCoq.

[smtAtom.mli](../src/trace/smtAtom.mli) contains the definitions for the types
of atoms in SMTCoq but also provides smart constructors for them. The modules
defined in this file have functions to reify Coq terms in OCaml and to
translate back OCaml atoms and types to their Coq counterpart interpretation.

[smtForm.mli](../src/trace/smtForm.mli) plays the same role as `smtAtom` but on
the level of formulas.

[smtCertif.ml](../src/trace/smtCertif.ml) contains definitions for an OCaml
version of the steps of the certificate. These are the objects that are
constructed when importing a certificate from an SMT solver for instance.

[smtTrace.ml](../src/trace/smtTrace.ml) contains functions to build the Coq
version of the certificate from the OCaml one.

[smtCommands.ml](../src/trace/smtCommands.ml) constitute the bulk of the
implementation of the plugin. It contains the OCaml functions that are used to
build the Coq vernacular commands (`Verit_checker`, `Lfsc_checker`, ...) and
the tactics. It also contains functions to reconstruct Coq counter-examples
from models returned by the SMT solver.

[smtCnf.ml](../src/trace/smtCnf.ml) implements a CNF conversion on the type of
SMTCoq formulas.

[smtMisc.ml](../src/trace/smtMisc.ml) contains miscellaneous functions used in
the previous modules.



### [smtlib2](../src/smtlib2)

This directory contains utilities to communicate directly with SMT
solvers. This includes a lexer/parser for the SMT-LIB 2 format
([smtlib2_parse.mly](../src/smtlib2/smtlib2_parse.mly)) a conversion module
from SMT-LIB 2 to formulas and atoms of SMTCoq
([smtlib2_genConstr.ml](../src/smtlib2/smtlib2_genConstr.ml)) and a way to call
and communicate with SMT solvers through pipes
([smtlib2_solver.mli](../src/smtlib2/smtlib2_solver.mli)).



### [zchaff](../src/zchaff)

Files in this directory allow to call the SAT solver ZChaff. It contains a
parser for the sat solver input files and ZChaff certificates. The
implementation for the Coq tactic `zchaff` can be found in
[zchaff.ml](../src/zchaff/zchaff.ml).



### [verit](../src/verit)

This directory contains the necessary modules to support the SMT solver veriT.
In particular it contains a parser for the format of certificates of veriT
([veritParser.mly](../src/verit/veritParser.mly)) and an intermediate
representation of those certificates
([veritSyntax.mli](../src/verit/veritSyntax.mli)). This module also implements
a conversion function from veriT certificates to SMTCoq format of
certificates. This pre-processor is a simple one-to-one conversion.

The file ([verit.ml](../src/verit/verit.ml)) contains the functions to invoke
veritT and create SMT-LIB 2 scripts. This is used by the definition of the
tactic `verit` of the same file.



### [lfsc](../src/lfsc)

This directory contains the pre-processor for LFSC proofs to SMTCoq
certificates (as well as veriT certificates). The files
[ast.ml](../src/lfsc/ast.ml) and [builtin.ml](../src/lfsc/builtin.ml) contain
an OCaml implementation of a type checker for LFSC proofs. This directory also
contains a parser and lexer for LFSC (*c.f.*,
[lfscParser.mly](../src/lfsc/lfscParser.mly)).

The pre-processor is implemented in the module
[converter.ml](../src/lfsc/converter.ml)) as a *functor*. Depending on the
module (for terms and clauses conversions) that is passed in the functor
application, we obtain either a pre-processor from LFSC proofs to SMTCoq
certificates directly or a converter from LFSC proofs to veriT certificates.

> **Note:** You can obtain a standalone version of the converter by issuing
> `make` in this directory. This produces a binary `lfsctosmtcoq.native` that
> can be run with an LFSC proof as argument and produces a veriT certificate
> on the standard output.

Finally, the tactic `cvc4_bool` is implemented in the file
[lfsc.ml](../src/lfsc/lfsc.ml)). It contains functions to call the SMT solver
CVC4, convert its proof and call the base tactic of `smtCommands`.


## Tactics: proof search

### [BoolToProp.v](../src/BoolToProp.v)
This module includes the tactic `bool2prop` that converts a goal, if Boolean, into
a goal in Coq's `Prop`, after introducing universally quantified variables into the
context. 

It simply performs a search in the goal and does the mentioned conversion step by step
benefitting the `reflect` predicate popularized by the `SSReflect` library:

```coq
Inductive reflect (P : Prop) : bool -> Set :=
   | ReflectT :   P -> reflect P true 
   | ReflectF : ~ P -> reflect P false.
```

In fact, the predicate `reflect` returns the Boolean counterpart of a proposition.
Besides, it makes below lemma easily provable:

```coq
Lemma reflect_iff : forall P b, (P<->b=true) -> reflect P b.
```

This simply says that if a Coq proposition `P` is equivalent to some Boolean 
`b` being `true` then `b` is indeed the Boolean counterpart of `P`.

Now, let's exemplify how the tactic `bool2prop` benefits above steps:

Imagine a very simple goal that embodies the `or` connective

```coq
G0 || G1
```

for some Booleans `G0` and `G1`. Then, the tactic performes the following 
rewrite step on the goal 

```coq
rewrite <- (@reflect_iff (G0 = true \/ G1 = true) (G0 || G1)).
```

which turns it into:

```coq
G0 = true \/ G1 = true
```

together with introducing an additional goal:

```coq
reflect (G0 = true \/ G1 = true) (G0 || G1)
```

The first goal is indeed the intended one. However, the tactic can still go a step further 
putting the goal into the following shape:

```coq
H0 \/ H1
```

for some propositions `H0` and `H1`. This is indeed the case for Boolean equality and comparison over bit-vectors,
Boolean equality and  comparison over Coq intergers `Z`, and Boolean equality over fuctional arrays;
since the corresponding propositional predicates are proven to be equivalent. E.g., 

```coq
Lemma bv_ult_B2P: forall n (a b: bitvector n), bv_ult a b = true <-> bv_ultP a b.
```
where `bv_ult: bitvector n -> bitvector n -> bool` and `bv_ultP: bitvector n -> bitvector n -> Prop`. 

However, the second one must somehow be solved. This is indeed not so hard:
it suffices to apply the below lemma which has already been proven again by benefitting the `reflect` predicate:


```coq
Lemma orP : forall (a b: bool), reflect (a = true \/ b = true) (a || b).
```

Notice that the same sort of conversion steps for the other Boolean connectives are also handled
by the tactic `bool2prop`.

### [PropToBool.v](../src/PropToBool.v)
This module includes the tactic `prop2bool` that converts a goal, if in Coq's `Prop`, into
a Boolean goal, after introducing universally quantified variables into the context.
It is, in fact, the inverse of the above explained `bool2prop` tactic.

It simply performs a search in the goal and does the mentioned conversion step by step
benefitting the `reflect` predicate (see above `BoolToProp.v`). The predicate `reflect`
makes the following goal easily proveable:

```coq
Lemma reflect_iff : forall P b, reflect P b -> (P<->b=true).
```

This basically tells us that if `b` is the Boolean counterpart of some proposition `P`,
then `P` is indeed equivalent to `b` being `true`.

Now, let's exemplify how the tactic `prop2bool` benefits above steps:

Imagine a very simple goal that embodies the `or` connective as

```coq
H0 \/ H1
```

for some propositions `H0` and `H1`. At this point, the tactic needs to go a step further and
puts the goal into the following shape to be able to make use of the `reflect_iff` fact:

```coq
G0 = true \/ G1 = true
```

for some Booleans `G0` and `G1`. This step is indeed doable for propositional equality and comparison over
bit-vectors, propsitional equality and comparison over Coq intergers `Z`, and propositional equality over
fuctional arrays, since the corresponding Boolean predicates are proven to be equivalent. E.g.,

```coq
Lemma bv_ult_B2P: forall n (a b: bitvector n), bv_ult a b = true <-> bv_ultP a b.
```
where `bv_ult: bitvector n -> bitvector n -> bool` and `bv_ultP: bitvector n -> bitvector n -> Prop`.


Then, the tactic performes the following rewrite step on the goal 

```coq
rewrite (@reflect_iff (G0 = true \/ G1 = true) (G0 || G1))
```

which turns it into:

```coq
G0 || G1 = true
```

together with introducing an additional goal:

```coq
reflect (G0 = true \/ G1 = true) (G0 || G1)
```

The first goal is indeed the intended one. So that the tactic leaves the goal as it is. But the second
one must somehow be solved. In fact, this not so hard: it suffices to apply the below lemma which
has already been proven again by benefitting the `reflect` predicate:

```coq
Lemma orP : forall (a b: bool), reflect (a = true \/ b = true) (a || b).
```

Notice that the same sort of conversion steps for the other propositional connectives are also handled
by the tactic `prop2bool`.

### [Tactics.v](../src/Tactics.v)
This file includes four tactics that are written in `Ltac` language:

 - `zchaff` -> can function on the goals in Coq's `Prop`: 
 first calls `prop2bool` on the goal, getting the goal in `bool`, 
 then calls the reificiation tactic `zchaff_bool` (which can only function on Boolean goals),
 and finally puts the goal back in Coq's `Prop`, by calling `bool2prop`, if not solved.
 
 - `verit` -> can function on the goals in Coq's `Prop`: 
 first calls `prop2bool` on the goal, getting the goal in `bool`, 
 then calls the reificiation tactic `verit_bool` (can only function on Boolean goals),
 and finally puts the goal back in Coq's `Prop`, by calling `bool2prop`, if not solved.
 
 - `cvc4` -> can function on the goals in Coq's `Prop`: 
 first calls `prop2bool` on the goal, getting the goal in `bool`, 
 then calls the reificiation tactic `cvc4_bool` (can only function on Boolean goals),
 and finally puts the goal(s) back in Coq's `Prop`, by calling `bool2prop`, in case it is not solved or additional goals returned.
 
 - `smt` -> subsumes the powers of `cvc4` and `verit` tactics: 
 first calls `prop2bool` on the goal, getting the goal in `bool`, 
 then calls either of the reificiation tactics `cvc4_bool`, `verit_bool` (can only function on Boolean goals),
 and finally puts the goal(s) back in Coq's `Prop`, by calling `bool2prop`, in case it is not solved or additional goals returned.