Upgrade to flocq 2.4.0

2 files changed, 106 insertions, 292 deletions

diff --git a/lib/Fappli_IEEE_extra.v b/lib/Fappli_IEEE_extra.v
index 5194a644..92ed11ae 100644
--- a/lib/Fappli_IEEE_extra.v
+++ b/lib/Fappli_IEEE_extra.v
@@ -75,8 +75,8 @@ Proof.
   intros. destruct x as [ [] | | | [] ex mx Bx ]; try discriminate; simpl.
 - rewrite Rlt_bool_false; auto. lra.
 - rewrite Rlt_bool_true; auto. apply F2R_lt_0_compat. compute; auto.
-- rewrite Rlt_bool_false; auto. 
-  assert ((F2R (Float radix2 (Z.pos ex) mx) > 0)%R) by 
+- rewrite Rlt_bool_false; auto.
+  assert ((F2R (Float radix2 (Z.pos ex) mx) > 0)%R) by
     ( apply F2R_gt_0_compat; compute; auto ).
   lra.
 Qed.
@@ -116,156 +116,6 @@ Proof.
   subst; left; f_equal; apply UIP_bool. 
 Defined.
 
-(** ** Comparison *)
-
-(** [Some c] means ordered as per [c]; [None] means unordered. *)
-
-Definition Bcompare (f1 f2: binary_float): option comparison :=
-  match f1, f2 with
-    | B754_nan _ _,_ | _,B754_nan _ _ => None
-    | B754_infinity true, B754_infinity true
-    | B754_infinity false, B754_infinity false => Some Eq
-    | B754_infinity true, _ => Some Lt
-    | B754_infinity false, _ => Some Gt
-    | _, B754_infinity true => Some Gt
-    | _, B754_infinity false => Some Lt
-    | B754_finite true _ _ _, B754_zero _ => Some Lt
-    | B754_finite false _ _ _, B754_zero _ => Some Gt
-    | B754_zero _, B754_finite true _ _ _ => Some Gt
-    | B754_zero _, B754_finite false _ _ _ => Some Lt
-    | B754_zero _, B754_zero _ => Some Eq
-    | B754_finite s1 m1 e1 _, B754_finite s2 m2 e2 _ =>
-      match s1, s2 with
-        | true, false => Some Lt
-        | false, true => Some Gt
-        | false, false =>
-          match Zcompare e1 e2 with
-            | Lt => Some Lt
-            | Gt => Some Gt
-            | Eq => Some (Pcompare m1 m2 Eq)
-          end
-        | true, true =>
-          match Zcompare e1 e2 with
-            | Lt => Some Gt
-            | Gt => Some Lt
-            | Eq => Some (CompOpp (Pcompare m1 m2 Eq))
-          end
-      end
-  end.
-
-Theorem Bcompare_finite_correct:
-  forall f1 f2,
-  is_finite _ _ f1 = true -> is_finite _ _ f2 = true ->
-  Bcompare f1 f2 = Some (Rcompare (B2R _ _ f1) (B2R _ _ f2)).
-Proof.
-  Ltac apply_Rcompare :=
-    match goal with
-      | [ |- Some Lt = Some (Rcompare _ _) ] => f_equal; symmetry; apply Rcompare_Lt
-      | [ |- Some Eq = Some (Rcompare _ _) ] => f_equal; symmetry; apply Rcompare_Eq
-      | [ |- Some Gt = Some (Rcompare _ _) ] => f_equal; symmetry; apply Rcompare_Gt
-    end.
-  unfold Bcompare; intros.
-  destruct f1, f2; try discriminate; unfold B2R, F2R, Fnum, Fexp, cond_Zopp;
-    try (replace 0%R with (Z2R 0 * bpow radix2 e)%R by (simpl Z2R; ring);
-         rewrite Rcompare_mult_r by (apply bpow_gt_0); rewrite Rcompare_Z2R).
-  apply_Rcompare; reflexivity.
-  destruct b0; reflexivity.
-  destruct b; reflexivity.
-  clear H H0.
-  apply andb_prop in e0; destruct e0; apply (canonic_canonic_mantissa _ _ false) in H.
-  apply andb_prop in e2; destruct e2; apply (canonic_canonic_mantissa _ _ false) in H1.
-  pose proof (Zcompare_spec e e1); unfold canonic, Fexp in H1, H.
-  assert (forall m1 m2 e1 e2,
-    let x := (Z2R (Zpos m1) * bpow radix2 e1)%R in
-    let y := (Z2R (Zpos m2) * bpow radix2 e2)%R in
-    (canonic_exp radix2 fexp x < canonic_exp radix2 fexp y)%Z -> (x < y)%R).
-  {  
-  intros; apply Rnot_le_lt; intro; apply (ln_beta_le radix2) in H5.
-  unfold canonic_exp in H4. apply (fexp_monotone prec emax) in H5.
-  unfold fexp, emin in H4. omega.
-  apply Rmult_gt_0_compat; [apply (Z2R_lt 0); reflexivity|now apply bpow_gt_0].
-  }
-  assert (forall m1 m2 e1 e2, (Z2R (- Zpos m1) * bpow radix2 e1 < Z2R (Zpos m2) * bpow radix2 e2)%R).
-  {
-  intros; apply (Rlt_trans _ 0%R).
-  replace 0%R with (0*bpow radix2 e0)%R by ring; apply Rmult_lt_compat_r;
-    [apply bpow_gt_0; reflexivity|now apply (Z2R_lt _ 0)].
-  apply Rmult_gt_0_compat; [apply (Z2R_lt 0); reflexivity|now apply bpow_gt_0].
-  }
-  destruct b, b0; try (now apply_Rcompare; apply H5); inversion H3;
-    try (apply_Rcompare; apply H4; rewrite H, H1 in H7; assumption);
-    try (apply_Rcompare; do 2 rewrite Z2R_opp, Ropp_mult_distr_l_reverse;
-      apply Ropp_lt_contravar; apply H4; rewrite H, H1 in H7; assumption);
-    rewrite H7, Rcompare_mult_r, Rcompare_Z2R by (apply bpow_gt_0); reflexivity.
-Qed.
-
-Theorem Bcompare_swap:
-  forall x y,
-  Bcompare y x = match Bcompare x y with Some c => Some (CompOpp c) | None => None end.
-Proof.
-  intros. 
-  destruct x as [ ? | [] | ? ? | [] mx ex Bx ];
-  destruct y as [ ? | [] | ? ? | [] my ey By ]; simpl; auto.
-- rewrite <- (Zcompare_antisym ex ey). destruct (ex ?= ey)%Z; auto.
-  simpl. f_equal; f_equal. symmetry. apply Pcompare_antisym. 
-- rewrite <- (Zcompare_antisym ex ey). destruct (ex ?= ey)%Z; auto. 
-  simpl. f_equal. symmetry. apply Pcompare_antisym.
-Qed.
-
-(** ** Absolute value *)
-
-Definition Babs abs_nan (x: binary_float) : binary_float :=
-  match x with
-  | B754_nan sx plx =>
-      let '(sres, plres) := abs_nan sx plx in B754_nan _ _ sres plres
-  | B754_infinity sx => B754_infinity _ _ false
-  | B754_finite sx mx ex Hx => B754_finite _ _ false mx ex Hx
-  | B754_zero sx => B754_zero _ _ false
-  end.
-
-Theorem B2R_Babs :
-  forall abs_nan x,
-  B2R _ _ (Babs abs_nan x) = Rabs (B2R _ _ x).
-Proof.
-  intros abs_nan [sx|sx|sx plx|sx mx ex Hx]; apply sym_eq ; try apply Rabs_R0.
-  simpl. destruct abs_nan. simpl. apply Rabs_R0.
-  simpl. rewrite <- F2R_abs. destruct sx; auto. 
-Qed.
-
-Theorem is_finite_Babs :
-  forall abs_nan x,
-  is_finite _ _ (Babs abs_nan x) = is_finite _ _ x.
-Proof.
-  intros abs_nan [| | |] ; try easy.
-  intros s pl.
-  simpl.
-  now case abs_nan.
-Qed.
-
-Theorem sign_Babs:
-  forall abs_nan x,
-  is_nan _ _ x = false ->
-  Bsign _ _ (Babs abs_nan x) = false.
-Proof.
-  intros abs_nan [| | |]; reflexivity || discriminate.
-Qed.
-
-Theorem Babs_idempotent :
-  forall abs_nan (x: binary_float),
-  is_nan _ _ x = false ->
-  Babs abs_nan (Babs abs_nan x) = Babs abs_nan x.
-Proof.
-  now intros abs_nan [sx|sx|sx plx|sx mx ex Hx] ; auto.
-Qed.
-
-Theorem Babs_opp:
-  forall abs_nan opp_nan x,
-  is_nan _ _ x = false ->
-  Babs abs_nan (Bopp _ _ opp_nan x) = Babs abs_nan x.
-Proof.
-  intros abs_nan opp_nan [| | |]; reflexivity || discriminate.
-Qed.
-
 (** ** Conversion from an integer to a FP number *)
 
 (** Integers that can be represented exactly as FP numbers. *)
@@ -1162,14 +1012,17 @@ Proof.
   rewrite Zabs2Nat.id_abs. rewrite Z.abs_eq by omega. auto.
 Qed.
 
-Remark Bexact_inverse_mantissa_digits2_Pnat:
-  digits2_Pnat Bexact_inverse_mantissa = Z.to_nat (prec - 1).
+Remark Bexact_inverse_mantissa_digits2_pos:
+  Z.pos (digits2_pos Bexact_inverse_mantissa) = prec.
 Proof.
-  assert (DIGITS: forall n, digits2_Pnat (nat_iter n xO xH) = n).
-  { induction n; simpl. auto. congruence. }
+  assert (DIGITS: forall n, digits2_pos (nat_iter n xO xH) = Pos.of_nat (n+1)).
+  { induction n; simpl. auto. rewrite IHn. destruct n; auto. }
   red in prec_gt_0_.
   unfold Bexact_inverse_mantissa. rewrite iter_nat_of_Z by omega. rewrite DIGITS.
-  apply Zabs2Nat.abs_nat_nonneg. omega.
+  rewrite Zabs2Nat.abs_nat_nonneg, Z2Nat.inj_sub by omega.
+  destruct prec; try  discriminate. rewrite NPeano.Nat.sub_add.
+  simpl. rewrite Pos2Nat.id. auto.
+  simpl. zify; omega.
 Qed.
 
 Remark bounded_Bexact_inverse:
@@ -1178,8 +1031,7 @@ Remark bounded_Bexact_inverse:
 Proof.
   intros. unfold bounded, canonic_mantissa. rewrite andb_true_iff. 
   rewrite <- Zeq_is_eq_bool. rewrite <- Zle_is_le_bool. 
-  rewrite Bexact_inverse_mantissa_digits2_Pnat. 
-  rewrite inj_S. red in prec_gt_0_. rewrite Z2Nat.id by omega. 
+  rewrite Bexact_inverse_mantissa_digits2_pos. 
   split. 
 - intros; split. unfold FLT_exp. unfold emin in H. zify; omega. omega.
 - intros [A B]. unfold FLT_exp in A. unfold emin. zify; omega.
@@ -1400,7 +1252,7 @@ Proof.
 - apply andb_true_iff in FIN. destruct FIN. 
   destruct (Bconv_widen_exact H H0 conv_nan m x H1) as (A & B & C).
   destruct (Bconv_widen_exact H H0 conv_nan m y H2) as (D & E & F).
-  rewrite ! Bcompare_finite_correct by auto. rewrite A, D. auto.
+  rewrite ! Bcompare_correct by auto. rewrite A, D. auto.
 - generalize (Bconv_widen_exact H H0 conv_nan m x)
              (Bconv_widen_exact H H0 conv_nan m y); intros P Q.
   destruct x, y; try discriminate; simpl in P, Q; simpl;
@@ -1459,48 +1311,3 @@ Proof.
 Qed.
 
 End Compose_Conversions.
-
-(** Specialization to binary32 and binary64 formats. *)
-
-Require Import Fappli_IEEE_bits.
-
-Section B3264.
-
-Let prec32 : (0 < 24)%Z.
-apply refl_equal.
-Qed.
-
-Let emax32 : (24 < 128)%Z.
-apply refl_equal.
-Qed.
-
-Let prec64 : (0 < 53)%Z.
-apply refl_equal.
-Qed.
-
-Let emax64 : (53 < 1024)%Z.
-apply refl_equal.
-Qed.
-
-Definition b32_abs : (bool -> nan_pl 24 -> bool * nan_pl 24) -> binary32 -> binary32 := Babs 24 128.
-Definition b32_eq_dec : forall (f1 f2: binary32), {f1=f2} + {f1<>f2} := Beq_dec 24 128.
-Definition b32_compare : binary32 -> binary32 -> option comparison := Bcompare 24 128.
-Definition b32_of_Z : Z -> binary32 := BofZ 24 128 prec32 emax32.
-Definition b32_to_Z : binary32 -> option Z := ZofB 24 128.
-Definition b32_to_Z_range : binary32 -> Z -> Z -> option Z := ZofB_range 24 128.
-Definition b32_exact_inverse : binary32 -> option binary32 := Bexact_inverse 24 128 prec32.
-
-Definition b64_abs : (bool -> nan_pl 53 -> bool * nan_pl 53) -> binary64 -> binary64 := Babs 53 1024.
-Definition b64_eq_dec : forall (f1 f2: binary64), {f1=f2} + {f1<>f2} := Beq_dec 53 1024.
-Definition b64_compare : binary64 -> binary64 -> option comparison := Bcompare 53 1024.
-Definition b64_of_Z : Z -> binary64 := BofZ 53 1024 prec64 emax64.
-Definition b64_to_Z : binary64 -> option Z := ZofB 53 1024.
-Definition b64_to_Z_range : binary64 -> Z -> Z -> option Z := ZofB_range 53 1024.
-Definition b64_exact_inverse : binary64 -> option binary64 := Bexact_inverse 53 1024 prec64.
-
-Definition b64_of_b32 : (bool -> nan_pl 24 -> bool * nan_pl 53) -> mode -> binary32 -> binary64 :=
-  Bconv 24 128 53 1024 prec32 prec64.
-Definition b32_of_b64 : (bool -> nan_pl 53 -> bool * nan_pl 24) -> mode -> binary64 -> binary32 :=
-  Bconv 53 1024 24 128 prec64 prec32.
-
-End B3264.
diff --git a/lib/Floats.v b/lib/Floats.v
index fbc78d96..e867cba8 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -136,10 +136,9 @@ Program Definition transform_quiet_pl (pl:nan_pl 53) : nan_pl 53 :=
 Next Obligation.
   destruct pl.
   simpl. rewrite Z.ltb_lt in *.
-  assert (forall x, S (Fcore_digits.digits2_Pnat x) = Pos.to_nat (Pos.size x)).
+  assert (forall x, Fcore_digits.digits2_pos x = Pos.size x).
   { induction x0; simpl; auto; rewrite IHx0; zify; omega. }
-  fold (Z.of_nat (S (Fcore_digits.digits2_Pnat (Pos.lor x 2251799813685248)))).
-  rewrite H, positive_nat_Z, Psize_log_inf, <- Zlog2_log_inf in *. clear H.
+  rewrite H, Psize_log_inf, <- Zlog2_log_inf in *. clear H.
   change (Z.pos (Pos.lor x 2251799813685248)) with (Z.lor (Z.pos x) 2251799813685248%Z).
   rewrite Z.log2_lor by (zify; omega).
   apply Z.max_case. auto. simpl. omega.
@@ -171,8 +170,8 @@ Definition expand_pl (pl: nan_pl 24) : nan_pl 53.
 Proof.
   refine (exist _ (Pos.shiftl_nat (proj1_sig pl) 29) _).
   abstract (
-    destruct pl; unfold proj1_sig, Pos.shiftl_nat, nat_iter, Fcore_digits.digits2_Pnat;
-    fold (Fcore_digits.digits2_Pnat x);
+    destruct pl; unfold proj1_sig, Pos.shiftl_nat, nat_iter, Fcore_digits.digits2_pos;
+    fold (Fcore_digits.digits2_pos x);
     rewrite Z.ltb_lt in *;
     zify; omega).
 Defined.
@@ -189,9 +188,11 @@ Proof.
   abstract (
     destruct pl; unfold proj1_sig, Pos.shiftr_nat, nat_iter;
     rewrite Z.ltb_lt in *;
-    assert (forall x, Fcore_digits.digits2_Pnat (Pos.div2 x) =
-                      (Fcore_digits.digits2_Pnat x - 1)%nat) by (destruct x0; simpl; zify; omega);
-    rewrite !H, <- !NPeano.Nat.sub_add_distr; zify; omega).
+    assert (forall x, Fcore_digits.digits2_pos (Pos.div2 x) =
+                      (Fcore_digits.digits2_pos x - 1)%positive)
+      by (destruct x0; simpl; auto; rewrite Pplus_one_succ_r, Pos.add_sub; auto);
+    rewrite !H, !Pos2Z.inj_sub_max;
+    repeat (apply Z.max_lub_lt; [reflexivity |apply Z.lt_sub_lt_add_l]); auto).
 Defined.
 
 Definition to_single_pl (s:bool) (pl:nan_pl 53) : (bool * nan_pl 24) :=
@@ -225,42 +226,46 @@ Definition binop_pl (x y: binary64) : bool*nan_pl 53 :=
 
 Definition zero: float := B754_zero _ _ false. (**r the float [+0.0] *)
 
-Definition eq_dec: forall (f1 f2: float), {f1 = f2} + {f1 <> f2} := b64_eq_dec.
+Definition eq_dec: forall (f1 f2: float), {f1 = f2} + {f1 <> f2} := Beq_dec _ _.
 
 (** Arithmetic operations *)
 
-Definition neg: float -> float := b64_opp neg_pl. (**r opposite (change sign) *)
-Definition abs: float -> float := b64_abs abs_pl. (**r absolute value (set sign to [+]) *)
-Definition add: float -> float -> float := b64_plus binop_pl mode_NE. (**r addition *)
-Definition sub: float -> float -> float := b64_minus binop_pl mode_NE. (**r subtraction *)
-Definition mul: float -> float -> float := b64_mult binop_pl mode_NE. (**r multiplication *)
-Definition div: float -> float -> float := b64_div binop_pl mode_NE. (**r division *)
+Definition neg: float -> float := Bopp _ _ neg_pl. (**r opposite (change sign) *)
+Definition abs: float -> float := Babs _ _ abs_pl. (**r absolute value (set sign to [+]) *)
+Definition add: float -> float -> float :=
+  Bplus 53 1024 __ __ binop_pl mode_NE. (**r addition *)
+Definition sub: float -> float -> float :=
+  Bminus 53 1024 __ __ binop_pl mode_NE. (**r subtraction *)
+Definition mul: float -> float -> float :=
+  Bmult 53 1024 __ __ binop_pl mode_NE. (**r multiplication *)
+Definition div: float -> float -> float :=
+  Bdiv 53 1024 __ __ binop_pl mode_NE. (**r division *)
 Definition cmp (c:comparison) (f1 f2: float) : bool := (**r comparison *)
-  cmp_of_comparison c (b64_compare f1 f2).
+  cmp_of_comparison c (Bcompare _ _ f1 f2).
 
 (** Conversions *)
 
-Definition of_single: float32 -> float := b64_of_b32 of_single_pl mode_NE.
-Definition to_single: float -> float32 := b32_of_b64 to_single_pl mode_NE.
+Definition of_single: float32 -> float := Bconv _ _ 53 1024 __ __ of_single_pl mode_NE.
+Definition to_single: float -> float32 := Bconv _ _ 24 128 __ __ to_single_pl mode_NE.
 
 Definition to_int (f:float): option int := (**r conversion to signed 32-bit int *)
-  option_map Int.repr (b64_to_Z_range f Int.min_signed Int.max_signed).
+  option_map Int.repr (ZofB_range _ _ f Int.min_signed Int.max_signed).
 Definition to_intu (f:float): option int := (**r conversion to unsigned 32-bit int *)
-  option_map Int.repr (b64_to_Z_range f 0 Int.max_unsigned).
+  option_map Int.repr (ZofB_range _ _ f 0 Int.max_unsigned).
 Definition to_long (f:float): option int64 := (**r conversion to signed 64-bit int *)
-  option_map Int64.repr (b64_to_Z_range f Int64.min_signed Int64.max_signed).
+  option_map Int64.repr (ZofB_range _ _ f Int64.min_signed Int64.max_signed).
 Definition to_longu (f:float): option int64 := (**r conversion to unsigned 64-bit int *)
-  option_map Int64.repr (b64_to_Z_range f 0 Int64.max_unsigned).
+  option_map Int64.repr (ZofB_range _ _ f 0 Int64.max_unsigned).
 
 Definition of_int (n:int): float := (**r conversion from signed 32-bit int *)
-  b64_of_Z (Int.signed n).
+  BofZ 53 1024 __ __ (Int.signed n).
 Definition of_intu (n:int): float:= (**r conversion from unsigned 32-bit int *)
-  b64_of_Z (Int.unsigned n).
+  BofZ 53 1024 __ __ (Int.unsigned n).
 
 Definition of_long (n:int64): float := (**r conversion from signed 64-bit int *)
-  b64_of_Z (Int64.signed n).
+  BofZ 53 1024 __ __ (Int64.signed n).
 Definition of_longu (n:int64): float:= (**r conversion from unsigned 64-bit int *)
-  b64_of_Z (Int64.unsigned n).
+  BofZ 53 1024 __ __ (Int64.unsigned n).
 
 Definition from_parsed (base:positive) (intPart:positive) (expPart:Z) : float :=
   build_from_parsed 53 1024 __ __ base intPart expPart.
@@ -323,7 +328,7 @@ Qed.
 
 (** Divisions that can be turned into multiplication by an inverse. *)
 
-Definition exact_inverse : float -> option float := b64_exact_inverse. 
+Definition exact_inverse : float -> option float := Bexact_inverse 53 1024 __ __. 
 
 Theorem div_mul_inverse:
   forall x y z, exact_inverse y = Some z -> div x y = mul x z.
@@ -340,7 +345,7 @@ Qed.
 Theorem cmp_swap:
   forall c x y, cmp (swap_comparison c) x y = cmp c y x.
 Proof.
-  unfold cmp, b64_compare; intros. rewrite (Bcompare_swap _ _ x y).
+  unfold cmp; intros. rewrite (Bcompare_swap _ _ x y).
   apply cmp_of_comparison_swap. 
 Qed.
 
@@ -422,7 +427,7 @@ Theorem of_intu_of_int_2:
   Int.ltu x ox8000_0000 = false ->
   of_intu x = add (of_int (Int.sub x ox8000_0000)) (of_intu ox8000_0000).
 Proof.
-  unfold add, b64_plus, of_intu, of_int, b64_of_Z; intros.
+  unfold add, of_intu, of_int; intros.
   set (y := Int.sub x ox8000_0000).
   pose proof (Int.unsigned_range x); pose proof (Int.signed_range y).
   assert (Ry: integer_representable 53 1024 (Int.signed y)).
@@ -443,9 +448,9 @@ Theorem to_intu_to_int_1:
   to_int x = Some n.
 Proof.
   intros. unfold to_intu in H0. 
-  destruct (b64_to_Z_range x 0 Int.max_unsigned) as [p|] eqn:E; simpl in H0; inv H0.
-  unfold b64_to_Z_range in E. exploit ZofB_range_inversion; eauto. intros (A & B & C).
-  unfold to_int, b64_to_Z_range. unfold ZofB_range. rewrite C. 
+  destruct (ZofB_range 53 1024 x 0 Int.max_unsigned) as [p|] eqn:E; simpl in H0; inv H0.
+  exploit ZofB_range_inversion; eauto. intros (A & B & C).
+  unfold to_int, ZofB_range. rewrite C. 
   rewrite Zle_bool_true by smart_omega. rewrite Zle_bool_true; auto.
   exploit (BofZ_exact 53 1024 __ __ (Int.unsigned ox8000_0000)).
   vm_compute; intuition congruence.
@@ -457,9 +462,9 @@ Proof.
   destruct (zeq p 0). 
   subst p; smart_omega.
   destruct (ZofB_range_pos 53 1024 __ __ x p C) as [P Q]. omega.
-  assert (CMP: b64_compare x y = Some Lt). 
-  { unfold cmp, cmp_of_comparison in H. destruct (b64_compare x y) as [[]|]; auto; discriminate. }
-  unfold b64_compare in CMP. rewrite Bcompare_finite_correct in CMP by auto. 
+  assert (CMP: Bcompare _ _ x y = Some Lt). 
+  { unfold cmp, cmp_of_comparison in H. destruct (Bcompare _ _ x y) as [[]|]; auto; discriminate. }
+  rewrite Bcompare_correct in CMP by auto. 
   inv CMP. apply Rcompare_Lt_inv in H1. rewrite EQy in H1.
   assert (p < Int.unsigned ox8000_0000).
   { apply lt_Z2R. eapply Rle_lt_trans; eauto. }
@@ -473,8 +478,8 @@ Theorem to_intu_to_int_2:
   to_int (sub x (of_intu ox8000_0000)) = Some (Int.sub n ox8000_0000).
 Proof.
   intros. unfold to_intu in H0. 
-  destruct (b64_to_Z_range x 0 Int.max_unsigned) as [p|] eqn:E; simpl in H0; inv H0.
-  unfold b64_to_Z_range in E. exploit ZofB_range_inversion; eauto. intros (A & B & C).
+  destruct (ZofB_range _ _ x 0 Int.max_unsigned) as [p|] eqn:E; simpl in H0; inv H0.
+  exploit ZofB_range_inversion; eauto. intros (A & B & C).
   exploit (BofZ_exact 53 1024 __ __ (Int.unsigned ox8000_0000)).
   vm_compute; intuition congruence.
   set (y := of_intu ox8000_0000) in *.
@@ -483,14 +488,14 @@ Proof.
   assert (FINx: is_finite _ _ x = true).
   { rewrite ZofB_correct in C. destruct (is_finite _ _ x) eqn:FINx; congruence. }
   assert (GE: (B2R _ _ x >= Z2R (Int.unsigned ox8000_0000))%R).
-  { rewrite <- EQy. unfold cmp, cmp_of_comparison, b64_compare in H.
-    rewrite Bcompare_finite_correct in H by auto. 
+  { rewrite <- EQy. unfold cmp, cmp_of_comparison in H.
+    rewrite Bcompare_correct in H by auto. 
     destruct (Rcompare (B2R 53 1024 x) (B2R 53 1024 y)) eqn:CMP.
     apply Req_ge; apply Rcompare_Eq_inv; auto.
     discriminate.
     apply Rgt_ge; apply Rcompare_Gt_inv; auto. 
   } 
-  assert (EQ: b64_to_Z_range (sub x y) Int.min_signed Int.max_signed = Some (p - Int.unsigned ox8000_0000)).
+  assert (EQ: ZofB_range _ _ (sub x y) Int.min_signed Int.max_signed = Some (p - Int.unsigned ox8000_0000)).
   {
     apply ZofB_range_minus. exact E. 
     compute_this (Int.unsigned ox8000_0000). smart_omega.
@@ -555,8 +560,8 @@ Theorem of_intu_from_words:
   of_intu x = sub (from_words ox4330_0000 x) (from_words ox4330_0000 Int.zero).
 Proof.
   intros. pose proof (Int.unsigned_range x).
-  rewrite ! from_words_eq. unfold sub, b64_minus. rewrite BofZ_minus. 
-  unfold of_intu, b64_of_Z. f_equal. rewrite Int.unsigned_zero. omega.
+  rewrite ! from_words_eq. unfold sub. rewrite BofZ_minus. 
+  unfold of_intu. f_equal. rewrite Int.unsigned_zero. omega.
   apply integer_representable_n; auto; smart_omega.
   apply integer_representable_n; auto; rewrite Int.unsigned_zero; smart_omega.
 Qed.
@@ -582,8 +587,8 @@ Proof.
   pose proof (Int.signed_range x).
   rewrite ! from_words_eq. rewrite ox8000_0000_signed_unsigned.
   change (Int.unsigned ox8000_0000) with Int.half_modulus.
-  unfold sub, b64_minus. rewrite BofZ_minus. 
-  unfold of_int, b64_of_Z. f_equal. omega.
+  unfold sub. rewrite BofZ_minus. 
+  unfold of_int. f_equal. omega.
   apply integer_representable_n; auto; smart_omega.
   apply integer_representable_n; auto; smart_omega.
 Qed.
@@ -654,11 +659,11 @@ Proof.
   set (x := Int64.unsigned l) in *;
   set (xl := Int.unsigned (Int64.loword l)) in *;
   set (xh := Int.unsigned (Int64.hiword l)) in *.
-  unfold sub, b64_minus. rewrite BofZ_minus.
+  unfold sub. rewrite BofZ_minus.
   replace (2^84 + xh * 2^32 - (2^84 + p20 * 2^32))
      with ((xh - p20) * 2^32) by ring.
-  unfold add, b64_plus. rewrite BofZ_plus. 
-  unfold of_longu, b64_of_Z. f_equal. 
+  unfold add. rewrite BofZ_plus. 
+  unfold of_longu. f_equal. 
   rewrite <- (Int64.ofwords_recompose l) at 1. rewrite Int64.ofwords_add'.
   fold xh; fold xl. compute_this (two_p 32); compute_this p20; ring.
   apply integer_representable_n2p; auto.
@@ -687,12 +692,12 @@ Proof.
   set (xl := Int.unsigned (Int64.loword l)) in *;
   set (xh := Int.signed (Int64.hiword l)) in *.
   rewrite ox8000_0000_signed_unsigned. fold xh. 
-  unfold sub, b64_minus. rewrite BofZ_minus.
+  unfold sub. rewrite BofZ_minus.
   replace (2^84 + (xh + Int.half_modulus) * 2^32 - (2^84 + p * 2^32))
      with ((xh - 2^20) * 2^32) 
        by (compute_this p; compute_this Int.half_modulus; ring).
-  unfold add, b64_plus. rewrite BofZ_plus. 
-  unfold of_long, b64_of_Z. f_equal. 
+  unfold add. rewrite BofZ_plus. 
+  unfold of_long. f_equal. 
   rewrite <- (Int64.ofwords_recompose l) at 1. rewrite Int64.ofwords_add''.
   fold xh; fold xl. compute_this (two_p 32); ring. 
   apply integer_representable_n2p; auto.
@@ -712,11 +717,11 @@ Qed.
 
 Theorem of_longu_decomp:
   forall l,
-  of_longu l = add (mul (of_intu (Int64.hiword l)) (b64_of_Z (2^32)))
+  of_longu l = add (mul (of_intu (Int64.hiword l)) (BofZ 53 1024 __ __ (2^32)))
                    (of_intu (Int64.loword l)).
 Proof.
   intros.
-  unfold of_longu, of_intu, b64_of_Z, add, mul, b64_plus, b64_mult.
+  unfold of_longu, of_intu, add, mul.
   pose proof (Int.unsigned_range (Int64.loword l)).
   pose proof (Int.unsigned_range (Int64.hiword l)).
   pose proof (Int64.unsigned_range l).
@@ -735,11 +740,11 @@ Qed.
 
 Theorem of_long_decomp:
   forall l,
-  of_long l = add (mul (of_int (Int64.hiword l)) (b64_of_Z (2^32)))
+  of_long l = add (mul (of_int (Int64.hiword l)) (BofZ 53 1024 __ __ (2^32)))
                   (of_intu (Int64.loword l)).
 Proof.
   intros.
-  unfold of_long, of_int, of_intu, b64_of_Z, add, mul, b64_plus, b64_mult.
+  unfold of_long, of_int, of_intu, add, mul.
   pose proof (Int.unsigned_range (Int64.loword l)).
   pose proof (Int.signed_range (Int64.hiword l)).
   pose proof (Int64.signed_range l).
@@ -823,7 +828,7 @@ Proof.
   change (2^0) with 1 in B0; rewrite Zdiv_1_r in B0; rewrite B0; auto.
   intros. rewrite NB2 by omega. rewrite ! dec_eq_false by omega. auto.
   }
-  unfold mul, of_long, of_longu, b64_mult, b64_of_Z. 
+  unfold mul, of_long, of_longu. 
   rewrite BofZ_mult_2p. 
 - change (2^1) with 2. rewrite EQ. apply BofZ_round_odd with (p := 1).
 + omega.
@@ -853,11 +858,10 @@ Program Definition transform_quiet_pl (pl:nan_pl 24) : nan_pl 24 :=
 Next Obligation.
   destruct pl.
   simpl. rewrite Z.ltb_lt in *.
-  assert (forall x, S (Fcore_digits.digits2_Pnat x) = Pos.to_nat (Pos.size x)).
+  assert (forall x, Fcore_digits.digits2_pos x = Pos.size x).
   { induction x0; simpl; auto; rewrite IHx0; zify; omega. }
-  fold (Z.of_nat (S (Fcore_digits.digits2_Pnat (Pos.lor x 4194304)))).
-  rewrite H, positive_nat_Z, Psize_log_inf, <- Zlog2_log_inf in *. clear H.
-  change (Z.pos (Pos.lor x 4194304)) with (Z.lor (Z.pos x) 4194304).
+  rewrite H, Psize_log_inf, <- Zlog2_log_inf in *. clear H.
+  change (Z.pos (Pos.lor x 4194304)) with (Z.lor (Z.pos x) 4194304%Z).
   rewrite Z.log2_lor by (zify; omega).
   apply Z.max_case. auto. simpl. omega.
 Qed.
@@ -887,18 +891,22 @@ Definition binop_pl (x y: binary32) : bool*nan_pl 24 :=
 
 Definition zero: float32 := B754_zero _ _ false. (**r the float [+0.0] *)
 
-Definition eq_dec: forall (f1 f2: float32), {f1 = f2} + {f1 <> f2} := b32_eq_dec.
+Definition eq_dec: forall (f1 f2: float32), {f1 = f2} + {f1 <> f2} := Beq_dec _ _.
 
 (** Arithmetic operations *)
 
-Definition neg: float32 -> float32 := b32_opp neg_pl. (**r opposite (change sign) *)
-Definition abs: float32 -> float32 := b32_abs abs_pl. (**r absolute value (set sign to [+]) *)
-Definition add: float32 -> float32 -> float32 := b32_plus binop_pl mode_NE. (**r addition *)
-Definition sub: float32 -> float32 -> float32 := b32_minus binop_pl mode_NE. (**r subtraction *)
-Definition mul: float32 -> float32 -> float32 := b32_mult binop_pl mode_NE. (**r multiplication *)
-Definition div: float32 -> float32 -> float32 := b32_div binop_pl mode_NE. (**r division *)
+Definition neg: float32 -> float32 := Bopp _ _ neg_pl. (**r opposite (change sign) *)
+Definition abs: float32 -> float32 := Babs _ _ abs_pl. (**r absolute value (set sign to [+]) *)
+Definition add: float32 -> float32 -> float32 :=
+  Bplus 24 128 __ __ binop_pl mode_NE. (**r addition *)
+Definition sub: float32 -> float32 -> float32 :=
+  Bminus 24 128 __ __ binop_pl mode_NE. (**r subtraction *)
+Definition mul: float32 -> float32 -> float32 :=
+  Bmult 24 128 __ __ binop_pl mode_NE. (**r multiplication *)
+Definition div: float32 -> float32 -> float32 :=
+  Bdiv 24 128 __ __ binop_pl mode_NE. (**r division *)
 Definition cmp (c:comparison) (f1 f2: float32) : bool := (**r comparison *)
-  cmp_of_comparison c (b32_compare f1 f2).
+  cmp_of_comparison c (Bcompare _ _ f1 f2).
 
 (** Conversions *)
 
@@ -906,23 +914,23 @@ Definition of_double : float -> float32 := Float.to_single.
 Definition to_double : float32 -> float := Float.of_single.
 
 Definition to_int (f:float32): option int := (**r conversion to signed 32-bit int *)
-  option_map Int.repr (b32_to_Z_range f Int.min_signed Int.max_signed).
+  option_map Int.repr (ZofB_range _ _ f Int.min_signed Int.max_signed).
 Definition to_intu (f:float32): option int := (**r conversion to unsigned 32-bit int *)
-  option_map Int.repr (b32_to_Z_range f 0 Int.max_unsigned).
+  option_map Int.repr (ZofB_range _ _ f 0 Int.max_unsigned).
 Definition to_long (f:float32): option int64 := (**r conversion to signed 64-bit int *)
-  option_map Int64.repr (b32_to_Z_range f Int64.min_signed Int64.max_signed).
+  option_map Int64.repr (ZofB_range _ _ f Int64.min_signed Int64.max_signed).
 Definition to_longu (f:float32): option int64 := (**r conversion to unsigned 64-bit int *)
-  option_map Int64.repr (b32_to_Z_range f 0 Int64.max_unsigned).
+  option_map Int64.repr (ZofB_range _ _ f 0 Int64.max_unsigned).
 
 Definition of_int (n:int): float32 := (**r conversion from signed 32-bit int to single-precision float *)
-  b32_of_Z (Int.signed n).
+  BofZ 24 128 __ __ (Int.signed n).
 Definition of_intu (n:int): float32 := (**r conversion from unsigned 32-bit int to single-precision float *)
-  b32_of_Z (Int.unsigned n).
+  BofZ 24 128 __ __ (Int.unsigned n).
 
 Definition of_long (n:int64): float32 := (**r conversion from signed 64-bit int to single-precision float *)
-  b32_of_Z (Int64.signed n).
+  BofZ 24 128 __ __ (Int64.signed n).
 Definition of_longu (n:int64): float32 := (**r conversion from unsigned 64-bit int to single-precision float *)
-  b32_of_Z (Int64.unsigned n).
+  BofZ 24 128 __ __ (Int64.unsigned n).
 
 Definition from_parsed (base:positive) (intPart:positive) (expPart:Z) : float32 :=
   build_from_parsed 24 128 __ __ base intPart expPart.
@@ -965,7 +973,7 @@ Qed.
 
 (** Divisions that can be turned into multiplication by an inverse. *)
 
-Definition exact_inverse : float32 -> option float32 := b32_exact_inverse. 
+Definition exact_inverse : float32 -> option float32 := Bexact_inverse 24 128 __ __.
 
 Theorem div_mul_inverse:
   forall x y z, exact_inverse y = Some z -> div x y = mul x z.
@@ -982,7 +990,7 @@ Qed.
 Theorem cmp_swap:
   forall c x y, cmp (swap_comparison c) x y = cmp c y x.
 Proof.
-  unfold cmp, b32_compare; intros. rewrite (Bcompare_swap _ _ x y).
+  unfold cmp; intros. rewrite (Bcompare_swap _ _ x y).
   apply cmp_of_comparison_swap. 
 Qed.
 
@@ -1076,8 +1084,8 @@ Theorem to_int_double:
 Proof.
   intros.
   unfold to_int in H.
-  destruct (b32_to_Z_range f Int.min_signed Int.max_signed) as [n'|] eqn:E; inv H.
-  unfold Float.to_int, to_double, Float.of_single, b64_to_Z_range, b64_of_b32. 
+  destruct (ZofB_range _ _ f Int.min_signed Int.max_signed) as [n'|] eqn:E; inv H.
+  unfold Float.to_int, to_double, Float.of_single. 
   erewrite ZofB_range_Bconv; eauto. auto. omega. omega. omega. omega. 
 Qed.
 
@@ -1086,8 +1094,8 @@ Theorem to_intu_double:
 Proof.
   intros.
   unfold to_intu in H.
-  destruct (b32_to_Z_range f 0 Int.max_unsigned) as [n'|] eqn:E; inv H.
-  unfold Float.to_intu, to_double, Float.of_single, b64_to_Z_range, b64_of_b32. 
+  destruct (ZofB_range _ _ f 0 Int.max_unsigned) as [n'|] eqn:E; inv H.
+  unfold Float.to_intu, to_double, Float.of_single. 
   erewrite ZofB_range_Bconv; eauto. auto. omega. omega. omega. omega. 
 Qed.
 
@@ -1096,8 +1104,8 @@ Theorem to_long_double:
 Proof.
   intros.
   unfold to_long in H.
-  destruct (b32_to_Z_range f Int64.min_signed Int64.max_signed) as [n'|] eqn:E; inv H.
-  unfold Float.to_long, to_double, Float.of_single, b64_to_Z_range, b64_of_b32. 
+  destruct (ZofB_range _ _ f Int64.min_signed Int64.max_signed) as [n'|] eqn:E; inv H.
+  unfold Float.to_long, to_double, Float.of_single. 
   erewrite ZofB_range_Bconv; eauto. auto. omega. omega. omega. omega. 
 Qed.
 
@@ -1106,8 +1114,8 @@ Theorem to_longu_double:
 Proof.
   intros.
   unfold to_longu in H.
-  destruct (b32_to_Z_range f 0 Int64.max_unsigned) as [n'|] eqn:E; inv H.
-  unfold Float.to_longu, to_double, Float.of_single, b64_to_Z_range, b64_of_b32. 
+  destruct (ZofB_range _ _ f 0 Int64.max_unsigned) as [n'|] eqn:E; inv H.
+  unfold Float.to_longu, to_double, Float.of_single. 
   erewrite ZofB_range_Bconv; eauto. auto. omega. omega. omega. omega. 
 Qed.
 
@@ -1160,14 +1168,13 @@ Qed.
 Lemma of_long_round_odd:
   forall n conv_nan,
   2^36 <= Z.abs n < 2^64 ->
-  b32_of_Z n = b32_of_b64 conv_nan mode_NE (b64_of_Z (Z.land (Z.lor n ((Z.land n 2047) + 2047)) (-2048))).
+  BofZ 24 128 __ __ n = Bconv _ _ 24 128 __ __ conv_nan mode_NE (BofZ 53 1024 __ __ (Z.land (Z.lor n ((Z.land n 2047) + 2047)) (-2048))).
 Proof.
   intros. rewrite <- (int_round_odd_plus 11) by omega.
   assert (-2^64 <= int_round_odd n 11). 
   { change (-2^64) with (int_round_odd (-2^64) 11). apply (int_round_odd_le 0 0); xomega. }
   assert (int_round_odd n 11 <= 2^64). 
   { change (2^64) with (int_round_odd (2^64) 11). apply (int_round_odd_le 0 0); xomega. }
-  unfold b32_of_Z, b32_of_b64, b64_of_Z. 
   rewrite Bconv_BofZ. 
   apply BofZ_round_odd with (p := 11).
   omega.