From 8ecdb858a416b945fd9bc429e9eecf8aa451f0e7 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Mon, 8 Jun 2020 18:17:30 +0200
Subject: Fix 12483

---
 doc/changelog/10-standard-library/12484-fix12483.rst |  6 ++++++
 test-suite/bugs/closed/bug_12483.v                   | 10 ++++++++++
 theories/Floats/SpecFloat.v                          |  2 +-
 3 files changed, 17 insertions(+), 1 deletion(-)
 create mode 100644 doc/changelog/10-standard-library/12484-fix12483.rst
 create mode 100644 test-suite/bugs/closed/bug_12483.v

diff --git a/doc/changelog/10-standard-library/12484-fix12483.rst b/doc/changelog/10-standard-library/12484-fix12483.rst
new file mode 100644
index 0000000000..95e7c150a3
--- /dev/null
+++ b/doc/changelog/10-standard-library/12484-fix12483.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  Fix the specification of :n:`PrimFloat.leb` which made
+  :n:`(x <= y)%float` true for any non NaN :n:`x` and :n:`y`.
+  (`#12484 <https://github.com/coq/coq/pull/12484>`_,
+  fixes `#12483 <https://github.com/coq/coq/issues/12483>`_,
+  by Pierre Roux).
diff --git a/test-suite/bugs/closed/bug_12483.v b/test-suite/bugs/closed/bug_12483.v
new file mode 100644
index 0000000000..0d034a65eb
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12483.v
@@ -0,0 +1,10 @@
+Require Import Floats.
+
+Goal False.
+Proof.
+cut (false = true).
+{ intro H; discriminate H. }
+change false with (1 <= 0)%float.
+rewrite leb_spec.
+Fail reflexivity.
+Abort.
diff --git a/theories/Floats/SpecFloat.v b/theories/Floats/SpecFloat.v
index 349b37c704..aaf7cbb8f7 100644
--- a/theories/Floats/SpecFloat.v
+++ b/theories/Floats/SpecFloat.v
@@ -222,7 +222,7 @@ Section FloatOps.
 
   Definition SFleb f1 f2 :=
     match SFcompare f1 f2 with
-    | Some Le => true
+    | Some (Lt | Eq) => true
     | _ => false
     end.
 
-- 
cgit v1.2.3


From 9c76e6b4c9ae24826668fa9f72faf93e5d4c6acf Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 9 Jun 2020 11:36:41 +0200
Subject: Update dev/doc/critical-bugs

---
 dev/doc/critical-bugs | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 3260040248..066facd5db 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -347,6 +347,16 @@ Conflicts with axioms in library
   GH issue number: none
   risk:
 
+  component: primitive floating-points
+  summary: Incorrect specification of PrimFloat.leb
+  introduced: 8.11
+  impacted released versions: 8.11.0, 8.11.1, 8.11.2
+  fixed by fixing the spec: #12484
+  found by: Pierre Roux
+  exploit: test-suite/bugs/closed/bug_12483.v 
+  GH issue number: #12483
+  risk: proof of false when using the incorrect axiom
+
 There were otherwise several bugs in beta-releases, from memory, bugs with beta versions of primitive projections or template polymorphism or native compilation or guard (e7fc96366, 2a4d714a1).
 
 There were otherwise maybe unexploitable kernel bugs, e.g. 2df88d83 (Require overloading), 0adf0838 ("Univs: uncovered bug in strengthening of opaque polymorphic definitions."), 5122a398 (#3746 about functors), #4346 (casts in VM), a14bef4 (guard condition in 8.1), 6ed40a8 ("Georges' bug" with ill-typed lazy machine), and various other bugs in 8.0 or 8.1 w/o knowing if they are critical.
-- 
cgit v1.2.3