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

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

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

Unpack a Float32.Model into the corresponding UnpackedFloat.

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.

def Float32.Model.nan : Model

The special NaN value.

def Float32.Model.inf : Model

The special Inf value.

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

Compute the sum of two Float32.Model.

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

Compute the difference of two Float32.Model.

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

Compute the product of two Float32.Model.

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

Compute the quotient of two Float32.Model.

@[instance_reducible]

instance Float32.Model.instAdd : Add Model

@[instance_reducible]

instance Float32.Model.instSub : Sub Model

@[instance_reducible]

instance Float32.Model.instMul : Mul Model

@[instance_reducible]

instance Float32.Model.instDiv : Div Model

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

Compute the square root of a Float32.Model.

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

Negate a Float32.Model.

@[instance_reducible]

instance Float32.Model.instNeg : Neg Model

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

Return a Float32.Model with positive sign.

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.

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.

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.

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.

@[instance_reducible]

instance Float32.Model.instLE : LE Model

@[instance_reducible]

instance Float32.Model.instDecidableLE : DecidableLE Model

@[instance_reducible]

instance Float32.Model.instLT : LT Model

@[instance_reducible]

instance Float32.Model.instDecidableLT : DecidableLT Model

@[instance_reducible]

instance Float32.Model.instBEq : BEq Model

@[instance_reducible]

instance Float32.Model.instMin : Min Model

@[instance_reducible]

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

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

Returns true if the float is positive or negative infinity.

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

Returns true if the float is NaN.

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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

Computes m * 10^e.

@[instance_reducible]

instance Float32.Model.instInhabited : Inhabited Model