IntervalValidation.v 20.7 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

Heiko Becker's avatar
Heiko Becker committed
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
32
            isSupersetIntv new_iv intv
Heiko Becker's avatar
Heiko Becker committed
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's avatar
Heiko Becker committed
41
        end
42
      else false
Heiko Becker's avatar
Heiko Becker committed
43
    | Binop op f1 f2 =>
Heiko Becker's avatar
Heiko Becker committed
44 45
      if ((validIntervalbounds f1 A P validVars) &&
          (validIntervalbounds f2 A P validVars))
46
      then
Heiko Becker's avatar
Heiko Becker committed
47 48
        match DaisyMap.find f1 A, DaisyMap.find f2 A with
        | Some (iv1, _), Some (iv2, _) =>
Heiko Becker's avatar
Heiko Becker committed
49
          match op with
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's avatar
Heiko Becker committed
59
          | Div =>
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
66
          end
Heiko Becker's avatar
Heiko Becker committed
67 68
        | _, _ => false
        end
69
      else false
70
    | Fma f1 f2 f3 =>
71 72 73
      if ((validIntervalbounds f1 A P validVars) &&
          (validIntervalbounds f2 A P validVars) &&
          (validIntervalbounds f3 A P validVars))
74
      then
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
81
      else false
82
    | Downcast _ f1 =>
Heiko Becker's avatar
Heiko Becker committed
83
      if (validIntervalbounds f1 A P validVars)
84
      then
Heiko Becker's avatar
Heiko Becker committed
85 86 87
        match DaisyMap.find f1 A with
        | None => false
        | Some (iv1, _) =>
88 89
        (* TODO: intv = iv1 might be a hard constraint... *)
        (isSupersetIntv intv iv1) && (isSupersetIntv iv1 intv)
Heiko Becker's avatar
Heiko Becker committed
90
        end
91 92
      else
        false
Heiko Becker's avatar
Heiko Becker committed
93 94
       end
  end.
95

Heiko Becker's avatar
Heiko Becker committed
96
Fixpoint validIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P:precond) (validVars:NatSet.t) :bool:=
97
  match f with
98
  | Let m x e g =>
Heiko Becker's avatar
Heiko Becker committed
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
108
  |Ret e =>
Heiko Becker's avatar
Heiko Becker committed
109
   validIntervalbounds e A P validVars
110 111
  end.

Heiko Becker's avatar
Heiko Becker committed
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).
117
Proof.
Heiko Becker's avatar
Heiko Becker committed
118 119
  induction f; cbn; intros approx_true var var_in_fV find_A; set_tac.
  - subst.
120
    Daisy_compute.
Heiko Becker's avatar
Heiko Becker committed
121
    destruct (var mem dVars) eqn:?; set_tac; try congruence.
122 123
    Daisy_compute.
    unfold isSupersetIntv.
Heiko Becker's avatar
Heiko Becker committed
124 125
    apply andb_prop_intro; split;
        apply Is_true_eq_left; auto.
126
  - Daisy_compute; try congruence.
Heiko Becker's avatar
Heiko Becker committed
127
    apply IHf; try auto.
Heiko Becker's avatar
Heiko Becker committed
128
    set_tac.
129
  - Daisy_compute; try congruence.
130
    destruct H.
Heiko Becker's avatar
Heiko Becker committed
131 132
    + apply IHf1; try auto; set_tac.
    + apply IHf2; try auto; set_tac.
133
  - Daisy_compute; try congruence.
134
    destruct H.
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's avatar
Heiko Becker committed
141
    apply IHf; try auto; set_tac.
142 143
Qed.

Heiko Becker's avatar
Heiko Becker committed
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's avatar
Heiko Becker committed
156
Lemma validBoundsDiv_uneq_zero e1 e2 A P V ivlo_e2 ivhi_e2 err:
157
  DaisyMap.find (elt:=intv * error) e2 A = Some ((ivlo_e2,ivhi_e2), err) ->
Heiko Becker's avatar
Heiko Becker committed
158
  validIntervalbounds (Binop Div e1 e2) A P V = true ->
159 160
  (ivhi_e2 < 0) \/ (0 < ivlo_e2).
Proof.
161
  intros A_eq validBounds; cbn in *.
162
  Daisy_compute; try congruence.
163
  apply le_neq_bool_to_lt_prop; auto.
164
Qed.
165

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,
169
         E v =  Some vR /\
170 171
         DaisyMap.find (Var Q v) A = Some (iv, err) /\
         (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
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's avatar
Heiko Becker committed
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's avatar
Heiko Becker committed
189
Theorem validIntervalbounds_sound (f:exp Q) (A:analysisResult) (P:precond)
190
        fVars dVars (E:env) Gamma:
Heiko Becker's avatar
Heiko Becker committed
191
    validIntervalbounds f A P dVars = true ->
192
    dVars_range_valid dVars E A ->
Raphaël Monat's avatar
Raphaël Monat committed
193
    NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
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) /\
198
      eval_exp E (toRMap Gamma) (toREval (toRExp f)) vR M0 /\
199
      (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
200
Proof.
201 202
  induction f;
    intros valid_bounds valid_definedVars usedVars_subset valid_freeVars types_defined;
203
    cbn in *.
204
  - Daisy_compute.
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]]]]];
208 209 210
        try set_tac.
      rewrite map_n in *.
      inversion Heqo; subst.
211 212
      kill_trivial_exists.
      eexists; split; [auto| split; try eauto ].
213 214 215 216
      eapply Var_load; simpl; try auto.
      destruct (types_defined n) as [m type_m];
        set_tac.
      match_simpl; auto.
217 218
    + destruct (valid_freeVars n) as [vR [env_valid bounds_valid]];
        set_tac; try auto.
219
      assert (NatSet.In n fVars) by set_tac.
220 221
      andb_to_prop valid_bounds.
      canonize_hyps; simpl in *.
222 223
      kill_trivial_exists.
      eexists; split; [auto | split].
224
      * econstructor; try eauto.
225 226
        destruct (types_defined n) as [m type_m];
          set_tac.
227
        match_simpl; auto.
228
      * lra.
229 230 231 232
  - Daisy_compute; canonize_hyps; simpl in *.
    kill_trivial_exists.
    exists (perturb (Q2R v) 0).
    split; [auto| split].
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]]]]];
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 ;
243
                            [econstructor; eauto | ]].
244 245
      canonize_hyps.
      rewrite Q2R_opp in *.
246 247
      simpl; lra.
    + rename L0 into nodiv0.
248
      apply le_neq_bool_to_lt_prop in nodiv0.
249 250
      kill_trivial_exists.
      exists (perturb (evalUnop Inv vF) 0); split;
251 252 253
        [destruct i; auto | split].
      * econstructor; eauto; try apply Rabs_0_equiv.
        (* Absence of division by zero *)
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.
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.
263
           - apply L1.
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.
275
             lra.
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]]]]];
291
      try auto; set_tac.
292
    destruct IHf2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]];
293
      try auto; set_tac.
294 295
    assert (M0 = join M0 M0) as M0_join by (cbv; auto);
      rewrite M0_join.
296
    kill_trivial_exists.
297
    exists (perturb (evalBinop b vF1 vF2) 0);
298 299
      split; [destruct i; auto | ].
    inversion env1; inversion env2; subst.
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.
306 307 308
      specialize (valid_add vF1 vF2 valid_f1 valid_f2).
      unfold isSupersetIntv in R.
      andb_to_prop R.
309
      canonize_hyps; simpl in *.
310 311
      repeat rewrite <- Q2R_plus in *;
        rewrite <- Q2R_min4, <- Q2R_max4 in *.
312
      unfold perturb. lra.
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)))
317
        as valid_sub.
318 319 320
      specialize (valid_sub vF1 vF2 valid_f1 valid_f2).
      unfold isSupersetIntv in R.
      andb_to_prop R.
321
      canonize_hyps; simpl in *.
322 323 324
      repeat rewrite <- Q2R_opp in *;
        repeat rewrite <- Q2R_plus in *;
        rewrite <- Q2R_min4, <- Q2R_max4 in *.
325
      unfold perturb; lra.
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)))
330
        as valid_mul.
331 332 333
      specialize (valid_mul vF1 vF2 valid_f1 valid_f2).
      unfold isSupersetIntv in R.
      andb_to_prop R.
334
      canonize_hyps; simpl in *.
335 336
      repeat rewrite <- Q2R_mult in *;
        rewrite <- Q2R_min4, <- Q2R_max4 in *.
337
      unfold perturb; lra.
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. }
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)))
349
        as valid_div.
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).
354
          { hnf; intros. destruct L; try lra.
355
            assert (0 < (snd iv_f2)) by (apply Rlt_Qlt; apply Qlt_Rlt in H2; lra).
356
            lra. }
357
          assert (~ (fst iv_f2) == 0).
358
          { hnf; intros; destruct L; try lra.
359
            assert ((fst iv_f2) < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H3; lra).
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.
      }
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.
371 372
    assert (M0 = join3 M0 M0 M0) as M0_join by (cbv; auto);
      rewrite M0_join.
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.
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).
380
      remember (multInterval (Q2R (fst iv_f2), Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as iv_f23prod.
381
      pose proof (interval_addition_valid (Q2R (fst iv_f1),Q2R (snd iv_f1)) (fst iv_f23prod, snd iv_f23prod)) as valid_add.
382
      rewrite Heqiv_f23prod in valid_add, valid_mul.
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).
391
      unfold evalFma, evalBinop, perturb.
392
      lra.
393
  - match_simpl.
394
    andb_to_prop valid_bounds.
395
    match_simpl.
396
    destruct IHf as [iv_f [err_f [vF [env_f [eval_f valid_f]]]]];
397 398
      try auto.
    inversion env_f; subst.
399
    kill_trivial_exists.
400
    exists (perturb vF 0).
401
    split; [destruct i; try auto |].
402
    split; [try econstructor; try eauto; try apply Rabs_0_equiv; unfold isMorePrecise; auto |].
403 404 405
    unfold isSupersetIntv in *; andb_to_prop R.
    canonize_hyps; simpl in *.
    unfold perturb; lra.
406 407
Qed.

408
Lemma Rmap_updVars_comm Gamma n m:
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.

416
Lemma swap_Gamma_eval_exp e E vR m Gamma1 Gamma2:
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.

429
Lemma swap_Gamma_bstep f E vR m Gamma1 Gamma2 :
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.
436
  - inversion eval_f; subst.
437
    econstructor; try eauto.
438
    +  eapply swap_Gamma_eval_exp; eauto.
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.
445
    eapply swap_Gamma_eval_exp; eauto.
446
Qed.
447

Heiko Becker's avatar
Heiko Becker committed
448
Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult) Gamma:
449
  forall E fVars dVars outVars P,
='s avatar
= committed
450
    ssa f (NatSet.union fVars dVars) outVars ->
451 452 453
    dVars_range_valid dVars E A ->
    fVars_P_sound fVars E P ->
    vars_typed (NatSet.union fVars dVars) Gamma ->
='s avatar
= committed
454
    NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
Heiko Becker's avatar
Heiko Becker committed
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) /\
458
      bstep (toREvalCmd (toRCmd f)) E (toRMap Gamma) vR M0 /\
459
      (Q2R (fst iv_e) <=  vR <= Q2R (snd iv_e))%R.
='s avatar
= committed
460
Proof.
461
  revert Gamma.
='s avatar
= committed
462
  induction f;
463 464
    intros *  ssa_f dVars_sound fVars_valid types_valid usedVars_subset valid_bounds_f;
    cbn in *.
465
  - Daisy_compute.
='s avatar
= committed
466
    inversion ssa_f; subst.
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]]]]];
470 471
      try auto.
    { set_tac. repeat split; auto.
472 473
      hnf; intros; subst.
      set_tac. }
474
    rewrite find_v in *; inversion Heqo; subst.
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))).
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]]]]];
483
        try eauto.
484
       eapply ssa_equal_set. symmetry in H. apply H. apply H7.
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. }
492 493 494
        { apply dVars_sound.
          set_tac.
          destruct mem_v0 as [? | [? ?]]; try auto.
495
          rewrite Nat.eqb_neq in v0_eq.
496
          congruence. }
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.
501 502
        assert (NatSet.In n (NatSet.union fVars dVars)) as in_union by set_tac.
        exfalso; set_tac. apply H6; set_tac; auto.
503 504 505
      * intros x x_contained.
        set_tac.
        destruct x_contained as [x_free | x_def].
506
        { destruct (types_valid x) as [m_x Gamma_x]; try set_tac.
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. }
512
        { set_tac.
513 514
          destruct x_def as [x_n | x_def]; subst.
          - exists M0; unfold updDefVars; rewrite Nat.eqb_refl; auto.
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. }
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].
='s avatar
= committed
525
        apply usedVars_subset.
526
        simpl.
='s avatar
= committed
527 528 529
        rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
        repeat split; try auto.
        { hnf; intros; subst.
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.
536
        econstructor; try eauto.
537
        eapply swap_Gamma_bstep with (Gamma1 := toRMap (updDefVars n M0 Gamma)) ; try eauto.
538
        intros n1; erewrite Rmap_updVars_comm; eauto.
='s avatar
= committed
539
  - unfold validIntervalboundsCmd in valid_bounds_f.
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.
542
    simpl in *. repeat eexists; repeat split; try eauto; [econstructor; eauto| | ]; lra.
543
Qed.