From 9540d8642c305a75bb8c159e9c7b0ed0ba3c121d Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 2 Dec 2010 17:59:41 +0000 Subject: [PATCH] Started a formalization of IEEE-754 binary floating-point numbers. --- src/Appli/Fappli_IEEE.v | 166 ++++++++++++++++++++++++++++++++++++++++ src/Makefile.am | 1 + 2 files changed, 167 insertions(+) create mode 100644 src/Appli/Fappli_IEEE.v diff --git a/src/Appli/Fappli_IEEE.v b/src/Appli/Fappli_IEEE.v new file mode 100644 index 0000000..97923e5 --- /dev/null +++ b/src/Appli/Fappli_IEEE.v @@ -0,0 +1,166 @@ +Require Import Fcore. +Require Import Fcalc_digits. + +Section Binary. + +Variable prec emax : Z. + +Let fexp := FLT_exp (1 - (emax + prec)) prec. + +Definition bounded_prec m e := + Zeq_bool (fexp (Z_of_nat (S (digits2_Pnat m)) + e)) e. + +Definition bounded m e := + andb (bounded_prec m e) (Zle_bool e emax). + +Inductive binary_float := + | B754_zero : bool -> binary_float + | B754_infinity : bool -> binary_float + | B754_nan : binary_float + | B754_finite : bool -> + forall (m : positive) (e : Z), bounded m e = true -> binary_float. + +Definition radix2 := Build_radix 2 (refl_equal true). + +Definition B2R f := + match f with + | B754_finite s m e _ => F2R (Float radix2 ((if s then Zneg else Zpos) m) e) + | _ => R0 + end. + +Theorem canonic_bounded_prec : + forall (sx : bool) mx ex, + bounded_prec mx ex = true -> + canonic radix2 fexp (Float radix2 ((if sx then Zneg else Zpos) mx) ex). +Proof. +intros sx mx ex H. +assert (Hx := Zeq_bool_eq _ _ H). clear H. +apply sym_eq. +simpl. +pattern ex at 2 ; rewrite <- Hx. +apply (f_equal fexp). +rewrite ln_beta_F2R_digits. +rewrite <- digits_abs. +rewrite Z_of_nat_S_digits2_Pnat. +now case sx. +now case sx. +Qed. + +Theorem generic_format_B2R : + forall x, + generic_format radix2 fexp (B2R x). +Proof. +intros [sx|sx| |sx mx ex Hx] ; try apply generic_format_0. +simpl. +apply generic_format_canonic. +apply canonic_bounded_prec. +now destruct (andb_prop _ _ Hx) as (H, _). +Qed. + +Definition is_finite_strict f := + match f with + | B754_finite _ _ _ _ => true + | _ => false + end. + +Theorem binary_unicity : + forall x y : binary_float, + is_finite_strict x = true -> + is_finite_strict y = true -> + B2R x = B2R y -> + x = y. +Proof. +intros [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ; try easy. +simpl. +intros _ _ Heq. +assert (Hs: sx = sy). +(* *) +revert Heq. clear. +case sx ; case sy ; try easy ; + intros Heq ; apply False_ind ; revert Heq. +apply Rlt_not_eq. +apply Rlt_trans with R0. +now apply F2R_lt_0_compat. +now apply F2R_gt_0_compat. +apply Rgt_not_eq. +apply Rgt_trans with R0. +now apply F2R_gt_0_compat. +now apply F2R_lt_0_compat. +assert (mx = my /\ ex = ey). +(* *) +refine (_ (canonic_unicity _ fexp _ _ _ _ Heq)). +rewrite Hs. +now case sy ; intro H ; injection H ; split. +apply canonic_bounded_prec. +exact (proj1 (andb_prop _ _ Hx)). +apply canonic_bounded_prec. +exact (proj1 (andb_prop _ _ Hy)). +(* *) +revert Hx. +rewrite Hs, (proj1 H), (proj2 H). +intros Hx. +apply f_equal. +apply eqbool_irrelevance. +Qed. + +Definition is_finite f := + match f with + | B754_finite _ _ _ _ => true + | B754_zero _ => true + | _ => false + end. + +Inductive mode := mode_NE | mode_ZR | mode_DN | mode_UP | mode_NA. + +Definition round_mode m := + match m with + | mode_NE => rndNE + | mode_ZR => rndZR + | mode_DN => rndDN + | mode_UP => rndUP + | mode_NA => rndNA + end. + +Definition Bplus m x y := + match x, y with + | B754_nan, _ => x + | _, B754_nan => y + | B754_infinity sx, B754_infinity sy => + if Bool.eqb sx sy then x else B754_nan + | B754_infinity _, _ => x + | _, B754_infinity _ => y + | B754_zero sx, B754_zero sy => + if Bool.eqb sx sy then x else + match m with mode_DN => B754_zero true | _ => B754_zero false end + | B754_zero _, _ => y + | _, B754_zero _ => x + | B754_finite sx mx ex Hx, B754_finite sy my ey Hy => + B754_nan + end. + +Theorem Bplus_finite : + forall m x y, + is_finite x = true -> + is_finite y = true -> + B2R (Bplus m x y) = round radix2 fexp (round_mode m) (B2R x + B2R y)%R. +Proof. +intros m [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ; try easy ; intros _ _. +(* *) +rewrite Rplus_0_r, round_0. +simpl. +case (Bool.eqb sx sy) ; try easy. +now case m. +(* *) +rewrite Rplus_0_l. +apply sym_eq. +apply round_generic. +apply generic_format_B2R. +(* *) +rewrite Rplus_0_r. +apply sym_eq. +apply round_generic. +apply generic_format_B2R. +(* *) +Admitted. + +End Binary. diff --git a/src/Makefile.am b/src/Makefile.am index 4257dc1..9d2892d 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -23,6 +23,7 @@ FILES = \ Prop/Fprop_div_sqrt_error.v \ Prop/Fprop_Sterbenz.v \ Appli/Fappli_Axpy.v \ + Appli/Fappli_IEEE.v \ Appli/Fappli_sqrt_FLT_ne.v EXTRA_DIST = \$(FILES) -- GitLab