Commit 5e618b49 authored by Heiko Becker's avatar Heiko Becker
Browse files

Prove precondition validation sound

parent 5f848dec
......@@ -6,16 +6,6 @@ needs "Expressions.hl";;
**)
new_type_abbrev("analysisResult",`:(real)exp->intv#err`);;
let envApproximatesPrecondFun = define
`envApproximatesPrecondFun (P:num->intv) (absenv:analysisResult) (u:num) =
let (ivlo,ivhi) = P u in
let (absIv,err) = absenv (Param u) in
let (abslo,abshi) = absIv in
abslo <= ivlo /\ ivhi <= abshi`;;
let envApproximatesPrecond = define
`envApproximatesPrecond (P:num->intv) (absenv:analysisResult) = !(u:num). envApproximatesPrecondFun P absenv u`;;
let precondValidForExecFun = define `
precondValidForExecFun (P:num->intv) (cenv:env_ty) (v:num) =
let (ivlo,ivhi) = P v in
......
......@@ -28,6 +28,8 @@ let auto = TRY reflexivity THEN TRY (ASM_SIMP_TAC[]);;
(* Abbreviation! *)
let lcontra asm ty = lcontradiction asm ty;;
let falsity asm = USE_THEN asm (fun th -> CONTR_TAC th);;
(* Only assumption manipulating tactics *)
let destruct (asm:string) (patt:string) =
REMOVE_THEN asm (DESTRUCT_TAC patt);;
......@@ -99,7 +101,7 @@ let spec thn varl =
LABEL_TAC thn (SPECL varl th));;
let simplify thn =
REMOVE_THEN thn (fun th -> LABEL_TAC thn (CONV_RULE let_CONV th));;
REMOVE_THEN thn (fun th -> LABEL_TAC thn (CONV_RULE (REPEATC let_CONV) th));;
let unfold thn th =
REMOVE_THEN thn
......
needs "Infra/Abbrevs.hl";;
needs "Expressions.hl";;
needs "Infra/RealSimps.hl";;
needs "Infra/ExpressionAbbrevs.hl";;
needs "IntervalArith.hl";;
let freeVars = define
`(freeVars (Const n) = []) /\
(freeVars (Var v) = []) /\
(freeVars ((Param v):(V)exp) = [v]) /\
(freeVars (Binop b e1 e2) = APPEND (freeVars e1) (freeVars e2))`;;
let approximatesPrecond = define
`(approximatesPrecond ((Const n):(real)exp) (absenv:analysisResult) (P:precond) = T) /\
(approximatesPrecond ((Param v):(real)exp) (absenv:analysisResult) (P:precond) =
let (vprelo, vprehi) = P v in
let (iv, err) = absenv (Param v) in
let (vlo, vhi) = iv in
(vlo <= vprelo) /\ (vprehi <= vhi)) /\
(approximatesPrecond ((Var v):(real)exp) (absenv:analysisResult) (P:precond) = T) /\
(approximatesPrecond ((Binop b e1 e2):(real)exp) (absenv:analysisResult) (P:precond) =
(approximatesPrecond e1 absenv P /\ approximatesPrecond e2 absenv P))`;;
let approximatesPrecond_sound = prove (
`! (e:(real)exp) (absenv:analysisResult) (P:precond).
approximatesPrecond e absenv P ==>
(!(v:num). MEM v (freeVars e) ==>
isSupersetInterval (P v) (FST (absenv (Param v))))`,
mp exp_IND
THEN SIMP_TAC[freeVars; MEM]
THEN split
THENL [
SIMP_TAC[approximatesPrecond; freeVars; MEM; isSupersetInterval]
THEN intros "!a absenv P; approx_absenv"
THEN intros "!v; v_eq"
THEN SUBGOAL_TAC "absenv_Param_def" `?(iv1:interval) (err1:error). (absenv:analysisResult) (Param a) = (iv1,err1)` [MESON_TAC[cases "prod"]]
THEN destruct "absenv_Param_def" "@iv1. @err1. absenv_param"
THEN rewrite_asm "absenv_param" "approx_absenv"
THEN SUBGOAL_TAC "P_a_def" `?ivlo ivhi. (P:precond) a = (ivlo, ivhi)` [MESON_TAC [cases "prod"]]
THEN destruct "P_a_def" "@ivlo. @ivhi. P_a_def"
THEN rewrite_asm "P_a_def" "approx_absenv"
THEN SUBGOAL_TAC "iv1_def" `?ivlo1 ivhi1. (iv1:interval) = (ivlo1, ivhi1)` [MESON_TAC [cases "prod"]]
THEN destruct "iv1_def" "@ivlo1. @ivhi1. iv1_def"
THEN rewrite_asm "iv1_def" "approx_absenv"
THEN simplify "approx_absenv"
THEN ASM_REWRITE_TAC[IVlo; FST; IVhi; SND];
SIMP_TAC[MEM_APPEND]
THEN intros "!a0 a1 a2; IH1 IH2; !absenv P; approximates_bin; !v; contained_v"
THEN rewrite approximatesPrecond "approximates_bin"
THEN destruct "approximates_bin" "approx_a1 approx_a2"
THEN destruct "contained_v" "mem_fv_a1 | mem_fv_a2"
THENL [
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;
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
]
]
);;
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