Commit f8feba16 authored by Heiko Becker's avatar Heiko Becker
Browse files


parent ee86245c
......@@ -25,15 +25,14 @@ or
$ ./daisy file --certificate=hol4
or for one of the binaries
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`.
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`.
The support for affine arithmetic is implemented in the branch [FMCAD2018][1] and is currently disabled on master.
## Checking Coq certificates
......@@ -62,8 +61,6 @@ $ 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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment