IEEE_connection.v 53.1 KB
Newer Older
1
Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qabs Coq.micromega.Psatz
2
        Coq.QArith.Qreals.
Heiko Becker's avatar
Heiko Becker committed
3 4 5 6
Require Import Daisy.Expressions Daisy.Infra.RationalSimps Daisy.Typing
        Daisy.IntervalValidation Daisy.ErrorValidation Daisy.CertificateChecker
        Daisy.FPRangeValidator Daisy.Environments Daisy.Infra.RealRationalProps
        Daisy.Commands Daisy.Infra.Ltacs.
7 8
Require Import Flocq.Appli.Fappli_IEEE_bits Flocq.Appli.Fappli_IEEE
        Flocq.Core.Fcore_Raux Flocq.Prop.Fprop_relative.
9

Heiko Becker's avatar
Heiko Becker committed
10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
Definition dmode := mode_NE.
Definition fl64:Type := binary_float 53 1024.

Definition optionLift (A B:Type) (e:option A) (some_cont:A -> B) (none_cont:B) :=
  match e with
  | Some v => some_cont v
  | None => none_cont
  end.

Definition normal_or_zero v :=
   (v = 0 \/ (Q2R (minValue M64)) <= (Rabs v))%R.

Definition updFlEnv x v E :=
  fun y => if y =? x
        then Some (A:=(binary_float 53 1024)) v
        else E y.

Fixpoint eval_exp_float (e:exp (binary_float 53 1024)) (E:nat -> option fl64):=
28 29 30 31 32 33 34 35 36 37 38 39 40
  match e with
  | Var _ x => E x
  | Const m v => Some v
  | Unop Neg e =>
    match eval_exp_float e E with
    |Some v1 => Some (b64_opp v1)
    |_ => None
    end
  | Unop Inv e => None
  | Binop b e1 e2 =>
    match eval_exp_float e1 E, eval_exp_float e2 E with
    | Some f1, Some f2 =>
      match b with
Heiko Becker's avatar
Heiko Becker committed
41 42 43 44
      | Plus => Some (b64_plus dmode f1 f2)
      | Sub => Some (b64_minus dmode f1 f2)
      | Mult => Some (b64_mult dmode f1 f2)
      | Div => Some (b64_div dmode f1 f2)
45 46 47
      end
    |_ , _ => None
    end
Nikita Zyuzin's avatar
Nikita Zyuzin committed
48 49
  | Fma e1 e2 e3 =>
    match eval_exp_float e1 E, eval_exp_float e2 E, eval_exp_float e3 E with
50
      (* | Some f1, Some f2, Some f3 => Some (b64_plus dmode f1 (b64_mult dmode f2 f3)) *)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
51 52
      | _, _, _ => None
    end
53
  | _ => None
54 55
  end.

Heiko Becker's avatar
Heiko Becker committed
56 57 58 59 60 61 62 63 64 65 66 67 68
Fixpoint bstep_float f E :option fl64 :=
  match f with
  | Let m x e g => optionLift (eval_exp_float e E)
                             (fun v => bstep_float g (updFlEnv x v E))
                             None
  | Ret e => eval_exp_float e E
  end.

Definition isValid e :=
  let trans_e := optionLift e (fun v => Some (B2R 53 1024 v)) None in
  optionLift trans_e normal_or_zero False.

Fixpoint eval_exp_valid (e:exp fl64) E :=
69
  match e with
Heiko Becker's avatar
Heiko Becker committed
70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85
  | Var _ x => True (*isValid (eval_exp_float (Var n) E)*)
  | Const m v => True (*isValid (eval_exp_float (Const m v) E)*)
  | Unop u e => eval_exp_valid e E
  | Binop b e1 e2 =>
    (eval_exp_valid e1 E) /\ (eval_exp_valid e2 E) /\
    (let e1_res := eval_exp_float e1 E in
     let e2_res := eval_exp_float e2 E in
     optionLift e1_res
                (fun v1 =>
                   let v1_real := B2R 53 1024 v1 in
                   optionLift e2_res
                              (fun v2 =>
                                 let v2_real := B2R 53 1024 v2 in
                                 normal_or_zero (evalBinop b v1_real v2_real))
                              True)
                True)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
86 87 88 89 90 91 92 93 94 95 96 97 98 99
  | Fma e1 e2 e3 =>
    (eval_exp_valid e1 E) /\ (eval_exp_valid e2 E) /\ (eval_exp_valid e3 E) /\
    (let e1_res := eval_exp_float e1 E in
     let e2_res := eval_exp_float e2 E in
     let e3_res := eval_exp_float e3 E in
     optionLift e1_res
                (fun v1 =>
                   let v1_real := B2R 53 1024 v1 in
                   optionLift e2_res
                              (fun v2 =>
                                 let v2_real := B2R 53 1024 v2 in
                                 optionLift e3_res
                                            (fun v3 =>
                                               let v3_real := B2R 53 1024 v3 in
100 101 102
                                               (* No support for fma yet *)
                                               (* normal_or_zero (evalFma v1_real v2_real v3_real)) *)
                                               False)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
103 104 105
                                            True)
                              True)
                True)
Heiko Becker's avatar
Heiko Becker committed
106
  | Downcast m e => eval_exp_valid e E
107 108
  end.

Heiko Becker's avatar
Heiko Becker committed
109 110
Fixpoint bstep_valid f E :=
  match f with
111 112 113 114 115
  | Let m x e g =>
    eval_exp_valid e E /\
    (optionLift (eval_exp_float e E)
                (fun v_e => bstep_valid g (updFlEnv x v_e E))
                True)
Heiko Becker's avatar
Heiko Becker committed
116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180
  | Ret e => eval_exp_valid e E
  end.

Definition bpowQ (r:radix) (e: Z) :=
  match e with
  |0%Z => 1%Q
  | (' p)%Z => (Z.pow_pos r p) #1
  | Z.neg p => Qinv ((Z.pow_pos r p)#1)
  end.

Definition B2Q :=
  fun prec emax : Z =>
    let emin := (3 - emax - prec)%Z in
    let fexp := Fcore_FLT.FLT_exp emin prec in
    fun f : binary_float prec emax =>
      match f with
      | B754_zero _ _ _ => 0%Q
      | B754_infinity _ _ _ => (bpowQ radix2 emax) +1%Q
      | B754_nan _ _ _ _ => (bpowQ radix2 emax) +1%Q
      | B754_finite _ _ s m e _ =>
        let f_new: Fcore_defs.float radix2 := {| Fcore_defs.Fnum := cond_Zopp s (' m); Fcore_defs.Fexp := e |} in
        (Fcore_defs.Fnum f_new # 1) * bpowQ radix2 (Fcore_defs.Fexp f_new)
      end.

Lemma B2Q_B2R_eq :
  forall v,
    is_finite 53 1024 v = true ->
    Q2R (B2Q v) = B2R 53 1024 v.
Proof.
  intros; unfold B2Q, B2R, is_finite in *.
  destruct v eqn:?; try congruence;
    try rewrite Q2R0_is_0; try lra.
  unfold Fcore_defs.F2R.
  rewrite Q2R_mult.
  f_equal.
  - unfold Z2R, Q2R.
    simpl. rewrite RMicromega.Rinv_1.
    destruct (cond_Zopp b (' m)); unfold IZR;
      try rewrite P2R_INR; try lra.
  - unfold Q2R; simpl.
    unfold bpow, bpowQ.
    destruct e; simpl; try lra.
    + rewrite RMicromega.Rinv_1.
      unfold Z2R, IZR.
      destruct (Z.pow_pos 2 p); try rewrite P2R_INR; auto.
    + unfold Z2R, IZR. unfold Qinv; simpl.
      destruct (Z.pow_pos 2 p) eqn:? ; try rewrite P2R_INR; simpl; try lra.
      * unfold bounded in e0.  simpl in e0. unfold canonic_mantissa in e0.
        simpl in e0.
        pose proof (Is_true_eq_left _ e0).
        apply Is_true_eq_true in H0; andb_to_prop H0.
        assert (0 < Z.pow_pos 2 p)%Z.
        { apply Zpower_pos_gt_0. cbv; auto. }
        rewrite Heqz in H0. inversion H0.
      * rewrite <- Ropp_mult_distr_l, Ropp_mult_distr_r, Ropp_inv_permute; try lra.
        hnf; intros.  pose proof (pos_INR_nat_of_P p0).
        rewrite H0 in H1; lra.
Qed.

Fixpoint B2Qexp (e: exp fl64) :=
  match e with
  | Var _ x =>  Var Q x
  | Const m v => Const m (B2Q v)
  | Unop u e => Unop u (B2Qexp e)
  | Binop b e1 e2 => Binop b (B2Qexp e1) (B2Qexp e2)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
181
  | Fma e1 e2 e3 => Fma (B2Qexp e1) (B2Qexp e2) (B2Qexp e3)
Heiko Becker's avatar
Heiko Becker committed
182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202
  | Downcast m e => Downcast m (B2Qexp e)
  end.

Fixpoint B2Qcmd (f:cmd fl64) :=
  match f with
  | Let m x e g => Let m x (B2Qexp e) (B2Qcmd g)
  | Ret e => Ret (B2Qexp e)
  end.

Definition toREnv (E: nat -> option fl64) (x:nat):option R :=
  match E x with
  |Some v => Some (Q2R (B2Q v))
  |_ => None
  end.

Fixpoint is64BitEval (V:Type) (e:exp V) :=
  match e with
  | Var _ x => True
  | Const m e => m = M64
  | Unop u e => is64BitEval e
  | Binop b e1 e2 => is64BitEval e1 /\ is64BitEval e2
Nikita Zyuzin's avatar
Nikita Zyuzin committed
203
  | Fma e1 e2 e3 => is64BitEval e1 /\ is64BitEval e2 /\ is64BitEval e3
Heiko Becker's avatar
Heiko Becker committed
204 205 206 207 208 209 210 211 212 213 214 215 216 217 218
  | Downcast m e => m = M64 /\ is64BitEval e
  end.

Fixpoint is64BitBstep (V:Type) (f:cmd V) :=
  match f with
  | Let m x e g => is64BitEval e /\ m = M64 /\ is64BitBstep g
  | Ret e => is64BitEval e
  end.

Fixpoint noDowncast (V:Type) (e:exp V) :=
  match e with
  | Var _ x => True
  | Const m e => True
  | Unop u e => noDowncast e
  | Binop b e1 e2 => noDowncast e1 /\ noDowncast e2
Nikita Zyuzin's avatar
Nikita Zyuzin committed
219
  | Fma e1 e2 e3 => noDowncast e1 /\ noDowncast e2 /\ noDowncast e3
Heiko Becker's avatar
Heiko Becker committed
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 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295
  | Downcast m e => False
  end.

Fixpoint noDowncastFun (V:Type) (f:cmd V) :=
  match f with
  | Let m x e g => noDowncast e /\ noDowncastFun g
  | Ret e => noDowncast e
  end.

Opaque mTypeToQ.

Lemma validValue_is_finite v:
  validFloatValue (Q2R (B2Q v)) M64 -> is_finite 53 1024 v = true.
Proof.
  intros validVal.
  unfold is_finite.
  unfold validFloatValue, B2Q in *.
  destruct v; try auto;
    destruct validVal; unfold Normal in *; unfold Denormal in *;
      unfold maxValue, minValue, maxExponent, minExponentPos in*;
      rewrite Q2R_inv in *; unfold bpowQ in *.
  - assert (Z.pow_pos radix2 1024 = 179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216%Z)
      by (vm_compute;auto).
    rewrite H0 in H; destruct H; try lra.
    assert (Z.pow_pos 2 1023 = 89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608%Z)
      by (vm_compute; auto).
    rewrite H2 in *.
    clear H0 H2.
    rewrite Rabs_right in H1.
    apply Rle_Qle in H1.
    + rewrite <- Qle_bool_iff in H1.
      cbv in H1; try congruence.
    + rewrite <- Q2R0_is_0.
      apply Rle_ge. apply Qle_Rle; rewrite <- Qle_bool_iff; cbv; auto.
  - vm_compute; intros; congruence.
  - destruct H.
    + destruct H. rewrite Rabs_right in H.
      * rewrite <- Q2R_inv in H.
        apply Rlt_Qlt in H.
        vm_compute in H.
        congruence.
        vm_compute; congruence.
      * rewrite <- Q2R0_is_0.
        apply Rle_ge. apply Qle_Rle; rewrite <- Qle_bool_iff; cbv; auto.
    + rewrite <- Q2R0_is_0 in H.
      apply eqR_Qeq in H.
      vm_compute in H; congruence.
  - vm_compute; congruence.
  - destruct H.
    rewrite Rabs_right in H0.
    + apply Rle_Qle in H0.
      rewrite <- Qle_bool_iff in H0.
      vm_compute in H0; auto.
    + rewrite <- Q2R0_is_0.
      apply Rle_ge. apply Qle_Rle; rewrite <- Qle_bool_iff; cbv; auto.
  - vm_compute; congruence.
  - destruct H.
    + rewrite Rabs_right in H.
      * destruct H. rewrite <- Q2R_inv in H.
        { apply Rlt_Qlt in H. rewrite Qlt_alt in H.
          vm_compute in H. congruence. }
        { vm_compute; congruence. }
      * rewrite <- Q2R0_is_0.
        apply Rle_ge. apply Qle_Rle; rewrite <- Qle_bool_iff; cbv; auto.
    + rewrite <- Q2R0_is_0 in H.
      apply eqR_Qeq in H. vm_compute in H; congruence.
  - vm_compute; congruence.
Qed.

Lemma typing_exp_64_bit e:
  forall Gamma tMap,
    noDowncast e ->
    is64BitEval e ->
    typeCheck e Gamma tMap = true ->
    (forall v,
        NatSet.In v (usedVars e) -> Gamma v = Some M64) ->
Heiko Becker's avatar
Heiko Becker committed
296
    DaisyMap.find e tMap = Some M64.
Heiko Becker's avatar
Heiko Becker committed
297 298
Proof.
  induction e; intros * noDowncast_e is64BitEval_e typecheck_e types_valid;
Heiko Becker's avatar
Heiko Becker committed
299 300 301 302 303 304
    cbn in *; try inversion noDowncast_e;
      subst; Daisy_compute; try congruence;
        type_conv; subst.
  - rewrite types_valid in *; try set_tac.
  - destruct m; try congruence.
  - erewrite IHe in *; eauto.
Heiko Becker's avatar
Heiko Becker committed
305 306 307 308 309
  - repeat (match goal with
            |H: _ /\ _ |- _=> destruct H
            end).
      erewrite IHe1 in *; eauto.
    + erewrite IHe2 in *; eauto.
Heiko Becker's avatar
Heiko Becker committed
310 311 312 313
      * unfold join in *.
        destr_factorize.
        rewrite <- isMorePrecise_morePrecise.
        rewrite isMorePrecise_refl. inversion Heqo0; auto.
Heiko Becker's avatar
Heiko Becker committed
314 315 316
      * intros.
        apply types_valid. set_tac.
    + intros; apply types_valid; set_tac.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
317 318 319
  - repeat (match goal with
            |H: _ /\ _ |- _=> destruct H
            end).
320 321 322 323 324 325 326 327
    erewrite IHe1 in *; eauto; try (intros; apply types_valid; set_tac; fail).
    erewrite IHe2 in *; eauto; try (intros; apply types_valid; set_tac; fail).
    unfold join3, join in *.
    erewrite IHe3 in *; eauto; try (intros; apply types_valid; set_tac; fail).
    repeat destr_factorize.
    repeat rewrite <- isMorePrecise_morePrecise.
    repeat rewrite isMorePrecise_refl;
      type_conv; subst; auto.
Heiko Becker's avatar
Heiko Becker committed
328 329 330 331 332 333 334 335 336
Qed.

Lemma typing_cmd_64_bit f:
  forall Gamma tMap,
    noDowncastFun f ->
    is64BitBstep f ->
    typeCheckCmd f Gamma tMap = true ->
    (forall v,
        NatSet.In v (freeVars f) -> Gamma v = Some M64) ->
Heiko Becker's avatar
Heiko Becker committed
337
    DaisyMap.find (getRetExp f) tMap = Some M64.
Heiko Becker's avatar
Heiko Becker committed
338 339
Proof.
  induction f; intros * noDowncast_f is64BitEval_f typecheck_f types_valid;
Heiko Becker's avatar
Heiko Becker committed
340 341 342
    cbn in *;
    subst; try eauto using typing_exp_64_bit;
      Daisy_compute; try congruence.
Heiko Becker's avatar
Heiko Becker committed
343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358
  destruct noDowncast_f; destruct is64BitEval_f as [Ha [Hb Hc]].
  eapply IHf; eauto.
  intros. unfold updDefVars.
  destruct (v =? n) eqn:?.
  - type_conv; auto.
  - apply types_valid.
    rewrite NatSet.remove_spec, NatSet.union_spec.
    split; try auto.
    hnf; intros; subst. rewrite Nat.eqb_neq in Heqb.
    congruence.
Qed.

Lemma typing_agrees_exp e:
  forall E Gamma tMap v m1 m2,
    typeCheck e Gamma tMap = true ->
    eval_exp E Gamma (toRExp e) v m1 ->
Heiko Becker's avatar
Heiko Becker committed
359
    DaisyMap.find e tMap = Some m2 ->
Heiko Becker's avatar
Heiko Becker committed
360 361
    m1 = m2.
Proof.
Heiko Becker's avatar
Heiko Becker committed
362
  induction e; intros * typeCheck_e eval_e tMap_e; cbn in *;
Heiko Becker's avatar
Heiko Becker committed
363
    rewrite tMap_e in *;
Heiko Becker's avatar
Heiko Becker committed
364 365 366 367
    inversion eval_e; subst; cbn in *;
      Daisy_compute; try congruence; type_conv; subst; try auto.
  - eapply IHe; eauto.
  - eapply IHe; eauto.
368 369
  - assert (m0 = m) by eauto using IHe1.
    assert (m3 = m1) by eauto using IHe2.
Heiko Becker's avatar
Heiko Becker committed
370
    subst; auto.
371 372 373
  - assert (m0 = m) by eauto using IHe1.
    assert (m3 = m1) by eauto using IHe2.
    assert (m4 = m5) by eauto using IHe3.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
374
    subst; auto.
Heiko Becker's avatar
Heiko Becker committed
375 376 377 378 379 380
Qed.

Lemma typing_agrees_cmd f:
  forall E Gamma tMap v m1 m2,
    typeCheckCmd f Gamma tMap = true ->
    bstep (toRCmd f) E Gamma v m1 ->
Heiko Becker's avatar
Heiko Becker committed
381
    DaisyMap.find (getRetExp f) tMap = Some m2 ->
Heiko Becker's avatar
Heiko Becker committed
382 383
    m1 = m2.
Proof.
Heiko Becker's avatar
Heiko Becker committed
384 385 386
  induction f; intros * typeCheck_f eval_f tMap_f; cbn in *;
    Daisy_compute; try congruence; type_conv; subst.
  - inversion eval_f; subst; simpl in *.
Heiko Becker's avatar
Heiko Becker committed
387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475
    specialize (IHf (updEnv n v0 E) (updDefVars n m3 Gamma) tMap v m1 m2).
    apply IHf; auto.
  - inversion eval_f; subst; eapply typing_agrees_exp; eauto.
Qed.

Lemma round_0_zero:
  (Fcore_generic_fmt.round radix2 (Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
                           (round_mode mode_NE) 0) = 0%R.
Proof.
  unfold Fcore_generic_fmt.round. simpl.
  unfold Fcore_generic_fmt.scaled_mantissa.
  rewrite Rmult_0_l.
  unfold Fcore_generic_fmt.Znearest.
  unfold Zfloor.
  assert (up 0 = 1%Z).
  { symmetry. apply tech_up; lra. }
  rewrite H.
  simpl. rewrite Rsub_eq_Ropp_Rplus. rewrite Rplus_opp_r.
  assert (Rcompare (0) (/ 2) = Lt).
  { apply Rcompare_Lt. lra. }
  rewrite H0.
  unfold Fcore_generic_fmt.canonic_exp.
  unfold Fcore_defs.F2R; simpl.
  rewrite Rmult_0_l. auto.
Qed.

Lemma validValue_bounded b v_e1 v_e2:
  (Normal (evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2)) M64\/
   ((evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2)) = 0)%R) ->
  (forall eps, (Rabs eps <= / 2 * bpow radix2 (- 53 + 1))%R ->
  validFloatValue ((evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2)) * (1 + eps)) M64) ->
  Rlt_bool
    (Rabs
       (Fcore_generic_fmt.round
          radix2
          (Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
          (round_mode mode_NE)
          (evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2))))
    (bpow radix2 1024) = true.
Proof.
  simpl.
  pose proof (fexp_correct 53 1024 eq_refl) as fexp_corr.
  assert (forall k : Z, (-1022 < k)%Z ->
                     (53 <= k - Fcore_FLT.FLT_exp (3 - 1024 - 53) 53 k)%Z)
    as exp_valid.
  { intros k k_pos.
    unfold Fcore_FLT.FLT_exp; simpl.
    destruct (Z.max_spec_le (k - 53) (-1074)); omega. }
  pose proof (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53)
                                  (-1022)%Z 53%Z exp_valid)
    as rel_error_exists.
  intros [normal_v | zero_v] validVal;
  apply Rlt_bool_true.
  - unfold Normal in *; destruct normal_v.
    specialize (rel_error_exists (fun x => negb (Zeven x))
                                 (evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2))%R).
    destruct (rel_error_exists) as [eps [bounded_eps round_eq]].
    + eapply Rle_trans; eauto.
      unfold minValue, Z.pow_pos; simpl.
      rewrite Q2R_inv.
      * apply Rinv_le.
        { rewrite <- Q2R0_is_0. apply Qlt_Rlt.
          apply Qlt_alt. vm_compute; auto. }
        { unfold Q2R.
          unfold Qnum, Qden. lra. }
      *  vm_compute; congruence.
    + simpl in *.
      rewrite round_eq.
      destruct (validVal eps) as [normal_v | [denormal_v | zero_v]]; try auto.
      * unfold Normal in *. destruct normal_v.
        eapply Rle_lt_trans; eauto.
        unfold maxValue, bpow. unfold maxExponent. unfold Q2R.
        unfold Qnum, Qden. rewrite <- Z2R_IZR. unfold IZR. simpl; lra.
      * unfold Denormal in *. destruct denormal_v.
        eapply Rlt_trans; eauto.
        unfold minValue, minExponentPos, bpow.
        rewrite Q2R_inv.
        { unfold Q2R, Qnum, Qden.
          rewrite <- Z2R_IZR; unfold IZR; simpl; lra. }
        { vm_compute; congruence. }
      * rewrite zero_v. unfold bpow; simpl. rewrite Rabs_R0. lra.
  - rewrite zero_v.
    pose proof round_0_zero. simpl in H. rewrite H.
    rewrite Rabs_R0.
    unfold bpow. lra.
Qed.

(* (fexp_correct 53 1024 eq_refl) as fexp_corr. *)
(* (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53) *)
476
(*                                     (-1022)%Z 53%Z) *)
Heiko Becker's avatar
Heiko Becker committed
477 478 479 480 481 482 483 484 485 486 487 488 489
Lemma eval_exp_gives_IEEE (e:exp fl64) :
  forall E1 E2 E2_real Gamma tMap vR A P fVars dVars,
    (forall x, (toREnv E2) x = E2_real x) ->
    typeCheck (B2Qexp e) Gamma tMap = true ->
    approxEnv E1 Gamma A fVars dVars E2_real ->
    validIntervalbounds (B2Qexp e) A P dVars = true ->
    validErrorbound (B2Qexp e) tMap A dVars = true ->
    FPRangeValidator (B2Qexp e) A tMap dVars = true ->
    eval_exp (toREnv E2) Gamma (toRExp (B2Qexp e)) vR M64 ->
    NatSet.Subset ((usedVars (B2Qexp e)) -- dVars) fVars ->
    is64BitEval (B2Qexp e) ->
    noDowncast (B2Qexp e) ->
    eval_exp_valid e E2 ->
Heiko Becker's avatar
Heiko Becker committed
490 491 492
    dVars_range_valid dVars E1 A ->
    fVars_P_sound fVars E1 P ->
    vars_typed (NatSet.union fVars dVars) Gamma ->
Heiko Becker's avatar
Heiko Becker committed
493 494 495
      (forall v,
        NatSet.In v dVars ->
        exists vF m,
Heiko Becker's avatar
Heiko Becker committed
496
        (E2_real v = Some vF /\ DaisyMap.find (Var Q v) tMap = Some m /\
Heiko Becker's avatar
Heiko Becker committed
497 498 499 500 501
        validFloatValue vF m)) ->
      (forall v, NatSet.In v (usedVars (B2Qexp e)) -> Gamma v = Some M64) ->
      exists v,
        eval_exp_float e E2 = Some v /\
        eval_exp (toREnv E2) Gamma (toRExp (B2Qexp e)) (Q2R (B2Q v)) M64.
502
Proof.
Heiko Becker's avatar
Heiko Becker committed
503 504 505 506 507 508 509
  induction e; simpl in *;
    intros * envs_eq typecheck_e approxEnv_E1_E2_real valid_rangebounds
                     valid_roundoffs valid_float_ranges eval_e_float
                     usedVars_sound is64BitEval_e noDowncast_e eval_IEEE_valid_e
                     fVars_defined vars_typed dVars_sound dVars_valid
                     usedVars_64bit;
    (match_pat (eval_exp _ _ _ _ _) (fun H => inversion H; subst; simpl in *));
Heiko Becker's avatar
Heiko Becker committed
510 511
     Daisy_compute_asm; try congruence; type_conv; subst;
     unfold Ltacs.optionLift.
Heiko Becker's avatar
Heiko Becker committed
512 513 514 515 516 517 518 519 520
  - unfold toREnv in *.
    destruct (E2 n) eqn:HE2; try congruence.
    exists f; split; try eauto.
    eapply Var_load; try auto. rewrite HE2; auto.
  - eexists; split; try eauto.
    eapply (Const_dist' (delta:=0%R)); eauto.
    + rewrite Rabs_R0; apply mTypeToQ_pos_R.
    + unfold perturb. lra.
  - edestruct IHe as [v_e [eval_float_e eval_rel_e]]; eauto.
Heiko Becker's avatar
Heiko Becker committed
521 522 523 524 525 526 527 528 529 530
    assert (is_finite 53 1024 v_e = true).
    { apply validValue_is_finite.
      eapply FPRangeValidator_sound; eauto.
      eapply eval_eq_env; eauto. }
    rewrite eval_float_e.
    exists (b64_opp v_e); split; try auto.
    unfold b64_opp. rewrite <- (is_finite_Bopp _ _ pair) in H.
    rewrite B2Q_B2R_eq; auto. rewrite B2R_Bopp.
    eapply Unop_neg'; eauto.
    unfold evalUnop. rewrite is_finite_Bopp in H. rewrite B2Q_B2R_eq; auto.
Heiko Becker's avatar
Heiko Becker committed
531 532 533
  - repeat (match goal with
            |H: _ /\ _ |- _ => destruct H
            end).
Heiko Becker's avatar
Heiko Becker committed
534 535 536
    assert (DaisyMap.find (B2Qexp e1) tMap = Some M64 /\
            DaisyMap.find (B2Qexp e2) tMap = Some M64 /\
            DaisyMap.find (Binop b (B2Qexp e1) (B2Qexp e2)) tMap = Some M64)
Heiko Becker's avatar
Heiko Becker committed
537 538 539 540
           as [tMap_e1 [tMap_e2 tMap_b]].
    { repeat split; apply (typing_exp_64_bit _ Gamma); simpl; auto.
      - intros; apply usedVars_64bit; set_tac.
      - intros; apply usedVars_64bit; set_tac.
Heiko Becker's avatar
Heiko Becker committed
541
      - rewrite Heqo, Heqo4, Heqo6.
Heiko Becker's avatar
Heiko Becker committed
542 543 544 545
        apply Is_true_eq_true; apply andb_prop_intro; split.
        + apply andb_prop_intro; split; apply Is_true_eq_left; auto.
          apply mTypeEq_refl.
        + apply Is_true_eq_left; auto. }
Heiko Becker's avatar
Heiko Becker committed
546
    repeat destr_factorize.
Heiko Becker's avatar
Heiko Becker committed
547 548 549 550 551 552 553 554 555 556 557 558 559 560
    assert (m1 = M64).
    { eapply (typing_agrees_exp (B2Qexp e1)); eauto. }
    assert (m2 = M64).
    { eapply typing_agrees_exp; eauto. }
    subst.
    destruct (IHe1 E1 E2 E2_real Gamma tMap v1 A P fVars dVars)
      as [v_e1 [eval_float_e1 eval_rel_e1]];
      try auto; try set_tac;
        [ intros; apply usedVars_64bit ; set_tac | ].
    destruct (IHe2 E1 E2 E2_real Gamma tMap v2 A P fVars dVars)
      as [v_e2 [eval_float_e2 eval_rel_e2]];
      try auto; try set_tac;
        [ intros; apply usedVars_64bit ; set_tac | ].
    rewrite eval_float_e1, eval_float_e2.
Heiko Becker's avatar
Heiko Becker committed
561 562 563 564 565
    edestruct (validIntervalbounds_sound (B2Qexp e2))
      as [iv_2 [err_2 [nR2 [map_e2 [eval_real_e2 e2_bounded_real]]]]];
      eauto; set_tac.
    destr_factorize.
    destruct iv_2 as [ivlo_2 ivhi_2].
Heiko Becker's avatar
Heiko Becker committed
566 567
    assert (forall vF2 m2,
               eval_exp E2_real Gamma (toRExp (B2Qexp e2)) vF2 m2 ->
Heiko Becker's avatar
Heiko Becker committed
568 569
               (Rabs (nR2 - vF2) <= Q2R err_2))%R.
    { eapply validErrorbound_sound; try eauto; try set_tac. }
Heiko Becker's avatar
Heiko Becker committed
570 571
    assert (contained (Q2R (B2Q v_e2))
                      (widenInterval
Heiko Becker's avatar
Heiko Becker committed
572
                         (Q2R ivlo_2, Q2R ivhi_2) (Q2R err_2))).
Heiko Becker's avatar
Heiko Becker committed
573 574 575 576 577 578
    { eapply distance_gives_iv.
      - simpl. eapply e2_bounded_real.
      - eapply H11. instantiate(1:=M64).
        eapply eval_eq_env; eauto. }
    assert (b = Div -> (Q2R (B2Q v_e2)) <> 0%R).
    { intros; subst; simpl in *.
Heiko Becker's avatar
Heiko Becker committed
579 580 581
      andb_to_prop R3.
      apply le_neq_bool_to_lt_prop in L3.
      destruct L3; hnf; intros.
Heiko Becker's avatar
Heiko Becker committed
582 583 584 585 586 587 588 589 590 591 592 593 594 595
      - rewrite H15 in *.
        apply Qlt_Rlt in H14.
        rewrite Q2R0_is_0, Q2R_plus in H14. lra.
      - rewrite H15 in *.
        apply Qlt_Rlt in H14.
        rewrite Q2R0_is_0, Q2R_minus in H14; lra. }
    assert (validFloatValue
              (evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2))) M64).
    { eapply (FPRangeValidator_sound (Binop b (B2Qexp e1) (B2Qexp e2)));
        try eauto; set_tac.
      - eapply eval_eq_env; eauto.
        eapply (Binop_dist' (delta:=0)); eauto.
        + rewrite Rabs_R0. apply mTypeToQ_pos_R.
        + unfold perturb; lra.
Heiko Becker's avatar
Heiko Becker committed
596
      - Daisy_compute.
Heiko Becker's avatar
Heiko Becker committed
597 598
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro); split; try auto using Is_true_eq_left.
Heiko Becker's avatar
Heiko Becker committed
599
      - Daisy_compute.
Heiko Becker's avatar
Heiko Becker committed
600 601 602
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro); split; try auto using Is_true_eq_left.
        apply andb_prop_intro; split; auto using Is_true_eq_left.
Heiko Becker's avatar
Heiko Becker committed
603
      - inversion Heqo1; subst. rewrite Heqo0. rewrite Heqo.
Heiko Becker's avatar
Heiko Becker committed
604 605
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left.
Heiko Becker's avatar
Heiko Becker committed
606 607 608
        rewrite Heqo3, Heqo5.
        apply Is_true_eq_left. inversion Heqo2; subst. auto.
      - rewrite Heqo, Heqo0.
Heiko Becker's avatar
Heiko Becker committed
609
        apply Is_true_eq_true.
Heiko Becker's avatar
Heiko Becker committed
610
        inversion Heqo1; inversion Heqo2; subst.
Heiko Becker's avatar
Heiko Becker committed
611
        repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left. }
Heiko Becker's avatar
Heiko Becker committed
612
    (** MARKER **)
Heiko Becker's avatar
Heiko Becker committed
613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642
    assert (validFloatValue (Q2R (B2Q v_e1)) M64).
    { eapply (FPRangeValidator_sound (B2Qexp e1)); try eauto; try set_tac.
      eapply eval_eq_env; eauto. }
    assert (validFloatValue (Q2R (B2Q v_e2)) M64).
    { eapply (FPRangeValidator_sound (B2Qexp e2)); try eauto; try set_tac.
      - eapply eval_eq_env; eauto. }
    assert (is_finite 53 1024 v_e1 = true) as finite_e1.
    { apply validValue_is_finite; simpl; auto. }
    assert (is_finite 53 1024 v_e2 = true) as finite_e2.
    { apply validValue_is_finite; simpl; auto. }
    assert (forall eps,
               (Rabs eps <= / 2 * bpow radix2 (- 53 + 1))%R ->
               validFloatValue
                 (evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2) * (1 + eps)) M64).
    { intros.
      eapply FPRangeValidator_sound with (e:=Binop b (B2Qexp e1) (B2Qexp e2)); eauto.
      - eapply eval_eq_env; eauto.
        eapply Binop_dist' with (delta:=eps); eauto.
        simpl in H2. Transparent mTypeToQ. unfold mTypeToQ.
        eapply Rle_trans; eauto.  unfold Qpower. unfold Qpower_positive.
        assert (pow_pos Qmult (2#1) 53 = 9007199254740992 # 1 )
          by (vm_compute; auto).
        rewrite H19. rewrite Q2R_inv; try lra.
        unfold Q2R, Qnum, Qden. unfold bpow.
        assert (-53 + 1 = -52)%Z by auto.
        rewrite H20.
        assert (Z.pow_pos radix2 52 = 4503599627370496%Z) by (vm_compute; auto).
        rewrite H21. unfold Z2R, P2R. lra.
        unfold perturb.
        repeat rewrite B2Q_B2R_eq; auto.
643
      - cbn. Daisy_compute.
Heiko Becker's avatar
Heiko Becker committed
644 645
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
646
      - cbn. Daisy_compute.
Heiko Becker's avatar
Heiko Becker committed
647 648
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
649 650
      - cbn. Daisy_compute.
        inversion Heqo1; inversion Heqo2; subst.
Heiko Becker's avatar
Heiko Becker committed
651 652
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
653 654
      - cbn. Daisy_compute.
        inversion Heqo1; inversion Heqo2; subst.
Heiko Becker's avatar
Heiko Becker committed
655 656 657 658
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left). }
    assert (b = Div -> (Q2R (B2Q v_e2)) <> 0%R) as no_div_zero_float.
    { intros; subst; simpl in *.
659 660 661
      andb_to_prop R3.
      apply le_neq_bool_to_lt_prop in L3.
      destruct L3 as [case_low | case_high]; hnf; intros.
Heiko Becker's avatar
Heiko Becker committed
662 663 664 665 666 667 668
      - rewrite H19 in *.
        apply Qlt_Rlt in case_low.
        rewrite Q2R0_is_0, Q2R_plus in case_low. lra.
      - rewrite H19 in *.
        apply Qlt_Rlt in case_high.
        rewrite Q2R0_is_0, Q2R_minus in case_high; lra. }
    clear H2 H12 dVars_sound dVars_valid usedVars_64bit vars_typed fVars_defined
669
    usedVars_sound R2 R1 L1 L R6 L0 R3 R4 L2 R5 R7 L5 Heqo Heqo0 Heqo1 IHe1
Heiko Becker's avatar
Heiko Becker committed
670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897
    IHe2.
    pose proof (fexp_correct 53 1024 eq_refl) as fexp_corr.
    assert (forall k : Z, (-1022 < k)%Z ->
                     (53 <= k - Fcore_FLT.FLT_exp (3 - 1024 - 53) 53 k)%Z)
      as exp_valid.
    { intros k k_pos.
      unfold Fcore_FLT.FLT_exp; simpl.
      destruct (Z.max_spec_le (k - 53) (-1074)); omega. }
    pose proof (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53)
                                    (-1022)%Z 53%Z exp_valid)
      as rel_error_exists.
    rewrite eval_float_e1, eval_float_e2 in H1.
    unfold optionLift, normal_or_zero in *; simpl in *.
    assert (Normal (evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2)) M64 \/
            (evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2)) = 0)%R.
    { revert H1; intros case_val. destruct case_val; try auto.
      left; unfold Normal, Denormal in H15; unfold Normal;
        destruct H15 as [normal_b | [denormal_b |zero_b]].
      - repeat rewrite <- B2Q_B2R_eq; try auto.
      - destruct denormal_b.
        assert ((Rabs (evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2)))) < (Rabs (evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2)))))%R.
        { eapply Rlt_le_trans; eauto.
          repeat rewrite B2Q_B2R_eq; auto. }
        lra.
      - rewrite B2Q_B2R_eq in zero_b; auto.
        rewrite B2Q_B2R_eq in zero_b; auto.
        rewrite zero_b in *.
        rewrite Rabs_R0 in H1.
        unfold minValue, minExponentPos in H1.
        rewrite Q2R_inv in H1; [|vm_compute; congruence].
        unfold Q2R, Qnum, Qden in H1.
        assert (Z.pow_pos 2 1022 = 44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304%Z)
          by (vm_compute; auto).
        rewrite H2 in H1. rewrite <- Z2R_IZR in H1.  unfold IZR in H1.
        simpl in H1. lra. }
    pose proof (validValue_bounded b v_e1 v_e2 H2 H18) as cond_valid.
    destruct b; revert H1; intros case_eval.

    (* Addition *)
    + unfold evalBinop in *. unfold b64_plus.
      pose proof (Bplus_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE
                                v_e1 v_e2 finite_e1 finite_e2)
        as addition_correct.
      rewrite cond_valid in addition_correct.
      destruct addition_correct as [add_round [finite_res _]].
      destruct case_eval as [eval_zero | eval_normal].
      (* resutl is zero *)
      * rewrite eval_zero in *.
        rewrite round_0_zero in *.
        exists (Bplus 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2).
        split; try auto.
        rewrite B2Q_B2R_eq; try auto.
        unfold dmode; rewrite add_round.
        eapply Binop_dist' with (delta:=0%R); eauto.
        rewrite Rabs_R0; apply mTypeToQ_pos_R.
        unfold perturb, evalBinop.
        repeat rewrite B2Q_B2R_eq; try auto; lra.
      * simpl in *.
        destruct (rel_error_exists
                    (fun x => negb (Zeven x))
                    (B2R 53 1024 v_e1 + B2R 53 1024 v_e2)%R)
          as [eps [eps_bounded round_eq]].
        { eapply Rle_trans; eauto. unfold minValue, minExponentPos.
          rewrite Q2R_inv; [ | vm_compute; congruence].
          unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
          vm_compute. lra. }
        { exists (Bplus 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2);
            split; try auto.
          rewrite B2Q_B2R_eq; try auto.
          unfold dmode.
          eapply Binop_dist' with (delta:=eps); eauto.
          - unfold mTypeToQ.
            assert (join M64 M64 = M64) by (vm_compute; auto).
            rewrite H1.
            eapply Rle_trans; eauto.
            unfold Qpower. unfold Qpower_positive.
            assert (pow_pos Qmult (2#1) 53 = 9007199254740992 # 1 )
              by (vm_compute; auto).
            rewrite H12. rewrite Q2R_inv; try lra.
            unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
            simpl; lra.
          - unfold perturb, evalBinop.
            repeat rewrite B2Q_B2R_eq; try auto.
            rewrite <- round_eq. rewrite <- add_round; auto. }
    (* Subtraction *)
    + unfold evalBinop in *. unfold b64_minus.
      pose proof (Bminus_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE
                                v_e1 v_e2 finite_e1 finite_e2)
        as subtraction_correct.
      rewrite cond_valid in subtraction_correct.
      destruct subtraction_correct as [add_round [finite_res _]].
      destruct case_eval as [eval_zero | eval_normal].
      (* resutl is zero *)
      * rewrite eval_zero in *.
        rewrite round_0_zero in *.
        exists (Bminus 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2).
        split; try auto.
        rewrite B2Q_B2R_eq; try auto.
        unfold dmode; rewrite add_round.
        eapply Binop_dist' with (delta:=0%R); eauto.
        rewrite Rabs_R0; apply mTypeToQ_pos_R.
        unfold perturb, evalBinop.
        repeat rewrite B2Q_B2R_eq; try auto; lra.
      * simpl in *.
        destruct (rel_error_exists
                    (fun x => negb (Zeven x))
                    (B2R 53 1024 v_e1 - B2R 53 1024 v_e2)%R)
          as [eps [eps_bounded round_eq]].
        { eapply Rle_trans; eauto. unfold minValue, minExponentPos.
          rewrite Q2R_inv; [ | vm_compute; congruence].
          unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
          vm_compute. lra. }
        { exists (Bminus 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2);
            split; try auto.
          rewrite B2Q_B2R_eq; try auto.
          unfold dmode.
          eapply Binop_dist' with (delta:=eps); eauto.
          - unfold mTypeToQ.
            assert (join M64 M64 = M64) by (vm_compute; auto).
            rewrite H1.
            eapply Rle_trans; eauto.
            unfold Qpower. unfold Qpower_positive.
            assert (pow_pos Qmult (2#1) 53 = 9007199254740992 # 1 )
              by (vm_compute; auto).
            rewrite H12. rewrite Q2R_inv; try lra.
            unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
            simpl; lra.
          - unfold perturb, evalBinop.
            repeat rewrite B2Q_B2R_eq; try auto.
            rewrite <- round_eq. rewrite <- add_round; auto. }
    (* Multiplication *)
    + unfold evalBinop in *. unfold b64_mult.
      pose proof (Bmult_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE
                                v_e1 v_e2)
        as mult_correct.
      rewrite cond_valid in mult_correct.
      destruct mult_correct as [mult_round [finite_res _]].
      destruct case_eval as [eval_zero | eval_normal].
      (* resutl is zero *)
      * rewrite eval_zero in *.
        rewrite round_0_zero in *.
        exists (Bmult 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2).
        split; try auto.
        rewrite B2Q_B2R_eq; try auto.
        unfold dmode; rewrite mult_round.
        eapply Binop_dist' with (delta:=0%R); eauto.
        rewrite Rabs_R0; apply mTypeToQ_pos_R.
        unfold perturb, evalBinop.
        repeat rewrite B2Q_B2R_eq; try auto; lra.
        rewrite finite_e1, finite_e2 in finite_res.
        auto.
      * simpl in *.
        destruct (rel_error_exists
                    (fun x => negb (Zeven x))
                    (B2R 53 1024 v_e1 * B2R 53 1024 v_e2)%R)
          as [eps [eps_bounded round_eq]].
        { eapply Rle_trans; eauto. unfold minValue, minExponentPos.
          rewrite Q2R_inv; [ | vm_compute; congruence].
          unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
          vm_compute. lra. }
        { exists (Bmult 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2);
            split; try auto.
          rewrite B2Q_B2R_eq; try auto.
          unfold dmode.
          eapply Binop_dist' with (delta:=eps); eauto.
          - unfold mTypeToQ.
            assert (join M64 M64 = M64) by (vm_compute; auto).
            rewrite H1.
            eapply Rle_trans; eauto.
            unfold Qpower. unfold Qpower_positive.
            assert (pow_pos Qmult (2#1) 53 = 9007199254740992 # 1 )
              by (vm_compute; auto).
            rewrite H12. rewrite Q2R_inv; try lra.
            unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
            simpl; lra.
          - unfold perturb, evalBinop.
            repeat rewrite B2Q_B2R_eq; try auto.
            rewrite <- round_eq. rewrite <- mult_round; auto.
          - rewrite finite_e1, finite_e2 in finite_res; auto. }
    (* Division *)
    + unfold evalBinop in *. unfold b64_div.
      pose proof (Bdiv_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE
                                v_e1 v_e2)
        as division_correct.
      rewrite cond_valid in division_correct.
      destruct division_correct as [div_round [finite_res _]].
      rewrite <- B2Q_B2R_eq; auto.
      destruct case_eval as [eval_zero | eval_normal].
      (* resutl is zero *)
      * rewrite eval_zero in *.
        rewrite round_0_zero in *.
        exists (Bdiv 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2).
        split; try auto.
        rewrite B2Q_B2R_eq; try auto.
        unfold dmode; rewrite div_round.
        eapply Binop_dist' with (delta:=0%R); eauto.
        rewrite Rabs_R0; apply mTypeToQ_pos_R.
        unfold perturb, evalBinop.
        repeat rewrite B2Q_B2R_eq; try auto; lra.
        rewrite finite_e1 in finite_res; auto.
      * simpl in *.
        destruct (rel_error_exists
                    (fun x => negb (Zeven x))
                    (B2R 53 1024 v_e1 / B2R 53 1024 v_e2)%R)
          as [eps [eps_bounded round_eq]].
        { eapply Rle_trans; eauto. unfold minValue, minExponentPos.
          rewrite Q2R_inv; [ | vm_compute; congruence].
          unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
          vm_compute. lra. }
        { exists (Bdiv 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2);
            split; try auto.
          rewrite B2Q_B2R_eq; try auto.
          unfold dmode.
          eapply Binop_dist' with (delta:=eps); eauto.
          - unfold mTypeToQ.
            assert (join M64 M64 = M64) by (vm_compute; auto).
            rewrite H1.
            eapply Rle_trans; eauto.
            unfold Qpower. unfold Qpower_positive.
            assert (pow_pos Qmult (2#1) 53 = 9007199254740992 # 1 )
              by (vm_compute; auto).
            rewrite H12. rewrite Q2R_inv; try lra.
            unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
            simpl; lra.
          - unfold perturb, evalBinop.
            repeat rewrite B2Q_B2R_eq; try auto.
            rewrite <- round_eq. rewrite <- div_round; auto.
          - rewrite finite_e1 in finite_res; auto. }
Nikita Zyuzin's avatar
Nikita Zyuzin committed
898 899 900
  - repeat (match goal with
            |H: _ /\ _ |- _ => destruct H
            end).
901 902 903 904
    assert (DaisyMap.find (B2Qexp e1) tMap = Some M64 /\
            DaisyMap.find (B2Qexp e2) tMap = Some M64 /\
            DaisyMap.find (B2Qexp e3) tMap = Some M64 /\
            DaisyMap.find (Fma (B2Qexp e1) (B2Qexp e2) (B2Qexp e3)) tMap = Some M64)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
905 906 907 908 909
           as [tMap_e1 [tMap_e2 [tMap_e3 tMap_fma]]].
    { repeat split; apply (typing_exp_64_bit _ Gamma); simpl; auto.
      - intros; apply usedVars_64bit; set_tac.
      - intros; apply usedVars_64bit; set_tac.
      - intros; apply usedVars_64bit; set_tac.
910
      - rewrite Heqo, Heqo4, Heqo6, Heqo8.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
911 912 913 914 915 916 917 918
        apply Is_true_eq_true; apply andb_prop_intro; split.
        + apply andb_prop_intro; split.
          * apply andb_prop_intro; split.
            ++ apply Is_true_eq_left; auto.
               apply mTypeEq_refl.
            ++ apply Is_true_eq_left; auto.
          * apply Is_true_eq_left; auto.
        + apply Is_true_eq_left; auto. }
919
    repeat destr_factorize.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935
    inversion Heqo; inversion Heqo0; inversion Heqo1; inversion Heqo2; subst.
    assert (m1 = M64).
    { eapply (typing_agrees_exp (B2Qexp e1)); eauto. }
    assert (m2 = M64).
    { eapply (typing_agrees_exp (B2Qexp e2)); eauto. }
    assert (m3 = M64).
    { eapply (typing_agrees_exp (B2Qexp e3)); eauto. }
    subst.
    destruct (IHe1 E1 E2 E2_real Gamma tMap v1 A P fVars dVars)
      as [v_e1 [eval_float_e1 eval_rel_e1]];
      try auto; try set_tac;
        [ intros; apply usedVars_64bit ; set_tac | ].
    destruct (IHe2 E1 E2 E2_real Gamma tMap v2 A P fVars dVars)
      as [v_e2 [eval_float_e2 eval_rel_e2]];
      try auto; try set_tac;
        [ intros; apply usedVars_64bit ; set_tac | ].
936 937 938 939 940 941 942 943
    destruct (IHe3 E1 E2 E2_real Gamma tMap v3 A P fVars dVars)
      as [v_e3 [eval_float_e3 eval_rel_e3]];
      try auto; try set_tac;
        [ intros; apply usedVars_64bit ; set_tac | ].
    unfold optionLift in H4.
    rewrite eval_float_e1, eval_float_e2, eval_float_e3 in H4.
    contradiction H4.
  - inversion noDowncast_e.
Heiko Becker's avatar
Heiko Becker committed
944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960
Qed.

Lemma bstep_gives_IEEE (f:cmd fl64) :
  forall E1 E2 E2_real Gamma tMap vR vF A P fVars dVars outVars,
    (forall x, (toREnv E2) x = E2_real x) ->
    approxEnv E1 Gamma A fVars dVars E2_real ->
    ssa (B2Qcmd f) (NatSet.union fVars dVars) outVars ->
    typeCheckCmd (B2Qcmd f) Gamma tMap = true ->
    validIntervalboundsCmd (B2Qcmd f) A P dVars = true ->
    validErrorboundCmd (B2Qcmd f) tMap A dVars = true ->
    FPRangeValidatorCmd (B2Qcmd f) A tMap dVars = true ->
    bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRMap Gamma) vR M0 ->
    bstep (toRCmd (B2Qcmd f)) (toREnv E2) Gamma vF M64 ->
    NatSet.Subset (NatSet.diff (freeVars (B2Qcmd f)) dVars) fVars ->
    is64BitBstep (B2Qcmd f) ->
    noDowncastFun (B2Qcmd f) ->
    bstep_valid f E2 ->
961 962 963
    dVars_range_valid dVars E1 A ->
    fVars_P_sound fVars E1 P ->
    vars_typed (NatSet.union fVars dVars) Gamma ->
Heiko Becker's avatar
Heiko Becker committed
964 965 966
      (forall v,
        NatSet.In v dVars ->
        exists vF m,
967
        (E2_real v = Some vF /\ DaisyMap.find (Var Q v) tMap= Some m /\
Heiko Becker's avatar
Heiko Becker committed
968 969 970 971 972 973 974 975 976 977
        validFloatValue vF m)) ->
      (forall v, NatSet.In v (freeVars (B2Qcmd f)) -> Gamma v = Some M64) ->
      exists v,
        bstep_float f E2 = Some v /\
        bstep (toRCmd (B2Qcmd f)) (toREnv E2) Gamma (Q2R (B2Q v)) M64.
Proof.
  induction f;
    intros * envs_eq approxEnv_E1_E2_real ssa_f typeCheck_f valid_ranges_f
                     valid_roundoffs_f valid_float_ranges bstep_real bstep_float
                     freeVars_sound is64_eval nodowncast_f bstep_sound
978
                     dVars_sound fVars_defined vars_typed dVars_valid
Heiko Becker's avatar
Heiko Becker committed
979
                     freeVars_typed;
980 981 982
    cbn in *; Daisy_compute_asm; try congruence; type_conv; subst;
      unfold Ltacs.optionLift;
      inversion bstep_float; inversion bstep_real;
Heiko Becker's avatar
Heiko Becker committed
983 984 985 986
      inversion ssa_f; subst; simpl in *;
        repeat (match goal with
                | H: _ = true |- _ => andb_to_prop H
                end).
987
  - assert (DaisyMap.find (B2Qexp e) tMap= Some M64).
Heiko Becker's avatar
Heiko Becker committed
988 989 990 991
    { eapply typing_exp_64_bit; try eauto.
      simpl in *; destruct nodowncast_f; auto.
      destruct is64_eval; auto.
      intros; apply freeVars_typed.
992
      set_tac.
Heiko Becker's avatar
Heiko Becker committed
993 994 995 996
      split; [ set_tac | ].
      hnf; intros; subst.
      apply H26.
      apply (H25 n H).  }
997
    assert (m1 = M64).
Heiko Becker's avatar
Heiko Becker committed
998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014
    { eapply typing_agrees_exp; eauto. }
    subst.
    assert (exists v_e, eval_exp_float e E2 = Some v_e /\
                   eval_exp (toREnv E2) Gamma (toRExp (B2Qexp e)) (Q2R (B2Q v_e)) M64)
           as eval_float_e.
    { eapply eval_exp_gives_IEEE; try eauto.
      - hnf; intros. rewrite NatSet.diff_spec in H0.
        destruct H0.
        specialize (H25 a H0). rewrite NatSet.union_spec in H25.
        destruct H25; try congruence; auto.
      - destruct is64_eval; auto.
      - destruct nodowncast_f; auto.
      - destruct bstep_sound; auto.
      - intros. apply freeVars_typed.
        rewrite NatSet.remove_spec, NatSet.union_spec.
        split; try auto.
        hnf; intros; subst.
1015 1016
        specialize (H25 n H0).
        set_tac.  apply H26; set_tac. }
Heiko Becker's avatar
Heiko Becker committed
1017 1018
    destruct eval_float_e as [v_e [eval_float_e eval_rel_e]].
    assert (forall v m, eval_exp E2_real Gamma (toRExp (B2Qexp e)) v m ->
1019
                   Rabs (v0 - v) <= Q2R e2)%R
Heiko Becker's avatar
Heiko Becker committed
1020 1021 1022 1023
      as err_e_valid.
    { eapply validErrorbound_sound; try eauto.
      - hnf; intros. rewrite NatSet.diff_spec in H0.
        destruct H0. specialize (H25 a H0). rewrite NatSet.union_spec in H25.
1024 1025
        destruct H25; try auto; congruence. }
    assert (Rabs (v0 - (Q2R (B2Q v_e))) <= Q2R e2)%R.
Heiko Becker's avatar
Heiko Becker committed
1026 1027 1028
    { eapply err_e_valid. eapply eval_eq_env; eauto. }
    (* Now construct a new evaluation according to our big-step semantics
       using lemma validErrorboundCmd_gives_eval *)
1029 1030
    (* destruct (A (getRetExp (B2Qcmd f))) as [iv_f err_f] eqn:A_f. *)
    (* destruct iv_f as [ivlo_f ivhi_f]. *)
Heiko Becker's avatar
Heiko Becker committed
1031 1032 1033 1034 1035 1036
    edestruct (validIntervalboundsCmd_sound) as [iv_ret [err_ret [v_ret
                                                                    [map_ret
                                                                       [eval_ret bound_ret]]]]];
      eauto.
    { cbn. Daisy_compute.
      rewrite L0, R4, R3, R2. auto. }
Heiko Becker's avatar
Heiko Becker committed
1037
    assert (exists vF m, bstep (toRCmd (B2Qcmd f)) (updEnv n (Q2R (B2Q v_e)) E2_real) (updDefVars n M64 Gamma) vF m).
Heiko Becker's avatar
Heiko Becker committed
1038 1039 1040 1041
    { eapply validErrorboundCmd_gives_eval with (E1 := updEnv n v0 E1)
                                                  (elo:=fst(iv_ret))
                                                  (ehi:=snd(iv_ret))
                                                  (err:= err_ret); eauto.
Heiko Becker's avatar
Heiko Becker committed
1042 1043 1044
      - eapply approxUpdBound; eauto.
        rewrite Qeq_bool_iff in R1.
        eapply Rle_trans; eauto.
1045 1046
        canonize_hyps. rewrite <- R1.
        inversion Heqo0; subst; lra.
Heiko Becker's avatar
Heiko Becker committed
1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064
      - eapply ssa_equal_set; eauto.
        hnf; split; intros.
        + rewrite NatSet.add_spec, NatSet.union_spec in *.
          rewrite NatSet.add_spec in H1; destruct H1; auto.
          destruct H1; auto.
        + rewrite NatSet.add_spec in H1;
            rewrite NatSet.union_spec, NatSet.add_spec in *;
            destruct H1; auto. destruct H1; auto.
      - hnf; intros. rewrite NatSet.diff_spec in H1.
        destruct H1. apply freeVars_sound.
        rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
        split; try auto. split; try auto.
        hnf; intros; subst. apply H2. rewrite NatSet.add_spec. auto.
        rewrite NatSet.add_spec in H2. hnf; intros; apply H2; auto.
      - eapply (swap_Gamma_bstep (Gamma1:= updDefVars n M0 (toRMap Gamma)));
          eauto.
        intros; unfold updDefVars, toRMap.
        destruct (n0 =? n); auto.
1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079
      - unfold dVars_range_valid in *. intros. unfold updEnv. set_tac.
        destruct H1; subst.
        + exists v0, (q1, q2), e1; split; try eauto.
          * rewrite Nat.eqb_refl; auto.
          * split; try auto.
            edestruct validIntervalbounds_sound
              as [iv_e [err_e [v_e' [map_e [? ?]]]]]; eauto.
            { set_tac; split; try auto. split; try auto.
              hnf; intros. eapply H26. subst; set_tac. }
            simpl. destr_factorize; simpl in *.
            canonize_hyps. rewrite <- R4, <- R3.
            rewrite <- (meps_0_deterministic _ H17 H1) in H2; auto.
        + destruct H1.
          rewrite <- Nat.eqb_neq in H1.
          rewrite H1.
Heiko Becker's avatar
Heiko Becker committed
1080
          apply dVars_sound; auto.
Heiko Becker's avatar
Heiko Becker committed
1081
      - unfold fVars_P_sound; intros; unfold updEnv.
Heiko Becker's avatar
Heiko Becker committed
1082 1083 1084
        destruct (v1 =? n) eqn:?.
        + rewrite Nat.eqb_eq in Heqb; subst; exfalso.
          set_tac. apply H26; rewrite NatSet.union_spec; auto.
Heiko Becker's avatar
Heiko Becker committed
1085 1086 1087
        + apply fVars_defined; auto.
      - unfold IntervalValidation.vars_typed. intros.
        unfold updDefVars. destruct (v1 =? n) eqn:?.
Heiko Becker's avatar
Heiko Becker committed
1088 1089 1090 1091
        + exists M64; auto.
        + apply vars_typed.
          rewrite Nat.eqb_neq in Heqb.
          rewrite NatSet.union_spec, NatSet.add_spec in H1.
Heiko Becker's avatar
Heiko Becker committed
1092 1093 1094 1095
          rewrite NatSet.union_spec.
          destruct H1 as [HA |[HB | HC]]; try auto; congruence.
      - destruct iv_ret; auto.
    }
Heiko Becker's avatar
Heiko Becker committed
1096
    unfold optionLift. rewrite eval_float_e.
Heiko Becker's avatar
Heiko Becker committed
1097 1098
    assert (DaisyMap.find (getRetExp (B2Qcmd f)) tMap= Some M64).
    { eapply typingSoundnessCmd; eauto. }
Heiko Becker's avatar
Heiko Becker committed
1099 1100
    destruct H1 as [vF_new [m_f bstep_float_new]].
    assert (m_f = M64).
Heiko Becker's avatar
Heiko Becker committed
1101
    { eapply typing_agrees_cmd; eauto. }
Heiko Becker's avatar
Heiko Becker committed
1102 1103 1104 1105 1106 1107
    subst.
    destruct (IHf (updEnv n v0 E1) (updFlEnv n v_e E2)
                  (updEnv n (Q2R (B2Q v_e)) E2_real) (updDefVars n M64 Gamma) tMap
                  vR vF_new A P fVars (NatSet.add n dVars) outVars); try eauto.
    + intros. unfold toREnv, updFlEnv, updEnv.
      destruct (x =? n); auto. rewrite <- envs_eq. unfold toREnv; auto.
Heiko Becker's avatar
Heiko Becker committed
1108
    + eapply approxUpdBound; eauto.
Heiko Becker's avatar
Heiko Becker committed
1109
      eapply Rle_trans; eauto.
Heiko Becker's avatar
Heiko Becker committed
1110 1111 1112
      canonize_hyps.
      inversion Heqo0; subst.
      lra.
Heiko Becker's avatar
Heiko Becker committed
1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139
    + eapply ssa_equal_set; eauto.
      hnf; split; intros.
      * rewrite NatSet.add_spec, NatSet.union_spec in *.
        rewrite NatSet.add_spec in H1; destruct H1; auto.
        destruct H1; auto.
      * rewrite NatSet.add_spec in H1;
          rewrite NatSet.union_spec, NatSet.add_spec in *;
          destruct H1; auto. destruct H1; auto.
    + eapply (swap_Gamma_bstep (Gamma1:= updDefVars n M0 (toRMap Gamma)));
        eauto.
      intros; unfold updDefVars, toRMap.
      destruct (n0 =? n); auto.
    + eapply (bstep_eq_env (E1 := updEnv n (Q2R (B2Q v_e)) E2_real)); eauto.
      intros x; unfold updEnv, updFlEnv, toREnv.
      destruct (x =? n); try auto.
      rewrite <- envs_eq. auto.
    + hnf; intros. rewrite NatSet.diff_spec in *.
      destruct H1. apply freeVars_sound.
      rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
      split; try auto. split; try auto.
      hnf; intros; subst. apply H3. rewrite NatSet.add_spec. auto.
      rewrite NatSet.add_spec in H3. hnf; intros; apply H3; auto.
    + destruct is64_eval as [HA [HB HC]]; auto.
    + destruct nodowncast_f as [HA HB]; auto.
    + destruct bstep_sound as [eval_sound bstep_sound].
      rewrite eval_float_e in bstep_sound; unfold optionLift in bstep_sound.
      auto.
Heiko Becker's avatar
Heiko Becker committed
1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157
    + unfold dVars_range_valid in *; intros; unfold updEnv.
      destruct (v1 =? n) eqn:?.
      * set_tac. rewrite Nat.eqb_eq in Heqb; subst.
        destruct H1 as [? | [? ?]]; try congruence.
        exists v0. edestruct validIntervalbounds_sound as [iv_e [err_e [? [? [? ?]]]]]; eauto.
        { set_tac; split; auto. split; auto.
          hnf; intros; subst; set_tac. }
        canonize_hyps.
        destr_factorize; simpl in *.
        exists (q1,q2), e1.
        split; try auto.
        split; try auto.
        simpl in *. rewrite R4, R3 in *.
        rewrite <- (meps_0_deterministic _ H4 H17). auto.
      * eapply dVars_sound; set_tac.
        destruct H1; rewrite Nat.eqb_neq in Heqb; try congruence.
        destruct H1; auto.
    + unfold fVars_P_sound. intros; unfold updEnv.
Heiko Becker's avatar
Heiko Becker committed
1158 1159 1160 1161
      destruct (v1 =? n) eqn:?.
      * rewrite Nat.eqb_eq in Heqb; subst; exfalso.
        set_tac. apply H26; rewrite NatSet.union_spec; auto.
      * apply fVars_defined. auto.
Heiko Becker's avatar
Heiko Becker committed
1162 1163
    + unfold IntervalValidation.vars_typed.
      intros. unfold updDefVars. destruct (v1 =? n) eqn:?.
Heiko Becker's avatar
Heiko Becker committed
1164 1165 1166
      * exists M64; auto.
      * apply vars_typed.
        rewrite Nat.eqb_neq in Heqb.
Heiko Becker's avatar
Heiko Becker committed
1167 1168 1169
        rewrite NatSet.union_spec, NatSet.add_spec in H1.
        rewrite NatSet.union_spec.
        destruct H1 as [HA |[HB | HC]]; try auto; congruence.
Heiko Becker's avatar
Heiko Becker committed
1170 1171
    + intros. rewrite NatSet.add_spec in H1; unfold updEnv.
      destruct (v1 =? n) eqn:?; destruct H1; subst; try congruence.
Heiko Becker's avatar
Heiko Becker committed
1172 1173
      * exists (Q2R (B2Q v_e)).
        exists M64; repeat split; try auto.
Heiko Becker's avatar
Heiko Becker committed
1174
        eapply FPRangeValidator_sound; eauto.
Heiko Becker's avatar
Heiko Becker committed
1175
        { eapply eval_eq_env; eauto. }
Heiko Becker's avatar
Heiko Becker committed
1176 1177
        { set_tac. split; try auto.
          split; try auto.
Heiko Becker's avatar
Heiko Becker committed
1178
          hnf; intros; subst. set_tac. }
Heiko Becker's avatar
Heiko Becker committed
1179 1180 1181 1182 1183 1184 1185
      * rewrite Nat.eqb_eq in Heqb; subst.
        exists (Q2R (B2Q v_e)); rewrite H in *.
        exists M64; repeat split; try auto.
        eapply FPRangeValidator_sound; eauto.
        { eapply eval_eq_env; eauto. }
        { set_tac. split; try auto.
          split; try auto.
Heiko Becker's avatar
Heiko Becker committed
1186
          hnf; intros; subst. set_tac. }
Heiko Becker's avatar
Heiko Becker committed
1187 1188 1189 1190 1191
      * rewrite Nat.eqb_neq in Heqb; congruence.
      * apply dVars_valid; auto.
    + intros. unfold updDefVars.
      destruct (v1 =? n) eqn:?; try auto.
      apply freeVars_typed; set_tac.
Heiko Becker's avatar
Heiko Becker committed
1192
      split; try auto.
Heiko Becker's avatar
Heiko Becker committed
1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221
      hnf; intros; subst; rewrite Nat.eqb_neq in Heqb; congruence.
    + exists x; destruct H1;
        split; try auto.
      eapply let_b; eauto.
      eapply bstep_eq_env with (E1:= toREnv (updFlEnv n v_e E2)); eauto.
      intros; unfold toREnv, updFlEnv, updEnv.
      destruct (x0 =? n); auto.
  - edestruct (eval_exp_gives_IEEE); eauto.
    exists x; destruct H.
    split; try auto. apply ret_b; auto.
Qed.

Theorem IEEE_connection_exp e A P E1 E2 defVars:
  approxEnv E1 defVars A (usedVars (B2Qexp e)) (NatSet.empty) (toREnv E2) ->
  is64BitEval (B2Qexp e) ->
  noDowncast (B2Qexp e) ->
  eval_exp_valid e E2 ->
  (forall v,
      NatSet.In v (usedVars (B2Qexp e)) ->
      defVars v = Some M64) ->
  (forall v,
      NatSet.In v (usedVars (B2Qexp e)) ->
      exists vR,
        (E1 v = Some vR) /\
        Q2R (fst (P v)) <= vR <= Q2R(snd (P v)))%R ->
  (forall v,
      NatSet.In v (usedVars (B2Qexp e)) ->
      exists m, defVars v = Some m) ->
  CertificateChecker (B2Qexp e) A P defVars = true ->
Heiko Becker's avatar
Heiko Becker committed
1222 1223
  exists iv err vR vF, (* m, currently = M64 *)
    DaisyMap.find (B2Qexp e) A = Some (iv, err) /\
Heiko Becker's avatar
Heiko Becker committed
1224 1225 1226
    eval_exp E1 (toRMap defVars) (toREval (toRExp (B2Qexp e))) vR M0 /\
    eval_exp_float e E2 = Some vF /\
    eval_exp (toREnv E2) defVars (toRExp (B2Qexp e)) (Q2R (B2Q vF)) M64 /\
Heiko Becker's avatar
Heiko Becker committed
1227
    (Rabs (vR - Q2R (B2Q vF )) <= Q2R err)%R.
Heiko Becker's avatar
Heiko Becker committed
1228 1229 1230
Proof.
  intros.
  edestruct Certificate_checking_is_sound; eauto.
Heiko Becker's avatar
Heiko Becker committed
1231 1232 1233 1234
  destruct H7 as [err [vR [vF [mF [map_e [eval_real [eval_float roundoff_sound]]]]]]].
  unfold CertificateChecker in H6.
  andb_to_prop H6.
  assert (DaisyMap.find (B2Qexp e) (typeMap defVars (B2Qexp e) (DaisyMap.empty mType))  = Some M64).
Heiko Becker's avatar
Heiko Becker committed
1235 1236 1237 1238 1239 1240
    { eapply typing_exp_64_bit; eauto. }
    assert (mF = M64).
    { eapply typing_agrees_exp; eauto. }
    subst.
    edestruct eval_exp_gives_IEEE; eauto.
    + set_tac.
Heiko Becker's avatar
Heiko Becker committed
1241 1242 1243 1244
    + unfold dVars_range_valid. intros. inversion H7.
    + unfold vars_typed. intros.
      apply H5.
      set_tac. destruct H7; try auto.
Heiko Becker's avatar
Heiko Becker committed
1245 1246 1247
      inversion H7.
    + intros. inversion H7.
    + destruct H7 as [eval_float_f eval_rel].
Heiko Becker's avatar
Heiko Becker committed
1248 1249
      exists x, err, vR, x0.
      repeat split; try auto.
Heiko Becker's avatar
Heiko Becker committed
1250 1251 1252
      eapply roundoff_sound; eauto.
Qed.

Heiko Becker's avatar
Heiko Becker committed
1253
Theorem IEEE_connection_cmd (f:cmd fl64) (A:analysisResult) P
Heiko Becker's avatar
Heiko Becker committed
1254
        defVars E1 E2:
Heiko Becker's avatar
Heiko Becker committed
1255
    approxEnv E1 defVars A (freeVars (B2Qcmd f)) NatSet.empty (toREnv E2) ->
Heiko Becker's avatar
Heiko Becker committed
1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266
    is64BitBstep (B2Qcmd f) ->
    noDowncastFun (B2Qcmd f) ->
    bstep_valid f E2 ->
    (forall v, NatSet.In v (freeVars (B2Qcmd f)) ->
          defVars v = Some M64) ->
    (forall v, NatSet.mem v (freeVars (B2Qcmd f))= true ->
          exists vR, E1 v = Some vR /\
                (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
    (forall v, (v) mem (freeVars (B2Qcmd f)) = true ->
          exists m : mType,
            defVars v = Some m) ->
Heiko Becker's avatar
Heiko Becker committed
1267 1268 1269
    CertificateCheckerCmd (B2Qcmd f) A P defVars = true ->
    exists iv err vR vF m,
      DaisyMap.find (getRetExp (B2Qcmd f)) A = Some (iv,err) /\
Heiko Becker's avatar
Heiko Becker committed
1270 1271 1272 1273 1274
    bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRMap defVars) vR M0 /\
    bstep_float f E2 = Some vF /\
    bstep (toRCmd (B2Qcmd f)) (toREnv E2) defVars (Q2R (B2Q vF)) m /\
    (forall vF m,
        bstep (toRCmd (B2Qcmd f)) (toREnv E2) defVars vF m ->
Heiko Becker's avatar
Heiko Becker committed
1275
        (Rabs (vR - vF) <= Q2R err)%R).
Heiko Becker's avatar
Heiko Becker committed
1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286
(**
   The proofs is a simple composition of the soundness proofs for the range
   validator and the error bound validator.
**)
Proof.
  intros.
  unfold CertificateCheckerCmd in *.
  andb_to_prop H6.
  pose proof (validSSA_sound _ _ R0).
  destruct H6 as [outVars ssa_f].
  edestruct Certificate_checking_cmds_is_sound; eauto.
Heiko Becker's avatar
Heiko Becker committed
1287 1288
  - intros.
    apply H4. set_tac.
Heiko Becker's avatar
Heiko Becker committed
1289 1290 1291
  - unfold CertificateCheckerCmd.
    apply Is_true_eq_true.
    repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
Heiko Becker's avatar
Heiko Becker committed
1292 1293
  - destruct H6 as [err [vR [vF [m [map_ret [bstep_real [bstep_float roundoff_sound]]]]]]].
    assert (DaisyMap.find (getRetExp (B2Qcmd f)) (typeMapCmd defVars (B2Qcmd f) (DaisyMap.empty mType)) = Some M64).
Heiko Becker's avatar
Heiko Becker committed
1294 1295 1296 1297 1298 1299 1300
    { eapply typing_cmd_64_bit; eauto.  }
    assert (m = M64).
    { eapply typing_agrees_cmd; eauto. }
    subst.
    edestruct bstep_gives_IEEE; eauto.
    + eapply ssa_equal_set; eauto.
      hnf; intros; split; intros; set_tac.
Heiko Becker's avatar
Heiko Becker committed
1301
      destruct H7; try auto.
Heiko Becker's avatar
Heiko Becker committed
1302 1303
      inversion H7.
    + set_tac.
Heiko Becker's avatar
Heiko Becker committed
1304 1305 1306 1307 1308
    + unfold dVars_range_valid. intros.
      inversion H7.
    + unfold fVars_P_sound; intros.
      apply H4; rewrite NatSet.mem_spec; auto.
    + unfold vars_typed. intros. apply H5. set_tac. destruct H7; try auto.
Heiko Becker's avatar
Heiko Becker committed
1309 1310
      inversion H7.
    + intros. inversion H7.
Heiko Becker's avatar
Heiko Becker committed
1311 1312
    + destruct H7.
      exists x, err, vR, x0, M64.
Heiko Becker's avatar
Heiko Becker committed
1313
      repeat split; auto.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
1314
Qed.