def Float.Model.totalExponent (mantissa : Nat) (exponent : Int) : Int

The position of the most significant digit, where the unit digit corresponds to 1. So, for example, 1.0b has total exponent 1, 0.1b has total exponent 0, 0.01b has total exponent -1, and so on.

Equations

• Float.Model.totalExponent mantissa exponent = ↑mantissa.log2 + 1 + exponent

structure Float.Model.Format : Type

A floating point format is specified by two pieces of information: the number of bits in the mantissa, and the number of bits in the exponent.

• mantissaBitsWithoutImplicit : Nat

  The number of bits in the mantissa, excluding the implicit bit.

• hm : 0 < self.mantissaBitsWithoutImplicit
• exponentBits : Nat

  The number of bits in the exponent.

• he : 0 < self.exponentBits

@[reducible, inline]

abbrev Float.Model.Format.binary32 : Format

Specification corresponding to the IEEE binary32 format.

Equations

• Float.Model.Format.binary32 = { mantissaBitsWithoutImplicit := 23, hm := Float.Model.Format.binary32._proof_1, exponentBits := 8, he := Float.Model.Format.binary32._proof_2 }

@[reducible, inline]

abbrev Float.Model.Format.binary64 : Format

Specification corresponding to the IEEE binary64 format.

Equations

• Float.Model.Format.binary64 = { mantissaBitsWithoutImplicit := 52, hm := Float.Model.Format.binary64._proof_1, exponentBits := 11, he := Float.Model.Format.binary64._proof_2 }

@[reducible, inline]

abbrev Float.Model.Format.numBits (spec : Format) : Nat

The total number of bits in the packed representation.

Equations

• spec.numBits = 1 + spec.exponentBits + spec.mantissaBitsWithoutImplicit

def Float.Model.Format.mantissaBits (spec : Format) : Nat

The number of bits in the mantissa, including the implicit bit.

Equations

• spec.mantissaBits = 1 + spec.mantissaBitsWithoutImplicit

def Float.Model.Format.exponentBias (spec : Format) : Nat

The exponent bias. In packed formats, we store the sum of the true exponent and the bias.

Equations

• spec.exponentBias = 2 ^ (spec.exponentBits - 1) - 1

def Float.Model.Format.minExponent (spec : Format) : Int

The smallest exponent possible for a number using the given specification, including subnormals.

Equations

• spec.minExponent = 3 - 2 ^ (spec.exponentBits - 1) - ↑spec.mantissaBits

def Float.Model.Format.targetExponent (spec : Format) (totalExponent : Int) : Int

Suppose we have written a number where totalExponent is the position of the most significant digit, where the unit digit corresponds to 1. So, for example, 1.0b has total exponent 1, 0.1b has total exponent 0, 0.01b has total exponent -1, and so on. This function computes which exponent that number should have according to the given Format. So, for example, for the number 0.1b in binary64 format, it wants us to use the exponent -53, corresponding to the representation 2^52 * 2^(-53), which has a 53-bit mantissa. If the total exponent gets quite small, then the result exponent eventually gets capped at spec.minExponent, which first forces the result to be a subnormal number and then, if the total exponent is even smaller, to be zero.

Equations

• spec.targetExponent totalExponent = max (totalExponent - ↑spec.mantissaBits) spec.minExponent