14.4. Fixed-Precision Integer Types🔗

Lean's standard library includes the usual assortment of fixed-width integer types. From the perspective of formalization and proofs, these types are wrappers around bitvectors of the appropriate size; the wrappers ensure that the correct implementations of e.g. arithmetic operations are applied. In compiled code, they are represented efficiently: the compiler has special support for them, as it does for other fundamental types.

14.4.1. Logical Model

Fixed-width integers may be unsigned or signed. Furthermore, they are available in five sizes: 8, 16, 32, and 64 bits, along with the current architecture's word size. In their logical models, the unsigned integers are structures that wrap a BitVec of the appropriate width. Signed integers wrap the corresponding unsigned integers, and use a twos-complement representation.

14.4.1.1. Unsigned

structure

USize : Type

A USize is an unsigned integer with the size of a word for the platform's architecture.

For example, if running on a 32-bit machine, USize is equivalent to UInt32. Or on a 64-bit machine, UInt64.

Constructor

USize.ofBitVec

Create a USize from a BitVec System.Platform.numBits. This function is overridden with a native implementation.

Fields

toBitVec : BitVec System.Platform.numBits

Unpack a USize as a BitVec System.Platform.numBits. This function is overridden with a native implementation.

structure

UInt8 : Type

The type of unsigned 8-bit integers. This type has special support in the compiler to make it actually 8 bits rather than wrapping a Nat.

Constructor

UInt8.ofBitVec

Create a UInt8 from a BitVec 8. This function is overridden with a native implementation.

Fields

toBitVec : BitVec 8

Unpack a UInt8 as a BitVec 8. This function is overridden with a native implementation.

structure

UInt16 : Type

The type of unsigned 16-bit integers. This type has special support in the compiler to make it actually 16 bits rather than wrapping a Nat.

Constructor

UInt16.ofBitVec

Create a UInt16 from a BitVec 16. This function is overridden with a native implementation.

Fields

toBitVec : BitVec 16

Unpack a UInt16 as a BitVec 16. This function is overridden with a native implementation.

structure

UInt32 : Type

The type of unsigned 32-bit integers. This type has special support in the compiler to make it actually 32 bits rather than wrapping a Nat.

Constructor

UInt32.ofBitVec

Create a UInt32 from a BitVec 32. This function is overridden with a native implementation.

Fields

toBitVec : BitVec 32

Unpack a UInt32 as a BitVec 32. This function is overridden with a native implementation.

structure

UInt64 : Type

The type of unsigned 64-bit integers. This type has special support in the compiler to make it actually 64 bits rather than wrapping a Nat.

Constructor

UInt64.ofBitVec

Create a UInt64 from a BitVec 64. This function is overridden with a native implementation.

Fields

toBitVec : BitVec 64

Unpack a UInt64 as a BitVec 64. This function is overridden with a native implementation.

14.4.1.2. Signed

structure

ISize : Type

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.

Constructor

ISize.ofUSize._@._hyg.0

Fields

toUSize : USize

Obtain the USize that is 2's complement equivalent to the ISize.

structure

Int8 : Type

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.

Constructor

Int8.ofUInt8._@._hyg.0

Fields

toUInt8 : UInt8

Obtain the UInt8 that is 2's complement equivalent to the Int8.

structure

Int16 : Type

The type of signed 16-bit integers. This type has special support in the compiler to make it actually 16 bits rather than wrapping a Nat.

Constructor

Int16.ofUInt16._@._hyg.0

Fields

toUInt16 : UInt16

Obtain the UInt16 that is 2's complement equivalent to the Int16.

structure

Int32 : Type

The type of signed 32-bit integers. This type has special support in the compiler to make it actually 32 bits rather than wrapping a Nat.

Constructor

Int32.ofUInt32._@._hyg.0

Fields

toUInt32 : UInt32

Obtain the UInt32 that is 2's complement equivalent to the Int32.

structure

Int64 : Type

The type of signed 64-bit integers. This type has special support in the compiler to make it actually 64 bits rather than wrapping a Nat.

Constructor

Int64.ofUInt64._@._hyg.0

Fields

toUInt64 : UInt64

Obtain the UInt64 that is 2's complement equivalent to the Int64.

14.4.2. Run-Time Representation

In compiled code, fixed-width integer types that fit in one less bit than the platform's pointer size are always represented unboxed, without additional allocations or indirections. This always includes Int8, UInt8, Int16, and UInt16. On 64-bit architectures, Int32 and UInt32 are also unboxed. On 32-bit architectures, Int32 and UInt32 are boxed, which means they may be represented by a pointer to an object on the heap. ISize, USize, Int64 and UInt64 are boxed on all architectures.

Even though some fixed-with integer types require boxing in general, the compiler is able to represent them without boxing in code paths that use only a specific fixed-width type rather than being polymorphic, potentially after a specialization pass. This applies in most practical situations where these types are used: their values are represented using the corresponding unsigned fixed-width C type when a constructor parameter, function parameter, function return value, or intermediate result is known to be a fixed-width integer type. The Lean run-time system includes primitives for storing fixed-width integers in constructors of inductive types, and the primitive operations are defined on the corresponding C types, so boxing tends to happen at the “edges” of integer calculations rather than for each intermediate result. In contexts where other types might occur, such as the contents of polymorphic containers like Array, these types are boxed, even if an array is statically known to contain only a single fixed-width integer type.The monomorphic array type ByteArray avoids boxing for arrays of UInt8. Lean does not specialize the representation of inductive types or arrays. Inspecting a function's type in Lean is not sufficient to determine how fixed-width integer values will be represented, because boxed values are not eagerly unboxed—a function that projects an Int64 from an array returns a boxed integer value.

14.4.3. Syntax

All the fixed-width integer types have OfNat instances, which allow numerals to be used as literals, both in expression and in pattern contexts. The signed types additionally have Neg instances, allowing negation to be applied.

Fixed-Width Literals

Lean allows both decimal and hexadecimal literals to be used for types with OfNat instances. In this example, literal notation is used to define masks.

structure Permissions where
  readable : Bool
  writable : Bool
  executable : Bool

def Permissions.encode (p : Permissions) : UInt8 :=
  let r := if p.readable then 0x01 else 0
  let w := if p.writable then 0x02 else 0
  let x := if p.executable then 0x04 else 0
  r ||| w ||| x

def Permissions.decode (i : UInt8) : Permissions :=
  ⟨i &&& 0x01 ≠ 0, i &&& 0x02 ≠ 0, i &&& 0x04 ≠ 0⟩

Literals that overflow their types' precision are interpreted modulus the precision. Signed types, are interpreted according to the underlying twos-complement representation.

Overflowing Fixed-Width Literals

The following statements are all true:

example : (255 : UInt8) = 255 := by⊢ 255 = 255 rflAll goals completed! 🐙
example : (256 : UInt8) = 0   := by⊢ 256 = 0 rflAll goals completed! 🐙
example : (257 : UInt8) = 1   := by⊢ 257 = 1 rflAll goals completed! 🐙

example : (0x7f : Int8) = 127  := by⊢ 127 = 127 rflAll goals completed! 🐙
example : (0x8f : Int8) = -113 := by⊢ 143 = -113 rflAll goals completed! 🐙
example : (0xff : Int8) = -1   := by⊢ 255 = -1 rflAll goals completed! 🐙

14.4.4. API Reference

14.4.4.1. Sizes

Each fixed-width integer has a size, which is the number of distinct values that can be represented by the type. This is not equivalent to C's sizeof operator, which instead determines how many bytes the type occupies.

def

USize.size : Nat

The size of type USize, that is, 2^System.Platform.numBits.

def

ISize.size : Nat

The size of type ISize, that is, 2^System.Platform.numBits.

def

UInt8.size : Nat

The size of type UInt8, that is, 2^8 = 256.

def

Int8.size : Nat

The size of type Int8, that is, 2^8 = 256.

def

UInt16.size : Nat

The size of type UInt16, that is, 2^16 = 65536.

def

Int16.size : Nat

The size of type Int16, that is, 2^16 = 65536.

def

UInt32.size : Nat

The size of type UInt32, that is, 2^32 = 4294967296.

def

Int32.size : Nat

The size of type Int32, that is, 2^32 = 4294967296.

def

UInt64.size : Nat

The size of type UInt64, that is, 2^64 = 18446744073709551616.

def

Int64.size : Nat

The size of type Int64, that is, 2^64 = 18446744073709551616.

14.4.4.2. Ranges

def

ISize.minValue : ISize

The minimum value an ISize may attain, that is, -2^(System.Platform.numBits - 1).

def

ISize.maxValue : ISize

The maximum value an ISize may attain, that is, 2^(System.Platform.numBits - 1) - 1.

def

Int8.minValue : Int8

The minimum value an Int8 may attain, that is, -2^7 = -128.

def

Int8.maxValue : Int8

The maximum value an Int8 may attain, that is, 2^7 - 1 = 127.

def

Int16.minValue : Int16

The minimum value an Int16 may attain, that is, -2^15 = -32768.

def

Int16.maxValue : Int16

The maximum value an Int16 may attain, that is, 2^15 - 1 = 32767.

def

Int32.minValue : Int32

The minimum value an Int32 may attain, that is, -2^31 = -2147483648.

def

Int32.maxValue : Int32

The maximum value an Int32 may attain, that is, 2^31 - 1 = 2147483647.

def

Int64.minValue : Int64

The minimum value an Int64 may attain, that is, -2^63 = -9223372036854775808.

def

Int64.maxValue : Int64

The maximum value an Int64 may attain, that is, 2^63 - 1 = 9223372036854775807.

14.4.4.3. Conversions

14.4.4.3.1. To and From `Int`

def

ISize.toInt (i : ISize) : Int

def

Int8.toInt (i : Int8) : Int

def

Int16.toInt (i : Int16) : Int

def

Int32.toInt (i : Int32) : Int

def

Int64.toInt (i : Int64) : Int

def

ISize.ofInt (i : Int) : ISize

def

Int8.ofInt (i : Int) : Int8

def

Int16.ofInt (i : Int) : Int16

def

Int32.ofInt (i : Int) : Int32

def

Int64.ofInt (i : Int) : Int64

def

ISize.ofIntTruncate (i : Int) : ISize

Constructs an ISize from an Int, clamping if the value is too small or too large.

def

Int8.ofIntTruncate (i : Int) : Int8

Constructs an Int8 from an Int, clamping if the value is too small or too large.

def

Int16.ofIntTruncate (i : Int) : Int16

Constructs an Int16 from an Int, clamping if the value is too small or too large.

def

Int32.ofIntTruncate (i : Int) : Int32

Constructs an Int32 from an Int, clamping if the value is too small or too large.

def

Int64.ofIntTruncate (i : Int) : Int64

Constructs an Int64 from an Int, clamping if the value is too small or too large.

def

ISize.ofIntLE (i : Int)
  (_hl : ISize.minValue.toInt ≤ i)
  (_hr : i ≤ ISize.maxValue.toInt) : ISize

Constructs an ISize from an Int which is known to be in bounds.

def

Int8.ofIntLE (i : Int)
  (_hl : Int8.minValue.toInt ≤ i)
  (_hr : i ≤ Int8.maxValue.toInt) : Int8

Constructs an Int8 from an Int which is known to be in bounds.

def

Int16.ofIntLE (i : Int)
  (_hl : Int16.minValue.toInt ≤ i)
  (_hr : i ≤ Int16.maxValue.toInt) : Int16

Constructs an Int16 from an Int which is known to be in bounds.

def

Int32.ofIntLE (i : Int)
  (_hl : Int32.minValue.toInt ≤ i)
  (_hr : i ≤ Int32.maxValue.toInt) : Int32

Constructs an Int32 from an Int which is known to be in bounds.

def

Int64.ofIntLE (i : Int)
  (_hl : Int64.minValue.toInt ≤ i)
  (_hr : i ≤ Int64.maxValue.toInt) : Int64

Constructs an Int64 from an Int which is known to be in bounds.

14.4.4.3.2. To and From `Nat`

def

USize.ofNat (n : Nat) : USize

def

ISize.ofNat (n : Nat) : ISize

def

UInt8.ofNat (n : Nat) : UInt8

def

Int8.ofNat (n : Nat) : Int8

def

UInt16.ofNat (n : Nat) : UInt16

def

Int16.ofNat (n : Nat) : Int16

def

UInt32.ofNat (n : Nat) : UInt32

def

Int32.ofNat (n : Nat) : Int32

def

UInt64.ofNat (n : Nat) : UInt64

def

Int64.ofNat (n : Nat) : Int64

def

USize.ofNat32 (n : Nat) (h : n < 4294967296) :
  USize

Upcast a Nat less than 2^32 to a USize. This is lossless because USize.size is either 2^32 or 2^64. This function is overridden with a native implementation.

def

USize.ofNatLT (n : Nat) (h : n < USize.size) :
  USize

Pack a Nat less than USize.size into a USize. This function is overridden with a native implementation.

def

UInt8.ofNatLT (n : Nat) (h : n < UInt8.size) :
  UInt8

Pack a Nat less than 2^8 into a UInt8. This function is overridden with a native implementation.

def

UInt16.ofNatLT (n : Nat) (h : n < UInt16.size) :
  UInt16

Pack a Nat less than 2^16 into a UInt16. This function is overridden with a native implementation.

def

UInt32.ofNatLT (n : Nat) (h : n < UInt32.size) :
  UInt32

Pack a Nat less than 2^32 into a UInt32. This function is overridden with a native implementation.

def

UInt64.ofNatLT (n : Nat) (h : n < UInt64.size) :
  UInt64

Pack a Nat less than 2^64 into a UInt64. This function is overridden with a native implementation.

def

USize.ofNatTruncate (n : Nat) : USize

Converts the given natural number to USize, but returns USize.size - 1 (i.e., 2^64 - 1 or 2^32 - 1 depending on the platform) for natural numbers >= USize.size.

def

UInt8.ofNatTruncate (n : Nat) : UInt8

Converts the given natural number to UInt8, but returns 2^8 - 1 for natural numbers >= 2^8.

def

UInt16.ofNatTruncate (n : Nat) : UInt16

Converts the given natural number to UInt16, but returns 2^16 - 1 for natural numbers >= 2^16.

def

UInt32.ofNatTruncate (n : Nat) : UInt32

Converts the given natural number to UInt32, but returns 2^32 - 1 for natural numbers >= 2^32.

def

UInt64.ofNatTruncate (n : Nat) : UInt64

Converts the given natural number to UInt64, but returns 2^64 - 1 for natural numbers >= 2^64.

def

USize.toNat (n : USize) : Nat

def

ISize.toNatClampNeg (i : ISize) : Nat