From f8d32a19caf88733a9bbeee976f5c2fc549d4f92 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 11 Feb 2022 10:32:15 +0100
Subject: rewrite with longu -> double -> single conversions

---
 kvx/FPDivision64.v | 61 ++++++++++++++++++++++++++++++++++--------------------
 1 file changed, 38 insertions(+), 23 deletions(-)

(limited to 'kvx')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 411865ba..a4d609f0 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -532,7 +532,7 @@ Proof.
 Qed.
 
 Definition step1_real_inv_longu b :=
-  let invb_s := ExtValues.invfs (Val.maketotal (Val.singleoflongu b)) in
+  let invb_s := ExtValues.invfs (Val.singleoffloat (Val.maketotal (Val.floatoflongu b))) in
   Val.floatofsingle invb_s.
 
 Definition step1_real_inv_thresh := (3/33554432)%R.
@@ -543,7 +543,7 @@ Theorem step1_real_inv_longu_correct :
     (0 < Int64.unsigned b)%Z ->
     exists (f : float),
       (step1_real_inv_longu (Vlong b)) = Vfloat f /\
-        (B2R _ _ f) = (rd (rs (1 / rs (IZR (Int64.unsigned b))))) /\
+        (B2R _ _ f) = (rd (rs (1 / rs (rd (IZR (Int64.unsigned b)))))) /\
         is_finite _ _ f = true /\
         Bsign _ _ f = false.
 Proof.
@@ -553,8 +553,8 @@ Proof.
   econstructor.
   split.
   reflexivity.
-  Local Transparent Float.neg Float.of_single Float32.of_longu Float32.div Float.of_longu Float32.of_int Float.of_int.
-  unfold Float.fma, Float.neg, Float.of_single, Float32.of_longu, ExtFloat32.inv, Float32.div, Float.of_longu, ExtFloat32.one, Float32.of_int, ExtFloat.one, Float.of_int.
+  Local Transparent Float.neg Float.of_single Float32.of_longu Float32.div Float.of_longu Float32.of_int Float.of_int Float.to_single.
+  unfold Float.fma, Float.neg, Float.of_single, Float32.of_longu, ExtFloat32.inv, Float32.div, Float.of_longu, ExtFloat32.one, Float32.of_int, ExtFloat.one, Float.of_int, Float.to_single.
   set (re := (@eq_refl Datatypes.comparison Lt)).
   change (Int.signed (Int.repr 1)) with 1%Z.
   set (b' := Int64.unsigned b) in *.
@@ -565,25 +565,37 @@ Proof.
   }
 
   assert (-16777216 <= 1 <= 16777216)%Z as SILLY by lia.
-  destruct (BofZ_exact 24 128 re re 1 SILLY) as (C0R & C0F & _).
+  destruct (BofZ_exact 24 128 re re 1 SILLY) as (C0R & C0F & C0S).
   clear SILLY.
   set (one_s := (BofZ 24 128 re re 1)) in *.
-  
-  pose proof (BofZ_correct 24 128 re re b') as C1.
-  cbn in C1.
+
+  pose proof (BofZ_correct 53 1024 re re b') as C0'.
+  rewrite Rlt_bool_true in C0'; cycle 1.
+  { apply (Rabs_relax (bpow radix2 64)).
+    { apply bpow_lt. lia. }
+    cbn.
+    gappa.
+  }
+  cbn in C0'.
+  destruct C0' as (C0'R & C0'F & C0'S).
+  set (b_d :=  (BofZ 53 1024 re re b')) in *.
+
+  pose proof (Bconv_correct 53 1024 24 128 re re Float.to_single_nan mode_NE b_d C0'F) as C1.
+  rewrite C0'R in C1.
+  rewrite C0'S in C1.
   rewrite Rlt_bool_true in C1; cycle 1.
   { clear C1.
-    eapply (Rabs_relax (IZR 18446744073709551616)).
-    lra.
-    set (b'' := IZR b') in *.
+    eapply (Rabs_relax (bpow radix2 64)).
+    { apply bpow_lt. lia. }
+    cbn.
     gappa.
   }
-  rewrite (Zlt_bool_false b' 0) in C1 by lia.
   destruct C1 as (C1R & C1F & C1S).
-  set (b_s :=  (BofZ 24 128 re re b')) in *.
+  set (b_s := (Bconv 53 1024 24 128 re re Float.to_single_nan mode_NE b_d)) in *.
 
   assert(1 <= B2R 24 128 b_s <= 18446744073709551616)%R as b_s_RANGE.
   { rewrite C1R.
+    cbn.
     gappa.
   }
   assert(B2R 24 128 b_s <> 0)%R as b_s_NONZ by lra.
@@ -599,9 +611,12 @@ Proof.
     gappa.
   }
   rewrite C1R in C2.
+  rewrite C1S in C2.
+  rewrite C0S in C2.
   destruct C2 as (C2R & C2F & C2Sz).
-  rewrite C1S in C2Sz.
-  change (xorb _ _) with false in C2Sz.
+  change (1 <? 0)%Z with false in C2Sz.
+  replace (b' <? 0)%Z with false in C2Sz by lia.
+  change (xorb false false) with false in C2Sz.
   set (invb_s := (Bdiv 24 128 re re Float32.binop_nan mode_NE one_s b_s)) in *.
   rewrite C0F in C2F.
   assert (is_nan 24 128 invb_s = false) as NAN.
@@ -709,7 +724,7 @@ Definition step1_div_longu a b :=
   Val.maketotal (Val.longuoffloat_ne (step1_real_div_longu a b)).
 
 Definition step1_real_quotient (a b : R) :=
-             rd ((rd (a)) * (rd (rs (1 / rs (b))))).
+             rd ((rd (a)) * (rd (rs (1 / rs (rd (b)))))).
   
 Theorem step1_real_div_longu_correct:
   forall a b,
@@ -794,10 +809,10 @@ Proof.
   unfold smallb_thresh in b_RANGE.
   unfold smallb_approx_real_range.
   unfold step1_real_quotient.
-  set (q := ((rd (a)) * (rd (rs (1 / rs (b)))))%R) in *.
+  set (q := ((rd (a)) * (rd (rs (1 / rs (rd b)))))%R) in *.
   replace ((rd q) *b - a)%R with
-     ((rd(q)-q)/q * rd(a) * (1 + (rd (rs (1 / rs (b))) - 1/b)/(1/b)) +
-  (rd (a)) * ((rd (rs (1 / rs (b))) - 1 / b) / (1/b)) +
+     ((rd(q)-q)/q * rd(a) * (1 + (rd (rs (1 / rs (rd b))) - 1/b)/(1/b)) +
+  (rd (a)) * ((rd (rs (1 / rs (rd b))) - 1 / b) / (1/b)) +
         (rd(a) - a))%R; cycle 1.
   { unfold q.
     field.
@@ -1140,7 +1155,7 @@ Proof.
   }
   cbn.
   econstructor; split. reflexivity.
-  set (q_r := (rd (rd (IZR a') * rd (rs (1 / rs (IZR b')))))%R).
+  set (q_r := (rd (rd (IZR a') * rd (rs (1 / rs ( rd (IZR b'))))))%R).
   assert (Rabs (IZR (ZnearestE q_r) - q_r) <= /2)%R as NEAR by apply Znearest_imp2.
   set (delta1 := (IZR (ZnearestE q_r) - q_r)%R) in NEAR.
   apply le_IZR3.
@@ -1159,11 +1174,11 @@ Proof.
   unfold q_r.
   set (a1 := IZR a') in *. 
   set (b1 := IZR b') in *.
-  replace (rd (rd a1 * rd (rs (1 / rs b1))))%R with
-    ((((rd (rd a1 * rd (rs (1 / rs b1)))-(a1 * (1 / b1))) / (a1 * (1 / b1)))+1) * (a1 / b1))%R;
+  replace (rd (rd a1 * rd (rs (1 / rs (rd b1)))))%R with
+    ((((rd (rd a1 * rd (rs (1 / rs (rd b1))))-(a1 * (1 / b1))) / (a1 * (1 / b1)))+1) * (a1 / b1))%R;
     cycle 1.
   { field. lra. }
-  set (delta2 := ((rd (rd a1 * rd (rs (1 / rs b1)))-(a1 * (1 / b1))) / (a1 * (1 / b1)))%R) in *.
+  set (delta2 := ((rd (rd a1 * rd (rs (1 / rs (rd b1))))-(a1 * (1 / b1))) / (a1 * (1 / b1)))%R) in *.
   (* assert (Rabs (delta2) <= 1/4194304)%R.
   {  unfold delta2. gappa. } *)
   replace (a1 - b1 * (delta1 + (delta2 + 1) * (a1 / b1)))%R with
-- 
cgit