def Float.Model.UnpackedFloat.packComponents (spec : Format) (sign : Sign) (exponent : BitVec spec.exponentBits) (mantissa : BitVec spec.mantissaBitsWithoutImplicit) : BitVec spec.numBits

Creates a packed float from a sign, an exponent and a mantissa.

Equations

• Float.Model.UnpackedFloat.packComponents spec sign exponent mantissa = sign.toBitVec ++ exponent ++ mantissa

def Float.Model.UnpackedFloat.packedInfinity (spec : Format) (sign : Sign) : BitVec spec.numBits

Creates the packed signed infinity representation for the given specification.

Equations

• Float.Model.UnpackedFloat.packedInfinity spec sign = Float.Model.UnpackedFloat.packComponents spec sign (-1#spec.exponentBits) 0

def Float.Model.UnpackedFloat.packedNaN (spec : Format) : BitVec spec.numBits

Creates the canonical packed NaN for the given specification.

Equations

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

def Float.Model.UnpackedFloat.packedZero (spec : Format) (sign : Sign) : BitVec spec.numBits

Creates the packed signed zero representation for the given specification.

Equations

• Float.Model.UnpackedFloat.packedZero spec sign = Float.Model.UnpackedFloat.packComponents spec sign 0 0

def Float.Model.UnpackedFloat.pack (spec : Format) : UnpackedFloat → BitVec spec.numBits

Packs the given float into the format given by the specification.

This function assumes that the float is already correctly rounded for the given specification. This means that the exponent must be equal to the exponent computed by spec.targetExponent.

Equations

• One or more equations did not get rendered due to their size.
• Float.Model.UnpackedFloat.pack spec Float.Model.UnpackedFloat.notANumber = Float.Model.UnpackedFloat.packedNaN spec
• Float.Model.UnpackedFloat.pack spec (Float.Model.UnpackedFloat.infinity s) = Float.Model.UnpackedFloat.packedInfinity spec s
• Float.Model.UnpackedFloat.pack spec (Float.Model.UnpackedFloat.zero s) = Float.Model.UnpackedFloat.packedZero spec s

def Float.Model.UnpackedFloat.unpackMantissa {spec : Format} (b : BitVec spec.numBits) : BitVec spec.mantissaBitsWithoutImplicit

Unpacks the mantissa portion of the packed float. If this is a normal number, this will be missing the implicit bit.

Equations

• Float.Model.UnpackedFloat.unpackMantissa b = BitVec.cast ⋯ (BitVec.extractLsb (spec.mantissaBitsWithoutImplicit - 1) 0 b)

def Float.Model.UnpackedFloat.unpackExponent {spec : Format} (b : BitVec spec.numBits) : BitVec spec.exponentBits

Unpacks the exponent portion of the packed float.

Equations

• Float.Model.UnpackedFloat.unpackExponent b = BitVec.cast ⋯ (BitVec.extractLsb (spec.mantissaBitsWithoutImplicit + spec.exponentBits - 1) spec.mantissaBitsWithoutImplicit b)

def Float.Model.UnpackedFloat.unpackSign {spec : Format} (b : BitVec spec.numBits) : BitVec 1

Unpacks the sign bit of the packed float.

Equations

• Float.Model.UnpackedFloat.unpackSign b = BitVec.cast ⋯ (BitVec.extractLsb (spec.mantissaBitsWithoutImplicit + spec.exponentBits) (spec.mantissaBitsWithoutImplicit + spec.exponentBits) b)

def Float.Model.UnpackedFloat.unpack (spec : Format) (b : BitVec spec.numBits) : UnpackedFloat

Unpacks the given float according to the given specification.

The resulting float may be assumed to be correctly rounded for the given specification.

Equations

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