Commit 06ad54de authored by Heiko Becker's avatar Heiko Becker
Browse files

Fix bug in FMA evaluation, add some small lemmas

parent 65bfd34f
......@@ -150,4 +150,12 @@ Proof
\\ fs[]
QED
Theorem CertificateCheckerCmd_Gamma_is_getValidMapCmd:
CertificateCheckerCmd f A P dVars = SOME Gamma
getValidMapCmd dVars f FloverMapTree_empty = Succes Gamma
Proof
fs[CertificateCheckerCmd_def]
\\ rpt (TOP_CASE_TAC \\ fs[])
QED
val _ = export_theory();
......@@ -30,6 +30,7 @@ val toREvalCmd_def = Define `
val (bstep_rules, bstep_ind, bstep_cases) = Hol_reln `
(!m m' x e s E v res Gamma.
eval_expr E Gamma e v m /\
Gamma (Var x) = SOME m
bstep s (updEnv x v E) Gamma res m' ==>
bstep (Let m x e s) E Gamma res m') /\
(!m e E v Gamma.
......
......@@ -293,8 +293,8 @@ Proof
QED
val float_fma_tac =
`e1R + e2R * e3R + -((e1F + e2F * e3F) * (1 + deltaF)) =
(e1R + e2R * e3R + -(e1F + e2F * e3F)) + (- (e1F + e2F * e3F) * deltaF)`
`e1R * e2R + e3R + -((1 + deltaF) * (e1F * e2F + e3F)) =
(e1R * e2R + e3R + -(e1F * e2F + e3F)) + (- (e1F * e2F + e3F) * deltaF)`
by REAL_ASM_ARITH_TAC
\\ simp[]
\\ triangle_tac
......@@ -324,8 +324,8 @@ Theorem fma_abs_err_bounded:
abs (e2R - e2F) <= err2 /\
abs (e3R - e3F) <= err3 ==>
abs (vR - vF) <=
abs ((e1R - e1F) + (e2R * e3R - e2F * e3F)) +
computeError (e1F + e2F * e3F) m
abs ((e1R * e2R - e1F * e2F) + (e3R - e3F)) +
computeError (e1F * e2F + e3F) m
Proof
rpt strip_tac \\ fs[toREval_def]
\\ inversion `eval_expr E1 _ (Fma _ _ _) _ _` eval_expr_cases
......@@ -350,15 +350,15 @@ Proof
\\ Cases_on `mF`
\\ fs[computeError_def, perturb_def]
\\ rewrite_tac[real_sub]
>- (`e1R + e2R * e3R + - (e1F + e2F * e3F) =
e1R + - e1F + (e2R * e3R + - (e2F * e3F))`
>- (`e1R * e2R + e3R + - (e1F * e2F + e3F) =
(e1R * e2R + - (e1F * e2F) + (e3R + - e3F))`
by REAL_ASM_ARITH_TAC
\\ simp[])
>- (float_fma_tac)
>- (float_fma_tac)
>- (float_fma_tac)
\\ `e1R + e2R * e3R + -(e1F + e2F * e3F + deltaF) =
(e1R + e2R * e3R + - (e1F + e2F * e3F)) + - deltaF`
\\ `e1R * e2R + e3R + -(e1F * e2F + e3F + deltaF) =
(e1R * e2R + e3R + - (e1F * e2F + e3F)) + - deltaF`
by REAL_ASM_ARITH_TAC
\\ simp[]
\\ triangle_tac
......
......@@ -98,10 +98,10 @@ val validErrorbound_def = Define `
upperBoundE1 = maxAbs ive1;
upperBoundE2 = maxAbs ive2;
upperBoundE3 = maxAbs ive3;
errIntv_prod = multInterval errIve2 errIve3;
mult_error_bound = (upperBoundE2 * err3 + upperBoundE3 * err2 + err2 * err3);
mAbs = maxAbs (addInterval errIve1 errIntv_prod) in
err1 + mult_error_bound + computeError mAbs m <= err
errIntv_prod = multInterval errIve1 errIve2;
mult_error_bound = (upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2);
mAbs = maxAbs (addInterval errIntv_prod errIve3 ) in
mult_error_bound + err3 + computeError mAbs m <= err
|_, _, _ => F
else F)
| Downcast m1 e1 =>
......@@ -2100,35 +2100,36 @@ val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
\\ assume_tac (REWRITE_RULE [contained_def] interval_division_valid)
\\ fs[contained_def, widenInterval_def, noDivzero_def]);
val validErrorboundCorrectFma = store_thm ("validErrorboundCorrectFma",
``!(E1 E2:env) (A:analysisResult) (e1:real expr) (e2:real expr) (e3: real expr)
(nR nR1 nR2 nR3 nF nF1 nF2 nF3:real) (e err1 err2 err3:real)
(alo ahi e1lo e1hi e2lo e2hi e3lo e3hi :real) dVars m m1 m2 m3 Gamma.
eval_Real E1 Gamma e1 nR1 /\
eval_Real E1 Gamma e2 nR2 /\
eval_Real E1 Gamma e3 nR3 /\
eval_Real E1 Gamma (Fma e1 e2 e3) nR /\
eval_Fin E2 Gamma e1 nF1 m1 /\
eval_Fin E2 Gamma e2 nF2 m2 /\
eval_Fin E2 Gamma e3 nF3 m3 /\
eval_expr (updEnv 3 nF3 (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)))
(updDefVars (Fma (Var 1) (Var 2) (Var 3)) m
(updDefVars (Var 3) m3
(updDefVars (Var 2) m2 (updDefVars (Var 1) m1 (toRExpMap Gamma)))))
(Fma (Var 1) (Var 2) (Var 3)) nF m /\
validErrorbound (Fma e1 e2 e3) Gamma A dVars /\
(e1lo <= nR1 /\ nR1 <= e1hi) /\
(e2lo <= nR2 /\ nR2 <= e2hi) /\
(e3lo <= nR3 /\ nR3 <= e3hi) /\
FloverMapTree_find e1 A = SOME ((e1lo, e1hi), err1) /\
FloverMapTree_find e2 A = SOME ((e2lo, e2hi), err2) /\
FloverMapTree_find e3 A = SOME ((e3lo, e3hi), err3) /\
FloverMapTree_find (Fma e1 e2 e3) A = SOME ((alo, ahi), e) /\
FloverMapTree_find (Fma e1 e2 e3) Gamma = SOME m /\
abs (nR1 - nF1) <= err1 /\
abs (nR2 - nF2) <= err2 /\
abs (nR3 - nF3) <= err3 ==>
abs (nR - nF) <= e``,
Theorem validErrorboundCorrectFma:
!(E1 E2:env) (A:analysisResult) (e1:real expr) (e2:real expr) (e3: real expr)
(nR nR1 nR2 nR3 nF nF1 nF2 nF3:real) (e err1 err2 err3:real)
(alo ahi e1lo e1hi e2lo e2hi e3lo e3hi :real) dVars m m1 m2 m3 Gamma.
eval_Real E1 Gamma e1 nR1 /\
eval_Real E1 Gamma e2 nR2 /\
eval_Real E1 Gamma e3 nR3 /\
eval_Real E1 Gamma (Fma e1 e2 e3) nR /\
eval_Fin E2 Gamma e1 nF1 m1 /\
eval_Fin E2 Gamma e2 nF2 m2 /\
eval_Fin E2 Gamma e3 nF3 m3 /\
eval_expr (updEnv 3 nF3 (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)))
(updDefVars (Fma (Var 1) (Var 2) (Var 3)) m
(updDefVars (Var 3) m3
(updDefVars (Var 2) m2 (updDefVars (Var 1) m1 (toRExpMap Gamma)))))
(Fma (Var 1) (Var 2) (Var 3)) nF m /\
validErrorbound (Fma e1 e2 e3) Gamma A dVars /\
(e1lo <= nR1 /\ nR1 <= e1hi) /\
(e2lo <= nR2 /\ nR2 <= e2hi) /\
(e3lo <= nR3 /\ nR3 <= e3hi) /\
FloverMapTree_find e1 A = SOME ((e1lo, e1hi), err1) /\
FloverMapTree_find e2 A = SOME ((e2lo, e2hi), err2) /\
FloverMapTree_find e3 A = SOME ((e3lo, e3hi), err3) /\
FloverMapTree_find (Fma e1 e2 e3) A = SOME ((alo, ahi), e) /\
FloverMapTree_find (Fma e1 e2 e3) Gamma = SOME m /\
abs (nR1 - nF1) <= err1 /\
abs (nR2 - nF2) <= err2 /\
abs (nR3 - nF3) <= err3 ==>
abs (nR - nF) <= e
Proof
fs [toREval_def]
\\ rpt strip_tac \\ simp[Once toREval_def]
\\ Flover_compute ``validErrorbound`` \\ fs [] \\ rveq
......@@ -2142,8 +2143,8 @@ val validErrorboundCorrectFma = store_thm ("validErrorboundCorrectFma",
by (irule err_always_positive
\\ rpt (asm_exists_tac \\ fs[]))
\\ irule REAL_LE_TRANS
\\ qexists_tac `abs ((nR1 - nF1) + (nR2 * nR3 - nF2 * nF3)) +
computeError (nF1 + nF2 * nF3) m`
\\ qexists_tac `abs ((nR1 * nR2 - nF1 * nF2) + (nR3 - nF3)) +
computeError (nF1 * nF2 + nF3) m`
\\ conj_tac
>- (irule fma_abs_err_bounded \\ rpt conj_tac
\\ rpt (find_exists_tac \\ fs[toREval_def]))
......@@ -2153,6 +2154,10 @@ val validErrorboundCorrectFma = store_thm ("validErrorboundCorrectFma",
>- (irule triangle_trans \\ fs[REAL_ABS_TRIANGLE]
\\ irule REAL_LE_ADD2 \\ fs[]
\\ irule multiplicationErrorBounded \\ fs[])
\\ `contained nF1 (widenInterval (e1lo,e1hi) err1)`
by (irule distance_gives_iv
\\ qexists_tac `nR1` \\ conj_tac
\\ simp[contained_def, IVlo_def, IVhi_def])
\\ `contained nF2 (widenInterval (e2lo,e2hi) err2)`
by (irule distance_gives_iv
\\ qexists_tac `nR2` \\ conj_tac
......@@ -2161,22 +2166,19 @@ val validErrorboundCorrectFma = store_thm ("validErrorboundCorrectFma",
by (irule distance_gives_iv
\\ qexists_tac `nR3` \\ conj_tac
\\ simp[contained_def, IVlo_def, IVhi_def])
\\ `contained (nF2 * nF3)
(multInterval (widenInterval (e2lo, e2hi) err2)
(widenInterval (e3lo, e3hi) err3))`
\\ `contained (nF1 * nF2)
(multInterval (widenInterval (e1lo, e1hi) err1)
(widenInterval (e2lo, e2hi) err2))`
by (irule
(ONCE_REWRITE_RULE [validIntervalMult_def] interval_multiplication_valid)
\\ conj_tac \\ simp[])
\\ `contained nF1 (widenInterval (e1lo,e1hi) err1)`
by (irule distance_gives_iv
\\ qexists_tac `nR1` \\ conj_tac
\\ simp[contained_def])
\\ qmatch_abbrev_tac `_ <= computeError (maxAbs iv) _`
\\ PairCases_on `iv` \\ irule computeError_up
\\ unabbrev_all_tac \\ fs[maxAbs_def]
\\ irule maxAbs
\\ assume_tac (REWRITE_RULE [validIntervalAdd_def, contained_def] interval_addition_valid)
\\ fs[contained_def, widenInterval_def, IVlo_def, IVhi_def, noDivzero_def]);
\\ fs[contained_def, widenInterval_def, IVlo_def, IVhi_def, noDivzero_def]
QED
val validErrorboundCorrectRounding = store_thm ("validErrorboundCorrectRounding",
``!(E1 E2:env) (A:analysisResult) (e:real expr)
......@@ -2543,21 +2545,21 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
\\ irule Var_load
\\ fs[updDefVars_def, updEnv_def]));
val validErrorboundCmd_gives_eval = store_thm (
"validErrorboundCmd_gives_eval",
``!(f:real cmd) (A:analysisResult) (E1 E2:env)
(outVars fVars dVars:num_set) (vR elo ehi err:real)
(m:mType) Gamma.
validTypesCmd f Gamma /\
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 /\
ssa f (union fVars dVars) outVars /\
((domain (freeVars f)) DIFF (domain dVars)) SUBSET (domain fVars) /\
bstep (toREvalCmd f) E1 (toRTMap (toRExpMap Gamma)) vR REAL /\
validErrorboundCmd f Gamma A dVars /\
validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) /\
FloverMapTree_find (getRetExp f) A = SOME ((elo,ehi),err) ==>
?vF m.
bstep f E2 (toRExpMap Gamma) vF m``,
Theorem validErrorboundCmd_gives_eval:
!(f:real cmd) (A:analysisResult) (E1 E2:env)
(outVars fVars dVars:num_set) (vR elo ehi err:real)
(m:mType) Gamma.
validTypesCmd f Gamma /\
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 /\
ssa f (union fVars dVars) outVars /\
((domain (freeVars f)) DIFF (domain dVars)) SUBSET (domain fVars) /\
bstep (toREvalCmd f) E1 (toRTMap (toRExpMap Gamma)) vR REAL /\
validErrorboundCmd f Gamma A dVars /\
validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) /\
FloverMapTree_find (getRetExp f) A = SOME ((elo,ehi),err) ==>
?vF m.
bstep f E2 (toRExpMap Gamma) vF m
Proof
Induct_on `f` \\ rpt strip_tac
\\ Flover_compute ``validErrorboundCmd``
\\ rveq \\ fs[Once toREvalCmd_def]
......@@ -2618,7 +2620,7 @@ val validErrorboundCmd_gives_eval = store_thm (
\\ fs[Once toREvalCmd_def])
\\ qexistsl_tac [`vF_res`, `m_res`]
\\ fs[bstep_cases]
\\ qexists_tac `vF` \\ rveq \\ fs[])
\\ qexists_tac `vF` \\ rveq \\ fs[toRExpMap_def])
>- (fs[getRetExp_def]
\\ inversion `ssa _ _ _` ssa_cases
\\ inversion `bstep _ _ _ _ _` bstep_cases
......@@ -2628,21 +2630,23 @@ val validErrorboundCmd_gives_eval = store_thm (
by (irule (REWRITE_RULE [eval_Fin_def] validErrorbound_sound)
\\ fs[validTypesCmd_def, validRangesCmd_def, freeVars_def]
\\ rpt (find_exists_tac \\ fs[]))
\\ qexistsl_tac [`vF`, `m`] \\ fs[]));
\\ qexistsl_tac [`vF`, `m`] \\ fs[])
QED
val validErrorboundCmd_sound = store_thm ("validErrorboundCmd_sound",
``!(f:real cmd) (A:analysisResult) (E1 E2:env)
(outVars fVars dVars:num_set) (vR vF elo ehi err:real) (m:mType) Gamma.
validTypesCmd f Gamma /\
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 /\
ssa f (union fVars dVars) outVars /\
((domain (freeVars f)) DIFF (domain dVars)) SUBSET (domain fVars) /\
bstep (toREvalCmd f) E1 (toRTMap (toRExpMap Gamma)) vR REAL /\
bstep f E2 (toRExpMap Gamma) vF m /\
validErrorboundCmd f Gamma A dVars /\
validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) /\
FloverMapTree_find (getRetExp f) A = SOME ((elo,ehi),err) ==>
abs (vR - vF) <= err``,
Theorem validErrorboundCmd_sound:
!(f:real cmd) (A:analysisResult) (E1 E2:env)
(outVars fVars dVars:num_set) (vR vF elo ehi err:real) (m:mType) Gamma.
validTypesCmd f Gamma /\
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 /\
ssa f (union fVars dVars) outVars /\
((domain (freeVars f)) DIFF (domain dVars)) SUBSET (domain fVars) /\
bstep (toREvalCmd f) E1 (toRTMap (toRExpMap Gamma)) vR REAL /\
bstep f E2 (toRExpMap Gamma) vF m /\
validErrorboundCmd f Gamma A dVars /\
validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) /\
FloverMapTree_find (getRetExp f) A = SOME ((elo,ehi),err) ==>
abs (vR - vF) <= err
Proof
Induct_on `f` \\ rpt strip_tac
\\ Flover_compute ``validErrorboundCmd``
\\ rveq \\ fs[Once toREvalCmd_def]
......@@ -2668,7 +2672,6 @@ val validErrorboundCmd_sound = store_thm ("validErrorboundCmd_sound",
>- (fs[Once toREvalCmd_def])
>- (irule approxEnvUpdBound \\ rpt conj_tac
\\ fs[]
>- (fs[Once validTypesCmd_def] \\ fs[toRExpMap_def])
>- (Cases_on `lookup n (union fVars dVars)` \\ fs [domain_lookup])
\\ qspecl_then
[`e`, `E1`, `E2`, `A`, `vr`, `err_e`, `FST (iv_e)`,
......@@ -2688,6 +2691,7 @@ val validErrorboundCmd_sound = store_thm ("validErrorboundCmd_sound",
destruct validErrorbound_sound
\\ fs[freeVars_def, getRetExp_def, Once validTypesCmd_def, Once validRangesCmd_def]
\\ first_x_assum irule \\ fs[]
\\ find_exists_tac \\ fs[]));
\\ find_exists_tac \\ fs[])
QED
val _ = export_theory();
......@@ -57,7 +57,7 @@ val _ = Datatype `
Errors are added on the exprression evaluation level later
**)
val evalFma_def = Define `
evalFma v1 v2 v3 = evalBinop Plus v1 (evalBinop Mult v2 v3)`;
evalFma v1 v2 v3 = evalBinop Plus (evalBinop Mult v1 v2) v3`;
val toREval_def = Define `
(toREval (Var n) = Var n) /\
......
......@@ -167,22 +167,22 @@ val FPRangeValidator_sound = store_thm (
\\ fs[] \\ rveq \\ fs[])
\\ solve_tac);
val FPRangeValidatorCmd_sound = store_thm (
"FPRangeValidatorCmd_sound",
``!f E1 E2 Gamma v vR m A fVars dVars outVars.
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2
ssa f (union fVars dVars) outVars /\
bstep (toREvalCmd f) E1 (toRTMap (toRExpMap Gamma)) vR m /\
bstep f E2 (toRExpMap Gamma) v m
validTypesCmd f Gamma /\
validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) /\
validErrorboundCmd f Gamma A dVars
FPRangeValidatorCmd f A Gamma dVars
domain (freeVars f) DIFF domain dVars domain fVars
(!(v:num). v IN domain dVars ==>
(?vF m. E2 v = SOME vF /\ FloverMapTree_find (Var v) Gamma = SOME m
/\ validFloatValue vF m)) ==>
validFloatValue v m``,
Theorem FPRangeValidatorCmd_sound:
!f E1 E2 Gamma v vR m A fVars dVars outVars.
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2
ssa f (union fVars dVars) outVars /\
bstep (toREvalCmd f) E1 (toRTMap (toRExpMap Gamma)) vR m /\
bstep f E2 (toRExpMap Gamma) v m
validTypesCmd f Gamma /\
validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) /\
validErrorboundCmd f Gamma A dVars
FPRangeValidatorCmd f A Gamma dVars
domain (freeVars f) DIFF domain dVars domain fVars
(!(v:num). v IN domain dVars ==>
(?vF m. E2 v = SOME vF /\ FloverMapTree_find (Var v) Gamma = SOME m
/\ validFloatValue vF m)) ==>
validFloatValue v m
Proof
Induct
\\ simp[Once toREvalCmd_def, Once FPRangeValidatorCmd_def,
Once freeVars_def]
......@@ -224,8 +224,6 @@ val FPRangeValidatorCmd_sound = store_thm (
impl_subgoal_tac)
>- (fs[] \\ rpt conj_tac
>- (irule approxEnvUpdBound \\ fs[lookup_NONE_domain]
\\ conj_tac
>- (fs[Once validTypesCmd_def, toRExpMap_def])
\\ first_x_assum (qspecl_then [`vF`, `m`] irule)
\\ qexists_tac `m` \\ fs[])
>- (irule ssa_equal_set
......@@ -285,6 +283,7 @@ val FPRangeValidatorCmd_sound = store_thm (
\\ rpt (inversion `bstep (Ret _) _ _ _ _` bstep_cases)
\\ drule FPRangeValidator_sound
\\ rpt (disch_then drule)
\\ fs[Once validTypesCmd_def, Once validRangesCmd_def]);
\\ fs[Once validTypesCmd_def, Once validRangesCmd_def]
QED
val _ = export_theory();
......@@ -41,8 +41,9 @@ val eval_expr_float_def = Define `
| Div => SOME (fp64_div dmode v1 v2))
| _, _ => NONE)) /\
(eval_expr_float (Fma e1 e2 e3) E =
(case (eval_expr_float e1 E), (eval_expr_float e2 E), (eval_expr_float e2 E) of
| _, _, _ => NONE)) /\
(case (eval_expr_float e1 E), (eval_expr_float e2 E), (eval_expr_float e3 E) of
| SOME v1, SOME v2, SOME v3 => SOME (fp64_mul_add roundTiesToEven v1 v2 v3)
| _, _, _ => NONE)) /\
(eval_expr_float (Downcast m e) E = NONE)`;
val bstep_float_def = Define `
......@@ -93,7 +94,7 @@ val eval_expr_valid_def = Define `
in
optionLift e3_res
(\ v3. let v3_real = float_to_real (fp64_to_float v3) in
F)
normal_or_zero (evalFma v1_real v2_real v3_real))
T)
T)
T)) /\
......@@ -530,29 +531,30 @@ val typing_cmd_64bit = store_thm (
\\ rpt strip_tac \\ fs[]
\\ res_tac);
val eval_expr_gives_IEEE = store_thm ("eval_expr_gives_IEEE",
``!(e:word64 expr) E1 E2 E2_real Gamma vR A fVars dVars.
(!x. (toREnv E2) x = E2_real x) /\
validTypes (toRExp e) Gamma /\
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2_real /\
validRanges (toRExp e) A E1 (toRTMap (toRExpMap Gamma)) /\
validErrorbound (toRExp e) Gamma A dVars /\
FPRangeValidator (toRExp e) A Gamma dVars /\
eval_expr (toREnv E2) (toRExpMap Gamma) (toRExp e) vR M64 /\
domain (usedVars (toRExp e)) DIFF domain dVars domain fVars
is64BitEval (toRExp e) /\
is64BitEnv Gamma /\
noDowncast (toRExp e) /\
eval_expr_valid e E2 /\
(v.
v domain dVars
vF m.
(E2_real v = SOME vF FloverMapTree_find (Var v) Gamma = SOME m
validFloatValue vF m)) ==>
?v.
eval_expr_float e E2 = SOME v /\
eval_expr (toREnv E2) (toRExpMap Gamma) (toRExp e)
(float_to_real (fp64_to_float v)) M64``,
Theorem eval_expr_gives_IEEE:
!(e:word64 expr) E1 E2 E2_real Gamma vR A fVars dVars.
(!x. (toREnv E2) x = E2_real x) /\
validTypes (toRExp e) Gamma /\
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2_real /\
validRanges (toRExp e) A E1 (toRTMap (toRExpMap Gamma)) /\
validErrorbound (toRExp e) Gamma A dVars /\
FPRangeValidator (toRExp e) A Gamma dVars /\
eval_expr (toREnv E2) (toRExpMap Gamma) (toRExp e) vR M64 /\
domain (usedVars (toRExp e)) DIFF domain dVars domain fVars
is64BitEval (toRExp e) /\
is64BitEnv Gamma /\
noDowncast (toRExp e) /\
eval_expr_valid e E2 /\
(v.
v domain dVars
vF m.
(E2_real v = SOME vF FloverMapTree_find (Var v) Gamma = SOME m
validFloatValue vF m)) ==>
?v.
eval_expr_float e E2 = SOME v /\
eval_expr (toREnv E2) (toRExpMap Gamma) (toRExp e)
(float_to_real (fp64_to_float v)) M64
Proof
Induct_on `e` \\ rewrite_tac[toRExp_def] \\ rpt strip_tac
\\ inversion `eval_expr _ _ _ _ _` eval_expr_cases
\\ once_rewrite_tac [eval_expr_float_def]
......@@ -1059,34 +1061,168 @@ val eval_expr_gives_IEEE = store_thm ("eval_expr_gives_IEEE",
\\ rw_asm_star `FloverMapTree_find (Fma _ _ _) Gamma = _`)
\\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
\\ fs[domain_union, DIFF_DEF, SUBSET_DEF])
\\ fs[optionLift_def]));
\\ rename1 eval_expr_float e1 E2 = SOME vF1
\\ rename1 eval_expr_float e2 E2 = SOME vF2
\\ rename1 eval_expr_float e3 E2 = SOME vF3
\\ `validFloatValue
(evalFma (float_to_real (fp64_to_float vF1))
(float_to_real (fp64_to_float vF2))
(float_to_real (fp64_to_float vF3))) M64`
by (drule FPRangeValidator_sound
\\ disch_then
(qspecl_then
[`(Fma (toRExp e1) (toRExp e2) (toRExp e3))`,
`evalFma (float_to_real (fp64_to_float vF1))
(float_to_real (fp64_to_float vF2))
(float_to_real (fp64_to_float vF3))`,
`M64`] irule)
\\ fs[]
\\ qexistsl_tac [`e1`, `e2`, e3] \\ fs[]
\\ rpt conj_tac
>- (simp[Once validTypes_def] \\ first_x_assum MATCH_ACCEPT_TAC)
>- (simp[Once validRanges_def] \\ find_exists_tac \\ fs[]
\\ fs[] \\ rveq \\ fs[])
\\ irule eval_eq_env
\\ find_exists_tac \\ fs[eval_expr_cases]
\\ qexistsl_tac [`M64`, `M64`, M64, `float_to_real (fp64_to_float vF1)`,
`float_to_real (fp64_to_float vF2)`,
`float_to_real (fp64_to_float vF3)`, `0:real`]
\\ fs[perturb_def, evalFma_def, mTypeToR_pos])
\\ `validFloatValue (float_to_real (fp64_to_float vF1)) M64`
by (drule FPRangeValidator_sound
\\ disch_then
(qspecl_then
[`toRExp e1`, `float_to_real (fp64_to_float vF1)`,
`M64`] irule)
\\ fs[]
\\ qexistsl_tac [`e1`] \\ fs[]
\\ rpt conj_tac
>- (rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
\\ fs[domain_union, DIFF_DEF, SUBSET_DEF, Once usedVars_def])
>- (rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
\\ fs[] \\ rveq
\\ rw_asm_star `FloverMapTree_find (Fma _ _ _) A = _`
\\ rw_asm_star `FloverMapTree_find (Fma _ _ _) Gamma = _`)
>- (Flover_compute ``validErrorbound``)
\\ irule eval_eq_env
\\ find_exists_tac \\ fs[])
\\ `validFloatValue (float_to_real (fp64_to_float vF2)) M64`
by (drule FPRangeValidator_sound
\\ disch_then
(qspecl_then
[`toRExp e2`, `float_to_real (fp64_to_float vF2)`,
`M64`] irule)
\\ fs[]
\\ qexists_tac `e2` \\ fs[]
\\ rpt conj_tac
>- (rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
\\ fs[domain_union, DIFF_DEF, SUBSET_DEF])
>- (rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
\\ fs[] \\ rveq
\\ rw_asm_star `FloverMapTree_find (Fma _ _ _) A = _`
\\ rw_asm_star `FloverMapTree_find (Fma _ _ _) Gamma = _`)
>- (Flover_compute ``validErrorbound``)
\\ irule eval_eq_env
\\ find_exists_tac \\ fs[])
\\ `validFloatValue (float_to_real (fp64_to_float vF3)) M64`
by (drule FPRangeValidator_sound
\\ disch_then
(qspecl_then
[`toRExp e3`, `float_to_real (fp64_to_float vF3)`,
`M64`] irule)
\\ fs[]
\\ qexists_tac `e3` \\ fs[]
\\ rpt conj_tac
>- (rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
\\ fs[domain_union, DIFF_DEF, SUBSET_DEF])
>- (rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
\\ fs[] \\ rveq
\\ rw_asm_star `FloverMapTree_find (Fma _ _ _) A = _`
\\ rw_asm_star `FloverMapTree_find (Fma _ _ _) Gamma = _`)
>- (Flover_compute ``validErrorbound``)
\\ irule eval_eq_env
\\ find_exists_tac \\ fs[])
\\ fs[optionLift_def, normal_or_zero_def]
\\ simp[Once eval_expr_cases, PULL_EXISTS]
\\ rewrite_tac [CONJ_ASSOC]
\\ ntac 3 (once_rewrite_tac [CONJ_COMM] \\ asm_exists_tac \\ fs[])
\\ fs[evalFma_def, evalBinop_def, fp64_mul_add_def, fp64_to_float_float_to_fp64]
>- (
`normal (evalFma (float_to_real (fp64_to_float vF1))
(float_to_real (fp64_to_float vF2))
(float_to_real (fp64_to_float vF3))) M64`
by (
rw_thm_asm `validFloatValue (_ + _) _` validFloatValue_def
\\ fs[normal_def, denormal_def, evalFma_def, evalBinop_def]
>- (
`abs (float_to_real (fp64_to_float vF1) *
float_to_real (fp64_to_float vF2) + float_to_real (fp64_to_float vF3)) <
abs (float_to_real (fp64_to_float vF1) *
float_to_real (fp64_to_float vF2) + float_to_real (fp64_to_float vF3))`
suffices_by (fs[])
\\ irule REAL_LTE_TRANS
\\ asm_exists_tac \\ fs[])
\\ qpat_x_assum `_ + _ = 0` (fn thm => fs[thm])
\\ fs[maxValue_def, maxExponent_def])
\\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
`(fp64_to_float vF2):(52,11) float`,
`(fp64_to_float vF3):(52,11) float`]
impl_subgoal_tac
float_mul_add_relative
>- (rpt conj_tac
\\ fs[validFloatValue_def,
normalTranslatedValue_implies_finiteness,
denormalTranslatedValue_implies_finiteness,
normalValue_implies_normalization,
GSYM float_is_zero_to_real, float_is_finite, evalFma_def, evalBinop_def])