SMTValidation.v 27.3 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
(**
    SMT arithmetic checker and its soundness proof.
    The function validSMTIntervalbounds 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 SMT arithmetic.
    The function is used in CertificateChecker.v to build the full checker.
**)
From Coq
     Require Import QArith.QArith QArith.Qreals QArith.Qminmax Lists.List
     micromega.Psatz.

From Flover
     Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
     Infra.Ltacs Infra.RealSimps TypeValidator.

From Flover
Joachim Bard's avatar
Joachim Bard committed
17
     Require Export IntervalArithQ IntervalArith SMTArith ssaPrgs
18
     RealRangeArith.
19

Joachim Bard's avatar
Joachim Bard committed
20 21 22 23 24 25 26 27 28
Definition let_env := nat -> option (expr Q).

Definition lets_sound L E Gamma :=
  forall x e v,
    L x = Some e ->
    eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp (Var _ x))) v REAL ->
    eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v REAL.

Definition updLets x (e: expr Q) (L: let_env) (y: nat) :=
29 30
  if y =? x then Some e else L y.

Joachim Bard's avatar
Joachim Bard committed
31
Fixpoint inlineLets (L: let_env) (e: expr Q) :=
32 33 34 35 36 37 38 39 40 41
  match e with
  | Var _ x => match L x with
            | Some e' => e'
            | None => e
            end
  | Const m r => e
  | Unop u e' => Unop u (inlineLets L e')
  | Binop b e1 e2 => Binop b (inlineLets L e1) (inlineLets L e2)
  | Fma e1 e2 e3 => Fma (inlineLets L e1) (inlineLets L e2) (inlineLets L e3)
  | Downcast m e' => Downcast m (inlineLets L e')
Joachim Bard's avatar
Joachim Bard committed
42
  | Let m x e1 e2 => Let m x (inlineLets L e1) (inlineLets L e2)
43
  (* | Cond e1 e2 e3 => Cond (inlineLets L e1) (inlineLets L e2) (inlineLets L e3) *)
44 45
  end.

Joachim Bard's avatar
Joachim Bard committed
46
Lemma inlineLets_sound L E Gamma inVars outVars e v :
Joachim Bard's avatar
Joachim Bard committed
47
  lets_sound L E Gamma ->
Joachim Bard's avatar
Joachim Bard committed
48 49
  (forall x e, L x = Some e -> NatSet.Subset (NatSet.add x (freeVars e)) inVars) ->
  ssa e inVars outVars ->
Joachim Bard's avatar
Joachim Bard committed
50 51
  eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v REAL ->
  eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp (inlineLets L e))) v
52 53
    REAL.
Proof.
54
  induction e in E, inVars, v |- *; cbn; intros Lsound LfVars_valid ssa_e H.
Joachim Bard's avatar
Joachim Bard committed
55 56 57
  - Flover_compute; eauto.
  - auto.
  - inversion H; subst; econstructor; eauto.
58
    + destruct m; try discriminate.
Joachim Bard's avatar
Joachim Bard committed
59
      inversion ssa_e; subst.
60 61
      eauto.
    + destruct m; try discriminate.
Joachim Bard's avatar
Joachim Bard committed
62
      inversion ssa_e; subst.
63
      eauto.
Joachim Bard's avatar
Joachim Bard committed
64
  - inversion H; subst; econstructor; eauto.
65
    + assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
Joachim Bard's avatar
Joachim Bard committed
66
      inversion ssa_e; subst.
67 68 69
      subst.
      eapply IHe1; try eauto.
      now extended_ssa.
70
    + assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
Joachim Bard's avatar
Joachim Bard committed
71
      inversion ssa_e; subst.
72 73
      eapply IHe2; try eauto.
      now extended_ssa.
Joachim Bard's avatar
Joachim Bard committed
74
  - inversion H; subst; econstructor; eauto.
75
    + assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
Joachim Bard's avatar
Joachim Bard committed
76
      inversion ssa_e; subst.
77 78
      eapply IHe1; try eauto.
      now extended_ssa.
79
    + assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
Joachim Bard's avatar
Joachim Bard committed
80
      inversion ssa_e; subst.
81 82
      eapply IHe2; try eauto.
      now extended_ssa.
83
    + assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
Joachim Bard's avatar
Joachim Bard committed
84
      inversion ssa_e; subst.
85 86
      eapply IHe3; try eauto.
      now extended_ssa.
Joachim Bard's avatar
Joachim Bard committed
87
  - inversion H; subst; econstructor; eauto.
Joachim Bard's avatar
Joachim Bard committed
88
    inversion ssa_e; subst.
89 90
    assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
    subst. eauto.
Joachim Bard's avatar
Joachim Bard committed
91 92
  - inversion H; subst.
    inversion ssa_e; subst.
93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115
    econstructor; try eauto.
    + eapply IHe1; try eauto.
      now extended_ssa.
    + destruct m2; try discriminate.
      eapply (IHe2 _ (NatSet.add n inVars)); eauto.
      2: intros; set_tac; right; eapply LfVars_valid; eauto;
        set_tac; tauto.
      intros x e v'.
      unfold updEnv.
      destruct (x =? n) eqn: Heq.
      * intros Hx He.
        apply beq_nat_true in Heq; subst.
        set_tac. exfalso. apply H5. eapply LfVars_valid; eauto.
        set_tac.
      * intros H0 H1.
        inversion H1; subst. rewrite Heq in *.
        apply eval_expr_ignore_bind.
        { eapply Lsound; eauto. now constructor. }
        { rewrite freeVars_toREval_toRExp_compat.
          set_tac. intros ?.
          apply H5. eapply LfVars_valid; eauto.
          set_tac. }
      * now extended_ssa.
116
            (*
Joachim Bard's avatar
Joachim Bard committed
117 118
  - inversion H; subst.
    + assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
Joachim Bard's avatar
Joachim Bard committed
119
      inversion ssa_e; subst.
Joachim Bard's avatar
Joachim Bard committed
120 121 122 123
      subst.
      assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
      subst. eapply Cond_then; eauto.
    + assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
Joachim Bard's avatar
Joachim Bard committed
124
      inversion ssa_e; subst.
Joachim Bard's avatar
Joachim Bard committed
125 126 127
      subst.
      assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
      subst. eapply Cond_else; eauto.
128
*)
129 130 131
Qed.

Definition tightenLowerBound (e: expr Q) (lo: Q) (q: SMTLogic) P L :=
132
  match q with
133 134
  | AndQ qP (AndQ (LessQ e' (ConstQ v)) TrueQ) =>
    if checkPre P qP && smt_expr_eq e' (inlineLets L e) then Qmax lo v else lo
135
  | _ => lo
136 137
  end.

138
Definition tightenUpperBound (e: expr Q) (hi: Q) (q: SMTLogic) P L :=
139
  match q with
140 141
  | AndQ qP (AndQ (LessQ (ConstQ v) e') TrueQ) =>
    if checkPre P qP && smt_expr_eq e' (inlineLets L e) then Qmin hi v else hi
142
  | _ => hi
143 144
  end.

145
Definition tightenBounds (e: expr Q) (iv: intv) (qMap: usedQueries) P L :=
146 147
  match FloverMap.find e qMap with
  | None => iv
148 149
  | Some (loQ, hiQ) =>
    (tightenLowerBound e (fst iv) loQ P L, tightenUpperBound e (snd iv) hiQ P L)
150 151
  end.

152 153 154 155 156 157 158
Lemma tightenBounds_low_sound E Gamma e v iv qMap P L :
  eval_precond E P ->
  (forall ql qh, FloverMap.find e qMap = Some (ql, qh) -> ~ eval_smt_logic E ql) ->
  eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR
            (toREval (toRExp (inlineLets L e))) v REAL ->
  (Q2R (fst iv) <= v)%R ->
  (Q2R (fst (tightenBounds e iv qMap P L)) <= v)%R.
159 160 161 162 163
Proof.
  intros prec_valid unsatQ H Hlo.
  unfold tightenBounds.
  destruct (FloverMap.find e qMap) as [[q ?]|]; auto.
  cbn. unfold tightenLowerBound.
164
  destruct q; auto.
165 166 167 168
  destruct q2; auto.
  destruct q2_1; auto.
  destruct e2; auto.
  destruct q2_2; auto.
169
  remember (checkPre P q1 && smt_expr_eq e1 (inlineLets L e)) as b eqn: Hchk.
170 171 172 173
  destruct b; auto.
  symmetry in Hchk.
  andb_to_prop Hchk.
  rewrite <- Q2R_max. apply Rmax_lub; auto.
174
  eapply RangeBound_low_sound; eauto.
175
  eapply eval_smt_expr_complete in H; eauto.
176 177 178 179
  rewrite SMTArith2Expr_exact.
  exact H.
Qed.

180 181 182 183 184 185 186
Lemma tightenBounds_high_sound E Gamma e v iv qMap P L :
  eval_precond E P ->
  (forall ql qh, FloverMap.find e qMap = Some (ql, qh) -> ~ eval_smt_logic E qh) ->
  eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR
            (toREval (toRExp (inlineLets L e))) v REAL ->
  (v <= Q2R (snd iv))%R ->
  (v <= Q2R (snd (tightenBounds e iv qMap P L)))%R.
187 188 189 190 191 192 193 194 195 196
Proof.
  intros prec_valid unsatQ H Hlo.
  unfold tightenBounds.
  destruct (FloverMap.find e qMap) as [[q ?]|]; auto.
  cbn. unfold tightenUpperBound.
  destruct s; auto.
  destruct s2; auto.
  destruct s2_1; auto.
  destruct e1; auto.
  destruct s2_2; auto.
197
  remember (checkPre P s1 && smt_expr_eq e2 (inlineLets L e)) as b eqn: Hchk.
198 199 200 201
  destruct b; auto.
  symmetry in Hchk.
  andb_to_prop Hchk.
  rewrite <- Q2R_min. apply Rmin_glb; auto.
202
  eapply RangeBound_high_sound; eauto.
203
  eapply eval_smt_expr_complete in H; eauto.
204 205 206 207
  rewrite SMTArith2Expr_exact.
  exact H.
Qed.

208 209 210 211 212 213 214 215
Lemma tightenBounds_sound E Gamma e v iv qMap P L :
  eval_precond E P ->
  (forall ql qh, FloverMap.find e qMap = Some (ql, qh) ->
            ~ eval_smt_logic E ql /\ ~ eval_smt_logic E qh) ->
  eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR
              (toREval (toRExp (inlineLets L e))) v REAL ->
  (Q2R (fst iv) <= v <= Q2R (snd iv))%R ->
  (Q2R (fst (tightenBounds e iv qMap P L)) <= v <= Q2R (snd (tightenBounds e iv qMap P L)))%R.
Joachim Bard's avatar
Joachim Bard committed
216 217 218 219 220 221 222 223
Proof.
  intros H unsatQ ? ?. split.
  - eapply tightenBounds_low_sound; try eassumption; [| lra].
    intros. edestruct unsatQ; eauto.
  - eapply tightenBounds_high_sound; try eassumption; [| lra].
    intros. edestruct unsatQ; eauto.
Qed.

Joachim Bard's avatar
Joachim Bard committed
224
Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond)
225
         (Q: usedQueries) L (validVars: NatSet.t) : bool :=
226 227 228 229 230 231 232 233
  match FloverMap.find e A with
  | None => false
  | Some (intv, _) =>
       match e with
       | Var _ x =>
         if NatSet.mem x validVars
         then true
         else
234
           match FloverMap.find e (fst P) with
235
           | None => false
236
           | Some iv =>
237
             let new_iv := tightenBounds e iv Q P L in
238
             isSupersetIntv new_iv intv
239 240 241
           end
       | Const _ n => (Qleb (ivlo intv) n) && (Qleb n (ivhi intv))
       | Unop o f =>
242
         if validSMTIntervalbounds f A P Q L validVars
243 244 245 246 247 248
         then
           match FloverMap.find f A with
           | None => false
           | Some (iv, _) =>
             match o with
             | Neg =>
249
               let new_iv := tightenBounds e (negateIntv iv) Q P L in
250 251 252 253 254
               isSupersetIntv new_iv intv
             | Inv =>
               if (((Qleb (ivhi iv) 0) && (negb (Qeq_bool (ivhi iv) 0))) ||
                   ((Qleb 0 (ivlo iv)) && (negb (Qeq_bool (ivlo iv) 0))))
               then
255
                 let new_iv := tightenBounds e (invertIntv iv) Q P L in
256 257 258 259 260 261
                 isSupersetIntv new_iv intv
               else false
             end
           end
         else false
       | Binop op f1 f2 =>
262 263
         if ((validSMTIntervalbounds f1 A P Q L validVars)
               && (validSMTIntervalbounds f2 A P Q L validVars))
264 265 266 267 268
         then
           match FloverMap.find f1 A, FloverMap.find f2 A with
           | Some (iv1, _), Some (iv2, _) =>
             match op with
             | Plus =>
269
               let new_iv := tightenBounds e (addIntv iv1 iv2) Q P L in
270 271
               isSupersetIntv new_iv intv
             | Sub =>
272
               let new_iv := tightenBounds e (subtractIntv iv1 iv2) Q P L in
273 274
               isSupersetIntv new_iv intv
             | Mult =>
275
               let new_iv := tightenBounds e (multIntv iv1 iv2) Q P L in
276 277 278 279 280
               isSupersetIntv new_iv intv
             | Div =>
               if (((Qleb (ivhi iv2) 0) && (negb (Qeq_bool (ivhi iv2) 0))) ||
                   ((Qleb 0 (ivlo iv2)) && (negb (Qeq_bool (ivlo iv2) 0))))
               then
281
                 let new_iv := tightenBounds e (divideIntv iv1 iv2) Q P L in
282 283 284 285 286 287 288
                 isSupersetIntv new_iv intv
               else false
             end
           | _, _ => false
           end
         else false
       | Fma f1 f2 f3 =>
289 290 291
         if ((validSMTIntervalbounds f1 A P Q L validVars)
               && (validSMTIntervalbounds f2 A P Q L validVars)
               && (validSMTIntervalbounds f3 A P Q L validVars))
292 293 294
         then
           match FloverMap.find f1 A, FloverMap.find f2 A, FloverMap.find f3 A with
           | Some (iv1, _), Some (iv2, _), Some (iv3, _) =>
Joachim Bard's avatar
Joachim Bard committed
295 296
             let mult_iv := tightenBounds (Binop Mult f1 f2) (multIntv iv1 iv2) Q P L in
             let new_iv := tightenBounds e (addIntv mult_iv iv3) Q P L in
297 298 299 300 301
             isSupersetIntv new_iv intv
           | _, _, _ => false
           end
         else false
       | Downcast _ f1 =>
302
         if (validSMTIntervalbounds f1 A P Q L validVars)
303 304 305 306
         then
           match FloverMap.find f1 A with
           | None => false
           | Some (iv1, _) =>
Joachim Bard's avatar
Joachim Bard committed
307
             isSupersetIntv (tightenBounds e iv1 Q P L) intv
308 309 310
           end
         else
           false
Joachim Bard's avatar
Joachim Bard committed
311 312 313 314 315 316 317 318 319 320 321 322
       | Let _ x e1 e2 =>
         if validSMTIntervalbounds e1 A P Q L validVars &&
            validSMTIntervalbounds e2 A P Q (updLets x e1 L) (NatSet.add x validVars)
         then
           match FloverMap.find e1 A, FloverMap.find (Var _ x) A, FloverMap.find e2 A with
           | Some ((e_lo,e_hi), _), Some ((x_lo, x_hi), _), Some (iv2, _) =>
             Qeq_bool (e_lo) (x_lo) &&
             Qeq_bool (e_hi) (x_hi) &&
             isSupersetIntv iv2 intv
           | _, _, _ => false
           end
         else false
323
       (* | Cond f1 f2 f3 => false *)
Joachim Bard's avatar
Joachim Bard committed
324 325 326 327 328 329 330 331 332 333 334 335
       (*
       if ((validSMTIntervalbounds f1 A P validVars) &&
           (validSMTIntervalbounds f2 A P validVars) &&
           (validSMTIntervalbounds f3 A P validVars))
       then
         match FloverMap.find f1 A, FloverMap.find f2 A, FloverMap.find f3 A with
         | Some (iv1, _), Some (iv2, _), Some (iv3, _) =>
           let new_iv := (* TODO *) in
           isSupersetIntv new_iv intv
         | _, _, _ => false
         end
       else false
336
            *)
337 338 339
       end
  end.

Joachim Bard's avatar
Joachim Bard committed
340
Theorem validSMTIntervalbounds_sound (f: expr Q) (A: analysisResult) (P: precond)
Joachim Bard's avatar
Joachim Bard committed
341
        (Q: usedQueries) L fVars dVars outVars (E: env) Gamma :
342
  unsat_queries Q ->
Joachim Bard's avatar
Joachim Bard committed
343
  lets_sound L E Gamma ->
Joachim Bard's avatar
Joachim Bard committed
344
  (forall x e, L x = Some e -> NatSet.Subset (NatSet.add x (freeVars e)) (fVars  dVars)) ->
Joachim Bard's avatar
Joachim Bard committed
345
  ssa f (fVars  dVars) outVars ->
346
  validSMTIntervalbounds f A P Q L dVars = true ->
347
  dVars_range_valid dVars E A ->
Joachim Bard's avatar
Joachim Bard committed
348 349
  NatSet.Subset (preVars P) fVars ->
  NatSet.Subset ((freeVars f) -- dVars) fVars ->
350
  eval_precond E P ->
351 352 353
  validTypes f Gamma ->
  validRanges f A E (toRTMap (toRExpMap Gamma)).
Proof.
Joachim Bard's avatar
Joachim Bard committed
354 355
  induction f in L, E, dVars |- *;
    intros unsat_qs Lsound Lvars_valid ssa_f valid_bounds valid_definedVars preVars_free usedVars_subset valid_precond types_defined;
356 357 358 359 360 361 362 363 364 365 366 367 368
    cbn in *.
  - destruct (NatSet.mem n dVars) eqn:?; cbn in *; split; auto.
    + destruct (valid_definedVars n)
        as [vR [iv_n [err_n [env_valid [map_n bounds_valid]]]]];
        try set_tac.
      rewrite map_n in *.
      kill_trivial_exists.
      eexists; split; [auto| split; try eauto ].
      eapply Var_load; cbn; try auto.
      destruct (types_defined) as [m [find_m _]].
      eapply toRExpMap_some in  find_m; cbn; eauto.
      match_simpl; auto.
    + Flover_compute.
369 370
      destruct valid_precond as [valid_pre_intv ?].
      destruct (valid_pre_intv n i0) as [vR [env_valid bounds_valid]];
371
        auto using find_in_precond; set_tac.
372 373
      canonize_hyps.
      kill_trivial_exists.
374 375 376
      assert (Heval: eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR
                               (Var Rdefinitions.R n) vR REAL).
      { constructor; auto.
Joachim Bard's avatar
Joachim Bard committed
377
        destruct types_defined as [m [find_m _]].
378
        eapply toRExpMap_some in find_m; cbn; eauto.
379 380 381 382
        match_simpl; auto. }
      eexists; split; [auto | split; eauto].
      eapply Rle_trans2; eauto.
      eapply tightenBounds_sound; eauto.
383 384
      * split; eauto.
      * cbn. Flover_compute; eauto.
385 386 387 388 389 390 391 392 393 394
  - split; [auto |].
    Flover_compute; canonize_hyps; cbn in *.
    kill_trivial_exists.
    exists (perturb (Q2R v) REAL 0).
    split; [eauto| split].
    + econstructor; try eauto.
      cbn. rewrite Rabs_R0; lra.
    + unfold perturb; cbn; lra.
  - Flover_compute; cbn in *; try congruence.
    assert (validRanges f A E (toRTMap (toRExpMap Gamma))) as valid_e.
Joachim Bard's avatar
Joachim Bard committed
395
    { inversion ssa_f. eapply IHf; eauto.
396 397 398 399 400 401 402 403
      destruct types_defined as [? [? [[? ?] ?]]]; auto. }
    split; try auto.
    apply validRanges_single in valid_e.
    destruct valid_e as [iv_f [err_f [vF [iveq_f [eval_f valid_bounds_f]]]]].
    rewrite Heqo0 in iveq_f; inversion iveq_f; subst.
    inversion iveq_f; subst.
    destruct u; try andb_to_prop R; cbn in *.
    + kill_trivial_exists.
404 405 406 407 408 409 410 411
      pose (v := ((evalUnop Neg vF) )).
      exists v; split; auto.
      assert (Heval: eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR
                               (Unop Neg (toREval (toRExp f))) v REAL)
        by (econstructor; try eassumption; auto).
      split; auto.
      canonize_hyps.
      eapply Rle_trans2; eauto.
Joachim Bard's avatar
Joachim Bard committed
412 413
      eapply tightenBounds_sound; eauto.
      eapply inlineLets_sound; eauto.
414
      cbn. rewrite !Q2R_opp. lra.
415
    + rename L1 into nodiv0.
416 417
      apply le_neq_bool_to_lt_prop in nodiv0.
      kill_trivial_exists.
418 419
      pose (v := (perturb (evalUnop Inv vF) REAL 0)).
      exists v.
420 421
      assert (Heval: eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR
                               (Unop Inv (toREval (toRExp f))) v REAL).
422 423 424 425
      { econstructor; eauto.
        - auto.
        - cbn. rewrite Rabs_R0. lra.
        - hnf. destruct nodiv0 as [nodiv0 | nodiv0]; apply Qlt_Rlt in nodiv0;
426
               rewrite Q2R0_is_0 in nodiv0; lra. }
427 428
       split; [destruct i; auto | split; auto].
      canonize_hyps.
429 430 431 432
        pose proof (interval_inversion_valid ((Q2R (fst iv_f)),(Q2R (snd iv_f)))
                                             (a :=vF))
          as inv_valid.
         unfold invertInterval in inv_valid; cbn in *.
Joachim Bard's avatar
Joachim Bard committed
433
         eapply Rle_trans2; eauto.
434
         eapply tightenBounds_sound; eauto using inlineLets_sound.
Joachim Bard's avatar
Joachim Bard committed
435 436 437 438 439 440 441 442 443
         cbn. rewrite ?Q2R_inv.
         * apply inv_valid; auto.
           destruct nodiv0; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto.
         * hnf; intros. destruct nodiv0; try lra.
           assert ((fst iv_f) < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H0; lra).
           lra.
         * hnf; intros. destruct nodiv0; try lra.
           assert (0 < (snd iv_f)) by (apply Rlt_Qlt; apply Qlt_Rlt in H0; lra).
           lra.
444 445
  - destruct types_defined
      as [? [? [[? [? ?]]?]]].
Joachim Bard's avatar
Joachim Bard committed
446
    inversion ssa_f.
447 448 449 450 451 452 453 454
    assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1.
    { Flover_compute; try congruence. eapply IHf1; try eauto.
      - now extended_ssa.
      - set_tac. }
    assert (validRanges f2 A E (toRTMap (toRExpMap Gamma))) as valid_f2.
    { Flover_compute; try congruence. eapply IHf2; try eauto.
      - now extended_ssa.
      - set_tac. }
455 456 457 458 459 460 461 462 463
    repeat split;
      [ intros; subst; Flover_compute; congruence |
                       auto | auto |].
    apply validRanges_single in valid_f1;
      apply validRanges_single in valid_f2.
    destruct valid_f1 as [iv_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]].
    destruct valid_f2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]].
    Flover_compute; try congruence.
    kill_trivial_exists.
Joachim Bard's avatar
Joachim Bard committed
464 465
    pose (v := perturb (evalBinop b vF1 vF2) REAL 0).
    exists v.
466 467
    assert (Heval: eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR
                             (Binop b (toREval (toRExp f1)) (toREval (toRExp f2))) v REAL).
Joachim Bard's avatar
Joachim Bard committed
468 469 470
    { destruct b; cbn in *;
      eapply Binop_dist' with (delta := 0%R); try congruence;
        try rewrite Rabs_R0; cbn; try lra; try reflexivity; eauto.
471
      andb_to_prop R. intros. rename L0 into nodiv0.
Joachim Bard's avatar
Joachim Bard committed
472 473 474 475
      apply le_neq_bool_to_lt_prop in nodiv0.
      hnf. destruct nodiv0 as [nodiv0 | nodiv0]; apply Qlt_Rlt in nodiv0;
             rewrite Q2R0_is_0 in nodiv0; lra. }
      split; [destruct i; auto | split; auto].
476
    inversion env1; inversion env2; subst.
Joachim Bard's avatar
Joachim Bard committed
477 478 479 480
    destruct b; cbn in *.
    * andb_to_prop R.
      canonize_hyps.
      pose proof (@interval_addition_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
481 482 483
                                          (Q2R (fst iv_f2), Q2R (snd iv_f2)))
        as valid_add.
      specialize (valid_add vF1 vF2 valid_f1 valid_f2).
484 485
      cbn in *.
      rewrite <- ?Q2R_plus, <- ?Q2R_min4, <- ?Q2R_max4 in valid_add.
Joachim Bard's avatar
Joachim Bard committed
486
      eapply Rle_trans2; eauto.
487
      eapply tightenBounds_sound; eauto using inlineLets_sound.
Joachim Bard's avatar
Joachim Bard committed
488
    * andb_to_prop R.
489 490 491 492 493
      canonize_hyps; cbn in *.
      pose proof (interval_subtraction_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
                                             (Q2R (fst iv_f2), Q2R (snd iv_f2)))
        as valid_sub.
      specialize (valid_sub vF1 vF2 valid_f1 valid_f2).
494 495
      cbn in *.
      rewrite <- ?Q2R_opp, <- ?Q2R_plus, <- ?Q2R_min4, <- ?Q2R_max4 in valid_sub.
Joachim Bard's avatar
Joachim Bard committed
496
      eapply Rle_trans2; eauto.
497
      eapply tightenBounds_sound; eauto using inlineLets_sound.
Joachim Bard's avatar
Joachim Bard committed
498
    * andb_to_prop R.
499 500 501 502 503
      canonize_hyps; cbn in *.
      pose proof (interval_multiplication_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
                                                (Q2R (fst iv_f2), Q2R (snd iv_f2)))
        as valid_mul.
      specialize (valid_mul vF1 vF2 valid_f1 valid_f2).
504 505
      cbn in *.
      rewrite <- ?Q2R_mult, <- ?Q2R_min4, <- ?Q2R_max4 in valid_mul.
Joachim Bard's avatar
Joachim Bard committed
506
      eapply Rle_trans2; eauto.
507
      eapply tightenBounds_sound; eauto using inlineLets_sound.
508 509
    * andb_to_prop R.
      canonize_hyps.
510 511
      rename L0 into nodiv0.
      apply le_neq_bool_to_lt_prop in nodiv0.
Joachim Bard's avatar
Joachim Bard committed
512
      pose proof (interval_division_valid (a:=vF1) (b:=vF2)
513 514 515 516 517
                                            ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
                                            (Q2R (fst iv_f2), Q2R (snd iv_f2)))
        as valid_div.
        cbn in *.
        destruct valid_div; try auto.
518
        { destruct nodiv0; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto. }
Joachim Bard's avatar
Joachim Bard committed
519
          assert (~ (snd iv_f2) == 0).
520
          { hnf; intros. destruct nodiv0; try lra.
521
            assert (0 < (snd iv_f2)) by (apply Rlt_Qlt; apply Qlt_Rlt in H8; lra).
522 523
            lra. }
          assert (~ (fst iv_f2) == 0).
524
          { hnf; intros; destruct nodiv0; try lra.
525
            assert ((fst iv_f2) < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H9; lra).
526 527
            lra. }
          repeat (rewrite <- Q2R_inv in *; try auto).
528
          rewrite <- ?Q2R_mult, <- ?Q2R_min4, <- ?Q2R_max4 in *.
Joachim Bard's avatar
Joachim Bard committed
529
          eapply Rle_trans2; eauto.
530
          eapply tightenBounds_sound; eauto using inlineLets_sound.
531 532
  - destruct types_defined
      as [mG [find_mg [[validt_f1 [validt_f2 [validt_f3 valid_join]]] valid_exec]]].
Joachim Bard's avatar
Joachim Bard committed
533
    inversion ssa_f.
534 535 536 537 538 539 540 541 542 543 544 545
    assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1.
    { Flover_compute; try congruence. eapply IHf1; try eauto.
      - now extended_ssa.
      - set_tac. }
    assert (validRanges f2 A E (toRTMap (toRExpMap Gamma))) as valid_f2.
    { Flover_compute; try congruence. eapply IHf2; try eauto.
      - now extended_ssa.
      - set_tac. }
    assert (validRanges f3 A E (toRTMap (toRExpMap Gamma))) as valid_f3.
    { Flover_compute; try congruence. eapply IHf3; try eauto.
      - now extended_ssa.
      - set_tac. }
546 547 548 549 550 551 552 553 554
    repeat split; try auto.
    apply validRanges_single in valid_f1;
      apply validRanges_single in valid_f2;
      apply validRanges_single in valid_f3.
    destruct valid_f1 as [iv_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]].
    destruct valid_f2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]].
    destruct valid_f3 as [iv_f3 [err3 [vF3 [env3 [eval_f3 valid_f3]]]]].
    Flover_compute; try congruence.
    kill_trivial_exists.
Joachim Bard's avatar
Joachim Bard committed
555 556 557 558 559 560 561
    pose (v := perturb (evalFma vF1 vF2 vF3) REAL 0).
    exists v; split; auto.
    assert (Heval: eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR
                             (Fma (toREval (toRExp f1)) (toREval (toRExp f2))
                                  (toREval (toRExp f3))) v REAL).
    { eapply Fma_dist' with (delta := 0%R); try congruence; cbn;
        try rewrite Rabs_R0; try auto; try lra; eauto. }
562 563
    inversion env1; inversion env2; inversion env3; subst.
    split; [auto | ].
Joachim Bard's avatar
Joachim Bard committed
564 565 566 567 568 569
    pose proof (interval_multiplication_valid (Q2R (fst iv_f1),Q2R (snd iv_f1)) (Q2R (fst iv_f2), Q2R (snd iv_f2))) as valid_mul.
    specialize (valid_mul vF1 vF2 valid_f1 valid_f2).
    pose (mult_interval := tightenBounds (Binop Mult f1 f2) (multIntv iv_f1 iv_f2) Q P L).
    pose proof (@interval_addition_valid (Q2R (fst mult_interval), Q2R (snd mult_interval))
                                         (Q2R (fst iv_f3), Q2R (snd iv_f3))
                                         (vF1 * vF2) vF3) as valid_add.
Joachim Bard's avatar
Joachim Bard committed
570 571 572 573 574 575 576
    unfold mult_interval in valid_add.
    canonize_hyps.
    eapply Rle_trans2; eauto.
    eapply tightenBounds_sound; eauto using inlineLets_sound.
    cbn in *. rewrite ?Q2R_min4, ?Q2R_max4, ?Q2R_plus.
    apply valid_add; auto.
    assert (Heval_mult: eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR
Joachim Bard's avatar
Joachim Bard committed
577 578
                                  (Binop Mult (toREval (toRExp f1)) (toREval (toRExp f2)))
                                  (vF1 * vF2) REAL).
Joachim Bard's avatar
Joachim Bard committed
579 580
    { eapply Binop_dist' with (delta := 0%R); try congruence;
        try rewrite Rabs_R0; cbn; try lra; try reflexivity; eauto. }
Joachim Bard's avatar
Joachim Bard committed
581 582
    eapply tightenBounds_sound; eauto.
    eapply inlineLets_sound; eauto.
583 584 585
    + instantiate (1:=(NatSet.union outVars1 outVars2)).
      econstructor; try eauto. set_tac.
    + cbn. now rewrite ?Q2R_min4, ?Q2R_max4, ?Q2R_mult.
586 587
  - destruct types_defined
      as [mG [find_mG [[validt_f _] _]]].
Joachim Bard's avatar
Joachim Bard committed
588
    inversion ssa_f.
589
    assert (validRanges f A E (toRTMap (toRExpMap Gamma))) as valid_f1
Joachim Bard's avatar
Joachim Bard committed
590
        by (Flover_compute; try congruence; eapply IHf; eauto).
591 592 593 594 595 596
    split; try auto.
    apply validRanges_single in valid_f1.
    destruct valid_f1 as [iv_f [err_f [vF [env_f [eval_f valid_f]]]]].
    Flover_compute.
    inversion env_f; subst.
    kill_trivial_exists.
Joachim Bard's avatar
Joachim Bard committed
597 598
    pose (v := perturb vF REAL 0).
    exists v.
599
    split; [destruct i; auto |].
600
    canonize_hyps.
Joachim Bard's avatar
Joachim Bard committed
601 602 603 604 605 606 607
    assert (Heval: eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR
                             (Downcast REAL (toREval (toRExp f))) v REAL).
    { eapply Downcast_dist'; try eassumption; cbn; auto; try reflexivity.
      rewrite Rabs_R0; lra. }
    split; auto.
    eapply Rle_trans2; eauto.
    eapply tightenBounds_sound; eauto using inlineLets_sound.
Joachim Bard's avatar
Joachim Bard committed
608 609 610 611 612
  - destruct types_defined
      as [mG [find_mG [[validt_f1 [validt_f2 valid_join]] valid_exec]]].
    Flover_compute; try congruence.
    inversion ssa_f; subst.
    canonize_hyps.
613 614 615 616
    assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1.
    { Flover_compute; try congruence. eapply IHf1; try eauto.
      - now extended_ssa.
      - set_tac. }
Joachim Bard's avatar
Joachim Bard committed
617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638
    pose proof (validRanges_single _ _ _ _ valid_f1) as valid_single_f1.
    destruct valid_single_f1 as [iv_f1 [err_f1 [v [find_v [eval_f1 valid_bounds_f1]]]]].
    rewrite find_v in *; inversion Heqo0; subst.
    assert (NatSet.Subset (freeVars f1) (fVars  dVars))
      by (eapply ssa_subset_freeVars; eauto).
    assert (validRanges f2 A (updEnv n v E) (toRTMap (toRExpMap Gamma))) as valid_f2.
    { eapply (IHf2 (updLets n f1 L)); eauto.
      - intros x e' v'. unfold updLets, updEnv.
        destruct (x =? n) eqn: Heq.
        + intros He. injection He.
          intros <- H0. inversion H0; subst.
          rewrite Heq in *.
          assert (v' = v) by congruence. subst.
          apply eval_expr_ignore_bind; auto.
          rewrite freeVars_toREval_toRExp_compat.
          set_tac.
        + intros H0 H1.
          inversion H1; subst. rewrite Heq in *.
          apply eval_expr_ignore_bind.
          * eapply Lsound; eauto. now constructor.
          * rewrite freeVars_toREval_toRExp_compat.
            set_tac. intros ?.
Joachim Bard's avatar
Joachim Bard committed
639
            assert (n  fVars  dVars) by (eapply Lvars_valid; eauto; set_tac).
Joachim Bard's avatar
Joachim Bard committed
640 641 642
            eauto.
      - intros x e'. unfold updLets. destruct (x =? n) eqn: Heq.
        + intros H0. injection H0. intros <-.
Joachim Bard's avatar
Joachim Bard committed
643 644 645
          apply beq_nat_true in Heq; subst.
          set_tac. destruct H1 as [? | [_ ?]]; auto.
          apply H in H1. set_tac. tauto.
Joachim Bard's avatar
Joachim Bard committed
646 647
        + intros H0.
          eapply NatSetProps.subset_trans. eauto. set_tac. tauto.
648 649 650
      - eapply ssa_outVars_extensible with (outVars1:=outVars2); try eauto;
          [ | set_tac].
        eapply ssa_equal_set; eauto.
Joachim Bard's avatar
Joachim Bard committed
651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668
        intros x. split; set_tac; intros; tauto.
      - intros v0 mem_v0.
        unfold updEnv.
        case_eq (v0 =? n); intros v0_eq.
        + rename L1 into eq_lo;
            rename R into eq_hi.
          rewrite Nat.eqb_eq in v0_eq; subst.
          exists v; eexists; eexists. repeat split; eauto; simpl in *; lra.
        + apply valid_definedVars.
          set_tac.  destruct mem_v0 as [? | [? ?]]; try auto.
          rewrite Nat.eqb_neq in v0_eq.
          congruence.
      - intros x x_contained.
        set_tac.
        repeat split; auto.
        + right. split; auto. hnf; intros. apply H1; set_tac.
        + hnf; intros. apply H1; set_tac.
      - apply eval_precond_updEnv; auto.
669
        intros ?. set_tac. apply H3. clear H. set_tac. }
Joachim Bard's avatar
Joachim Bard committed
670 671 672 673 674 675 676 677 678
    repeat split; auto.
    + intros vR ?.
      assert (vR = v) by (eapply meps_0_deterministic; eauto); now subst.
    + apply validRanges_single in valid_f2.
      destruct valid_f2 as [? [? [v2 [find_v2 [? ?]]]]].
      rewrite find_v2 in *; inversion Heqo2; subst.
      cbn in *.
      eexists. eexists. exists v2.
      repeat split; eauto; try lra.
679
      econstructor; eauto; reflexivity.
680
Qed.