Source construction for the portable Miri and backtrace extern families. The physical operations are projected from canonical machine state; the remaining fields are explicit host/compiler effects, never complete shim operation records supplied as opaque fallbacks.

@[reducible, inline]

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

Equations

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

Equations

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

Equations

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

Equations

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

Equations

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

@[reducible, inline]

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

Equations

• Miri.Input.EvalPortableForeignConstruction.EntryUser Os R P H D O Aff B Host = Miri.Interpreter.ValidityMachine.UserState (Miri.Input.EvalPortableForeignConstruction.World Os R P H D O Aff B Host)

@[reducible, inline]

abbrev Miri.Input.EvalPortableForeignConstruction.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.

structure Miri.Input.EvalPortableForeignConstruction.MiriEffects (Os R P H D O Aff B Host HostPath : Type) : Type

Host/source effects which have no canonical physical implementation in MiriShimMachine. stdout/stderr failures are interpreted by the caller using Miri's ignored-I/O-error policy; absence of a host implementation is an error.

• sourceAllocIdNumber : Option (Memory.AllocId → M Os R P H D O Aff B Host UInt64)

  Optional authoritative AllocId.0.get() evidence from the source compiler identity domain. This must not be reconstructed from the importer's dense runtime allocation IDs. When absent, miri_get_alloc_id remains an explicit Unsupported obligation after its source pointer checks.

• namePointer : Memory.Pointer (Option Memory.Provenance) → UInt8 → ByteArray → M Os R P H D O Aff B Host Unit
• printBorrowState : UInt64 → Bool → M Os R P H D O Aff B Host Unit
• checkNoIsolation : String → M Os R P H D O Aff B Host Unit
• readHostPath : Memory.Pointer (Option Memory.Provenance) → M Os R P H D O Aff B Host HostPath
• writeTargetPath : HostPath → Memory.Pointer (Option Memory.Provenance) → UInt64 → M Os R P H D O Aff B Host (Bool × UInt64)
• writeHost : Bool → ByteArray → M Os R P H D O Aff B Host Unit

def Miri.Input.EvalPortableForeignConstruction.miriCore {Os R P H D O Aff B Host C Other HostPath : Type} [DecidableEq Memory.MiriMemoryKind] (machine : Interpreter.MiriShimMachine.Hooks Memory.MiriMemoryKind (Control Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra Other) (choice : C) (thread : Interpreter.ThreadMachine.Hooks Memory.MiriMemoryKind (EntryUser Os R P H D O Aff B Host) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff) (unitLayout : M Os R P H D O Aff B Host Interpreter.LocalLayout) (reuseClock : Option Concurrency.VectorIdx) (effects : MiriEffects Os R P H D O Aff B Host HostPath) (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.MiriShims.CoreHooks Memory.Provenance (Interpreter.MiriShimMachine.State Memory.MiriMemoryKind (Control Os R P H D O Aff B Host)) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.RuntimePlace Memory.Provenance) Interpreter.LoadedBody Interpreter.CallInstance HostPath

Build the Miri-only operation record from canonical memory/provenance/GC and thread machines. The caller supplies only the true host, diagnostic, and selected-backend effects. Allocation, scalar access, byte slices, unwind, bookkeeping, yielding, and symbolic promises come from MiriShimMachine.core.

Equations

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

def Miri.Input.EvalPortableForeignConstruction.backtraceCore {Os R P H D O Aff B Host C : Type} [DecidableEq Memory.MiriMemoryKind] (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (EvalCoreMachine.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) (prepared : CompilerBacktraceSource.Prepared) (hostUsizeMax : Nat) (unitPointerLayout : M Os R P H D O Aff B Host Interpreter.LocalLayout) (misaligned : Memory.Pointer (Option Memory.Provenance) → ABI.Align → M Os R P H D O Aff B Host (Option Memory.Misalignment)) (functionPointer : Interpreter.CallInstance → M Os R P H D O Aff B Host (Memory.Pointer (Option Memory.Provenance))) (allocation : Memory.Pointer (Option Memory.Provenance) → M Os R P H D O Aff B Host (Memory.AllocId × ABI.Size)) (globalFunction : Memory.AllocId → M Os R P H D O Aff B Host (Option Interpreter.CallInstance)) (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

Construct the connected backtrace family with real machine stack and memory operations, exact compiler-exported hygiene/source-map queries, and canonical function allocation/global lookup capabilities.

Equations

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

def Miri.Input.EvalPortableForeignConstruction.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) (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)) (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)

Full portable order uses the source Miri family, then backtrace, then memory/string. This constructor cannot accept whole Miri or backtrace Hooks; their physical portions are built from the canonical source machines above.

Equations

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

def Miri.Input.EvalPortableForeignConstruction.portableOtherFromSource {Os R P H D O Aff B Host C Other HostPath : Type} [DecidableEq Memory.MiriMemoryKind] (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 (Control Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra Other) (choice : C) (thread : Interpreter.ThreadMachine.Hooks Memory.MiriMemoryKind (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 : MiriEffects Os R P H D O Aff B Host HostPath) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (EvalCoreMachine.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) (prepared : CompilerBacktraceSource.Prepared) (hostUsizeMax : Nat) (unitPointerLayout : M Os R P H D O Aff B Host Interpreter.LocalLayout) (misaligned : Memory.Pointer (Option Memory.Provenance) → ABI.Align → M Os R P H D O Aff B Host (Option Memory.Misalignment)) (functionPointer : Interpreter.CallInstance → M Os R P H D O Aff B Host (Memory.Pointer (Option Memory.Provenance))) (allocation : Memory.Pointer (Option Memory.Provenance) → M Os R P H D O Aff B Host (Memory.AllocId × ABI.Size)) (globalFunction : Memory.AllocId → M Os R P H D O Aff B Host (Option Interpreter.CallInstance)) (adtReprC : MIR.TyId → M Os R P H D O Aff B Host (Option Bool)) (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-family constructor: no complete Miri or backtrace Hooks record crosses this boundary. Their operations are derived here from canonical machine configurations and exact compiler source tables.

Equations

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