The logical model for the Float type.

This is defined as the type of UInt64 with the additional restriction that bit patterns encoding a NaN must be exactly a chosen canonical NaN.

Most functions on Float.Model work by unpacking the Float.Model into the inductive type UnpackedFloat, performing the operation there, and then repacking the result into a Float.Model.

It is not a goal of this development to serve as the basis for a general-purpose floating-point library or to have any direct lemmas written about it at all. Rather, users interested in a library about floating-point numbers should develop such a library completely separately, and users interested in proving properties of their programs involving Float should prove that the operations defined here are equivalent to the operations defined in the separate library and then transfer lemmas from the library to the Float and Float32 types.

Constructor

Float.Model.mk

Fields

toBits : UInt64

valid : Float.Model.Format.binary64.Valid self.toBits.toBitVec

The logical model for the Float32 type.

This is defined as the type of UInt32 with the additional restriction that bit patterns encoding a NaN must be exactly a chosen canonical NaN.

Most functions on Float32.Model work by unpacking the Float32.Model into the inductive type UnpackedFloat, performing the operation there, and then repacking the result into a Float32.Model.

It is not a goal of this development to serve as the basis for a general-purpose floating-point library or to have any direct lemmas written about it at all. Rather, users interested in a library about floating-point numbers should develop such a library completely separately, and users interested in proving properties of their programs involving Float32 should prove that the operations defined here are equivalent to the operations defined in the separate library and then transfer lemmas from the library to the Float and Float32 types.

Constructor

Float32.Model.mk

Fields

toBits : UInt32

valid : Float.Model.Format.binary32.Valid self.toBits.toBitVec

Pack an UnpackedFloat into the corresponding Float.Model. This operation only gives a meaningful result if the float is already correctly rounded for the Format.binary64 format.

Pack an UnpackedFloat into the corresponding Float32.Model. This operation only gives a meaningful result if the float is already correctly rounded for the Format.binary32 format.

Unpack a Float.Model into the corresponding UnpackedFloat.

Unpack a Float32.Model into the corresponding UnpackedFloat.

An inductive type representing a floating-point number with constructors for signed infinity, not-a-number without payload, signed zero, and finite floats with a sign, positive natural mantissa and integral exponent.

Finite floats do not have a unique representation in this format: multiplying the mantissa by two and decreasing the exponent by one yields a finite float that represents the same rational number.

For a given Format, we say that an unpacked float is in canonical form if the exponent is equal to the targetExponent according to that format. Some operations on UnpackedFloat, such as compare, assume that the input(s) are all in canonical form for the same format.

Note that an unpacked float in canonical form for a given format may not actually be representable in that format as the exponent is too large to fit. In this case, the pack function will overflow the float to infinity.

This type exists solely for the purpose of supporting Float.Model and Float32.Model. It is not a goal of this development to serve as the basis for a general-purpose floating-point library or to have any direct lemmas written about it at all. Rather, users interested in a library about floating-point numbers should develop such a library completely separately, and users interested in proving properties of their programs involving Float should prove that the operations defined here are equivalent to the operations defined in the separate library and then transfer lemmas from the library to the Float and Float32 types.

Constructors

Float.Model.UnpackedFloat.infinity
  (sign : Float.Model.UnpackedFloat.Sign) :
  Float.Model.UnpackedFloat

Float.Model.UnpackedFloat.notANumber :
  Float.Model.UnpackedFloat

Float.Model.UnpackedFloat.zero
  (sign : Float.Model.UnpackedFloat.Sign) :
  Float.Model.UnpackedFloat

Float.Model.UnpackedFloat.finite
  (sign : Float.Model.UnpackedFloat.Sign) (mantissa : Nat)
  (exponent : Int) (mantissa_pos : 0 < mantissa) :
  Float.Model.UnpackedFloat

Computes the sum of two floating point numbers and rounds the result according to the given specification.

Computes the difference of two floating point numbers and rounds the result according to the given specification.

Computes the product of two floating-point numbers and rounds the result according to the given specification.

Computes the quotient of two floating point numbers and rounds the result according to the given specification.

Computes the square root of a floating-point number and rounds the result according to the given specification.

Negates the given float.

Returns the given float with positive sign.

Returns true if the float is NaN.

Returns true if the float is positive or negative infinity.

Returns true if the float represents a real number, i.e., it is neither infinite nor NaN.

Computes the ordering between the two floats as specificed by IEEE. Returns an Option Ordering to account for the fact that NaN is incomparable with everything. Also, positive and negative zero are equal.

Important: this operation only works correctly if the two inputs are in canonical form for a common format (see the docstring for UnpackedFloat for details.)

Determines whether a is equal to b according to IEEE rules.

This is not a reflexive relation.

Determines whether a is less than b according to IEEE rules.

This is not a total ordering.

Determines whether a is less than or equal to b according to IEEE rules.

This is not a total ordering, and ≤ is not reflexive.

Converts a Nat to an UnpackedFloat, returning positive zero on zero.

Converts an Int to an UnpackedFloat, returning positive zero on zero.

Computes m * 10 ^ e.

Converts an UnpackedFloat to an Int8, truncating after the decimal point, sending NaN to 0 and clamping out-of-range values and infinities.

Converts an Int8 to an UnpackedFloat, returning positive zero on zero.

Converts an UnpackedFloat to an Int16, truncating after the decimal point, sending NaN to 0 and clamping out-of-range values and infinities.

Converts an Int16 to an UnpackedFloat, returning positive zero on zero.

Converts an UnpackedFloat to an Int32, truncating after the decimal point, sending NaN to 0 and clamping out-of-range values and infinities.

Converts an Int32 to an UnpackedFloat, returning positive zero on zero.

Converts an UnpackedFloat to an Int64, truncating after the decimal point, sending NaN to 0 and clamping out-of-range values and infinities.

Converts an Int64 to an UnpackedFloat, returning positive zero on zero.

Converts an UnpackedFloat to an ISize, truncating after the decimal point, sending NaN to 0 and clamping out-of-range values and infinities.

Converts an ISize to an UnpackedFloat, returning positive zero on zero.

Converts an UnpackedFloat to a UInt8, truncating after the decimal point, sending NaN to 0 and clamping out-of-range values and infinities.

Converts a UInt8 to an UnpackedFloat, returning positive zero on zero.

Converts an UnpackedFloat to a UInt16, truncating after the decimal point, sending NaN to 0 and clamping out-of-range values and infinities.

Converts a UInt16 to an UnpackedFloat, returning positive zero on zero.

Converts an UnpackedFloat to a UInt32, truncating after the decimal point, sending NaN to 0 and clamping out-of-range values and infinities.

Converts a UInt32 to an UnpackedFloat, returning positive zero on zero.

Converts an UnpackedFloat to a UInt64, truncating after the decimal point, sending NaN to 0 and clamping out-of-range values and infinities.

Converts a UInt64 to an UnpackedFloat, returning positive zero on zero.

Converts an UnpackedFloat to a USize, truncating after the decimal point, sending NaN to 0 and clamping out-of-range values and infinities.

Converts a USize to an UnpackedFloat, returning positive zero on zero.

Checks whether a floating-point number is a positive or negative infinite number, but not a finite number or NaN.

This function has a logical model in terms of Float.Model. It is compiled to the C operator isinf.

Checks whether a floating-point number is a positive or negative infinite number, but not a finite number or NaN.

This function has a logical model in terms of Float32.Model. It is compiled to the C operator isinf.

Checks whether a floating point number is NaN (“not a number”) value.

NaN values result from operations that might otherwise be errors, such as dividing zero by zero.

This function has a logical model in terms of Float.Model. It is compiled to the C operator isnan.

Checks whether a floating point number is NaN ("not a number") value.

NaN values result from operations that might otherwise be errors, such as dividing zero by zero.

This function has a logical model in terms of Float32.Model. It is compiled to the C operator isnan.

Checks whether a floating-point number is finite, that is, whether it is normal, subnormal, or zero, but not infinite or NaN.

This function has a logical model in terms of Float.Model. It is compiled to the C operator isfinite.

Checks whether a floating-point number is finite, that is, whether it is normal, subnormal, or zero, but not infinite or NaN.

This function has a logical model in terms of Float32.Model. It is compiled to the C operator isfinite.

Bit-for-bit conversion to UInt64. Interprets a Float as a UInt64, ignoring the numeric value and treating the Float's bit pattern as a UInt64.

Floats and UInt64s have the same endianness on all supported platforms. IEEE 754 very precisely specifies the bit layout of floats.

This function is distinct from Float.toUInt64, which attempts to preserve the numeric value rather than reinterpreting the bit pattern.

Bit-for-bit conversion to UInt32. Interprets a Float32 as a UInt32, ignoring the numeric value and treating the Float32's bit pattern as a UInt32.

Float32s and UInt32s have the same endianness on all supported platforms. IEEE 754 very precisely specifies the bit layout of floats.

This function is distinct from Float.toUInt32, which attempts to preserve the numeric value rather than reinterpreting the bit pattern.

Bit-for-bit conversion from UInt64. Interprets a UInt64 as a Float, ignoring the numeric value and treating the UInt64's bit pattern as a Float.

Floats and UInt64s have the same endianness on all supported platforms. IEEE 754 very precisely specifies the bit layout of floats.

This function has a logical model in terms of Float.Model.

Bit-for-bit conversion from UInt32. Interprets a UInt32 as a Float32, ignoring the numeric value and treating the UInt32's bit pattern as a Float32.

Float32s and UInt32s have the same endianness on all supported platforms. IEEE 754 very precisely specifies the bit layout of floats.

This function has a logical model in terms of Float32.Model.

Converts a 64-bit floating-point number to a 32-bit floating-point number. This may lose precision.

This function does not reduce in the kernel.

Converts a 32-bit floating-point number to a 64-bit floating-point number.

This function does not reduce in the kernel.

Converts a floating-point number to a string.

This function does not reduce in the kernel.

Converts a floating-point number to a string.

This function does not reduce in the kernel.

Converts a floating-point number to an 8-bit unsigned integer.

If the given Float is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of UInt8. Returns 0 if the Float is negative or NaN, and returns the largest UInt8 value (i.e. UInt8.size - 1) if the float is larger than it.

This function has a logical model in terms of Float.Model.

Truncates a floating-point number to the nearest 8-bit signed integer, rounding towards zero.

If the Float is larger than the maximum value for Int8 (including Inf), returns the maximum value of Int8 (i.e. Int8.maxValue). If it is smaller than the minimum value for Int8 (including -Inf), returns the minimum value of Int8 (i.e. Int8.minValue). If it is NaN, returns 0.

This function does not reduce in the kernel.

Converts a floating-point number to an 8-bit unsigned integer.

If the given Float32 is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of UInt8. Returns 0 if the Float32 is negative or NaN, and returns the largest UInt8 value (i.e. UInt8.size - 1) if the float is larger than it.

This function has a logical model in terms of Float32.Model.

Truncates a floating-point number to the nearest 8-bit signed integer, rounding towards zero.

If the Float is larger than the maximum value for Int8 (including Inf), returns the maximum value of Int8 (i.e. Int8.maxValue). If it is smaller than the minimum value for Int8 (including -Inf), returns the minimum value of Int8 (i.e. Int8.minValue). If it is NaN, returns 0.

This function does not reduce in the kernel.

Converts a floating-point number to a 16-bit unsigned integer.

If the given Float is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of UInt16. Returns 0 if the Float is negative or NaN, and returns the largest UInt16 value (i.e. UInt16.size - 1) if the float is larger than it.

This function has a logical model in terms of Float.Model.

Truncates a floating-point number to the nearest 16-bit signed integer, rounding towards zero.

If the Float is larger than the maximum value for Int16 (including Inf), returns the maximum value of Int16 (i.e. Int16.maxValue). If it is smaller than the minimum value for Int16 (including -Inf), returns the minimum value of Int16 (i.e. Int16.minValue). If it is NaN, returns 0.

This function does not reduce in the kernel.

Converts a floating-point number to a 16-bit unsigned integer.

If the given Float32 is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of UInt16. Returns 0 if the Float32 is negative or NaN, and returns the largest UInt16 value (i.e. UInt16.size - 1) if the float is larger than it.

This function has a logical model in terms of Float32.Model.

Truncates a floating-point number to the nearest 16-bit signed integer, rounding towards zero.

If the Float is larger than the maximum value for Int16 (including Inf), returns the maximum value of Int16 (i.e. Int16.maxValue). If it is smaller than the minimum value for Int16 (including -Inf), returns the minimum value of Int16 (i.e. Int16.minValue). If it is NaN, returns 0.

This function does not reduce in the kernel.

Converts a floating-point number to a 32-bit unsigned integer.

If the given Float is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of UInt32. Returns 0 if the Float is negative or NaN, and returns the largest UInt32 value (i.e. UInt32.size - 1) if the float is larger than it.

This function has a logical model in terms of Float.Model.

Converts a floating-point number to a 32-bit unsigned integer.

If the given Float32 is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of UInt32. Returns 0 if the Float32 is negative or NaN, and returns the largest UInt32 value (i.e. UInt32.size - 1) if the float is larger than it.

This function has a logical model in terms of Float32.Model.

Truncates a floating-point number to the nearest 32-bit signed integer, rounding towards zero.

If the Float is larger than the maximum value for Int32 (including Inf), returns the maximum value of Int32 (i.e. Int32.maxValue). If it is smaller than the minimum value for Int32 (including -Inf), returns the minimum value of Int32 (i.e. Int32.minValue). If it is NaN, returns 0.

This function does not reduce in the kernel.

Truncates a floating-point number to the nearest 32-bit signed integer, rounding towards zero.

If the Float is larger than the maximum value for Int32 (including Inf), returns the maximum value of Int32 (i.e. Int32.maxValue). If it is smaller than the minimum value for Int32 (including -Inf), returns the minimum value of Int32 (i.e. Int32.minValue). If it is NaN, returns 0.

This function does not reduce in the kernel.

Converts a floating-point number to a 64-bit unsigned integer.

If the given Float is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of UInt64. Returns 0 if the Float is negative or NaN, and returns the largest UInt64 value (i.e. UInt64.size - 1) if the float is larger than it.

This function has a logical model in terms of Float.Model.

Truncates a floating-point number to the nearest 64-bit signed integer, rounding towards zero.

If the Float is larger than the maximum value for Int64 (including Inf), returns the maximum value of Int64 (i.e. Int64.maxValue). If it is smaller than the minimum value for Int64 (including -Inf), returns the minimum value of Int64 (i.e. Int64.minValue). If it is NaN, returns 0.

This function does not reduce in the kernel.

Converts a floating-point number to a 64-bit unsigned integer.

If the given Float32 is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of UInt64. Returns 0 if the Float32 is negative or NaN, and returns the largest UInt64 value (i.e. UInt64.size - 1) if the float is larger than it.

This function has a logical model in terms of Float32.Model.

Truncates a floating-point number to the nearest 64-bit signed integer, rounding towards zero.

If the Float is larger than the maximum value for Int64 (including Inf), returns the maximum value of Int64 (i.e. Int64.maxValue). If it is smaller than the minimum value for Int64 (including -Inf), returns the minimum value of Int64 (i.e. Int64.minValue). If it is NaN, returns 0.

This function does not reduce in the kernel.

Converts a floating-point number to a word-sized unsigned integer.

If the given Float is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of USize. Returns 0 if the Float is negative or NaN, and returns the largest USize value (i.e. USize.size - 1) if the float is larger than it.

This function has a logical model in terms of Float.Model.

Converts a floating-point number to a word-sized unsigned integer.

If the given Float32 is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of USize. Returns 0 if the Float32 is negative or NaN, and returns the largest USize value (i.e. USize.size - 1) if the float is larger than it.

This function has a logical model in terms of Float32.Model.

Truncates a floating-point number to the nearest word-sized signed integer, rounding towards zero.

If the Float is larger than the maximum value for ISize (including Inf), returns the maximum value of ISize (i.e. ISize.maxValue). If it is smaller than the minimum value for ISize (including -Inf), returns the minimum value of ISize (i.e. ISize.minValue). If it is NaN, returns 0.

This function does not reduce in the kernel.

Truncates a floating-point number to the nearest word-sized signed integer, rounding towards zero.

If the Float is larger than the maximum value for ISize (including Inf), returns the maximum value of ISize (i.e. ISize.maxValue). If it is smaller than the minimum value for ISize (including -Inf), returns the minimum value of ISize (i.e. ISize.minValue). If it is NaN, returns 0.

This function does not reduce in the kernel.

Converts an integer into the closest-possible 64-bit floating-point number, or positive or negative infinite floating-point value if the range of Float is exceeded.

Converts an integer into the closest-possible 32-bit floating-point number, or positive or negative infinite floating-point value if the range of Float32 is exceeded.

Converts a natural number into the closest-possible 64-bit floating-point number, or an infinite floating-point value if the range of Float is exceeded.

Converts a natural number into the closest-possible 32-bit floating-point number, or an infinite floating-point value if the range of Float32 is exceeded.

Splits the given float x into a significand/exponent pair (s, i) such that x = s * 2^i where s ∈ (-1;-0.5] ∪ [0.5; 1). Returns an undefined value if x is not finite.

This function does not reduce in the kernel. It is implemented in compiled code by the C function frexp.

Splits the given float x into a significand/exponent pair (s, i) such that x = s * 2^i where s ∈ (-1;-0.5] ∪ [0.5; 1). Returns an undefined value if x is not finite.

This function does not reduce in the kernel. It is implemented in compiled code by the C function frexp.

Checks whether two floating-point numbers are equal according to IEEE 754.

Floating-point equality does not correspond with propositional equality. In particular, it is not reflexive since NaN != NaN, and it is not a congruence because 0.0 == -0.0, but 1.0 / 0.0 != 1.0 / -0.0.

This function does not reduce in the kernel. It is compiled to the C equality operator.

Checks whether two floating-point numbers are equal according to IEEE 754.

Floating-point equality does not correspond with propositional equality. In particular, it is not reflexive since NaN != NaN, and it is not a congruence because 0.0 == -0.0, but 1.0 / 0.0 != 1.0 / -0.0.

This function does not reduce in the kernel. It is compiled to the C equality operator.

Adds two 64-bit floating-point numbers according to IEEE 754. Typically used via the + operator.

This function has a logical model in terms of Float.Model. It is compiled to the C addition operator.

Adds two 32-bit floating-point numbers according to IEEE 754. Typically used via the + operator.

This function has a logical model in terms of Float32.Model. It is compiled to the C addition operator.

Subtracts 64-bit floating-point numbers according to IEEE 754. Typically used via the - operator.

This function has a logical model in terms of Float.Model. It is compiled to the C subtraction operator.

Subtracts 32-bit floating-point numbers according to IEEE 754. Typically used via the - operator.

This function has a logical model in terms of Float32.Model. It is compiled to the C subtraction operator.

Multiplies 64-bit floating-point numbers according to IEEE 754. Typically used via the * operator.

This function has a logical model in terms of Float.Model. It is compiled to the C multiplication operator.

Multiplies 32-bit floating-point numbers according to IEEE 754. Typically used via the * operator.

This function has a logical model in terms of Float32.Model. It is compiled to the C multiplication operator.

Divides 64-bit floating-point numbers according to IEEE 754. Typically used via the / operator.

In Lean, division by zero typically yields zero. For Float, it instead yields either Inf, -Inf, or NaN.

This function has a logical model in terms of Float.Model. It is compiled to the C division operator.

Divides 32-bit floating-point numbers according to IEEE 754. Typically used via the / operator.

In Lean, division by zero typically yields zero. For Float32, it instead yields either Inf, -Inf, or NaN.

This function has a logical model in terms of Float32.Model. It is compiled to the C division operator.

Raises one floating-point number to the power of another. Typically used via the ^ operator.

This function does not reduce in the kernel. It is implemented in compiled code by the C function pow.

Raises one floating-point number to the power of another. Typically used via the ^ operator.

This function does not reduce in the kernel. It is implemented in compiled code by the C function powf.

Computes the exponential e^x of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function exp.

Computes the exponential e^x of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function expf.

Computes the base-2 exponential 2^x of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function exp2.

Computes the base-2 exponential 2^x of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function exp2f.

Computes the natural logarithm ln x of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function log.

Computes the natural logarithm ln x of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function logf.

Computes the base-10 logarithm of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function log10.

Computes the base-10 logarithm of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function log10f.

Computes the base-2 logarithm of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function log2.

Computes the base-2 logarithm of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function log2f.

Efficiently computes x * 2^i.

This function does not reduce in the kernel.

Efficiently computes x * 2^i.

This function does not reduce in the kernel.

Rounds to the nearest integer, rounding away from zero at half-way points.

This function does not reduce in the kernel. It is implemented in compiled code by the C function round.

Rounds to the nearest integer, rounding away from zero at half-way points.

This function does not reduce in the kernel. It is implemented in compiled code by the C function roundf.

Computes the floor of a floating-point number, which is the largest integer that's no larger than the given number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function floor.

Examples:

• Float.floor 1.5 = 1

• Float.floor (-1.5) = (-2)

Computes the floor of a floating-point number, which is the largest integer that's no larger than the given number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function floorf.

Examples:

• Float32.floor 1.5 = 1

• Float32.floor (-1.5) = (-2)

Computes the ceiling of a floating-point number, which is the smallest integer that's no smaller than the given number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function ceil.

Examples:

• Float.ceil 1.5 = 2

• Float.ceil (-1.5) = (-1)

Computes the ceiling of a floating-point number, which is the smallest integer that's no smaller than the given number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function ceilf.

Examples:

• Float32.ceil 1.5 = 2

• Float32.ceil (-1.5) = (-1)