Physical source construction for Miri-only portable foreign operations. Memory, allocation identity, unwind, bookkeeping, and provenance collection are derived from the same live EvalWorld as execution. Host and diagnostic leaves remain in EvalMiriHostEffectsConstruction.

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

Equations

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

Equations

• Miri.Input.EvalMiriSourceConstruction.Control Os R P H D O Aff B Host = Miri.Interpreter.ValidityMachine.Control (Miri.Input.EvalMiriSourceConstruction.Stored Os R P H D O Aff B Host)

@[reducible, inline]

abbrev Miri.Input.EvalMiriSourceConstruction.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.EvalMiriSourceConstruction.fromContext [DecidableEq Memory.MiriMemoryKind] {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C ClockHost Assembly : Type} (options : EvalConfigurationCore.Options) (context : EvalConfigurationCore.ForeignContext Os R P H D (Other Raw Listener TcpStream Error) Aff B (Host Poll Instant System H D Raw Listener TcpStream Error Native Profiler) C ClockHost Assembly) : Interpreter.MiriShimMachine.Hooks Memory.MiriMemoryKind (Control Os R P H D (Other Raw Listener TcpStream Error) Aff B (Host Poll Instant System H D Raw Listener TcpStream Error Native Profiler)) C Interpreter.MachineHooks.FrameExtra (Other Raw Listener TcpStream Error)

Build physical Miri operations from the source-owned Core context. The source static-root list is the exact TLS leak-check list; tracked allocations use the persistent World set initialized from InitialMachine.Configuration. No complete Miri hooks or caller-selected bookkeeping callbacks cross this boundary.

Equations

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