fix: toUInt64LE! and toUInt64BE! are swapped (#3660)

fixes #3657

These functions are mostly not used by lean itself, but it does affect
two occurrences of `ByteArray.toUInt64LE! <$> IO.getRandomBytes 8` which
I left as is instead of switching them to use `toUInt64BE!` to preserve
behavior; but they are random bytes anyway seeded by the OS so it's
unlikely any use of them depending on particular values was sound to
begin with.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/Init/Data/ByteArray/Basic.lean

@@ -195,18 +195,6 @@ instance : ToString ByteArray := ⟨fun bs => bs.toList.toString⟩
 
 /-- Interpret a `ByteArray` of size 8 as a little-endian `UInt64`. -/
 def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 :=
-  assert! bs.size == 8
-  (bs.get! 0).toUInt64 <<< 0x38 |||
-  (bs.get! 1).toUInt64 <<< 0x30 |||
-  (bs.get! 2).toUInt64 <<< 0x28 |||
-  (bs.get! 3).toUInt64 <<< 0x20 |||
-  (bs.get! 4).toUInt64 <<< 0x18 |||
-  (bs.get! 5).toUInt64 <<< 0x10 |||
-  (bs.get! 6).toUInt64 <<< 0x8  |||
-  (bs.get! 7).toUInt64
-
-/-- Interpret a `ByteArray` of size 8 as a big-endian `UInt64`. -/
-def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
   assert! bs.size == 8
   (bs.get! 7).toUInt64 <<< 0x38 |||
   (bs.get! 6).toUInt64 <<< 0x30 |||
@@ -216,3 +204,15 @@ def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
   (bs.get! 2).toUInt64 <<< 0x10 |||
   (bs.get! 1).toUInt64 <<< 0x8  |||
   (bs.get! 0).toUInt64
+
+/-- Interpret a `ByteArray` of size 8 as a big-endian `UInt64`. -/
+def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
+  assert! bs.size == 8
+  (bs.get! 0).toUInt64 <<< 0x38 |||
+  (bs.get! 1).toUInt64 <<< 0x30 |||
+  (bs.get! 2).toUInt64 <<< 0x28 |||
+  (bs.get! 3).toUInt64 <<< 0x20 |||
+  (bs.get! 4).toUInt64 <<< 0x18 |||
+  (bs.get! 5).toUInt64 <<< 0x10 |||
+  (bs.get! 6).toUInt64 <<< 0x8  |||
+  (bs.get! 7).toUInt64

tests/lean/bytearray.lean

@@ -19,5 +19,5 @@ pure ()
 #eval "abcd".hash
 #eval [97, 98, 99, 100].toByteArray.hash
 
-#eval [0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77, 0x88].toByteArray.toUInt64LE! == 0x1122334455667788
-#eval [0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77, 0x88].toByteArray.toUInt64BE! == 0x8877665544332211
+#eval [0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77, 0x88].toByteArray.toUInt64LE! == 0x8877665544332211
+#eval [0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77, 0x88].toByteArray.toUInt64BE! == 0x1122334455667788