Commit dac0edc4 authored by Heiko Becker's avatar Heiko Becker
Browse files

Some cleanup and progress on Error Validator soundness

parent 9325d322
......@@ -6,12 +6,13 @@
encoded in the analysis result. The validator is used in the file
CertificateChecker.v to build the complete checker.
**)
open simpLib realTheory realLib RealArith pred_setTheory
open AbbrevsTheory ExpressionsTheory RealSimpsTheory FloverTactics
MachineTypeTheory ExpressionAbbrevsTheory ErrorBoundsTheory
IntervalArithTheory TypingTheory IntervalValidationTheory
EnvironmentsTheory CommandsTheory ssaPrgsTheory FloverMapTheory;
open preamble
open simpLib realTheory realLib RealArith pred_setTheory;
open AbbrevsTheory ExpressionsTheory ExpressionSemanticsTheory RealSimpsTheory
RealRangeArithTheory FloverTactics MachineTypeTheory
ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
TypeValidatorTheory IntervalValidationTheory EnvironmentsTheory
CommandsTheory ssaPrgsTheory FloverMapTheory;
open preamble;
val _ = new_theory "ErrorValidation";
......@@ -19,7 +20,7 @@ val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
val _ = temp_overload_on("abs",``real$abs``);
val validErrorbound_def = Define `
validErrorbound e (typeMap: (real expr # mType) binTree) (A:analysisResult) (dVars:num_set)=
validErrorbound e (typeMap: typeMap) (A:analysisResult) (dVars:num_set)=
case FloverMapTree_find e A, FloverMapTree_find e typeMap of
| NONE, _ => F
| _, NONE => F
......@@ -122,9 +123,19 @@ val validErrorboundCmd_def = Define `
add_unevaluated_function ``validErrorboundCmd``;
val eval_Real_def = Define `
eval_Real E1 Gamma e nR =
eval_expr E1 (toRTMap (toRExpMap Gamma)) (toREval e) nR REAL`;
val eval_Fin_def = Define `
eval_Fin E2 Gamma e nF m =
eval_expr E2 (toRExpMap Gamma) e nF m`;
val _ = export_rewrites ["eval_Real_def", "eval_Fin_def"]
val err_always_positive = store_thm (
"err_always_positive",
``!(e:real expr) (A:analysisResult) (iv:interval) (err:real) dVars tmap.
``! (e:real expr) (A:analysisResult) (iv:interval) (err:real) dVars tmap.
(validErrorbound e tmap A dVars) /\
(FloverMapTree_find e A = SOME (iv,err)) ==>
0 <= err``,
......@@ -133,56 +144,46 @@ val err_always_positive = store_thm (
val validErrorboundCorrectVariable_eval = store_thm (
"validErrorboundCorrectVariable_eval",
``!E1 E2 A v e nR nlo nhi P fVars dVars Gamma exprTypes fBits.
eval_expr E1 (toRMap Gamma) (toRBMap fBits) (toREval (Var v)) nR REAL /\
typeCheck (Var v) Gamma exprTypes fBits /\
approxEnv E1 Gamma A fVars dVars E2 /\
validIntervalbounds (Var v) A P dVars /\
validErrorbound (Var v) exprTypes A dVars /\
``! E1 E2 A v e nR nlo nhi P fVars dVars Gamma.
eval_Real E1 Gamma (Var v) nR /\
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 /\
validTypes (Var v) Gamma /\
validRanges (Var v) A E1 (toRTMap (toRExpMap Gamma)) /\
validErrorbound (Var v) Gamma A dVars /\
(domain (usedVars ((Var v):real expr)) DIFF (domain dVars)) SUBSET (domain fVars) /\
dVars_range_valid dVars E1 A /\
fVars_P_sound fVars E1 P /\
vars_typed ((domain fVars) UNION (domain dVars)) Gamma /\
FloverMapTree_find (Var v) A = SOME ((nlo,nhi),e) ==>
? nF m.
eval_expr E2 Gamma (toRBMap fBits) (Var v) nF m``,
eval_Fin E2 Gamma (Var v) nF m``,
rpt strip_tac
\\ qspecl_then [`Var v`, `A`, `P`, `fVars`, `dVars`, `E1`, `Gamma`, `toRBMap fBits`]
destruct validIntervalbounds_sound
\\ fs[] \\ rveq
\\ `nR = vR` by (metis_tac[meps_0_deterministic]) \\ rveq
\\ IMP_RES_TAC validRanges_single \\ fs[]
\\ IMP_RES_TAC meps_0_deterministic \\ rveq
\\ fs[toREval_def]
\\ inversion `eval_expr E1 _ _ _ _ _` eval_expr_cases
\\ Flover_compute ``validErrorbound``
\\ qspecl_then [`E1`, `E2`, `v`, `nR`, `fVars`, `dVars`, `A`, `Gamma`] destruct approxEnv_gives_value
\\ inversion `eval_expr E1 _ _ _ _` eval_expr_cases
\\ rveq
\\ qspecl_then [`E1`, `E2`, `v`, `nR`, `fVars`, `dVars`, `A`, `toRExpMap Gamma`]
destruct approxEnv_gives_value
\\ fs[domain_union, domain_lookup, usedVars_def]
\\ `?m. Gamma v = SOME m` by (Cases_on `Gamma v` \\ fs [toRMap_def])
\\ qexistsl_tac [`v2`, `m`] \\ fs[eval_expr_cases]);
>- (Cases_on `lookup v dVars` \\ fs[domain_lookup])
\\ fs[eval_expr_cases, toRExpMap_def, toRTMap_def, option_case_eq]);
val validErrorboundCorrectVariable = store_thm (
"validErrorboundCorrectVariable",
``!(E1 E2:env) A fVars dVars (v:num) (nR nF err nlo nhi:real) (P:precond) m
exprTypes Gamma fBits.
eval_expr E1 (toRMap Gamma) (toRBMap fBits) (toREval (Var v)) nR REAL /\
eval_expr E2 Gamma (toRBMap fBits) (Var v) nF m /\
typeCheck (Var v) Gamma exprTypes fBits /\
approxEnv E1 Gamma A fVars dVars E2 /\
validIntervalbounds (Var v) A P dVars /\
validErrorbound (Var v) exprTypes A dVars /\
``! (E1 E2:env) A fVars dVars (v:num) (nR nF err nlo nhi:real) (P:precond) m
Gamma.
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 /\
eval_Real E1 Gamma (Var v) nR /\
eval_Fin E2 Gamma (Var v) nF m /\
validTypes (Var v) Gamma /\
validRanges (Var v) A E1 (toRTMap (toRExpMap Gamma)) /\
validErrorbound (Var v) Gamma A dVars /\
(domain (usedVars ((Var v):real expr)) DIFF (domain dVars)) SUBSET (domain fVars) /\
dVars_range_valid dVars E1 A /\
fVars_P_sound fVars E1 P /\
vars_typed ((domain fVars) UNION (domain dVars)) Gamma /\
FloverMapTree_find (Var v) A = SOME ((nlo,nhi),err) ==>
abs (nR - nF) <= err``,
rpt strip_tac
\\ drule validIntervalbounds_sound \\ rpt (disch_then drule)
\\ disch_then (qspec_then `toRBMap fBits` assume_tac)
\\ fs[] \\ rveq
\\ `vR = nR` by (metis_tac[meps_0_deterministic]) \\ rveq
\\ IMP_RES_TAC validRanges_single \\ fs[]
\\ IMP_RES_TAC meps_0_deterministic \\ rveq
\\ fs[toREval_def]
\\ rpt (inversion `eval_expr _ _ _ _ _ _` eval_expr_cases)
\\ Flover_compute ``typeCheck``
\\ rpt (inversion `eval_expr _ _ _ _ _` eval_expr_cases)
\\ Flover_compute ``validErrorbound`` \\ rveq \\ fs[]
>- (drule approxEnv_dVar_bounded
\\ rpt (disch_then drule)
......@@ -194,19 +195,19 @@ val validErrorboundCorrectVariable = store_thm (
\\ rpt (disch_then drule)
\\ disch_then (qspec_then `m` assume_tac)
\\ irule REAL_LE_TRANS
\\ res_tac
\\ qexists_tac `computeError nR m`
\\ conj_tac \\ TRY (first_x_assum irule \\ fs[domain_lookup])
\\ fs[toRExpMap_def] \\ rveq
\\ irule computeError_up
\\ irule contained_leq_maxAbs \\ fs[contained_def, IVlo_def, IVhi_def]);
val validErrorboundCorrectConstant_eval = store_thm (
"validErrorboundCorrectConstant_eval",
``!(E1 E2:env) (n nR:real) m Gamma fBits.
eval_expr E1 (toRMap Gamma) fBits (toREval (Const m n)) nR REAL ==>
?nF m1.
eval_expr E2 Gamma fBits (Const m n) nF m1``,
rpt strip_tac
``!(E:env) (n nR:real) m Gamma.
validTypes (Const m n) Gamma ==>
? nF m1.
eval_Fin E Gamma (Const m n) nF m1``,
rpt strip_tac \\ fs[validTypes_def]
\\ qexistsl_tac [`perturb n m (mTypeToR m)`,`m`] \\ irule Const_dist'
\\ fs[]
\\ qexists_tac `mTypeToR m`
......@@ -215,30 +216,28 @@ val validErrorboundCorrectConstant_eval = store_thm (
val validErrorboundCorrectConstant = store_thm (
"validErrorboundCorrectConstant",
``!(E1 E2:env) (A:analysisResult) (n nR nF e nlo nhi:real) dVars m exprTypes
Gamma fBits.
eval_expr E1 (toRMap Gamma) (toRBMap fBits) (toREval (Const m n)) nR REAL /\
eval_expr E2 Gamma (toRBMap fBits) (Const m n) nF m /\
typeCheck (Const m n) Gamma exprTypes fBits /\
validErrorbound (Const m n) exprTypes A dVars /\
``!(E1 E2:env) (A:analysisResult) (n nR nF e nlo nhi:real) dVars m Gamma.
eval_Real E1 Gamma (Const m n) nR /\
eval_Fin E2 Gamma (Const m n) nF m /\
validTypes (Const m n) Gamma /\
validErrorbound (Const m n) Gamma A dVars /\
(nlo <= nR /\ nR <= nhi) /\
FloverMapTree_find (Const m n) A = SOME ((nlo,nhi),e) ==>
(abs (nR - nF)) <= e``,
rpt strip_tac \\ fs[toREval_def]
\\ Flover_compute ``validErrorbound``
\\ Flover_compute ``typeCheck`` \\ rveq \\ fs[]
\\ rveq \\ fs[validTypes_def] \\ rveq
\\ irule REAL_LE_TRANS
\\ find_exists_tac \\ fs[]
\\ irule REAL_LE_TRANS
\\ qexists_tac `computeError nR m`
\\ inversion `eval_expr _ _ _ _ _ REAL` eval_expr_cases
\\ inversion `eval_expr _ _ _ _ REAL` eval_expr_cases
\\ `nR = n` by (rveq \\ irule delta_REAL_deterministic \\ fs[])
\\ rveq
\\ conj_tac
\\ rveq \\ conj_tac
>- (irule const_abs_err_bounded
\\ qexistsl_tac [`E1`, `E2`, `Gamma`, `toRBMap fBits`]
\\ qexistsl_tac [`E1`, `E2`, `toRExpMap Gamma`]
\\ inversion `eval_expr _ _ _ _ m` eval_expr_cases \\ rveq
\\ conj_tac \\ irule Const_dist' \\ fs[]
\\ inversion `eval_expr _ _ _ _ _ m` eval_expr_cases
\\ find_exists_tac \\ fs[])
\\ irule computeError_up
\\ fs[maxAbs_def] \\ irule maxAbs \\ fs[]);
......@@ -247,62 +246,36 @@ val validErrorboundCorrectAddition = store_thm (
"validErrorboundCorrectAddition",
``!(E1 E2:env) (A:analysisResult) (e1:real expr) (e2:real expr)
(nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real)
(alo ahi e1lo e1hi e2lo e2hi :real) dVars m m1 m2 exprTypes Gamma fBits fBit.
(isFixedPoint m1 /\ isFixedPoint m2 ==>
FloverMapTree_find (Binop Plus e1 e2) fBits = SOME fBit) /\
(SOME m = join m1 m2 fBit) /\
eval_expr E1 (toRMap Gamma) (toRBMap fBits) (toREval e1) nR1 REAL /\
eval_expr E1 (toRMap Gamma) (toRBMap fBits) (toREval e2) nR2 REAL /\
eval_expr E1 (toRMap Gamma) (toRBMap fBits) (toREval (Binop Plus e1 e2)) nR REAL /\
eval_expr E2 Gamma (toRBMap fBits) e1 nF1 m1 /\
eval_expr E2 Gamma (toRBMap fBits) e2 nF2 m2 /\
(alo ahi e1lo e1hi e2lo e2hi :real) dVars m m1 m2 Gamma.
eval_Real E1 Gamma e1 nR1 /\
eval_Real E1 Gamma e2 nR2 /\
eval_Real E1 Gamma (Binop Plus e1 e2) nR /\
eval_Fin E2 Gamma e1 nF1 m1 /\
eval_Fin E2 Gamma e2 nF2 m2 /\
eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 Gamma))
(\e. if e = Binop Plus (Var 1) (Var 2)
then toRBMap fBits (Binop Plus e1 e2)
else toRBMap fBits e)
(updDefVars (Binop Plus (Var 1) (Var 2)) m
(updDefVars (Var 2) m2 (updDefVars (Var 1) m1 (toRExpMap Gamma))))
(Binop Plus (Var 1) (Var 2)) nF m /\
typeCheck (Binop Plus e1 e2) Gamma exprTypes fBits /\
validErrorbound (Binop Plus e1 e2) exprTypes A dVars /\
validErrorbound (Binop Plus e1 e2) Gamma A dVars /\
(e1lo <= nR1 /\ nR1 <= e1hi) /\
(e2lo <= nR2 /\ nR2 <= e2hi) /\
FloverMapTree_find e1 A = SOME ((e1lo, e1hi), err1) /\
FloverMapTree_find e2 A = SOME ((e2lo, e2hi), err2) /\
FloverMapTree_find (Binop Plus e1 e2) A = SOME ((alo, ahi), e) /\
FloverMapTree_find (Binop Plus e1 e2) Gamma = SOME m /\
abs (nR1 - nF1) <= err1 /\
abs (nR2 - nF2) <= err2 ==>
abs (nR - nF) <= e``,
rpt strip_tac \\ simp[Once toREval_def]
\\ `FloverMapTree_find e1 exprTypes = SOME m1`
by (irule typingSoundnessExp
\\ qexistsl_tac [`E2`, `Gamma`, `fBits`, `nF1`]
\\ Flover_compute ``typeCheck`` \\ fs[])
\\ `FloverMapTree_find e2 exprTypes = SOME m2`
by (irule typingSoundnessExp
\\ qexistsl_tac [`E2`, `Gamma`, `fBits`, `nF2`]
\\ Flover_compute ``typeCheck`` \\ fs[])
\\ `FloverMapTree_find (Binop Plus e1 e2) exprTypes = SOME m`
by (irule typingSoundnessExp
\\ qexistsl_tac [`E2`, `Gamma`, `fBits`, `nF`]
\\ fs[]
\\ inversion `eval_expr _ _ _ (Binop Plus (Var 1) (Var 2)) _ _` eval_expr_cases
\\ rveq
\\ irule Binop_dist'
\\ qexists_tac `delta`
\\ find_exists_tac \\ fs[]
\\ qexistsl_tac [`v1`, `v2`] \\ fs[]
\\ rpt (inversion `eval_expr _ _ _ (Var _) _ _` eval_expr_cases)
\\ fs[updDefVars_def]
\\ rveq \\ fs[toRBMap_def])
\\ Flover_compute ``validErrorbound`` \\ rveq
\\ fs [] \\ rveq
\\ fs[toRExpMap_def]
\\ irule REAL_LE_TRANS
\\ qexists_tac `err1 + err2 + (computeError (nF1 + nF2) m)`
\\ conj_tac
>- (irule add_abs_err_bounded
\\ rpt (find_exists_tac \\ fs[]))
\\ irule REAL_LE_TRANS \\ find_exists_tac
\\ conj_tac \\ fs[join_def]
\\ conj_tac \\ fs[]
\\ qmatch_abbrev_tac `_ <= computeError (maxAbs iv) _`
\\ PairCases_on `iv` \\ irule computeError_up
\\ unabbrev_all_tac \\ fs[maxAbs_def]
......@@ -310,73 +283,46 @@ val validErrorboundCorrectAddition = store_thm (
\\ `contained nF1 (widenInterval (e1lo,e1hi) err1)`
by (match_mp_tac distance_gives_iv
\\ qexists_tac `nR1` \\ conj_tac
\\ simp[contained_def, IVlo_def, IVhi_def])
\\ simp[contained_def])
\\ `contained nF2 (widenInterval (e2lo,e2hi) err2)`
by (match_mp_tac distance_gives_iv
\\ qexists_tac `nR2` \\ conj_tac
\\ simp[contained_def, IVlo_def, IVhi_def])
\\ irule (REWRITE_RULE [validIntervalAdd_def, contained_def, IVlo_def, IVhi_def] interval_addition_valid)
\\ fs[contained_def, IVlo_def, IVhi_def]);
\\ simp[contained_def])
\\ assume_tac (REWRITE_RULE [validIntervalAdd_def, contained_def] interval_addition_valid)
\\ fs[contained_def]);
val validErrorboundCorrectSubtraction = store_thm ("validErrorboundCorrectSubtraction",
``!(E1 E2:env) (A:analysisResult) (e1:real expr) (e2:real expr)
(nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real)
(alo ahi e1lo e1hi e2lo e2hi:real) dVars m m1 m2 exprTypes Gamma fBits fBit.
(isFixedPoint m1 /\ isFixedPoint m2 ==>
FloverMapTree_find (Binop Sub e1 e2) fBits = SOME fBit) /\
(SOME m = join m1 m2 fBit) /\
eval_expr E1 (toRMap Gamma) (toRBMap fBits) (toREval e1) nR1 REAL /\
eval_expr E1 (toRMap Gamma) (toRBMap fBits) (toREval e2) nR2 REAL /\
eval_expr E1 (toRMap Gamma) (toRBMap fBits) (toREval (Binop Sub e1 e2)) nR REAL /\
eval_expr E2 Gamma (toRBMap fBits) e1 nF1 m1 /\
eval_expr E2 Gamma (toRBMap fBits) e2 nF2 m2 /\
(alo ahi e1lo e1hi e2lo e2hi:real) dVars m m1 m2 Gamma.
eval_Real E1 Gamma e1 nR1 /\
eval_Real E1 Gamma e2 nR2 /\
eval_Real E1 Gamma (Binop Sub e1 e2) nR /\
eval_Fin E2 Gamma e1 nF1 m1 /\
eval_Fin E2 Gamma e2 nF2 m2 /\
eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 Gamma))
(\e. if e = Binop Sub (Var 1) (Var 2)
then toRBMap fBits (Binop Sub e1 e2)
else toRBMap fBits e)
(updDefVars (Binop Sub (Var 1) (Var 2)) m
(updDefVars (Var 2) m2 (updDefVars (Var 1) m1 (toRExpMap Gamma))))
(Binop Sub (Var 1) (Var 2)) nF m /\
typeCheck (Binop Sub e1 e2) Gamma exprTypes fBits /\
validErrorbound (Binop Sub e1 e2) exprTypes A dVars /\
validErrorbound (Binop Sub e1 e2) Gamma A dVars /\
(e1lo <= nR1 /\ nR1 <= e1hi) /\
(e2lo <= nR2 /\ nR2 <= e2hi) /\
FloverMapTree_find e1 A = SOME ((e1lo, e1hi), err1) /\
FloverMapTree_find e2 A = SOME ((e2lo, e2hi), err2) /\
FloverMapTree_find (Binop Sub e1 e2) A = SOME ((alo, ahi), e) /\
FloverMapTree_find (Binop Sub e1 e2) Gamma = SOME m /\
abs (nR1 - nF1) <= err1 /\
abs (nR2 - nF2) <= err2 ==>
abs (nR - nF) <= e``,
rpt strip_tac \\ simp[Once toREval_def]
\\ `FloverMapTree_find e1 exprTypes = SOME m1`
by (irule typingSoundnessExp
\\ qexistsl_tac [`E2`, `Gamma`, `fBits`, `nF1`]
\\ Flover_compute ``typeCheck`` \\ fs[])
\\ `FloverMapTree_find e2 exprTypes = SOME m2`
by (irule typingSoundnessExp
\\ qexistsl_tac [`E2`, `Gamma`, `fBits`, `nF2`]
\\ Flover_compute ``typeCheck`` \\ fs[])
\\ `FloverMapTree_find (Binop Sub e1 e2) exprTypes = SOME m`
by (irule typingSoundnessExp
\\ qexistsl_tac [`E2`, `Gamma`, `fBits`, `nF`]
\\ fs[]
\\ inversion `eval_expr _ _ _ (Binop Sub (Var 1) (Var 2)) _ _` eval_expr_cases
\\ rveq
\\ irule Binop_dist'
\\ qexists_tac `delta`
\\ find_exists_tac \\ fs[]
\\ qexistsl_tac [`v1`, `v2`] \\ fs[]
\\ rpt (inversion `eval_expr _ _ _ (Var _) _ _` eval_expr_cases)
\\ fs[updDefVars_def]
\\ rveq \\ fs[toRBMap_def])
\\ Flover_compute ``validErrorbound`` \\ rveq
\\ fs [] \\ rveq
\\ irule REAL_LE_TRANS
\\ qexists_tac `err1 + err2 + computeError (nF1 - nF2) m`
\\ conj_tac
>- (irule subtract_abs_err_bounded
\\ rpt (find_exists_tac \\ fs[]))
\\ irule REAL_LE_TRANS \\ find_exists_tac
\\ conj_tac \\ fs[join_def]
\\ conj_tac \\ fs[]
\\ qmatch_abbrev_tac `_ <= computeError (maxAbs iv) _`
\\ PairCases_on `iv` \\ irule computeError_up
\\ unabbrev_all_tac \\ fs[maxAbs_def]
......@@ -384,13 +330,13 @@ val validErrorboundCorrectSubtraction = store_thm ("validErrorboundCorrectSubtra
\\ `contained nF1 (widenInterval (e1lo,e1hi) err1)`
by (match_mp_tac distance_gives_iv
\\ qexists_tac `nR1` \\ conj_tac
\\ simp[contained_def, IVlo_def, IVhi_def])
\\ simp[contained_def])
\\ `contained nF2 (widenInterval (e2lo,e2hi) err2)`
by (match_mp_tac distance_gives_iv
\\ qexists_tac `nR2` \\ conj_tac
\\ simp[contained_def, IVlo_def, IVhi_def])
\\ irule (REWRITE_RULE [validIntervalSub_def, contained_def, IVlo_def, IVhi_def] interval_subtraction_valid)
\\ fs[contained_def, IVlo_def, IVhi_def]);
\\ simp[contained_def])
\\ assume_tac (REWRITE_RULE [validIntervalSub_def, contained_def] interval_subtraction_valid)
\\ fs[contained_def]);
val multiplicationErroBounded = store_thm ("multiplicationErrorBounded",
``!(nR1 nR2 nF1 nF2: real) (err1 err2: real) (e1lo e1hi e2lo e2hi: real).
......@@ -986,58 +932,31 @@ val multiplicationErroBounded = store_thm ("multiplicationErrorBounded",
val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
``!(E1 E2:env) (A:analysisResult) (e1:real expr) (e2:real expr)
(nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real)
(alo ahi e1lo e1hi e2lo e2hi :real) dVars m m1 m2 exprTypes Gamma fBits fBit.
(isFixedPoint m1 /\ isFixedPoint m2 ==>
FloverMapTree_find (Binop Mult e1 e2) fBits = SOME fBit) /\
(SOME m = join m1 m2 fBit) /\
eval_expr E1 (toRMap Gamma) (toRBMap fBits) (toREval e1) nR1 REAL /\
eval_expr E1 (toRMap Gamma) (toRBMap fBits) (toREval e2) nR2 REAL /\
eval_expr E1 (toRMap Gamma) (toRBMap fBits) (toREval (Binop Mult e1 e2)) nR REAL /\
eval_expr E2 Gamma (toRBMap fBits) e1 nF1 m1 /\
eval_expr E2 Gamma (toRBMap fBits) e2 nF2 m2 /\
(alo ahi e1lo e1hi e2lo e2hi :real) dVars m m1 m2 Gamma.
eval_Real E1 Gamma e1 nR1 /\
eval_Real E1 Gamma e2 nR2 /\
eval_Real E1 Gamma (Binop Mult e1 e2) nR /\
eval_Fin E2 Gamma e1 nF1 m1 /\
eval_Fin E2 Gamma e2 nF2 m2 /\
eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 Gamma))
(\e. if e = Binop Mult (Var 1) (Var 2)
then toRBMap fBits (Binop Mult e1 e2)
else toRBMap fBits e)
(updDefVars (Binop Mult (Var 1) (Var 2)) m
(updDefVars (Var 2) m2 (updDefVars (Var 1) m1 (toRExpMap Gamma))))
(Binop Mult (Var 1) (Var 2)) nF m /\
typeCheck (Binop Mult e1 e2) Gamma exprTypes fBits /\
validErrorbound (Binop Mult e1 e2) exprTypes A dVars /\
validErrorbound (Binop Mult e1 e2) Gamma A dVars /\
(e1lo <= nR1 /\ nR1 <= e1hi) /\
(e2lo <= nR2 /\ nR2 <= e2hi) /\
FloverMapTree_find e1 A = SOME ((e1lo, e1hi), err1) /\
FloverMapTree_find e2 A = SOME ((e2lo, e2hi), err2) /\
FloverMapTree_find (Binop Mult e1 e2) A = SOME ((alo, ahi), e) /\
FloverMapTree_find (Binop Mult e1 e2) Gamma = SOME m /\
abs (nR1 - nF1) <= err1 /\
abs (nR2 - nF2) <= err2 ==>
abs (nR - nF) <= e``,
rpt strip_tac \\ simp[Once toREval_def]
\\ `FloverMapTree_find e1 exprTypes = SOME m1`
by (irule typingSoundnessExp
\\ qexistsl_tac [`E2`, `Gamma`, `fBits`, `nF1`]
\\ Flover_compute ``typeCheck`` \\ fs[])
\\ `FloverMapTree_find e2 exprTypes = SOME m2`
by (irule typingSoundnessExp
\\ qexistsl_tac [`E2`, `Gamma`, `fBits`, `nF2`]
\\ Flover_compute ``typeCheck`` \\ fs[])
\\ `FloverMapTree_find (Binop Mult e1 e2) exprTypes = SOME m`
by (irule typingSoundnessExp
\\ qexistsl_tac [`E2`, `Gamma`, `fBits`, `nF`]
\\ fs[]
\\ inversion `eval_expr _ _ _ (Binop Mult (Var 1) (Var 2)) _ _` eval_expr_cases
\\ rveq
\\ irule Binop_dist'
\\ qexists_tac `delta`
\\ find_exists_tac \\ fs[]
\\ qexistsl_tac [`v1`, `v2`] \\ fs[]
\\ rpt (inversion `eval_expr _ _ _ (Var _) _ _` eval_expr_cases)
\\ fs[updDefVars_def]
\\ rveq \\ fs[toRBMap_def])
\\ Flover_compute ``validErrorbound`` \\ rveq
\\ fs [] \\ rveq
\\ `0 <= err1`
by (irule err_always_positive
\\ qexistsl_tac [`A`, `dVars`, `e1`, `(e1lo,e1hi)`, `exprTypes`]
\\ qexistsl_tac [`A`, `dVars`, `e1`, `(e1lo,e1hi)`, `Gamma`]
\\ fs[])
\\ `0 <= err2`
by (drule err_always_positive
......@@ -1049,7 +968,7 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
>- (irule mult_abs_err_bounded \\ rpt conj_tac
\\ rpt (find_exists_tac \\ fs[]))
\\ irule REAL_LE_TRANS \\ find_exists_tac
\\ conj_tac \\ fs[join_def]
\\ conj_tac \\ fs[]
\\ irule REAL_LE_ADD2 \\ conj_tac
>- (irule multiplicationErroBounded \\ fs[])
\\ qmatch_abbrev_tac `_ <= computeError (maxAbs iv) _`
......@@ -1059,13 +978,13 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
\\ `contained nF1 (widenInterval (e1lo,e1hi) err1)`
by (match_mp_tac distance_gives_iv
\\ qexists_tac `nR1` \\ conj_tac
\\ simp[contained_def, IVlo_def, IVhi_def])
\\ simp[contained_def])
\\ `contained nF2 (widenInterval (e2lo,e2hi) err2)`
by (match_mp_tac distance_gives_iv
\\ qexists_tac `nR2` \\ conj_tac
\\ simp[contained_def, IVlo_def, IVhi_def])
\\ irule (REWRITE_RULE [contained_def, IVlo_def, IVhi_def] interval_multiplication_valid)
\\ fs[contained_def, IVlo_def, IVhi_def]);
\\ simp[contained_def])
\\ assume_tac (REWRITE_RULE [contained_def] interval_multiplication_valid)
\\ fs[contained_def]);
val divisionErrorBounded = store_thm (
"divisionErrorBounded",
......@@ -2125,59 +2044,32 @@ val divisionErrorBounded = store_thm (
val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
``!(E1 E2:env) (A:analysisResult) (e1:real expr) (e2:real expr)
(nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real)
(alo ahi e1lo e1hi e2lo e2hi :real) dVars m m1 m2 exprTypes Gamma fBits fBit.
(isFixedPoint m1 /\ isFixedPoint m2 ==>
FloverMapTree_find (Binop Div e1 e2) fBits = SOME fBit) /\
(SOME m = join m1 m2 fBit) /\
eval_expr E1 (toRMap Gamma) (toRBMap fBits) (toREval e1) nR1 REAL /\
eval_expr E1 (toRMap Gamma) (toRBMap fBits) (toREval e2) nR2 REAL /\
eval_expr E1 (toRMap Gamma) (toRBMap fBits) (toREval (Binop Div e1 e2)) nR REAL /\
eval_expr E2 Gamma (toRBMap fBits) e1 nF1 m1 /\
eval_expr E2 Gamma (toRBMap fBits) e2 nF2 m2 /\
(alo ahi e1lo e1hi e2lo e2hi :real) dVars m m1 m2 Gamma.
eval_Real E1 Gamma e1 nR1 /\
eval_Real E1 Gamma e2 nR2 /\
eval_Real E1 Gamma (Binop Div e1 e2) nR /\
eval_Fin E2 Gamma e1 nF1 m1 /\
eval_Fin E2 Gamma e2 nF2 m2 /\
eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 Gamma))
(\e. if e = Binop Div (Var 1) (Var 2)
then toRBMap fBits (Binop Div e1 e2)
else toRBMap fBits e)
(updDefVars (Binop Div (Var 1) (Var 2)) m
(updDefVars (Var 2) m2 (updDefVars (Var 1) m1 (toRExpMap Gamma))))
(Binop Div (Var 1) (Var 2)) nF m /\
typeCheck (Binop Div e1 e2) Gamma exprTypes fBits /\
validErrorbound (Binop Div e1 e2) exprTypes A dVars /\
noDivzero e2hi e2lo /\
validErrorbound (Binop Div e1 e2) Gamma A dVars /\
(e1lo <= nR1 /\ nR1 <= e1hi) /\
(e2lo <= nR2 /\ nR2 <= e2hi) /\
noDivzero e2hi e2lo /\
FloverMapTree_find e1 A = SOME ((e1lo, e1hi), err1) /\
FloverMapTree_find e2 A = SOME ((e2lo, e2hi), err2) /\
FloverMapTree_find (Binop Div e1 e2) A = SOME ((alo, ahi), e) /\
FloverMapTree_find (Binop Div e1 e2) Gamma = SOME m /\
abs (nR1 - nF1) <= err1 /\
abs (nR2 - nF2) <= err2 ==>
abs (nR - nF) <= e``,
rpt strip_tac \\ simp[Once toREval_def]
\\ `FloverMapTree_find e1 exprTypes = SOME m1`
by (irule typingSoundnessExp
\\ qexistsl_tac [`E2`, `Gamma`, `fBits`, `nF1`]
\\ Flover_compute ``typeCheck`` \\ fs[])
\\ `FloverMapTree_find e2 exprTypes = SOME m2`
by (irule typingSoundnessExp
\\ qexistsl_tac [`E2`, `Gamma`, `fBits`, `nF2`]
\\ Flover_compute ``typeCheck`` \\ fs[])
\\ `FloverMapTree_find (Binop Div e1 e2) exprTypes = SOME m`
by (irule typingSoundnessExp
\\ qexistsl_tac [`E2`, `Gamma`, `fBits`, `nF`]
\\ fs[]
\\ inversion `eval_expr _ _ _ (Binop Div (Var 1) (Var 2)) _ _` eval_expr_cases
\\ rveq
\\ irule Binop_dist'
\\ qexists_tac `delta`
\\ find_exists_tac \\ fs[]
\\ qexistsl_tac [`v1`, `v2`] \\ fs[]
\\ rpt (inversion `eval_expr _ _ _ (Var _) _ _` eval_expr_cases)
\\ fs[updDefVars_def]
\\ rveq \\ fs[toRBMap_def])
\\ Flover_compute ``validErrorbound`` \\ rveq
\\ fs [] \\ rveq
\\ `0 <= err1`
by (irule err_always_positive
\\ qexistsl_tac [`A`, `dVars`, `e1`, `(e1lo,e1hi)`, `exprTypes`]
\\ qexistsl_tac [`A`, `dVars`, `e1`, `(e1lo,e1hi)`, `Gamma`]
\\ fs[])
\\ `0 <= err2`
by (drule err_always_positive
......@@ -2189,87 +2081,57 @@ val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
>- (irule div_abs_err_bounded \\ rpt conj_tac
\\ rpt (find_exists_tac \\ fs[]))
\\ irule REAL_LE_TRANS \\ find_exists_tac
\\ conj_tac \\ fs[join_def]
\\ conj_tac \\ fs[]
\\ `contained nF1 (widenInterval (e1lo,e1hi) err1)`
by (match_mp_tac distance_gives_iv
\\ qexists_tac `nR1` \\ conj_tac
\\ simp[contained_def, IVlo_def, IVhi_def])
\\ simp[contained_def])
\\ `contained nF2 (widenInterval (e2lo,e2hi) err2)`
by (match_mp_tac distance_gives_iv
\\ qexists_tac `nR2` \\ conj_tac
\\ simp[contained_def, IVlo_def, IVhi_def])
\\ simp[contained_def])
\\ irule REAL_LE_ADD2 \\ conj_tac
>- (irule divisionErrorBounded \\ fs[])
\\ qmatch_abbrev_tac `_ <= computeError (maxAbs iv) _`
\\ PairCases_on `iv` \\ irule computeError_up
\\ unabbrev_all_tac \\ fs[maxAbs_def]
\\ match_mp_tac maxAbs
\\ irule (REWRITE_RULE [contained_def,