Skip to content

GitLab

Commit 57805bbd authored by ='s avatar =
Browse files
Options

Merge branch 'rmonat/daisy-typing3' into mixed-certificates 

Conflicts:
	coq/CertificateChecker.v
	coq/ErrorBounds.v
	coq/ErrorValidation.v
	coq/Expressions.v
	coq/IntervalValidation.v
	coq/ssaPrgs.v
parents 98d9efcf c3d56410
Hide whitespace changes
Inline Side-by-side
Showing with 3465 additions and 977 deletions
coq/CertificateChecker.v
View file @ 57805bbd
......@@ -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.
Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments Daisy.Typing.
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) :=
if (validIntervalbounds e absenv P NatSet.empty)
then (validErrorbound e absenv NatSet.empty)
then (validErrorbound e (fun (e:exp Q) => typeExpression e) absenv NatSet.empty)
else false.
(**
......@@ -23,14 +23,14 @@ Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
the real valued execution respects the precondition.
**)
Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
forall (E1 E2:env) (vR:R) (vF:R) fVars,
forall (E1 E2:env) (vR:R) (vF:R) fVars m,
approxEnv E1 absenv fVars NatSet.empty E2 ->
(forall v, NatSet.mem v fVars = true ->
exists vR, E1 v = Some vR /\
exists vR, E1 v = Some (vR, M0) /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
NatSet.Subset (usedVars e) fVars ->
eval_exp 0%R E1 (toRExp e) vR ->
eval_exp (Q2R machineEpsilon) E2 (toRExp e) vF ->
NatSet.Subset (Expressions.usedVars e) fVars ->
eval_exp E1 (toREval (toRExp e)) vR M0 ->
eval_exp E2 (toRExp e) vF m ->
CertificateChecker e absenv P = true ->
(Rabs (vR - vF) <= Q2R (snd (absenv e)))%R.
(**
......@@ -38,8 +38,7 @@ Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
validator and the error bound validator.
**)
Proof.
intros E1 E2 vR vF fVars approxE1E2 P_valid fVars_subset eval_real eval_float
certificate_valid.
intros * approxE1E2 P_valid fVars_subset eval_real eval_float certificate_valid.
unfold CertificateChecker in certificate_valid.
rewrite <- andb_lazy_alt in certificate_valid.
andb_to_prop certificate_valid.
......@@ -48,30 +47,32 @@ Proof.
destruct iv as [ivlo ivhi].
rewrite absenv_eq; simpl.
eapply validErrorbound_sound; eauto.
- admit. (*eapply validTypeMap; eauto. *)
- hnf. intros a in_diff.
rewrite NatSet.diff_spec in in_diff.
apply fVars_subset.
destruct in_diff; auto.
- intros v v_in_empty.
- intros v m0 v_in_empty.
rewrite NatSet.mem_spec in v_in_empty.
inversion v_in_empty.
Qed.
Admitted.
(* Qed. *)
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) :=
if (validIntervalboundsCmd f absenv P NatSet.empty)
then (validErrorboundCmd f absenv NatSet.empty)
then (validErrorboundCmd f (fun e => typeExpression e) absenv NatSet.empty)
else false.
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P:
forall (E1 E2:env) outVars vR vF fVars,
forall (E1 E2:env) outVars vR vF fVars m,
approxEnv E1 absenv fVars NatSet.empty E2 ->
(forall v, NatSet.mem v fVars= true ->
exists vR, E1 v = Some vR /\
exists vR, E1 v = Some (vR, M0) /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
NatSet.Subset (Commands.freeVars f) fVars ->
ssa f fVars outVars ->
bstep (toRCmd f) E1 0 vR ->
bstep (toRCmd f) E2 (Q2R machineEpsilon) vF ->
bstep (toREvalCmd (toRCmd f)) E1 vR M0 ->
bstep (toRCmd f) E2 vF m ->
CertificateCheckerCmd f absenv P = true ->
(Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp f))))%R.
(**
......@@ -79,7 +80,7 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P:
validator and the error bound validator.
**)
Proof.
intros E1 E2 outVars vR vF fVars approxE1E2 P_valid fVars_subset ssa_f eval_real eval_float
intros * approxE1E2 P_valid fVars_subset ssa_f eval_real eval_float
certificate_valid.
unfold CertificateCheckerCmd in certificate_valid.
rewrite <- andb_lazy_alt in certificate_valid.
......@@ -89,6 +90,7 @@ Proof.
destruct iv as [ivlo ivhi].
rewrite absenv_eq; simpl.
eapply (validErrorboundCmd_sound); eauto.
- admit. (* eapply typeMapCmdValid; eauto.*)
- instantiate (1 := outVars).
eapply ssa_equal_set; try eauto.
hnf.
......@@ -101,7 +103,7 @@ Proof.
rewrite NatSet.diff_spec in in_diff.
destruct in_diff.
apply fVars_subset; auto.
- intros v v_in_empty.
- intros v m1 v_in_empty.
rewrite NatSet.mem_spec in v_in_empty.
inversion v_in_empty.
Qed.
Admitted.
\ No newline at end of file
coq/Commands.v
View file @ 57805bbd
......@@ -2,6 +2,7 @@
Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework
**)
Require Import Coq.Reals.Reals Coq.QArith.QArith.
Require Import Daisy.Expressions.
Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Infra.NatSet.
(**
......@@ -10,21 +11,67 @@ Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Infra.NatSet.
Only assignments and return statement
**)
Inductive cmd (V:Type) :Type :=
Let: nat -> exp V -> cmd V -> cmd V
Let: mType -> nat -> exp V -> cmd V -> cmd V
| Ret: exp V -> cmd V.
Fixpoint getRetExp (V:Type) (f:cmd V) :=
match f with
|Let m x e g => getRetExp g
| Ret e => e
end.
Fixpoint toRCmd (f:cmd Q) :=
match f with
|Let m x e g => Let m x (toRExp e) (toRCmd g)
|Ret e => Ret (toRExp e)
end.
Fixpoint toREvalCmd (f:cmd R) :=
match f with
|Let m x e g => Let M0 x (toREval e) (toREvalCmd g)
|Ret e => Ret (toREval e)
end.
(*| Nop: cmd V. *)
(*
UNUSED!
Small Step semantics for Daisy language
Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
let_s x e s E v eps:
eval_exp eps E e v ->
sstep (Let x e s) E eps s (updEnv x v E)
|ret_s e E v eps:
eval_exp eps E e v ->
sstep (Ret e) E eps (Nop R) (updEnv 0 v E).
*)
(**
Define big step semantics for the Daisy language, terminating on a "returned"
result value
**)
Inductive bstep : cmd R -> env -> R -> R -> Prop :=
let_b x e s E v eps res:
eval_exp eps E e v ->
bstep s (updEnv x v E) eps res ->
bstep (Let x e s) E eps res
|ret_b e E v eps:
eval_exp eps E e v ->
bstep (Ret e) E eps v.
(* meaning of this -> mType ??? *)
(* Inductive bstep : cmd R -> env -> R -> mType -> Prop := *)
(* let_b m x e s E v res: *)
(* eval_exp E e v m -> *)
(* bstep s (updEnv x m v E) res m -> *)
(* bstep (Let m x e s) E res m *)
(* |ret_b m e E v: *)
(* eval_exp E e v m -> *)
(* bstep (Ret e) E v m. *)
Inductive bstep : cmd R -> env -> R -> mType -> Prop :=
let_b m m' x e s E v res:
eval_exp E e v m ->
bstep s (updEnv x m v E) res m' ->
bstep (Let m x e s) E res m'
|ret_b m e E v:
eval_exp E e v m ->
bstep (Ret e) E v m.
(**
The free variables of a command are all used variables of expressions
......@@ -32,8 +79,8 @@ Inductive bstep : cmd R -> env -> R -> R -> Prop :=
**)
Fixpoint freeVars V (f:cmd V) :NatSet.t :=
match f with
| Let x e g => NatSet.remove x (NatSet.union (usedVars e) (freeVars g))
| Ret e => usedVars e
| Let _ x e1 g => NatSet.remove x (NatSet.union (Expressions.usedVars e1) (freeVars g))
| Ret e => Expressions.usedVars e
end.
(**
......@@ -41,7 +88,7 @@ Fixpoint freeVars V (f:cmd V) :NatSet.t :=
**)
Fixpoint definedVars V (f:cmd V) :NatSet.t :=
match f with
| Let x _ g => NatSet.add x (definedVars g)
| Let _ x _ g => NatSet.add x (definedVars g)
| Ret _ => NatSet.empty
end.
......@@ -51,6 +98,6 @@ Fixpoint definedVars V (f:cmd V) :NatSet.t :=
**)
Fixpoint liveVars V (f:cmd V) :NatSet.t :=
match f with
| Let _ e g => NatSet.union (usedVars e) (liveVars g)
| Let _ _ e g => NatSet.union (usedVars e) (liveVars g)
| Ret e => usedVars e
end.
\ No newline at end of file
coq/Environments.v
View file @ 57805bbd
......@@ -15,21 +15,21 @@ expression may yield different values for different machine epsilons
Inductive approxEnv : env -> analysisResult -> NatSet.t -> NatSet.t -> env -> Prop :=
|approxRefl A:
approxEnv emptyEnv A NatSet.empty NatSet.empty emptyEnv
|approxUpdFree E1 E2 A v1 v2 x fVars dVars:
|approxUpdFree E1 E2 A v1 v2 x fVars dVars m:
approxEnv E1 A fVars dVars E2 ->
(Rabs (v1 - v2) <= Rabs v1 * Q2R machineEpsilon)%R ->
(Rabs (v1 - v2) <= (Rabs v1) * Q2R (meps m))%R ->
NatSet.mem x (NatSet.union fVars dVars) = false ->
approxEnv (updEnv x v1 E1) A (NatSet.add x fVars) dVars (updEnv x v2 E2)
|approxUpdBound E1 E2 A v1 v2 x fVars dVars:
approxEnv (updEnv x M0 v1 E1) A (NatSet.add x fVars) dVars (updEnv x m v2 E2)
|approxUpdBound E1 E2 A v1 v2 x fVars dVars m:
approxEnv E1 A fVars dVars E2 ->
(Rabs (v1 - v2) <= Q2R (snd (A (Var Q x))))%R ->
(Rabs (v1 - v2) <= Q2R (snd (A (Var Q m x))))%R ->
NatSet.mem x (NatSet.union fVars dVars) = false ->
approxEnv (updEnv x v1 E1) A fVars (NatSet.add x dVars) (updEnv x v2 E2).
approxEnv (updEnv x M0 v1 E1) A fVars (NatSet.add x dVars) (updEnv x m v2 E2).
Inductive approxParams :env -> R -> env -> Prop :=
|approxParamRefl eps:
approxParams emptyEnv eps emptyEnv
|approxParamUpd E1 E2 eps x v1 v2 :
approxParams E1 eps E2 ->
(Rabs (v1 - v2) <= eps)%R ->
approxParams (updEnv x v1 E1) eps (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).
coq/ErrorBounds.v
View file @ 57805bbd
......@@ -7,10 +7,10 @@ Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps.
Require Import Daisy.Environments Daisy.Infra.ExpressionAbbrevs.
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (absenv:analysisResult):
eval_exp 0%R E1 (Const n) nR ->
eval_exp (Q2R machineEpsilon) E2 (Const n) nF ->
(Rabs (nR - nF) <= Rabs n * (Q2R machineEpsilon))%R.
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (absenv:analysisResult) (m:mType):
eval_exp E1 (Const M0 n) nR M0 ->
eval_exp E2 (Const m n) nF m ->
(Rabs (nR - nF) <= Rabs n * (Q2R (meps m)))%R.
Proof.
intros eval_real eval_float.
inversion eval_real; subst.
......@@ -19,6 +19,9 @@ Proof.
unfold perturb; simpl.
rewrite Rabs_err_simpl, Rabs_mult.
apply Rmult_le_compat_l; [apply Rabs_pos | auto].
simpl (meps M0) in *.
apply (Rle_trans _ (Q2R 0) _); try auto.
rewrite Q2R0_is_0; lra.
Qed.
(*
......@@ -42,39 +45,41 @@ 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):
eval_exp 0%R E1 (toRExp e1) e1R ->
eval_exp (Q2R machineEpsilon) E2 (toRExp e1) e1F ->
eval_exp 0%R E1 (toRExp e2) e2R ->
eval_exp (Q2R machineEpsilon) E2 (toRExp e2) e2F ->
eval_exp 0%R E1 (Binop Plus (toRExp e1) (toRExp e2)) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Plus (Var R 1) (Var R 2)) vF ->
(vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType):
eval_exp E1 (toREval (toRExp e1)) e1R M0 ->
eval_exp E2 (toRExp e1) e1F m1->
eval_exp E1 (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 (toRExp e2) e2F m2 ->
eval_exp E1 (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) (Binop Plus (Var R m1 1) (Var R m2 2)) vF m->
(Rabs (e1R - e1F) <= Q2R err1)%R ->
(Rabs (e2R - e2F) <= Q2R err2)%R ->
(Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R machineEpsilon)))%R.
(Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R (meps m))))%R.
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.
rewrite delta_0_deterministic in plus_real; auto.
rewrite (delta_0_deterministic (evalBinop Plus v1 v2) delta); auto.
unfold evalBinop in *; simpl in *.
clear delta H2.
rewrite (meps_0_deterministic H3 e1_real);
rewrite (meps_0_deterministic H5 e2_real).
rewrite (meps_0_deterministic H3 e1_real) in plus_real.
rewrite (meps_0_deterministic H5 e2_real) in plus_real.
clear H3 H5 H6 v1 v2.
clear delta H3.
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
rewrite (meps_0_deterministic (toRExp e2) H6 e2_real).
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in plus_real.
rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in plus_real.
clear H5 H6 H7 v1 v2.
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
inversion plus_float; subst.
unfold perturb; simpl.
inversion H3; subst; inversion H5; subst.
inversion H4; subst; inversion H7; subst.
unfold updEnv; simpl.
unfold updEnv in H0,H1; simpl in *.
symmetry in H0, H1.
inversion H0; inversion H1; subst.
unfold updEnv in H6,H9; simpl in *.
symmetry in H6,H9.
inversion H6; inversion H9; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear plus_float H3 H5 plus_real e1_real e1_float e2_real e2_float H0 H1.
clear plus_float H4 H7 plus_real e1_real e1_float e2_real e2_float H8 H6 H9.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rsub_eq_Ropp_Rplus.
......@@ -97,7 +102,7 @@ Proof.
eapply Rle_trans.
eapply Rmult_le_compat_l.
apply Rabs_pos.
apply H2.
apply H3.
apply Req_le; auto.
Qed.
......@@ -105,39 +110,41 @@ Qed.
Copy-Paste proof with minor differences, was easier then manipulating the evaluations and then applying the lemma
**)
Lemma subtract_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:
eval_exp 0%R E1 (toRExp e1) e1R ->
eval_exp (Q2R machineEpsilon) E2 (toRExp e1) e1F ->
eval_exp 0%R E1 (toRExp e2) e2R ->
eval_exp (Q2R machineEpsilon) E2 (toRExp e2) e2F ->
eval_exp 0%R E1 (Binop Sub (toRExp e1) (toRExp e2)) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Sub (Var R 1) (Var R 2)) vF ->
(e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m m1 m2:mType):
eval_exp E1 (toREval (toRExp e1)) e1R M0 ->
eval_exp E2 (toRExp e1) e1F m1 ->
eval_exp E1 (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 (toRExp e2) e2F m2 ->
eval_exp E1 (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) (Binop Sub (Var R m1 1) (Var R m2 2)) vF m ->
(Rabs (e1R - e1F) <= Q2R err1)%R ->
(Rabs (e2R - e2F) <= Q2R err2)%R ->
(Rabs (vR - vF) <= Q2R err1 + Q2R err2 + ((Rabs (e1F - e2F)) * (Q2R machineEpsilon)))%R.
(Rabs (vR - vF) <= Q2R err1 + Q2R err2 + ((Rabs (e1F - e2F)) * (Q2R (meps m))))%R.
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.
inversion sub_real; subst;
destruct m0; destruct m3; inversion H2;
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 *.
clear delta H2.
rewrite (meps_0_deterministic H3 e1_real);
rewrite (meps_0_deterministic H5 e2_real).
rewrite (meps_0_deterministic H3 e1_real) in sub_real.
rewrite (meps_0_deterministic H5 e2_real) in sub_real.
clear H3 H5 H6 v1 v2.
clear delta H3.
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
rewrite (meps_0_deterministic (toRExp e2) H6 e2_real).
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in sub_real.
rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in sub_real.
clear H5 H6 H7 v1 v2.
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
inversion sub_float; subst.
unfold perturb; simpl.
inversion H3; subst; inversion H5; subst.
inversion H4; subst; inversion H7; subst.
unfold updEnv; simpl.
symmetry in H0, H1.
unfold updEnv in H0, H1; simpl in H0, H1.
inversion H0; inversion H1; subst.
symmetry in H6, H9.
unfold updEnv in H6, H9; simpl in H6, H9.
inversion H6; inversion H9; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear sub_float H3 H5 sub_real e1_real e1_float e2_real e2_float H0 H1.
clear sub_float H4 H7 sub_real e1_real e1_float e2_real e2_float H6 H9 H8.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
repeat rewrite Rsub_eq_Ropp_Rplus.
......@@ -161,36 +168,37 @@ Proof.
Qed.
Lemma mult_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env):
eval_exp 0%R E1 (toRExp e1) e1R ->
eval_exp (Q2R machineEpsilon) E2 (toRExp e1) e1F ->
eval_exp 0%R E1 (toRExp e2) e2R ->
eval_exp (Q2R machineEpsilon) E2 (toRExp e2) e2F ->
eval_exp 0%R E1 (Binop Mult (toRExp e1) (toRExp e2)) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Mult (Var R 1) (Var R 2)) vF ->
(Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R machineEpsilon))%R.
(vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType):
eval_exp E1 (toREval (toRExp e1)) e1R M0 ->
eval_exp E2 (toRExp e1) e1F m1 ->
eval_exp E1 (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 (toRExp e2) e2F m2 ->
eval_exp E1 (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) (Binop Mult (Var R m1 1) (Var R m2 2)) vF m->
(Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R (meps m)))%R.
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.
inversion mult_real; subst;
destruct m0; destruct m3; inversion H2;
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 *.
clear delta H2.
rewrite (meps_0_deterministic H3 e1_real);
rewrite (meps_0_deterministic H5 e2_real).
rewrite (meps_0_deterministic H3 e1_real) in mult_real.
rewrite (meps_0_deterministic H5 e2_real) in mult_real.
clear H3 H5 H6 v1 v2.
clear delta H3.
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
rewrite (meps_0_deterministic (toRExp e2) H6 e2_real).
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in mult_real.
rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in mult_real.
clear H5 H6 v1 v2 H7 H2.
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
inversion mult_float; subst.
unfold perturb; simpl.
inversion H3; subst; inversion H5; subst.
symmetry in H0, H1;
inversion H3; subst; inversion H6; subst.
unfold updEnv in *; simpl in *.
inversion H0; inversion H1; subst.
inversion H5; inversion H8; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear mult_float H3 H5 mult_real e1_real e1_float e2_real e2_float H0 H1.
clear mult_float H7 H8 mult_real e1_real e1_float e2_real e2_float H5 H8.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rsub_eq_Ropp_Rplus.
......@@ -208,36 +216,37 @@ Proof.
Qed.
Lemma div_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env):
eval_exp 0%R E1 (toRExp e1) e1R ->
eval_exp (Q2R machineEpsilon) E2 (toRExp e1) e1F ->
eval_exp 0%R E1 (toRExp e2) e2R ->
eval_exp (Q2R machineEpsilon) E2 (toRExp e2) e2F ->
eval_exp 0%R E1 (Binop Div (toRExp e1) (toRExp e2)) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Div (Var R 1) (Var R 2)) vF ->
(Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R machineEpsilon))%R.
(vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType):
eval_exp E1 (toREval (toRExp e1)) e1R M0 ->
eval_exp E2 (toRExp e1) e1F m1 ->
eval_exp E1 (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 (toRExp e2) e2F m2 ->
eval_exp E1 (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) (Binop Div (Var R m1 1) (Var R m2 2)) vF m ->
(Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R (meps m)))%R.
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.
inversion div_real; subst;
destruct m0; destruct m3; inversion H2;
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 *.
clear delta H2.
rewrite (meps_0_deterministic H3 e1_real);
rewrite (meps_0_deterministic H5 e2_real).
rewrite (meps_0_deterministic H3 e1_real) in div_real.
rewrite (meps_0_deterministic H5 e2_real) in div_real.
clear H3 H5 H6 v1 v2.
clear delta H3 H2.
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
rewrite (meps_0_deterministic (toRExp e2) H6 e2_real).
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in div_real.
rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in div_real.
(* clear H5 H6 v1 v2. *)
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
inversion div_float; subst.
unfold perturb; simpl.
inversion H3; subst; inversion H5; subst.
symmetry in H0, H1;
inversion H3; subst; inversion H9; subst.
unfold updEnv in *; simpl in *.
inversion H0; inversion H1; subst.
inversion H8; inversion H11; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear div_float H3 H5 div_real e1_real e1_float e2_real e2_float H0 H1.
clear div_float H8 H11 div_real e1_real e1_float e2_real e2_float.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rsub_eq_Ropp_Rplus.
......@@ -431,3 +440,29 @@ Proof.
auto.
rewrite Q2R0_is_0; auto.
Qed.
Lemma round_abs_err_bounded (e:exp R) (nR nF1 nF:R) (E1 E2: env) (err:R) (machineEpsilon m:mType):
eval_exp E1 (toREval e) nR M0 ->
eval_exp E2 e nF1 m ->
eval_exp (updEnv 1 m nF1 emptyEnv) (toRExp (Downcast machineEpsilon (Var Q m 1))) nF machineEpsilon->
(Rabs (nR - nF1) <= err)%R ->
(Rabs (nR - nF) <= err + (Rabs nF1) * Q2R (meps machineEpsilon))%R.
Proof.
intros eval_real eval_float eval_float_rnd err_bounded.
replace (nR - nF)%R with ((nR - nF1) + (nF1 - nF))%R by lra.
eapply Rle_trans.
apply (Rabs_triang (nR - nF1) (nF1 - nF)).
apply (Rle_trans _ (err + Rabs (nF1 - nF)) _).
- apply Rplus_le_compat_r; assumption.
- apply Rplus_le_compat_l.
inversion eval_float_rnd; subst.
inversion H5; subst.
inversion H7.
unfold perturb; simpl.
replace (v1 - v1 * (1 + delta))%R with (- (v1 * delta))%R by lra.
replace (Rabs (-(v1*delta))) with (Rabs (v1*delta)) by (symmetry; apply Rabs_Ropp).
rewrite Rabs_mult.
apply Rmult_le_compat_l.
+ apply Rabs_pos.
+ auto.
Qed.
coq/ErrorValidation.v
View file @ 57805bbd
......@@ -9,63 +9,70 @@
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals Coq.Lists.List.
Require Import Coq.micromega.Psatz Coq.Reals.Reals.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.RealSimps Daisy.Infra.Ltacs.
Require Import Daisy.Environments Daisy.IntervalValidation Daisy.ErrorBounds.
Require Import Daisy.Environments Daisy.IntervalValidation Daisy.Typing Daisy.ErrorBounds.