From 4f8bd24d05bcea0a8b9793ee61450b1e0c7234c1 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 7 Jan 2022 15:17:12 +0100
Subject: this works

---
 kvx/FPDivision64.v | 31 ++++++++++++++++++++-----------
 1 file changed, 20 insertions(+), 11 deletions(-)

(limited to 'kvx')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 33a980c6..424dfc77 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -1,3 +1,12 @@
+(*
+This needs a special gappa script
+
+#!/bin/sh
+/home/monniaux/.opam/4.12.0+flambda/bin/gappa -Eprecision=100 "$@"
+
+in PATH before the normal gappa
+ *)
+
 From Flocq Require Import Core Digits Operations Round Bracket Sterbenz
                           Binary Round_odd Bits.
 Require Archi.
@@ -38,10 +47,10 @@ Proof.
   apply Rabs_lt.
   lra.
 Qed.
-
+    
 Theorem approx_inv_longu_correct :
   forall b,
-    (1 <= Int64.unsigned b <= 9223372036854775808)%Z ->
+    (1 <= Int64.unsigned b <= 18446744073709551616)%Z ->
     exists (f : float),
       (approx_inv_longu (Vlong b)) = Vfloat f /\
       is_finite _ _ f = true /\ (Rabs((B2R _ _ f) - (1 / IZR (Int64.unsigned b))) <= approx_inv_thresh)%R.
@@ -57,7 +66,7 @@ Proof.
   set (re := (@eq_refl Datatypes.comparison Lt)).
   change (Int.signed (Int.repr 1)) with 1%Z.
   set (b' := Int64.unsigned b) in *.
-  assert(1 <= IZR b' <= 9223372036854775808)%R as RANGE.
+  assert(1 <= IZR b' <= 18446744073709551616)%R as RANGE.
   { split; apply IZR_le; lia.
   }
 
@@ -70,7 +79,7 @@ Proof.
   cbn in C1.
   rewrite Rlt_bool_true in C1; cycle 1.
   { clear C1.
-    eapply (Rabs_relax (IZR 9223372036854775808)).
+    eapply (Rabs_relax (IZR 18446744073709551616)).
     lra.
     set (b'' := IZR b') in *.
     gappa.
@@ -78,7 +87,7 @@ Proof.
   destruct C1 as (C1R & C1F & _).
   set (b_s :=  (BofZ 24 128 re re b')) in *.
 
-  assert(1 <= B2R 24 128 b_s <= 9223372036854775808)%R as b_s_RANGE.
+  assert(1 <= B2R 24 128 b_s <= 18446744073709551616)%R as b_s_RANGE.
   { rewrite C1R.
     gappa.
   }
@@ -99,7 +108,7 @@ Proof.
   set (invb_s := (Bdiv 24 128 re re Float32.binop_nan mode_NE one_s b_s)) in *.
   rewrite C0F in C2F.
 
-  assert ((1/9223372036854775808 <= B2R 24 128 invb_s <= 1)%R) as invb_s_RANGE.
+  assert ((1/18446744073709551616 <= B2R 24 128 invb_s <= 1)%R) as invb_s_RANGE.
   { rewrite C2R.
     set (r_b_s := B2R 24 128 b_s) in *.
     rewrite C0R.
@@ -122,7 +131,7 @@ Proof.
   
   destruct C3 as (C3R & C3F & _).
   set (invb_d :=  (Bconv 24 128 53 1024 re re Float.of_single_nan mode_NE invb_s)) in *.
-  assert ((1/9223372036854775808 <= B2R 53 1024 invb_d <= 1)%R) as invb_d_RANGE.
+  assert ((1/18446744073709551616 <= B2R 53 1024 invb_d <= 1)%R) as invb_d_RANGE.
   { 
     rewrite C3R.
     set (r_invb_s := B2R 24 128 invb_s) in *.
@@ -137,7 +146,7 @@ Proof.
   rewrite Rlt_bool_true in C4; cycle 1.
   { clear C4.
     cbn.
-    eapply (Rabs_relax (IZR 9223372036854775808)).
+    eapply (Rabs_relax (IZR 18446744073709551616)).
     lra.
     set (b'' := IZR b') in *.
     gappa.
@@ -148,7 +157,7 @@ Proof.
   cbn in C5.
   rewrite Rlt_bool_true in C5; cycle 1.
   { clear C5.
-    eapply (Rabs_relax (IZR 9223372036854775808)).
+    eapply (Rabs_relax (IZR 18446744073709551616)).
     lra.
     set (b'' := IZR b') in *.
     gappa.
@@ -156,7 +165,7 @@ Proof.
   destruct C5 as (C5R & C5F & _).
   set (b_d :=  (BofZ 53 1024 re re b')) in *.
   
-  assert(1 <= B2R 53 1024 b_d <= 9223372036854775808)%R as b_d_RANGE.
+  assert(1 <= B2R 53 1024 b_d <= 18446744073709551616)%R as b_d_RANGE.
   { rewrite C5R.
     gappa.
   }
@@ -169,7 +178,7 @@ Proof.
     rewrite C4R.
     rewrite B2R_Bopp.
     cbn.
-    eapply (Rabs_relax (IZR 9223372036854775808)).
+    eapply (Rabs_relax (IZR 18446744073709551616)).
     { lra. }
     fold invb_d.
     fold b_d.
-- 
cgit