def Miri.Interpreter.Math.unaryName : String → Option Unary

Equations

• Miri.Interpreter.Math.unaryName "sin" = some Miri.Interpreter.Math.Unary.sin
• Miri.Interpreter.Math.unaryName "cos" = some Miri.Interpreter.Math.Unary.cos
• Miri.Interpreter.Math.unaryName "exp" = some Miri.Interpreter.Math.Unary.exp
• Miri.Interpreter.Math.unaryName "exp2" = some Miri.Interpreter.Math.Unary.exp2
• Miri.Interpreter.Math.unaryName "log" = some Miri.Interpreter.Math.Unary.log
• Miri.Interpreter.Math.unaryName "log10" = some Miri.Interpreter.Math.Unary.log10
• Miri.Interpreter.Math.unaryName "log2" = some Miri.Interpreter.Math.Unary.log2
• Miri.Interpreter.Math.unaryName "cbrt" = some Miri.Interpreter.Math.Unary.cbrt
• Miri.Interpreter.Math.unaryName "cosh" = some Miri.Interpreter.Math.Unary.cosh
• Miri.Interpreter.Math.unaryName "sinh" = some Miri.Interpreter.Math.Unary.sinh
• Miri.Interpreter.Math.unaryName "tan" = some Miri.Interpreter.Math.Unary.tan
• Miri.Interpreter.Math.unaryName "tanh" = some Miri.Interpreter.Math.Unary.tanh
• Miri.Interpreter.Math.unaryName "acos" = some Miri.Interpreter.Math.Unary.acos
• Miri.Interpreter.Math.unaryName "asin" = some Miri.Interpreter.Math.Unary.asin
• Miri.Interpreter.Math.unaryName "atan" = some Miri.Interpreter.Math.Unary.atan
• Miri.Interpreter.Math.unaryName "acosh" = some Miri.Interpreter.Math.Unary.acosh
• Miri.Interpreter.Math.unaryName "asinh" = some Miri.Interpreter.Math.Unary.asinh
• Miri.Interpreter.Math.unaryName "log1p" = some Miri.Interpreter.Math.Unary.log1p
• Miri.Interpreter.Math.unaryName "expm1" = some Miri.Interpreter.Math.Unary.expm1
• Miri.Interpreter.Math.unaryName "tgamma" = some Miri.Interpreter.Math.Unary.tgamma
• Miri.Interpreter.Math.unaryName "erf" = some Miri.Interpreter.Math.Unary.erf
• Miri.Interpreter.Math.unaryName "erfc" = some Miri.Interpreter.Math.Unary.erfc
• Miri.Interpreter.Math.unaryName x✝ = none

def Miri.Interpreter.Math.runUnary {P S C V : Type} (h : Hooks P S C V) (choice : C) (name : String) (op : Unary) (value : FloatBits) : M S FloatBits

Equations

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

def Miri.Interpreter.Math.runBinary {P S C V : Type} (h : Hooks P S C V) (choice : C) (name : String) (op : Binary) (a b : FloatBits) (clampResult : Bool) : M S FloatBits

Equations

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

def Miri.Interpreter.Math.floatFastError {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (value : RvalueImmTy P) (bound : Nat) : M S (RvalueImmTy P)

Equations

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

def Miri.Interpreter.Math.evalIntrinsic {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (name : String) (generics : Array MIR.TyId) (args : Array (OpTy P)) (dest : V) : M S Bool

All remaining source math intrinsic arms. Host f128 preserves the pinned unimplemented arm; sqrtf128 uses the fully portable integer algorithm.

def Miri.Interpreter.Math.evalShim {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (name : String) (args : Array (OpTy P)) (dest : V) : M S Bool

Full shims/math.rs dispatch. Gamma's sign pointer is dereferenced before host evaluation and written before error perturbation/clamping/NaN choice.

Equations

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