Converts a Fin UInt8.size into the corresponding UInt8.
Equations
- UInt8.ofFin a = { toBitVec := { toFin := a } }
Converts a natural number to an 8-bit unsigned integer. Requires a proof that the number is small
enough to be representable without overflow; it must be smaller than 2^8.
This function is overridden at runtime with an efficient implementation.
Equations
- UInt8.ofNatCore n h = UInt8.ofNatLT n h
Subtracts one 8-bit unsigned integer from another, wrapping around on underflow. Usually accessed
via the - operator.
This function is overridden at runtime with an efficient implementation.
Multiplies two 8-bit unsigned integers, wrapping around on overflow. Usually accessed via the *
operator.
This function is overridden at runtime with an efficient implementation.
Unsigned division for 8-bit unsigned integers, discarding the remainder. Usually accessed
via the / operator.
This operation is sometimes called “floor division.” Division by zero is defined to be zero.
This function is overridden at runtime with an efficient implementation.
The modulo operator for 8-bit unsigned integers, which computes the remainder when dividing one
integer by another. Usually accessed via the % operator.
When the divisor is 0, the result is the dividend rather than an error.
This function is overridden at runtime with an efficient implementation.
Examples:
Bitwise and for 8-bit unsigned integers. Usually accessed via the &&& operator.
Each bit of the resulting integer is set if the corresponding bits of both input integers are set.
This function is overridden at runtime with an efficient implementation.
Bitwise or for 8-bit unsigned integers. Usually accessed via the ||| operator.
Each bit of the resulting integer is set if at least one of the corresponding bits of both input integers are set.
This function is overridden at runtime with an efficient implementation.
Bitwise exclusive or for 8-bit unsigned integers. Usually accessed via the ^^^ operator.
Each bit of the resulting integer is set if exactly one of the corresponding bits of both input integers are set.
This function is overridden at runtime with an efficient implementation.
Bitwise left shift for 8-bit unsigned integers. Usually accessed via the <<< operator.
This function is overridden at runtime with an efficient implementation.
Bitwise right shift for 8-bit unsigned integers. Usually accessed via the >>> operator.
This function is overridden at runtime with an efficient implementation.
Equations
- instHModUInt8Nat = { hMod := UInt8.modn }
Bitwise complement, also known as bitwise negation, for 8-bit unsigned integers. Usually accessed
via the ~~~ prefix operator.
Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
This function is overridden at runtime with an efficient implementation.
Equations
- a.complement = { toBitVec := ~~~a.toBitVec }
Equations
- instComplementUInt8 = { complement := UInt8.complement }
Equations
- instShiftLeftUInt8 = { shiftLeft := UInt8.shiftLeft }
Equations
- instShiftRightUInt8 = { shiftRight := UInt8.shiftRight }
Decides whether one 8-bit unsigned integer is strictly less than another. Usually accessed via the
DecidableLT UInt8 instance.
This function is overridden at runtime with an efficient implementation.
Examples:
(if (6 : UInt8) < 7 then "yes" else "no") = "yes"(if (5 : UInt8) < 5 then "yes" else "no") = "no"show ¬((7 : UInt8) < 7) by decide
Decides whether one 8-bit unsigned integer is less than or equal to another. Usually accessed via the
DecidableLE UInt8 instance.
This function is overridden at runtime with an efficient implementation.
Examples:
(if (15 : UInt8) ≤ 15 then "yes" else "no") = "yes"(if (15 : UInt8) ≤ 5 then "yes" else "no") = "no"(if (5 : UInt8) ≤ 15 then "yes" else "no") = "yes"show (7 : UInt8) ≤ 7 by decide
Equations
- instDecidableLtUInt8 a b = a.decLt b
Equations
- instDecidableLeUInt8 a b = a.decLe b
Converts a Fin UInt16.size into the corresponding UInt16.
Equations
- UInt16.ofFin a = { toBitVec := { toFin := a } }
Converts a natural number to a 16-bit unsigned integer. Requires a proof that the number is small
enough to be representable without overflow; it must be smaller than 2^16.
This function is overridden at runtime with an efficient implementation.
Equations
- UInt16.ofNatCore n h = UInt16.ofNatLT n h
Subtracts one 16-bit unsigned integer from another, wrapping around on underflow. Usually accessed
via the - operator.
This function is overridden at runtime with an efficient implementation.
Multiplies two 16-bit unsigned integers, wrapping around on overflow. Usually accessed via the *
operator.
This function is overridden at runtime with an efficient implementation.
Unsigned division for 16-bit unsigned integers, discarding the remainder. Usually accessed
via the / operator.
This operation is sometimes called “floor division.” Division by zero is defined to be zero.
This function is overridden at runtime with an efficient implementation.
The modulo operator for 16-bit unsigned integers, which computes the remainder when dividing one
integer by another. Usually accessed via the % operator.
When the divisor is 0, the result is the dividend rather than an error.
This function is overridden at runtime with an efficient implementation.
Examples:
UInt16.mod 5 2 = 1UInt16.mod 4 2 = 0UInt16.mod 4 0 = 4
Bitwise and for 16-bit unsigned integers. Usually accessed via the &&& operator.
Each bit of the resulting integer is set if the corresponding bits of both input integers are set.
This function is overridden at runtime with an efficient implementation.
Bitwise or for 16-bit unsigned integers. Usually accessed via the ||| operator.
Each bit of the resulting integer is set if at least one of the corresponding bits of both input integers are set.
This function is overridden at runtime with an efficient implementation.
Bitwise exclusive or for 8-bit unsigned integers. Usually accessed via the ^^^ operator.
Each bit of the resulting integer is set if exactly one of the corresponding bits of both input integers are set.
This function is overridden at runtime with an efficient implementation.
Bitwise left shift for 16-bit unsigned integers. Usually accessed via the <<< operator.
This function is overridden at runtime with an efficient implementation.
Bitwise right shift for 16-bit unsigned integers. Usually accessed via the >>> operator.
This function is overridden at runtime with an efficient implementation.
Equations
- instHModUInt16Nat = { hMod := UInt16.modn }
Bitwise complement, also known as bitwise negation, for 16-bit unsigned integers. Usually accessed
via the ~~~ prefix operator.
Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
This function is overridden at runtime with an efficient implementation.
Equations
- a.complement = { toBitVec := ~~~a.toBitVec }
Negation of 16-bit unsigned integers, computed modulo UInt16.size.
UInt16.neg a is equivalent to 65_535 - a + 1.
This function is overridden at runtime with an efficient implementation.
Equations
- instComplementUInt16 = { complement := UInt16.complement }
Equations
- instShiftLeftUInt16 = { shiftLeft := UInt16.shiftLeft }
Equations
- instShiftRightUInt16 = { shiftRight := UInt16.shiftRight }
Decides whether one 16-bit unsigned integer is strictly less than another. Usually accessed via the
DecidableLT UInt16 instance.
This function is overridden at runtime with an efficient implementation.
Examples:
(if (6 : UInt16) < 7 then "yes" else "no") = "yes"(if (5 : UInt16) < 5 then "yes" else "no") = "no"show ¬((7 : UInt16) < 7) by decide
Decides whether one 16-bit unsigned integer is less than or equal to another. Usually accessed via the
DecidableLE UInt16 instance.
This function is overridden at runtime with an efficient implementation.
Examples:
(if (15 : UInt16) ≤ 15 then "yes" else "no") = "yes"(if (15 : UInt16) ≤ 5 then "yes" else "no") = "no"(if (5 : UInt16) ≤ 15 then "yes" else "no") = "yes"show (7 : UInt16) ≤ 7 by decide
Equations
- instDecidableLtUInt16 a b = a.decLt b
Equations
- instDecidableLeUInt16 a b = a.decLe b
Converts a Fin UInt32.size into the corresponding UInt32.
Equations
- UInt32.ofFin a = { toBitVec := { toFin := a } }
Converts a natural number to a 32-bit unsigned integer. Requires a proof that the number is small
enough to be representable without overflow; it must be smaller than 2^32.
This function is overridden at runtime with an efficient implementation.
Equations
- UInt32.ofNatCore n h = UInt32.ofNatLT n h
Subtracts one 32-bit unsigned integer from another, wrapping around on underflow. Usually accessed
via the - operator.
This function is overridden at runtime with an efficient implementation.
Multiplies two 32-bit unsigned integers, wrapping around on overflow. Usually accessed via the *
operator.
This function is overridden at runtime with an efficient implementation.
Unsigned division for 32-bit unsigned integers, discarding the remainder. Usually accessed
via the / operator.
This operation is sometimes called “floor division.” Division by zero is defined to be zero.
This function is overridden at runtime with an efficient implementation.
The modulo operator for 32-bit unsigned integers, which computes the remainder when dividing one
integer by another. Usually accessed via the % operator.
When the divisor is 0, the result is the dividend rather than an error.
This function is overridden at runtime with an efficient implementation.
Examples:
UInt32.mod 5 2 = 1UInt32.mod 4 2 = 0UInt32.mod 4 0 = 4
Bitwise and for 32-bit unsigned integers. Usually accessed via the &&& operator.
Each bit of the resulting integer is set if the corresponding bits of both input integers are set.
This function is overridden at runtime with an efficient implementation.
Bitwise or for 32-bit unsigned integers. Usually accessed via the ||| operator.
Each bit of the resulting integer is set if at least one of the corresponding bits of both input integers are set.
This function is overridden at runtime with an efficient implementation.
Bitwise exclusive or for 32-bit unsigned integers. Usually accessed via the ^^^ operator.
Each bit of the resulting integer is set if exactly one of the corresponding bits of both input integers are set.
This function is overridden at runtime with an efficient implementation.
Bitwise left shift for 32-bit unsigned integers. Usually accessed via the <<< operator.
This function is overridden at runtime with an efficient implementation.
Bitwise right shift for 32-bit unsigned integers. Usually accessed via the >>> operator.
This function is overridden at runtime with an efficient implementation.
Equations
- instHModUInt32Nat = { hMod := UInt32.modn }
Bitwise complement, also known as bitwise negation, for 32-bit unsigned integers. Usually accessed
via the ~~~ prefix operator.
Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
This function is overridden at runtime with an efficient implementation.
Equations
- a.complement = { toBitVec := ~~~a.toBitVec }
Negation of 32-bit unsigned integers, computed modulo UInt32.size.
UInt32.neg a is equivalent to 429_4967_295 - a + 1.
This function is overridden at runtime with an efficient implementation.
Equations
- instComplementUInt32 = { complement := UInt32.complement }
Equations
- instShiftLeftUInt32 = { shiftLeft := UInt32.shiftLeft }
Equations
- instShiftRightUInt32 = { shiftRight := UInt32.shiftRight }
Converts a Fin UInt64.size into the corresponding UInt64.
Equations
- UInt64.ofFin a = { toBitVec := { toFin := a } }
Converts a natural number to a 64-bit unsigned integer. Requires a proof that the number is small
enough to be representable without overflow; it must be smaller than 2^64.
This function is overridden at runtime with an efficient implementation.
Equations
- UInt64.ofNatCore n h = UInt64.ofNatLT n h
Subtracts one 64-bit unsigned integer from another, wrapping around on underflow. Usually accessed
via the - operator.
This function is overridden at runtime with an efficient implementation.
Multiplies two 64-bit unsigned integers, wrapping around on overflow. Usually accessed via the *
operator.
This function is overridden at runtime with an efficient implementation.
Unsigned division for 64-bit unsigned integers, discarding the remainder. Usually accessed
via the / operator.
This operation is sometimes called “floor division.” Division by zero is defined to be zero.
This function is overridden at runtime with an efficient implementation.
The modulo operator for 64-bit unsigned integers, which computes the remainder when dividing one
integer by another. Usually accessed via the % operator.
When the divisor is 0, the result is the dividend rather than an error.
This function is overridden at runtime with an efficient implementation.
Examples:
UInt64.mod 5 2 = 1UInt64.mod 4 2 = 0UInt64.mod 4 0 = 4
Bitwise and for 64-bit unsigned integers. Usually accessed via the &&& operator.
Each bit of the resulting integer is set if the corresponding bits of both input integers are set.
This function is overridden at runtime with an efficient implementation.
Bitwise or for 64-bit unsigned integers. Usually accessed via the ||| operator.
Each bit of the resulting integer is set if at least one of the corresponding bits of both input integers are set.
This function is overridden at runtime with an efficient implementation.
Bitwise exclusive or for 64-bit unsigned integers. Usually accessed via the ^^^ operator.
Each bit of the resulting integer is set if exactly one of the corresponding bits of both input integers are set.
This function is overridden at runtime with an efficient implementation.
Bitwise left shift for 64-bit unsigned integers. Usually accessed via the <<< operator.
This function is overridden at runtime with an efficient implementation.
Bitwise right shift for 64-bit unsigned integers. Usually accessed via the >>> operator.
This function is overridden at runtime with an efficient implementation.
Equations
- instHModUInt64Nat = { hMod := UInt64.modn }
Bitwise complement, also known as bitwise negation, for 64-bit unsigned integers. Usually accessed
via the ~~~ prefix operator.
Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
This function is overridden at runtime with an efficient implementation.
Equations
- a.complement = { toBitVec := ~~~a.toBitVec }
Negation of 32-bit unsigned integers, computed modulo UInt64.size.
UInt64.neg a is equivalent to 18_446_744_073_709_551_615 - a + 1.
This function is overridden at runtime with an efficient implementation.
Equations
- instComplementUInt64 = { complement := UInt64.complement }
Equations
- instShiftLeftUInt64 = { shiftLeft := UInt64.shiftLeft }
Equations
- instShiftRightUInt64 = { shiftRight := UInt64.shiftRight }
Decides whether one 64-bit unsigned integer is strictly less than another. Usually accessed via the
DecidableLT UInt64 instance.
This function is overridden at runtime with an efficient implementation.
Examples:
(if (6 : UInt64) < 7 then "yes" else "no") = "yes"(if (5 : UInt64) < 5 then "yes" else "no") = "no"show ¬((7 : UInt64) < 7) by decide
Decides whether one 64-bit unsigned integer is less than or equal to another. Usually accessed via the
DecidableLE UInt64 instance.
This function is overridden at runtime with an efficient implementation.
Examples:
(if (15 : UInt64) ≤ 15 then "yes" else "no") = "yes"(if (15 : UInt64) ≤ 5 then "yes" else "no") = "no"(if (5 : UInt64) ≤ 15 then "yes" else "no") = "yes"show (7 : UInt64) ≤ 7 by decide
Equations
- instDecidableLtUInt64 a b = a.decLt b
Equations
- instDecidableLeUInt64 a b = a.decLe b
Converts a Fin USize.size into the corresponding USize.
Equations
- USize.ofFin a = { toBitVec := { toFin := a } }
Creates a USize from a BitVec System.Platform.numBits. This function is overridden with a
native implementation.
Converts a natural number to a USize. Requires a proof that the number is small enough to be
representable without overflow.
This function is overridden at runtime with an efficient implementation.
Equations
- USize.ofNatCore n h = USize.ofNatLT n h
Multiplies two word-sized unsigned integers, wrapping around on overflow. Usually accessed via the
* operator.
This function is overridden at runtime with an efficient implementation.
Unsigned division for word-sized unsigned integers, discarding the remainder. Usually accessed
via the / operator.
This operation is sometimes called “floor division.” Division by zero is defined to be zero.
This function is overridden at runtime with an efficient implementation.
The modulo operator for word-sized unsigned integers, which computes the remainder when dividing one
integer by another. Usually accessed via the % operator.
When the divisor is 0, the result is the dividend rather than an error.
This function is overridden at runtime with an efficient implementation.
Examples:
Bitwise and for word-sized unsigned integers. Usually accessed via the &&& operator.
Each bit of the resulting integer is set if the corresponding bits of both input integers are set.
This function is overridden at runtime with an efficient implementation.
Bitwise or for word-sized unsigned integers. Usually accessed via the ||| operator.
Each bit of the resulting integer is set if at least one of the corresponding bits of both input integers are set.
This function is overridden at runtime with an efficient implementation.
Bitwise exclusive or for word-sized unsigned integers. Usually accessed via the ^^^ operator.
Each bit of the resulting integer is set if exactly one of the corresponding bits of both input integers are set.
This function is overridden at runtime with an efficient implementation.
Bitwise left shift for word-sized unsigned integers. Usually accessed via the <<< operator.
This function is overridden at runtime with an efficient implementation.
Equations
- a.shiftLeft b = { toBitVec := a.toBitVec <<< (b.mod (USize.ofNat System.Platform.numBits)).toBitVec }
Bitwise right shift for word-sized unsigned integers. Usually accessed via the >>> operator.
This function is overridden at runtime with an efficient implementation.
Equations
- a.shiftRight b = { toBitVec := a.toBitVec >>> (b.mod (USize.ofNat System.Platform.numBits)).toBitVec }
Converts a natural number to a USize. Overflow is impossible on any supported platform because
USize.size is either 2^32 or 2^64.
This function is overridden at runtime with an efficient implementation.
Equations
- USize.ofNat32 n h = USize.ofNatLT n ⋯
Converts 8-bit unsigned integers to word-sized unsigned integers.
This function is overridden at runtime with an efficient implementation.
Equations
- a.toUSize = USize.ofNat32 a.toBitVec.toNat ⋯
Converts 16-bit unsigned integers to word-sized unsigned integers.
This function is overridden at runtime with an efficient implementation.
Equations
- a.toUSize = USize.ofNat32 a.toBitVec.toNat ⋯
Converts 32-bit unsigned integers to word-sized unsigned integers.
This function is overridden at runtime with an efficient implementation.
Equations
- a.toUSize = USize.ofNat32 a.toBitVec.toNat ⋯
Converts word-sized unsigned integers to 32-bit unsigned integers. Wraps around on overflow, which might occur on 64-bit architectures.
This function is overridden at runtime with an efficient implementation.
Converts 64-bit unsigned integers to word-sized unsigned integers. On 32-bit machines, this may
overflow, which results in the value wrapping around (that is, it is reduced modulo USize.size).
This function is overridden at runtime with an efficient implementation.
Converts word-sized unsigned integers to 32-bit unsigned integers. This cannot overflow because
USize.size is either 2^32 or 2^64.
This function is overridden at runtime with an efficient implementation.
Equations
- a.toUInt64 = UInt64.ofNatLT a.toBitVec.toNat ⋯
Equations
- instHModUSizeNat = { hMod := USize.modn }
Bitwise complement, also known as bitwise negation, for word-sized unsigned integers. Usually
accessed via the ~~~ prefix operator.
Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
This function is overridden at runtime with an efficient implementation.
Equations
- a.complement = { toBitVec := ~~~a.toBitVec }
Equations
- instComplementUSize = { complement := USize.complement }
Equations
- instShiftLeftUSize = { shiftLeft := USize.shiftLeft }
Equations
- instShiftRightUSize = { shiftRight := USize.shiftRight }