Source-owned Math.Hooks construction. Pinned intrinsics/math.rs generic float selection and shims/math.rs lgamma{f,}_r sign-pointer/write_int operations use the same canonical scalar, pointer, typed-place and memory policies as MIR. Actual host numerical functions and session choices remain explicit leaves.

@[reducible, inline]

abbrev Miri.Interpreter.ExecutionMath.State (K User : Type) : Type

Equations

• Miri.Interpreter.ExecutionMath.State = Miri.Interpreter.ValidityMachine.State

@[reducible, inline]

abbrev Miri.Interpreter.ExecutionMath.M (K User A : Type) : Type

Equations

• Miri.Interpreter.ExecutionMath.M = Miri.Interpreter.ValidityMachine.M

structure Miri.Interpreter.ExecutionMath.Leaves (S C : Type) : Type

• checkCSignature : C → String → Nat → RvalueM S Unit
• hostUnary : C → Math.Unary → Math.HostBits → RvalueM S Math.HostBits
• hostBinary : C → Math.Binary → Math.HostBits → Math.HostBits → RvalueM S Math.HostBits
• hostPowi : C → Math.HostBits → Int32 → RvalueM S Math.HostBits
• hostLgamma : C → Math.HostBits → RvalueM S (Math.HostBits × Int32)
• errorMode : Math.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

def Miri.Interpreter.ExecutionMath.hooks {K U C : Type} [DecidableEq K] (leaves : Leaves (State K U) C) (access : ValidityMachine.Access K U) (place : PlaceHooks Memory.Provenance (State K U) C MachineHooks.FrameExtra) (scalar : ScalarOpsHooks Memory.Provenance (State K U) C) (floats : FloatOpsHooks Memory.Provenance (State K U) C) (i32Layout : LocalLayout) (returnToBlock : C → Option MIR.BasicBlockId → M K U Unit) : Math.Hooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)

Equations

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