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

Heiko Becker's avatar
Heiko Becker committed
10
11
12
13
14
15
16
17
18
19
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 :=
20
   (v = 0 \/ (Q2R (minValue_pos M64)) <= (Rabs v))%R.
Heiko Becker's avatar
Heiko Becker committed
21
22
23
24
25
26

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

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

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

68
Fixpoint eval_expr_valid (e:expr fl64) E :=
69
  match e with
70
71
72
  | 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
73
  | Binop b e1 e2 =>
74
75
76
    (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
Heiko Becker's avatar
Heiko Becker committed
77
78
79
80
81
82
83
84
85
     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
  | Fma e1 e2 e3 =>
87
88
89
90
    (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
Nikita Zyuzin's avatar
Nikita Zyuzin committed
91
92
93
94
95
96
97
98
99
     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)
106
  | Downcast m e => eval_expr_valid e E
107
108
  end.

Heiko Becker's avatar
Heiko Becker committed
109
110
Fixpoint bstep_valid f E :=
  match f with
111
  | Let m x e g =>
112
113
    eval_expr_valid e E /\
    (optionLift (eval_expr_float e E)
114
115
                (fun v_e => bstep_valid g (updFlEnv x v_e E))
                True)
116
  | Ret e => eval_expr_valid e E
Heiko Becker's avatar
Heiko Becker committed
117
118
119
120
121
122
123
124
125
126
127
128
  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
Heiko Becker's avatar
Heiko Becker committed
129
    let fexpr := Fcore_FLT.FLT_exp emin prec in
Heiko Becker's avatar
Heiko Becker committed
130
131
132
133
134
135
    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 _ =>
Heiko Becker's avatar
Heiko Becker committed
136
137
        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)
Heiko Becker's avatar
Heiko Becker committed
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
      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;
Heiko Becker's avatar
Heiko Becker committed
154
      try rewrite P2R_INR, INR_IPR; lra.
Heiko Becker's avatar
Heiko Becker committed
155
156
157
158
159
  - 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
160
      destruct (Z.pow_pos 2 p); try rewrite P2R_INR, INR_IPR; auto.
Heiko Becker's avatar
Heiko Becker committed
161
    + unfold Z2R, IZR. unfold Qinv; simpl.
Heiko Becker's avatar
Heiko Becker committed
162
      destruct (Z.pow_pos 2 p) eqn:? ; try rewrite P2R_INR, INR_IPR; simpl; try lra.
Heiko Becker's avatar
Heiko Becker committed
163
164
165
166
167
168
169
      * 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
170
171
172
173
174
      * 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
175
176
177
        rewrite H0 in H1; lra.
Qed.

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

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

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

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

216
Fixpoint noDowncast (V:Type) (e:expr V) :=
Heiko Becker's avatar
Heiko Becker committed
217
218
219
220
221
  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
222
  | Fma e1 e2 e3 => noDowncast e1 /\ noDowncast e2 /\ noDowncast e3
Heiko Becker's avatar
Heiko Becker committed
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
  | 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 *;
242
      unfold maxValue, minValue_pos, maxExponent, minExponentPos in*;
Heiko Becker's avatar
Heiko Becker committed
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
      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.

292
Lemma typing_expr_64_bit e:
Heiko Becker's avatar
Heiko Becker committed
293
294
295
296
297
298
  forall Gamma tMap,
    noDowncast e ->
    is64BitEval e ->
    typeCheck e Gamma tMap = true ->
    (forall v,
        NatSet.In v (usedVars e) -> Gamma v = Some M64) ->
299
    FloverMap.find e tMap = Some M64.
Heiko Becker's avatar
Heiko Becker committed
300
301
Proof.
  induction e; intros * noDowncast_e is64BitEval_e typecheck_e types_valid;
Heiko Becker's avatar
Heiko Becker committed
302
    cbn in *; try inversion noDowncast_e;
303
      subst; Flover_compute; try congruence;
Heiko Becker's avatar
Heiko Becker committed
304
305
306
307
        type_conv; subst.
  - rewrite types_valid in *; try set_tac.
  - destruct m; try congruence.
  - erewrite IHe in *; eauto.
Heiko Becker's avatar
Heiko Becker committed
308
309
310
311
312
  - repeat (match goal with
            |H: _ /\ _ |- _=> destruct H
            end).
      erewrite IHe1 in *; eauto.
    + erewrite IHe2 in *; eauto.
Heiko Becker's avatar
Heiko Becker committed
313
314
315
316
      * unfold join in *.
        destr_factorize.
        rewrite <- isMorePrecise_morePrecise.
        rewrite isMorePrecise_refl. inversion Heqo0; auto.
Heiko Becker's avatar
Heiko Becker committed
317
318
319
      * intros.
        apply types_valid. set_tac.
    + intros; apply types_valid; set_tac.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
320
321
322
  - repeat (match goal with
            |H: _ /\ _ |- _=> destruct H
            end).
323
324
325
326
327
328
329
330
    erewrite IHe1 in *; eauto; try (intros; apply types_valid; set_tac; fail).
    erewrite IHe2 in *; eauto; try (intros; apply types_valid; set_tac; fail).
    unfold join3, join in *.
    erewrite IHe3 in *; eauto; try (intros; apply types_valid; set_tac; fail).
    repeat destr_factorize.
    repeat rewrite <- isMorePrecise_morePrecise.
    repeat rewrite isMorePrecise_refl;
      type_conv; subst; auto.
Heiko Becker's avatar
Heiko Becker committed
331
332
333
334
335
336
337
338
339
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) ->
340
    FloverMap.find (getRetExp f) tMap = Some M64.
Heiko Becker's avatar
Heiko Becker committed
341
342
Proof.
  induction f; intros * noDowncast_f is64BitEval_f typecheck_f types_valid;
Heiko Becker's avatar
Heiko Becker committed
343
    cbn in *;
344
    subst; try eauto using typing_expr_64_bit;
345
      Flover_compute; try congruence.
Heiko Becker's avatar
Heiko Becker committed
346
347
348
349
350
351
352
353
354
355
356
357
  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.

358
Lemma typing_agrees_expr e:
Heiko Becker's avatar
Heiko Becker committed
359
360
  forall E Gamma tMap v m1 m2,
    typeCheck e Gamma tMap = true ->
361
    eval_expr E Gamma (toRExp e) v m1 ->
362
    FloverMap.find e tMap = Some m2 ->
Heiko Becker's avatar
Heiko Becker committed
363
364
    m1 = m2.
Proof.
Heiko Becker's avatar
Heiko Becker committed
365
  induction e; intros * typeCheck_e eval_e tMap_e; cbn in *;
Heiko Becker's avatar
Heiko Becker committed
366
    rewrite tMap_e in *;
Heiko Becker's avatar
Heiko Becker committed
367
    inversion eval_e; subst; cbn in *;
368
      Flover_compute; try congruence; type_conv; subst; try auto.
Heiko Becker's avatar
Heiko Becker committed
369
370
  - eapply IHe; eauto.
  - eapply IHe; eauto.
371
372
  - assert (m0 = m) by eauto using IHe1.
    assert (m3 = m1) by eauto using IHe2.
Heiko Becker's avatar
Heiko Becker committed
373
    subst; auto.
374
375
376
  - assert (m0 = m) by eauto using IHe1.
    assert (m3 = m1) by eauto using IHe2.
    assert (m4 = m5) by eauto using IHe3.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
377
    subst; auto.
Heiko Becker's avatar
Heiko Becker committed
378
379
380
381
382
383
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 ->
384
    FloverMap.find (getRetExp f) tMap = Some m2 ->
Heiko Becker's avatar
Heiko Becker committed
385
386
    m1 = m2.
Proof.
Heiko Becker's avatar
Heiko Becker committed
387
  induction f; intros * typeCheck_f eval_f tMap_f; cbn in *;
388
    Flover_compute; try congruence; type_conv; subst.
Heiko Becker's avatar
Heiko Becker committed
389
  - inversion eval_f; subst; simpl in *.
Heiko Becker's avatar
Heiko Becker committed
390
391
    specialize (IHf (updEnv n v0 E) (updDefVars n m3 Gamma) tMap v m1 m2).
    apply IHf; auto.
392
  - inversion eval_f; subst; eapply typing_agrees_expr; eauto.
Heiko Becker's avatar
Heiko Becker committed
393
394
395
Qed.

Lemma round_0_zero:
Heiko Becker's avatar
Heiko Becker committed
396
  (Fcore_generic_fmt.round radix2 (Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
Heiko Becker's avatar
Heiko Becker committed
397
398
399
400
401
402
403
404
405
406
407
408
409
410
                           (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
411
  unfold Fcore_generic_fmt.canonic_exp.
Heiko Becker's avatar
Heiko Becker committed
412
413
414
415
416
417
418
419
420
421
422
423
424
  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
425
          (Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
Heiko Becker's avatar
Heiko Becker committed
426
427
428
429
430
          (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
431
  pose proof (fexp_correct 53 1024 eq_refl) as fexpr_corr.
Heiko Becker's avatar
Heiko Becker committed
432
  assert (forall k : Z, (-1022 < k)%Z ->
Heiko Becker's avatar
Heiko Becker committed
433
                     (53 <= k - Fcore_FLT.FLT_exp (3 - 1024 - 53) 53 k)%Z)
434
    as expr_valid.
Heiko Becker's avatar
Heiko Becker committed
435
  { intros k k_pos.
Heiko Becker's avatar
Heiko Becker committed
436
    unfold Fcore_FLT.FLT_exp; simpl.
Heiko Becker's avatar
Heiko Becker committed
437
    destruct (Z.max_spec_le (k - 53) (-1074)); omega. }
Heiko Becker's avatar
Heiko Becker committed
438
  pose proof (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53)
439
                                  (-1022)%Z 53%Z expr_valid)
Heiko Becker's avatar
Heiko Becker committed
440
441
442
443
444
445
446
447
    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.
448
      unfold minValue_pos, Z.pow_pos; simpl.
Heiko Becker's avatar
Heiko Becker committed
449
450
451
452
453
454
455
456
457
458
459
460
461
      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.
Heiko Becker's avatar
Heiko Becker committed
462
463
        unfold Qnum, Qden. rewrite <- Z2R_IZR. unfold IZR.
        repeat rewrite <- INR_IPR. simpl. lra.
Heiko Becker's avatar
Heiko Becker committed
464
465
      * unfold Denormal in *. destruct denormal_v.
        eapply Rlt_trans; eauto.
466
        unfold minValue_pos, minExponentPos, bpow.
Heiko Becker's avatar
Heiko Becker committed
467
468
        rewrite Q2R_inv.
        { unfold Q2R, Qnum, Qden.
Heiko Becker's avatar
Heiko Becker committed
469
470
          rewrite <- Z2R_IZR; unfold IZR.
          repeat rewrite <- INR_IPR; simpl; lra. }
Heiko Becker's avatar
Heiko Becker committed
471
        { vm_compute; congruence. }
Heiko Becker's avatar
Heiko Becker committed
472
      * rewrite zero_v. simpl. rewrite Rabs_R0. lra.
Heiko Becker's avatar
Heiko Becker committed
473
474
475
  - rewrite zero_v.
    pose proof round_0_zero. simpl in H. rewrite H.
    rewrite Rabs_R0.
Heiko Becker's avatar
Heiko Becker committed
476
    lra.
Heiko Becker's avatar
Heiko Becker committed
477
478
Qed.

479
(* (fexpr_correct 53 1024 eq_refl) as fexpr_corr. *)
Heiko Becker's avatar
Heiko Becker committed
480
(* (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53) *)
481
(*                                     (-1022)%Z 53%Z) *)
482
Lemma eval_expr_gives_IEEE (e:expr fl64) :
Heiko Becker's avatar
Heiko Becker committed
483
484
  forall E1 E2 E2_real Gamma tMap vR A P fVars dVars,
    (forall x, (toREnv E2) x = E2_real x) ->
485
    typeCheck (B2Qexpr e) Gamma tMap = true ->
Heiko Becker's avatar
Heiko Becker committed
486
    approxEnv E1 Gamma A fVars dVars E2_real ->
487
488
489
490
491
492
493
494
    validIntervalbounds (B2Qexpr e) A P dVars = true ->
    validErrorbound (B2Qexpr e) tMap A dVars = true ->
    FPRangeValidator (B2Qexpr e) A tMap dVars = true ->
    eval_expr (toREnv E2) Gamma (toRExp (B2Qexpr e)) vR M64 ->
    NatSet.Subset ((usedVars (B2Qexpr e)) -- dVars) fVars ->
    is64BitEval (B2Qexpr e) ->
    noDowncast (B2Qexpr e) ->
    eval_expr_valid e E2 ->
Heiko Becker's avatar
Heiko Becker committed
495
496
497
    dVars_range_valid dVars E1 A ->
    fVars_P_sound fVars E1 P ->
    vars_typed (NatSet.union fVars dVars) Gamma ->
Heiko Becker's avatar
Heiko Becker committed
498
499
500
      (forall v,
        NatSet.In v dVars ->
        exists vF m,
501
        (E2_real v = Some vF /\ FloverMap.find (Var Q v) tMap = Some m /\
Heiko Becker's avatar
Heiko Becker committed
502
        validFloatValue vF m)) ->
503
      (forall v, NatSet.In v (usedVars (B2Qexpr e)) -> Gamma v = Some M64) ->
Heiko Becker's avatar
Heiko Becker committed
504
      exists v,
505
506
        eval_expr_float e E2 = Some v /\
        eval_expr (toREnv E2) Gamma (toRExp (B2Qexpr e)) (Q2R (B2Q v)) M64.
507
Proof.
Heiko Becker's avatar
Heiko Becker committed
508
509
510
511
512
513
  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;
514
    (match_pat (eval_expr _ _ _ _ _) (fun H => inversion H; subst; simpl in *));
515
     Flover_compute_asm; try congruence; type_conv; subst;
Heiko Becker's avatar
Heiko Becker committed
516
     unfold Ltacs.optionLift.
Heiko Becker's avatar
Heiko Becker committed
517
518
519
520
521
  - 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.
522
523
    eapply (Const_dist') with (delta:=0%R); eauto.
    + rewrite Rabs_R0; apply mTypeToR_pos_R.
Heiko Becker's avatar
Heiko Becker committed
524
525
    + unfold perturb. lra.
  - edestruct IHe as [v_e [eval_float_e eval_rel_e]]; eauto.
Heiko Becker's avatar
Heiko Becker committed
526
527
528
529
530
531
532
533
534
535
    assert (is_finite 53 1024 v_e = true).
    { apply validValue_is_finite.
      eapply FPRangeValidator_sound; eauto.
      eapply eval_eq_env; eauto. }
    rewrite eval_float_e.
    exists (b64_opp v_e); split; try auto.
    unfold b64_opp. rewrite <- (is_finite_Bopp _ _ pair) in H.
    rewrite B2Q_B2R_eq; auto. rewrite B2R_Bopp.
    eapply Unop_neg'; eauto.
    unfold evalUnop. rewrite is_finite_Bopp in H. rewrite B2Q_B2R_eq; auto.
Heiko Becker's avatar
Heiko Becker committed
536
537
538
  - repeat (match goal with
            |H: _ /\ _ |- _ => destruct H
            end).
539
540
541
    assert (FloverMap.find (B2Qexpr e1) tMap = Some M64 /\
            FloverMap.find (B2Qexpr e2) tMap = Some M64 /\
            FloverMap.find (Binop b (B2Qexpr e1) (B2Qexpr e2)) tMap = Some M64)
Heiko Becker's avatar
Heiko Becker committed
542
           as [tMap_e1 [tMap_e2 tMap_b]].
543
    { repeat split; apply (typing_expr_64_bit _ Gamma); simpl; auto.
Heiko Becker's avatar
Heiko Becker committed
544
545
      - intros; apply usedVars_64bit; set_tac.
      - intros; apply usedVars_64bit; set_tac.
Heiko Becker's avatar
Heiko Becker committed
546
      - rewrite Heqo, Heqo4, Heqo6.
Heiko Becker's avatar
Heiko Becker committed
547
548
549
550
        apply Is_true_eq_true; apply andb_prop_intro; split.
        + apply andb_prop_intro; split; apply Is_true_eq_left; auto.
          apply mTypeEq_refl.
        + apply Is_true_eq_left; auto. }
Heiko Becker's avatar
Heiko Becker committed
551
    repeat destr_factorize.
Heiko Becker's avatar
Heiko Becker committed
552
    assert (m1 = M64).
553
    { eapply (typing_agrees_expr (B2Qexpr e1)); eauto. }
Heiko Becker's avatar
Heiko Becker committed
554
    assert (m2 = M64).
555
    { eapply typing_agrees_expr; eauto. }
Heiko Becker's avatar
Heiko Becker committed
556
557
558
559
560
561
562
563
564
565
    subst.
    destruct (IHe1 E1 E2 E2_real Gamma tMap v1 A P fVars dVars)
      as [v_e1 [eval_float_e1 eval_rel_e1]];
      try auto; try set_tac;
        [ intros; apply usedVars_64bit ; set_tac | ].
    destruct (IHe2 E1 E2 E2_real Gamma tMap v2 A P fVars dVars)
      as [v_e2 [eval_float_e2 eval_rel_e2]];
      try auto; try set_tac;
        [ intros; apply usedVars_64bit ; set_tac | ].
    rewrite eval_float_e1, eval_float_e2.
566
    edestruct (validIntervalbounds_sound (B2Qexpr e2))
Heiko Becker's avatar
Heiko Becker committed
567
568
569
570
      as [iv_2 [err_2 [nR2 [map_e2 [eval_real_e2 e2_bounded_real]]]]];
      eauto; set_tac.
    destr_factorize.
    destruct iv_2 as [ivlo_2 ivhi_2].
Heiko Becker's avatar
Heiko Becker committed
571
    assert (forall vF2 m2,
572
               eval_expr E2_real Gamma (toRExp (B2Qexpr e2)) vF2 m2 ->
Heiko Becker's avatar
Heiko Becker committed
573
574
               (Rabs (nR2 - vF2) <= Q2R err_2))%R.
    { eapply validErrorbound_sound; try eauto; try set_tac. }
Heiko Becker's avatar
Heiko Becker committed
575
576
    assert (contained (Q2R (B2Q v_e2))
                      (widenInterval
Heiko Becker's avatar
Heiko Becker committed
577
                         (Q2R ivlo_2, Q2R ivhi_2) (Q2R err_2))).
Heiko Becker's avatar
Heiko Becker committed
578
579
580
581
582
583
    { eapply distance_gives_iv.
      - simpl. eapply e2_bounded_real.
      - eapply H11. instantiate(1:=M64).
        eapply eval_eq_env; eauto. }
    assert (b = Div -> (Q2R (B2Q v_e2)) <> 0%R).
    { intros; subst; simpl in *.
Heiko Becker's avatar
Heiko Becker committed
584
585
586
      andb_to_prop R3.
      apply le_neq_bool_to_lt_prop in L3.
      destruct L3; hnf; intros.
Heiko Becker's avatar
Heiko Becker committed
587
588
589
590
591
592
593
594
      - 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).
595
    { eapply (FPRangeValidator_sound (Binop b (B2Qexpr e1) (B2Qexpr e2)));
Heiko Becker's avatar
Heiko Becker committed
596
597
        try eauto; set_tac.
      - eapply eval_eq_env; eauto.
598
599
        eapply Binop_dist' with (delta:=0%R); eauto.
        + rewrite Rabs_R0. apply mTypeToR_pos_R.
Heiko Becker's avatar
Heiko Becker committed
600
        + unfold perturb; lra.
601
      - Flover_compute.
Heiko Becker's avatar
Heiko Becker committed
602
603
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro); split; try auto using Is_true_eq_left.
604
      - Flover_compute.
Heiko Becker's avatar
Heiko Becker committed
605
606
607
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro); split; try auto using Is_true_eq_left.
        apply andb_prop_intro; split; auto using Is_true_eq_left.
Heiko Becker's avatar
Heiko Becker committed
608
      - inversion Heqo1; subst. rewrite Heqo0. rewrite Heqo.
Heiko Becker's avatar
Heiko Becker committed
609
610
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left.
Heiko Becker's avatar
Heiko Becker committed
611
612
613
        rewrite Heqo3, Heqo5.
        apply Is_true_eq_left. inversion Heqo2; subst. auto.
      - rewrite Heqo, Heqo0.
Heiko Becker's avatar
Heiko Becker committed
614
        apply Is_true_eq_true.
Heiko Becker's avatar
Heiko Becker committed
615
        inversion Heqo1; inversion Heqo2; subst.
Heiko Becker's avatar
Heiko Becker committed
616
617
        repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left. }
    assert (validFloatValue (Q2R (B2Q v_e1)) M64).
618
    { eapply (FPRangeValidator_sound (B2Qexpr e1)); try eauto; try set_tac.
Heiko Becker's avatar
Heiko Becker committed
619
620
      eapply eval_eq_env; eauto. }
    assert (validFloatValue (Q2R (B2Q v_e2)) M64).
621
    { eapply (FPRangeValidator_sound (B2Qexpr e2)); try eauto; try set_tac.
Heiko Becker's avatar
Heiko Becker committed
622
623
624
625
626
627
628
629
630
631
      - 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.
632
      eapply FPRangeValidator_sound with (e:=Binop b (B2Qexpr e1) (B2Qexpr e2)); eauto.
Heiko Becker's avatar
Heiko Becker committed
633
634
      - eapply eval_eq_env; eauto.
        eapply Binop_dist' with (delta:=eps); eauto.
635
636
637
638
        + simpl in H2. Transparent mTypeToQ. unfold mTypeToQ.
          eapply Rle_trans; eauto.
          simpl. lra.
        + unfold perturb. repeat rewrite B2Q_B2R_eq; try auto.
639
      - cbn. Flover_compute.
Heiko Becker's avatar
Heiko Becker committed
640
641
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
642
      - cbn. Flover_compute.
Heiko Becker's avatar
Heiko Becker committed
643
644
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
645
      - cbn. Flover_compute.
646
        inversion Heqo1; inversion Heqo2; subst.
Heiko Becker's avatar
Heiko Becker committed
647
648
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
649
      - cbn. Flover_compute.
650
        inversion Heqo1; inversion Heqo2; subst.
Heiko Becker's avatar
Heiko Becker committed
651
652
653
654
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left). }
    assert (b = Div -> (Q2R (B2Q v_e2)) <> 0%R) as no_div_zero_float.
    { intros; subst; simpl in *.
655
656
657
      andb_to_prop R3.
      apply le_neq_bool_to_lt_prop in L3.
      destruct L3 as [case_low | case_high]; hnf; intros.
Heiko Becker's avatar
Heiko Becker committed
658
659
660
661
662
663
664
      - 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
665
    usedVars_sound R2 R1 L1 L R6 L0 R3 R4 L2 R5 R7 L5 Heqo Heqo0 Heqo1 IHe1
Heiko Becker's avatar
Heiko Becker committed
666
    IHe2.
Heiko Becker's avatar
Heiko Becker committed
667
    pose proof (fexp_correct 53 1024 eq_refl) as fexpr_corr.
Heiko Becker's avatar
Heiko Becker committed
668
    assert (forall k : Z, (-1022 < k)%Z ->
Heiko Becker's avatar
Heiko Becker committed
669
                     (53 <= k - Fcore_FLT.FLT_exp (3 - 1024 - 53) 53 k)%Z)
670
      as expr_valid.
Heiko Becker's avatar
Heiko Becker committed
671
    { intros k k_pos.
Heiko Becker's avatar
Heiko Becker committed
672
      unfold Fcore_FLT.FLT_exp; simpl.
Heiko Becker's avatar
Heiko Becker committed
673
      destruct (Z.max_spec_le (k - 53) (-1074)); omega. }
Heiko Becker's avatar
Heiko Becker committed
674
    pose proof (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53)
675
                                    (-1022)%Z 53%Z expr_valid)
Heiko Becker's avatar
Heiko Becker committed
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
      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.
694
        unfold minValue_pos, minExponentPos in H1.
Heiko Becker's avatar
Heiko Becker committed
695
696
697
698
699
        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.
Heiko Becker's avatar
Heiko Becker committed
700
        simpl in H1. rewrite <- INR_IPR in H1. simpl in H1. lra. }
Heiko Becker's avatar
Heiko Becker committed
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
    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.
719
720
721
        { rewrite Rabs_R0; apply mTypeToR_pos_R. }
        { unfold perturb, evalBinop. cbn.
        repeat rewrite B2Q_B2R_eq; try auto; lra. }
Heiko Becker's avatar
Heiko Becker committed
722
723
724
725
726
      * simpl in *.
        destruct (rel_error_exists
                    (fun x => negb (Zeven x))
                    (B2R 53 1024 v_e1 + B2R 53 1024 v_e2)%R)
          as [eps [eps_bounded round_eq]].
727
        { eapply Rle_trans; eauto. unfold minValue_pos, minExponentPos.
Heiko Becker's avatar
Heiko Becker committed
728
729
730
731
732
733
734
735
          rewrite Q2R_inv; [ | vm_compute; congruence].
          unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
          vm_compute. lra. }
        { exists (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.
736
          - cbn; lra.
Heiko Becker's avatar
Heiko Becker committed
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
          - 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.
756
757
        rewrite Rabs_R0; apply mTypeToR_pos_R.
        unfold perturb, evalBinop; cbn.
Heiko Becker's avatar
Heiko Becker committed
758
759
760
761
762
763
        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]].
764
        { eapply Rle_trans; eauto. unfold minValue_pos, minExponentPos.
Heiko Becker's avatar
Heiko Becker committed
765
766
767
768
769
770
771
772
          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.
773
774
          - cbn; lra.
          - unfold perturb, evalBinop; cbn.
Heiko Becker's avatar
Heiko Becker committed
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
            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.
793
794
        rewrite Rabs_R0; apply mTypeToR_pos_R.
        unfold perturb, evalBinop; cbn.
Heiko Becker's avatar
Heiko Becker committed
795
796
797
798
799
800
801
802
        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]].
803
        { eapply Rle_trans; eauto. unfold minValue_pos, minExponentPos.
Heiko Becker's avatar
Heiko Becker committed
804
805
806
807
808
809
810
811
          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.
812
          - cbn; lra.
Heiko Becker's avatar
Heiko Becker committed
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
          - 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.
834
835
        rewrite Rabs_R0; apply mTypeToR_pos_R.
        unfold perturb, evalBinop; cbn.
Heiko Becker's avatar
Heiko Becker committed
836
837
838
839
840
841
842
        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]].
843
        { eapply Rle_trans; eauto. unfold minValue_pos, minExponentPos.
Heiko Becker's avatar
Heiko Becker committed
844
845
846
847
848
849
850
851
          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.
852
          - cbn; lra.
Heiko Becker's avatar
Heiko Becker committed
853
854
855
856
          - 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
857
858
859
  - repeat (match goal with
            |H: _ /\ _ |- _ => destruct H
            end).
860
861
862
863
    assert (FloverMap.find (B2Qexpr e1) tMap = Some M64 /\
            FloverMap.find (B2Qexpr e2) tMap = Some M64 /\
            FloverMap.find (B2Qexpr e3) tMap = Some M64 /\
            FloverMap.find (Fma (B2Qexpr e1) (B2Qexpr e2) (B2Qexpr e3)) tMap = Some M64)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
864
           as [tMap_e1 [tMap_e2 [tMap_e3 tMap_fma]]].
865
    { repeat split; apply (typing_expr_64_bit _ Gamma); simpl; auto.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
866
867
868
      - intros; apply usedVars_64bit; set_tac.
      - intros; apply usedVars_64bit; set_tac.
      - intros; apply usedVars_64bit; set_tac.
869
      - rewrite Heqo, Heqo4, Heqo6, Heqo8.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
870
871
872
873
874
875
876
877
        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. }
878
    repeat destr_factorize.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
879
880
    inversion Heqo; inversion Heqo0; inversion Heqo1; inversion Heqo2; subst.
    assert (m1 = M64).
881
    { eapply (typing_agrees_expr (B2Qexpr e1)); eauto. }
Nikita Zyuzin's avatar
Nikita Zyuzin committed
882
    assert (m2 = M64).
883
    { eapply (typing_agrees_expr (B2Qexpr e2)); eauto. }
Nikita Zyuzin's avatar
Nikita Zyuzin committed
884
    assert (m3 = M64).
885
    { eapply (typing_agrees_expr (B2Qexpr e3)); eauto. }
Nikita Zyuzin's avatar
Nikita Zyuzin committed
886
887
888
889
890
891
892
893
894
    subst.
    destruct (IHe1 E1 E2 E2_real Gamma tMap v1 A P fVars dVars)
      as [v_e1 [eval_float_e1 eval_rel_e1]];
      try auto; try set_tac;
        [ intros; apply usedVars_64bit ; set_tac | ].
    destruct (IHe2 E1 E2 E2_real Gamma tMap v2 A P fVars dVars)
      as [v_e2 [eval_float_e2 eval_rel_e2]];
      try auto; try set_tac;
        [ intros; apply usedVars_64bit ; set_tac | ].
895
896
897
898
899
900
901
902
    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
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
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 ->
920
921
922
    dVars_range_valid dVars E1 A ->
    fVars_P_sound fVars E1 P ->
    vars_typed (NatSet.union fVars dVars) Gamma ->
Heiko Becker's avatar
Heiko Becker committed
923
924
925
      (forall v,
        NatSet.In v dVars ->
        exists vF m,
926
        (E2_real v = Some vF /\ FloverMap.find (Var Q v) tMap= Some m /\
Heiko Becker's avatar
Heiko Becker committed
927
928
929
930
931
932
933
934
935
936
        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
937
                     dVars_sound fVars_defined vars_typed dVars_valid
Heiko Becker's avatar
Heiko Becker committed
938
                     freeVars_typed;
939
    cbn in *; Flover_compute_asm; try congruence; type_conv; subst;
940
941
      unfold Ltacs.optionLift;
      inversion bstep_float; inversion bstep_real;
Heiko Becker's avatar
Heiko Becker committed
942
943
944
945
      inversion ssa_f; subst; simpl in *;
        repeat (match goal with
                | H: _ = true |- _ => andb_to_prop H
                end).
946
947
  - assert (FloverMap.find (B2Qexpr e) tMap= Some M64).
    { eapply typing_expr_64_bit; try eauto.
Heiko Becker's avatar
Heiko Becker committed
948
949
950
      simpl in *; destruct nodowncast_f; auto.
      destruct is64_eval; auto.
      intros; apply freeVars_typed.
951
      set_tac.
Heiko Becker's avatar
Heiko Becker committed
952
953
954
955
      split; [ set_tac | ].
      hnf; intros; subst.
      apply H26.
      apply (H25 n H).  }
956
    assert (m1 = M64).
957
    { eapply typing_agrees_expr; eauto. }
Heiko Becker's avatar
Heiko Becker committed
958
    subst.
959
960
    assert (exists v_e, eval_expr_float e E2 = Some v_e /\
                   eval_expr (toREnv E2) Gamma (toRExp (B2Qexpr e)) (Q2R (B2Q v_e)) M64)
Heiko Becker's avatar
Heiko Becker committed
961
           as eval_float_e.
962
    { eapply eval_expr_gives_IEEE; try eauto.
Heiko Becker's avatar
Heiko Becker committed
963
964
965
966
967
968
969
970
971
972
973
      - 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.
974
975
        specialize (H25 n H0).
        set_tac.  apply H26; set_tac. }
Heiko Becker's avatar
Heiko Becker committed
976
    destruct eval_float_e as [v_e [eval_float_e eval_rel_e]].
977
    assert (forall v m, eval_expr E2_real Gamma (toRExp (B2Qexpr e)) v m ->
978
                   Rabs (v0 - v) <= Q2R e2)%R
Heiko Becker's avatar
Heiko Becker committed
979
980
981
982
      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.
983
984
        destruct H25; try auto; congruence. }
    assert (Rabs (v0 - (Q2R (B2Q v_e))) <= Q2R e2)%R.
Heiko Becker's avatar
Heiko Becker committed
985
986
987
    { 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 *)
988
989
    (* destruct (A (getRetExp (B2Qcmd f))) as [iv_f err_f] eqn:A_f. *)
    (* destruct iv_f as [ivlo_f ivhi_f]. *)
Heiko Becker's avatar
Heiko Becker committed
990
991
992
993
    edestruct (validIntervalboundsCmd_sound) as [iv_ret [err_ret [v_ret
                                                                    [map_ret
                                                                       [eval_ret bound_ret]]]]];
      eauto.
994
    { cbn. Flover_compute.
Heiko Becker's avatar
Heiko Becker committed
995
      rewrite L0, R4, R3, R2. auto. }
Heiko Becker's avatar
Heiko Becker committed
996
    assert (exists vF m, bstep (toRCmd (B2Qcmd f)) (updEnv n (Q2R (B2Q v_e)) E2_real) (updDefVars n M64 Gamma) vF m).
Heiko Becker's avatar
Heiko Becker committed
997
998
999
1000
    { eapply validErrorboundCmd_gives_eval with (E1 := updEnv n v0 E1)
                                                  (elo:=fst(iv_ret))
                                                  (ehi:=snd(iv_ret))
                                                  (err:= err_ret); eauto.
Heiko Becker's avatar
Heiko Becker committed
1001
1002
1003
      - eapply approxUpdBound; eauto.
        rewrite Qeq_bool_iff in R1.
        eapply Rle_trans; eauto.
1004
1005
        canonize_hyps. rewrite <- R1.
        inversion Heqo0; subst; lra.
Heiko Becker's avatar
Heiko Becker committed
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
      - 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.
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
      - unfold dVars_range_valid in *. intros. unfold updEnv. set_tac.
        destruct H1; subst.
        + exists v0, (q1, q2), e1; split; try eauto.
          * rewrite Nat.eqb_refl; auto.
          * split; try auto.
            edestruct validIntervalbounds_sound
              as [iv_e [err_e [v_e' [map_e [? ?]]]]]; eauto.
            { set_tac; split; try auto. split; try auto.
              hnf; intros. eapply H26. subst; set_tac. }
            simpl. destr_factorize; simpl in *.
            canonize_hyps. rewrite <- R4, <- R3.
            rewrite <- (meps_0_deterministic _ H17 H1) in H2; auto.
        + destruct H1.
          rewrite <- Nat.eqb_neq in H1.
          rewrite H1.
Heiko Becker's avatar
Heiko Becker committed
1039
          apply dVars_sound; auto.
Heiko Becker's avatar
Heiko Becker committed
1040
      - unfold fVars_P_sound; intros; unfold updEnv.
Heiko Becker's avatar
Heiko Becker committed
1041
1042
1043
        destruct (v1 =? n) eqn:?.
        + rewrite Nat.eqb_eq in Heqb; subst; exfalso.
          set_tac. apply H26; rewrite NatSet.union_spec; auto.
Heiko Becker's avatar
Heiko Becker committed
1044
1045
1046
        + apply fVars_defined; auto.
      - unfold IntervalValidation.vars_typed. intros.
        unfold updDefVars. destruct (v1 =? n) eqn:?.
Heiko Becker's avatar
Heiko Becker committed
1047
1048
1049
1050
        + exists M64; auto.
        + apply vars_typed.
          rewrite Nat.eqb_neq in Heqb.
          rewrite NatSet.union_spec, NatSet.add_spec in H1.
Heiko Becker's avatar
Heiko Becker committed
1051
1052
1053
1054
          rewrite NatSet.union_spec.
          destruct H1 as [HA |[HB | HC]]; try auto; congruence.
      - destruct iv_ret; auto.
    }
Heiko Becker's avatar
Heiko Becker committed
1055
    unfold optionLift. rewrite eval_float_e.
1056
    assert (FloverMap.find (getRetExp (B2Qcmd f)) tMap= Some M64).
Heiko Becker's avatar
Heiko Becker committed
1057
    { eapply typingSoundnessCmd; eauto. }
Heiko Becker's avatar
Heiko Becker committed
1058
1059
    destruct H1 as [vF_new [m_f bstep_float_new]].
    assert (m_f = M64).
Heiko Becker's avatar
Heiko Becker committed
1060
    { eapply typing_agrees_cmd; eauto. }
Heiko Becker's avatar
Heiko Becker committed
1061
1062
1063
1064
1065
1066
    subst.
    destruct (IHf (updEnv n v0 E1) (updFlEnv n v_e E2)
                  (updEnv n (Q2R (B2Q v_e)) E2_real) (updDefVars n M64 Gamma) tMap
                  vR vF_new A P fVars (NatSet.add n dVars) outVars); try eauto.
    + intros. unfold toREnv, updFlEnv, updEnv.
      destruct (x =? n); auto. rewrite <- envs_eq. unfold toREnv; auto.
Heiko Becker's avatar
Heiko Becker committed
1067
    + eapply approxUpdBound; eauto.
Heiko Becker's avatar
Heiko Becker committed
1068
      eapply Rle_trans; eauto.
Heiko Becker's avatar
Heiko Becker committed
1069
1070
1071
      canonize_hyps.
      inversion Heqo0; subst.
      lra.
Heiko Becker's avatar
Heiko Becker committed
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
    + eapply ssa_equal_set; eauto.
      hnf; split; intros.
      * rewrite NatSet.add_spec, NatSet.union_spec in *.
        rewrite NatSet.add_spec in H1; destruct H1; auto.
        destruct H1; auto.
      * rewrite NatSet.add_spec in H1;
          rewrite NatSet.union_spec, NatSet.add_spec in *;
          destruct H1; auto. destruct H1; auto.
    + eapply (swap_Gamma_bstep (Gamma1:= updDefVars n M0 (toRMap Gamma)));
        eauto.
      intros; unfold updDefVars, toRMap.
      destruct (n0 =? n); auto.
    + eapply (bstep_eq_env (E1 := updEnv n (Q2R (B2Q v_e)) E2_real)); eauto.
      intros x; unfold updEnv, updFlEnv, toREnv.
      destruct (x =? n); try auto.
      rewrite <- envs_eq. auto.
    + hnf; intros. rewrite NatSet.diff_spec in *.
      destruct H1. apply freeVars_sound.
      rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
      split; try auto. split; try auto.
      hnf; intros; subst. apply H3. rewrite NatSet.add_spec. auto.
      rewrite NatSet.add_spec in H3. hnf; intros; apply H3; auto.
    + destruct is64_eval as [HA [HB HC]]; auto.
    + destruct nodowncast_f as [HA HB]; auto.
    + destruct bstep_sound as [eval_sound bstep_sound].
      rewrite eval_float_e in bstep_sound; unfold optionLift in bstep_sound.
      auto.
Heiko Becker's avatar
Heiko Becker committed
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
    + unfold dVars_range_valid in *; intros; unfold updEnv.
      destruct (v1 =? n) eqn:?.
      * set_tac. rewrite Nat.eqb_eq in Heqb; subst.
        destruct H1 as [? | [? ?]]; try congruence.
        exists v0. edestruct validIntervalbounds_sound as [iv_e [err_e [? [? [? ?]]]]]; eauto.
        { set_tac; split; auto. split; auto.
          hnf; intros; subst; set_tac. }
        canonize_hyps.
        destr_factorize; simpl in *.
        exists (q1,q2), e1.
        split; try auto.
        split; try auto.
        simpl in *. rewrite R4, R3 in *.
        rewrite <- (meps_0_deterministic _ H4 H17). auto.
      * eapply dVars_sound; set_tac.
        destruct H1; rewrite Nat.eqb_neq in Heqb; try congruence.
        destruct H1; auto.
    + unfold fVars_P_sound. intros; unfold updEnv.
Heiko Becker's avatar
Heiko Becker committed
1117
1118
1119
1120
      destruct (v1 =? n) eqn:?.
      * rewrite Nat.eqb_eq in Heqb; subst; exfalso.
        set_tac. apply H26; rewrite NatSet.union_spec; auto.
      * apply fVars_defined. auto.
Heiko Becker's avatar
Heiko Becker committed
1121
1122
    + unfold IntervalValidation.vars_typed.
      intros. unfold updDefVars. destruct (v1 =? n) eqn:?.
Heiko Becker's avatar
Heiko Becker committed
1123
1124
1125
      * exists M64; auto.
      * apply vars_typed.
        rewrite Nat.eqb_neq in Heqb.
Heiko Becker's avatar
Heiko Becker committed
1126
1127
1128
        rewrite NatSet.union_spec, NatSet.add_spec in H1.
        rewrite NatSet.union_spec.
        destruct H1 as [HA |[HB | HC]]; try auto; congruence.
Heiko Becker's avatar
Heiko Becker committed
1129
1130
    + intros. rewrite NatSet.add_spec in H1; unfold updEnv.
      destruct (v1 =? n) eqn:?; destruct H1; subst; try congruence.
Heiko Becker's avatar
Heiko Becker committed
1131
1132
      * exists (Q2R (B2Q v_e)).
        exists M64; repeat split; try auto.
Heiko Becker's avatar
Heiko Becker committed
1133
        eapply FPRangeValidator_sound; eauto.
Heiko Becker's avatar
Heiko Becker committed
1134
        { eapply eval_eq_env; eauto. }
Heiko Becker's avatar
Heiko Becker committed
1135
1136
        { set_tac. split; try auto.
          split; try auto.
Heiko Becker's avatar
Heiko Becker committed
1137
          hnf; intros; subst. set_tac. }
Heiko Becker's avatar
Heiko Becker committed
1138