diff --git a/src/Init/Data/SInt/Basic.lean b/src/Init/Data/SInt/Basic.lean
index 6b4127dc8944..84189c7c77a4 100644
--- a/src/Init/Data/SInt/Basic.lean
+++ b/src/Init/Data/SInt/Basic.lean
@@ -52,6 +52,18 @@ structure Int64 where
   -/
   toUInt64 : UInt64
 
+/--
+A `ISize` is a signed integer with the size of a word for the platform's architecture.
+
+For example, if running on a 32-bit machine, ISize is equivalent to `Int32`.
+Or on a 64-bit machine, `Int64`.
+-/
+structure ISize where
+  /--
+  Obtain the `USize` that is 2's complement equivalent to the `ISize`.
+  -/
+  toUSize : USize
+
 /-- The size of type `Int8`, that is, `2^8 = 256`. -/
 abbrev Int8.size : Nat := 256
 
@@ -463,3 +475,114 @@ instance (a b : Int64) : Decidable (a < b) := Int64.decLt a b
 instance (a b : Int64) : Decidable (a ≤ b) := Int64.decLe a b
 instance : Max Int64 := maxOfLe
 instance : Min Int64 := minOfLe
+
+/-- The size of type `ISize`, that is, `2^System.Platform.numBits`. -/
+abbrev ISize.size : Nat := 2^System.Platform.numBits
+
+/--
+Obtain the `BitVec` that contains the 2's complement representation of the `ISize`.
+-/
+@[inline] def ISize.toBitVec (x : ISize) : BitVec System.Platform.numBits := x.toUSize.toBitVec
+
+@[extern "lean_isize_of_int"]
+def ISize.ofInt (i : @& Int) : ISize := ⟨⟨BitVec.ofInt System.Platform.numBits i⟩⟩
+@[extern "lean_isize_of_nat"]
+def ISize.ofNat (n : @& Nat) : ISize := ⟨⟨BitVec.ofNat System.Platform.numBits n⟩⟩
+abbrev Int.toISize := ISize.ofInt
+abbrev Nat.toISize := ISize.ofNat
+@[extern "lean_isize_to_int"]
+def ISize.toInt (i : ISize) : Int := i.toBitVec.toInt
+/--
+This function has the same behavior as `Int.toNat` for negative numbers.
+If you want to obtain the 2's complement representation use `toBitVec`.
+-/
+@[inline] def ISize.toNat (i : ISize) : Nat := i.toInt.toNat
+@[extern "lean_isize_to_int32"]
+def ISize.toInt32 (a : ISize) : Int32 := ⟨⟨a.toBitVec.signExtend 32⟩⟩
+/--
+Upcast `ISize` to `Int64`. This function is losless as `ISize` is either `Int32` or `Int64`.
+-/
+@[extern "lean_isize_to_int64"]
+def ISize.toInt64 (a : ISize) : Int64 := ⟨⟨a.toBitVec.signExtend 64⟩⟩
+/--
+Upcast `Int32` to `ISize`. This function is losless as `ISize` is either `Int32` or `Int64`.
+-/
+@[extern "lean_int32_to_isize"]
+def Int32.toISize (a : Int32) : ISize := ⟨⟨a.toBitVec.signExtend System.Platform.numBits⟩⟩
+@[extern "lean_int64_to_isize"]
+def Int64.toISize (a : Int64) : ISize := ⟨⟨a.toBitVec.signExtend System.Platform.numBits⟩⟩
+@[extern "lean_isize_neg"]
+def ISize.neg (i : ISize) : ISize := ⟨⟨-i.toBitVec⟩⟩
+
+instance : ToString ISize where
+  toString i := toString i.toInt
+
+instance : OfNat ISize n := ⟨ISize.ofNat n⟩
+instance : Neg ISize where
+  neg := ISize.neg
+
+@[extern "lean_isize_add"]
+def ISize.add (a b : ISize) : ISize := ⟨⟨a.toBitVec + b.toBitVec⟩⟩
+@[extern "lean_isize_sub"]
+def ISize.sub (a b : ISize) : ISize := ⟨⟨a.toBitVec - b.toBitVec⟩⟩
+@[extern "lean_isize_mul"]
+def ISize.mul (a b : ISize) : ISize := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
+@[extern "lean_isize_div"]
+def ISize.div (a b : ISize) : ISize := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
+@[extern "lean_isize_mod"]
+def ISize.mod (a b : ISize) : ISize := ⟨⟨BitVec.srem a.toBitVec b.toBitVec⟩⟩
+@[extern "lean_isize_land"]
+def ISize.land (a b : ISize) : ISize := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
+@[extern "lean_isize_lor"]
+def ISize.lor (a b : ISize) : ISize := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
+@[extern "lean_isize_xor"]
+def ISize.xor (a b : ISize) : ISize := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
+@[extern "lean_isize_shift_left"]
+def ISize.shiftLeft (a b : ISize) : ISize := ⟨⟨a.toBitVec <<< (b.toBitVec.smod System.Platform.numBits)⟩⟩
+@[extern "lean_isize_shift_right"]
+def ISize.shiftRight (a b : ISize) : ISize := ⟨⟨BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod System.Platform.numBits)⟩⟩
+@[extern "lean_isize_complement"]
+def ISize.complement (a : ISize) : ISize := ⟨⟨~~~a.toBitVec⟩⟩
+
+@[extern "lean_isize_dec_eq"]
+def ISize.decEq (a b : ISize) : Decidable (a = b) :=
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ =>
+    if h : n = m then
+      isTrue <| h ▸ rfl
+    else
+      isFalse (fun h' => ISize.noConfusion h' (fun h' => absurd h' h))
+
+def ISize.lt (a b : ISize) : Prop := a.toBitVec.slt b.toBitVec
+def ISize.le (a b : ISize) : Prop := a.toBitVec.sle b.toBitVec
+
+instance : Inhabited ISize where
+  default := 0
+
+instance : Add ISize         := ⟨ISize.add⟩
+instance : Sub ISize         := ⟨ISize.sub⟩
+instance : Mul ISize         := ⟨ISize.mul⟩
+instance : Mod ISize         := ⟨ISize.mod⟩
+instance : Div ISize         := ⟨ISize.div⟩
+instance : LT ISize          := ⟨ISize.lt⟩
+instance : LE ISize          := ⟨ISize.le⟩
+instance : Complement ISize  := ⟨ISize.complement⟩
+instance : AndOp ISize       := ⟨ISize.land⟩
+instance : OrOp ISize        := ⟨ISize.lor⟩
+instance : Xor ISize         := ⟨ISize.xor⟩
+instance : ShiftLeft ISize   := ⟨ISize.shiftLeft⟩
+instance : ShiftRight ISize  := ⟨ISize.shiftRight⟩
+instance : DecidableEq ISize := ISize.decEq
+
+@[extern "lean_isize_dec_lt"]
+def ISize.decLt (a b : ISize) : Decidable (a < b) :=
+  inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
+
+@[extern "lean_isize_dec_le"]
+def ISize.decLe (a b : ISize) : Decidable (a ≤ b) :=
+  inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
+
+instance (a b : ISize) : Decidable (a < b) := ISize.decLt a b
+instance (a b : ISize) : Decidable (a ≤ b) := ISize.decLe a b
+instance : Max ISize := maxOfLe
+instance : Min ISize := minOfLe
diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
index 4f96f57a5c7a..652ba744ac1c 100644
--- a/src/include/lean/lean.h
+++ b/src/include/lean/lean.h
@@ -2229,6 +2229,7 @@ static inline uint8_t lean_int32_dec_le(uint32_t a1, uint32_t a2) {
 static inline uint8_t lean_int32_to_int8(uint32_t a) { return (uint8_t)(int8_t)(int32_t)a; }
 static inline uint16_t lean_int32_to_int16(uint32_t a) { return (uint16_t)(int16_t)(int32_t)a; }
 static inline uint64_t lean_int32_to_int64(uint32_t a) { return (uint64_t)(int64_t)(int32_t)a; }
+static inline size_t lean_int32_to_isize(uint32_t a) { return (size_t)(ptrdiff_t)(int32_t)a; }
 
 /* Int64 */
 LEAN_EXPORT int64_t lean_int64_of_big_int(b_lean_obj_arg a);
@@ -2368,6 +2369,147 @@ static inline uint8_t lean_int64_dec_le(uint64_t a1, uint64_t a2) {
 static inline uint8_t lean_int64_to_int8(uint64_t a) { return (uint8_t)(int8_t)(int64_t)a; }
 static inline uint16_t lean_int64_to_int16(uint64_t a) { return (uint16_t)(int16_t)(int64_t)a; }
 static inline uint32_t lean_int64_to_int32(uint64_t a) { return (uint32_t)(int32_t)(int64_t)a; }
+static inline size_t lean_int64_to_isize(uint64_t a) { return (size_t)(ptrdiff_t)(int64_t)a; }
+
+/* ISize */
+LEAN_EXPORT ptrdiff_t lean_isize_of_big_int(b_lean_obj_arg a);
+static inline size_t lean_isize_of_int(b_lean_obj_arg a) {
+    ptrdiff_t res;
+
+    if (lean_is_scalar(a)) {
+        res = (ptrdiff_t)lean_scalar_to_int64(a);
+    } else {
+        res = lean_isize_of_big_int(a);
+    }
+
+    return (size_t)res;
+}
+
+static inline size_t lean_isize_of_nat(b_lean_obj_arg a) {
+    ptrdiff_t res;
+
+    if (lean_is_scalar(a)) {
+        res = (ptrdiff_t)lean_unbox(a);
+    } else {
+        res = lean_isize_of_big_int(a);
+    }
+
+    return (size_t)res;
+}
+
+static inline lean_obj_res lean_isize_to_int(size_t a) {
+    ptrdiff_t arg = (ptrdiff_t)a;
+    return lean_int64_to_int((int64_t)arg);
+}
+
+static inline size_t lean_isize_neg(size_t a) {
+    ptrdiff_t arg = (ptrdiff_t)a;
+
+    return (size_t)(-arg);
+}
+
+static inline size_t lean_isize_add(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t rhs = (ptrdiff_t)a2;
+
+    return (size_t)(lhs + rhs);
+}
+
+static inline size_t lean_isize_sub(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t rhs = (ptrdiff_t)a2;
+
+    return (size_t)(lhs - rhs);
+}
+
+static inline size_t lean_isize_mul(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t rhs = (ptrdiff_t)a2;
+
+    return (size_t)(lhs * rhs);
+}
+
+static inline size_t lean_isize_div(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t rhs = (ptrdiff_t)a2;
+
+    return (size_t)(rhs == 0 ? 0 : lhs / rhs);
+}
+
+static inline size_t lean_isize_mod(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t rhs = (ptrdiff_t)a2;
+
+    return (size_t)(rhs == 0 ? lhs : lhs % rhs);
+}
+
+static inline size_t lean_isize_land(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t rhs = (ptrdiff_t)a2;
+
+    return (size_t)(lhs & rhs);
+}
+
+static inline size_t lean_isize_lor(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t rhs = (ptrdiff_t)a2;
+
+    return (size_t)(lhs | rhs);
+}
+
+static inline size_t lean_isize_xor(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t rhs = (ptrdiff_t)a2;
+
+    return (size_t)(lhs ^ rhs);
+}
+
+static inline size_t lean_isize_shift_right(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t size = sizeof(ptrdiff_t) * 8;
+    ptrdiff_t rhs = (((ptrdiff_t)a2 % size) + size) % size; // this is smod
+
+    return (size_t)(lhs >> rhs);
+}
+
+static inline size_t lean_isize_shift_left(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t size = sizeof(ptrdiff_t) * 8;
+    ptrdiff_t rhs = (((ptrdiff_t)a2 % size) + size) % size; // this is smod
+
+    return (size_t)(lhs << rhs);
+}
+
+static inline size_t lean_isize_complement(size_t a) {
+    ptrdiff_t arg = (ptrdiff_t)a;
+
+    return (size_t)(~arg);
+}
+
+static inline uint8_t lean_isize_dec_eq(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t rhs = (ptrdiff_t)a2;
+
+    return lhs == rhs;
+}
+
+static inline uint8_t lean_isize_dec_lt(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t rhs = (ptrdiff_t)a2;
+
+    return lhs < rhs;
+}
+
+static inline uint8_t lean_isize_dec_le(size_t a1, size_t a2) {
+    ptrdiff_t lhs = (ptrdiff_t)a1;
+    ptrdiff_t rhs = (ptrdiff_t)a2;
+
+    return lhs <= rhs;
+}
+
+/* ISize -> other */
+static inline uint32_t lean_isize_to_int32(size_t a) { return (uint32_t)(int32_t)(ptrdiff_t)a; }
+static inline uint64_t lean_isize_to_int64(size_t a) { return (uint64_t)(int64_t)(ptrdiff_t)a; }
 
 /* Float */
 
diff --git a/src/runtime/int.h b/src/runtime/int.h
index 1163570244eb..0f130be69380 100644
--- a/src/runtime/int.h
+++ b/src/runtime/int.h
@@ -29,5 +29,9 @@ static_assert(sizeof(int64) == 8,  "unexpected int64 size");  // NOLINT
 static_assert(sizeof(uint64) == 8, "unexpected uint64 size"); // NOLINT
                                                               //
 typedef size_t usize;
+typedef ptrdiff_t isize;
+static_assert(sizeof(usize) == sizeof(isize), "unexpected size difference usize/isize");   // NOLINT
+static_assert(sizeof(usize) == 4 || sizeof(usize) == 8, "usize is neither 32 nor 64 bit"); // NOLINT
+                                                                                           //
 
 }
diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index 374455593f4d..b23a29177d72 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -1578,6 +1578,15 @@ extern "C" LEAN_EXPORT int64 lean_int64_of_big_int(b_obj_arg a) {
     return mpz_value(a).smod64();
 }
 
+extern "C" LEAN_EXPORT isize lean_isize_of_big_int(b_obj_arg a) {
+    if (sizeof(ptrdiff_t) == 8) {
+        return static_cast<isize>(mpz_value(a).smod64());
+    } else {
+        // We assert in int.h that the size of ptrdiff_t is 8 or 4.
+        return static_cast<isize>(mpz_value(a).smod32());
+    }
+}
+
 // =======================================
 // Float
 
diff --git a/tests/lean/sint_basic.lean b/tests/lean/sint_basic.lean
index 998561fc45c7..3fb2bebe2c56 100644
--- a/tests/lean/sint_basic.lean
+++ b/tests/lean/sint_basic.lean
@@ -347,3 +347,85 @@ def myId32 (x : Int32) : Int32 := x
 -- runtime representation
 set_option trace.compiler.ir.result true in
 def myId64 (x : Int64) : Int64 := x
+
+
+#check ISize
+#eval ISize.ofInt 20
+#eval ISize.ofInt (-20)
+#eval ISize.ofInt (-20) = -20
+#eval 2^63 - 10 = 9223372036854775798 ∧ ISize.ofInt (-(2^63) - 10) = 9223372036854775798
+#eval (10 : ISize) ≠ (11 : ISize)
+#eval (-10 : ISize) ≠ (10 : ISize)
+#eval ISize.ofNat 10 = 10
+#eval 2^63 + 10 = 9223372036854775818 ∧ ISize.ofNat 9223372036854775818 = 9223372036854775818
+#eval ISize.ofNat 120 = 120
+#eval ISize.ofInt (-20) = -20
+#eval (ISize.ofInt (-2)).toInt = -2
+#eval (ISize.ofInt (-2)).toNat = 0
+#eval (ISize.ofInt (10)).toNat = 10
+#eval (ISize.ofInt (10)).toInt = 10
+#eval ISize.ofNat (2^64) == 0
+#eval ISize.ofInt (-2^64) == 0
+#eval ISize.neg 10 = -10
+#eval (20 : ISize) + 20 = 40
+#eval (2^63 - 1) = 9223372036854775807 ∧ -2^63 = -9223372036854775808 ∧ (9223372036854775807 : ISize) + 1 = -9223372036854775808
+#eval (-10 : ISize) + 10 = 0
+#eval (1 : ISize) - 2 = -1
+#eval (2^63 - 1) = 9223372036854775807 ∧ -2^63 = -9223372036854775808 ∧ (-9223372036854775808 : ISize) - 1 = 9223372036854775807
+#eval (1 : ISize) * 120 = 120
+#eval (2 : ISize) * 10 = 20
+#eval 18446744073709551616 = 2^64 ∧ (2 : ISize) * 18446744073709551616 = 0
+#eval (-1 : ISize) * (-1) = 1
+#eval (1 : ISize) * (-1) = -1
+#eval (2 : ISize) * (-10) = -20
+#eval (-5 : ISize) * (-5) = 25
+#eval (10 : ISize) / 2 = 5
+#eval (-10 : ISize) / 2 = -5
+#eval (-10 : ISize) / -2 = 5
+#eval (10 : ISize) / -2 = -5
+#eval (10 : ISize) / 0 = 0
+#eval (10 : ISize) % 1 = 0
+#eval (10 : ISize) % 0 = 10
+#eval (-10 : ISize) % 0 = -10
+#eval (10 : ISize) % 3 = 1
+#eval (-10 : ISize) % 3 = -1
+#eval (-10 : ISize) % -3 = -1
+#eval (10 : ISize) % -3 = 1
+#eval (10 : ISize) &&& 10 = 10
+#eval (-1 : ISize) &&& 1 = 1
+#eval (-1 : ISize) ^^^ 123 = ~~~123
+#eval (10 : ISize) ||| 10 = 10
+#eval (10 : ISize) ||| 0 = 10
+#eval (10 : ISize) ||| -1 = -1
+#eval (16 : ISize) >>> 1 = 8
+#eval (16 : ISize) >>> 64 = 16
+#eval (16 : ISize) >>> (64 + 1) = 8
+#eval (-16 : ISize) >>> 1 = -8
+#eval (16 : ISize) <<< 1 = 32
+#eval (16 : ISize) <<< (64 + 1) = 32
+#eval (-16 : ISize) <<< 1 = -32
+#eval (-16 : ISize) <<< (64 + 1) = -32
+#eval (-16 : ISize) >>> 1 <<< 1 = -16
+#eval (0 : ISize) < 1
+#eval (0 : ISize) < 120
+#eval (120 : ISize) > 0
+#eval -1 < (0 : ISize)
+#eval -120 < (0 : ISize)
+#eval ¬((0 : ISize) < (0 : ISize))
+#eval (0 : ISize) ≤ 1
+#eval (0 : ISize) ≤ 120
+#eval -1 ≤ (0 : ISize)
+#eval -120 ≤ (0 : ISize)
+#eval (0 : ISize) ≤ (0 : ISize)
+#eval (-10 : ISize) ≥ (-10 : ISize)
+#eval max (10 : ISize) 20 = 20
+#eval max (10 : ISize) (-1) = 10
+#eval min (10 : ISize) 20 = 10
+#eval min (10 : ISize) (-1) = -1
+
+
+#eval test System.Platform.numBits (⟨⟨·⟩⟩) ISize.ofInt ISize.ofNat
+
+-- runtime representation
+set_option trace.compiler.ir.result true in
+def myIdSize (x : ISize) : ISize := x
diff --git a/tests/lean/sint_basic.lean.expected.out b/tests/lean/sint_basic.lean.expected.out
index 79702c9fd17f..40f67f40be26 100644
--- a/tests/lean/sint_basic.lean.expected.out
+++ b/tests/lean/sint_basic.lean.expected.out
@@ -334,3 +334,87 @@ def myId64._boxed (x_1 : obj) : obj :=
   let x_3 : u64 := myId64 x_2;
   let x_4 : obj := box x_3;
   ret x_4
+ISize : Type
+20
+-20
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+
+[result]
+def myIdSize (x_1 : usize) : usize :=
+  ret x_1
+def myIdSize._boxed (x_1 : obj) : obj :=
+  let x_2 : usize := unbox x_1;
+  dec x_1;
+  let x_3 : usize := myIdSize x_2;
+  let x_4 : obj := box x_3;
+  ret x_4