inductive Miri.Interpreter.Math.ErrorMode : Type

• none : ErrorMode
• random : ErrorMode
• max : ErrorMode

@[instance_reducible]

instance Miri.Interpreter.Math.instDecidableEqErrorMode : DecidableEq ErrorMode

Equations

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

@[instance_reducible]

instance Miri.Interpreter.Math.instReprErrorMode : Repr ErrorMode

Equations

• Miri.Interpreter.Math.instReprErrorMode = { reprPrec := Miri.Interpreter.Math.instReprErrorMode.repr }

def Miri.Interpreter.Math.instReprErrorMode.repr : ErrorMode → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.Math.Unary : Type

• sin : Unary
• cos : Unary
• exp : Unary
• exp2 : Unary
• log : Unary
• log10 : Unary
• log2 : Unary
• cbrt : Unary
• cosh : Unary
• sinh : Unary
• tan : Unary
• tanh : Unary
• acos : Unary
• asin : Unary
• atan : Unary
• acosh : Unary
• asinh : Unary
• log1p : Unary
• expm1 : Unary
• tgamma : Unary
• erf : Unary
• erfc : Unary

@[instance_reducible]

instance Miri.Interpreter.Math.instDecidableEqUnary : DecidableEq Unary

Equations

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

def Miri.Interpreter.Math.instReprUnary.repr : Unary → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.Math.instReprUnary : Repr Unary

Equations

• Miri.Interpreter.Math.instReprUnary = { reprPrec := Miri.Interpreter.Math.instReprUnary.repr }

inductive Miri.Interpreter.Math.Binary : Type

• pow : Binary
• hypot : Binary
• atan2 : Binary
• fdim : Binary

@[instance_reducible]

instance Miri.Interpreter.Math.instDecidableEqBinary : DecidableEq Binary

Equations

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

def Miri.Interpreter.Math.instReprBinary.repr : Binary → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.Math.instReprBinary : Repr Binary

Equations

• Miri.Interpreter.Math.instReprBinary = { reprPrec := Miri.Interpreter.Math.instReprBinary.repr }

inductive Miri.Interpreter.Math.HostBits : Type

Actual host f16/f32/f64 bit representations; conversion is bit identity, never an intermediate Lean Float or an implicit promotion to binary64.

• half (bits : BitVec 16) : HostBits
• single (bits : BitVec 32) : HostBits
• double (bits : BitVec 64) : HostBits

def Miri.Interpreter.Math.instDecidableEqHostBits.decEq (x✝ x✝¹ : HostBits) : Decidable (x✝ = x✝¹)

Equations

• Miri.Interpreter.Math.instDecidableEqHostBits.decEq (Miri.Interpreter.Math.HostBits.half a) (Miri.Interpreter.Math.HostBits.half b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.Math.instDecidableEqHostBits.decEq (Miri.Interpreter.Math.HostBits.half bits) (Miri.Interpreter.Math.HostBits.single bits_1) = isFalse ⋯
• Miri.Interpreter.Math.instDecidableEqHostBits.decEq (Miri.Interpreter.Math.HostBits.half bits) (Miri.Interpreter.Math.HostBits.double bits_1) = isFalse ⋯
• Miri.Interpreter.Math.instDecidableEqHostBits.decEq (Miri.Interpreter.Math.HostBits.single bits) (Miri.Interpreter.Math.HostBits.half bits_1) = isFalse ⋯
• Miri.Interpreter.Math.instDecidableEqHostBits.decEq (Miri.Interpreter.Math.HostBits.single a) (Miri.Interpreter.Math.HostBits.single b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.Math.instDecidableEqHostBits.decEq (Miri.Interpreter.Math.HostBits.single bits) (Miri.Interpreter.Math.HostBits.double bits_1) = isFalse ⋯
• Miri.Interpreter.Math.instDecidableEqHostBits.decEq (Miri.Interpreter.Math.HostBits.double bits) (Miri.Interpreter.Math.HostBits.half bits_1) = isFalse ⋯
• Miri.Interpreter.Math.instDecidableEqHostBits.decEq (Miri.Interpreter.Math.HostBits.double bits) (Miri.Interpreter.Math.HostBits.single bits_1) = isFalse ⋯
• Miri.Interpreter.Math.instDecidableEqHostBits.decEq (Miri.Interpreter.Math.HostBits.double a) (Miri.Interpreter.Math.HostBits.double b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.Math.instDecidableEqHostBits : DecidableEq HostBits

Equations

• Miri.Interpreter.Math.instDecidableEqHostBits = Miri.Interpreter.Math.instDecidableEqHostBits.decEq

def Miri.Interpreter.Math.instReprHostBits.repr : HostBits → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.Math.instReprHostBits : Repr HostBits

Equations

• Miri.Interpreter.Math.instReprHostBits = { reprPrec := Miri.Interpreter.Math.instReprHostBits.repr }

def Miri.Interpreter.Math.HostBits.toSoft : HostBits → FloatBits

Equations

• (Miri.Interpreter.Math.HostBits.half a).toSoft = { format := Miri.Interpreter.FloatFormat.binary16, bits := BitVec.ofNat 128 a.toNat }
• (Miri.Interpreter.Math.HostBits.single a).toSoft = { format := Miri.Interpreter.FloatFormat.binary32, bits := BitVec.ofNat 128 a.toNat }
• (Miri.Interpreter.Math.HostBits.double a).toSoft = { format := Miri.Interpreter.FloatFormat.binary64, bits := BitVec.ofNat 128 a.toNat }

def Miri.Interpreter.Math.toHost (value : FloatBits) : Except StepError HostBits

Equations

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

structure Miri.Interpreter.Math.Hooks (P S C V : Type) : Type

• floatOps : FloatOpsHooks P S C
• scalarOps : ScalarOpsHooks P S C
• readImmediate : C → OpTy P → RvalueM S (RvalueImmTy P)
• writeImmediate : C → Immediate P → V → RvalueM S Unit
• destLayout : V → ABI.TyAndLayout MIR.TyId
• genericFloat : C → Array MIR.TyId → RvalueM S FloatFormat
• checkCSignature : C → String → Nat → RvalueM S Unit

  Source C ABI/deprecated shim argument check; compiler call ABI retained.

• derefI32 : C → OpTy P → RvalueM S V
• writeI32 : C → Int32 → V → RvalueM S Unit
• hostUnary : C → Unary → HostBits → RvalueM S HostBits
• hostBinary : C → Binary → HostBits → HostBits → RvalueM S HostBits
• hostPowi : C → HostBits → Int32 → RvalueM S HostBits
• hostLgamma : C → HostBits → RvalueM S (HostBits × Int32)
• errorMode : ErrorMode
• ulpError : C → Nat → RvalueM S Int
• maxErrorPositive : C → RvalueM S Bool
• relativeMagnitude : C → Nat → RvalueM S Nat
• relativeNegative : C → RvalueM S Bool
• snanPowNaN : C → RvalueM S Bool
• returnToBlock : C → Option MIR.BasicBlockId → RvalueM S Unit

@[reducible, inline]

abbrev Miri.Interpreter.Math.M (S A : Type) : Type

Equations

• Miri.Interpreter.Math.M S A = Miri.Interpreter.RvalueM S A

def Miri.Interpreter.Math.liftResult {A S : Type} (result : Except StepError A) : M S A

Equations

• Miri.Interpreter.Math.liftResult (Except.ok value) = pure value
• Miri.Interpreter.Math.liftResult (Except.error error) = throw error

def Miri.Interpreter.Math.engine {A S : Type} (result : Except FloatError A) : M S A

Equations

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

def Miri.Interpreter.Math.invalid {S A : Type} (message : String) : M S A

Equations

• Miri.Interpreter.Math.invalid message = throw (Miri.Interpreter.StepError.invalidProgram message)

def Miri.Interpreter.Math.scalarResult {A S : Type} (result : Except Memory.ScalarError A) : M S A

Equations

• Miri.Interpreter.Math.scalarResult result = Miri.Interpreter.Math.liftResult (Except.mapError Miri.Interpreter.ScalarOps.scalarError result)

def Miri.Interpreter.Math.arity {P S : Type} (args : Array (OpTy P)) (count : Nat) : M S Unit

Equations

• Miri.Interpreter.Math.arity args count = if (args.size == count) = true then pure () else throw (Miri.Interpreter.StepError.undefinedBehavior "incorrect number of arguments for intrinsic")

def Miri.Interpreter.Math.arg {P S : Type} (args : Array (OpTy P)) (i : Nat) : M S (OpTy P)

Equations

• Miri.Interpreter.Math.arg args i = match args[i]? with | some op => pure op | none => Miri.Interpreter.Math.invalid "math argument missing"

def Miri.Interpreter.Math.readScalar {P S C V : Type} (h : Hooks P S C V) (choice : C) (op : OpTy P) : M S (Memory.Scalar P)

Equations

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

def Miri.Interpreter.Math.readFloat {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (op : OpTy P) (format : FloatFormat) : M S FloatBits

Equations

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

def Miri.Interpreter.Math.writeFloat {P S C V : Type} (h : Hooks P S C V) (choice : C) (value : FloatBits) (dest : V) : M S Unit

Equations

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

def Miri.Interpreter.Math.hostResult {S : Type} (expected : FloatFormat) (result : HostBits) : M S FloatBits

Equations

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

def Miri.Interpreter.Math.applyUlpError {P S C V : Type} (h : Hooks P S C V) (choice : C) (value : FloatBits) (bound : Nat) : M S FloatBits

Equations

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

def Miri.Interpreter.Math.applyRelativeError {P S C V : Type} (h : Hooks P S C V) (choice : C) (value : FloatBits) (scale : Int32) : M S FloatBits

Equations

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