Commit 712ea61c authored by Heiko Becker's avatar Heiko Becker
Browse files

Prove full IEEE connection in HOL4

parent 4ef8e1a3
......@@ -82,7 +82,7 @@ val Certificate_checking_is_sound = store_thm ("Certificate_checking_is_sound",
val CertificateCmd_checking_is_sound = store_thm ("CertificateCmd_checking_is_sound",
``!(f:real cmd) (absenv:analysisResult) (P:precond) defVars
(E1 E2:env) (outVars:num_set) fVars.
(E1 E2:env) (fVars:num_set).
approxEnv E1 defVars absenv (freeVars f) LN E2 /\
(!v.
v IN (domain (freeVars f)) ==>
......
......@@ -3,7 +3,7 @@
**)
open preamble
open simpLib realTheory realLib RealArith
open AbbrevsTheory ExpressionAbbrevsTheory MachineTypeTheory
open AbbrevsTheory ExpressionsTheory ExpressionAbbrevsTheory MachineTypeTheory
val _ = new_theory "Commands";
......@@ -68,4 +68,17 @@ val definedVars_def = Define `
|Let m (x:num) e g => insert x () (definedVars g)
|Ret e => LN`;
val bstep_eq_env = store_thm (
"bstep_eq_env",
``!f E1 E2 Gamma v m.
(!x. E1 x = E2 x) /\
bstep f E1 Gamma v m ==>
bstep f E2 Gamma v m``,
Induct \\ rpt strip_tac \\ fs[bstep_cases]
>- (qexists_tac `v'` \\ conj_tac
\\ TRY (drule eval_eq_env \\ disch_then drule \\ fs[] \\ FAIL_TAC"")
\\ first_x_assum irule \\ qexists_tac `updEnv n v' E1` \\ fs[]
\\ rpt strip_tac \\ fs[updEnv_def])
\\ irule eval_eq_env \\ asm_exists_tac \\ fs[]);
val _ = export_theory ();
......@@ -290,6 +290,26 @@ 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 eval_eq_env = store_thm (
"eval_eq_env",
``!e E1 E2 Gamma v m.
(!x. E1 x = E2 x) /\
eval_exp E1 Gamma e v m ==>
eval_exp E2 Gamma e v m``,
Induct \\ rpt strip_tac \\ fs[eval_exp_cases]
>- (`E1 n = E2 n` by (first_x_assum irule)
\\ fs[])
>- (qexists_tac `delta'` \\ fs[])
>- (rveq \\ qexists_tac `v1` \\ fs[]
\\ first_x_assum drule \\ disch_then irule \\ fs[])
>- (rveq \\ qexists_tac `v1` \\ fs[]
\\ qexists_tac `delta'` \\ fs[]
\\ 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'`, `v1`, `delta'`] \\ fs[]
\\ first_x_assum drule \\ disch_then irule \\ fs[]));
(* (** *)
(* Analogous lemma for unary expressions *)
(* **) *)
......
......@@ -2,8 +2,10 @@ open preamble
open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory
open MachineTypeTheory ExpressionsTheory RealSimpsTheory DaisyTactics CertificateCheckerTheory
open FPRangeValidatorTheory IntervalValidationTheory TypingTheory ErrorValidationTheory IntervalArithTheory AbbrevsTheory
open MachineTypeTheory ExpressionsTheory RealSimpsTheory DaisyTactics
CertificateCheckerTheory FPRangeValidatorTheory IntervalValidationTheory
TypingTheory ErrorValidationTheory IntervalArithTheory AbbrevsTheory
CommandsTheory ssaPrgsTheory EnvironmentsTheory
val _ = new_theory "IEEE_connection";
......@@ -13,6 +15,13 @@ val _ = temp_overload_on("abs",``real$abs``);
a rounding mode here **)
val dmode_def = Define `dmode = roundTiesToEven`;
val optionLift_def = Define `
(optionLift (SOME v) some_cont none_cont = some_cont v) /\
(optionLift (NONE) some_cont none_cont = none_cont)`;
val updFlEnv_def = Define `
updFlEnv x v E = \ y. if y = x then SOME v else E y`;
val eval_exp_float_def = Define `
(eval_exp_float (Var n) E = E n) /\
(eval_exp_float (Const m v) E = SOME v) /\
......@@ -32,9 +41,12 @@ val eval_exp_float_def = Define `
| _, _ => NONE)) /\
(eval_exp_float (Downcast m e) E = NONE)`;
val optionLift_def = Define `
(optionLift (SOME v) some_cont none_cont = some_cont v) /\
(optionLift (NONE) some_cont none_cont = none_cont)`;
val bstep_float_def = Define `
(bstep_float (Let m x e g) E :word64 option=
optionLift (eval_exp_float e E)
(\ v. bstep_float g (updFlEnv x v E))
NONE) /\
(bstep_float (Ret e) E = eval_exp_float e E)`;
val normal_or_zero_def = Define `
normal_or_zero (v:real) =
......@@ -64,6 +76,13 @@ val eval_exp_valid_def = Define `
normal_or_zero (evalBinop b v1_real v2_real)) F) F
else F)`;
val bstep_valid_def = Define `
(bstep_valid (Let m x e g) E =
optionLift (eval_exp_float e E)
(\v_e. eval_exp_valid e E /\ bstep_valid g (updFlEnv x v_e E))
F) /\
(bstep_valid (Ret e) E = eval_exp_valid e E)`;
val toRExp_def = Define `
(toRExp ((Var v):word64 exp) = Var v) /\
(toRExp (Const m c) = Const m (float_to_real (fp64_to_float c))) /\
......@@ -71,6 +90,10 @@ val toRExp_def = Define `
(toRExp (Binop b e1 e2) = Binop b (toRExp e1) (toRExp e2)) /\
(toRExp (Downcast m e1) = Downcast m (toRExp e1))`;
val toRCmd_def = Define `
(toRCmd (Let m x e g) = Let m x (toRExp e) (toRCmd g)) /\
(toRCmd (Ret e) = Ret (toRExp e))`;
val toREnv_def = Define `
toREnv (E:num -> word64 option) (x:num):real option =
case E x of
......@@ -413,6 +436,10 @@ val noDowncast_def = Define `
(noDowncast (Binop b e1 e2) = (noDowncast e1 /\ noDowncast e2)) /\
(noDowncast (Downcast _ _) = F)`;
val noDowncastFun_def = Define `
(noDowncastFun (Let m x e g) = (noDowncast e /\ noDowncastFun g)) /\
(noDowncastFun (Ret e) = noDowncast e)`;
(* val noDenormalCst_def = Define ` *)
(* (noDenormalCst (Const m v) = ~ denormal (float_to_real (fp64_to_float v)) m) /\ *)
(* (noDenormalCst (Var v) = T) /\ *)
......@@ -427,10 +454,14 @@ val is64BitEval_def = Define `
(is64BitEval (Downcast m e) = is64BitEval e) /\
(is64BitEval ((Var v):real exp) = T)`;
val is64BitBstep_def = Define `
(is64BitBstep (Let m x e g) = ((m = M64) /\ is64BitEval e /\ is64BitBstep g)) /\
(is64BitBstep (Ret e) = is64BitEval e)`;
val typeMap_eq_typeExp = Q.prove(`!e. typeMap Gamma e e = typeExpression Gamma e`,
Induct \\ fs[Once typeMap_def] \\ rpt strip_tac \\ fs[Once typeExpression_def] );
val typing_is_64bit = store_thm("typing_is_64bit",
val typing_exp_64bit = store_thm("typing_exp_64bit",
``!e Gamma tMap.
noDowncast e /\ is64BitEval e /\
typeCheck e Gamma tMap /\
......@@ -471,8 +502,36 @@ Induct
\\ Cases_on `tMap e1` \\ Cases_on `tMap e2` \\ fs[])
\\ fs[join_def]));
val typing_agrees = store_thm (
"typing_agrees",
val typing_cmd_64bit = store_thm (
"typing_cmd_64bit",
``!f Gamma tMap.
noDowncastFun f /\
is64BitBstep f /\
typeCheckCmd f Gamma tMap /\
(!v. v IN domain (freeVars f) ==> Gamma v = SOME M64) ==>
tMap (getRetExp f) = SOME M64``,
Induct \\ rpt strip_tac
\\ rw_thm_asm `typeCheckCmd _ _ _` typeCheckCmd_def
\\ fs[]
>- (every_case_tac \\ fs[]
\\ rveq
\\ once_rewrite_tac [getRetExp_def]
\\ fs[]
\\ first_x_assum irule
\\ fs[Once is64BitBstep_def, Once noDowncastFun_def]
\\ qexists_tac `updDefVars n m Gamma`
\\ fs[]
\\ rpt strip_tac
\\ fs[updDefVars_def] \\ IF_CASES_TAC \\ fs[]
\\ first_x_assum irule
\\ simp[Once freeVars_def, domain_union])
\\ fs [getRetExp_def, freeVars_def]
\\ irule typing_exp_64bit
\\ fs[Once is64BitBstep_def, Once noDowncastFun_def]
\\ asm_exists_tac \\ fs[]);
val typing_agrees_exp = store_thm (
"typing_agrees_exp",
``!e E Gamma tMap v m1 m2 .
typeCheck e Gamma tMap /\
eval_exp E Gamma e v m1 /\
......@@ -507,6 +566,24 @@ val typing_agrees = store_thm (
\\ qpat_x_assum `tMap (Downcast m e) = SOME _` (fn thm => fs[thm])
\\ Cases_on `tMap e` \\ fs[]));
val typing_agrees_cmd = store_thm (
"typing_agrees_cmd",
``!f E Gamma v m1 m2 tMap.
typeCheckCmd f Gamma tMap /\
bstep f E Gamma v m1 /\
tMap (getRetExp f) = SOME m2 ==>
m1 = m2``,
Induct \\ rpt strip_tac \\ fs[bstep_cases]
>- (rw_thm_asm `typeCheckCmd _ _ _` typeCheckCmd_def
\\ Cases_on `tMap e` \\ Cases_on `tMap (Var n)` \\ fs[]
\\ rveq \\ first_x_assum irule
\\ rewrite_tac [CONJ_ASSOC] \\ rpt (once_rewrite_tac[CONJ_COMM] \\ asm_exists_tac \\ fs[])
\\ fs[Once getRetExp_def])
\\ fs[typeCheckCmd_def, getRetExp_def]
\\ drule typing_agrees_exp
\\ rpt (disch_then drule)
\\ fs[] );
(* val asFpOp_def = Define ` *)
(* (asFpOp (Plus) = fp64_add dmode) /\ *)
(* (asFpOp (Sub) = fp64_sub dmode) /\ *)
......@@ -532,10 +609,11 @@ val typing_agrees = store_thm (
(* no_denormal_binds E = *)
(* !n v. E n = SOME v ==> ~ (denormal (float_to_real (fp64_to_float v)) M64)`; *)
val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
``!(e:word64 exp) E1 E2 Gamma tMap vR A P fVars dVars .
val eval_exp_gives_IEEE = store_thm ("eval_exp_gives_IEEE",
``!(e:word64 exp) E1 E2 E2_real Gamma tMap vR A P fVars dVars .
(!x. (toREnv E2) x = E2_real x) /\
typeCheck (toRExp e) Gamma tMap /\
approxEnv E1 Gamma A fVars dVars (toREnv E2) /\
approxEnv E1 Gamma A fVars dVars E2_real /\
validIntervalbounds (toRExp e) A P dVars /\
validErrorbound (toRExp e) tMap A dVars /\
FPRangeValidator (toRExp e) A tMap dVars /\
......@@ -556,7 +634,7 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
(v.
v domain dVars
vF m.
(toREnv E2 v = SOME vF tMap (Var v) = SOME m
(E2_real v = SOME vF tMap (Var v) = SOME m
validFloatValue vF m)) /\
(!v. v IN domain (usedVars (toRExp e)) ==> Gamma v = SOME M64) ==>
?v.
......@@ -586,7 +664,7 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
\\ fs[mTypeToQ_pos, perturb_def, fp64_to_float_float_to_fp64,
zero_to_real])
>- (fs[eval_exp_float_def, optionLift_def]
\\ first_x_assum (qspecl_then [`E1`, `E2`, `Gamma`, `tMap`, `v1`, `A`, `P`, `fVars`, `dVars`] destruct)
\\ first_x_assum (qspecl_then [`E1`, `E2`, `E2_real`, `Gamma`, `tMap`, `v1`, `A`, `P`, `fVars`, `dVars`] destruct)
>- (rw_thm_asm `typeCheck _ _ _` typeCheck_def
\\ rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def
\\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
......@@ -594,6 +672,7 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
\\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
\\ rw_thm_asm `is64BitEval _` is64BitEval_def
\\ fs[]
\\ rveq
\\ Cases_on `A (Unop Neg (toRExp e))` \\ Cases_on ` A (toRExp e)` \\ fs[]
\\ Cases_on `tMap (Unop Neg (toRExp e))` \\ Cases_on `tMap (toRExp e)` \\fs[]
\\ rpt conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
......@@ -610,7 +689,7 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
>- (rename1 `Binop b (toRExp e1) (toRExp e2)`
\\ qpat_x_assum `M64 = _` (fn thm => fs [GSYM thm])
\\ `tMap (toRExp e1) = SOME M64 /\ tMap(toRExp e2) = SOME M64 /\ tMap (Binop b (toRExp e1) (toRExp e2)) = SOME M64`
by (rpt conj_tac \\ irule typing_is_64bit \\ fs[is64BitEval_def, noDowncast_def]
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)`
......@@ -619,7 +698,7 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
\\ `m1 = M64 /\ m2 = M64`
by (conj_tac
\\ rw_thm_asm `typeCheck _ _ _` typeCheck_def
\\ irule typing_agrees
\\ irule typing_agrees_exp
\\ qexistsl_tac [`toREnv E2`, `Gamma`]
THENL [qexists_tac `toRExp e1`, qexists_tac `toRExp e2`]
\\ qexistsl_tac [`tMap`]
......@@ -629,7 +708,7 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
\\ rw_asm_star `tMap (toRExp e2) = _`
\\ rw_asm_star `tMap (Binop b (toRExp e1) (toRExp e2)) = _`)
\\ rveq
\\ ntac 2 (first_x_assum (qspecl_then [`E1`, `E2`, `Gamma`, `tMap`] assume_tac))
\\ ntac 2 (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
......@@ -673,9 +752,10 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
\\ fs [DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
\\ `!vF2 m2. eval_exp (toREnv E2) Gamma (toRExp e2) vF2 m2 ==>
(* Obtain evaluation for E2_real*)
\\ `!vF2 m2. eval_exp E2_real Gamma (toRExp e2) vF2 m2 ==>
abs (nR2 - vF2) <= SND (A (toRExp e2))`
by (qspecl_then [`toRExp e2`, `E1`, `toREnv E2`, `A`,`nR2`,
by (qspecl_then [`toRExp e2`, `E1`, `E2_real`, `A`,`nR2`,
`SND (A (toRExp e2))`, `P`,
`FST (FST (A (toRExp e2)))`,
`SND (FST (A (toRExp e2)))`, `fVars`, `dVars`,
......@@ -699,7 +779,9 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
by (irule distance_gives_iv
\\ qexists_tac `nR2` \\ fs [contained_def, IVlo_def, IVhi_def]
\\ first_x_assum irule
\\ qexists_tac `M64` \\ fs[])
\\ qexists_tac `M64`
\\ drule eval_eq_env
\\ rpt (disch_then drule) \\ fs[])
\\ `b = Div ==> float_to_real (fp64_to_float vF2) <> 0`
by (strip_tac
\\ rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def
......@@ -732,11 +814,23 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
\\ fs[]
\\ qexistsl_tac [`P`, `e1`, `e2`, `tMap`]
\\ fs[]
\\ simp[typeCheck_def, eval_exp_cases]
(* \\ conj_tac *)
(* >- (rpt strip_tac *)
(* \\ `?vF m. (toREnv E2) v = SOME vF /\ *)
(* tMap (Var v) = SOME m /\ *)
(* validFloatValue vF m` *)
(* by (first_x_assum irule \\ fs[]) *)
(* \\ fs[] \\ qexists_tac `vF` \\ fs[] *)
(* \\ `E2_real v = toREnv E2 v` by metis_tac[] *)
(* \\ fs[]) *)
\\ irule eval_eq_env
\\ asm_exists_tac \\ fs[eval_exp_cases]
\\ rewrite_tac [CONJ_ASSOC]
\\ rpt (once_rewrite_tac [CONJ_COMM] \\ asm_exists_tac \\ fs[])
\\ rpt (once_rewrite_tac [CONJ_COMM]
\\ asm_exists_tac \\ fs[])
\\ qexists_tac ` 0:real`
\\ Cases_on `b` \\ fs[perturb_def, evalBinop_def, mTypeToQ_pos, join_def])
\\ Cases_on `b`
\\ fs[perturb_def, evalBinop_def, mTypeToQ_pos, join_def])
\\ `validFloatValue (float_to_real (fp64_to_float vF1)) M64`
by (drule FPRangeValidator_sound
\\ disch_then
......@@ -753,11 +847,13 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
\\ rw_asm_star `tMap (Binop b (toRExp e1) (toRExp e2)) = SOME _`
\\ rw_asm_star `tMap (toRExp e1) = _`
\\ rw_asm_star `tMap (toRExp e2) = _`
\\ Cases_on `A (Binop b (toRExp e1) (toRExp e2))` \\ Cases_on `A (toRExp e1)`
\\ Cases_on `A (toRExp e2)` \\ fs[]
\\ fs[SUBSET_DEF, DIFF_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ simp[Once usedVars_def, domain_union] \\ fs[])
\\ rewrite_tac[CONJ_ASSOC] \\ conj_tac
>- (Cases_on `A (Binop b (toRExp e1) (toRExp e2))` \\ Cases_on `A (toRExp e1)`
\\ Cases_on `A (toRExp e2)` \\ fs[]
\\ fs[SUBSET_DEF, DIFF_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ simp[Once usedVars_def, domain_union] \\ fs[])
\\ irule eval_eq_env \\ asm_exists_tac \\ fs[])
\\ `validFloatValue (float_to_real (fp64_to_float vF2)) M64`
by (drule FPRangeValidator_sound
\\ disch_then
......@@ -775,11 +871,13 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
\\ rw_asm_star `tMap (Binop b (toRExp e1) (toRExp e2)) = SOME _`
\\ rw_asm_star `tMap (toRExp e1) = _`
\\ rw_asm_star `tMap (toRExp e2) = _`
\\ Cases_on `A (Binop b (toRExp e1) (toRExp e2))` \\ Cases_on `A (toRExp e1)`
\\ Cases_on `A (toRExp e2)` \\ fs[]
\\ fs[SUBSET_DEF, DIFF_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ simp[Once usedVars_def, domain_union] \\ fs[])
\\ rewrite_tac[CONJ_ASSOC] \\ conj_tac
>- (Cases_on `A (Binop b (toRExp e1) (toRExp e2))` \\ Cases_on `A (toRExp e1)`
\\ Cases_on `A (toRExp e2)` \\ fs[]
\\ fs[SUBSET_DEF, DIFF_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ simp[Once usedVars_def, domain_union] \\ fs[])
\\ irule eval_eq_env \\ asm_exists_tac \\ fs[])
\\ simp[eval_exp_cases]
(** Case distinction for operator **)
......@@ -976,8 +1074,307 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
`float_to_real (fp64_to_float vF2)`, `0:real`]
\\ fs[perturb_def, join_def, mTypeToQ_pos])));
val final_thm = store_thm (
"final_thm",
val bstep_gives_IEEE = store_thm (
"bstep_gives_IEEE",
``!(f:word64 cmd) E1 E2 E2_real Gamma tMap vR vF A P fVars dVars outVars.
(!x. (toREnv E2) x = E2_real x) /\
approxEnv E1 Gamma A fVars dVars E2_real /\
ssa (toRCmd f) (union fVars dVars) outVars /\
typeCheckCmd (toRCmd f) Gamma tMap /\
validIntervalboundsCmd (toRCmd f) A P dVars /\
validErrorboundCmd (toRCmd f) tMap A dVars /\
FPRangeValidatorCmd (toRCmd f) A tMap dVars /\
bstep (toREvalCmd (toRCmd f)) E1 (toRMap Gamma) vR M0 /\
bstep (toRCmd f) (toREnv E2) Gamma vF M64 /\
domain (freeVars (toRCmd f)) DIFF domain dVars domain fVars
is64BitBstep (toRCmd f) /\
noDowncastFun (toRCmd f) /\
bstep_valid f E2 /\
(v.
v domain fVars
vR. E1 v = SOME vR FST (P v) vR vR SND (P v))
(v. v domain fVars v domain dVars m. Gamma v = SOME m)
(v.
v domain dVars
vR.
E1 v = SOME vR FST (FST (A (Var v))) vR
vR SND (FST (A (Var v)))) /\
(v.
v domain dVars
vF m.
(E2_real v = SOME vF tMap (Var v) = SOME m
validFloatValue vF m)) /\
(!v. v IN domain (freeVars (toRCmd f)) ==> Gamma v = SOME M64) ==>
?v.
bstep_float f E2 = SOME v /\
bstep (toRCmd f) (toREnv E2) Gamma (float_to_real (fp64_to_float v)) M64``,
Induct_on `f`
\\ simp [toRCmd_def, Once toREvalCmd_def, is64BitBstep_def,
noDowncastFun_def, bstep_valid_def]
\\ rpt strip_tac
\\ rpt (inversion `bstep (Let _ _ _ _) _ _ _ _` bstep_cases)
\\ inversion `ssa _ _ _` ssa_cases
\\ once_rewrite_tac [bstep_float_def]
\\ fs[bstep_valid_def, noDowncast_def]
>- (`?v_e. eval_exp_float e E2 = SOME v_e /\
eval_exp (toREnv E2) Gamma (toRExp e) (float_to_real (fp64_to_float v_e)) M64`
by (irule eval_exp_gives_IEEE \\ fs[]
>- (rpt strip_tac \\ first_x_assum irule
\\ fs[Once freeVars_def, domain_union]
\\ CCONTR_TAC \\ fs[] \\ rveq \\ fs[]
\\ fs[SUBSET_DEF, domain_union]
\\ `n IN domain fVars \/ n IN domain dVars`
by (first_x_assum irule \\ fs[]))
>- (fs[optionLift_def] \\ Cases_on `eval_exp_float e E2`
\\ fs[optionLift_def])
>- (rveq \\ asm_exists_tac \\ fs[])
\\ fs [Once validIntervalboundsCmd_def, Once validErrorboundCmd_def,
Once typeCheckCmd_def, Once FPRangeValidatorCmd_def]
\\ rewrite_tac [CONJ_ASSOC]
\\ rpt (once_rewrite_tac [CONJ_COMM] \\ asm_exists_tac \\ fs[])
\\ rpt conj_tac \\ fs[] \\ rpt strip_tac
>- (qpat_x_assum `!v. v IN domain dVars ==> _`
(qspec_then `v''` impl_subgoal_tac)
\\ fs[])
>- (qpat_x_assum `!v. v IN domain dVars ==> ?vR. _ /\ _ /\ _`
(qspec_then `v''` impl_subgoal_tac)
\\ fs[])
>- (qpat_x_assum `!v. v IN domain fVars ==> _`
(qspec_then `v''` impl_subgoal_tac)
\\ fs[])
\\ fs[Once freeVars_def, domain_union, DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac
\\ `x IN domain fVars \/ x IN domain dVars`
by (first_x_assum irule \\ fs[]))
(* prove validity of errorbound for floating-point value *)
\\ qspecl_then
[`toRExp e`, `E1`, `E2_real`, `A`, `v'`,
`SND (A (toRExp e))`, `P`, `FST(FST(A (toRExp e)))`,
`SND (FST (A (toRExp e)))`, `fVars`, `dVars`, `tMap`, `Gamma`]
impl_subgoal_tac
validErrorbound_sound
>- (fs[Once typeCheckCmd_def, Once validIntervalboundsCmd_def,
Once validErrorboundCmd_def]
\\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
\\ fs[DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule \\ fs[Once freeVars_def, domain_union]
\\ CCONTR_TAC \\ fs[] \\ rveq \\ fs[]
\\ `n IN domain fVars \/ n IN domain dVars`
by (first_x_assum irule \\ fs[]))
\\ fs[]
\\ `abs (v' - (float_to_real (fp64_to_float v_e))) <= SND (A (toRExp e))`
by (first_x_assum irule \\ fs[]
\\ qexists_tac `M64` \\ irule eval_eq_env \\ asm_exists_tac \\ fs[])
(* Now construct a new evaluation according to our big-step semantics
using lemma validErrorboundCmd_gives_eval *)
(* CONTINUE HERE *)
\\ Cases_on `A (getRetExp (toRCmd f))`
\\ rename1 `A (getRetExp _) = (iv_f,err_f)`
\\ Cases_on `iv_f` \\ rename1 `A (getRetExp _) = ((f_lo, f_hi), err_f)`
\\ qspecl_then
[ `toRCmd f`, `A`, `updEnv n v' E1`,
`updEnv n (float_to_real (fp64_to_float v_e)) E2_real`,
`outVars`, `fVars`, `insert n () dVars`, `vR`, `f_lo`, `f_hi`,
`err_f`, `P`, `M64`, `tMap`, `updDefVars n M64 Gamma`]
impl_subgoal_tac
validErrorboundCmd_gives_eval
>- (rw_thm_asm `typeCheckCmd _ _ _` typeCheckCmd_def
\\ fs[Once validIntervalboundsCmd_def,
Once validErrorboundCmd_def]
\\ Cases_on `tMap (toRExp e)` \\ Cases_on `tMap (Var n)` \\ fs[]
\\ rveq \\ fs[]
\\ rpt conj_tac \\ fs[]
>- (irule approxUpdBound
\\ fs[lookup_NONE_domain]
\\ `A (Var n) = A (toRExp e)` by (fs[])
\\ qpat_x_assum `A (Var n) = A (toRExp e)`
(fn thm => fs[thm]))
>- (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[DIFF_DEF, domain_insert, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ fs[Once freeVars_def]
\\ simp[Once freeVars_def, domain_union])
>- (irule swap_Gamma_bstep
\\ qexists_tac `updDefVars n M0 (toRMap Gamma)` \\ fs[]
\\ MATCH_ACCEPT_TAC Rmap_updVars_comm)
>- (rpt strip_tac \\ simp[updEnv_def]
\\ rveq \\ fs[]
>- (qpat_x_assum `A (toRExp e) = A (Var n)` (fn thm=> once_rewrite_tac [GSYM thm])
\\ drule validIntervalbounds_sound
\\ rpt (disch_then drule)
\\ disch_then (qspecl_then [`fVars`, `Gamma`] impl_subgoal_tac)
>- (fs[] \\ 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 freeVars_def, domain_union]
\\ CCONTR_TAC \\ fs[]
\\ rveq
\\ `n IN domain fVars \/ n IN domain dVars`
by (first_x_assum irule \\ fs[]))
\\ fs[]
\\ metis_tac [meps_0_deterministic])
\\ IF_CASES_TAC \\ fs[]
\\ rveq
\\ fs[domain_union])
>- (rpt strip_tac \\ simp[updEnv_def]
\\ IF_CASES_TAC \\ fs[]
\\ rveq
\\ fs[domain_union])
\\ rpt strip_tac \\ fs[updDefVars_def]
\\ IF_CASES_TAC \\ fs[]
\\ TRY (first_x_assum irule \\ fs[]))
\\ fs[optionLift_def]
\\ `tMap (getRetExp (toRCmd f)) = SOME M64`
by (irule typingSoundnessCmd
\\ qexistsl_tac [`updEnv n v (toREnv E2)`, `updDefVars n M64 Gamma`, `vF`]
\\ fs[]
\\ rw_thm_asm `typeCheckCmd _ _ _` typeCheckCmd_def
\\ EVERY_CASE_TAC \\ fs[]\\ rveq \\ fs[])
\\ `m' = M64`
by (irule typing_agrees_cmd
\\ rewrite_tac [CONJ_ASSOC] \\ once_rewrite_tac[CONJ_COMM]
\\ rpt (asm_exists_tac \\ fs[])
\\ rw_thm_asm `typeCheckCmd _ _ _` typeCheckCmd_def
\\ EVERY_CASE_TAC \\ fs[] \\ rveq \\ fs[])
\\ rveq \\ fs[bstep_cases, PULL_EXISTS]
(* Instantiate IH with newly obtained evaluation, to get the conclusion *)
\\ first_x_assum
(qspecl_then [`updEnv n v' E1`, `updFlEnv n v_e E2`,
`updEnv n (float_to_real (fp64_to_float v_e)) E2_real`,
`updDefVars n M64 Gamma`, `tMap`, `vR`, `vF'`, `A`,
`P`, `fVars`, `insert n () dVars`, `outVars`]
impl_subgoal_tac)
>- (fs[Once validErrorboundCmd_def, Once validIntervalboundsCmd_def,
Once FPRangeValidatorCmd_def]
\\ rw_thm_asm `typeCheckCmd _ _ _` typeCheckCmd_def
\\ fs[] \\ Cases_on `tMap (toRExp e)` \\ Cases_on `tMap (Var n)`
\\ fs[] \\ rveq \\ fs[]
\\ rpt conj_tac
>- (strip_tac \\ fs[updFlEnv_def, updEnv_def, toREnv_def]
\\ IF_CASES_TAC \\ fs[])
>- (drule approxUpdBound
\\ disch_then
(qspecl_then
[`M64`, `v'`, `float_to_real (fp64_to_float v_e)`, `n`]
irule)
\\ fs[domain_lookup, lookup_NONE_domain]
\\ `A (Var n) = A (toRExp e)` by (fs[])
\\ qpat_x_assum `A (Var n) = A (toRExp e)`
(fn thm => fs[thm]))
>- (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[])
>- (irule swap_Gamma_bstep
\\ qexists_tac `updDefVars n M0 (toRMap Gamma)` \\ fs[]
\\ MATCH_ACCEPT_TAC Rmap_updVars_comm)
>- (irule bstep_eq_env
\\ qexists_tac `updEnv n (float_to_real (fp64_to_float v_e)) E2_real`
\\ fs[]
\\ strip_tac \\ fs[updEnv_def, toREnv_def, updFlEnv_def]
\\ IF_CASES_TAC \\ fs[])