Commit 7dd4f12f authored by Nikita Zyuzin's avatar Nikita Zyuzin

Merge branch 'certificates' of https://gitlab.mpi-sws.org/AVA/daisy into fma_proofs_merge

Conflicts:
	coq/ErrorValidation.v
	coq/Expressions.v
	coq/FPRangeValidator.v
	coq/IEEE_connection.v
	coq/Infra/Ltacs.v
	coq/IntervalValidation.v
	coq/Typing.v
parents 5bbb6b4a 13ae6d87
......@@ -112,7 +112,7 @@ $ git submodule init
Then, initialize the CakeML submodule and start compilation:
```bash
$ git submodule update --recursive --remote
$ git submodule update --recursive
$ cd hol4/
$ Holmake
```
......
......@@ -13,9 +13,11 @@ 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) && FPRangeValidator e absenv (typeMap defVars e) NatSet.empty
then (validErrorbound e (typeMap defVars e) absenv NatSet.empty)
let tMap := (typeMap defVars e (DaisyMap.empty mType)) in
if (typeCheck e defVars tMap)
then
if (validIntervalbounds e absenv P NatSet.empty) && FPRangeValidator e absenv tMap NatSet.empty
then (validErrorbound e tMap absenv NatSet.empty)
else false
else false.
......@@ -27,19 +29,20 @@ Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) (def
Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P defVars:
forall (E1 E2:env),
approxEnv E1 defVars absenv (usedVars e) NatSet.empty E2 ->
(forall v, NatSet.mem v (Expressions.usedVars e) = true ->
(forall v, NatSet.In v (Expressions.usedVars e) ->
exists vR, E1 v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
(forall v, (v) mem (usedVars e) = true ->
(forall v, NatSet.In v (usedVars e) ->
exists m : mType,
defVars v = Some m) ->
CertificateChecker e absenv P defVars = true ->
exists vR vF m,
eval_exp E1 (toRMap defVars) (toREval (toRExp e)) vR M0 /\
eval_exp E2 defVars (toRExp e) vF m /\
(forall vF m,
eval_exp E2 defVars (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R (snd (absenv e))))%R.
exists iv err vR vF m,
DaisyMap.find e absenv = Some (iv, err) /\
eval_exp E1 (toRMap defVars) (toREval (toRExp e)) vR M0 /\
eval_exp E2 defVars (toRExp e) vF m /\
(forall vF m,
eval_exp E2 defVars (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R err))%R.
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
......@@ -49,55 +52,52 @@ Proof.
unfold CertificateChecker in certificate_valid.
rewrite <- andb_lazy_alt in certificate_valid.
andb_to_prop certificate_valid.
env_assert absenv e env_e.
destruct env_e as [iv [err absenv_eq]].
destruct iv as [ivlo ivhi].
rewrite absenv_eq; simpl.
pose proof (NatSetProps.empty_union_2 (Expressions.usedVars e) NatSet.empty_spec) as union_empty.
hnf in union_empty.
assert (forall v1, (v1) mem (Expressions.usedVars e NatSet.empty) = true ->
exists m0 : mType, defVars v1 = Some m0).
{ intros; eapply types_defined.
rewrite NatSet.mem_spec in *.
rewrite <- union_empty; eauto. }
assert (dVars_range_valid NatSet.empty E1 absenv).
{ unfold dVars_range_valid.
intros; set_tac. }
assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)).
{ hnf; intros a in_empty.
set_tac. }
assert (vars_typed (usedVars e NatSet.empty) defVars).
{ unfold vars_typed. intros; apply types_defined. set_tac. destruct H1; set_tac.
split; try auto. hnf; intros; set_tac. }
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 L1 H1 P_valid H absenv_eq) as [[vF [mF eval_float]] err_bounded]; auto.
exists vR; exists vF; exists mF; split; auto.
edestruct (validIntervalbounds_sound e (A:=absenv) (P:=P) (fVars:=usedVars e) (dVars:=NatSet.empty) (Gamma:=defVars) (E:=E1))
as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]]; eauto.
destruct iv_e as [elo ehi].
edestruct (validErrorbound_sound e (typeMap defVars e (DaisyMap.empty mType)) L approxE1E2 H0 eval_real R0 L1 H P_valid H1 map_e) as [[vF [mF eval_float]] err_bounded]; auto.
exists (elo, ehi), err_e, vR, vF, 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))
let tMap := typeMapCmd defVars f (DaisyMap.empty mType) in
if (typeCheckCmd f defVars tMap && validSSA f (freeVars f))
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)
FPRangeValidatorCmd f absenv tMap NatSet.empty
then (validErrorboundCmd f tMap absenv NatSet.empty)
else false
else false.
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P defVars:
forall (E1 E2:env),
approxEnv E1 defVars absenv (freeVars f) NatSet.empty E2 ->
(forall v, NatSet.mem v (freeVars f)= true ->
(forall v, NatSet.In v (freeVars f) ->
exists vR, E1 v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
(forall v, (v) mem (freeVars f) = true ->
(forall v, NatSet.In v (freeVars f) ->
exists m : mType,
defVars v = Some m) ->
CertificateCheckerCmd f absenv P defVars = true ->
exists vR vF m,
exists iv err vR vF m,
DaisyMap.find (getRetExp f) absenv = Some (iv,err) /\
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR M0 /\
bstep (toRCmd f) E2 defVars vF m /\
(forall vF m,
bstep (toRCmd f) E2 defVars vF m ->
(Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp f))))%R).
(Rabs (vR - vF) <= Q2R (err))%R).
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
......@@ -109,32 +109,25 @@ Proof.
andb_to_prop certificate_valid.
apply validSSA_sound in R0.
destruct R0 as [outVars ssa_f].
env_assert absenv (getRetExp f) env_f.
destruct env_f as [iv [err absenv_eq]].
destruct iv as [ivlo ivhi].
assert (ssa f (freeVars f NatSet.empty) outVars) as ssa_valid.
{ 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.
{ intros v v_in_empty.
set_tac. inversion v_in_empty. }
assert (forall v, (v) mem (freeVars f NatSet.empty) = true ->
exists m : mType, defVars v = Some m) as types_valid.
{ intros v v_mem; apply types_defined.
set_tac. rewrite NatSet.union_spec in v_mem.
destruct v_mem; try auto.
inversion H. }
assert (dVars_range_valid NatSet.empty E1 absenv).
{ unfold dVars_range_valid.
intros; set_tac. }
assert (vars_typed (freeVars f NatSet.empty) defVars).
{ unfold vars_typed. intros; apply types_defined. set_tac.
destruct H0; set_tac. }
assert (NatSet.Subset (freeVars f -- NatSet.empty) (freeVars f))
as freeVars_contained by set_tac.
edestruct (validIntervalboundsCmd_sound) as [vR [eval_real bounded_real_f]] ; eauto.
rewrite absenv_eq; simpl.
edestruct (validIntervalboundsCmd_sound)
as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]]; eauto.
destruct iv as [f_lo f_hi].
edestruct validErrorboundCmd_gives_eval as [vF [mF eval_float]]; eauto.
exists vR; exists vF; exists mF; split; try auto.
split; try auto.
exists (f_lo, f_hi), err, vR, vF, mF; split; try auto.
split; try auto; split; try auto.
intros.
eapply validErrorboundCmd_sound; eauto.
Qed.
\ No newline at end of file
......@@ -20,124 +20,113 @@ Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t
(Rabs (v1 - v2) <= (Rabs v1) * Q2R (mTypeToQ m))%R ->
NatSet.mem x (NatSet.union fVars dVars) = false ->
approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A (NatSet.add x fVars) dVars (updEnv x v2 E2)
|approxUpdBound E1 E2 defVars A v1 v2 x fVars dVars m:
|approxUpdBound E1 E2 defVars A v1 v2 x fVars dVars m iv err:
approxEnv E1 defVars A fVars dVars E2 ->
(Rabs (v1 - v2) <= Q2R (snd (A (Var Q x))))%R ->
DaisyMap.find (Var Q x) A = Some (iv, err) ->
(Rabs (v1 - v2) <= Q2R err)%R ->
NatSet.mem x (NatSet.union fVars dVars) = false ->
approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A fVars (NatSet.add x dVars) (updEnv x v2 E2).
(* Inductive approxParams :env -> env -> Prop := *)
(* |approxParamRefl: *)
(* approxParams emptyEnv emptyEnv *)
(* |approxParamUpd E1 E2 m x v1 v2 : *)
(* approxParams E1 E2 -> *)
(* (Rabs (v1 - v2) <= Q2R (meps m))%R -> *)
(* approxParams (updEnv x M0 v1 E1) (updEnv x m v2 E2). *)
Section RelationProperties.
Variable (x:nat) (v:R) (E1 E2:env) (Gamma:nat -> option mType) (A:analysisResult) (fVars dVars: NatSet.t).
Variable (x:nat) (v:R) (E1 E2:env) (Gamma:nat -> option mType)
(A:analysisResult) (fVars dVars: NatSet.t).
Hypothesis approxEnvs: approxEnv E1 Gamma A fVars dVars E2.
Lemma approxEnv_gives_value:
E1 x = Some v ->
NatSet.In x (NatSet.union fVars dVars) ->
exists v',
E2 x = Some v'.
Proof.
induction approxEnvs;
intros E1_def x_valid.
- unfold emptyEnv in E1_def; simpl in E1_def. congruence.
- unfold updEnv in *.
case_eq (x =? x0); intros eq_case; rewrite eq_case in *.
+ eexists; eauto.
+ eapply IHa; auto.
set_tac.
rewrite NatSet.union_spec in x_valid.
destruct x_valid; set_tac.
rewrite NatSet.add_spec in H1.
destruct H1; subst; try auto.
rewrite Nat.eqb_refl in eq_case; congruence.
- unfold updEnv in *.
case_eq (x =? x0); intros eq_case; rewrite eq_case in *.
+ eexists; eauto.
+ eapply IHa; auto.
set_tac.
rewrite NatSet.union_spec in x_valid.
destruct x_valid; set_tac.
rewrite NatSet.add_spec in H1.
destruct H1; subst; try auto.
rewrite Nat.eqb_refl in eq_case; congruence.
Qed.
Lemma approxEnv_gives_value:
E1 x = Some v ->
NatSet.In x (NatSet.union fVars dVars) ->
exists v',
E2 x = Some v'.
Proof.
induction approxEnvs;
intros E1_def x_valid.
- unfold emptyEnv in E1_def; simpl in E1_def. congruence.
- unfold updEnv in *.
case_eq (x =? x0); intros eq_case; rewrite eq_case in *.
+ eexists; eauto.
+ eapply IHa; eauto.
set_tac.
destruct x_valid; set_tac.
destruct H1 as [? | [? ?]]; subst; try auto.
rewrite Nat.eqb_refl in eq_case; congruence.
- unfold updEnv in *.
case_eq (x =? x0); intros eq_case; rewrite eq_case in *.
+ eexists; eauto.
+ eapply IHa; auto.
set_tac.
destruct x_valid; set_tac.
destruct H2 as [? | [ ? ?]]; subst; try auto.
rewrite Nat.eqb_refl in eq_case; congruence.
Qed.
Arguments mTypeToQ _ : simpl nomatch.
Arguments mTypeToQ _ : simpl nomatch.
Lemma approxEnv_fVar_bounded v2 m:
E1 x = Some v ->
E2 x = Some v2 ->
NatSet.In x fVars ->
Gamma x = Some m ->
(Rabs (v - v2) <= (Rabs v) * Q2R (mTypeToQ m))%R.
Proof.
induction approxEnvs;
intros E1_def E2_def x_free x_typed.
- unfold emptyEnv in *; simpl in *; congruence.
- set_tac.
rewrite add_spec_strong in x_free.
destruct x_free as [x_x0 | [x_neq x_free]]; subst.
+ unfold updEnv in *;
rewrite Nat.eqb_refl in *; simpl in *.
unfold updDefVars in x_typed.
rewrite Nat.eqb_refl in x_typed.
inversion x_typed; subst.
inversion E1_def; inversion E2_def; subst; auto.
+ unfold updEnv in *; simpl in *.
rewrite <- Nat.eqb_neq in x_neq.
rewrite x_neq in *; simpl in *.
unfold updDefVars in x_typed; rewrite x_neq in x_typed.
Lemma approxEnv_fVar_bounded v2 m:
E1 x = Some v ->
E2 x = Some v2 ->
NatSet.In x fVars ->
Gamma x = Some m ->
(Rabs (v - v2) <= (Rabs v) * Q2R (mTypeToQ m))%R.
Proof.
induction approxEnvs;
intros E1_def E2_def x_free x_typed.
- unfold emptyEnv in *; simpl in *; congruence.
- set_tac.
destruct x_free as [x_x0 | [x_neq x_free]]; subst.
+ unfold updEnv in *;
rewrite Nat.eqb_refl in *; simpl in *.
unfold updDefVars in x_typed.
rewrite Nat.eqb_refl in x_typed.
inversion x_typed; subst.
inversion E1_def; inversion E2_def; subst; auto.
+ unfold updEnv in *; simpl in *.
rewrite <- Nat.eqb_neq in x_neq.
rewrite x_neq in *; simpl in *.
unfold updDefVars in x_typed; rewrite x_neq in x_typed.
apply IHa; auto.
- assert (x =? x0 = false) as x_x0_neq.
{ rewrite Nat.eqb_neq; hnf; intros; subst.
set_tac.
apply H1.
set_tac. }
unfold updEnv in *; rewrite x_x0_neq in *.
apply IHa; auto.
- assert (x =? x0 = false) as x_x0_neq.
{ rewrite Nat.eqb_neq; hnf; intros; subst.
set_tac.
apply H0.
set_tac. }
unfold updEnv in *; rewrite x_x0_neq in *.
apply IHa; auto.
unfold updDefVars in x_typed;
rewrite x_x0_neq in x_typed; auto.
Qed.
unfold updDefVars in x_typed;
rewrite x_x0_neq in x_typed; auto.
Qed.
Lemma approxEnv_dVar_bounded v2 m e:
E1 x = Some v ->
E2 x = Some v2 ->
NatSet.In x dVars ->
Gamma x = Some m ->
snd (A (Var Q x)) = e ->
(Rabs (v - v2) <= Q2R e)%R.
Proof.
induction approxEnvs;
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.
set_tac.
apply H0; set_tac.
}
unfold updEnv in *; rewrite x_x0_neq in *.
unfold updDefVars in x_typed; rewrite x_x0_neq in x_typed.
apply IHa; auto.
- set_tac.
rewrite add_spec_strong in x_def.
destruct x_def as [x_x0 | [x_neq x_def]]; subst.
+ unfold updEnv in *;
rewrite Nat.eqb_refl in *; simpl in *.
inversion E1_def; inversion E2_def; subst; auto.
+ unfold updEnv in *; simpl in *.
rewrite <- Nat.eqb_neq in x_neq.
rewrite x_neq in *; simpl in *.
unfold updDefVars in x_typed; rewrite x_neq in x_typed.
Lemma approxEnv_dVar_bounded v2 m iv e:
E1 x = Some v ->
E2 x = Some v2 ->
NatSet.In x dVars ->
Gamma x = Some m ->
DaisyMap.find (Var Q x) A = Some (iv, e) ->
(Rabs (v - v2) <= Q2R e)%R.
Proof.
induction approxEnvs;
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.
set_tac.
apply H0; set_tac.
}
unfold updEnv in *; rewrite x_x0_neq in *.
unfold updDefVars in x_typed; rewrite x_x0_neq in x_typed.
apply IHa; auto.
Qed.
- set_tac.
destruct x_def as [x_x0 | [x_neq x_def]]; subst.
+ unfold updEnv in *;
rewrite Nat.eqb_refl in *; simpl in *.
inversion E1_def; inversion E2_def; subst.
rewrite A_e in *; inversion H; auto.
+ unfold updEnv in *; simpl in *.
rewrite <- Nat.eqb_neq in x_neq.
rewrite x_neq in *; simpl in *.
unfold updDefVars in x_typed; rewrite x_neq in x_typed.
apply IHa; auto.
Qed.
End RelationProperties.
\ No newline at end of file
......@@ -6,23 +6,21 @@
encoded in the analysis result. The validator is used in the file
CertificateChecker.v to build the complete checker.
**)
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs
Coq.QArith.Qreals Coq.micromega.Psatz Coq.Reals.Reals.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps
Daisy.Infra.RealRationalProps Daisy.Infra.RealSimps
Daisy.Infra.Ltacs Daisy.Environments
Daisy.IntervalValidation Daisy.Typing Daisy.ErrorBounds.
From Coq
Require Import QArith.QArith QArith.Qminmax QArith.Qabs QArith.Qreals
micromega.Psatz Reals.Reals.
From Daisy
Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
Infra.RealSimps Infra.Ltacs Environments IntervalValidation Typing
ErrorBounds.
(** Error bound validator **)
Fixpoint validErrorbound (e:exp Q) (* analyzed expression *)
(typeMap:exp Q -> option mType) (* derived types for e *)
(typeMap:DaisyMap.t mType) (* derived types for e *)
(A:analysisResult) (* encoded result of Daisy *)
(dVars:NatSet.t) (* let-bound variables encountered previously *):=
let (intv, err) := (A e) in
let mopt := typeMap e in
match mopt with
| None => false
| Some m =>
match DaisyMap.find e A, DaisyMap.find e typeMap with
| Some (intv, err), Some m =>
if (Qleb 0 err) (* encoding soundness: errors are positive *)
then
match e with (* case analysis for the expression *)
......@@ -34,35 +32,41 @@ Fixpoint validErrorbound (e:exp Q) (* analyzed expression *)
Qleb (maxAbs intv * (mTypeToQ m)) err
|Unop Neg e1 =>
if (validErrorbound e1 typeMap A dVars)
then Qeq_bool err (snd (A e1))
then
match DaisyMap.find e1 A with
| Some (iv_e1, err1) => Qeq_bool err err1
| None => false
end
else false
|Unop Inv e1 => false
|Binop b e1 e2 =>
if ((validErrorbound e1 typeMap A dVars)
&& (validErrorbound e2 typeMap A dVars))
then
let (ive1, err1) := A e1 in
let (ive2, err2) := A e2 in
let errIve1 := widenIntv ive1 err1 in
let errIve2 := widenIntv ive2 err2 in
let upperBoundE1 := maxAbs ive1 in
let upperBoundE2 := maxAbs ive2 in
match b with
| Plus =>
Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * (mTypeToQ m)) err
| Sub =>
Qleb (err1 + err2 + (maxAbs (subtractIntv errIve1 errIve2)) * (mTypeToQ m)) err
| Mult =>
Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multIntv errIve1 errIve2)) * (mTypeToQ m)) err
| Div =>
if (((Qleb (ivhi errIve2) 0) && (negb (Qeq_bool (ivhi errIve2) 0))) ||
((Qleb 0 (ivlo errIve2)) && (negb (Qeq_bool (ivlo errIve2) 0))))
then
let upperBoundInvE2 := maxAbs (invertIntv ive2) in
let minAbsIve2 := minAbs (errIve2) in
let errInv := (1 / (minAbsIve2 * minAbsIve2)) * err2 in
Qleb ((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideIntv errIve1 errIve2)) * (mTypeToQ m)) err
else false
match DaisyMap.find e1 A, DaisyMap.find e2 A with
| Some (ive1, err1), Some (ive2, err2) =>
let errIve1 := widenIntv ive1 err1 in
let errIve2 := widenIntv ive2 err2 in
let upperBoundE1 := maxAbs ive1 in
let upperBoundE2 := maxAbs ive2 in
match b with
| Plus =>
Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * (mTypeToQ m)) err
| Sub =>
Qleb (err1 + err2 + (maxAbs (subtractIntv errIve1 errIve2)) * (mTypeToQ m)) err
| Mult =>
Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multIntv errIve1 errIve2)) * (mTypeToQ m)) err
| Div =>
if (((Qleb (ivhi errIve2) 0) && (negb (Qeq_bool (ivhi errIve2) 0))) ||
((Qleb 0 (ivlo errIve2)) && (negb (Qeq_bool (ivlo errIve2) 0))))
then
let upperBoundInvE2 := maxAbs (invertIntv ive2) in
let minAbsIve2 := minAbs (errIve2) in
let errInv := (1 / (minAbsIve2 * minAbsIve2)) * err2 in
Qleb ((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideIntv errIve1 errIve2)) * (mTypeToQ m)) err
else false
end
| _, _ => false
end
else false
| Fma e1 e2 e3 =>
......@@ -86,26 +90,34 @@ Fixpoint validErrorbound (e:exp Q) (* analyzed expression *)
|Downcast m1 e1 =>
if validErrorbound e1 typeMap A dVars
then
let (ive1, err1) := A e1 in
let errIve1 := widenIntv ive1 err1 in
(Qleb (err1 + maxAbs errIve1 * (mTypeToQ m1)) err)
match DaisyMap.find e1 A with
| Some (ive1, err1) =>
let errIve1 := widenIntv ive1 err1 in
(Qleb (err1 + maxAbs errIve1 * (mTypeToQ m1)) err)
| None => false
end
else
false
end
else false
| _, _ => false
end.
(** Error bound command validator **)
Fixpoint validErrorboundCmd (f:cmd Q) (* analyzed cmd with let's *)
(typeMap:exp Q -> option mType) (* inferred types *)
typeMap (* inferred types *)
(A:analysisResult) (* Daisy's encoded result *)
(dVars:NatSet.t) (* defined variables *)
: bool :=
match f with
|Let m x e g =>
if ((validErrorbound e typeMap A dVars) && (Qeq_bool (snd (A e)) (snd (A (Var Q x)))))
then validErrorboundCmd g typeMap A (NatSet.add x dVars)
else false
match DaisyMap.find e A, DaisyMap.find (Var Q x) A with
| Some (iv_e, err_e), Some (iv_x, err_x) =>
if ((validErrorbound e typeMap A dVars) && (Qeq_bool err_e err_x))
then validErrorboundCmd g typeMap A (NatSet.add x dVars)
else false
| _,_ => false
end
|Ret e => validErrorbound e typeMap A dVars
end.
......@@ -117,57 +129,52 @@ Arguments mTypeToQ _ :simpl nomatch.
This lemma enables us to deduce from each run of the validator the invariant
that when it succeeds, the errors must be positive.
**)
Lemma err_always_positive e tmap (absenv:analysisResult) iv err dVars:
validErrorbound e tmap absenv dVars = true ->
(iv,err) = absenv e ->
(0 <= Q2R err)%R.
Lemma err_always_positive e tmap (A:analysisResult) dVars iv err:
validErrorbound e tmap A dVars = true ->
DaisyMap.find e A = Some (iv,err) ->
(0 <= Q2R err)%R.
Proof.
destruct e; intros validErrorbound_e absenv_e;
unfold validErrorbound in validErrorbound_e;
rewrite <- absenv_e in validErrorbound_e; simpl in *;
repeat match goal with
| [H: context [match ?E with | Some _ => _ |None => _ end] |- _ ] => destruct (E) eqn:?; try congruence
| [H: context [if ?c then _ else _ ] |- _] => destruct (c) eqn:?; try congruence end;
canonize_hyps; auto.
destruct e; cbn; intros;
Daisy_compute; canonize_hyps;
auto.
Qed.
Lemma validErrorboundCorrectVariable_eval:
forall E1 E2 absenv (v:nat) e nR nlo nhi P fVars dVars Gamma expTypes,
Ltac destruct_ex H pat :=
match type of H with
| exists v, ?H' =>
let vFresh:=fresh v in
let fN := fresh "ex" in
destruct H as [vFresh fN];
destruct_ex fN pat
| _ => destruct H as pat
end.
Tactic Notation "destruct_smart" simple_intropattern(pat) hyp(H) := destruct_ex H pat.
Lemma validErrorboundCorrectVariable_eval E1 E2 A (v:nat) e nR nlo nhi P fVars
dVars Gamma expTypes:
eval_exp E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR M0 ->
typeCheck (Var Q v) Gamma expTypes = true ->
approxEnv E1 Gamma absenv fVars dVars E2 ->
validIntervalbounds (Var Q v) absenv P dVars = true ->
validErrorbound (Var Q v) expTypes absenv dVars = true ->
approxEnv E1 Gamma A fVars dVars E2 ->
validIntervalbounds (Var Q v) A P dVars = true ->
validErrorbound (Var Q v) expTypes A dVars = true ->
NatSet.Subset (NatSet.diff (usedVars (Var Q v)) dVars) fVars ->
(forall v1,
NatSet.mem v1 dVars = true ->
exists r, E1 v1 = Some r /\
(Q2R (fst (fst (absenv (Var Q v1)))) <= r <= Q2R (snd (fst (absenv (Var Q v1)))))%R) ->
(forall v1, NatSet.mem v1 fVars= true ->
exists r, E1 v1 = Some r /\
(Q2R (fst (P v1)) <= r <= Q2R (snd (P v1)))%R) ->
(forall v1 : NatSet.elt,
NatSet.mem v1 (NatSet.union fVars dVars) = true ->
exists m0 : mType, Gamma v1 = Some m0) ->
absenv (Var Q v) = ((nlo, nhi), e) ->
dVars_range_valid dVars E1 A ->
fVars_P_sound fVars E1 P ->
vars_typed (NatSet.union fVars dVars) Gamma ->