From cf534a7a5144f4dadc0b98fc078cd2b11530650f Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 7 Jan 2022 23:02:33 +0100
Subject: qed for proof

---
 kvx/FPDivision64.v | 39 +++++++++++++++++++++++++++++++++++++--
 1 file changed, 37 insertions(+), 2 deletions(-)

(limited to 'kvx')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index f61cc48c..608b3710 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -242,5 +242,40 @@ Proof.
     field.
     lra.
   }
-  
-Admitted.
+  assert(Rabs alpha0 <= 257/2147483648)%R as alpha0_ABS.
+  { rewrite alpha0_EQ.
+    unfold x0, bd.
+    gappa.
+  }
+  assert (Rabs (x0 - 1 / b1) <= 3/33554432)%R as x0_delta_ABS.
+  { unfold x0.
+    gappa.
+  }
+  set (x0_delta := (x0 - 1 / b1)%R) in *.
+  assert (Rabs ((bd - b1) / b1) <= 1/9007199254740992)%R as bd_delta_ABS.
+  { unfold bd.
+    gappa.
+  }
+  set (bd_delta := ((bd - b1) / b1)%R) in *.
+  set (rnd_alpha0_delta := (round radix2 (FLT_exp (-1074) 53) ZnearestE alpha0 - alpha0)%R) in *.
+  assert (Rabs rnd_alpha0_delta <= 1/75557863725914323419136)%R as rnd_alpha0_delta_ABS.
+  { unfold rnd_alpha0_delta.
+    gappa.
+  }
+  assert (1/18446744073709551616 <= x0 <= 1)%R as x0_RANGE.
+  { unfold x0.
+    gappa.
+  }
+  assert (Rabs (y1 - 1 / b1) <= 49/4503599627370496)%R as y1_delta_ABS.
+  { rewrite y1_EQ.
+    gappa.
+  }
+  assert (Rabs(x1 - y1) <= 1/9007199254740992)%R as x1_delta_ABS.
+  { unfold x1.
+    gappa.
+  }
+  set (y1_delta := (y1 - 1 / b1)%R) in *.
+  set (x1_delta := (x1-y1)%R) in *.
+  unfold approx_inv_thresh.
+  gappa.
+Qed.
-- 
cgit