IntervalValidation.v 25.1 KB
Newer Older
Heiko Becker's avatar
Heiko Becker committed
1
(**
Heiko Becker's avatar
Heiko Becker committed
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's avatar
Heiko Becker committed
7
**)
8
Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List Coq.micromega.Psatz.
9
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps.
10 11
Require Import Daisy.Infra.Ltacs Daisy.Infra.RealSimps.
Require Export Daisy.IntervalArithQ Daisy.IntervalArith Daisy.ssaPrgs.
12

13
Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond) (validVars:NatSet.t) :=
14 15
  let (intv, _) := absenv e in
    match e with
16 17 18 19
    | Var _ v =>
      if NatSet.mem v validVars
      then true
      else isSupersetIntv (P v) intv && (Qleb (ivlo (P v)) (ivhi (P v)))
Heiko Becker's avatar
Heiko Becker committed
20 21
    | Const n => isSupersetIntv (n,n) intv
    | Unop o f =>
22 23 24
      if validIntervalbounds f absenv P validVars
      then
        let (iv, _) := absenv f in
Heiko Becker's avatar
Heiko Becker committed
25
        match o with
26
        | Neg =>
Heiko Becker's avatar
Heiko Becker committed
27
          let new_iv := negateIntv iv in
28 29
          isSupersetIntv new_iv intv
        | Inv =>
30 31 32 33 34 35
          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
Heiko Becker's avatar
Heiko Becker committed
36
        end
37
      else false
Heiko Becker's avatar
Heiko Becker committed
38
    | Binop op f1 f2 =>
39 40 41 42 43
      if ((validIntervalbounds f1 absenv P validVars) &&
          (validIntervalbounds f2 absenv P validVars))
      then
        let (iv1,_) := absenv f1 in
        let (iv2,_) := absenv f2 in
Heiko Becker's avatar
Heiko Becker committed
44
          match op with
45 46 47 48 49 50 51 52 53
          | 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's avatar
Heiko Becker committed
54
          | Div =>
55 56 57 58 59 60
            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
61
          end
62
      else false
63 64
    end.

65
Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) (validVars:NatSet.t) :bool:=
66
  match f with
67
  | Let x e g =>
68 69 70 71 72
    if (validIntervalbounds e absenv P validVars &&
        Qeq_bool (fst (fst (absenv e))) (fst (fst (absenv (Var Q x)))) &&
        Qeq_bool (snd (fst (absenv e))) (snd (fst (absenv (Var Q x)))))
    then validIntervalboundsCmd g absenv P (NatSet.add x validVars)
    else false
73 74
  |Ret e =>
   validIntervalbounds e absenv P validVars
75 76 77 78
  end.

Theorem ivbounds_approximatesPrecond_sound f absenv P V:
  validIntervalbounds f absenv P V = true ->
Heiko Becker's avatar
Heiko Becker committed
79
  forall v, NatSet.In v (NatSet.diff (usedVars f) V) ->
80
       Is_true(isSupersetIntv (P v) (fst (absenv (Var Q v)))).
81
Proof.
Heiko Becker's avatar
Heiko Becker committed
82
  induction f; unfold validIntervalbounds.
83
  - intros approx_true v v_in_fV; simpl in *.
84 85 86 87 88 89 90 91
    rewrite NatSet.diff_spec in v_in_fV.
    rewrite NatSet.singleton_spec in v_in_fV;
      destruct v_in_fV; subst.
    destruct (absenv (Var Q n)); simpl in *.
    case_eq (NatSet.mem n V); intros case_mem;
      rewrite case_mem in approx_true; simpl in *.
    + rewrite NatSet.mem_spec in case_mem.
      contradiction.
92 93 94
    + apply Is_true_eq_left in approx_true.
      apply andb_prop_elim in approx_true.
      destruct approx_true; auto.
95 96
  - intros approx_true v0 v_in_fV; simpl in *.
    inversion v_in_fV.
Heiko Becker's avatar
Heiko Becker committed
97 98 99 100 101 102 103 104
  - intros approx_unary_true v v_in_fV.
    unfold freeVars in v_in_fV.
    apply Is_true_eq_left in approx_unary_true.
    destruct (absenv (Unop u f)); destruct (absenv f); simpl in *.
    apply andb_prop_elim in approx_unary_true.
    destruct approx_unary_true.
    apply IHf; try auto.
    apply Is_true_eq_true; auto.
105
  - intros approx_bin_true v v_in_fV.
106 107 108 109
    simpl in v_in_fV.
    rewrite NatSet.diff_spec in v_in_fV.
    destruct v_in_fV as [ v_in_fV v_not_in_V].
    rewrite NatSet.union_spec in v_in_fV.
110
    apply Is_true_eq_left in approx_bin_true.
Heiko Becker's avatar
Heiko Becker committed
111
    destruct (absenv (Binop b f1 f2)); destruct (absenv f1); destruct (absenv f2); simpl in *.
112 113 114 115
    apply andb_prop_elim in approx_bin_true.
    destruct approx_bin_true.
    apply andb_prop_elim in H.
    destruct H.
116
    destruct v_in_fV.
Heiko Becker's avatar
Heiko Becker committed
117
    + apply IHf1; auto.
118
      apply Is_true_eq_true; auto.
119
      rewrite NatSet.diff_spec; split; auto.
Heiko Becker's avatar
Heiko Becker committed
120
    + apply IHf2; auto.
121
      apply Is_true_eq_true; auto.
122
      rewrite NatSet.diff_spec; split; auto.
123 124
Qed.

Heiko Becker's avatar
Heiko Becker committed
125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
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.

Ltac env_assert absenv e name :=
  assert (exists iv err, absenv e = (iv,err)) as name by (destruct (absenv e); repeat eexists; auto).

140
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) fVars dVars E:
Heiko Becker's avatar
Heiko Becker committed
141
  forall vR,
142 143
    validIntervalbounds f absenv P dVars = true ->
    (forall v, NatSet.mem v dVars = true ->
144
          exists vR, E v = Some vR /\
145
                (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
Heiko Becker's avatar
Heiko Becker committed
146
    NatSet.Subset (NatSet.diff (usedVars f) dVars) fVars ->
147
    (forall v, NatSet.mem v fVars = true ->
148 149 150
          exists vR, E v = Some vR /\
                (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
    eval_exp 0%R E (toRExp f) vR ->
Heiko Becker's avatar
Heiko Becker committed
151
  (Q2R (fst (fst(absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R.
152
Proof.
153
  induction f; intros vR valid_bounds valid_definedVars freeVars_subset valid_freeVars eval_f.
154 155 156 157 158 159
  - unfold validIntervalbounds in valid_bounds.
    env_assert absenv (Var Q n) absenv_var.
    destruct absenv_var as [ iv [err absenv_var]].
    specialize (valid_freeVars n).
    rewrite absenv_var in *; simpl in *.
    inversion eval_f; subst.
160
    case_eq (NatSet.mem n dVars); intros case_mem; rewrite case_mem in *; simpl in *.
161 162
    + specialize (valid_definedVars n case_mem).
      destruct valid_definedVars as [vR' [E_n_eq precond_sound]].
163 164
      rewrite E_n_eq in *.
      inversion H0; subst.
165
      rewrite absenv_var in *; auto.
166 167 168
    + repeat (rewrite delta_0_deterministic in *; try auto).
      unfold isSupersetIntv in valid_bounds.
      andb_to_prop valid_bounds.
169 170 171 172
      apply Qle_bool_iff in L0;
        apply Qle_bool_iff in R0.
      apply Qle_Rle in L0;
        apply Qle_Rle in R0.
173
      simpl in *.
174 175 176 177 178 179 180
      assert (NatSet.mem n fVars = true) as in_fVars.
      * assert (NatSet.In n (NatSet.singleton n))
          as in_singleton by (rewrite NatSet.singleton_spec; auto).
        rewrite NatSet.mem_spec.
        hnf in freeVars_subset.
        apply freeVars_subset.
        rewrite NatSet.diff_spec, NatSet.singleton_spec.
181
        split; try auto.
182 183 184 185
        hnf; intros in_dVars.
        rewrite <- NatSet.mem_spec in in_dVars.
        rewrite in_dVars in case_mem; congruence.
      * specialize (valid_freeVars in_fVars);
186 187 188
          destruct valid_freeVars as [vR' [vR_def P_valid]].
        rewrite vR_def in H0; inversion H0; subst.
        lra.
189
  - unfold validIntervalbounds in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
190
    destruct (absenv (Const v)) as [intv err]; simpl.
191 192
    apply Is_true_eq_left in valid_bounds.
    apply andb_prop_elim in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
193
    destruct valid_bounds as [valid_lo valid_hi].
Heiko Becker's avatar
Heiko Becker committed
194
    inversion eval_f; subst.
195
    rewrite delta_0_deterministic; auto.
196 197
    unfold contained; simpl.
    split.
Heiko Becker's avatar
Heiko Becker committed
198
    + apply Is_true_eq_true in valid_lo.
199
      unfold Qleb in *.
Heiko Becker's avatar
Heiko Becker committed
200 201 202 203 204 205
      apply Qle_bool_iff in valid_lo.
      apply Qle_Rle in valid_lo; auto.
    + apply Is_true_eq_true in valid_hi.
      unfold Qleb in *.
      apply Qle_bool_iff in valid_hi.
      apply Qle_Rle in valid_hi; auto.
206
  - case_eq (absenv (Unop u f)); intros intv err absenv_unop.
Heiko Becker's avatar
Heiko Becker committed
207 208 209 210 211 212 213 214 215 216
    destruct intv as [unop_lo unop_hi]; simpl.
    unfold validIntervalbounds in valid_bounds.
    rewrite absenv_unop in valid_bounds.
    case_eq (absenv f); intros intv_f err_f absenv_f.
    rewrite absenv_f in valid_bounds.
    apply Is_true_eq_left in valid_bounds.
    apply andb_prop_elim in valid_bounds.
    destruct valid_bounds as [valid_rec valid_unop].
    apply Is_true_eq_true in valid_rec.
    inversion eval_f; subst.
217
    + specialize (IHf v1 valid_rec valid_definedVars freeVars_subset valid_freeVars H2).
Heiko Becker's avatar
Heiko Becker committed
218
      rewrite absenv_f in IHf; simpl in IHf.
219 220 221 222 223 224
      (* TODO: Make lemma *)
      unfold isSupersetIntv in valid_unop.
      apply andb_prop_elim in valid_unop.
      destruct valid_unop as [valid_lo valid_hi].
      apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
      apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
225
      pose proof (interval_negation_valid (iv :=(Q2R (fst intv_f),(Q2R (snd intv_f)))) (a :=v1)) as negation_valid.
226 227 228
      unfold contained, negateInterval in negation_valid; simpl in *.
      apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
      destruct IHf.
229
      split.
230 231 232 233 234
      * eapply Rle_trans. apply valid_lo.
        rewrite Q2R_opp; lra.
      * eapply Rle_trans.
        Focus 2. apply valid_hi.
        rewrite Q2R_opp; lra.
235
    + specialize (IHf v1 valid_rec valid_definedVars freeVars_subset valid_freeVars H2).
Heiko Becker's avatar
Heiko Becker committed
236
      rewrite absenv_f in IHf; simpl in IHf.
237
      apply andb_prop_elim in valid_unop.
238
      destruct valid_unop as [nodiv0 valid_unop].
239 240 241 242 243 244 245 246 247 248 249 250
      (* TODO: Make lemma *)
      unfold isSupersetIntv in valid_unop.
      apply andb_prop_elim in valid_unop.
      destruct valid_unop as [valid_lo valid_hi].
      apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
      apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
      assert ((Q2R (ivhi intv_f) < 0)%R \/ (0 < Q2R (ivlo intv_f))%R) as nodiv0_prop.
       * apply Is_true_eq_true in nodiv0.
         apply le_neq_bool_to_lt_prop in nodiv0.
         destruct nodiv0.
         { left; rewrite <- Q2R0_is_0; apply Qlt_Rlt; auto. }
         { right; rewrite <- Q2R0_is_0; apply Qlt_Rlt; auto. }
251
       * pose proof (interval_inversion_valid (iv :=(Q2R (fst intv_f),(Q2R (snd intv_f)))) (a :=v1)) as inv_valid.
252 253 254
         unfold contained, invertInterval in inv_valid; simpl in *.
         apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
         destruct IHf.
255
         rewrite delta_0_deterministic; auto.
256
         unfold perturb; split.
257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275
         { eapply Rle_trans. apply valid_lo.
           destruct nodiv0_prop as [nodiv0_neg | nodiv0_pos].
           (* TODO: Extract lemma maybe *)
           - assert (0 < - (Q2R (snd intv_f)))%R as negation_pos by lra.
             assert (- (Q2R (snd intv_f)) <= - v1)%R as negation_flipped_hi by lra.
             apply Rinv_le_contravar in negation_flipped_hi; try auto.
             rewrite <- Ropp_inv_permute in negation_flipped_hi; try lra.
             rewrite <- Ropp_inv_permute in negation_flipped_hi; try lra.
             apply Ropp_le_contravar in negation_flipped_hi.
             repeat rewrite Ropp_involutive in negation_flipped_hi;
               rewrite Q2R_inv; auto.
             hnf; intros is_0.
             rewrite <- Q2R0_is_0 in nodiv0_neg.
             apply Rlt_Qlt in nodiv0_neg; lra.
           - rewrite Q2R_inv.
             apply Rinv_le_contravar; try lra.
             hnf; intros is_0.
             assert (Q2R (fst intv_f) <= Q2R (snd intv_f))%R by lra.
             rewrite <- Q2R0_is_0 in nodiv0_pos.
276
             apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H3; lra.
277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300
         }
         { eapply Rle_trans.
           Focus 2. apply valid_hi.
           destruct nodiv0_prop as [nodiv0_neg | nodiv0_pos].
           - assert (Q2R (fst intv_f) < 0)%R as fst_lt_0 by lra.
             assert (0 < - (Q2R (fst intv_f)))%R as negation_pos by lra.
             assert (- v1 <= - (Q2R (fst intv_f)))%R as negation_flipped_lo by lra.
             apply Rinv_le_contravar in negation_flipped_lo; try auto.
             rewrite <- Ropp_inv_permute in negation_flipped_lo; try lra.
             rewrite <- Ropp_inv_permute in negation_flipped_lo; try lra.
             apply Ropp_le_contravar in negation_flipped_lo.
             repeat rewrite Ropp_involutive in negation_flipped_lo;
               rewrite Q2R_inv; auto.
             hnf; intros is_0.
             rewrite <- Q2R0_is_0 in negation_pos.
             rewrite <- Q2R_opp in negation_pos.
             apply Rlt_Qlt in negation_pos; lra.
             assert (0 < - (Q2R (snd intv_f)))%R by lra.
             lra.
           - rewrite Q2R_inv.
             apply Rinv_le_contravar; try lra.
             hnf; intros is_0.
             assert (Q2R (fst intv_f) <= Q2R (snd intv_f))%R by lra.
             rewrite <- Q2R0_is_0 in nodiv0_pos.
301
             apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H3; lra.
302
         }
303
  - inversion eval_f; subst.
304 305
    rewrite delta_0_deterministic in eval_f; auto.
    rewrite delta_0_deterministic; auto.
Heiko Becker's avatar
Heiko Becker committed
306
    simpl in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
307 308 309 310
    case_eq (absenv (Binop b f1 f2)); intros iv err absenv_bin.
    case_eq (absenv f1); intros iv1 err1 absenv_f1.
    case_eq (absenv f2); intros iv2 err2 absenv_f2.
    rewrite absenv_bin, absenv_f1, absenv_f2 in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
311 312 313 314 315 316
    apply Is_true_eq_left in valid_bounds.
    apply andb_prop_elim in valid_bounds.
    destruct valid_bounds as [valid_rec valid_bin].
    apply andb_prop_elim in valid_rec.
    destruct valid_rec as [valid_e1 valid_e2].
    apply Is_true_eq_true in valid_e1; apply Is_true_eq_true in  valid_e2.
317 318
    specialize (IHf1 v1 valid_e1 valid_definedVars);
      specialize (IHf2 v2 valid_e2 valid_definedVars).
Heiko Becker's avatar
Heiko Becker committed
319 320
    rewrite absenv_f1 in IHf1.
    rewrite absenv_f2 in IHf2.
321 322 323
    assert ((Q2R (fst (fst (iv1, err1))) <= v1 <= Q2R (snd (fst (iv1, err1))))%R) as valid_bounds_e1.
    + apply IHf1; try auto.
      intros v in_diff_e1.
324 325 326 327 328
      apply freeVars_subset.
      simpl. rewrite NatSet.diff_spec,NatSet.union_spec.
      rewrite NatSet.diff_spec in in_diff_e1.
      destruct in_diff_e1 as [ in_freeVars not_dVar].
      split; try auto.
329 330 331
    + assert (Q2R (fst (fst (iv2, err2))) <= v2 <= Q2R (snd (fst (iv2, err2))))%R as valid_bounds_e2.
      * apply IHf2; try auto.
        intros v in_diff_e2.
332 333 334 335
        apply freeVars_subset.
        simpl. rewrite NatSet.diff_spec, NatSet.union_spec.
        rewrite NatSet.diff_spec in in_diff_e2.
        destruct in_diff_e2; split; auto.
336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412
      * destruct b; simpl in *.
        { pose proof (interval_addition_valid (iv1 :=(Q2R (fst iv1),Q2R (snd iv1))) (iv2 :=(Q2R (fst iv2), Q2R (snd iv2)))) as valid_add.
          unfold validIntervalAdd in valid_add.
          specialize (valid_add v1 v2 valid_bounds_e1 valid_bounds_e2).
          unfold contained in valid_add.
          unfold isSupersetIntv in valid_bin.
          apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
          apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
          apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
          apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
          destruct valid_add as [valid_add_lo valid_add_hi].
          split.
          - eapply Rle_trans. apply valid_lo.
            unfold ivlo. unfold addIntv.
            simpl in valid_add_lo.
            repeat rewrite <- Q2R_plus in valid_add_lo.
            rewrite <- Q2R_min4 in valid_add_lo.
            unfold absIvUpd; auto.
          - eapply Rle_trans.
            Focus 2.
            apply valid_hi.
            unfold ivlo, addIntv.
            simpl in valid_add_hi.
            repeat rewrite <- Q2R_plus in valid_add_hi.
            rewrite <- Q2R_max4 in valid_add_hi.
            unfold absIvUpd; auto. }
        { pose proof (interval_subtraction_valid (iv1 := (Q2R (fst iv1),Q2R (snd iv1))) (iv2 :=(Q2R (fst iv2), Q2R (snd iv2)))) as valid_sub.
          specialize (valid_sub v1 v2 valid_bounds_e1 valid_bounds_e2).
          unfold contained in valid_sub.
          unfold isSupersetIntv in valid_bin.
          apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
          apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
          apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
          apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
          destruct valid_sub as [valid_sub_lo valid_sub_hi].
          split.
          - eapply Rle_trans. apply valid_lo.
            unfold ivlo. unfold subtractIntv.
            simpl in valid_sub_lo.
            repeat rewrite <- Rsub_eq_Ropp_Rplus in valid_sub_lo.
            repeat rewrite <- Q2R_minus in valid_sub_lo.
            rewrite <- Q2R_min4 in valid_sub_lo.
            unfold absIvUpd; auto.
          - eapply Rle_trans.
            Focus 2.
            apply valid_hi.
            unfold ivlo, addIntv.
            simpl in valid_sub_hi.
            repeat rewrite <- Rsub_eq_Ropp_Rplus in valid_sub_hi.
            repeat rewrite <- Q2R_minus in valid_sub_hi.
            rewrite <- Q2R_max4 in valid_sub_hi.
            unfold absIvUpd; auto. }
        { pose proof (interval_multiplication_valid (iv1 :=(Q2R (fst iv1),Q2R (snd iv1))) (iv2:=(Q2R (fst iv2), Q2R (snd iv2)))) as valid_mul.
          specialize (valid_mul v1 v2 valid_bounds_e1 valid_bounds_e2).
          unfold contained in valid_mul.
          unfold isSupersetIntv in valid_bin.
          apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
          apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
          apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
          apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
          destruct valid_mul as [valid_mul_lo valid_mul_hi].
          split.
          - eapply Rle_trans. apply valid_lo.
            unfold ivlo. unfold multIntv.
            simpl in valid_mul_lo.
            repeat rewrite <- Q2R_mult in valid_mul_lo.
            rewrite <- Q2R_min4 in valid_mul_lo.
            unfold absIvUpd; auto.
          - eapply Rle_trans.
            Focus 2.
            apply valid_hi.
            unfold ivlo, addIntv.
            simpl in valid_mul_hi.
            repeat rewrite <- Q2R_mult in valid_mul_hi.
            rewrite <- Q2R_max4 in valid_mul_hi.
            unfold absIvUpd; auto. }
        { pose proof (interval_division_valid (a:=v1) (b:=v2) (iv1:=(Q2R (fst iv1), Q2R (snd iv1))) (iv2:=(Q2R (fst iv2),Q2R (snd iv2)))) as valid_div.
413
          rewrite <- andb_lazy_alt in valid_bin.
414 415
          unfold contained in valid_div.
          unfold isSupersetIntv in valid_bin.
416 417
          apply andb_prop_elim in valid_bin; destruct valid_bin as [nodiv0 valid_bin].
          (** CONTINUE **)
418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464
          apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
          apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
          apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
          apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
          apply orb_prop_elim in nodiv0.
          assert (snd iv2 < 0 \/ 0 < fst iv2).
          - destruct nodiv0 as [lt_0 | lt_0];
              apply andb_prop_elim in lt_0; destruct lt_0 as [le_0 neq_0];
                apply Is_true_eq_true in le_0; apply Is_true_eq_true in neq_0;
                  apply negb_true_iff in neq_0; apply Qeq_bool_neq in neq_0;
                    rewrite Qle_bool_iff in le_0;
                    rewrite Qle_lteq in le_0; destruct le_0 as [lt_0 | eq_0];
                      [ | exfalso; apply neq_0; auto | | exfalso; apply neq_0; symmetry; auto]; auto.
          - destruct valid_div as [valid_div_lo valid_div_hi]; simpl; try auto.
            + rewrite <- Q2R0_is_0.
              destruct H; [left | right]; apply Qlt_Rlt; auto.
            + unfold divideInterval, IVlo, IVhi in valid_div_lo, valid_div_hi.
              simpl in *.
              assert (Q2R (fst iv2) <= (Q2R (snd iv2)))%R by lra.
              assert (~ snd iv2 == 0).
              * destruct H; try lra.
                hnf; intros ivhi2_0.
                apply Rle_Qle in H0.
                rewrite ivhi2_0 in H0.
                lra.
              * assert (~ fst iv2 == 0).
                { destruct H; try lra.
                  hnf; intros ivlo2_0.
                  apply Rle_Qle in H0.
                  rewrite ivlo2_0 in H0.
                  lra. }
                { split.
                  - eapply Rle_trans. apply valid_lo.
                    unfold ivlo. unfold multIntv.
                    simpl in valid_div_lo.
                    rewrite <- Q2R_inv in valid_div_lo; [ | auto].
                    rewrite <- Q2R_inv in valid_div_lo; [ | auto].
                    repeat rewrite <- Q2R_mult in valid_div_lo.
                    rewrite <- Q2R_min4 in valid_div_lo; auto.
                  - eapply Rle_trans.
                    Focus 2.
                    apply valid_hi.
                    simpl in valid_div_hi.
                    rewrite <- Q2R_inv in valid_div_hi; [ | auto].
                    rewrite <- Q2R_inv in valid_div_hi; [ | auto].
                    repeat rewrite <- Q2R_mult in valid_div_hi.
                    rewrite <- Q2R_max4 in valid_div_hi; auto. } }
465
Qed.
466

467 468 469 470 471 472
Fixpoint getRetExp (V:Type) (f:cmd V) :=
  match f with
  |Let x e g => getRetExp g
  | Ret e => e
  end.

473
Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult):
474
  forall E vR fVars dVars outVars elo ehi err P,
Heiko Becker's avatar
Heiko Becker committed
475
    ssa f (NatSet.union fVars dVars) outVars ->
476 477
    bstep (toRCmd f) E 0%R vR  ->
    (forall v, NatSet.mem v dVars = true ->
478 479
          exists vR,
            E v = Some vR /\
480 481 482 483 484
            (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
    (forall v, NatSet.mem v fVars = true ->
          exists vR,
            E v = Some vR /\
            (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
485
    NatSet.Subset (NatSet.diff (freeVars f) dVars) fVars ->
486
    validIntervalboundsCmd f absenv P dVars = true ->
487
    absenv (getRetExp f) = ((elo, ehi), err) ->
Heiko Becker's avatar
Heiko Becker committed
488
    (Q2R elo <=  vR <= Q2R ehi)%R.
489 490
Proof.
  induction f;
491 492
    intros E vR fVars dVars outVars elo ehi err P ssa_f eval_f dVars_sound
           fVars_valid freeVars_subset valid_bounds_f absenv_f.
493 494 495 496
  - inversion ssa_f; subst.
    inversion eval_f; subst.
    unfold validIntervalboundsCmd in valid_bounds_f.
    andb_to_prop valid_bounds_f.
497 498
    inversion ssa_f; subst.
    specialize (IHf (updEnv n v E) vR fVars (NatSet.add n dVars)).
499
    eapply IHf; eauto.
500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560
    + assert (NatSet.Equal (NatSet.add n (NatSet.union fVars dVars)) (NatSet.union fVars (NatSet.add n dVars))).
      * hnf. intros a; split; intros in_set.
        { rewrite NatSet.add_spec, NatSet.union_spec in in_set.
          rewrite NatSet.union_spec, NatSet.add_spec.
          destruct in_set as [P1 | [ P2 | P3]]; auto. }
        { rewrite NatSet.add_spec, NatSet.union_spec.
          rewrite NatSet.union_spec, NatSet.add_spec in in_set.
          destruct in_set as [P1 | [ P2 | P3]]; auto. }
      * eapply ssa_equal_set; eauto.
        symmetry; eauto.
    + intros v0 mem_v0.
      unfold updEnv.
      case_eq (v0 =? n); intros v0_eq.
      * rename R1 into eq_lo;
          rename R0 into eq_hi.
        apply Qeq_bool_iff in eq_lo;
          apply Qeq_eqR in eq_lo.
        apply Qeq_bool_iff in eq_hi;
          apply Qeq_eqR in eq_hi.
        rewrite Nat.eqb_eq in v0_eq; subst.
        rewrite <- eq_lo, <- eq_hi.
        exists v; split; auto.
        eapply validIntervalbounds_sound; eauto.
        simpl in freeVars_subset.
        hnf. intros a in_freeVars.
        apply freeVars_subset.
        rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
        rewrite NatSet.diff_spec in in_freeVars.
        destruct in_freeVars as [ in_freeVars not_dVar].
        repeat split; try auto.
        { hnf; intros; subst.
          specialize (H2 n in_freeVars).
          rewrite <- NatSet.mem_spec in H2.
          rewrite H2 in H5; congruence. }
      * apply dVars_sound. rewrite NatSet.mem_spec.
        rewrite NatSet.mem_spec in mem_v0.
        rewrite NatSet.add_spec in mem_v0.
        destruct mem_v0; try auto.
        rewrite Nat.eqb_neq in v0_eq.
        exfalso; apply v0_eq; auto.
    + intros v0 mem_fVars.
      unfold updEnv.
      case_eq (v0 =? n); intros case_v0; auto.
      rewrite Nat.eqb_eq in case_v0; subst.
      assert (NatSet.mem n (NatSet.union fVars dVars) = true) as in_union.
      * rewrite NatSet.mem_spec, NatSet.union_spec; rewrite <- NatSet.mem_spec; auto.
      * rewrite in_union in *; congruence.
    + 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].
      apply freeVars_subset.
      simpl.
      rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
      repeat split; try auto.
      * hnf; intros; subst.
        apply a_no_dVar.
        rewrite NatSet.add_spec; auto.
      * hnf; intros a_dVar.
        apply a_no_dVar.
        rewrite NatSet.add_spec; auto.
561 562 563
  - unfold validIntervalboundsCmd in valid_bounds_f.
    inversion eval_f; subst.
    unfold updEnv.
564
    assert (Q2R (fst (fst (absenv e))) <= vR <= Q2R (snd (fst (absenv e))))%R.
565 566
    + eapply validIntervalbounds_sound; eauto.
    + simpl in *. rewrite absenv_f in *; auto.
567
Qed.