Skip to content

GitLab

Commit 4c69ae3a authored by Heiko Becker's avatar Heiko Becker
Browse files
Options

Refactor exp type into expr type because of name clash with new coq version,... 

Refactor exp type into expr type because of name clash with new coq version, move ExpOrderedType module into separate file
parent b3fc8947
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 1061 additions and 1056 deletions
coq/CertificateChecker.v
View file @ 4c69ae3a
......@@ -12,7 +12,7 @@ Require Export Coq.QArith.QArith.
Require Export Flover.Infra.ExpressionAbbrevs Flover.Commands.
(** Certificate checking function **)
Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) (defVars:nat -> option mType) :=
Definition CertificateChecker (e:expr Q) (absenv:analysisResult) (P:precond) (defVars:nat -> option mType) :=
let tMap := (typeMap defVars e (FloverMap.empty mType)) in
if (typeCheck e defVars tMap)
then
......@@ -26,7 +26,7 @@ Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) (def
Apart from assuming two executions, one in R and one on floats, we assume that
the real valued execution respects the precondition.
**)
Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P defVars:
Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVars:
forall (E1 E2:env),
approxEnv E1 defVars absenv (usedVars e) NatSet.empty E2 ->
(forall v, NatSet.In v (Expressions.usedVars e) ->
......@@ -38,10 +38,10 @@ Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P defVar
CertificateChecker e absenv P defVars = true ->
exists iv err vR vF m,
FloverMap.find e absenv = Some (iv, err) /\
eval_exp E1 (toRMap defVars) (toREval (toRExp e)) vR M0 /\
eval_exp E2 defVars (toRExp e) vF m /\
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) vR M0 /\
eval_expr E2 defVars (toRExp e) vF m /\
(forall vF m,
eval_exp E2 defVars (toRExp e) vF m ->
eval_expr E2 defVars (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R err))%R.
(**
The proofs is a simple composition of the soundness proofs for the range
......
coq/Commands.v
View file @ 4c69ae3a
......@@ -11,8 +11,8 @@ Require Export Flover.Infra.ExpressionAbbrevs Flover.Infra.NatSet.
Only assignments and return statement
**)
Inductive cmd (V:Type) :Type :=
Let: mType -> nat -> exp V -> cmd V -> cmd V
| Ret: exp V -> cmd V.
Let: mType -> nat -> expr V -> cmd V -> cmd V
| Ret: expr V -> cmd V.
Fixpoint getRetExp (V:Type) (f:cmd V) :=
match f with
......@@ -38,10 +38,10 @@ UNUSED!
Small Step semantics for Flover 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 ->
eval_expr 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 ->
eval_expr eps E e v ->
sstep (Ret e) E eps (Nop R) (updEnv 0 v E).
*)
......@@ -51,15 +51,15 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
**)
Inductive bstep : cmd R -> env -> (nat -> option mType) -> R -> mType -> Prop :=
let_b m m' x e s E v res defVars:
eval_exp E defVars e v m ->
eval_expr E defVars e v m ->
bstep s (updEnv x v E) (updDefVars x m defVars) res m' ->
bstep (Let m x e s) E defVars res m'
|ret_b m e E v defVars:
eval_exp E defVars e v m ->
eval_expr E defVars e v m ->
bstep (Ret e) E defVars v m.
(**
The free variables of a command are all used variables of expressions
The free variables of a command are all used variables of exprressions
without the let bound variables
**)
Fixpoint freeVars V (f:cmd V) :NatSet.t :=
......
coq/Environments.v
View file @ 4c69ae3a
......@@ -9,7 +9,7 @@ Require Import Flover.Infra.ExpressionAbbrevs Flover.Infra.RationalSimps Flover.
Define an approximation relation between two environments.
We use this relation for the soundness proofs.
It is necessary to have this relation, since two evaluations of the very same
expression may yield different values for different machine epsilons
exprression may yield different values for different machine epsilons
(or environments that already only approximate each other)
**)
Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t -> NatSet.t -> env -> Prop :=
......
coq/ErrorBounds.v
View file @ 4c69ae3a
(**
Proofs of general bounds on the error of arithmetic expressions.
Proofs of general bounds on the error of arithmetic exprressions.
This shortens soundness proofs later.
Bounds are explained in section 5, Deriving Computable Error Bounds
Bounds are exprlained in section 5, Deriving Computable Error Bounds
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps Flover.Infra.RealSimps Flover.Infra.RealRationalProps.
......@@ -9,8 +9,8 @@ Require Import Flover.Environments Flover.Infra.ExpressionAbbrevs.
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (m:mType) defVars:
eval_exp E1 (toRMap defVars) (Const M0 n) nR M0 ->
eval_exp E2 defVars (Const m n) nF m ->
eval_expr E1 (toRMap defVars) (Const M0 n) nR M0 ->
eval_expr E2 defVars (Const m n) nF m ->
(Rabs (nR - nF) <= Rabs n * (Q2R (mTypeToQ m)))%R.
Proof.
intros eval_real eval_float.
......@@ -26,14 +26,14 @@ Proof.
Qed.
Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
Lemma add_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType) defVars:
eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
eval_exp E2 defVars (toRExp e1) e1F m1->
eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 defVars (toRExp e2) e2F m2 ->
eval_exp E1 (toRMap defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
eval_expr E2 defVars (toRExp e1) e1F m1->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 ->
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(Binop Plus (Var R 1) (Var R 2)) vF m ->
(Rabs (e1R - e1F) <= Q2R err1)%R ->
......@@ -94,14 +94,14 @@ 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)
Lemma subtract_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R)
(e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m m1 m2:mType) defVars:
eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
eval_exp E2 defVars (toRExp e1) e1F m1 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 defVars (toRExp e2) e2F m2 ->
eval_exp E1 (toRMap defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
eval_expr E2 defVars (toRExp e1) e1F m1 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 ->
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(Binop Sub (Var R 1) (Var R 2)) vF m ->
(Rabs (e1R - e1F) <= Q2R err1)%R ->
......@@ -156,14 +156,14 @@ Proof.
eapply Rmult_le_compat_l; [apply Rabs_pos | auto].
Qed.
Lemma mult_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
Lemma mult_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
eval_exp E2 defVars (toRExp e1) e1F m1 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 defVars (toRExp e2) e2F m2 ->
eval_exp E1 (toRMap defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
eval_expr E2 defVars (toRExp e1) e1F m1 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 ->
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(Binop Mult (Var R 1) (Var R 2)) vF m ->
(Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R (mTypeToQ m)))%R.
......@@ -208,14 +208,14 @@ Proof.
apply Rabs_pos.
Qed.
Lemma div_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
Lemma div_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
eval_exp E2 defVars (toRExp e1) e1F m1 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 defVars (toRExp e2) e2F m2 ->
eval_exp E1 (toRMap defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
eval_expr E2 defVars (toRExp e1) e1F m1 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 ->
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(Binop Div (Var R 1) (Var R 2)) vF m ->
(Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R (mTypeToQ m)))%R.
......@@ -258,17 +258,17 @@ Proof.
apply Rabs_pos.
Qed.
Lemma fma_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
(e3:exp Q) (e3R:R) (e3F:R)
Lemma fma_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
(e3:expr Q) (e3R:R) (e3F:R)
(vR:R) (vF:R) (E1 E2:env) (m m1 m2 m3:mType) defVars:
eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
eval_exp E2 defVars (toRExp e1) e1F m1->
eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 defVars (toRExp e2) e2F m2 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp e3)) e3R M0 ->
eval_exp E2 defVars (toRExp e3) e3F m3->
eval_exp E1 (toRMap defVars) (toREval (Fma (toRExp e1) (toRExp e2) (toRExp e3))) vR M0 ->
eval_exp (updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv)))
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
eval_expr E2 defVars (toRExp e1) e1F m1->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e3)) e3R M0 ->
eval_expr E2 defVars (toRExp e3) e3F m3->
eval_expr E1 (toRMap defVars) (toREval (Fma (toRExp e1) (toRExp e2) (toRExp e3))) vR M0 ->
eval_expr (updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv)))
(updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 defVars)))
(Fma (Var R 1) (Var R 2) (Var R 3)) vF m ->
(Rabs (vR - vF) <= Rabs ((e1R - e1F) + (e2R * e3R - e2F * e3F)) + Rabs (e1F + e2F * e3F) * (Q2R (mTypeToQ m)))%R.
......@@ -505,10 +505,10 @@ Proof.
auto.
Qed.
Lemma round_abs_err_bounded (e:exp R) (nR nF1 nF:R) (E1 E2: env) (err:R) (machineEpsilon m:mType) defVars:
eval_exp E1 (toRMap defVars) (toREval e) nR M0 ->
eval_exp E2 defVars e nF1 m ->
eval_exp (updEnv 1 nF1 emptyEnv)
Lemma round_abs_err_bounded (e:expr R) (nR nF1 nF:R) (E1 E2: env) (err:R) (machineEpsilon m:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval e) nR M0 ->
eval_expr E2 defVars e nF1 m ->
eval_expr (updEnv 1 nF1 emptyEnv)
(updDefVars 1 m defVars)
(toRExp (Downcast machineEpsilon (Var Q 1))) nF machineEpsilon->
(Rabs (nR - nF1) <= err)%R ->
......
coq/ErrorValidation.v
View file @ 4c69ae3a
......@@ -15,7 +15,7 @@ From Flover
ErrorBounds.
(** Error bound validator **)
Fixpoint validErrorbound (e:exp Q) (* analyzed expression *)
Fixpoint validErrorbound (e:expr Q) (* analyzed exprression *)
(typeMap:FloverMap.t mType) (* derived types for e *)
(A:analysisResult) (* encoded result of Flover *)
(dVars:NatSet.t) (* let-bound variables encountered previously *):=
......@@ -23,7 +23,7 @@ Fixpoint validErrorbound (e:exp Q) (* analyzed expression *)
| Some (intv, err), Some m =>
if (Qleb 0 err) (* encoding soundness: errors are positive *)
then
match e with (* case analysis for the expression *)
match e with (* case analysis for the exprression *)
|Var _ v =>
if (NatSet.mem v dVars)
then true (* defined variables are checked at definition point *)
......@@ -153,19 +153,19 @@ Ltac destruct_ex H pat :=
Tactic Notation "destruct_smart" simple_intropattern(pat) hyp(H) := destruct_ex H pat.
Lemma validErrorboundCorrectVariable_eval E1 E2 A (v:nat) e nR nlo nhi P fVars
dVars Gamma expTypes:
eval_exp E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR M0 ->
typeCheck (Var Q v) Gamma expTypes = true ->
dVars Gamma exprTypes:
eval_expr E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR M0 ->
typeCheck (Var Q v) Gamma exprTypes = true ->
approxEnv E1 Gamma A fVars dVars E2 ->
validIntervalbounds (Var Q v) A P dVars = true ->
validErrorbound (Var Q v) expTypes A dVars = true ->
validErrorbound (Var Q v) exprTypes A dVars = true ->
NatSet.Subset (NatSet.diff (usedVars (Var Q v)) dVars) fVars ->
dVars_range_valid dVars E1 A ->
fVars_P_sound fVars E1 P ->
vars_typed (NatSet.union fVars dVars) Gamma ->
FloverMap.find (Var Q v) A = Some ((nlo, nhi), e) ->
exists nF m,
eval_exp E2 Gamma (toRExp (Var Q v)) nF m.
eval_expr E2 Gamma (toRExp (Var Q v)) nF m.
Proof.
intros eval_real typing_ok approxCEnv bounds_valid error_valid v_sound
dVars_sound P_valid types_valid A_var.
......@@ -183,13 +183,13 @@ Proof.
Qed.
Lemma validErrorboundCorrectVariable:
forall E1 E2 A (v:nat) e nR nF mF nlo nhi P fVars dVars Gamma expTypes,
eval_exp E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR M0 ->
eval_exp E2 Gamma (toRExp (Var Q v)) nF mF ->
typeCheck (Var Q v) Gamma expTypes = true ->
forall E1 E2 A (v:nat) e nR nF mF nlo nhi P fVars dVars Gamma exprTypes,
eval_expr E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR M0 ->
eval_expr E2 Gamma (toRExp (Var Q v)) nF mF ->
typeCheck (Var Q v) Gamma exprTypes = true ->
approxEnv E1 Gamma A fVars dVars E2 ->
validIntervalbounds (Var Q v) A P dVars = true ->
validErrorbound (Var Q v) expTypes A dVars = true ->
validErrorbound (Var Q v) exprTypes A dVars = true ->
NatSet.Subset (NatSet.diff (usedVars (Var Q v)) dVars) fVars ->
dVars_range_valid dVars E1 A ->
fVars_P_sound fVars E1 P ->
......@@ -231,9 +231,9 @@ Proof.
Qed.
Lemma validErrorboundCorrectConstant_eval E1 E2 m n nR Gamma:
eval_exp E1 (toRMap Gamma) (toREval (toRExp (Const m n))) nR M0 ->
eval_expr E1 (toRMap Gamma) (toREval (toRExp (Const m n))) nR M0 ->
exists nF m',
eval_exp E2 Gamma (toRExp (Const m n)) nF m'.
eval_expr E2 Gamma (toRExp (Const m n)) nF m'.
Proof.
intros eval_real .
repeat eexists.
......@@ -245,15 +245,15 @@ Proof.
Qed.
Lemma validErrorboundCorrectConstant E1 E2 A m n nR nF e nlo nhi dVars Gamma defVars:
eval_exp E1 (toRMap defVars) (toREval (toRExp (Const m n))) nR M0 ->
eval_exp E2 defVars (toRExp (Const m n)) nF m ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Const m n))) nR M0 ->
eval_expr E2 defVars (toRExp (Const m n)) nF m ->
typeCheck (Const m n) defVars Gamma = true ->
validErrorbound (Const m n) Gamma A dVars = true ->
(Q2R nlo <= nR <= Q2R nhi)%R ->
FloverMap.find (Const m n) A = Some ((nlo,nhi),e) ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros eval_real eval_float subexpr_ok error_valid intv_valid A_const.
intros eval_real eval_float subexprr_ok error_valid intv_valid A_const.
cbn in *; Flover_compute; type_conv.
eapply Rle_trans.
eapply const_abs_err_bounded; eauto.
......@@ -273,15 +273,15 @@ Proof.
Qed.
Lemma validErrorboundCorrectAddition E1 E2 A
(e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars m m1 m2 Gamma defVars:
m = join m1 m2 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp (Binop Plus e1 e2))) nR M0 ->
eval_exp E2 defVars (toRExp e1) nF1 m1 ->
eval_exp E2 defVars (toRExp e2) nF2 m2 ->
eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Plus e1 e2))) nR M0 ->
eval_expr E2 defVars (toRExp e1) nF1 m1 ->
eval_expr E2 defVars (toRExp e2) nF2 m2 ->
eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF m ->
typeCheck (Binop Plus e1 e2) defVars Gamma = true ->
......@@ -296,7 +296,7 @@ Lemma validErrorboundCorrectAddition E1 E2 A
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
subexpr_ok valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_add
subexprr_ok valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_add
err1_bounded err2_bounded.
cbn in *; Flover_compute; type_conv.
eapply Rle_trans.
......@@ -349,15 +349,15 @@ Proof.
Qed.
Lemma validErrorboundCorrectSubtraction E1 E2 A
(e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars:
m = join m1 m2 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp (Binop Sub e1 e2))) nR M0 ->
eval_exp E2 defVars (toRExp e1) nF1 m1->
eval_exp E2 defVars (toRExp e2) nF2 m2 ->
eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Sub e1 e2))) nR M0 ->
eval_expr E2 defVars (toRExp e1) nF1 m1->
eval_expr E2 defVars (toRExp e2) nF2 m2 ->
eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(toRExp (Binop Sub (Var Q 1) (Var Q 2))) nF m ->
typeCheck (Binop Sub e1 e2) defVars Gamma = true ->
......@@ -372,7 +372,7 @@ Lemma validErrorboundCorrectSubtraction E1 E2 A
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
subexpr_ok valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_sub
subexprr_ok valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_sub
err1_bounded err2_bounded.
cbn in *; Flover_compute; type_conv.
eapply Rle_trans.
......@@ -889,15 +889,15 @@ Proof.
Qed.
Lemma validErrorboundCorrectMult E1 E2 A
(e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars:
m = join m1 m2 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp (Binop Mult e1 e2))) nR M0 ->
eval_exp E2 defVars (toRExp e1) nF1 m1 ->
eval_exp E2 defVars (toRExp e2) nF2 m2 ->
eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Mult e1 e2))) nR M0 ->
eval_expr E2 defVars (toRExp e1) nF1 m1 ->
eval_expr E2 defVars (toRExp e2) nF2 m2 ->
eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(toRExp (Binop Mult (Var Q 1) (Var Q 2))) nF m ->
typeCheck (Binop Mult e1 e2) defVars Gamma = true ->
......@@ -912,7 +912,7 @@ Lemma validErrorboundCorrectMult E1 E2 A
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
subexpr_ok valid_error valid_e1 valid_e2 A_e1 A_e2 A_mult
subexprr_ok valid_error valid_e1 valid_e2 A_e1 A_e2 A_mult
err1_bounded err2_bounded.
cbn in *; Flover_compute; type_conv; subst.
eapply Rle_trans.
......@@ -967,15 +967,15 @@ Proof.
Qed.
Lemma validErrorboundCorrectDiv E1 E2 A
(e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars:
m = join m1 m2 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp (Binop Div e1 e2))) nR M0 ->
eval_exp E2 defVars (toRExp e1) nF1 m1 ->
eval_exp E2 defVars (toRExp e2) nF2 m2 ->
eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Div e1 e2))) nR M0 ->
eval_expr E2 defVars (toRExp e1) nF1 m1 ->
eval_expr E2 defVars (toRExp e2) nF2 m2 ->
eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(toRExp (Binop Div (Var Q 1) (Var Q 2))) nF m ->
typeCheck (Binop Div e1 e2) defVars Gamma = true ->
......@@ -991,7 +991,7 @@ Lemma validErrorboundCorrectDiv E1 E2 A
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
subexpr_ok valid_error valid_bounds_e1 valid_bounds_e2 no_div_zero_real A_e1
subexprr_ok valid_error valid_bounds_e1 valid_bounds_e2 no_div_zero_real A_e1
A_e2 A_div err1_bounded err2_bounded.
cbn in *; Flover_compute; type_conv; subst.
eapply Rle_trans.
......@@ -1891,17 +1891,17 @@ Proof.
Qed.
Lemma validErrorboundCorrectFma E1 E2 A
(e1:exp Q) (e2:exp Q) (e3: exp Q) (nR nR1 nR2 nR3 nF nF1 nF2 nF3: R) (e err1 err2 err3 :error)
(e1:expr Q) (e2:expr Q) (e3: expr Q) (nR nR1 nR2 nR3 nF nF1 nF2 nF3: R) (e err1 err2 err3 :error)
(alo ahi e1lo e1hi e2lo e2hi e3lo e3hi:Q) dVars (m m1 m2 m3:mType) Gamma defVars:
m = join3 m1 m2 m3 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp e3)) nR3 M0 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp (Fma e1 e2 e3))) nR M0 ->
eval_exp E2 defVars (toRExp e1) nF1 m1 ->
eval_exp E2 defVars (toRExp e2) nF2 m2 ->
eval_exp E2 defVars (toRExp e3) nF3 m3 ->
eval_exp (updEnv 3 nF3 (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)))
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e3)) nR3 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Fma e1 e2 e3))) nR M0 ->
eval_expr E2 defVars (toRExp e1) nF1 m1 ->
eval_expr E2 defVars (toRExp e2) nF2 m2 ->
eval_expr E2 defVars (toRExp e3) nF3 m3 ->
eval_expr (updEnv 3 nF3 (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)))
(updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 defVars)))
(toRExp (Fma (Var Q 1) (Var Q 2) (Var Q 3))) nF m ->
typeCheck (Fma e1 e2 e3) defVars Gamma = true ->
......@@ -1919,7 +1919,7 @@ Lemma validErrorboundCorrectFma E1 E2 A
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros mIsJoin e1_real e2_real e3_real eval_real e1_float e2_float e3_float eval_float
subexpr_ok valid_error valid_e1 valid_e2 valid_e3 A_e1 A_e2 A_e3 A_fma
subexprr_ok valid_error valid_e1 valid_e2 valid_e3 A_e1 A_e2 A_e3 A_fma
err1_bounded err2_bounded err3_bounded.
cbn in *; Flover_compute; type_conv; subst.
eapply Rle_trans.
......@@ -1993,10 +1993,10 @@ Proof.
assumption.
Qed.
Lemma validErrorboundCorrectRounding E1 E2 A (e: exp Q) (nR nF nF1: R) (err err':error) (elo ehi alo ahi: Q) dVars (m: mType) (machineEpsilon:mType) Gamma defVars:
eval_exp E1 (toRMap defVars) (toREval (toRExp e)) nR M0 ->
eval_exp E2 defVars (toRExp e) nF1 m ->
eval_exp (updEnv 1 nF1 emptyEnv)
Lemma validErrorboundCorrectRounding E1 E2 A (e: expr Q) (nR nF nF1: R) (err err':error) (elo ehi alo ahi: Q) dVars (m: mType) (machineEpsilon:mType) Gamma defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR M0 ->
eval_expr E2 defVars (toRExp e) nF1 m ->
eval_expr (updEnv 1 nF1 emptyEnv)
(updDefVars 1 m defVars)
(toRExp (Downcast machineEpsilon (Var Q 1))) nF machineEpsilon ->
typeCheck (Downcast machineEpsilon e) defVars Gamma = true ->
......@@ -2007,7 +2007,7 @@ Lemma validErrorboundCorrectRounding E1 E2 A (e: exp Q) (nR nF nF1: R) (err err'
(Rabs (nR - nF1) <= (Q2R err))%R ->
(Rabs (nR - nF) <= (Q2R err'))%R.
Proof.
intros eval_real eval_float eval_float_rnd subexpr_ok valid_error valid_intv
intros eval_real eval_float eval_float_rnd subexprr_ok valid_error valid_intv
A_e A_rnd err_bounded.
cbn in *; Flover_compute; type_conv; subst.
eapply Rle_trans.
......@@ -2040,15 +2040,15 @@ Qed.
(**
Soundness theorem for the error bound validator.
Proof is by induction on the expression e.
Proof is by induction on the exprression e.
Each case requires the application of one of the soundness lemmata proven before
**)
Theorem validErrorbound_sound (e:exp Q):
Theorem validErrorbound_sound (e:expr Q):
forall E1 E2 fVars dVars A nR err P elo ehi Gamma defVars,
typeCheck e defVars Gamma = true ->
approxEnv E1 defVars A fVars dVars E2 ->
NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
eval_exp E1 (toRMap defVars) (toREval (toRExp e)) nR M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR M0 ->
validErrorbound e Gamma A dVars = true ->
validIntervalbounds e A P dVars = true ->
dVars_range_valid dVars E1 A ->
......@@ -2056,9 +2056,9 @@ Theorem validErrorbound_sound (e:exp Q):
vars_typed (NatSet.union fVars dVars) defVars ->
FloverMap.find e A = Some ((elo,ehi),err) ->
(exists nF m,
eval_exp E2 defVars (toRExp e) nF m) /\
eval_expr E2 defVars (toRExp e) nF m) /\
(forall nF m,
eval_exp E2 defVars (toRExp e) nF m ->
eval_expr E2 defVars (toRExp e) nF m ->
(Rabs (nR - nF) <= (Q2R err))%R).
Proof.
revert e; induction e;
......
coq/Expressions.v
View file @ 4c69ae3a
This diff is collapsed.
coq/FPRangeValidator.v
View file @ 4c69ae3a
......@@ -5,7 +5,7 @@ Require Import Coq.QArith.QArith Coq.QArith.Qreals Coq.Reals.Reals Coq.micromega
Require Import Flover.Infra.MachineType Flover.Typing Flover.Infra.RealSimps Flover.IntervalValidation Flover.ErrorValidation Flover.Commands Flover.Environments Flover.ssaPrgs Flover.Infra.Ltacs Flover.Infra.RealRationalProps.
Fixpoint FPRangeValidator (e:exp Q) (A:analysisResult) typeMap dVars {struct e} : bool :=
Fixpoint FPRangeValidator (e:expr Q) (A:analysisResult) typeMap dVars {struct e} : bool :=
match FloverMap.find e typeMap, FloverMap.find e A with
|Some m, Some (iv_e, err_e) =>
let iv_e_float := widenIntv iv_e err_e in
......@@ -72,9 +72,9 @@ Ltac prove_fprangeval m v L1 R:=
destruct (Rle_lt_dec (Rabs v) (Q2R (maxValue m)))%R; lra.
Theorem FPRangeValidator_sound:
forall (e:exp Q) E1 E2 Gamma v m A tMap P fVars dVars,
forall (e:expr Q) E1 E2 Gamma v m A tMap P fVars dVars,
approxEnv E1 Gamma A fVars dVars E2 ->
eval_exp E2 Gamma (toRExp e) v m ->
eval_expr E2 Gamma (toRExp e) v m ->
typeCheck e Gamma tMap = true ->
validIntervalbounds e A P dVars = true ->
validErrorbound e tMap A dVars = true ->
......
coq/IEEE_connection.v
View file @ 4c69ae3a
This diff is collapsed.