SMTValidation.v 17.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 SMTArith2 ssaPrgs RealRangeArith.
18

Joachim Bard's avatar
Joachim Bard committed
19
Definition tightenLowerBound (e: expr Q) (lo: Q) (q: SMTLogic) P :=
20 21 22
  match q with
  | AndQ qP (AndQ (LessQ e' (ConstQ v)) TrueQ) => if checkPre P qP && smt_expr_eq e' e then Qmax lo v else lo
  | _ => lo
23 24
  end.

Joachim Bard's avatar
Joachim Bard committed
25
Definition tightenUpperBound (e: expr Q) (hi: Q) (q: SMTLogic) P :=
26 27 28
  match q with
  | AndQ qP (AndQ (LessQ (ConstQ v) e') TrueQ) => if checkPre P qP && smt_expr_eq e' e then Qmin hi v else hi
  | _ => hi
29 30
  end.

Joachim Bard's avatar
Joachim Bard committed
31
Definition tightenBounds (e: expr Q) (iv: intv) (qMap: FloverMap.t (SMTLogic * SMTLogic)) P :=
32 33 34
  match FloverMap.find e qMap with
  | None => iv
  | Some (loQ, hiQ) => (tightenLowerBound e (fst iv) loQ P, tightenUpperBound e (snd iv) hiQ P)
35 36
  end.

37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97
(* TODO: debug this ltac *)
Ltac query_simpl :=
  match goal with
  | [ |- context[match ?q with | _ => _ end ]] => fail; destruct q; query_simpl
  | _ => idtac
  end.

Lemma tightenBounds_low_sound E Gamma e v iv qMap P :
  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)) (toREval (toRExp e)) v REAL
  -> (Q2R (fst iv) <= v)%R
  -> (Q2R (fst (tightenBounds e iv qMap P)) <= v)%R.
Proof.
  intros prec_valid unsatQ H Hlo.
  unfold tightenBounds.
  destruct (FloverMap.find e qMap) as [[q ?]|]; auto.
  cbn. unfold tightenLowerBound.
  destruct q; auto. cbn.
  destruct q2; auto.
  destruct q2_1; auto.
  destruct e2; auto.
  destruct q2_2; auto.
  remember (checkPre P q1 && smt_expr_eq e1 e) as b eqn: Hchk.
  destruct b; auto.
  symmetry in Hchk.
  andb_to_prop Hchk.
  rewrite <- Q2R_max. apply Rmax_lub; auto.
  eapply RangeBound_low_sound; eauto.
  erewrite eval_smt_expr_complete in H; eauto.
  rewrite SMTArith2Expr_exact.
  exact H.
Qed.

Lemma tightenBounds_high_sound E Gamma e v iv qMap P :
  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)) (toREval (toRExp e)) v REAL
  -> (v <= Q2R (snd iv))%R
  -> (v <= Q2R (snd (tightenBounds e iv qMap P)))%R.
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.
  remember (checkPre P s1 && smt_expr_eq e2 e) as b eqn: Hchk.
  destruct b; auto.
  symmetry in Hchk.
  andb_to_prop Hchk.
  rewrite <- Q2R_min. apply Rmin_glb; auto.
  eapply RangeBound_high_sound; eauto.
  erewrite eval_smt_expr_complete in H; eauto.
  rewrite SMTArith2Expr_exact.
  exact H.
Qed.

Joachim Bard's avatar
Joachim Bard committed
98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115
Lemma tightenBounds_sound E Gamma e v iv qMap P :
  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)) (toREval (toRExp e)) v REAL
  -> (Q2R (fst iv) <= v <= Q2R (snd iv))%R
  -> (Q2R (fst (tightenBounds e iv qMap P)) <= v <= Q2R (snd (tightenBounds e iv qMap P)))%R.
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.

Lemma Rle_trans2 a b x y z :
  (a <= x)%R -> (z <= b)%R -> (x <= y <= z)%R -> (a <= y <= b)%R.
Proof. lra. Qed.

116 117 118 119 120 121 122 123 124 125 126 127
Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: FloverMap.t intv)
         (Q: FloverMap.t (SMTLogic * SMTLogic)) (validVars: NatSet.t) : bool:=
  match FloverMap.find e A with
  | None => false
  | Some (intv, _) =>
       match e with
       | Var _ x =>
         if NatSet.mem x validVars
         then true
         else
           match FloverMap.find e P with
           | None => false
Joachim Bard's avatar
Joachim Bard committed
128 129
           | Some new_iv => isSupersetIntv new_iv intv
                                          (* && (Qleb lo hi) *)
130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145
           end
       | Const _ n => (Qleb (ivlo intv) n) && (Qleb n (ivhi intv))
       | Unop o f =>
         if validSMTIntervalbounds f A P Q validVars
         then
           match FloverMap.find f A with
           | None => false
           | Some (iv, _) =>
             match o with
             | Neg =>
               let new_iv := negateIntv iv in
               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
Joachim Bard's avatar
Joachim Bard committed
146
                 let new_iv := tightenBounds e (invertIntv iv) Q P in
147 148 149 150 151 152 153 154 155 156 157 158 159
                 isSupersetIntv new_iv intv
               else false
             end
           end
         else false
       | Binop op f1 f2 =>
         if ((validSMTIntervalbounds f1 A P Q validVars)
               && (validSMTIntervalbounds f2 A P Q validVars))
         then
           match FloverMap.find f1 A, FloverMap.find f2 A with
           | Some (iv1, _), Some (iv2, _) =>
             match op with
             | Plus =>
Joachim Bard's avatar
Joachim Bard committed
160
               let new_iv := tightenBounds e (addIntv iv1 iv2) Q P in
161 162
               isSupersetIntv new_iv intv
             | Sub =>
Joachim Bard's avatar
Joachim Bard committed
163
               let new_iv := tightenBounds e (subtractIntv iv1 iv2) Q P in
164 165
               isSupersetIntv new_iv intv
             | Mult =>
Joachim Bard's avatar
Joachim Bard committed
166
               let new_iv := tightenBounds e (multIntv iv1 iv2) Q P in
167 168 169 170 171
               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
Joachim Bard's avatar
Joachim Bard committed
172
                 let new_iv := tightenBounds e (divideIntv iv1 iv2) Q P in
173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208
                 isSupersetIntv new_iv intv
               else false
             end
           | _, _ => false
           end
         else false
       | Fma f1 f2 f3 =>
         if ((validSMTIntervalbounds f1 A P Q validVars)
               && (validSMTIntervalbounds f2 A P Q validVars)
               && (validSMTIntervalbounds f3 A P Q 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 := addIntv iv1 (multIntv iv2 iv3) in
             isSupersetIntv new_iv intv
           | _, _, _ => false
           end
         else false
       | Downcast _ f1 =>
         if (validSMTIntervalbounds f1 A P Q validVars)
         then
           match FloverMap.find f1 A with
           | None => false
           | Some (iv1, _) =>
             (isSupersetIntv intv iv1) && (isSupersetIntv iv1 intv)
           end
         else
           false
       end
  end.

Theorem validSMTIntervalbounds_sound (f: expr Q) (A: analysisResult) (P: FloverMap.t intv)
        (Q: FloverMap.t (SMTLogic * SMTLogic)) fVars dVars (E: env) Gamma :
  (forall e loQ hiQ, FloverMap.find e Q = Some (loQ, hiQ) -> ~ eval_smt_logic E loQ /\ ~ eval_smt_logic E hiQ) ->
  validSMTIntervalbounds f A P Q dVars = true ->
  dVars_range_valid dVars E A ->
Joachim Bard's avatar
Joachim Bard committed
209
  NatSet.Subset (usedVars f -- dVars) fVars ->
210 211 212 213
  eval_precond E P ->
  validTypes f Gamma ->
  validRanges f A E (toRTMap (toRExpMap Gamma)).
Proof.
Joachim Bard's avatar
Joachim Bard committed
214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267
  induction f;
    intros unsat_queries valid_bounds valid_definedVars usedVars_subset valid_precond types_defined;
    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.
      destruct (valid_precond n i0) as [vR [env_valid bounds_valid]].
      admit.
      assert (NatSet.In n fVars) by set_tac.
      canonize_hyps.
      kill_trivial_exists.
      eexists; split; [auto | split].
      * econstructor; try eauto.
        destruct (types_defined) as [m [find_m _]].
        eapply toRExpMap_some in find_m; cbn; eauto.
        match_simpl; auto.
      * cbn in *. lra.
  - 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.
    { apply IHf; try auto.
      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.
      exists (evalUnop Neg vF); split;
        [auto | split ; [econstructor; eauto | ]].
      * cbn; auto.
      *  canonize_hyps.
         rewrite Q2R_opp in *.
         cbn; lra.
    + rename L0 into nodiv0.
      apply le_neq_bool_to_lt_prop in nodiv0.
      kill_trivial_exists.
268 269 270 271 272 273 274
      pose (v := (perturb (evalUnop Inv vF) REAL 0)).
      exists v.
      assert (Heval: eval_expr E (toRTMap (toRExpMap Gamma)) (Unop Inv (toREval (toRExp f))) v REAL).
      { econstructor; eauto.
        - auto.
        - cbn. rewrite Rabs_R0. lra.
        - hnf. destruct nodiv0 as [nodiv0 | nodiv0]; apply Qlt_Rlt in nodiv0;
Joachim Bard's avatar
Joachim Bard committed
275
               rewrite Q2R0_is_0 in nodiv0; lra. }
276 277
       split; [destruct i; auto | split; auto].
      canonize_hyps.
Joachim Bard's avatar
Joachim Bard committed
278 279 280 281
        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
282 283 284 285 286 287 288 289 290 291 292
         eapply Rle_trans2; eauto.
         eapply tightenBounds_sound; eauto.
         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.
Joachim Bard's avatar
Joachim Bard committed
293 294 295 296 297 298 299 300 301 302 303 304 305 306 307
  - destruct types_defined
      as [? [? [[? [? ?]]?]]].
    assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1
        by (Flover_compute; try congruence; apply IHf1; try auto; set_tac).
    assert (validRanges f2 A E (toRTMap (toRExpMap Gamma))) as valid_f2
        by (Flover_compute; try congruence; apply IHf2; try auto; set_tac).
    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
308 309 310 311 312 313 314 315 316 317 318
    pose (v := perturb (evalBinop b vF1 vF2) REAL 0).
    exists v.
    assert (Heval: eval_expr E (toRTMap (toRExpMap Gamma)) (Binop b (toREval (toRExp f1)) (toREval (toRExp f2))) v REAL).
    { destruct b; cbn in *;
      eapply Binop_dist' with (delta := 0%R); try congruence;
        try rewrite Rabs_R0; cbn; try lra; try reflexivity; eauto.
      andb_to_prop R. intros. rename L into nodiv0.
      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].
Joachim Bard's avatar
Joachim Bard committed
319
    inversion env1; inversion env2; subst.
Joachim Bard's avatar
Joachim Bard committed
320 321 322 323
    destruct b; cbn in *.
    * andb_to_prop R.
      canonize_hyps.
      pose proof (@interval_addition_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
Joachim Bard's avatar
Joachim Bard committed
324 325 326
                                          (Q2R (fst iv_f2), Q2R (snd iv_f2)))
        as valid_add.
      specialize (valid_add vF1 vF2 valid_f1 valid_f2).
Joachim Bard's avatar
Joachim Bard committed
327 328 329 330 331
      cbn in *. unfold min4, max4 in valid_add.
      rewrite <- ?Q2R_plus, ?Q2R_min, ?Q2R_max in valid_add.
      eapply Rle_trans2; eauto.
      eapply tightenBounds_sound; eauto.
    * andb_to_prop R.
Joachim Bard's avatar
Joachim Bard committed
332 333 334 335 336
      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).
Joachim Bard's avatar
Joachim Bard committed
337 338 339 340 341
      cbn in *. unfold min4, max4 in valid_sub.
      rewrite <- ?Q2R_opp, <- ?Q2R_plus, ?Q2R_min, ?Q2R_max in valid_sub.
      eapply Rle_trans2; eauto.
      eapply tightenBounds_sound; eauto.
    * andb_to_prop R.
Joachim Bard's avatar
Joachim Bard committed
342 343 344 345 346
      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).
Joachim Bard's avatar
Joachim Bard committed
347 348 349 350
      cbn in *. unfold min4, max4 in valid_mul.
      rewrite <- ?Q2R_mult, ?Q2R_min, ?Q2R_max in valid_mul.
      eapply Rle_trans2; eauto.
      eapply tightenBounds_sound; eauto.
Joachim Bard's avatar
Joachim Bard committed
351 352 353
    * andb_to_prop R.
      canonize_hyps.
      apply le_neq_bool_to_lt_prop in L.
Joachim Bard's avatar
Joachim Bard committed
354
      pose proof (interval_division_valid (a:=vF1) (b:=vF2)
Joachim Bard's avatar
Joachim Bard committed
355 356 357 358 359
                                            ((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.
Joachim Bard's avatar
Joachim Bard committed
360 361
        { destruct L; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto. }
          assert (~ (snd iv_f2) == 0).
Joachim Bard's avatar
Joachim Bard committed
362 363 364 365 366 367 368 369
          { hnf; intros. destruct L; try lra.
            assert (0 < (snd iv_f2)) by (apply Rlt_Qlt; apply Qlt_Rlt in H9; lra).
            lra. }
          assert (~ (fst iv_f2) == 0).
          { hnf; intros; destruct L; try lra.
            assert ((fst iv_f2) < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H10; lra).
            lra. }
          repeat (rewrite <- Q2R_inv in *; try auto).
Joachim Bard's avatar
Joachim Bard committed
370 371 372 373
          unfold min4, max4 in *.
          rewrite <- ?Q2R_mult, ?Q2R_min, ?Q2R_max in *.
          eapply Rle_trans2; eauto.
          eapply tightenBounds_sound; eauto.
Joachim Bard's avatar
Joachim Bard committed
374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393
  - destruct types_defined
      as [mG [find_mg [[validt_f1 [validt_f2 [validt_f3 valid_join]]] valid_exec]]].
        assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1
        by (Flover_compute; try congruence; apply IHf1; try auto; set_tac).
    assert (validRanges f2 A E (toRTMap (toRExpMap Gamma))) as valid_f2
        by (Flover_compute; try congruence; apply IHf2; try auto; set_tac).
    assert (validRanges f3 A E (toRTMap (toRExpMap Gamma))) as valid_f3
        by (Flover_compute; try congruence; apply IHf3; try auto; set_tac).
    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.
    exists (perturb (evalFma vF1 vF2 vF3) REAL 0); split; try auto.
    inversion env1; inversion env2; inversion env3; subst.
    split; [auto | ].
Joachim Bard's avatar
Joachim Bard committed
394 395
    * eapply Fma_dist' with (delta := 0%R); try congruence; cbn;
        try rewrite Rabs_R0; try auto; try lra; eauto.
Joachim Bard's avatar
Joachim Bard committed
396 397 398 399 400 401 402
    * 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).
      remember (multInterval (Q2R (fst iv_f2), Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as iv_f23prod.
      pose proof (interval_addition_valid (Q2R (fst iv_f1),Q2R (snd iv_f1)) (fst iv_f23prod, snd iv_f23prod)) as valid_add.
      rewrite Heqiv_f23prod in valid_add, valid_mul.
      unfold multIntv in valid_add.
      canonize_hyps.
Joachim Bard's avatar
Joachim Bard committed
403 404 405
      cbn in *. unfold min4, max4 in *.
      rewrite <- ?Q2R_mult, ?Q2R_min , ?Q2R_max in *.
      rewrite <- ?Q2R_plus, ?Q2R_min, ?Q2R_max in *.
Joachim Bard's avatar
Joachim Bard committed
406
      specialize (valid_add vF1 (vF2 * vF3)%R valid_f1 valid_mul).
Joachim Bard's avatar
Joachim Bard committed
407
      eapply Rle_trans2; eauto.
Joachim Bard's avatar
Joachim Bard committed
408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423
  - destruct types_defined
      as [mG [find_mG [[validt_f _] _]]].
        assert (validRanges f A E (toRTMap (toRExpMap Gamma))) as valid_f1
        by (Flover_compute; try congruence; apply IHf; auto).
    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.
    exists (perturb vF REAL 0).
    split; [destruct i; try auto |].
    split; [eapply Downcast_dist'; try eauto; cbn; try rewrite Rabs_R0 |];
      try lra; try auto.
    canonize_hyps.
    cbn in *; lra.
424
Abort.