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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Fixpoint noDowncast (V:Type) (e:exp V) :=
  match e with
  | Var _ x => True
  | Const m e => True
  | Unop u e => noDowncast e
  | Binop b e1 e2 => noDowncast e1 /\ noDowncast e2
Nikita Zyuzin's avatar
Nikita Zyuzin committed
219
  | Fma e1 e2 e3 => noDowncast e1 /\ noDowncast e2 /\ noDowncast e3
Heiko Becker's avatar
Heiko Becker committed
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
  | Downcast m e => False
  end.

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

Opaque mTypeToQ.

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

Lemma typing_exp_64_bit e:
  forall Gamma tMap,
    noDowncast e ->
    is64BitEval e ->
    typeCheck e Gamma tMap = true ->
    (forall v,
        NatSet.In v (usedVars e) -> Gamma v = Some M64) ->
    tMap e  = Some M64.
Proof.
  induction e; intros * noDowncast_e is64BitEval_e typecheck_e types_valid;
    simpl in *; try inversion noDowncast_e;
      subst.
  - destruct (tMap (Var Q n)); try congruence.
    rewrite types_valid in *; try set_tac.
    type_conv; subst; auto.
  - destruct (tMap (Const M64 v)) eqn:?; try congruence; type_conv; subst; auto.
  - destruct (tMap (Unop u e)) eqn:?; try congruence.
    erewrite IHe in *; eauto.
    + andb_to_prop typecheck_e; type_conv; subst; auto.
    + destruct (tMap e); try congruence; andb_to_prop typecheck_e; auto.
  - repeat (match goal with
            |H: _ /\ _ |- _=> destruct H
            end).
    destruct (tMap (Binop b e1 e2)) eqn:?; try congruence;
      erewrite IHe1 in *; eauto.
    + erewrite IHe2 in *; eauto.
      * unfold join in typecheck_e.
        rewrite isMorePrecise_refl in typecheck_e; andb_to_prop typecheck_e;
          type_conv; subst; auto.
      * destruct (tMap e2); try congruence.
        andb_to_prop typecheck_e; eauto.
      * intros.
        apply types_valid. set_tac.
    + destruct (tMap e1); destruct (tMap e2); try congruence;
        andb_to_prop typecheck_e; eauto.
    + intros; apply types_valid; set_tac.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
  - repeat (match goal with
            |H: _ /\ _ |- _=> destruct H
            end).
    destruct (tMap (Fma e1 e2 e3)) eqn:?; try congruence;
      erewrite IHe1 in *; eauto.
    + erewrite IHe2 in *; eauto.
      * unfold join3, join in typecheck_e.
        erewrite IHe3 in *; eauto.
        ++ rewrite isMorePrecise_refl in typecheck_e; andb_to_prop typecheck_e;
          type_conv; subst; auto.
        ++ destruct (tMap e3); try congruence.
           andb_to_prop typecheck_e; eauto.
        ++ intros; apply types_valid. set_tac.
      * destruct (tMap e2); destruct (tMap e3); try congruence.
        andb_to_prop typecheck_e; eauto.
      * intros.
        apply types_valid. set_tac.
    + destruct (tMap e1); destruct (tMap e2); destruct (tMap e3); try congruence;
        andb_to_prop typecheck_e; eauto.
    + intros; apply types_valid; set_tac.
Heiko Becker's avatar
Heiko Becker committed
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
Qed.

Lemma typing_cmd_64_bit f:
  forall Gamma tMap,
    noDowncastFun f ->
    is64BitBstep f ->
    typeCheckCmd f Gamma tMap = true ->
    (forall v,
        NatSet.In v (freeVars f) -> Gamma v = Some M64) ->
    tMap (getRetExp f)  = Some M64.
Proof.
  induction f; intros * noDowncast_f is64BitEval_f typecheck_f types_valid;
    simpl in *;
    subst; try eauto using typing_exp_64_bit.
  andb_to_prop typecheck_f.
  destruct (tMap e) eqn:?; destruct (tMap (Var Q n)); try congruence.
  andb_to_prop R.
  destruct noDowncast_f; destruct is64BitEval_f as [Ha [Hb Hc]].
  eapply IHf; eauto.
  intros. unfold updDefVars.
  destruct (v =? n) eqn:?.
  - type_conv; auto.
  - apply types_valid.
    rewrite NatSet.remove_spec, NatSet.union_spec.
    split; try auto.
    hnf; intros; subst. rewrite Nat.eqb_neq in Heqb.
    congruence.
Qed.

Lemma typing_agrees_exp e:
  forall E Gamma tMap v m1 m2,
    typeCheck e Gamma tMap = true ->
    eval_exp E Gamma (toRExp e) v m1 ->
    tMap e = Some m2 ->
    m1 = m2.
Proof.
  induction e; intros * typeCheck_e eval_e tMap_e; simpl in *;
    rewrite tMap_e in *;
    inversion eval_e; subst; simpl in *.
  - rewrite H0 in *; type_conv; subst; auto.
  - type_conv; subst; auto.
  - destruct (tMap e) eqn:?; try congruence; type_conv; subst.
    andb_to_prop typeCheck_e.
    eapply IHe; eauto.
    type_conv; subst; auto.
  - destruct (tMap e) eqn:?; try congruence; type_conv; subst.
    andb_to_prop typeCheck_e.
    eapply IHe; eauto.
    type_conv; subst; auto.
  - destruct (tMap e1) eqn:?; try congruence;
      destruct (tMap e2) eqn:?; try congruence.
    andb_to_prop typeCheck_e.
    type_conv; subst.
    assert (m0 = m).
    { eapply IHe1; eauto. }
    assert (m3 = m1).
    { eapply IHe2; eauto. }
    subst; auto.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
403
404
405
406
407
408
409
410
411
412
413
414
  - destruct (tMap e1) eqn:?; try congruence;
      destruct (tMap e2) eqn:?; try congruence;
      destruct (tMap e3) eqn:?; try congruence.
    andb_to_prop typeCheck_e.
    type_conv; subst.
    assert (m0 = m).
    { eapply IHe1; eauto. }
    assert (m3 = m1).
    { eapply IHe2; eauto. }
    assert (m4 = m5).
    { eapply IHe3; eauto. }
    subst; auto.
Heiko Becker's avatar
Heiko Becker committed
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
  - destruct (tMap e) eqn:?; try congruence; type_conv; subst.
    andb_to_prop typeCheck_e.
    type_conv; subst; auto.
Qed.

Lemma typing_agrees_cmd f:
  forall E Gamma tMap v m1 m2,
    typeCheckCmd f Gamma tMap = true ->
    bstep (toRCmd f) E Gamma v m1 ->
    tMap (getRetExp f) = Some m2 ->
    m1 = m2.
Proof.
  induction f; intros * typeCheck_f eval_f tMap_f; simpl in *.
  - andb_to_prop typeCheck_f.
    inversion eval_f; subst; simpl in *.
    destruct (tMap e); destruct (tMap (Var Q n)); try congruence.
    andb_to_prop R; type_conv.
    specialize (IHf (updEnv n v0 E) (updDefVars n m3 Gamma) tMap v m1 m2).
    apply IHf; auto.
  - inversion eval_f; subst; eapply typing_agrees_exp; eauto.
Qed.

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

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

(* (fexp_correct 53 1024 eq_refl) as fexp_corr. *)
(* (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53) *)
521
(*                                     (-1022)%Z 53%Z) *)
Heiko Becker's avatar
Heiko Becker committed
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
Lemma eval_exp_gives_IEEE (e:exp fl64) :
  forall E1 E2 E2_real Gamma tMap vR A P fVars dVars,
    (forall x, (toREnv E2) x = E2_real x) ->
    typeCheck (B2Qexp e) Gamma tMap = true ->
    approxEnv E1 Gamma A fVars dVars E2_real ->
    validIntervalbounds (B2Qexp e) A P dVars = true ->
    validErrorbound (B2Qexp e) tMap A dVars = true ->
    FPRangeValidator (B2Qexp e) A tMap dVars = true ->
    eval_exp (toREnv E2) Gamma (toRExp (B2Qexp e)) vR M64 ->
    NatSet.Subset ((usedVars (B2Qexp e)) -- dVars) fVars ->
    is64BitEval (B2Qexp e) ->
    noDowncast (B2Qexp e) ->
    eval_exp_valid e E2 ->
    (forall v,
        NatSet.In v fVars ->
        exists vR, E1 v = Some vR /\ Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R ->
    (forall v, NatSet.In v fVars \/ NatSet.In v dVars -> exists m, Gamma v = Some m) ->
    (forall v,
        NatSet.In v dVars ->
        exists vR,
          E1 v = Some vR /\ Q2R (fst (fst (A (Var Q v)))) <= vR
          <= Q2R (snd (fst (A (Var Q v)))))%R ->
      (forall v,
        NatSet.In v dVars ->
        exists vF m,
        (E2_real v = Some vF /\ tMap (Var Q v) = Some m /\
        validFloatValue vF m)) ->
      (forall v, NatSet.In v (usedVars (B2Qexp e)) -> Gamma v = Some M64) ->
      exists v,
        eval_exp_float e E2 = Some v /\
        eval_exp (toREnv E2) Gamma (toRExp (B2Qexp e)) (Q2R (B2Q v)) M64.
553
Proof.
Heiko Becker's avatar
Heiko Becker committed
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
  induction e; simpl in *;
    intros * envs_eq typecheck_e approxEnv_E1_E2_real valid_rangebounds
                     valid_roundoffs valid_float_ranges eval_e_float
                     usedVars_sound is64BitEval_e noDowncast_e eval_IEEE_valid_e
                     fVars_defined vars_typed dVars_sound dVars_valid
                     usedVars_64bit;
    (match_pat (eval_exp _ _ _ _ _) (fun H => inversion H; subst; simpl in *));
  repeat match goal with
         | H : _ = true |- _ => andb_to_prop H
         end.
  - unfold toREnv in *.
    destruct (E2 n) eqn:HE2; try congruence.
    exists f; split; try eauto.
    eapply Var_load; try auto. rewrite HE2; auto.
  - eexists; split; try eauto.
    eapply (Const_dist' (delta:=0%R)); eauto.
    + rewrite Rabs_R0; apply mTypeToQ_pos_R.
    + unfold perturb. lra.
  - edestruct IHe as [v_e [eval_float_e eval_rel_e]]; eauto.
    + destruct (tMap (Unop Neg (B2Qexp e)));
        destruct (tMap (B2Qexp e)); try congruence; andb_to_prop typecheck_e; auto.
    + destruct (A (Unop Neg (B2Qexp e))); andb_to_prop valid_rangebounds; auto.
    + destruct (A (Unop Neg (B2Qexp e))); destruct (tMap (Unop Neg (B2Qexp e)));
        try congruence; andb_to_prop valid_roundoffs; auto.
    + destruct (A (Unop Neg (B2Qexp e))); destruct (tMap (Unop Neg (B2Qexp e)));
        try congruence; andb_to_prop valid_float_ranges; auto.
    + assert (is_finite 53 1024 v_e = true).
      { apply validValue_is_finite.
        eapply FPRangeValidator_sound; eauto.
        eapply eval_eq_env; eauto.
        destruct (tMap (Unop Neg (B2Qexp e)));
          destruct (tMap (B2Qexp e)); try congruence; andb_to_prop typecheck_e; auto.
        destruct (A (Unop Neg (B2Qexp e))); try congruence;
          andb_to_prop valid_rangebounds; auto.
        destruct (A (Unop Neg (B2Qexp e))); destruct (tMap (Unop Neg (B2Qexp e)));
          try congruence. andb_to_prop valid_roundoffs; auto.
        destruct (A (Unop Neg (B2Qexp e))); destruct (tMap (Unop Neg (B2Qexp e)));
          try congruence. andb_to_prop valid_float_ranges; auto. }
      exists (b64_opp v_e); rewrite eval_float_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.
  - destruct (A (Unop Inv (B2Qexp e))); destruct (tMap (Unop Inv (B2Qexp e)));
      try congruence; andb_to_prop valid_roundoffs; congruence.
  - repeat (match goal with
            |H: _ /\ _ |- _ => destruct H
            end).
    destruct (tMap (Binop b (B2Qexp e1) (B2Qexp e2))) eqn:?; try congruence;
      destruct (tMap (B2Qexp e1)) eqn:?; try congruence;
      destruct (tMap (B2Qexp e2)) eqn:?; try congruence.
    andb_to_prop typecheck_e; type_conv; subst.
    assert (tMap (B2Qexp e1) = Some M64 /\
            tMap (B2Qexp e2) = Some M64 /\
            tMap (Binop b (B2Qexp e1) (B2Qexp e2)) = Some M64)
           as [tMap_e1 [tMap_e2 tMap_b]].
    { repeat split; apply (typing_exp_64_bit _ Gamma); simpl; auto.
      - intros; apply usedVars_64bit; set_tac.
      - intros; apply usedVars_64bit; set_tac.
      - rewrite Heqo, Heqo0, Heqo1.
        apply Is_true_eq_true; apply andb_prop_intro; split.
        + apply andb_prop_intro; split; apply Is_true_eq_left; auto.
          apply mTypeEq_refl.
        + apply Is_true_eq_left; auto. }
    rewrite tMap_e1, tMap_e2, tMap_b in *.
    inversion Heqo; inversion Heqo0; inversion Heqo1; subst.
    assert (m1 = M64).
    { eapply (typing_agrees_exp (B2Qexp e1)); eauto. }
    assert (m2 = M64).
    { eapply typing_agrees_exp; eauto. }
    subst.
    destruct (A (Binop b (B2Qexp e1) (B2Qexp e2))) eqn:?;
             destruct (A (B2Qexp e1)) eqn:?;
             destruct (A (B2Qexp e2)) eqn:?;
             simpl in *.
    repeat (match goal with
            |H: _ = true |- _ => andb_to_prop H
            end).
    destruct (IHe1 E1 E2 E2_real Gamma tMap v1 A P fVars dVars)
      as [v_e1 [eval_float_e1 eval_rel_e1]];
      try auto; try set_tac;
        [ intros; apply usedVars_64bit ; set_tac | ].
    destruct (IHe2 E1 E2 E2_real Gamma tMap v2 A P fVars dVars)
      as [v_e2 [eval_float_e2 eval_rel_e2]];
      try auto; try set_tac;
        [ intros; apply usedVars_64bit ; set_tac | ].
    rewrite eval_float_e1, eval_float_e2.
    assert (exists nR2,
               eval_exp E1 (toRMap Gamma) (toREval (toRExp (B2Qexp e2))) nR2 M0 /\
               Q2R (fst (fst (A (B2Qexp e2)))) <= nR2 <= Q2R (snd (fst (A (B2Qexp e2)))))%R
           as [nR2 [eval_e2_real e2_bounded_real]].
    { eapply validIntervalbounds_sound; eauto.
      - intros; eapply dVars_sound; set_tac.
      - set_tac. hnf in usedVars_sound. apply usedVars_sound.
        set_tac.
      - intros. eapply fVars_defined. rewrite NatSet.mem_spec in *; auto.
      - intros. apply vars_typed. set_tac. rewrite NatSet.union_spec in *; auto. }
    assert (forall vF2 m2,
               eval_exp E2_real Gamma (toRExp (B2Qexp e2)) vF2 m2 ->
               (Rabs (nR2 - vF2) <= Q2R (snd (A (B2Qexp e2)))))%R.
    { eapply validErrorbound_sound; try eauto; try set_tac.
      - intros. eapply dVars_sound; set_tac.
      - intros. eapply fVars_defined. rewrite NatSet.mem_spec in *; auto.
      - intros. apply vars_typed; set_tac. rewrite NatSet.union_spec in *; auto.
      - rewrite Heqp1.
        simpl. instantiate (1:=snd(i1)).
        instantiate (1:=fst(i1)). destruct i1; simpl; auto. }
    assert (contained (Q2R (B2Q v_e2))
                      (widenInterval
                         (Q2R (fst (fst (A (B2Qexp e2)))), Q2R (snd (fst (A (B2Qexp e2)))))
                         (Q2R (snd(A (B2Qexp e2)))))).
    { eapply distance_gives_iv.
      - simpl. eapply e2_bounded_real.
      - eapply H11. instantiate(1:=M64).
        eapply eval_eq_env; eauto. }
    assert (b = Div -> (Q2R (B2Q v_e2)) <> 0%R).
    { intros; subst; simpl in *.
      andb_to_prop R2.
      apply le_neq_bool_to_lt_prop in L4.
      rewrite Heqp1 in *; simpl in *.
      destruct L4; hnf; intros.
      - rewrite H15 in *.
        apply Qlt_Rlt in H14.
        rewrite Q2R0_is_0, Q2R_plus in H14. lra.
      - rewrite H15 in *.
        apply Qlt_Rlt in H14.
        rewrite Q2R0_is_0, Q2R_minus in H14; lra. }
    assert (validFloatValue
              (evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2))) M64).
    { eapply (FPRangeValidator_sound (Binop b (B2Qexp e1) (B2Qexp e2)));
        try eauto; set_tac.
      - eapply eval_eq_env; eauto.
        eapply (Binop_dist' (delta:=0)); eauto.
        + rewrite Rabs_R0. apply mTypeToQ_pos_R.
        + unfold perturb; lra.
      - rewrite tMap_b, tMap_e1, tMap_e2.
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro); split; try auto using Is_true_eq_left.
      - rewrite Heqp, Heqp0, Heqp1.
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro); split; try auto using Is_true_eq_left.
        apply andb_prop_intro; split; auto using Is_true_eq_left.
      - rewrite Heqp, Heqp0, Heqp1.
        rewrite tMap_b.
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left.
      - rewrite tMap_b, Heqp.
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left. }
    assert (validFloatValue (Q2R (B2Q v_e1)) M64).
    { eapply (FPRangeValidator_sound (B2Qexp e1)); try eauto; try set_tac.
      eapply eval_eq_env; eauto. }
    assert (validFloatValue (Q2R (B2Q v_e2)) M64).
    { eapply (FPRangeValidator_sound (B2Qexp e2)); try eauto; try set_tac.
      - eapply eval_eq_env; eauto. }
    assert (is_finite 53 1024 v_e1 = true) as finite_e1.
    { apply validValue_is_finite; simpl; auto. }
    assert (is_finite 53 1024 v_e2 = true) as finite_e2.
    { apply validValue_is_finite; simpl; auto. }
    assert (forall eps,
               (Rabs eps <= / 2 * bpow radix2 (- 53 + 1))%R ->
               validFloatValue
                 (evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2) * (1 + eps)) M64).
    { intros.
      eapply FPRangeValidator_sound with (e:=Binop b (B2Qexp e1) (B2Qexp e2)); eauto.
      - eapply eval_eq_env; eauto.
        eapply Binop_dist' with (delta:=eps); eauto.
        simpl in H2. Transparent mTypeToQ. unfold mTypeToQ.
        eapply Rle_trans; eauto.  unfold Qpower. unfold Qpower_positive.
        assert (pow_pos Qmult (2#1) 53 = 9007199254740992 # 1 )
          by (vm_compute; auto).
        rewrite H19. rewrite Q2R_inv; try lra.
        unfold Q2R, Qnum, Qden. unfold bpow.
        assert (-53 + 1 = -52)%Z by auto.
        rewrite H20.
        assert (Z.pow_pos radix2 52 = 4503599627370496%Z) by (vm_compute; auto).
        rewrite H21. unfold Z2R, P2R. lra.
        unfold perturb.
        repeat rewrite B2Q_B2R_eq; auto.
      - simpl. rewrite tMap_b, tMap_e1, tMap_e2.
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
      - simpl; rewrite Heqp, Heqp0, Heqp1.
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
      - simpl. rewrite Heqp, Heqp0, Heqp1, tMap_b.
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
      - simpl. rewrite Heqp, tMap_b.
        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 *.
      andb_to_prop R2.
      apply le_neq_bool_to_lt_prop in L4.
      rewrite Heqp1 in *; simpl in *.
      destruct L4 as [case_low | case_high]; hnf; intros.
      - rewrite H19 in *.
        apply Qlt_Rlt in case_low.
        rewrite Q2R0_is_0, Q2R_plus in case_low. lra.
      - rewrite H19 in *.
        apply Qlt_Rlt in case_high.
        rewrite Q2R0_is_0, Q2R_minus in case_high; lra. }
    clear H2 H12 dVars_sound dVars_valid usedVars_64bit vars_typed fVars_defined
    usedVars_sound R2 R1 L1 L R6 L0 R3 L3 R4 L2 R5 R7 L5 Heqo Heqo0 Heqo1 IHe1
    IHe2.
    pose proof (fexp_correct 53 1024 eq_refl) as fexp_corr.
    assert (forall k : Z, (-1022 < k)%Z ->
                     (53 <= k - Fcore_FLT.FLT_exp (3 - 1024 - 53) 53 k)%Z)
      as exp_valid.
    { intros k k_pos.
      unfold Fcore_FLT.FLT_exp; simpl.
      destruct (Z.max_spec_le (k - 53) (-1074)); omega. }
    pose proof (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53)
                                    (-1022)%Z 53%Z exp_valid)
      as rel_error_exists.
    rewrite eval_float_e1, eval_float_e2 in H1.
    unfold optionLift, normal_or_zero in *; simpl in *.
    assert (Normal (evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2)) M64 \/
            (evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2)) = 0)%R.
    { revert H1; intros case_val. destruct case_val; try auto.
      left; unfold Normal, Denormal in H15; unfold Normal;
        destruct H15 as [normal_b | [denormal_b |zero_b]].
      - repeat rewrite <- B2Q_B2R_eq; try auto.
      - destruct denormal_b.
        assert ((Rabs (evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2)))) < (Rabs (evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2)))))%R.
        { eapply Rlt_le_trans; eauto.
          repeat rewrite B2Q_B2R_eq; auto. }
        lra.
      - rewrite B2Q_B2R_eq in zero_b; auto.
        rewrite B2Q_B2R_eq in zero_b; auto.
        rewrite zero_b in *.
        rewrite Rabs_R0 in H1.
        unfold minValue, minExponentPos in H1.
        rewrite Q2R_inv in H1; [|vm_compute; congruence].
        unfold Q2R, Qnum, Qden in H1.
        assert (Z.pow_pos 2 1022 = 44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304%Z)
          by (vm_compute; auto).
        rewrite H2 in H1. rewrite <- Z2R_IZR in H1.  unfold IZR in H1.
        simpl in H1. lra. }
    pose proof (validValue_bounded b v_e1 v_e2 H2 H18) as cond_valid.
    destruct b; revert H1; intros case_eval.

    (* Addition *)
    + unfold evalBinop in *. unfold b64_plus.
      pose proof (Bplus_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE
                                v_e1 v_e2 finite_e1 finite_e2)
        as addition_correct.
      rewrite cond_valid in addition_correct.
      destruct addition_correct as [add_round [finite_res _]].
      destruct case_eval as [eval_zero | eval_normal].
      (* resutl is zero *)
      * rewrite eval_zero in *.
        rewrite round_0_zero in *.
        exists (Bplus 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2).
        split; try auto.
        rewrite B2Q_B2R_eq; try auto.
        unfold dmode; rewrite add_round.
        eapply Binop_dist' with (delta:=0%R); eauto.
        rewrite Rabs_R0; apply mTypeToQ_pos_R.
        unfold perturb, evalBinop.
        repeat rewrite B2Q_B2R_eq; try auto; lra.
      * simpl in *.
        destruct (rel_error_exists
                    (fun x => negb (Zeven x))
                    (B2R 53 1024 v_e1 + B2R 53 1024 v_e2)%R)
          as [eps [eps_bounded round_eq]].
        { eapply Rle_trans; eauto. unfold minValue, minExponentPos.
          rewrite Q2R_inv; [ | vm_compute; congruence].
          unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
          vm_compute. lra. }
        { exists (Bplus 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2);
            split; try auto.
          rewrite B2Q_B2R_eq; try auto.
          unfold dmode.
          eapply Binop_dist' with (delta:=eps); eauto.
          - unfold mTypeToQ.
            assert (join M64 M64 = M64) by (vm_compute; auto).
            rewrite H1.
            eapply Rle_trans; eauto.
            unfold Qpower. unfold Qpower_positive.
            assert (pow_pos Qmult (2#1) 53 = 9007199254740992 # 1 )
              by (vm_compute; auto).
            rewrite H12. rewrite Q2R_inv; try lra.
            unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
            simpl; lra.
          - unfold perturb, evalBinop.
            repeat rewrite B2Q_B2R_eq; try auto.
            rewrite <- round_eq. rewrite <- add_round; auto. }
    (* Subtraction *)
    + unfold evalBinop in *. unfold b64_minus.
      pose proof (Bminus_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE
                                v_e1 v_e2 finite_e1 finite_e2)
        as subtraction_correct.
      rewrite cond_valid in subtraction_correct.
      destruct subtraction_correct as [add_round [finite_res _]].
      destruct case_eval as [eval_zero | eval_normal].
      (* resutl is zero *)
      * rewrite eval_zero in *.
        rewrite round_0_zero in *.
        exists (Bminus 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2).
        split; try auto.
        rewrite B2Q_B2R_eq; try auto.
        unfold dmode; rewrite add_round.
        eapply Binop_dist' with (delta:=0%R); eauto.
        rewrite Rabs_R0; apply mTypeToQ_pos_R.
        unfold perturb, evalBinop.
        repeat rewrite B2Q_B2R_eq; try auto; lra.
      * simpl in *.
        destruct (rel_error_exists
                    (fun x => negb (Zeven x))
                    (B2R 53 1024 v_e1 - B2R 53 1024 v_e2)%R)
          as [eps [eps_bounded round_eq]].
        { eapply Rle_trans; eauto. unfold minValue, minExponentPos.
          rewrite Q2R_inv; [ | vm_compute; congruence].
          unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
          vm_compute. lra. }
        { exists (Bminus 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2);
            split; try auto.
          rewrite B2Q_B2R_eq; try auto.
          unfold dmode.
          eapply Binop_dist' with (delta:=eps); eauto.
          - unfold mTypeToQ.
            assert (join M64 M64 = M64) by (vm_compute; auto).
            rewrite H1.
            eapply Rle_trans; eauto.
            unfold Qpower. unfold Qpower_positive.
            assert (pow_pos Qmult (2#1) 53 = 9007199254740992 # 1 )
              by (vm_compute; auto).
            rewrite H12. rewrite Q2R_inv; try lra.
            unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
            simpl; lra.
          - unfold perturb, evalBinop.
            repeat rewrite B2Q_B2R_eq; try auto.
            rewrite <- round_eq. rewrite <- add_round; auto. }
    (* Multiplication *)
    + unfold evalBinop in *. unfold b64_mult.
      pose proof (Bmult_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE
                                v_e1 v_e2)
        as mult_correct.
      rewrite cond_valid in mult_correct.
      destruct mult_correct as [mult_round [finite_res _]].
      destruct case_eval as [eval_zero | eval_normal].
      (* resutl is zero *)
      * rewrite eval_zero in *.
        rewrite round_0_zero in *.
        exists (Bmult 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2).
        split; try auto.
        rewrite B2Q_B2R_eq; try auto.
        unfold dmode; rewrite mult_round.
        eapply Binop_dist' with (delta:=0%R); eauto.
        rewrite Rabs_R0; apply mTypeToQ_pos_R.
        unfold perturb, evalBinop.
        repeat rewrite B2Q_B2R_eq; try auto; lra.
        rewrite finite_e1, finite_e2 in finite_res.
        auto.
      * simpl in *.
        destruct (rel_error_exists
                    (fun x => negb (Zeven x))
                    (B2R 53 1024 v_e1 * B2R 53 1024 v_e2)%R)
          as [eps [eps_bounded round_eq]].
        { eapply Rle_trans; eauto. unfold minValue, minExponentPos.
          rewrite Q2R_inv; [ | vm_compute; congruence].
          unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
          vm_compute. lra. }
        { exists (Bmult 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2);
            split; try auto.
          rewrite B2Q_B2R_eq; try auto.
          unfold dmode.
          eapply Binop_dist' with (delta:=eps); eauto.
          - unfold mTypeToQ.
            assert (join M64 M64 = M64) by (vm_compute; auto).
            rewrite H1.
            eapply Rle_trans; eauto.
            unfold Qpower. unfold Qpower_positive.
            assert (pow_pos Qmult (2#1) 53 = 9007199254740992 # 1 )
              by (vm_compute; auto).
            rewrite H12. rewrite Q2R_inv; try lra.
            unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
            simpl; lra.
          - unfold perturb, evalBinop.
            repeat rewrite B2Q_B2R_eq; try auto.
            rewrite <- round_eq. rewrite <- mult_round; auto.
          - rewrite finite_e1, finite_e2 in finite_res; auto. }
    (* Division *)
    + unfold evalBinop in *. unfold b64_div.
      pose proof (Bdiv_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE
                                v_e1 v_e2)
        as division_correct.
      rewrite cond_valid in division_correct.
      destruct division_correct as [div_round [finite_res _]].
      rewrite <- B2Q_B2R_eq; auto.
      destruct case_eval as [eval_zero | eval_normal].
      (* resutl is zero *)
      * rewrite eval_zero in *.
        rewrite round_0_zero in *.
        exists (Bdiv 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2).
        split; try auto.
        rewrite B2Q_B2R_eq; try auto.
        unfold dmode; rewrite div_round.
        eapply Binop_dist' with (delta:=0%R); eauto.
        rewrite Rabs_R0; apply mTypeToQ_pos_R.
        unfold perturb, evalBinop.
        repeat rewrite B2Q_B2R_eq; try auto; lra.
        rewrite finite_e1 in finite_res; auto.
      * simpl in *.
        destruct (rel_error_exists
                    (fun x => negb (Zeven x))
                    (B2R 53 1024 v_e1 / B2R 53 1024 v_e2)%R)
          as [eps [eps_bounded round_eq]].
        { eapply Rle_trans; eauto. unfold minValue, minExponentPos.
          rewrite Q2R_inv; [ | vm_compute; congruence].
          unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
          vm_compute. lra. }
        { exists (Bdiv 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2);
            split; try auto.
          rewrite B2Q_B2R_eq; try auto.
          unfold dmode.
          eapply Binop_dist' with (delta:=eps); eauto.
          - unfold mTypeToQ.
            assert (join M64 M64 = M64) by (vm_compute; auto).
            rewrite H1.
            eapply Rle_trans; eauto.
            unfold Qpower. unfold Qpower_positive.
            assert (pow_pos Qmult (2#1) 53 = 9007199254740992 # 1 )
              by (vm_compute; auto).
            rewrite H12. rewrite Q2R_inv; try lra.
            unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
            simpl; lra.
          - unfold perturb, evalBinop.
            repeat rewrite B2Q_B2R_eq; try auto.
            rewrite <- round_eq. rewrite <- div_round; auto.
          - rewrite finite_e1 in finite_res; auto. }
Nikita Zyuzin's avatar
Nikita Zyuzin committed
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
  - repeat (match goal with
            |H: _ /\ _ |- _ => destruct H
            end).
    destruct (tMap (Fma (B2Qexp e1) (B2Qexp e2) (B2Qexp e3))) eqn:?; try congruence;
      destruct (tMap (B2Qexp e1)) eqn:?; try congruence;
      destruct (tMap (B2Qexp e2)) eqn:?; try congruence;
      destruct (tMap (B2Qexp e3)) eqn:?; try congruence.
    andb_to_prop typecheck_e; type_conv; subst.
    assert (tMap (B2Qexp e1) = Some M64 /\
            tMap (B2Qexp e2) = Some M64 /\
            tMap (B2Qexp e3) = Some M64 /\
            tMap (Fma (B2Qexp e1) (B2Qexp e2) (B2Qexp e3)) = Some M64)
           as [tMap_e1 [tMap_e2 [tMap_e3 tMap_fma]]].
    { repeat split; apply (typing_exp_64_bit _ Gamma); simpl; auto.
      - intros; apply usedVars_64bit; set_tac.
      - intros; apply usedVars_64bit; set_tac.
      - intros; apply usedVars_64bit; set_tac.
      - rewrite Heqo, Heqo0, Heqo1, Heqo2.
        apply Is_true_eq_true; apply andb_prop_intro; split.
        + apply andb_prop_intro; split.
          * apply andb_prop_intro; split.
            ++ apply Is_true_eq_left; auto.
               apply mTypeEq_refl.
            ++ apply Is_true_eq_left; auto.
          * apply Is_true_eq_left; auto.
        + apply Is_true_eq_left; auto. }
    rewrite tMap_e1, tMap_e2, tMap_e3, tMap_fma in *.
    inversion Heqo; inversion Heqo0; inversion Heqo1; inversion Heqo2; subst.
    assert (m1 = M64).
    { eapply (typing_agrees_exp (B2Qexp e1)); eauto. }
    assert (m2 = M64).
    { eapply (typing_agrees_exp (B2Qexp e2)); eauto. }
    assert (m3 = M64).
    { eapply (typing_agrees_exp (B2Qexp e3)); eauto. }
    subst.
    destruct (A (Fma (B2Qexp e1) (B2Qexp e2) (B2Qexp e3))) eqn:?;
             destruct (A (B2Qexp e1)) eqn:?;
             destruct (A (B2Qexp e2)) eqn:?;
             destruct (A (B2Qexp e3)) eqn:?;
             simpl in *.
    repeat (match goal with
            |H: _ = true |- _ => andb_to_prop H
            end).
    destruct (IHe1 E1 E2 E2_real Gamma tMap v1 A P fVars dVars)
      as [v_e1 [eval_float_e1 eval_rel_e1]];
      try auto; try set_tac;
        [ intros; apply usedVars_64bit ; set_tac | ].
    destruct (IHe2 E1 E2 E2_real Gamma tMap v2 A P fVars dVars)
      as [v_e2 [eval_float_e2 eval_rel_e2]];
      try auto; try set_tac;
        [ intros; apply usedVars_64bit ; set_tac | ].
1038
1039
1040
1041
1042
1043
1044
1045
    destruct (IHe3 E1 E2 E2_real Gamma tMap v3 A P fVars dVars)
      as [v_e3 [eval_float_e3 eval_rel_e3]];
      try auto; try set_tac;
        [ intros; apply usedVars_64bit ; set_tac | ].
    unfold optionLift in H4.
    rewrite eval_float_e1, eval_float_e2, eval_float_e3 in H4.
    contradiction H4.
  - inversion noDowncast_e.
Heiko Becker's avatar
Heiko Becker committed
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
Qed.

Lemma bstep_gives_IEEE (f:cmd fl64) :
  forall E1 E2 E2_real Gamma tMap vR vF A P fVars dVars outVars,
    (forall x, (toREnv E2) x = E2_real x) ->
    approxEnv E1 Gamma A fVars dVars E2_real ->
    ssa (B2Qcmd f) (NatSet.union fVars dVars) outVars ->
    typeCheckCmd (B2Qcmd f) Gamma tMap = true ->
    validIntervalboundsCmd (B2Qcmd f) A P dVars = true ->
    validErrorboundCmd (B2Qcmd f) tMap A dVars = true ->
    FPRangeValidatorCmd (B2Qcmd f) A tMap dVars = true ->
    bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRMap Gamma) vR M0 ->
    bstep (toRCmd (B2Qcmd f)) (toREnv E2) Gamma vF M64 ->
    NatSet.Subset (NatSet.diff (freeVars (B2Qcmd f)) dVars) fVars ->
    is64BitBstep (B2Qcmd f) ->
    noDowncastFun (B2Qcmd f) ->
    bstep_valid f E2 ->
    (forall v,
        NatSet.In v fVars ->
        exists vR, E1 v = Some vR /\ Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R ->
    (forall v, NatSet.In v fVars \/ NatSet.In v dVars -> exists m, Gamma v = Some m) ->
    (forall v,
        NatSet.In v dVars ->
        exists vR,
          E1 v = Some vR /\ Q2R (fst (fst (A (Var Q v)))) <= vR
          <= Q2R (snd (fst (A (Var Q v)))))%R ->
      (forall v,
        NatSet.In v dVars ->
        exists vF m,
        (E2_real v = Some vF /\ tMap (Var Q v) = Some m /\
        validFloatValue vF m)) ->
      (forall v, NatSet.In v (freeVars (B2Qcmd f)) -> Gamma v = Some M64) ->
      exists v,
        bstep_float f E2 = Some v /\
        bstep (toRCmd (B2Qcmd f)) (toREnv E2) Gamma (Q2R (B2Q v)) M64.
Proof.
  induction f;
    intros * envs_eq approxEnv_E1_E2_real ssa_f typeCheck_f valid_ranges_f
                     valid_roundoffs_f valid_float_ranges bstep_real bstep_float
                     freeVars_sound is64_eval nodowncast_f bstep_sound
                     fVars_defined vars_typed dVars_sound dVars_valid
                     freeVars_typed;
    inversion bstep_float; inversion bstep_real;
      inversion ssa_f; subst; simpl in *;
        repeat (match goal with
                | H: _ = true |- _ => andb_to_prop H
                end).
  - assert (tMap (B2Qexp e) = Some M64).
    { eapply typing_exp_64_bit; try eauto.
      simpl in *; destruct nodowncast_f; auto.
      destruct is64_eval; auto.
      intros; apply freeVars_typed.
      set_tac. rewrite NatSet.remove_spec.
      split; [ set_tac | ].
      hnf; intros; subst.
      apply H26.
      apply (H25 n H).  }
    assert (m = M64).
    { eapply typing_agrees_exp; eauto. }
    subst.
    assert (exists v_e, eval_exp_float e E2 = Some v_e /\
                   eval_exp (toREnv E2) Gamma (toRExp (B2Qexp e)) (Q2R (B2Q v_e)) M64)
           as eval_float_e.
    { eapply eval_exp_gives_IEEE; try eauto.
      - hnf; intros. rewrite NatSet.diff_spec in H0.
        destruct H0.
        specialize (H25 a H0). rewrite NatSet.union_spec in H25.
        destruct H25; try congruence; auto.
      - destruct is64_eval; auto.
      - destruct nodowncast_f; auto.
      - destruct bstep_sound; auto.
      - intros. apply freeVars_typed.
        rewrite NatSet.remove_spec, NatSet.union_spec.
        split; try auto.
        hnf; intros; subst.
        specialize (H25 n H0); set_tac. }
    destruct eval_float_e as [v_e [eval_float_e eval_rel_e]].
    assert (forall v m, eval_exp E2_real Gamma (toRExp (B2Qexp e)) v m ->
                   Rabs (v0 - v) <= Q2R (snd (A (B2Qexp e))))%R
      as err_e_valid.
    { eapply validErrorbound_sound; try eauto.
      - hnf; intros. rewrite NatSet.diff_spec in H0.
        destruct H0. specialize (H25 a H0). rewrite NatSet.union_spec in H25.
        destruct H25; try auto; congruence.
      - intros. apply dVars_sound. rewrite <- NatSet.mem_spec; auto.
      - intros. apply fVars_defined. rewrite <- NatSet.mem_spec; auto.
      - intros. apply vars_typed.
        rewrite <- NatSet.union_spec, <- NatSet.mem_spec; auto.
      - instantiate (1:= snd (fst(A (B2Qexp e)))).
        instantiate (1:= fst (fst(A (B2Qexp e)))).
        destruct (A (B2Qexp e)) eqn:?. simpl.
        destruct i; auto. }
    assert (Rabs (v0 - (Q2R (B2Q v_e))) <= Q2R( snd (A (B2Qexp e))))%R.
    { 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 *)
    destruct (A (getRetExp (B2Qcmd f))) as [iv_f err_f] eqn:A_f.
    destruct iv_f as [ivlo_f ivhi_f].
    assert (exists vF m, bstep (toRCmd (B2Qcmd f)) (updEnv n (Q2R (B2Q v_e)) E2_real) (updDefVars n M64 Gamma) vF m).
    { eapply validErrorboundCmd_gives_eval; eauto.
      - destruct (tMap (B2Qexp e)); destruct  (tMap (Var Q n)); try congruence;
          andb_to_prop R5; inversion H; subst; auto.
      - eapply approxUpdBound; eauto.
        instantiate (1:= v0).
        rewrite Qeq_bool_iff in R1.
        eapply Rle_trans; eauto.
        apply Qle_Rle. rewrite R1. lra.
      - eapply ssa_equal_set; eauto.
        hnf; split; intros.
        + rewrite NatSet.add_spec, NatSet.union_spec in *.
          rewrite NatSet.add_spec in H1; destruct H1; auto.
          destruct H1; auto.
        + rewrite NatSet.add_spec in H1;
            rewrite NatSet.union_spec, NatSet.add_spec in *;
            destruct H1; auto. destruct H1; auto.
      - hnf; intros. rewrite NatSet.diff_spec in H1.
        destruct H1. apply freeVars_sound.
        rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
        split; try auto. split; try auto.
        hnf; intros; subst. apply H2. rewrite NatSet.add_spec. auto.
        rewrite NatSet.add_spec in H2. hnf; intros; apply H2; auto.
      - eapply (swap_Gamma_bstep (Gamma1:= updDefVars n M0 (toRMap Gamma)));
          eauto.
        intros; unfold updDefVars, toRMap.
        destruct (n0 =? n); auto.
      - intros. unfold updEnv. set_tac.
        rewrite NatSet.add_spec in H1. destruct (v1 =? n) eqn:?.
        destruct H1; subst; try congruence.
        + exists v0; split; try auto.
          assert (exists vR, eval_exp E1 (toRMap Gamma) (toREval (toRExp (B2Qexp e))) vR M0 /\
                        Q2R (fst (fst (A (B2Qexp e)))) <= vR <= Q2R (snd (fst (A (B2Qexp e)))))%R.
          { eapply validIntervalbounds_sound; eauto.
            - intros. eapply dVars_sound; rewrite NatSet.mem_spec in *; auto.
            - instantiate (1:=fVars).
              hnf; intros; rewrite NatSet.diff_spec in *.
              destruct H1.
              specialize (H25 a H1); rewrite NatSet.union_spec in H25;
                destruct H25; try auto; congruence.
            - intros; apply fVars_defined. rewrite NatSet.mem_spec in *; auto.
            - intros. apply vars_typed.
              rewrite NatSet.mem_spec, NatSet.union_spec in *; auto. }
          destruct H1 as [vR_e [eval_real_e bounded_e]].
          rewrite <- (meps_0_deterministic (toRExp (B2Qexp e)) eval_real_e H17).
          split;
            destruct bounded_e; eapply Rle_trans; eauto;
            apply Qle_Rle.
          apply Qeq_bool_iff in R4; rewrite R4; lra.
          apply Qeq_bool_iff in R3; rewrite R3; lra.
        + rewrite Nat.eqb_eq in Heqb; subst.
          exfalso; apply H26; rewrite NatSet.union_spec; auto.
        + rewrite Nat.eqb_neq in Heqb.
          destruct H1; try congruence.
          apply dVars_sound; auto.
      - intros; unfold updEnv.
        destruct (v1 =? n) eqn:?.
        + rewrite Nat.eqb_eq in Heqb; subst; exfalso.
          set_tac. apply H26; rewrite NatSet.union_spec; auto.
        + apply fVars_defined; rewrite NatSet.mem_spec in *; auto.
      - intros. unfold updDefVars. destruct (v1 =? n) eqn:?.
        + exists M64; auto.
        + apply vars_typed.
          rewrite Nat.eqb_neq in Heqb.
          set_tac.
          rewrite NatSet.union_spec, NatSet.add_spec in H1.
          destruct H1 as [HA |[HB | HC]]; try auto; congruence. }
    unfold optionLift. rewrite eval_float_e.
    assert (tMap (getRetExp (B2Qcmd f)) = Some M64).
    { eapply typingSoundnessCmd; eauto.
      destruct (tMap (B2Qexp e)); destruct (tMap (Var Q n)); try congruence;
        andb_to_prop R5; type_conv; auto. }
    destruct H1 as [vF_new [m_f bstep_float_new]].
    assert (m_f = M64).
    { eapply typing_agrees_cmd; eauto.
      destruct (tMap (B2Qexp e));
        destruct (tMap (Var Q n)); try congruence; andb_to_prop R5;
          type_conv; subst; auto. }
    subst.
    destruct (IHf (updEnv n v0 E1) (updFlEnv n v_e E2)
                  (updEnv n (Q2R (B2Q v_e)) E2_real) (updDefVars n M64 Gamma) tMap
                  vR vF_new A P fVars (NatSet.add n dVars) outVars); try eauto.
    + intros. unfold toREnv, updFlEnv, updEnv.
      destruct (x =? n); auto. rewrite <- envs_eq. unfold toREnv; auto.
    + apply approxUpdBound; auto.
      eapply Rle_trans; eauto.
      rewrite Qeq_bool_iff in R1; apply Qle_Rle; rewrite R1; lra.
    + 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.
    + destruct (tMap (B2Qexp e)); destruct (tMap (Var Q n)); try congruence;
        andb_to_prop R5; type_conv; auto.
    + eapply (swap_Gamma_bstep (Gamma1:= updDefVars n M0 (toRMap Gamma)));
        eauto.
      intros; unfold updDefVars, toRMap.
      destruct (n0 =? n); auto.
    + eapply (bstep_eq_env (E1 := updEnv n (Q2R (B2Q v_e)) E2_real)); eauto.
      intros x; unfold updEnv, updFlEnv, toREnv.
      destruct (x =? n); try auto.
      rewrite <- envs_eq. auto.
    + hnf; intros. rewrite NatSet.diff_spec in *.
      destruct H1. apply freeVars_sound.
      rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
      split; try auto. split; try auto.
      hnf; intros; subst. apply H3. rewrite NatSet.add_spec. auto.
      rewrite NatSet.add_spec in H3. hnf; intros; apply H3; auto.
    + destruct is64_eval as [HA [HB HC]]; auto.
    + destruct nodowncast_f as [HA HB]; auto.
    + destruct bstep_sound as [eval_sound bstep_sound].
      rewrite eval_float_e in bstep_sound; unfold optionLift in bstep_sound.
      auto.
    + intros; unfold updEnv.
      destruct (v1 =? n) eqn:?.
      * rewrite Nat.eqb_eq in Heqb; subst; exfalso.
        set_tac. apply H26; rewrite NatSet.union_spec; auto.
      * apply fVars_defined. auto.
    + intros. unfold updDefVars. destruct (v1 =? n) eqn:?.
      * exists M64; auto.
      * apply vars_typed.
        rewrite Nat.eqb_neq in Heqb.
        set_tac.
        destruct H1 as [HA |HB]; try auto.
        rewrite NatSet.add_spec in HB. destruct HB; try auto; congruence.
    + intros. unfold updEnv. set_tac.
      rewrite NatSet.add_spec in H1.
      destruct (v1 =? n) eqn:?;
      destruct H1; subst; try congruence.
      * exists v0; split; try auto.
        assert (exists vR, eval_exp E1 (toRMap Gamma) (toREval (toRExp (B2Qexp e))) vR M0 /\
                      Q2R (fst (fst (A (B2Qexp e)))) <= vR <= Q2R (snd (fst (A (B2Qexp e)))))%R.
        { eapply validIntervalbounds_sound; eauto.
            - intros. eapply dVars_sound; rewrite NatSet.mem_spec in *; auto.
            - instantiate (1:=fVars).
              hnf; intros; rewrite NatSet.diff_spec in *.
              destruct H1.
              specialize (H25 a H1); rewrite NatSet.union_spec in H25;
                destruct H25; try auto; congruence.
            - intros; apply fVars_defined. rewrite NatSet.mem_spec in *; auto.
            - intros. apply vars_typed.
              rewrite NatSet.mem_spec, NatSet.union_spec in *; auto. }
        destruct H1 as [vR_e [eval_real_e bounded_e]].
        rewrite <- (meps_0_deterministic (toRExp (B2Qexp e)) eval_real_e H17).
        rewrite Nat.eqb_eq in Heqb; subst.
        split;
            destruct bounded_e; eapply Rle_trans; eauto;
            apply Qle_Rle.
        apply Qeq_bool_iff in R4; rewrite R4; lra.
        apply Qeq_bool_iff in R3; rewrite R3; lra.
      * rewrite Nat.eqb_eq in Heqb; subst.
        exfalso; apply H26; rewrite NatSet.union_spec; auto.
      * rewrite Nat.eqb_neq in Heqb.
        congruence.
      * rewrite Nat.eqb_neq in Heqb.
        apply dVars_sound; auto.
    + intros. rewrite NatSet.add_spec in H1; unfold updEnv.
      destruct (v1 =? n) eqn:?; destruct H1; subst; try congruence.
      * destruct (tMap (Var Q n)) eqn:?; exists (Q2R (B2Q v_e)).
        exists m; repeat split; try auto.
        eapply FPRangeValidator_sound; eauto.
        { eapply eval_eq_env; eauto.
          rewrite H in *; andb_to_prop R5;
            type_conv; subst; auto. }
        { set_tac. split; try auto.
          rewrite NatSet.remove_spec, NatSet.union_spec.
          split; try auto.
          hnf; intros; subst. apply H26. apply H25; auto. }
        { rewrite H in *; congruence. }
      * rewrite Nat.eqb_eq in Heqb; subst.
        exists (Q2R (B2Q v_e)); rewrite H in *.
        destruct (tMap (Var Q n)) eqn:?; try congruence;
          andb_to_prop R5; type_conv; subst.
        exists M64; repeat split; try auto.
        eapply FPRangeValidator_sound; eauto.
        { eapply eval_eq_env; eauto. }
        { set_tac. split; try auto.
          rewrite NatSet.remove_spec, NatSet.union_spec.
          split; try auto.
          hnf; intros; subst. apply H26. apply H25; auto. }
      * rewrite Nat.eqb_neq in Heqb; congruence.
      * apply dVars_valid; auto.
    + intros. unfold updDefVars.
      destruct (v1 =? n) eqn:?; try auto.
      apply freeVars_typed; set_tac.
      rewrite NatSet.remove_spec, NatSet.union_spec; split; try auto.
      hnf; intros; subst; rewrite Nat.eqb_neq in Heqb; congruence.
    + exists x; destruct H1;
        split; try auto.
      eapply let_b; eauto.
      eapply bstep_eq_env with (E1:= toREnv (updFlEnv n v_e E2)); eauto.
      intros; unfold toREnv, updFlEnv, updEnv.
      destruct (x0 =? n); auto.
  - edestruct (eval_exp_gives_IEEE); eauto.
    exists x; destruct H.
    split; try auto. apply ret_b; auto.
Qed.

Theorem IEEE_connection_exp e A P E1 E2 defVars:
  approxEnv E1 defVars A (usedVars (B2Qexp e)) (NatSet.empty) (toREnv E2) ->
  is64BitEval (B2Qexp e) ->
  noDowncast (B2Qexp e) ->
  eval_exp_valid e E2 ->
  (forall v,
      NatSet.In v (usedVars (B2Qexp e)) ->
      defVars v = Some M64) ->
  (forall v,
      NatSet.In v (usedVars (B2Qexp e)) ->
      exists vR,
        (E1 v = Some vR) /\
        Q2R (fst (P v)) <= vR <= Q2R(snd (P v)))%R ->
  (forall v,
      NatSet.In v (usedVars (B2Qexp e)) ->
      exists m, defVars v = Some m) ->
  CertificateChecker (B2Qexp e) A P defVars = true ->
  exists vR vF, (* m, currently = M64 *)
    eval_exp E1 (toRMap defVars) (toREval (toRExp (B2Qexp e))) vR M0 /\
    eval_exp_float e E2 = Some vF /\
    eval_exp (toREnv E2) defVars (toRExp (B2Qexp e)) (Q2R (B2Q vF)) M64 /\
    (Rabs (vR - Q2R (B2Q vF )) <= Q2R (snd (A (B2Qexp e))))%R.
Proof.
  intros.
  edestruct Certificate_checking_is_sound; eauto.
  - intros. set_tac.
  - intros. set_tac.
  - destruct H7 as [vF [mF [eval_real [eval_float roundoff_sound]]]].
    unfold CertificateChecker in H6.
    andb_to_prop H6.
    assert (typeMap defVars (B2Qexp e) (B2Qexp e) = Some M64).
    { eapply typing_exp_64_bit; eauto. }
    assert (mF = M64).
    { eapply typing_agrees_exp; eauto. }
    subst.
    edestruct eval_exp_gives_IEEE; eauto.
    + set_tac.
    + intros. apply H5. destruct H7; try auto.
      inversion H7.
    + intros. inversion H7.
    + intros. inversion H7.
    + destruct H7 as [eval_float_f eval_rel].
      exists x; exists x0. repeat split; try auto.
      eapply roundoff_sound; eauto.
Qed.

Theorem IEEE_connection_cmd (f:cmd fl64) (absenv:analysisResult) P
        defVars E1 E2:
    approxEnv E1 defVars absenv (freeVars (B2Qcmd f)) NatSet.empty (toREnv E2) ->
    is64BitBstep (B2Qcmd f) ->
    noDowncastFun (B2Qcmd f) ->
    bstep_valid f E2 ->
    (forall v, NatSet.In v (freeVars (B2Qcmd f)) ->
          defVars v = Some M64) ->
    (forall v, NatSet.mem v (freeVars (B2Qcmd f))= true ->
          exists vR, E1 v = Some vR /\
                (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
    (forall v, (v) mem (freeVars (B2Qcmd f)) = true ->
          exists m : mType,
            defVars v = Some m) ->
    CertificateCheckerCmd (B2Qcmd f) absenv P defVars = true ->
    exists vR vF m,
    bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRMap defVars) vR M0 /\
    bstep_float f E2 = Some vF /\
    bstep (toRCmd (B2Qcmd f)) (toREnv E2) defVars (Q2R (B2Q vF)) m /\
    (forall vF m,
        bstep (toRCmd (B2Qcmd f)) (toREnv E2) defVars vF m ->
        (Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp (B2Qcmd f)))))%R).
(**
   The proofs is a simple composition of the soundness proofs for the range
   validator and the error bound validator.
**)
Proof.
  intros.
  unfold CertificateCheckerCmd in *.
  andb_to_prop H6.
  pose proof (validSSA_sound _ _ R0).
  destruct H6 as [outVars ssa_f].
  edestruct Certificate_checking_cmds_is_sound; eauto.
  - unfold CertificateCheckerCmd.
    apply Is_true_eq_true.
    repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
  - destruct H6 as [vF [m [bstep_real [bstep_float roundoff_sound]]]].
    assert (typeMapCmd defVars (B2Qcmd f) (getRetExp (B2Qcmd f)) = Some M64).
    { eapply typing_cmd_64_bit; eauto.  }
    assert (m = M64).
    { eapply typing_agrees_cmd; eauto. }
    subst.
    edestruct bstep_gives_IEEE; eauto.
    + eapply ssa_equal_set; eauto.
      hnf; intros; split; intros; set_tac.
      rewrite NatSet.union_spec in H7; destruct H7; try auto.
      inversion H7.
    + set_tac.
    + intros. apply H4; rewrite NatSet.mem_spec; auto.
    + intros. apply H5. set_tac. destruct H7; try auto.
      inversion H7.
    + intros. inversion H7.
    + intros * HA; inversion HA.
    + exists x; exists x0; exists M64.
      destruct H7 as [bstep_float2 bstep_rel].
      repeat split; auto.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
1447
Qed.