Commit c7165590 authored by Heiko Becker's avatar Heiko Becker

Strengthen typeChecker to be able to prove let binding floating point range validation

parent 97c5452a
......@@ -18,7 +18,7 @@ val _ = temp_overload_on("abs",``real$abs``);
val CertificateChecker_def = Define
`CertificateChecker (e:real exp) (absenv:analysisResult) (P:precond) (defVars: num -> mType option)=
if (typeCheck e defVars (typeMap defVars e)) then
if (validIntervalbounds e absenv P LN /\ FPRangeValidator e absenv (typeMap defVars e)) then
if (validIntervalbounds e absenv P LN /\ FPRangeValidator e absenv (typeMap defVars e) LN) then
(validErrorbound e (typeMap defVars e) absenv LN)
else F
else F`;
......@@ -26,7 +26,7 @@ val CertificateChecker_def = Define
val CertificateCheckerCmd_def = Define
`CertificateCheckerCmd (f:real cmd) (absenv:analysisResult) (P:precond) defVars =
if (typeCheckCmd f defVars (typeMapCmd defVars f) /\ validSSA f (freeVars f)) then
if (validIntervalboundsCmd f absenv P LN) (*/\ validFloatRanges f absenv P LN *)then
if ((validIntervalboundsCmd f absenv P LN) /\ FPRangeValidatorCmd f absenv (typeMapCmd defVars f) LN) then
(validErrorboundCmd f (typeMapCmd defVars f) absenv LN)
else F
else F`;
......
......@@ -2554,6 +2554,7 @@ val validErrorboundCmd_gives_eval = store_thm (
by (irule typingSoundnessExp
\\ qexistsl_tac [`E2`, `Gamma`, `vF`] \\ fs[])
\\ fs[]
\\ Cases_on `expTypes (Var n)` \\ fs[]
\\ `?vF_res m_res. bstep f (updEnv n vF E2) (updDefVars n mF Gamma) vF_res m_res`
by (first_x_assum irule
\\ qexistsl_tac [`updEnv n v E1`, `P`, `absenv`,
......@@ -2664,7 +2665,7 @@ val validErrorboundCmd_sound = store_thm ("validErrorboundCmd_sound",
\\ rw_thm_asm `validIntervalboundsCmd _ _ _ _` validIntervalboundsCmd_def
\\ rw_thm_asm `typeCheckCmd _ _ _` typeCheckCmd_def
\\ `expTypes e = SOME m` by (irule typingSoundnessExp \\ qexistsl_tac [`E2`, `Gamma`, `vf`] \\ fs[])
\\ fs[]
\\ Cases_on `expTypes (Var n)` \\ fs[]
\\ qexistsl_tac [`absenv`, `updEnv n vr E1`, `updEnv n vf E2`, `outVars`,
`fVars`, `insert n () dVars`, `elo`, `ehi`, `P`, `m'`,
`expTypes`, `updDefVars n m Gamma`]
......
......@@ -35,6 +35,10 @@ val FPRangeValidator_def = Define `
FPRangeValidator e A typeMap dVars
| Downcast m e => FPRangeValidator e A typeMap dVars
| _ => T
in
let normal_or_zero =
((normal (IVlo iv_e_float) m \/ (IVlo iv_e_float) = 0) /\
(normal (IVhi iv_e_float) m \/ (IVhi iv_e_float) = 0))
in
(case e of
| Var v =>
......@@ -43,18 +47,21 @@ val FPRangeValidator_def = Define `
else
if (validValue (IVhi iv_e_float) m /\
validValue (IVlo iv_e_float) m)
then ((normal (IVlo iv_e_float) m) \/ ((IVlo iv_e_float) = 0) \/
normal (IVhi iv_e_float) m \/ (IVhi iv_e_float) = 0) /\ recRes
then normal_or_zero /\ recRes
else
F
| _ => if (validValue (IVhi iv_e_float) m /\
validValue (IVlo iv_e_float) m)
then ((normal (IVlo iv_e_float) m) \/ ((IVlo iv_e_float) = 0) \/
normal (IVhi iv_e_float) m \/ (IVhi iv_e_float) = 0) /\ recRes
then normal_or_zero /\ recRes
else
F)
| NONE => F`;
val normalOrZero_def = Define `
normalOrZero iv_e_float m =
((normal (IVlo iv_e_float) m \/ (IVlo iv_e_float) = 0) /\
(normal (IVhi iv_e_float) m \/ (IVhi iv_e_float) = 0))`;
val FPRangeValidatorCmd_def = Define `
(FPRangeValidatorCmd ((Let m x e g):real cmd) A typeMap dVars =
if FPRangeValidator e A typeMap dVars
......@@ -139,7 +146,8 @@ val FPRangeValidator_sound = store_thm (
(!(v:num). v IN domain dVars ==>
(?vF m. E2 v = SOME vF /\ tMap (Var v) = SOME m /\ validFloatValue vF m)) ==>
validFloatValue v m``,
once_rewrite_tac [FPRangeValidator_def] \\ rpt strip_tac
once_rewrite_tac [FPRangeValidator_def] \\ rewrite_tac [GSYM normalOrZero_def]
\\ rpt strip_tac
\\`tMap e = SOME m`
by (drule typingSoundnessExp
\\ disch_then drule \\ fs[])
......@@ -161,7 +169,9 @@ val FPRangeValidator_sound = store_thm (
\\ first_x_assum drule
\\ rw_asm_star `A e = _`)
\\ rw_asm_star `A e = _`
\\ qspecl_then [`vR`, `v`, `err_e`, `(e_lo,e_hi)`] impl_subgoal_tac (SIMP_RULE std_ss [contained_def, widenInterval_def] distance_gives_iv)
\\ qspecl_then [`vR`, `v`, `err_e`, `(e_lo,e_hi)`]
impl_subgoal_tac
(SIMP_RULE std_ss [contained_def, widenInterval_def] distance_gives_iv)
\\ fs[IVlo_def, IVhi_def]
\\ Cases_on `e`
>- (fs[]
......@@ -216,22 +226,100 @@ val FPRangeValidatorCmd_sound = store_thm (
\\ rpt (disch_then drule)
\\ fs[])
\\ fs[]
\\ 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)
\\ 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`] impl_subgoal_tac)
>- (fs[] \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
\\ 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[]
\\ `vR_e = vR'` by metis_tac[meps_0_deterministic]
\\ rveq
\\ rename1 `vR_e <= SND (FST _)`
\\ first_x_assum
(qspecl_then [`updEnv n vR_e E1`, `updEnv n vF_e E2`,
(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`]
impl_subgoal_tac)
>- (inversion `ssa _ _ _` ssa_cases
\\ fs[] \\ rpt conj_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])
\\ drule validErrorbound_sound
\\ first_x_assum (qspecl_then [`vF`, `m`] irule)
\\ qexists_tac `m` \\ fs[])
>- (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)
>- (fs[DIFF_DEF, domain_insert, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ simp[Once freeVars_def]
\\ once_rewrite_tac [domain_union]
\\ fs[]
\\ rw_thm_asm `x IN domain (freeVars f)` freeVars_def
\\ fs[])
>- (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[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]))
\\ rpt strip_tac
\\ fs[updEnv_def] \\ rveq \\ fs[]
>- (qpat_x_assum `eval_exp E2 Gamma e nF _` kall_tac
\\ drule FPRangeValidator_sound
\\ rpt (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[]
);
\\ disch_then irule \\ fs[]
\\ fs[DIFF_DEF, domain_insert, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ simp[Once freeVars_def]
\\ once_rewrite_tac [domain_union]
\\ fs[]
\\ CCONTR_TAC \\ fs[] \\ rveq
\\ first_x_assum (qspec_then `n` assume_tac)
\\ res_tac)
\\ TOP_CASE_TAC \\ fs[]
\\ qpat_x_assum `eval_exp E2 Gamma e nF _` kall_tac
\\ drule FPRangeValidator_sound
\\ rpt (disch_then drule)
\\ disch_then irule \\ fs[]
\\ fs[DIFF_DEF, domain_insert, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ simp[Once freeVars_def]
\\ once_rewrite_tac [domain_union]
\\ fs[]
\\ CCONTR_TAC \\ fs[] \\ rveq
\\ first_x_assum (qspec_then `n` assume_tac)
\\ res_tac)
\\ fs[])
\\ rpt (inversion `bstep (Ret _) _ _ _ _` bstep_cases)
\\ drule FPRangeValidator_sound
\\ rpt (disch_then drule)
\\ fs[]);
val _ = export_theory();
......@@ -123,6 +123,12 @@ val normal_def = Define `
normal (v:real) (m:mType) =
(minValue m <= abs v /\ abs v <= maxValue m)`;
val denormal_def = Define `
denormal (v:real) (m:mType) =
case m of
| M0 => F
| _ => ((abs v) < (minValue m) /\ v <> 0)`;
(**
Predicate that is true if and only if the given value v is a valid
floating-point value according to the the type m.
......@@ -133,7 +139,7 @@ val validFloatValue_def = Define `
validFloatValue (v:real) (m:mType) =
case m of
| M0 => T
| _ => normal v m \/ v = 0`
| _ => normal v m \/ denormal v m \/ v = 0`
val validValue_def = Define `
validValue (v:real) (m:mType) =
......
......@@ -92,8 +92,9 @@ val typeCheckCmd_def = Define `
case c of
| Let m x e g => if (typeCheck e Gamma tMap)
then
case tMap e of
| SOME me => me = m /\ typeCheckCmd g (updDefVars x me Gamma) tMap
case tMap e, tMap (Var x) of
| SOME me, SOME mx =>
mx = m /\ me = m /\ typeCheckCmd g (updDefVars x me Gamma) tMap
| _ => F
else F
| Ret e => typeCheck e Gamma tMap`
......
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