README.md 4.05 KB
Newer Older
Heiko Becker's avatar
Heiko Becker committed
1
# Project FloVer
2

Heiko Becker's avatar
Heiko Becker committed
3
## Interval Subdivisions and SMT-based range analysis
4

Heiko Becker's avatar
Heiko Becker committed
5 6 7
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`.
8 9
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].

10 11
## FMCAD 2018

12
The artifact and scripts used to run the evaluation for FMCAD 2018 can be found on the branch [FMCAD 2018][1].
13 14 15
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.
Eva Darulova's avatar
Eva Darulova committed
16

Heiko Becker's avatar
Heiko Becker committed
17
## Generating Error Bound Certificates
Heiko Becker's avatar
Heiko Becker committed
18

Heiko Becker's avatar
Heiko Becker committed
19 20
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
21 22 23 24 25
```bash
$ ./daisy file --certificate=coq
```
or
```bash
Heiko Becker's avatar
Heiko Becker committed
26
$ ./daisy file --certificate=hol4
27
```
Heiko Becker's avatar
Heiko Becker committed
28
or for the HOL4 binary
Heiko Becker's avatar
Heiko Becker committed
29 30 31
```bash
$ ./daisy file --certificate=binary
```
Heiko Becker's avatar
Heiko Becker committed
32 33 34
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`.
Heiko Becker's avatar
Heiko Becker committed
35
The support for affine arithmetic is implemented in the branch [FMCAD2018][1] and is currently disabled on master.
36

Heiko Becker's avatar
Heiko Becker committed
37
## Checking Coq certificates
38

39
FloVer is known to compile with coq `8.8.2`.
Heiko Becker's avatar
Heiko Becker committed
40 41 42
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
43 44 45 46 47
```bash
$ ./configure_coq.sh
$ make
```
This will compile all coq files and then in the end the certificate in the output directory.
Heiko Becker's avatar
Heiko Becker committed
48

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

Heiko Becker's avatar
Heiko Becker committed
55 56
The coq binary is build in the directory `coq/binary` and you can compile it by
running `make native` in the directory.
Heiko Becker's avatar
Heiko Becker committed
57

58 59
If an additional certificate should be checked later on, it suffices to call the Coq compiler:
```bash
Heiko Becker's avatar
Heiko Becker committed
60
$ coqc -R ./ Flover output/CERTIFICATE_FILE.v
61
```
Heiko Becker's avatar
Heiko Becker committed
62
where `./` is FloVer's `coq` folder.
63

Heiko Becker's avatar
Heiko Becker committed
64 65
## Checking HOL4 certificates

Heiko Becker's avatar
Heiko Becker committed
66 67
As only some versions of HOL4 are known to compile with CakeML, we provide a
configure script that sets up HOL4 accordingly:
Heiko Becker's avatar
Heiko Becker committed
68
```bash
Heiko Becker's avatar
Heiko Becker committed
69 70
$ cd hol4
$ ./configure_hol.sh --init
Heiko Becker's avatar
Heiko Becker committed
71
```
Heiko Becker's avatar
Heiko Becker committed
72 73
This will initialize the CakeML submodule and check out a HOL4 version that is
known to be compatible with it in your `$HOLDIR`.
Heiko Becker's avatar
Heiko Becker committed
74

Heiko Becker's avatar
Heiko Becker committed
75
Then, you can start compilation:
76
```bash
Heiko Becker's avatar
Heiko Becker committed
77 78
$ Holmake
```
Heiko Becker's avatar
Heiko Becker committed
79 80 81
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:
Heiko Becker's avatar
Heiko Becker committed
82 83 84 85
```bash
$ Holmake --fast
```

Heiko Becker's avatar
Heiko Becker committed
86 87
To check HOL4 certificates, put them in the `hol4/output` directory , `cd` there
and run
Heiko Becker's avatar
Heiko Becker committed
88 89 90
```bash
$ Holmake ${CERTIFICATE_FILE/Script.sml/Theory.sig}
```
Heiko Becker's avatar
Heiko Becker committed
91 92
The HOL4 binary is build by entering the directory `hol4/binary`. Then one needs
to run
Heiko Becker's avatar
Heiko Becker committed
93 94 95 96 97 98 99
```bash
$ Holmake checkerBinaryTheory.sig
$ Holmake
```
The generated file `cake_checker` is the binary.
It can be run by
```bash
Heiko Becker's avatar
Heiko Becker committed
100
$ ./cake_checker CERTIFICATE_FILE
101 102
```

Heiko Becker's avatar
Heiko Becker committed
103 104
## Contributors

105
In no particular order: Raphael Monat, Nikita Zyuzin, Joachim Bard, Heiko Becker
Eva Darulova's avatar
Eva Darulova committed
106

107

108 109
Acknowledgements
----
Heiko Becker's avatar
Heiko Becker committed
110
We would like to thank Jacques-Henri Jourdan for the many insightful discussions
111 112
and technical help while working on the initial version of FloVer.

113
[1]: https://gitlab.mpi-sws.org/AVA/FloVer/tree/FMCAD2018
Heiko Becker's avatar
Heiko Becker committed
114 115 116
[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