Commit bc72a362 authored by Magnus Myreen's avatar Magnus Myreen

Merge branch 'master' into 'certificates'

Add a stable version of let Bindings to HOL4 and Coq certificates

See merge request !76
parents 1e2cf7d3 df325c1a
......@@ -9,8 +9,7 @@ scalaVersion in ThisBuild := "2.11.6"
scalacOptions ++= Seq(
"-deprecation",
"-unchecked",
"-feature"
)
"-feature")
resolvers += "Typesafe Repository" at "http://repo.typesafe.com/typesafe/releases/"
resolvers += "Sonatype OSS Snapshots" at "https://oss.sonatype.org/content/repositories/snapshots"
......@@ -22,8 +21,13 @@ libraryDependencies ++= Seq(
"org.fusesource.hawtjni" % "hawtjni-runtime" % "1.9" //for JNI
)
envVars := Map("LC_NUMERIC" -> "en_US.UTF-8")
Keys.fork in run := true
javaOptions in run ++= Seq(
"-Xms256M", "-Xmx2G", "-XX:+UseConcMarkSweepGC")
Keys.fork in Test := true //for native libraries to be on correct path
val scalaMeterFramework = new TestFramework("org.scalameter.ScalaMeterFramework")
......@@ -78,7 +82,12 @@ script := {
|
|SCALACLASSPATH="$paths"
|
|TMP=$$LC_NUMERIC
|LC_NUMERIC=en_US.UTF-8
|
|java -Xmx2G -Xms512M -Xss64M -classpath "$${SCALACLASSPATH}" -Dscala.usejavacp=false scala.tools.nsc.MainGenericRunner -classpath "$${SCALACLASSPATH}" daisy.Main $$@ 2>&1 | tee -i last.log
|
|LC_NUMERIC=$$TMP
|""".stripMargin)
f.setExecutable(true)
} catch {
......
......@@ -5,26 +5,29 @@
as shown in the soundness theorem.
**)
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Daisy.Infra.RealSimps Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps.
Require Import Daisy.IntervalValidation Daisy.ErrorValidation.
Require Import Daisy.Infra.RealSimps Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.Ltacs.
Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments.
Require Export Coq.QArith.QArith.
Require Export Daisy.Infra.ExpressionAbbrevs.
(** Certificate checking function **)
Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
andb (validIntervalbounds e absenv P) (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 (cenv:env) (vR:R) (vF:R),
eval_exp 0%R cenv P (toRExp e) vR ->
eval_exp (Q2R machineEpsilon) cenv 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.
(**
......@@ -32,17 +35,59 @@ Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
validator and the error bound validator.
**)
Proof.
intros cenv vR vF 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.
apply Is_true_eq_left in certificate_valid.
apply andb_prop_elim in certificate_valid.
destruct certificate_valid as [iv_valid errorbound_valid].
apply Is_true_eq_true in iv_valid;
apply Is_true_eq_true in errorbound_valid.
andb_to_prop certificate_valid.
assert (exists iv err, absenv e = (iv,err)) by (destruct (absenv e); 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 (validErrorbound_sound e cenv absenv vR vF err P); eauto.
eapply (validErrorbound_sound); eauto.
intros v v_in_empty.
rewrite NatSet.mem_spec in v_in_empty.
hnf in v_in_empty.
inversion v_in_empty.
admit.
Admitted.
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) :=
andb (validIntervalboundsCmd f absenv P NatSet.empty)
(validErrorboundCmd f absenv NatSet.empty).
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P:
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 (getRetExp f))))%R.
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
**)
Proof.
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 (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.
- 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
(**
Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework
FIXME: Currently the semantics are stateful. But daisy actually assumes that a variable may not be verwritten?
**)
Require Import Coq.Reals.Reals.
Require Import Daisy.Expressions.
Require Import Coq.Reals.Reals Coq.QArith.QArith.
Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Infra.NatSet.
(**
Next define what a program is.
Currently no loops, only conditionals and assignments
......@@ -11,29 +11,41 @@ Require Import Daisy.Expressions.
**)
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. *)
(**
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).
(*
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).
*)
(**
Analogously define Big Step semantics for the Daisy language,
parametric by the evaluation function
Analogously define Big Step semantics for the Daisy language
**)
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 -> 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 freeVars (f:cmd Q) :NatSet.t :=
match f with
| Let x e1 g => NatSet.remove x (NatSet.union (Expressions.freeVars e1) (freeVars g))
| Ret e => Expressions.freeVars e
end.
Fixpoint definedVars (f:cmd Q) :NatSet.t :=
match f with
| 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.
Require Import Daisy.Expressions Daisy.Commands.
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.Qreals.
Require Import Daisy.Infra.ExpressionAbbrevs Daisy.Infra.RationalSimps Daisy.Commands.
(**
Define an approximation relation between two environments.
......@@ -13,30 +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 : 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 -> 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).
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 H7.
apply H16.
- inversion stepLet1; inversion stepLet2; subst.
eapply approxUpd.
apply approxBefore.
apply H0.
auto.
- inversion stepLet1.
Qed.
\ No newline at end of file
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).
......@@ -4,15 +4,15 @@ This shortens soundness proofs later.
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.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):
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 (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 cenv eval_real eval_float.
intros eval_real eval_float.
inversion eval_real; subst.
rewrite delta_0_deterministic; auto.
inversion eval_float; subst.
......@@ -21,31 +21,37 @@ 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) (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 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) (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.
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 *)
......@@ -64,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.
......@@ -95,16 +104,17 @@ 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 ->
(Rabs (e1R - e1F) <= err1)%R ->
(Rabs (e2R - e2F) <= err2)%R ->
(Rabs (vR - vF) <= err1 + err2 + ((Rabs (e1F - e2F)) * (Q2R machineEpsilon)))%R.
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 ->
(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.
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 *)
......@@ -123,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.
......@@ -147,13 +160,14 @@ 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 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.
Proof.
intros e1_real e1_float e2_real e2_float mult_real mult_float.
......@@ -172,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.
......@@ -191,13 +207,14 @@ 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 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.
Proof.
intros e1_real e1_float e2_real e2_float div_real div_float.
......@@ -216,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,25 +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) (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 ->
((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)
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 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 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)
| 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 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 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 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.
......@@ -150,15 +149,17 @@ 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) (E:env):
forall v1 v2,
eval_exp R0 E P f v1 ->
eval_exp R0 E P f v2 ->