Commit 28fb7c69 authored by Heiko Becker's avatar Heiko Becker
Browse files

Add very coarse way of computing Sqrt for errors and intervals

parent 780f8cd7
......@@ -440,6 +440,42 @@ Proof
\\ rewrite_tac [ABS_MUL] \\ irule REAL_LE_LMUL_IMP \\ fs[]
QED
Theorem sqrt_abs_err_bounded:
!(e:real expr) (nR:real) nR1 (nF1:real) (nF:real) (E1:env) (E2:env) (err:real)
(m1 m:mType) (Gamma: real expr -> mType option).
eval_expr E1 (toRTMap Gamma) (toREval e) nR1 REAL /\
eval_expr E2 Gamma e nF1 m1 /\
eval_expr E1 (toRTMap Gamma) (toREval (Unop Sqrt e)) nR REAL /\
eval_expr (updEnv 1 nF1 emptyEnv)
(updDefVars (Unop Sqrt (Var 1)) m
(updDefVars (Var 1) m1 Gamma))
(Unop Sqrt (Var 1)) nF m /\
abs (nR1 - nF1) <= err
abs (nR - nF) <= abs (sqrt nR1 - sqrt nF1) + computeError (sqrt nF1) m
Proof
rpt strip_tac
\\ inversion `eval_expr (updEnv _ _ _) _ _ _ _` eval_expr_cases \\ gs[]
\\ inversion `eval_expr (updEnv _ _ _) _ _ _ _` eval_expr_cases \\ gs[]
\\ rveq \\ gs[toREval_def, updDefVars_def] \\ rveq
\\ inversion `eval_expr _ _ (Unop Sqrt _) _ _` eval_expr_cases \\ gs[]
\\ rveq \\ gs[]
\\ m1' = REAL by (Cases_on m1' \\ gs[isCompat_def])
\\ rveq \\ gs[perturb_def]
\\ v1 = nR1 by (imp_res_tac meps_0_deterministic \\ gs[])
\\ rveq
\\ Cases_on m \\ gs[perturb_def, evalUnop_def, computeError_pos, real_sub]
\\ TRY (COND_CASES_TAC \\ gs[])
\\ rewrite_tac [REAL_NEG_ADD, REAL_ADD_ASSOC, REAL_ADD_LDISTRIB]
\\ triangle_tac \\ gs[computeError_def, REAL_ABS_MUL]
\\ irule REAL_LE_TRANS THENL [
qexists_tac mTypeToR M16 (sqrt nF1) * abs (sqrt nF1),
qexists_tac mTypeToR M32 (sqrt nF1) * abs (sqrt nF1),
qexists_tac mTypeToR M64 (sqrt nF1) * abs (sqrt nF1)]
\\ conj_tac
\\ TRY (irule REAL_LE_RMUL_IMP \\ gs[])
\\ gs[REAL_MUL_COMM, mTypeToR_def]
QED
Theorem nonzerop_EQ1_I'[simp]:
0 < r (nonzerop r = 1)
Proof
......
......@@ -37,6 +37,22 @@ Definition inferErrorbound_def:
SOME (FloverMapTree_insert e (iv_f, err1) recRes);
od
| Unop Inv e1 => NONE
| Unop Sqrt e1 =>
do
recRes <- inferErrorbound e1 typeMap I akk;
(iv1, err1) <- FloverMapTree_find e1 recRes;
let errIve1 = widenInterval iv1 err1;
sqrtRealLo = newton ITERCOUNT (IVlo iv1 * 0.99) (IVlo iv1 * 0.99);
sqrtRealHi = newton ITERCOUNT (IVhi iv1 * 1.01) (IVhi iv1 * 1.01);
sqrtRealIv = (sqrtRealLo, sqrtRealHi);
sqrtFinLo= newton ITERCOUNT (IVlo errIve1 * 0.99) (IVlo errIve1 * 0.99);
sqrtFinHi = newton ITERCOUNT (IVhi errIve1 * 1.01) (IVhi errIve1 * 1.01);
sqrtFinIv = (sqrtFinLo, sqrtFinHi);
propError = maxAbs (subtractInterval sqrtRealIv sqrtFinIv);
mAbs = maxAbs sqrtFinIv
in
SOME (FloverMapTree_insert e (iv_f, propError + computeError mAbs m) recRes);
od
| Binop op e1 e2 =>
do
recRes1 <- inferErrorbound e1 typeMap I akk;
......
......@@ -11,7 +11,7 @@ open AbbrevsTheory ExpressionsTheory ExpressionSemanticsTheory RealSimpsTheory
RealRangeArithTheory FloverTactics MachineTypeTheory
ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
TypeValidatorTheory IntervalValidationTheory EnvironmentsTheory
CommandsTheory ssaPrgsTheory FloverMapTheory;
CommandsTheory ssaPrgsTheory FloverMapTheory sqrtApproxTheory;
open preambleFloVer;
val _ = new_theory "ErrorValidation";
......@@ -29,26 +29,51 @@ val triangle_tac =
fun real_rewrite t =
rewrite_tac [REAL_ARITH (Parse.Term t)];
val real_prove =
rpt (qpat_x_assum `!x. _` kall_tac)
\\ rpt (qpat_x_assum `_ ==> ! x. _` kall_tac)
\\ REAL_ASM_ARITH_TAC;
Definition validErrorbound_def:
validErrorbound e (typeMap: typeMap) (A:analysisResult) (dVars:num_set)=
case FloverMapTree_find e A, FloverMapTree_find e typeMap of
| NONE, _ => F
| _, NONE => F
| SOME (intv, err), SOME m =>
(if (0 <= err)
then
(if (0 <= err) then
case e of
| Var v =>
if (lookup v dVars = SOME ())
then T
if (lookup v dVars = SOME ()) then T
else computeError (maxAbs intv) m <= err
| Const _ n => (computeError (maxAbs intv) m <= err)
| Unop Neg e1 =>
if (validErrorbound e1 typeMap A dVars)
then
if (validErrorbound e1 typeMap A dVars) then
case (FloverMapTree_find e1 A) of
| SOME (_, err1) => err = err1
| _ => F
| SOME (_, err1) => err = err1
| _ => F
else F
| Unop Sqrt e1 =>
if (validErrorbound e1 typeMap A dVars) then
case (FloverMapTree_find e1 A) of
| SOME (iv1, err1) =>
let errIve1 = widenInterval iv1 err1;
sqrtRealLo = newton ITERCOUNT (IVlo iv1 * 0.99) (IVlo iv1 * 0.99);
sqrtRealHi = newton ITERCOUNT (IVhi iv1 * 1.01) (IVhi iv1 * 1.01);
sqrtRealIv = (sqrtRealLo, sqrtRealHi);
sqrtFinLo= newton ITERCOUNT (IVlo errIve1 * 0.99) (IVlo errIve1 * 0.99);
sqrtFinHi = newton ITERCOUNT (IVhi errIve1 * 1.01) (IVhi errIve1 * 1.01);
sqrtFinIv = (sqrtFinLo, sqrtFinHi);
propError = maxAbs (subtractInterval sqrtRealIv sqrtFinIv);
mAbs = maxAbs sqrtFinIv
in
if (validate_newton_down sqrtRealLo (IVlo iv1)
validate_newton_up sqrtRealHi (IVhi iv1)
validate_newton_down sqrtFinLo (IVlo errIve1)
validate_newton_up sqrtFinHi (IVhi errIve1)
0 < IVlo errIve1) then
propError + computeError mAbs m <= err
else F
| _ => F
else F
| Unop Inv e1 => F
| Binop op e1 e2 =>
......@@ -2232,6 +2257,80 @@ Proof
\\ rpt (first_x_assum (destruct) \\ fs[])
QED
Theorem validErrorboundCorrectSqrt:
(E1 E2:env) (A:analysisResult) (e:real expr)
(nR nR1 nF nF1:real) (err err1:real) (alo ahi elo ehi:real) dVars m m1 Gamma.
eval_Real E1 Gamma e nR1
eval_Fin E2 Gamma e nF1 m1
eval_Real E1 Gamma (Unop Sqrt e) nR
eval_expr (updEnv 1 nF1 emptyEnv)
(updDefVars (Unop Sqrt (Var 1)) m
(updDefVars (Var 1) m1 (toRExpMap Gamma)))
(Unop Sqrt (Var 1)) nF m /\
validErrorbound (Unop Sqrt e) Gamma A dVars
elo <= nR1 nR1 <= ehi
0 < elo
FloverMapTree_find e A = SOME ((elo, ehi), err1)
FloverMapTree_find (Unop Sqrt e) A = SOME ((alo, ahi), err)
FloverMapTree_find (Unop Sqrt e) Gamma = SOME m
abs (nR1 - nF1) <= err1
abs (nR - nF) <= err
Proof
fs [toREval_def] \\ rpt strip_tac
\\ fs[Once validErrorbound_eq] \\ rveq
\\ irule REAL_LE_TRANS
\\ qexists_tac abs (sqrt nR1 - sqrt nF1) + computeError (sqrt nF1) m
\\ conj_tac
>- (drule sqrt_abs_err_bounded \\ rpt $ disch_then drule
\\ disch_then $ qspecl_then [nR, nF, err1, m] mp_tac
\\ gs[toREval_def])
\\ contained nF1 (widenInterval (elo, ehi) err1)
by (irule distance_gives_iv \\ find_exists_tac \\ gs[contained_def])
\\ rpt (
qpat_x_assum `validate_newton_down _ _` $ mp_then Any mp_tac validate_newton_lb_valid
\\ impl_tac
>- (conj_tac
>- (irule newton_method_pos \\ conj_tac \\ irule REAL_LE_MUL \\ gs[] \\ real_prove)
\\ real_prove)
\\ strip_tac)
\\ 0 < ehi
by (
irule REAL_LTE_TRANS \\ qexists_tac elo \\ gs[]
\\ irule REAL_LE_TRANS \\ asm_exists_tac \\ gs[])
\\ 0 < SND (widenInterval (elo, ehi) err1)
by (
irule REAL_LTE_TRANS \\ qexists_tac FST (widenInterval (elo, ehi) err1) \\ gs[widenInterval_def]
\\ REAL_ASM_ARITH_TAC)
\\ rpt (
qpat_x_assum `validate_newton_up _ _` $ mp_then Any mp_tac validate_newton_ub_valid
\\ impl_tac
>- (conj_tac
>- (irule newton_method_pos \\ conj_tac \\ irule REAL_LE_MUL \\ gs[] \\ real_prove)
\\ real_prove)
\\ strip_tac)
\\ irule REAL_LE_TRANS \\ once_rewrite_tac[CONJ_COMM] \\ asm_exists_tac \\ gs[]
\\ irule REAL_LE_ADD2 \\ conj_tac
(* Prove propagation error *)
>- (
irule contained_leq_maxAbs
\\ assume_tac $ SIMP_RULE std_ss [validIntervalSub_def] interval_subtraction_valid
\\ pop_assum irule \\ conj_tac \\ gs[contained_def]
\\ conj_tac \\ irule REAL_LE_TRANS
>- (asm_exists_tac \\ gs[] \\ irule transcTheory.SQRT_MONO_LE \\ real_prove)
>- (once_rewrite_tac[CONJ_COMM] \\ asm_exists_tac \\ gs[]
\\ irule transcTheory.SQRT_MONO_LE \\ gs[] \\ REAL_ASM_ARITH_TAC)
>- (asm_exists_tac \\ gs[] \\ irule transcTheory.SQRT_MONO_LE \\ real_prove)
\\ once_rewrite_tac[CONJ_COMM] \\ asm_exists_tac \\ gs[]
\\ irule transcTheory.SQRT_MONO_LE \\ gs[] \\ REAL_ASM_ARITH_TAC)
(* New error *)
\\ irule computeError_up
\\ irule contained_leq_maxAbs
\\ gs[contained_def] \\ conj_tac \\ irule REAL_LE_TRANS
>- (asm_exists_tac \\ gs[] \\ irule transcTheory.SQRT_MONO_LE \\ real_prove)
\\ once_rewrite_tac[CONJ_COMM] \\ asm_exists_tac \\ gs[]
\\ irule transcTheory.SQRT_MONO_LE \\ gs[] \\ REAL_ASM_ARITH_TAC
QED
(**
Soundness theorem for the error bound validator.
Proof is by induction on the expression e.
......@@ -2277,31 +2376,79 @@ Proof
\\ qpat_x_assum `validErrorbound _ _ _ _` mp_tac
\\ simp[Once validErrorbound_eq] \\ strip_tac
\\ Cases_on `u` \\ fs[toREval_def] \\ rveq
>- (
rw_thm_asm `(domain _) DIFF _ SUBSET _` usedVars_def
\\ inversion `eval_expr E1 _ _ _ _` eval_expr_cases \\ fs[]
\\ `m' = REAL` by (irule toRTMap_eval_REAL \\ find_exists_tac \\ fs[])
\\ PairCases_on `v4` \\ fs[] \\ rveq
\\ rename1 `FloverMapTree_find e A = SOME ((e_lo, e_hi) , err)`
\\ once_rewrite_tac [eval_expr_cases] \\ fs[]
\\ first_x_assum
(qspecl_then
[`E1`, `E2`, `A`, `v1`, `err`, `e_lo`, `e_hi`, `fVars`,
`dVars`, `Gamma`]
destruct)
>- (fs[Once validTypes_def, Once validRanges_def])
\\ fs[Once validTypes_def, toRExpMap_def] \\ conj_tac \\ rpt strip_tac
>- (qexistsl_tac [`me`, `nF`] \\ fs[]
\\ `m' = me`
by (irule validTypes_exec
\\ rpt (find_exists_tac \\ fs[toRExpMap_def]))
\\ rveq \\ fs[])
\\ fs[evalUnop_def]
\\ once_rewrite_tac [real_sub]
\\ rewrite_tac [GSYM REAL_NEG_ADD, ABS_NEG, GSYM real_sub]
\\ first_x_assum drule
\\ rpt (disch_then drule)
\\ disch_then assume_tac \\ fs[]
\\ first_x_assum irule \\ asm_exists_tac \\ fs[])
\\ rw_thm_asm `(domain _) DIFF _ SUBSET _` usedVars_def
\\ inversion `eval_expr E1 _ _ _ _` eval_expr_cases \\ fs[]
\\ `m' = REAL` by (irule toRTMap_eval_REAL \\ find_exists_tac \\ fs[])
\\ PairCases_on `v4` \\ fs[] \\ rveq
\\ rename1 `FloverMapTree_find e A = SOME ((e_lo, e_hi) , err)`
\\ `m1 = REAL` by (irule toRTMap_eval_REAL \\ find_exists_tac \\ fs[])
\\ PairCases_on `iv1` \\ fs[] \\ rveq
\\ rename1 `FloverMapTree_find e A = SOME ((e_lo, e_hi) , err1)`
\\ once_rewrite_tac [eval_expr_cases] \\ fs[]
\\ first_x_assum
(qspecl_then
[`E1`, `E2`, `A`, `v1`, `err`, `e_lo`, `e_hi`, `fVars`,
`dVars`, `Gamma`]
destruct)
>- (fs[Once validTypes_def, Once validRanges_def])
\\ fs[Once validTypes_def, toRExpMap_def] \\ conj_tac \\ rpt strip_tac
>- (qexistsl_tac [`me`, `nF`] \\ fs[]
(qspecl_then
[`E1`, `E2`, `A`, `v1`, `err1`, `e_lo`, `e_hi`, `fVars`,
`dVars`, `Gamma`]
destruct)
>- (fs[Once validTypes_def, Once validRanges_def])
\\ qpat_x_assum `validRanges _ _ _ _` mp_tac
\\ qpat_x_assum `validTypes _ _` mp_tac
\\ simp[Once validRanges_def, Once validTypes_def]
\\ rpt $ disch_then strip_assume_tac
\\ imp_res_tac validRanges_single
\\ imp_res_tac meps_0_deterministic \\ rveq
\\ gs[] \\ rveq \\ gs[]
\\ fs[toRExpMap_def] \\ conj_tac \\ rpt strip_tac
>- (qexistsl_tac [`me`, `nF`, 0] \\ fs[]
\\ `m' = me`
by (irule validTypes_exec
\\ rpt (find_exists_tac \\ fs[toRExpMap_def]))
\\ rveq \\ fs[])
\\ fs[evalUnop_def]
\\ once_rewrite_tac [real_sub]
\\ rewrite_tac [GSYM REAL_NEG_ADD, ABS_NEG, GSYM real_sub]
\\ first_x_assum drule
\\ rpt (disch_then drule)
\\ disch_then assume_tac \\ fs[]
\\ first_x_assum irule \\ asm_exists_tac \\ fs[])
\\ rveq \\ fs[] \\ conj_tac
>- (irule mTypeToR_pos)
\\ res_tac \\ first_x_assum $ mp_then Any mp_tac distance_gives_iv
\\ gs[contained_def]
\\ disch_then $ qspec_then (e_lo, e_hi) mp_tac \\ gs[]
\\ strip_tac \\ irule REAL_LTE_TRANS
\\ qexists_tac FST (widenInterval (e_lo, e_hi) err') \\ gs[])
\\ rveq \\ res_tac
\\ irule validErrorboundCorrectSqrt
\\ qexistsl_tac [A, E1, E2, Gamma, ehi, elo, dVars, e,
e_hi, e_lo, err', m, m1, v1', v1]
\\ gs[toRExpMap_def] \\ rpt conj_tac
>- (gs[perturb_def, toRExpMap_def, toREval_def]
\\ vR = evalUnop Sqrt v1
by (
inversion `eval_expr E1 _ (Unop Sqrt _) _ _` eval_expr_cases \\ fs[]
\\ Cases_on m1' \\ gs[isCompat_def, perturb_def]
\\ imp_res_tac meps_0_deterministic \\ gs[])
\\ rveq \\ gs[])
>- simp[Once validErrorbound_def]
\\ irule Unop_sqrt' \\ fsrw_tac [SATISFY_ss] [updDefVars_def]
\\ qexistsl_tac [delta', m1, v1'] \\ gs[]
\\ simp[Once eval_expr_cases] \\ gs[updDefVars_def])
>- (rename1 `Binop op e1 e2` \\ fs[]
\\ qpat_x_assum `validErrorbound _ _ _ _` mp_tac
\\ simp[Once validErrorbound_eq] \\ strip_tac
......
......@@ -33,8 +33,12 @@ Definition eval_expr_float_def:
(eval_expr_float (Unop Neg e) E =
case eval_expr_float e E of
| SOME v => SOME (fp64_negate v)
| _ => NONE) /\
(eval_expr_float (Unop Inv e) E = NONE) /\
| _ => NONE)
(eval_expr_float (Unop Inv e) E = NONE)
(eval_expr_float (Unop Sqrt e) E =
case eval_expr_float e E of
| SOME v => SOME (fp64_sqrt dmode v)
| _ => NONE)
(eval_expr_float (Binop b e1 e2) E =
(case (eval_expr_float e1 E), (eval_expr_float e2 E) of
| SOME v1, SOME v2 =>
......@@ -115,6 +119,26 @@ Proof
\\ fs[REAL_MUL_RINV]
QED
Theorem zero_lt_sign_zero:
0 < float_to_real fp
fp.Sign = 0w
Proof
rpt strip_tac \\ CCONTR_TAC
\\ fp.Sign = 1w by (Cases_on fp.Sign \\ gs[])
\\ gs[float_to_real_def]
\\ 0 < 0:real suffices_by gs[]
\\ irule REAL_LTE_TRANS
\\ asm_exists_tac \\ gs[REAL_MUL_LNEG]
\\ Cases_on fp.Exponent = 0w \\ gs[real_div]
>- (
irule realTheory.REAL_LE_MUL \\ conj_tac
\\ irule realTheory.REAL_LE_MUL \\ gs[] )
\\ gs[real_div] \\ irule REAL_LE_MUL \\ conj_tac
\\ TRY (irule REAL_LE_MUL \\ gs[])
\\ irule REAL_LE_ADD \\ conj_tac \\ gs[]
\\ irule REAL_LE_MUL \\ conj_tac \\ gs[]
QED
Theorem pow_simp1[local] = Q.prove (`2 pow 2047 / 2 pow 1023 = 2 pow 1024`,
qspecl_then [`2`, `2047`,`1023`] destruct real_div_pow \\ fs[]);
......@@ -529,7 +553,6 @@ Theorem eval_expr_gives_IEEE:
is64BitEval (toRExp e) /\
is64BitEnv Gamma /\
noDowncast (toRExp e) /\
(* eval_expr_valid e E2 /\ *)
(v.
v domain dVars
vF m.
......@@ -604,6 +627,189 @@ Proof
qpat_x_assum validErrorbound _ _ _ _
(fn thm => mp_tac (ONCE_REWRITE_RULE [validErrorbound_def] thm))
\\ fs[option_case_eq] \\ rpt (TOP_CASE_TAC \\ fs[]))
>- (
fs[Once validTypes_def] \\ rveq
\\ imp_res_tac validTypes_single
\\ M64 = m1
by (qpat_x_assum isCompat m1 _ mp_tac \\ Cases_on m1
\\ simp[isCompat_def])
\\ rveq
\\ M64 = mG
by (qpat_x_assum toRExpMap _ _ = SOME _ mp_tac
\\ qpat_x_assum FloVerMapTree_find _ _ = SOME mG mp_tac
\\ simp[toRExpMap_def])
\\ me = M64
by (qpat_x_assum isCompat me _ mp_tac \\ rveq \\ Cases_on me
\\ simp[isCompat_def])
\\ rveq \\ fs[isCompat_def] \\ rpt (qpat_x_assum T kall_tac)
\\ rveq
\\ fs[eval_expr_float_def]
\\ first_x_assum
(qspecl_then
[`E1`, `E2`, `E2_real`, `Gamma`, `v1`, `A`, `fVars`, `dVars`]
destruct)
>- (
fs[] \\ rpt conj_tac
>- (fs[Once validTypes_def])
>- (rveq \\ rpt strip_tac
\\ drule validTypes_single \\ strip_tac \\ rfs[] \\ rveq
\\ first_x_assum irule
\\ find_exists_tac \\ fs[]
\\ asm_exists_tac \\ fs[])
>- (fs[Once validRanges_def])
>- (
qpat_x_assum validErrorbound _ _ _ _
(fn thm => assume_tac (ONCE_REWRITE_RULE [validErrorbound_def] thm))
\\ fs[option_case_eq]
\\ pop_assum mp_tac \\ rpt (TOP_CASE_TAC \\ fs[]))
>- (
rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
\\ fs[]
\\ Cases_on `FloverMapTree_find (Unop Sqrt (toRExp e)) A` \\ fs[]
\\ PairCases_on `x` \\ fs[]
\\ rw_asm_star `FloverMapTree_find (Unop _ _) Gamma = _`)
>- (rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def \\ fs[])
\\ rw_thm_asm `is64BitEval _` is64BitEval_def \\ fs[])
\\ fs[fp64_sqrt_def, fp64_to_float_float_to_fp64]
\\ qpat_x_assum `validRanges _ _ _ _` mp_tac
\\ simp[Once validRanges_def] \\ rpt strip_tac
\\ imp_res_tac validRanges_single
\\ rename1 FloverMapTree_find (toRExp e) A = SOME (iv1, err1)
\\ 0 < IVlo iv1 by (res_tac \\ gs[IVlo_def])
\\ rename1 IVlo iv1 vR1
(* Obtain evaluation for E2_real*)
\\ !vF1 m1. eval_expr E2_real (toRExpMap Gamma) (toRExp e) vF1 m1 ==>
abs (vR1 - vF1) <= err1
by (qspecl_then [`toRExp e`, `E1`, `E2_real`, `A`,`vR1`,
`err1`, `IVlo iv1`, `IVhi iv1`, `fVars`,
`dVars`,`Gamma`] destruct validErrorbound_sound
\\ rpt conj_tac \\ fs[]
>- (fs [DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
\\ qpat_x_assum validErrorbound _ _ _ _
(fn thm => mp_tac (ONCE_REWRITE_RULE [validErrorbound_def] thm))
\\ fs[option_case_eq] \\ rpt (TOP_CASE_TAC \\ fs[]))
\\ validFloatValue (float_to_real (fp64_to_float v)) M64
by (drule FPRangeValidator_sound
\\ disch_then $ qspecl_then [toRExp e, fp64_to_real v, M64] mp_tac
\\ gs[] \\ impl_tac
>- (rpt conj_tac
>- (drule eval_eq_env
\\ rpt $ disch_then drule \\ gs[fp64_to_real_def])
>- (
qpat_x_assum validErrorbound _ _ _ _
(fn thm => mp_tac (ONCE_REWRITE_RULE [validErrorbound_def] thm))
\\ fs[option_case_eq] \\ rpt (TOP_CASE_TAC \\ fs[]))
>- (
qpat_x_assum FPRangeValidator _ _ _ _
(fn thm => mp_tac (ONCE_REWRITE_RULE [FPRangeValidator_def] thm))
\\ fs[option_case_eq] \\ rpt (TOP_CASE_TAC \\ fs[]))
\\ fs [DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
\\ simp[fp64_to_real_def])
\\ contained (float_to_real (fp64_to_float v))
(widenInterval (FST iv1, SND iv1) err1)
by (
irule distance_gives_iv
\\ qexists_tac `vR1` \\ fs [contained_def]
\\ first_x_assum irule
\\ qexists_tac `M64`
\\ drule eval_eq_env
\\ rpt (disch_then drule) \\ fs[])
\\ 0 < FST (widenInterval (FST iv1, SND iv1) err1)
by (
qpat_x_assum validErrorbound _ _ _ _
(fn thm => mp_tac (ONCE_REWRITE_RULE [validErrorbound_def] thm))
\\ fs[option_case_eq] \\ rpt (TOP_CASE_TAC \\ fs[]))
\\ 0 < float_to_real (fp64_to_float v)
by (gs[contained_def, widenInterval_def] \\ irule REAL_LTE_TRANS
\\ asm_exists_tac \\ gs[])
\\ (fp64_to_float v).Sign = 0w
by imp_res_tac zero_lt_sign_zero
\\ validFloatValue (evalUnop Sqrt (float_to_real (fp64_to_float v))) M64
by (
drule FPRangeValidator_sound
\\ disch_then
(qspecl_then
[`Unop Sqrt (toRExp e)`,
`evalUnop Sqrt (float_to_real (fp64_to_float v))`, `M64`]
irule)
\\ fs[]
\\ qexists_tac e \\ fs[]
\\ rpt conj_tac
>- (simp[Once validTypes_def, isCompat_def] \\ first_x_assum MATCH_ACCEPT_TAC)
>- (simp[Once validRanges_def] \\ asm_exists_tac \\ fs[]
\\ fs[] \\ rveq \\ fs[])
\\ irule eval_eq_env
\\ qexists_tac toREnv E2 \\ rpt conj_tac >- fs[]
\\ irule Unop_sqrt'
\\ qexistsl_tac [0, `M64`, M64, `float_to_real (fp64_to_float v)`]
\\ fs[perturb_def, evalUnop_def, mTypeToR_pos, isCompat_def])
\\ qpat_x_assum `validFloatValue (evalUnop _ _) M64` (assume_tac o SIMP_RULE std_ss [validFloatValue_def])
\\ gs[]
(* normal sqrt *)
>- (
Q.ISPEC_THEN `(fp64_to_float v):(52,11) float`
impl_subgoal_tac
float_sqrt_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, evalUnop_def,
normalizes_def])
\\ fs[dmode_def] \\ simp[Once eval_expr_cases]
\\ qexistsl_tac [`M64`, `float_to_real (fp64_to_float v)`, e']
\\ fs[perturb_def, evalUnop_def]
\\ imp_res_tac normal_not_denormal
\\ fs[REAL_INV_1OVER, mTypeToR_def, isCompat_def])
(* denormal sqrt *)
>- (
Q.ISPEC_THEN `(fp64_to_float v):(52,11) float`
impl_subgoal_tac
float_sqrt_relative_denorm
>- (rpt conj_tac
>- fs[validFloatValue_def,
normalTranslatedValue_implies_finiteness,
denormalTranslatedValue_implies_finiteness,
normalValue_implies_normalization, float_is_finite,
GSYM float_is_zero_to_real, evalUnop_def]
>- fs[validFloatValue_def,
normalTranslatedValue_implies_finiteness,
denormalTranslatedValue_implies_finiteness,
normalValue_implies_normalization, float_is_finite,
GSYM float_is_zero_to_real, evalUnop_def]
>- (
fs[normalTranslatedValue_implies_finiteness,
denormalTranslatedValue_implies_finiteness,
normalValue_implies_normalization, float_is_finite,
GSYM float_is_zero_to_real, evalUnop_def, denormal_def, minValue_pos_def]
\\ rewrite_tac [INT_MAX_def, INT_MIN_def, dimindex_11, EVAL 2 ** (11 - 1) - 1 - 1]
\\ irule REAL_LT_TRANS
\\ asm_exists_tac \\ fs[GSYM REAL_OF_NUM_POW, minExponentPos_def]
\\ irule REAL_LET_TRANS \\ qexists_tac 1 * inv (2 pow 1022)
\\ conj_tac
>- (rewrite_tac[real_div] \\ irule REAL_LT_RMUL_IMP \\ fs[])
\\ fs[])
>- (irule REAL_LT_TRANS \\ qexists_tac maxValue M64
\\ fs[threshold_64_bit_lt_maxValue, denormal_def]
\\ irule REAL_LTE_TRANS \\ qexists_tac minValue_pos M64
\\ fs[minValue_pos_def, maxValue_def, GSYM REAL_OF_NUM_POW, evalUnop_def]
\\ irule REAL_LE_TRANS \\ qexists_tac 1 \\ conj_tac
>- (once_rewrite_tac[GSYM REAL_INV1] \\ irule REAL_INV_LE_ANTIMONO_IMPR
\\ fs[POW_2_LE1])
\\ fs[POW_2_LE1])
\\ fs[INT_MAX_def, INT_MIN_def, dimindex_11])
\\ gs[dmode_def] \\ simp[Once eval_expr_cases]
\\ qexistsl_tac [`M64`, `float_to_real (fp64_to_float v)`, e']
\\ fs[perturb_def, evalUnop_def]
\\ fs[REAL_INV_1OVER, mTypeToR_def, isCompat_def, minExponentPos_def])
(* sqrt 0 *)
\\ 0 < sqrt (float_to_real (fp64_to_float v)) by (irule transcTheory.SQRT_POS_LT \\ gs[])
\\ gs[evalUnop_def])
>- (
rename1 `Binop b (toRExp e1) (toRExp e2)` \\ rveq
\\ IMP_RES_TAC validRanges_single
......@@ -1786,9 +1992,8 @@ Proof
\\ rpt conj_tac \\ fs[is64BitBstep_def]
QED
val IEEE_connection_expr = store_thm (
"IEEE_connection_expr",
``!(e:word64 expr) (A:analysisResult) (P:precond) E1 E2 defVars fVars Gamma.
Theorem IEEE_connection_expr:
!(e:word64 expr) (A:analysisResult) (P:precond) E1 E2 defVars fVars Gamma.
is64BitEval (toRExp e) /\
is64BitEnv defVars /\
noDowncast (toRExp e) /\
......@@ -1802,7 +2007,8 @@ val IEEE_connection_expr = store_thm (
eval_expr_float e E2 = SOME vF /\
eval_expr (toREnv E2) (toRExpMap Gamma) (toRExp e)
(float_to_real (fp64_to_float vF)) M64 /\
abs (vR - (float_to_real (fp64_to_float vF))) <= err``,
abs (vR - (float_to_real (fp64_to_float vF))) <= err
Proof
simp [CertificateChecker_def]
\\ rpt strip_tac
\\ Cases_on `getValidMap defVars (toRExp e) FloverMapTree_empty` \\ fs[]
......@@ -1837,11 +2043,11 @@ val IEEE_connection_expr = store_thm (
\\ rveq \\ fs[])
\\ fs[is64BitEnv_def] \\ first_x_assum MATCH_ACCEPT_TAC)
\\ rpt (find_exists_tac \\ fs[])