Init.Data.UInt.BasicAux

UInt8.toFin definition

(x : UInt8) : Fin UInt8.size

Full source

/-- Converts a `UInt8` into the corresponding `Fin UInt8.size`. -/
def UInt8.toFin (x : UInt8) : Fin UInt8.size := x.toBitVec.toFin

Conversion from UInt8 to Fin 256

Informal description

The function maps an unsigned 8-bit integer $x$ to the corresponding element of the finite type $\mathrm{Fin}(256)$, representing the integer's value modulo 256.

UInt8.val definition

(x : UInt8) : Fin UInt8.size

Full source

@[deprecated UInt8.toFin (since := "2025-02-12"), inherit_doc UInt8.toFin]
def UInt8.val (x : UInt8) : Fin UInt8.size := x.toFin

Value of an unsigned 8-bit integer as a finite natural number

Informal description

The function maps an unsigned 8-bit integer $x$ to the corresponding element of the finite type $\mathrm{Fin}(256)$, representing the integer's value modulo 256.

UInt8.ofNat definition

(n : @& Nat) : UInt8

Full source

/--
Converts a natural number to an 8-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `UInt8.ofNat 5 = 5`
 * `UInt8.ofNat 255 = 255`
 * `UInt8.ofNat 256 = 0`
 * `UInt8.ofNat 259 = 3`
 * `UInt8.ofNat 32770 = 2`
-/
@[extern "lean_uint8_of_nat"]
def UInt8.ofNat (n : @& Nat) : UInt8 := ⟨BitVec.ofNat 8 n⟩

Conversion from natural number to 8-bit unsigned integer with wrapping

Informal description

The function maps a natural number $n$ to an 8-bit unsigned integer by taking $n \mod 256$. This operation wraps around when $n$ exceeds the maximum value of 255. Examples: - $5 \mapsto 5$ - $255 \mapsto 255$ - $256 \mapsto 0$ - $259 \mapsto 3$ - $32770 \mapsto 2$

UInt8.ofNatTruncate definition

(n : Nat) : UInt8

Full source

/--
Converts a natural number to an 8-bit unsigned integer, returning the largest representable value if
the number is too large.

Returns `2^8 - 1` for natural numbers greater than or equal to `2^8`.
-/
def UInt8.ofNatTruncate (n : Nat) : UInt8 :=
  if h : n < UInt8.size then
    UInt8.ofNatLT n h
  else
    UInt8.ofNatLT (UInt8.size - 1) (by decide)

Truncated conversion from natural number to 8-bit unsigned integer

Informal description

The function converts a natural number $ n $ to an 8-bit unsigned integer. If $ n $ is less than $ 256 $, it returns $ n $ as the unsigned 8-bit integer. Otherwise, it returns the maximum representable value $ 255 $.

Nat.toUInt8 abbrev

Full source

/--
Converts a natural number to an 8-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `Nat.toUInt8 5 = 5`
 * `Nat.toUInt8 255 = 255`
 * `Nat.toUInt8 256 = 0`
 * `Nat.toUInt8 259 = 3`
 * `Nat.toUInt8 32770 = 2`
-/
abbrev Nat.toUInt8 := UInt8.ofNat

Natural Number to 8-bit Unsigned Integer Conversion with Wrapping

Informal description

The function maps a natural number $n$ to an 8-bit unsigned integer by taking $n \mod 256$. This operation wraps around when $n$ exceeds the maximum value of 255. Examples: - $5 \mapsto 5$ - $255 \mapsto 255$ - $256 \mapsto 0$ - $259 \mapsto 3$ - $32770 \mapsto 2$

UInt8.toNat definition

(n : UInt8) : Nat

Full source

/--
Converts an 8-bit unsigned integer to an arbitrary-precision natural number.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_to_nat"]
def UInt8.toNat (n : UInt8) : Nat := n.toBitVec.toNat

Natural number representation of an 8-bit unsigned integer

Informal description

The function converts an 8-bit unsigned integer $ n $ to its natural number representation by interpreting the underlying bit pattern as a natural number.

UInt8.instOfNat instance

: OfNat UInt8 n

Full source

instance UInt8.instOfNat : OfNat UInt8 n := ⟨UInt8.ofNat n⟩

Numeric Literal Interpretation for Unsigned 8-bit Integers

Informal description

For any natural number $n$, there is a canonical interpretation of $n$ as an unsigned 8-bit integer via the wrapping operation $n \mod 256$.

UInt16.toFin definition

(x : UInt16) : Fin UInt16.size

Full source

/-- Converts a `UInt16` into the corresponding `Fin UInt16.size`. -/
def UInt16.toFin (x : UInt16) : Fin UInt16.size := x.toBitVec.toFin

Conversion from 16-bit unsigned integer to finite natural number

Informal description

The function converts a 16-bit unsigned integer $x$ to an element of the finite type $\text{Fin } 2^{16}$, which represents natural numbers less than $65536$. This conversion preserves the value of $x$ modulo $2^{16}$.

UInt16.val definition

(x : UInt16) : Fin UInt16.size

Full source

@[deprecated UInt16.toFin (since := "2025-02-12"), inherit_doc UInt16.toFin]
def UInt16.val (x : UInt16) : Fin UInt16.size := x.toFin

Value of a 16-bit unsigned integer as a finite natural number

Informal description

The function maps a 16-bit unsigned integer $ x $ to its value as a natural number less than $ 2^{16} $, represented as an element of the finite type $ \text{Fin } 2^{16} $.

UInt16.ofNat definition

(n : @& Nat) : UInt16

Full source

/--
Converts a natural number to a 16-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `UInt16.ofNat 5 = 5`
 * `UInt16.ofNat 255 = 255`
 * `UInt16.ofNat 32770 = 32770`
 * `UInt16.ofNat 65537 = 1`
-/
@[extern "lean_uint16_of_nat"]
def UInt16.ofNat (n : @& Nat) : UInt16 := ⟨BitVec.ofNat 16 n⟩

Natural number to 16-bit unsigned integer conversion with wrapping

Informal description

The function converts a natural number $n$ to a 16-bit unsigned integer by taking $n$ modulo $2^{16}$. This operation wraps around on overflow, meaning numbers larger than $2^{16} - 1$ are reduced to their remainder when divided by $2^{16}$.

UInt16.ofNatTruncate definition

(n : Nat) : UInt16

Full source

/--
Converts a natural number to a 16-bit unsigned integer, returning the largest representable value if
the number is too large.

Returns `2^16 - 1` for natural numbers greater than or equal to `2^16`.
-/
def UInt16.ofNatTruncate (n : Nat) : UInt16 :=
  if h : n < UInt16.size then
    UInt16.ofNatLT n h
  else
    UInt16.ofNatLT (UInt16.size - 1) (by decide)

Truncated conversion from natural number to 16-bit unsigned integer

Informal description

The function converts a natural number $ n $ to a 16-bit unsigned integer. If $ n $ is less than $ 2^{16} $, it returns the corresponding 16-bit unsigned integer. Otherwise, it returns the maximum representable value $ 2^{16} - 1 $.

Nat.toUInt16 abbrev

Full source

/--
Converts a natural number to a 16-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `Nat.toUInt16 5 = 5`
 * `Nat.toUInt16 255 = 255`
 * `Nat.toUInt16 32770 = 32770`
 * `Nat.toUInt16 65537 = 1`
-/
abbrev Nat.toUInt16 := UInt16.ofNat

Natural number to 16-bit unsigned integer conversion with wrapping

Informal description

The function $\mathrm{Nat.toUInt16}$ converts a natural number $n$ to a 16-bit unsigned integer by computing $n \mod 2^{16}$. This operation wraps around on overflow, meaning numbers larger than $2^{16} - 1$ are reduced to their remainder when divided by $2^{16}$.

UInt16.toNat definition

(n : UInt16) : Nat

Full source

/--
Converts a 16-bit unsigned integer to an arbitrary-precision natural number.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_to_nat"]
def UInt16.toNat (n : UInt16) : Nat := n.toBitVec.toNat

Natural number representation of a 16-bit unsigned integer

Informal description

The function converts a 16-bit unsigned integer $ n $ to its corresponding natural number representation. This is implemented by first converting the integer to a bitvector and then extracting the underlying natural number.

UInt16.toUInt8 definition

(a : UInt16) : UInt8

Full source

/--
Converts 16-bit unsigned integers to 8-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_to_uint8"]
def UInt16.toUInt8 (a : UInt16) : UInt8 := a.toNat.toUInt8

Conversion from 16-bit to 8-bit unsigned integer with wrapping

Informal description

The function converts a 16-bit unsigned integer $ a $ to an 8-bit unsigned integer by first converting $ a $ to a natural number and then taking the result modulo 256 (wrapping around on overflow).

UInt8.toUInt16 definition

(a : UInt8) : UInt16

Full source

/--
Converts 8-bit unsigned integers to 16-bit unsigned integers.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_to_uint16"]
def UInt8.toUInt16 (a : UInt8) : UInt16 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩

Conversion from 8-bit to 16-bit unsigned integer

Informal description

The function converts an 8-bit unsigned integer $ a $ to a 16-bit unsigned integer by interpreting the underlying natural number representation of $ a $ as a 16-bit value. This conversion preserves the numeric value of $ a $.

UInt16.instOfNat instance

: OfNat UInt16 n

Full source

instance UInt16.instOfNat : OfNat UInt16 n := ⟨UInt16.ofNat n⟩

Natural Number Literals as Unsigned 16-bit Integers

Informal description

For any natural number $n$, there is a canonical interpretation of $n$ as an unsigned 16-bit integer, obtained by taking $n \mod 2^{16}$.

UInt32.toFin definition

(x : UInt32) : Fin UInt32.size

Full source

/-- Converts a `UInt32` into the corresponding `Fin UInt32.size`. -/
def UInt32.toFin (x : UInt32) : Fin UInt32.size := x.toBitVec.toFin

Conversion from 32-bit unsigned integer to finite natural number

Informal description

The function maps a 32-bit unsigned integer $x$ to an element of the finite type $\text{Fin}(2^{32})$, which represents natural numbers less than $2^{32}$.

UInt32.val definition

(x : UInt32) : Fin UInt32.size

Full source

@[deprecated UInt32.toFin (since := "2025-02-12"), inherit_doc UInt32.toFin]
def UInt32.val (x : UInt32) : Fin UInt32.size := x.toFin

Conversion from 32-bit unsigned integer to finite natural number

Informal description

The function maps a 32-bit unsigned integer $x$ to an element of the finite type $\text{Fin}(2^{32})$, which represents natural numbers less than $2^{32}$.

UInt32.ofNat definition

(n : @& Nat) : UInt32

Full source

/--
Converts a natural number to a 32-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `UInt32.ofNat 5 = 5`
 * `UInt32.ofNat 65539 = 65539`
 * `UInt32.ofNat 4_294_967_299 = 3`
-/
@[extern "lean_uint32_of_nat"]
def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨BitVec.ofNat 32 n⟩

Natural number to 32-bit unsigned integer conversion (with wrap-around)

Informal description

The function maps a natural number $n$ to a 32-bit unsigned integer by taking $n$ modulo $2^{32}$. This operation wraps around on overflow, meaning that numbers larger than $2^{32} - 1$ are truncated to their least significant 32 bits.

UInt32.ofNat' definition

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

Full source

@[inline, deprecated UInt32.ofNatLT (since := "2025-02-13"), inherit_doc UInt32.ofNatLT]
def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32 := UInt32.ofNatLT n h

Natural number to unsigned 32-bit integer conversion (bounded)

Informal description

The function converts a natural number $ n $ to an unsigned 32-bit integer, given a proof that $ n < 2^{32} $.

UInt32.ofNatTruncate definition

(n : Nat) : UInt32

Full source

/--
Converts a natural number to a 32-bit unsigned integer, returning the largest representable value if
the number is too large.

Returns `2^32 - 1` for natural numbers greater than or equal to `2^32`.
-/
def UInt32.ofNatTruncate (n : Nat) : UInt32 :=
  if h : n < UInt32.size then
    UInt32.ofNatLT n h
  else
    UInt32.ofNatLT (UInt32.size - 1) (by decide)

Natural number to 32-bit unsigned integer conversion (with truncation)

Informal description

The function converts a natural number $ n $ to a 32-bit unsigned integer. If $ n $ is less than $ 2^{32} $, it returns the corresponding unsigned 32-bit integer representation of $ n $. Otherwise, it returns the largest representable 32-bit unsigned integer, $ 2^{32} - 1 $.

Nat.toUInt32 abbrev

Full source

/--
Converts a natural number to a 32-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `Nat.toUInt32 5 = 5`
 * `Nat.toUInt32 65_539 = 65_539`
 * `Nat.toUInt32 4_294_967_299 = 3`
-/
abbrev Nat.toUInt32 := UInt32.ofNat

Natural Number to 32-bit Unsigned Integer Conversion (with Wrap-around)

Informal description

The function maps a natural number $n$ to a 32-bit unsigned integer by taking $n \mod 2^{32}$. This operation wraps around on overflow, meaning that numbers larger than $2^{32} - 1$ are truncated to their least significant 32 bits.

UInt32.toUInt8 definition

(a : UInt32) : UInt8

Full source

/--
Converts a 32-bit unsigned integer to an 8-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_to_uint8"]
def UInt32.toUInt8 (a : UInt32) : UInt8 := a.toNat.toUInt8

32-bit to 8-bit unsigned integer conversion with wrapping

Informal description

The function converts a 32-bit unsigned integer $ a $ to an 8-bit unsigned integer by first converting $ a $ to a natural number and then taking the result modulo 256 (wrapping on overflow).

UInt32.toUInt16 definition

(a : UInt32) : UInt16

Full source

/--
Converts 32-bit unsigned integers to 16-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_to_uint16"]
def UInt32.toUInt16 (a : UInt32) : UInt16 := a.toNat.toUInt16

32-bit to 16-bit unsigned integer conversion with wrapping

Informal description

The function converts a 32-bit unsigned integer $ a $ to a 16-bit unsigned integer by first converting $ a $ to its natural number representation and then taking the result modulo $ 2^{16} $. This operation wraps around on overflow, meaning that numbers larger than $ 2^{16} - 1 $ are truncated to their least significant 16 bits.

UInt8.toUInt32 definition

(a : UInt8) : UInt32

Full source

/--
Converts 8-bit unsigned integers to 32-bit unsigned integers.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_to_uint32"]
def UInt8.toUInt32 (a : UInt8) : UInt32 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩

Conversion from 8-bit to 32-bit unsigned integer

Informal description

The function converts an 8-bit unsigned integer $ a $ to a 32-bit unsigned integer by interpreting the underlying bit pattern as a natural number and ensuring it fits within 32 bits.

UInt16.toUInt32 definition

(a : UInt16) : UInt32

Full source

/--
Converts 16-bit unsigned integers to 32-bit unsigned integers.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_to_uint32"]
def UInt16.toUInt32 (a : UInt16) : UInt32 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩

Conversion from 16-bit to 32-bit unsigned integer

Informal description

The function converts a 16-bit unsigned integer $ a $ to a 32-bit unsigned integer by preserving its value. The implementation ensures that the resulting 32-bit integer correctly represents the original 16-bit value.

UInt32.instOfNat instance

: OfNat UInt32 n

Full source

instance UInt32.instOfNat : OfNat UInt32 n := ⟨UInt32.ofNat n⟩

Natural Number Literals as Unsigned 32-bit Integers

Informal description

For any natural number $n$, there is a canonical interpretation of $n$ as an unsigned 32-bit integer via the modulo operation $n \mod 2^{32}$.

UInt32.ofNatLT_lt_of_lt theorem

{n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) : n < m → UInt32.ofNatLT n h1 < UInt32.ofNat m

Full source

theorem UInt32.ofNatLT_lt_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
     n < m → UInt32.ofNatLT n h1 < UInt32.ofNat m := by
  simp only [(· < ·), BitVec.toNat, ofNatLT, BitVec.ofNatLT, ofNat, BitVec.ofNat, Fin.ofNat',
    Nat.mod_eq_of_lt h2, imp_self]

Preservation of Strict Inequality in Conversion from Natural Numbers to Unsigned 32-bit Integers

Informal description

For any natural numbers $n$ and $m$ such that $n < 2^{32}$ and $m < 2^{32}$, if $n < m$, then the unsigned 32-bit integer representation of $n$ (constructed with a proof that $n < 2^{32}$) is strictly less than the unsigned 32-bit integer representation of $m$.

UInt32.ofNat'_lt_of_lt theorem

{n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) : n < m → UInt32.ofNatLT n h1 < UInt32.ofNat m

Full source

@[deprecated UInt32.ofNatLT_lt_of_lt (since := "2025-02-13")]
theorem UInt32.ofNat'_lt_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
     n < m → UInt32.ofNatLT n h1 < UInt32.ofNat m := UInt32.ofNatLT_lt_of_lt h1 h2

Preservation of Strict Inequality in Conversion from Natural Numbers to Unsigned 32-bit Integers

Informal description

For any natural numbers $n$ and $m$ such that $n < 2^{32}$ and $m < 2^{32}$, if $n < m$, then the unsigned 32-bit integer representation of $n$ (constructed with a proof that $n < 2^{32}$) is strictly less than the unsigned 32-bit integer representation of $m$.

UInt32.lt_ofNatLT_of_lt theorem

{n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) : m < n → UInt32.ofNat m < UInt32.ofNatLT n h1

Full source

theorem UInt32.lt_ofNatLT_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
     m < n → UInt32.ofNat m < UInt32.ofNatLT n h1 := by
  simp only [(· < ·), BitVec.toNat, ofNatLT, BitVec.ofNatLT, ofNat, BitVec.ofNat, Fin.ofNat',
    Nat.mod_eq_of_lt h2, imp_self]

Strict Order Preservation in UInt32 Conversion: $m < n \Rightarrow \text{ofNat}(m) < \text{ofNatLT}(n)$

Informal description

For any natural numbers $n$ and $m$ such that $n < 2^{32}$ and $m < 2^{32}$, if $m < n$ then the unsigned 32-bit integer representation of $m$ is less than the unsigned 32-bit integer representation of $n$ (constructed with the bound check proof $h1$).

UInt32.lt_ofNat'_of_lt theorem

{n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) : m < n → UInt32.ofNat m < UInt32.ofNatLT n h1

Full source

@[deprecated UInt32.lt_ofNatLT_of_lt (since := "2025-02-13")]
theorem UInt32.lt_ofNat'_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
     m < n → UInt32.ofNat m < UInt32.ofNatLT n h1 := UInt32.lt_ofNatLT_of_lt h1 h2

Strict Order Preservation in UInt32 Conversion: $m < n \Rightarrow \text{ofNat}(m) < \text{ofNatLT}(n)$

Informal description

For any natural numbers $n$ and $m$ such that $n < 2^{32}$ and $m < 2^{32}$, if $m < n$ then the unsigned 32-bit integer representation of $m$ (via `ofNat`) is less than the unsigned 32-bit integer representation of $n$ (via `ofNatLT` with bound check proof $h1$).

UInt64.toFin definition

(x : UInt64) : Fin UInt64.size

Full source

/-- Converts a `UInt64` into the corresponding `Fin UInt64.size`. -/
def UInt64.toFin (x : UInt64) : Fin UInt64.size := x.toBitVec.toFin

Conversion from 64-bit unsigned integer to finite natural number

Informal description

The function converts a 64-bit unsigned integer `x` into the corresponding element of the finite type `Fin UInt64.size`, where `UInt64.size` is $2^{64}$. This effectively maps `x` to its value interpreted as a natural number less than $2^{64}$.

UInt64.val definition

(x : UInt64) : Fin UInt64.size

Full source

@[deprecated UInt64.toFin (since := "2025-02-12"), inherit_doc UInt64.toFin]
def UInt64.val (x : UInt64) : Fin UInt64.size := x.toFin

Value of a 64-bit unsigned integer as a finite natural number

Informal description

The function maps a 64-bit unsigned integer `x` to its value as an element of the finite type `Fin UInt64.size`, which represents natural numbers less than $2^{64}$.

UInt64.ofNat definition

(n : @& Nat) : UInt64

Full source

/--
Converts a natural number to a 64-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `UInt64.ofNat 5 = 5`
 * `UInt64.ofNat 65539 = 65539`
 * `UInt64.ofNat 4_294_967_299 = 4_294_967_299`
 * `UInt64.ofNat 18_446_744_073_709_551_620 = 4`
-/
@[extern "lean_uint64_of_nat"]
def UInt64.ofNat (n : @& Nat) : UInt64 := ⟨BitVec.ofNat 64 n⟩

Conversion from natural numbers to 64-bit unsigned integers with wrapping

Informal description

The function converts a natural number $n$ to a 64-bit unsigned integer by taking the value modulo $2^{64}$. This operation wraps around on overflow, meaning that numbers larger than $2^{64}-1$ will be truncated to their least significant 64 bits.

UInt64.ofNatTruncate definition

(n : Nat) : UInt64

Full source

/--
Converts a natural number to a 64-bit unsigned integer, returning the largest representable value if
the number is too large.

Returns `2^64 - 1` for natural numbers greater than or equal to `2^64`.
-/
def UInt64.ofNatTruncate (n : Nat) : UInt64 :=
  if h : n < UInt64.size then
    UInt64.ofNatLT n h
  else
    UInt64.ofNatLT (UInt64.size - 1) (by decide)

Natural number to 64-bit unsigned integer conversion with truncation

Informal description

The function converts a natural number $ n $ to a 64-bit unsigned integer. If $ n $ is less than $ 2^{64} $, it returns the exact representation of $ n $. Otherwise, it returns the maximum representable value $ 2^{64} - 1 $.

Nat.toUInt64 abbrev

Full source

/--
Converts a natural number to a 64-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `Nat.toUInt64 5 = 5`
 * `Nat.toUInt64 65539 = 65539`
 * `Nat.toUInt64 4_294_967_299 = 4_294_967_299`
 * `Nat.toUInt64 18_446_744_073_709_551_620 = 4`
-/
abbrev Nat.toUInt64 := UInt64.ofNat

Natural Number to 64-bit Unsigned Integer Conversion with Wrapping

Informal description

The function $\mathrm{Nat.toUInt64}$ converts a natural number $n$ to a 64-bit unsigned integer by computing $n \mod 2^{64}$. This operation wraps around on overflow, meaning that numbers larger than $2^{64}-1$ are truncated to their least significant 64 bits.

UInt64.toNat definition

(n : UInt64) : Nat

Full source

/--
Converts a 64-bit unsigned integer to an arbitrary-precision natural number.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_to_nat"]
def UInt64.toNat (n : UInt64) : Nat := n.toBitVec.toNat

Conversion from 64-bit unsigned integer to natural number

Informal description

The function converts a 64-bit unsigned integer $ n $ to its representation as an arbitrary-precision natural number. This is implemented by first converting the integer to a bitvector and then extracting the natural number representation from the bitvector.

UInt64.toUInt8 definition

(a : UInt64) : UInt8

Full source

/--
Converts 64-bit unsigned integers to 8-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_to_uint8"]
def UInt64.toUInt8 (a : UInt64) : UInt8 := a.toNat.toUInt8

Conversion from 64-bit to 8-bit unsigned integer with wrapping

Informal description

The function converts a 64-bit unsigned integer $ a $ to an 8-bit unsigned integer by first converting $ a $ to a natural number and then taking the result modulo 256. This operation wraps around on overflow.

UInt64.toUInt16 definition

(a : UInt64) : UInt16

Full source

/--
Converts 64-bit unsigned integers to 16-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_to_uint16"]
def UInt64.toUInt16 (a : UInt64) : UInt16 := a.toNat.toUInt16

Conversion from 64-bit to 16-bit unsigned integer with wrapping

Informal description

The function converts a 64-bit unsigned integer $ a $ to a 16-bit unsigned integer by first converting $ a $ to a natural number and then taking the result modulo $ 2^{16} $. This operation wraps around on overflow.

UInt64.toUInt32 definition

(a : UInt64) : UInt32

Full source

/--
Converts 64-bit unsigned integers to 32-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_to_uint32"]
def UInt64.toUInt32 (a : UInt64) : UInt32 := a.toNat.toUInt32

Conversion from 64-bit to 32-bit unsigned integer (with wrap-around)

Informal description

The function converts a 64-bit unsigned integer $ a $ to a 32-bit unsigned integer by taking $ a \mod 2^{32} $. This operation wraps around on overflow, meaning that numbers larger than $ 2^{32} - 1 $ are truncated to their least significant 32 bits.

UInt8.toUInt64 definition

(a : UInt8) : UInt64

Full source

/--
Converts 8-bit unsigned integers to 64-bit unsigned integers.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_to_uint64"]
def UInt8.toUInt64 (a : UInt8) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩

Conversion from 8-bit to 64-bit unsigned integer

Informal description

The function converts an 8-bit unsigned integer $ a $ to a 64-bit unsigned integer by interpreting the underlying bit pattern as a natural number and ensuring it fits within 64 bits.

UInt16.toUInt64 definition

(a : UInt16) : UInt64

Full source

/--
Converts 16-bit unsigned integers to 64-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_to_uint64"]
def UInt16.toUInt64 (a : UInt16) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩

Conversion from 16-bit to 64-bit unsigned integer

Informal description

The function converts a 16-bit unsigned integer $ a $ to a 64-bit unsigned integer by interpreting the underlying bit pattern as a natural number and ensuring it fits within 64 bits. This operation wraps around on overflow.

UInt32.toUInt64 definition

(a : UInt32) : UInt64

Full source

/--
Converts 32-bit unsigned integers to 64-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_to_uint64"]
def UInt32.toUInt64 (a : UInt32) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩

Conversion from 32-bit to 64-bit unsigned integer

Informal description

The function converts a 32-bit unsigned integer $ a $ to a 64-bit unsigned integer by extending its value, wrapping around on overflow if necessary.

UInt64.instOfNat instance

: OfNat UInt64 n

Full source

instance UInt64.instOfNat : OfNat UInt64 n := ⟨UInt64.ofNat n⟩

Numeric Literal Interpretation for 64-bit Unsigned Integers

Informal description

For any natural number $n$, the type `UInt64` (unsigned 64-bit integers) can interpret $n$ as an element of `UInt64` via modular arithmetic (wrapping around at $2^{64}$).

usize_size_eq theorem

: USize.size = 4294967296 ∨ USize.size = 18446744073709551616

Full source

@[deprecated USize.size_eq (since := "2025-02-24")]
theorem usize_size_eq : USize.sizeUSize.size = 4294967296 ∨ USize.size = 18446744073709551616 :=
  USize.size_eq

Size of `USize` is $2^{32}$ or $2^{64}$

Informal description

The size of the unsigned word-size integer type `USize` is either $2^{32} = 4294967296$ or $2^{64} = 18446744073709551616$.

usize_size_pos theorem

: 0 < USize.size

Full source

@[deprecated USize.size_pos (since := "2025-02-24")]
theorem usize_size_pos : 0 < USize.size :=
  USize.size_pos

Positivity of USize Size: $0 < \text{USize.size}$

Informal description

The size of the unsigned word-size integer type `USize` is strictly positive, i.e., $0 < \text{USize.size}$.

usize_size_gt_zero theorem

: USize.size > 0

Full source

@[deprecated USize.size_pos (since := "2024-11-24")] theorem usize_size_gt_zero : USize.size > 0 :=
  USize.size_pos

Positivity of USize Size: $\text{USize.size} > 0$

Informal description

The size of the unsigned word-size integer type `USize` is strictly greater than zero, i.e., $\text{USize.size} > 0$.

USize.toFin definition

(x : USize) : Fin USize.size

Full source

/-- Converts a `USize` into the corresponding `Fin USize.size`. -/
def USize.toFin (x : USize) : Fin USize.size := x.toBitVec.toFin

Conversion from unsigned word-size integer to finite type

Informal description

The function converts an unsigned word-size integer $x$ into the corresponding element of `Fin USize.size`, where `USize.size` is $2^{\text{numBits}}$ (with `numBits` being the platform word size of 32 or 64 bits). This effectively maps the unsigned integer to a finite type with exactly `USize.size` elements.

USize.val definition

(x : USize) : Fin USize.size

Full source

@[deprecated USize.toFin (since := "2025-02-12"), inherit_doc USize.toFin]
def USize.val (x : USize) : Fin USize.size := x.toFin

Value of unsigned word-size integer as finite natural number

Informal description

The function maps an unsigned word-size integer $x$ to its corresponding element in the finite type `Fin USize.size`, where `USize.size` is $2^n$ with $n$ being the platform's word size (32 or 64 bits). This effectively represents $x$ as a natural number less than `USize.size$.

USize.ofNat definition

(n : @& Nat) : USize

Full source

/--
Converts an arbitrary-precision natural number to an unsigned word-sized integer, wrapping around on
overflow.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_of_nat"]
def USize.ofNat (n : @& Nat) : USize := ⟨BitVec.ofNat _ n⟩

Natural number to unsigned word-size integer conversion

Informal description

The function converts a natural number $n$ to an unsigned word-sized integer by taking the least significant bits of $n$ (wrapping around on overflow). The exact number of bits preserved depends on the platform's word size (32 or 64 bits).

USize.ofNatTruncate definition

(n : Nat) : USize

Full source

/--
Converts a natural number to `USize`, returning the largest representable value if the number is too
large.

Returns `USize.size - 1`, which is  `2^64 - 1` or `2^32 - 1` depending on the platform, for natural
numbers greater than or equal to `USize.size`.
-/
def USize.ofNatTruncate (n : Nat) : USize :=
  if h : n < USize.size then
    USize.ofNatLT n h
  else
    USize.ofNatLT (USize.size - 1) (Nat.pred_lt (Nat.ne_zero_of_lt USize.size_pos))

Truncated conversion from natural number to `USize`

Informal description

The function converts a natural number $ n $ to a `USize` value. If $ n $ is less than `USize.size` (the maximum representable value for `USize`), it returns the corresponding `USize` value. Otherwise, it returns the largest representable `USize` value, which is `USize.size - 1` (either $2^{32} - 1$ or $2^{64} - 1$ depending on the platform).

Nat.toUSize abbrev

Full source

@[inherit_doc USize.ofNat] abbrev Nat.toUSize := USize.ofNat

Natural number to unsigned word-size integer conversion

Informal description

The function converts a natural number to an unsigned word-sized integer by taking the least significant bits (wrapping around on overflow). The exact number of bits preserved depends on the platform's word size (32 or 64 bits).

USize.toNat definition

(n : USize) : Nat

Full source

/--
Converts a word-sized unsigned integer to an arbitrary-precision natural number.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_to_nat"]
def USize.toNat (n : USize) : Nat := n.toBitVec.toNat

Natural number representation of a word-sized unsigned integer

Informal description

The function converts a platform-dependent unsigned word-size integer $ n $ to its natural number representation by first interpreting it as a bitvector and then extracting the underlying natural number.

USize.add definition

(a b : USize) : USize

Full source

/--
Adds two word-sized unsigned integers, wrapping around on overflow.  Usually accessed via the `+`
operator.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_add"]
def USize.add (a b : USize) : USize := ⟨a.toBitVec + b.toBitVec⟩

Addition of platform-dependent unsigned word-size integers with wrap-around

Informal description

The function adds two platform-dependent unsigned word-size integers $ a $ and $ b $, wrapping around on overflow. The addition is performed by converting the integers to bitvectors and then adding them as natural numbers.

USize.sub definition

(a b : USize) : USize

Full source

/--
Subtracts one word-sized-bit unsigned integer from another, wrapping around on underflow. Usually
accessed via the `-` operator.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_sub"]
def USize.sub (a b : USize) : USize := ⟨a.toBitVec - b.toBitVec⟩

Subtraction of word-sized unsigned integers (with underflow wrap-around)

Informal description

The function subtracts one word-sized unsigned integer `b` from another `a`, wrapping around on underflow. The result is another word-sized unsigned integer. This operation is typically accessed via the `-` operator.

USize.lt definition

(a b : USize) : Prop

Full source

/--
Strict inequality of word-sized unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the `<` operator.
-/
def USize.lt (a b : USize) : Prop := a.toBitVec < b.toBitVec

Strict inequality of word-sized unsigned integers

Informal description

The strict inequality relation `<` for platform-dependent unsigned word-size integers is defined by converting the integers to bitvectors and comparing them as natural numbers.

USize.le definition

(a b : USize) : Prop

Full source

/--
Non-strict inequality of word-sized unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the `≤` operator.
-/
def USize.le (a b : USize) : Prop := a.toBitVec ≤ b.toBitVec

Inequality of word-sized unsigned integers

Informal description

The non-strict inequality relation for word-sized unsigned integers, defined as the natural number inequality of their corresponding bitvector representations. For any two unsigned word-size integers $a$ and $b$, $a \leq b$ holds if and only if the bitvector representation of $a$ is less than or equal to that of $b$.

USize.instOfNat instance

: OfNat USize n

Full source

instance USize.instOfNat : OfNat USize n := ⟨USize.ofNat n⟩

Natural Number Interpretation as Unsigned Word-Size Integer

Informal description

For any natural number $n$, there is a canonical interpretation of $n$ as an unsigned word-size integer.

instAddUSize instance

: Add USize

Full source

instance : Add USize       := ⟨USize.add⟩

Addition on Platform-Dependent Unsigned Integers

Informal description

The type `USize` of platform-dependent unsigned word-size integers has an addition operation `+` defined on it.

instSubUSize instance

: Sub USize

Full source

instance : Sub USize       := ⟨USize.sub⟩

Subtraction Operation on Word-Sized Unsigned Integers

Informal description

The type `USize` of platform-dependent unsigned word-size integers is equipped with a subtraction operation that wraps around on underflow.

instLTUSize instance

: LT USize

Full source

instance : LT USize        := ⟨USize.lt⟩

Strict Order on Platform-Dependent Unsigned Integers

Informal description

The type `USize` of platform-dependent unsigned word-size integers is equipped with a strict inequality relation `<`.

instLEUSize instance

: LE USize

Full source

instance : LE USize        := ⟨USize.le⟩

Non-strict Order on Platform-Dependent Unsigned Integers

Informal description

The type `USize` of platform-dependent unsigned word-size integers is equipped with a non-strict inequality relation `≤`.

USize.decLt definition

(a b : USize) : Decidable (a < b)

Full source

/--
Decides whether one word-sized unsigned integer is strictly less than another. Usually accessed via
the `DecidableLT USize` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if (6 : USize) < 7 then "yes" else "no") = "yes"`
 * `(if (5 : USize) < 5 then "yes" else "no") = "no"`
 * `show ¬((7 : USize) < 7) by decide`
-/
@[extern "lean_usize_dec_lt"]
def USize.decLt (a b : USize) : Decidable (a < b) :=
  inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))

Decidability of strict order on platform-dependent unsigned integers

Informal description

The function `USize.decLt` takes two platform-dependent unsigned word-size integers `a` and `b` and returns a constructive proof that the proposition `a < b` is decidable. This is implemented by converting the integers to bitvectors and using the decidability instance for the strict order on bitvectors.

USize.decLe definition

(a b : USize) : Decidable (a ≤ b)

Full source

/--
Decides whether one word-sized unsigned integer is less than or equal to another. Usually accessed
via the `DecidableLE USize` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if (15 : USize) ≤ 15 then "yes" else "no") = "yes"`
 * `(if (15 : USize) ≤ 5 then "yes" else "no") = "no"`
 * `(if (5 : USize) ≤ 15 then "yes" else "no") = "yes"`
 * `show (7 : USize) ≤ 7 by decide`
-/
@[extern "lean_usize_dec_le"]
def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
  inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))

Decidability of non-strict ordering for platform-dependent unsigned integers

Informal description

The function `USize.decLe` takes two platform-dependent unsigned word-size integers `a` and `b` and returns a constructive proof that the proposition `a ≤ b` is decidable. This is implemented by converting the integers to bitvectors and using the decidability instance for bitvector ordering.

instDecidableLtUSize instance

(a b : USize) : Decidable (a < b)

Full source

instance (a b : USize) : Decidable (a < b) := USize.decLt a b

Decidability of Strict Order on USize

Informal description

For any two platform-dependent unsigned word-size integers $a$ and $b$, the proposition $a < b$ is decidable.

instDecidableLeUSize instance

(a b : USize) : Decidable (a ≤ b)

Full source

instance (a b : USize) : Decidable (a ≤ b) := USize.decLe a b

Decidability of Non-strict Ordering on Platform-dependent Unsigned Integers

Informal description

For any two platform-dependent unsigned word-size integers $a$ and $b$, the proposition $a \leq b$ is decidable.