Source math.rs portable bit operations and digit-by-digit square root. IEEE encodings/rational rounding use the existing exact FloatBits engine.

def Miri.Interpreter.Math.scalbn (value : FloatBits) (power : Int) : Except FloatError FloatBits

Equations

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

def Miri.Interpreter.Math.sqrt (value : FloatBits) : Except FloatError FloatBits

Source software square root: zero/NaN signs are preserved before the wrapper's separate NaN adjustment; finite values run the actual bit-by-bit loop.

Equations

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

def Miri.Interpreter.Math.isZero (value : FloatBits) : Except FloatError Bool

Equations

• Miri.Interpreter.Math.isZero value = do let __do_lift ← value.decode pure (match __do_lift.value with | Miri.Interpreter.FloatClass.finite n denominator => n == 0 | x => false)

def Miri.Interpreter.Math.isInfinite (value : FloatBits) : Except FloatError Bool

Equations

• Miri.Interpreter.Math.isInfinite value = do let __do_lift ← value.decode pure (match __do_lift.value with | Miri.Interpreter.FloatClass.infinite => true | x => false)

def Miri.Interpreter.Math.isFinite (value : FloatBits) : Except FloatError Bool

Equations

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

def Miri.Interpreter.Math.negative (value : FloatBits) : Except FloatError Bool

Equations

• Miri.Interpreter.Math.negative value = do let __do_lift ← value.decode pure __do_lift.negative

def Miri.Interpreter.Math.nextUp (value : FloatBits) : Except FloatError FloatBits

IEEE nextUp, including source signaling-NaN default result.

Equations

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

def Miri.Interpreter.Math.nextDown (value : FloatBits) : Except FloatError FloatBits

Equations

• Miri.Interpreter.Math.nextDown value = do let negated ← value.negate let __do_lift ← Miri.Interpreter.Math.nextUp negated __do_lift.negate

def Miri.Interpreter.Math.extremum (left right : FloatBits) (maximum : Bool) : Except FloatError FloatBits

Source rustc_apfloat maximum/minimum preserve the selected NaN payload, with -0 less than +0. NaN nondeterminism belongs to the outer machine wrapper.

Equations

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

def Miri.Interpreter.Math.pi (format : FloatFormat) : Except StepError FloatBits

Source uses these exact core float PI bit patterns, not a real-number π.

Equations

• Miri.Interpreter.Math.pi Miri.Interpreter.FloatFormat.binary16 = pure { format := Miri.Interpreter.FloatFormat.binary16, bits := 16968 }
• Miri.Interpreter.Math.pi Miri.Interpreter.FloatFormat.binary32 = pure { format := Miri.Interpreter.FloatFormat.binary32, bits := 1078530011 }
• Miri.Interpreter.Math.pi Miri.Interpreter.FloatFormat.binary64 = pure { format := Miri.Interpreter.FloatFormat.binary64, bits := 4614256656552045848 }
• Miri.Interpreter.Math.pi Miri.Interpreter.FloatFormat.binary128 = throw (Miri.Interpreter.StepError.unsupported "source host math f128 is unimplemented")

def Miri.Interpreter.Math.stripSuffix (name : String) : String

Equations

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