Commit 0b96b0da authored by Nikita Zyuzin's avatar Nikita Zyuzin

Complete error validation proofs

parent 450c6c09
......@@ -209,7 +209,7 @@ val fma_abs_err_bounded = store_thm ("fma_abs_err_bounded",
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 m2 /\
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 /\
......
This diff is collapsed.
......@@ -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
......
......@@ -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",
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment