Commit f677adf0 authored by Heiko Becker's avatar Heiko Becker

Start working on interval checker

parent ff3f460d
(**
Interval arithmetic checker and its soundness proof.
The function validIntervalbounds checks wether the given analysis result is
a valid range arithmetic for each sub term of the given expression e.
The computation is done using our formalized interval arithmetic.
The function is used in CertificateChecker.v to build the full checker.
**)
open preamble
open realTheory realLib RealArith simpLib
open abbrevsTheory expressionsTheory RealSimpsTheory IntervalArithTheory;
val freeVars_def = Define `
(freeVars (Const n) = []) /\
(freeVars (Var v) = []) /\
(freeVars (Param v) = [v] ) /\
(freeVars (Unop op f1) = freeVars f1) /\
(freeVars (Binop op f1 f2) = APPEND (freeVars f1) (freeVars f2))`;
val validIntervalbounds_def = Define `
validIntervalbounds e (absenv:analysisResult) (P:precond) =
let (intv, _) = absenv e in
case e of
| Var v => F
| Param v => isSupersetInterval (P v) intv
| Const n => isSupersetInterval (n,n) intv
| Unop op f =>
let rec = validIntervalbounds f absenv P in
let (iv, _) = absenv f in
let opres = case op of
| Neg =>
let new_iv = negateInterval iv in
isSupersetInterval new_iv intv
| Inv =>
let nodiv0 = IVhi iv < 0 \/ 0 < IVlo iv in
let new_iv = invertInterval iv in
isSupersetInterval new_iv intv /\ nodiv0
in
rec /\ opres
| Binop op f1 f2 =>
let rec = (validIntervalbounds f1 absenv P /\ validIntervalbounds f2 absenv P) in
let (iv1, _ ) = absenv f1 in
let (iv2, _) = absenv f2 in
let opres = case op of
| Plus =>
let new_iv = addInterval iv1 iv2 in
isSupersetInterval new_iv intv
| Sub =>
let new_iv = subtractInterval iv1 iv2 in
isSupersetInterval new_iv intv
| Mult =>
let new_iv = multInterval iv1 iv2 in
isSupersetInterval new_iv intv
| Div =>
let nodiv0 = IVhi iv2 < 0 \/ 0 < IVlo iv2 in
let new_iv = divideInterval iv1 iv2 in
isSupersetInterval new_iv intv /\ nodiv0
in
rec /\ opres `;
val ivbounds_approximatesPrecond_sound = store_thm ("ivbounds_approximatesPrecond_sound",
``!(f:real exp) (absenv:analysisResult) (P:precond).
validIntervalbounds f absenv P ==>
(!(v:num). MEM v (freeVars f) ==>
isSupersetInterval (P v) (FST (absenv (Param v))))``,
Induct_on `f` \\ REPEAT STRIP_TAC \\ fs [freeVars_def]
>- (RULE_ASSUM_TAC (ONCE_REWRITE_RULE [validIntervalbounds_def]) \\
`?(iv1:interval) (err1:real). (absenv:analysisResult) (Param n) = (iv1,err1)` by metis_tac [pair_CASES] \\
fs[] )
>- (FIRST_X_ASSUM (Q.SPEC_THEN `absenv` (Q.SPEC_THEN `P` ASSUME_TAC)) \\
UNDISCH_TAC `` MEM (v :num) (freeVars (f :real exp))`` \\
FIRST_X_ASSUM MATCH_MP_TAC \\
PAT_ASSUM ``validIntervalbounds (Unop (u :unop) (f :real exp)) (absenv :analysisResult) (P :precond)``
(fn th => ASSUME_TAC (ASM_SIMP_RULE bool_ss [] (ONCE_REWRITE_RULE [validIntervalbounds_def] th))) \\
ASM_SIMP_TAC bool_ss[] \\
Cases_on `absenv (Unop u f)` \\
Cases_on `u` \\ Cases_on `absenv f` \\ fs[])
>- (REPEAT (FIRST_X_ASSUM (Q.SPEC_THEN `absenv` (Q.SPEC_THEN `P` ASSUME_TAC))) \\
UNDISCH_TAC `` MEM (v :num) (freeVars (f :real exp))`` \\
FIRST_X_ASSUM MATCH_MP_TAC \\
PAT_ASSUM ``validIntervalbounds (Binop (b :binop) (f :real exp) f') (absenv :analysisResult) (P :precond)``
(fn th => ASSUME_TAC (ASM_SIMP_RULE bool_ss [] (ONCE_REWRITE_RULE [validIntervalbounds_def] th))) \\
ASM_SIMP_TAC bool_ss[] \\
Cases_on `absenv (Binop b f f')` \\
Cases_on `b` \\ Cases_on `absenv f` \\ Cases_on `absenv f'` \\ fs[])
>- (REPEAT (FIRST_X_ASSUM (Q.SPEC_THEN `absenv` (Q.SPEC_THEN `P` ASSUME_TAC))) \\
UNDISCH_TAC `` MEM (v :num) (freeVars (f' :real exp))`` \\
FIRST_X_ASSUM MATCH_MP_TAC \\
PAT_ASSUM ``validIntervalbounds (Binop (b :binop) (f :real exp) f') (absenv :analysisResult) (P :precond)``
(fn th => ASSUME_TAC (ASM_SIMP_RULE bool_ss [] (ONCE_REWRITE_RULE [validIntervalbounds_def] th))) \\
ASM_SIMP_TAC bool_ss[] \\
Cases_on `absenv (Binop b f f')` \\
Cases_on `b` \\ Cases_on `absenv f` \\ Cases_on `absenv f'` \\ fs[]));
)
>- (FIRST_X_ASSUM (Q.SPEC_THEN `absenv` (Q.SPEC_THEN `P` ASSUME_TAC))
POP_ASSUM SIMP_TAC[MEM_APPEND]
THEN intros "!a0 a1 a2; IH1 IH2; !absenv P; approximates_bin; !v; contained_v"
THEN SUBGOAL_TAC "cases_a0" `a0 = Plus \/ a0 = Sub \/ a0 = Mult \/ a0 = Div` [MESON_TAC[cases "binop"]]
THEN destruct "cases_a0" "a0_eq | a0_eq | a0_eq | a0_eq"
THEN rewrite_asm "a0_eq" "approximates_bin"
THEN rewrite validIntervalbounds "approximates_bin"
THEN TRY (falsity "approximates_bin")
THEN destruct "approximates_bin" "approx_a1 approx_a2 _"
THEN destruct "contained_v" "mem_fv_a1 | mem_fv_a2"
THEN TRY (lspecialize "IH1" [`absenv:analysisResult`; `P:precond`]
THEN mp_spec "IH1" "approx_a1"
THEN specialize "IH1" `v:num`
THEN mp_spec "IH1" "mem_fv_a1"
THEN auto)
THEN lspecialize "IH2" [`absenv:analysisResult`; `P:precond`]
THEN mp_spec "IH2" "approx_a2"
THEN specialize "IH2" `v:num`
THEN mp_spec "IH2" "mem_fv_a2"
THEN auto
val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
``!(f:real exp) (absenv:analysisResult) (P:precond) cenv vR.
validIntervalbounds f absenv P /\
eval_exp 0 cenv P f vR ==>
(FST (FST (absenv f))) <= vR /\ vR <= (SND (FST (absenv f)))``,
GEN_TAC \\ Induct_on `f` \\ REPEAT GEN_TAC
......@@ -24,6 +24,7 @@ val _ = type_abbrev ("precond", ``:num->interval``);
Abbreviations for the environment types
**)
val _ = type_abbrev("env",``:num->real``);
val _ = type_abbrev("analysisResult", ``:real exp->(interval # real)``);
(**
Define environment update function as abbreviation.
......
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