Commit 0b909223 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Start error validation FMA proofs

parent 15ce5f84
......@@ -55,6 +55,23 @@ val validErrorbound_def = Define `
((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideInterval errIve1 errIve2) * (mTypeToQ m)) <= err)
else F)
else F)
| Fma f1 f2 f3 =>
(if (validErrorbound f1 typeMap absenv dVars /\
validErrorbound f2 typeMap absenv dVars /\
validErrorbound f3 typeMap absenv dVars) then
let (ive1, err1) = absenv f1 in
let (ive2, err2) = absenv f2 in
let (ive3, err3) = absenv f3 in
let errIve1 = widenInterval ive1 err1 in
let errIve2 = widenInterval ive2 err2 in
let errIve3 = widenInterval ive3 err3 in
let upperBoundE1 = maxAbs ive1 in
let upperBoundE2 = maxAbs ive2 in
let upperBoundE3 = maxAbs ive3 in
let errIntv_prod = multInterval errIve2 errIve3 in
let mult_error_bound = (upperBoundE2 * err3 + upperBoundE3 * err2 + err2 * err3) in
(err1 + mult_error_bound + (maxAbs (addInterval errIve1 errIntv_prod)) * (mTypeToQ m)) <= err
else F)
| Downcast m1 e1 =>
let (ive1, err1) = absenv e1 in
let rec_res = validErrorbound e1 typeMap absenv dVars in
......@@ -85,6 +102,7 @@ val err_always_positive = store_thm (
>- (Cases_on `tmap (Const m v)` \\ fs [])
>- (Cases_on `tmap (Unop u e')` \\ fs [])
>- (Cases_on `tmap (Binop b e' e0)` \\ fs [])
>- (Cases_on `tmap (Fma e' e0 e1)` \\ fs [])
>- (Cases_on `tmap (Downcast m e')` \\ fs []));
val validErrorboundCorrectVariable_eval = store_thm (
......@@ -2121,6 +2139,63 @@ val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
rule_assum_tac (fn thm => REWRITE_RULE [contained_def, IVlo_def, IVhi_def] thm) \\
fs[widenInterval_def, IVlo_def, IVhi_def,noDivzero_def])));
val validErrorboundCorrectFma = store_thm ("validErrorboundCorrectFma",
``!(E1 E2:env) (absenv:analysisResult) (e1:real exp) (e2:real exp) (e3: real exp)
(nR nR1 nR2 nR3 nF nF1 nF2 nF3:real) (e err1 err2 err3:real) (alo ahi e1lo e1hi e2lo e2hi e3lo e3hi :real) dVars m m1 m2 m3 expTypes Gamma.
(m = join3 m1 m2 m3) /\
eval_exp E1 (toRMap Gamma) (toREval e1) nR1 M0 /\
eval_exp E1 (toRMap Gamma) (toREval e2) nR2 M0 /\
eval_exp E1 (toRMap Gamma) (toREval e3) nR3 M0 /\
eval_exp E1 (toRMap Gamma) (toREval (Fma e1 e2 e3)) nR M0 /\
eval_exp E2 Gamma e1 nF1 m1 /\
eval_exp E2 Gamma e2 nF2 m2 /\
eval_exp E2 Gamma e3 nF3 m3 /\
eval_exp (updEnv 3 nF3 (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)))
(updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 Gamma)))
(Fma (Var 1) (Var 2) (Var 3)) nF m /\
typeCheck (Fma e1 e2 e3) Gamma expTypes /\
validErrorbound (Fma e1 e2 e3) expTypes absenv dVars /\
FST (FST (absenv e1)) <= nR1 /\
nR1 <= SND (FST (absenv e1)) /\
FST (FST (absenv e2)) <= nR2 /\
nR2 <= SND (FST (absenv e2)) /\
FST (FST (absenv e3)) <= nR3 /\
nR3 <= SND (FST (absenv e3)) /\
(absenv e1 = ((e1lo,e1hi),err1)) /\
(absenv e2 = ((e2lo, e2hi),err2)) /\
(absenv e3 = ((e3lo, e3hi),err3)) /\
(absenv (Fma e1 e2 e3) = ((alo,ahi),e)) /\
abs (nR1 - nF1) <= err1 /\
abs (nR2 - nF2) <= err2 /\
abs (nR3 - nF3) <= err3 ==>
abs (nR - nF) <= e``,
once_rewrite_tac [validErrorbound_def]
\\ rpt strip_tac \\ fs[]
\\ qpat_x_assum `absenv (Fma _ _ _) = _` (fn thm => fs [thm] \\ assume_tac thm)
\\ qpat_x_assum `absenv e1 = _` (fn thm => fs [thm] \\ assume_tac thm)
\\ qpat_x_assum `absenv e2 = _` (fn thm => fs [thm] \\ assume_tac thm)
\\ qpat_x_assum `absenv e3 = _` (fn thm => fs [thm] \\ assume_tac thm)
\\ fs [Once typeCheck_def]
\\ Cases_on `expTypes (Fma e1 e2 e3)` \\ rveq \\ fs []
\\ Cases_on `expTypes e1` \\ rveq \\ fs []
\\ Cases_on `expTypes e2` \\ rveq \\ fs []
\\ Cases_on `expTypes e3` \\ rveq \\ fs []
\\ `expTypes e1 = SOME m1` by (match_mp_tac typingSoundnessExp \\ metis_tac [])
\\ `expTypes e2 = SOME m2` by (match_mp_tac typingSoundnessExp \\ metis_tac [])
\\ `expTypes e3 = SOME m3` by (match_mp_tac typingSoundnessExp \\ metis_tac [])
\\ fs [] \\ rveq
\\ `0 <= err1`
by (match_mp_tac err_always_positive
\\ qexistsl_tac [`e1`, `absenv`, `(e1lo,e1hi)`, `dVars`, `expTypes`] \\ fs[])
\\ `0 <= err2`
by (match_mp_tac err_always_positive
\\ qexistsl_tac [`e2`, `absenv`, `(e2lo,e2hi)`, `dVars`, `expTypes`] \\ fs[])
\\ `0 <= err3`
by (match_mp_tac err_always_positive
\\ qexistsl_tac [`e3`, `absenv`, `(e3lo,e3hi)`, `dVars`, `expTypes`] \\ fs[])
\\ match_mp_tac REAL_LE_TRANS
\\ );
val validErrorboundCorrectRounding = store_thm ("validErrorboundCorrectRounding",
``!(E1 E2:env) (absenv:analysisResult) (e:real exp)
(nR nF nF1:real) (err err':real) (alo ahi elo ehi:real) dVars m machineEpsilon expTypes Gamma.
......@@ -2424,6 +2499,154 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
\\ irule Binop_dist'
\\ qexistsl_tac [`0`, `M0`, `M0`, `nR1`, `nR2`]
\\ fs[perturb_def, mTypeToQ_pos])))
>- (rename1 `Fma e1 e2 e3`
\\ Cases_on `expTypes (Fma e1 e2 e3)` \\ fs[]
\\ Cases_on `absenv e1` \\ rename1 `absenv e1 = (iv_e1, err_e1)`
\\ Cases_on `iv_e1` \\ rename1 `absenv e1= ((e1_lo, e1_hi), err_e1)`
\\ Cases_on `absenv e2` \\ rename1 `absenv e2 = (iv_e2, err_e2)`
\\ Cases_on `iv_e2` \\ rename1 `absenv e2 = ((e2_lo, e2_hi), err_e2)`
\\ Cases_on `absenv e3` \\ rename1 `absenv e3 = (iv_e3, err_e3)`
\\ Cases_on `iv_e3` \\ rename1 `absenv e3 = ((e3_lo, e3_hi), err_e3)`
\\ rw_thm_asm `eval_exp E1 _ _ _ _` toREval_def
\\ fs[]
\\ inversion `eval_exp E1 _ _ _ _` eval_exp_cases
\\ `m1 = M0 /\ m2 = M0 /\ m3 = M0` by (rpt (conj_tac) \\ irule toRMap_eval_M0 \\ asm_exists_tac \\ fs[])
\\ rveq
\\ `(?nF1 m1. eval_exp E2 Gamma e1 nF1 m1) /\
(!nF1 m1. eval_exp E2 Gamma e1 nF1 m1 ==> abs (v1 - nF1) <= err_e1)`
by (first_x_assum irule
\\ qexistsl_tac [`E1`, `P`, `absenv`, `dVars`, `e1_hi`, `e1_lo`, `expTypes`, `fVars`]
\\ fs[Once validIntervalbounds_def]
\\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
\\ rw_thm_asm `typeCheck _ _ _` typeCheck_def
\\ rw_asm_star `expTypes _ = _`
\\ Cases_on `expTypes e1`
\\ Cases_on `expTypes e2`
\\ Cases_on `expTypes e3`
\\ fs[DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
\\ `(?nF2 m2. eval_exp E2 Gamma e2 nF2 m2) /\
(!nF2 m2. eval_exp E2 Gamma e2 nF2 m2 ==> abs (v2 - nF2) <= err_e2)`
by (first_x_assum irule
\\ qexistsl_tac [`E1`, `P`, `absenv`, `dVars`, `e2_hi`, `e2_lo`, `expTypes`, `fVars`]
\\ fs[Once validIntervalbounds_def]
\\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
\\ rw_thm_asm `typeCheck _ _ _` typeCheck_def
\\ rw_asm_star `expTypes _ = _`
\\ Cases_on `expTypes e1`
\\ Cases_on `expTypes e2`
\\ Cases_on `expTypes e3`
\\ fs[DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
\\ `(?nF3 m3. eval_exp E2 Gamma e3 nF3 m3) /\
(!nF3 m3. eval_exp E2 Gamma e3 nF3 m3 ==> abs (v3 - nF3) <= err_e3)`
by (first_x_assum irule
\\ qexistsl_tac [`E1`, `P`, `absenv`, `dVars`, `e3_hi`, `e3_lo`, `expTypes`, `fVars`]
\\ fs[Once validIntervalbounds_def]
\\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
\\ rw_thm_asm `typeCheck _ _ _` typeCheck_def
\\ rw_asm_star `expTypes _ = _`
\\ Cases_on `expTypes e1`
\\ Cases_on `expTypes e2`
\\ Cases_on `expTypes e3`
\\ fs[DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
\\ `?nR1. eval_exp E1 (toRMap Gamma) (toREval e1) nR1 M0 /\
FST (FST (absenv e1)) <= nR1 /\ nR1 <= SND (FST (absenv e1))`
by (irule validIntervalbounds_sound
\\ qexistsl_tac [`P`, `dVars`, `fVars`]
\\ fs[Once validIntervalbounds_def]
\\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
\\ fs [DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
\\ `?nR2. eval_exp E1 (toRMap Gamma) (toREval e2) nR2 M0 /\
FST (FST (absenv e2)) <= nR2 /\ nR2 <= SND (FST (absenv e2))`
by (irule validIntervalbounds_sound
\\ qexistsl_tac [`P`, `dVars`, `fVars`]
\\ fs[Once validIntervalbounds_def]
\\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
\\ fs [DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
\\ `?nR3. eval_exp E1 (toRMap Gamma) (toREval e3) nR3 M0 /\
FST (FST (absenv e3)) <= nR3 /\ nR3 <= SND (FST (absenv e3))`
by (irule validIntervalbounds_sound
\\ qexistsl_tac [`P`, `dVars`, `fVars`]
\\ fs[Once validIntervalbounds_def]
\\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
\\ fs [DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
\\ `nR1 = v1 /\ nR2 = v2 /\ nR3 = v3` by (metis_tac[meps_0_deterministic]) \\ rveq
\\ rw_asm_star `absenv e1 = _`
\\ rw_asm_star `absenv e2 = _`
\\ rw_asm_star `absenv e3 = _`
\\ `contained nF1 (widenInterval (e1_lo,e1_hi) err_e1)`
by (irule distance_gives_iv
\\ qexists_tac `nR1` \\ fs[contained_def, IVlo_def, IVhi_def]
\\ first_x_assum irule
\\ qexists_tac `m1` \\ fs[])
\\ `contained nF2 (widenInterval (e2_lo, e2_hi) err_e2)`
by (irule distance_gives_iv
\\ qexists_tac `nR2` \\ fs [contained_def, IVlo_def, IVhi_def]
\\ first_x_assum irule
\\ qexists_tac `m2` \\ fs[])
\\ `contained nF3 (widenInterval (e3_lo, e3_hi) err_e3)`
by (irule distance_gives_iv
\\ qexists_tac `nR3` \\ fs [contained_def, IVlo_def, IVhi_def]
\\ first_x_assum irule
\\ qexists_tac `m3` \\ fs[])
\\ conj_tac
>- (qexistsl_tac [`perturb (evalFma nF1 nF2 nF3) 0`, `join3 m1 m2 m3`]
\\ irule Fma_dist'
\\ qexistsl_tac [`0`, `m1`, `m2`, `m3`, `nF1`, `nF2`, `nF3`]
\\ fs[mTypeToQ_pos])
\\ rpt strip_tac
\\ `perturb (evalFma nR1 nR2 nR3) delta = evalFma nR1 nR2 nR3`
by (irule delta_0_deterministic \\ fs[mTypeToQ_def, join3_def, join_def])
\\ fs[]
\\ inversion `eval_exp E2 _ (Fma e1 e2 e3) _ _` eval_exp_cases
\\ rename1 `abs delta2 <= mTypeToQ (join3 mF1 mF2 mF3)`
\\ `eval_exp (updEnv 3 v3 (updEnv 2 v2 (updEnv 1 v1 emptyEnv)))
(updDefVars 3 mF3 (updDefVars 2 mF2 (updDefVars 1 mF1 Gamma)))
(Fma (Var 1) (Var 2) (Var 3)) (perturb (evalFma v1 v2 v3) delta2)
(join3 mF1 mF2 mF3)`
by (irule fma_unfolding \\ fs[]
\\ qexistsl_tac [`E2`, `e1`, `e2`, `e3`] \\ fs[eval_exp_cases]
\\ qexistsl_tac [`mF1`, `mF2`, `mF3`, `v1`, `v2`, `v3`, `delta2`] \\ fs[])
\\ rveq
>- (irule validErrorboundCorrectAddition
\\ qexistsl_tac [`E1`, `E2`, `Gamma`, `absenv`, `ehi`, `elo`, `dVars`,
`e1`, `e1_hi`, `e1_lo`, `e2`,`e2_hi`, `e2_lo`,
`err_e1`, `err_e2`, `expTypes`, `join mF1 mF2`,
`mF1`, `mF2`, `v1`, `v2`, `nR1`, `nR2`]
\\ fs[]
\\ rpt conj_tac \\ TRY (first_x_assum irule)
>- (qexists_tac `mF1` \\ fs[])
>- (qexists_tac `mF2` \\ fs[])
>- (once_rewrite_tac [validErrorbound_def] \\ fs[])
>- (simp [Once toREval_def]
\\ irule Binop_dist'
\\ qexistsl_tac [`0`, `M0`, `M0`, `nR1`, `nR2`]
\\ fs[perturb_def, mTypeToQ_pos]))
>- (irule validErrorboundCorrectMult
\\ qexistsl_tac [`E1`, `E2`, `Gamma`, `absenv`, `ehi`, `elo`, `dVars`,
`e1`, `e1_hi`, `e1_lo`, `e2`,`e2_hi`, `e2_lo`,
`err_e1`, `err_e2`, `expTypes`, `join mF1 mF2`,
`mF1`, `mF2`, `v1`, `v2`, `nR1`, `nR2`]
\\ fs[]
\\ rpt conj_tac \\ TRY (first_x_assum irule)
>- (qexists_tac `mF1` \\ fs[])
>- (qexists_tac `mF2` \\ fs[])
>- (once_rewrite_tac [validErrorbound_def] \\ fs[])
>- (simp [Once toREval_def]
\\ irule Binop_dist'
\\ qexistsl_tac [`0`, `M0`, `M0`, `nR1`, `nR2`]
\\ fs[perturb_def, mTypeToQ_pos]))
>- (rename1 `Downcast m1 e1`
\\ Cases_on `expTypes (Downcast m1 e1)` \\ fs[]
\\ Cases_on `absenv e1` \\ rename1 `absenv e1 = (iv_e1, err_e1)`
......
......@@ -319,10 +319,10 @@ val meps_0_deterministic = store_thm("meps_0_deterministic",
\\ res_tac));
(**
Helping lemma. Needed in soundness proof.
Helping lemmas. Needed in soundness proof.
For each evaluation of using an arbitrary epsilon, we can replace it by
evaluating the subExpressions and then binding the result values to different
variables in the Eironment.
variables in the Environment.
**)
val binary_unfolding = store_thm("binary_unfolding",
``!(b:binop) (f1:(real)exp) (f2:(real)exp) E Gamma (v:real) v1 v2 m1 m2 delta.
......@@ -337,6 +337,21 @@ 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 fma_unfolding = store_thm("fma_unfolding",
``!(f1:(real)exp) (f2:(real)exp) (f3:(real)exp) E Gamma (v:real) v1 v2 v3 m1 m2 m3 delta.
(abs delta) <= (mTypeToQ (join3 m1 m2 m3)) /\
eval_exp E Gamma f1 v1 m1 /\
eval_exp E Gamma f2 v2 m2 /\
eval_exp E Gamma f3 v3 m3 /\
eval_exp E Gamma (Fma f1 f2 f3) (perturb (evalFma v1 v2 v3) delta) (join3 m1 m2 m3) ==>
eval_exp (updEnv 3 v3 (updEnv 2 v2 (updEnv 1 v1 emptyEnv)))
(updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 Gamma)))
(Fma (Var 1) (Var 2) (Var 3)) (perturb (evalFma v1 v2 v3) delta) (join3 m1 m2 m3)``,
fs [updEnv_def,updDefVars_def,join3_def,join_def,eval_exp_cases,APPLY_UPDATE_THM,PULL_EXISTS]
\\ rpt strip_tac
\\ qexists_tac `delta'`
\\ conj_tac \\ fs[]);
val eval_eq_env = store_thm (
"eval_eq_env",
``!e E1 E2 Gamma v m.
......
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