structure Float.Model : Type

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.

• toBits : UInt64

  The underlying bit pattern of the Float.Model.

• valid : Format.binary64.Valid self.toBits.toBitVec

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

@[instance_reducible]

instance Float.instDecidableEqModel : DecidableEq Model

Equations

• Float.instDecidableEqModel = Float.instDecidableEqModel.decEq

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

Equations

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

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

Unpack a Float.Model into the corresponding UnpackedFloat.

Equations

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

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

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.

Equations

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

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

Compute the sum of two Float.Model.

Equations

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

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

Compute the difference of two Float.Model.

Equations

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

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

Compute the product of two Float.Model.

Equations

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

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

Compute the quotient of two Float.Model.

Equations

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

@[instance_reducible]

instance Float.Model.instAdd : Add Model

Equations

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

@[instance_reducible]

instance Float.Model.instSub : Sub Model

Equations

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

@[instance_reducible]

instance Float.Model.instMul : Mul Model

Equations

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

@[instance_reducible]

instance Float.Model.instDiv : Div Model

Equations

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

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

Compute the square root of a Float.Model.

Equations

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

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

Negate a Float.Model.

Equations

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

@[instance_reducible]

instance Float.Model.instNeg : Neg Model

Equations

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

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

Return a Float.Model with positive sign.

Equations

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

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

Compute the ordering between two Float.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 Float.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 Float.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 Float.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 Float.Model.instLE : LE Model

Equations

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

@[instance_reducible]

instance Float.Model.instDecidableLE : DecidableLE Model

Equations

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

@[instance_reducible]

instance Float.Model.instLT : LT Model

Equations

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

@[instance_reducible]

instance Float.Model.instDecidableLT : DecidableLT Model

Equations

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

@[instance_reducible]

instance Float.Model.instBEq : BEq Model

Equations

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

@[instance_reducible]

instance Float.Model.instMin : Min Model

Equations

• Float.Model.instMin = Min.leftLeaningOfLE Float.Model

@[instance_reducible]

instance Float.Model.instMax : Max Model

Equations

• Float.Model.instMax = Max.leftLeaningOfLE Float.Model

def Float.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 Float.Model.isInf (a : Model) : Bool

Returns true if the float is positive or negative infinity.

Equations

• a.isInf = a.unpack.isInf

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

Returns true if the float is NaN.

Equations

• a.isNaN = a.unpack.isNaN

def Float.Model.ofBits (a : UInt64) : Model

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

Converts a Float.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 Float.Model.toUInt16 (f : Model) : UInt16

Converts a Float.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 Float.Model.toUInt32 (f : Model) : UInt32

Converts a Float.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 Float.Model.toUInt64 (f : Model) : UInt64

Converts a Float.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 Float.Model.toUSize (f : Model) : USize

Converts a Float.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 Float.Model.toInt8 (f : Model) : Int8

Converts a Float.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 Float.Model.toInt16 (f : Model) : Int16

Converts a Float.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 Float.Model.toInt32 (f : Model) : Int32

Converts a Float.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 Float.Model.toInt64 (f : Model) : Int64

Converts a Float.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 Float.Model.toISize (f : Model) : ISize

Converts a Float.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 Float.Model.ofScientific (m : Nat) (e : Int) : Model

Computes m * 10^e.

Equations

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

@[instance_reducible]

instance Float.Model.instInhabited : Inhabited Model

Equations

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