Commit 2f33f960 authored by Joachim Bard's avatar Joachim Bard
Browse files

Merge remote-tracking branch 'upstream/master'

parents f5ee5c23 babc1c42
...@@ -25,15 +25,14 @@ or ...@@ -25,15 +25,14 @@ or
```bash ```bash
$ ./daisy file --certificate=hol4 $ ./daisy file --certificate=hol4
``` ```
or for one of the binaries or for the HOL4 binary
```bash ```bash
$ ./daisy file --certificate=binary $ ./daisy file --certificate=binary
``` ```
The certificate will be generated in the output folder of Daisy. 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 To make sure that the certificate can be validated in the logics, please use
`--errorMethod=interval` and either `--rangeMethod=interval` or `--rangeMethod=affine`. `--errorMethod=interval` and either `--rangeMethod=interval` or `--rangeMethod=affine`.
Unfortunately, affine polynomials are currently only supported on the branch `affine_arithmetic`. The support for affine arithmetic is implemented in the branch [FMCAD2018][1] and is currently disabled on master.
Full support for fixed-point programs is also only available in `affine_arithmetic`.
## Checking Coq certificates ## Checking Coq certificates
...@@ -62,8 +61,6 @@ $ coqc -R ./ Flover output/CERTIFICATE_FILE.v ...@@ -62,8 +61,6 @@ $ coqc -R ./ Flover output/CERTIFICATE_FILE.v
``` ```
where `./` is FloVer's `coq` folder. where `./` is FloVer's `coq` folder.
The generated binary can be run with `coq_checker_native CERTIFICATE_FILE`.
## Checking HOL4 certificates ## Checking HOL4 certificates
As only some versions of HOL4 are known to compile with CakeML, we provide a As only some versions of HOL4 are known to compile with CakeML, we provide a
......
...@@ -610,7 +610,12 @@ Definition checkPreconds (subdivs: list precond) (P: precond) := ...@@ -610,7 +610,12 @@ Definition checkPreconds (subdivs: list precond) (P: precond) :=
let Piv := FloverMap.elements (fst P) in let Piv := FloverMap.elements (fst P) in
let Ps := map (fun P => FloverMap.elements (fst P)) subdivs in let Ps := map (fun P => FloverMap.elements (fst P)) subdivs in
let S_qs := map snd subdivs in let S_qs := map snd subdivs in
covers Piv (sort Ps) && forallbTailrec (fun q => SMTLogic_eqb q (snd P)) S_qs. (* Check that join of the preconditions for the subdivisions
covers the global precondition *)
covers Piv (sort Ps) &&
(* Check that additional constraints encoded by Daisy agree
for each subdivision *)
forallbTailrec (fun q => SMTLogic_eqb q (snd P)) S_qs.
Lemma checkPreconds_sound (subdivs: list precond) E P : Lemma checkPreconds_sound (subdivs: list precond) E P :
checkPreconds subdivs P = true -> checkPreconds subdivs P = true ->
...@@ -703,7 +708,7 @@ Proof. ...@@ -703,7 +708,7 @@ Proof.
{ apply unsat_qs. apply in_map_iff. now exists (P1, A, Qmap). } { apply unsat_qs. apply in_map_iff. now exists (P1, A, Qmap). }
repeat split; eauto using resultLeq_range_sound, resultLeq_error_sound. repeat split; eauto using resultLeq_range_sound, resultLeq_error_sound.
Qed. Qed.
(* (*
exists Gamma; intros approxE1E2. exists Gamma; intros approxE1E2.
assert (approxEnv E1 (toRExpMap Gamma) A (freeVars e) NatSet.empty E2) as approxE1E2' assert (approxEnv E1 (toRExpMap Gamma) A (freeVars e) NatSet.empty E2) as approxE1E2'
......
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