Portable scalar float helpers from pinned interpret/intrinsics.rs. Finite FMA computes the exact product-plus-addend before its single rounding.

inductive Miri.Interpreter.FloatIntegralRound : Type

• floor : FloatIntegralRound
• ceil : FloatIntegralRound
• trunc : FloatIntegralRound
• away : FloatIntegralRound
• even : FloatIntegralRound

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqFloatIntegralRound : DecidableEq FloatIntegralRound

Equations

• Miri.Interpreter.instDecidableEqFloatIntegralRound x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instReprFloatIntegralRound : Repr FloatIntegralRound

Equations

• Miri.Interpreter.instReprFloatIntegralRound = { reprPrec := Miri.Interpreter.instReprFloatIntegralRound.repr }

def Miri.Interpreter.instReprFloatIntegralRound.repr : FloatIntegralRound → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.FloatMinMax : Type

• minimum : FloatMinMax
• maximum : FloatMinMax
• minimumNumber : FloatMinMax
• maximumNumber : FloatMinMax

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqFloatMinMax : DecidableEq FloatMinMax

Equations

• Miri.Interpreter.instDecidableEqFloatMinMax x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instReprFloatMinMax : Repr FloatMinMax

Equations

• Miri.Interpreter.instReprFloatMinMax = { reprPrec := Miri.Interpreter.instReprFloatMinMax.repr }

def Miri.Interpreter.instReprFloatMinMax.repr : FloatMinMax → Nat → Std.Format

Equations

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

def Miri.Interpreter.IntrinsicFloat.abs (value : FloatBits) : Except FloatError FloatBits

Equations

• Miri.Interpreter.IntrinsicFloat.abs value = do let _ ← value.decode pure { format := value.format, bits := BitVec.ofNat 128 (BitVec.toNat value.bits % 2 ^ (value.format.width - 1)) }

def Miri.Interpreter.IntrinsicFloat.copySign (left right : FloatBits) : Except FloatError FloatBits

Equations

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

def Miri.Interpreter.IntrinsicFloat.roundIntegral (value : FloatBits) (mode : FloatIntegralRound) : Except FloatError FloatBits

Equations

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

def Miri.Interpreter.IntrinsicFloat.minMax (left right : FloatBits) (op : FloatMinMax) (chooseRightEqual : Bool) : Except FloatError FloatBits

Equations

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

def Miri.Interpreter.IntrinsicFloat.fusedMulAdd (a b c : FloatBits) : Except FloatError FloatBits

Equations

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

def Miri.Interpreter.IntrinsicFloat.toIntegerChecked (value : FloatBits) (width : Nat) (isSigned : Bool) : Except FloatError (Option Int)

Checked float-to-int before source saturation: compare the truncated exact integer against bounds; NaNs and infinities cannot be represented.

Equations

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