Commit 6ad313ba authored by Heiko Becker's avatar Heiko Becker
Browse files

Merge branch 'new_semantics' into translation

parents 80f0d0c4 df325c1a
......@@ -13,19 +13,21 @@ Require Export Daisy.Infra.ExpressionAbbrevs.
(** Certificate checking function **)
Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
andb (validIntervalbounds e absenv P NatSet.empty) (validErrorbound e absenv).
andb (validIntervalbounds e absenv P NatSet.empty) (validErrorbound e absenv NatSet.empty).
(**
Soundness proof for the certificate checker.
Apart from assuming two executions, one in R and one on floats, we assume that
the real valued execution respects the precondition.
This property is expressed by the predicate precondValidForExec.
**)
Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
forall (VarEnv1 VarEnv2 ParamEnv:env) (vR:R) (vF:R),
approxEnv VarEnv1 absenv VarEnv2 ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp e) vR ->
eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e) vF ->
forall (E1 E2:env) (vR:R) (vF:R) fVars,
(forall v, NatSet.mem v (Expressions.freeVars e)= true ->
exists vR, E1 v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
approxEnv E1 absenv fVars NatSet.empty E2 ->
eval_exp 0%R E1 (toRExp e) vR ->
eval_exp (Q2R machineEpsilon) E2 (toRExp e) vF ->
CertificateChecker e absenv P = true ->
(Rabs (vR - vF) <= Q2R (snd (absenv e)))%R.
(**
......@@ -33,7 +35,7 @@ Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
validator and the error bound validator.
**)
Proof.
intros VarEnv1 VarEnv2 ParamEnv vR vF approxC1C2 eval_real eval_float certificate_valid.
intros VarEnv1 VarEnv2 ParamEnv vR vF P_valid approxC1C2 eval_real eval_float certificate_valid.
unfold CertificateChecker in certificate_valid.
andb_to_prop certificate_valid.
assert (exists iv err, absenv e = (iv,err)) by (destruct (absenv e); repeat eexists).
......@@ -46,37 +48,46 @@ Proof.
rewrite NatSet.mem_spec in v_in_empty.
hnf in v_in_empty.
inversion v_in_empty.
Qed.
admit.
Admitted.
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) :=
andb (validIntervalboundsCmd f absenv P NatSet.empty)
(validErrorboundCmd f absenv).
(validErrorboundCmd f absenv NatSet.empty).
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P:
forall (VarEnv1 VarEnv2 ParamEnv:env) outVars vR vF,
approxEnv VarEnv1 absenv VarEnv2 ->
ssaPrg Q f NatSet.empty outVars ->
bstep (toRCmd f) VarEnv1 ParamEnv P 0 (Nop R) vR ->
bstep (toRCmd f) VarEnv2 ParamEnv P (Q2R machineEpsilon) (Nop R) vF ->
forall (E1 E2:env) outVars vR vF fVars,
(forall v, NatSet.mem v fVars= true ->
exists vR, E1 v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
approxEnv E1 absenv fVars NatSet.empty E2 ->
ssaPrg f fVars outVars ->
bstep (toRCmd f) E1 0 vR ->
bstep (toRCmd f) E2 (Q2R machineEpsilon) vF ->
CertificateCheckerCmd f absenv P = true ->
(Rabs (vR - vF) <= Q2R (snd (absenv (Var Q 0))))%R.
(Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp f))))%R.
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
**)
Proof.
intros VarEnv1 VarEnv2 ParamEnv outVars envR envF
approxC1C2 ssa_f eval_real eval_float certificate_valid.
intros E1 E2 outVars vR vF fVars P_valid approxC1C2 ssa_f eval_real eval_float
certificate_valid.
unfold CertificateCheckerCmd in certificate_valid.
andb_to_prop certificate_valid.
assert (exists iv err, absenv (Var Q 0) = (iv,err)) by (destruct (absenv (Var Q 0)); repeat eexists).
assert (exists iv err, absenv (getRetExp f) = (iv,err)) by (destruct (absenv (getRetExp f)); repeat eexists).
destruct H as [iv [err absenv_eq]].
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) by (destruct iv; repeat eexists).
destruct H as [ivlo [ ivhi iv_eq]].
subst; rewrite absenv_eq in *; simpl in *.
eapply (validErrorboundCmd_sound); eauto.
intros v v_in_empty.
rewrite NatSet.mem_spec in v_in_empty.
hnf in v_in_empty.
inversion v_in_empty.
- hnf.
intros a; split; intros in_set.
+ rewrite NatSet.union_spec in in_set.
destruct in_set; try auto.
inversion H.
+ rewrite NatSet.union_spec; auto.
- intros v v_in_empty.
rewrite NatSet.mem_spec in v_in_empty.
inversion v_in_empty.
Qed.
\ No newline at end of file
......@@ -2,7 +2,8 @@
Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework
**)
Require Import Coq.Reals.Reals Coq.QArith.QArith.
Require Export Daisy.Infra.ExpressionAbbrevs.
Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Infra.NatSet.
(**
Next define what a program is.
Currently no loops, only conditionals and assignments
......@@ -10,65 +11,41 @@ Require Export Daisy.Infra.ExpressionAbbrevs.
**)
Inductive cmd (V:Type) :Type :=
Let: nat -> exp V -> cmd V -> cmd V
| Ret: exp V -> cmd V
| Nop: cmd V.
| Ret: exp V -> cmd V.
(*| Nop: cmd V. *)
(**
(*
UNUSED!
Small Step semantics for Daisy language
**)
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).
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).
*)
(**
Analogously define Big Step semantics for the Daisy language
**)
Inductive bstep : cmd R -> env -> env -> precond -> R -> cmd R -> R -> Prop :=
let_b x e s s' VarEnv ParamEnv P v eps res:
eval_exp eps VarEnv ParamEnv P e v ->
bstep s (updEnv x v VarEnv) ParamEnv P eps s' res ->
bstep (Let R x e s) VarEnv ParamEnv P eps s' res
|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) v.
Fixpoint substitute_exp (v:nat) (e:exp Q) (e_old:exp Q) :=
match e_old with
|Var _ v_old => if (v =? v_old) then e else Var Q v_old
|Unop op e' => Unop op (substitute_exp v e e')
|Binop op e1 e2 => Binop op (substitute_exp v e e1) (substitute_exp v e e2)
|e => e
end.
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.
Fixpoint substitute (v:nat) (e:exp Q) (f:cmd Q) :=
Fixpoint freeVars (f:cmd Q) :NatSet.t :=
match f with
|Let _ x e_x g =>
let new_e := substitute_exp v e e_x in
Let Q x new_e (substitute v e g)
|Ret _ e_ret => Ret Q (substitute_exp v e e_ret)
|Nop _ => Nop Q
| Let x e1 g => NatSet.remove x (NatSet.union (Expressions.freeVars e1) (freeVars g))
| Ret e => Expressions.freeVars e
end.
Fixpoint expand_lets (f:cmd Q) (fuel:nat) :option (cmd Q):=
match fuel with
|0%nat => Some f
|S fuel' =>
match f with
|Let _ x e g =>
(expand_lets (substitute x e g) fuel')
|Ret _ e => Some (Ret Q e)
|Nop _ => None
end
end.
Fixpoint count_lets (f:cmd Q) :nat :=
Fixpoint definedVars (f:cmd Q) :NatSet.t :=
match f with
|Let _ x e g => S (count_lets g)
| _ => 0%nat
end.
Definition expand (f:cmd Q) := expand_lets f (count_lets f).
\ No newline at end of file
| Let x _ g => NatSet.add x (definedVars g)
| Ret _ => NatSet.empty
end.
\ No newline at end of file
(**
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 Coq.micromega.Psatz Coq.QArith.Qreals.
Require Import Daisy.Infra.ExpressionAbbrevs Daisy.Commands.
Require Import Daisy.Infra.ExpressionAbbrevs Daisy.Infra.RationalSimps Daisy.Commands.
(**
Define an approximation relation between two environments.
......@@ -13,8 +12,24 @@ 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 : 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).
\ No newline at end of file
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:
approxEnv E1 A fVars dVars E2 ->
(Rabs (v1 - v2) <= v1 * Q2R machineEpsilon)%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 E1 A fVars dVars E2 ->
(Rabs (v1 - v2) <= Q2R (snd (A (Var Q 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).
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).
......@@ -7,9 +7,9 @@ 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 (P:precond) (n:R) (nR:R) (nF:R) (VarEnv1 VarEnv2 ParamEnv:env) (absenv:analysisResult):
eval_exp 0%R VarEnv1 ParamEnv P (Const n) nR ->
eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (Const n) nF ->
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.
Proof.
intros eval_real eval_float.
......@@ -21,30 +21,34 @@ Proof.
apply Rmult_le_compat_l; [apply Rabs_pos | auto].
Qed.
Lemma param_abs_err_bounded (P:precond) (n:nat) (nR:R) (nF:R) (VarEnv1 VarEnv2 ParamEnv:env) (absenv:analysisResult):
eval_exp 0%R VarEnv1 ParamEnv P (Param R n) nR ->
eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (Param R n) nF ->
(Rabs (nR - nF) <= Rabs (ParamEnv n) * (Q2R machineEpsilon))%R.
(*
Lemma param_abs_err_bounded (P:precond) (n:nat) (nR:R) (nF:R) (E1 E2:env) (absenv:analysisResult):
eval_exp 0%R E1 P (Param R n) nR ->
eval_exp (Q2R machineEpsilon) E2 P (Param R n) nF ->
(Rabs (nR - nF) <= * (Q2R machineEpsilon))%R.
Proof.
intros eval_real eval_float.
inversion eval_real; subst.
rewrite delta_0_deterministic; auto.
inversion eval_float; subst.
unfold perturb; simpl.
exists v; split; try auto.
rewrite H3 in H8; inversion H8.
rewrite Rabs_err_simpl.
repeat rewrite Rabs_mult.
apply Rmult_le_compat_l; [ apply Rabs_pos | auto].
Qed.
*)
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)
(err1 err2 :Q):
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 ->
(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 ->
(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.
......@@ -66,8 +70,11 @@ Proof.
unfold perturb; simpl.
inversion H4; subst; inversion H5; subst.
unfold updEnv; simpl.
unfold updEnv in H0,H1; simpl in *.
symmetry in H0, H1.
inversion H0; inversion H1; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear plus_float H4 H5 plus_real e1_real e1_float e2_real e2_float.
clear plus_float H4 H5 plus_real e1_real e1_float e2_real e2_float H0 H1.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rsub_eq_Ropp_Rplus.
......@@ -98,13 +105,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 Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R)
(e2F:R) (vR:R) (vF:R) (VarEnv1 VarEnv2 ParamEnv:nat->R) P err1 err2:
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 Sub (toRExp e1) (toRExp e2)) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Sub (Var R 1) (Var R 2)) vF ->
(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 ->
(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.
......@@ -126,8 +133,11 @@ Proof.
unfold perturb; simpl.
inversion H4; subst; inversion H5; subst.
unfold updEnv; simpl.
symmetry in H0, H1.
unfold updEnv in H0, H1; simpl in H0, H1.
inversion H0; inversion H1; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear sub_float H4 H5 sub_real e1_real e1_float e2_real e2_float.
clear sub_float H4 H5 sub_real e1_real e1_float e2_real e2_float H0 H1.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
repeat rewrite Rsub_eq_Ropp_Rplus.
......@@ -151,13 +161,13 @@ 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) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond):
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 Mult (toRExp e1) (toRExp e2)) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Mult (Var R 1) (Var R 2)) vF ->
(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.
Proof.
intros e1_real e1_float e2_real e2_float mult_real mult_float.
......@@ -176,9 +186,11 @@ Proof.
inversion mult_float; subst.
unfold perturb; simpl.
inversion H4; subst; inversion H5; subst.
unfold updEnv; simpl.
symmetry in H0, H1;
unfold updEnv in *; simpl in *.
inversion H0; inversion H1; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear mult_float H4 H5 mult_real e1_real e1_float e2_real e2_float.
clear mult_float H4 H5 mult_real e1_real e1_float e2_real e2_float H0 H1.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rsub_eq_Ropp_Rplus.
......@@ -196,13 +208,13 @@ 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) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond):
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 Div (toRExp e1) (toRExp e2)) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Div (Var R 1) (Var R 2)) vF ->
(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.
Proof.
intros e1_real e1_float e2_real e2_float div_real div_float.
......@@ -221,9 +233,11 @@ Proof.
inversion div_float; subst.
unfold perturb; simpl.
inversion H4; subst; inversion H5; subst.
unfold updEnv; simpl.
symmetry in H0, H1;
unfold updEnv in *; simpl in *.
inversion H0; inversion H1; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear div_float H4 H5 div_real e1_real e1_float e2_real e2_float.
clear div_float H4 H5 div_real e1_real e1_float e2_real e2_float H0 H1.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rsub_eq_Ropp_Rplus.
......
This diff is collapsed.
......@@ -3,8 +3,8 @@ 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 Coq.QArith.Qreals.
Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps.
Set Implicit Arguments.
Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet Daisy.IntervalArithQ Daisy.IntervalArith.
(**
Expressions will use binary operators.
Define them first
......@@ -56,13 +56,9 @@ Definition evalUnop (o:unop) (v:R):=
(**
Define expressions parametric over some value type V.
Will ease reasoning about different instantiations later.
Note that we differentiate between wether we use a variable from the environment or a parameter.
Parameters do not have error bounds in the invariants, so they must be perturbed, but variables from the
program will be perturbed upon binding, so we do not need to perturb them.
**)
Inductive exp (V:Type): Type :=
Var: nat -> exp V
| Param: nat -> exp V
| Const: V -> exp V
| Unop: unop -> exp V -> exp V
| Binop: binop -> exp V -> exp V -> exp V.
......@@ -78,11 +74,6 @@ Fixpoint expEqBool (e1:exp Q) (e2:exp Q) :=
|Var _ v2 => v1 =? v2
| _=> false
end
|Param _ v1 =>
match e2 with
|Param _ v2 => v1 =? v2
| _=> false
end
|Const n1 =>
match e2 with
|Const n2 => Qeq_bool n1 n2
......@@ -115,29 +106,33 @@ 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) (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 delta_lo delta_hi:
((Rabs delta) <= eps)%R ->
((Rabs delta_lo) <= eps)%R ->
((Rabs delta_hi) <= eps)%R ->
((perturb (Q2R (fst (P x))) delta_lo) <= perturb (ParamEnv x) delta <= (perturb (Q2R (snd (P x))) delta_hi))%R ->
eval_exp eps VarEnv ParamEnv P (Param R x) (perturb (ParamEnv x) delta)
Inductive eval_exp (eps:R) (E:env) :(exp R) -> R -> Prop :=
| Var_load x v:
E x = Some v ->
eval_exp eps E (Var R x) v
| Const_dist n delta:
Rle (Rabs delta) eps ->
eval_exp eps VarEnv ParamEnv P (Const n) (perturb n delta)
eval_exp eps E (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)
eval_exp eps E f1 v1 ->
eval_exp eps E (Unop Neg f1) (evalUnop Neg v1)
| Unop_inv f1 v1 delta:
Rle (Rabs delta) eps ->
eval_exp eps VarEnv ParamEnv P f1 v1 ->
eval_exp eps VarEnv ParamEnv P (Unop Inv f1) (perturb (evalUnop Inv v1) delta)
eval_exp eps E f1 v1 ->
eval_exp eps E (Unop Inv f1) (perturb (evalUnop Inv v1) delta)
| Binop_dist op f1 f2 v1 v2 delta:
Rle (Rabs delta) eps ->
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).
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).
Fixpoint freeVars (V:Type) (e:exp V) :NatSet.t :=
match e with
| Var _ x => NatSet.singleton x
| Unop u e1 => freeVars e1
| Binop b e1 e2 => NatSet.union (freeVars e1) (freeVars e2)
| _ => NatSet.empty
end.
(**
If |delta| <= 0 then perturb v delta is exactly v.
......@@ -154,15 +149,17 @@ Qed.
(**
Evaluation with 0 as machine epsilon is deterministic
**)
Lemma meps_0_deterministic (f:exp R) (VarEnv ParamEnv:env) (P:precond):
Lemma meps_0_deterministic (f:exp R) (E:env):
forall v1 v2,
eval_exp R0 VarEnv ParamEnv P f v1 ->
eval_exp R0 VarEnv ParamEnv P f v2 ->
eval_exp 0 E f v1 ->
eval_exp 0 E f v2 ->
v1 = v2.
Proof.
induction f; intros v1 v2 eval_v1 eval_v2;
inversion eval_v1; inversion eval_v2;
repeat try rewrite delta_0_deterministic; subst; auto.
- rewrite H3 in H0; inversion H0;
subst; auto.
- rewrite (IHf v0 v3); auto.
- inversion H3.
- inversion H4.
......@@ -178,36 +175,32 @@ 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) (VarEnv ParamEnv:env) (P:precond) (v:R):
(eval_exp eps VarEnv ParamEnv P (Binop b f1 f2) v <->
exists v1 v2,
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).
Lemma binary_unfolding b f1 f2 eps E vF:
eval_exp eps E (Binop b f1 f2) vF ->
exists vF1 vF2,
eval_exp eps E f1 vF1 /\
eval_exp eps E f2 vF2 /\
eval_exp eps (updEnv 2 vF2 (updEnv 1 vF1 emptyEnv))
(Binop b (Var R 1) (Var R 2)) vF.
Proof.
split.
- intros eval_bin.
inversion eval_bin; subst.
exists v1, v2.
repeat split; try auto.
constructor; try auto;
constructor; auto.
- intros exists_val.
destruct exists_val as [v1 [v2 [eval_f1 [eval_f2 eval_e_E]]]].
inversion eval_e_E; subst.
inversion H4; inversion H5; subst.
unfold updEnv in *; simpl in *.
constructor; auto.
intros eval_float.
inversion eval_float; subst.
exists v1 ; exists v2; repeat split; try auto.
constructor; try auto.