IEEE_connection.v 49.9 KB
Newer Older
1
Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qabs Coq.micromega.Psatz
2
        Coq.QArith.Qreals.
3 4 5 6
Require Import Flover.Expressions Flover.Infra.RationalSimps Flover.Typing
        Flover.IntervalValidation Flover.ErrorValidation Flover.CertificateChecker
        Flover.FPRangeValidator Flover.Environments Flover.Infra.RealRationalProps
        Flover.Commands Flover.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
Definition dmode := mode_NE.
Definition fl64:Type := binary_float 53 1024.

Definition normal_or_zero v :=
14
   (v = 0 \/ (Q2R (minValue_pos M64)) <= (Rabs v))%R.
Heiko Becker's avatar
Heiko Becker committed
15 16 17 18 19 20

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

21
Fixpoint eval_expr_float (e:expr (binary_float 53 1024)) (E:nat -> option fl64):=
22 23 24 25
  match e with
  | Var _ x => E x
  | Const m v => Some v
  | Unop Neg e =>
26
    match eval_expr_float e E with
27 28 29 30 31
    |Some v1 => Some (b64_opp v1)
    |_ => None
    end
  | Unop Inv e => None
  | Binop b e1 e2 =>
32
    match eval_expr_float e1 E, eval_expr_float e2 E with
33 34
    | Some f1, Some f2 =>
      match b with
Heiko Becker's avatar
Heiko Becker committed
35 36 37 38
      | 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)
39 40 41
      end
    |_ , _ => None
    end
Nikita Zyuzin's avatar
Nikita Zyuzin committed
42
  | Fma e1 e2 e3 =>
43
    match eval_expr_float e1 E, eval_expr_float e2 E, eval_expr_float e3 E with
44
      (* | Some f1, Some f2, Some f3 => Some (b64_plus dmode f1 (b64_mult dmode f2 f3)) *)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
45 46
      | _, _, _ => None
    end
47
  | _ => None
48 49
  end.

Heiko Becker's avatar
Heiko Becker committed
50 51
Fixpoint bstep_float f E :option fl64 :=
  match f with
52
  | Let m x e g =>
53
    olet res :=  eval_expr_float e E in
54
        bstep_float g (updFlEnv x res E)
55
  | Ret e => eval_expr_float e E
Heiko Becker's avatar
Heiko Becker committed
56 57 58
  end.

Definition isValid e :=
59 60
  plet v := e in
        normal_or_zero (B2R 53 1024 v).
Heiko Becker's avatar
Heiko Becker committed
61

62
Fixpoint eval_expr_valid (e:expr fl64) E :=
63
  match e with
64 65 66
  | Var _ x => True (*isValid (eval_expr_float (Var n) E)*)
  | Const m v => True (*isValid (eval_expr_float (Const m v) E)*)
  | Unop u e => eval_expr_valid e E
Heiko Becker's avatar
Heiko Becker committed
67
  | Binop b e1 e2 =>
68 69 70
    (eval_expr_valid e1 E) /\ (eval_expr_valid e2 E) /\
    (let e1_res := eval_expr_float e1 E in
     let e2_res := eval_expr_float e2 E in
71
     optionBind e1_res
Heiko Becker's avatar
Heiko Becker committed
72 73
                (fun v1 =>
                   let v1_real := B2R 53 1024 v1 in
74
                   optionBind e2_res
Heiko Becker's avatar
Heiko Becker committed
75 76 77 78 79
                              (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
80
  | Fma e1 e2 e3 =>
81 82 83 84
    (eval_expr_valid e1 E) /\ (eval_expr_valid e2 E) /\ (eval_expr_valid e3 E) /\
    (let e1_res := eval_expr_float e1 E in
     let e2_res := eval_expr_float e2 E in
     let e3_res := eval_expr_float e3 E in
85
     optionBind e1_res
Nikita Zyuzin's avatar
Nikita Zyuzin committed
86 87
                (fun v1 =>
                   let v1_real := B2R 53 1024 v1 in
88
                   optionBind e2_res
Nikita Zyuzin's avatar
Nikita Zyuzin committed
89 90
                              (fun v2 =>
                                 let v2_real := B2R 53 1024 v2 in
91
                                 optionBind e3_res
Nikita Zyuzin's avatar
Nikita Zyuzin committed
92 93
                                            (fun v3 =>
                                               let v3_real := B2R 53 1024 v3 in
94 95 96
                                               (* No support for fma yet *)
                                               (* normal_or_zero (evalFma v1_real v2_real v3_real)) *)
                                               False)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
97 98 99
                                            True)
                              True)
                True)
100
  | Downcast m e => eval_expr_valid e E
101 102
  end.

Heiko Becker's avatar
Heiko Becker committed
103 104
Fixpoint bstep_valid f E :=
  match f with
105
  | Let m x e g =>
106 107
    eval_expr_valid e E /\
    (optionBind (eval_expr_float e E)
108 109
                (fun v_e => bstep_valid g (updFlEnv x v_e E))
                True)
110
  | Ret e => eval_expr_valid e E
Heiko Becker's avatar
Heiko Becker committed
111 112 113 114 115
  end.

Definition bpowQ (r:radix) (e: Z) :=
  match e with
  |0%Z => 1%Q
116
  | Zpos p => (Z.pow_pos r p) #1
Heiko Becker's avatar
Heiko Becker committed
117 118 119 120 121 122
  | Z.neg p => Qinv ((Z.pow_pos r p)#1)
  end.

Definition B2Q :=
  fun prec emax : Z =>
    let emin := (3 - emax - prec)%Z in
Heiko Becker's avatar
Heiko Becker committed
123
    let fexpr := Fcore_FLT.FLT_exp emin prec in
Heiko Becker's avatar
Heiko Becker committed
124 125 126 127 128 129
    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 _ =>
130
        let f_new: Fcore_defs.float radix2 := {| Fcore_defs.Fnum := cond_Zopp s (Zpos m); Fcore_defs.Fexp := e |} in
Heiko Becker's avatar
Heiko Becker committed
131
        (Fcore_defs.Fnum f_new # 1) * bpowQ radix2 (Fcore_defs.Fexp f_new)
Heiko Becker's avatar
Heiko Becker committed
132 133 134 135 136 137 138 139 140 141 142 143 144 145 146
      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.
147
    destruct (cond_Zopp b (Zpos m)); unfold IZR;
Heiko Becker's avatar
Heiko Becker committed
148
      try rewrite P2R_INR, INR_IPR; lra.
Heiko Becker's avatar
Heiko Becker committed
149 150 151 152 153
  - unfold Q2R; simpl.
    unfold bpow, bpowQ.
    destruct e; simpl; try lra.
    + rewrite RMicromega.Rinv_1.
      unfold Z2R, IZR.
Heiko Becker's avatar
Heiko Becker committed
154
      destruct (Z.pow_pos 2 p); try rewrite P2R_INR, INR_IPR; auto.
Heiko Becker's avatar
Heiko Becker committed
155
    + unfold Z2R, IZR. unfold Qinv; simpl.
Heiko Becker's avatar
Heiko Becker committed
156
      destruct (Z.pow_pos 2 p) eqn:? ; try rewrite P2R_INR, INR_IPR; simpl; try lra.
Heiko Becker's avatar
Heiko Becker committed
157 158 159 160 161 162 163
      * 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.
Heiko Becker's avatar
Heiko Becker committed
164 165 166 167 168
      * unfold IPR at 1. rewrite Rmult_1_l; auto.
      * rewrite <- Ropp_mult_distr_l, Ropp_mult_distr_r, Ropp_inv_permute;
        [ unfold IPR at 1; lra | ].
        hnf; intros. pose proof (pos_INR_nat_of_P p0).
        rewrite INR_IPR in *.
Heiko Becker's avatar
Heiko Becker committed
169 170 171
        rewrite H0 in H1; lra.
Qed.

172
Fixpoint B2Qexpr (e: expr fl64) :=
Heiko Becker's avatar
Heiko Becker committed
173 174 175
  match e with
  | Var _ x =>  Var Q x
  | Const m v => Const m (B2Q v)
176 177 178 179
  | Unop u e => Unop u (B2Qexpr e)
  | Binop b e1 e2 => Binop b (B2Qexpr e1) (B2Qexpr e2)
  | Fma e1 e2 e3 => Fma (B2Qexpr e1) (B2Qexpr e2) (B2Qexpr e3)
  | Downcast m e => Downcast m (B2Qexpr e)
Heiko Becker's avatar
Heiko Becker committed
180 181 182 183
  end.

Fixpoint B2Qcmd (f:cmd fl64) :=
  match f with
184 185
  | Let m x e g => Let m x (B2Qexpr e) (B2Qcmd g)
  | Ret e => Ret (B2Qexpr e)
Heiko Becker's avatar
Heiko Becker committed
186 187 188 189 190 191 192 193
  end.

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

194
Fixpoint is64BitEval (V:Type) (e:expr V) :=
Heiko Becker's avatar
Heiko Becker committed
195 196 197 198 199
  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
200
  | Fma e1 e2 e3 => is64BitEval e1 /\ is64BitEval e2 /\ is64BitEval e3
Heiko Becker's avatar
Heiko Becker committed
201 202 203 204 205 206 207 208 209
  | 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.

210
Fixpoint noDowncast (V:Type) (e:expr V) :=
Heiko Becker's avatar
Heiko Becker committed
211 212 213 214 215
  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
216
  | Fma e1 e2 e3 => noDowncast e1 /\ noDowncast e2 /\ noDowncast e3
Heiko Becker's avatar
Heiko Becker committed
217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235
  | 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 *;
236
      unfold maxValue, minValue_pos, maxExponent, minExponentPos in*;
Heiko Becker's avatar
Heiko Becker committed
237
      rewrite Q2R_inv in *; unfold bpowQ in *.
238 239 240 241 242 243
  - cbn in *.
    destruct H; try lra.
    rewrite Rabs_right in H0.
    apply Rle_Qle in H0.
    + rewrite <- Qle_bool_iff in H0.
      cbv in H0; try congruence.
Heiko Becker's avatar
Heiko Becker committed
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
    + 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.

281
Lemma typing_expr_64_bit e fBits:
Heiko Becker's avatar
Heiko Becker committed
282 283 284
  forall Gamma tMap,
    noDowncast e ->
    is64BitEval e ->
285
    typeCheck e Gamma tMap fBits = true ->
Heiko Becker's avatar
Heiko Becker committed
286 287
    (forall v,
        NatSet.In v (usedVars e) -> Gamma v = Some M64) ->
288
    FloverMap.find e tMap = Some M64.
Heiko Becker's avatar
Heiko Becker committed
289 290
Proof.
  induction e; intros * noDowncast_e is64BitEval_e typecheck_e types_valid;
Heiko Becker's avatar
Heiko Becker committed
291
    cbn in *; try inversion noDowncast_e;
292 293 294 295 296 297 298
      subst.
  - Flover_compute; try congruence; type_conv; subst.
    rewrite types_valid in *; try set_tac.
  - Flover_compute; try congruence; type_conv; subst.
    destruct m; try congruence.
  - Flover_compute; try congruence; type_conv; subst.
    erewrite IHe in *; eauto.
Heiko Becker's avatar
Heiko Becker committed
299 300 301
  - repeat (match goal with
            |H: _ /\ _ |- _=> destruct H
            end).
302 303 304 305 306 307
      erewrite IHe1 with (Gamma:=Gamma) in *; eauto.
    + erewrite IHe2 with (Gamma:=Gamma) in *; eauto.
      * simpl in *.
        Flover_compute; try congruence.
        type_conv; subst; auto.
      * Flover_compute; auto.
Heiko Becker's avatar
Heiko Becker committed
308 309
      * intros.
        apply types_valid. set_tac.
310
    + Flover_compute; auto.
Heiko Becker's avatar
Heiko Becker committed
311
    + intros; apply types_valid; set_tac.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
312 313 314
  - repeat (match goal with
            |H: _ /\ _ |- _=> destruct H
            end).
315 316 317 318 319 320 321 322 323 324 325 326
    erewrite IHe1 with (Gamma:=Gamma) in *;
      eauto;
      [ | Flover_compute; try congruence; auto
        | intros; apply types_valid; set_tac].
    erewrite IHe2 with (Gamma:=Gamma) in *;
      eauto;
      [ | Flover_compute; try congruence; auto
        | intros; apply types_valid; set_tac].
    erewrite IHe3 with (Gamma:=Gamma) in *;
      eauto;
      [ | Flover_compute; try congruence; auto
        | intros; apply types_valid; set_tac].
327
    unfold join3, join in *.
328 329
    simpl in *.
    Flover_compute; try congruence; type_conv; auto.
Heiko Becker's avatar
Heiko Becker committed
330 331 332
Qed.

Lemma typing_cmd_64_bit f:
333
  forall Gamma tMap fBits,
Heiko Becker's avatar
Heiko Becker committed
334 335
    noDowncastFun f ->
    is64BitBstep f ->
336
    typeCheckCmd f Gamma tMap fBits = true ->
Heiko Becker's avatar
Heiko Becker committed
337 338
    (forall v,
        NatSet.In v (freeVars f) -> Gamma v = Some M64) ->
339
    FloverMap.find (getRetExp f) tMap = Some M64.
Heiko Becker's avatar
Heiko Becker committed
340 341
Proof.
  induction f; intros * noDowncast_f is64BitEval_f typecheck_f types_valid;
Heiko Becker's avatar
Heiko Becker committed
342
    cbn in *;
343
    subst; try eauto using typing_expr_64_bit;
344
      Flover_compute; try congruence.
Heiko Becker's avatar
Heiko Becker committed
345 346 347 348 349 350 351 352 353 354 355 356
  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.

357
Lemma typing_agrees_expr e:
358 359 360
  forall E Gamma tMap v m1 m2 fBits,
    typeCheck e Gamma tMap fBits = true ->
    eval_expr E Gamma (toRBMap fBits) (toRExp e) v m1 ->
361
    FloverMap.find e tMap = Some m2 ->
Heiko Becker's avatar
Heiko Becker committed
362 363
    m1 = m2.
Proof.
364 365 366
  intros.
  pose proof (typingSoundnessExp _ _ H H0).
  congruence.
Heiko Becker's avatar
Heiko Becker committed
367 368 369
Qed.

Lemma typing_agrees_cmd f:
370 371 372
  forall E Gamma tMap v m1 m2 fBits,
    typeCheckCmd f Gamma tMap fBits = true ->
    bstep (toRCmd f) E Gamma (toRBMap fBits) v m1 ->
373
    FloverMap.find (getRetExp f) tMap = Some m2 ->
Heiko Becker's avatar
Heiko Becker committed
374 375
    m1 = m2.
Proof.
376 377 378
  intros.
  pose proof (typingSoundnessCmd _ _ H H0).
  congruence.
Heiko Becker's avatar
Heiko Becker committed
379 380 381
Qed.

Lemma round_0_zero:
Heiko Becker's avatar
Heiko Becker committed
382
  (Fcore_generic_fmt.round radix2 (Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
Heiko Becker's avatar
Heiko Becker committed
383 384 385 386 387 388 389 390 391 392 393 394 395 396
                           (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.
Heiko Becker's avatar
Heiko Becker committed
397
  unfold Fcore_generic_fmt.canonic_exp.
Heiko Becker's avatar
Heiko Becker committed
398 399 400 401 402 403 404 405 406 407 408 409 410
  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
Heiko Becker's avatar
Heiko Becker committed
411
          (Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
Heiko Becker's avatar
Heiko Becker committed
412 413 414 415 416
          (round_mode mode_NE)
          (evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2))))
    (bpow radix2 1024) = true.
Proof.
  simpl.
Heiko Becker's avatar
Heiko Becker committed
417
  pose proof (fexp_correct 53 1024 eq_refl) as fexpr_corr.
Heiko Becker's avatar
Heiko Becker committed
418
  assert (forall k : Z, (-1022 < k)%Z ->
Heiko Becker's avatar
Heiko Becker committed
419
                     (53 <= k - Fcore_FLT.FLT_exp (3 - 1024 - 53) 53 k)%Z)
420
    as expr_valid.
Heiko Becker's avatar
Heiko Becker committed
421
  { intros k k_pos.
Heiko Becker's avatar
Heiko Becker committed
422
    unfold Fcore_FLT.FLT_exp; simpl.
Heiko Becker's avatar
Heiko Becker committed
423
    destruct (Z.max_spec_le (k - 53) (-1074)); omega. }
Heiko Becker's avatar
Heiko Becker committed
424
  pose proof (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53)
425
                                  (-1022)%Z 53%Z expr_valid)
Heiko Becker's avatar
Heiko Becker committed
426 427 428 429 430 431 432 433
    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.
434
      unfold minValue_pos.
Heiko Becker's avatar
Heiko Becker committed
435 436 437 438 439
      rewrite Q2R_inv.
      * apply Rinv_le.
        { rewrite <- Q2R0_is_0. apply Qlt_Rlt.
          apply Qlt_alt. vm_compute; auto. }
        { unfold Q2R.
440 441 442 443
          unfold Qnum, Qden. unfold minExponentPos.
          rewrite Z2R_IZR.
          rewrite Rinv_1. rewrite Rmult_1_r.
          apply IZR_le; vm_compute; congruence. }
Heiko Becker's avatar
Heiko Becker committed
444 445 446 447 448 449 450
      *  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.
Heiko Becker's avatar
Heiko Becker committed
451 452
        unfold Qnum, Qden. rewrite <- Z2R_IZR. unfold IZR.
        repeat rewrite <- INR_IPR. simpl. lra.
Heiko Becker's avatar
Heiko Becker committed
453 454
      * unfold Denormal in *. destruct denormal_v.
        eapply Rlt_trans; eauto.
455
        unfold minValue_pos, minExponentPos, bpow.
Heiko Becker's avatar
Heiko Becker committed
456 457
        rewrite Q2R_inv.
        { unfold Q2R, Qnum, Qden.
Heiko Becker's avatar
Heiko Becker committed
458 459
          rewrite <- Z2R_IZR; unfold IZR.
          repeat rewrite <- INR_IPR; simpl; lra. }
Heiko Becker's avatar
Heiko Becker committed
460
        { vm_compute; congruence. }
Heiko Becker's avatar
Heiko Becker committed
461
      * rewrite zero_v. simpl. rewrite Rabs_R0. lra.
Heiko Becker's avatar
Heiko Becker committed
462 463 464
  - rewrite zero_v.
    pose proof round_0_zero. simpl in H. rewrite H.
    rewrite Rabs_R0.
Heiko Becker's avatar
Heiko Becker committed
465
    lra.
Heiko Becker's avatar
Heiko Becker committed
466 467
Qed.

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

Lemma bstep_gives_IEEE (f:cmd fl64) :
904
  forall E1 E2 E2_real Gamma tMap vR vF A fVars dVars outVars fBits,
Heiko Becker's avatar
Heiko Becker committed
905 906 907
    (forall x, (toREnv E2) x = E2_real x) ->
    approxEnv E1 Gamma A fVars dVars E2_real ->
    ssa (B2Qcmd f) (NatSet.union fVars dVars) outVars ->
908 909
    typeCheckCmd (B2Qcmd f) Gamma tMap fBits = true ->
    validRangesCmd (B2Qcmd f) A E1 Gamma (toRBMap fBits) ->
Heiko Becker's avatar
Heiko Becker committed
910 911
    validErrorboundCmd (B2Qcmd f) tMap A dVars = true ->
    FPRangeValidatorCmd (B2Qcmd f) A tMap dVars = true ->
912 913
    bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRMap Gamma) (toRBMap fBits) vR REAL ->
    bstep (toRCmd (B2Qcmd f)) (toREnv E2) Gamma (toRBMap fBits) vF M64 ->
Heiko Becker's avatar
Heiko Becker committed
914 915 916 917
    NatSet.Subset (NatSet.diff (freeVars (B2Qcmd f)) dVars) fVars ->
    is64BitBstep (B2Qcmd f) ->
    noDowncastFun (B2Qcmd f) ->
    bstep_valid f E2 ->
918
    vars_typed (NatSet.union fVars dVars) Gamma ->
Heiko Becker's avatar
Heiko Becker committed
919 920 921
      (forall v,
        NatSet.In v dVars ->
        exists vF m,
922
        (E2_real v = Some vF /\ FloverMap.find (Var Q v) tMap= Some m /\
Heiko Becker's avatar
Heiko Becker committed
923 924 925 926
        validFloatValue vF m)) ->
      (forall v, NatSet.In v (freeVars (B2Qcmd f)) -> Gamma v = Some M64) ->
      exists v,
        bstep_float f E2 = Some v /\
927
        bstep (toRCmd (B2Qcmd f)) (toREnv E2) Gamma (toRBMap fBits) (Q2R (B2Q v)) M64.
Heiko Becker's avatar
Heiko Becker committed
928 929 930 931 932
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
933
                     vars_typed dVars_valid freeVars_typed;
934 935 936 937
    cbn in *;
    revert bstep_sound;
    Flover_compute_asm; try congruence; type_conv; subst;
      intros bstep_sound;
938
      unfold Ltacs.optionBind;