Skip to content

GitLab

F
FloVer
Commit 61171aef authored by Heiko Becker's avatar Heiko Becker
Browse files
Options

Merge branch 'fma_proofs_merge' into 'certificates' 

Fma proofs merge

See merge request AVA/daisy!170
parents 13ae6d87 c14fe5f4
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 2432 additions and 1069 deletions
coq/ErrorBounds.v
View file @ 61171aef
......@@ -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 @ 61171aef
This diff is collapsed.
coq/Expressions.v
View file @ 61171aef
This diff is collapsed.
coq/FPRangeValidator.v
View file @ 61171aef
......@@ -14,6 +14,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
......@@ -123,6 +127,9 @@ Proof.
- Daisy_compute; try congruence.
type_conv; subst.
prove_fprangeval (join m0 m1) v L1 R.
- Daisy_compute; try congruence.
type_conv; subst.
prove_fprangeval (join3 m0 m1 m2) v L1 R.
- Daisy_compute; try congruence.
type_conv; subst.
prove_fprangeval m v L1 R.
......@@ -238,4 +245,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 @ 61171aef
......@@ -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.
......@@ -286,6 +314,17 @@ Proof.
* intros.
apply types_valid. set_tac.
+ intros; apply types_valid; set_tac.
- repeat (match goal with
|H: _ /\ _ |- _=> destruct H
end).
erewrite IHe1 in *; eauto; try (intros; apply types_valid; set_tac; fail).
erewrite IHe2 in *; eauto; try (intros; apply types_valid; set_tac; fail).
unfold join3, join in *.
erewrite IHe3 in *; eauto; try (intros; apply types_valid; set_tac; fail).
repeat destr_factorize.
repeat rewrite <- isMorePrecise_morePrecise.
repeat rewrite isMorePrecise_refl;
type_conv; subst; auto.
Qed.
Lemma typing_cmd_64_bit f:
......@@ -326,10 +365,12 @@ Proof.
Daisy_compute; try congruence; type_conv; subst; try auto.
- eapply IHe; eauto.
- eapply IHe; eauto.
- assert (m0 = m).
{ eapply IHe1; eauto. }
assert (m3 = m1).
{ eapply IHe2; eauto. }
- assert (m0 = m) by eauto using IHe1.
assert (m3 = m1) by eauto using IHe2.
subst; auto.
- assert (m0 = m) by eauto using IHe1.
assert (m3 = m1) by eauto using IHe2.
assert (m4 = m5) by eauto using IHe3.
subst; auto.
Qed.
......@@ -458,6 +499,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
......@@ -853,6 +895,51 @@ 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).
assert (DaisyMap.find (B2Qexp e1) tMap = Some M64 /\
DaisyMap.find (B2Qexp e2) tMap = Some M64 /\
DaisyMap.find (B2Qexp e3) tMap = Some M64 /\
DaisyMap.find (Fma (B2Qexp e1) (B2Qexp e2) (B2Qexp e3)) tMap = 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, Heqo4, Heqo6, Heqo8.
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. }
repeat destr_factorize.
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 (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.
......@@ -1224,4 +1311,4 @@ Proof.
+ destruct H7.
exists x, err, vR, x0, M64.
repeat split; auto.
Qed.
\ No newline at end of file
Qed.
coq/Infra/Ltacs.v
View file @ 61171aef
......@@ -78,7 +78,6 @@ Ltac match_factorize_asm :=
=> destruct t eqn:?; cbn in H; try congruence
end.
Ltac match_factorize :=
match_factorize_asm ||
match goal with
......
coq/Infra/MachineType.v
View file @ 61171aef
......@@ -169,6 +169,9 @@ Qed.
Definition join (m1:mType) (m2:mType) :=
if (morePrecise 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. *)
......@@ -238,4 +241,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 @ 61171aef
......@@ -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 @ 61171aef
......@@ -67,6 +67,18 @@ Fixpoint validIntervalbounds (e:exp Q) (A:analysisResult) (P:precond) (validVars
| _, _ => false
end
else false
| Fma f1 f2 f3 =>
if ((validIntervalbounds f1 A P validVars) &&
(validIntervalbounds f2 A P validVars) &&
(validIntervalbounds f3 A P validVars))
then
match DaisyMap.find f1 A, DaisyMap.find f2 A, DaisyMap.find f3 A with
| Some (iv1, _), Some (iv2, _), Some (iv3, _) =>
let new_iv := addIntv iv1 (multIntv iv2 iv3) in
isSupersetIntv new_iv intv
| _, _, _ => false
end
else false
| Downcast _ f1 =>
if (validIntervalbounds f1 A P validVars)
then
......@@ -118,6 +130,13 @@ Proof.
destruct H.
+ apply IHf1; try auto; set_tac.
+ apply IHf2; try auto; set_tac.
- Daisy_compute; try congruence.
destruct H.
+ apply IHf1; try auto; set_tac.
+ set_tac.
destruct H.
* apply IHf2; try auto; set_tac.
* apply IHf3; try auto; set_tac.
- Daisy_compute; try congruence.
apply IHf; try auto; set_tac.
Qed.
......@@ -345,6 +364,32 @@ Proof.
unfold perturb.
lra.
}
- Daisy_compute; try congruence.
destruct IHf1 as [iv_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]]; try auto; set_tac.
destruct IHf2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]]; try auto; set_tac.
destruct IHf3 as [iv_f3 [err3 [vF3 [env3 [eval_f3 valid_f3]]]]]; try auto; set_tac.
assert (M0 = join3 M0 M0 M0) as M0_join by (cbv; auto);
rewrite M0_join.
kill_trivial_exists.
exists (perturb (evalFma vF1 vF2 vF3) 0); split; try auto.
inversion env1; inversion env2; inversion env3; subst.
split; [auto | ].
* econstructor; try congruence; apply Rabs_0_equiv.
* pose proof (interval_multiplication_valid (Q2R (fst iv_f2),Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as valid_mul.
specialize (valid_mul vF2 vF3 valid_f2 valid_f3).
remember (multInterval (Q2R (fst iv_f2), Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as iv_f23prod.
pose proof (interval_addition_valid (Q2R (fst iv_f1),Q2R (snd iv_f1)) (fst iv_f23prod, snd iv_f23prod)) as valid_add.
rewrite Heqiv_f23prod in valid_add, valid_mul.
unfold multIntv in valid_add.
canonize_hyps.
simpl in *.
repeat rewrite <- Q2R_mult in *;
repeat rewrite <- Q2R_min4, <- Q2R_max4 in *;
repeat rewrite <- Q2R_plus in *;
repeat rewrite <- Q2R_min4, <- Q2R_max4 in *.
specialize (valid_add vF1 (vF2 * vF3)%R valid_f1 valid_mul).
unfold evalFma, evalBinop, perturb.
lra.
- match_simpl.
andb_to_prop valid_bounds.
match_simpl.
......@@ -495,4 +540,4 @@ Proof.
pose proof (validIntervalbounds_sound e (E:=E) (Gamma:=Gamma) valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e.
destruct valid_iv_e as [?[?[? [? [? ?]]]]]; try auto.
simpl in *. repeat eexists; repeat split; try eauto; [econstructor; eauto| | ]; lra.
Qed.
\ No newline at end of file
Qed.
coq/Typing.v
View file @ 61171aef
......@@ -24,7 +24,15 @@ Fixpoint typeExpression (V:Type) (Gamma:nat -> option mType) (e:exp V) : option
let tm2 := typeExpression Gamma e2 in
match tm1, tm2 with
| Some m1, Some m2 => Some (join m1 m2)
| _, _=> None
| _, _ => None
end
| Fma e1 e2 e3 =>
let tm1 := typeExpression Gamma e1 in
let tm2 := typeExpression Gamma e2 in
let tm3 := typeExpression Gamma e3 in
match tm1, tm2, tm3 with
| Some m1, Some m2, Some m3 => Some (join3 m1 m2 m3)
| _, _,_ => None
end
| Downcast m e1 =>
let tm1 := typeExpression Gamma e1 in
......@@ -47,6 +55,12 @@ Fixpoint typeMap (Gamma:nat -> option mType) (e:exp Q) (e': exp Q) : option mTyp
| None, Some m2 => Some m2
| None, None => None
end
| Fma e1 e2 e3 => if expEq e e' then typeExpression Gamma e
else
match (typeMap Gamma e1 e'), (typeMap Gamma e2 e'), (typeMap Gamma e3 e') with
| Some m1, Some m2, Some m3 => Some (join3 m1 m2 m3)
| _, _, _ => None
end
| Downcast m e1 => if expEq e e' then typeExpression Gamma (Downcast m e1) else typeMap Gamma e1 e'
end. *)
......@@ -76,6 +90,17 @@ Fixpoint typeMap (Gamma:nat -> option mType) (e:exp Q) (tMap:DaisyMap.t mType)
|Some t1, Some t2 => DaisyMap.add e (join t1 t2) tMap2
| _, _ => DaisyMap.empty mType
end
| Fma e1 e2 e3 =>
let tMap1 := typeMap Gamma e1 tMap in
let tMap2 := typeMap Gamma e2 tMap1 in
let tMap3 := typeMap Gamma e3 tMap2 in
let m1 := DaisyMap.find e1 tMap3 in
let m2 := DaisyMap.find e2 tMap3 in
let m3 := DaisyMap.find e3 tMap3 in
match m1, m2, m3 with
|Some t1, Some t2, Some t3 => DaisyMap.add e (join3 t1 t2 t3) tMap3
| _, _, _ => DaisyMap.empty mType
end
| Downcast m e1 =>
let tMap_new := typeMap Gamma e1 tMap in
let m1 := DaisyMap.find e1 tMap in
......@@ -135,10 +160,18 @@ Fixpoint typeCheck (e:exp Q) (Gamma:nat -> option mType)
| Binop b e1 e2 => match DaisyMap.find e tMap, DaisyMap.find e1 tMap, DaisyMap.find e2 tMap with
| Some m, Some m1, Some m2 =>
mTypeEq m (join m1 m2)
&& typeCheck e1 Gamma tMap
&& typeCheck e2 Gamma tMap
&& typeCheck e1 Gamma tMap
&& typeCheck e2 Gamma tMap
| _, _, _ => false
end
| Fma e1 e2 e3 => match DaisyMap.find e tMap, DaisyMap.find e1 tMap, DaisyMap.find e2 tMap, DaisyMap.find e3 tMap with
| Some m, Some m1, Some m2, Some m3 =>
mTypeEq m (join3 m1 m2 m3)
&& typeCheck e1 Gamma tMap
&& typeCheck e2 Gamma tMap
&& typeCheck e3 Gamma tMap
| _, _, _, _ => false
end
| Downcast m e1 => match DaisyMap.find e tMap, DaisyMap.find e1 tMap with
| Some m', Some m1 => mTypeEq m m' && isMorePrecise m1 m && typeCheck e1 Gamma tMap
| _, _ => false
......@@ -254,6 +287,10 @@ Proof.
- erewrite IHe1 in *; eauto.
erewrite IHe2 in *; eauto.
inversion Heqo0; subst; inversion Heqo1; subst; auto.
- erewrite IHe1 in *; eauto.
erewrite IHe2 in *; eauto.
erewrite IHe3 in *; eauto.
inversion Heqo0; subst; inversion Heqo1; subst; inversion Heqo2; subst; auto.
Qed.
Theorem typingSoundnessCmd c Gamma E v m expTypes:
......@@ -265,4 +302,4 @@ Proof.
Daisy_compute; try congruence; type_conv; subst; inversion bc; subst.
- eapply IHc; eauto.
- eapply typingSoundnessExp; eauto.
Qed.
\ No newline at end of file
Qed.
coq/ssaPrgs.v
View file @ 61171aef
......@@ -35,6 +35,10 @@ Proof.
hnf; intros.
apply in_vars.
rewrite NatSet.union_spec; auto.
- intros vars_fma.
simpl in *.
intros a used_vars.
firstorder.
Qed.
(*
......@@ -588,4 +592,4 @@ Fixpoint exp_subst (e:exp Q) x e_new :=
(* induction ssa_f; *)
(* intros VarEnv ParamEnv P eps fVars_live. *)
(* - *)
(* *) *)
\ No newline at end of file
(* *) *)
hol4/ErrorBoundsScript.sml
View file @ 61171aef
......@@ -201,6 +201,52 @@ val div_abs_err_bounded = store_thm ("div_abs_err_bounded",
\\ once_rewrite_tac[REAL_ABS_MUL]
\\ match_mp_tac REAL_LE_MUL2 \\ fs[REAL_ABS_POS]));
val fma_abs_err_bounded = store_thm ("fma_abs_err_bounded",
``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real) (e3:real exp) (e3R:real) (e3F:real) (err1:real) (err2:real) (err3:real)
(vR:real) (vF:real) (E1 E2 :env) (m m1 m2 m3:mType) (defVars: num -> mType option).
eval_exp E1 (toRMap defVars) (toREval e1) e1R M0 /\
eval_exp E2 defVars e1 e1F m1 /\
eval_exp E1 (toRMap defVars) (toREval e2) e2R M0 /\
eval_exp E2 defVars e2 e2F m2 /\
eval_exp E1 (toRMap defVars) (toREval e3) e3R M0 /\
eval_exp E2 defVars e3 e3F m3 /\
eval_exp E1 (toRMap defVars) (toREval (Fma e1 e2 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 1) (Var 2) (Var 3)) vF m /\
abs (e1R - e1F) <= err1 /\
abs (e2R - e2F) <= err2 /\
abs (e3R - e3F) <= err3 ==>
abs (vR - vF) <= abs ((e1R - e1F) + (e2R * e3R - e2F * e3F)) + abs (e1F + e2F * e3F) * (mTypeToQ m)``,
rpt strip_tac
\\ qpat_x_assum `eval_exp E1 _ (toREval (Fma e1 e2 e3)) _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [toREval_def] thm))
\\ fs []
\\ inversion `eval_exp E1 _ (Fma _ _ _) _ _` eval_exp_cases
\\ rename1 `vR = perturb (evalFma v1R v2R v3R) deltaR`
\\ inversion `eval_exp _ _ (Fma (Var 1) (Var 2) (Var 3)) _ _` eval_exp_cases
\\ rename1 `vF = perturb (evalFma v1F v2F v3F) deltaF`
\\ `(m1' = M0) /\ (m2' = M0) /\ (m3' = M0)` by (rpt conj_tac \\ irule toRMap_eval_M0\\ asm_exists_tac \\ fs[]) \\ fs []
\\ rpt (qpat_x_assum `M0 = _` (fn thm => fs [GSYM thm]))
\\ `perturb (evalFma v1R v2R v3R) deltaR = evalFma v1R v2R v3R` by (match_mp_tac delta_M0_deterministic \\ fs[])
\\ `vR = evalFma v1R v2R v3R` by simp[]
\\ `v1R = e1R` by metis_tac[meps_0_deterministic]
\\ `v2R = e2R` by metis_tac[meps_0_deterministic]
\\ `v3R = e3R` by metis_tac[meps_0_deterministic]
\\ fs[evalFma_def, evalBinop_def, perturb_def]
\\ rpt (inversion `eval_exp (updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv))) _ _ _ _` eval_exp_cases)
\\ fs [updEnv_def] \\ rveq
\\ fs [updDefVars_def] \\ rveq
\\ rewrite_tac [real_sub]
\\ `e1R + e2R * e3R + -((e1F + e2F * e3F) * (1 + deltaF)) = (e1R + e2R * e3R + -(e1F + e2F * e3F)) + (- (e1F + e2F * e3F) * deltaF)` by REAL_ASM_ARITH_TAC
\\ simp[]
\\ qspecl_then [`abs (e1R + e2R * e3R + -(e1F + e2F * e3F)) + abs (-(e1F + e2F * e3F) * deltaF)`] match_mp_tac real_le_trans2
\\ conj_tac
>- (REAL_ASM_ARITH_TAC)
>- (match_mp_tac REAL_LE_ADD2
\\ conj_tac \\ TRY (REAL_ASM_ARITH_TAC)
\\ once_rewrite_tac[REAL_ABS_MUL]
\\ match_mp_tac REAL_LE_MUL2 \\ fs[REAL_ABS_POS]
\\ once_rewrite_tac[GSYM REAL_NEG_LMUL, REAL_ABS_MUL]
\\ once_rewrite_tac[ABS_NEG] \\ fs[]));
val round_abs_err_bounded = store_thm ("round_abs_err_bounded",
``!(e:real exp) (nR:real) (nF1:real) (nF:real) (E1:env) (E2:env) (err:real) (machineEpsilon:mType) (m:mType) (defVars: num -> mType option).
eval_exp E1 (toRMap defVars) (toREval e) nR M0 /\
......
hol4/ErrorValidationScript.sml
View file @ 61171aef
This source diff could not be displayed because it is too large. You can view the blob instead.
hol4/ExpressionsScript.sml
View file @ 61171aef
......@@ -52,15 +52,24 @@ val _ = Datatype `
| Const mType 'v
| Unop unop exp
| Binop binop exp exp
| Fma exp exp exp
| Downcast mType exp`
(**
Define evaluation of FMA (fused multiply-add) on reals
Errors are added on the expression evaluation level later
**)
val evalFma_def = Define `
evalFma v1 v2 v3 = evalBinop Plus v1 (evalBinop Mult v2 v3)`
val toREval_def = Define `
toREval e :real exp =
case e of
| (Var n) => Var n
| (Const m n) => Const M0 n
| (Unop u e1) => Unop u (toREval e1)
| (Unop u e1) => Unop u (toREval e1)
| (Binop bop e1 e2) => Binop bop (toREval e1) (toREval e2)
| (Fma e1 e2 e3) => Fma (toREval e1) (toREval e2) (toREval e3)
| (Downcast m e1) => (toREval e1)`;
(**
......@@ -101,7 +110,13 @@ val (eval_exp_rules, eval_exp_ind, eval_exp_cases) = Hol_reln `
eval_exp E defVars f1 v1 m1 /\
eval_exp E defVars f2 v2 m2 /\
((b = Div) ==> (v2 <> 0)) ==>
eval_exp E defVars (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta) (join m1 m2))`;
eval_exp E defVars (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta) (join m1 m2)) /\
(!E defVars m1 m2 m3 f1 f2 f3 v1 v2 v3 delta.
abs delta <= (mTypeToQ (join3 m1 m2 m3)) /\
eval_exp E defVars f1 v1 m1 /\
eval_exp E defVars f2 v2 m2 /\
eval_exp E defVars f3 v3 m3 ==>
eval_exp E defVars (Fma f1 f2 f3) (perturb (evalFma v1 v2 v3) delta) (join3 m1 m2 m3))`;
val eval_exp_cases_old = save_thm ("eval_exp_cases_old", eval_exp_cases);
......@@ -114,15 +129,17 @@ val eval_exp_cases =
``eval_exp E defVars (Const m1 n) res m2``,
``eval_exp E defVars (Unop u e) res m``,
``eval_exp E defVars (Binop n e1 e2) res m``,
``eval_exp E defVars (Fma e1 e2 e3) res m``,
``eval_exp E defVars (Downcast m1 e1) res m2``]
|> LIST_CONJ |> curry save_thm "eval_exp_cases";
val [Var_load, Const_dist, Unop_neg, Unop_inv, Downcast_dist, Binop_dist] = CONJ_LIST 6 eval_exp_rules;
val [Var_load, Const_dist, Unop_neg, Unop_inv, Downcast_dist, Binop_dist, Fma_dist] = CONJ_LIST 7 eval_exp_rules;
save_thm ("Var_load", Var_load);
save_thm ("Const_dist", Const_dist);
save_thm ("Unop_neg", Unop_neg);
save_thm ("Unop_inv", Unop_inv);
save_thm ("Binop_dist", Binop_dist);
save_thm ("Fma_dist", Fma_dist);
save_thm ("Downcast_dist", Downcast_dist);
(**
......@@ -182,6 +199,17 @@ val Binop_dist' = store_thm ("Binop_dist'",
eval_exp E Gamma (Binop op f1 f2) v m'``,
fs [Binop_dist]);
val Fma_dist' = store_thm ("Fma_dist'",
``!m1 m2 m3 f1 f2 f3 v1 v2 v3 delta v m' E Gamma.
(abs delta) <= (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'``,
fs [Fma_dist]);
(**
Define the set of "used" variables of an expression to be the set of variables
occuring in it
......@@ -192,6 +220,7 @@ val usedVars_def = Define `
| Var x => insert x () (LN)
| Unop u e1 => usedVars e1
| Binop b e1 e2 => union (usedVars e1) (usedVars e2)
| Fma e1 e2 e3 => union (usedVars e1) (union (usedVars e2) (usedVars e3))
| Downcast m e1 => usedVars e1
| _ => LN`;
......@@ -223,7 +252,11 @@ val toRMap_eval_M0 = store_thm (
>- (rveq \\ first_x_assum drule \\ strip_tac \\ fs[])
>- (`m1 = M0` by (rpt (first_x_assum drule \\ strip_tac) \\ fs[])
\\ `m2 = M0` by (rpt (first_x_assum drule \\ strip_tac) \\ fs[])
\\ rveq \\ fs[join_def]));
\\ rveq \\ fs[join_def])
>- (`m1 = M0` by (rpt (first_x_assum drule \\ strip_tac) \\ fs[])
\\ `m2 = M0` by (rpt (first_x_assum drule \\ strip_tac) \\ fs[])
\\ `m3 = M0` by (rpt (first_x_assum drule \\ strip_tac) \\ fs[])
\\ rveq \\ fs[join3_def] \\ fs[join_def]));
(**
Evaluation with 0 as machine epsilon is deterministic
......@@ -264,6 +297,20 @@ val meps_0_deterministic = store_thm("meps_0_deterministic",
\\ qpat_x_assum `!v1 v2 E defVars. _ /\ _ ==> v1 = v2` (fn thm =>qspecl_then [`vf11`,`vf12`] ASSUME_TAC thm)
\\ res_tac
\\ rw[])
>- (rw[]
\\ rpt (
qpat_x_assum `eval_exp _ _ (toREval _) _ _`
(fn thm => assume_tac (ONCE_REWRITE_RULE [toREval_def] thm)))
\\ fs [eval_exp_cases]
\\ `m1 = M0 /\ m2 = M0` by (conj_tac \\ irule toRMap_eval_M0 \\ asm_exists_tac \\ fs [])
\\ `m3 = M0` by (irule toRMap_eval_M0 \\ asm_exists_tac \\ fs [])
\\ `m1' = M0 /\ m2' = M0` by (conj_tac \\ irule toRMap_eval_M0 \\ asm_exists_tac \\ fs [])
\\ `m3' = M0` by (irule toRMap_eval_M0 \\ asm_exists_tac \\ fs [])
\\ rw[]
\\ qpat_x_assum `!v1 v2 E defVars. _ /\ _ ==> v1 = v2` (fn thm =>qspecl_then [`v3`,`v3'`, `E`, `defVars`] ASSUME_TAC thm)
\\ qpat_x_assum `!v1 v2 E defVars. _ /\ _ ==> v1 = v2` (fn thm =>qspecl_then [`v2'`,`v2''`, `E`, `defVars`] ASSUME_TAC thm)
\\ qpat_x_assum `!v1 v2 E defVars. _ /\ _ ==> v1 = v2` (fn thm =>qspecl_then [`v1'`,`v1''`, `E`, `defVars`] ASSUME_TAC thm)
\\ fs [join3_def, join_def, mTypeToQ_def, delta_0_deterministic])
>- (rw[]
\\ rpt (
qpat_x_assum `eval_exp _ _ (toREval (Downcast _ _)) _ _`
......@@ -272,10 +319,10 @@ val meps_0_deterministic = store_thm("meps_0_deterministic",
\\ res_tac));
(**
Helping lemma. Needed in soundness proof.
Helping lemmas. Needed in soundness proof.