IntervalValidation.v 33.9 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
Require Import Daisy.Infra.Ltacs Daisy.Infra.RealSimps Daisy.Typing.
11
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
    | Var _ _ v =>
17 18 19
      if NatSet.mem v validVars
      then true
      else isSupersetIntv (P v) intv && (Qleb (ivlo (P v)) (ivhi (P v)))
20
    | Const _ n => isSupersetIntv (n,n) intv
Heiko Becker's avatar
Heiko Becker committed
21
    | 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
    | Downcast _ f1 =>
64 65 66
      let (iv1, _) := absenv f1 in
      andb (validIntervalbounds f1 absenv P validVars) (andb (isSupersetIntv intv iv1) (isSupersetIntv iv1 intv))
           (* TODO: intv = iv1 might be a hard constraint... *)
67 68
    end.

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

='s avatar
= committed
81
Theorem ivbounds_approximatesPrecond_sound f absenv P V Gamma mF:
82
  validIntervalbounds f absenv P V = true ->
='s avatar
= committed
83
  validType Gamma f mF ->
84
  forall v m, NatSet.In v (NatSet.diff (Expressions.usedVars f) V) ->
='s avatar
= committed
85 86
         Gamma (Var Q m v) = Some m ->
         Is_true(isSupersetIntv (P v) (fst (absenv (Var Q m v)))).
87
Proof.
Heiko Becker's avatar
Heiko Becker committed
88
  induction f; unfold validIntervalbounds.
='s avatar
= committed
89 90
  - simpl. intros approx_true valid_tf v m0 v_in_fV type_var; simpl in *.
    inversion valid_tf; subst.
91 92 93
    rewrite NatSet.diff_spec in v_in_fV.
    rewrite NatSet.singleton_spec in v_in_fV;
      destruct v_in_fV; subst.
='s avatar
= committed
94
    destruct (absenv (Var Q mF n)); simpl in *.
95 96 97 98
    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.
99 100 101
    + apply Is_true_eq_left in approx_true.
      apply andb_prop_elim in approx_true.
      destruct approx_true; auto.
102 103 104 105
  - intros approx_true v0 m0 v_in_fV typef; simpl in *.
    inversion v_in_fV. 
  - intros approx_unary_true v m0 v_in_fV typef; simpl in *.  
    unfold typeExpression in typef; inversion typef.
Heiko Becker's avatar
Heiko Becker committed
106
    apply Is_true_eq_left in approx_unary_true.
107
    simpl in *.
108
    destruct (absenv (Unop u f)); destruct (absenv f); simpl in *.
Heiko Becker's avatar
Heiko Becker committed
109 110 111 112
    apply andb_prop_elim in approx_unary_true.
    destruct approx_unary_true.
    apply IHf; try auto.
    apply Is_true_eq_true; auto.
113
  - intros approx_bin_true v m0 v_in_fV typef.
114 115 116 117
    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.
118
    apply Is_true_eq_left in approx_bin_true.
='s avatar
= committed
119 120 121 122 123
    case_eq (typeMap f1 (Var Q m0 v));
      case_eq (typeMap f2 (Var Q m0 v)); intros; auto; subst.
    + pose proof (typeMapVarDet _ _ _ H);
        pose proof (typeMapVarDet _ _ _ H0); subst.
      (* pose proof (detTypingBinop f1 f2 b _ _ typef H0 H) as [H01 H02]; subst. *)
124 125 126 127 128 129 130 131 132
      destruct (absenv (Binop b f1 f2)); destruct (absenv f1);
        destruct (absenv f2); simpl in *.
      apply andb_prop_elim in approx_bin_true.
      destruct approx_bin_true.
      apply andb_prop_elim in H1.
      destruct H1.
      apply IHf1; auto.
      apply Is_true_eq_true; auto.
      rewrite NatSet.diff_spec; split; auto.
133
      eapply typedVarIsUsed; eauto.
='s avatar
= committed
134
    + simpl in *; rewrite H0 in typef; inversion typef; subst.
135 136 137 138 139 140 141
      destruct (absenv (Binop b f1 f2)); destruct (absenv f1);
        destruct (absenv f2); simpl in *.
      apply andb_prop_elim in approx_bin_true.
      destruct approx_bin_true.
      apply andb_prop_elim in H1.
      destruct H1.
      apply IHf1; auto.
142
      apply Is_true_eq_true; auto.
143
      rewrite NatSet.diff_spec; split; auto.
144
      eapply typedVarIsUsed; eauto.
145 146 147 148 149 150 151 152
    + simpl in *; rewrite H0,H in typef; inversion typef; subst.
      destruct (absenv (Binop b f1 f2)); destruct (absenv f1);
        destruct (absenv f2); simpl in *.
      apply andb_prop_elim in approx_bin_true.
      destruct approx_bin_true.
      apply andb_prop_elim in H1.
      destruct H1.
      apply IHf2; auto.
153
      apply Is_true_eq_true; auto.
154
      rewrite NatSet.diff_spec; split; auto.
155
      eapply typedVarIsUsed; eauto.
156 157 158
    + simpl in *; rewrite H0,H in typef; inversion typef; subst.
  - intros approx_rnd_true v m0 v_in_fV typef.
    simpl in *; destruct (absenv (Downcast m f)); destruct (absenv f).
159 160 161 162 163 164
    apply Is_true_eq_left in approx_rnd_true.
    apply andb_prop_elim in approx_rnd_true.
    destruct approx_rnd_true.
    apply IHf; auto.
    apply Is_true_eq_true in H; auto.
Qed.
165

Heiko Becker's avatar
Heiko Becker committed
166 167 168 169 170 171 172 173 174 175 176 177 178 179 180
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).

181
Lemma validBoundsDiv_uneq_zero e1 e2 absenv P V ivlo_e2 ivhi_e2 err:
182
  absenv e2 = ((ivlo_e2,ivhi_e2), err) ->
183
  validIntervalbounds (Binop Div e1 e2) absenv P V = true ->
184 185 186 187 188 189 190
  (ivhi_e2 < 0) \/ (0 < ivlo_e2).
Proof.
  intros absenv_eq validBounds.
  unfold validIntervalbounds in validBounds.
  env_assert absenv (Binop Div e1 e2) abs_div; destruct abs_div as [iv_div [err_div abs_div]].
  env_assert absenv e1 abs_e1; destruct abs_e1 as [iv_e1 [err_e1 abs_e1]].
  rewrite abs_div, abs_e1, absenv_eq in validBounds.
191
  repeat (rewrite <- andb_lazy_alt in validBounds).
192 193 194
  apply Is_true_eq_left in validBounds.
  apply andb_prop_elim in validBounds.
  destruct validBounds as [_ validBounds]; apply andb_prop_elim in validBounds.
195
  destruct validBounds as [nodiv0 _].
196
  apply Is_true_eq_true in nodiv0.
197
  unfold isSupersetIntv in *; simpl in *.
198
  apply le_neq_bool_to_lt_prop; auto.
199 200
Qed.

201
Lemma validVarsUnfolding_l (E:env) (absenv:analysisResult) (f1 f2: exp Q) dVars (b:binop) m0:
='s avatar
= committed
202
  (typeMap (Binop b f1 f2)) (Binop b f1 f2) = Some m0 ->
203 204
  (forall (v : NatSet.elt) (m : mType),
      NatSet.mem v dVars = true ->
='s avatar
= committed
205
      typeMap (Binop b f1 f2) (Var Q m v) = Some m ->
206 207 208 209 210 211
      exists vR : R,
        E v = Some (vR, M0) /\
        (Q2R (fst (fst (absenv (Var Q m v)))) <= vR <= Q2R (snd (fst (absenv (Var Q m v)))))%R)
  ->
  (forall (v : NatSet.elt) (m : mType),
      NatSet.mem v dVars = true ->
='s avatar
= committed
212
      typeMap f1 (Var Q m v) = Some m ->
213 214 215 216 217 218
      exists vR : R,
        E v = Some (vR, M0) /\
        (Q2R (fst (fst (absenv (Var Q m v)))) <= vR <= Q2R (snd (fst (absenv (Var Q m v)))))%R).
Proof.
  intros.
  specialize (H0 v m H1).
='s avatar
= committed
219
  case_eq (typeMap f2 (Var Q m v)); intros; auto.
220 221
  - case_eq (mTypeEqBool m m1); intros.
    + (*apply EquivEqBoolEq in H4. ; rewrite <- H4 in H3.*)
='s avatar
= committed
222 223 224
      assert (typeMap (Binop b f1 f2) (Var Q m v) = Some m).
      simpl typeMap. rewrite H2. 
      auto. 
225
      specialize (H0 H5); auto.
='s avatar
= committed
226
    + pose proof (typeMapVarDet _ _ _ H3).
227 228 229
      rewrite H5 in H4.
      rewrite mTypeEqBool_refl in H4.
      inversion H4.
='s avatar
= committed
230
  - assert (typeMap (Binop b f1 f2) (Var Q m v) = Some m) by (simpl; rewrite H2; auto).
231 232
    specialize (H0 H4).
    auto.
='s avatar
= committed
233
Qed.
234

235
Lemma validVarsUnfolding_r (E:env) (absenv:analysisResult) (f1 f2: exp Q) dVars (b:binop) m0:
='s avatar
= committed
236
  (typeMap (Binop b f1 f2)) (Binop b f1 f2) = Some m0 ->
237 238
  (forall (v : NatSet.elt) (m : mType),
      NatSet.mem v dVars = true ->
='s avatar
= committed
239
      typeMap (Binop b f1 f2) (Var Q m v) = Some m ->
240 241 242 243 244 245
      exists vR : R,
        E v = Some (vR, M0) /\
        (Q2R (fst (fst (absenv (Var Q m v)))) <= vR <= Q2R (snd (fst (absenv (Var Q m v)))))%R)
  ->
  (forall (v : NatSet.elt) (m : mType),
      NatSet.mem v dVars = true ->
='s avatar
= committed
246
      typeMap f2 (Var Q m v) = Some m ->
247 248 249 250 251 252
      exists vR : R,
        E v = Some (vR, M0) /\
        (Q2R (fst (fst (absenv (Var Q m v)))) <= vR <= Q2R (snd (fst (absenv (Var Q m v)))))%R).
Proof.
  intros.
  specialize (H0 v m H1).
='s avatar
= committed
253
  case_eq (typeMap f1 (Var Q m v)); intros; auto.
254 255
  - case_eq (mTypeEqBool m1 m); intros.
    + (*apply EquivEqBoolEq in H4. ; rewrite <- H4 in H3.*)
='s avatar
= committed
256 257
      assert (typeMap (Binop b f1 f2) (Var Q m v) = Some m).
      simpl typeMap; rewrite H3. 
258 259
      apply EquivEqBoolEq in H4; rewrite H4; auto.
      specialize (H0 H5); auto.
='s avatar
= committed
260
    + pose proof (typeMapVarDet _ _ _ H3).
261 262 263
      rewrite H5 in H4.
      rewrite mTypeEqBool_refl in H4.
      inversion H4.
='s avatar
= committed
264
  - assert (typeMap (Binop b f1 f2) (Var Q m v) = Some m) by (simpl; rewrite H2,H3; auto).
265 266 267 268
    specialize (H0 H4).
    auto.
Qed.
    
269
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) fVars dVars (E:env):
270
  forall vR m,
='s avatar
= committed
271
    (typeMap f) f = Some m ->
272 273
    validIntervalbounds f absenv P dVars = true ->
    (forall v m, NatSet.mem v dVars = true ->
='s avatar
= committed
274
                 (typeMap f) (Var Q m v) = Some m ->
275
                 exists vR, E v = Some (vR, M0) /\
276
                (Q2R (fst (fst (absenv (Var Q m v)))) <= vR <= Q2R (snd (fst (absenv (Var Q m v)))))%R) ->
Raphaël Monat's avatar
Raphaël Monat committed
277
    NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
278
    (forall v, NatSet.mem v fVars = true ->
279
          exists vR, E v = Some (vR, M0) /\
280
                (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
281
    eval_exp E (toREval (toRExp f)) vR M0 ->
282
  (Q2R (fst (fst (absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R.
283
Proof.
284
  induction f; intros vR mf typing_ok valid_bounds valid_definedVars usedVars_subset valid_usedVars eval_f.
285
  - unfold validIntervalbounds in valid_bounds.
286
    env_assert absenv (Var Q m n) absenv_var.
287
    destruct absenv_var as [ iv [err absenv_var]].
Raphaël Monat's avatar
Raphaël Monat committed
288
    specialize (valid_usedVars n).
289
    simpl; rewrite absenv_var in *; simpl in *.
290
    inversion eval_f; subst.
291
    case_eq (NatSet.mem n dVars); intros case_mem; rewrite case_mem in *; simpl in *.
292 293
    + specialize (valid_definedVars n m case_mem).
      assert (mTypeEqBool m m && (n =? n) = true).
294
      apply andb_true_iff; split; [ apply EquivEqBoolEq | rewrite <- beq_nat_refl ]; auto.
295 296 297
      (* rewrite H in valid_definedVars. *)
      (* assert (Some m = Some m) by auto. *)
      (* specialize (valid_definedVars H0). *)
298
      destruct valid_definedVars as [vR' [E_n_eq precond_sound]].
299
      rewrite H; auto.
300
      rewrite E_n_eq in *.
301
      inversion H2; subst.
302
      rewrite absenv_var in *; auto.
303 304 305
    + repeat (rewrite delta_0_deterministic in *; try auto).
      unfold isSupersetIntv in valid_bounds.
      andb_to_prop valid_bounds.
306 307 308 309
      apply Qle_bool_iff in L0;
        apply Qle_bool_iff in R0.
      apply Qle_Rle in L0;
        apply Qle_Rle in R0.
310
      simpl in *.
311 312 313 314
      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.
Raphaël Monat's avatar
Raphaël Monat committed
315 316
        hnf in usedVars_subset.
        apply usedVars_subset.
317
        rewrite NatSet.diff_spec, NatSet.singleton_spec.
318
        split; try auto.
319 320 321
        hnf; intros in_dVars.
        rewrite <- NatSet.mem_spec in in_dVars.
        rewrite in_dVars in case_mem; congruence.
Raphaël Monat's avatar
Raphaël Monat committed
322 323
      * specialize (valid_usedVars in_fVars);
          destruct valid_usedVars as [vR' [vR_def P_valid]].
324
        rewrite vR_def in H2; inversion H2; subst.
325
        lra.
326
  - unfold validIntervalbounds in valid_bounds.
327
    simpl in *;  destruct (absenv (Const m v)) as [intv err]; simpl in *.
328 329
    apply Is_true_eq_left in valid_bounds.
    apply andb_prop_elim in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
330
    destruct valid_bounds as [valid_lo valid_hi].
Heiko Becker's avatar
Heiko Becker committed
331
    inversion eval_f; subst.
332
    rewrite delta_0_deterministic; auto.
333 334
    unfold contained; simpl.
    split.
Heiko Becker's avatar
Heiko Becker committed
335
    + apply Is_true_eq_true in valid_lo.
336
      unfold Qleb in *.
Heiko Becker's avatar
Heiko Becker committed
337 338 339 340 341 342
      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.
343 344
    + simpl in H2; rewrite Q2R0_is_0 in H2; auto.
  - case_eq (absenv (Unop u f)); intros intv err absenv_unop.
Heiko Becker's avatar
Heiko Becker committed
345 346
    destruct intv as [unop_lo unop_hi]; simpl.
    unfold validIntervalbounds in valid_bounds.
347
    simpl in valid_bounds; rewrite absenv_unop in valid_bounds.
348
    case_eq (absenv f); intros intv_f err_f absenv_f.
Heiko Becker's avatar
Heiko Becker committed
349 350 351 352 353 354
    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.
='s avatar
= committed
355
    + assert (typeMap f f = Some mf) as typing_f_ok by (simpl in typing_ok; rewrite expEqBool_refl in typing_ok; apply typeGivesTypeMap; auto).
356
      specialize (IHf v1 mf typing_f_ok valid_rec valid_definedVars usedVars_subset valid_usedVars H3).
Heiko Becker's avatar
Heiko Becker committed
357
      rewrite absenv_f in IHf; simpl in IHf.
358 359 360 361 362 363
      (* 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.
364
      pose proof (interval_negation_valid (iv :=(Q2R (fst intv_f),(Q2R (snd intv_f)))) (a :=v1)) as negation_valid.
365 366 367
      unfold contained, negateInterval in negation_valid; simpl in *.
      apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
      destruct IHf.
368
      split.
369
      * eapply Rle_trans. apply valid_lo.
370 371
        rewrite Q2R_opp; lra.
      * eapply Rle_trans.
372
        Focus 2. apply valid_hi.
373
        rewrite Q2R_opp; lra.
='s avatar
= committed
374
    + assert (typeMap f f = Some mf) as typing_f_ok by (simpl in typing_ok; rewrite expEqBool_refl in typing_ok; apply typeGivesTypeMap; auto).
375
      specialize (IHf v1 mf typing_f_ok valid_rec valid_definedVars usedVars_subset valid_usedVars H4).
Heiko Becker's avatar
Heiko Becker committed
376
      rewrite absenv_f in IHf; simpl in IHf.
377
      apply andb_prop_elim in valid_unop.
378
      destruct valid_unop as [nodiv0 valid_unop].
379 380 381 382 383 384 385 386 387 388 389 390
      (* 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. }
391
       * pose proof (interval_inversion_valid (iv :=(Q2R (fst intv_f),(Q2R (snd intv_f)))) (a :=v1)) as inv_valid.
392 393 394
         unfold contained, invertInterval in inv_valid; simpl in *.
         apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
         destruct IHf.
395
         rewrite delta_0_deterministic; auto.
396
         unfold perturb; split.
397
         { eapply Rle_trans. apply valid_lo.
398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418
           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.
             apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H2; lra.
         }
         { eapply Rle_trans.
419
           Focus 2. apply valid_hi.
420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442
           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.
             apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H2; lra.
         }
443
         { rewrite Q2R0_is_0 in H1; auto. }
444
  - inversion eval_f; subst.
445 446
    rewrite delta_0_deterministic in eval_f; auto.
    rewrite delta_0_deterministic; auto.
Heiko Becker's avatar
Heiko Becker committed
447
    simpl in valid_bounds.
448 449 450
    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.
451
    simpl.
Heiko Becker's avatar
Heiko Becker committed
452
    rewrite absenv_bin, absenv_f1, absenv_f2 in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
453 454 455 456 457 458
    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.
='s avatar
= committed
459 460 461 462
    destruct m1; destruct m2; cbv in H2; inversion H2.
    pose proof (typeMap_gives_type _ typing_ok).
    simpl in H. case_eq (typeExpression f1); intros; rewrite H0 in H; [ | inversion H ].
    case_eq (typeExpression f2); intros; rewrite H1 in H; inversion H.
463 464
    pose proof (validVarsUnfolding_l _ _ _ _ _ _ typing_ok valid_definedVars) as valid_definedVars_f1.
    pose proof (validVarsUnfolding_r _ _ _ _ _ _ typing_ok valid_definedVars) as valid_definedVars_f2.
='s avatar
= committed
465 466 467 468 469
    (* pose proof (binop_type_unfolding _ _ _ typing_ok) as subtypes. *)
    (* destruct subtypes as [mf1 [mf2 [typing_f1 [typing_f2 join_f1_f2]]]]. *)
    apply typeGivesTypeMap in H0. apply typeGivesTypeMap in H1.
    specialize (IHf1 v1 m H0 valid_e1 valid_definedVars_f1).
      specialize (IHf2 v2 m0 H1 valid_e2 valid_definedVars_f2).
Heiko Becker's avatar
Heiko Becker committed
470 471
    rewrite absenv_f1 in IHf1.
    rewrite absenv_f2 in IHf2.
472 473 474
    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.
Raphaël Monat's avatar
Raphaël Monat committed
475
      apply usedVars_subset.
476 477
      simpl. rewrite NatSet.diff_spec,NatSet.union_spec.
      rewrite NatSet.diff_spec in in_diff_e1.
Raphaël Monat's avatar
Raphaël Monat committed
478
      destruct in_diff_e1 as [ in_usedVars not_dVar].
479
      split; try auto.
480 481 482
    + 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.
Raphaël Monat's avatar
Raphaël Monat committed
483
        apply usedVars_subset.
484 485 486
        simpl. rewrite NatSet.diff_spec, NatSet.union_spec.
        rewrite NatSet.diff_spec in in_diff_e2.
        destruct in_diff_e2; split; auto.
487 488 489 490 491 492 493 494 495 496 497 498
      * 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.
499
          - eapply Rle_trans. (*rewrite absenv_bin;*) apply valid_lo.
500 501 502 503 504 505 506
            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.
507
            (*rewrite absenv_bin;*) apply valid_hi.
508 509 510 511 512 513 514 515 516 517 518 519 520 521 522
            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.
523
          - eapply Rle_trans. (*rewrite absenv_bin;*) apply valid_lo.
524 525 526 527 528 529 530 531
            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.
532
            (*rewrite absenv_bin;*) apply valid_hi.
533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548
            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.
549
          - eapply Rle_trans. (*rewrite absenv_bin;*) apply valid_lo.
550 551 552 553 554 555 556
            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.
557
            (*rewrite absenv_bin;*) apply valid_hi.
558 559 560 561 562 563
            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.
564
          rewrite <- andb_lazy_alt in valid_bin.
565 566
          unfold contained in valid_div.
          unfold isSupersetIntv in valid_bin.
567 568
          apply andb_prop_elim in valid_bin; destruct valid_bin as [nodiv0 valid_bin].
          (** CONTINUE **)
569 570 571 572 573 574 575 576 577 578 579 580 581 582 583
          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.
='s avatar
= committed
584
              destruct H3; [left | right]; apply Qlt_Rlt; auto.
585 586 587 588 589 590
            + 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.
='s avatar
= committed
591 592
                apply Rle_Qle in H8.
                rewrite ivhi2_0 in H8.
593 594 595 596
                lra.
              * assert (~ fst iv2 == 0).
                { destruct H; try lra.
                  hnf; intros ivlo2_0.
='s avatar
= committed
597 598
                  apply Rle_Qle in H8.
                  rewrite ivlo2_0 in H8.
599 600
                  lra. }
                { split.
601
                  - eapply Rle_trans. (*rewrite absenv_bin;*) apply valid_lo.
602 603 604 605 606 607 608 609
                    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.
610
                    (*rewrite absenv_bin;*) apply valid_hi.
611 612 613 614 615
                    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. } }
616 617 618 619
    + destruct m1; destruct m2; inversion H2.
      simpl in H4; rewrite Q2R0_is_0 in H4; auto.
    + destruct m1; destruct m2; inversion H2.
      simpl in H4; rewrite Q2R0_is_0 in H4; auto.
620
  - unfold validIntervalbounds in valid_bounds.
='s avatar
= committed
621
    pose proof (typeMap_gives_type _ typing_ok) as t_downcast.
622 623
    (*simpl erasure in valid_bounds.*)
    simpl in *; destruct (absenv (Downcast m f)); destruct (absenv f); simpl in *.
624 625 626 627
    apply Is_true_eq_left in valid_bounds.
    apply andb_prop_elim in valid_bounds.
    destruct valid_bounds as [vI1 vI2].
    apply andb_prop_elim in vI2.
628
    destruct vI2 as [vI2 vI2'].
629 630 631 632 633 634 635
    apply Is_true_eq_true in vI2.
    apply Is_true_eq_true in vI2'.
    assert (isEqIntv i i0) as Eq by (apply supIntvAntisym; auto).
    destruct Eq as [Eqlo Eqhi].
    simpl in *.
    apply Qeq_eqR in Eqlo; rewrite Eqlo.
    apply Qeq_eqR in Eqhi; rewrite Eqhi.
='s avatar
= committed
636
    pose proof (expEqBool_refl (Downcast m f)); simpl in H; rewrite H in typing_ok; inversion typing_ok; subst.
='s avatar
= committed
637 638 639 640 641
    case_eq (typeExpression f); intros. 
    + apply (IHf vR m); auto.
      * apply typeGivesTypeMap; auto.
      * apply Is_true_eq_true in vI1; auto.
    + rewrite H0 in t_downcast; inversion t_downcast.       
642
Qed.
643

644

645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741
(* Unused, proof not up-to-date *)
(* Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult): *)
(*   forall E vR fVars dVars outVars elo ehi err P, *)
(*     ssaPrg f (NatSet.union fVars dVars) outVars -> *)
(*     bstep (toREvalCmd (toRCmd f)) E vR M0  -> *)
(*     (forall v m, NatSet.mem v dVars = true -> *)
(*           exists vR, *)
(*             E v = Some (vR, m) /\ *)
(*             (Q2R (fst (fst (absenv (Var Q m v)))) <= vR <= Q2R (snd (fst (absenv (Var Q m v)))))%R) -> *)
(*     (forall v m, NatSet.mem v fVars = true -> *)
(*           exists vR, *)
(*             E v = Some (vR, m) /\ *)
(*             (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> *)
(*     NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars -> *)
(*     validIntervalboundsCmd f  absenv P dVars = true -> *)
(*     absenv (getRetExp f) = ((elo, ehi), err) -> *)
(*     (Q2R elo <=  vR <= Q2R ehi)%R. *)
(* Proof. *)
(*   induction f; *)
(*     intros *  ssa_f eval_f dVars_sound fVars_valid usedVars_subset valid_bounds_f absenv_f. *)
(*   - inversion ssa_f; subst. *)
(*     inversion eval_f; subst. *)
(*     unfold validIntervalboundsCmd in valid_bounds_f. *)
(*     andb_to_prop valid_bounds_f. *)
(*     inversion ssa_f; subst. *)
(*     specialize (IHf (updEnv n m v E) vR fVars (NatSet.add n dVars)). *)
(*     eapply IHf; eauto. *)
(*     + 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. *)
(*     + admit. *)
(*     + *)
(*       intros v0 m0 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 usedVars_subset. *)
(*         hnf. intros a in_usedVars. *)
(*         apply usedVars_subset. *)
(*         rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. *)
(*         rewrite NatSet.diff_spec in in_usedVars. *)
(*         destruct in_usedVars as [ in_usedVars not_dVar]. *)
(*         repeat split; try auto. *)
(*         { hnf; intros; subst. *)
(*           specialize (H5 n in_usedVars). *)
(*           rewrite <- NatSet.mem_spec in H5. *)
(*           rewrite H5 in H6; 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 usedVars_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. *)
(*   - unfold validIntervalboundsCmd in valid_bounds_f. *)
(*     inversion eval_f; subst. *)
(*     unfold updEnv. *)
(*     assert (Q2R (fst (fst (absenv (erasure e)))) <= vR <= Q2R (snd (fst (absenv (erasure e)))))%R. *)
(*     + simpl in valid_bounds_f; eapply validIntervalbounds_sound; eauto. *)
(*     + simpl in *. rewrite absenv_f in *; auto. *)
(* Qed. *)