Skip to content

GitLab

F
FloVer
Commit 583f101f authored by Heiko Becker's avatar Heiko Becker
Browse files
Options

WIP for finite maps port

parent 369a1703
Hide whitespace changes
Inline Side-by-side
Showing with 127 additions and 162 deletions
coq/ErrorValidation.v
View file @ 583f101f
......@@ -230,12 +230,8 @@ Proof.
apply RmaxAbs; eauto.
Qed.
Lemma validErrorboundCorrectConstant_eval E1 E2 A m n nR e nlo nhi dVars Gamma defVars:
Lemma validErrorboundCorrectConstant_eval E1 E2 A m n nR Gamma:
eval_exp E1 (toRMap defVars) (toREval (toRExp (Const m n))) nR M0 ->
typeCheck (Const m n) defVars Gamma = true ->
validErrorbound (Const m n) Gamma A dVars = true ->
(Q2R nlo <= nR <= Q2R nhi)%R ->
DaisyMap.find (Const m n) A = Some ((nlo,nhi),e) ->
exists nF m',
eval_exp E2 defVars (toRExp (Const m n)) nF m'.
Proof.
......
hol4/ErrorValidationScript.sml
View file @ 583f101f
......@@ -12,6 +12,7 @@ open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics MachineTypeThe
open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory TypingTheory
open IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory DaisyMapTheory
val _ = new_theory "ErrorValidation";
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
......@@ -56,23 +57,25 @@ val validErrorbound_def = Define `
else F))
| _, _ => 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)
| Fma e1 e2 e3 =>
(if (validErrorbound e1 typeMap A dVars /\
validErrorbound e2 typeMap A dVars /\
validErrorbound e3 typeMap A dVars) then
case (DaisyMapTree_find e1 A,
DaisyMapTree_find e2 A,
DaisyMapTree_find e3 A) of
| SOME (ive1, err1), SOME (ive2, err2), SOME (ive3, err3) =>
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
|_, _, _ => F
else F)
| Downcast m1 e1 =>
case DaisyMapTree_find e1 A of
| SOME (ive1, err1) =>
......@@ -82,6 +85,16 @@ val validErrorbound_def = Define `
else F)
| _, _ => F`;
``validErrorbound e Gamma A dVars ==> F``
rpt strip_tac
Induct_on `e`
cheat
qpat_x_assum `validErrorbound _ _ _ _` (fn thm => assume_tac (SIMP_RULE std_ss [] (ONCE_REWRITE_RULE [validErrorbound_def] thm)))
BasicProvers.TOP_CASE_TAC
BasicProvers.EVERY_CASE_TAC
Cases_on `
add_unevaluated_function ``validErrorbound``;
val validErrorboundCmd_def = Define `
validErrorboundCmd (f:real cmd) (typeMap: (real exp # mType) binTree)
(A:analysisResult) (dVars:num_set) =
......@@ -96,129 +109,89 @@ val validErrorboundCmd_def = Define `
| Ret e =>
validErrorbound e typeMap A dVars`;
add_unevaluated_function ``validErrorboundCmd``;
val err_always_positive = store_thm (
"err_always_positive",
``!(e:real exp) (absenv:analysisResult) (iv:interval) (err:real) dVars (tmap: real exp -> mType option).
(validErrorbound e tmap absenv dVars) /\
((iv,err) = absenv e) ==>
``!(e:real exp) (A:analysisResult) (iv:interval) (err:real) dVars tmap.
(validErrorbound e tmap A dVars) /\
(DaisyMapTree_find e A = SOME (iv,err)) ==>
0 <= err``,
once_rewrite_tac [validErrorbound_def] \\ rpt strip_tac \\
Cases_on `e` \\
qpat_assum `(iv,err) = absenv e` (fn thm => fs [GSYM thm])
>- (Cases_on `tmap (Var n)` \\ fs [])
>- (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 []));
rpt strip_tac \\ Cases_on `e`
\\ Daisy_compute ``validErrorbound`` \\ rveq \\ fs[])
val validErrorboundCorrectVariable_eval = store_thm (
"validErrorboundCorrectVariable_eval",
``!E1 E2 absenv v e nR nlo nhi P fVars dVars Gamma expTypes.
``!E1 E2 A v e nR nlo nhi P fVars dVars Gamma expTypes.
eval_exp E1 (toRMap Gamma) (toREval (Var v)) nR M0 /\
typeCheck (Var v) Gamma expTypes /\
approxEnv E1 Gamma absenv fVars dVars E2 /\
validIntervalbounds (Var v) absenv P dVars /\
approxEnv E1 Gamma A fVars dVars E2 /\
validIntervalbounds (Var v) A P dVars /\
validErrorbound (Var v) expTypes A dVars /\
(domain (usedVars ((Var v):real exp)) DIFF (domain dVars)) SUBSET (domain fVars) /\
(!v. v IN domain dVars ==>
?r. E1 v = SOME r /\
FST(FST(absenv (Var v))) <= r /\ r <= SND (FST (absenv (Var v)))) /\
(!v. v IN domain fVars ==>
?r. E1 v = SOME r /\
FST (P v) <= r /\ r <= SND (P v)) /\
(!v. v IN ((domain fVars) UNION (domain dVars)) ==>
?m. Gamma v = SOME m) /\
absenv (Var v) = ((nlo, nhi),e) ==>
dVars_range_valid dVars E1 A /\
fVars_P_sound fVars E1 P /\
vars_typed ((domain fVars) UNION (domain dVars)) Gamma /\
DaisyMapTree_find (Var v) A = SOME ((nlo,nhi),e) ==>
? nF m.
eval_exp E2 Gamma (Var v) nF m``,
rpt strip_tac
\\ `?n. eval_exp E1 (toRMap Gamma) (toREval (Var v)) n M0 /\
FST(FST(absenv (Var v))) <= n /\ n <= SND (FST (absenv (Var v)))`
by (irule validIntervalbounds_sound
\\ qexistsl_tac[`P`, `dVars`, `fVars`]
\\ fs[SUBSET_DEF, domain_union]
\\ rpt strip_tac \\ first_x_assum irule \\ fs[])
\\ `nR = n` by (metis_tac[meps_0_deterministic])
\\ rveq
\\ qspecl_then [`Var v`, `A`, `P`, `fVars`, `dVars`, `E1`, `Gamma`] destruct validIntervalbounds_sound
\\ fs[] \\ rveq
\\ `nR = vR` by (metis_tac[meps_0_deterministic]) \\ rveq
\\ fs[toREval_def]
\\ inversion `eval_exp E1 _ _ _ _` eval_exp_cases
\\ Daisy_compute ``validErrorbound``
\\ qspecl_then [`E1`, `E2`, `v`, `nR`, `fVars`, `dVars`, `A`, `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])
\\ `?vF. E2 v = SOME vF`
by (irule approxEnv_gives_value
\\ qexistsl_tac [`E1`, `Gamma`, `absenv`, `dVars`, `fVars`, `n`]
\\ fs[domain_union, SUBSET_DEF, usedVars_def]
\\ Cases_on `v IN (domain dVars)` \\ fs[])
\\ qexistsl_tac [`vF`, `m`] \\ fs[eval_exp_cases]);
\\ qexistsl_tac [`v2`, `m`] \\ fs[eval_exp_cases]);
val validErrorboundCorrectVariable = store_thm (
"validErrorboundCorrectVariable",
``!(E1 E2:env) absenv fVars dVars (v:num) (nR nF err nlo nhi:real) (P:precond) m expTypes Gamma.
``!(E1 E2:env) A fVars dVars (v:num) (nR nF err nlo nhi:real) (P:precond) m expTypes Gamma.
eval_exp E1 (toRMap Gamma) (toREval (Var v)) nR M0 /\
eval_exp E2 Gamma (Var v) nF m /\
typeCheck (Var v) Gamma expTypes /\
approxEnv E1 Gamma absenv fVars dVars E2 /\
validIntervalbounds (Var v) absenv P dVars /\
validErrorbound (Var v) expTypes absenv dVars /\
(domain (usedVars ((Var v):real exp)) DIFF domain dVars) SUBSET domain fVars /\
(!v.
v IN domain dVars ==>
?r.
(E1 v = SOME r) /\
FST (FST (absenv (Var v))) <= r /\
r <= SND (FST (absenv (Var v)))) /\
(!v.
v IN domain fVars ==>
?r.
(E1 v = SOME r) /\
FST (P v) <= r /\ r <= SND (P v)) /\
(!v.
v IN domain fVars \/ v IN domain dVars ==>
?m. Gamma v = SOME m) /\
(absenv (Var v) = ((nlo, nhi),err)) ==>
approxEnv E1 Gamma A fVars dVars E2 /\
validIntervalbounds (Var v) A P dVars /\
validErrorbound (Var v) expTypes A dVars /\
(domain (usedVars ((Var v):real exp)) 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 /\
DaisyMapTree_find (Var v) A = SOME ((nlo,nhi),err) ==>
abs (nR - nF) <= err``,
rpt strip_tac
\\ `?vR. eval_exp E1 (toRMap Gamma) (toREval (Var v)) vR M0 /\
FST (FST (absenv (Var v))) <= vR /\ vR <= SND(FST(absenv (Var v)))`
by (irule validIntervalbounds_sound
\\ qexistsl_tac [`P`, `dVars`, `fVars`]
\\ fs[] \\ first_x_assum MATCH_ACCEPT_TAC)
\\ qspecl_then [`Var v`, `A`, `P`, `fVars`, `dVars`, `E1`, `Gamma`] destruct validIntervalbounds_sound
\\ fs[]
\\ `vR = nR` by (metis_tac[meps_0_deterministic]) \\ rveq
\\ fs[toREval_def]
\\ rpt (inversion `eval_exp _ _ _ _ _` eval_exp_cases)
\\ rw_thm_asm `typeCheck _ _ _` typeCheck_def
\\ rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def
\\ rw_asm_star `absenv (Var v) = _`
\\ rw_asm_star `Gamma v = _`
\\ Cases_on `expTypes (Var v)`
>- (fs[])
>- (Cases_on `lookup v dVars` \\ fs[]
>- (fs[usedVars_def,domain_lookup]
\\ irule REAL_LE_TRANS
\\ qexists_tac `maxAbs (nlo,nhi) * mTypeToQ x`
\\ fs[]
\\ `abs (nR - nF) <= abs nR * mTypeToQ m`
by (irule approxEnv_fVar_bounded
\\ qexistsl_tac [`E1`, `E2`, `Gamma`, `absenv`, `dVars`, `fVars`, `v`]
\\ fs[domain_lookup])
\\ irule REAL_LE_TRANS
\\ qexists_tac `abs nR * mTypeToQ m` \\ fs[]
\\ irule REAL_LE_RMUL_IMP
>- (irule contained_leq_maxAbs
\\ fs[contained_def, IVlo_def, IVhi_def])
>- (irule mTypeToQ_pos))
>- (irule approxEnv_dVar_bounded
\\ qexistsl_tac [`E1`, `E2`, `Gamma`, `absenv`, `dVars`, `fVars`, `m`, `v`]
\\ fs[domain_lookup])));
\\ Daisy_compute ``typeCheck``
\\ Daisy_compute ``validErrorbound`` \\ rveq \\ fs[]
>- (drule approxEnv_dVar_bounded
\\ rpt (disch_then drule)
\\ disch_then (qspecl_then [`m`, `(nlo,nhi)`, `e`] irule)
\\ fs[domain_lookup])
\\ fs[usedVars_def,domain_lookup]
\\ irule REAL_LE_TRANS
\\ qexists_tac `maxAbs (nlo,nhi) * mTypeToQ m` \\ fs[]
\\ drule approxEnv_fVar_bounded
\\ rpt (disch_then drule)
\\ disch_then (qspec_then `m` assume_tac)
\\ irule REAL_LE_TRANS
\\ qexists_tac `abs nR * mTypeToQ m`
\\ conj_tac \\ TRY (first_x_assum irule \\ fs[domain_lookup])
\\ irule REAL_LE_RMUL_IMP
>- (irule contained_leq_maxAbs
\\ fs[contained_def, IVlo_def, IVhi_def])
\\ irule mTypeToQ_pos);
val validErrorboundCorrectConstant_eval = store_thm (
"validErrorboundCorrectConstant_eval",
``!(E1 E2:env) (absenv:analysisResult) (n nR nF e nlo nhi:real) dVars m expTypes Gamma.
eval_exp E1 (toRMap Gamma) (toREval (Const m n)) nR M0 /\
typeCheck (Const m n) Gamma expTypes /\
validErrorbound (Const m n) expTypes absenv dVars /\
FST (FST (absenv (Const m n))) <= nR /\
nR <= SND (FST (absenv (Const m n))) /\
(absenv (Const m n) = ((nlo,nhi),e)) ==>
``!(E1 E2:env) (n nR:real) m Gamma.
eval_exp E1 (toRMap Gamma) (toREval (Const m n)) nR M0 ==>
?nF m1.
eval_exp E2 Gamma (Const m n) nF m1``,
rpt strip_tac
......@@ -229,41 +202,34 @@ val validErrorboundCorrectConstant_eval = store_thm (
val validErrorboundCorrectConstant = store_thm (
"validErrorboundCorrectConstant",
``!(E1 E2:env) (absenv:analysisResult) (n nR nF e nlo nhi:real) dVars m expTypes Gamma.
``!(E1 E2:env) (A:analysisResult) (n nR nF e nlo nhi:real) dVars m expTypes Gamma.
eval_exp E1 (toRMap Gamma) (toREval (Const m n)) nR M0 /\
eval_exp E2 Gamma (Const m n) nF m /\
typeCheck (Const m n) Gamma expTypes /\
validErrorbound (Const m n) expTypes absenv dVars /\
FST (FST (absenv (Const m n))) <= nR /\
nR <= SND (FST (absenv (Const m n))) /\
(absenv (Const m n) = ((nlo,nhi),e)) ==>
validErrorbound (Const m n) expTypes A dVars /\
(nlo <= nR /\ nR <= nhi) /\
DaisyMapTree_find (Const m n) A = SOME ((nlo,nhi),e) ==>
(abs (nR - nF)) <= e``,
once_rewrite_tac [validErrorbound_def]
\\ rpt strip_tac \\ fs[]
\\ fs [toREval_def]
rpt strip_tac \\ fs[toREval_def]
\\ Daisy_compute ``validErrorbound``
\\ Daisy_compute ``typeCheck`` \\ rveq \\ fs[]
\\ inversion `eval_exp _ _ _ _ M0` eval_exp_cases
\\ simp [delta_M0_deterministic]
\\ `nR = n` by (metis_tac [delta_M0_deterministic]) \\ rveq
\\ inversion `eval_exp _ _ _ _ m` eval_exp_cases
\\ simp[perturb_def]
\\ rename1 `abs deltaF <= (mTypeToQ m)`
\\ simp [Rabs_err_simpl, ABS_MUL]
\\ fs [typeCheck_def]
\\ `expTypes (Const m n) = SOME m`
by (Cases_on `expTypes (Const m n)` \\ fs [] \\ rveq)
\\ fs []
\\ match_mp_tac REAL_LE_TRANS
\\ irule REAL_LE_TRANS
\\ qexists_tac `maxAbs (nlo, nhi) * (mTypeToQ m)` \\ conj_tac \\ simp[]
\\ match_mp_tac REAL_LE_MUL2 \\ rpt (conj_tac) \\ TRY (simp[ABS_POS])
\\ simp[maxAbs_def]
\\ match_mp_tac maxAbs
\\ qspecl_then [`delta`] (fn thm => fs [thm]) delta_M0_deterministic
\\ qpat_x_assum `absenv _ = _` (fn thm => rule_assum_tac (fn thm2 => REWRITE_RULE [thm] thm2))
\\ simp[]);
\\ irule REAL_LE_MUL2 \\ rpt (conj_tac) \\ TRY (simp[ABS_POS])
\\ simp[maxAbs_def] \\ irule maxAbs
\\ qspecl_then [`delta`] (fn thm => fs [thm]) delta_M0_deterministic \\ fs[]);
val validErrorboundCorrectAddition = store_thm (
"validErrorboundCorrectAddition",
``!(E1 E2:env) (absenv:analysisResult) (e1:real exp) (e2:real exp)
(nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real) (alo ahi e1lo e1hi e2lo e2hi :real) dVars m m1 m2 expTypes Gamma.
``!(E1 E2:env) (A:analysisResult) (e1:real exp) (e2:real exp)
(nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real)
(alo ahi e1lo e1hi e2lo e2hi :real) dVars m m1 m2 expTypes Gamma.
(m = join m1 m2) /\
eval_exp E1 (toRMap Gamma) (toREval e1) nR1 M0 /\
eval_exp E1 (toRMap Gamma) (toREval e2) nR2 M0 /\
......@@ -274,21 +240,17 @@ val validErrorboundCorrectAddition = store_thm (
(updDefVars 2 m2 (updDefVars 1 m1 Gamma))
(Binop Plus (Var 1) (Var 2)) nF m /\
typeCheck (Binop Plus e1 e2) Gamma expTypes /\
validErrorbound (Binop Plus e1 e2) expTypes absenv dVars /\
FST (FST (absenv e1)) <= nR1 /\
nR1 <= SND (FST (absenv e1)) /\
FST (FST (absenv e2)) <= nR2 /\
nR2 <= SND (FST (absenv e2)) /\
(absenv e1 = ((e1lo,e1hi),err1)) /\
(absenv e2 = ((e2lo, e2hi),err2)) /\
(absenv (Binop Plus e1 e2) = ((alo,ahi),e)) /\
validErrorbound (Binop Plus e1 e2) expTypes A dVars /\
(e1lo <= nR1 /\ nR1 <= e1hi) /\
(e2lo <= nR2 /\ nR2 <= e2hi) /\
DaisyMapTree_find e1 A = SOME ((e1lo, e1hi), err1) /\
DaisyMapTree_find e2 A = SOME ((e2lo, e2hi), err2) /\
DaisyMapTree_find (Binop Plus e1 e2) A = SOME ((alo, ahi), e) /\
abs (nR1 - nF1) <= err1 /\
abs (nR2 - nF2) <= err2 ==>
abs (nR - nF) <= e``,
once_rewrite_tac [validErrorbound_def]
\\ rpt strip_tac \\ fs[]
\\ rw_asm `absenv _ = _`
\\ rw_asm `absenv e1 = _`
rpt strip_tac \\ simp[Once toREval_def]
\\ Daisy_compute ``validErrorbound``
\\ fs [Once typeCheck_def]
\\ Cases_on `expTypes (Binop Plus e1 e2)` \\ rveq \\ fs []
\\ Cases_on `expTypes e1` \\ rveq \\ fs []
......
hol4/ExpressionsScript.sml
View file @ 583f101f
......@@ -60,17 +60,15 @@ val _ = Datatype `
Errors are added on the expression evaluation level later
**)
val evalFma_def = Define `
evalFma v1 v2 v3 = evalBinop Plus v1 (evalBinop Mult v2 v3)`
evalFma v1 v2 v3 = evalBinop Plus v1 (evalBinop Mult v2 v3)`;
val toREval_def = Define `
toREval e :real exp =
case e of
| (Var n) => Var n
| (Const m n) => Const M0 n
| (Unop u e1) => Unop u (toREval e1)
| (Binop bop e1 e2) => Binop bop (toREval e1) (toREval e2)
| (Fma e1 e2 e3) => Fma (toREval e1) (toREval e2) (toREval e3)
| (Downcast m e1) => (toREval e1)`;
(toREval (Var n) = Var n) /\
(toREval (Const m n) = Const M0 n) /\
(toREval (Unop u e1) = Unop u (toREval e1)) /\
(toREval (Binop b e1 e2) = Binop b (toREval e1) (toREval e2)) /\
(toREval (Fma e1 e2 e3) = Fma (toREval e1) (toREval e2) (toREval e3)) /\
(toREval (Downcast m e1) = toREval e1)`;
(**
Define a perturbation function to ease writing of basic definitions
......@@ -245,7 +243,7 @@ val toRMap_eval_M0 = store_thm (
"toRMap_eval_M0",
``!f v E Gamma m.
eval_exp E (toRMap Gamma) (toREval f) v m ==> m = M0``,
Induct \\ simp[Once toREval_def] \\ fs[eval_exp_cases, toRMap_def]
Induct \\ fs[toREval_def] \\ fs[eval_exp_cases, toRMap_def]
\\ rpt strip_tac \\ fs[]
>- (every_case_tac \\ fs[])
>- (rveq \\ first_x_assum drule \\ strip_tac \\ fs[])
......
hol4/Infra/DaisyTactics.sml
View file @ 583f101f
......@@ -152,12 +152,21 @@ end;
(* This variable is supposed to hold all defined functions *)
val eval_funs:term list ref = ref [];
open TextIO;
val t = TextIO.openIn("/home/hbecker/Downloads/test.txt");
inputLine(t);
closeIn(t);
val t2 = openIn("./test.txt");
inputLine(t2);
output(t2, "ABC\n");
closeOut(t2);
fun add_unevaluated_function (t:term) :unit =
eval_funs := t :: (!eval_funs);
fun Daisy_compute t =
let
val eval_thm = DB.theorem ((term_to_string t)^"_def");
val eval_thm = fst (snd (hd (DB.find ((term_to_string t)^"_def"))));
val (pat,_) = getPatTerm t in
TRY (
Tactical.PAT_X_ASSUM
......
cakeml @ c760e35a
Compare 4273d509...c760e35a
Subproject commit 4273d509b99f86716a40d18895a091bbd043f24d
Subproject commit c760e35a371970c83a07a154bb67d4b842115a1f
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