IntervalValidation.v 19.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 10 11
Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps Flover.Infra.RealRationalProps.
Require Import Flover.Infra.Ltacs Flover.Infra.RealSimps Flover.Typing.
Require Export Flover.IntervalArithQ Flover.IntervalArith Flover.ssaPrgs.
12

Heiko Becker's avatar
Heiko Becker committed
13
Fixpoint validIntervalbounds (e:exp Q) (A:analysisResult) (P:precond) (validVars:NatSet.t) :bool:=
14
  match FloverMap.find e A with
Heiko Becker's avatar
Heiko Becker committed
15 16 17 18 19 20 21 22 23 24 25
  | None => false
  | Some (intv, _) =>
       match e with
       | Var _ v =>
         if NatSet.mem v validVars
         then true
         else isSupersetIntv (P v) intv && (Qleb (ivlo (P v)) (ivhi (P v)))
       | Const _ n => isSupersetIntv (n,n) intv
       | Unop o f =>
         if validIntervalbounds f A P validVars
         then
26
           match FloverMap.find f A with
Heiko Becker's avatar
Heiko Becker committed
27 28 29 30 31
           | 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
47
        match FloverMap.find f1 A, FloverMap.find f2 A with
Heiko Becker's avatar
Heiko Becker committed
48
        | 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
        match FloverMap.find f1 A, FloverMap.find f2 A, FloverMap.find f3 A with
76 77 78 79 80
        | Some (iv1, _), Some (iv2, _), Some (iv3, _) =>
          let new_iv := addIntv iv1 (multIntv iv2 iv3) in
          isSupersetIntv new_iv intv
        | _, _, _ => false
        end
81
      else false
82
    | Downcast _ f1 =>
Heiko Becker's avatar
Heiko Becker committed
83
      if (validIntervalbounds f1 A P validVars)
84
      then
85
        match FloverMap.find f1 A with
Heiko Becker's avatar
Heiko Becker committed
86 87
        | 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 =>
99
    match FloverMap.find e A, FloverMap.find (Var Q x) A with
Heiko Becker's avatar
Heiko Becker committed
100 101 102 103 104 105 106 107
    | Some ((e_lo,e_hi), _), Some ((x_lo, x_hi), _) =>
      if (validIntervalbounds e A P validVars &&
                              Qeq_bool (e_lo) (x_lo) &&
                              Qeq_bool (e_hi) (x_hi))
      then validIntervalboundsCmd g A P (NatSet.add x validVars)
      else false
    | _, _ => false
    end
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 117 118 119 120 121 122 123
Corollary Q2R_max4 a b c d:
  Q2R (IntervalArithQ.max4 a b c d) = max4 (Q2R a) (Q2R b) (Q2R c) (Q2R d).
Proof.
  unfold IntervalArithQ.max4, max4; repeat rewrite Q2R_max; auto.
Qed.

Corollary Q2R_min4 a b c d:
  Q2R (IntervalArithQ.min4 a b c d) = min4 (Q2R a) (Q2R b) (Q2R c) (Q2R d).
Proof.
  unfold IntervalArith.min4, min4; repeat rewrite Q2R_min; auto.
Qed.

Heiko Becker's avatar
Heiko Becker committed
124
Lemma validBoundsDiv_uneq_zero e1 e2 A P V ivlo_e2 ivhi_e2 err:
125
  FloverMap.find (elt:=intv * error) e2 A = Some ((ivlo_e2,ivhi_e2), err) ->
Heiko Becker's avatar
Heiko Becker committed
126
  validIntervalbounds (Binop Div e1 e2) A P V = true ->
127 128
  (ivhi_e2 < 0) \/ (0 < ivlo_e2).
Proof.
129
  intros A_eq validBounds; cbn in *.
130
  Flover_compute; try congruence.
131
  apply le_neq_bool_to_lt_prop; auto.
132
Qed.
133

134 135
Definition dVars_range_valid (dVars:NatSet.t) (E:env) (A:analysisResult) :Prop :=
  forall v, NatSet.In v dVars ->
136
       exists vR iv err,
137
         E v =  Some vR /\
138
         FloverMap.find (Var Q v) A = Some (iv, err) /\
139
         (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
140 141 142 143 144 145 146 147 148 149 150

Definition fVars_P_sound (fVars:NatSet.t) (E:env) (P:precond) :Prop :=
  forall v,
    NatSet.In v fVars ->
    exists vR, E v = Some vR /\
          (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R.

Definition vars_typed (S:NatSet.t) (Gamma: nat -> option mType) :=
  forall v, NatSet.In v S ->
       exists m :mType, Gamma v = Some m.

151 152
Ltac kill_trivial_exists :=
  match goal with
Heiko Becker's avatar
Heiko Becker committed
153 154
  | [ |- exists iv err v, Some (?i,?e) = Some (iv, err) /\ _ ] => exists i, e
  | [ |- exists iv err, Some (?i,?e) = Some (iv, err) /\ _ ] => exists i, e
155 156
  end.

Heiko Becker's avatar
Heiko Becker committed
157
Theorem validIntervalbounds_sound (f:exp Q) (A:analysisResult) (P:precond)
158
        fVars dVars (E:env) Gamma:
Heiko Becker's avatar
Heiko Becker committed
159
    validIntervalbounds f A P dVars = true ->
160
    dVars_range_valid dVars E A ->
Raphaël Monat's avatar
Raphaël Monat committed
161
    NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
162 163
    fVars_P_sound fVars E P ->
    vars_typed (NatSet.union fVars dVars) Gamma ->
164
    exists iv err vR,
165
      FloverMap.find f A = Some (iv, err) /\
166
      eval_exp E (toRMap Gamma) (toREval (toRExp f)) vR M0 /\
167
      (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
168
Proof.
169 170
  induction f;
    intros valid_bounds valid_definedVars usedVars_subset valid_freeVars types_defined;
171
    cbn in *.
172
  - Flover_compute.
173 174
    destruct (NatSet.mem n dVars) eqn:?; simpl in *.
    + destruct (valid_definedVars n)
175
        as [vR [iv_n [err_n [env_valid [map_n bounds_valid]]]]];
176 177 178
        try set_tac.
      rewrite map_n in *.
      inversion Heqo; subst.
179 180
      kill_trivial_exists.
      eexists; split; [auto| split; try eauto ].
181 182 183 184
      eapply Var_load; simpl; try auto.
      destruct (types_defined n) as [m type_m];
        set_tac.
      match_simpl; auto.
185 186
    + destruct (valid_freeVars n) as [vR [env_valid bounds_valid]];
        set_tac; try auto.
187
      assert (NatSet.In n fVars) by set_tac.
188 189
      andb_to_prop valid_bounds.
      canonize_hyps; simpl in *.
190 191
      kill_trivial_exists.
      eexists; split; [auto | split].
192
      * econstructor; try eauto.
193 194
        destruct (types_defined n) as [m type_m];
          set_tac.
195
        match_simpl; auto.
196
      * lra.
197
  - Flover_compute; canonize_hyps; simpl in *.
198 199 200
    kill_trivial_exists.
    exists (perturb (Q2R v) 0).
    split; [auto| split].
201 202
    + econstructor; try eauto. apply Rabs_0_equiv.
    + unfold perturb; simpl; lra.
203
  - Flover_compute; simpl in *; try congruence.
204
    destruct IHf as [iv_f [err_f [vF [iveq_f [eval_f valid_bounds_f]]]]];
205
      try auto.
206 207 208 209 210
    inversion iveq_f; subst.
    destruct u; try andb_to_prop R; simpl in *.
    + kill_trivial_exists.
      exists (evalUnop Neg vF); split;
        [auto | split ;
211
                            [econstructor; eauto | ]].
212 213
      canonize_hyps.
      rewrite Q2R_opp in *.
214 215
      simpl; lra.
    + rename L0 into nodiv0.
216
      apply le_neq_bool_to_lt_prop in nodiv0.
217 218
      kill_trivial_exists.
      exists (perturb (evalUnop Inv vF) 0); split;
219 220 221
        [destruct i; auto | split].
      * econstructor; eauto; try apply Rabs_0_equiv.
        (* Absence of division by zero *)
222 223 224
        hnf. destruct nodiv0 as [nodiv0 | nodiv0]; apply Qlt_Rlt in nodiv0;
               rewrite Q2R0_is_0 in nodiv0; lra.
      * canonize_hyps.
225
        pose proof (interval_inversion_valid ((Q2R (fst iv_f)),(Q2R (snd iv_f))) (a :=vF)) as inv_valid.
226 227 228 229 230
         unfold invertInterval in inv_valid; simpl in *.
         rewrite delta_0_deterministic; [| rewrite Rbasic_fun.Rabs_R0; lra].
         destruct inv_valid; try auto.
         { destruct nodiv0; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto. }
         { split; eapply Rle_trans.
231
           - apply L1.
232 233 234 235 236 237 238 239 240 241 242
           - rewrite Q2R_inv; try auto.
             destruct nodiv0; try lra.
             hnf; intros.
             assert (0 < Q2R (snd iv_f))%R.
             { eapply Rlt_le_trans.
               apply Qlt_Rlt in H1.
               rewrite <- Q2R0_is_0.
               apply H1. lra.
             }
             rewrite <- Q2R0_is_0 in H3.
             apply Rlt_Qlt in H3.
243
             lra.
244 245 246 247 248 249 250 251 252 253 254 255 256
           - apply H0.
           - rewrite <- Q2R_inv; try auto.
             hnf; intros.
             destruct nodiv0; try lra.
             assert (Q2R (fst iv_f) < 0)%R.
             { eapply Rle_lt_trans.
               Focus 2.
               rewrite <- Q2R0_is_0;
                 apply Qlt_Rlt in H2; apply H2.
               lra.
             }
             rewrite <- Q2R0_is_0 in H3.
             apply Rlt_Qlt in H3. lra. }
257
  - Flover_compute; try congruence.
258
    destruct IHf1 as [iv_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]];
259
      try auto; set_tac.
260
    destruct IHf2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]];
261
      try auto; set_tac.
262 263
    assert (M0 = join M0 M0) as M0_join by (cbv; auto);
      rewrite M0_join.
264
    kill_trivial_exists.
265
    exists (perturb (evalBinop b vF1 vF2) 0);
266 267
      split; [destruct i; auto | ].
    inversion env1; inversion env2; subst.
268 269 270
      destruct b; simpl in *.
    * split;
        [econstructor; try congruence; apply Rabs_0_equiv | ].
271 272 273
      pose proof (interval_addition_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
                                          (Q2R (fst iv_f2), Q2R (snd iv_f2)))
        as valid_add.
274 275 276
      specialize (valid_add vF1 vF2 valid_f1 valid_f2).
      unfold isSupersetIntv in R.
      andb_to_prop R.
277
      canonize_hyps; simpl in *.
278 279
      repeat rewrite <- Q2R_plus in *;
        rewrite <- Q2R_min4, <- Q2R_max4 in *.
280
      unfold perturb. lra.
281 282
    * split;
        [econstructor; try congruence; apply Rabs_0_equiv |].
283 284
      pose proof (interval_subtraction_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
                                             (Q2R (fst iv_f2), Q2R (snd iv_f2)))
285
        as valid_sub.
286 287 288
      specialize (valid_sub vF1 vF2 valid_f1 valid_f2).
      unfold isSupersetIntv in R.
      andb_to_prop R.
289
      canonize_hyps; simpl in *.
290 291 292
      repeat rewrite <- Q2R_opp in *;
        repeat rewrite <- Q2R_plus in *;
        rewrite <- Q2R_min4, <- Q2R_max4 in *.
293
      unfold perturb; lra.
294 295
    * split;
        [ econstructor; try congruence; apply Rabs_0_equiv |].
296 297
      pose proof (interval_multiplication_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
                                                (Q2R (fst iv_f2), Q2R (snd iv_f2)))
298
        as valid_mul.
299 300 301
      specialize (valid_mul vF1 vF2 valid_f1 valid_f2).
      unfold isSupersetIntv in R.
      andb_to_prop R.
302
      canonize_hyps; simpl in *.
303 304
      repeat rewrite <- Q2R_mult in *;
        rewrite <- Q2R_min4, <- Q2R_max4 in *.
305
      unfold perturb; lra.
306 307 308 309 310 311 312 313
    * andb_to_prop R.
      canonize_hyps.
      apply le_neq_bool_to_lt_prop in L.
      split;
        [ econstructor; try congruence; try apply Rabs_0_equiv | ].
      (* No division by zero proof *)
      { hnf; intros.
        destruct L as [L | L]; apply Qlt_Rlt in L; rewrite Q2R0_is_0 in L; lra. }
314
      { pose proof (interval_division_valid (a:=vF1) (b:=vF2)
315 316
                                            ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
                                            (Q2R (fst iv_f2), Q2R (snd iv_f2)))
317
        as valid_div.
318 319 320
        simpl in *.
        destruct valid_div; try auto.
        - destruct L; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto.
321
        - assert (~ (snd iv_f2) == 0).
322
          { hnf; intros. destruct L; try lra.
323
            assert (0 < (snd iv_f2)) by (apply Rlt_Qlt; apply Qlt_Rlt in H2; lra).
324
            lra. }
325
          assert (~ (fst iv_f2) == 0).
326
          { hnf; intros; destruct L; try lra.
327
            assert ((fst iv_f2) < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H3; lra).
328 329 330 331 332 333 334
            lra. }
          repeat (rewrite <- Q2R_inv in *; try auto).
          repeat rewrite <- Q2R_mult in *.
          rewrite <- Q2R_min4, <- Q2R_max4 in *.
          unfold perturb.
          lra.
      }
335
  - Flover_compute; try congruence.
336 337 338
    destruct IHf1 as [iv_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]]; try auto; set_tac.
    destruct IHf2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]]; try auto; set_tac.
    destruct IHf3 as [iv_f3 [err3 [vF3 [env3 [eval_f3 valid_f3]]]]]; try auto; set_tac.
339 340
    assert (M0 = join3 M0 M0 M0) as M0_join by (cbv; auto);
      rewrite M0_join.
341 342 343 344 345
    kill_trivial_exists.
    exists (perturb (evalFma vF1 vF2 vF3) 0); split; try auto.
    inversion env1; inversion env2; inversion env3; subst.
    split; [auto | ].
    * econstructor; try congruence; apply Rabs_0_equiv.
346 347
    * pose proof (interval_multiplication_valid (Q2R (fst iv_f2),Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as valid_mul.
      specialize (valid_mul vF2 vF3 valid_f2 valid_f3).
348
      remember (multInterval (Q2R (fst iv_f2), Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as iv_f23prod.
349
      pose proof (interval_addition_valid (Q2R (fst iv_f1),Q2R (snd iv_f1)) (fst iv_f23prod, snd iv_f23prod)) as valid_add.
350
      rewrite Heqiv_f23prod in valid_add, valid_mul.
351 352 353 354 355 356 357 358
      unfold multIntv in valid_add.
      canonize_hyps.
      simpl in *.
      repeat rewrite <- Q2R_mult in *;
        repeat rewrite <- Q2R_min4, <- Q2R_max4 in *;
        repeat rewrite <- Q2R_plus in *;
        repeat rewrite <- Q2R_min4, <- Q2R_max4 in *.
      specialize (valid_add vF1 (vF2 * vF3)%R valid_f1 valid_mul).
359
      unfold evalFma, evalBinop, perturb.
360
      lra.
361
  - match_simpl.
362
    andb_to_prop valid_bounds.
363
    match_simpl.
364
    destruct IHf as [iv_f [err_f [vF [env_f [eval_f valid_f]]]]];
365 366
      try auto.
    inversion env_f; subst.
367
    kill_trivial_exists.
368
    exists (perturb vF 0).
369
    split; [destruct i; try auto |].
370
    split; [try econstructor; try eauto; try apply Rabs_0_equiv; unfold isMorePrecise; auto |].
371 372 373
    unfold isSupersetIntv in *; andb_to_prop R.
    canonize_hyps; simpl in *.
    unfold perturb; lra.
374 375
Qed.

376
Lemma Rmap_updVars_comm Gamma n m:
377 378 379 380 381 382 383
  forall x,
    updDefVars n M0 (toRMap Gamma) x = toRMap (updDefVars n m Gamma) x.
Proof.
  unfold updDefVars, toRMap; simpl.
  intros x; destruct (x =? n); try auto.
Qed.

384
Lemma swap_Gamma_eval_exp e E vR m Gamma1 Gamma2:
385 386 387 388 389 390 391 392 393 394 395 396
  (forall n, Gamma1 n = Gamma2 n) ->
  eval_exp E Gamma1 e vR m ->
  eval_exp E Gamma2 e vR m.
Proof.
  revert E vR Gamma1 Gamma2 m;
    induction e; intros * Gamma_eq eval_e;
      inversion eval_e; subst; simpl in *;
        try eauto.
  apply Var_load; try auto.
  rewrite <- Gamma_eq; auto.
Qed.

397
Lemma swap_Gamma_bstep f E vR m Gamma1 Gamma2 :
398 399 400 401 402 403
  (forall n, Gamma1 n = Gamma2 n) ->
  bstep f E Gamma1 vR m ->
  bstep f E Gamma2 vR m.
Proof.
  revert E Gamma1 Gamma2;
  induction f; intros * Gamma_eq eval_f.
404
  - inversion eval_f; subst.
405
    econstructor; try eauto.
406
    +  eapply swap_Gamma_eval_exp; eauto.
407 408 409 410 411 412
    + apply (IHf _ (updDefVars n m0 Gamma1) _); try eauto.
      intros n1.
      unfold updDefVars.
      case (n1 =? n); auto.
  - inversion eval_f; subst.
    econstructor; try eauto.
413
    eapply swap_Gamma_eval_exp; eauto.
414
Qed.
415

416 417
Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult):
  forall Gamma E fVars dVars outVars P,
='s avatar
= committed
418
    ssa f (NatSet.union fVars dVars) outVars ->
419 420 421
    dVars_range_valid dVars E A ->
    fVars_P_sound fVars E P ->
    vars_typed (NatSet.union fVars dVars) Gamma ->
='s avatar
= committed
422
    NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
Heiko Becker's avatar
Heiko Becker committed
423
    validIntervalboundsCmd f A P dVars = true ->
424
    exists iv_e err_e vR,
425
      FloverMap.find (getRetExp f) A = Some (iv_e, err_e) /\
426
      bstep (toREvalCmd (toRCmd f)) E (toRMap Gamma) vR M0 /\
427
      (Q2R (fst iv_e) <=  vR <= Q2R (snd iv_e))%R.
='s avatar
= committed
428 429
Proof.
  induction f;
430 431
    intros *  ssa_f dVars_sound fVars_valid types_valid usedVars_subset valid_bounds_f;
    cbn in *.
432
  - Flover_compute.
='s avatar
= committed
433
    inversion ssa_f; subst.
434 435
    canonize_hyps.
    pose proof (validIntervalbounds_sound e (Gamma:=Gamma) (E:=E) (fVars:=fVars) L) as validIV_e.
436
    destruct validIV_e as [iv_e [err_v [v [find_v [eval_e valid_bounds_e]]]]];
437 438
      try auto.
    { set_tac. repeat split; auto.
439 440
      hnf; intros; subst.
      set_tac. }
441
    rewrite find_v in *; inversion Heqo; subst.
442 443
    specialize (IHf (updDefVars n M0 Gamma) (updEnv n v E) fVars (NatSet.add n dVars)).
    assert (NatSet.Equal (NatSet.add n (NatSet.union fVars dVars)) (NatSet.union fVars (NatSet.add n dVars))).
444 445 446 447 448
    + hnf. intros a; split; intros in_set; set_tac.
      * destruct in_set as [ ? | [? ?]]; try auto; set_tac.
        destruct H0; auto.
      * destruct in_set as [? | ?]; try auto; set_tac.
        destruct H as [? | [? ?]]; auto.
449
    + edestruct IHf as [iv_f [err_f [vR [env_f [eval_f valid_bounds_f]]]]];
450
        try eauto.
451
       eapply ssa_equal_set. symmetry in H. apply H. apply H7.
452 453 454 455 456 457
      * intros v0 mem_v0.
        unfold updEnv.
        case_eq (v0 =? n); intros v0_eq.
        { rename R1 into eq_lo;
            rename R0 into eq_hi.
          rewrite Nat.eqb_eq in v0_eq; subst.
458
          exists v; eexists; eexists; repeat split; try eauto; simpl in *; lra. }
459 460 461
        { apply dVars_sound.
          set_tac.
          destruct mem_v0 as [? | [? ?]]; try auto.
462
          rewrite Nat.eqb_neq in v0_eq.
463
          congruence. }
464 465 466 467
      * intros v0 mem_fVars.
        unfold updEnv.
        case_eq (v0 =? n); intros case_v0; auto.
        rewrite Nat.eqb_eq in case_v0; subst.
468 469
        assert (NatSet.In n (NatSet.union fVars dVars)) as in_union by set_tac.
        exfalso; set_tac. apply H6; set_tac; auto.
470 471 472
      * intros x x_contained.
        set_tac.
        destruct x_contained as [x_free | x_def].
473
        { destruct (types_valid x) as [m_x Gamma_x]; try set_tac.
474 475 476 477 478
          exists m_x.
          unfold updDefVars. case_eq (x =? n); intros eq_case; try auto.
          rewrite Nat.eqb_eq in eq_case.
          subst.
          exfalso; apply H6; set_tac. }
479
        { set_tac.
480 481
          destruct x_def as [x_n | x_def]; subst.
          - exists M0; unfold updDefVars; rewrite Nat.eqb_refl; auto.
482 483 484 485 486 487
          - destruct x_def. destruct (types_valid x) as [m_x Gamma_x].
            + rewrite NatSet.union_spec; auto.
            + exists m_x.
              unfold updDefVars; case_eq (x =? n); intros eq_case; try auto.
              rewrite Nat.eqb_eq in eq_case; subst.
              congruence. }
488 489 490 491
      * clear L R1 R0 R IHf.
        hnf. intros a a_freeVar.
        rewrite NatSet.diff_spec in a_freeVar.
        destruct a_freeVar as [a_freeVar a_no_dVar].
='s avatar
= committed
492
        apply usedVars_subset.
493
        simpl.
='s avatar
= committed
494 495 496
        rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
        repeat split; try auto.
        { hnf; intros; subst.
497 498 499 500 501
          apply a_no_dVar.
          rewrite NatSet.add_spec; auto. }
        { hnf; intros a_dVar.
          apply a_no_dVar.
          rewrite NatSet.add_spec; auto. }
502
      * simpl. exists iv_f, err_f, vR; repeat split; try auto; try lra.
503
        econstructor; try eauto.
504
        eapply swap_Gamma_bstep with (Gamma1 := toRMap (updDefVars n M0 Gamma)) ; try eauto.
505
        intros n1; erewrite Rmap_updVars_comm; eauto.
='s avatar
= committed
506
  - unfold validIntervalboundsCmd in valid_bounds_f.
507
    pose proof (validIntervalbounds_sound e (E:=E) (Gamma:=Gamma) valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e.
508
    destruct valid_iv_e as [?[?[? [? [? ?]]]]]; try auto.
509
    simpl in *. repeat eexists; repeat split; try eauto; [econstructor; eauto| | ]; lra.
510
Qed.