Commit 476f146c authored by Heiko Becker's avatar Heiko Becker

Rework Coq proofs, to get rid of specifying precondition validity for...

Rework Coq proofs, to get rid of specifying precondition validity for execution by adding this as a property of the semantics
parent 6c74ae4e
......@@ -23,9 +23,8 @@ Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
**)
Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
forall (cenv:env) (vR:R) (vF:R),
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e) vR ->
eval_exp (Q2R machineEpsilon) cenv (toRExp e) vF ->
eval_exp 0%R cenv P (toRExp e) vR ->
eval_exp (Q2R machineEpsilon) cenv P (toRExp e) vF ->
CertificateChecker e absenv P = true ->
(Rabs (vR - vF) <= Q2R (snd (absenv e)))%R.
(**
......@@ -33,7 +32,7 @@ Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
validator and the error bound validator.
**)
Proof.
intros cenv vR vF precondValid eval_real eval_float certificate_valid.
intros cenv vR vF eval_real eval_float certificate_valid.
unfold CertificateChecker in certificate_valid.
apply Is_true_eq_left in certificate_valid.
apply andb_prop_elim in certificate_valid.
......
......@@ -17,23 +17,23 @@ Let: nat -> exp V -> cmd V -> cmd V
(**
Small Step semantics for Daisy language, parametric by evaluation function.
**)
Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
let_s x e s env v eps:
eval_exp eps env e v ->
sstep (Let R x e s) env eps s (updEnv x v env)
|ret_s e v eps env:
eval_exp eps env e v ->
sstep (Ret R e) env eps (Nop R) (updEnv 0 v env).
Inductive sstep : cmd R -> env -> precond -> R -> cmd R -> env -> Prop :=
let_s x e s env P v eps:
eval_exp eps env P e v ->
sstep (Let R x e s) env P eps s (updEnv x v env)
|ret_s e env P v eps:
eval_exp eps env P e v ->
sstep (Ret R e) env P eps (Nop R) (updEnv 0 v env).
(**
Analogously define Big Step semantics for the Daisy language,
parametric by the evaluation function
**)
Inductive bstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
let_b x e s s' env v eps env2:
eval_exp eps env e v ->
bstep s (updEnv x v env) eps s' env2 ->
bstep (Let R x e s) env eps s' env2
|ret_b e v eps env:
eval_exp eps env e v ->
bstep (Ret R e) env eps (Nop R) (updEnv 0 v env).
\ No newline at end of file
Inductive bstep : cmd R -> env -> precond -> R -> cmd R -> env -> Prop :=
let_b x e s s' env P v eps env2:
eval_exp eps env P e v ->
bstep s (updEnv x v env) P eps s' env2 ->
bstep (Let R x e s) env P eps s' env2
|ret_b e env P v eps:
eval_exp eps env P e v ->
bstep (Ret R e) env P eps (Nop R) (updEnv 0 v env).
\ No newline at end of file
......@@ -13,28 +13,26 @@ It is necessary to have this relation, since two evaluations of the very same
expression may yield different values for different machine epsilons
(or environments that already only approximate each other)
**)
Inductive approxEnv : R -> env -> R -> env -> Prop :=
|approxRefl eps E: approxEnv eps E eps E
|approxUpd eps1 E1 eps2 E2 t x v1 v2: approxEnv eps1 E1 eps2 E2 ->
eval_exp eps1 E1 t v1 ->
eval_exp eps2 E2 t v2 ->
approxEnv eps1 (updEnv x v1 E1) eps2 (updEnv x v2 E2).
Inductive approxEnv : precond -> R -> env -> R -> env -> Prop :=
|approxRefl eps P E: approxEnv P eps E eps E
|approxUpd P eps1 E1 eps2 E2 t x v1 v2: approxEnv P eps1 E1 eps2 E2 ->
eval_exp eps1 E1 P t v1 ->
eval_exp eps2 E2 P t v2 ->
approxEnv P eps1 (updEnv x v1 E1) eps2 (updEnv x v2 E2).
(** TODO: Show small step preservation of sim **)
Lemma small_step_preserves_sim f g E1 E2 E1' E2' eps1 eps2:
approxEnv eps1 E1 eps2 E2 ->
sstep f E1 eps1 g E1' ->
sstep f E2 eps2 g E2' ->
approxEnv eps1 E1' eps2 E2'.
Lemma small_step_preserves_sim P f g E1 E2 E1' E2' eps1 eps2:
approxEnv P eps1 E1 eps2 E2 ->
sstep f E1 P eps1 g E1' ->
sstep f E2 P eps2 g E2' ->
approxEnv P eps1 E1' eps2 E2'.
Proof.
intros approxBefore.
induction f; intros stepLet1 stepLet2.
- inversion stepLet1; inversion stepLet2; subst.
eapply approxUpd.
apply approxBefore.
apply H6.
apply H14.
apply H7.
apply H16.
- inversion stepLet1; inversion stepLet2; subst.
eapply approxUpd.
apply approxBefore.
......
......@@ -6,10 +6,10 @@ Bounds are explained in section 5, Deriving Computable Error Bounds
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps Daisy.Expressions.
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R):
Lemma const_abs_err_bounded (P:precond) (n:R) (nR:R) (nF:R):
forall cenv:nat -> R,
eval_exp 0%R cenv (Const n) nR ->
eval_exp (Q2R machineEpsilon) cenv (Const n) nF ->
eval_exp 0%R cenv P (Const n) nR ->
eval_exp (Q2R machineEpsilon) cenv P (Const n) nF ->
(Rabs (nR - nF) <= Rabs n * (Q2R machineEpsilon))%R.
Proof.
intros cenv eval_real eval_float.
......@@ -22,9 +22,9 @@ Proof.
apply Rmult_le_compat_l; [apply Rabs_pos | auto].
Qed.
Lemma param_abs_err_bounded (n:nat) (nR:R) (nF:R) (cenv:nat->R):
eval_exp 0%R cenv (Param R n) nR ->
eval_exp (Q2R machineEpsilon) cenv (Param R n) nF ->
Lemma param_abs_err_bounded (P:precond) (n:nat) (nR:R) (nF:R) (cenv:nat->R):
eval_exp 0%R cenv P (Param R n) nR ->
eval_exp (Q2R machineEpsilon) cenv P (Param R n) nF ->
(Rabs (nR - nF) <= Rabs (cenv n) * (Q2R machineEpsilon))%R.
Proof.
intros eval_real eval_float.
......@@ -37,13 +37,13 @@ Proof.
apply Rmult_le_compat_l; [ apply Rabs_pos | auto].
Qed.
Lemma add_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:nat->R) (err1:R) (err2:R):
eval_exp 0%R cenv e1 e1R ->
eval_exp (Q2R machineEpsilon) cenv e1 e1F ->
eval_exp 0%R cenv e2 e2R ->
eval_exp (Q2R machineEpsilon) cenv e2 e2F ->
eval_exp 0%R cenv (Binop Plus e1 e2) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F cenv)) (Binop Plus (Var R 1) (Var R 2)) vF ->
Lemma add_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:nat->R) (P:precond) (err1:R) (err2:R):
eval_exp 0%R cenv P e1 e1R ->
eval_exp (Q2R machineEpsilon) cenv P e1 e1F ->
eval_exp 0%R cenv P e2 e2R ->
eval_exp (Q2R machineEpsilon) cenv P e2 e2F ->
eval_exp 0%R cenv P (Binop Plus e1 e2) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F cenv)) P (Binop Plus (Var R 1) (Var R 2)) vF ->
(Rabs (e1R - e1F) <= err1)%R ->
(Rabs (e2R - e2F) <= err2)%R ->
(Rabs (vR - vF) <= err1 + err2 + (Rabs (e1F + e2F) * (Q2R machineEpsilon)))%R.
......@@ -96,13 +96,13 @@ 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 R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:nat->R) (err1:R) (err2:R):
eval_exp 0%R cenv e1 e1R ->
eval_exp (Q2R machineEpsilon) cenv e1 e1F ->
eval_exp 0%R cenv e2 e2R ->
eval_exp (Q2R machineEpsilon) cenv e2 e2F ->
eval_exp 0%R cenv (Binop Sub e1 e2) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F cenv)) (Binop Sub (Var R 1) (Var R 2)) vF ->
Lemma subtract_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:nat->R) P (err1:R) (err2:R):
eval_exp 0%R cenv P e1 e1R ->
eval_exp (Q2R machineEpsilon) cenv P e1 e1F ->
eval_exp 0%R cenv P e2 e2R ->
eval_exp (Q2R machineEpsilon) cenv P e2 e2F ->
eval_exp 0%R cenv P (Binop Sub e1 e2) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F cenv)) P (Binop Sub (Var R 1) (Var R 2)) vF ->
(Rabs (e1R - e1F) <= err1)%R ->
(Rabs (e2R - e2F) <= err2)%R ->
(Rabs (vR - vF) <= err1 + err2 + ((Rabs (e1F - e2F)) * (Q2R machineEpsilon)))%R.
......@@ -148,13 +148,13 @@ Proof.
eapply Rmult_le_compat_l; [apply Rabs_pos | auto].
Qed.
Lemma mult_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:env) (err1:R) (err2:R):
eval_exp 0%R cenv e1 e1R ->
eval_exp (Q2R machineEpsilon) cenv e1 e1F ->
eval_exp 0%R cenv e2 e2R ->
eval_exp (Q2R machineEpsilon) cenv e2 e2F ->
eval_exp 0%R cenv (Binop Mult e1 e2) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F cenv)) (Binop Mult (Var R 1) (Var R 2)) vF ->
Lemma mult_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:env) (P:precond) (err1:R) (err2:R):
eval_exp 0%R cenv P e1 e1R ->
eval_exp (Q2R machineEpsilon) cenv P e1 e1F ->
eval_exp 0%R cenv P e2 e2R ->
eval_exp (Q2R machineEpsilon) cenv P e2 e2F ->
eval_exp 0%R cenv P (Binop Mult e1 e2) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F cenv)) P (Binop Mult (Var R 1) (Var R 2)) vF ->
(Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R machineEpsilon))%R.
Proof.
intros e1_real e1_float e2_real e2_float mult_real mult_float.
......@@ -192,13 +192,13 @@ Proof.
apply Rabs_pos.
Qed.
Lemma div_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:env) (err1:R) (err2:R):
eval_exp 0%R cenv e1 e1R ->
eval_exp (Q2R machineEpsilon) cenv e1 e1F ->
eval_exp 0%R cenv e2 e2R ->
eval_exp (Q2R machineEpsilon) cenv e2 e2F ->
eval_exp 0%R cenv (Binop Div e1 e2) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F cenv)) (Binop Div (Var R 1) (Var R 2)) vF ->
Lemma div_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:env) (P:precond) (err1:R) (err2:R):
eval_exp 0%R cenv P e1 e1R ->
eval_exp (Q2R machineEpsilon) cenv P e1 e1F ->
eval_exp 0%R cenv P e2 e2R ->
eval_exp (Q2R machineEpsilon) cenv P e2 e2F ->
eval_exp 0%R cenv P (Binop Div e1 e2) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F cenv)) P (Binop Div (Var R 1) (Var R 2)) vF ->
(Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R machineEpsilon))%R.
Proof.
intros e1_real e1_float e2_real e2_float div_real div_float.
......
......@@ -83,8 +83,8 @@ Qed.
Lemma validErrorboundCorrectConstant:
forall cenv absenv (n:Q) nR nF e nlo nhi (P:precond),
eval_exp 0%R cenv (Const (Q2R n)) nR ->
eval_exp (Q2R (RationalSimps.machineEpsilon)) cenv (Const (Q2R n)) nF ->
eval_exp 0%R cenv P (Const (Q2R n)) nR ->
eval_exp (Q2R (RationalSimps.machineEpsilon)) cenv P (Const (Q2R n)) nF ->
validErrorbound (Const n) absenv = true ->
validIntervalbounds (Const n) absenv P = true ->
absenv (Const n) = ((nlo,nhi),e) ->
......@@ -131,15 +131,14 @@ Qed.
Lemma validErrorboundCorrectParam:
forall cenv absenv (v:nat) nR nF e P plo phi,
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp (Param Q v)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp (Param Q v)) nF ->
eval_exp 0%R cenv P (toRExp (Param Q v)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv P (toRExp (Param Q v)) nF ->
validErrorbound (Param Q v) absenv = true ->
validIntervalbounds (Param Q v) absenv P = true ->
absenv (Param Q v) = ((plo,phi),e) ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros cenv absenv v nR nF e P plo phi cenv_approx_p eval_real eval_float error_valid intv_valid absenv_param.
intros cenv absenv v nR nF e P plo phi eval_real eval_float error_valid intv_valid absenv_param.
pose proof (ivbounds_approximatesPrecond_sound (Param Q v) absenv P intv_valid) as absenv_approx_p.
unfold validErrorbound in error_valid.
rewrite absenv_param in error_valid.
......@@ -147,12 +146,10 @@ Proof.
rewrite delta_0_deterministic in eval_real; auto.
rewrite delta_0_deterministic; auto.
inversion eval_float; subst.
unfold precondValidForExec in cenv_approx_p.
specialize (absenv_approx_p v).
specialize (cenv_approx_p v).
assert (exists ivlo ivhi, (ivlo,ivhi) = P v) by (destruct (P v) as [ivlo ivhi]; repeat eexists).
destruct H as [ivlo [ivhi P_eq]].
rewrite <- P_eq in absenv_approx_p, cenv_approx_p.
rewrite <- P_eq in absenv_approx_p, H1.
rewrite absenv_param in absenv_approx_p.
unfold freeVars in absenv_approx_p; simpl in absenv_approx_p.
assert (v = v \/ False) by auto.
......@@ -162,38 +159,32 @@ Proof.
destruct absenv_approx_p as [plo_le_ivlo ivhi_le_phi].
apply Is_true_eq_true, Qle_bool_iff in plo_le_ivlo.
apply Is_true_eq_true, Qle_bool_iff in ivhi_le_phi.
destruct cenv_approx_p as [ivlo_le_cenv cenv_le_ivhi].
simpl in H1;destruct H1.
apply Qle_Rle in plo_le_ivlo; apply Qle_Rle in ivhi_le_phi.
pose proof (Rle_trans (Q2R plo) (Q2R ivlo) (cenv v) plo_le_ivlo ivlo_le_cenv).
pose proof (Rle_trans (cenv v) (Q2R ivhi) (Q2R phi) cenv_le_ivhi ivhi_le_phi).
pose proof (RmaxAbs (Q2R plo) (cenv v) (Q2R phi) H2 H3).
unfold perturb.
rewrite Rabs_err_simpl.
rewrite Rabs_mult.
eapply Rle_trans.
eapply Rmult_le_compat; [ apply Rabs_pos | apply Rabs_pos | | ].
apply H4.
apply H1.
pose proof (maxAbs_impl_RmaxAbs plo phi).
unfold RmaxAbsFun in H5.
simpl in H5.
rewrite H5.
andb_to_prop error_valid.
rename R into error_valid.
apply Qle_bool_iff in error_valid.
apply Qle_Rle in error_valid.
rewrite Q2R_mult in error_valid.
apply error_valid.
unfold perturb.
rewrite Rabs_err_simpl.
rewrite Rabs_mult.
eapply Rle_trans;[ | apply error_valid].
apply Rmult_le_compat;try (apply Rabs_pos);[ | apply H2].
pose proof (Rle_trans (Q2R plo) (Q2R ivlo) (cenv v) plo_le_ivlo H1).
pose proof (Rle_trans (cenv v) (Q2R ivhi) (Q2R phi) H4 ivhi_le_phi).
pose proof (RmaxAbs (Q2R plo) (cenv v) (Q2R phi) H5 H6).
pose proof (maxAbs_impl_RmaxAbs plo phi).
rewrite <- H8;unfold RmaxAbsFun;simpl;auto.
Qed.
Lemma validErrorboundCorrectAddition cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) P :
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e1) nR1 ->
eval_exp 0%R cenv (toRExp e2) nR2 ->
eval_exp 0%R cenv (toRExp (Binop Plus e1 e2)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e1) nF1 ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e2) nF2 ->
eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 cenv)) (toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF ->
eval_exp 0%R cenv P (toRExp e1) nR1 ->
eval_exp 0%R cenv P (toRExp e2) nR2 ->
eval_exp 0%R cenv P (toRExp (Binop Plus e1 e2)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv P (toRExp e1) nF1 ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv P (toRExp e2) nF2 ->
eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 cenv)) P (toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF ->
validErrorbound (Binop Plus e1 e2) absenv = true ->
validIntervalbounds (Binop Plus e1 e2) absenv P = true ->
absenv e1 = ((e1lo,e1hi),err1) ->
......@@ -203,7 +194,7 @@ Lemma validErrorboundCorrectAddition cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 n
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros p_valid e1_real e2_real eval_real e1_float e2_float eval_float valid_error valid_intv absenv_e1 absenv_e2 absenv_add err1_bounded err2_bounded.
intros e1_real e2_real eval_real e1_float e2_float eval_float valid_error valid_intv absenv_e1 absenv_e2 absenv_add err1_bounded err2_bounded.
pose proof (ivbounds_approximatesPrecond_sound (Binop Plus e1 e2) absenv P valid_intv) as env_approx_p.
eapply Rle_trans.
eapply add_abs_err_bounded.
......@@ -245,11 +236,11 @@ Proof.
assert (ivlo iv = ivl) by (rewrite iv_unf; auto).
assert (ivhi iv = ivh) by (rewrite iv_unf; auto).
rewrite <- H, <- H0.
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid L0 e1_real) as valid_bounds_e1.
pose proof (validIntervalbounds_sound _ _ _ _ _ L0 e1_real) as valid_bounds_e1.
rewrite absenv_e1 in valid_bounds_e1.
simpl in valid_bounds_e1.
pose proof (distance_gives_iv nR1 nF1 (Q2R err1) (Q2R e1lo, Q2R e1hi) valid_bounds_e1 err1_bounded).
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid R1 e2_real) as valid_bounds_e2.
pose proof (validIntervalbounds_sound _ _ _ _ _ R1 e2_real) as valid_bounds_e2.
rewrite absenv_e2 in valid_bounds_e2.
simpl in valid_bounds_e2.
pose proof (distance_gives_iv nR2 nF2 (Q2R err2) (Q2R e2lo, Q2R e2hi) valid_bounds_e2 err2_bounded).
......@@ -267,13 +258,12 @@ Proof.
Qed.
Lemma validErrorboundCorrectSubtraction cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) P :
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e1) nR1 ->
eval_exp 0%R cenv (toRExp e2) nR2 ->
eval_exp 0%R cenv (toRExp (Binop Sub e1 e2)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e1) nF1 ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e2) nF2 ->
eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 cenv)) (toRExp (Binop Sub (Var Q 1) (Var Q 2))) nF ->
eval_exp 0%R cenv P (toRExp e1) nR1 ->
eval_exp 0%R cenv P (toRExp e2) nR2 ->
eval_exp 0%R cenv P (toRExp (Binop Sub e1 e2)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv P (toRExp e1) nF1 ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv P (toRExp e2) nF2 ->
eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 cenv)) P (toRExp (Binop Sub (Var Q 1) (Var Q 2))) nF ->
validErrorbound (Binop Sub e1 e2) absenv = true ->
validIntervalbounds (Binop Sub e1 e2) absenv P = true ->
absenv e1 = ((e1lo,e1hi),err1) ->
......@@ -283,7 +273,7 @@ Lemma validErrorboundCorrectSubtraction cenv absenv (e1:exp Q) (e2:exp Q) (nR nR
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros p_valid e1_real e2_real eval_real e1_float e2_float eval_float
intros e1_real e2_real eval_real e1_float e2_float eval_float
valid_error valid_intv absenv_e1 absenv_e2 absenv_sub
err1_bounded err2_bounded.
pose proof (ivbounds_approximatesPrecond_sound (Binop Sub e1 e2) absenv P valid_intv) as env_approx_p.
......@@ -326,11 +316,11 @@ Proof.
assert (ivlo iv = ivl) by (rewrite iv_unf; auto).
assert (ivhi iv = ivh) by (rewrite iv_unf; auto).
rewrite <- H, <- H0.
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid L1 e1_real) as valid_bounds_e1.
pose proof (validIntervalbounds_sound _ _ _ _ _ L1 e1_real) as valid_bounds_e1.
rewrite absenv_e1 in valid_bounds_e1.
simpl in valid_bounds_e1.
pose proof (distance_gives_iv nR1 nF1 (Q2R err1) (Q2R e1lo, Q2R e1hi) valid_bounds_e1 err1_bounded).
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid R2 e2_real) as valid_bounds_e2.
pose proof (validIntervalbounds_sound _ _ _ _ _ R2 e2_real) as valid_bounds_e2.
rewrite absenv_e2 in valid_bounds_e2.
simpl in valid_bounds_e2.
pose proof (distance_gives_iv nR2 nF2 (Q2R err2) (Q2R e2lo, Q2R e2hi) valid_bounds_e2 err2_bounded).
......@@ -354,13 +344,12 @@ Proof.
Qed.
Lemma validErrorboundCorrectMult cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) P :
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e1) nR1 ->
eval_exp 0%R cenv (toRExp e2) nR2 ->
eval_exp 0%R cenv (toRExp (Binop Mult e1 e2)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e1) nF1 ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e2) nF2 ->
eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 cenv)) (toRExp (Binop Mult (Var Q 1) (Var Q 2))) nF ->
eval_exp 0%R cenv P (toRExp e1) nR1 ->
eval_exp 0%R cenv P (toRExp e2) nR2 ->
eval_exp 0%R cenv P (toRExp (Binop Mult e1 e2)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv P (toRExp e1) nF1 ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv P (toRExp e2) nF2 ->
eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 cenv)) P (toRExp (Binop Mult (Var Q 1) (Var Q 2))) nF ->
validErrorbound (Binop Mult e1 e2) absenv = true ->
validIntervalbounds (Binop Mult e1 e2) absenv P = true ->
absenv e1 = ((e1lo,e1hi),err1) ->
......@@ -370,7 +359,7 @@ Lemma validErrorboundCorrectMult cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 n
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros p_valid e1_real e2_real eval_real e1_float e2_float eval_float
intros e1_real e2_real eval_real e1_float e2_float eval_float
valid_error valid_intv absenv_e1 absenv_e2 absenv_mult
err1_bounded err2_bounded.
pose proof (ivbounds_approximatesPrecond_sound (Binop Mult e1 e2) absenv P valid_intv) as env_approx_p.
......@@ -398,8 +387,8 @@ Proof.
simpl in valid_intv.
rewrite absenv_mult, absenv_e1, absenv_e2 in valid_intv.
andb_to_prop valid_intv.
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid L0 e1_real) as valid_e1.
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid R1 e2_real) as valid_e2.
pose proof (validIntervalbounds_sound _ _ _ _ _ L0 e1_real) as valid_e1.
pose proof (validIntervalbounds_sound _ _ _ _ _ R1 e2_real) as valid_e2.
apply Rplus_le_compat.
- unfold Rabs in err1_bounded.
unfold Rabs in err2_bounded.
......@@ -857,11 +846,11 @@ Proof.
assert (ivlo iv = ivl) by (rewrite iv_unf; auto).
assert (ivhi iv = ivh) by (rewrite iv_unf; auto).
rewrite <- H, <- H0.
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid L0 e1_real) as valid_bounds_e1.
pose proof (validIntervalbounds_sound _ _ _ _ _ L0 e1_real) as valid_bounds_e1.
rewrite absenv_e1 in valid_bounds_e1.
simpl in valid_bounds_e1.
pose proof (distance_gives_iv nR1 nF1 (Q2R err1) (Q2R e1lo, Q2R e1hi) valid_bounds_e1 err1_bounded).
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid R1 e2_real) as valid_bounds_e2.
pose proof (validIntervalbounds_sound _ _ _ _ _ R1 e2_real) as valid_bounds_e2.
rewrite absenv_e2 in valid_bounds_e2.
simpl in valid_bounds_e2.
pose proof (distance_gives_iv nR2 nF2 (Q2R err2) (Q2R e2lo, Q2R e2hi) valid_bounds_e2 err2_bounded).
......@@ -928,13 +917,12 @@ Proof.
Qed.
Lemma validErrorboundCorrectDiv cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) P :
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e1) nR1 ->
eval_exp 0%R cenv (toRExp e2) nR2 ->
eval_exp 0%R cenv (toRExp (Binop Div e1 e2)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e1) nF1 ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e2) nF2 ->
eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 cenv)) (toRExp (Binop Div (Var Q 1) (Var Q 2))) nF ->
eval_exp 0%R cenv P (toRExp e1) nR1 ->
eval_exp 0%R cenv P (toRExp e2) nR2 ->
eval_exp 0%R cenv P (toRExp (Binop Div e1 e2)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv P (toRExp e1) nF1 ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv P (toRExp e2) nF2 ->
eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 cenv)) P (toRExp (Binop Div (Var Q 1) (Var Q 2))) nF ->
validErrorbound (Binop Div e1 e2) absenv = true ->
validIntervalbounds (Binop Div e1 e2) absenv P = true ->
absenv e1 = ((e1lo,e1hi),err1) ->
......@@ -944,12 +932,12 @@ Lemma validErrorboundCorrectDiv cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros p_valid e1_real e2_real eval_real e1_float e2_float eval_float
intros e1_real e2_real eval_real e1_float e2_float eval_float
valid_error valid_intv absenv_e1 absenv_e2 absenv_div
err1_bounded err2_bounded.
pose proof (ivbounds_approximatesPrecond_sound (Binop Div e1 e2) absenv P valid_intv) as env_approx_p.
eapply Rle_trans.
apply (div_abs_err_bounded (toRExp e1) nR1 nF1 (toRExp e2) nR2 nF2 nR nF cenv); auto.
apply (div_abs_err_bounded (toRExp e1) nR1 nF1 (toRExp e2) nR2 nF2 nR nF cenv P); auto.
unfold validErrorbound in valid_error at 1;
unfold validIntervalbounds in valid_intv.
rewrite absenv_div, absenv_e1, absenv_e2 in valid_error, valid_intv.
......@@ -960,11 +948,11 @@ Proof.
rename R2 into valid_error.
rename L0 into no_div_zero_float.
andb_to_prop valid_intv.
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid L0 e1_real) as valid_bounds_e1.
pose proof (validIntervalbounds_sound _ _ _ _ _ L0 e1_real) as valid_bounds_e1.
rewrite absenv_e1 in valid_bounds_e1.
simpl in valid_bounds_e1.
pose proof (distance_gives_iv nR1 nF1 (Q2R err1) (Q2R e1lo, Q2R e1hi) valid_bounds_e1 err1_bounded) as valid_bounds_e1_err.
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid R0 e2_real) as valid_bounds_e2.
pose proof (validIntervalbounds_sound _ _ _ _ _ R0 e2_real) as valid_bounds_e2.
rewrite absenv_e2 in valid_bounds_e2.
simpl in valid_bounds_e2.
pose proof (distance_gives_iv nR2 nF2 (Q2R err2) (Q2R e2lo, Q2R e2hi) valid_bounds_e2 err2_bounded) as valid_bounds_e2_err.
......@@ -994,7 +982,7 @@ Proof.
apply Rplus_le_compat.
(* Error Propagation proof *)
+ clear absenv_e1 absenv_e2 valid_error eval_float eval_real e1_float
e1_real e2_float e2_real p_valid env_approx_p absenv_div
e1_real e2_float e2_real env_approx_p absenv_div
valid_err_e1 valid_err_e2 cenv absenv alo ahi nR nF e1 e2 e P.
unfold IntervalArith.contained, widenInterval in *.
simpl in *.
......@@ -1853,9 +1841,8 @@ Qed.
**)
Theorem validErrorbound_sound (e:exp Q):
forall cenv absenv nR nF err P elo ehi,
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e) nF ->
eval_exp 0%R cenv P (toRExp e) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv P (toRExp e) nF ->
validErrorbound e absenv = true ->
validIntervalbounds e absenv P = true ->
absenv e = ((elo,ehi),err) ->
......@@ -1863,14 +1850,14 @@ Theorem validErrorbound_sound (e:exp Q):
Proof.
induction e.
- intros; simpl in *.
rewrite H4 in H2; rewrite H4 in H3; inversion H2.
rewrite H3 in H1; rewrite H3 in H2; inversion H1.
- intros; eapply validErrorboundCorrectParam; eauto.
- intros; eapply validErrorboundCorrectConstant; eauto.
- intros cenv absenv nR nF err P elo ehi p_valid eval_real eval_float valid_error valid_intv absenv_eq.
- intros cenv absenv nR nF err P elo ehi eval_real eval_float valid_error valid_intv absenv_eq.
unfold validErrorbound in valid_error.
rewrite absenv_eq in valid_error.
inversion valid_error.
- intros cenv absenv nR nF err P elo ehi p_valid eval_real eval_float valid_error valid_intv absenv_eq.
- intros cenv absenv nR nF err P elo ehi eval_real eval_float valid_error valid_intv absenv_eq.
pose proof (ivbounds_approximatesPrecond_sound (Binop b e1 e2) absenv P valid_intv) as env_approx_p.
simpl in valid_error.
env_assert absenv e1 absenv_e1.
......@@ -1966,10 +1953,10 @@ Proof.
{ apply Is_true_eq_left; auto. }
Qed.
(*
Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult):
forall cenv1 cenv2 envR envF elo ehi err P,
precondValidForExec P cenv1 ->
precondValidForExec P cenv2 ->
approxEnv 0%R cenv1 (Q2R machineEpsilon) cenv2 ->
bstep (toRCmd f) cenv1 0%R (Nop R) envR ->
bstep (toRCmd f) cenv2 (Q2R RationalSimps.machineEpsilon) (Nop R) envF ->
......@@ -2006,4 +1993,4 @@ Proof.
eapply validErrorbound_sound.
admit.
- intros. inversion H0.
Admitted.
Admitted.*)
......@@ -2,7 +2,7 @@
Formalization of the base expression language for the daisy framework
Required in all files, since we will always reason about expressions.
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith.
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals.
Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps.
Set Implicit Arguments.
(**
......@@ -115,24 +115,25 @@ It is important that variables are not perturbed when loading from an environmen
This is the case, since loading a float value should not increase an additional error.
Unary negation is special! We do not have a new error here since IEE 754 gives us a sign bit
**)
Inductive eval_exp (eps:R) (E:env) : (exp R) -> R -> Prop :=
Var_load x: eval_exp eps E (Var R x) (E x)
Inductive eval_exp (eps:R) (E:env) (P:precond) : (exp R) -> R -> Prop :=
Var_load x: eval_exp eps E P (Var R x) (E x)
| Param_acc x delta:
((Rabs delta) <= eps)%R ->
eval_exp eps E (Param R x) (perturb (E x) delta)
((Q2R (fst (P x))) <= E x <= (Q2R (snd (P x))))%R ->
eval_exp eps E P (Param R x) (perturb (E x) delta)
| Const_dist n delta:
Rle (Rabs delta) eps ->
eval_exp eps E (Const n) (perturb n delta)
| Unop_neg f1 v1: eval_exp eps E f1 v1 -> eval_exp eps E (Unop Neg f1) (evalUnop Neg v1)
eval_exp eps E P (Const n) (perturb n delta)
| Unop_neg f1 v1: eval_exp eps E P f1 v1 -> eval_exp eps E P (Unop Neg f1) (evalUnop Neg v1)
| Unop_inv f1 v1 delta:
Rle (Rabs delta) eps ->
eval_exp eps E f1 v1 ->
eval_exp eps E (Unop Inv f1) (perturb (evalUnop Inv v1) delta)
eval_exp eps E P f1 v1 ->
eval_exp eps E P (Unop Inv f1) (perturb (evalUnop Inv v1) delta)
| Binop_dist op f1 f2 v1 v2 delta:
Rle (Rabs delta) eps ->
eval_exp eps E f1 v1 ->
eval_exp eps E f2 v2 ->
eval_exp eps E (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta).
eval_exp eps E P f1 v1 ->
eval_exp eps E P f2 v2 ->
eval_exp eps E P (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta).
(**
If |delta| <= 0 then perturb v delta is exactly v.
......@@ -149,10 +150,10 @@ Qed.
(**
Evaluation with 0 as machine epsilon is deterministic
**)
Lemma meps_0_deterministic (f:exp R) (E:env):
Lemma meps_0_deterministic (f:exp R) (E:env) (P:precond):
forall v1 v2,