Tighten and prove correct the underflow/overflow bounds for parsing of FP literals.

This is a follow-up to commit 350354c.
- Move Float.build_from_parsed to Fappli_IEEE_extra.Bparse
- Add early checks for overflow and underflow and prove them correct.
- Improve speed of Bparse by using a fast exponentiation (square-and-multiply).

1 files changed, 2 insertions, 96 deletions

diff --git a/lib/Floats.v b/lib/Floats.v
index f86632b9..e893e3e7 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -92,100 +92,6 @@ Proof.
   destruct x as [[]|]; simpl; intros; discriminate.
 Qed.
 
-Section FP_PARSING.
-
-Variables prec emax: Z.
-Context (prec_gt_0 : Prec_gt_0 prec).
-Hypothesis Hmax : (prec < emax)%Z.
-
-(** Function used to convert literals into FP numbers during parsing.
-   [intPart] is the mantissa
-   [expPart] is the exponent
-   [base] is the base for the exponent (usually 10 or 16).
-   The result is [intPart * base^expPart] rounded to the nearest FP number,
-   ties to even. *)
-
-Definition build_from_parsed (base:positive) (intPart:positive) (expPart:Z) : binary_float prec emax :=
-  match expPart with
-    | Z0 =>
-      binary_normalize prec emax prec_gt_0 Hmax mode_NE (Zpos intPart) Z0 false
-    | Zpos p =>
-      binary_normalize prec emax prec_gt_0 Hmax mode_NE ((Zpos intPart) * Zpower_pos (Zpos base) p) Z0 false
-    | Zneg p =>
-      FF2B prec emax _ (proj1 (Bdiv_correct_aux prec emax prec_gt_0 Hmax mode_NE
-                                  false intPart Z0 false (Pos.pow base p) Z0))
-  end.
-
-Let emin := (3 - emax - prec)%Z.
-Let fexp := FLT_exp emin prec.
-
-Theorem build_from_parsed_correct:
-  forall base m e (BASE: 2 <= Zpos base),
-  let base_r := {| radix_val := Zpos base; radix_prop := Zle_imp_le_bool _ _ BASE |} in
-  let r := round radix2 fexp (round_mode mode_NE) (Z2R (Zpos m) * bpow base_r e) in
-  if Rlt_bool (Rabs r) (bpow radix2 emax) then
-     B2R _ _ (build_from_parsed base m e) = r
-  /\ is_finite _ _ (build_from_parsed base m e) = true
-  /\ Bsign _ _ (build_from_parsed base m e) = false
-  else
-    B2FF _ _ (build_from_parsed base m e) = F754_infinity false.
-Proof.
-  intros. 
-  assert (A: forall x, @F2R radix2 {| Fnum := x; Fexp := 0 |} = Z2R x).
-  { intros. unfold F2R, Fnum; simpl. ring. }
-  unfold build_from_parsed, r; destruct e. 
-- change (bpow base_r 0) with (1%R). rewrite Rmult_1_r.  
-  generalize (binary_normalize_correct _ _ _ Hmax mode_NE (Zpos m) 0 false).
-  fold emin; fold fexp. rewrite ! A.
-  destruct (Rlt_bool (Rabs (round radix2 fexp (round_mode mode_NE) (Z2R (Z.pos m))))
-                     (bpow radix2 emax)).
-  + intros (P & Q & R). split. auto. split. auto. rewrite R. rewrite Rcompare_Gt; auto. 
-    apply (Z2R_lt 0). compute; auto.
-  + intros P; rewrite P. unfold binary_overflow.
-    replace (Rlt_bool (Z2R (Z.pos m)) 0%R) with false. auto. 
-    rewrite Rlt_bool_false; auto. apply (Z2R_le 0). xomega.
-- generalize (binary_normalize_correct _ _ _ Hmax mode_NE (Zpos m * Z.pow_pos (Zpos base) p) 0 false).
-  fold emin; fold fexp. rewrite ! A.
-  assert (B: Z2R (Z.pos m * Z.pow_pos (Z.pos base) p) = (Z2R (Z.pos m) * bpow base_r (Z.pos p))%R).
-  { unfold bpow. apply Z2R_mult. }
-  rewrite B. 
-  destruct (Rlt_bool
-     (Rabs
-        (round radix2 fexp (round_mode mode_NE)
-           (Z2R (Z.pos m) * bpow base_r (Z.pos p)))) (bpow radix2 emax)).
-  + intros (P & Q & R). split. auto. split. auto. rewrite R. rewrite Rcompare_Gt; auto. 
-    apply Rmult_lt_0_compat. apply (Z2R_lt 0). xomega. apply bpow_gt_0. 
-  + intros P. rewrite P. unfold binary_overflow. 
-    replace (Rlt_bool (Z2R (Z.pos m) * bpow base_r (Z.pos p)) 0) with false.
-    auto.
-    rewrite Rlt_bool_false; auto. apply Rlt_le. apply Rmult_lt_0_compat. apply (Z2R_lt 0). xomega. apply bpow_gt_0. 
-- generalize (Bdiv_correct_aux prec emax prec_gt_0 Hmax mode_NE false m 0 false (base ^ p) 0).
-  set (f := 
-      match Fdiv_core_binary prec (Z.pos m) 0 (Z.pos (base ^ p)) 0 with
-      | (0, _, _) => F754_nan false 1
-      | (Z.pos mz0, ez, lz) =>
-          binary_round_aux prec emax mode_NE (xorb false false) mz0 ez lz
-      | (Z.neg _, _, _) => F754_nan false 1
-      end).
-  fold emin; fold fexp. rewrite ! A. unfold cond_Zopp. 
-  assert (B: (Z2R (Z.pos m) / Z2R (Z.pos (base ^ p)) =
-              Z2R (Z.pos m) * bpow base_r (Z.neg p))%R).
-  { change (Z.neg p) with (- (Z.pos p)). rewrite bpow_opp. unfold Rdiv. f_equal. f_equal. 
-    unfold bpow. f_equal. simpl. apply Pos2Z.inj_pow_pos. }
-  rewrite ! B. 
-  destruct (Rlt_bool
-     (Rabs
-        (round radix2 fexp (round_mode mode_NE)
-           (Z2R (Z.pos m) * bpow base_r (Z.neg p)))) (bpow radix2 emax)).
-  + intros (P & Q & R & S).
-    split. rewrite B2R_FF2B. exact Q. 
-    split. rewrite is_finite_FF2B. auto.
-    rewrite Bsign_FF2B. auto. 
-  + intros (P & Q). rewrite B2FF_FF2B. auto.
-Qed.
-
-End FP_PARSING.
-
 Local Notation __ := (refl_equal Datatypes.Lt).
 
 Local Hint Extern 1 (Prec_gt_0 _) => exact (refl_equal Datatypes.Lt).
@@ -339,7 +245,7 @@ Definition of_longu (n:int64): float:= (**r conversion from unsigned 64-bit int
   BofZ 53 1024 __ __ (Int64.unsigned n).
 
 Definition from_parsed (base:positive) (intPart:positive) (expPart:Z) : float :=
-  build_from_parsed 53 1024 __ __ base intPart expPart.
+  Bparse 53 1024 __ __ base intPart expPart.
 
 (** Conversions between floats and their concrete in-memory representation
     as a sequence of 64 bits. *)
@@ -1004,7 +910,7 @@ Definition of_longu (n:int64): float32 := (**r conversion from unsigned 64-bit i
   BofZ 24 128 __ __ (Int64.unsigned n).
 
 Definition from_parsed (base:positive) (intPart:positive) (expPart:Z) : float32 :=
-  build_from_parsed 24 128 __ __ base intPart expPart.
+  Bparse 24 128 __ __ base intPart expPart.
 
 (** Conversions between floats and their concrete in-memory representation
     as a sequence of 32 bits. *)