Commit 62199ab1 authored by Heiko Becker's avatar Heiko Becker
Browse files

Prove IEEE connection in Coq, at least without admits for the moment,...

Prove IEEE connection in Coq, at least without admits for the moment, assumptions need to be checked
parent ebcdc69c
......@@ -51,27 +51,31 @@ Definition Binop_to_Rop (b:binop) :=
end.
Definition no_overflow b fl1 fl2 :=
(* TODO: Connect to evaluation *)
let the_val := (Binop_to_Rop b) (B2R 53 1024 fl1) (B2R 53 1024 fl2) in
(Rlt_bool
(Rabs
(Fcore_generic_fmt.round radix2
(Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
(round_mode mode_NE)
the_val ))
the_val))
(bpow radix2 1024) = true).
Definition no_overflow_in_eval :=
forall b e1 e2 E fl1 fl2,
eval_exp_float e1 E = Some fl1 ->
eval_exp_float e2 E = Some fl2 ->
no_overflow b fl1 fl2.
(* TODO: Maybe move to Prop *)
Definition no_underflow b fl1 fl2 :=
let the_val := (Binop_to_Rop b) (B2R 53 1024 fl1) (B2R 53 1024 fl2) in
(Rlt_bool
(bpow radix2 (-1022))
(Rabs
(Fcore_generic_fmt.round radix2
(Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
(round_mode mode_NE)
the_val))
= true).
((bpow radix2 (-1022)) <= (Rabs the_val))%R.
Definition no_underflow_in_eval :=
forall b e1 e2 E fl1 fl2,
eval_exp_float e1 E = Some fl1 ->
eval_exp_float e2 E = Some fl2 ->
no_underflow b fl1 fl2.
Lemma b64_plus_preserves_finite f1 f2:
is_finite 53 1024 (b64_plus mode_NE f1 f2) = true ->
......@@ -106,7 +110,6 @@ Proof.
try congruence; try auto.
Qed.
Lemma b64_mult_preserves_finite f1 f2:
is_finite 53 1024 (b64_mult mode_NE f1 f2) = true ->
is_finite 53 1024 f1 = true /\ is_finite 53 1024 f2 = true.
......@@ -141,11 +144,13 @@ Qed.
Theorem eval_gives_sem e E v:
eval_exp_float e E = Some v ->
no_overflow_in_eval ->
no_underflow_in_eval ->
is_finite 53 1024 v = true ->
eval_exp (Q2R machineEpsilon) (toREnv E) (toRExp e) (B2R 53 1024 v).
Proof.
revert v; induction e;
intros v1 eval_succeeds (*no_overflow*) finite_res;
intros v1 eval_succeeds eval_not_overf eval_not_underf finite_res;
simpl in eval_succeeds.
- econstructor.
unfold toREnv.
......@@ -168,9 +173,11 @@ Proof.
case_eq (eval_exp_float e2 E); intros * eval_float_e2;
rewrite eval_float_e1, eval_float_e2 in *;
try congruence.
(* specialize (IHe1 b0 (refl_equal (Some b0)) no_overflow);
specialize (IHe2 b1 (refl_equal (Some b1)) no_overflow).
specialize (no_overflow (Binop b e1 e2) E). *)
specialize (IHe1 b0 (refl_equal (Some b0)) eval_not_overf eval_not_underf);
specialize (IHe2 b1 (refl_equal (Some b1)) eval_not_overf eval_not_underf).
specialize (eval_not_overf b e1 e2 E b0 b1 eval_float_e1 eval_float_e2).
specialize (eval_not_underf b e1 e2 E b0 b1 eval_float_e1 eval_float_e2).
unfold no_overflow, no_underflow in *.
simpl.
pose proof (fexp_correct 53 1024 eq_refl) as fexp_corr.
pose proof (relative_error_N_ex radix2
......@@ -185,14 +192,11 @@ Proof.
+ specialize (relative_error_binop exp_valid (fun x0 : Z => negb (Zeven x0))).
clear exp_valid fexp_corr.
destruct b.
* pose proof (Bplus_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE b0 b1).
unfold b64_plus in *.
unfold Bplus in *.
finite_b0 finite_b1).
* pose proof (Bplus_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE b0 b1)
as addition_correct.
assert (is_finite 53 1024 b0 = true /\ is_finite 53 1024 b1 = true)
as [finite_b0 finite_b1]
by (apply b64_plus_preserves_finite; auto).
by (apply b64_plus_preserves_finite; inversion eval_succeeds; subst; auto).
assert (eval_exp (Q2R machineEpsilon) (toREnv E) (toRExp e1) (B2R 53 1024 b0))
as eval_e1
by (apply IHe1; auto).
......@@ -200,53 +204,38 @@ Proof.
as eval_e2
by (apply IHe2; auto).
clear IHe1 IHe2.
simpl in *.
remember (179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216)%R as cst.
unfold b64_plus in *.
destruct (
Rlt_bool
(Rabs
(Fcore_generic_fmt.round radix2 (Fcore_FLT.FLT_exp (-1074) 53)
(Fcore_generic_fmt.Znearest (fun x : Z => negb (Zeven x))) (B2R 53 1024 b0 + B2R 53 1024 b1))) cst).
Focus 2.
exfalso; apply no_overflow; auto. ; try congruence; auto).
rewrite H0 in *.
destruct H.
destruct H1.
unfold Binop_to_Rop in eval_not_overf.
specialize (addition_correct finite_b0 finite_b1).
rewrite eval_not_overf in addition_correct.
destruct addition_correct as [add_is_round _].
inversion eval_succeeds; subst.
unfold b64_plus.
rewrite H.
rewrite add_is_round.
assert (exists delta,(Rabs(delta) <= Q2R machineEpsilon)%R /\
Fcore_generic_fmt.round radix2
(Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
(round_mode mode_NE)
(B2R 53 1024 b0 + B2R 53 1024 b1) =
perturb (B2R 53 1024 b0 + B2R 53 1024 b1) delta).
perturb (B2R 53 1024 b0 + B2R 53 1024 b1) delta)
as delta_exists.
{ specialize (relative_error_binop (B2R 53 1024 b0 + B2R 53 1024 b1)%R).
destruct relative_error_binop.
- unfold bpow, radix2.
(* This is the proof that we do not handle denormals! *) admit.
- destruct H3.
unfold round_mode; simpl in *.
rewrite H4.
unfold perturb.
exists x.
destruct relative_error_binop as [eps [abs_less round_eps]].
- auto. (* This is the proof that we do not handle denormals! *)
- unfold round_mode; rewrite round_eps.
unfold perturb; exists eps.
split; try auto.
eapply Rle_trans; eauto.
unfold machineEpsilon.
unfold Q2R.
unfold Qnum, Qden.
assert (2 ^ 53 = 9007199254740992)%positive by (cbv; auto).
rewrite H5.
lra. }
{ destruct H3 as [delta [delta_valid eval_perturb]].
unfold Qnum, Qden. repeat rewrite <- Z2R_IZR.
unfold Z2R. unfold P2R. simpl. lra. }
{ destruct delta_exists as [delta [delta_valid eval_perturb]].
rewrite eval_perturb.
econstructor; eauto.
intros; congruence. }
* assert (is_finite 53 1024 b0 = true /\ is_finite 53 1024 b1 = true)
as [finite_b0 finite_b1]
by (apply b64_minus_preserves_finite; auto).
specialize (IHe1 b0).
specialize (IHe2 b1).
by (apply b64_minus_preserves_finite; inversion eval_succeeds; subst; auto).
assert (eval_exp (Q2R machineEpsilon) (toREnv E) (toRExp e1) (B2R 53 1024 b0))
as eval_e1
by (apply IHe1; auto).
......@@ -254,52 +243,40 @@ Proof.
as eval_e2
by (apply IHe2; auto).
clear IHe1 IHe2.
pose proof (Bminus_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE b0 b1 finite_b0 finite_b1).
assert (Rlt_bool
(Rabs
(Fcore_generic_fmt.round radix2
(Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
(round_mode mode_NE)
(B2R 53 1024 b0 - B2R 53 1024 b1)))
(bpow radix2 1024) = true)
by admit (* TODO: Overflow assumption *).
rewrite H0 in *.
destruct H.
destruct H1.
pose proof (Bminus_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE b0 b1 finite_b0 finite_b1)
as minus_correct.
unfold Binop_to_Rop in eval_not_overf.
rewrite eval_not_overf in minus_correct.
destruct minus_correct as [minus_is_round _].
inversion eval_succeeds; subst.
unfold b64_minus.
rewrite H.
rewrite minus_is_round.
assert (exists delta,(Rabs(delta) <= Q2R machineEpsilon)%R /\
Fcore_generic_fmt.round radix2
(Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
(round_mode mode_NE)
(B2R 53 1024 b0 - B2R 53 1024 b1) =
perturb (B2R 53 1024 b0 - B2R 53 1024 b1) delta).
perturb (B2R 53 1024 b0 - B2R 53 1024 b1) delta)
as delta_exists.
{ specialize (relative_error_binop (B2R 53 1024 b0 - B2R 53 1024 b1)%R).
destruct relative_error_binop.
- unfold bpow, radix2.
(* This is the proof that we do not handle denormals! *) admit.
- destruct H3.
unfold round_mode; simpl in *.
rewrite H4.
unfold perturb.
exists x.
destruct relative_error_binop as [eps [abs_less round_eps]].
- auto. (* This is the proof that we do not handle denormals! *)
- unfold round_mode; rewrite round_eps.
unfold perturb; exists eps.
split; try auto.
eapply Rle_trans; eauto.
unfold machineEpsilon.
unfold Q2R.
unfold Qnum, Qden.
assert (2 ^ 53 = 9007199254740992)%positive by (cbv; auto).
rewrite H5.
lra. }
{ destruct H3 as [delta [delta_valid eval_perturb]].
repeat rewrite <- Z2R_IZR.
unfold Z2R; unfold P2R; simpl. lra. }
{ destruct delta_exists as [delta [delta_valid eval_perturb]].
rewrite eval_perturb.
econstructor; eauto.
intros; congruence. }
* assert (is_finite 53 1024 b0 = true /\ is_finite 53 1024 b1 = true)
as [finite_b0 finite_b1]
by (apply b64_mult_preserves_finite; auto).
specialize (IHe1 b0).
specialize (IHe2 b1).
by (apply b64_mult_preserves_finite; inversion eval_succeeds; subst; auto).
assert (eval_exp (Q2R machineEpsilon) (toREnv E) (toRExp e1) (B2R 53 1024 b0))
as eval_e1
by (apply IHe1; auto).
......@@ -307,60 +284,46 @@ Proof.
as eval_e2
by (apply IHe2; auto).
clear IHe1 IHe2.
pose proof (Bmult_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE b0 b1).
assert (Rlt_bool
(Rabs
(Fcore_generic_fmt.round radix2
(Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
(round_mode mode_NE)
(B2R 53 1024 b0 * B2R 53 1024 b1)))
(bpow radix2 1024) = true)
by admit (* TODO: Overflow assumption *).
rewrite H0 in *.
destruct H.
destruct H1.
(*assert (is_nan 53 1024 (Bmult 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE b0 b1) = false).
{ unfold is_nan, is_finite, b64_mult in *.
destruct (Bmult 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE b0 b1); auto. } *)
pose proof (Bmult_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE b0 b1)
as mult_correct.
unfold Binop_to_Rop in eval_not_overf.
rewrite eval_not_overf in mult_correct.
destruct mult_correct as [mult_round _].
inversion eval_succeeds; subst.
unfold b64_mult.
rewrite H.
rewrite mult_round.
assert (exists delta,(Rabs(delta) <= Q2R machineEpsilon)%R /\
Fcore_generic_fmt.round radix2
(Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
(round_mode mode_NE)
(B2R 53 1024 b0 * B2R 53 1024 b1) =
perturb (B2R 53 1024 b0 * B2R 53 1024 b1) delta).
perturb (B2R 53 1024 b0 * B2R 53 1024 b1) delta)
as delta_exists.
{ specialize (relative_error_binop (B2R 53 1024 b0 * B2R 53 1024 b1)%R).
destruct relative_error_binop.
- unfold bpow, radix2.
(* This is the proof that we do not handle denormals! *) admit.
- destruct H3.
unfold round_mode; simpl in *.
rewrite H4.
unfold perturb.
exists x.
destruct relative_error_binop as [eps [abs_less round_eps]].
- auto. (* This is the proof that we do not handle denormals! *)
- unfold round_mode; rewrite round_eps.
unfold perturb; exists eps.
split; try auto.
eapply Rle_trans; eauto.
unfold machineEpsilon.
unfold Q2R.
unfold Qnum, Qden.
assert (2 ^ 53 = 9007199254740992)%positive by (cbv; auto).
rewrite H5.
lra. }
{ destruct H3 as [delta [delta_valid eval_perturb]].
repeat rewrite <- Z2R_IZR.
unfold Z2R; unfold P2R; simpl. lra. }
{ destruct delta_exists as [delta [delta_valid eval_perturb]].
rewrite eval_perturb.
econstructor; eauto.
intros; congruence. }
* assert (valid_div b1 = true) by (destruct (valid_div b1); congruence).
rewrite H in H0.
inversion H0; subst.
* assert (valid_div b1 = true)
as div_valid
by (destruct (valid_div b1); congruence).
rewrite div_valid in eval_succeeds.
assert (forall sgn, b1 = B754_infinity 53 1024 sgn -> False)
by (intros; unfold valid_div in H; destruct b1; congruence).
by (intros; unfold valid_div in *; destruct b1; congruence).
assert (is_finite 53 1024 b0 = true /\ is_finite 53 1024 b1 = true)
as [finite_b0 finite_b1]
by (apply b64_div_preserves_finite; auto).
specialize (IHe1 b0).
specialize (IHe2 b1).
by (apply b64_div_preserves_finite; inversion eval_succeeds; subst; auto).
assert (eval_exp (Q2R machineEpsilon) (toREnv E) (toRExp e1) (B2R 53 1024 b0))
as eval_e1
by (apply IHe1; auto).
......@@ -368,63 +331,53 @@ Proof.
as eval_e2
by (apply IHe2; auto).
clear IHe1 IHe2.
pose proof (Bdiv_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE b0 b1).
assert (Rlt_bool
(Rabs
(Fcore_generic_fmt.round radix2
(Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
(round_mode mode_NE)
(B2R 53 1024 b0 / B2R 53 1024 b1)))
(bpow radix2 1024) = true)
by admit (* TODO: Overflow assumption *).
pose proof (Bdiv_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE b0 b1)
as div_correct.
unfold Binop_to_Rop in eval_not_overf.
rewrite eval_not_overf in div_correct.
assert (B2R 53 1024 b1 <> 0%R).
{ hnf. intros. unfold B2R in H4. unfold valid_div in H. destruct b1; simpl in H; try congruence.
unfold Fcore_defs.F2R in H4.
simpl in H4.
{ hnf. intros. unfold B2R in H0. unfold valid_div in div_valid. destruct b1; simpl in H; try congruence.
unfold Fcore_defs.F2R in H0.
simpl in H0.
pose proof (bpow_gt_0 radix2 e).
rewrite Z2R_cond_Zopp in H4.
unfold cond_Ropp in H4.
rewrite Z2R_cond_Zopp in H0.
unfold cond_Ropp in H0.
destruct b.
- pose proof (Zgt_pos_0 m).
rewrite Z.gt_lt_iff in H6.
apply Z2R_lt in H6.
apply Rmult_integral in H4.
rewrite Z.gt_lt_iff in H2.
apply Z2R_lt in H2.
apply Rmult_integral in H0.
unfold Z2R in *.
destruct H4; try lra.
destruct H0; try lra.
- pose proof (Zgt_pos_0 m).
rewrite Z.gt_lt_iff in H6.
apply Z2R_lt in H6.
apply Rmult_integral in H4.
unfold Z2R in *; destruct H4; lra. }
rewrite H3 in H2.
destruct H2; try auto.
destruct H5.
rewrite Z.gt_lt_iff in H2.
apply Z2R_lt in H2.
apply Rmult_integral in H0.
unfold Z2R in *; destruct H0; lra. }
destruct div_correct as [round_correct _]; try auto.
inversion eval_succeeds; subst.
unfold b64_div.
rewrite H2.
rewrite round_correct.
assert (exists delta,(Rabs(delta) <= Q2R machineEpsilon)%R /\
Fcore_generic_fmt.round radix2
(Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
(round_mode mode_NE)
(B2R 53 1024 b0 / B2R 53 1024 b1) =
perturb (B2R 53 1024 b0 / B2R 53 1024 b1) delta).
perturb (B2R 53 1024 b0 / B2R 53 1024 b1) delta)
as delta_exists.
{ specialize (relative_error_binop (B2R 53 1024 b0 / B2R 53 1024 b1)%R).
destruct relative_error_binop.
- unfold bpow, radix2.
(* This is the proof that we do not handle denormals! *) admit.
- destruct H7.
unfold round_mode; simpl in *.
rewrite H8.
unfold perturb.
exists x.
destruct relative_error_binop as [eps [abs_less round_eps]].
- auto. (* This is the proof that we do not handle denormals! *)
- unfold round_mode; rewrite round_eps.
unfold perturb; exists eps.
split; try auto.
eapply Rle_trans; eauto.
unfold machineEpsilon.
unfold Q2R.
unfold Qnum, Qden.
assert (2 ^ 53 = 9007199254740992)%positive by (cbv; auto).
rewrite H9.
lra. }
{ destruct H7 as [delta [delta_valid eval_perturb]].
repeat rewrite <- Z2R_IZR.
unfold Z2R; unfold P2R; simpl. lra. }
{ destruct delta_exists as [delta [delta_valid eval_perturb]].
rewrite eval_perturb.
econstructor; eauto. }
Admitted.
\ No newline at end of file
Qed.
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment