Commit 1b06f787 authored by Heiko Becker's avatar Heiko Becker
Browse files

Update FloVer to work with latest HOL4 develop

parent eadccab4
......@@ -125,7 +125,7 @@ Proof
QED
Theorem approxEnv_dVar_bounded:
!E1 Gamma A fVars dVars E2 x v v2 m iv e.
!E1 (Gamma:real expr -> mType option) (A:analysisResult) fVars dVars E2 x v v2 m iv e.
approxEnv E1 Gamma A fVars dVars E2 /\
E1 x = SOME v /\
E2 x = SOME v2 /\
......@@ -151,8 +151,8 @@ Theorem approxEnv_refl:
approxEnv E1 Gamma A fVars dVars E1
Proof
rw[approxEnv_def] \\ res_tac \\ fsrw_tac [SATISFY_ss] []
\\ Cases_on m \\ fs[computeError_def, mTypeToR_pos]
\\ irule REAL_LE_MUL \\ fs[mTypeToR_pos]
\\ Cases_on m \\ fs[mTypeToR_pos]
\\ irule computeError_pos
QED
val _ = export_theory ();;
......@@ -14,7 +14,7 @@ val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
val _ = temp_overload_on("abs",``real$abs``);
val triangle_tac =
irule triangle_trans \\ fs[REAL_ABS_TRIANGLE];
irule triangle_trans \\ rpt conj_tac \\ TRY (fs[REAL_ABS_TRIANGLE] \\ NO_TAC);
Theorem const_abs_err_bounded:
!(n:real) (nR:real) (nF:real) (E1 E2:env) (m:mType) Gamma.
......@@ -109,14 +109,14 @@ val float_sub_tac =
\\ `e1R + (-e2R + -((1 + deltaF) * (e1F + -e2F))) =
(e1R + - e1F) + ((- e2R + e2F) + - (e1F + - e2F) * deltaF)`
by REAL_ASM_ARITH_TAC
\\ simp []
\\ pop_assum (once_rewrite_tac o single)
\\ triangle_tac
\\ irule REAL_LE_ADD2 \\ conj_tac
>- fs[GSYM real_sub]
\\ triangle_tac
\\ irule REAL_LE_ADD2 \\ conj_tac
>- REAL_ASM_ARITH_TAC
\\ once_rewrite_tac [REAL_ABS_MUL, ABS_NEG]
\\ rewrite_tac [REAL_ABS_MUL, ABS_NEG]
\\ metis_tac [REAL_ABS_POS, REAL_LE_LMUL_IMP, REAL_MUL_COMM];
Theorem subtract_abs_err_bounded:
......@@ -181,12 +181,11 @@ val float_mul_tac =
`e1R * e2R + -(e1F * e2F * (1 + deltaF)) =
(e1R * e2R + - (e1F * e2F)) + - (e1F * e2F * deltaF)`
by REAL_ASM_ARITH_TAC
\\ simp[]
\\ pop_assum (once_rewrite_tac o single)
\\ triangle_tac
\\ rewrite_tac[GSYM REAL_MUL_ASSOC]
\\ once_rewrite_tac [REAL_ABS_MUL]
\\ rewrite_tac [ABS_NEG, REAL_ABS_MUL] \\ rename1 abs errF mTypeToR _
\\ simp[computeError_def]
\\ metis_tac [REAL_LE_LMUL_IMP, REAL_MUL_COMM, REAL_ABS_POS];
\\ metis_tac [REAL_LE_LMUL_IMP, REAL_ABS_MUL, REAL_ABS_POS];
Theorem mult_abs_err_bounded:
! (e1:real expr) (e1R:real) (e1F:real) (e2:real expr) (e2R:real) (e2F:real)
......@@ -235,15 +234,23 @@ Proof
\\ fs[ABS_NEG, computeError_def]
QED
Theorem REAL_LE_MUL_SWAP:
(a b c:real).
a * b a * c b * a a * c
Proof
rpt strip_tac \\ fs[]
QED
val float_div_tac =
`e1R / e2R + -(e1F / e2F * (1 + deltaF)) =
(e1R / e2R + - (e1F / e2F)) + - (e1F / e2F * deltaF)`
by REAL_ASM_ARITH_TAC
\\ simp[]
\\ once_rewrite_tac [GSYM real_div]
\\ pop_assum (fn thm => once_rewrite_tac [thm])
\\ triangle_tac
\\ once_rewrite_tac [REAL_ABS_MUL]
\\ simp[computeError_def]
\\ metis_tac [REAL_LE_LMUL_IMP, REAL_MUL_COMM, REAL_ABS_POS];
\\ once_rewrite_tac [ABS_NEG]
\\ simp[computeError_def, REAL_ABS_MUL]
\\ metis_tac [REAL_LE_LMUL_IMP, REAL_ABS_POS, REAL_LE_MUL_SWAP];
Theorem div_abs_err_bounded:
!(e1:real expr) (e1R:real) (e1F:real) (e2:real expr) (e2R:real) (e2F:real)
......@@ -300,8 +307,8 @@ val float_fma_tac =
\\ triangle_tac
\\ irule REAL_LE_ADD2 \\ conj_tac
\\ TRY (REAL_ASM_ARITH_TAC)
\\ once_rewrite_tac[REAL_ABS_MUL]
\\ metis_tac [REAL_LE_LMUL_IMP, REAL_MUL_COMM, REAL_ABS_POS];
\\ rewrite_tac[REAL_ABS_MUL, ABS_NEG]
\\ metis_tac [REAL_LE_LMUL_IMP, REAL_MUL_COMM, REAL_ABS_POS, REAL_LE_MUL_SWAP];
Theorem fma_abs_err_bounded:
!(e1:real expr) (e1R:real) (e1F:real) (e2:real expr) (e2R:real) (e2F:real)
......@@ -389,7 +396,7 @@ Proof
\\ Cases_on `m1` \\ fs[perturb_def, computeError_def]
\\ once_rewrite_tac [REAL_LDISTRIB]
\\ simp[real_sub, REAL_NEG_ADD, REAL_ADD_ASSOC, ABS_NEG, ABS_MUL]
\\ metis_tac [REAL_LE_LMUL_IMP, ABS_POS, REAL_MUL_COMM]
\\ metis_tac [REAL_LE_LMUL_IMP, ABS_POS, REAL_MUL_COMM, REAL_LE_MUL_SWAP]
QED
Theorem nonzerop_EQ1_I'[simp]:
......@@ -424,34 +431,35 @@ Proof
\\ `0 <= - (inv nR - inv nF) ` by REAL_ASM_ARITH_TAC
\\ `abs (- (inv nR - inv nF)) = - (inv nR - inv nF)` by fs [ABS_REFL]
\\ `abs (inv nR - inv nF) = - (inv nR - inv nF)` by metis_tac[ABS_NEG]
\\ simp[REAL_INV_1OVER, real_sub, REAL_NEG_ADD]
\\ simp[real_sub, REAL_NEG_ADD]
\\ rpt (qpat_x_assum `abs v = v'` kall_tac)
\\ `- (1 / nR) = 1 / - nR`
\\ `- (inv nR) = inv (- nR)`
by (fs [real_div] \\ irule REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
\\ simp[]
\\ qspec_then `1 / -nR + 1 / (nR - err)` match_mp_tac real_le_trans2 \\ conj_tac
\\ qspec_then `inv (-nR) + inv (nR - err)` match_mp_tac real_le_trans2 \\ conj_tac
>- (match_mp_tac REAL_LE_LADD_IMP
\\ 0 < nR - err nR - err nF by REAL_ASM_ARITH_TAC
\\ simp[GSYM REAL_INV_1OVER])
\\ simp[])
>- (`- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
\\ fs [REAL_ADD_RAT] (* Goal: (nR − err + -nR) / (-nR * (nR − err)) ≤ err * (1 / (elo + -err) pow 2) *)
\\ (nR - err + -nR) / (-nR * (nR - err)) err * (1 / (elo + -err) pow 2)
suffices_by (rewrite_tac[REAL_INV_1OVER] \\ fs[REAL_ADD_RAT])
\\ `nR - err + - nR = - err` by REAL_ASM_ARITH_TAC
\\ pop_assum (rewrite_tac o single)
\\ qspec_then `nR` (fn thm => fs [real_div, GSYM thm]) REAL_NEG_LMUL
(* Goal: -(err * inv (-(nR * (nR − err)))) ≤ err * inv ((elo + -err)pow 2) *)
\\ `nR <> 0` by REAL_ASM_ARITH_TAC
(* Goal: -(err * inv (-(nR * (nR − err)))) ≤ err * inv ((elo + -err) pow 2) *)
\\ `nR * (nR - err) <> 0` by fs[REAL_ENTIRE]
\\ fs [GSYM REAL_NEG_INV, GSYM REAL_NEG_LMUL, GSYM REAL_NEG_RMUL]
(* Goal: err * inv (nR * (nR − err)) ≤ err * inv ((elo + -err) pow 2) *)
\\ rewrite_tac [REAL_POW_INV]
\\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[]
\\ rpt (qpat_x_assum `T` kall_tac)
\\ `0 < elo + - err` by REAL_ASM_ARITH_TAC
\\ `0 < (elo + - err) * (elo + - err)` by fs[REAL_LT_MUL]
\\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
>- (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
>- (conj_tac
>- (fs[POW_2])
>- (once_rewrite_tac [POW_2] \\ irule REAL_LE_MUL2 \\ REAL_ASM_ARITH_TAC))))
\\ conj_tac
>- (fs[POW_2])
\\ once_rewrite_tac [POW_2] \\ irule REAL_LE_MUL2 \\ REAL_ASM_ARITH_TAC))
>- (fs[]
\\ `nR <= nF` by REAL_ASM_ARITH_TAC
\\ `0 < nF` by REAL_ASM_ARITH_TAC
......@@ -459,28 +467,38 @@ Proof
\\ `inv nF <= inv nR` by fs [REAL_INV_LE_ANTIMONO]
\\ `0 <= inv nR - inv nF` by REAL_ASM_ARITH_TAC \\ qpat_x_assum `inv nF <= inv nR` kall_tac
\\ `abs (inv nR - inv nF) = inv nR - inv nF` by fs[ABS_REFL] \\ qpat_x_assum `0 <= inv a - b` kall_tac
\\ simp [REAL_INV_1OVER, real_sub, REAL_NEG_ADD]
\\ simp [real_sub, REAL_NEG_ADD]
\\ rpt (qpat_x_assum `abs x = y` kall_tac)
\\ qspec_then `1 / nR + - (1 / (nR + err))` match_mp_tac real_le_trans2 \\ conj_tac
\\ qspec_then `inv nR + - (inv (nR + err))` match_mp_tac real_le_trans2 \\ conj_tac
>- (match_mp_tac REAL_LE_LADD_IMP
\\ `0 < nR + err /\ nF <= nR + err` by REAL_ASM_ARITH_TAC
\\ fs[GSYM REAL_INV_1OVER, REAL_INV_LE_ANTIMONO])
>- (` - nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
\\ `- (1 / (nR + err)) = 1 / - (nR + err)` by (fs [real_div] \\ match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
>- (`- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
\\ `- (inv (nR + err)) = inv (- (nR + err))`
by (fs [real_div] \\ match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
\\ pop_assum (rewrite_tac o single)
\\ `- (nR + err) <> 0` by REAL_ASM_ARITH_TAC
\\ `nR <> 0` by REAL_ASM_ARITH_TAC
\\ fs [REAL_ADD_RAT] (* Goal: (-(nR + err) + nR) / (nR * -(nR + err)) ≤ err * (1 / (elo + -err) pow 2) *)
\\ rewrite_tac[REAL_INV_1OVER]
\\ 1 / - (nR + err) = -1 / (nR + err) by (fs[neg_rat])
\\ pop_assum (rewrite_tac o single)
\\ 1 / nR + -1 / (nR + err) = (-(nR + err) + nR) / (nR * -(nR + err))
by (fs[REAL_ADD_RAT, real_div, REAL_MUL_LNEG, REAL_MUL_RNEG]
\\ rewrite_tac[GSYM REAL_MUL_RNEG, REAL_NEG_ADD, REAL_NEG_NEG])
\\ pop_assum (rewrite_tac o single)
(* Goal: (-(nR + err) + nR) / (nR * -(nR + err)) ≤ err * (1 / (elo + -err) pow 2) *)
\\ `- (nR + err) + nR = - err` by REAL_ASM_ARITH_TAC
\\ qspec_then `nR` (fn thm => fs [real_div, GSYM thm]) REAL_NEG_LMUL
\\ simp [REAL_NEG_RMUL, REAL_NEG_INV]
(* Goal: err * inv (nR * (nR + err)) ≤ err * inv ((elo + -err) pow 2) *)
\\ pop_assum (rewrite_tac o single)
\\ rewrite_tac[real_div, GSYM REAL_NEG_LMUL, REAL_NEG_RMUL]
\\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[]
\\ fs [REAL_NEG_INV, REAL_NEG_RMUL, REAL_NEG_NEG]
(* Goal: inv (nR * (nR + err)) ≤ inv ((elo + -err) pow 2)) *)
\\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
>- (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
>- (conj_tac \\ once_rewrite_tac [POW_2]
>- (match_mp_tac REAL_LT_MUL
\\ REAL_ASM_ARITH_TAC)
>- (match_mp_tac REAL_LE_MUL2 \\ REAL_ASM_ARITH_TAC))))
>- (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
\\ conj_tac \\ once_rewrite_tac [POW_2]
>- (match_mp_tac REAL_LT_MUL
\\ REAL_ASM_ARITH_TAC)
\\ match_mp_tac REAL_LE_MUL2 \\ REAL_ASM_ARITH_TAC))
QED
Theorem err_prop_inversion_neg:
......@@ -508,14 +526,18 @@ Proof
\\ `0 <= - (inv (- nF) - inv (-nR)) ` by REAL_ASM_ARITH_TAC
\\ `abs (- (inv (- nF) - inv (- nR))) = - (inv (- nF) - inv (- nR))` by fs [ABS_REFL]
\\ `abs (inv (- nF) - inv (- nR)) = - (inv (- nF) - inv (- nR))` by metis_tac[ABS_NEG]
\\ `inv (- nF) - inv (- nR) = inv nR - inv nF` by (fs[GSYM REAL_NEG_INV, real_sub] \\ REAL_ASM_ARITH_TAC)
\\ `inv (- nF) - inv (- nR) = inv nR - inv nF`
by (fs[GSYM REAL_NEG_INV, real_sub] \\ REAL_ASM_ARITH_TAC)
\\ `abs (inv nR - inv nF) = - (inv nR - inv nF)` by fs[]
\\ simp[REAL_INV_1OVER, real_sub, REAL_NEG_ADD]
\\ simp[real_sub, REAL_NEG_ADD]
\\ rpt (qpat_x_assum `abs v = v'` kall_tac)
\\ `- (1 / nR) = 1 / - nR` by (fs [real_div] \\ match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
\\ `- (1 / nR) = 1 / - nR`
by (fs [real_div] \\ match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
\\ simp[]
\\ qspec_then `1 / -nR + 1 / (nR - err)` match_mp_tac real_le_trans2 \\ conj_tac
>- (match_mp_tac REAL_LE_LADD_IMP
>- (once_rewrite_tac [REAL_INV_1OVER]
\\ pop_assum (rewrite_tac o single)
\\ match_mp_tac REAL_LE_LADD_IMP
\\ simp[GSYM REAL_INV_1OVER]
\\ `nR - err <= nF` by REAL_ASM_ARITH_TAC
\\ `- nF <= - (nR - err)` by REAL_ASM_ARITH_TAC
......@@ -528,9 +550,14 @@ Proof
\\ qpat_x_assum `-(inv nRerr) = v` (fn thm => once_rewrite_tac [thm])
\\ qpat_x_assum `-(inv nF) = v` (fn thm => once_rewrite_tac [thm])
\\ simp[])
>- (`- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC \\ fs [REAL_ADD_RAT]
>- (`- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
\\ 1 / -nR + 1 / (nR - err) = (1 * (nR - err) + -nR * 1) / (-nR * (nR - err))
by (fs [REAL_ADD_RAT])
\\ pop_assum (rewrite_tac o single)
\\ rewrite_tac [REAL_MUL_LID, REAL_MUL_RID]
\\ `nR - err + - nR = - err` by REAL_ASM_ARITH_TAC
\\ qspec_then `nR` (fn thm => fs [real_div, GSYM thm]) REAL_NEG_LMUL
\\ pop_assum (rewrite_tac o single)
\\ rewrite_tac [GSYM REAL_NEG_LMUL, real_div]
\\ `nR <> 0` by REAL_ASM_ARITH_TAC
\\ `nR * (nR - err) <> 0` by fs[REAL_ENTIRE]
\\ fs [GSYM REAL_NEG_INV, GSYM REAL_NEG_LMUL, GSYM REAL_NEG_RMUL]
......@@ -563,23 +590,28 @@ Proof
\\ `inv (- nR) - inv (- nF) = inv nF - inv nR` by (fs[GSYM REAL_NEG_INV, real_sub] \\ REAL_ASM_ARITH_TAC)
\\ `abs (inv nF - inv nR) = - (inv (- nR) - inv (- nF))` by fs[]
\\ `abs (inv nR - inv nF) = - (inv (- nR) - inv (- nF))` by fs[ABS_SUB]
\\ simp[REAL_INV_1OVER, real_sub, REAL_NEG_ADD]
\\ simp[real_sub, REAL_NEG_ADD]
\\ rpt (qpat_x_assum `abs v = v'` kall_tac)
\\ `- (1 / nF) = 1 / - nF` by (fs [real_div] \\ match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
\\ simp[]
\\ qspec_then `1 / -(nR + err) + 1 / nR` match_mp_tac real_le_trans2 \\ conj_tac
>- (once_rewrite_tac [REAL_ADD_COMM] \\ match_mp_tac REAL_LE_LADD_IMP
>- (once_rewrite_tac [REAL_ADD_COMM] \\ rewrite_tac [REAL_INV_1OVER]
\\ pop_assum (rewrite_tac o single)
\\ match_mp_tac REAL_LE_LADD_IMP
\\ `0 < - (nR + err) /\ nF <= nR + err` by REAL_ASM_ARITH_TAC
\\ simp [GSYM REAL_INV_1OVER, REAL_LE_NEG, REAL_INV_LE_ANTIMONO])
\\ simp [REAL_LE_NEG, REAL_INV_LE_ANTIMONO])
>- (`- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
\\ `- (nR + err) <> 0` by REAL_ASM_ARITH_TAC
\\ fs [REAL_ADD_RAT]
\\ 1 / - (nR + err) + 1 / nR = (1 * nR + - (nR + err) * 1) / (- (nR + err) * nR)
by (fs[REAL_ADD_RAT])
\\ pop_assum (rewrite_tac o single)
\\ `nR + - (nR + err) = - err` by REAL_ASM_ARITH_TAC
\\ fs [real_div, GSYM REAL_NEG_RMUL]
\\ simp [GSYM REAL_NEG_RMUL, GSYM REAL_NEG_LMUL]
\\ rewrite_tac [REAL_MUL_RID, REAL_MUL_LID, real_div, GSYM REAL_NEG_RMUL, GSYM REAL_NEG_LMUL]
\\ pop_assum (rewrite_tac o single)
\\ `inv (- ((nR + err) * nR)) = - (inv ((nR + err) * nR))`
by (match_mp_tac (GSYM REAL_NEG_INV) \\ fs[] \\ REAL_ASM_ARITH_TAC)
\\ simp[REAL_NEG_RMUL]
\\ pop_assum (rewrite_tac o single)
\\ simp[GSYM REAL_NEG_RMUL, GSYM REAL_NEG_LMUL, REAL_NEG_NEG]
\\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[]
\\ `0 < - (ehi + err)` by REAL_ASM_ARITH_TAC
\\ `0 < - (ehi + err) * -(ehi + err)` by (match_mp_tac REAL_LT_MUL \\ fs[])
......
......@@ -128,20 +128,22 @@ val solve_tac =
by (fs[widenInterval_def, IVlo_def, IVhi_def] \\ RealArith.REAL_ASM_ARITH_TAC)
\\ TRY (every_case_tac \\ RealArith.REAL_ASM_ARITH_TAC);
val FPRangeValidator_sound = store_thm (
"FPRangeValidator_sound",
``!e E1 E2 Gamma v m A fVars (dVars:num_set).
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 /\
eval_expr E2 (toRExpMap Gamma) e v m /\
validTypes e Gamma /\
validRanges e A E1 (toRTMap (toRExpMap Gamma)) /\
validErrorbound e Gamma A dVars /\
FPRangeValidator e A Gamma dVars /\
domain (usedVars e) DIFF (domain dVars) SUBSET (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 FPRangeValidator_sound:
e E1 E2 Gamma v m A fVars (dVars:num_set).
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2
eval_expr E2 (toRExpMap Gamma) e v m
validTypes e Gamma
validRanges e A E1 (toRTMap (toRExpMap Gamma))
validErrorbound e Gamma A dVars
FPRangeValidator e A Gamma dVars
domain (usedVars e) DIFF (domain dVars) SUBSET (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
rpt strip_tac
\\ IMP_RES_TAC validTypes_single
\\ `m = mG`
......@@ -165,10 +167,11 @@ val FPRangeValidator_sound = store_thm (
\\ fs[] \\ rveq \\ fs[]
\\ rpt (inversion `eval_expr E2 _ _ _ _` eval_expr_cases)
\\ fs[] \\ rveq \\ fs[])
\\ solve_tac);
\\ solve_tac
QED
Theorem FPRangeValidatorCmd_sound:
!f E1 E2 Gamma v vR m A fVars dVars outVars.
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 /\
......@@ -187,99 +190,107 @@ Proof
\\ simp[Once toREvalCmd_def, Once FPRangeValidatorCmd_def,
Once freeVars_def]
\\ rpt strip_tac
>- (Flover_compute ``validErrorboundCmd``
\\ rveq \\ fs[]
\\ rpt (inversion `bstep (Let _ _ _ _) _ _ _ _` bstep_cases)
\\ rveq
\\ rename1 `bstep (toREvalCmd f) (updEnv n vR_e E1) _ _ mR`
\\ rename1 `bstep f (updEnv n vF E2) _ _ mF`
\\ fs[Once validTypesCmd_def]
\\ IMP_RES_TAC validTypes_single
\\ `m = mG`
by (first_x_assum irule
\\ qexistsl_tac [`E2`, `Gamma`, `vF`] \\ fs[])
\\ rveq
\\ inversion `ssa _ _ _` ssa_cases
\\ drule validErrorbound_sound
\\ disch_then drule
\\ disch_then
(qspecl_then [`vR_e`, `err_e`, `FST iv_e`, `SND iv_e`]
impl_subgoal_tac)
>- (fs[Once validRangesCmd_def]
\\ fs[DIFF_DEF, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule
\\ fs[domain_union]
\\ CCONTR_TAC \\ fs[] \\ rveq
\\ first_x_assum (qspec_then `n` assume_tac)
\\ `n IN domain fVars \/ n IN domain dVars`
suffices_by (fs[])
\\ fs[])
\\ fs[Once validRangesCmd_def]
\\ IMP_RES_TAC validRanges_single
\\ IMP_RES_TAC meps_0_deterministic \\ rveq \\ fs[]
\\ rename1 `vR_e <= SND _`
\\ first_x_assum
(qspecl_then [`updEnv n vR_e E1`, `updEnv n vF E2`,
`Gamma`, `v`, `vR`, `mF`, `A`,
`fVars`, `insert n () dVars`, `outVars`]
impl_subgoal_tac)
>- (fs[] \\ rpt conj_tac
>- (irule approxEnvUpdBound \\ fs[lookup_NONE_domain]
\\ first_x_assum (qspecl_then [`vF`, `m`] irule)
\\ qexists_tac `m` \\ fs[])
>- (irule ssa_equal_set
\\ qexists_tac `insert n () (union fVars dVars)`
\\ conj_tac \\ TRY (fs[] \\ FAIL_TAC "")
\\ rewrite_tac [domain_union, domain_insert]
\\ rewrite_tac [UNION_DEF, INSERT_DEF]
\\ fs[EXTENSION]
\\ rpt strip_tac
\\ metis_tac[])
>- (fs[Once validTypesCmd_def])
>- (IMP_RES_TAC validTypesCmd_single
\\ find_exists_tac \\ fs[]
\\ first_x_assum MATCH_ACCEPT_TAC)
>- (fs[Once validRangesCmd_def])
>- (`validRangesCmd f A (updEnv n vR_e E1) (toRTMap (toRExpMap Gamma))`
by (first_x_assum irule \\ fs[])
\\ IMP_RES_TAC validRangesCmd_single
\\ rpt (find_exists_tac \\ fs[]))
>- (fs[DIFF_DEF, domain_insert, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ simp[Once freeVars_def]
\\ once_rewrite_tac [domain_union]
\\ fs[]
\\ rw_thm_asm `x IN domain (freeVars f)` freeVars_def
\\ fs[])
\\ rpt strip_tac
\\ fs[updEnv_def] \\ rveq \\ fs[]
>- (qpat_x_assum `eval_expr E2 _ e nF _` kall_tac
\\ drule FPRangeValidator_sound
\\ rpt (disch_then drule)
\\ disch_then irule \\ fs[]
\\ fs[DIFF_DEF, domain_insert, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ simp[Once freeVars_def]
\\ once_rewrite_tac [domain_union]
\\ fs[]
\\ CCONTR_TAC \\ fs[] \\ rveq
\\ first_x_assum (qspec_then `n` assume_tac)
\\ res_tac)
\\ TOP_CASE_TAC \\ fs[]
\\ qpat_x_assum `eval_expr E2 _ e nF _` kall_tac
\\ drule FPRangeValidator_sound
\\ rpt (disch_then drule)
\\ disch_then irule \\ fs[]
\\ fs[DIFF_DEF, domain_insert, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ simp[Once freeVars_def]
\\ once_rewrite_tac [domain_union]
\\ fs[]
\\ CCONTR_TAC \\ fs[] \\ rveq
\\ first_x_assum (qspec_then `n` assume_tac)
\\ res_tac)
\\ fs[])
\\ Flover_compute ``validErrorboundCmd``
\\ rveq \\ fs[]
>- (
qpat_x_assum validErrorboundCmd _ _ _ _
(mp_tac o SIMP_RULE std_ss [Once validErrorboundCmd_def]) \\ fs[]
\\ ntac 4 (TOP_CASE_TAC \\ fs[]) \\ strip_tac \\ rveq
\\ rpt (inversion `bstep (Let _ _ _ _) _ _ _ _` bstep_cases) \\ rveq
\\ rename1 `bstep (toREvalCmd f) (updEnv n vR_e E1) _ _ mR`
\\ rename1 `bstep f (updEnv n vF E2) _ _ mF`
\\ rename1 FloverMapTree_find e A = SOME (iv_e, err_e)
\\ fs[Once validTypesCmd_def]
\\ imp_res_tac validTypes_single
\\ `m = mG`
by (first_x_assum irule
\\ qexistsl_tac [`E2`, `Gamma`, `vF`] \\ fs[])
\\ rveq
\\ inversion `ssa _ _ _` ssa_cases
\\ drule validErrorbound_sound
\\ disch_then drule
\\ disch_then
(qspecl_then [`vR_e`, `err_e`, `FST iv_e`, `SND iv_e`]
impl_subgoal_tac)
>- (
fs[Once validRangesCmd_def]
\\ fs[DIFF_DEF, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule
\\ fs[domain_union]
\\ CCONTR_TAC \\ fs[] \\ rveq
\\ first_x_assum (qspec_then `n` assume_tac)
\\ `n IN domain fVars \/ n IN domain dVars`
suffices_by (fs[])
\\ fs[])
\\ fs[Once validRangesCmd_def]
\\ imp_res_tac validRanges_single
\\ imp_res_tac meps_0_deterministic \\ rveq \\ fs[]
\\ rename1 `vR_e <= SND _`
\\ first_x_assum
(qspecl_then [`updEnv n vR_e E1`, `updEnv n vF E2`, `Gamma`, `v`, `vR`,
`mF`, `A`, `fVars`, `insert n () dVars`, `outVars`]
impl_subgoal_tac)
>- (
fs[] \\ rpt conj_tac
>- (
irule approxEnvUpdBound \\ fs[lookup_NONE_domain]
\\ first_x_assum (qspecl_then [`vF`, `m`] irule)
\\ qexists_tac `m` \\ fs[])
>- (
irule ssa_equal_set
\\ qexists_tac `insert n () (union fVars dVars)`
\\ conj_tac \\ TRY (fs[] \\ FAIL_TAC "")
\\ rewrite_tac [domain_union, domain_insert]
\\ rewrite_tac [UNION_DEF, INSERT_DEF]
\\ fs[EXTENSION]
\\ rpt strip_tac
\\ metis_tac[])
>- fs[Once validTypesCmd_def]
>- (
imp_res_tac validTypesCmd_single
\\ find_exists_tac \\ fs[]
\\ first_x_assum MATCH_ACCEPT_TAC)
>- (fs[Once validRangesCmd_def])
>- (
`validRangesCmd f A (updEnv n vR_e E1) (toRTMap (toRExpMap Gamma))`
by (first_x_assum irule \\ fs[])
\\ imp_res_tac validRangesCmd_single
\\ rpt (find_exists_tac \\ fs[]))
>- (
fs[DIFF_DEF, domain_insert, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ simp[Once freeVars_def]
\\ once_rewrite_tac [domain_union]
\\ fs[]
\\ rw_thm_asm `x IN domain (freeVars f)` freeVars_def
\\ fs[])
\\ rpt strip_tac
\\ fs[updEnv_def] \\ rveq \\ fs[]
>- (qpat_x_assum `eval_expr E2 _ e nF _` kall_tac
\\ drule FPRangeValidator_sound
\\ rpt (disch_then drule)
\\ disch_then irule \\ fs[]
\\ fs[DIFF_DEF, domain_insert, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ simp[Once freeVars_def]
\\ once_rewrite_tac [domain_union]
\\ fs[]
\\ CCONTR_TAC \\ fs[] \\ rveq
\\ first_x_assum (qspec_then `n` assume_tac)
\\ res_tac)
\\ TOP_CASE_TAC \\ fs[]
\\ qpat_x_assum `eval_expr E2 _ e nF _` kall_tac
\\ drule FPRangeValidator_sound
\\ rpt (disch_then drule)
\\ disch_then irule \\ fs[]
\\ fs[DIFF_DEF, domain_insert, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ simp[Once freeVars_def]
\\ once_rewrite_tac [domain_union]
\\ fs[]
\\ CCONTR_TAC \\ fs[] \\ rveq
\\ first_x_assum (qspec_then `n` assume_tac)
\\ res_tac)
\\ fs[])
\\ qpat_x_assum validErrorboundCmd _ _ _ _
(assume_tac o SIMP_RULE std_ss [Once validErrorboundCmd_def]) \\ fs[]
\\ rpt (inversion `bstep (Ret _) _ _ _ _` bstep_cases)
\\ drule FPRangeValidator_sound
\\ rpt (disch_then drule)
......
This diff is collapsed.
......@@ -33,6 +33,45 @@ Definition mTypeToR_def:
| F w f => 1 / (2 pow f)
End
Definition maxExponent_def:
(maxExponent (REAL) = 0n) /\
(maxExponent (M16) = 15) /\
(maxExponent (M32) = 127) /\
(maxExponent (M64) = 1023) /\
(maxExponent (F w f) = f)
End
Definition minExponentPos_def:
(minExponentPos (REAL) = 0n) /\
(minExponentPos (M16) = 14) /\
(minExponentPos (M32) = 126) /\
(minExponentPos (M64) = 1022) /\
(minExponentPos (F w f) = f)
End
(**
Goldberg - Handbook of Floating-Point Arithmetic: (p.183)
(𝛃 - 𝛃^(1 - p)) * 𝛃^(e_max)
which simplifies to 2^(e_max) for base 2
**)
Definition maxValue_def:
maxValue (m:mType) =
case m of
| F w f => &((2n ** (w-1)) - 1) * inv &(2n ** (maxExponent m))
| _ => (&(2n ** (maxExponent m))):real
End
(** Using the sign bit, the very same number is representable as a negative number,
thus just apply negation here **)
Definition minValue_pos_def:
minValue_pos (m:mType) =
case m of
| F w f => 0
| _ => inv (&(2n ** (minExponentPos m)))
End