12.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.

12.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.

12.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.mk

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.mk

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.mk

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.mk

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.mk

Fields

toBitVec : BitVec 64

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

12.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.mk

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.mk

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.mk

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.mk

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.mk

Fields

toUInt64 : UInt64

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

12.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 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.

Fixed-width integer types that take at least as many bits as the platform's pointer type are represented the same way as Nat: if they are sufficiently small, then they are represented unboxed; if they are larger, then they are represented by a heap-allocated number value. Int64, UInt64, ISize, and USize are always represented this way, as are Int32 and UInt32 on 32-bit architectures.

12.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! 🐙

12.4.4. API Reference

12.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.

12.4.4.2. Conversions

12.4.4.2.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

12.4.4.2.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

UInt32.ofNat' (n : Nat) (h : n < UInt32.size)
    : UInt32

def

UInt32.ofNatTruncate (n : Nat) : UInt32

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

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.ofNatCore (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.ofNatCore (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.ofNatCore (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.ofNatCore (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.ofNatCore (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.toNat (n : USize) : Nat

def

ISize.toNat (i : ISize) : Nat