...
 
Commits (3)
......@@ -25,15 +25,14 @@ or
```bash
$ ./daisy file --certificate=hol4
```
or for one of the binaries
or for the HOL4 binary
```bash
$ ./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
......
......@@ -610,7 +610,12 @@ Definition checkPreconds (subdivs: list precond) (P: precond) :=
let Piv := FloverMap.elements (fst P) in
let Ps := map (fun P => FloverMap.elements (fst P)) 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 :
checkPreconds subdivs P = true ->
......@@ -703,7 +708,7 @@ Proof.
{ apply unsat_qs. apply in_map_iff. now exists (P1, A, Qmap). }
repeat split; eauto using resultLeq_range_sound, resultLeq_error_sound.
Qed.
(*
exists Gamma; intros approxE1E2.
assert (approxEnv E1 (toRExpMap Gamma) A (freeVars e) NatSet.empty E2) as approxE1E2'
......