Skip to content

GitLab

F
FloVer
Commit 423830ed authored by Heiko Becker's avatar Heiko Becker
Browse files
Options

Merge branch 'certificates' into 'fma_proofs' 

Coq proofs for FMA support

See merge request AVA/daisy!154
parents d05a7b09 ec70dd8e
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 1126 additions and 481 deletions
coq/ErrorBounds.v
View file @ 423830ed
......@@ -258,6 +258,75 @@ 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)
(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)))
(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.
Proof.
intros e1_real e1_float e2_real e2_float e3_real e3_float fma_real fma_float.
inversion fma_real; subst;
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m4 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m5 = M0) by (eapply toRMap_eval_M0; eauto).
subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
rewrite delta_0_deterministic in fma_real; auto.
rewrite delta_0_deterministic; auto.
unfold evalFma in *; simpl in *.
clear delta H3.
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
rewrite (meps_0_deterministic (toRExp e2) H6 e2_real);
rewrite (meps_0_deterministic (toRExp e3) H7 e3_real).
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in fma_real.
rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in fma_real.
rewrite (meps_0_deterministic (toRExp e3) H7 e3_real) in fma_real.
clear H5 H6 v1 v2 v3 H7 H2.
inversion fma_float; subst.
unfold evalFma in *.
unfold perturb; simpl.
inversion H3; subst; inversion H6; subst; inversion H7; subst.
unfold updEnv in *; simpl in *.
inversion H5; inversion H1; inversion H9; subst.
clear fma_float H7 fma_real e1_real e1_float e2_real e2_float e3_real e3_float H6 H1 H5 H9 H3 H0 H4 H8.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rsub_eq_Ropp_Rplus.
rewrite Ropp_plus_distr.
rewrite <- Rplus_assoc.
setoid_rewrite <- Rsub_eq_Ropp_Rplus at 2.
rewrite Rsub_eq_Ropp_Rplus.
rewrite Rsub_eq_Ropp_Rplus.
rewrite Rsub_eq_Ropp_Rplus.
rewrite <- Rplus_assoc.
setoid_rewrite Rplus_comm at 8.
rewrite <- Rplus_assoc.
setoid_rewrite Rplus_comm at 9.
rewrite Rplus_assoc.
setoid_rewrite Rplus_assoc at 2.
rewrite <- Rplus_assoc.
rewrite <- Rsub_eq_Ropp_Rplus.
rewrite <- Rsub_eq_Ropp_Rplus.
rewrite <- Ropp_plus_distr.
rewrite <- Rsub_eq_Ropp_Rplus.
eapply Rle_trans.
eapply Rabs_triang.
eapply Rplus_le_compat_l.
rewrite Rabs_Ropp.
repeat rewrite Rabs_mult.
eapply Rmult_le_compat_l; auto.
apply Rabs_pos.
Qed.
Lemma err_prop_inversion_pos_real nF nR err elo ehi
(float_iv_pos : (0 < elo - err)%R)
(real_iv_pos : (0 < elo)%R)
......
coq/ErrorValidation.v
View file @ 423830ed
This diff is collapsed.
coq/Expressions.v
View file @ 423830ed
......@@ -91,6 +91,9 @@ Definition evalUnop (o:unop) (v:R):=
|Inv => (/ v)%R
end .
Definition evalFma (v1:R) (v2:R) (v3:R):=
evalBinop Plus v1 (evalBinop Mult v2 v3).
(**
Define expressions parametric over some value type V.
Will ease reasoning about different instantiations later.
......@@ -100,6 +103,7 @@ Inductive exp (V:Type): Type :=
| Const: mType -> V -> exp V
| Unop: unop -> exp V -> exp V
| Binop: binop -> exp V -> exp V -> exp V
| Fma: exp V -> exp V -> exp V -> exp V
| Downcast: mType -> exp V -> exp V.
(**
......@@ -115,6 +119,8 @@ Fixpoint expEq (e1:exp Q) (e2:exp Q) :=
(unopEq o1 o2) && (expEq e11 e22)
| Binop o1 e11 e12, Binop o2 e21 e22 =>
(binopEq o1 o2) && (expEq e11 e21) && (expEq e12 e22)
| Fma e11 e12 e13, Fma e21 e22 e23 =>
(expEq e11 e21) && (expEq e12 e22) && (expEq e13 e23)
| Downcast m1 f1, Downcast m2 f2 =>
(mTypeEq m1 m2) && (expEq f1 f2)
| _, _ => false
......@@ -129,6 +135,7 @@ Proof.
- apply Qeq_bool_iff; lra.
- case u; auto.
- case b; auto.
- firstorder.
- apply mTypeEq_refl.
Qed.
......@@ -149,6 +156,9 @@ Proof.
* destruct b; auto.
* apply IHe1.
+ apply IHe2.
- f_equal.
+ f_equal; auto.
+ auto.
- f_equal.
+ apply mTypeEq_sym; auto.
+ apply IHe.
......@@ -180,6 +190,11 @@ Proof.
rewrite binopEq_refl; simpl.
apply andb_true_iff.
split; [eapply IHe1; eauto | eapply IHe2; eauto].
- andb_to_prop eq1;
andb_to_prop eq2.
rewrite andb_true_iff.
rewrite andb_true_iff.
split; [split; [eapply IHe1; eauto | eapply IHe2; eauto] | eapply IHe3; eauto].
- andb_to_prop eq1;
andb_to_prop eq2.
rewrite mTypeEq_compat_eq in *; subst.
......@@ -189,11 +204,12 @@ Qed.
Fixpoint toRExp (e:exp Q) :=
match e with
|Var _ v => Var R v
|Const m n => Const m (Q2R n)
|Unop o e1 => Unop o (toRExp e1)
|Binop o e1 e2 => Binop o (toRExp e1) (toRExp e2)
|Downcast m e1 => Downcast m (toRExp e1)
| Var _ v => Var R v
| Const m n => Const m (Q2R n)
| Unop o e1 => Unop o (toRExp e1)
| Binop o e1 e2 => Binop o (toRExp e1) (toRExp e2)
| Fma e1 e2 e3 => Fma (toRExp e1) (toRExp e2) (toRExp e3)
| Downcast m e1 => Downcast m (toRExp e1)
end.
Fixpoint toREval (e:exp R) :=
......@@ -202,6 +218,7 @@ Fixpoint toREval (e:exp R) :=
| Const _ n => Const M0 n
| Unop o e1 => Unop o (toREval e1)
| Binop o e1 e2 => Binop o (toREval e1) (toREval e2)
| Fma e1 e2 e3 => Fma (toREval e1) (toREval e2) (toREval e3)
| Downcast _ e1 => Downcast M0 (toREval e1)
end.
......@@ -254,7 +271,15 @@ Inductive eval_exp (E:env) (Gamma: nat -> option mType) :(exp R) -> R -> mType -
eval_exp E Gamma f1 v1 m1 ->
eval_exp E Gamma f2 v2 m2 ->
((op = Div) -> (~ v2 = 0)%R) ->
eval_exp E Gamma (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta) (join m1 m2).
eval_exp E Gamma (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta) (join m1 m2)
| Fma_dist m1 m2 m3 f1 f2 f3 v1 v2 v3 delta:
Rle (Rabs delta) (Q2R (mTypeToQ (join3 m1 m2 m3))) ->
eval_exp E Gamma f1 v1 m1 ->
eval_exp E Gamma f2 v2 m2 ->
eval_exp E Gamma f3 v3 m3 ->
eval_exp E Gamma (Fma f1 f2 f3)
(perturb (evalFma v1 v2 v3) delta)
(join3 m1 m2 m3).
Hint Constructors eval_exp.
......@@ -323,6 +348,20 @@ Qed.
Hint Resolve Binop_dist'.
Lemma Fma_dist' m1 m2 m3 f1 f2 f3 v1 v2 v3 delta v m' E Gamma:
Rle (Rabs delta) (Q2R (mTypeToQ m')) ->
eval_exp E Gamma f1 v1 m1 ->
eval_exp E Gamma f2 v2 m2 ->
eval_exp E Gamma f3 v3 m3 ->
v = perturb (evalFma v1 v2 v3) delta ->
m' = join3 m1 m2 m3 ->
eval_exp E Gamma (Fma f1 f2 f3) v m'.
Proof.
intros; subst; auto.
Qed.
Hint Resolve Fma_dist'.
(**
Define the set of "used" variables of an expression to be the set of variables
occuring in it
......@@ -332,6 +371,7 @@ Fixpoint usedVars (V:Type) (e:exp V) :NatSet.t :=
| Var _ x => NatSet.singleton x
| Unop u e1 => usedVars e1
| Binop b e1 e2 => NatSet.union (usedVars e1) (usedVars e2)
| Fma e1 e2 e3 => NatSet.union (usedVars e1) (NatSet.union (usedVars e2) (usedVars e3))
| Downcast _ e1 => usedVars e1
| _ => NatSet.empty
end.
......@@ -355,6 +395,13 @@ Proof.
assert (m2 = M0)
by (eapply IHf2; eauto);
subst; auto.
- assert (m1 = M0)
by (eapply IHf1; eauto).
assert (m2 = M0)
by (eapply IHf2; eauto).
assert (m3 = M0)
by (eapply IHf3; eauto);
subst; auto.
Qed.
(**
......@@ -403,6 +450,20 @@ Proof.
simpl in *.
rewrite Q2R0_is_0 in *.
repeat (rewrite delta_0_deterministic; try auto).
- inversion ev1; inversion ev2; subst.
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m1 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m2 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m4 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m5 = M0) by (eapply toRMap_eval_M0; eauto).
subst.
rewrite (IHf1 v0 v5); try auto.
rewrite (IHf2 v3 v6); try auto.
rewrite (IHf3 v4 v7); try auto.
simpl in *.
rewrite Q2R0_is_0 in *.
repeat (rewrite delta_0_deterministic; try auto).
- inversion ev1; inversion ev2; subst.
apply M0_least_precision in H1;
apply M0_least_precision in H7; subst.
......@@ -413,7 +474,7 @@ Proof.
Qed.
(**
Helping lemma. Needed in soundness proof.
Helping lemmas. Needed in soundness proof.
For each evaluation of using an arbitrary epsilon, we can replace it by
evaluating the subexpressions and then binding the result values to different
variables in the Environment.
......@@ -432,6 +493,19 @@ Proof.
econstructor; try auto.
Qed.
Lemma fma_unfolding f1 f2 f3 E v1 v2 v3 m1 m2 m3 Gamma delta:
(Rabs delta <= Q2R (mTypeToQ (join3 m1 m2 m3)))%R ->
eval_exp E Gamma f1 v1 m1 ->
eval_exp E Gamma f2 v2 m2 ->
eval_exp E Gamma f3 v3 m3 ->
eval_exp E Gamma (Fma f1 f2 f3) (perturb (evalFma v1 v2 v3) delta) (join3 m1 m2 m3) ->
eval_exp (updEnv 3 v3 (updEnv 2 v2 (updEnv 1 v1 emptyEnv)))
(updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 Gamma)))
(Fma (Var R 1) (Var R 2) (Var R 3)) (perturb (evalFma v1 v2 v3) delta) (join3 m1 m2 m3).
Proof.
econstructor; try auto.
Qed.
Lemma eval_eq_env e:
forall E1 E2 Gamma v m,
(forall x, E1 x = E2 x) ->
......@@ -493,4 +567,4 @@ Qed. *)
(* Simplify arithmetic later by making > >= only abbreviations *)
(* **) *)
(* Definition gr := fun (V:Type) (f1: exp V) (f2: exp V) => less f2 f1. *)
(* Definition greq := fun (V:Type) (f1:exp V) (f2: exp V) => leq f2 f1. *)
\ No newline at end of file
(* Definition greq := fun (V:Type) (f1:exp V) (f2: exp V) => leq f2 f1. *)
coq/FPRangeValidator.v
View file @ 423830ed
......@@ -15,6 +15,10 @@ Fixpoint FPRangeValidator (e:exp Q) (A:analysisResult) typeMap dVars {struct e}
| Binop b e1 e2 =>
FPRangeValidator e1 A typeMap dVars &&
FPRangeValidator e2 A typeMap dVars
| Fma e1 e2 e3 =>
FPRangeValidator e1 A typeMap dVars &&
FPRangeValidator e2 A typeMap dVars &&
FPRangeValidator e3 A typeMap dVars
| Unop u e =>
FPRangeValidator e A typeMap dVars
| Downcast m e => FPRangeValidator e A typeMap dVars
......@@ -149,6 +153,8 @@ Proof.
prove_fprangeval m v L1 R.
- andb_to_prop H4.
prove_fprangeval m v L1 R.
- andb_to_prop H4.
prove_fprangeval m v L1 R.
Qed.
Lemma FPRangeValidatorCmd_sound (f:cmd Q):
......@@ -284,4 +290,4 @@ Proof.
rewrite NatSet.add_spec in H4; destruct H4;
auto; subst; congruence. }
- eapply FPRangeValidator_sound; eauto.
Qed.
\ No newline at end of file
Qed.
coq/IEEE_connection.v
View file @ 423830ed
......@@ -45,6 +45,11 @@ Fixpoint eval_exp_float (e:exp (binary_float 53 1024)) (E:nat -> option fl64):=
end
|_ , _ => None
end
| Fma e1 e2 e3 =>
match eval_exp_float e1 E, eval_exp_float e2 E, eval_exp_float e3 E with
(* | Some f1, Some f2, Some f3 => Some (b64_plus dmode f1 (b64_mult dmode f2 f3)) *)
| _, _, _ => None
end
| _ => None
end.
......@@ -78,6 +83,26 @@ Fixpoint eval_exp_valid (e:exp fl64) E :=
normal_or_zero (evalBinop b v1_real v2_real))
True)
True)
| Fma e1 e2 e3 =>
(eval_exp_valid e1 E) /\ (eval_exp_valid e2 E) /\ (eval_exp_valid e3 E) /\
(let e1_res := eval_exp_float e1 E in
let e2_res := eval_exp_float e2 E in
let e3_res := eval_exp_float e3 E in
optionLift e1_res
(fun v1 =>
let v1_real := B2R 53 1024 v1 in
optionLift e2_res
(fun v2 =>
let v2_real := B2R 53 1024 v2 in
optionLift e3_res
(fun v3 =>
let v3_real := B2R 53 1024 v3 in
(* No support for fma yet *)
(* normal_or_zero (evalFma v1_real v2_real v3_real)) *)
False)
True)
True)
True)
| Downcast m e => eval_exp_valid e E
end.
......@@ -153,6 +178,7 @@ Fixpoint B2Qexp (e: exp fl64) :=
| Const m v => Const m (B2Q v)
| Unop u e => Unop u (B2Qexp e)
| Binop b e1 e2 => Binop b (B2Qexp e1) (B2Qexp e2)
| Fma e1 e2 e3 => Fma (B2Qexp e1) (B2Qexp e2) (B2Qexp e3)
| Downcast m e => Downcast m (B2Qexp e)
end.
......@@ -174,6 +200,7 @@ Fixpoint is64BitEval (V:Type) (e:exp V) :=
| Const m e => m = M64
| Unop u e => is64BitEval e
| Binop b e1 e2 => is64BitEval e1 /\ is64BitEval e2
| Fma e1 e2 e3 => is64BitEval e1 /\ is64BitEval e2 /\ is64BitEval e3
| Downcast m e => m = M64 /\ is64BitEval e
end.
......@@ -189,6 +216,7 @@ Fixpoint noDowncast (V:Type) (e:exp V) :=
| Const m e => True
| Unop u e => noDowncast e
| Binop b e1 e2 => noDowncast e1 /\ noDowncast e2
| Fma e1 e2 e3 => noDowncast e1 /\ noDowncast e2 /\ noDowncast e3
| Downcast m e => False
end.
......@@ -294,6 +322,26 @@ Proof.
+ destruct (tMap e1); destruct (tMap e2); try congruence;
andb_to_prop typecheck_e; eauto.
+ intros; apply types_valid; set_tac.
- repeat (match goal with
|H: _ /\ _ |- _=> destruct H
end).
destruct (tMap (Fma e1 e2 e3)) eqn:?; try congruence;
erewrite IHe1 in *; eauto.
+ erewrite IHe2 in *; eauto.
* unfold join3, join in typecheck_e.
erewrite IHe3 in *; eauto.
++ rewrite isMorePrecise_refl in typecheck_e; andb_to_prop typecheck_e;
type_conv; subst; auto.
++ destruct (tMap e3); try congruence.
andb_to_prop typecheck_e; eauto.
++ intros; apply types_valid. set_tac.
* destruct (tMap e2); destruct (tMap e3); try congruence.
andb_to_prop typecheck_e; eauto.
* intros.
apply types_valid. set_tac.
+ destruct (tMap e1); destruct (tMap e2); destruct (tMap e3); try congruence;
andb_to_prop typecheck_e; eauto.
+ intros; apply types_valid; set_tac.
Qed.
Lemma typing_cmd_64_bit f:
......@@ -352,6 +400,18 @@ Proof.
assert (m3 = m1).
{ eapply IHe2; eauto. }
subst; auto.
- destruct (tMap e1) eqn:?; try congruence;
destruct (tMap e2) eqn:?; try congruence;
destruct (tMap e3) eqn:?; try congruence.
andb_to_prop typeCheck_e.
type_conv; subst.
assert (m0 = m).
{ eapply IHe1; eauto. }
assert (m3 = m1).
{ eapply IHe2; eauto. }
assert (m4 = m5).
{ eapply IHe3; eauto. }
subst; auto.
- destruct (tMap e) eqn:?; try congruence; type_conv; subst.
andb_to_prop typeCheck_e.
type_conv; subst; auto.
......@@ -490,6 +550,7 @@ Lemma eval_exp_gives_IEEE (e:exp fl64) :
exists v,
eval_exp_float e E2 = Some v /\
eval_exp (toREnv E2) Gamma (toRExp (B2Qexp e)) (Q2R (B2Q v)) M64.
Proof.
induction e; simpl in *;
intros * envs_eq typecheck_e approxEnv_E1_E2_real valid_rangebounds
valid_roundoffs valid_float_ranges eval_e_float
......@@ -923,6 +984,64 @@ Lemma eval_exp_gives_IEEE (e:exp fl64) :
repeat rewrite B2Q_B2R_eq; try auto.
rewrite <- round_eq. rewrite <- div_round; auto.
- rewrite finite_e1 in finite_res; auto. }
- repeat (match goal with
|H: _ /\ _ |- _ => destruct H
end).
destruct (tMap (Fma (B2Qexp e1) (B2Qexp e2) (B2Qexp e3))) eqn:?; try congruence;
destruct (tMap (B2Qexp e1)) eqn:?; try congruence;
destruct (tMap (B2Qexp e2)) eqn:?; try congruence;
destruct (tMap (B2Qexp e3)) eqn:?; try congruence.
andb_to_prop typecheck_e; type_conv; subst.
assert (tMap (B2Qexp e1) = Some M64 /\
tMap (B2Qexp e2) = Some M64 /\
tMap (B2Qexp e3) = Some M64 /\
tMap (Fma (B2Qexp e1) (B2Qexp e2) (B2Qexp e3)) = Some M64)
as [tMap_e1 [tMap_e2 [tMap_e3 tMap_fma]]].
{ repeat split; apply (typing_exp_64_bit _ Gamma); simpl; auto.
- intros; apply usedVars_64bit; set_tac.
- intros; apply usedVars_64bit; set_tac.
- intros; apply usedVars_64bit; set_tac.
- rewrite Heqo, Heqo0, Heqo1, Heqo2.
apply Is_true_eq_true; apply andb_prop_intro; split.
+ apply andb_prop_intro; split.
* apply andb_prop_intro; split.
++ apply Is_true_eq_left; auto.
apply mTypeEq_refl.
++ apply Is_true_eq_left; auto.
* apply Is_true_eq_left; auto.
+ apply Is_true_eq_left; auto. }
rewrite tMap_e1, tMap_e2, tMap_e3, tMap_fma in *.
inversion Heqo; inversion Heqo0; inversion Heqo1; inversion Heqo2; subst.
assert (m1 = M64).
{ eapply (typing_agrees_exp (B2Qexp e1)); eauto. }
assert (m2 = M64).
{ eapply (typing_agrees_exp (B2Qexp e2)); eauto. }
assert (m3 = M64).
{ eapply (typing_agrees_exp (B2Qexp e3)); eauto. }
subst.
destruct (A (Fma (B2Qexp e1) (B2Qexp e2) (B2Qexp e3))) eqn:?;
destruct (A (B2Qexp e1)) eqn:?;
destruct (A (B2Qexp e2)) eqn:?;
destruct (A (B2Qexp e3)) eqn:?;
simpl in *.
repeat (match goal with
|H: _ = true |- _ => andb_to_prop H
end).
destruct (IHe1 E1 E2 E2_real Gamma tMap v1 A P fVars dVars)
as [v_e1 [eval_float_e1 eval_rel_e1]];
try auto; try set_tac;
[ intros; apply usedVars_64bit ; set_tac | ].
destruct (IHe2 E1 E2 E2_real Gamma tMap v2 A P fVars dVars)
as [v_e2 [eval_float_e2 eval_rel_e2]];
try auto; try set_tac;
[ intros; apply usedVars_64bit ; set_tac | ].
destruct (IHe3 E1 E2 E2_real Gamma tMap v3 A P fVars dVars)
as [v_e3 [eval_float_e3 eval_rel_e3]];
try auto; try set_tac;
[ intros; apply usedVars_64bit ; set_tac | ].
unfold optionLift in H4.
rewrite eval_float_e1, eval_float_e2, eval_float_e3 in H4.
contradiction H4.
- inversion noDowncast_e.
Qed.
......@@ -1306,7 +1425,6 @@ Proof.
apply Is_true_eq_true.
repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
- destruct H6 as [vF [m [bstep_real [bstep_float roundoff_sound]]]].
assert (typeMapCmd defVars (B2Qcmd f) (getRetExp (B2Qcmd f)) = Some M64).
{ eapply typing_cmd_64_bit; eauto. }
assert (m = M64).
......@@ -1326,4 +1444,4 @@ Proof.
+ exists x; exists x0; exists M64.
destruct H7 as [bstep_float2 bstep_rel].
repeat split; auto.
Qed.
\ No newline at end of file
Qed.
coq/Infra/Ltacs.v
View file @ 423830ed
......@@ -65,11 +65,6 @@ Ltac NatSet_prop :=
| _ => try auto
end.
Ltac match_simpl :=
match goal with
| [ H: ?t = ?u |- context [match ?t with _ => _ end]] => rewrite H; simpl
end.
Ltac destruct_if :=
match goal with
| [H: (if ?c then ?a else ?b) = _ |- _ ] =>
......@@ -80,6 +75,60 @@ Ltac destruct_if :=
try congruence
end.
Definition optionLift (X Y:Type) (v:option X) (f:X -> Y) (e:Y) :=
match v with
|Some val => f val
| None => e
end.
Lemma optionLift_eq (X Y:Type) v (f:X -> Y) (e:Y):
match v with |Some val => f val | None => e end = optionLift X Y v f e.
Proof.
cbv; auto.
Qed.
Lemma optionLift_cond X (a:bool) (b c :X):
(if a then b else c) = match a with |true => b |false => c end.
Proof.
cbv; auto.
Qed.
Ltac remove_matches := rewrite optionLift_eq in *.
Ltac remove_conds := rewrite <- andb_lazy_alt, optionLift_cond in *.
Ltac match_factorize :=
match goal with
| [ H: ?t = ?u |- context [optionLift _ _ ?t _ _]]
=> rewrite H; cbn
| [ H1: ?t = ?u, H2: context [optionLift _ _ ?t _ _] |- _ ]
=> rewrite H1 in H2; cbn in H2
| [ H: context [optionLift _ _ ?t _ _] |- _ ]
=> destruct t eqn:?; cbn in H; try congruence
| [ |- context [optionLift _ _ ?t _ _] ]
=> destruct t eqn:?; cbn; try congruence
end.
Ltac pair_factorize :=
match goal with
| [H: context[let (_, _) := ?p in _] |- _] => destruct p; cbn in H
end.
Ltac match_simpl :=
try remove_conds;
try remove_matches;
repeat match_factorize;
try pair_factorize.
Ltac bool_factorize :=
match goal with
| [H: _ = true |- _] => andb_to_prop H
end.
Ltac Daisy_compute :=
repeat
(match_simpl || bool_factorize).
(* HOL4 Style patter matching tactics *)
Tactic Notation "lift " tactic(t) :=
fun H => t H.
......@@ -87,4 +136,4 @@ Tactic Notation "lift " tactic(t) :=
Tactic Notation "match_pat" open_constr(pat) tactic(t) :=
match goal with
| [H: ?ty |- _ ] => unify pat ty; t H
end.
\ No newline at end of file
end.
coq/Infra/MachineType.v
View file @ 423830ed
......@@ -138,6 +138,9 @@ Qed.
Definition join (m1:mType) (m2:mType) :=
if (isMorePrecise m1 m2) then m1 else m2.
Definition join3 (m1:mType) (m2:mType) (m3:mType) :=
join m1 (join m2 m3).
(* Lemma M0_join_is_M0 m1 m2: *)
(* join m1 m2 = M0 -> m1 = M0 /\ m2 = M0. *)
(* Proof. *)
......@@ -207,4 +210,4 @@ Definition validValue (v:Q) (m:mType) :=
match m with
| M0 => true
| _ => Qle_bool (Qabs v) (maxValue m)
end.
\ No newline at end of file
end.
coq/IntervalArith.v
View file @ 423830ed
......@@ -354,4 +354,4 @@ Proof.
assert (Rabs b = - b)%R as Rabs_neg_b by (apply Rabs_left; lra).
rewrite Rabs_neg_a, Rabs_neg_b.
rewrite Rmin_right; lra.
Qed.
\ No newline at end of file
Qed.
coq/IntervalValidation.v
View file @ 423830ed
......@@ -60,6 +60,17 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond) (vali
else false
end
else false
| Fma f1 f2 f3 =>
if ((validIntervalbounds f1 absenv P validVars) &&
(validIntervalbounds f2 absenv P validVars) &&
(validIntervalbounds f3 absenv P validVars))
then
let (iv1,_) := absenv f1 in
let (iv2,_) := absenv f2 in
let (iv3,_) := absenv f3 in
let new_iv := addIntv iv1 (multIntv iv2 iv3) in
isSupersetIntv new_iv intv
else false
| Downcast _ f1 =>
if (validIntervalbounds f1 absenv P validVars)
then
......@@ -129,6 +140,31 @@ Proof.
+ apply IHf2; try auto.
* apply Is_true_eq_true; auto.
* rewrite NatSet.diff_spec; split; auto.
- intros approx_fma_true v v_in_fV.
simpl in v_in_fV.
rewrite NatSet.diff_spec in v_in_fV.
destruct v_in_fV as [ v_in_fV v_not_in_V].
repeat rewrite NatSet.union_spec in v_in_fV.
apply Is_true_eq_left in approx_fma_true.
destruct (absenv (Fma f1 f2 f3)); destruct (absenv f1);
destruct (absenv f2); destruct (absenv f3); simpl in *.
apply andb_prop_elim in approx_fma_true.
destruct approx_fma_true.
apply andb_prop_elim in H.
destruct H.
<