Skip to content

GitLab

F
FloVer
Commit 5b919837 authored by Heiko Becker's avatar Heiko Becker
Browse files
Options

Start seriously working on let-Bindings, does not cpompile!

parent 1aba0115
Hide whitespace changes
Inline Side-by-side
Showing with 186 additions and 144 deletions
coq/Commands.v
View file @ 5b919837
......@@ -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 -> 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).
Inductive sstep : cmd R -> env -> env -> precond -> R -> cmd R -> env -> Prop :=
let_s x e s VarEnv ParamEnv P v eps:
eval_exp eps VarEnv ParamEnv P e v ->
sstep (Let R x e s) VarEnv ParamEnv P eps s (updEnv x v VarEnv)
|ret_s e VarEnv ParamEnv P v eps:
eval_exp eps VarEnv ParamEnv P e v ->
sstep (Ret R e) VarEnv ParamEnv P eps (Nop R) (updEnv 0 v VarEnv).
(**
Analogously define Big Step semantics for the Daisy language,
parametric by the evaluation function
**)
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
Inductive bstep : cmd R -> env -> env -> precond -> R -> cmd R -> env -> Prop :=
let_b x e s s' VarEnv ParamEnv P v eps env2:
eval_exp eps VarEnv ParamEnv P e v ->
bstep s (updEnv x v VarEnv) ParamEnv P eps s' env2 ->
bstep (Let R x e s) VarEnv ParamEnv P eps s' env2
|ret_b e VarEnv ParamEnv P v eps:
eval_exp eps VarEnv ParamEnv P e v ->
bstep (Ret R e) VarEnv ParamEnv P eps (Nop R) (updEnv 0 v VarEnv).
\ No newline at end of file
coq/Environments.v
View file @ 5b919837
......@@ -3,8 +3,8 @@ Environment library.
Defines the environment type for the Daisy framework and a simulation relation between environments.
FIXME: Would it make sense to differenciate between a parameter environment and a variable environment?
**)
Require Import Coq.Reals.Reals.
Require Import Daisy.Expressions Daisy.Commands.
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.Qreals.
Require Import Daisy.Infra.ExpressionAbbrevs Daisy.Commands.
(**
Define an approximation relation between two environments.
......@@ -13,30 +13,30 @@ 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 : 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).
Inductive approxEnv : env -> analysisResult -> env -> Prop :=
|approxRefl E A: approxEnv E A E
|approxUpd E1 E2 A v1 v2 x: approxEnv E1 A E2 ->
(Rabs (v1 - v2) <= Q2R (snd (A (Var Q x))))%R ->
approxEnv (updEnv x v1 E1) A (updEnv x v2 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'.
(*
Lemma small_step_preserves_sim A P f g E1 E2 E1' E2' eps:
approxEnv E1 A E2 ->
sstep f E1 P 0 g E1' ->
sstep f E2 P eps g E2' ->
approxEnv E1' A E2'.
Proof.
intros approxBefore.
induction f; intros stepLet1 stepLet2.
- inversion stepLet1; inversion stepLet2; subst.
eapply approxUpd.
apply approxBefore.
apply H7.
apply H16.
instantiate (1 := Rabs (v - v0)).
lra.
- inversion stepLet1; inversion stepLet2; subst.
eapply approxUpd.
apply approxBefore.
apply H0.
auto.
instantiate (1 := Rabs(v - v0)).
lra.
- inversion stepLet1.
Qed.
\ No newline at end of file
Qed. *)
\ No newline at end of file
coq/ErrorBounds.v
View file @ 5b919837
......@@ -5,14 +5,14 @@ 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.
Require Import Daisy.Environments.
Lemma const_abs_err_bounded (P:precond) (n:R) (nR:R) (nF:R):
forall cenv:nat -> R,
eval_exp 0%R cenv P (Const n) nR ->
eval_exp (Q2R machineEpsilon) cenv P (Const n) nF ->
Lemma const_abs_err_bounded (P:precond) (n:R) (nR:R) (nF:R) (VarEnv ParamEnv:env):
eval_exp 0%R VarEnv ParamEnv P (Const n) nR ->
eval_exp (Q2R machineEpsilon) VarEnv ParamEnv P (Const n) nF ->
(Rabs (nR - nF) <= Rabs n * (Q2R machineEpsilon))%R.
Proof.
intros cenv eval_real eval_float.
intros eval_real eval_float.
inversion eval_real; subst.
rewrite delta_0_deterministic; auto.
inversion eval_float; subst.
......@@ -21,10 +21,10 @@ Proof.
apply Rmult_le_compat_l; [apply Rabs_pos | auto].
Qed.
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.
Lemma param_abs_err_bounded (P:precond) (n:nat) (nR:R) (nF:R) (VarEnv ParamEnv:env):
eval_exp 0%R VarEnv ParamEnv P (Param R n) nR ->
eval_exp (Q2R machineEpsilon) VarEnv ParamEnv P (Param R n) nF ->
(Rabs (nR - nF) <= Rabs (ParamEnv n) * (Q2R machineEpsilon))%R.
Proof.
intros eval_real eval_float.
inversion eval_real; subst.
......@@ -36,18 +36,20 @@ 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) (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.
Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond) absenv:
approxEnv VarEnv1 absenv VarEnv2 ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) e1R ->
eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e1) e1F ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) e2R ->
eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e2) e2F ->
eval_exp 0%R VarEnv1 ParamEnv P (Binop Plus (toRExp e1) (toRExp e2)) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Plus (Var R 1) (Var R 2)) vF ->
(Rabs (e1R - e1F) <= Q2R (snd (absenv e1)))%R ->
(Rabs (e2R - e2F) <= Q2R (snd (absenv e2)))%R ->
(Rabs (vR - vF) <= Q2R (snd(absenv e1)) + Q2R (snd (absenv e2)) + (Rabs (e1F + e2F) * (Q2R machineEpsilon)))%R.
Proof.
intros e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2.
intros approxCEnv 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.
rewrite delta_0_deterministic in plus_real; auto.
......@@ -95,13 +97,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) 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 ->
Lemma subtract_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (VarEnv ParamEnv:nat->R) P (err1:R) (err2:R):
eval_exp 0%R VarEnv ParamEnv P e1 e1R ->
eval_exp (Q2R machineEpsilon) VarEnv ParamEnv P e1 e1F ->
eval_exp 0%R VarEnv ParamEnv P e2 e2R ->
eval_exp (Q2R machineEpsilon) VarEnv ParamEnv P e2 e2F ->
eval_exp 0%R VarEnv ParamEnv P (Binop Sub e1 e2) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv)) ParamEnv 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.
......@@ -147,13 +149,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) (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 ->
Lemma mult_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (VarEnv ParamEnv:env) (P:precond) (err1:R) (err2:R):
eval_exp 0%R VarEnv ParamEnv P e1 e1R ->
eval_exp (Q2R machineEpsilon) VarEnv ParamEnv P e1 e1F ->
eval_exp 0%R VarEnv ParamEnv P e2 e2R ->
eval_exp (Q2R machineEpsilon) VarEnv ParamEnv P e2 e2F ->
eval_exp 0%R VarEnv ParamEnv P (Binop Mult e1 e2) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv)) ParamEnv 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.
......@@ -191,13 +193,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) (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 ->
Lemma div_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (VarEnv ParamEnv:env) (P:precond) (err1:R) (err2:R):
eval_exp 0%R VarEnv ParamEnv P e1 e1R ->
eval_exp (Q2R machineEpsilon) VarEnv ParamEnv P e1 e1F ->
eval_exp 0%R VarEnv ParamEnv P e2 e2R ->
eval_exp (Q2R machineEpsilon) VarEnv ParamEnv P e2 e2F ->
eval_exp 0%R VarEnv ParamEnv P (Binop Div e1 e2) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv)) ParamEnv 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.
......
coq/ErrorValidation.v
View file @ 5b919837
......@@ -18,7 +18,7 @@ Fixpoint validErrorbound (e:exp Q) (absenv:analysisResult) :=
let (intv, err) := (absenv e) in
let errPos := Qleb 0 err in
match e with
|Var _ v => false
|Var _ v => errPos (* Variables will have been checked before *)
|Param _ v => andb errPos (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
|Const n => andb errPos (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
|Unop _ _ => false
......@@ -70,7 +70,8 @@ Proof.
destruct e;intros validErrorbound_e absenv_e;
unfold validErrorbound in validErrorbound_e;
rewrite <- absenv_e in validErrorbound_e; simpl in *.
- inversion validErrorbound_e.
- apply Qle_bool_iff in validErrorbound_e; apply Qle_Rle in validErrorbound_e.
rewrite Q2R0_is_0 in validErrorbound_e; auto.
- andb_to_prop validErrorbound_e.
apply Qle_bool_iff in L; apply Qle_Rle in L; rewrite Q2R0_is_0 in L; auto.
- andb_to_prop validErrorbound_e.
......@@ -81,23 +82,47 @@ Proof.
apply Qle_bool_iff in R0; apply Qle_Rle in R0; rewrite Q2R0_is_0 in R0; auto.
Qed.
Lemma validErrorboundCorrectVariable:
forall VarEnv1 VarEnv2 ParamEnv absenv (v:nat) nR nF e nlo nhi (P:precond),
approxEnv VarEnv1 absenv VarEnv2 ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp (Var Q v)) nR ->
eval_exp (Q2R (RationalSimps.machineEpsilon)) VarEnv2 ParamEnv P (toRExp (Var Q v)) nF ->
validErrorbound (Var Q v) absenv = true ->
absenv (Var Q v) = ((nlo,nhi),e) ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros cenv1 cenv2 PEnv absenv v nR nF e nlo nhi P approxCEnv eval_real eval_float
error_valid absenv_var.
inversion eval_real; inversion eval_float; subst.
induction approxCEnv.
- rewrite Rminus_diag_eq; [ | reflexivity].
rewrite Rabs_R0.
eapply err_always_positive; eauto.
- unfold updEnv.
case_eq (v =? x); intros eq_case; subst.
+ rewrite Nat.eqb_eq in eq_case. rewrite <- eq_case in H.
rewrite absenv_var in H; auto.
+ apply IHapproxCEnv; auto; apply Var_load.
Qed.
Lemma validErrorboundCorrectConstant:
forall cenv absenv (n:Q) nR nF e nlo nhi (P:precond),
eval_exp 0%R cenv P (Const (Q2R n)) nR ->
eval_exp (Q2R (RationalSimps.machineEpsilon)) cenv P (Const (Q2R n)) nF ->
forall VarEnv1 VarEnv2 ParamEnv absenv (n:Q) nR nF e nlo nhi (P:precond),
approxEnv VarEnv1 absenv VarEnv2 ->
eval_exp 0%R VarEnv1 ParamEnv P (Const (Q2R n)) nR ->
eval_exp (Q2R (RationalSimps.machineEpsilon)) VarEnv2 ParamEnv P (Const (Q2R n)) nF ->
validErrorbound (Const n) absenv = true ->
validIntervalbounds (Const n) absenv P = true ->
absenv (Const n) = ((nlo,nhi),e) ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros cenv absenv n nR nF e nlo nhi P eval_real eval_float error_valid intv_valid absenv_const.
intros cenv1 cenv2 PEnv absenv n nR nF e nlo nhi P approx_CEnv eval_real eval_float error_valid intv_valid absenv_const.
unfold validErrorbound in error_valid.
inversion eval_real; subst.
rewrite delta_0_deterministic in eval_real; auto.
rewrite delta_0_deterministic; auto.
clear delta H0.
inversion eval_float; subst.
pose proof (validIntervalbounds_sound (Const n) absenv P cenv (Q2R n) intv_valid eval_real) as iv_valid.
pose proof (validIntervalbounds_sound (Const n) absenv P cenv1 PEnv (Q2R n) intv_valid eval_real) as iv_valid.
rewrite absenv_const in *; simpl in *.
unfold perturb in *; simpl in *.
rewrite Rabs_err_simpl.
......@@ -121,21 +146,23 @@ Proof.
Qed.
Lemma validErrorboundCorrectParam:
forall cenv absenv (v:nat) nR nF e P plo phi,
eval_exp 0%R cenv P (toRExp (Param Q v)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv P (toRExp (Param Q v)) nF ->
forall VarEnv1 VarEnv2 ParamEnv absenv (v:nat) nR nF e P plo phi,
approxEnv VarEnv1 absenv VarEnv2 ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp (Param Q v)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) VarEnv2 ParamEnv 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 eval_real eval_float error_valid intv_valid absenv_param.
intros cenv1 cenv2 PEnv absenv v nR nF e P plo phi approx_CEnv 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.
inversion eval_real; subst.
rewrite delta_0_deterministic in eval_real; auto.
rewrite delta_0_deterministic; auto.
rewrite delta_0_deterministic in *; auto.
rewrite delta_0_deterministic in H1; auto.
rewrite delta_0_deterministic in H1; auto.
inversion eval_float; subst.
specialize (absenv_approx_p v).
assert (exists ivlo ivhi, (ivlo,ivhi) = P v) by (destruct (P v) as [ivlo ivhi]; repeat eexists).
......@@ -162,22 +189,24 @@ Proof.
rewrite Rabs_mult.
eapply Rle_trans;[ | apply error_valid].
apply Rmult_le_compat;try (apply Rabs_pos);[ | apply H2].
rewrite (delta_0_deterministic (cenv v) delta) in *; auto.
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 (Rle_trans (Q2R plo) (Q2R ivlo) (PEnv v) plo_le_ivlo H1).
pose proof (Rle_trans (PEnv v) (Q2R ivhi) (Q2R phi) H4 ivhi_le_phi).
pose proof (RmaxAbs (Q2R plo) (PEnv v) (Q2R phi) H5 H6).
pose proof (maxAbs_impl_RmaxAbs plo phi).
rewrite <- H8;unfold RmaxAbsFun;simpl;auto.
rewrite <- H8;unfold RmaxAbsFun; simpl; auto.
Qed.
(* TODO: Maybe extract subproof for ivbounds of operands into main lemma *)
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 :
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 ->
Lemma validErrorboundCorrectAddition VarEnv1 VarEnv2 ParamEnv 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 :
approxEnv VarEnv1 absenv VarEnv2 ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) nR1 ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) nR2 ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp (Binop Plus e1 e2)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) VarEnv2 ParamEnv P (toRExp e1) nF1 ->
eval_exp (Q2R RationalSimps.machineEpsilon) VarEnv2 ParamEnv P (toRExp e2) nF2 ->
eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 VarEnv2)) ParamEnv 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) ->
......@@ -187,10 +216,12 @@ 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 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 approx_CEnv 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.
eapply Rle_trans.
apply
(add_abs_err_bounded (toRExp e1) nR1 nF1 (toRExp e2) nR2 nF2 nR nF cenv P (Q2R err1) (Q2R err2));
(add_abs_err_bounded (toRExp e1) nR1 nF1 (toRExp e2) nR2 nF2 nR nF VarEnv1 ParamEnv P (Q2R err1) (Q2R err2));
try auto.
unfold validErrorbound in valid_error at 1.
rewrite absenv_add, absenv_e1, absenv_e2 in valid_error.
......@@ -1789,9 +1820,10 @@ Qed.
Each case requires the application of one of the soundness lemmata proven before
**)
Theorem validErrorbound_sound (e:exp Q):
forall cenv absenv nR nF err P elo ehi,
eval_exp 0%R cenv P (toRExp e) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv P (toRExp e) nF ->
forall cenv1 cenv2 absenv nR nF err P elo ehi,
approxEnv cenv1 cenv2 ->
eval_exp 0%R cenv1 P (toRExp e) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv2 P (toRExp e) nF ->
validErrorbound e absenv = true ->
validIntervalbounds e absenv P = true ->
absenv e = ((elo,ehi),err) ->
......@@ -1799,7 +1831,7 @@ Theorem validErrorbound_sound (e:exp Q):
Proof.
induction e.
- intros; simpl in *.
rewrite H3 in H1; rewrite H3 in H2; inversion H1.
rewrite H4 in H2; inversion H2.
- intros; eapply validErrorboundCorrectParam; eauto.
- intros; eapply validErrorboundCorrectConstant; eauto.
- intros cenv absenv nR nF err P elo ehi eval_real eval_float valid_error valid_intv absenv_eq.
......@@ -1902,23 +1934,28 @@ 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,
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 ->
approxEnv cenv1 cenv2 ->
bstep (toRCmd f) cenv1 P 0%R (Nop R) envR ->
bstep (toRCmd f) cenv2 P (Q2R RationalSimps.machineEpsilon) (Nop R) envF ->
validErrorboundCmd f absenv = true ->
absenv (Var Q 0%nat) = ((elo,ehi),err) ->
(Rabs ((envR 0%nat) - (envF 0%nat)) <= (Q2R err))%R.
Proof.
induction f.
- intros cenv1 cenv2 envR envF elo ehi err P.
intros p_valid_cenv1 p_valid_cenv2 approxc1c2 eval_real eval_float valid_bounds absenv_res.
intros approxc1c2 eval_real eval_float valid_bounds absenv_res.
simpl in eval_real, eval_float.
inversion eval_real; inversion eval_float; subst.
assert (approxEnv (updEnv n v cenv1) (updEnv n v0 cenv2)).
+ eapply approxUpd; try auto.
unfold validErrorboundCmd in valid_bounds.
andb_to_prop valid_bounds.
rename L0 into validErrorbound_e.
assert (
eapply IHf.
admit.
admit.
eapply (small_step_preserves_sim (Let R n (toRExp e) (toRCmd f)) (toRCmd f)).
......@@ -1942,4 +1979,4 @@ Proof.
eapply validErrorbound_sound.
admit.
- intros. inversion H0.
Admitted.*)
Admitted.
coq/Expressions.v
View file @ 5b919837
......@@ -115,25 +115,27 @@ 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) (P:precond) : (exp R) -> R -> Prop :=
Var_load x: eval_exp eps E P (Var R x) (E x)
Inductive eval_exp (eps:R) (VarEnv:env) (ParamEnv:env) (P:precond) : (exp R) -> R -> Prop :=
Var_load x: eval_exp eps VarEnv ParamEnv P (Var R x) (VarEnv x)
| Param_acc x delta:
((Rabs delta) <= eps)%R ->
((Q2R (fst (P x))) <= perturb (E x) delta <= (Q2R (snd (P x))))%R ->
eval_exp eps E P (Param R x) (perturb (E x) delta)
((perturb (Q2R (fst (P x))) delta) <= perturb (ParamEnv x) delta <= (perturb (Q2R (snd (P x))) delta))%R ->
eval_exp eps VarEnv ParamEnv P (Param R x) (perturb (ParamEnv x) delta)
| Const_dist n delta:
Rle (Rabs delta) eps ->
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)
eval_exp eps VarEnv ParamEnv P (Const n) (perturb n delta)
| Unop_neg f1 v1:
eval_exp eps VarEnv ParamEnv P f1 v1 ->
eval_exp eps VarEnv ParamEnv P (Unop Neg f1) (evalUnop Neg v1)
| Unop_inv f1 v1 delta:
Rle (Rabs delta) eps ->
eval_exp eps E P f1 v1 ->
eval_exp eps E P (Unop Inv f1) (perturb (evalUnop Inv v1) delta)
eval_exp eps VarEnv ParamEnv P f1 v1 ->
eval_exp eps VarEnv ParamEnv 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 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).
eval_exp eps VarEnv ParamEnv P f1 v1 ->
eval_exp eps VarEnv ParamEnv P f2 v2 ->
eval_exp eps VarEnv ParamEnv P (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta).
(**
If |delta| <= 0 then perturb v delta is exactly v.
......@@ -150,10 +152,10 @@ Qed.
(**
Evaluation with 0 as machine epsilon is deterministic
**)
Lemma meps_0_deterministic (f:exp R) (E:env) (P:precond):
Lemma meps_0_deterministic (f:exp R) (VarEnv ParamEnv:env) (P:precond):
forall v1 v2,
eval_exp R0 E P f v1 ->
eval_exp R0 E P f v2 ->
eval_exp R0 VarEnv ParamEnv P f v1 ->
eval_exp R0 VarEnv ParamEnv P f v2 ->
v1 = v2.
Proof.
induction f; intros v1 v2 eval_v1 eval_v2;
......@@ -174,12 +176,12 @@ evaluating the subexpressions and then binding the result values to different
variables in the Eironment.
This relies on the property that variables are not perturbed as opposed to parameters
**)
Lemma binary_unfolding (b:binop) (f1:exp R) (f2:exp R) (eps:R) (cE:env) (P:precond) (v:R):
(eval_exp eps cE P (Binop b f1 f2) v <->
Lemma binary_unfolding (b:binop) (f1:exp R) (f2:exp R) (eps:R) (VarEnv ParamEnv:env) (P:precond) (v:R):
(eval_exp eps VarEnv ParamEnv P (Binop b f1 f2) v <->
exists v1 v2,
eval_exp eps cE P f1 v1 /\
eval_exp eps cE P f2 v2 /\
eval_exp eps (updEnv 2 v2 (updEnv 1 v1 cE)) P (Binop b (Var R 1) (Var R 2)) v).
eval_exp eps VarEnv ParamEnv P f1 v1 /\
eval_exp eps VarEnv ParamEnv P f2 v2 /\
eval_exp eps (updEnv 2 v2 (updEnv 1 v1 VarEnv)) ParamEnv P (Binop b (Var R 1) (Var R 2)) v).
Proof.
split.
- intros eval_bin.
......@@ -199,11 +201,11 @@ Qed.
(**
Analogous lemma for unary expressions.
**)
Lemma unary_unfolding (e:exp R) (eps:R) (cE:env) (P:precond) (v:R):
(eval_exp eps cE P (Unop Inv e) v <->
Lemma unary_unfolding (e:exp R) (eps:R) (VarEnv ParamEnv:env) (P:precond) (v:R):
(eval_exp eps VarEnv ParamEnv P (Unop Inv e) v <->
exists v1,
eval_exp eps cE P e v1 /\
eval_exp eps (updEnv 1 v1 cE) P (Unop Inv (Var R 1)) v).
eval_exp eps VarEnv ParamEnv P e v1 /\
eval_exp eps (updEnv 1 v1 VarEnv) ParamEnv P (Unop Inv (Var R 1)) v).
Proof.
split.
- intros eval_un.
......@@ -229,15 +231,15 @@ Inductive bexp (V:Type) : Type :=
(**
Define evaluation of booleans for reals
**)
Inductive bval (eps:R) (E:env) (P:precond): (bexp R) -> Prop -> Prop :=
Inductive bval (eps:R) (VarEnv ParamEnv:env) (P:precond): (bexp R) -> Prop -> Prop :=
leq_eval (f1:exp R) (f2:exp R) (v1:R) (v2:R):
eval_exp eps E P f1 v1 ->
eval_exp eps E P f2 v2 ->
bval eps E P (leq f1 f2) (Rle v1 v2)
eval_exp eps VarEnv ParamEnv P f1 v1 ->
eval_exp eps VarEnv ParamEnv P f2 v2 ->
bval eps VarEnv ParamEnv P (leq f1 f2) (Rle v1 v2)
|less_eval (f1:exp R) (f2:exp R) (v1:R) (v2:R):
eval_exp eps E P f1 v1 ->
eval_exp eps E P f2 v2 ->
bval eps E P (less f1 f2) (Rlt v1 v2).
eval_exp eps VarEnv ParamEnv P f1 v1 ->
eval_exp eps VarEnv ParamEnv P f2 v2 ->
bval eps VarEnv ParamEnv P (less f1 f2) (Rlt v1 v2).
(**
Simplify arithmetic later by making > >= only abbreviations
**)
......
coq/IntervalValidation.v
View file @ 5b919837
......@@ -139,11 +139,11 @@ Proof.
apply le_neq_bool_to_lt_prop; auto.
Qed.
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) cenv:
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) VarEnv ParamEnv:
forall vR,
(* precondValidForExec P cenv ->*)
validIntervalbounds f absenv P = true ->
eval_exp 0%R cenv P (toRExp f) vR ->
eval_exp 0%R VarEnv ParamEnv P (toRExp f) vR ->
(Q2R (fst (fst(absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R.
Proof.
induction f.
......@@ -174,6 +174,7 @@ Proof.
unfold Qleb in abslo_le_ivlo, ivhi_le_abshi.
apply Qle_bool_iff in abslo_le_ivlo; apply Qle_bool_iff in ivhi_le_abshi.
apply Qle_Rle in abslo_le_ivlo; apply Qle_Rle in ivhi_le_abshi.
rewrite delta_0_deterministic in *; auto.
rewrite delta_0_deterministic in *; auto.
split; lra.
- intros vR valid_bounds eval_f.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.