Skip to content

GitLab

F
FloVer
Commit 5bbb6b4a authored by Heiko Becker's avatar Heiko Becker
Browse files
Options

Merge branch 'certificates' into 'fma_proofs' 

hol4 FMA proofs

See merge request AVA/daisy!167
parents 423830ed eb84cd10
Expand all Show whitespace changes
Inline Side-by-side
Showing with 1295 additions and 588 deletions
hol4/ErrorBoundsScript.sml
View file @ 5bbb6b4a
......@@ -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 @ 5bbb6b4a
This diff is collapsed.
hol4/ExpressionsScript.sml
View file @ 5bbb6b4a
......@@ -52,8 +52,16 @@ 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
......@@ -61,6 +69,7 @@ val toREval_def = Define `
| (Const m n) => Const M0 n
| (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.
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 Eironment.
variables in the Environment.
**)
val binary_unfolding = store_thm("binary_unfolding",
``!(b:binop) (f1:(real)exp) (f2:(real)exp) E Gamma (v:real) v1 v2 m1 m2 delta.
......@@ -290,6 +337,21 @@ val binary_unfolding = store_thm("binary_unfolding",
fs [updEnv_def,updDefVars_def,join_def,eval_exp_cases,APPLY_UPDATE_THM,PULL_EXISTS]
\\ metis_tac []);
val fma_unfolding = store_thm("fma_unfolding",
``!(f1:(real)exp) (f2:(real)exp) (f3:(real)exp) E Gamma (v:real) v1 v2 v3 m1 m2 m3 delta.
(abs delta) <= (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) ==>
eval_exp (updEnv 3 v3 (updEnv 2 v2 (updEnv 1 v1 emptyEnv)))
(updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 Gamma)))
(Fma (Var 1) (Var 2) (Var 3)) (perturb (evalFma v1 v2 v3) delta) (join3 m1 m2 m3)``,
fs [updEnv_def,updDefVars_def,join3_def,join_def,eval_exp_cases,APPLY_UPDATE_THM,PULL_EXISTS]
\\ rpt strip_tac
\\ qexists_tac `delta'`
\\ conj_tac \\ fs[]);
val eval_eq_env = store_thm (
"eval_eq_env",
``!e E1 E2 Gamma v m.
......@@ -307,6 +369,8 @@ val eval_eq_env = store_thm (
\\ first_x_assum drule \\ disch_then irule \\ fs[])
>- (rveq \\ qexistsl_tac [`m1`, `m2`, `v1`, `v2`, `delta'`]
\\ fs[] \\ conj_tac \\ first_x_assum irule \\ asm_exists_tac \\ fs[])
>- (rveq \\ qexistsl_tac [`m1`, `m2`, `m3`, `v1`, `v2`, `v3`, `delta'`]
\\ fs[] \\ prove_tac [])
>- (rveq \\ qexistsl_tac [`m1'`, `v1`, `delta'`] \\ fs[]
\\ first_x_assum drule \\ disch_then irule \\ fs[]));
......
hol4/FPRangeValidatorScript.sml
View file @ 5bbb6b4a
......@@ -31,6 +31,10 @@ val FPRangeValidator_def = Define `
| 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
......
hol4/IEEE_connectionScript.sml
View file @ 5bbb6b4a
......@@ -39,6 +39,9 @@ val eval_exp_float_def = Define `
| Mult => SOME (fp64_mul dmode v1 v2)
| Div => SOME (fp64_div dmode v1 v2))
| _, _ => NONE)) /\
(eval_exp_float (Fma e1 e2 e3) E =
(case (eval_exp_float e1 E), (eval_exp_float e2 E), (eval_exp_float e2 E) of
| _, _, _ => NONE)) /\
(eval_exp_float (Downcast m e) E = NONE)`;
val bstep_float_def = Define `
......@@ -75,6 +78,24 @@ val eval_exp_valid_def = Define `
normal_or_zero (evalBinop b v1_real v2_real))
T)
T)) /\
(eval_exp_valid (Fma e1 e2 e3) E =
(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)
(\ v1. let v1_real = float_to_real (fp64_to_float v1)
in
optionLift e2_res
(\ v2.
let v2_real = float_to_real (fp64_to_float v2)
in
optionLift e3_res
(\ v3. let v3_real = float_to_real (fp64_to_float v3) in
F)
T)
T)
T)) /\
(eval_exp_valid (Downcast m e) E = eval_exp_valid e E)`;
val bstep_valid_def = Define `
......@@ -90,6 +111,7 @@ val toRExp_def = Define `
(toRExp (Const m c) = Const m (float_to_real (fp64_to_float c))) /\
(toRExp (Unop u e1) = Unop u (toRExp e1)) /\
(toRExp (Binop b e1 e2) = Binop b (toRExp e1) (toRExp e2)) /\
(toRExp (Fma e1 e2 e3) = Fma (toRExp e1) (toRExp e2) (toRExp e3)) /\
(toRExp (Downcast m e1) = Downcast m (toRExp e1))`;
val toRCmd_def = Define `
......@@ -436,6 +458,7 @@ val noDowncast_def = Define `
(noDowncast (Const _ _) = T) /\
(noDowncast (Unop _ e) = noDowncast e) /\
(noDowncast (Binop b e1 e2) = (noDowncast e1 /\ noDowncast e2)) /\
(noDowncast (Fma e1 e2 e3) = (noDowncast e1 /\ noDowncast e2 /\ noDowncast e3)) /\
(noDowncast (Downcast _ _) = F)`;
val noDowncastFun_def = Define `
......@@ -453,6 +476,7 @@ val is64BitEval_def = Define `
(is64BitEval ((Const m c):real exp) = (m = M64)) /\
(is64BitEval (Unop _ e) = is64BitEval e) /\
(is64BitEval (Binop b e1 e2) = (is64BitEval e1 /\ is64BitEval e2)) /\
(is64BitEval (Fma e1 e2 e3) = (is64BitEval e1 /\ is64BitEval e2 /\ is64BitEval e3)) /\
(is64BitEval (Downcast m e) = is64BitEval e) /\
(is64BitEval ((Var v):real exp) = T)`;
......@@ -502,7 +526,30 @@ Induct
\\ qexists_tac `Gamma` \\ rpt strip_tac
>- (first_x_assum irule \\ simp[Once usedVars_def, domain_union])
\\ Cases_on `tMap e1` \\ Cases_on `tMap e2` \\ fs[])
\\ fs[join_def]));
\\ fs[join_def])
>- (rename1 `Fma e1 e2 e3`
\\ rw_thm_asm `typeCheck (Fma e1 e2 e3) _ _` typeCheck_def
\\ fs[]
\\ Cases_on `tMap (Fma e1 e2 e3)` \\ fs[]
\\ `tMap e3 = SOME M64`
by (first_x_assum irule
>- (rw_thm_asm `is64BitEval _` is64BitEval_def \\ fs[])
\\ qexists_tac `Gamma` \\ rpt strip_tac
>- (first_x_assum irule \\ simp[Once usedVars_def, domain_union])
\\ Cases_on `tMap e1` \\ Cases_on `tMap e2` \\ Cases_on `tMap e3` \\ fs[])
\\ `tMap e2 = SOME M64`
by (first_x_assum irule
>- (rw_thm_asm `is64BitEval _` is64BitEval_def \\ fs[])
\\ qexists_tac `Gamma` \\ rpt strip_tac
>- (first_x_assum irule \\ simp[Once usedVars_def, domain_union])
\\ Cases_on `tMap e1` \\ Cases_on `tMap e2` \\ Cases_on `tMap e3` \\ fs[])
\\ `tMap e1 = SOME M64`
by (first_x_assum irule
>- (rw_thm_asm `is64BitEval _` is64BitEval_def \\ fs[])
\\ qexists_tac `Gamma` \\ rpt strip_tac
>- (first_x_assum irule \\ simp[Once usedVars_def, domain_union])
\\ Cases_on `tMap e1` \\ Cases_on `tMap e2` \\ Cases_on `tMap e3` \\ fs[])
\\ fs[join3_def, join_def]));
val typing_cmd_64bit = store_thm (
"typing_cmd_64bit",
......@@ -563,6 +610,18 @@ val typing_agrees_exp = store_thm (
\\ rpt (disch_then drule) \\ fs[])
\\ `m2' = x'` by (first_x_assum drule\\ rpt (disch_then drule) \\ fs[])
\\ rveq \\ fs[])
>- (rw_thm_asm `typeCheck _ _ _` typeCheck_def
\\ fs[]
\\ qpat_x_assum `tMap (Fma _ _ _) = SOME _` (fn thm => fs[thm])
\\ Cases_on `tMap e` \\ Cases_on `tMap e'` \\ Cases_on `tMap e''` \\ fs[]
\\ `m1' = x`
by (qpat_x_assum `!E Gamma tMap v m1 m2. typeCheck e _ _ /\ _ /\ _ ==> _` drule
\\ rpt (disch_then drule) \\ fs[])
\\ `m2' = x'`
by (qpat_x_assum `!E Gamma tMap v m1 m2. typeCheck e' _ _ /\ _ /\ _ ==> _` drule
\\ rpt (disch_then drule) \\ fs[])
\\ `m3 = x''` by (first_x_assum drule\\ rpt (disch_then drule) \\ fs[])
\\ rveq \\ fs[])
>- (rw_thm_asm `typeCheck _ _ _` typeCheck_def
\\ fs[]
\\ qpat_x_assum `tMap (Downcast m e) = SOME _` (fn thm => fs[thm])
......@@ -1074,7 +1133,87 @@ val eval_exp_gives_IEEE = store_thm ("eval_exp_gives_IEEE",
by (fs[GSYM float_is_zero_to_real, float_is_zero_def])
\\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
`float_to_real (fp64_to_float vF2)`, `0:real`]
\\ fs[perturb_def, join_def, mTypeToQ_pos])));
\\ fs[perturb_def, join_def, mTypeToQ_pos]))
>- (rename1 `Fma (toRExp e1) (toRExp e2) (toRExp e3)`
\\ qpat_x_assum `M64 = _` (fn thm => fs [GSYM thm])
\\ `tMap (toRExp e1) = SOME M64 /\ tMap(toRExp e2) = SOME M64 /\ tMap (toRExp e3) = SOME M64 /\ tMap (Fma (toRExp e1) (toRExp e2) (toRExp e3)) = SOME M64`
by (rpt conj_tac \\ irule typing_exp_64bit \\ fs[is64BitEval_def, noDowncast_def]
\\ qexists_tac `Gamma` \\ fs[]
\\ rw_thm_asm `typeCheck _ _ _` typeCheck_def \\ fs[]
\\ Cases_on `tMap (toRExp e1)` \\ Cases_on `tMap (toRExp e2)` \\ Cases_on `tMap (toRExp e3)`
\\ Cases_on `tMap (Fma (toRExp e1) (toRExp e2) (toRExp e3))` \\ fs[]
\\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def, domain_union])
\\ `m1 = M64 /\ m2 = M64 /\ m3 = M64`
by (rpt conj_tac
\\ rw_thm_asm `typeCheck _ _ _` typeCheck_def
\\ irule typing_agrees_exp
\\ qexistsl_tac [`toREnv E2`, `Gamma`]
THENL [qexists_tac `toRExp e1`, qexists_tac `toRExp e2`, qexists_tac `toRExp e3`]
\\ qexistsl_tac [`tMap`]
THENL [qexists_tac `v1`, qexists_tac `v2`, qexists_tac `v3`]
\\ fs[]
\\ rw_asm_star `tMap (toRExp e1) = _`
\\ rw_asm_star `tMap (toRExp e2) = _`
\\ rw_asm_star `tMap (toRExp e3) = _`
\\ rw_asm_star `tMap (Fma (toRExp e1) (toRExp e2) (toRExp e3)) = _`)
\\ rveq
\\ ntac 3 (first_x_assum (qspecl_then [`E1`, `E2`,`E2_real`, `Gamma`, `tMap`] assume_tac))
\\ first_x_assum (qspecl_then [`v1`, `A`, `P`, `fVars`, `dVars`] destruct)
>- (rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def
\\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
\\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
\\ rw_thm_asm `typeCheck _ _ _` typeCheck_def
\\ rw_thm_asm `is64BitEval _` is64BitEval_def
\\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
\\ rw_thm_asm `noDowncast _` noDowncast_def
\\ Cases_on `A (Fma (toRExp e1) (toRExp e2) (toRExp e3))`
\\ Cases_on `A (toRExp e1)`
\\ Cases_on `A (toRExp e2)`
\\ Cases_on `A (toRExp e3)` \\ fs[]
\\ rpt (qpat_x_assum `tMap _ = _` (fn thm => fs[thm]))
\\ fs[]
\\ rpt conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
\\ fs[domain_union, DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def, domain_union])
\\ first_x_assum (qspecl_then [`v2`, `A`, `P`, `fVars`, `dVars`] destruct)
>- (rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def
\\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
\\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
\\ rw_thm_asm `typeCheck _ _ _` typeCheck_def
\\ rw_thm_asm `is64BitEval _` is64BitEval_def
\\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
\\ rw_thm_asm `noDowncast _` noDowncast_def
\\ Cases_on `A (Fma (toRExp e1) (toRExp e2) (toRExp e3))`
\\ Cases_on `A (toRExp e1)`
\\ Cases_on `A (toRExp e2)`
\\ Cases_on `A (toRExp e3)` \\ fs[]
\\ rpt (qpat_x_assum `tMap _ = _` (fn thm => fs[thm]))
\\ fs[]
\\ rpt conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
\\ fs[domain_union, DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def, domain_union])
\\ first_x_assum (qspecl_then [`v3`, `A`, `P`, `fVars`, `dVars`] destruct)
>- (rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def
\\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
\\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
\\ rw_thm_asm `typeCheck _ _ _` typeCheck_def
\\ rw_thm_asm `is64BitEval _` is64BitEval_def
\\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
\\ rw_thm_asm `noDowncast _` noDowncast_def
\\ Cases_on `A (Fma (toRExp e1) (toRExp e2) (toRExp e3))`
\\ Cases_on `A (toRExp e1)`
\\ Cases_on `A (toRExp e2)`
\\ Cases_on `A (toRExp e3)` \\ fs[]
\\ rpt (qpat_x_assum `tMap _ = _` (fn thm => fs[thm]))
\\ fs[]
\\ rpt conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
\\ fs[domain_union, DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def, domain_union])
\\ fs[]
\\ rename1 `eval_exp_float e1 _ = SOME vF1`
\\ rename1 `eval_exp_float e2 _ = SOME vF2`
\\ rename1 `eval_exp_float e3 _ = SOME vF3`
\\ fs[optionLift_def]));
val bstep_gives_IEEE = store_thm (
"bstep_gives_IEEE",
......
hol4/Infra/MachineTypeScript.sml
View file @ 5bbb6b4a
......@@ -64,6 +64,9 @@ val join_def = Define `
join (m1:mType) (m2:mType) =
if (isMorePrecise m1 m2) then m1 else m2`;
val join3_def = Define `
join3 (m1: mType) (m2: mType) (m3: mType) = join m1 (join m2 m3)`;
(* val M0_join_is_M0 = store_thm ("M0_join_is_M0", *)
(* ``!m1 m2. *)
(* join m1 m2 = M0 ==> *)
......
hol4/IntervalValidationScript.sml
View file @ 5bbb6b4a
......@@ -69,6 +69,17 @@ val validIntervalbounds_def = Define `
let new_iv = divideInterval iv1 iv2 in
isSupersetInterval new_iv intv
else F
else F)
| 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 = addInterval iv1 (multInterval iv2 iv3) in
isSupersetInterval new_iv intv
else F)`;
val validIntervalboundsCmd_def = Define `
......@@ -108,6 +119,13 @@ val ivbounds_approximatesPrecond_sound = store_thm ("ivbounds_approximatesPrecon
\\ `validIntervalbounds f1 absenv P V /\ validIntervalbounds f2 absenv P V`
by (Cases_on `absenv (Binop b f1 f2)` \\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ fs [Once validIntervalbounds_def])
\\ fs [domain_union])
>- (rpt (
first_x_assum
(fn thm => qspecl_then [`absenv`, `P`, `V`] assume_tac thm))
\\ rename1 `Fma f1 f2 f3`
\\ `validIntervalbounds f1 absenv P V /\ validIntervalbounds f2 absenv P V /\ validIntervalbounds f3 absenv P V`
by (Cases_on `absenv (Fma f1 f2 f3)` \\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ Cases_on `absenv f3` \\ fs [Once validIntervalbounds_def])
\\ fs [domain_union])
>- (rpt (
first_x_assum
(fn thm => qspecl_then [`absenv`, `P`, `V`] assume_tac thm))
......@@ -425,6 +443,103 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
(SND iv_f * (inv (SND iv_f')))
(SND iv_f * (inv (FST iv_f')))`
\\ metis_tac []))))
(* FMA case *)
>- (rename1 `Fma f1 f2 f3`
\\ `?v1. eval_exp E (toRMap Gamma) (toREval f1) v1 M0 /\
(FST (FST (absenv f1))) <= v1 /\ (v1 <= SND (FST (absenv f1)))`
by (first_x_assum match_mp_tac
\\ qexistsl_tac [`P`, `fVars`, `dVars`]
\\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
\\ Cases_on `absenv (Fma f1 f2 f3)`
\\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ Cases_on `absenv f3`
\\ fs []
\\ conj_tac
\\ fs[Once usedVars_def, domain_union, UNION_DEF, DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac
\\ first_x_assum match_mp_tac \\ fs[]
\\ DISJ1_TAC
\\ simp[Once usedVars_def])
\\ qpat_x_assum `! absenv P fVars dVars E Gamma. _ ==> ?vR. eval_exp E (toRMap Gamma) (toREval f1) _ _ /\ _ /\ _` kall_tac
\\ `?v2. eval_exp E (toRMap Gamma) (toREval f2) v2 M0 /\
(FST (FST (absenv f2))) <= v2 /\ (v2 <= SND (FST (absenv f2)))`
by (first_x_assum match_mp_tac
\\ qexistsl_tac [`P`, `fVars`, `dVars`]
\\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
\\ Cases_on `absenv (Fma f1 f2 f3)`
\\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ Cases_on `absenv f3`
\\ fs []
\\ conj_tac \\ fs []
\\ fs[Once usedVars_def, domain_union, UNION_DEF, DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac
\\ first_x_assum match_mp_tac \\ fs[]
\\ DISJ2_TAC
\\ simp[Once usedVars_def])
\\ qpat_x_assum `! absenv P fVars dVars E Gamma. _ ==> ?vR. eval_exp E (toRMap Gamma) (toREval f2) _ _ /\ _ /\ _` kall_tac
\\ `?v3. eval_exp E (toRMap Gamma) (toREval f3) v3 M0 /\
(FST (FST (absenv f3))) <= v3 /\ (v3 <= SND (FST (absenv f3)))`
by (first_x_assum match_mp_tac
\\ qexistsl_tac [`P`, `fVars`, `dVars`]
\\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
\\ Cases_on `absenv (Fma f1 f2 f3)`
\\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ Cases_on `absenv f3`
\\ fs []
\\ conj_tac \\ fs []
\\ fs[Once usedVars_def, domain_union, UNION_DEF, DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac
\\ first_x_assum match_mp_tac \\ fs[]
\\ DISJ2_TAC \\ DISJ2_TAC
\\ simp[Once usedVars_def])
\\ qpat_x_assum `! absenv P fVars dVars E Gamma. _ ==> ?vR. eval_exp E (toRMap Gamma) (toREval f3) _ _ /\ _ /\ _` kall_tac
\\ fs []
\\ rw_thm_asm `validIntervalbounds (Fma f1 f2 f3) absenv P V` validIntervalbounds_def
\\ Cases_on `absenv (Fma f1 f2 f3)` \\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ Cases_on `absenv f3`
\\ qmatch_assum_rename_tac `absenv (Fma f1 f2 f3) = (iv_b,err_b)`
\\ qmatch_assum_rename_tac `absenv f1 = (iv_f1,err_f1)`
\\ qmatch_assum_rename_tac `absenv f2 = (iv_f2,err_f2)`
\\ qmatch_assum_rename_tac `absenv f3 = (iv_f3,err_f3)`
\\ qexists_tac `evalFma v1 v2 v3`
\\ fs[evalFma_def, evalBinop_def, isSupersetInterval_def, absIntvUpd_def, IVlo_def, IVhi_def, multInterval_def, addInterval_def]
\\ qspecl_then [`iv_f2`, `iv_f3`, `v2`, `v3`]
assume_tac
(REWRITE_RULE
[validIntervalAdd_def,
multInterval_def,
absIntvUpd_def,
contained_def,
IVhi_def,
IVlo_def] interval_multiplication_valid)
\\ qspecl_then [`iv_f1`, `multInterval iv_f2 iv_f3`, `v1`, `v2 * v3`]
assume_tac
(REWRITE_RULE
[validIntervalAdd_def,
addInterval_def,
multInterval_def,
absIntvUpd_def,
contained_def,
IVhi_def, IVlo_def] interval_addition_valid)
\\ fs[multInterval_def, absIntvUpd_def, IVlo_def, IVhi_def] \\ res_tac
\\ rpt conj_tac
>- (match_mp_tac Fma_dist'
\\ qexistsl_tac [`M0`, `M0`, `M0`, `v1`, `v2`, `v3`, `0:real`]
\\ fs [mTypeToQ_def, perturb_def, evalFma_def, evalBinop_def, join3_def, join_def])
>- (match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac
\\ conj_tac \\ fs[])
>- (match_mp_tac REAL_LE_TRANS
\\ qexists_tac `max4
(FST iv_f1 +
min4 (FST iv_f2 * FST iv_f3) (FST iv_f2 * SND iv_f3)
(SND iv_f2 * FST iv_f3) (SND iv_f2 * SND iv_f3))
(FST iv_f1 +
max4 (FST iv_f2 * FST iv_f3) (FST iv_f2 * SND iv_f3)
(SND iv_f2 * FST iv_f3) (SND iv_f2 * SND iv_f3))
(SND iv_f1 +
min4 (FST iv_f2 * FST iv_f3) (FST iv_f2 * SND iv_f3)
(SND iv_f2 * FST iv_f3) (SND iv_f2 * SND iv_f3))
(SND iv_f1 +
max4 (FST iv_f2 * FST iv_f3) (FST iv_f2 * SND iv_f3)
(SND iv_f2 * FST iv_f3) (SND iv_f2 * SND iv_f3))`
\\conj_tac \\ fs[]))
(* Downcast case *)
>- (`?v. eval_exp E (toRMap Gamma) (toREval f) v M0 /\
FST(FST(absenv f)) <= v /\ v <= SND (FST(absenv f))`
......@@ -483,6 +598,7 @@ val swap_Gamma_eval_exp = store_thm (
>- (qexists_tac `v1` \\ fs[])
>- (qexistsl_tac [`v1`, `delta`] \\ fs[])
>- (qexistsl_tac [`m1`, `m2`, `v1`, `v2`, `delta`] \\ fs[])
>- (qexistsl_tac [`m1`, `m2`, `m3`, `v1`, `v2`, `v3`, `delta`] \\ fs[])
>- (qexistsl_tac [`m1'`, `v1`, `delta`] \\ fs[]));
val swap_Gamma_bstep = store_thm (
......@@ -678,6 +794,36 @@ val validIntervalbounds_validates_iv = store_thm ("validIntervalbounds_validates
\\ asm_exists_tac \\ fs []
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs []))
>- (rename1 `Fma f1 f2 f3`
\\ qpat_x_assum `validIntervalbounds _ _ _ _`
(fn thm => ASSUME_TAC (ONCE_REWRITE_RULE[validIntervalbounds_def] thm))
\\ Cases_on `absenv (Fma f1 f2 f3)` \\ rename1 `absenv (Fma f1 f2 f3) = (iv,err)`
\\ fs[]
\\ `valid (FST (absenv f1))`
by (first_x_assum match_mp_tac
\\ qexists_tac `P` \\ qexists_tac `dVars`
\\ fs[])
\\ `valid (FST (absenv f2))`
by (first_x_assum match_mp_tac
\\ qexists_tac `P` \\ qexists_tac `dVars`