# Project FloVer

## Interval Subdivisions and SMT-based range analysis

Interval subdivisions and SMT-based range analysis are implemented on the branch [SMT_Subdiv][2].
The folder `scripts` contains the scripts we used to evaluate the new features.
Our Coq implementation is in the folder `coq`. The overall soundness theorem is stated in file `CertificateChecker.v`.
The SMT-based range validator and its soundness proof can be found in file [SMTValidation.v][3], and the Subdivision checker can be found in file [SubdivsChecker.v][4].

## FMCAD 2018

The artifact and scripts used to run the evaluation for FMCAD 2018 can be found on the branch [FMCAD 2018][1].
The folder `artifacts` contains the results of the evaluation and `scripts` contains the scripts used to obtain the values.
`eval_interval.sh` runs the evaluation for floating-points on intervals, `eval_affine.sh` for floating-points and affine polynomials, and
`eval_fixed.sh` for 32bit word fixed-point numbers.

## Generating Error Bound Certificates

If you want to generate error bound certificates, you have to install Daisy from [https://github.com/malyzajko/daisy/tree/certified].
You then have to call Daisy with
```bash
$ ./daisy file --certificate=coq
```
or
```bash
$ ./daisy file --certificate=hol4
```
or for one of the binaries
```bash
$ ./daisy file --certificate=binary
```
The certificate will be generated in the output folder of Daisy.
To make sure that the certificate can be validated in the logics, please use
`--errorMethod=interval` and either `--rangeMethod=interval` or `--rangeMethod=affine`.
Unfortunately, affine polynomials are currently only supported on the branch `affine_arithmetic`.
Full support for fixed-point programs is also only available in `affine_arithmetic`.

## Checking Coq certificates

FloVer is known to compile with coq `8.8.2`.
To check the Coq certificate, you need to enter the `coq` directory.
Place any certificate you want to have checked into the `output` folder in the
coq directory and then run
```bash
$ ./configure_coq.sh
$ make
```
This will compile all coq files and then in the end the certificate in the output directory.

To compile the file `IEEE_connection.v` showing the relation to IEEE754 semantics, it is necessary to install
the Flocq library via opam:
```bash
$ opam install coq-flocq.3.1.0
```

The coq binary is build in the directory `coq/binary` and you can compile it by
running `make native` in the directory.

If an additional certificate should be checked later on, it suffices to call the Coq compiler:
```bash
$ coqc -R ./ Flover output/CERTIFICATE_FILE.v
```
where `./` is FloVer's `coq` folder.

The generated binary can be run with `coq_checker_native CERTIFICATE_FILE`.

## Checking HOL4 certificates

As only some versions of HOL4 are known to compile with CakeML, we provide a
configure script that sets up HOL4 accordingly:
```bash
$ cd hol4
$ ./configure_hol.sh --init
```
This will initialize the CakeML submodule and check out a HOL4 version that is
known to be compatible with it in your `$HOLDIR`.

Then, you can start compilation:
```bash
$ Holmake
```
Note that this may take some time, since it also builds all files from CakeML on
which the binary code extraction depends. If you don't want to wait for so long,
you can cheat the compilation:
```bash
$ Holmake --fast
```

To check HOL4 certificates, put them in the `hol4/output` directory , `cd` there
and run
```bash
$ Holmake ${CERTIFICATE_FILE/Script.sml/Theory.sig}
```
The HOL4 binary is build by entering the directory `hol4/binary`. Then one needs
to run
```bash
$ Holmake checkerBinaryTheory.sig
$ Holmake
```
The generated file `cake_checker` is the binary.
It can be run by
```bash
$ ./cake_checker CERTIFICATE_FILE
```

## Contributors

In no particular order: Raphael Monat, Nikita Zyuzin, Joachim Bard, Heiko Becker


Acknowledgements
----
We would like to thank Jacques-Henri Jourdan for the many insightful discussions
and technical help while working on the initial version of FloVer.

[1]: https://gitlab.mpi-sws.org/AVA/FloVer/tree/FMCAD2018
[2]: https://gitlab.mpi-sws.org/AVA/FloVer/tree/SMT_Subdiv
[3]: https://gitlab.mpi-sws.org/AVA/FloVer/blob/SMT_Subdiv/coq/SMTValidation.v
[4]: https://gitlab.mpi-sws.org/AVA/FloVer/blob/SMT_Subdiv/coq/SubdivsChecker.v