Commit b6376565 authored by Heiko Becker's avatar Heiko Becker
Browse files

Show stronger IV soundnes in HOL4

parent f4caeb89
......@@ -259,7 +259,7 @@ Inductive eval_exp (E:env) (Gamma: nat -> option mType) :(exp R) -> R -> mType -
Hint Constructors eval_exp.
(**
Show some simpler rule lemmata
Show some simpler (more general) rule lemmata
**)
Lemma Const_dist' m n delta v m' E Gamma:
Rle (Rabs delta) (Q2R (mTypeToQ m)) ->
......@@ -276,7 +276,7 @@ Lemma Unop_neg' m f1 v1 v m' E Gamma:
eval_exp E Gamma f1 v1 m ->
v = evalUnop Neg v1 ->
m' = m ->
eval_exp E Gamma (Unop Neg f1) (evalUnop Neg v1) m'.
eval_exp E Gamma (Unop Neg f1) v m'.
Proof.
intros; subst; auto.
Qed.
......
......@@ -370,7 +370,7 @@ Proof.
lra.
Qed.
Lemma test3 Gamma n m:
Lemma Rmap_updVars_comm Gamma n m:
forall x,
updDefVars n M0 (toRMap Gamma) x = toRMap (updDefVars n m Gamma) x.
Proof.
......@@ -378,25 +378,25 @@ Proof.
intros x; destruct (x =? n); try auto.
Qed.
Lemma test2 e n Gamma E v:
eval_exp E (toRMap (updDefVars n M0 Gamma)) (toREval (toRExp e)) v M0 ->
eval_exp E (updDefVars n M0 (toRMap Gamma)) (toREval (toRExp e)) v M0.
Proof.
revert v;
induction e; intros * eval_e; inversion eval_e; subst; simpl in *;
auto.
- constructor; try auto.
erewrite test3; eauto.
- rewrite H2 in *.
apply M0_join_is_M0 in H2.
destruct H2; subst.
eauto.
- apply M0_least_precision in H1; subst.
econstructor; try eauto.
apply isMorePrecise_refl.
Qed.
(* Lemma eval_exp_Rmap_updVars_comm e n Gamma E v: *)
(* eval_exp E (toRMap (updDefVars n M0 Gamma)) (toREval (toRExp e)) v M0 -> *)
(* eval_exp E (updDefVars n M0 (toRMap Gamma)) (toREval (toRExp e)) v M0. *)
(* Proof. *)
(* revert v; *)
(* induction e; intros * eval_e; inversion eval_e; subst; simpl in *; *)
(* auto. *)
(* - constructor; try auto. *)
(* erewrite test3; eauto. *)
(* - rewrite H2 in *. *)
(* apply M0_join_is_M0 in H2. *)
(* destruct H2; subst. *)
(* eauto. *)
(* - apply M0_least_precision in H1; subst. *)
(* econstructor; try eauto. *)
(* apply isMorePrecise_refl. *)
(* Qed. *)
Lemma test5 e E vR m Gamma1 Gamma2:
Lemma swap_Gamma_eval_exp e E vR m Gamma1 Gamma2:
(forall n, Gamma1 n = Gamma2 n) ->
eval_exp E Gamma1 e vR m ->
eval_exp E Gamma2 e vR m.
......@@ -409,7 +409,7 @@ Proof.
rewrite <- Gamma_eq; auto.
Qed.
Lemma test4 f E vR m Gamma1 Gamma2 :
Lemma swap_Gamma_bstep f E vR m Gamma1 Gamma2 :
(forall n, Gamma1 n = Gamma2 n) ->
bstep f E Gamma1 vR m ->
bstep f E Gamma2 vR m.
......@@ -418,14 +418,14 @@ Proof.
induction f; intros * Gamma_eq eval_f.
- inversion eval_f; subst.
econstructor; try eauto.
+ eapply test5; eauto.
+ eapply swap_Gamma_eval_exp; eauto.
+ apply (IHf _ (updDefVars n m0 Gamma1) _); try eauto.
intros n1.
unfold updDefVars.
case (n1 =? n); auto.
- inversion eval_f; subst.
econstructor; try eauto.
eapply test5; eauto.
eapply swap_Gamma_eval_exp; eauto.
Qed.
Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult) Gamma:
......@@ -474,7 +474,7 @@ Proof.
rewrite NatSet.union_spec, NatSet.add_spec in in_set.
destruct in_set as [P1 | [ P2 | P3]]; auto.
+ edestruct IHf as [vR [eval_f valid_bounds_f]]; try eauto.
{ eapply ssa_equal_set. symmetry in H. apply H. apply H7. }
eapply ssa_equal_set. symmetry in H. apply H. apply H7. }
* intros v0 mem_v0.
unfold updEnv.
case_eq (v0 =? n); intros v0_eq.
......@@ -533,7 +533,7 @@ Proof.
apply a_no_dVar.
rewrite NatSet.add_spec; auto. }
* simpl. exists vR; split; [econstructor; eauto | auto].
eapply test4 with (Gamma1 := toRMap (updDefVars n M0 Gamma)) ; try eauto.
eapply swap_Gamma_bstep with (Gamma1 := toRMap (updDefVars n M0 Gamma)) ; try eauto.
intros n1; rewrite <- test3; auto.
- unfold validIntervalboundsCmd in valid_bounds_f.
pose proof (validIntervalbounds_sound e absenv P E Gamma valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e.
......
......@@ -28,14 +28,13 @@ val toREvalCmd_def = Define `
result value
**)
val (bstep_rules, bstep_ind, bstep_cases) = Hol_reln `
(!m m' x e s E v res defVars.
eval_exp E defVars e v m /\
(defVars x = SOME m) /\
bstep s (updEnv x v E) defVars res m' ==>
bstep (Let m x e s) E defVars res m') /\
(!m e E v defVars.
eval_exp E defVars e v m ==>
bstep (Ret e) E defVars v m)`;
(!m m' x e s E v res Gamma.
eval_exp E Gamma e v m /\
bstep s (updEnv x v E) (updDefVars x m Gamma) res m' ==>
bstep (Let m x e s) E Gamma res m') /\
(!m e E v Gamma.
eval_exp E Gamma e v m ==>
bstep (Ret e) E Gamma v m)`;
(**
Generate a better case lemma again
......
......@@ -87,6 +87,7 @@ val (eval_exp_rules, eval_exp_ind, eval_exp_cases) = Hol_reln `
eval_exp E defVars (Unop Neg f1) (evalUnop Neg v1) m) /\
(!E defVars m f1 v1 delta.
abs delta <= (mTypeToQ m) /\
(v1 <> 0) /\
eval_exp E defVars f1 v1 m ==>
eval_exp E defVars (Unop Inv f1) (perturb (evalUnop Inv v1) delta) m) /\
(!E defVars m m1 f1 v1 delta.
......@@ -109,10 +110,10 @@ val eval_exp_cases_old = save_thm ("eval_exp_cases_old", eval_exp_cases);
val eval_exp_cases =
map (GEN_ALL o SIMP_CONV (srw_ss()) [Once eval_exp_cases])
[``eval_exp E defVars (Var v) res m``,
``eval_exp E defVars (Const m n) res m``,
``eval_exp E defVars (Const m1 n) res m2``,
``eval_exp E defVars (Unop u e) res m``,
``eval_exp E defVars (Binop n e1 e2) res m``,
``eval_exp E defVars (Downcast m e1) res m``]
``eval_exp E defVars (Downcast m1 e1) res m2``]
|> LIST_CONJ |> curry save_thm "eval_exp_cases";
val [Var_load, Const_dist, Unop_neg, Unop_inv, Downcast_dist, Binop_dist] = CONJ_LIST 6 eval_exp_rules;
......
......@@ -113,7 +113,7 @@ val ivbounds_approximatesPrecond_sound = store_thm ("ivbounds_approximatesPrecon
\\ fs []));
val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
``!(f:real exp) (absenv:analysisResult) (P:precond) fVars dVars E Gamma.
``!(f:real exp) (absenv:analysisResult) (P:precond) (fVars:num_set) (dVars:num_set) E Gamma.
validIntervalbounds f absenv P dVars /\ (* The checker succeeded *)
(* All defined vars have already been analyzed *)
(!v. v IN (domain dVars) ==>
......@@ -397,7 +397,7 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
>- ( `0 < 0:real` suffices_by (fs[])
\\ match_mp_tac REAL_LTE_TRANS
\\ qexists_tac `FST iv_f'`
\\ fs[])
\\ fs[]))
>- (fs[evalBinop_def, isSupersetInterval_def, absIntvUpd_def, IVlo_def,
IVhi_def, divideInterval_def, multInterval_def,
invertInterval_def, GSYM REAL_INV_1OVER]
......@@ -421,7 +421,7 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
(FST iv_f * (inv (FST iv_f')))
(SND iv_f * (inv (SND iv_f')))
(SND iv_f * (inv (FST iv_f')))`
\\ metis_tac [])
\\ metis_tac []))))
(* Downcast case *)
>- (`?v. eval_exp E (toRMap Gamma) (toREval f) v M0 /\
FST(FST(absenv f)) <= v /\ v <= SND (FST(absenv f))`
......@@ -434,10 +434,7 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
\\ rpt strip_tac
\\ first_x_assum match_mp_tac \\ fs[]
\\ simp[Once usedVars_def])
\\ fs[]
fs []
\\ qexists_tac `v` \\ fs []
\\ rw_thm_asm `validIntervalbounds (Downcast m f) absenv P dVars` validIntervalbounds_def
\\ Cases_on `absenv (Downcast m f)`
\\ qmatch_assum_rename_tac `absenv (Downcast m f) = (iv_u, err_u)`
......@@ -460,10 +457,79 @@ val getRetExp_def = Define `
|Let m x e g => getRetExp g
|Ret e => e`;
val Rmap_updVars_comm = store_thm (
"Rmap_updVars_comm",
``!Gamma n m x.
updDefVars n M0 (toRMap Gamma) x = toRMap (updDefVars n m Gamma) x``,
fs [updDefVars_def, toRMap_def]
\\ rpt strip_tac
\\ Cases_on `x = n` \\ fs[]);
(* val eval_exp_Rmap_updVars_comm = store_thm ( *)
(* "eval_exp_Rmap_updVars_comm", *)
(* ``!E e v n Gamma. *)
(* eval_exp E (toRMap (updDefVars n M0 Gamma)) (toREval e) v M0 ==> *)
(* eval_exp E (updDefVars n M0 (toRMap Gamma)) (toREval e) v M0``, *)
(* Induct_on `e` *)
(* \\ rpt strip_tac \\ simp[Once toREval_def] *)
(* >- (fs [toREval_def] \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases *)
(* \\ irule Var_load \\ fs[] *)
(* \\ rw_sym_asm `_ = SOME M0` *)
(* \\ irule Rmap_updVars_comm) *)
(* >- (fs [toREval_def] \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases *)
(* \\ irule Const_dist' \\ fs[] *)
(* \\ qexists_tac `delta` \\ fs[]) *)
(* >- (rw_thm_asm `eval_exp _ _ _ _ _` toREval_def *)
(* \\ fs[] \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases *)
(* \\ fs[] \\ res_tac *)
(* >- (irule Unop_neg' *)
(* \\ qexistsl_tac [`M0`, `v1`] \\ fs[]) *)
(* >- (irule Unop_inv' *)
(* \\ qexistsl_tac [`delta`, `M0`, `v1`] \\ fs[])) *)
(* >- (rw_thm_asm `eval_exp _ _ _ _ _` toREval_def *)
(* \\ fs [] \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases *)
(* \\ `m1 = M0 /\ m2 = M0` by (irule M0_join_is_M0 \\ fs[]) *)
(* \\ fs[] \\ res_tac *)
(* \\ irule Binop_dist' *)
(* \\ qexistsl_tac [`delta`, `M0`, `M0`, `v1`, `v2`] \\ fs[join_def, mTypeToQ_def]) *)
(* >- (rw_thm_asm `eval_exp _ _ _ _ _` toREval_def *)
(* \\ fs[])); *)
val swap_Gamma_eval_exp = store_thm (
"swap_Gamma_exp_exp",
``!e E vR m Gamma1 Gamma2.
(!n. Gamma1 n = Gamma2 n) /\
eval_exp E Gamma1 e vR m ==>
eval_exp E Gamma2 e vR m``,
Induct_on `e`
\\ rpt strip_tac
\\ inversion `eval_exp _ _ _ _ _` eval_exp_cases
\\ fs[eval_exp_cases] \\ res_tac
>- (qpat_x_assum `!n. _ = _` (fn thm => fs [GSYM thm]))
>- (qexists_tac `delta` \\ fs[])
>- (qexists_tac `v1` \\ fs[])
>- (qexistsl_tac [`v1`, `delta`] \\ fs[])
>- (qexistsl_tac [`m1`, `m2`, `v1`, `v2`, `delta`] \\ fs[])
>- (qexistsl_tac [`m1'`, `v1`, `delta`] \\ fs[]));
val swap_Gamma_bstep = store_thm (
"swap_Gamma_bstep",
``!f E vR m Gamma1 Gamma2.
(!n. Gamma1 n = Gamma2 n) /\
bstep f E Gamma1 vR m ==>
bstep f E Gamma2 vR m``,
Induct_on `f`
\\ rpt strip_tac \\ inversion `bstep _ _ _ _ _` bstep_cases
\\ fs[bstep_cases]
>- (qexists_tac `v` \\ conj_tac
>- (irule swap_Gamma_eval_exp \\ qexists_tac `Gamma1` \\ fs[])
>- (res_tac \\ first_x_assum irule
\\ fs [updDefVars_def]))
>- (irule swap_Gamma_eval_exp \\ qexists_tac `Gamma1` \\ fs[]));
val validIntervalboundsCmd_sound = store_thm ("validIntervalboundsCmd_sound",
``!f (absenv:analysisResult) E vR (fVars dVars outVars:num_set) elo ehi err P defVars.
``!f (absenv:analysisResult) E vR fVars dVars outVars elo ehi err P Gamma.
ssa f (union fVars dVars) outVars /\
bstep (toREvalCmd f) E (toREvalVars defVars) vR M0 /\
(!v. v IN (domain dVars) ==>
?vR.
(E v = SOME vR) /\
......@@ -474,62 +540,73 @@ val validIntervalboundsCmd_sound = store_thm ("validIntervalboundsCmd_sound",
(E v = SOME vR) /\
(FST (P v)) <= vR /\ vR <= SND (P v)) /\
(((domain (freeVars f)) DIFF (domain dVars)) SUBSET (domain fVars)) /\
(!v. v IN (domain fVars) \/ v IN (domain dVars) ==>
?m. Gamma v = SOME m) /\
validIntervalboundsCmd f absenv P dVars /\
(absenv (getRetExp f) = ((elo, ehi), err)) ==>
elo <= vR /\ vR <= ehi``,
gen_tac \\ Induct_on `f`
\\ once_rewrite_tac [validIntervalboundsCmd_def,toREvalCmd_def]
\\ rpt gen_tac \\ strip_tac
>- (inversion `ssa _ _ _` ssa_cases
\\ fs [] \\ inversion `bstep _ _ _ _ _` bstep_cases
\\ fs []
\\ first_x_assum match_mp_tac
\\ qexistsl_tac [`absenv`, `updEnv n v E`, `fVars`, `insert n () dVars`, `outVars`, `err`, `P`, `defVars`]
\\ fs [updEnv_def]
\\ rpt conj_tac
>- (match_mp_tac ssa_equal_set
\\ qexists_tac `(insert n () (union fVars dVars))`
\\ fs [domain_union, domain_insert]
\\ once_rewrite_tac [UNION_COMM]
\\ fs [INSERT_UNION_EQ, UNION_COMM])
>- (rpt strip_tac
\\ Cases_on `v' = n` \\ fs[]
>- (rveq
\\ rw_sym_asm `FST (absenv e) = _`
\\ match_mp_tac validIntervalbounds_sound
\\ qexistsl_tac [`P`, `fVars`, `dVars`, `E`, `defVars`] \\ fs [SUBSET_DEF]
?vR.
(bstep (toREvalCmd f) E (toRMap Gamma) vR M0 /\
elo <= vR /\ vR <= ehi)``,
Induct_on `f`
\\ rpt gen_tac
\\ once_rewrite_tac [validIntervalboundsCmd_def, toREvalCmd_def, getRetExp_def]
\\ rpt strip_tac
\\ first_x_assum match_mp_tac \\ fs [Once freeVars_def, domain_union]
\\ metis_tac [])
>- (rveq
\\ rw_sym_asm `FST (absenv e) = _`
\\ match_mp_tac validIntervalbounds_sound
\\ qexistsl_tac [`P`, `fVars`, `dVars`, `E`, `defVars`] \\ fs [SUBSET_DEF]
>- (inversion `ssa _ _ _` ssa_cases \\ rveq
\\ fs[]
\\ Cases_on `absenv e` \\ rename1 `absenv e = (iv_e, err_e)`
\\ `?v. eval_exp E (toRMap Gamma) (toREval e) v M0 /\ FST (FST (absenv e)) <= v /\ v <= SND (FST (absenv e))`
by (irule validIntervalbounds_sound
\\ qexistsl_tac [`P`, `dVars`, `fVars`]
\\ fs []
\\ conj_tac
\\ fs [SUBSET_DEF, domain_union]
\\ rpt strip_tac
\\ first_x_assum match_mp_tac \\ fs [Once freeVars_def, domain_union]
\\ metis_tac []))
>- (rpt strip_tac
\\ Cases_on `v' = n` \\ fs[domain_union])
>- (fs [ domain_insert, SUBSET_DEF]
\\ `x IN domain fVars \/ x IN domain dVars` by (first_x_assum irule \\ fs[]))
\\ `? vR. bstep (toREvalCmd f) (updEnv n v E) (toRMap (updDefVars n M0 Gamma)) vR M0 /\ elo <= vR /\ vR <= ehi`
by (first_x_assum irule
\\ qexistsl_tac [`P`, `absenv`, `insert n () dVars`, `err`, `fVars`, `outVars`]
\\ fs [domain_insert]
\\ rpt conj_tac
>- (rpt strip_tac \\ fs[updEnv_def]
>- (rw_sym_asm `iv_e = FST _`
\\ rw_asm_star `absenv e = _ ` \\ fs[])
>- (rename1 `v2 IN domain dVars`
\\ Cases_on `v2 = n` \\ fs[]
\\ rveq \\ fs [domain_union]))
>- (rpt strip_tac \\ fs[updEnv_def]
\\ rename1 `v2 IN domain fVars`
\\ Cases_on `v2 = n` \\ rveq \\ fs[domain_union])
>- (rpt strip_tac \\ rveq \\ fs [updDefVars_def]
\\ rename1 `v2 IN domain _` \\ Cases_on `v2 = n` \\ fs[])
>- (fs [domain_insert, SUBSET_DEF]
\\ rpt strip_tac
\\ first_x_assum match_mp_tac
\\ once_rewrite_tac [freeVars_def, domain_union]
\\ fs [domain_union])
>- (fs [Once getRetExp_def]))
>- (inversion `ssa _ _ _` ssa_cases
\\ fs [] \\ inversion `bstep _ _ _ _ _` bstep_cases
\\ fs [updEnv_def, getRetExp_def]
\\ drule validIntervalbounds_sound
\\ disch_then (qspecl_then [`fVars`, `E`, `vR`, `defVars`] assume_tac)
\\ qpat_x_assum `absenv _ = _` (fn thm => fs [thm])
\\ first_x_assum match_mp_tac
\\ fs [SUBSET_DEF]
>- (match_mp_tac ssa_equal_set
\\ qexists_tac `(insert n () (union fVars dVars))`
\\ fs [domain_union, domain_insert]
\\ once_rewrite_tac [UNION_COMM]
\\ fs [INSERT_UNION_EQ, UNION_COMM]))
\\ qexists_tac `vR` \\ fs[bstep_cases]
\\ qexists_tac `v` \\ fs[]
\\ irule swap_Gamma_bstep
\\ qexists_tac `(toRMap (updDefVars n M0 Gamma))` \\ fs[Rmap_updVars_comm])
>- (fs []
\\ inversion `ssa _ _ _` ssa_cases
\\ `? v. eval_exp E (toRMap Gamma) (toREval e) v M0 /\ FST (FST (absenv e)) <= v /\ v <= SND (FST (absenv e))`
by (irule validIntervalbounds_sound
\\ qexistsl_tac [`P`, `dVars`, `fVars`] \\ fs[]
\\ conj_tac \\ fs[SUBSET_DEF, domain_union]
\\ rpt strip_tac
\\ qpat_x_assum `domain (union fVars dVars) = _` (fn thm => fs [GSYM thm])
\\ specialize `!x'. x' IN domain (usedVars e) ==> _` `x`
\\ specialize `x IN domain (usedVars e) ==> _` `x IN domain (usedVars e)`
\\ fs [domain_union]
\\ CCONTR_TAC \\ metis_tac []));
\\ rw_sym_asm `_ = domain outVars`
\\ `x IN domain outVars` by (first_x_assum irule \\ fs[])
\\ qpat_x_assum `_ = domain outVars` (fn thm => fs[GSYM thm])
\\ fs[])
\\ `bstep (Ret (toREval e)) E (toRMap Gamma) v M0`
by (fs[bstep_cases])
\\ qexists_tac `v` \\ fs[]
\\ rw_asm_star `absenv e = _`));
val validIntervalbounds_noDivzero_real = store_thm("validIntervalbounds_noDivzero_real",
``!(f1 f2:real exp) (absenv:analysisResult) (P:precond) (dVars:num_set).
......
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