Skip to content
GitLab
Commit 12f88723 authored by Heiko Becker's avatar Heiko Becker
Browse files

Intermediate state

parent 5a079f2d
Hide whitespace changes
Inline Side-by-side
hol4/EnvironmentsScript.sml
View file @ 12f88723
......@@ -2,9 +2,13 @@ open preamble
open simpLib realTheory realLib RealArith
open abbrevsTheory ExpressionAbbrevsTheory CommandsTheory
val _ = new_theory "Environments";
val (approxEnv_rules, approxEnv_ind, approxEnv_cases) = Hol_reln `
(!(E:env) (A:analysisResult). approxEnv E A E) /\
(!(E1:env) (E2:env) (A:analysisResult) v1 v2 x.
approxEnv E1 A E2 /\
(abs (v1 - v2) <= SND (A (Var x))) ==>
approxEnv (updEnv x v1 E1) A (updEnv x v2 E2))`;
val _ = export_theory ();;
hol4/ErrorBoundsScript.sml
View file @ 12f88723
......@@ -11,50 +11,55 @@ open ExpressionAbbrevsTheory EnvironmentsTheory
val _ = new_theory "ErrorBounds";
val const_abs_err_bounded = store_thm ("const_abs_err_bounded",
``!(P:precond) (n:real) (nR:real) (nF:real) (cenv:env).
eval_exp 0 cenv P (Const n) nR /\ eval_exp machineEpsilon cenv P (Const n) nF ==>
abs (nR - nF) <= abs n * machineEpsilon``,
``!(P:precond) (n:real) (nR:real) (nF:real) (VarEnv1 VarEnv2 ParamEnv:env) (absenv:analysisResult).
approxEnv VarEnv1 absenv VarEnv2 /\
eval_exp 0 VarEnv1 ParamEnv P (Const n) nR /\
eval_exp machineEpsilon VarEnv2 ParamEnv P (Const n) nF ==>
abs (nR - nF) <= abs n * machineEpsilon``,
rpt strip_tac \\
fs[eval_exp_cases] \\
`perturb n delta = n` by metis_tac[delta_0_deterministic] \\
`nR = n` by fs[]\\
simp[perturb_def, Rabs_err_simpl, REAL_ABS_MUL] \\
match_mp_tac REAL_LE_LMUL_IMP \\ REAL_ASM_ARITH_TAC );
match_mp_tac REAL_LE_LMUL_IMP \\ REAL_ASM_ARITH_TAC);
val param_abs_err_bounded = store_thm ("param_abs_err_bounded",
``!(P:precond) (n:num) (nR:real) (nF:real) (cenv:env).
eval_exp 0 cenv P (Param n) nR /\ eval_exp machineEpsilon cenv P (Param n) nF ==>
abs (nR - nF) <= abs (cenv n) * machineEpsilon``,
``!(P:precond) (n:num) (nR:real) (nF:real) (VarEnv1 VarEnv2 ParamEnv:env) (absenv:analysisResult).
approxEnv VarEnv1 absenv VarEnv2 /\
eval_exp 0 VarEnv1 ParamEnv P (Param n) nR /\
eval_exp machineEpsilon VarEnv2 ParamEnv P (Param n) nF ==>
abs (nR - nF) <= abs (ParamEnv n) * machineEpsilon``,
rpt strip_tac \\
fs[eval_exp_cases] \\
`perturb (cenv n) delta = (cenv n)` by metis_tac[delta_0_deterministic] \\
`nR = (cenv n)` by fs[]\\
`perturb (ParamEnv n) delta = (ParamEnv n)` by metis_tac[delta_0_deterministic] \\
`nR = (ParamEnv n)` by fs[]\\
simp[perturb_def, Rabs_err_simpl, REAL_ABS_MUL] \\
match_mp_tac REAL_LE_LMUL_IMP \\ REAL_ASM_ARITH_TAC);
val add_abs_err_bounded = store_thm ("add_abs_err_bounded",
``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real)
(vR:real) (vF:real) (cenv:num->real) (P:precond) (err1:real) (err2:real).
eval_exp 0 cenv P e1 e1R /\
eval_exp machineEpsilon cenv P e1 e1F /\
eval_exp 0 cenv P e2 e2R /\
eval_exp machineEpsilon cenv P e2 e2F /\
eval_exp 0 cenv P (Binop Plus e1 e2) vR /\
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F cenv)) P (Binop Plus (Var 1) (Var 2)) vF /\
``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real) (err1:real) (err2:real)
(vR:real) (vF:real) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond) (absenv:analysisResult).
approxEnv VarEnv1 absenv VarEnv2 /\
eval_exp 0 VarEnv1 ParamEnv P e1 e1R /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e1 e1F /\
eval_exp 0 VarEnv1 ParamEnv P e2 e2R /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e2 e2F /\
eval_exp 0 VarEnv1 ParamEnv P (Binop Plus e1 e2) vR /\
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Plus (Var 1) (Var 2)) vF /\
abs (e1R - e1F) <= err1 /\
abs (e2R - e2F) <= err2 ==>
abs (vR - vF) <= err1 + err2 + (abs (e1F + e2F) * machineEpsilon)``,
rpt strip_tac \\
inversion `eval_exp 0 cenv P (Binop Plus e1 e2) vR` eval_exp_cases \\
inversion `eval_exp 0 VarEnv1 ParamEnv P (Binop Plus e1 e2) vR` eval_exp_cases \\
rename1 `vR = perturb (evalBinop Plus v1R v2R) deltaR` \\
inversion `eval_exp machineEpsilon E P (Binop Plus (Var 1) (Var 2)) vF` eval_exp_cases \\
inversion `eval_exp machineEpsilon _ _ P (Binop Plus (Var 1) (Var 2)) vF` eval_exp_cases \\
rename1 `vF = perturb (evalBinop Plus v1F v2F) deltaF` \\
`perturb (evalBinop Plus v1R v2R) deltaR = evalBinop Plus v1R v2R` by (match_mp_tac delta_0_deterministic \\ fs[]) \\
`vR = evalBinop Plus v1R v2R` by simp[] \\
`v1R = e1R` by metis_tac[meps_0_deterministic] \\
`v2R = e2R` by metis_tac[meps_0_deterministic] \\
fs[evalBinop_def, perturb_def] \\
rpt (inversion `eval_exp machineEpsilon (updEnv n e E) P expr vE` eval_exp_cases) \\
rpt (inversion `eval_exp machineEpsilon (updEnv n e E) _ P expr vE` eval_exp_cases) \\
fs [updEnv_def]\\
once_rewrite_tac[real_sub] \\
`e1R + e2R + -((e1F + e2F) * (1 + deltaF)) = (e1R + - e1F) + ((e2R + - e2F) + - (e1F + e2F) * deltaF)` by REAL_ASM_ARITH_TAC \\
......@@ -73,28 +78,29 @@ val add_abs_err_bounded = store_thm ("add_abs_err_bounded",
fs [REAL_ABS_POS, ABS_NEG]);
val subtract_abs_err_bounded = store_thm ("subtract_abs_err_bounded",
``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real)
(vR:real) (vF:real) (cenv:num->real) (P:precond) (err1:real) (err2:real).
eval_exp 0 cenv P e1 e1R /\
eval_exp machineEpsilon cenv P e1 e1F /\
eval_exp 0 cenv P e2 e2R /\
eval_exp machineEpsilon cenv P e2 e2F /\
eval_exp 0 cenv P (Binop Sub e1 e2) vR /\
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F cenv)) P (Binop Sub (Var 1) (Var 2)) vF /\
``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real) (err1:real) (err2:real)
(vR:real) (vF:real) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond) (absenv:analysisResult).
approxEnv VarEnv1 absenv VarEnv2 /\
eval_exp 0 VarEnv1 ParamEnv P e1 e1R /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e1 e1F /\
eval_exp 0 VarEnv1 ParamEnv P e2 e2R /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e2 e2F /\
eval_exp 0 VarEnv1 ParamEnv P (Binop Sub e1 e2) vR /\
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Sub (Var 1) (Var 2)) vF /\
abs (e1R - e1F) <= err1 /\
abs (e2R - e2F) <= err2 ==>
abs (vR - vF) <= err1 + err2 + (abs (e1F - e2F) * machineEpsilon)``,
rpt strip_tac \\
inversion `eval_exp 0 cenv P (Binop Subs e1 e2) vR` eval_exp_cases \\
inversion `eval_exp 0 _ _ P (Binop Subs e1 e2) vR` eval_exp_cases \\
rename1 `vR = perturb (evalBinop Sub v1R v2R) deltaR` \\
inversion `eval_exp machineEpsilon E P (Binop Sub (Var 1) (Var 2)) vF` eval_exp_cases \\
inversion `eval_exp machineEpsilon _ _ P (Binop Sub (Var 1) (Var 2)) vF` eval_exp_cases \\
rename1 `vF = perturb (evalBinop Sub v1F v2F) deltaF` \\
`perturb (evalBinop Sub v1R v2R) deltaR = evalBinop Sub v1R v2R` by (match_mp_tac delta_0_deterministic \\ fs[]) \\
`vR = evalBinop Sub v1R v2R` by simp[] \\
`v1R = e1R` by metis_tac[meps_0_deterministic] \\
`v2R = e2R` by metis_tac[meps_0_deterministic] \\
fs[evalBinop_def, perturb_def] \\
rpt (inversion `eval_exp machineEpsilon (updEnv n e E) P expr vE` eval_exp_cases) \\
rpt (inversion `eval_exp machineEpsilon (updEnv n e E) _ P expr vE` eval_exp_cases) \\
fs [updEnv_def]\\
rewrite_tac[real_sub] \\
`e1R + -e2R + -((e1F + -e2F) * (1 + deltaF)) = (e1R + - e1F) + ((- e2R + e2F) + - (e1F + - e2F) * deltaF)` by REAL_ASM_ARITH_TAC \\
......@@ -116,28 +122,29 @@ val subtract_abs_err_bounded = store_thm ("subtract_abs_err_bounded",
fs [REAL_ABS_POS, ABS_NEG]));
val mult_abs_err_bounded = store_thm ("mult_abs_err_bounded",
``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real)
(vR:real) (vF:real) (cenv:num->real) (P:precond) (err1:real) (err2:real).
eval_exp 0 cenv P e1 e1R /\
eval_exp machineEpsilon cenv P e1 e1F /\
eval_exp 0 cenv P e2 e2R /\
eval_exp machineEpsilon cenv P e2 e2F /\
eval_exp 0 cenv P (Binop Mult e1 e2) vR /\
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F cenv)) P (Binop Mult (Var 1) (Var 2)) vF /\
``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real) (err1:real) (err2:real)
(vR:real) (vF:real) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond) (absenv:analysisResult).
approxEnv VarEnv1 absenv VarEnv2 /\
eval_exp 0 VarEnv1 ParamEnv P e1 e1R /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e1 e1F /\
eval_exp 0 VarEnv1 ParamEnv P e2 e2R /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e2 e2F /\
eval_exp 0 VarEnv1 ParamEnv P (Binop Mult e1 e2) vR /\
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Mult (Var 1) (Var 2)) vF /\
abs (e1R - e1F) <= err1 /\
abs (e2R - e2F) <= err2 ==>
abs (vR - vF) <= abs (e1R * e2R - e1F * e2F) + (abs (e1F * e2F) * machineEpsilon)``,
rpt strip_tac \\
inversion `eval_exp 0 cenv P (Binop Mult e1 e2) vR` eval_exp_cases \\
inversion `eval_exp 0 _ _ P (Binop Mult e1 e2) vR` eval_exp_cases \\
rename1 `vR = perturb (evalBinop Mult v1R v2R) deltaR`\\
inversion `eval_exp machineEpsilon E P (Binop Mult (Var 1) (Var 2)) v` eval_exp_cases \\
inversion `eval_exp machineEpsilon _ _ P (Binop Mult (Var 1) (Var 2)) v` eval_exp_cases \\
rename1 `vF = perturb (evalBinop Mult v1F v2F) deltaF` \\
`perturb (evalBinop Mult v1R v2R) deltaR = evalBinop Mult v1R v2R` by (match_mp_tac delta_0_deterministic \\ fs[]) \\
`vR = evalBinop Mult v1R v2R` by simp[] \\
`v1R = e1R` by metis_tac[meps_0_deterministic] \\
`v2R = e2R` by metis_tac[meps_0_deterministic] \\
fs[evalBinop_def, perturb_def] \\
rpt (inversion `eval_exp machineEpsilon (updEnv n e E) P expr vE` eval_exp_cases) \\
rpt (inversion `eval_exp machineEpsilon (updEnv n e E) _ P expr vE` eval_exp_cases) \\
fs [updEnv_def] \\
rewrite_tac [real_sub] \\
`e1R * e2R + -(e1F * e2F * (1 + deltaF)) = (e1R * e2R + - (e1F * e2F)) + - (e1F * e2F * deltaF)` by REAL_ASM_ARITH_TAC \\
......@@ -153,28 +160,29 @@ val mult_abs_err_bounded = store_thm ("mult_abs_err_bounded",
once_rewrite_tac[ABS_NEG] \\ fs[]));
val div_abs_err_bounded = store_thm ("div_abs_err_bounded",
``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real)
(vR:real) (vF:real) (cenv:num->real) (P:precond) (err1:real) (err2:real).
eval_exp 0 cenv P e1 e1R /\
eval_exp machineEpsilon cenv P e1 e1F /\
eval_exp 0 cenv P e2 e2R /\
eval_exp machineEpsilon cenv P e2 e2F /\
eval_exp 0 cenv P (Binop Div e1 e2) vR /\
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F cenv)) P (Binop Div (Var 1) (Var 2)) vF /\
``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real) (err1:real) (err2:real)
(vR:real) (vF:real) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond) (absenv:analysisResult).
approxEnv VarEnv1 absenv VarEnv2 /\
eval_exp 0 VarEnv1 ParamEnv P e1 e1R /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e1 e1F /\
eval_exp 0 VarEnv1 ParamEnv P e2 e2R /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e2 e2F /\
eval_exp 0 VarEnv1 ParamEnv P (Binop Div e1 e2) vR /\
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Div (Var 1) (Var 2)) vF /\
abs (e1R - e1F) <= err1 /\
abs (e2R - e2F) <= err2 ==>
abs (vR - vF) <= abs (e1R / e2R - e1F / e2F) + (abs (e1F / e2F) * machineEpsilon)``,
rpt strip_tac \\
inversion `eval_exp 0 cenv P (Binop Div e1 e2) vR` eval_exp_cases \\
inversion `eval_exp 0 _ _ P (Binop Div e1 e2) vR` eval_exp_cases \\
rename1 `vR = perturb (evalBinop Div v1R v2R) deltaR`\\
inversion `eval_exp machineEpsilon E P (Binop Div (Var 1) (Var 2)) v` eval_exp_cases \\
inversion `eval_exp machineEpsilon _ _ P (Binop Div (Var 1) (Var 2)) v` eval_exp_cases \\
rename1 `vF = perturb (evalBinop Div v1F v2F) deltaF` \\
`perturb (evalBinop Div v1R v2R) deltaR = evalBinop Div v1R v2R` by (match_mp_tac delta_0_deterministic \\ fs[]) \\
`vR = evalBinop Div v1R v2R` by simp[] \\
`v1R = e1R` by metis_tac[meps_0_deterministic] \\
`v2R = e2R` by metis_tac[meps_0_deterministic] \\
fs[evalBinop_def, perturb_def] \\
rpt (inversion `eval_exp machineEpsilon (updEnv n e E) P expr vE` eval_exp_cases) \\
rpt (inversion `eval_exp machineEpsilon (updEnv n e E) _ P expr vE` eval_exp_cases) \\
fs [updEnv_def] \\
rewrite_tac [real_sub] \\
`e1R / e2R + -(e1F / e2F * (1 + deltaF)) = (e1R / e2R + - (e1F / e2F)) + - (e1F / e2F * deltaF)` by REAL_ASM_ARITH_TAC \\
......@@ -186,7 +194,7 @@ val div_abs_err_bounded = store_thm ("div_abs_err_bounded",
conj_tac \\ TRY (REAL_ASM_ARITH_TAC) \\
once_rewrite_tac [ABS_NEG] \\
once_rewrite_tac[REAL_ABS_MUL] \\
match_mp_tac REAL_LE_MUL2 \\ fs[REAL_ABS_POS] ));
match_mp_tac REAL_LE_MUL2 \\ fs[REAL_ABS_POS]));
val err_prop_inversion_pos = store_thm ("err_prop_inversion_pos",
``!(nF:real) (nR:real) (err:real) (elo:real) (ehi:real).
......
hol4/ErrorValidationScript.sml
View file @ 12f88723
......@@ -10,7 +10,7 @@ open preamble
open simpLib realTheory realLib RealArith
open abbrevsTheory expressionsTheory RealSimpsTheory
open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
open IntervalValidationTheory
open IntervalValidationTheory EnvironmentsTheory
val _ = new_theory "ErrorValidation";
......@@ -19,7 +19,7 @@ validErrorbound e (absenv:analysisResult) =
let (intv, err) = absenv e in
let errPos = 0 <= err in
case e of
| Var v => F
| Var v => errPos
| Param v => (errPos /\ (maxAbsFun intv * machineEpsilon <= err))
| Const n => (errPos /\ (maxAbsFun intv * machineEpsilon <= err))
| Unop op f => F
......@@ -46,15 +46,46 @@ let (intv, err) = absenv e in
else F
in rec /\ errPos /\ theVal`;
val validErrorboundCmd_def = Define `
validErrorboundCmd (f:real cmd) (env:analysisResult) =
case f of
| Let x e g =>
validErrorbound e env /\
(env e = env (Var x)) /\
validErrorboundCmd g env
| Ret e =>
validErrorbound e env /\
(env e = env (Var 0))
| Nop => F`;
val err_always_positive = store_thm ("err_always_positive",
``!(e:real exp) (absenv:analysisResult) (iv:interval) (err:real).
(validErrorbound (e:real exp) (absenv:analysisResult)) /\ ((iv,err) = absenv e) ==>
(validErrorbound (e:real exp) (absenv:analysisResult)) /\
((iv,err) = absenv e) ==>
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 `absenv e0` \\ Cases_on `absenv e'` \\ fs[]);
val validErrorboundCorrectVariable = store_thm ("validErrorboundCorrectVariable",
``!(VarEnv1 VarEnv2 ParamEnv:env) (absenv:analysisResult) (v:num)
(nR nF err nlo nhi:real) (P:precond).
approxEnv VarEnv1 absenv VarEnv2 /\
eval_exp 0 VarEnv1 ParamEnv P (Var v) nR /\
eval_exp machineEpsilon VarEnv2 ParamEnv P (Var v) nF /\
validErrorbound (Var v) absenv /\
(absenv (Var v) = ((nlo, nhi),err)) ==>
abs (nR - nF) <= err``,
once_rewrite_tac [validErrorbound_def] \\
Induct_on `` \\
rpt strip_tac \\
inversion `eval_exp 0 _ _ _ _ _` eval_exp_cases \\
inversion `eval_exp machineEpsilon _ _ _ _ _` eval_exp_cases \\
fs[] \\
>- (rpt strip_tac \\)
>- ()
val validErrorboundCorrectConstant = store_thm ("validErrorboundCorrectConstant",
``!(cenv:env) (absenv:analysisResult) (n:real) (nR:real) (nF:real) (e:real) (nlo:real) (nhi:real) (P:precond).
eval_exp 0 cenv P (Const n) nR /\
......
Supports Markdown
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