Merge PR #12484: Fix #12483 Incorrect specification of PrimFloat.leb

Ack-by: Zimmi48
Reviewed-by: erikmd
Reviewed-by: silene

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.

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).

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.

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.