Final compiler/runtime binding for the portable foreign source family. This layer replaces caller-chosen symbol, function-pointer, allocation and backtrace-global callbacks with the prepared compiler tables and canonical runtime registries. True host effects and physical machine configurations remain explicit.

@[reducible, inline]

abbrev Miri.Input.EvalPortableForeignRuntime.User (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalPortableForeignRuntime.User Os R P H D O Aff B Host = Miri.Input.EvalCoreMachine.User Os R P H D O Aff B Host

@[reducible, inline]

abbrev Miri.Input.EvalPortableForeignRuntime.State (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalPortableForeignRuntime.State Os R P H D O Aff B Host = Miri.Input.EvalCoreMachine.State Os R P H D O Aff B Host

@[reducible, inline]

abbrev Miri.Input.EvalPortableForeignRuntime.M (Os R P H D O Aff B Host A : Type) : Type

Equations

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

def Miri.Input.EvalPortableForeignRuntime.prepareSymbols (providers : CompilerProviders.Prepared) : Except String CompilerForeignSymbols.Prepared

Equations

• Miri.Input.EvalPortableForeignRuntime.prepareSymbols providers = providers.foreignSymbols

def Miri.Input.EvalPortableForeignRuntime.sourceSymbols {Os R P H D O Aff B Host : Type} (providers : CompilerProviders.Prepared) (prepared : CompilerForeignSymbols.Prepared) : EvalForeignConstruction.Symbols (State Os R P H D O Aff B Host)

Equations

• Miri.Input.EvalPortableForeignRuntime.sourceSymbols providers prepared = Miri.Input.CompilerForeignSymbols.hooks prepared providers.lifecycle.calls

def Miri.Input.EvalPortableForeignRuntime.sourceOptions (prepared : CompilerForeignSymbols.Prepared) (options : EvalForeignConstruction.Options) : EvalForeignConstruction.Options

Equations

• Miri.Input.EvalPortableForeignRuntime.sourceOptions prepared options = Miri.Input.CompilerForeignSymbols.options prepared options

def Miri.Input.EvalPortableForeignRuntime.backtraceCore {Os R P H D O Aff B Host C : Type} [DecidableEq Memory.MiriMemoryKind] (providers : CompilerProviders.Prepared) (image : AllocationImage.Imported) (functionPointers : Interpreter.FunctionPointers.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) O) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (User Os R P H D O Aff B Host)) (arithmetic : Memory.PointerArithmetic) (projection : Interpreter.PlaceProjectionHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) (choice : C) (hostUsizeMax : Nat) (foreign : Interpreter.ForeignItems.Core Memory.Provenance (State Os R P H D O Aff B Host) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.RuntimePlace Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Interpreter.LoadedBody Interpreter.CallInstance) : Interpreter.Backtrace.CoreHooks Memory.Provenance (State Os R P H D O Aff B Host) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.RuntimePlace Memory.Provenance) Interpreter.LoadedBody Interpreter.CallInstance Interpreter.MachineHooks.FrameExtra CompilerBacktraceSource.Position

The actual backtrace source engine uses CompilerBacktraceSource.Prepared from the final provider pipeline, FunctionPointers for concrete function identity/address/provenance, PointerPlaceMachine for source misalignment, and the exact compiler unit-pointer layout query.

Equations

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

def Miri.Input.EvalPortableForeignRuntime.bindBacktrace {Os R P H D O Aff B Host C : Type} [DecidableEq Memory.MiriMemoryKind] (providers : CompilerProviders.Prepared) (image : AllocationImage.Imported) (functionPointers : Interpreter.FunctionPointers.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) O) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (User Os R P H D O Aff B Host)) (arithmetic : Memory.PointerArithmetic) (projection : Interpreter.PlaceProjectionHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) (choice : C) (hostUsizeMax : Nat) (foreign : Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R P H D O Aff B Host) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.RuntimePlace Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Interpreter.LoadedBody Interpreter.CallInstance) : Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R P H D O Aff B Host) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.RuntimePlace Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Interpreter.LoadedBody Interpreter.CallInstance

Attach the exact compiler-backed backtrace source family to an existing foreign resolver. Layout and source-map queries remain lazy until requested; other portable calls continue through the existing resolver.

Equations

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

def Miri.Input.EvalPortableForeignRuntime.portableOther {Os R P H D O Aff B Host C Other HostPath : Type} [DecidableEq Memory.MiriMemoryKind] (providers : CompilerProviders.Prepared) (symbols : CompilerForeignSymbols.Prepared) (image : AllocationImage.Imported) (foreign : Interpreter.ForeignItems.Core Memory.Provenance (State Os R P H D O Aff B Host) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.RuntimePlace Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Interpreter.LoadedBody Interpreter.CallInstance) (machine : Interpreter.MiriShimMachine.Hooks Memory.MiriMemoryKind (EvalPortableForeignConstruction.Control Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra Other) (choice : C) (thread : Interpreter.ThreadMachine.Hooks Memory.MiriMemoryKind (EvalPortableForeignConstruction.EntryUser Os R P H D O Aff B Host) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff) (unitLayout : Interpreter.LocalLayout) (reuseClock : Option Concurrency.VectorIdx) (effects : EvalPortableForeignConstruction.MiriEffects Os R P H D O Aff B Host HostPath) (functionPointers : Interpreter.FunctionPointers.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) O) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (User Os R P H D O Aff B Host)) (arithmetic : Memory.PointerArithmetic) (projection : Interpreter.PlaceProjectionHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) (hostUsizeMax : Nat) (memory : Interpreter.MemoryShims.CoreHooks Memory.Provenance (State Os R P H D O Aff B Host) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.RuntimePlace Memory.Provenance) Interpreter.LoadedBody Interpreter.CallInstance) (stringBudget : Nat) : String → ABI.FnAbi MIR.TyId → Array (Interpreter.OpTy Memory.Provenance) → Interpreter.RuntimePlace Memory.Provenance → M Os R P H D O Aff B Host (Option Interpreter.ForeignItems.EmulateItemResult)

Complete portable source family binding. Allocator identity, fallback function lookup and symbol-clash checks are compiler evidence; backtrace addresses and allocation identities are source machine registries. The only unbound external effects are the actual host/diagnostic effects in MiriEffects.

Equations

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