Commit 58bb46dc authored by Heiko Becker's avatar Heiko Becker

Port FPRangeValidator

parent a5076909
......@@ -8,11 +8,13 @@
value according to IEEE 754.
**)
open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory
open AbbrevsTheory MachineTypeTheory TypingTheory RealSimpsTheory IntervalArithTheory
ExpressionsTheory FloverTactics IntervalValidationTheory ErrorValidationTheory
CommandsTheory EnvironmentsTheory ssaPrgsTheory
open preamble
open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory;
open AbbrevsTheory MachineTypeTheory TypeValidatorTheory RealSimpsTheory
RealRangeArithTheory IntervalArithTheory ExpressionsTheory
ExpressionAbbrevsTheory ExpressionSemanticsTheory FloverTactics
IntervalValidationTheory ErrorValidationTheory CommandsTheory
EnvironmentsTheory ssaPrgsTheory;
open preamble;
val _ = new_theory "FPRangeValidator";
......@@ -128,74 +130,57 @@ val solve_tac =
val FPRangeValidator_sound = store_thm (
"FPRangeValidator_sound",
``!e E1 E2 Gamma v m A tMap P fVars (dVars:num_set) fBits.
approxEnv E1 Gamma A fVars dVars E2 /\
eval_expr E2 Gamma (toRBMap fBits) e v m /\
typeCheck e Gamma tMap fBits /\
validIntervalbounds e A P dVars /\
validErrorbound e tMap A dVars /\
FPRangeValidator e A tMap dVars /\
``!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) /\
dVars_range_valid dVars E1 A /\
fVars_P_sound fVars E1 P /\
vars_typed ((domain fVars) UNION (domain dVars)) Gamma /\
(!(v:num). v IN domain dVars ==>
(?vF m. E2 v = SOME vF /\ FloverMapTree_find (Var v) tMap = SOME m
(?vF m. E2 v = SOME vF /\ FloverMapTree_find (Var v) Gamma = SOME m
/\ validFloatValue vF m)) ==>
validFloatValue v m``,
once_rewrite_tac [FPRangeValidator_def] \\ rewrite_tac [GSYM normalOrZero_def]
\\ rpt strip_tac
\\`FloverMapTree_find e tMap = SOME m`
by (drule typingSoundnessExp
\\ disch_then drule \\ fs[])
rpt strip_tac
\\ IMP_RES_TAC validTypes_single
\\ `m = mG`
by (first_x_assum irule
\\ qexistsl_tac [`E2`, `Gamma`, `v`] \\ fs[])
\\ rveq
\\ once_rewrite_tac [validFloatValue_def]
\\ `?iv err vR. FloverMapTree_find e A = SOME (iv, err) /\
eval_expr E1 (toRMap Gamma) (toRBMap fBits) (toREval e) vR REAL /\
FST iv <= vR /\ vR <= SND iv`
by (drule validIntervalbounds_sound
\\ disch_then (qspecl_then [`fVars`, `E1`, `Gamma`, `toRBMap fBits`] impl_subgoal_tac)
\\ fs[] \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
\\ qexists_tac `vR` \\ fs[])
\\ IMP_RES_TAC validRanges_single \\ fs[]
\\ rename1 `FloverMapTree_find e A = SOME (iv_e, err_e)` \\ fs[]
\\ drule validErrorbound_sound
\\ rpt (disch_then drule)
\\ disch_then (qspecl_then [`err_e`, `FST iv_e`, `SND iv_e`] destruct)
\\ disch_then (qspecl_then [`vR`, `err_e`, `FST iv_e`, `SND iv_e`] destruct)
\\ fs[]
\\ qspecl_then [`vR`, `v`, `err_e`, `iv_e`]
impl_subgoal_tac
(SIMP_RULE std_ss [contained_def, widenInterval_def] distance_gives_iv)
\\ fs[IVlo_def, IVhi_def]
\\ fs[]
>- (first_x_assum irule \\ qexists_tac `m` \\ fs[])
\\ Cases_on `e`
>- (fs[]
>- (fs[validFloatValue_def]
\\ first_x_assum (qspecl_then [`n`] impl_subgoal_tac) \\ fs[domain_lookup]
\\ `FloverMapTree_find (Var n) tMap = SOME m`
by (drule typingSoundnessExp \\ rpt (disch_then drule)
\\ fs[])
\\ fs[] \\ rveq
\\ rpt (inversion `eval_expr E2 _ _ _ _ _` eval_expr_cases)
\\ qpat_x_assum `E2 n = SOME v` (fn thm => fs[thm]))
\\ solve_tac)
\\ Cases_on `e` \\ fs[Once FPRangeValidator_def]
>- (fs[validFloatValue_def, domain_lookup] \\ res_tac
\\ fs[] \\ rveq \\ fs[]
\\ rpt (inversion `eval_expr E2 _ _ _ _` eval_expr_cases)
\\ fs[] \\ rveq \\ fs[])
\\ solve_tac);
val FPRangeValidatorCmd_sound = store_thm (
"FPRangeValidatorCmd_sound",
``!f E1 E2 Gamma v vR m A tMap P fVars dVars outVars fBits.
approxEnv E1 Gamma A fVars dVars E2
``!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 (toRMap Gamma) (toRBMap fBits) vR m /\
bstep f E2 Gamma (toRBMap fBits) v m
typeCheckCmd f Gamma tMap fBits
validIntervalboundsCmd f A P dVars
validErrorboundCmd f tMap A dVars
FPRangeValidatorCmd f A tMap dVars
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
dVars_range_valid dVars E1 A /\
fVars_P_sound fVars E1 P /\
vars_typed ((domain fVars) UNION (domain dVars)) Gamma /\
(!(v:num). v IN domain dVars ==>
(?vF m. E2 v = SOME vF /\ FloverMapTree_find (Var v) tMap = SOME m
(?vF m. E2 v = SOME vF /\ FloverMapTree_find (Var v) Gamma = SOME m
/\ validFloatValue vF m)) ==>
validFloatValue v m``,
Induct
......@@ -203,48 +188,44 @@ val FPRangeValidatorCmd_sound = store_thm (
Once freeVars_def]
\\ rpt strip_tac
>- (Flover_compute ``validErrorboundCmd``
\\ Flover_compute ``validIntervalboundsCmd``
\\ Flover_compute ``typeCheckCmd``
\\ rveq \\ fs[]
\\ rpt (inversion `bstep (Let _ _ _ _) _ _ _ _ _` bstep_cases)
\\ rename1 `bstep (toREvalCmd f) (updEnv n vR_e E1) _ _ _ mR`
\\ rename1 `bstep f (updEnv n vF E2) _ _ _ mF`
\\ `FloverMapTree_find e tMap = SOME m`
by (drule typingSoundnessExp
\\ rpt (disch_then drule)
\\ fs[])
\\ 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`, `P`, `FST iv_e`, `SND iv_e`] impl_subgoal_tac)
>- (fs[]
\\ 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)
\\ res_tac)
\\ fs[]
\\ drule validIntervalbounds_sound
\\ rpt (disch_then drule)
\\ disch_then (qspecl_then [`fVars`, `Gamma`, `toRBMap fBits`] impl_subgoal_tac)
>- (fs[]
\\ 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)
\\ res_tac)
\\ fs[] \\ rveq \\ fs[]
\\ `vR_e = vR'` by metis_tac[meps_0_deterministic]
\\ rveq
\\ `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`,
`updDefVars n m Gamma`, `v`, `vR`, `mF`, `A`, `tMap`, `P`,
`fVars`, `insert n () dVars`, `outVars`, `fBits`]
`Gamma`, `v`, `vR`, `mF`, `A`,
`fVars`, `insert n () dVars`, `outVars`]
impl_subgoal_tac)
>- (fs[] \\ rpt conj_tac
>- (irule approxUpdBound \\ 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
......@@ -255,9 +236,15 @@ val FPRangeValidatorCmd_sound = store_thm (
\\ fs[EXTENSION]
\\ rpt strip_tac
\\ metis_tac[])
>- (irule swap_Gamma_bstep
\\ qexists_tac `updDefVars n REAL (toRMap Gamma)` \\ fs[]
\\ fs [updDefVars_def, REWRITE_RULE [updDefVars_def] Rmap_updVars_comm])
>- (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]
......@@ -265,21 +252,9 @@ val FPRangeValidatorCmd_sound = store_thm (
\\ fs[]
\\ rw_thm_asm `x IN domain (freeVars f)` freeVars_def
\\ fs[])
>- (fs [dVars_range_valid_def]
\\ rpt strip_tac \\ simp[updEnv_def]
\\ IF_CASES_TAC \\ fs[]
\\ rveq
\\ fs[domain_union])
>- (fs[fVars_P_sound_def] \\ rpt strip_tac
\\ IF_CASES_TAC \\ fs[]
\\ rveq \\ fs[domain_union])
>- (fs[vars_typed_def] \\ rpt gen_tac \\ disch_then assume_tac
\\ fs[updEnv_def] \\ rveq \\ fs[]
>- (IF_CASES_TAC \\ fs[] \\ rveq \\ fs[domain_union])
\\ TOP_CASE_TAC \\ rveq \\ fs[])
\\ rpt strip_tac
\\ fs[updEnv_def] \\ rveq \\ fs[]
>- (qpat_x_assum `eval_expr E2 Gamma _ e nF _` kall_tac
>- (qpat_x_assum `eval_expr E2 _ e nF _` kall_tac
\\ drule FPRangeValidator_sound
\\ rpt (disch_then drule)
\\ disch_then irule \\ fs[]
......@@ -292,7 +267,7 @@ val FPRangeValidatorCmd_sound = store_thm (
\\ first_x_assum (qspec_then `n` assume_tac)
\\ res_tac)
\\ TOP_CASE_TAC \\ fs[]
\\ qpat_x_assum `eval_expr E2 Gamma _ e nF _` kall_tac
\\ qpat_x_assum `eval_expr E2 _ e nF _` kall_tac
\\ drule FPRangeValidator_sound
\\ rpt (disch_then drule)
\\ disch_then irule \\ fs[]
......@@ -306,12 +281,10 @@ val FPRangeValidatorCmd_sound = store_thm (
\\ res_tac)
\\ fs[])
\\ Flover_compute ``validErrorboundCmd``
\\ Flover_compute ``validIntervalboundsCmd``
\\ Flover_compute ``typeCheckCmd``
\\ rveq \\ fs[]
\\ rpt (inversion `bstep (Ret _) _ _ _ _ _` bstep_cases)
\\ rpt (inversion `bstep (Ret _) _ _ _ _` bstep_cases)
\\ drule FPRangeValidator_sound
\\ rpt (disch_then drule)
\\ fs[]);
\\ fs[Once validTypesCmd_def, Once validRangesCmd_def]);
val _ = export_theory();
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment