From ec337b6e5be76b69b4c82af682a08cfec2a8e12a Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sun, 22 Dec 2019 11:07:01 +0400
Subject: Do not hide constants from the compiler.

---
 kernel/uint63_31.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index e38389ca13..df8a354dcf 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -15,8 +15,8 @@ let _ = assert (Sys.word_size = 32)
 
 let uint_size = 63
 
-let maxuint63 = Int64.of_string "0x7FFFFFFFFFFFFFFF"
-let maxuint31 = Int64.of_string "0x7FFFFFFF"
+let maxuint63 = 0x7FFF_FFFF_FFFF_FFFFL
+let maxuint31 = 0x7FFF_FFFFL
 
 let zero = Int64.zero
 let one = Int64.one
-- 
cgit v1.2.3


From 6e8c8068a8cbaf34dbb5e32a2eda61f190737f86 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sun, 22 Dec 2019 11:09:54 +0400
Subject: Simplify equality of 63-bit integers.

The sign bit is supposed to be zero, so no need to mask it out. If it was
not zero, most of the algorithms in this file would fail horribly.
---
 kernel/uint63_31.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index df8a354dcf..3d7dd1792a 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -138,7 +138,7 @@ let mulc x y =
   then Int64.(sub !hr one, mask63 !lr)
   else (!hr, !lr)
 
-let equal x y = mask63 x = mask63 y
+let equal (x : t) y = x = y
 
 let compare x y = Int64.compare x y
 
-- 
cgit v1.2.3


From 4e176a7ee4660d505321ca55c5ce70a6c3d50d3b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sun, 22 Dec 2019 11:17:22 +0400
Subject: Use a more straightforward algorithm for mulc on 32-bit
 architectures. (Fixes #11321)

It has the added advantage of performing 6 less 64-bit operations per
long multiplication.
---
 kernel/uint63_31.ml | 34 ++++++++++++++++++----------------
 1 file changed, 18 insertions(+), 16 deletions(-)

diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index 3d7dd1792a..ddb6ba656e 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -118,25 +118,27 @@ let div21 xh xl y =
 let div21 xh xl y =
   if Int64.compare y xh <= 0 then zero, zero else div21 xh xl y
 
-     (* exact multiplication *)
+(* exact multiplication *)
 let mulc x y =
-  let lx = ref (Int64.logand x maxuint31) in
-  let ly = ref (Int64.logand y maxuint31) in
+  let lx = Int64.logand x maxuint31 in
+  let ly = Int64.logand y maxuint31 in
   let hx = Int64.shift_right x 31 in
   let hy = Int64.shift_right y 31 in
-  let hr = ref (Int64.mul hx hy) in
-  let lr = ref (Int64.logor (Int64.mul !lx !ly) (Int64.shift_left !hr 62)) in
-  hr := (Int64.shift_right_logical !hr 1);
-  lx := Int64.mul !lx hy;
-  ly := Int64.mul hx !ly;
-  hr := Int64.logor !hr (Int64.add (Int64.shift_right !lx 32) (Int64.shift_right !ly 32));
-  lr := Int64.add !lr (Int64.shift_left !lx 31);
-  hr := Int64.add !hr (Int64.shift_right_logical !lr 63);
-  lr := Int64.add (Int64.shift_left !ly 31) (mask63 !lr);
-  hr := Int64.add !hr (Int64.shift_right_logical !lr 63);
-  if Int64.logand !lr Int64.min_int <> 0L
-  then Int64.(sub !hr one, mask63 !lr)
-  else (!hr, !lr)
+  (* compute the median products *)
+  let s = Int64.add (Int64.mul lx hy) (Int64.mul hx ly) in
+  (* s fits on 64 bits, split it into a 33-bit high part and a 31-bit low part *)
+  let lr = Int64.shift_left (Int64.logand s maxuint31) 31 in
+  let hr = Int64.shift_right_logical s 31 in
+  (* add the outer products *)
+  let lr = Int64.add (Int64.mul lx ly) lr in
+  let hr = Int64.add (Int64.mul hx hy) hr in
+  (* now x * y = hr * 2^62 + lr and lr < 2^63 *)
+  let lr = Int64.add lr (Int64.shift_left (Int64.logand hr 1L) 62) in
+  let hr = Int64.shift_right_logical hr 1 in
+  (* now x * y = hr * 2^63 + lr, but lr might be too large *)
+  if Int64.logand lr Int64.min_int <> 0L
+  then Int64.add hr 1L, mask63 lr
+  else hr, lr
 
 let equal (x : t) y = x = y
 
-- 
cgit v1.2.3


From 00c0b652311b8c6b26c7e21b17db4ab12a35f286 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 27 Dec 2019 09:04:39 +0400
Subject: Add critical-bugs entry, tests-suite file, and code comment.

---
 dev/doc/critical-bugs              | 12 ++++++++++++
 kernel/uint63_31.ml                |  1 +
 test-suite/bugs/closed/bug_11321.v | 10 ++++++++++
 3 files changed, 23 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_11321.v

diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 67becb251a..2d187f7bae 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -255,6 +255,18 @@ Conversion machines
   GH issue number: #9925
   risk:
 
+  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
+  summary: broken long multiplication primitive integer emulation layer on 32 bits
+  introduced: e43b176
+  impacted released versions: 8.10.0, 8.10.1, 8.10.2
+  impacted development branches: 8.11
+  impacted coqchk versions: none (no virtual machine in coqchk)
+  fixed in: 4e176a7
+  found by: Soegtrop, Melquiond
+  exploit: test-suite/bugs/closed/bug_11321.v
+  GH issue number: #11321
+  risk: critical, as any BigN computation on 32-bit architectures is wrong
+
   component: "native" conversion machine (translation to OCaml which compiles to native code)
   summary: translation of identifier from Coq to OCaml was not bijective, leading to identify True and False
   introduced: V8.5
diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index ddb6ba656e..445166f6af 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -132,6 +132,7 @@ let mulc x y =
   (* add the outer products *)
   let lr = Int64.add (Int64.mul lx ly) lr in
   let hr = Int64.add (Int64.mul hx hy) hr in
+  (* hr fits on 64 bits, since the final result fits on 126 bits *)
   (* now x * y = hr * 2^62 + lr and lr < 2^63 *)
   let lr = Int64.add lr (Int64.shift_left (Int64.logand hr 1L) 62) in
   let hr = Int64.shift_right_logical hr 1 in
diff --git a/test-suite/bugs/closed/bug_11321.v b/test-suite/bugs/closed/bug_11321.v
new file mode 100644
index 0000000000..ce95280fb1
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11321.v
@@ -0,0 +1,10 @@
+Require Import Cyclic63.
+
+Goal False.
+Proof.
+assert (4294967296 *c 2147483648 = WW 2 0)%int63 as H.
+  vm_cast_no_check (@eq_refl (zn2z int) (WW 2 0)%int63).
+generalize (f_equal (zn2z_to_Z wB to_Z) H).
+now rewrite mulc_WW_spec.
+Fail Qed.
+Abort.
-- 
cgit v1.2.3