Connect source-built physical Miri operations to a selected Core's portable foreign resolver. The Miri machine, thread machine, host capabilities, compiler queries, and environment memory all come from this exact source configuration and callback package.

@[reducible, inline]

abbrev Miri.Input.EvalMiriConnectedSourceConstruction.Other (Raw Listener TcpStream Error : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalMiriConnectedSourceConstruction.Host (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.EvalMiriConnectedSourceConstruction.User (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalMiriConnectedSourceConstruction.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.EvalMiriConnectedSourceConstruction.State (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalMiriConnectedSourceConstruction.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.EvalMiriConnectedSourceConstruction.World (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalMiriConnectedSourceConstruction.World Os R P H D O Aff B Host = Miri.Input.EvalWorld.World Os R P H D O Aff B Host

@[reducible, inline]

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

Equations

• Miri.Input.EvalMiriConnectedSourceConstruction.Stored Os R P H D O Aff B Host = Miri.Input.EvalCoreMachine.Stored Os R P H D O Aff B Host

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

def Miri.Input.EvalMiriConnectedSourceConstruction.bind [DecidableEq Memory.MiriMemoryKind] {Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path C ClockHost I AddrIter Assembly : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (options : EvalConfigurationCore.Options) (sourceLeaves : EvalConfigurationCore.SourceLeaves Os R EvalSyncObjectAccess.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path MIR.Place C ClockHost I AddrIter) (context : EvalConfigurationCore.ForeignContext Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Aff B (Host Poll Instant System H D Raw Listener TcpStream Error Native Profiler) C ClockHost Assembly) (thread : Interpreter.ThreadMachine.Hooks Memory.MiriMemoryKind (EntryUser Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Aff B (Host Poll Instant System H D Raw Listener TcpStream Error Native Profiler)) C (Other Raw Listener TcpStream Error) ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff) (foreign : Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Aff B (Host Poll Instant System H D Raw Listener TcpStream Error Native Profiler)) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.RuntimePlace Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Interpreter.LoadedBody Interpreter.CallInstance) : Except Interpreter.StepError (Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Aff B (Host Poll Instant System H D Raw Listener TcpStream Error Native Profiler)) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.RuntimePlace Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Interpreter.LoadedBody Interpreter.CallInstance)

Install Miri on the selected, already callback-rebound Core configuration. The supplied thread hooks are projected from the same source Main package; Miri spawn/join therefore share its actual TLS, scheduler, and return behavior.

Equations

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