structure Float32.Model : Type

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.

• toBits : UInt32

  The underlying bit pattern of the Float32.Model.

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

  The underlying bit pattern is valid according to the IEEE binary32 format.

@[instance_reducible]

instance Float32.instDecidableEqModel : DecidableEq Model

Equations

• Float32.instDecidableEqModel = Float32.instDecidableEqModel.decEq

def Float32.instDecidableEqModel.decEq (x✝ x✝¹ : Model) : Decidable (x✝ = x✝¹)

Equations

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

def Float32.Model.unpack (f : Model) : Float.Model.UnpackedFloat

Unpack a Float32.Model into the corresponding UnpackedFloat.

Equations

• f.unpack = Float.Model.UnpackedFloat.unpack Float.Model.Format.binary32 f.toBits.toBitVec

def Float32.Model.pack (f : Float.Model.UnpackedFloat) : Model

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.

Equations

• Float32.Model.pack f = { toBits := { toBitVec := Float.Model.UnpackedFloat.pack Float.Model.Format.binary32 f }, valid := ⋯ }

def Float32.Model.add (a b : Model) : Model

Compute the sum of two Float32.Model.

Equations

• a.add b = Float32.Model.pack (Float.Model.UnpackedFloat.add Float.Model.Format.binary32 a.unpack b.unpack)

def Float32.Model.sub (a b : Model) : Model

Compute the difference of two Float32.Model.

Equations

• a.sub b = Float32.Model.pack (Float.Model.UnpackedFloat.sub Float.Model.Format.binary32 a.unpack b.unpack)

def Float32.Model.mul (a b : Model) : Model

Compute the product of two Float32.Model.

Equations

• a.mul b = Float32.Model.pack (Float.Model.UnpackedFloat.mul Float.Model.Format.binary32 a.unpack b.unpack)

def Float32.Model.div (a b : Model) : Model

Compute the quotient of two Float32.Model.

Equations

• a.div b = Float32.Model.pack (Float.Model.UnpackedFloat.div Float.Model.Format.binary32 a.unpack b.unpack)

@[instance_reducible]

instance Float32.Model.instAdd : Add Model

Equations

• Float32.Model.instAdd = { add := fun (a b : Float32.Model) => a.add b }

@[instance_reducible]

instance Float32.Model.instSub : Sub Model

Equations

• Float32.Model.instSub = { sub := fun (a b : Float32.Model) => a.sub b }

@[instance_reducible]

instance Float32.Model.instMul : Mul Model

Equations

• Float32.Model.instMul = { mul := fun (a b : Float32.Model) => a.mul b }

@[instance_reducible]

instance Float32.Model.instDiv : Div Model

Equations

• Float32.Model.instDiv = { div := fun (a b : Float32.Model) => a.div b }

def Float32.Model.sqrt (a : Model) : Model

Compute the square root of a Float32.Model.

Equations

• a.sqrt = Float32.Model.pack (Float.Model.UnpackedFloat.sqrt Float.Model.Format.binary32 a.unpack)

def Float32.Model.neg (a : Model) : Model

Negate a Float32.Model.

Equations

• a.neg = Float32.Model.pack a.unpack.neg

@[instance_reducible]

instance Float32.Model.instNeg : Neg Model

Equations

• Float32.Model.instNeg = { neg := fun (a : Float32.Model) => a.neg }

def Float32.Model.abs (a : Model) : Model

Return a Float32.Model with positive sign.

Equations

• a.abs = Float32.Model.pack a.unpack.abs

def Float32.Model.compare (a b : Model) : Option Ordering

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

Equations

• a.compare b = a.unpack.compare b.unpack

def Float32.Model.le (a b : Model) : Bool

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

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

Equations

• a.le b = a.unpack.le b.unpack

def Float32.Model.lt (a b : Model) : Bool

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

This is not a total ordering.

Equations

• a.lt b = a.unpack.lt b.unpack

def Float32.Model.beq (a b : Model) : Bool

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

This is not a reflexive relation.

Equations

• a.beq b = a.unpack.beq b.unpack

@[instance_reducible]

instance Float32.Model.instLE : LE Model

Equations

• Float32.Model.instLE = { le := fun (a b : Float32.Model) => a.le b = true }

@[instance_reducible]

instance Float32.Model.instDecidableLE : DecidableLE Model

Equations

• a.instDecidableLE b = instDecidableEqBool (a.le b) true

@[instance_reducible]

instance Float32.Model.instLT : LT Model

Equations

• Float32.Model.instLT = { lt := fun (a b : Float32.Model) => a.lt b = true }

@[instance_reducible]

instance Float32.Model.instDecidableLT : DecidableLT Model

Equations

• a.instDecidableLT b = instDecidableEqBool (a.lt b) true

@[instance_reducible]

instance Float32.Model.instBEq : BEq Model

Equations

• Float32.Model.instBEq = { beq := fun (a b : Float32.Model) => a.beq b }

@[instance_reducible]

instance Float32.Model.instMin : Min Model

Equations

• Float32.Model.instMin = Min.leftLeaningOfLE Float32.Model

@[instance_reducible]

instance Float32.Model.instMax : Max Model

Equations

• Float32.Model.instMax = Max.leftLeaningOfLE Float32.Model

def Float32.Model.isFinite (a : Model) : Bool

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

Equations

• a.isFinite = a.unpack.isFinite

def Float32.Model.isInf (a : Model) : Bool

Returns true if the float is positive or negative infinity.

Equations

• a.isInf = a.unpack.isInf

def Float32.Model.isNaN (a : Model) : Bool

Returns true if the float is NaN.

Equations

• a.isNaN = a.unpack.isNaN

def Float32.Model.ofBits (a : UInt32) : Model

Construct a Float32.Model from its bit representation. This operation canonicalizes all NaN inputs into the canonical NaN.

Equations

• Float32.Model.ofBits a = Float32.Model.pack (Float.Model.UnpackedFloat.unpack Float.Model.Format.binary32 a.toBitVec)

def Float32.Model.ofInt (n : Int) : Model

Converts an Int to a Float32.Model, returning positive zero on zero.

Equations

• Float32.Model.ofInt n = Float32.Model.pack (Float.Model.UnpackedFloat.ofInt Float.Model.Format.binary32 n)

def Float32.Model.ofNat (n : Nat) : Model

Converts a Nat to a Float32.Model, returning positive zero on zero.

Equations

• Float32.Model.ofNat n = Float32.Model.pack (Float.Model.UnpackedFloat.ofNat Float.Model.Format.binary32 n)

def Float32.Model.ofUInt8 (n : UInt8) : Model

Converts a UInt8 to a Float32.Model, returning positive zero on zero.

Equations

• Float32.Model.ofUInt8 n = Float32.Model.pack (Float.Model.UnpackedFloat.ofUInt8 Float.Model.Format.binary32 n)

def Float32.Model.ofUInt16 (n : UInt16) : Model

Converts a UInt16 to a Float32.Model, returning positive zero on zero.

Equations

• Float32.Model.ofUInt16 n = Float32.Model.pack (Float.Model.UnpackedFloat.ofUInt16 Float.Model.Format.binary32 n)

def Float32.Model.ofUInt32 (n : UInt32) : Model

Converts a UInt32 to a Float32.Model, returning positive zero on zero.

Equations

• Float32.Model.ofUInt32 n = Float32.Model.pack (Float.Model.UnpackedFloat.ofUInt32 Float.Model.Format.binary32 n)

def Float32.Model.ofUInt64 (n : UInt64) : Model

Converts a UInt64 to a Float32.Model, returning positive zero on zero.

Equations

• Float32.Model.ofUInt64 n = Float32.Model.pack (Float.Model.UnpackedFloat.ofUInt64 Float.Model.Format.binary32 n)

def Float32.Model.ofUSize (n : USize) : Model

Converts a USize to a Float32.Model, returning positive zero on zero.

Equations

• Float32.Model.ofUSize n = Float32.Model.pack (Float.Model.UnpackedFloat.ofUSize Float.Model.Format.binary32 n)

def Float32.Model.ofInt8 (n : Int8) : Model

Converts an Int8 to a Float32.Model, returning positive zero on zero.

Equations

• Float32.Model.ofInt8 n = Float32.Model.pack (Float.Model.UnpackedFloat.ofInt8 Float.Model.Format.binary32 n)

def Float32.Model.ofInt16 (n : Int16) : Model

Converts an Int16 to a Float32.Model, returning positive zero on zero.

Equations

• Float32.Model.ofInt16 n = Float32.Model.pack (Float.Model.UnpackedFloat.ofInt16 Float.Model.Format.binary32 n)

def Float32.Model.ofInt32 (n : Int32) : Model

Converts an Int32 to a Float32.Model, returning positive zero on zero.

Equations

• Float32.Model.ofInt32 n = Float32.Model.pack (Float.Model.UnpackedFloat.ofInt32 Float.Model.Format.binary32 n)

def Float32.Model.ofInt64 (n : Int64) : Model

Converts an Int64 to a Float32.Model, returning positive zero on zero.

Equations

• Float32.Model.ofInt64 n = Float32.Model.pack (Float.Model.UnpackedFloat.ofInt64 Float.Model.Format.binary32 n)

def Float32.Model.ofISize (n : ISize) : Model

Converts an ISize to a Float32.Model, returning positive zero on zero.

Equations

• Float32.Model.ofISize n = Float32.Model.pack (Float.Model.UnpackedFloat.ofISize Float.Model.Format.binary32 n)

def Float32.Model.toUInt8 (f : Model) : UInt8

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

Equations

• f.toUInt8 = f.unpack.toUInt8

def Float32.Model.toUInt16 (f : Model) : UInt16

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

Equations

• f.toUInt16 = f.unpack.toUInt16

def Float32.Model.toUInt32 (f : Model) : UInt32

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

Equations

• f.toUInt32 = f.unpack.toUInt32

def Float32.Model.toUInt64 (f : Model) : UInt64

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

Equations

• f.toUInt64 = f.unpack.toUInt64

def Float32.Model.toUSize (f : Model) : USize

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

Equations

• f.toUSize = f.unpack.toUSize

def Float32.Model.toInt8 (f : Model) : Int8

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

Equations

• f.toInt8 = f.unpack.toInt8

def Float32.Model.toInt16 (f : Model) : Int16

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

Equations

• f.toInt16 = f.unpack.toInt16

def Float32.Model.toInt32 (f : Model) : Int32

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

Equations

• f.toInt32 = f.unpack.toInt32

def Float32.Model.toInt64 (f : Model) : Int64

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

Equations

• f.toInt64 = f.unpack.toInt64

def Float32.Model.toISize (f : Model) : ISize

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

Equations

• f.toISize = f.unpack.toISize

def Float32.Model.ofScientific (m : Nat) (e : Int) : Model

Computes m * 10^e.

Equations

• Float32.Model.ofScientific m e = Float32.Model.pack (Float.Model.UnpackedFloat.ofScientific Float.Model.Format.binary32 m e)

@[instance_reducible]

instance Float32.Model.instInhabited : Inhabited Model

Equations

• Float32.Model.instInhabited = { default := Float32.Model.ofNat 0 }