feat: define Int8 (#5790)

src/CMakeLists.txt

@@ -155,6 +155,10 @@ endif ()
 # We want explicit stack probes in huge Lean stack frames for robust stack overflow detection
 string(APPEND LEANC_EXTRA_FLAGS " -fstack-clash-protection")
 
+# This makes signed integer overflow guaranteed to match 2's complement.
+string(APPEND CMAKE_CXX_FLAGS " -fwrapv")
+string(APPEND LEANC_EXTRA_FLAGS " -fwrapv")
+
 if(NOT MULTI_THREAD)
   message(STATUS "Disabled multi-thread support, it will not be safe to run multiple threads in parallel")
   set(AUTO_THREAD_FINALIZATION OFF)

src/Init/Data.lean

@@ -19,6 +19,7 @@ import Init.Data.ByteArray
 import Init.Data.FloatArray
 import Init.Data.Fin
 import Init.Data.UInt
+import Init.Data.SInt
 import Init.Data.Float
 import Init.Data.Option
 import Init.Data.Ord

src/Init/Data/SInt.lean

@@ -0,0 +1,11 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Init.Data.SInt.Basic
+
+/-!
+This module contains the definitions and basic theory about signed fixed width integer types.
+-/

src/Init/Data/SInt/Basic.lean

@@ -0,0 +1,116 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Init.Data.UInt.Basic
+
+/-!
+This module contains the definition of signed fixed width integer types as well as basic arithmetic
+and bitwise operations on top of it.
+-/
+
+
+/--
+The type of signed 8-bit integers. This type has special support in the
+compiler to make it actually 8 bits rather than wrapping a `Nat`.
+-/
+structure Int8 where
+  /--
+  Obtain the `UInt8` that is 2's complement equivalent to the `Int8`.
+  -/
+  toUInt8 : UInt8
+
+/-- The size of type `Int8`, that is, `2^8 = 256`. -/
+abbrev Int8.size : Nat := 256
+
+/--
+Obtain the `BitVec` that contains the 2's complement representation of the `Int8`.
+-/
+@[inline] def Int8.toBitVec (x : Int8) : BitVec 8 := x.toUInt8.toBitVec
+
+@[extern "lean_int8_of_int"]
+def Int8.ofInt (i : @& Int) : Int8 := ⟨⟨BitVec.ofInt 8 i⟩⟩
+@[extern "lean_int8_of_int"]
+def Int8.ofNat (n : @& Nat) : Int8 := ⟨⟨BitVec.ofNat 8 n⟩⟩
+abbrev Int.toInt8 := Int8.ofInt
+abbrev Nat.toInt8 := Int8.ofNat
+@[extern "lean_int8_to_int"]
+def Int8.toInt (i : Int8) : Int := i.toBitVec.toInt
+@[inline] def Int8.toNat (i : Int8) : Nat := i.toInt.toNat
+@[extern "lean_int8_neg"]
+def Int8.neg (i : Int8) : Int8 := ⟨⟨-i.toBitVec⟩⟩
+
+instance : ToString Int8 where
+  toString i := toString i.toInt
+
+instance : OfNat Int8 n := ⟨Int8.ofNat n⟩
+instance : Neg Int8 where
+  neg := Int8.neg
+
+@[extern "lean_int8_add"]
+def Int8.add (a b : Int8) : Int8 := ⟨⟨a.toBitVec + b.toBitVec⟩⟩
+@[extern "lean_int8_sub"]
+def Int8.sub (a b : Int8) : Int8 := ⟨⟨a.toBitVec - b.toBitVec⟩⟩
+@[extern "lean_int8_mul"]
+def Int8.mul (a b : Int8) : Int8 := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
+@[extern "lean_int8_div"]
+def Int8.div (a b : Int8) : Int8 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
+@[extern "lean_int8_mod"]
+def Int8.mod (a b : Int8) : Int8 := ⟨⟨BitVec.smod a.toBitVec b.toBitVec⟩⟩
+@[extern "lean_int8_land"]
+def Int8.land (a b : Int8) : Int8 := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
+@[extern "lean_int8_lor"]
+def Int8.lor (a b : Int8) : Int8 := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
+@[extern "lean_int8_xor"]
+def Int8.xor (a b : Int8) : Int8 := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
+@[extern "lean_int8_shift_left"]
+def Int8.shiftLeft (a b : Int8) : Int8 := ⟨⟨a.toBitVec <<< (mod b 8).toBitVec⟩⟩
+@[extern "lean_int8_shift_right"]
+def Int8.shiftRight (a b : Int8) : Int8 := ⟨⟨BitVec.sshiftRight' a.toBitVec (mod b 8).toBitVec⟩⟩
+@[extern "lean_int8_complement"]
+def Int8.complement (a : Int8) : Int8 := ⟨⟨~~~a.toBitVec⟩⟩
+
+@[extern "lean_int8_dec_eq"]
+def Int8.decEq (a b : Int8) : Decidable (a = b) :=
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ =>
+    if h : n = m then
+      isTrue <| h ▸ rfl
+    else
+      isFalse (fun h' => Int8.noConfusion h' (fun h' => absurd h' h))
+
+def Int8.lt (a b : Int8) : Prop := a.toBitVec.slt b.toBitVec
+def Int8.le (a b : Int8) : Prop := a.toBitVec.sle b.toBitVec
+
+instance : Inhabited Int8 where
+  default := 0
+
+instance : Add Int8         := ⟨Int8.add⟩
+instance : Sub Int8         := ⟨Int8.sub⟩
+instance : Mul Int8         := ⟨Int8.mul⟩
+instance : Mod Int8         := ⟨Int8.mod⟩
+instance : Div Int8         := ⟨Int8.div⟩
+instance : LT Int8          := ⟨Int8.lt⟩
+instance : LE Int8          := ⟨Int8.le⟩
+instance : Complement Int8  := ⟨Int8.complement⟩
+instance : AndOp Int8       := ⟨Int8.land⟩
+instance : OrOp Int8        := ⟨Int8.lor⟩
+instance : Xor Int8         := ⟨Int8.xor⟩
+instance : ShiftLeft Int8   := ⟨Int8.shiftLeft⟩
+instance : ShiftRight Int8  := ⟨Int8.shiftRight⟩
+instance : DecidableEq Int8 := Int8.decEq
+
+@[extern "lean_int8_dec_lt"]
+def Int8.decLt (a b : Int8) : Decidable (a < b) :=
+  inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
+
+@[extern "lean_int8_dec_le"]
+def Int8.decLe (a b : Int8) : Decidable (a ≤ b) :=
+  inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
+
+instance (a b : Int8) : Decidable (a < b) := Int8.decLt a b
+instance (a b : Int8) : Decidable (a ≤ b) := Int8.decLe a b
+instance : Max Int8 := maxOfLe
+instance : Min Int8 := minOfLe

src/include/lean/lean.h

@@ -1847,6 +1847,140 @@ static inline uint8_t lean_usize_dec_le(size_t a1, size_t a2) { return a1 <= a2;
 static inline uint32_t lean_usize_to_uint32(size_t a) { return ((uint32_t)a); }
 static inline uint64_t lean_usize_to_uint64(size_t a) { return ((uint64_t)a); }
 
+/*
+ * Note that we compile all files with -frwapv so in the following section all potential UB that
+ * may arise from signed overflow is forced to match 2's complement behavior.
+ *
+ * We furthermore rely on the implementation defined behavior of gcc/clang to apply reduction mod
+ * 2^N when casting to an integer type of size N:
+ * https://gcc.gnu.org/onlinedocs/gcc/Integers-implementation.html#Integers-implementation
+ * Unfortunately LLVM does not yet document their implementation defined behavior but it is
+ * most likely fine to rely on the fact that GCC and LLVM match on this:
+ * https://github.com/llvm/llvm-project/issues/11644
+ */
+
+/* Int8 */
+LEAN_EXPORT int8_t lean_int8_of_big_int(b_lean_obj_arg a);
+static inline uint8_t lean_int8_of_int(b_lean_obj_arg a) {
+    int8_t res;
+
+    if (lean_is_scalar(a)) {
+        res = (int8_t)lean_scalar_to_int64(a);
+    } else {
+        res = lean_int8_of_big_int(a);
+    }
+
+    return (uint8_t)res;
+}
+
+static inline lean_obj_res lean_int8_to_int(uint8_t a) {
+    int8_t arg = (int8_t)a;
+    return lean_int64_to_int((int64_t)arg);
+}
+
+static inline uint8_t lean_int8_neg(uint8_t a) {
+    int8_t arg = (int8_t)a;
+
+    return (uint8_t)(-arg);
+}
+
+static inline uint8_t lean_int8_add(uint8_t a1, uint8_t a2) {
+    int8_t lhs = (int8_t) a1;
+    int8_t rhs = (int8_t) a2;
+
+    return (uint8_t)(lhs + rhs);
+}
+
+static inline uint8_t lean_int8_sub(uint8_t a1, uint8_t a2) {
+    int8_t lhs = (int8_t) a1;
+    int8_t rhs = (int8_t) a2;
+
+    return (uint8_t)(lhs - rhs);
+}
+
+static inline uint8_t lean_int8_mul(uint8_t a1, uint8_t a2) {
+    int8_t lhs = (int8_t) a1;
+    int8_t rhs = (int8_t) a2;
+
+    return (uint8_t)(lhs * rhs);
+}
+
+static inline uint8_t lean_int8_div(uint8_t a1, uint8_t a2) {
+    int8_t lhs = (int8_t) a1;
+    int8_t rhs = (int8_t) a2;
+
+    return (uint8_t)(rhs == 0 ? 0 : lhs / rhs);
+}
+
+static inline uint8_t lean_int8_mod(uint8_t a1, uint8_t a2) {
+    int8_t lhs = (int8_t) a1;
+    int8_t rhs = (int8_t) a2;
+
+    return (uint8_t)(rhs == 0 ? 0 : lhs % rhs);
+}
+
+static inline uint8_t lean_int8_land(uint8_t a1, uint8_t a2) {
+    int8_t lhs = (int8_t) a1;
+    int8_t rhs = (int8_t) a2;
+
+    return (uint8_t)(lhs & rhs);
+}
+
+static inline uint8_t lean_int8_lor(uint8_t a1, uint8_t a2) {
+    int8_t lhs = (int8_t) a1;
+    int8_t rhs = (int8_t) a2;
+
+    return (uint8_t)(lhs | rhs);
+}
+
+static inline uint8_t lean_int8_xor(uint8_t a1, uint8_t a2) {
+    int8_t lhs = (int8_t) a1;
+    int8_t rhs = (int8_t) a2;
+
+    return (uint8_t)(lhs ^ rhs);
+}
+
+static inline uint8_t lean_int8_shift_right(uint8_t a1, uint8_t a2) {
+    int8_t lhs = (int8_t) a1;
+    int8_t rhs = (int8_t) a2;
+
+    return (uint8_t)(lhs >> (rhs % 8));
+}
+
+static inline uint8_t lean_int8_shift_left(uint8_t a1, uint8_t a2) {
+    int8_t lhs = (int8_t) a1;
+    int8_t rhs = (int8_t) a2;
+
+    return (uint8_t)(lhs << (rhs % 8));
+}
+
+static inline uint8_t lean_int8_complement(uint8_t a) {
+    int8_t arg = (int8_t)a;
+
+    return (uint8_t)(~arg);
+}
+
+static inline uint8_t lean_int8_dec_eq(uint8_t a1, uint8_t a2) {
+    int8_t lhs = (int8_t) a1;
+    int8_t rhs = (int8_t) a2;
+
+    return lhs == rhs;
+}
+
+static inline uint8_t lean_int8_dec_lt(uint8_t a1, uint8_t a2) {
+    int8_t lhs = (int8_t) a1;
+    int8_t rhs = (int8_t) a2;
+
+    return lhs < rhs;
+}
+
+static inline uint8_t lean_int8_dec_le(uint8_t a1, uint8_t a2) {
+    int8_t lhs = (int8_t) a1;
+    int8_t rhs = (int8_t) a2;
+
+    return lhs <= rhs;
+}
+
 /* Float */
 
 LEAN_EXPORT lean_obj_res lean_float_to_string(double a);

src/runtime/hash.h

@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "runtime/debug.h"
-#include "runtime/int64.h"
+#include "runtime/int.h"
 
 namespace lean {
 

src/runtime/int.h

@@ -0,0 +1,33 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <stdint.h>
+#include <cstddef>
+namespace lean {
+
+typedef int8_t  int8;
+typedef uint8_t uint8;
+static_assert(sizeof(int8) == 1,  "unexpected int8 size");  // NOLINT
+static_assert(sizeof(uint8) == 1, "unexpected uint8 size"); // NOLINT
+                                                              //
+typedef int16_t  int16;
+typedef uint16_t uint16;
+static_assert(sizeof(int16) == 2,  "unexpected int16 size");  // NOLINT
+static_assert(sizeof(uint16) == 2, "unexpected uint16 size"); // NOLINT
+                                                              //
+typedef int32_t  int32;
+typedef uint32_t uint32;
+static_assert(sizeof(int32) == 4,  "unexpected int32 size");  // NOLINT
+static_assert(sizeof(uint32) == 4, "unexpected uint32 size"); // NOLINT
+
+typedef int64_t  int64;
+typedef uint64_t uint64;
+static_assert(sizeof(int64) == 8,  "unexpected int64 size");  // NOLINT
+static_assert(sizeof(uint64) == 8, "unexpected uint64 size"); // NOLINT
+                                                              //
+typedef size_t usize;
+
+}