Commit 4ba5b551 authored by Heiko Becker's avatar Heiko Becker

Get rid of calls of "inv" in computing expressions

parent ad293692
open preamble
open expressionsTheory
val _ = new_theory "ExpressionAbbrevs"
val _ = type_abbrev("analysisResult", ``:real exp->(interval # real)``);
val _ = export_theory()
......@@ -73,7 +73,7 @@ val negateInterval_def = Define `
negateInterval (iv:interval) = ((- IVhi iv), (- IVlo iv))`;
val invertInterval_def = Define `
invertInterval (iv:interval) = (inv (IVhi iv), inv (IVlo iv))`;
invertInterval (iv:interval) = (1 /(IVhi iv), 1 /(IVlo iv))`;
val addInterval_def = Define `
addInterval (iv1:interval) (iv2:interval) = absIntvUpd (+) iv1 iv2`;
......@@ -187,7 +187,7 @@ val interval_inversion_valid = store_thm ("interval_inversion_valid",
``!iv a.
(IVhi iv < 0 \/ 0 < IVlo iv) /\ contained a iv ==>
contained (inv a) (invertInterval iv)``,
fs iv_ss \\ rpt strip_tac
fs iv_ss \\ rpt strip_tac \\ once_rewrite_tac [GSYM REAL_INV_1OVER]
(* First subgoal *)
>- (once_rewrite_tac [GSYM REAL_LE_NEG] \\
`0 < - a` by REAL_ASM_ARITH_TAC \\
......
......@@ -11,7 +11,7 @@ open abbrevsTheory expressionsTheory RealSimpsTheory
open ExpressionAbbrevsTheory IntervalArithTheory
val _ = new_theory "IntervalValidation";
val freeVars_def = Define `
(freeVars (Const n) = []) /\
(freeVars (Var v) = []) /\
......@@ -158,7 +158,7 @@ gen_tac \\ Induct_on `f` \\ once_rewrite_tac [eval_exp_cases] \\ rpt gen_tac \\
Cases_on `absenv f` \\
qmatch_assum_rename_tac `absenv f = (iv_f, err_f)` \\
`absenv (Unop Inv f) = (iv_u,err_u)` by metis_tac [] \\
fs[evalUnop_def, isSupersetInterval_def, IVlo_def, IVhi_def, invertInterval_def] \\
fs[evalUnop_def, isSupersetInterval_def, IVlo_def, IVhi_def, invertInterval_def, GSYM REAL_INV_1OVER] \\
`FST iv_f <= v1 /\ v1 <= SND iv_f` by metis_tac [] \\
Cases_on `u`
>- (CCONTR_TAC \\ fs[])
......@@ -198,7 +198,7 @@ gen_tac \\ Induct_on `f` \\ once_rewrite_tac [eval_exp_cases] \\ rpt gen_tac \\
(fn thm => qspecl_then [`absenv`,`P`, `cenv`,`v1`] ASSUME_TAC thm) \\
qpat_x_assum `!absenv P cenv vR. validIntervalbounds f' absenv P /\ eval_exp 0 cenv P f' vR ==> R`
(fn thm => qspecl_then [`absenv`,`P`, `cenv`,`v2`] ASSUME_TAC thm) \\
Cases_on `b` \\ simp[evalBinop_def]
Cases_on `b` \\ simp[evalBinop_def]
(* Plus case *)
>- (Cases_on `absenv (Binop Plus f f')` \\ Cases_on `absenv f` \\ Cases_on `absenv f'` \\
qmatch_assum_rename_tac `absenv (Binop Plus f f') = (iv_b,err_b)` \\
......@@ -252,12 +252,12 @@ gen_tac \\ Induct_on `f` \\ once_rewrite_tac [eval_exp_cases] \\ rpt gen_tac \\
qmatch_assum_rename_tac `absenv (Binop Div f f') = (iv_b,err_b)` \\
qmatch_assum_rename_tac `absenv f = (iv_f,err_f)` \\
qmatch_assum_rename_tac `absenv f' = (iv_f',err_f')` \\
fs[evalBinop_def, isSupersetInterval_def, absIntvUpd_def, IVlo_def, IVhi_def, divideInterval_def, multInterval_def, invertInterval_def] \\
fs[evalBinop_def, isSupersetInterval_def, absIntvUpd_def, IVlo_def, IVhi_def, divideInterval_def, multInterval_def, invertInterval_def, GSYM REAL_INV_1OVER] \\
`FST iv_f <= v1 /\ v1 <= SND iv_f` by metis_tac [] \\
`FST iv_f' <= v2 /\ v2 <= SND iv_f'` by metis_tac [] \\
qspecl_then [`iv_f`, `iv_f'`, `v1`, `v2`] ASSUME_TAC
(REWRITE_RULE
[validIntervalSub_def, divideInterval_def, multInterval_def, invertInterval_def, absIntvUpd_def, contained_def, IVhi_def, IVlo_def]interval_division_valid) \\
[validIntervalSub_def, divideInterval_def, multInterval_def, invertInterval_def, absIntvUpd_def, contained_def, IVhi_def, IVlo_def, GSYM REAL_INV_1OVER]interval_division_valid) \\
conj_tac \\ match_mp_tac REAL_LE_TRANS
>- (qexists_tac `min4 (FST iv_f * (inv (SND iv_f')))
(FST iv_f * (inv (FST iv_f'))) (SND iv_f * (inv (SND iv_f'))) (SND iv_f * (inv (FST iv_f')))` \\
......
open preamble
open realTheory realLib
val _ = new_theory "abbrevs";
(**
For the moment we need only one interval type in HOL, since we do not have the
problem of computability as we have it in Coq
**)
val _ = type_abbrev("interval", ``:real#real``);
val IVlo_def = Define `IVlo (iv:interval) = FST iv`;
val IVhi_def = Define `IVhi (iv:interval) = SND iv`;
val _ = type_abbrev("ann", ``:interval#real``);
(**
Later we will argue about program preconditions.
Define a precondition to be a function mapping numbers (resp. variables) to intervals.
**)
val _ = type_abbrev ("precond", ``:num->interval``);
(**
Abbreviations for the environment types
**)
val _ = type_abbrev("env",``:num->real``);
(**
Define environment update function as abbreviation.
**)
val updEnv_def = Define `
updEnv (x:num) (v:real) (E:env) (y:num) :real = if y = x then v else E y`;
val - = export_theory();
open preamble
open realTheory realLib
open abbrevsTheory
val _ = ParseExtras.temp_tight_equality()
val _ = new_theory "expressions";
(**
Expressions will use binary operators.
Define them first
**)
val _ = Datatype `
binop = Plus | Sub | Mult | Div`;
(**
Next define an evaluation function for binary operators.
Errors are added on the expression evaluation level later
*)
val evalBinop_def = Define `
evalBinop Plus v1 v2 = v1 + v2 /\
evalBinop Sub v1 v2 = v1 - v2 /\
evalBinop Mult v1 v2 = v1 * v2 /\
evalBinop Div v1 v2 = v1 / (v2:real)`;
(**
Expressions will use unary operators.
Define them first
**)
val _ = Datatype `
unop = Neg | Inv`
(**
Define evaluation for unary operators on reals.
Errors are added in the expression evaluation level later
**)
val evalUnop_def = Define `
evalUnop Neg v = - v /\
evalUnop Inv v = inv(v:real)`
(**
Define expressions parametric over some value type 'v. Will ease
reasoning about different instantiations later. Note that we
differentiate between whether we use a variable from the environment
or a parameter. Parameters do not have error bounds in the
invariants, so they must be perturbed, but variables from the
program will be perturbed upon binding, so we do not need to perturb
them.
**)
val _ = Datatype `
exp = Var num
| Param num
| Const 'v
| Unop unop exp
| Binop binop exp exp`
(**
Define a perturbation function to ease writing of basic definitions
**)
val perturb_def = Define `
perturb (r:real) (e:real) = r * (1 + e)`
(**
Define expression evaluation relation parametric by an "error"
delta. This value will be used later to express float computations
using a perturbation of the real valued computation by (1 + d)
**)
val (eval_exp_rules, eval_exp_ind, eval_exp_cases) = Hol_reln `
(!eps E (P:num->(real # real)) x.
eval_exp eps E P (Var x) (E x)) /\
(!eps E P x delta.
abs delta <= eps /\
FST (P x) <= perturb (E x) delta /\
perturb (E x) delta <= SND (P x) ==>
eval_exp eps E P (Param x) (perturb (E x) delta)) /\
(!eps E P delta.
abs delta <= eps ==>
eval_exp eps E P (Const n) (perturb n delta)) /\
(!eps E P f1 v1.
eval_exp eps E P f1 v1 ==>
eval_exp eps E P (Unop Neg f1) (evalUnop Neg v1)) /\
(!eps E P f1 v1 delta.
abs delta <= eps /\
eval_exp eps E P f1 v1 ==>
eval_exp eps E P (Unop Inv f1) (perturb (evalUnop Inv v1) delta)) /\
(!eps E P b f1 f2 v1 v2 delta.
abs delta <= eps /\
eval_exp eps E P f1 v1 /\
eval_exp eps E P f2 v2 ==>
eval_exp eps E P (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta))`;
val eval_exp_cases =
map (GEN_ALL o SIMP_CONV (srw_ss()) [Once eval_exp_cases])
[``eval_exp eps E P (Var v) res``,
``eval_exp eps E P (Param v) res``,
``eval_exp eps E P (Const n) res``,
``eval_exp eps E P (Unop u e) res``,
``eval_exp eps E P (Binop n e1 e2) res``]
|> LIST_CONJ |> curry save_thm "eval_exp_cases";
val delta_0_deterministic = store_thm("delta_0_deterministic",
``!(v:real) (delta:real). abs delta <= 0 ==> perturb v delta = v``,
fs [perturb_def,ABS_BOUNDS,REAL_LE_ANTISYM]);
val meps_0_deterministic = store_thm("meps_0_deterministic",
``!(e: real exp) v1:real v2:real E P.
eval_exp (&0) E P e v1 /\ eval_exp (&0) E P e v2 ==> v1 = v2``,
Induct \\ fs [eval_exp_cases]
\\ rw [] \\ fs [delta_0_deterministic]
\\ res_tac \\ fs []);
(*
Using the parametric expressions, define boolean expressions for conditionals
*)
val _ = Datatype `
bexp = Leq ('v exp) ('v exp)
| Less ('v exp) ('v exp)`
(*
Define evaluation of boolean expressions
*)
val (bval_exp_rules, bval_exp_ind, bval_exp_cases) = Hol_reln `
(!eps E P e1 e2 v1 v2.
eval_exp eps E P e1 v1 /\
eval_exp eps E P e2 v2 ==>
bval eps E P (Leq e1 e2) (v1 <= v2))/\
(!eps E P e1 e2 v1 v2.
eval_exp eps E P e1 v1 /\
eval_exp eps E P e2 v2 ==>
bval eps E P (Less e1 e2) (v1 < v2))`;
val bval_exp_cases =
map (GEN_ALL o SIMP_CONV (srw_ss()) [Once bval_exp_cases])
[``bval eps E P (Leq e1 e2) res``,
``bval eps E P (Less e1 e2) res``]
|> LIST_CONJ |> curry save_thm "bval_exp_cases";
(* Simplify arithmetic later by making > >= only abbreviations *)
val _ = overload_on("Gr",``\(e1:('v)exp). \(e2:('v)exp). Less e2 e1``);
val _ = overload_on("Greq",``\(e1:('v)exp). \(e2:('v)exp). Leq e2 e1``);
(**
Helping lemma. 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.
This relies on the property that variables are not perturbed as opposed to parameters
**)
val binary_unfolding = store_thm("binary_unfolding",
``!(b:binop) (e1:(real)exp) (e2:(real)exp) (eps:real) (cenv:env) (P:precond) (v:real).
(eval_exp eps cenv P (Binop b e1 e2) v <=>
(?(v1:real) (v2:real).
eval_exp eps cenv P e1 v1 /\
eval_exp eps cenv P e2 v2 /\
eval_exp eps (updEnv 2 v2 (updEnv 1 v1 cenv)) P (Binop b (Var 1) (Var 2)) v))``,
fs [updEnv_def, eval_exp_cases,APPLY_UPDATE_THM,PULL_EXISTS]
\\ metis_tac []);
val _ = export_theory();
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple ../
OPTIONS = QUIT_ON_FAILURE
open CertificateCheckerTheory;
val ExpCst1 = Define `ExpCst1:(real exp) = Const ((1657)/(5))`;
val ExpVaru = Define `ExpVaru:(real exp) = Param 1`;
val PlusExpCst1ExpVaru = Define `PlusExpCst1ExpVaru:(real exp) = Binop Plus ExpCst1 ExpVaru`;;
val thePrecondition_def = Define `
thePrecondition (n:num) =
if n = 1 then ( (-100)/(1), (100)/(1)) else (0,1)`;
val absenv_def = Define `absenv:analysisResult =
\e.
if e = PlusExpCst1ExpVaru then (( (1157)/(5), (2157)/(5)),(7771411516990528329)/(81129638414606681695789005144064))
else if e = ExpVaru then (( (-100)/(1), (100)/(1)),(25)/(2251799813685248))
else if e = ExpCst1 then (( (1657)/(5), (1657)/(5)),(1657)/(45035996273704960))
else ((0,1),1)`;
EVAL ``CertificateChecker PlusExpCst1ExpVaru absenv thePrecondition``;
\ No newline at end of file
open CertificateCheckerTheory;
open simpLib realTheory realLib RealArith;
val ExpCst1 = Define `ExpCst1:(real exp) = Const ((1657)/(5))`;
val ExpVaru = Define `ExpVaru:(real exp) = Param 1`;
val DivExpCst1ExpVaru = Define `DivExpCst1ExpVaru:(real exp) = Binop Div ExpCst1 ExpVaru`;;
val thePrecondition_def = Define `
thePrecondition (n:num) =
if n = 1 then ( (1)/(1), (100)/(1)) else (0,1)`;
val absenv_def = Define `absenv:analysisResult =
\e.
if e = DivExpCst1ExpVaru then (( (1657)/(500), (1657)/(5)),(1543838985824032326958855430137511160223694676240661)/(411376139330292376153508977546804877224608665699390244473798656))
else if e = ExpVaru then (( (1)/(1), (100)/(1)),(25)/(2251799813685248))
else if e = ExpCst1 then (( (1657)/(5), (1657)/(5)),(1657)/(45035996273704960))
else ((0,1),1)`;
val test = EVAL ``CertificateChecker DivExpCst1ExpVaru absenv thePrecondition``;
open CertificateCheckerTheory;
open simpLib realTheory realLib RealArith;
val ExpCst1 = Define `ExpCst1:(real exp) = Const ((100)/(1))`;
val ExpVaru = Define `ExpVaru:(real exp) = Param 1`;
val MultExpCst1ExpVaru = Define `MultExpCst1ExpVaru:(real exp) = Binop Mult ExpCst1 ExpVaru`;;
val thePrecondition_def = Define `
thePrecondition (n:num) =
if n = 1 then ( (-100)/(1), (100)/(1)) else (0,1)`;
val absenv_def = Define `absenv:analysisResult =
\e.
if e = MultExpCst1ExpVaru then (( (-10000)/(1), (10000)/(1)),(152118072027387545068102987284480625)/(45671926166590716193865151022383844364247891968))
else if e = ExpVaru then (( (-100)/(1), (100)/(1)),(25)/(2251799813685248))
else if e = ExpCst1 then (( (100)/(1), (100)/(1)),(25)/(2251799813685248))
else ((0,1),1)`;
val _ = store_thm ("ErrorBoundSound",
``CertificateChecker MultExpCst1ExpVaru absenv thePrecondition``,
EVAL_TAC);
\ No newline at end of file
open CertificateCheckerTheory;
val ExpCst1 = Define `ExpCst1:(real exp) = Const ((1657)/(5))`;
val ExpVaru = Define `ExpVaru:(real exp) = Param 1`;
val SubExpCst1ExpVaru = Define `SubExpCst1ExpVaru:(real exp) = Binop Sub ExpCst1 ExpVaru`;;
val thePrecondition_def = Define `
thePrecondition (n:num) =
if n = 1 then ( (-100)/(1), (100)/(1)) else (0,1)`;
val absenv_def = Define `absenv:analysisResult =
\e.
if e = SubExpCst1ExpVaru then (( (1157)/(5), (2157)/(5)),(7771411516990528329)/(81129638414606681695789005144064))
else if e = ExpVaru then (( (-100)/(1), (100)/(1)),(25)/(2251799813685248))
else if e = ExpCst1 then (( (1657)/(5), (1657)/(5)),(1657)/(45035996273704960))
else ((0,1),1)`;
EVAL ``CertificateChecker SubExpCst1ExpVaru absenv thePrecondition``;
\ No newline at end of file
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