Math construction on the canonical World. Host numerical operations and source C-signature checking remain genuine capabilities; every choice draw uses the single execution tape and every operand/store uses the MIR engine.

structure Miri.Input.EvalMathMachine.Host (S C : Type) : Type

• unary : C → Interpreter.Math.Unary → Interpreter.Math.HostBits → Interpreter.RvalueM S Interpreter.Math.HostBits
• binary : C → Interpreter.Math.Binary → Interpreter.Math.HostBits → Interpreter.Math.HostBits → Interpreter.RvalueM S Interpreter.Math.HostBits
• powi : C → Interpreter.Math.HostBits → Int32 → Interpreter.RvalueM S Interpreter.Math.HostBits
• lgamma : C → Interpreter.Math.HostBits → Interpreter.RvalueM S (Interpreter.Math.HostBits × Int32)

def Miri.Input.EvalMathMachine.optionalHost {S C : Type} (host : Option (Host S C)) : Host S C

Absence of actual numerical host operations is an explicit capability boundary at the call event, never a fabricated floating-point result.

Equations

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

def Miri.Input.EvalMathMachine.leaves {S C : Type} (tape : Interpreter.ExecutionChoices.Access S) (host : Host S C) (mode : Interpreter.Math.ErrorMode) (signature : C → String → Nat → Interpreter.RvalueM S Unit) : Interpreter.ExecutionMath.Leaves S C

Source random calls consume a new tape entry at the callback event, not one reused operation-wide index. Session error mode is an explicit real input.

Equations

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

def Miri.Input.EvalMathMachine.hooks {Os R P H D O Aff B WorldHost C : Type} (p : CompilerProviders.Prepared) (host : Host (EvalCoreMachine.State Os R P H D O Aff B WorldHost) C) (mode : Interpreter.Math.ErrorMode) (signature : Option (C → String → Nat → Interpreter.RvalueM (EvalCoreMachine.State Os R P H D O Aff B WorldHost) Unit)) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (EvalCoreMachine.Stored Os R P H D O Aff B WorldHost)) (place : Interpreter.PlaceHooks Memory.Provenance (EvalCoreMachine.State Os R P H D O Aff B WorldHost) C Interpreter.MachineHooks.FrameExtra) (scalar : Interpreter.ScalarOpsHooks Memory.Provenance (EvalCoreMachine.State Os R P H D O Aff B WorldHost) C) (floats : Interpreter.FloatOpsHooks Memory.Provenance (EvalCoreMachine.State Os R P H D O Aff B WorldHost) C) (returnToBlock : C → Option MIR.BasicBlockId → Interpreter.RvalueM (EvalCoreMachine.State Os R P H D O Aff B WorldHost) Unit) : Except Interpreter.StepError (Interpreter.Math.Hooks Memory.Provenance (EvalCoreMachine.State Os R P H D O Aff B WorldHost) C (Interpreter.RuntimePlace Memory.Provenance))

The i32 pointee identity comes from the compiler's exact primitive catalog. No guessed type ID, overwritten MathHooks baseline, or empty choice defaults.

Equations

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