Commit 9325d322 authored by Heiko Becker's avatar Heiko Becker

WIP: Next step for IV validation

parent 7b1808b0
7ed3f12092db2062b6fccb60e9735143ecd5c7e5
f243fe78da5dcc426046ce1b6a0f756e6aa524b9
......@@ -9,7 +9,8 @@ open simpLib realTheory realLib RealArith pred_setTheory sptreeTheory
sptreeLib;
open AbbrevsTheory ExpressionsTheory RealSimpsTheory FloverTactics
ExpressionAbbrevsTheory IntervalArithTheory CommandsTheory ssaPrgsTheory
MachineTypeTheory FloverMapTheory TypeValidatorTheory;
MachineTypeTheory FloverMapTheory TypeValidatorTheory RealRangeArithTheory
ExpressionSemanticsTheory;
open preamble;
val _ = new_theory "IntervalValidation";
......@@ -114,6 +115,10 @@ val cond_simpl = store_thm (
``!a b. (if a then T else b) <=> (a \/ (~ a /\ b))``,
rpt strip_tac \\ metis_tac[]);
val real_prove =
rpt (qpat_x_assum `!x. _` kall_tac)
\\ REAL_ASM_ARITH_TAC;
val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
``!(f:real expr) (A:analysisResult) (P:precond) (fVars:num_set)
(dVars:num_set) E Gamma.
......@@ -123,109 +128,114 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
(((domain (usedVars f)) DIFF (domain dVars)) SUBSET (domain fVars)) /\
fVars_P_sound fVars E P /\
validTypes f Gamma ==>
? iv err vR.
FloverMapTree_find f A = SOME(iv, err) /\
eval_expr E (toRMap Gamma) fBits (toREval f) vR REAL /\
(FST iv) <= vR /\ vR <= (SND iv)``,
validRanges f A E (toRTMap (toRExpMap Gamma))``,
Induct_on `f`
\\ once_rewrite_tac [usedVars_def, toREval_def] \\ rpt strip_tac
\\ Flover_compute ``validIntervalbounds``
\\ Flover_compute ``validIntervalbounds`` \\ rveq
(* Defined variable case *)
>- (rw_thm_asm `dVars_range_valid _ _ _` dVars_range_valid_def
\\ specialize `!v. v IN domain dVars ==> _` `n`
\\ first_x_assum destruct
>- (fs [domain_lookup])
\\ qexists_tac `vR` \\ fs[] \\ rveq \\ fs[]
\\ fs[validRanges_def]
\\ qexists_tac `vR` \\ fs[] \\ rveq \\ fs[toREval_def]
\\ irule Var_load \\ TRY (fs[])
\\ rw_thm_asm `vars_typed _ _` vars_typed_def
\\ first_x_assum (qspec_then `n` destruct)
\\ fs[toRMap_def, domain_lookup])
\\ fs[toRExpMap_def, toRTMap_def, domain_lookup, validTypes_def])
(* Free variable case *)
>- (rw_thm_asm `fVars_P_sound _ _ _` fVars_P_sound_def
\\ specialize `!v. v IN domain fVars ==> _` `n`
\\ `lookup n dVars = NONE` by (Cases_on `lookup n dVars` \\ fs [])
\\ first_x_assum destruct
>- (fs[usedVars_def, lookup_NONE_domain])
\\ simp[validRanges_def]
\\ qexists_tac `vR`
\\ fs [isSupersetInterval_def, IVlo_def, IVhi_def]
\\ fs [isSupersetInterval_def, toREval_def]
\\ rpt conj_tac
>- (irule Var_load \\ TRY (fs[])
\\ rw_thm_asm `vars_typed _ _` vars_typed_def
\\ first_x_assum (qspec_then `n` destruct)
\\ fs[toRMap_def, domain_lookup])
\\ fs[toRExpMap_def, toRTMap_def, domain_lookup, validTypes_def])
\\ irule REAL_LE_TRANS \\ asm_exists_tac \\ fs[] \\ rveq \\ fs[])
(* Const case *)
>- (qexists_tac `v` \\ fs[]
>- (simp[validRanges_def]
\\ qexists_tac `v` \\ fs[toREval_def]
\\ irule Const_dist' \\ fs[perturb_def, mTypeToR_def])
(* Unary operator case *)
>- (first_x_assum (qspecl_then [`A`, `P`, `fVars`, `dVars`, `E`, `Gamma`, `fBits`] destruct)
\\ fs[]
\\ rveq
\\ Cases_on `u`
>- (rw_thm_asm `validTypes _ _` validTypes_def
\\ first_x_assum
(qspecl_then [`A`, `P`, `fVars`, `dVars`, `E`, `Gamma`] destruct)
\\ fs[] \\ rveq
\\ IMP_RES_TAC validRanges_single
\\ simp[Once validRanges_def] \\ Cases_on `u`
(* Negation case *)
>- (qexists_tac `- vR` \\ fs[negateInterval_def, isSupersetInterval_def]
\\ Cases_on `iv` \\ fs[IVlo_def, IVhi_def]
\\ rpt conj_tac \\ TRY REAL_ASM_ARITH_TAC
\\ irule Unop_neg' \\ qexistsl_tac [`REAL`, `vR`] \\ fs[evalUnop_def])
\\ rveq \\ Cases_on `iv` \\ fs[]
\\ rpt conj_tac \\ fs[toREval_def] \\ TRY real_prove
\\ irule Unop_neg' \\ qexistsl_tac [`REAL`, `REAL`, `vR`]
\\ fs[evalUnop_def, isCompat_def, toRTMap_def])
(* Inversion case *)
\\ qexists_tac `1 / vR`
\\ conj_tac
>- (irule Unop_inv' \\ fs[mTypeToR_def] \\ qexistsl_tac [`vR`]
\\ fs[evalUnop_def, mTypeToR_def, perturb_def, REAL_INV_1OVER, mTypeToR_pos, IVhi_def, IVlo_def]
>- (simp[toREval_def]
\\ irule Unop_inv' \\ qexistsl_tac [`0`, `REAL`, `REAL`, `vR`]
\\ simp[evalUnop_def, mTypeToR_def, perturb_def, REAL_INV_1OVER,
mTypeToR_pos, isCompat_def, toRTMap_def]
\\ CCONTR_TAC \\ fs[] \\ rveq
\\ `0 < 0:real` by (REAL_ASM_ARITH_TAC)
\\ `0 < 0:real` by (real_prove)
\\ fs[])
\\ conj_tac
\\ fs[invertInterval_def, isSupersetInterval_def]
\\ Cases_on `iv` \\ fs[IVlo_def, IVhi_def]
\\ fs[invertInterval_def, isSupersetInterval_def] \\ rveq
\\ Cases_on `iv` \\ fs[]
>- (irule REAL_LE_TRANS \\ qexists_tac `1 / r` \\ conj_tac \\ fs[]
\\ fs[GSYM REAL_INV_1OVER] \\ irule REAL_INV_LE_ANTIMONO_IMPL \\ fs[]
\\ REAL_ASM_ARITH_TAC)
\\ real_prove)
>- (irule REAL_LE_TRANS \\ qexists_tac `1 / r` \\ conj_tac \\ fs[]
\\ fs[GSYM REAL_INV_1OVER] \\ irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[]
\\ REAL_ASM_ARITH_TAC)
\\ real_prove)
>- (irule REAL_LE_TRANS \\ qexists_tac `1 / q` \\ conj_tac \\ fs[]
\\ fs[GSYM REAL_INV_1OVER] \\ irule REAL_INV_LE_ANTIMONO_IMPL \\ fs[]
\\ REAL_ASM_ARITH_TAC)
\\ real_prove)
\\ irule REAL_LE_TRANS \\ qexists_tac `1/q` \\ conj_tac \\ fs[]
\\ fs[GSYM REAL_INV_1OVER] \\ irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[]
\\ REAL_ASM_ARITH_TAC)
\\ real_prove)
(* Binary operator case *)
>- (rename1 `Binop b (toREval f1) (toREval f2)`
>- (rename1 `Binop b f1 f2` \\ simp[Once validRanges_def, toREval_def]
\\ rw_thm_asm `validTypes _ _` validTypes_def \\ fs[]
\\ rpt (
first_x_assum
(qspecl_then [`A`, `P`, `fVars`, `dVars`, `E`, `Gamma`, `fBits`] destruct)
(qspecl_then [`A`, `P`, `fVars`, `dVars`, `E`, `Gamma`] destruct)
\\ fs[domain_union, UNION_DEF, DIFF_DEF, SUBSET_DEF])
\\ rveq
\\ rename1 `eval_expr E (toRMap Gamma) fBits (toREval f1) vR1 REAL`
\\ rename1 `eval_expr E (toRMap Gamma) fBits (toREval f2) vR2 REAL`
\\ IMP_RES_TAC validRanges_single
\\ rename1 `eval_expr E _ (toREval f1) vR1 REAL`
\\ rename1 `eval_expr E _ (toREval f2) vR2 REAL`
\\ conj_tac >- (rpt strip_tac \\ fs[])
\\ qexists_tac `evalBinop b vR1 vR2`
\\ conj_tac
>- (irule Binop_dist' \\ fs[mTypeToR_def]
\\ qexistsl_tac [`0`, `REAL`, `REAL`, `vR1`, `vR2`]
\\ fs[join_def, mTypeToR_pos, perturb_def, isFixedPoint_def]
\\ strip_tac \\ rveq \\ fs[IVlo_def, IVhi_def]
\\ qexistsl_tac [`REAL`, `REAL`, `vR1`, `vR2`]
\\ fs[isJoin_def, isFixedPoint_def, join_fl_def, mTypeToR_pos,
perturb_def, toRTMap_def]
\\ strip_tac \\ rveq \\ fs[]
\\ CCONTR_TAC \\ fs[] \\ rveq
>- (`0 < 0:real` by (irule REAL_LET_TRANS \\ asm_exists_tac \\ fs[])
\\ fs[])
\\ `0 < 0:real` by (irule REAL_LTE_TRANS \\ asm_exists_tac \\ fs[])
\\ `0 < 0:real` by (real_prove)
\\ fs[])
\\ fs[] \\ rveq
\\ rename1 `FloverMapTree_find f1 A = SOME (iv1, err1)`
\\ rename1 `FloverMapTree_find f2 A = SOME (iv2, err2)`
\\ Cases_on `b` \\ simp[evalBinop_def]
(* Plus case *)
>- (fs[evalBinop_def, isSupersetInterval_def, absIntvUpd_def, IVlo_def, IVhi_def, addInterval_def]
>- (fs[evalBinop_def, isSupersetInterval_def, absIntvUpd_def,
addInterval_def]
\\ qspecl_then [`iv1`, `iv2`, `vR1`, `vR2`]
assume_tac
(REWRITE_RULE
[validIntervalAdd_def,
addInterval_def,
absIntvUpd_def,
contained_def,
IVhi_def, IVlo_def] interval_addition_valid)
\\ qpat_x_assum `!x. _` kall_tac \\ REAL_ASM_ARITH_TAC)
contained_def] interval_addition_valid)
\\ fs[] \\ real_prove)
(* Sub case *)
>- (fs[evalBinop_def, isSupersetInterval_def, absIntvUpd_def, IVlo_def, IVhi_def, subtractInterval_def, addInterval_def, negateInterval_def]
>- (fs[evalBinop_def, isSupersetInterval_def, absIntvUpd_def,
subtractInterval_def, addInterval_def, negateInterval_def]
\\ qspecl_then [`iv1`, `iv2`, `vR1`, `vR2`]
assume_tac
(REWRITE_RULE
......@@ -234,51 +244,52 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
addInterval_def,
negateInterval_def,
absIntvUpd_def,
contained_def,
IVhi_def,
IVlo_def] interval_subtraction_valid)
\\ qpat_x_assum `!x. _` kall_tac \\ REAL_ASM_ARITH_TAC)
contained_def] interval_subtraction_valid)
\\ fs[] \\ real_prove)
(* Mult case *)
>- (fs[evalBinop_def, isSupersetInterval_def, absIntvUpd_def, IVlo_def, IVhi_def, multInterval_def]
>- (fs[evalBinop_def, isSupersetInterval_def, absIntvUpd_def,
multInterval_def]
\\ qspecl_then [`iv1`, `iv2`, `vR1`, `vR2`]
assume_tac
(REWRITE_RULE
[validIntervalAdd_def,
multInterval_def,
absIntvUpd_def,
contained_def,
IVhi_def,
IVlo_def] interval_multiplication_valid)
\\ qpat_x_assum `!x. _` kall_tac \\ REAL_ASM_ARITH_TAC)
contained_def] interval_multiplication_valid)
\\ fs[] \\ real_prove)
(* Div case *)
\\ fs[evalBinop_def, isSupersetInterval_def, absIntvUpd_def, IVlo_def,
IVhi_def, divideInterval_def, multInterval_def, invertInterval_def,
\\ fs[evalBinop_def, isSupersetInterval_def, absIntvUpd_def,
divideInterval_def, multInterval_def, invertInterval_def,
GSYM REAL_INV_1OVER]
\\ qspecl_then [`iv1`, `iv2`, `vR1`, `vR2`]
assume_tac
(REWRITE_RULE
[validIntervalSub_def, divideInterval_def,
multInterval_def, invertInterval_def,
absIntvUpd_def, contained_def, IVhi_def, IVlo_def,
absIntvUpd_def, contained_def,
GSYM REAL_INV_1OVER]
interval_division_valid)
\\ qpat_x_assum `!x. _` kall_tac \\ REAL_ASM_ARITH_TAC)
\\ fs[] \\ real_prove)
(* FMA case *)
>- (rename1 `Fma (toREval f1) (toREval f2) (toREval f3)`
>- (rename1 `Fma f1 f2 f3`
\\ rw_thm_asm `validTypes _ _` validTypes_def \\ fs[]
\\ rpt (
first_x_assum
(qspecl_then [`A`, `P`, `fVars`, `dVars`, `E`, `Gamma`, `fBits`] destruct)
(qspecl_then [`A`, `P`, `fVars`, `dVars`, `E`, `Gamma`] destruct)
\\ fs[domain_union, UNION_DEF, DIFF_DEF, SUBSET_DEF])
\\ rveq
\\ rename1 `eval_expr E (toRMap Gamma) fBits (toREval f1) vR1 REAL`
\\ rename1 `eval_expr E (toRMap Gamma) fBits (toREval f2) vR2 REAL`
\\ rename1 `eval_expr E (toRMap Gamma) fBits (toREval f3) vR3 REAL`
\\ IMP_RES_TAC validRanges_single
\\ rename1 `eval_expr E _ (toREval f1) vR1 REAL`
\\ rename1 `eval_expr E _ (toREval f2) vR2 REAL`
\\ rename1 `eval_expr E _ (toREval f3) vR3 REAL`
\\ simp[Once validRanges_def, toREval_def]
\\ qexists_tac `evalFma vR1 vR2 vR3`
\\ conj_tac
>- (irule Fma_dist'
\\ qexistsl_tac [`0:real`, `0`, `REAL`, `REAL`, `REAL`, `vR1`, `vR2`, `vR3`]
\\ qexistsl_tac [`0:real`, `REAL`, `REAL`, `REAL`, `REAL`, `vR1`, `vR2`, `vR3`]
\\ fs [mTypeToR_def, perturb_def, evalFma_def, evalBinop_def,
join3_def, join_def, isFixedPoint_def])
toRTMap_def, isJoin3_def, join_fl3_def, join_fl_def,
isFixedPoint_def])
\\ fs[] \\ rveq
\\ rename1 `FloverMapTree_find f1 A = SOME (iv_f1, err1)`
\\ rename1 `FloverMapTree_find f2 A = SOME (iv_f2, err2)`
\\ rename1 `FloverMapTree_find f3 A = SOME (iv_f3, err3)`
......@@ -288,9 +299,7 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
[validIntervalAdd_def,
multInterval_def,
absIntvUpd_def,
contained_def,
IVhi_def,
IVlo_def] interval_multiplication_valid)
contained_def] interval_multiplication_valid)
\\ fs[]
\\ qspecl_then [`iv_f1`, `multInterval iv_f2 iv_f3`, `vR1`, `vR2 * vR3`]
destruct
......@@ -299,17 +308,22 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
addInterval_def,
multInterval_def,
absIntvUpd_def,
contained_def,
IVhi_def, IVlo_def] interval_addition_valid)
\\ fs[multInterval_def, absIntvUpd_def, IVlo_def, IVhi_def,
isSupersetInterval_def, addInterval_def, multInterval_def,
absIntvUpd_def, IVlo_def, IVhi_def, evalFma_def, evalBinop_def]
\\ qpat_x_assum `!x. _` kall_tac \\ REAL_ASM_ARITH_TAC)
contained_def] interval_addition_valid)
\\ fs[multInterval_def, absIntvUpd_def, isSupersetInterval_def,
addInterval_def, multInterval_def, absIntvUpd_def, evalFma_def,
evalBinop_def]
\\ real_prove)
(* Downcast case *)
>- (first_x_assum
(qspecl_then [`A`, `P`, `fVars`, `dVars`, `E`, `Gamma`, `fBits`] destruct)
>- (rw_thm_asm `validTypes _ _` validTypes_def
\\ fs[]
\\ first_x_assum
(qspecl_then [`A`, `P`, `fVars`, `dVars`, `E`, `Gamma`] destruct)
\\ fs[] \\ rveq
\\ simp[Once validRanges_def]
\\ IMP_RES_TAC validRanges_single
\\ fs[] \\ rveq
\\ qexists_tac `vR` \\ fs[Downcast_dist', isSupersetInterval_def, IVlo_def, IVhi_def]
\\ qexists_tac `vR`
\\ fs[Downcast_dist', toREval_def, isSupersetInterval_def]
\\ `FST iv = FST intv` by (metis_tac [REAL_LE_ANTISYM])
\\ `SND iv = SND intv` by (metis_tac [REAL_LE_ANTISYM])
\\ fs[]));
......
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