fix: constant folding for Nat.ble and Nat.blt (#6087)

This PR fixes a bug in the constant folding for the `Nat.ble` and
`Nat.blt` function in the old code generator, leading to a
miscompilation.

Closes #6086

src/Lean/Compiler/ConstFolding.lean

@@ -133,8 +133,8 @@ def foldNatBinBoolPred (fn : Nat → Nat → Bool) (a₁ a₂ : Expr) : Option E
     return mkConst ``Bool.false
 
 def foldNatBeq := fun _ : Bool => foldNatBinBoolPred (fun a b => a == b)
-def foldNatBle := fun _ : Bool => foldNatBinBoolPred (fun a b => a < b)
-def foldNatBlt := fun _ : Bool => foldNatBinBoolPred (fun a b => a ≤ b)
+def foldNatBlt := fun _ : Bool => foldNatBinBoolPred (fun a b => a < b)
+def foldNatBle := fun _ : Bool => foldNatBinBoolPred (fun a b => a ≤ b)
 
 def natFoldFns : List (Name × BinFoldFn) :=
   [(``Nat.add, foldNatAdd),

src/include/lean/lean.h

@@ -1259,6 +1259,8 @@ static inline lean_obj_res lean_nat_mod(b_lean_obj_arg a1, b_lean_obj_arg a2) {
 
 static inline bool lean_nat_eq(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
+        // This comparison is UB according to the standard but allowed as per the
+        // GCC documentation and the address sanitizer does not complain about it.
         return a1 == a2;
     } else {
         return lean_nat_big_eq(a1, a2);
@@ -1275,6 +1277,8 @@ static inline bool lean_nat_ne(b_lean_obj_arg a1, b_lean_obj_arg a2) {
 
 static inline bool lean_nat_le(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
+        // This comparison is UB according to the standard but allowed as per the
+        // GCC documentation and the address sanitizer does not complain about it.
         return a1 <= a2;
     } else {
         return lean_nat_big_le(a1, a2);
@@ -1287,6 +1291,8 @@ static inline uint8_t lean_nat_dec_le(b_lean_obj_arg a1, b_lean_obj_arg a2) {
 
 static inline bool lean_nat_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
+        // This comparison is UB according to the standard but allowed as per the
+        // GCC documentation and the address sanitizer does not complain about it.
         return a1 < a2;
     } else {
         return lean_nat_big_lt(a1, a2);

tests/lean/run/6086.lean

@@ -0,0 +1,3 @@
+/-- info: [true, true, false, true, false, false, true, true, false, true, false, false] -/
+#guard_msgs in
+#eval [Nat.ble 36 37, Nat.ble 37 37, Nat.ble 38 37, Nat.blt 36 37, Nat.blt 37 37, Nat.blt 38 37, 36 ≤ 37, 37 ≤ 37, 38 ≤ 37 ,36 < 37, 37 < 37, 38 < 37]