Source-owned common foreign operations. This stage has no foreign/platform interpreter input and no allocator/read/write/control behavior supplied by the caller. Platform and portable dispatch assembly consumes this constructed record; it must not be substituted for a complete final foreign dictionary.

@[reducible, inline]

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

Equations

• Miri.Input.EvalForeignConstruction.User = Miri.Input.EvalCoreMachine.User

@[reducible, inline]

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

Equations

• Miri.Input.EvalForeignConstruction.State = Miri.Input.EvalCoreMachine.State

@[reducible, inline]

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

Equations

• Miri.Input.EvalForeignConstruction.Stored = Miri.Input.EvalCoreMachine.Stored

@[reducible, inline]

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

Equations

• Miri.Input.EvalForeignConstruction.M Os R P H D O Aff B Host A = Miri.Interpreter.MachineHooks.M Miri.Memory.MiriMemoryKind (Miri.Input.EvalForeignConstruction.User Os R P H D O Aff B Host) A

structure Miri.Input.EvalForeignConstruction.Options : Type

• family : Interpreter.ForeignItems.Family
• os : String
• arch : String
• noAllocShimSymbol : String
• compatibilityBudget : Nat
• debugAssertions : Bool

structure Miri.Input.EvalForeignConstruction.Symbols (S : Type) : Type

Exact compiler queries which are not yet in the prepared symbol catalog. Their outcomes are evidence obligations, not arbitrary foreign execution.

• allocatorSymbol : String → EStateM Interpreter.StepError S (Option (Interpreter.ForeignItems.AllocatorSymbol Interpreter.CallInstance))
• lookupFunction : String → EStateM Interpreter.StepError S (Option (Interpreter.LoadedBody × Interpreter.CallInstance))
• checkSymbolClash : String → EStateM Interpreter.StepError S Unit

structure Miri.Input.EvalForeignConstruction.HostEffects (S : Type) : Type

Genuine host FFI and OS-error effects. The native destination is known to be memory because source force_allocation has already run.

• nativeLibraryPaths : S → Array String
• callNative : String → Interpreter.MPlaceTy Memory.Provenance → Array (Interpreter.OpTy Memory.Provenance) → EStateM Interpreter.StepError S Bool
• setEnomem : EStateM Interpreter.StepError S Unit

structure Miri.Input.EvalForeignConstruction.Common (S : Type) : Type

Constructed common source bodies, deliberately without platform/portable execution slots. This is a source construction intermediate, not a whole ForeignItems.Hooks baseline that an external caller may override.

• options : Options
• maximumSize : UInt64
• symbols : Symbols S
• native : HostEffects S
• expectedAbi : Interpreter.ForeignItems.Signature → EStateM Interpreter.StepError S (ABI.FnAbi MIR.TyId)
• argumentCompat : ABI.ArgAbi MIR.TyId → ABI.ArgAbi MIR.TyId → EStateM Interpreter.StepError S Bool
• forceAllocation : Interpreter.RuntimePlace Memory.Provenance → EStateM Interpreter.StepError S (Interpreter.RuntimePlace Memory.Provenance)
• returnToBlock : Option MIR.BasicBlockId → EStateM Interpreter.StepError S Unit
• unwindToBlock : MIR.UnwindAction → EStateM Interpreter.StepError S Unit
• transmute : Interpreter.OpTy Memory.Provenance → Interpreter.LocalLayout → EStateM Interpreter.StepError S (Interpreter.OpTy Memory.Provenance)
• readUsize : Interpreter.OpTy Memory.Provenance → EStateM Interpreter.StepError S UInt64
• readU32 : Interpreter.OpTy Memory.Provenance → EStateM Interpreter.StepError S UInt32
• readPointer : Interpreter.OpTy Memory.Provenance → EStateM Interpreter.StepError S (Memory.Pointer (Option Memory.Provenance))
• readI32 : Interpreter.OpTy Memory.Provenance → EStateM Interpreter.StepError S Int32
• allocate : UInt64 → ABI.Align → Interpreter.ForeignItems.Init → Interpreter.ForeignItems.AllocationKind → EStateM Interpreter.StepError S (Memory.Pointer (Option Memory.Provenance))
• deallocate : Memory.Pointer (Option Memory.Provenance) → Option (UInt64 × ABI.Align) → Interpreter.ForeignItems.AllocationKind → EStateM Interpreter.StepError S Unit
• reallocate : Memory.Pointer (Option Memory.Provenance) → Option (UInt64 × ABI.Align) → UInt64 → ABI.Align → Interpreter.ForeignItems.AllocationKind → EStateM Interpreter.StepError S (Memory.Pointer (Option Memory.Provenance))
• writePointer : Memory.Pointer (Option Memory.Provenance) → Interpreter.RuntimePlace Memory.Provenance → EStateM Interpreter.StepError S Unit
• writeNull : Interpreter.RuntimePlace Memory.Provenance → EStateM Interpreter.StepError S Unit

def Miri.Input.EvalForeignConstruction.common {Os R P H D O Aff B Host C : Type} (p : CompilerProviders.Prepared) (options : Options) (symbols : Symbols (State Os R P H D O Aff B Host)) (host : HostEffects (State Os R P H D O Aff B Host)) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (Stored Os R P H D O Aff B Host)) (allocation : Interpreter.PlaceMachine.AllocationConfig Memory.MiriMemoryKind (User Os R P H D O Aff B Host)) (extras : Interpreter.MemoryExtras.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) P) (deallocationDiagnostic : Memory.AllocId → Interpreter.PlaceMachine.MachineM Memory.MiriMemoryKind (User Os R P H D O Aff B Host) Unit) (nativeDrop : Option (Memory.Allocation Memory.Provenance TreeBorrows.BorrowTree → Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D O Aff B Host) Unit)) (pointer : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (Stored Os R P H D O Aff B Host))) (spans : Interpreter.AllocationDriver.SpanHooks) (place : Interpreter.PlaceHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) (callFunction : C → Interpreter.CallInstance → Array (Interpreter.RvalueImmTy Memory.Provenance) → Interpreter.ReturnContinuation → M Os R P H D O Aff B Host Unit) (choice : C) : Except Interpreter.StepError (Common (State Os R P H D O Aff B Host))

The common interpreter is assembled from the same source allocation, place, ABI and pointer dictionaries as MIR execution. callFunction is the internal recursive edge supplied by source Config construction.

Equations

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

def Miri.Input.EvalForeignConstruction.core {Os R P H D O Aff B Host : Type} (h : Common (State Os R P H D O Aff B Host)) (spans : Interpreter.AllocationDriver.SpanHooks) : M Os R P H D O Aff B Host (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)

Project source-built primitives into the nonrecursive foreign Core. Exit replacement reads the actual World and needs only exact source span metadata; no whole MainMachine or platform interpreter is supplied. Native enablement is sampled from the actual loaded library list at this construction event.

Equations

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

def Miri.Input.EvalForeignConstruction.math {Os R P H D O Aff B Host C : Type} (h : Interpreter.Math.Hooks Memory.Provenance (State Os R P H D O Aff B Host) C (Interpreter.RuntimePlace Memory.Provenance)) (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) (choice : C) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (Interpreter.OpTy Memory.Provenance)) (dest : Interpreter.RuntimePlace Memory.Provenance) : M Os R P H D O Aff B Host Interpreter.ForeignItems.EmulateItemResult

math.rs uses sig.rs294–331's deprecated check for every exported arm. Capture this call's actual ABI, preserving symbol-clash before ABI/count checks; no expected ABI or scalar-layout compatibility check is added to this rule.

Equations

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

def Miri.Input.EvalForeignConstruction.memoryCore {Os R P H D O Aff B Host C : Type} (p : CompilerProviders.Prepared) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (Stored Os R P H D O Aff B Host)) (pointer : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (Stored Os R P H D O Aff B Host))) (place : Interpreter.PlaceHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) (symbolicAlignment enforceAlignment : Bool) (choice : C) (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.MemoryShims.CoreHooks Memory.Provenance (Interpreter.MemoryShimMachine.State Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (Stored Os R P H D O Aff B Host))) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.RuntimePlace Memory.Provenance) Interpreter.LoadedBody Interpreter.CallInstance

Portable memory/string operations consume only Core. Every byte access, write, copy and alignment check is constructed from actual MIR operations; libc::wchar_t remains an exact compiler query.

Equations

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

def Miri.Input.EvalForeignConstruction.bindMemory {Os R P H D O Aff B Host C : Type} (p : CompilerProviders.Prepared) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (Stored Os R P H D O Aff B Host)) (pointer : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (Stored Os R P H D O Aff B Host))) (place : Interpreter.PlaceHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) (symbolicAlignment enforceAlignment : Bool) (choice : C) (stringBudget : 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

Bind portable C memory/string calls to the same physical access, pointer and place machine as MIR. Other portable names retain their existing resolver. The memory dispatcher checks its source name table before reading operands.

Equations

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

def Miri.Input.EvalForeignConstruction.unixRandom {Os R P H D O Aff B Host C : Type} (h : Common (State Os R P H D O Aff B Host)) (spans : Interpreter.AllocationDriver.SpanHooks) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (User Os R P H D O Aff B Host)) (tape : Interpreter.ExecutionChoices.Access (State Os R P H D O Aff B Host)) (place : Interpreter.PlaceHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) (choice : C) (communicate : Bool) (hostUsizeBits : Nat) (hostFill : Nat → M Os R P H D O Aff B Host (Except String ByteArray)) (signature : String → M Os R P H D O Aff B Host (ABI.FnAbi MIR.TyId)) (errnoNegOne : String → Interpreter.MPlaceTy Memory.Provenance → M Os R P H D O Aff B Host Unit) : M Os R P H D O Aff B Host (String → ABI.FnAbi MIR.TyId → Array (Interpreter.OpTy Memory.Provenance) → Interpreter.RuntimePlace Memory.Provenance → M Os R P H D O Aff B Host Interpreter.ForeignItems.EmulateItemResult)

Construct the connected Unix entropy family from Common source effects. ForeignItems uses a typed RuntimePlace, while the Unix shim ABI writes through an allocated MPlaceTy. The adapter below materializes only at the source force-allocation boundary and routes every write back through Common's actual place operations. Isolated bytes use EvalCoreMachine's tape; communicate mode requires the caller's real host getrandom effect. The signature and errno providers are the pinned compiler and Unix environment queries respectively.

Equations

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

def Miri.Input.EvalForeignConstruction.windowsRandom {Os R P H D O Aff B Host C : Type} (h : Common (State Os R P H D O Aff B Host)) (spans : Interpreter.AllocationDriver.SpanHooks) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (User Os R P H D O Aff B Host)) (tape : Interpreter.ExecutionChoices.Access (State Os R P H D O Aff B Host)) (place : Interpreter.PlaceHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) (choice : C) (communicate : Bool) (hostUsizeBits : Nat) (hostFill : Nat → M Os R P H D O Aff B Host (Except String ByteArray)) (signature : String → M Os R P H D O Aff B Host (ABI.FnAbi MIR.TyId)) : M Os R P H D O Aff B Host (String → ABI.FnAbi MIR.TyId → Array (Interpreter.OpTy Memory.Provenance) → Interpreter.RuntimePlace Memory.Provenance → M Os R P H D O Aff B Host Interpreter.ForeignItems.EmulateItemResult)

Construct the Windows entropy family through the same Common runtime place materialization and canonical memory access as ordinary MIR. The host random fill and exact named System ABI are required effects; isolated bytes consume the shared source-choice tape.

Equations

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

def Miri.Input.EvalForeignConstruction.portableOther {Os R P H D O Aff B Host HostPath : Type} (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) (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) (miri : Interpreter.MiriShims.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 HostPath) (backtrace : 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) (adtReprC : MIR.TyId → M Os R P H D O Aff B Host (Option Bool)) : 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)

Source portable-extern order from shims/foreign_items.rs: Miri-specific, backtrace, then C memory/string arms. These three families all consume the same nonrecursive Core, so a portable shim observes the canonical state and ABI/pointer checks made by common construction. The compiler repr(C) query is kept lazy until miri_resolve_frame is selected.

Equations

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

def Miri.Input.EvalForeignConstruction.assemble {Os R P H D O Aff B Host : Type} (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) (math unix windows : String → ABI.FnAbi MIR.TyId → Array (Interpreter.OpTy Memory.Provenance) → Interpreter.RuntimePlace Memory.Provenance → M Os R P H D O Aff B Host Interpreter.ForeignItems.EmulateItemResult) (otherPortable : 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)) : 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

Close the source dispatcher only after each source family has been constructed. The platform functions are required values (not a copied baseline Hook record); callers must pass the actual Unix or Windows source dispatcher and exact math source.

Equations

• Miri.Input.EvalForeignConstruction.assemble foreign math unix windows otherPortable = { toCore := foreign, math := math, unix := unix, windows := windows, otherPortable := otherPortable }