IEEE_connection.v 51.5 KB
Newer Older
1
2
3
4
5
6
From Coq
     Require Import Reals.Reals QArith.QArith QArith.Qabs micromega.Psatz
     QArith.Qreals.

From Flover
     Require Import Expressions Infra.RationalSimps TypeValidator IntervalValidation
7
8
     ErrorAnalysis CertificateChecker FPRangeValidator RoundoffErrorValidator
     Environments Infra.RealRationalProps Commands Infra.Ltacs.
9
10
11
12

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

Lemma bstep_gives_IEEE (f:cmd fl64) :
824
825
826
  forall E1 E2 E2_real Gamma DeltaMap vR vF A fVars dVars outVars,
    (forall (e' : expr R) (m' : mType),
        exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
Heiko Becker's avatar
Heiko Becker committed
827
    (forall x, (toREnv E2) x = E2_real x) ->
828
    approxEnv E1 (toRExpMap Gamma) A fVars dVars E2_real ->
Heiko Becker's avatar
Heiko Becker committed
829
    ssa (B2Qcmd f) (NatSet.union fVars dVars) outVars ->
830
831
    validTypesCmd (B2Qcmd f) Gamma ->
    validRangesCmd (B2Qcmd f) A E1 (toRTMap (toRExpMap Gamma)) ->
832
    validErrorBoundsCmd (B2Qcmd f) E1 E2_real A Gamma DeltaMap ->
833
    FPRangeValidatorCmd (B2Qcmd f) A Gamma dVars = true ->
834
835
    bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR vR REAL ->
    bstep (toRCmd (B2Qcmd f)) (toREnv E2) (toRExpMap Gamma) DeltaMap vF M64 ->
Heiko Becker's avatar
Heiko Becker committed
836
837
    NatSet.Subset (NatSet.diff (freeVars (B2Qcmd f)) dVars) fVars ->
    is64BitBstep (B2Qcmd f) ->
838
    is64BitEnv Gamma ->
Heiko Becker's avatar
Heiko Becker committed
839
840
841
842
843
    noDowncastFun (B2Qcmd f) ->
    bstep_valid f E2 ->
      (forall v,
        NatSet.In v dVars ->
        exists vF m,
844
        (E2_real v = Some vF /\ FloverMap.find (Var Q v) Gamma= Some m /\
Heiko Becker's avatar
Heiko Becker committed
845
846
847
        validFloatValue vF m)) ->
      exists v,
        bstep_float f E2 = Some v /\
848
        bstep (toRCmd (B2Qcmd f)) (toREnv E2) (toRExpMap Gamma) DeltaMap (Q2R (B2Q v)) M64.
Heiko Becker's avatar
Heiko Becker committed
849
850
Proof.
  induction f;
851
    intros * deltas_matched envs_eq approxEnv_E1_E2_real ssa_f typeCheck_f valid_ranges_f
Heiko Becker's avatar
Heiko Becker committed
852
                     valid_roundoffs_f valid_float_ranges bstep_real bstep_float
853
854
                     freeVars_sound is64_eval is64_env nodowncast_f bstep_sound
                     dVars_valid ;
855
856
857
858
    cbn in *;
    revert bstep_sound;
    Flover_compute_asm; try congruence; type_conv; subst;
      intros bstep_sound;
859
      unfold Ltacs.optionBind;
860
      inversion bstep_float; inversion bstep_real;
Heiko Becker's avatar
Heiko Becker committed
861
862
863
864
      inversion ssa_f; subst; simpl in *;
        repeat (match goal with
                | H: _ = true |- _ => andb_to_prop H
                end).
865
866
867
868
  - 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. }
869
    pose proof (validTypes_exec _ validt_e H H8); subst.
870
    destruct valid_roundoffs_f as ((valid_error & valid_error_cmd) & valid_roundoffs_f).
871
    assert (exists v_e, eval_expr_float e E2 = Some v_e /\
872
873
                   eval_expr (toREnv E2) (toRExpMap Gamma) DeltaMap
                             (toRExp (B2Qexpr e)) (Q2R (B2Q v_e)) M64)
Heiko Becker's avatar
Heiko Becker committed
874
           as eval_float_e.
875
    { eapply eval_expr_gives_IEEE; try eauto.
876
      - destruct valid_ranges_f as [[? ?] ?]; auto.
Heiko Becker's avatar
Heiko Becker committed
877
878
      - hnf; intros. rewrite NatSet.diff_spec in H0.
        destruct H0.
879
880
        specialize (H27 a H0). rewrite NatSet.union_spec in H27.
        destruct H27; try congruence; auto.
Heiko Becker's avatar
Heiko Becker committed
881
882
      - destruct is64_eval; auto.
      - destruct nodowncast_f; auto.
883
      - destruct bstep_sound; auto. }
Heiko Becker's avatar
Heiko Becker committed
884
    destruct eval_float_e as [v_e [eval_float_e eval_rel_e]].
885
886
887
    assert (exists iv err, FloverMap.find (B2Qexpr e) A = Some (iv, err)) as Hcert.
    {
      intuition.
888
889
      eapply validRanges_single in H12.
      destruct H12 as (? & ? & ? & ? & ?); eauto.
890
891
892
893
894
895
    }
    specialize Hcert as (? & ? & Hcert).
    pose proof valid_error as valid_error'.
    eapply validErrorBounds_single in valid_error; eauto.
    specialize valid_error as (exists_exec & err_e_valid).
    assert (Rabs (v0 - (Q2R (B2Q v_e))) <= Q2R x0)%R.
Heiko Becker's avatar
Heiko Becker committed
896
897
898
    { 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 *)
899
900
    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]]]]].
901
902
903
    assert (exists vF m,
               bstep (toRCmd (B2Qcmd f))
                     (updEnv n (Q2R (B2Q v_e)) E2_real)
904
                     (toRExpMap Gamma) DeltaMap vF m).
905
906
    {
      admit.
Heiko Becker's avatar
Heiko Becker committed
907
    }
908
    unfold optionBind. rewrite eval_float_e.
Heiko Becker's avatar
Heiko Becker committed
909
    destruct H1 as [vF_new [m_f bstep_float_new]].
910
    assert (m_f = M64) by (eapply bstep_Gamma_det; eauto); subst.
Heiko Becker's avatar
Heiko Becker committed
911
    destruct (IHf (updEnv n v0 E1) (updFlEnv n v_e E2)
912
                  (updEnv n (Q2R (B2Q v_e)) E2_real) Gamma DeltaMap
913
                  vR vF_new A fVars (NatSet.add n dVars) outVars); try eauto.
Heiko Becker's avatar
Heiko Becker committed
914
    + intros. unfold toREnv, updFlEnv, updEnv.
915
      destruct (x1 =? n); auto. rewrite <- envs_eq. unfold toREnv; auto.
916
917
    + destruct valid_error_cmd as [[? [? [? [? [? [? ?]]]]]] ?].
      eapply approxUpdBound; eauto.
918
      * eapply toRExpMap_some with (e:=Var Q n); eauto.
919
920
      * canonize_hyps. rewrite Hcert in *. inversion H1; subst.
        lra.
Heiko Becker's avatar
Heiko Becker committed
921
922
923
924
925
926
927
928
    + 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.
929
        (*
930
931
932
933
    + eapply validRangesCmd_swap with (Gamma1 := updDefVars n REAL Gamma);
        try auto.
      intros x; unfold toRMap, updDefVars.
      destruct (x =? n); auto.
934
    + eapply (swap_Gamma_bstep (Gamma1:= updDefVars n REAL (toRMap Gamma)));
Heiko Becker's avatar
Heiko Becker committed
935
936
        eauto.
      intros; unfold updDefVars, toRMap.
937
      destruct (n0 =? n); auto. *)
938
939
    + eapply valid_error_cmd; eauto.
      eapply eval_eq_env; eauto.
Heiko Becker's avatar
Heiko Becker committed
940
    + eapply (bstep_eq_env (E1 := updEnv n (Q2R (B2Q v_e)) E2_real)); eauto.
941
942
      intros x1; unfold updEnv, updFlEnv, toREnv.
      destruct (x1 =? n); try auto.
Heiko Becker's avatar
Heiko Becker committed
943
944
945
946
947
      rewrite <- envs_eq. auto.
    + hnf; intros. rewrite NatSet.diff_spec in *.
      destruct H1. apply freeVars_sound.
      rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
      split; try auto. split; try auto.
948
949
      hnf; intros; subst. apply H2. rewrite NatSet.add_spec. auto.
      rewrite NatSet.add_spec in H2. hnf; intros; apply H2; auto.
Heiko Becker's avatar
Heiko Becker committed
950
951
952
    + destruct is64_eval as [HA [HB HC]]; auto.
    + destruct nodowncast_f as [HA HB]; auto.
    + destruct bstep_sound as [eval_sound bstep_sound].
953
      rewrite eval_float_e in bstep_sound; unfold optionBind in bstep_sound.
Heiko Becker's avatar
Heiko Becker committed
954
      auto.
955
    + intros. unfold updEnv. destruct (v1 =? n) eqn:?.
956
957
958
959
960
961
962
963
964
965
      * eexists; exists M64; repeat split; eauto.
        { rewrite Nat.eqb_eq in Heqb; subst; auto. }
        { eapply FPRangeValidator_sound; eauto.
          - eapply eval_eq_env; eauto.
          - set_tac. split; try auto.
            split; try auto.
            hnf; intros; subst. set_tac. }
      * apply dVars_valid.
        set_tac.
        destruct H1 as [? | [? ?]]; rewrite Nat.eqb_neq in Heqb; congruence.
966
    + exists x1; destruct H1;
Heiko Becker's avatar
Heiko Becker committed
967
968
969
970
        split; try auto.
      eapply let_b; eauto.
      eapply bstep_eq_env with (E1:= toREnv (updFlEnv n v_e E2)); eauto.
      intros; unfold toREnv, updFlEnv, updEnv.
971
      destruct (x2 =? n); auto.
972
  - destruct valid_ranges_f as [? ?].
973
    destruct typeCheck_f.
974
    intuition.
975
976
977
    edestruct (eval_expr_gives_IEEE) as [v_res [eval_float eval_e]]; eauto.
    exists v_res; split; try auto.
    apply ret_b; auto.
978
Admitted.
Heiko Becker's avatar
Heiko Becker committed
979

980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
<