Commit d05a7b09 authored by Heiko Becker's avatar Heiko Becker

Merge branch 'master' into 'certificates'

Add IEEE connection in HOL4 and IEEE range validator in Coq and HOL4

See merge request AVA/daisy!116
parents f24a4152 27105163
......@@ -24,6 +24,8 @@ coq/binary/*.cmi
coq/binary/*.cmo
coq/binary/CoqChecker*
coq/binary/coq_checker_*
coq/binary/*.cmx
coq/binary/*.o
hol4/*Theory*
hol4/*.ui
......
......@@ -58,7 +58,7 @@ You can then run Daisy on an input file as follows:
$ ./daisy testcases/rosa/Doppler.scala
```
## Checking Interval Arithmetic Certificates
## Generating Error Bound Certificates
If you want to produce certificates to check them in either of the supported backends,
you have to call Daisy as with
......@@ -67,26 +67,74 @@ $ ./daisy file --certificate=coq
```
or
```bash
$ ./daisy file --certificate=hol
$ ./daisy file --certificate=hol4
```
or for one of the binaries
```bash
$ ./daisy file --certificate=binary
```
The certificate can then be found in the folder `coq/output`, `hol4/output` or `output` for binary certificates.
The certificate can then be found in the folder `coq/output` or `hol/output`.
## Checking Coq certificates
To check the Coq certificate, you need to enter the coq directory and then run
To check the Coq certificate, you need to enter the `coq` directory and then run
```bash
$ ./configure_coq.sh
$ make
```
This will compile all coq files and then in the end the certificate in the output directory.
The coq binaries are build in the directory `coq/binary` and you can compile them by running
either `make native` or make byte` in the directory.
If an additional certificate should be checked later on, it suffices to call the Coq compiler:
```bash
$ coqc -R ./ Daisy output/CERTIFICATE_FILE.v
```
To check the HOL-Light certificates, you need to enter the hol directory and then run
The generated binaries can be run with `coq_checker_{native/byte} CERTIFICATE_FILE`.
## Checking HOL4 certificates
If you haven't updated your HOL4 installation in a while, update it first:
```bash
$ cd path/to/HOL
$ bin/build cleanAll
$ poly < tools/smart-configure.sml
$ bin/build
```
Then, back in the Daisy home directory, if you haven't done so before:
```bash
$ git submodule init
```
(If successfull, you should see a message like ```Submodule 'hol4/cakeml' (https://github.com/CakeML/cakeml.git) registered for path 'hol4/cakeml'```)
Then, initialize the CakeML submodule and start compilation:
```bash
$ ./configure_hol.sh
$ ocaml output/CERTIFICATE_FILE.hl
$ git submodule update --recursive --remote
$ cd hol4/
$ Holmake
```
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:
```bash
$ Holmake --fast
```
To check the HOL4 certificates, enter the `hol4/output` directory and run
```bash
$ Holmake ${CERTIFICATE_FILE/Script.sml/Theory.sig}
```
The HOL4 binary is build by entering the directory `hol4/binary`. Then one needs to run
```bash
$ Holmake checkerBinaryTheory.sig
$ Holmake
```
The generated file `cake_checker` is the binary.
It can be run by
```bash
$ ./cake_checker < CERTIFICATE_FILE
```
## Additional Software
......@@ -102,12 +150,6 @@ Currently, this is
* Coq: Version 8.5pl2 if you want to extract certificates for it, [install it](https://coq.inria.fr/download)
* HOL-Light: Git checkout (no later than 1.08.2016) if you want to extract certificates for it, [downloadit](https://github.com/jrh13/hol-light/)
Afterwards configure the environment variable HOLLIGHT_HOME to point to the directory you downloaded HOL-Light into with
```
$ export HOLLIGHT_HOME=path_to_hol_light_git
```
## Documentation
## Intellij Idea Setup
......
......@@ -6,7 +6,7 @@
**)
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Daisy.Infra.RealSimps Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.Ltacs.
Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments Daisy.Typing.
Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments Daisy.Typing Daisy.FPRangeValidator.
Require Export Coq.QArith.QArith.
Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Commands.
......@@ -14,7 +14,7 @@ Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Commands.
(** Certificate checking function **)
Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) (defVars:nat -> option mType) :=
if (typeCheck e defVars (typeMap defVars e)) then
if (validIntervalbounds e absenv P NatSet.empty)
if (validIntervalbounds e absenv P NatSet.empty) && FPRangeValidator e absenv (typeMap defVars e) NatSet.empty
then (validErrorbound e (typeMap defVars e) absenv NatSet.empty)
else false
else false.
......@@ -37,7 +37,9 @@ Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P defVar
exists vR vF m,
eval_exp E1 (toRMap defVars) (toREval (toRExp e)) vR M0 /\
eval_exp E2 defVars (toRExp e) vF m /\
(Rabs (vR - vF) <= Q2R (snd (absenv e)))%R.
(forall vF m,
eval_exp E2 defVars (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R (snd (absenv e))))%R.
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
......@@ -61,20 +63,23 @@ Proof.
assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)).
{ hnf; intros a in_empty.
set_tac. }
assert (forall v, (v) mem (NatSet.empty) = true -> exists vR : R, E1 v = Some vR /\ (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R).
rename R into validFPRanges.
assert (forall v, (v) mem (NatSet.empty) = true -> exists vR :R, E1 v = Some vR /\ (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R).
{ intros v v_in_empty.
rewrite NatSet.mem_spec in v_in_empty.
inversion v_in_empty. }
edestruct validIntervalbounds_sound as [vR [eval_real real_bounds_e]]; eauto.
destruct (validErrorbound_sound e P (typeMap defVars e) L approxE1E2 H0 eval_real R0 L0 H1 P_valid H absenv_eq) as [vF [mF [eval_float err_bounded]]]; auto.
destruct (validErrorbound_sound e P (typeMap defVars e) L approxE1E2 H0 eval_real R0 L1 H1 P_valid H absenv_eq) as [[vF [mF eval_float]] err_bounded]; auto.
exists vR; exists vF; exists mF; split; auto.
Qed.
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) defVars:=
if (typeCheckCmd f defVars (typeMapCmd defVars f) && validSSA f (freeVars f))
then if (validIntervalboundsCmd f absenv P NatSet.empty)
then (validErrorboundCmd f (typeMapCmd defVars f) absenv NatSet.empty)
else false
then
if (validIntervalboundsCmd f absenv P NatSet.empty) &&
FPRangeValidatorCmd f absenv (typeMapCmd defVars f) NatSet.empty
then (validErrorboundCmd f (typeMapCmd defVars f) absenv NatSet.empty)
else false
else false.
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P defVars:
......@@ -90,7 +95,9 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P d
exists vR vF m,
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR M0 /\
bstep (toRCmd f) E2 defVars vF m /\
(Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp f))))%R.
(forall vF m,
bstep (toRCmd f) E2 defVars vF m ->
(Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp f))))%R).
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
......@@ -109,6 +116,7 @@ Proof.
{ eapply ssa_equal_set; try eauto.
apply NatSetProps.empty_union_2.
apply NatSet.empty_spec. }
rename R into validFPRanges.
assert (forall v, (v) mem (NatSet.empty) = true ->
exists vR : R,
E1 v = Some vR /\ (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R) as no_dVars_valid.
......@@ -124,6 +132,9 @@ Proof.
as freeVars_contained by set_tac.
edestruct (validIntervalboundsCmd_sound) as [vR [eval_real bounded_real_f]] ; eauto.
rewrite absenv_eq; simpl.
edestruct (validErrorboundCmd_sound) as [vF [mF [eval_float bounded_float]]]; eauto.
exists vR; exists vF; exists mF; split; auto.
edestruct validErrorboundCmd_gives_eval as [vF [mF eval_float]]; eauto.
exists vR; exists vF; exists mF; split; try auto.
split; try auto.
intros.
eapply validErrorboundCmd_sound; eauto.
Qed.
\ No newline at end of file
......@@ -86,3 +86,19 @@ Fixpoint liveVars V (f:cmd V) :NatSet.t :=
| Let _ _ e g => NatSet.union (usedVars e) (liveVars g)
| Ret e => usedVars e
end.
Lemma bstep_eq_env f:
forall E1 E2 Gamma v m,
(forall x, E1 x = E2 x) ->
bstep f E1 Gamma v m ->
bstep f E2 Gamma v m.
Proof.
induction f; intros * eq_envs bstep_E1;
inversion bstep_E1; subst; simpl in *.
- eapply eval_eq_env in H7; eauto. eapply let_b; eauto.
eapply IHf. instantiate (1:=(updEnv n v0 E1)).
+ intros; unfold updEnv.
destruct (x=? n); auto.
+ auto.
- apply ret_b. eapply eval_eq_env; eauto.
Qed.
\ No newline at end of file
......@@ -108,15 +108,16 @@ Proof.
rewrite x_x0_neq in x_typed; auto.
Qed.
Lemma approxEnv_dVar_bounded v2 m:
Lemma approxEnv_dVar_bounded v2 m e:
E1 x = Some v ->
E2 x = Some v2 ->
NatSet.In x dVars ->
Gamma x = Some m ->
(Rabs (v - v2) <= Q2R (snd (A (Var Q x))))%R.
snd (A (Var Q x)) = e ->
(Rabs (v - v2) <= Q2R e)%R.
Proof.
induction approxEnvs;
intros E1_def E2_def x_def x_typed.
intros E1_def E2_def x_def x_typed A_e; subst.
- unfold emptyEnv in *; simpl in *; congruence.
- assert (x =? x0 = false) as x_x0_neq.
{ rewrite Nat.eqb_neq; hnf; intros; subst.
......
......@@ -25,6 +25,7 @@ Proof.
rewrite Q2R0_is_0; lra.
Qed.
Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType) defVars:
eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
......@@ -42,8 +43,9 @@ Proof.
intros e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2.
(* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
inversion plus_real; subst.
destruct m0; destruct m3; inversion H2;
simpl in H3; rewrite Q2R0_is_0 in H3; auto.
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
rewrite delta_0_deterministic in plus_real; auto.
rewrite (delta_0_deterministic (evalBinop Plus v1 v2) delta); auto.
unfold evalBinop in *; simpl in *.
......@@ -109,8 +111,9 @@ Proof.
intros e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2.
(* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
inversion sub_real; subst;
destruct m0; destruct m3; inversion H2;
simpl in H3; rewrite Q2R0_is_0 in H3; auto.
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
rewrite delta_0_deterministic in sub_real; auto.
rewrite delta_0_deterministic; auto.
unfold evalBinop in *; simpl in *.
......@@ -168,8 +171,9 @@ Proof.
intros e1_real e1_float e2_real e2_float mult_real mult_float.
(* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
inversion mult_real; subst;
destruct m0; destruct m3; inversion H2;
simpl in H3; rewrite Q2R0_is_0 in H3; auto.
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
rewrite delta_0_deterministic in mult_real; auto.
rewrite delta_0_deterministic; auto.
unfold evalBinop in *; simpl in *.
......@@ -219,8 +223,9 @@ Proof.
intros e1_real e1_float e2_real e2_float div_real div_float.
(* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
inversion div_real; subst;
destruct m0; destruct m3; inversion H2;
simpl in H3; rewrite Q2R0_is_0 in H3; auto.
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
rewrite delta_0_deterministic in div_real; auto.
rewrite delta_0_deterministic; auto.
unfold evalBinop in *; simpl in *.
......
This diff is collapsed.
......@@ -259,7 +259,7 @@ Inductive eval_exp (E:env) (Gamma: nat -> option mType) :(exp R) -> R -> mType -
Hint Constructors eval_exp.
(**
Show some simpler rule lemmata
Show some simpler (more general) rule lemmata
**)
Lemma Const_dist' m n delta v m' E Gamma:
Rle (Rabs delta) (Q2R (mTypeToQ m)) ->
......@@ -276,7 +276,7 @@ Lemma Unop_neg' m f1 v1 v m' E Gamma:
eval_exp E Gamma f1 v1 m ->
v = evalUnop Neg v1 ->
m' = m ->
eval_exp E Gamma (Unop Neg f1) (evalUnop Neg v1) m'.
eval_exp E Gamma (Unop Neg f1) v m'.
Proof.
intros; subst; auto.
Qed.
......@@ -336,6 +336,27 @@ Fixpoint usedVars (V:Type) (e:exp V) :NatSet.t :=
| _ => NatSet.empty
end.
Lemma toRMap_eval_M0 f v E Gamma m:
eval_exp E (toRMap Gamma) (toREval f) v m -> m = M0.
Proof.
revert v E Gamma m.
induction f; intros * eval_f; inversion eval_f; subst;
repeat
match goal with
| H: context[toRMap _ _] |- _ => unfold toRMap in H
| H: context[match ?Gamma ?v with | _ => _ end ] |- _ => destruct (Gamma v) eqn:?
| H: Some ?m1 = Some ?m2 |- _ => inversion H; try auto
| H: None = Some ?m |- _ => inversion H
end; try auto.
- eapply IHf; eauto.
- eapply IHf; eauto.
- assert (m1 = M0)
by (eapply IHf1; eauto).
assert (m2 = M0)
by (eapply IHf2; eauto);
subst; auto.
Qed.
(**
If |delta| <= 0 then perturb v delta is exactly v.
**)
......@@ -352,8 +373,8 @@ Evaluation with 0 as machine epsilon is deterministic
**)
Lemma meps_0_deterministic (f:exp R) (E:env) Gamma:
forall v1 v2,
eval_exp E Gamma (toREval f) v1 M0 ->
eval_exp E Gamma (toREval f) v2 M0 ->
eval_exp E (toRMap Gamma) (toREval f) v1 M0 ->
eval_exp E (toRMap Gamma) (toREval f) v2 M0 ->
v1 = v2.
Proof.
induction f;
......@@ -372,8 +393,11 @@ Proof.
rewrite Q2R0_is_0 in *;
repeat (rewrite delta_0_deterministic; try auto).
- inversion ev1; inversion ev2; subst.
apply M0_join_is_M0 in H11; apply M0_join_is_M0 in H2.
destruct H2, H11; subst.
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m1 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m2 = M0) by (eapply toRMap_eval_M0; eauto).
subst.
rewrite (IHf1 v0 v4); try auto.
rewrite (IHf2 v3 v5); try auto.
simpl in *.
......@@ -394,19 +418,31 @@ For each evaluation of using an arbitrary epsilon, we can replace it by
evaluating the subexpressions and then binding the result values to different
variables in the Environment.
**)
Lemma binary_unfolding b f1 f2 E v1 v2 m1 m2 Gamma:
Lemma binary_unfolding b f1 f2 E v1 v2 m1 m2 Gamma delta:
(b = Div -> ~(v2 = 0 )%R) ->
(Rabs delta <= Q2R (mTypeToQ (join m1 m2)))%R ->
eval_exp E Gamma f1 v1 m1 ->
eval_exp E Gamma f2 v2 m2 ->
eval_exp E Gamma (Binop b f1 f2) (perturb (evalBinop b v1 v2) (Q2R (mTypeToQ (join m1 m2)))) (join m1 m2) ->
eval_exp E Gamma (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta) (join m1 m2) ->
eval_exp (updEnv 2 v2 (updEnv 1 v1 emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 Gamma))
(Binop b (Var R 1) (Var R 2)) (perturb (evalBinop b v1 v2) (Q2R (mTypeToQ (join m1 m2)))) (join m1 m2).
(Binop b (Var R 1) (Var R 2)) (perturb (evalBinop b v1 v2) delta) (join m1 m2).
Proof.
intros no_div_zero eval_f1 eval_f2 eval_float.
econstructor; try auto.
rewrite Rabs_right; try lra.
auto using Rle_ge, mTypeToQ_pos_R.
Qed.
Lemma eval_eq_env e:
forall E1 E2 Gamma v m,
(forall x, E1 x = E2 x) ->
eval_exp E1 Gamma e v m ->
eval_exp E2 Gamma e v m.
Proof.
induction e; intros;
(match_pat (eval_exp _ _ _ _ _) (fun H => inversion H; subst; simpl in *));
try eauto.
eapply Var_load; auto.
rewrite <- (H n); auto.
Qed.
(*
......
(* TODO: Flocq ops open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory *)
Require Import Coq.QArith.QArith Coq.QArith.Qreals Coq.Reals.Reals Coq.micromega.Psatz.
Require Import Daisy.Infra.MachineType Daisy.Typing Daisy.Infra.RealSimps Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Commands Daisy.Environments Daisy.ssaPrgs Daisy.Infra.Ltacs Daisy.Infra.RealRationalProps.
Fixpoint FPRangeValidator (e:exp Q) (A:analysisResult) typeMap dVars {struct e} : bool :=
match typeMap e with
|Some m =>
let (iv_e, err_e) := A e in
let iv_e_float := widenIntv iv_e err_e in
let recRes :=
match e with
| Binop b e1 e2 =>
FPRangeValidator e1 A typeMap dVars &&
FPRangeValidator e2 A typeMap dVars
| Unop u e =>
FPRangeValidator e A typeMap dVars
| Downcast m e => FPRangeValidator e A typeMap dVars
| _ => true
end
in
match e with
| Var _ v =>
if NatSet.mem v dVars
then true
else
if (validValue (ivhi iv_e_float) m &&
validValue (ivlo iv_e_float) m)
then ((normal (ivlo iv_e_float) m) || (Qeq_bool (ivlo iv_e_float) 0)) &&
(normal (ivhi iv_e_float) m || (Qeq_bool (ivhi iv_e_float) 0)) && recRes
else
false
| _ => if (validValue (ivhi iv_e_float) m &&
validValue (ivlo iv_e_float) m)
then ((normal (ivlo iv_e_float) m) || (Qeq_bool (ivlo iv_e_float) 0)) &&
(normal (ivhi iv_e_float) m || (Qeq_bool (ivhi iv_e_float) 0)) && recRes
else
false
end
| None => false
end.
Fixpoint FPRangeValidatorCmd (f:cmd Q) (A:analysisResult) typeMap dVars :=
match f with
| Let m n e g =>
if FPRangeValidator e A typeMap dVars
then FPRangeValidatorCmd g A typeMap (NatSet.add n dVars)
else false
| Ret e => FPRangeValidator e A typeMap dVars
end.
Ltac prove_fprangeval m v L1 R:=
destruct m eqn:?; try auto;
unfold normal, Normal, validValue, Denormal in *; canonize_hyps;
rewrite orb_true_iff in *;
destruct L1; destruct R; canonize_hyps;
rewrite <- Rabs_eq_Qabs in *;
Q2R_to_head;
rewrite <- Q2R_minus, <- Q2R_plus in *;
repeat (match goal with
|H: _ = true |- _ => andb_to_prop H
end);
destruct (Req_dec v 0); try auto;
destruct (Rle_lt_dec (Rabs v) (Q2R (minValue m)))%R (* denormal case *);
try auto;
destruct (Rle_lt_dec (Rabs v) (Q2R (maxValue m)))%R; lra.
Theorem FPRangeValidator_sound:
forall (e:exp Q) E1 E2 Gamma v m A tMap P fVars dVars,
approxEnv E1 Gamma A fVars dVars E2 ->
eval_exp E2 Gamma (toRExp e) v m ->
typeCheck e Gamma tMap = true ->
validIntervalbounds e A P dVars = true ->
validErrorbound e tMap A dVars = true ->
FPRangeValidator e A tMap dVars = true ->
NatSet.Subset (NatSet.diff (usedVars e) dVars) fVars ->
(forall v, NatSet.In v fVars ->
exists vR, E1 v = Some vR /\ Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R ->
(forall v, NatSet.In v fVars \/ NatSet.In v dVars ->
exists m, Gamma v = Some m) ->
(forall v, NatSet.In v dVars ->
exists vR, E1 v = Some vR /\
Q2R (fst (fst (A (Var Q v)))) <= vR <= Q2R (snd (fst (A (Var Q v)))))%R ->
(forall v, NatSet.In v dVars ->
exists vF m, E2 v = Some vF /\ tMap (Var Q v) = Some m /\ validFloatValue vF m) ->
validFloatValue v m.
Proof.
intros *.
unfold FPRangeValidator.
intros.
destruct (A e) as [iv_e err_e] eqn:?;
destruct iv_e as [e_lo e_hi] eqn:?; simpl in *.
assert (tMap e = Some m)
as type_e
by (eapply typingSoundnessExp; eauto).
subst; simpl in *.
unfold validFloatValue.
assert (exists vR, eval_exp E1 (toRMap Gamma) (toREval (toRExp e)) vR M0 /\
Q2R (fst (fst (A e))) <= vR <= Q2R (snd (fst (A e))))%R
as eval_real_exists.
{ eapply validIntervalbounds_sound; eauto.
- intros; apply H8.
rewrite <- NatSet.mem_spec; auto.
- intros. apply H6.
rewrite <- NatSet.mem_spec; auto.
- intros. apply H7.
set_tac.
rewrite <- NatSet.union_spec; auto. }
destruct eval_real_exists as [vR [eval_real vR_bounded]].
assert (Rabs (vR - v) <= Q2R (snd (A e)))%R.
{ eapply validErrorbound_sound; eauto.
- intros * v1_dVar.
apply H8; set_tac.
- intros * v0_fVar.
apply H6. rewrite <- NatSet.mem_spec; auto.
- intros * v1_in_union.
apply H7; set_tac.
rewrite NatSet.union_spec in v1_in_union; auto.
- eauto ; instantiate (1:= e_hi).
instantiate (1:=e_lo). rewrite Heqp. reflexivity. }
rewrite Heqp in *; simpl in *.
destruct (distance_gives_iv (a:=vR) v (e:=Q2R err_e) (Q2R e_lo, Q2R e_hi))
as [v_in_errIv];
try auto.
unfold IVlo, IVhi in *; simpl in *.
assert (Rabs v <= Rabs (Q2R e_hi + Q2R err_e) \/
Rabs v <= Rabs (Q2R e_lo - Q2R err_e))%R
as abs_bounded
by (apply bounded_inAbs; auto).
destruct e;
unfold validFloatValue in *; simpl in *;
rewrite type_e, Heqp in *; simpl in *.
- destruct (n mem dVars) eqn:?; simpl in *.
+ destruct (H9 n); try set_tac.
destruct H12 as [m2 [env_eq [map_eq validVal]]].
inversion H0; subst.
rewrite env_eq in H14; inversion H14; subst.
rewrite map_eq in type_e; inversion type_e; subst; auto.
+ andb_to_prop H4.
prove_fprangeval m v L1 R.
- andb_to_prop H4.
prove_fprangeval m v L1 R.
- andb_to_prop H4.
prove_fprangeval m v L1 R.
- andb_to_prop H4.
prove_fprangeval m v L1 R.
- andb_to_prop H4.
prove_fprangeval m v L1 R.
Qed.
Lemma FPRangeValidatorCmd_sound (f:cmd Q):
forall E1 E2 Gamma v vR m A tMap P fVars dVars outVars,
approxEnv E1 Gamma A fVars dVars E2 ->
ssa f (NatSet.union fVars dVars) outVars ->
bstep (toREvalCmd (toRCmd f)) E1 (toRMap Gamma) vR m ->
bstep (toRCmd f) E2 Gamma v m ->
typeCheckCmd f Gamma tMap = true ->
validIntervalboundsCmd f A P dVars = true ->
validErrorboundCmd f tMap A dVars = true ->
FPRangeValidatorCmd f A tMap dVars = true ->
NatSet.Subset (NatSet.diff (freeVars f) dVars) fVars ->
(forall v,
NatSet.In v fVars ->
exists vR, E1 v = Some vR /\ Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R ->