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

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

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

Unpack a Float.Model into the corresponding UnpackedFloat.

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.

def Float.Model.nan : Model

The special NaN value.

def Float.Model.inf : Model

The special Inf value.

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

Compute the sum of two Float.Model.

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

Compute the difference of two Float.Model.

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

Compute the product of two Float.Model.

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

Compute the quotient of two Float.Model.

@[instance_reducible]

instance Float.Model.instAdd : Add Model

@[instance_reducible]

instance Float.Model.instSub : Sub Model

@[instance_reducible]

instance Float.Model.instMul : Mul Model

@[instance_reducible]

instance Float.Model.instDiv : Div Model

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

Compute the square root of a Float.Model.

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

Negate a Float.Model.

@[instance_reducible]

instance Float.Model.instNeg : Neg Model

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

Return a Float.Model with positive sign.

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.

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.

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.

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.

@[instance_reducible]

instance Float.Model.instLE : LE Model

@[instance_reducible]

instance Float.Model.instDecidableLE : DecidableLE Model

@[instance_reducible]

instance Float.Model.instLT : LT Model

@[instance_reducible]

instance Float.Model.instDecidableLT : DecidableLT Model

@[instance_reducible]

instance Float.Model.instBEq : BEq Model

@[instance_reducible]

instance Float.Model.instMin : Min Model

@[instance_reducible]

instance Float.Model.instMax : Max 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.

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

Returns true if the float is positive or negative infinity.

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

Returns true if the float is NaN.

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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

Computes m * 10^e.

@[instance_reducible]

instance Float.Model.instInhabited : Inhabited Model