Project FloVer

Interval Subdivisions and SMT-based range analysis

Interval subdivisions and SMT-based range analysis are implemented on the branch SMT_Subdiv. 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, and the Subdivision checker can be found in file SubdivsChecker.v.

FMCAD 2018

The artifact and scripts used to run the evaluation for FMCAD 2018 can be found on the branch FMCAD 2018. 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

$ ./daisy file --certificate=coq

or

$ ./daisy file --certificate=hol4

or for the HOL4 binary

$ ./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. The support for affine arithmetic is implemented in the branch FMCAD2018 and is currently disabled on master.

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

$ ./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:

$ 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:

$ coqc -R ./ Flover output/CERTIFICATE_FILE.v

where ./ is FloVer's coq folder.

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:

$ 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:

$ 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:

$ Holmake --fast

To check HOL4 certificates, put them in the hol4/output directory , cd there and run

$ Holmake ${CERTIFICATE_FILE/Script.sml/Theory.sig}

The HOL4 binary is build by entering the directory hol4/binary. Then one needs to run

$ Holmake checkerBinaryTheory.sig
$ Holmake

The generated file cake_checker is the binary. It can be run by

$ ./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.