IntervalValidation.v 19.7 KB
 Heiko Becker committed Sep 18, 2016 1 ``````(** `````` Heiko Becker committed Oct 11, 2016 2 3 4 5 6 `````` 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. `````` Heiko Becker committed Sep 18, 2016 7 ``````**) `````` Heiko Becker committed Oct 07, 2016 8 ``````Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List Coq.micromega.Psatz. `````` Heiko Becker committed Feb 28, 2018 9 10 11 ``````Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps Flover.Infra.RealRationalProps. Require Import Flover.Infra.Ltacs Flover.Infra.RealSimps Flover.Typing. Require Export Flover.IntervalArithQ Flover.IntervalArith Flover.ssaPrgs. `````` Heiko Becker committed Aug 21, 2016 12 `````` `````` Heiko Becker committed Oct 30, 2017 13 ``````Fixpoint validIntervalbounds (e:exp Q) (A:analysisResult) (P:precond) (validVars:NatSet.t) :bool:= `````` Heiko Becker committed Feb 28, 2018 14 `````` match FloverMap.find e A with `````` Heiko Becker committed Oct 30, 2017 15 16 17 18 19 20 21 22 23 24 25 `````` | None => false | Some (intv, _) => match e with | Var _ v => if NatSet.mem v validVars then true else isSupersetIntv (P v) intv && (Qleb (ivlo (P v)) (ivhi (P v))) | Const _ n => isSupersetIntv (n,n) intv | Unop o f => if validIntervalbounds f A P validVars then `````` Heiko Becker committed Feb 28, 2018 26 `````` match FloverMap.find f A with `````` Heiko Becker committed Oct 30, 2017 27 28 29 30 31 `````` | None => false | Some (iv, _) => match o with | Neg => let new_iv := negateIntv iv in `````` Heiko Becker committed Feb 24, 2017 32 `````` isSupersetIntv new_iv intv `````` Heiko Becker committed Oct 30, 2017 33 34 35 36 37 38 39 40 `````` | Inv => if (((Qleb (ivhi iv) 0) && (negb (Qeq_bool (ivhi iv) 0))) || ((Qleb 0 (ivlo iv)) && (negb (Qeq_bool (ivlo iv) 0)))) then let new_iv := invertIntv iv in isSupersetIntv new_iv intv else false end `````` Heiko Becker committed Oct 12, 2016 41 `````` end `````` Heiko Becker committed Feb 24, 2017 42 `````` else false `````` Heiko Becker committed Jan 05, 2017 43 `````` | Binop op f1 f2 => `````` Heiko Becker committed Oct 30, 2017 44 45 `````` if ((validIntervalbounds f1 A P validVars) && (validIntervalbounds f2 A P validVars)) `````` Heiko Becker committed Feb 24, 2017 46 `````` then `````` Heiko Becker committed Feb 28, 2018 47 `````` match FloverMap.find f1 A, FloverMap.find f2 A with `````` Heiko Becker committed Oct 30, 2017 48 `````` | Some (iv1, _), Some (iv2, _) => `````` Heiko Becker committed Jan 05, 2017 49 `````` match op with `````` Heiko Becker committed Aug 21, 2016 50 51 52 53 54 55 56 57 58 `````` | Plus => let new_iv := addIntv iv1 iv2 in isSupersetIntv new_iv intv | Sub => let new_iv := subtractIntv iv1 iv2 in isSupersetIntv new_iv intv | Mult => let new_iv := multIntv iv1 iv2 in isSupersetIntv new_iv intv `````` Heiko Becker committed Oct 04, 2016 59 `````` | Div => `````` Heiko Becker committed Feb 24, 2017 60 61 62 63 64 65 `````` if (((Qleb (ivhi iv2) 0) && (negb (Qeq_bool (ivhi iv2) 0))) || ((Qleb 0 (ivlo iv2)) && (negb (Qeq_bool (ivlo iv2) 0)))) then let new_iv := divideIntv iv1 iv2 in isSupersetIntv new_iv intv else false `````` Heiko Becker committed Aug 21, 2016 66 `````` end `````` Heiko Becker committed Oct 30, 2017 67 68 `````` | _, _ => false end `````` Heiko Becker committed Feb 24, 2017 69 `````` else false `````` Nikita Zyuzin committed Oct 23, 2017 70 `````` | Fma f1 f2 f3 => `````` Nikita Zyuzin committed Dec 18, 2017 71 72 73 `````` if ((validIntervalbounds f1 A P validVars) && (validIntervalbounds f2 A P validVars) && (validIntervalbounds f3 A P validVars)) `````` Nikita Zyuzin committed Oct 23, 2017 74 `````` then `````` Heiko Becker committed Feb 28, 2018 75 `````` match FloverMap.find f1 A, FloverMap.find f2 A, FloverMap.find f3 A with `````` Nikita Zyuzin committed Dec 18, 2017 76 77 78 79 80 `````` | Some (iv1, _), Some (iv2, _), Some (iv3, _) => let new_iv := addIntv iv1 (multIntv iv2 iv3) in isSupersetIntv new_iv intv | _, _, _ => false end `````` Nikita Zyuzin committed Oct 23, 2017 81 `````` else false `````` Raphaël Monat committed Mar 03, 2017 82 `````` | Downcast _ f1 => `````` Heiko Becker committed Oct 30, 2017 83 `````` if (validIntervalbounds f1 A P validVars) `````` Heiko Becker committed Jun 29, 2017 84 `````` then `````` Heiko Becker committed Feb 28, 2018 85 `````` match FloverMap.find f1 A with `````` Heiko Becker committed Oct 30, 2017 86 87 `````` | None => false | Some (iv1, _) => `````` Heiko Becker committed Jun 29, 2017 88 89 `````` (* TODO: intv = iv1 might be a hard constraint... *) (isSupersetIntv intv iv1) && (isSupersetIntv iv1 intv) `````` Heiko Becker committed Oct 30, 2017 90 `````` end `````` Heiko Becker committed Jun 29, 2017 91 92 `````` else false `````` Heiko Becker committed Oct 30, 2017 93 94 `````` end end. `````` Heiko Becker committed Aug 21, 2016 95 `````` `````` Heiko Becker committed Oct 30, 2017 96 ``````Fixpoint validIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P:precond) (validVars:NatSet.t) :bool:= `````` Heiko Becker committed Feb 03, 2017 97 `````` match f with `````` 98 `````` | Let m x e g => `````` Heiko Becker committed Feb 28, 2018 99 `````` match FloverMap.find e A, FloverMap.find (Var Q x) A with `````` Heiko Becker committed Oct 30, 2017 100 101 102 103 104 105 106 107 `````` | Some ((e_lo,e_hi), _), Some ((x_lo, x_hi), _) => if (validIntervalbounds e A P validVars && Qeq_bool (e_lo) (x_lo) && Qeq_bool (e_hi) (x_hi)) then validIntervalboundsCmd g A P (NatSet.add x validVars) else false | _, _ => false end `````` Heiko Becker committed Feb 17, 2017 108 `````` |Ret e => `````` Heiko Becker committed Oct 30, 2017 109 `````` validIntervalbounds e A P validVars `````` Heiko Becker committed Feb 03, 2017 110 111 `````` end. `````` Heiko Becker committed Aug 23, 2016 112 113 114 115 116 117 118 119 120 121 122 123 ``````Corollary Q2R_max4 a b c d: Q2R (IntervalArithQ.max4 a b c d) = max4 (Q2R a) (Q2R b) (Q2R c) (Q2R d). Proof. unfold IntervalArithQ.max4, max4; repeat rewrite Q2R_max; auto. Qed. Corollary Q2R_min4 a b c d: Q2R (IntervalArithQ.min4 a b c d) = min4 (Q2R a) (Q2R b) (Q2R c) (Q2R d). Proof. unfold IntervalArith.min4, min4; repeat rewrite Q2R_min; auto. Qed. `````` Heiko Becker committed Oct 30, 2017 124 ``````Lemma validBoundsDiv_uneq_zero e1 e2 A P V ivlo_e2 ivhi_e2 err: `````` Heiko Becker committed Feb 28, 2018 125 `````` FloverMap.find (elt:=intv * error) e2 A = Some ((ivlo_e2,ivhi_e2), err) -> `````` Heiko Becker committed Oct 30, 2017 126 `````` validIntervalbounds (Binop Div e1 e2) A P V = true -> `````` Heiko Becker committed Oct 08, 2016 127 128 `````` (ivhi_e2 < 0) \/ (0 < ivlo_e2). Proof. `````` Heiko Becker committed Nov 02, 2017 129 `````` intros A_eq validBounds; cbn in *. `````` Heiko Becker committed Feb 28, 2018 130 `````` Flover_compute; try congruence. `````` Heiko Becker committed Oct 09, 2016 131 `````` apply le_neq_bool_to_lt_prop; auto. `````` Heiko Becker committed Oct 08, 2016 132 ``````Qed. `````` = committed Apr 05, 2017 133 `````` `````` Heiko Becker committed Nov 02, 2017 134 135 ``````Definition dVars_range_valid (dVars:NatSet.t) (E:env) (A:analysisResult) :Prop := forall v, NatSet.In v dVars -> `````` 136 `````` exists vR iv err, `````` Heiko Becker committed Nov 02, 2017 137 `````` E v = Some vR /\ `````` Heiko Becker committed Feb 28, 2018 138 `````` FloverMap.find (Var Q v) A = Some (iv, err) /\ `````` 139 `````` (Q2R (fst iv) <= vR <= Q2R (snd iv))%R. `````` Heiko Becker committed Nov 02, 2017 140 141 142 143 144 145 146 147 148 149 150 `````` Definition fVars_P_sound (fVars:NatSet.t) (E:env) (P:precond) :Prop := forall v, NatSet.In v fVars -> exists vR, E v = Some vR /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R. Definition vars_typed (S:NatSet.t) (Gamma: nat -> option mType) := forall v, NatSet.In v S -> exists m :mType, Gamma v = Some m. `````` 151 152 ``````Ltac kill_trivial_exists := match goal with `````` Heiko Becker committed Nov 03, 2017 153 154 `````` | [ |- exists iv err v, Some (?i,?e) = Some (iv, err) /\ _ ] => exists i, e | [ |- exists iv err, Some (?i,?e) = Some (iv, err) /\ _ ] => exists i, e `````` 155 156 `````` end. `````` Heiko Becker committed Oct 30, 2017 157 ``````Theorem validIntervalbounds_sound (f:exp Q) (A:analysisResult) (P:precond) `````` Heiko Becker committed Jun 29, 2017 158 `````` fVars dVars (E:env) Gamma: `````` Heiko Becker committed Oct 30, 2017 159 `````` validIntervalbounds f A P dVars = true -> `````` Heiko Becker committed Nov 02, 2017 160 `````` dVars_range_valid dVars E A -> `````` Raphaël Monat committed Feb 28, 2017 161 `````` NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars -> `````` Heiko Becker committed Nov 02, 2017 162 163 `````` fVars_P_sound fVars E P -> vars_typed (NatSet.union fVars dVars) Gamma -> `````` 164 `````` exists iv err vR, `````` Heiko Becker committed Feb 28, 2018 165 `````` FloverMap.find f A = Some (iv, err) /\ `````` Heiko Becker committed Nov 02, 2017 166 `````` eval_exp E (toRMap Gamma) (toREval (toRExp f)) vR M0 /\ `````` 167 `````` (Q2R (fst iv) <= vR <= Q2R (snd iv))%R. `````` Heiko Becker committed Aug 21, 2016 168 ``````Proof. `````` Heiko Becker committed Jun 29, 2017 169 170 `````` induction f; intros valid_bounds valid_definedVars usedVars_subset valid_freeVars types_defined; `````` Heiko Becker committed Nov 02, 2017 171 `````` cbn in *. `````` Heiko Becker committed Feb 28, 2018 172 `````` - Flover_compute. `````` Heiko Becker committed Nov 02, 2017 173 174 `````` destruct (NatSet.mem n dVars) eqn:?; simpl in *. + destruct (valid_definedVars n) `````` 175 `````` as [vR [iv_n [err_n [env_valid [map_n bounds_valid]]]]]; `````` Heiko Becker committed Nov 02, 2017 176 177 178 `````` try set_tac. rewrite map_n in *. inversion Heqo; subst. `````` 179 180 `````` kill_trivial_exists. eexists; split; [auto| split; try eauto ]. `````` Heiko Becker committed Jun 29, 2017 181 182 183 184 `````` eapply Var_load; simpl; try auto. destruct (types_defined n) as [m type_m]; set_tac. match_simpl; auto. `````` Heiko Becker committed Nov 02, 2017 185 186 `````` + destruct (valid_freeVars n) as [vR [env_valid bounds_valid]]; set_tac; try auto. `````` Heiko Becker committed Jun 29, 2017 187 `````` assert (NatSet.In n fVars) by set_tac. `````` Heiko Becker committed Nov 02, 2017 188 189 `````` andb_to_prop valid_bounds. canonize_hyps; simpl in *. `````` 190 191 `````` kill_trivial_exists. eexists; split; [auto | split]. `````` Heiko Becker committed Nov 02, 2017 192 `````` * econstructor; try eauto. `````` 193 194 `````` destruct (types_defined n) as [m type_m]; set_tac. `````` Heiko Becker committed Jun 29, 2017 195 `````` match_simpl; auto. `````` Heiko Becker committed Nov 02, 2017 196 `````` * lra. `````` Heiko Becker committed Feb 28, 2018 197 `````` - Flover_compute; canonize_hyps; simpl in *. `````` 198 199 200 `````` kill_trivial_exists. exists (perturb (Q2R v) 0). split; [auto| split]. `````` Heiko Becker committed Nov 02, 2017 201 202 `````` + econstructor; try eauto. apply Rabs_0_equiv. + unfold perturb; simpl; lra. `````` Heiko Becker committed Feb 28, 2018 203 `````` - Flover_compute; simpl in *; try congruence. `````` 204 `````` destruct IHf as [iv_f [err_f [vF [iveq_f [eval_f valid_bounds_f]]]]]; `````` Heiko Becker committed Nov 02, 2017 205 `````` try auto. `````` 206 207 208 209 210 `````` inversion iveq_f; subst. destruct u; try andb_to_prop R; simpl in *. + kill_trivial_exists. exists (evalUnop Neg vF); split; [auto | split ; `````` Heiko Becker committed Nov 02, 2017 211 `````` [econstructor; eauto | ]]. `````` Heiko Becker committed Jun 29, 2017 212 213 `````` canonize_hyps. rewrite Q2R_opp in *. `````` 214 215 `````` simpl; lra. + rename L0 into nodiv0. `````` Heiko Becker committed Jun 29, 2017 216 `````` apply le_neq_bool_to_lt_prop in nodiv0. `````` 217 218 `````` kill_trivial_exists. exists (perturb (evalUnop Inv vF) 0); split; `````` Heiko Becker committed Nov 02, 2017 219 220 221 `````` [destruct i; auto | split]. * econstructor; eauto; try apply Rabs_0_equiv. (* Absence of division by zero *) `````` Heiko Becker committed Jun 29, 2017 222 223 224 `````` hnf. destruct nodiv0 as [nodiv0 | nodiv0]; apply Qlt_Rlt in nodiv0; rewrite Q2R0_is_0 in nodiv0; lra. * canonize_hyps. `````` 225 `````` pose proof (interval_inversion_valid ((Q2R (fst iv_f)),(Q2R (snd iv_f))) (a :=vF)) as inv_valid. `````` Heiko Becker committed Jun 29, 2017 226 227 228 229 230 `````` unfold invertInterval in inv_valid; simpl in *. rewrite delta_0_deterministic; [| rewrite Rbasic_fun.Rabs_R0; lra]. destruct inv_valid; try auto. { destruct nodiv0; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto. } { split; eapply Rle_trans. `````` Heiko Becker committed Nov 02, 2017 231 `````` - apply L1. `````` Heiko Becker committed Jun 29, 2017 232 233 234 235 236 237 238 239 240 241 242 `````` - rewrite Q2R_inv; try auto. destruct nodiv0; try lra. hnf; intros. assert (0 < Q2R (snd iv_f))%R. { eapply Rlt_le_trans. apply Qlt_Rlt in H1. rewrite <- Q2R0_is_0. apply H1. lra. } rewrite <- Q2R0_is_0 in H3. apply Rlt_Qlt in H3. `````` Heiko Becker committed Oct 13, 2016 243 `````` lra. `````` Heiko Becker committed Jun 29, 2017 244 245 246 247 248 249 250 251 252 253 254 255 256 `````` - apply H0. - rewrite <- Q2R_inv; try auto. hnf; intros. destruct nodiv0; try lra. assert (Q2R (fst iv_f) < 0)%R. { eapply Rle_lt_trans. Focus 2. rewrite <- Q2R0_is_0; apply Qlt_Rlt in H2; apply H2. lra. } rewrite <- Q2R0_is_0 in H3. apply Rlt_Qlt in H3. lra. } `````` Heiko Becker committed Feb 28, 2018 257 `````` - Flover_compute; try congruence. `````` 258 `````` destruct IHf1 as [iv_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]]; `````` Heiko Becker committed Nov 02, 2017 259 `````` try auto; set_tac. `````` 260 `````` destruct IHf2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]]; `````` Heiko Becker committed Nov 02, 2017 261 `````` try auto; set_tac. `````` Heiko Becker committed Jun 29, 2017 262 263 `````` assert (M0 = join M0 M0) as M0_join by (cbv; auto); rewrite M0_join. `````` 264 `````` kill_trivial_exists. `````` Heiko Becker committed Jun 29, 2017 265 `````` exists (perturb (evalBinop b vF1 vF2) 0); `````` Heiko Becker committed Nov 02, 2017 266 267 `````` split; [destruct i; auto | ]. inversion env1; inversion env2; subst. `````` Heiko Becker committed Jun 29, 2017 268 269 270 `````` destruct b; simpl in *. * split; [econstructor; try congruence; apply Rabs_0_equiv | ]. `````` 271 272 273 `````` pose proof (interval_addition_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1)) (Q2R (fst iv_f2), Q2R (snd iv_f2))) as valid_add. `````` Heiko Becker committed Jun 29, 2017 274 275 276 `````` specialize (valid_add vF1 vF2 valid_f1 valid_f2). unfold isSupersetIntv in R. andb_to_prop R. `````` Heiko Becker committed Nov 02, 2017 277 `````` canonize_hyps; simpl in *. `````` Heiko Becker committed Jun 29, 2017 278 279 `````` repeat rewrite <- Q2R_plus in *; rewrite <- Q2R_min4, <- Q2R_max4 in *. `````` Heiko Becker committed Nov 02, 2017 280 `````` unfold perturb. lra. `````` Heiko Becker committed Jun 29, 2017 281 282 `````` * split; [econstructor; try congruence; apply Rabs_0_equiv |]. `````` 283 284 `````` pose proof (interval_subtraction_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1)) (Q2R (fst iv_f2), Q2R (snd iv_f2))) `````` Heiko Becker committed Nov 02, 2017 285 `````` as valid_sub. `````` Heiko Becker committed Jun 29, 2017 286 287 288 `````` specialize (valid_sub vF1 vF2 valid_f1 valid_f2). unfold isSupersetIntv in R. andb_to_prop R. `````` Heiko Becker committed Nov 02, 2017 289 `````` canonize_hyps; simpl in *. `````` Heiko Becker committed Jun 29, 2017 290 291 292 `````` repeat rewrite <- Q2R_opp in *; repeat rewrite <- Q2R_plus in *; rewrite <- Q2R_min4, <- Q2R_max4 in *. `````` Heiko Becker committed Nov 02, 2017 293 `````` unfold perturb; lra. `````` Heiko Becker committed Jun 29, 2017 294 295 `````` * split; [ econstructor; try congruence; apply Rabs_0_equiv |]. `````` 296 297 `````` pose proof (interval_multiplication_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1)) (Q2R (fst iv_f2), Q2R (snd iv_f2))) `````` Heiko Becker committed Nov 02, 2017 298 `````` as valid_mul. `````` Heiko Becker committed Jun 29, 2017 299 300 301 `````` specialize (valid_mul vF1 vF2 valid_f1 valid_f2). unfold isSupersetIntv in R. andb_to_prop R. `````` Heiko Becker committed Nov 02, 2017 302 `````` canonize_hyps; simpl in *. `````` Heiko Becker committed Jun 29, 2017 303 304 `````` repeat rewrite <- Q2R_mult in *; rewrite <- Q2R_min4, <- Q2R_max4 in *. `````` Heiko Becker committed Nov 02, 2017 305 `````` unfold perturb; lra. `````` Heiko Becker committed Jun 29, 2017 306 307 308 309 310 311 312 313 `````` * andb_to_prop R. canonize_hyps. apply le_neq_bool_to_lt_prop in L. split; [ econstructor; try congruence; try apply Rabs_0_equiv | ]. (* No division by zero proof *) { hnf; intros. destruct L as [L | L]; apply Qlt_Rlt in L; rewrite Q2R0_is_0 in L; lra. } `````` Heiko Becker committed Nov 02, 2017 314 `````` { pose proof (interval_division_valid (a:=vF1) (b:=vF2) `````` 315 316 `````` ((Q2R (fst iv_f1)), Q2R (snd iv_f1)) (Q2R (fst iv_f2), Q2R (snd iv_f2))) `````` Heiko Becker committed Nov 02, 2017 317 `````` as valid_div. `````` Heiko Becker committed Jun 29, 2017 318 319 320 `````` simpl in *. destruct valid_div; try auto. - destruct L; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto. `````` 321 `````` - assert (~ (snd iv_f2) == 0). `````` Heiko Becker committed Jun 29, 2017 322 `````` { hnf; intros. destruct L; try lra. `````` 323 `````` assert (0 < (snd iv_f2)) by (apply Rlt_Qlt; apply Qlt_Rlt in H2; lra). `````` Heiko Becker committed Jun 29, 2017 324 `````` lra. } `````` 325 `````` assert (~ (fst iv_f2) == 0). `````` Heiko Becker committed Jun 29, 2017 326 `````` { hnf; intros; destruct L; try lra. `````` 327 `````` assert ((fst iv_f2) < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H3; lra). `````` Heiko Becker committed Jun 29, 2017 328 329 330 331 332 333 334 `````` lra. } repeat (rewrite <- Q2R_inv in *; try auto). repeat rewrite <- Q2R_mult in *. rewrite <- Q2R_min4, <- Q2R_max4 in *. unfold perturb. lra. } `````` Heiko Becker committed Feb 28, 2018 335 `````` - Flover_compute; try congruence. `````` Nikita Zyuzin committed Dec 18, 2017 336 337 338 `````` destruct IHf1 as [iv_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]]; try auto; set_tac. destruct IHf2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]]; try auto; set_tac. destruct IHf3 as [iv_f3 [err3 [vF3 [env3 [eval_f3 valid_f3]]]]]; try auto; set_tac. `````` Nikita Zyuzin committed Oct 23, 2017 339 340 `````` assert (M0 = join3 M0 M0 M0) as M0_join by (cbv; auto); rewrite M0_join. `````` Nikita Zyuzin committed Dec 18, 2017 341 342 343 344 345 `````` kill_trivial_exists. exists (perturb (evalFma vF1 vF2 vF3) 0); split; try auto. inversion env1; inversion env2; inversion env3; subst. split; [auto | ]. * econstructor; try congruence; apply Rabs_0_equiv. `````` Nikita Zyuzin committed Oct 23, 2017 346 347 `````` * pose proof (interval_multiplication_valid (Q2R (fst iv_f2),Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as valid_mul. specialize (valid_mul vF2 vF3 valid_f2 valid_f3). `````` Nikita Zyuzin committed Nov 16, 2017 348 `````` remember (multInterval (Q2R (fst iv_f2), Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as iv_f23prod. `````` Nikita Zyuzin committed Oct 23, 2017 349 `````` pose proof (interval_addition_valid (Q2R (fst iv_f1),Q2R (snd iv_f1)) (fst iv_f23prod, snd iv_f23prod)) as valid_add. `````` Nikita Zyuzin committed Nov 16, 2017 350 `````` rewrite Heqiv_f23prod in valid_add, valid_mul. `````` Nikita Zyuzin committed Oct 23, 2017 351 352 353 354 355 356 357 358 `````` unfold multIntv in valid_add. canonize_hyps. simpl in *. repeat rewrite <- Q2R_mult in *; repeat rewrite <- Q2R_min4, <- Q2R_max4 in *; repeat rewrite <- Q2R_plus in *; repeat rewrite <- Q2R_min4, <- Q2R_max4 in *. specialize (valid_add vF1 (vF2 * vF3)%R valid_f1 valid_mul). `````` Nikita Zyuzin committed Dec 18, 2017 359 `````` unfold evalFma, evalBinop, perturb. `````` Nikita Zyuzin committed Oct 23, 2017 360 `````` lra. `````` Heiko Becker committed Nov 02, 2017 361 `````` - match_simpl. `````` Heiko Becker committed Jun 29, 2017 362 `````` andb_to_prop valid_bounds. `````` Heiko Becker committed Nov 02, 2017 363 `````` match_simpl. `````` 364 `````` destruct IHf as [iv_f [err_f [vF [env_f [eval_f valid_f]]]]]; `````` Heiko Becker committed Nov 02, 2017 365 366 `````` try auto. inversion env_f; subst. `````` 367 `````` kill_trivial_exists. `````` Heiko Becker committed Jun 29, 2017 368 `````` exists (perturb vF 0). `````` Heiko Becker committed Nov 02, 2017 369 `````` split; [destruct i; try auto |]. `````` Heiko Becker committed Jun 29, 2017 370 `````` split; [try econstructor; try eauto; try apply Rabs_0_equiv; unfold isMorePrecise; auto |]. `````` Heiko Becker committed Nov 02, 2017 371 372 373 `````` unfold isSupersetIntv in *; andb_to_prop R. canonize_hyps; simpl in *. unfold perturb; lra. `````` Heiko Becker committed Jun 29, 2017 374 375 ``````Qed. `````` Heiko Becker committed Aug 28, 2017 376 ``````Lemma Rmap_updVars_comm Gamma n m: `````` Heiko Becker committed Jun 29, 2017 377 378 379 380 381 382 383 `````` forall x, updDefVars n M0 (toRMap Gamma) x = toRMap (updDefVars n m Gamma) x. Proof. unfold updDefVars, toRMap; simpl. intros x; destruct (x =? n); try auto. Qed. `````` Heiko Becker committed Aug 28, 2017 384 ``````Lemma swap_Gamma_eval_exp e E vR m Gamma1 Gamma2: `````` Heiko Becker committed Jun 29, 2017 385 386 387 388 389 390 391 392 393 394 395 396 `````` (forall n, Gamma1 n = Gamma2 n) -> eval_exp E Gamma1 e vR m -> eval_exp E Gamma2 e vR m. Proof. revert E vR Gamma1 Gamma2 m; induction e; intros * Gamma_eq eval_e; inversion eval_e; subst; simpl in *; try eauto. apply Var_load; try auto. rewrite <- Gamma_eq; auto. Qed. `````` Heiko Becker committed Aug 28, 2017 397 ``````Lemma swap_Gamma_bstep f E vR m Gamma1 Gamma2 : `````` Heiko Becker committed Jun 29, 2017 398 399 400 401 402 403 `````` (forall n, Gamma1 n = Gamma2 n) -> bstep f E Gamma1 vR m -> bstep f E Gamma2 vR m. Proof. revert E Gamma1 Gamma2; induction f; intros * Gamma_eq eval_f. `````` Heiko Becker committed Feb 03, 2017 404 `````` - inversion eval_f; subst. `````` Heiko Becker committed Jun 29, 2017 405 `````` econstructor; try eauto. `````` Heiko Becker committed Aug 28, 2017 406 `````` + eapply swap_Gamma_eval_exp; eauto. `````` Heiko Becker committed Jun 29, 2017 407 408 409 410 411 412 `````` + apply (IHf _ (updDefVars n m0 Gamma1) _); try eauto. intros n1. unfold updDefVars. case (n1 =? n); auto. - inversion eval_f; subst. econstructor; try eauto. `````` Heiko Becker committed Aug 28, 2017 413 `````` eapply swap_Gamma_eval_exp; eauto. `````` Heiko Becker committed Oct 13, 2016 414 ``````Qed. `````` Heiko Becker committed Feb 03, 2017 415 `````` `````` Heiko Becker committed Jan 03, 2018 416 417 ``````Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult): forall Gamma E fVars dVars outVars P, `````` = committed Apr 06, 2017 418 `````` ssa f (NatSet.union fVars dVars) outVars -> `````` Heiko Becker committed Nov 02, 2017 419 420 421 `````` dVars_range_valid dVars E A -> fVars_P_sound fVars E P -> vars_typed (NatSet.union fVars dVars) Gamma -> `````` = committed Apr 06, 2017 422 `````` NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars -> `````` Heiko Becker committed Oct 30, 2017 423 `````` validIntervalboundsCmd f A P dVars = true -> `````` 424 `````` exists iv_e err_e vR, `````` Heiko Becker committed Feb 28, 2018 425 `````` FloverMap.find (getRetExp f) A = Some (iv_e, err_e) /\ `````` Heiko Becker committed Jun 29, 2017 426 `````` bstep (toREvalCmd (toRCmd f)) E (toRMap Gamma) vR M0 /\ `````` 427 `````` (Q2R (fst iv_e) <= vR <= Q2R (snd iv_e))%R. `````` = committed Apr 06, 2017 428 429 ``````Proof. induction f; `````` Heiko Becker committed Nov 02, 2017 430 431 `````` intros * ssa_f dVars_sound fVars_valid types_valid usedVars_subset valid_bounds_f; cbn in *. `````` Heiko Becker committed Feb 28, 2018 432 `````` - Flover_compute. `````` = committed Apr 06, 2017 433 `````` inversion ssa_f; subst. `````` Heiko Becker committed Nov 02, 2017 434 435 `````` canonize_hyps. pose proof (validIntervalbounds_sound e (Gamma:=Gamma) (E:=E) (fVars:=fVars) L) as validIV_e. `````` 436 `````` destruct validIV_e as [iv_e [err_v [v [find_v [eval_e valid_bounds_e]]]]]; `````` Heiko Becker committed Nov 02, 2017 437 438 `````` try auto. { set_tac. repeat split; auto. `````` Heiko Becker committed Jun 29, 2017 439 440 `````` hnf; intros; subst. set_tac. } `````` Heiko Becker committed Nov 02, 2017 441 `````` rewrite find_v in *; inversion Heqo; subst. `````` Heiko Becker committed Jun 29, 2017 442 443 `````` specialize (IHf (updDefVars n M0 Gamma) (updEnv n v E) fVars (NatSet.add n dVars)). assert (NatSet.Equal (NatSet.add n (NatSet.union fVars dVars)) (NatSet.union fVars (NatSet.add n dVars))). `````` Heiko Becker committed Nov 02, 2017 444 445 446 447 448 `````` + hnf. intros a; split; intros in_set; set_tac. * destruct in_set as [ ? | [? ?]]; try auto; set_tac. destruct H0; auto. * destruct in_set as [? | ?]; try auto; set_tac. destruct H as [? | [? ?]]; auto. `````` 449 `````` + edestruct IHf as [iv_f [err_f [vR [env_f [eval_f valid_bounds_f]]]]]; `````` Heiko Becker committed Nov 02, 2017 450 `````` try eauto. `````` Heiko Becker committed Sep 05, 2017 451 `````` eapply ssa_equal_set. symmetry in H. apply H. apply H7. `````` Heiko Becker committed Jun 29, 2017 452 453 454 455 456 457 `````` * intros v0 mem_v0. unfold updEnv. case_eq (v0 =? n); intros v0_eq. { rename R1 into eq_lo; rename R0 into eq_hi. rewrite Nat.eqb_eq in v0_eq; subst. `````` 458 `````` exists v; eexists; eexists; repeat split; try eauto; simpl in *; lra. } `````` Heiko Becker committed Nov 02, 2017 459 460 461 `````` { apply dVars_sound. set_tac. destruct mem_v0 as [? | [? ?]]; try auto. `````` Heiko Becker committed Jun 29, 2017 462 `````` rewrite Nat.eqb_neq in v0_eq. `````` Heiko Becker committed Nov 02, 2017 463 `````` congruence. } `````` Heiko Becker committed Jun 29, 2017 464 465 466 467 `````` * intros v0 mem_fVars. unfold updEnv. case_eq (v0 =? n); intros case_v0; auto. rewrite Nat.eqb_eq in case_v0; subst. `````` Heiko Becker committed Nov 02, 2017 468 469 `````` assert (NatSet.In n (NatSet.union fVars dVars)) as in_union by set_tac. exfalso; set_tac. apply H6; set_tac; auto. `````` Heiko Becker committed Jun 29, 2017 470 471 472 `````` * intros x x_contained. set_tac. destruct x_contained as [x_free | x_def]. `````` Heiko Becker committed Nov 02, 2017 473 `````` { destruct (types_valid x) as [m_x Gamma_x]; try set_tac. `````` Heiko Becker committed Jun 29, 2017 474 475 476 477 478 `````` exists m_x. unfold updDefVars. case_eq (x =? n); intros eq_case; try auto. rewrite Nat.eqb_eq in eq_case. subst. exfalso; apply H6; set_tac. } `````` Heiko Becker committed Nov 02, 2017 479 `````` { set_tac. `````` Heiko Becker committed Jun 29, 2017 480 481 `````` destruct x_def as [x_n | x_def]; subst. - exists M0; unfold updDefVars; rewrite Nat.eqb_refl; auto. `````` Heiko Becker committed Nov 02, 2017 482 483 484 485 486 487 `````` - destruct x_def. destruct (types_valid x) as [m_x Gamma_x]. + rewrite NatSet.union_spec; auto. + exists m_x. unfold updDefVars; case_eq (x =? n); intros eq_case; try auto. rewrite Nat.eqb_eq in eq_case; subst. congruence. } `````` Heiko Becker committed Jun 29, 2017 488 489 490 491 `````` * clear L R1 R0 R IHf. hnf. intros a a_freeVar. rewrite NatSet.diff_spec in a_freeVar. destruct a_freeVar as [a_freeVar a_no_dVar]. `````` = committed Apr 06, 2017 492 `````` apply usedVars_subset. `````` Heiko Becker committed Jun 29, 2017 493 `````` simpl. `````` = committed Apr 06, 2017 494 495 496 `````` rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. repeat split; try auto. { hnf; intros; subst. `````` Heiko Becker committed Jun 29, 2017 497 498 499 500 501 `````` apply a_no_dVar. rewrite NatSet.add_spec; auto. } { hnf; intros a_dVar. apply a_no_dVar. rewrite NatSet.add_spec; auto. } `````` 502 `````` * simpl. exists iv_f, err_f, vR; repeat split; try auto; try lra. `````` Heiko Becker committed Nov 02, 2017 503 `````` econstructor; try eauto. `````` Heiko Becker committed Aug 28, 2017 504 `````` eapply swap_Gamma_bstep with (Gamma1 := toRMap (updDefVars n M0 Gamma)) ; try eauto. `````` Heiko Becker committed Sep 05, 2017 505 `````` intros n1; erewrite Rmap_updVars_comm; eauto. `````` = committed Apr 06, 2017 506 `````` - unfold validIntervalboundsCmd in valid_bounds_f. `````` Heiko Becker committed Nov 02, 2017 507 `````` pose proof (validIntervalbounds_sound e (E:=E) (Gamma:=Gamma) valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e. `````` 508 `````` destruct valid_iv_e as [?[?[? [? [? ?]]]]]; try auto. `````` Heiko Becker committed Nov 02, 2017 509 `````` simpl in *. repeat eexists; repeat split; try eauto; [econstructor; eauto| | ]; lra. `````` Nikita Zyuzin committed Oct 23, 2017 510 ``Qed.``