README.md 4.2 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
29
30
31
or for one of the binaries
```bash
$ ./daisy file --certificate=binary
```
Heiko Becker's avatar
Heiko Becker committed
32
33
34
35
36
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`.
37

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

40
FloVer is known to compile with coq `8.8.2`.
Heiko Becker's avatar
Heiko Becker committed
41
42
43
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
44
45
46
47
48
```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
49

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

Heiko Becker's avatar
Heiko Becker committed
56
57
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
58

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

Heiko Becker's avatar
Heiko Becker committed
65
The generated binary can be run with `coq_checker_native CERTIFICATE_FILE`.
Heiko Becker's avatar
Heiko Becker committed
66
67
68

## Checking HOL4 certificates

Heiko Becker's avatar
Heiko Becker committed
69
70
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
71
```bash
Heiko Becker's avatar
Heiko Becker committed
72
73
$ cd hol4
$ ./configure_hol.sh --init
Heiko Becker's avatar
Heiko Becker committed
74
```
Heiko Becker's avatar
Heiko Becker committed
75
76
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
77

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

Heiko Becker's avatar
Heiko Becker committed
89
90
To check HOL4 certificates, put them in the `hol4/output` directory , `cd` there
and run
Heiko Becker's avatar
Heiko Becker committed
91
92
93
```bash
$ Holmake ${CERTIFICATE_FILE/Script.sml/Theory.sig}
```
Heiko Becker's avatar
Heiko Becker committed
94
95
The HOL4 binary is build by entering the directory `hol4/binary`. Then one needs
to run
Heiko Becker's avatar
Heiko Becker committed
96
97
98
99
100
101
102
```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
103
$ ./cake_checker CERTIFICATE_FILE
104
105
```

Heiko Becker's avatar
Heiko Becker committed
106
107
## Contributors

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

110

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

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