inductive Float.Model.UnpackedFloat.Accuracy : Type

Suppose given a real number x : ℝ with binary expansion x = ± x₀.x₁x₂x₃…. Truncating the expansion at some point gives an approximation of x as a floating-point number y. We can then ask how y is related to x. If y is exactly x, then we say that we are exact. Otherwise we are inexact, and y is slightly smaller than x, but x is also smaller than y + 1ulp. Together with the information that we are inexact, we store the information of where x is located relative to y + ½ulp. This is sufficient information for rounding y according to the various IEEE rounding rules.

• exact : Accuracy

  The approximation is exactly equal to the infinitely precise value.

• inexact (relativeToPlusOneHalfUlp : Ordering) : Accuracy

  The approximation is strictly smaller than the infinitely precise value, and the given Ordering describes the result of comparing the infinitely precise value and the approximation plus half a ulp.

def Float.Model.UnpackedFloat.Accuracy.roundToNearestEven (mantissa : Nat) : Accuracy → Nat

Rounds the given mantissa with the given accuracy according to the round-to-nearest strategy, with ties breaking in favor of even mantissas.

Equations

• Float.Model.UnpackedFloat.Accuracy.roundToNearestEven mantissa Float.Model.UnpackedFloat.Accuracy.exact = mantissa
• Float.Model.UnpackedFloat.Accuracy.roundToNearestEven mantissa (Float.Model.UnpackedFloat.Accuracy.inexact Ordering.lt) = mantissa
• Float.Model.UnpackedFloat.Accuracy.roundToNearestEven mantissa (Float.Model.UnpackedFloat.Accuracy.inexact Ordering.eq) = mantissa + mantissa % 2
• Float.Model.UnpackedFloat.Accuracy.roundToNearestEven mantissa (Float.Model.UnpackedFloat.Accuracy.inexact Ordering.gt) = mantissa + 1

structure Float.Model.UnpackedFloat.ExtendedMantissa : Type

Pairs a mantissa with two residual bits, the 'round bit' and the 'sticky bit', which carry precisely the required information to compute the Accuracy of the mantissa.

• mantissa : Nat

  The mantissa.

• roundBit : Bool

  The next bit after the least significant bit of the mantissa.

• stickyBit : Bool

  The bitwise or of all bits that are even less significant than the round bit.

def Float.Model.UnpackedFloat.ExtendedMantissa.accuracy : ExtendedMantissa → Accuracy

Extract the accuracy of the mantissa.

Equations

• { mantissa := mantissa, roundBit := false, stickyBit := false }.accuracy = Float.Model.UnpackedFloat.Accuracy.exact
• { mantissa := mantissa, roundBit := false, stickyBit := true }.accuracy = Float.Model.UnpackedFloat.Accuracy.inexact Ordering.lt
• { mantissa := mantissa, roundBit := true, stickyBit := false }.accuracy = Float.Model.UnpackedFloat.Accuracy.inexact Ordering.eq
• { mantissa := mantissa, roundBit := true, stickyBit := true }.accuracy = Float.Model.UnpackedFloat.Accuracy.inexact Ordering.gt

def Float.Model.UnpackedFloat.ExtendedMantissa.roundedMantissa (em : ExtendedMantissa) : Nat

Extracts the mantissa, rounded according to the data in the residual bits.

Equations

• em.roundedMantissa = Float.Model.UnpackedFloat.Accuracy.roundToNearestEven em.mantissa em.accuracy

def Float.Model.UnpackedFloat.ExtendedMantissa.ofMantissaAndAccuracy (mantissa : Nat) (accuracy : Accuracy) : ExtendedMantissa

Transforms a mantissa and an accuracy into an extended mantissa with the residual bits initialized to represent the given accuracy.

Equations

• One or more equations did not get rendered due to their size.
• Float.Model.UnpackedFloat.ExtendedMantissa.ofMantissaAndAccuracy mantissa Float.Model.UnpackedFloat.Accuracy.exact = { mantissa := mantissa, roundBit := false, stickyBit := false }

def Float.Model.UnpackedFloat.ExtendedMantissa.shiftRightOne (em : ExtendedMantissa) : ExtendedMantissa

Shift the mantissa right by one, propagating information into the residual bits as required.

Equations

• em.shiftRightOne = { mantissa := em.mantissa / 2, roundBit := em.mantissa % 2 != 0, stickyBit := em.roundBit || em.stickyBit }

@[instance_reducible]

instance Float.Model.UnpackedFloat.ExtendedMantissa.instHShiftRightNat : HShiftRight ExtendedMantissa Nat ExtendedMantissa

Equations

• One or more equations did not get rendered due to their size.

def Float.Model.UnpackedFloat.shiftToExponent (mantissa : Nat) (exponent : Int) (accuracy : Accuracy) (targetExponent : Int) : ExtendedMantissa × Int

Shifts the mantissa and exponent and initial accuracy to the target exponent, returning the new extended mantissa and exponent.

Important: this function will only drop bits from the mantissa and increase the exponent, not the other way around. The result will only conform to the given specification if the exponent was not too large to begin with. If this may be the case, you should call round instead.

Equations

• One or more equations did not get rendered due to their size.

def Float.Model.UnpackedFloat.shiftToTargetExponent (spec : Format) (mantissa : Nat) (exponent : Int) (accuracy : Accuracy) : ExtendedMantissa × Int

Computes the target exponent for the given mantissa and exponent and shifts the mantissa and exponent and initial accuracy to the target exponent, returning the new extended mantissa and exponent.

Important: this function will only drop bits from the mantissa and increase the exponent, not the other way around. The result will only conform to the given specification if the exponent was not too large to begin with. If this may be the case, you should call round instead.

Equations

• One or more equations did not get rendered due to their size.

def Float.Model.UnpackedFloat.roundWithAccuracy (spec : Format) (sign : Sign) (mantissa : Nat) (exponent : Int) (accuracy : Accuracy) : UnpackedFloat

Given a finite float represented by a sign, mantissa and exponent, together with an Accuracy datum, round it to conform to the given Format.

Important: this function will only drop bits from the mantissa and increase the exponent, not the other way around. The result will only conform to the given specification if the exponent was not too large to begin with. If this may be the case, you should call round instead.

Equations

• One or more equations did not get rendered due to their size.

def Float.Model.UnpackedFloat.decreaseExponent (mantissa : Nat) (exponent targetExponent : Int) : Nat × Int

If the target exponent is smaller than the given exponent, decreases the exponent of the mantissa to the target exponent; otherwise does nothing.

Equations

• Float.Model.UnpackedFloat.decreaseExponent mantissa exponent targetExponent = (mantissa <<< (exponent - targetExponent).toNat, exponent - ↑(exponent - targetExponent).toNat)

def Float.Model.UnpackedFloat.round (spec : Format) (sign : Sign) (mantissa : Nat) (exponent : Int) : UnpackedFloat

Given a finite float represented by a sign, mantissa and exponent, round it to conform to the given Format.

If necessary, this will both decrease and increase the exponent.

Equations

• One or more equations did not get rendered due to their size.

def Float.Model.UnpackedFloat.normalize (spec : Format) (mantissa exponent : Int) (zeroSign : Sign) : UnpackedFloat

Given a finite float represented as a signed mantissa and an exponent, round it to conform to the given Format.

If necessary, this will both decrease and increase the exponent.

Equations

• One or more equations did not get rendered due to their size.