Commit f25307fb authored by Arthur Correnson's avatar Arthur Correnson Committed by François Bobot
Browse files

[Farith2] Runtime checks with assertions

+ Add Assert.v module to describe runtime assertions
+ Rename some theorem in Correction_thm.v for better readability
+ Minimal implementation of a GenericFloat module using runtime assertions
parent 1d920615
No preview for this file type
From Flocq Require Import IEEE754.BinarySingleNaN.
From Coq Require Import Program ZArith.
Module Type Inhabited.
Parameter t : Type.
Parameter dummy : t.
End Inhabited.
Module Assert (M : Inhabited).
Program Definition assert (x : bool) (f : x = true -> M.t) : M.t :=
match x with
| true => f _
| false => M.dummy
end.
Lemma assert_spec:
forall (pre : bool) (f : M.t),
pre = true -> assert pre (fun _ => f) = f.
Proof.
intros.
unfold assert.
now rewrite H.
Qed.
End Assert.
Module GenericFloat.
Record F : Type := {
prec : Z;
emax : Z;
Hprec : FLX.Prec_gt_0 prec;
Hemax : Prec_lt_emax prec emax;
value : binary_float prec emax;
}.
Module F_inhab.
Definition t : Type := F.
Program Definition dummy := {|
prec := 24;
emax := 128;
value := BinarySingleNaN.B754_nan;
Hprec := _;
Hemax := _;
|}.
Solve All Obligations with easy.
End F_inhab.
Module AssertF := Assert (F_inhab).
Definition same_format (x y : F) : bool :=
Z.eqb (prec x) (prec y) && Z.eqb (emax x) (emax y).
Program Definition Fadd (m : mode) (x y : F) : F :=
AssertF.assert (same_format x y) (fun _ => {|
prec := prec x;
emax := emax x;
Hprec := Hprec x;
Hemax := Hemax x;
value := _;
|}).
Next Obligation.
apply andb_prop in H as [Hp He].
rewrite Z.eqb_eq in Hp, He.
destruct x as [ ? ? ? ? vx ], y as [ ? ? ? ? vy ]; simpl in *; subst.
apply (Bplus m vx vy).
Defined.
Program Definition Fsub (m : mode) (x y : F) : F :=
AssertF.assert (same_format x y) (fun _ => {|
prec := prec x;
emax := emax x;
Hprec := Hprec x;
Hemax := Hemax x;
value := _;
|}).
Next Obligation.
apply andb_prop in H as [Hp He].
rewrite Z.eqb_eq in Hp, He.
destruct x as [ ? ? ? ? vx ], y as [ ? ? ? ? vy ]; simpl in *; subst.
apply (Bminus m vx vy).
Defined.
End GenericFloat.
......@@ -142,7 +142,7 @@ Proof.
now destruct H as [<- [Hf _]], (Bplus _ _ _).
Qed.
Theorem Bplus_le_compat:
Theorem Bplus_le_mono_l:
forall m (a b c : float),
is_nan (Bplus m a c) = false ->
is_nan (Bplus m b c) = false ->
......@@ -150,46 +150,13 @@ Theorem Bplus_le_compat:
Bplus m a c <= Bplus m b c.
Proof.
intros m a b c Hnan1 Hnan2 Hab.
apply B2Rx_le; try easy.
rewrite (Bplus_correct m a c Hnan1).
rewrite (Bplus_correct m b c Hnan2).
apply B2Rx_le; auto.
repeat (rewrite Bplus_correct; auto).
apply round_le.
apply add_leb_mono_l.
fdestruct a; fdestruct b; simpl.
- apply Raux.Rle_bool_true; lra.
- apply Raux.Rle_bool_true; lra.
- destruct s; simpl; try easy.
unfold Defs.F2R; simpl.
apply Raux.Rle_bool_true.
pose proof (IZR_pos m0).
pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
nra.
- apply Raux.Rle_bool_true; lra.
- apply Raux.Rle_bool_true; lra.
- destruct s; simpl; try easy.
unfold Defs.F2R; simpl.
apply Raux.Rle_bool_true.
pose proof (IZR_pos m0).
pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
nra.
- destruct s; simpl; try easy.
unfold Defs.F2R; simpl.
apply Raux.Rle_bool_true.
pose proof (IZR_neg m0).
pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
nra.
- destruct s; simpl; try easy.
unfold Defs.F2R; simpl.
apply Raux.Rle_bool_true.
pose proof (IZR_neg m0).
pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
nra.
- destruct s, s0; simpl; try easy;
apply Bleb_Rle in Hab; auto;
now apply Raux.Rle_bool_true.
apply (add_leb_mono_l _ _ _ (le_B2Rx _ _ Hab)).
Qed.
Theorem Bplus_le_compat_l:
Theorem Bplus_le_mono_r:
forall m (a b c : float),
is_nan (Bplus m c a) = false ->
is_nan (Bplus m c b) = false ->
......@@ -197,46 +164,13 @@ Theorem Bplus_le_compat_l:
Bplus m c a <= Bplus m c b.
Proof.
intros m a b c Hnan1 Hnan2 Hab.
apply B2Rx_le; try easy.
rewrite (Bplus_correct m c a Hnan1).
rewrite (Bplus_correct m c b Hnan2).
apply B2Rx_le; auto.
repeat (rewrite Bplus_correct; auto).
apply round_le.
apply add_leb_mono_r.
fdestruct a; fdestruct b; simpl.
- apply Raux.Rle_bool_true; lra.
- apply Raux.Rle_bool_true; lra.
- destruct s; simpl; try easy.
unfold Defs.F2R; simpl.
apply Raux.Rle_bool_true.
pose proof (IZR_pos m0).
pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
nra.
- apply Raux.Rle_bool_true; lra.
- apply Raux.Rle_bool_true; lra.
- destruct s; simpl; try easy.
unfold Defs.F2R; simpl.
apply Raux.Rle_bool_true.
pose proof (IZR_pos m0).
pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
nra.
- destruct s; simpl; try easy.
unfold Defs.F2R; simpl.
apply Raux.Rle_bool_true.
pose proof (IZR_neg m0).
pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
nra.
- destruct s; simpl; try easy.
unfold Defs.F2R; simpl.
apply Raux.Rle_bool_true.
pose proof (IZR_neg m0).
pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
nra.
- destruct s, s0; simpl; try easy;
apply Bleb_Rle in Hab; auto;
now apply Raux.Rle_bool_true.
apply (add_leb_mono_r _ _ _ (le_B2Rx _ _ Hab)).
Qed.
Theorem Bplus_le_compat':
Theorem Bplus_le_compat:
forall m (a b c d : float),
is_nan (Bplus m a b) = false ->
is_nan (Bplus m c d) = false ->
......@@ -245,16 +179,11 @@ Theorem Bplus_le_compat':
Bplus m a b <= Bplus m c d.
Proof.
intros.
apply B2Rx_le; try easy.
rewrite (Bplus_correct m a b); auto.
rewrite (Bplus_correct m c d); auto.
eapply leb_trans.
- apply round_le.
apply add_leb_mono_l.
apply (le_B2Rx _ _ H1).
- apply round_le.
apply add_leb_mono_r.
apply (le_B2Rx _ _ H2).
apply B2Rx_le; auto.
repeat (rewrite Bplus_correct); auto.
eapply leb_trans; apply round_le.
- apply (add_leb_mono_l _ _ _ (le_B2Rx _ _ H1)).
- apply (add_leb_mono_r _ _ _ (le_B2Rx _ _ H2)).
Qed.
End Correction.
\ No newline at end of file
From Flocq Require Import IEEE754.BinarySingleNaN.
From Coq Require Import ZArith.
From F Require Import Utils Correction_thms.
From Coq Require Import ZArith Psatz Reals.
From F Require Import Utils Correction_thms Rextended.
(**
The usual ordering relation on [binary_float] is [Bleb]. As defined
......@@ -121,6 +121,19 @@ Proof.
now apply Beqb_Bleb, Beqb_refl.
Qed.
(* Inductive interv : Type :=
| I_val : float -> interv
| I_closed : forall (lo hi : float) (nan : bool) (H : Bltb lo hi = true), interv.
Definition contains (i : interv) (x : float) : Prop :=
match i with
| I_val v => x = v
| I_closed lo hi nan _ =>
(x = NaN /\ nan = true) \/ lo <= x <= hi
end. *)
Inductive interv : Type :=
| I_closed : forall (lo hi : float) (nan : bool) (H : Fle0 lo hi = true), interv
| I_nan : interv.
......@@ -173,6 +186,521 @@ Proof.
+ now destruct s.
Qed.
Lemma Bsign_B2SF:
forall ( x : float ), sign_SF (B2SF x) = Bsign x.
Proof.
fdestruct x.
Qed.
Lemma Bsign_Bplus :
forall m (x y : float),
Bsign x = Bsign y -> Bsign (Bplus m x y) = Bsign x.
Proof.
intros m x y H.
fdestruct x; fdestruct y.
pose proof (BinarySingleNaN.Bplus_correct _ _ _ _ m (B754_finite s m0 e e0) (B754_finite s0 m1 e1 e2) eq_refl eq_refl).
destruct Raux.Rlt_bool; intuition.
+ destruct Raux.Rcompare eqn:E;
replace s with s0 in *.
* now destruct m, s0.
* rewrite H3.
destruct s0; try easy; simpl.
apply Raux.Rcompare_Lt_inv in E.
cbn in E.
assert (@Defs.F2R Zaux.radix2 {| Defs.Fnum := Z.pos m0; Defs.Fexp := e |} >= 0)%R. unfold Defs.F2R; simpl.
pose proof (IZR_pos m0).
pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
nra.
assert (@Defs.F2R Zaux.radix2 {| Defs.Fnum := Z.pos m1; Defs.Fexp := e1 |} >= 0)%R. unfold Defs.F2R; simpl.
pose proof (IZR_pos m1).
pose proof (Raux.bpow_gt_0 Zaux.radix2 e1).
nra.
nra.
* rewrite H3.
destruct s0; try easy; simpl.
apply Raux.Rcompare_Gt_inv in E.
cbn in E.
pose proof (IZR_neg m0).
pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
assert (@Defs.F2R Zaux.radix2 {| Defs.Fnum := Z.neg m0; Defs.Fexp := e |} <= 0)%R. unfold Defs.F2R; simpl. nra.
pose proof (IZR_neg m1).
pose proof (Raux.bpow_gt_0 Zaux.radix2 e1).
assert (@Defs.F2R Zaux.radix2 {| Defs.Fnum := Z.neg m1; Defs.Fexp := e1 |} < 0)%R. unfold Defs.F2R; simpl. nra.
nra.
+ replace s with s0. destruct s0, s; try easy.
* rewrite <- Bsign_B2SF.
rewrite H1. simpl.
unfold binary_overflow.
destruct overflow_to_inf; reflexivity.
* rewrite <- Bsign_B2SF.
rewrite H1. simpl.
unfold binary_overflow.
destruct overflow_to_inf; reflexivity.
Qed.
Lemma sum_to_0 :
forall mode m e H m' e' H',
Bplus mode (B754_finite true m e H) (B754_finite true m' e' H') <> -0.
Proof.
intros. intros Hcontr.
pose proof (BinarySingleNaN.Bplus_correct _ _ _ _ mode (B754_finite true m e H) (B754_finite true m' e' H') eq_refl eq_refl).
destruct Raux.Rlt_bool; intuition.
+ destruct Raux.Rcompare eqn:E.
* apply Raux.Rcompare_Eq_inv in E.
cbn in E.
assert (@Defs.F2R Zaux.radix2 {| Defs.Fnum := Z.neg m; Defs.Fexp := e |} < 0)%R. unfold Defs.F2R; simpl.
pose proof (IZR_neg m).
pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
nra.
assert (@Defs.F2R Zaux.radix2 {| Defs.Fnum := Z.neg m'; Defs.Fexp := e' |} < 0)%R. unfold Defs.F2R; simpl.
pose proof (IZR_neg m').
pose proof (Raux.bpow_gt_0 Zaux.radix2 e').
nra.
nra.
* apply Raux.Rcompare_Lt_inv in E.
apply Rlt_le in E.
apply (Generic_fmt.round_le Zaux.radix2 (SpecFloat.fexp prec emax)
(round_mode mode)) in E.
rewrite Generic_fmt.round_0 in E by intuition.
rewrite <- H1 in E.
assert (B2R (Bplus mode (B754_finite true m e H) (B754_finite true m' e' H')) = 0%R) by now rewrite Hcontr.
destruct E.
- nra.
Admitted.
Theorem Fle0_is_Bleb_r:
forall (x y : float),
(y <> +0 /\ y <> -0) ->
Fle0 x y = Bleb x y.
Proof.
fdestruct x; fdestruct y.
Qed.
Theorem Fle0_is_Bleb_l:
forall (x y : float),
(x <> +0 /\ x <> -0) ->
Fle0 x y = Bleb x y.
Proof.
fdestruct x; fdestruct y.
Qed.
Theorem Bsign_Fle0:
forall x y,
is_nan x = false ->
is_nan y = false ->
Bsign x = true -> Bsign y = false -> Fle0 x y = true.
Proof.
intros.
fdestruct x; fdestruct y.
+ now destruct s.
+ now destruct s.
+ now destruct s, s0.
Qed.
Theorem Bplus_pos:
forall (x y : float) m,
Fle0 -0 x = true ->
Fle0 -0 y = true ->
Fle0 -0 (Bplus m x y) = true.
Proof.
intros.
pose proof Bsign_Bplus m x y.
fdestruct x; fdestruct y.
+ now destruct m.
+ now destruct m.
+ simpl in H, H0.
destruct s, s0; try easy.
apply Bsign_Fle0; try easy.
- now apply Bplus_finites_not_nan.
- now apply H1.
Qed.
Theorem finite_Fle0_pos:
forall (f : float), is_nan f = false -> Bsign f = false -> Fle0 -0 f = true.
Proof.
intros.
fdestruct f.
now destruct s.
Qed.
Theorem finite_Fle0_neg:
forall (f : float), is_nan f = false -> Bsign f = true -> Fle0 f +0 = true.
Proof.
intros.
fdestruct f.
now destruct s.
Qed.
Inductive Rx0 : Type :=
| Rx0_NaN : Rx0
| Rx0_zero : bool -> Rx0
| Rx0_inf : bool -> Rx0
| Rx0_real : R -> Rx0.
Definition B2Rx0 (f : float) : Rx0 :=
match f with
| B754_zero s => Rx0_zero s
| B754_infinity s => Rx0_inf s
| NaN => Rx0_NaN
| B754_finite _ _ _ _ => Rx0_real (B2R f)
end.
Definition Rx0le (x y : Rx0) : bool :=
match x with
| Rx0_NaN => false
| Rx0_zero s =>
match y with
| Rx0_NaN => false
| Rx0_zero s' => if negb s then negb s' else true
| Rx0_inf s' => negb s'
| Rx0_real r => Raux.Rle_bool 0%R r
end
| Rx0_inf s =>
match y with
| Rx0_NaN => false
| Rx0_zero s' => s
| Rx0_inf s' =>
if negb s then negb s' else true
| Rx0_real r => s
end
| Rx0_real r =>
if Raux.Req_bool r 0%R then
match y with
| Rx0_NaN => false
| Rx0_zero s' => negb s'
| Rx0_inf s' => negb s'
| Rx0_real r' => Raux.Rle_bool r r'
end
else
match y with
| Rx0_NaN => false
| Rx0_zero s' => Raux.Rle_bool r 0%R
| Rx0_inf s' => negb s'
| Rx0_real r' => Raux.Rle_bool r r'
end
end.
Theorem B2Rx0_le:
forall (x y : float),
Rx0le (B2Rx0 x) (B2Rx0 y) = true -> x <= y.
Proof.
intros.
destruct x as [[ ] | [ ] | | ] eqn:E1; destruct y as [ [ ] | [ ] | | ] eqn:E2; try easy.
+ repeat (unfold B2Rx0 in H); unfold Rx0le in H.
apply Rleb_Rle in H; now apply Rle_Bleb.
+ repeat (unfold B2Rx0 in H); unfold Rx0le in H.
apply Rleb_Rle in H; now apply Rle_Bleb.
+ repeat (unfold B2Rx0 in H); unfold Rx0le in H.
destruct Raux.Req_bool eqn:E.
* apply Reqb_Req in E.
apply Rle_Bleb; auto; rewrite E; simpl; lra.
* apply Rleb_Rle in H.
now apply Rle_Bleb.
+ repeat (unfold B2Rx0 in H); unfold Rx0le in H.
destruct Raux.Req_bool eqn:E.
* apply Reqb_Req in E.
apply Rle_Bleb; auto; rewrite E; simpl; lra.
* apply Rleb_Rle in H.
now apply Rle_Bleb.
+ repeat (unfold B2Rx0 in H); unfold Rx0le in H.
now destruct Raux.Req_bool eqn:E.
+ repeat (unfold B2Rx0 in H); unfold Rx0le in H.
now destruct Raux.Req_bool eqn:E.
+ repeat (unfold B2Rx0 in H); unfold Rx0le in H.
destruct Raux.Req_bool eqn:E;
apply Rle_Bleb; auto;
now apply Rleb_Rle in H.
Qed.
Theorem Fle0_B2Rx0 :
forall (x y : float),
Fle0 x y = true -> Rx0le (B2Rx0 x) (B2Rx0 y) = true.
Proof.
intros.
fdestruct x; fdestruct y;
repeat (unfold B2Rx0);
unfold Rx0le.
- apply Raux.Rle_bool_true; now apply Bleb_Rle in H.
- apply Raux.Rle_bool_true; now apply Bleb_Rle in H.
- destruct Raux.Req_bool eqn:E; auto.
+ apply Reqb_Req in E.
unfold B2R, Defs.F2R in E.
destruct s; simpl in E.
* pose proof (IZR_neg m);
pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
nra.
* pose proof (IZR_pos m);
pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
nra.
+ apply Raux.Rle_bool_true.
now apply Bleb_Rle in H.
- destruct Raux.Req_bool eqn:E; auto.
apply Raux.Rle_bool_true.
now apply Bleb_Rle in H.
- now destruct Raux.Req_bool eqn:E.
- destruct Raux.Req_bool eqn:E;
apply Bleb_Rle in H; auto;
now apply Raux.Rle_bool_true.
Qed.
Theorem B2Rx0_Fle0 :
forall (x y : float), Rx0le (B2Rx0 x) (B2Rx0 y) = true -> Fle0 x y = true.
Proof.
intros.
fdestruct x; fdestruct y;
repeat (unfold B2Rx0 in H);
unfold Rx0le in H;
apply Rle_Bleb; try easy.
+ now apply Rleb_Rle.
+ now apply Rleb_Rle.
+ destruct Raux.Req_bool eqn:E in H.
- rewrite (Reqb_Req _ _ E); simpl; lra.
- now apply Rleb_Rle in H.
+ destruct Raux.Req_bool eqn:E in H.
- apply Reqb_Req in E.
unfold B2R, Defs.F2R in E.
destruct s; simpl in E.
* pose proof (IZR_neg m);
pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
nra.
* pose proof (IZR_pos m);
pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
nra.
- now apply Rleb_Rle in H.
+ now destruct Raux.Req_bool eqn:E in H.
+ now destruct Raux.Req_bool eqn:E in H.
+ now destruct Raux.Req_bool eqn:E in H.
+ now destruct Raux.Req_bool eqn:E in H.
+ destruct Raux.Req_bool eqn:E in H.
- rewrite (Reqb_Req _ _ E) in *.
now apply Rleb_Rle in H.
- now apply Rleb_Rle in H.
Qed.
Definition add (x y : Rx0) :=
match x with
| Rx0_NaN => x
| Rx0_inf true =>
match y with
| Rx0_NaN => Rx0_NaN
| Rx0_inf false => Rx0_NaN
| _ => x
end
| Rx0_inf false =>
match y with
| Rx0_NaN => Rx0_NaN
| Rx0_inf true => Rx0_NaN
| _ => x
end
| Rx0_zero _ =>
match y with
| Rx0_zero _ => Rx0_real 0%R
| _ => y
end
| Rx0_real r =>
match y with
| Rx0_NaN => Rx0_NaN
| Rx0_inf _ => y
| Rx0_zero _ => x
| Rx0_real r' => Rx0_real (r + r')%R
end
end.
Compute (add (Rx0_real R0) (Rx0_zero true)).
Compute (add (Rx0_real R0) (Rx0_zero false)).
Lemma Req_0_true:
Raux.Req_bool 0 0 = true.
Proof.
now apply Raux.Req_bool_true.
Qed.
Definition add_Rx0le_mono_l :
forall (x y z : Rx0),
add x z <> Rx0_NaN ->
add y z <> Rx0_NaN ->
Rx0le x y = true -> Rx0le (add x z) (add y z) = true.
Proof.
intros.
destruct x eqn:Ex, y eqn:Ey, z eqn:Ez; simpl; try easy;
try (destruct b; try easy; destruct b0; try easy; destruct b1; try easy);
try (rewrite Req_0_true; apply Raux.Rle_bool_true; lra).
+ destruct Raux.Req_bool eqn:E;
apply Raux.Rle_bool_true; lra.
+ now destruct Raux.Req_bool eqn:E.
+ now destruct Raux.Req_bool eqn:E.
+ now destruct Raux.Req_bool eqn:E.
+ now destruct Raux.Req_bool eqn:E.
+ destruct Raux.Req_bool eqn:E; now destruct b0.
+ now destruct Raux.Req_bool eqn:E.
+ destruct Raux.Req_bool eqn:E.
- rewrite (Reqb_Req _ _ E).
apply Rleb_Rle in H1.
apply Raux.Rle_bool_true.
lra.
- apply Raux.Rle_bool_true.
apply Rleb_Rle in H1.
lra.
+ destruct Raux.Req_bool eqn:E.
- rewrite (Reqb_Req _ _ E).