IntervalValidation.v 20.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 Sep 18, 2016 9 ``````Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps. `````` Raphaël Monat committed Mar 03, 2017 10 ``````Require Import Daisy.Infra.Ltacs Daisy.Infra.RealSimps Daisy.Typing. `````` Heiko Becker committed Feb 03, 2017 11 ``````Require Export Daisy.IntervalArithQ Daisy.IntervalArith Daisy.ssaPrgs. `````` Heiko Becker committed Aug 21, 2016 12 `````` `````` Heiko Becker committed Oct 30, 2017 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 ``````Fixpoint validIntervalbounds (e:exp Q) (A:analysisResult) (P:precond) (validVars:NatSet.t) :bool:= match DaisyMap.find e A with | 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 match DaisyMap.find f A with | 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 Oct 30, 2017 47 48 `````` match DaisyMap.find f1 A, DaisyMap.find f2 A with | 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 `````` Nikita Zyuzin committed Dec 18, 2017 75 76 77 78 79 80 `````` match DaisyMap.find f1 A, DaisyMap.find f2 A, DaisyMap.find f3 A with | 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 Oct 30, 2017 85 86 87 `````` match DaisyMap.find f1 A with | 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 Oct 30, 2017 99 100 101 102 103 104 105 106 107 `````` match DaisyMap.find e A, DaisyMap.find (Var Q x) A with | 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 Oct 30, 2017 112 113 114 115 116 ``````Theorem ivbounds_approximatesPrecond_sound f A P dVars iv err: validIntervalbounds f A P dVars = true -> forall v, NatSet.In v (NatSet.diff (Expressions.usedVars f) dVars) -> DaisyMap.find (Var Q v) A = Some (iv, err) -> Is_true(isSupersetIntv (P v) iv). `````` Heiko Becker committed Sep 19, 2016 117 ``````Proof. `````` Heiko Becker committed Oct 30, 2017 118 119 `````` induction f; cbn; intros approx_true var var_in_fV find_A; set_tac. - subst. `````` 120 `````` Daisy_compute. `````` Heiko Becker committed Oct 30, 2017 121 `````` destruct (var mem dVars) eqn:?; set_tac; try congruence. `````` 122 123 `````` Daisy_compute. unfold isSupersetIntv. `````` Heiko Becker committed Oct 30, 2017 124 125 `````` apply andb_prop_intro; split; apply Is_true_eq_left; auto. `````` 126 `````` - Daisy_compute; try congruence. `````` Heiko Becker committed Oct 12, 2016 127 `````` apply IHf; try auto. `````` Heiko Becker committed Oct 30, 2017 128 `````` set_tac. `````` 129 `````` - Daisy_compute; try congruence. `````` Heiko Becker committed Sep 19, 2016 130 `````` destruct H. `````` Heiko Becker committed Oct 30, 2017 131 132 `````` + apply IHf1; try auto; set_tac. + apply IHf2; try auto; set_tac. `````` Nikita Zyuzin committed Dec 18, 2017 133 `````` - Daisy_compute; try congruence. `````` Nikita Zyuzin committed Oct 23, 2017 134 `````` destruct H. `````` Nikita Zyuzin committed Dec 18, 2017 135 136 137 138 139 `````` + apply IHf1; try auto; set_tac. + set_tac. destruct H. * apply IHf2; try auto; set_tac. * apply IHf3; try auto; set_tac. `````` 140 `````` - Daisy_compute; try congruence. `````` Heiko Becker committed Oct 30, 2017 141 `````` apply IHf; try auto; set_tac. `````` Heiko Becker committed Sep 19, 2016 142 143 ``````Qed. `````` Heiko Becker committed Aug 23, 2016 144 145 146 147 148 149 150 151 152 153 154 155 ``````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 156 ``````Lemma validBoundsDiv_uneq_zero e1 e2 A P V ivlo_e2 ivhi_e2 err: `````` Heiko Becker committed Nov 02, 2017 157 `````` DaisyMap.find (elt:=intv * error) e2 A = Some ((ivlo_e2,ivhi_e2), err) -> `````` Heiko Becker committed Oct 30, 2017 158 `````` validIntervalbounds (Binop Div e1 e2) A P V = true -> `````` Heiko Becker committed Oct 08, 2016 159 160 `````` (ivhi_e2 < 0) \/ (0 < ivlo_e2). Proof. `````` Heiko Becker committed Nov 02, 2017 161 `````` intros A_eq validBounds; cbn in *. `````` 162 `````` Daisy_compute; try congruence. `````` Heiko Becker committed Oct 09, 2016 163 `````` apply le_neq_bool_to_lt_prop; auto. `````` Heiko Becker committed Oct 08, 2016 164 ``````Qed. `````` = committed Apr 05, 2017 165 `````` `````` Heiko Becker committed Nov 02, 2017 166 167 ``````Definition dVars_range_valid (dVars:NatSet.t) (E:env) (A:analysisResult) :Prop := forall v, NatSet.In v dVars -> `````` 168 `````` exists vR iv err, `````` Heiko Becker committed Nov 02, 2017 169 `````` E v = Some vR /\ `````` 170 171 `````` DaisyMap.find (Var Q v) A = Some (iv, err) /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R. `````` Heiko Becker committed Nov 02, 2017 172 173 174 175 176 177 178 179 180 181 182 `````` 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. `````` 183 184 ``````Ltac kill_trivial_exists := match goal with `````` Heiko Becker committed Nov 03, 2017 185 186 `````` | [ |- 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 `````` 187 188 `````` end. `````` Heiko Becker committed Oct 30, 2017 189 ``````Theorem validIntervalbounds_sound (f:exp Q) (A:analysisResult) (P:precond) `````` Heiko Becker committed Jun 29, 2017 190 `````` fVars dVars (E:env) Gamma: `````` Heiko Becker committed Oct 30, 2017 191 `````` validIntervalbounds f A P dVars = true -> `````` Heiko Becker committed Nov 02, 2017 192 `````` dVars_range_valid dVars E A -> `````` Raphaël Monat committed Feb 28, 2017 193 `````` NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars -> `````` Heiko Becker committed Nov 02, 2017 194 195 `````` fVars_P_sound fVars E P -> vars_typed (NatSet.union fVars dVars) Gamma -> `````` 196 197 `````` exists iv err vR, DaisyMap.find f A = Some (iv, err) /\ `````` Heiko Becker committed Nov 02, 2017 198 `````` eval_exp E (toRMap Gamma) (toREval (toRExp f)) vR M0 /\ `````` 199 `````` (Q2R (fst iv) <= vR <= Q2R (snd iv))%R. `````` Heiko Becker committed Aug 21, 2016 200 ``````Proof. `````` Heiko Becker committed Jun 29, 2017 201 202 `````` induction f; intros valid_bounds valid_definedVars usedVars_subset valid_freeVars types_defined; `````` Heiko Becker committed Nov 02, 2017 203 `````` cbn in *. `````` 204 `````` - Daisy_compute. `````` Heiko Becker committed Nov 02, 2017 205 206 `````` destruct (NatSet.mem n dVars) eqn:?; simpl in *. + destruct (valid_definedVars n) `````` 207 `````` as [vR [iv_n [err_n [env_valid [map_n bounds_valid]]]]]; `````` Heiko Becker committed Nov 02, 2017 208 209 210 `````` try set_tac. rewrite map_n in *. inversion Heqo; subst. `````` 211 212 `````` kill_trivial_exists. eexists; split; [auto| split; try eauto ]. `````` Heiko Becker committed Jun 29, 2017 213 214 215 216 `````` 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 217 218 `````` + destruct (valid_freeVars n) as [vR [env_valid bounds_valid]]; set_tac; try auto. `````` Heiko Becker committed Jun 29, 2017 219 `````` assert (NatSet.In n fVars) by set_tac. `````` Heiko Becker committed Nov 02, 2017 220 221 `````` andb_to_prop valid_bounds. canonize_hyps; simpl in *. `````` 222 223 `````` kill_trivial_exists. eexists; split; [auto | split]. `````` Heiko Becker committed Nov 02, 2017 224 `````` * econstructor; try eauto. `````` 225 226 `````` destruct (types_defined n) as [m type_m]; set_tac. `````` Heiko Becker committed Jun 29, 2017 227 `````` match_simpl; auto. `````` Heiko Becker committed Nov 02, 2017 228 `````` * lra. `````` 229 230 231 232 `````` - Daisy_compute; canonize_hyps; simpl in *. kill_trivial_exists. exists (perturb (Q2R v) 0). split; [auto| split]. `````` Heiko Becker committed Nov 02, 2017 233 234 `````` + econstructor; try eauto. apply Rabs_0_equiv. + unfold perturb; simpl; lra. `````` 235 236 `````` - Daisy_compute; simpl in *; try congruence. destruct IHf as [iv_f [err_f [vF [iveq_f [eval_f valid_bounds_f]]]]]; `````` Heiko Becker committed Nov 02, 2017 237 `````` try auto. `````` 238 239 240 241 242 `````` 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 243 `````` [econstructor; eauto | ]]. `````` Heiko Becker committed Jun 29, 2017 244 245 `````` canonize_hyps. rewrite Q2R_opp in *. `````` 246 247 `````` simpl; lra. + rename L0 into nodiv0. `````` Heiko Becker committed Jun 29, 2017 248 `````` apply le_neq_bool_to_lt_prop in nodiv0. `````` 249 250 `````` kill_trivial_exists. exists (perturb (evalUnop Inv vF) 0); split; `````` Heiko Becker committed Nov 02, 2017 251 252 253 `````` [destruct i; auto | split]. * econstructor; eauto; try apply Rabs_0_equiv. (* Absence of division by zero *) `````` Heiko Becker committed Jun 29, 2017 254 255 256 `````` hnf. destruct nodiv0 as [nodiv0 | nodiv0]; apply Qlt_Rlt in nodiv0; rewrite Q2R0_is_0 in nodiv0; lra. * canonize_hyps. `````` 257 `````` pose proof (interval_inversion_valid ((Q2R (fst iv_f)),(Q2R (snd iv_f))) (a :=vF)) as inv_valid. `````` Heiko Becker committed Jun 29, 2017 258 259 260 261 262 `````` 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 263 `````` - apply L1. `````` Heiko Becker committed Jun 29, 2017 264 265 266 267 268 269 270 271 272 273 274 `````` - 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 275 `````` lra. `````` Heiko Becker committed Jun 29, 2017 276 277 278 279 280 281 282 283 284 285 286 287 288 `````` - 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. } `````` 289 290 `````` - Daisy_compute; try congruence. destruct IHf1 as [iv_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]]; `````` Heiko Becker committed Nov 02, 2017 291 `````` try auto; set_tac. `````` 292 `````` destruct IHf2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]]; `````` Heiko Becker committed Nov 02, 2017 293 `````` try auto; set_tac. `````` Heiko Becker committed Jun 29, 2017 294 295 `````` assert (M0 = join M0 M0) as M0_join by (cbv; auto); rewrite M0_join. `````` 296 `````` kill_trivial_exists. `````` Heiko Becker committed Jun 29, 2017 297 `````` exists (perturb (evalBinop b vF1 vF2) 0); `````` Heiko Becker committed Nov 02, 2017 298 299 `````` split; [destruct i; auto | ]. inversion env1; inversion env2; subst. `````` Heiko Becker committed Jun 29, 2017 300 301 302 `````` destruct b; simpl in *. * split; [econstructor; try congruence; apply Rabs_0_equiv | ]. `````` 303 304 305 `````` 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 306 307 308 `````` specialize (valid_add vF1 vF2 valid_f1 valid_f2). unfold isSupersetIntv in R. andb_to_prop R. `````` Heiko Becker committed Nov 02, 2017 309 `````` canonize_hyps; simpl in *. `````` Heiko Becker committed Jun 29, 2017 310 311 `````` repeat rewrite <- Q2R_plus in *; rewrite <- Q2R_min4, <- Q2R_max4 in *. `````` Heiko Becker committed Nov 02, 2017 312 `````` unfold perturb. lra. `````` Heiko Becker committed Jun 29, 2017 313 314 `````` * split; [econstructor; try congruence; apply Rabs_0_equiv |]. `````` 315 316 `````` 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 317 `````` as valid_sub. `````` Heiko Becker committed Jun 29, 2017 318 319 320 `````` specialize (valid_sub vF1 vF2 valid_f1 valid_f2). unfold isSupersetIntv in R. andb_to_prop R. `````` Heiko Becker committed Nov 02, 2017 321 `````` canonize_hyps; simpl in *. `````` Heiko Becker committed Jun 29, 2017 322 323 324 `````` repeat rewrite <- Q2R_opp in *; repeat rewrite <- Q2R_plus in *; rewrite <- Q2R_min4, <- Q2R_max4 in *. `````` Heiko Becker committed Nov 02, 2017 325 `````` unfold perturb; lra. `````` Heiko Becker committed Jun 29, 2017 326 327 `````` * split; [ econstructor; try congruence; apply Rabs_0_equiv |]. `````` 328 329 `````` 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 330 `````` as valid_mul. `````` Heiko Becker committed Jun 29, 2017 331 332 333 `````` specialize (valid_mul vF1 vF2 valid_f1 valid_f2). unfold isSupersetIntv in R. andb_to_prop R. `````` Heiko Becker committed Nov 02, 2017 334 `````` canonize_hyps; simpl in *. `````` Heiko Becker committed Jun 29, 2017 335 336 `````` repeat rewrite <- Q2R_mult in *; rewrite <- Q2R_min4, <- Q2R_max4 in *. `````` Heiko Becker committed Nov 02, 2017 337 `````` unfold perturb; lra. `````` Heiko Becker committed Jun 29, 2017 338 339 340 341 342 343 344 345 `````` * 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 346 `````` { pose proof (interval_division_valid (a:=vF1) (b:=vF2) `````` 347 348 `````` ((Q2R (fst iv_f1)), Q2R (snd iv_f1)) (Q2R (fst iv_f2), Q2R (snd iv_f2))) `````` Heiko Becker committed Nov 02, 2017 349 `````` as valid_div. `````` Heiko Becker committed Jun 29, 2017 350 351 352 `````` simpl in *. destruct valid_div; try auto. - destruct L; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto. `````` 353 `````` - assert (~ (snd iv_f2) == 0). `````` Heiko Becker committed Jun 29, 2017 354 `````` { hnf; intros. destruct L; try lra. `````` 355 `````` assert (0 < (snd iv_f2)) by (apply Rlt_Qlt; apply Qlt_Rlt in H2; lra). `````` Heiko Becker committed Jun 29, 2017 356 `````` lra. } `````` 357 `````` assert (~ (fst iv_f2) == 0). `````` Heiko Becker committed Jun 29, 2017 358 `````` { hnf; intros; destruct L; try lra. `````` 359 `````` assert ((fst iv_f2) < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H3; lra). `````` Heiko Becker committed Jun 29, 2017 360 361 362 363 364 365 366 `````` lra. } repeat (rewrite <- Q2R_inv in *; try auto). repeat rewrite <- Q2R_mult in *. rewrite <- Q2R_min4, <- Q2R_max4 in *. unfold perturb. lra. } `````` Nikita Zyuzin committed Dec 18, 2017 367 368 369 370 `````` - Daisy_compute; try congruence. 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 371 372 `````` assert (M0 = join3 M0 M0 M0) as M0_join by (cbv; auto); rewrite M0_join. `````` Nikita Zyuzin committed Dec 18, 2017 373 374 375 376 377 `````` 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 378 379 `````` * 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 380 `````` 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 381 `````` 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 382 `````` rewrite Heqiv_f23prod in valid_add, valid_mul. `````` Nikita Zyuzin committed Oct 23, 2017 383 384 385 386 387 388 389 390 `````` 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 391 `````` unfold evalFma, evalBinop, perturb. `````` Nikita Zyuzin committed Oct 23, 2017 392 `````` lra. `````` Heiko Becker committed Nov 02, 2017 393 `````` - match_simpl. `````` Heiko Becker committed Jun 29, 2017 394 `````` andb_to_prop valid_bounds. `````` Heiko Becker committed Nov 02, 2017 395 `````` match_simpl. `````` 396 `````` destruct IHf as [iv_f [err_f [vF [env_f [eval_f valid_f]]]]]; `````` Heiko Becker committed Nov 02, 2017 397 398 `````` try auto. inversion env_f; subst. `````` 399 `````` kill_trivial_exists. `````` Heiko Becker committed Jun 29, 2017 400 `````` exists (perturb vF 0). `````` Heiko Becker committed Nov 02, 2017 401 `````` split; [destruct i; try auto |]. `````` Heiko Becker committed Jun 29, 2017 402 `````` split; [try econstructor; try eauto; try apply Rabs_0_equiv; unfold isMorePrecise; auto |]. `````` Heiko Becker committed Nov 02, 2017 403 404 405 `````` unfold isSupersetIntv in *; andb_to_prop R. canonize_hyps; simpl in *. unfold perturb; lra. `````` Heiko Becker committed Jun 29, 2017 406 407 ``````Qed. `````` Heiko Becker committed Aug 28, 2017 408 ``````Lemma Rmap_updVars_comm Gamma n m: `````` Heiko Becker committed Jun 29, 2017 409 410 411 412 413 414 415 `````` 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 416 ``````Lemma swap_Gamma_eval_exp e E vR m Gamma1 Gamma2: `````` Heiko Becker committed Jun 29, 2017 417 418 419 420 421 422 423 424 425 426 427 428 `````` (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 429 ``````Lemma swap_Gamma_bstep f E vR m Gamma1 Gamma2 : `````` Heiko Becker committed Jun 29, 2017 430 431 432 433 434 435 `````` (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 436 `````` - inversion eval_f; subst. `````` Heiko Becker committed Jun 29, 2017 437 `````` econstructor; try eauto. `````` Heiko Becker committed Aug 28, 2017 438 `````` + eapply swap_Gamma_eval_exp; eauto. `````` Heiko Becker committed Jun 29, 2017 439 440 441 442 443 444 `````` + 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 445 `````` eapply swap_Gamma_eval_exp; eauto. `````` Heiko Becker committed Oct 13, 2016 446 ``````Qed. `````` Heiko Becker committed Feb 03, 2017 447 `````` `````` Heiko Becker committed Oct 30, 2017 448 ``````Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult) Gamma: `````` Heiko Becker committed Nov 02, 2017 449 `````` forall E fVars dVars outVars P, `````` = committed Apr 06, 2017 450 `````` ssa f (NatSet.union fVars dVars) outVars -> `````` Heiko Becker committed Nov 02, 2017 451 452 453 `````` dVars_range_valid dVars E A -> fVars_P_sound fVars E P -> vars_typed (NatSet.union fVars dVars) Gamma -> `````` = committed Apr 06, 2017 454 `````` NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars -> `````` Heiko Becker committed Oct 30, 2017 455 `````` validIntervalboundsCmd f A P dVars = true -> `````` 456 457 `````` exists iv_e err_e vR, DaisyMap.find (getRetExp f) A = Some (iv_e, err_e) /\ `````` Heiko Becker committed Jun 29, 2017 458 `````` bstep (toREvalCmd (toRCmd f)) E (toRMap Gamma) vR M0 /\ `````` 459 `````` (Q2R (fst iv_e) <= vR <= Q2R (snd iv_e))%R. `````` = committed Apr 06, 2017 460 ``````Proof. `````` Heiko Becker committed Jun 29, 2017 461 `````` revert Gamma. `````` = committed Apr 06, 2017 462 `````` induction f; `````` Heiko Becker committed Nov 02, 2017 463 464 `````` intros * ssa_f dVars_sound fVars_valid types_valid usedVars_subset valid_bounds_f; cbn in *. `````` 465 `````` - Daisy_compute. `````` = committed Apr 06, 2017 466 `````` inversion ssa_f; subst. `````` Heiko Becker committed Nov 02, 2017 467 468 `````` canonize_hyps. pose proof (validIntervalbounds_sound e (Gamma:=Gamma) (E:=E) (fVars:=fVars) L) as validIV_e. `````` 469 `````` destruct validIV_e as [iv_e [err_v [v [find_v [eval_e valid_bounds_e]]]]]; `````` Heiko Becker committed Nov 02, 2017 470 471 `````` try auto. { set_tac. repeat split; auto. `````` Heiko Becker committed Jun 29, 2017 472 473 `````` hnf; intros; subst. set_tac. } `````` Heiko Becker committed Nov 02, 2017 474 `````` rewrite find_v in *; inversion Heqo; subst. `````` Heiko Becker committed Jun 29, 2017 475 476 `````` 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 477 478 479 480 481 `````` + 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. `````` 482 `````` + edestruct IHf as [iv_f [err_f [vR [env_f [eval_f valid_bounds_f]]]]]; `````` Heiko Becker committed Nov 02, 2017 483 `````` try eauto. `````` Heiko Becker committed Sep 05, 2017 484 `````` eapply ssa_equal_set. symmetry in H. apply H. apply H7. `````` Heiko Becker committed Jun 29, 2017 485 486 487 488 489 490 `````` * 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. `````` 491 `````` exists v; eexists; eexists; repeat split; try eauto; simpl in *; lra. } `````` Heiko Becker committed Nov 02, 2017 492 493 494 `````` { apply dVars_sound. set_tac. destruct mem_v0 as [? | [? ?]]; try auto. `````` Heiko Becker committed Jun 29, 2017 495 `````` rewrite Nat.eqb_neq in v0_eq. `````` Heiko Becker committed Nov 02, 2017 496 `````` congruence. } `````` Heiko Becker committed Jun 29, 2017 497 498 499 500 `````` * 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 501 502 `````` 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 503 504 505 `````` * intros x x_contained. set_tac. destruct x_contained as [x_free | x_def]. `````` Heiko Becker committed Nov 02, 2017 506 `````` { destruct (types_valid x) as [m_x Gamma_x]; try set_tac. `````` Heiko Becker committed Jun 29, 2017 507 508 509 510 511 `````` 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 512 `````` { set_tac. `````` Heiko Becker committed Jun 29, 2017 513 514 `````` destruct x_def as [x_n | x_def]; subst. - exists M0; unfold updDefVars; rewrite Nat.eqb_refl; auto. `````` Heiko Becker committed Nov 02, 2017 515 516 517 518 519 520 `````` - 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 521 522 523 524 `````` * 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 525 `````` apply usedVars_subset. `````` Heiko Becker committed Jun 29, 2017 526 `````` simpl. `````` = committed Apr 06, 2017 527 528 529 `````` rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. repeat split; try auto. { hnf; intros; subst. `````` Heiko Becker committed Jun 29, 2017 530 531 532 533 534 `````` apply a_no_dVar. rewrite NatSet.add_spec; auto. } { hnf; intros a_dVar. apply a_no_dVar. rewrite NatSet.add_spec; auto. } `````` 535 `````` * simpl. exists iv_f, err_f, vR; repeat split; try auto; try lra. `````` Heiko Becker committed Nov 02, 2017 536 `````` econstructor; try eauto. `````` Heiko Becker committed Aug 28, 2017 537 `````` eapply swap_Gamma_bstep with (Gamma1 := toRMap (updDefVars n M0 Gamma)) ; try eauto. `````` Heiko Becker committed Sep 05, 2017 538 `````` intros n1; erewrite Rmap_updVars_comm; eauto. `````` = committed Apr 06, 2017 539 `````` - unfold validIntervalboundsCmd in valid_bounds_f. `````` Heiko Becker committed Nov 02, 2017 540 `````` pose proof (validIntervalbounds_sound e (E:=E) (Gamma:=Gamma) valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e. `````` 541 `````` destruct valid_iv_e as [?[?[? [? [? ?]]]]]; try auto. `````` Heiko Becker committed Nov 02, 2017 542 `````` simpl in *. repeat eexists; repeat split; try eauto; [econstructor; eauto| | ]; lra. `````` Nikita Zyuzin committed Oct 23, 2017 543 ``Qed.``