IEEE_connection.v 52.8 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12
From Coq
     Require Import Reals.Reals QArith.QArith QArith.Qabs micromega.Psatz
     QArith.Qreals.

From Flover
     Require Import Expressions Infra.RationalSimps TypeValidator IntervalValidation
     ErrorValidation CertificateChecker FPRangeValidator Environments
     Infra.RealRationalProps Commands Infra.Ltacs.

From Flocq
     Require Import Appli.Fappli_IEEE_bits Appli.Fappli_IEEE Core.Fcore_Raux
     Fprop_relative.
13

Heiko Becker's avatar
Heiko Becker committed
14 15 16 17
Definition dmode := mode_NE.
Definition fl64:Type := binary_float 53 1024.

Definition normal_or_zero v :=
18
   (v = 0 \/ (Q2R (minValue_pos M64)) <= (Rabs v))%R.
Heiko Becker's avatar
Heiko Becker committed
19 20 21 22 23 24

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

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

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

Definition isValid e :=
63
  plet v := e in
64
  normal_or_zero (B2R 53 1024 v).
Heiko Becker's avatar
Heiko Becker committed
65

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

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

Definition bpowQ (r:radix) (e: Z) :=
  match e with
  |0%Z => 1%Q
120
  | Zpos p => (Z.pow_pos r p) #1
Heiko Becker's avatar
Heiko Becker committed
121 122 123 124 125 126
  | 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
127
    let fexpr := Fcore_FLT.FLT_exp emin prec in
Heiko Becker's avatar
Heiko Becker committed
128 129 130 131 132 133
    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 _ =>
134
        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
135
        (Fcore_defs.Fnum f_new # 1) * bpowQ radix2 (Fcore_defs.Fexp f_new)
Heiko Becker's avatar
Heiko Becker committed
136 137 138 139 140 141 142 143 144 145 146 147 148 149 150
      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.
151
    destruct (cond_Zopp b (Zpos m)); unfold IZR;
Heiko Becker's avatar
Heiko Becker committed
152
      try rewrite P2R_INR, INR_IPR; lra.
Heiko Becker's avatar
Heiko Becker committed
153 154 155 156 157
  - 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
158
      destruct (Z.pow_pos 2 p); try rewrite P2R_INR, INR_IPR; auto.
Heiko Becker's avatar
Heiko Becker committed
159
    + unfold Z2R, IZR. unfold Qinv; simpl.
Heiko Becker's avatar
Heiko Becker committed
160
      destruct (Z.pow_pos 2 p) eqn:? ; try rewrite P2R_INR, INR_IPR; simpl; try lra.
Heiko Becker's avatar
Heiko Becker committed
161 162 163 164 165 166 167
      * 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
168 169 170 171 172
      * 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
173 174 175
        rewrite H0 in H1; lra.
Qed.

176
Fixpoint B2Qexpr (e: expr fl64) :=
Heiko Becker's avatar
Heiko Becker committed
177 178 179
  match e with
  | Var _ x =>  Var Q x
  | Const m v => Const m (B2Q v)
180 181 182 183
  | 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
184 185 186 187
  end.

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

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

198 199 200 201 202
Definition is64BitEnv (Gamma:FloverMap.t mType) :=
  forall (e:expr Q) (m:mType),
    FloverMap.find e Gamma = Some m ->
    m = M64.

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

219
Fixpoint noDowncast (V:Type) (e:expr V) :=
Heiko Becker's avatar
Heiko Becker committed
220 221 222 223 224
  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
225
  | Fma e1 e2 e3 => noDowncast e1 /\ noDowncast e2 /\ noDowncast e3
Heiko Becker's avatar
Heiko Becker committed
226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244
  | 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 *;
245
      unfold maxValue, minValue_pos, maxExponent, minExponentPos in*;
Heiko Becker's avatar
Heiko Becker committed
246
      rewrite Q2R_inv in *; unfold bpowQ in *.
247 248 249 250 251 252
  - 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
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
    + 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.

290 291 292 293 294
Lemma typing_expr_64_bit e:
  forall Gamma,
    is64BitEnv Gamma ->
    validTypes e Gamma ->
    FloverMap.find e Gamma = Some M64.
Heiko Becker's avatar
Heiko Becker committed
295
Proof.
296 297 298
  destruct e; intros * Gamma_64Bit [mG [find_mG ?]];
    erewrite <- Gamma_64Bit; eauto.
Qed.
Heiko Becker's avatar
Heiko Becker committed
299 300

Lemma typing_cmd_64_bit f:
301 302 303 304
  forall Gamma,
    is64BitEnv Gamma ->
    validTypesCmd f Gamma ->
    FloverMap.find (getRetExp f) Gamma = Some M64.
Heiko Becker's avatar
Heiko Becker committed
305
Proof.
306 307 308 309 310
  induction f; intros * Gamma_64BitEnv valid_f.
  - destruct valid_f as [(? & ? & ? & ? & ? & ?) ?].
    eapply IHf; eauto.
  - destruct valid_f; simpl in *; eapply typing_expr_64_bit; auto.
Qed.
Heiko Becker's avatar
Heiko Becker committed
311 312

Lemma round_0_zero:
Heiko Becker's avatar
Heiko Becker committed
313
  (Fcore_generic_fmt.round radix2 (Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
Heiko Becker's avatar
Heiko Becker committed
314 315 316 317 318 319 320 321 322 323 324 325 326 327
                           (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
328
  unfold Fcore_generic_fmt.canonic_exp.
Heiko Becker's avatar
Heiko Becker committed
329 330 331 332 333 334 335 336 337 338 339 340 341
  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
342
          (Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
Heiko Becker's avatar
Heiko Becker committed
343 344 345 346 347
          (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
348
  pose proof (fexp_correct 53 1024 eq_refl) as fexpr_corr.
Heiko Becker's avatar
Heiko Becker committed
349
  assert (forall k : Z, (-1022 < k)%Z ->
Heiko Becker's avatar
Heiko Becker committed
350
                     (53 <= k - Fcore_FLT.FLT_exp (3 - 1024 - 53) 53 k)%Z)
351
    as expr_valid.
Heiko Becker's avatar
Heiko Becker committed
352
  { intros k k_pos.
Heiko Becker's avatar
Heiko Becker committed
353
    unfold Fcore_FLT.FLT_exp; simpl.
Heiko Becker's avatar
Heiko Becker committed
354
    destruct (Z.max_spec_le (k - 53) (-1074)); omega. }
Heiko Becker's avatar
Heiko Becker committed
355
  pose proof (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53)
356
                                  (-1022)%Z 53%Z expr_valid)
Heiko Becker's avatar
Heiko Becker committed
357 358 359 360 361 362 363 364
    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.
365
      unfold minValue_pos.
Heiko Becker's avatar
Heiko Becker committed
366 367 368 369 370
      rewrite Q2R_inv.
      * apply Rinv_le.
        { rewrite <- Q2R0_is_0. apply Qlt_Rlt.
          apply Qlt_alt. vm_compute; auto. }
        { unfold Q2R.
371 372 373 374
          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
375 376 377 378 379 380 381
      *  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
382 383
        unfold Qnum, Qden. rewrite <- Z2R_IZR. unfold IZR.
        repeat rewrite <- INR_IPR. simpl. lra.
Heiko Becker's avatar
Heiko Becker committed
384 385
      * unfold Denormal in *. destruct denormal_v.
        eapply Rlt_trans; eauto.
386
        unfold minValue_pos, minExponentPos, bpow.
Heiko Becker's avatar
Heiko Becker committed
387 388
        rewrite Q2R_inv.
        { unfold Q2R, Qnum, Qden.
Heiko Becker's avatar
Heiko Becker committed
389 390
          rewrite <- Z2R_IZR; unfold IZR.
          repeat rewrite <- INR_IPR; simpl; lra. }
Heiko Becker's avatar
Heiko Becker committed
391
        { vm_compute; congruence. }
Heiko Becker's avatar
Heiko Becker committed
392
      * rewrite zero_v. simpl. rewrite Rabs_R0. lra.
Heiko Becker's avatar
Heiko Becker committed
393 394 395
  - rewrite zero_v.
    pose proof round_0_zero. simpl in H. rewrite H.
    rewrite Rabs_R0.
Heiko Becker's avatar
Heiko Becker committed
396
    lra.
Heiko Becker's avatar
Heiko Becker committed
397 398
Qed.

399
(* (fexpr_correct 53 1024 eq_refl) as fexpr_corr. *)
Heiko Becker's avatar
Heiko Becker committed
400
(* (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53) *)
401
(*                                     (-1022)%Z 53%Z) *)
402
Lemma eval_expr_gives_IEEE (e:expr fl64) :
403
  forall E1 E2 E2_real Gamma vR A fVars dVars,
Heiko Becker's avatar
Heiko Becker committed
404
    (forall x, (toREnv E2) x = E2_real x) ->
405 406 407 408 409 410
    validTypes (B2Qexpr e) Gamma ->
    approxEnv E1 (toRExpMap Gamma) A fVars dVars E2_real ->
    validRanges (B2Qexpr e) A E1 (toRTMap (toRExpMap Gamma)) ->
    validErrorbound (B2Qexpr e) Gamma A dVars = true ->
    FPRangeValidator (B2Qexpr e) A Gamma dVars = true ->
    eval_expr (toREnv E2) (toRExpMap Gamma) (toRExp (B2Qexpr e)) vR M64 ->
411 412
    NatSet.Subset ((usedVars (B2Qexpr e)) -- dVars) fVars ->
    is64BitEval (B2Qexpr e) ->
413
    is64BitEnv Gamma ->
414 415
    noDowncast (B2Qexpr e) ->
    eval_expr_valid e E2 ->
Heiko Becker's avatar
Heiko Becker committed
416 417 418
      (forall v,
        NatSet.In v dVars ->
        exists vF m,
419
        (E2_real v = Some vF /\ FloverMap.find (Var Q v) Gamma = Some m /\
Heiko Becker's avatar
Heiko Becker committed
420 421
        validFloatValue vF m)) ->
      exists v,
422
        eval_expr_float e E2 = Some v /\
423
        eval_expr (toREnv E2) (toRExpMap Gamma) (toRExp (B2Qexpr e)) (Q2R (B2Q v)) M64.
424
Proof.
425
  Opaque validTypes.
426
  induction e; simpl in *;
Heiko Becker's avatar
Heiko Becker committed
427 428
    intros * envs_eq typecheck_e approxEnv_E1_E2_real valid_rangebounds
                     valid_roundoffs valid_float_ranges eval_e_float
429 430 431
                     usedVars_sound is64BitTEnv is64BitEval_e noDowncast_e
                     eval_IEEE_valid_e dVars_sound;
    (match_pat (eval_expr _ _ _ _ _) (fun H => inversion H; subst; simpl in *));
432
     revert eval_IEEE_valid_e;
433
     Flover_compute_asm; try congruence; type_conv; subst;
434 435
     unfold optionBind;
     intros eval_IEEE_valid_e.
436 437
     Transparent validTypes.
     all:validTypes_split.
438
     - unfold toREnv in *.
439 440 441
       destruct (E2 n) eqn:HE2; try congruence.
       exists f; split; try eauto.
       eapply Var_load; try auto. rewrite HE2; auto.
442
     - eexists; split; try eauto.
443 444 445 446
       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].
447 448
       destruct m eqn:?; cbn in *; try congruence.
       subst.
449 450 451
       edestruct IHe as [v_e [eval_float_e eval_rel_e]]; eauto.
       assert (is_finite 53 1024 v_e = true).
       { apply validValue_is_finite.
452
         eapply FPRangeValidator_sound with (e:=B2Qexpr e); eauto.
453 454
         eapply eval_eq_env; eauto. }
         (* - cbn in typecheck_e; Flover_compute; auto. } *)
455 456 457 458 459 460
       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.
461
     - repeat (match goal with
462
               |H: _ /\ _ |- _ => destruct H
Heiko Becker's avatar
Heiko Becker committed
463
            end).
464 465 466
       assert (FloverMap.find (B2Qexpr e1) Gamma = Some M64 /\
               FloverMap.find (B2Qexpr e2) Gamma = Some M64 /\
               FloverMap.find (Binop b (B2Qexpr e1) (B2Qexpr e2)) Gamma = Some M64)
467
         as [tMap_e1 [tMap_e2 tMap_b]].
468 469 470 471 472 473 474 475 476
       { repeat split; apply (typing_expr_64_bit _ (Gamma := Gamma)); simpl; auto. }
       (*
         - cbn in typecheck_e; Flover_compute; auto;
           intros; apply usedVars_64bit; set_tac.
         - intros; apply usedVars_64bit; set_tac. } *)
       assert (m = M64) by congruence; subst.
       pose proof (validTypes_exec _ valid_arg tMap_e1 H5); subst.
       pose proof (validTypes_exec _ valid_arg0 tMap_e2 H8); subst.
       destruct (IHe1 E1 E2 E2_real Gamma v1 A fVars dVars)
477
         as [v_e1 [eval_float_e1 eval_rel_e1]];
478 479
         try auto; try set_tac.
       destruct (IHe2 E1 E2 E2_real Gamma v2 A fVars dVars)
480
         as [v_e2 [eval_float_e2 eval_rel_e2]];
481 482
         try auto; try set_tac.
       pose proof (validRanges_single _ _ _ _ H15) as valid_e.
483 484 485 486 487 488
       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,
489
               eval_expr E2_real (toRExpMap Gamma) (toRExp (B2Qexpr e2)) vF2 m2 ->
Heiko Becker's avatar
Heiko Becker committed
490
               (Rabs (nR2 - vF2) <= Q2R err_2))%R.
491
       { eapply validErrorbound_sound; try eauto; set_tac. }
Heiko Becker's avatar
Heiko Becker committed
492 493
    assert (contained (Q2R (B2Q v_e2))
                      (widenInterval
Heiko Becker's avatar
Heiko Becker committed
494
                         (Q2R ivlo_2, Q2R ivhi_2) (Q2R err_2))).
Heiko Becker's avatar
Heiko Becker committed
495 496
    { eapply distance_gives_iv.
      - simpl. eapply e2_bounded_real.
497
      - eapply H16. instantiate(1:=M64).
Heiko Becker's avatar
Heiko Becker committed
498 499 500
        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
501 502
      andb_to_prop R3.
      apply le_neq_bool_to_lt_prop in L3.
503 504
      rewrite Heqo2 in *.
      destruct i1; symmetry in map_e2; inversion map_e2; subst.
Heiko Becker's avatar
Heiko Becker committed
505
      destruct L3; hnf; intros.
506 507
      - rewrite H19 in *.
        apply Qlt_Rlt in H18.
508
        rewrite Q2R0_is_0, Q2R_plus in H18. simpl in *; lra.
509 510
      - rewrite H19 in *.
        apply Qlt_Rlt in H18.
511
        rewrite Q2R0_is_0, Q2R_minus in H18; simpl in *; lra. }
Heiko Becker's avatar
Heiko Becker committed
512 513
    assert (validFloatValue
              (evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2))) M64).
514
    { eapply (FPRangeValidator_sound (Binop b (B2Qexpr e1) (B2Qexpr e2)));
Heiko Becker's avatar
Heiko Becker committed
515 516
        try eauto; set_tac.
      - eapply eval_eq_env; eauto.
517 518
        eapply Binop_dist' with (delta:=0%R); eauto.
        + rewrite Rabs_R0. apply mTypeToR_pos_R.
Heiko Becker's avatar
Heiko Becker committed
519
        + unfold perturb; lra.
520 521 522
      - repeat split; try auto.
        + intros ? iv2 err2 find. subst.
          destruct iv2; rewrite find in *;
523
            eapply H12; eauto.
524
        + rewrite Heqo0. auto.
525
      - Flover_compute.
Heiko Becker's avatar
Heiko Becker committed
526 527
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro); split; try auto using Is_true_eq_left.
528 529
        rewrite Heqo2 in map_e2; destruct i0; inversion map_e2; subst.
        apply andb_prop_intro; split; apply Is_true_eq_left; try auto.
530
        rewrite L4, R1. auto.
531
      - Flover_compute.
Heiko Becker's avatar
Heiko Becker committed
532 533
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left. }
534
    rewrite Heqo2 in map_e2; destruct i0; inversion map_e2; subst.
Heiko Becker's avatar
Heiko Becker committed
535
    assert (validFloatValue (Q2R (B2Q v_e1)) M64).
536
    { eapply (FPRangeValidator_sound (B2Qexpr e1)); try eauto; try set_tac.
537
      eapply eval_eq_env; eauto. }
Heiko Becker's avatar
Heiko Becker committed
538
    assert (validFloatValue (Q2R (B2Q v_e2)) M64).
539
    { eapply (FPRangeValidator_sound (B2Qexpr e2)); try eauto; try set_tac.
540
      - eapply eval_eq_env; eauto. }
Heiko Becker's avatar
Heiko Becker committed
541 542 543 544 545 546 547 548 549
    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.
550
      eapply FPRangeValidator_sound with (e:=Binop b (B2Qexpr e1) (B2Qexpr e2)); eauto.
Heiko Becker's avatar
Heiko Becker committed
551 552
      - eapply eval_eq_env; eauto.
        eapply Binop_dist' with (delta:=eps); eauto.
553 554 555 556
        + simpl in H2. Transparent mTypeToQ. unfold mTypeToQ.
          eapply Rle_trans; eauto.
          simpl. lra.
        + unfold perturb. repeat rewrite B2Q_B2R_eq; try auto.
557 558 559
      - cbn; repeat split; try auto.
        + intros ? iv2 err2 find. subst.
          destruct iv2; rewrite find in *;
560
            eapply H12; eauto.
561
        + rewrite Heqo0. auto.
562
      - cbn. Flover_compute.
Heiko Becker's avatar
Heiko Becker committed
563 564
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
565
      - cbn. Flover_compute.
566
        inversion Heqo1; inversion Heqo2; subst.
Heiko Becker's avatar
Heiko Becker committed
567 568 569 570
        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 *.
571 572 573
      andb_to_prop R3.
      apply le_neq_bool_to_lt_prop in L3.
      destruct L3 as [case_low | case_high]; hnf; intros.
574
      - rewrite H23 in *.
Heiko Becker's avatar
Heiko Becker committed
575 576
        apply Qlt_Rlt in case_low.
        rewrite Q2R0_is_0, Q2R_plus in case_low. lra.
577
      - rewrite H23 in *.
Heiko Becker's avatar
Heiko Becker committed
578 579
        apply Qlt_Rlt in case_high.
        rewrite Q2R0_is_0, Q2R_minus in case_high; lra. }
580
    clear H2 H12 dVars_sound usedVars_sound R2 R1 L1 L
581
    L0 R3 L2 Heqo Heqo0 Heqo1 IHe1
Heiko Becker's avatar
Heiko Becker committed
582
    IHe2.
Heiko Becker's avatar
Heiko Becker committed
583
    pose proof (fexp_correct 53 1024 eq_refl) as fexpr_corr.
Heiko Becker's avatar
Heiko Becker committed
584
    assert (forall k : Z, (-1022 < k)%Z ->
Heiko Becker's avatar
Heiko Becker committed
585
                     (53 <= k - Fcore_FLT.FLT_exp (3 - 1024 - 53) 53 k)%Z)
586
      as expr_valid.
Heiko Becker's avatar
Heiko Becker committed
587
    { intros k k_pos.
Heiko Becker's avatar
Heiko Becker committed
588
      unfold Fcore_FLT.FLT_exp; simpl.
Heiko Becker's avatar
Heiko Becker committed
589
      destruct (Z.max_spec_le (k - 53) (-1074)); omega. }
Heiko Becker's avatar
Heiko Becker committed
590
    pose proof (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53)
591
                                    (-1022)%Z 53%Z expr_valid)
Heiko Becker's avatar
Heiko Becker committed
592
      as rel_error_exists.
593
    rewrite eval_float_e1, eval_float_e2 in H1.
594
    unfold optionBind, normal_or_zero in *; simpl in *.
Heiko Becker's avatar
Heiko Becker committed
595 596
    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.
597 598
    { revert H1; intros case_val.
      destruct case_val as [eval_is_zero | eval_normal]; try auto.
Heiko Becker's avatar
Heiko Becker committed
599
      left; unfold Normal, Denormal in H15; unfold Normal;
600
        destruct H19 as [normal_b | [denormal_b |zero_b]].
Heiko Becker's avatar
Heiko Becker committed
601 602 603
      - 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.
604
        { eapply Rlt_le_trans; eauto.
Heiko Becker's avatar
Heiko Becker committed
605 606 607 608 609
          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 *.
610 611 612 613
        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
614 615
        assert (Z.pow_pos 2 1022 = 44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304%Z)
          by (vm_compute; auto).
616 617 618 619
        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. }
620
    pose proof (validValue_bounded b v_e1 v_e2 H2 H22) as cond_valid.
Heiko Becker's avatar
Heiko Becker committed
621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637
    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.
638 639 640
        { rewrite Rabs_R0; apply mTypeToR_pos_R. }
        { unfold perturb, evalBinop. cbn.
        repeat rewrite B2Q_B2R_eq; try auto; lra. }
641
        { eapply toRExpMap_some; eauto. simpl; auto. }
Heiko Becker's avatar
Heiko Becker committed
642 643 644 645 646
      * 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]].
647
        { eapply Rle_trans; eauto. unfold minValue_pos, minExponentPos.
Heiko Becker's avatar
Heiko Becker committed
648 649 650 651 652 653 654 655
          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.
656
          - cbn; lra.
Heiko Becker's avatar
Heiko Becker committed
657 658
          - unfold perturb, evalBinop.
            repeat rewrite B2Q_B2R_eq; try auto.
659 660
            rewrite <- round_eq. rewrite <- add_round; auto.
          - eapply toRExpMap_some; eauto. simpl; auto. }
Heiko Becker's avatar
Heiko Becker committed
661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676
    (* 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.
677 678 679 680
        { rewrite Rabs_R0; apply mTypeToR_pos_R. }
        { unfold perturb, evalBinop; cbn.
          repeat rewrite B2Q_B2R_eq; try auto; lra. }
        { eapply toRExpMap_some; try eauto. simpl; auto. }
Heiko Becker's avatar
Heiko Becker committed
681 682 683 684 685
      * 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]].
686
        { eapply Rle_trans; eauto. unfold minValue_pos, minExponentPos.
Heiko Becker's avatar
Heiko Becker committed
687 688 689 690 691 692 693 694
          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.
695 696
          - cbn; lra.
          - unfold perturb, evalBinop; cbn.
Heiko Becker's avatar
Heiko Becker committed
697
            repeat rewrite B2Q_B2R_eq; try auto.
698 699
            rewrite <- round_eq. rewrite <- add_round; auto.
          - eapply toRExpMap_some; try eauto. simpl; auto. }
Heiko Becker's avatar
Heiko Becker committed
700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715
    (* 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.
716 717 718 719 720 721
        { rewrite Rabs_R0; apply mTypeToR_pos_R. }
        { unfold perturb, evalBinop; cbn.
          repeat rewrite B2Q_B2R_eq; try auto; lra. }
        { eapply toRExpMap_some; try eauto. simpl; auto. }
        { rewrite finite_e1, finite_e2 in finite_res.
          auto. }
Heiko Becker's avatar
Heiko Becker committed
722 723 724 725 726
      * 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]].
727
        { eapply Rle_trans; eauto. unfold minValue_pos, minExponentPos.
Heiko Becker's avatar
Heiko Becker committed
728 729 730 731 732 733 734 735
          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.
736
          - cbn; lra.
Heiko Becker's avatar
Heiko Becker committed
737 738 739
          - unfold perturb, evalBinop.
            repeat rewrite B2Q_B2R_eq; try auto.
            rewrite <- round_eq. rewrite <- mult_round; auto.
740
          - eapply toRExpMap_some; try eauto. simpl; auto.
Heiko Becker's avatar
Heiko Becker committed
741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758
          - 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.
759 760 761 762 763
        { rewrite Rabs_R0; apply mTypeToR_pos_R. }
        { unfold perturb, evalBinop; cbn.
          repeat rewrite B2Q_B2R_eq; try auto; lra. }
        { eapply toRExpMap_some; try eauto. simpl; auto. }
        { rewrite finite_e1 in finite_res; auto. }
Heiko Becker's avatar
Heiko Becker committed
764 765 766 767 768
      * 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]].
769
        { eapply Rle_trans; eauto. unfold minValue_pos, minExponentPos.
Heiko Becker's avatar
Heiko Becker committed
770 771 772 773 774 775 776 777
          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.
778
          - cbn; lra.
Heiko Becker's avatar
Heiko Becker committed
779 780 781
          - unfold perturb, evalBinop.
            repeat rewrite B2Q_B2R_eq; try auto.
            rewrite <- round_eq. rewrite <- div_round; auto.
782
          - eapply toRExpMap_some; try eauto. simpl; auto.
Heiko Becker's avatar
Heiko Becker committed
783
          - rewrite finite_e1 in finite_res; auto. }
Nikita Zyuzin's avatar
Nikita Zyuzin committed
784 785 786
  - repeat (match goal with
            |H: _ /\ _ |- _ => destruct H
            end).
787 788 789 790
    assert (FloverMap.find (B2Qexpr e1) Gamma = Some M64 /\
            FloverMap.find (B2Qexpr e2) Gamma = Some M64 /\
            FloverMap.find (B2Qexpr e3) Gamma = Some M64 /\
            FloverMap.find (Fma (B2Qexpr e1) (B2Qexpr e2) (B2Qexpr e3)) Gamma = Some M64)
791
      as [tMap_e1 [tMap_e2 [tMap_e3 tMap_fma]]].
792 793 794 795 796 797
    { repeat split; apply (typing_expr_64_bit _ (Gamma := Gamma)); simpl; auto. }
    assert (m = M64) by congruence.
    pose proof (validTypes_exec _ valid_arg tMap_e1 H5); subst.
    pose proof (validTypes_exec _ valid_arg0 tMap_e2 H8); subst.
    pose proof (validTypes_exec _ valid_arg1 tMap_e3 H9); subst.
    destruct (IHe1 E1 E2 E2_real Gamma v1 A fVars dVars)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
798
      as [v_e1 [eval_float_e1 eval_rel_e1]];
799 800
      try auto; try set_tac.
    destruct (IHe2 E1 E2 E2_real Gamma v2 A fVars dVars)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
801
      as [v_e2 [eval_float_e2 eval_rel_e2]];
802 803
      try auto; try set_tac.
    destruct (IHe3 E1 E2 E2_real Gamma v3 A fVars dVars)
804
      as [v_e3 [eval_float_e3 eval_rel_e3]];
805
      try auto; try set_tac.
806 807
    rewrite eval_float_e1, eval_float_e2, eval_float_e3 in H6.
    contradiction H6.
808
  - inversion noDowncast_e.
Heiko Becker's avatar
Heiko Becker committed
809 810 811
Qed.

Lemma bstep_gives_IEEE (f:cmd fl64) :
812
  forall E1 E2 E2_real Gamma vR vF A fVars dVars outVars,
Heiko Becker's avatar
Heiko Becker committed
813
    (forall x, (toREnv E2) x = E2_real x) ->
814
    approxEnv E1 (toRExpMap Gamma) A fVars dVars E2_real ->
Heiko Becker's avatar
Heiko Becker committed
815
    ssa (B2Qcmd f) (NatSet.union fVars dVars) outVars ->
816 817 818 819 820 821
    validTypesCmd (B2Qcmd f) Gamma ->
    validRangesCmd (B2Qcmd f) A E1 (toRTMap (toRExpMap Gamma)) ->
    validErrorboundCmd (B2Qcmd f) Gamma A dVars = true ->
    FPRangeValidatorCmd (B2Qcmd f) A Gamma dVars = true ->
    bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRTMap (toRExpMap Gamma)) vR REAL ->
    bstep (toRCmd (B2Qcmd f)) (toREnv E2) (toRExpMap Gamma) vF M64 ->
Heiko Becker's avatar
Heiko Becker committed
822 823
    NatSet.Subset (NatSet.diff (freeVars (B2Qcmd f)) dVars) fVars ->
    is64BitBstep (B2Qcmd f) ->
824
    is64BitEnv Gamma ->
Heiko Becker's avatar
Heiko Becker committed
825 826 827 828 829
    noDowncastFun (B2Qcmd f) ->
    bstep_valid f E2 ->
      (forall v,
        NatSet.In v dVars ->
        exists vF m,
830
        (E2_real v = Some vF /\ FloverMap.find (Var Q v) Gamma= Some m /\
Heiko Becker's avatar
Heiko Becker committed
831 832 833
        validFloatValue vF m)) ->
      exists v,
        bstep_float f E2 = Some v /\
834
        bstep (toRCmd (B2Qcmd f)) (toREnv E2) (toRExpMap Gamma) (Q2R (B2Q v)) M64.
Heiko Becker's avatar
Heiko Becker committed
835 836 837 838
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
839 840
                     freeVars_sound is64_eval is64_env nodowncast_f bstep_sound
                     dVars_valid ;
841 842 843 844
    cbn in *;
    revert bstep_sound;
    Flover_compute_asm; try congruence; type_conv; subst;
      intros bstep_sound;
845
      unfold Ltacs.optionBind;
846
      inversion bstep_float; inversion bstep_real;
Heiko Becker's avatar
Heiko Becker committed
847 848 849 850
      inversion ssa_f; subst; simpl in *;
        repeat (match goal with
                | H: _ = true |- _ => andb_to_prop H
                end).
851 852 853 854 855
  - destruct typeCheck_f as [[me [find_e [find_var [eq_t [validt_e validt_f]]]]] typeCheck_f].
    type_conv; subst.
    assert (FloverMap.find (B2Qexpr e) Gamma = Some M64).
    { eapply typing_expr_64_bit; eauto. }
    pose proof (validTypes_exec _ validt_e H H7); subst.
856
    assert (exists v_e, eval_expr_float e E2 = Some v_e /\
857
                   eval_expr (toREnv E2) (toRExpMap Gamma) (toRExp (B2Qexpr e)) (Q2R (B2Q v_e)) M64)
Heiko Becker's avatar
Heiko Becker committed
858
           as eval_float_e.
859
    { eapply eval_expr_gives_IEEE; try eauto.
860
      - destruct valid_ranges_f as [[? ?] ?]; auto.
Heiko Becker's avatar
Heiko Becker committed
861 862
      - hnf; intros. rewrite NatSet.diff_spec in H0.
        destruct H0.
863 864
        specialize (H25 a H0). rewrite NatSet.union_spec in H25.
        destruct H25; try congruence; auto.
Heiko Becker's avatar
Heiko Becker committed
865 866
      - destruct is64_eval; auto.
      - destruct nodowncast_f; auto.
867
      - destruct bstep_sound; auto. }
Heiko Becker's avatar
Heiko Becker committed
868
    destruct eval_float_e as [v_e [eval_float_e eval_rel_e]].
869
    assert (forall v m, eval_expr E2_real (toRExpMap Gamma) (toRExp (B2Qexpr e)) v m ->
870
                   Rabs (v0 - v) <= Q2R e0)%R
Heiko Becker's avatar
Heiko Becker committed
871 872 873
      as err_e_valid.
    { eapply validErrorbound_sound; try eauto.
      - hnf; intros. rewrite NatSet.diff_spec in H0.
874 875 876
        destruct H0. specialize (H25 a H0). rewrite NatSet.union_spec in H25.
        destruct H25; try auto; congruence.
      - unfold eval_Real. destruct valid_ranges_f as [[? ?] ?]; auto.
877 878 879
      - instantiate (1:= snd i). instantiate (1:=fst i).
        destruct i; simpl in *; auto. }
    assert (Rabs (v0 - (Q2R (B2Q v_e))) <= Q2R e0)%R.
Heiko Becker's avatar
Heiko Becker committed
880 881 882
    { 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 *)
883 884
    destruct valid_ranges_f as [[valid_e valid_cont] valid_single].
    destruct valid_single as [iv_ret [err_ret [v_ret [map_ret [eval_ret bound_ret]]]]].
885 886 887
    assert (exists vF m,
               bstep (toRCmd (B2Qcmd f))
                     (updEnv n (Q2R (B2Q v_e)) E2_real)
888
                     (toRExpMap Gamma) vF m).
Heiko Becker's avatar
Heiko Becker committed
889 890 891 892
    { 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
893
      - eapply approxUpdBound; eauto.
894 895 896 897 898
        + eapply toRExpMap_some with (e:=Var Q n); eauto.
        + rewrite Qeq_bool_iff in R1.
          eapply Rle_trans; eauto.
          canonize_hyps. rewrite <- R1.
          inversion Heqo0; subst; lra.
Heiko Becker's avatar
Heiko Becker committed
899 900 901 902 903 904 905 906 907 908 909 910 911 912
      - 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.
913
        (*
914
      - eapply (swap_Gamma_bstep (Gamma1:= updDefVars n REAL (toRMap Gamma)));
Heiko Becker's avatar
Heiko Becker committed
915 916 917
          eauto.
        intros; unfold updDefVars, toRMap.
        destruct (n0 =? n); auto.
918 919 920 921 922
      - eapply validRangesCmd_swap with (Gamma1 :=updDefVars n REAL Gamma);
          try auto.
        intros x; unfold toRMap, updDefVars.
        destruct (x =? n); auto.
      - unfold RealRangeArith.vars_typed. intros.
Heiko Becker's avatar
Heiko Becker committed
923
        unfold updDefVars. destruct (v1 =? n) eqn:?.
Heiko Becker's avatar
Heiko Becker committed
924 925 926 927
        + 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
928
          rewrite NatSet.union_spec.
929
          destruct H1 as [HA |[HB | HC]]; try auto; congruence. *)
Heiko Becker's avatar
Heiko Becker committed
930 931
      - destruct iv_ret; auto.
    }
932
    unfold optionBind. rewrite eval_float_e.
Heiko Becker's avatar
Heiko Becker committed
933
    destruct H1 as [vF_new [m_f bstep_float_new]].
934
    assert (m_f = M64) by (eapply bstep_Gamma_det; eauto); subst.
Heiko Becker's avatar
Heiko Becker committed
935
    destruct (IHf (updEnv n v0 E1) (updFlEnv n v_e E2)
936 937
                  (updEnv n (Q2R (B2Q v_e)) E2_real) Gamma
                  vR vF_new A fVars (NatSet.add n dVars) outVars); try eauto.
Heiko Becker's avatar
Heiko Becker committed
938 939
    + intros. unfold toREnv, updFlEnv, updEnv.
      destruct (x =? n); auto. rewrite <- envs_eq. unfold toREnv; auto.
Heiko Becker's avatar
Heiko Becker committed
940
    + eapply approxUpdBound; eauto.
941 942 943 944 945
      * eapply toRExpMap_some with (e:=Var Q n); eauto.
      * eapply Rle_trans; eauto.
        canonize_hyps.
        inversion Heqo0; subst.
        lra.
Heiko Becker's avatar
Heiko Becker committed
946 947 948