Source-owned execution configuration. Compiler/global-memory, platform and native numerical capabilities remain explicit. Callback capacity is an execution resource, not a safety guarantee.

@[reducible, inline]

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

Equations

• Miri.Input.EvalConfigurationCore.User = Miri.Input.EvalCoreMachine.User

@[reducible, inline]

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

Equations

• Miri.Input.EvalConfigurationCore.State = Miri.Input.EvalCoreMachine.State

@[reducible, inline]

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

Equations

• Miri.Input.EvalConfigurationCore.Stored = Miri.Input.EvalCoreMachine.Stored

@[reducible, inline]

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

Equations

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

structure Miri.Input.EvalConfigurationCore.PlaceOptions : Type

• debugAssertions : Bool
• dynamicFuel : Nat
• validation : Interpreter.ValidityMachine.ValidationMode

structure Miri.Input.EvalConfigurationCore.Options : Type

• place : PlaceOptions
• limits : Interpreter.ExecutionMachine.Limits
• compatibilityBudget : Nat
• varArgsBudget : Nat
• callbackCapacity : Nat
• floatNondeterministic : Bool
• weakFailureRate : UInt64
• crossCrateInlineAlways : Bool
• userRelevantCrates : Array Nat
• ignoreOptionalOverflowChecks : Bool
• panicUnwinds : Bool
• retag : CompilerRetagOptions.Options
• miriWriteRetryBudget : Nat

  Bound host write-all retries independently of guest string scans or ABI work. Exhaustion is an explicit resource outcome, never successful output.

structure Miri.Input.EvalConfigurationCore.Leaves (Os R P H D O Aff B Host C ClockHost : Type) : Type

Genuine residual effects and compiler queries. Physical reads/writes, local storage, retagging, calls/returns and every ordinary MIR operation are constructed below, rather than independently chosen callbacks.

• pointerSource : EvalPointerSource.Leaves Os R P H D O Aff B Host C
• sync : P → Concurrency.SyncObject.AccessKind → Interpreter.PlaceMachine.MachineM Memory.MiriMemoryKind (User Os R P H D O Aff B Host) Unit
• storage : ABI.Size → ABI.Align → Option (Array UInt8)
• spans : Interpreter.AllocationDriver.SpanHooks
• foreign : Option (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)
• dynSymName : O → String
• checkLlvmSymbolClash : String → M Os R P H D O Aff B Host Unit
• math : Option (EvalMathMachine.Host (State Os R P H D O Aff B Host) C)
• mathError : Interpreter.Math.ErrorMode
• control : EvalTerminatorMachine.ControlAccess Host ClockHost
• blockingSources : EvalTerminatorMachine.IoSourcesAccess Host

@[reducible, inline]

abbrev Miri.Input.EvalConfigurationCore.SourceOther (Raw Listener TcpStream Error : Type) : Type

Equations

• Miri.Input.EvalConfigurationCore.SourceOther Raw Listener TcpStream Error = Miri.Input.EvalUnixSourceConstruction.Other Raw Listener TcpStream Error

@[reducible, inline]

abbrev Miri.Input.EvalConfigurationCore.SourceHost (Poll Instant System H D Raw Listener TcpStream Error Native Profiler : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalConfigurationCore.SourceUser (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalConfigurationCore.SourceState (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalConfigurationCore.SourceControl (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

Equations

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

structure Miri.Input.EvalConfigurationCore.SourceLeaves (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path Place C ClockHost I AddrIter : Type) : Type 1

Source-route inputs for the specialized production Core path. Unlike the legacy Leaves, this record cannot carry a completed ForeignItems.Hooks; the ordered source resolver is constructed internally from foreignSource. The dimensions match EvalWorld's canonical Unix Other/Host payload exactly.

• hostConfiguration : HostRuntime.Configuration

  The actual runtime configuration selected by the source runner. Foreign callback and scheduler bindings project communication/host limits from this value; they do not choose an independent mode.

• nativeHost : Option (CompilerNativeSignatures.Host Memory.MiriMemoryKind (SourceControl Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C)
• nativeBackend : Option (EvalNativeSourceConstruction.RawHost (EvalNativeMachine.U Os R P H D (SourceOther Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler) C Native Nat)

  Actual native-call backend leaves. The semantic native-call pipeline is source-built; this optional record contains only real host operations.

• sync : P → Concurrency.SyncObject.AccessKind → Interpreter.PlaceMachine.MachineM Memory.MiriMemoryKind (SourceUser Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Unit
• storage : ABI.Size → ABI.Align → Option (Array UInt8)
• spans : Interpreter.AllocationDriver.SpanHooks
• foreignSource : EvalCallDispatchConstruction.SourceInput Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path AddrIter
• dynSymName : SourceOther Raw Listener TcpStream Error → String
• checkLlvmSymbolClash : String → Interpreter.MachineHooks.M Memory.MiriMemoryKind (SourceUser Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Unit
• math : Option (EvalMathMachine.Host (SourceState Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C)
• mathError : Interpreter.Math.ErrorMode
• control : EvalTerminatorMachine.ControlAccess (SourceHost Poll Instant System H D Raw Listener TcpStream Error Native Profiler) ClockHost
• blockingSources : EvalTerminatorMachine.IoSourcesAccess (SourceHost Poll Instant System H D Raw Listener TcpStream Error Native Profiler)

structure Miri.Input.EvalConfigurationCore.ForeignContext (Os R P H D O Aff B Host C ClockHost : Type) (Assembly : Type := Unit) : Type 1

• prepared : CompilerProviders.Prepared
• hostConfiguration : Option HostRuntime.Configuration
• sourceAssembly : Option (Unit → M Os R P H D O Aff B Host Assembly)

  Rebuild the source foreign assembly against the current live state. The same callable is installed as the Core foreign resolver and is exposed to startup/callback construction; it does not capture an initial-world copy.

• validityAccess : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (Stored Os R P H D O Aff B Host)
• validity : Interpreter.ValidityVisitor.Hooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra (Interpreter.FnVal O) (ABI.FnAbi MIR.TyId) Interpreter.ValidityMemory.PaddingHandle

  The exact visitor built from this configuration's retag/projection and source facts. Native calls reuse it rather than rebuilding weaker validation.

• access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (User 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)
• compiler : Interpreter.PlaceMachine.CompilerHooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) C
• dynamic : Interpreter.DynamicLayoutHooks Memory.Provenance (State Os R P H D O Aff B Host) C
• vtable : Interpreter.VTableHooks Memory.Provenance (State Os R P H D O Aff B Host) C (Interpreter.FnVal O) (ABI.FnAbi MIR.TyId)
• dynamicFuel : Nat
• atomics : Interpreter.AtomicAccessHooks Memory.Provenance (State Os R P H D O Aff B Host) C (Interpreter.RuntimePlace Memory.Provenance)
• 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)
• pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (Stored Os R P H D O Aff B Host))
• functions : Interpreter.FunctionPointers.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) O

  The exact per-world function registry used by MIR calls and source function-pointer resolution. Foreign source constructors consume this registry rather than rebuilding or snapshotting a separate one.

• threadFunctions : Unit → Except Interpreter.StepError (Interpreter.FunctionCalls.Hooks Memory.Provenance (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ExecutionStateTransport.Outer (EvalCoreMachine.World Os R P H D O Aff B Host))) C Interpreter.MachineHooks.FrameExtra O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId))

  Derived from this configuration and transported to the canonical outer thread state.

• spans : Interpreter.AllocationDriver.SpanHooks
• projection : Interpreter.PlaceProjectionHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra
• 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
• math : Interpreter.Math.Hooks Memory.Provenance (State Os R P H D O Aff B Host) C (Interpreter.RuntimePlace Memory.Provenance)

structure Miri.Input.EvalConfigurationCore.SourceCallbackProduct (Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C AddrIter : Type) : Type 1

Existential source callback package. The host timezone and timestamp representations are not part of EvalWorld, so a real time-shim dictionary is carried at the higher-universe factory boundary instead of being erased to Unit inside EStateM state.

• Zone : Type
• Timestamp : Type
• hooks : EvalCallbackMachine.Hooks Os R EvalSyncObjectAccess.Payload H D (SourceOther Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler C ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) self.Zone self.Timestamp Error EvalUnixFdConstruction.ArrayCursor Raw Listener TcpStream Error AddrIter
• main : Interpreter.MainMachine.Hooks (EvalCallbackMachine.ThreadUser Os R EvalSyncObjectAccess.Payload H D (SourceOther Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler) C (SourceOther Raw Listener TcpStream Error) ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff EvalSyncObjectAccess.Payload
• objects : Interpreter.ForeignSyncMachine.Objects (SourceState Os R EvalSyncObjectAccess.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)
• deadline : Interpreter.DeadlineMachine.Hooks Memory.MiriMemoryKind (EvalSyncMachine.User Os R EvalSyncObjectAccess.Payload H D (SourceOther Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler) Instant System
• time : Option (Interpreter.TimeShims.Hooks (SourceState Os R EvalSyncObjectAccess.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Instant System self.Zone self.Timestamp)

structure Miri.Input.EvalConfigurationCore.SourcePackage (Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path Place C ClockHost AddrIter : Type) : Type 1

Higher-universe source callback factory paired with the already-created configuration and canonical assembly. The builder consumes that exact assembly and execution config after Main and startup initialization exist; it does not rerun the source constructors or accept caller-built callbacks.

• execution : Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (SourceUser Os R EvalSyncObjectAccess.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C (SourceOther Raw Listener TcpStream Error) ABI.ExternAbi ClockHost
• panicUnwinds : Bool

  Panic behavior resolved from the compiler session that produced this source program. Source-backed call and catch-unwind hooks use this value; the low-level Options API remains caller-controlled.

• context : ForeignContext Os R EvalSyncObjectAccess.Payload H D (SourceOther Raw Listener TcpStream Error) Aff B (SourceHost Poll Instant System H D Raw Listener TcpStream Error Native Profiler) C ClockHost (EvalCallDispatchConstruction.SourceAssembly Os R EvalSyncObjectAccess.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C (EvalCallDispatchConstruction.SourceCallbackSeed Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path Place C (Interpreter.Clock.HostHooks Instant System (SourceState Os R EvalSyncObjectAccess.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) Interpreter.CallInstance AddrIter))
• callbackBuilder : EvalCallDispatchConstruction.SourceAssembly Os R EvalSyncObjectAccess.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C (EvalCallDispatchConstruction.SourceCallbackSeed Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path Place C (Interpreter.Clock.HostHooks Instant System (SourceState Os R EvalSyncObjectAccess.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) Interpreter.CallInstance AddrIter) → Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (SourceUser Os R EvalSyncObjectAccess.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C (SourceOther Raw Listener TcpStream Error) ABI.ExternAbi ClockHost → Interpreter.MainMachine.Hooks (EvalCallbackMachine.ThreadUser Os R EvalSyncObjectAccess.Payload H D (SourceOther Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler) C (SourceOther Raw Listener TcpStream Error) ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff EvalSyncObjectAccess.Payload → EvalCallbackMachine.State Os R EvalSyncObjectAccess.Payload H D (SourceOther Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler → Except (Interpreter.StepError × EvalCallbackMachine.State Os R EvalSyncObjectAccess.Payload H D (SourceOther Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler) (SourceCallbackProduct Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C AddrIter × EvalCallbackMachine.State Os R EvalSyncObjectAccess.Payload H D (SourceOther Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler)
• rebindCallbacks : SourceCallbackProduct Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C AddrIter → Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (SourceUser Os R EvalSyncObjectAccess.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C (SourceOther Raw Listener TcpStream Error) ABI.ExternAbi ClockHost → Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (SourceUser Os R EvalSyncObjectAccess.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C (SourceOther Raw Listener TcpStream Error) ABI.ExternAbi ClockHost

  Rebind a selected Core's foreign resolver to the callback router built from this same package. The resolver still constructs a fresh view of the live source assembly at each actual foreign call, then routes its IO through these canonical callback hooks.

def Miri.Input.EvalConfigurationCore.environmentMemoryFromCore {Os R P H D O Aff B Host C : Type} [DecidableEq Memory.MiriMemoryKind] (prepared : CompilerProviders.Prepared) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (User 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)) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (Stored Os R P H D O Aff B Host))) (spans : Interpreter.AllocationDriver.SpanHooks) (projection : Interpreter.PlaceProjectionHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) (choice : C) (alignment : Interpreter.ValidityMachine.AlignmentCheck) (stringScanBudget : Nat) : Except Interpreter.StepError (EvalHostRuntimeConstruction.EnvironmentMemory (Interpreter.ValidityMachine.Control (Stored Os R P H D O Aff B Host)) C P)

Build startup/foreign environment memory from the exact live Core fields. This deliberately lives below EvalSyncObjectConstruction: it avoids a module cycle and does not take a separately assembled execution Config or memory record. The returned state lens is the same EvalWorld runtime used by MIR.

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalConfigurationCore.ForeignBuilder (Os R P H D O Aff B Host C ClockHost Assembly : Type) : Type 1

Internal platform assembly edge. Production platform packages derive this builder from compiler facts and raw host leaves; this is not an input contract for client Rust safety claims.

Equations

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

def Miri.Input.EvalConfigurationCore.makeWithForeignContext {Os R P H D O Aff B Host C ClockHost Assembly : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (bytes : CompilerGlobalBytes.Prepared) (options : Options) (leaves : Leaves Os R P H D O Aff B Host C ClockHost) (choice : C) (sourceHostConfiguration : Option HostRuntime.Configuration) (foreignBuilder : Option (ForeignBuilder Os R P H D O Aff B Host C ClockHost Assembly)) : Nat → Except Interpreter.StepError (Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (User Os R P H D O Aff B Host) C O ABI.ExternAbi ClockHost × ForeignContext Os R P H D O Aff B Host C ClockHost Assembly)

Construct a fresh view of the same canonical state. The decreasing count is consumed only by synchronous visitor/helper/catch re-entry; exhaustion is an explicit runner resource result. Ordinary frame execution uses Step.step. Shared internal construction for source-owned platform packages retains the same live source assembly factory in startup and each recursive call.

Equations

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

The legacy generic entry retains its complete semantic-hook input. The production source entry below fixes the canonical Unix state dimensions and constructs the ordered foreign resolver internally.

def Miri.Input.EvalConfigurationCore.make {Os R P H D O Aff B Host C ClockHost : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (bytes : CompilerGlobalBytes.Prepared) (options : Options) (leaves : Leaves Os R P H D O Aff B Host C ClockHost) (choice : C) : Nat → Except Interpreter.StepError (Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (User Os R P H D O Aff B Host) C O ABI.ExternAbi ClockHost)

Equations

• Miri.Input.EvalConfigurationCore.make p image bytes options leaves choice = Miri.Input.EvalConfigurationCore.makeWithForeign✝ p image bytes options leaves choice none none

def Miri.Input.EvalConfigurationCore.makeFromSourcePackage {Os R H D B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path C ClockHost I AddrIter : Type} [DecidableEq Os] (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (bytes : CompilerGlobalBytes.Prepared) (options : Options) (sourceLeaves : SourceLeaves Os R EvalSyncObjectAccess.Payload H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path MIR.Place C ClockHost I AddrIter) (choice : C) : Nat → Except Interpreter.StepError (SourcePackage Os R H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path MIR.Place C ClockHost AddrIter)

Source-owned Core construction for the canonical Unix EvalWorld. This entry fixes the Other/Host state dimensions, derives native-library paths from the active HostRuntime, and internally constructs the ordered foreign factory from typed source components. There is no complete foreign-hook input.

Equations

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

def Miri.Input.EvalConfigurationCore.makeFromSource {Os R H D B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path C ClockHost I AddrIter : Type} [DecidableEq Os] (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (bytes : CompilerGlobalBytes.Prepared) (options : Options) (sourceLeaves : SourceLeaves Os R EvalSyncObjectAccess.Payload H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path MIR.Place C ClockHost I AddrIter) (choice : C) : Nat → Except Interpreter.StepError (Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (SourceUser Os R EvalSyncObjectAccess.Payload H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error) C (SourceOther Raw Listener TcpStream Error) ABI.ExternAbi ClockHost)

Compatibility projection for callers that need only the executable configuration. The production startup runner uses makeFromSourcePackage so it can build startup and callback adapters from the exact context paired with that configuration.

Equations

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

def Miri.Input.EvalConfigurationCore.validateInitialization {Os R P H D O Aff B Host C ClockHost : Type} (leaves : Leaves Os R P H D O Aff B Host C ClockHost) : M Os R P H D O Aff B Host Unit

Source initialization consistency belongs to runner input construction, not an additional Rust memory-operation check. Call after configuring actual native libraries/backend and before interpreting the first MIR step.

Equations

• Miri.Input.EvalConfigurationCore.validateInitialization leaves = Miri.Interpreter.NativeAllocationLifecycle.liftMachineAction (Miri.Input.EvalPointerSource.validateMode leaves.pointerSource)

def Miri.Input.EvalConfigurationCore.step {Os R P H D O Aff B Host C ClockHost : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (bytes : CompilerGlobalBytes.Prepared) (options : Options) (leaves : Leaves Os R P H D O Aff B Host C ClockHost) (choice : C) (state : Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ExecutionStateTransport.Outer (EvalWorld.World Os R P H D O Aff B Host))) : Interpreter.StepResult (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ExecutionStateTransport.Outer (EvalWorld.World Os R P H D O Aff B Host))) Bool

Ordinary exported MIR enters the same fixed small-step interpreter. Unknown compiler/host/backend effects and resource exhaustion remain error outcomes.

Equations

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

theorem Miri.Input.EvalConfigurationCore.make_eq_context {Os R P H D O Aff B Host C ClockHost : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (bytes : CompilerGlobalBytes.Prepared) (options : Options) (leaves : Leaves Os R P H D O Aff B Host C ClockHost) (choice : C) (capacity : Nat) : make p image bytes options leaves choice capacity = Except.map Prod.fst (makeWithForeignContext p image bytes options leaves choice none none capacity)

Public proof boundary for the canonical factory. Operational dictionaries remain exactly those assembled by makeWithForeignContext.

theorem Miri.Input.EvalConfigurationCore.pureQuery_eq {A : Type} (value : Except String A) : Miri.Input.EvalConfigurationCore.pureQuery✝ value = Except.mapError Interpreter.StepError.unsupported value

Reveal only the pure construction-error adapter to client proofs.

theorem Miri.Input.EvalConfigurationCore.liftConstruction_eq {A : Type} (value : Except Interpreter.StepError A) : Miri.Input.EvalConfigurationCore.liftConstruction✝ value = Except.map (fun (item : A) => { down := item }) value

Reveal only the universe lift used during factory construction.