Commit 730713b3 authored by Heiko Becker's avatar Heiko Becker

Finish porting of FPRangeValidator and ErrorValidator

parent 0e7eb8d8
......@@ -71,7 +71,6 @@ Ltac prove_fprangeval m v L1 R:=
try auto;
destruct (Rle_lt_dec (Rabs v) (Q2R (maxValue m)))%R; lra.
Theorem FPRangeValidator_sound:
forall (e:exp Q) E1 E2 Gamma v m A tMap P fVars dVars,
approxEnv E1 Gamma A fVars dVars E2 ->
......
This diff is collapsed.
......@@ -22,9 +22,8 @@ val _ = temp_overload_on("abs",``real$abs``);
val FPRangeValidator_def = Define `
FPRangeValidator (e:real exp) A typeMap dVars =
case typeMap e of
| SOME m =>
let (iv_e, err_e) = A e in
case DaisyMapTree_find e A, DaisyMapTree_find e typeMap of
| SOME (iv_e, err_e), SOME m =>
let iv_e_float = widenInterval iv_e err_e in
let recRes =
case e of
......@@ -59,7 +58,7 @@ val FPRangeValidator_def = Define `
then normal_or_zero /\ recRes
else
F)
| NONE => F`;
| _, _ => F`;
val normalOrZero_def = Define `
normalOrZero iv_e_float m =
......@@ -123,13 +122,11 @@ val solve_tac =
\\ Cases_on `denormal v m` \\ TRY (every_case_tac \\ fs[] \\ FAIL_TAC "")
\\ Cases_on `normal v m` \\ TRY (every_case_tac \\ fs[] \\ FAIL_TAC"")
\\ fs[normal_def, denormal_def, validValue_def] \\ rveq \\ fs[]
\\ TRY (RealArith.REAL_ASM_ARITH_TAC)
\\ fs []
\\ every_case_tac \\ fs[]
\\ `abs v <= abs (FST (widenInterval (e_lo, e_hi) err_e)) \/
abs v <= abs (SND (widenInterval (e_lo, e_hi) err_e))`
\\ `abs v <= abs (FST (widenInterval iv_e err_e)) \/
abs v <= abs (SND (widenInterval iv_e err_e))`
by (fs[widenInterval_def, IVlo_def, IVhi_def] \\ RealArith.REAL_ASM_ARITH_TAC)
\\ every_case_tac \\ RealArith.REAL_ASM_ARITH_TAC;
\\ TRY (every_case_tac \\ RealArith.REAL_ASM_ARITH_TAC);
val FPRangeValidator_sound = store_thm (
"FPRangeValidator_sound",
......@@ -141,52 +138,46 @@ val FPRangeValidator_sound = store_thm (
validErrorbound e tMap A dVars /\
FPRangeValidator e A tMap dVars /\
domain (usedVars e) DIFF (domain dVars) SUBSET (domain fVars) /\
(!v. v IN domain fVars ==>
?vR. E1 v = SOME vR /\ FST (P v) <= vR /\ vR <= SND (P v)) /\
(!v. v IN domain fVars \/ v IN domain dVars ==>
?m. Gamma v = SOME m) /\
(!v. v IN domain dVars ==>
?vR. E1 v = SOME vR /\ FST (FST (A (Var v))) <= vR /\ vR <= SND (FST (A (Var v)))) /\
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 /\ tMap (Var v) = SOME m /\ validFloatValue vF m)) ==>
(?vF m. E2 v = SOME vF /\ DaisyMapTree_find (Var v) tMap = SOME m
/\ validFloatValue vF m)) ==>
validFloatValue v m``,
once_rewrite_tac [FPRangeValidator_def] \\ rewrite_tac [GSYM normalOrZero_def]
\\ rpt strip_tac
\\`tMap e = SOME m`
\\`DaisyMapTree_find e tMap = SOME m`
by (drule typingSoundnessExp
\\ disch_then drule \\ fs[])
\\ fs[]
\\ Cases_on `A e` \\ rename1 `A e = (iv_e, err_e)` \\ fs[]
\\ Cases_on `iv_e` \\ rename1 `A e = ((e_lo, e_hi), err_e)`
\\ once_rewrite_tac [validFloatValue_def]
\\ `?vR. eval_exp E1 (toRMap Gamma) (toREval e) vR M0 /\
FST (FST (A e)) <= vR /\ vR <= SND (FST (A e))`
\\ `?iv err vR. DaisyMapTree_find e A = SOME (iv, err) /\
eval_exp E1 (toRMap Gamma) (toREval e) vR M0 /\
FST iv <= vR /\ vR <= SND iv`
by (drule validIntervalbounds_sound
\\ disch_then (qspecl_then [`fVars`, `E1`, `Gamma`] impl_subgoal_tac)
\\ fs[] \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
\\ qexists_tac `vR` \\ rw_asm_star `A _ = _`)
\\ `abs (vR - v) <= SND (A e)`
by (drule validErrorbound_sound
\\ rpt (disch_then drule)
\\ strip_tac
\\ qpat_x_assum `eval_exp E2 Gamma e nF _` kall_tac
\\ first_x_assum drule
\\ rw_asm_star `A e = _`)
\\ rw_asm_star `A e = _`
\\ qspecl_then [`vR`, `v`, `err_e`, `(e_lo,e_hi)`]
\\ qexists_tac `vR` \\ fs[])
\\ rename1 `DaisyMapTree_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)
\\ 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]
>- (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]
\\ `tMap (Var n) = SOME m` by (drule typingSoundnessExp \\ rpt (disch_then drule)
\\ fs[])
\\ qpat_x_assum `tMap (Var n) = SOME _` (fn thm => fs[thm])
\\ inversion `eval_exp E2 _ _ _ _` eval_exp_cases
\\ qpat_x_assum `E2 n = SOME v` (fn thm => fs[thm])
\\ rveq \\ fs[])
\\ `DaisyMapTree_find (Var n) tMap = SOME m`
by (drule typingSoundnessExp \\ rpt (disch_then drule)
\\ fs[])
\\ fs[] \\ rveq
\\ rpt (inversion `eval_exp E2 _ _ _ _` eval_exp_cases)
\\ qpat_x_assum `E2 n = SOME v` (fn thm => fs[thm]))
\\ solve_tac)
\\ solve_tac);
......@@ -202,30 +193,25 @@ val FPRangeValidatorCmd_sound = store_thm (
validErrorboundCmd f tMap A dVars
FPRangeValidatorCmd f A tMap dVars
domain (freeVars f) DIFF domain dVars domain fVars
(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 v = SOME vF tMap (Var v) = SOME m
validFloatValue vF m)
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 /\ DaisyMapTree_find (Var v) tMap = SOME m
/\ validFloatValue vF m)) ==>
validFloatValue v m``,
Induct
\\ simp[Once toREvalCmd_def, Once validIntervalboundsCmd_def,
Once validErrorboundCmd_def, Once FPRangeValidatorCmd_def,
Once typeCheckCmd_def, Once freeVars_def, FPRangeValidatorCmd_def]
\\ simp[Once toREvalCmd_def, Once FPRangeValidatorCmd_def,
Once freeVars_def]
\\ rpt strip_tac
>- (rpt (inversion `bstep (Let _ _ _ _) _ _ _ _` bstep_cases)
>- (Daisy_compute ``validErrorboundCmd``
\\ Daisy_compute ``validIntervalboundsCmd``
\\ Daisy_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`
\\ `tMap e = SOME m`
\\ `DaisyMapTree_find e tMap = SOME m`
by (drule typingSoundnessExp
\\ rpt (disch_then drule)
\\ fs[])
......@@ -233,8 +219,8 @@ val FPRangeValidatorCmd_sound = store_thm (
\\ inversion `ssa _ _ _` ssa_cases
\\ drule validErrorbound_sound
\\ disch_then drule
\\ disch_then (qspecl_then [`vR_e`, `SND (A e)`, `P`, `FST(FST (A e))`, `SND(FST (A e))`] impl_subgoal_tac)
>- (fs[] \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
\\ disch_then (qspecl_then [`vR_e`, `err_e`, `P`, `FST iv_e`, `SND iv_e`] impl_subgoal_tac)
>- (fs[]
\\ fs[DIFF_DEF, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule
\\ fs[domain_union]
\\ CCONTR_TAC \\ fs[] \\ rveq
......@@ -244,16 +230,16 @@ val FPRangeValidatorCmd_sound = store_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[]
\\ 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)
\\ Cases_on `tMap (Var n)` \\ fs[]
\\ fs[] \\ rveq \\ fs[]
\\ `vR_e = vR'` by metis_tac[meps_0_deterministic]
\\ rveq
\\ rename1 `vR_e <= SND (FST _)`
\\ 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`,
......@@ -261,7 +247,6 @@ val FPRangeValidatorCmd_sound = store_thm (
impl_subgoal_tac)
>- (fs[] \\ rpt conj_tac
>- (irule approxUpdBound \\ fs[lookup_NONE_domain]
\\ qpat_x_assum `A e = A (Var n)` (fn thm => once_rewrite_tac [GSYM thm])
\\ first_x_assum (qspecl_then [`vF`, `m`] irule)
\\ qexists_tac `m` \\ fs[])
>- (irule ssa_equal_set
......@@ -274,7 +259,7 @@ val FPRangeValidatorCmd_sound = store_thm (
\\ metis_tac[])
>- (irule swap_Gamma_bstep
\\ qexists_tac `updDefVars n M0 (toRMap Gamma)` \\ fs[]
\\ MATCH_ACCEPT_TAC Rmap_updVars_comm)
\\ fs [updDefVars_def, REWRITE_RULE [updDefVars_def] Rmap_updVars_comm])
>- (fs[DIFF_DEF, domain_insert, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ simp[Once freeVars_def]
......@@ -282,17 +267,18 @@ val FPRangeValidatorCmd_sound = store_thm (
\\ fs[]
\\ rw_thm_asm `x IN domain (freeVars f)` freeVars_def
\\ fs[])
>- (rpt strip_tac \\ simp[updEnv_def]
>- (fs [dVars_range_valid_def]
\\ rpt strip_tac \\ simp[updEnv_def]
\\ IF_CASES_TAC \\ fs[]
\\ rveq
\\ fs[domain_union])
>- (rpt strip_tac \\ fs[updDefVars_def]
\\ TOP_CASE_TAC \\ fs[])
>- (rpt gen_tac \\ disch_then assume_tac
>- (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[]
>- (qpat_x_assum `A e = A (Var n)` (fn thm => fs[GSYM thm]))
\\ TOP_CASE_TAC \\ rveq \\ fs[]
\\ qpat_x_assum `A e = A (Var n)` (fn thm => fs[GSYM thm]))
>- (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_exp E2 Gamma e nF _` kall_tac
......@@ -321,6 +307,10 @@ val FPRangeValidatorCmd_sound = store_thm (
\\ first_x_assum (qspec_then `n` assume_tac)
\\ res_tac)
\\ fs[])
\\ Daisy_compute ``validErrorboundCmd``
\\ Daisy_compute ``validIntervalboundsCmd``
\\ Daisy_compute ``typeCheckCmd``
\\ rveq \\ fs[]
\\ rpt (inversion `bstep (Ret _) _ _ _ _` bstep_cases)
\\ drule FPRangeValidator_sound
\\ rpt (disch_then drule)
......
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