Direct native production-effect construction. The source supervisor and interchange policy are actual NativeExecutor operations; only compiler queries, real library/backing operations and process-global observations are inputs.

structure Miri.Input.EvalNativeConstruction.Compiler (U C : Type) : Type

• typeShape : C → Interpreter.LocalLayout → Interpreter.NativeMachine.M Memory.MiriMemoryKind U Interpreter.Native.TypeShape
• layoutOf : C → MIR.TyId → Interpreter.NativeMachine.M Memory.MiriMemoryKind U (Except Unit Interpreter.LocalLayout)

structure Miri.Input.EvalNativeConstruction.Backing (U : Type) : Type

• address : Memory.AllocId → Interpreter.NativeMachine.Data → Interpreter.NativeMachine.M Memory.MiriMemoryKind U Nat
• expose : Memory.AllocId → Bool → Interpreter.NativeMachine.M Memory.MiriMemoryKind U Unit

structure Miri.Input.EvalNativeConstruction.IsolatedBacking (U : Type) : Type

Persistent source allocator access is supplied by the canonical backing owner. It must refer to the same store used by Allocation creation/drop; this record does not create a second AllocId/address registry.

• storage : Interpreter.NativeIsolatedAlloc.Access (Interpreter.NativeMachine.State Memory.MiriMemoryKind U)
• host : Interpreter.NativeAllocBytes.Host (Interpreter.NativeMachine.State Memory.MiriMemoryKind U)

def Miri.Input.EvalNativeConstruction.initializeIsolated {U : Type} (backing : IsolatedBacking U) : Interpreter.NativeMachine.M Memory.MiriMemoryKind U Unit

Equations

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

def Miri.Input.EvalNativeConstruction.isolatedFromBytes {U : Type} (backing : IsolatedBacking U) (bytes : Array UInt8) (align : Nat) : Interpreter.NativeMachine.M Memory.MiriMemoryKind U Interpreter.NativeAllocBytes.Buffer

Equations

• Miri.Input.EvalNativeConstruction.isolatedFromBytes backing bytes align = Miri.Interpreter.NativeAllocBytes.fromBytes backing.storage backing.host bytes align

def Miri.Input.EvalNativeConstruction.isolatedZeroed {U : Type} (backing : IsolatedBacking U) (size align : Nat) : Interpreter.NativeMachine.M Memory.MiriMemoryKind U Interpreter.NativeAllocBytes.Buffer

Equations

• Miri.Input.EvalNativeConstruction.isolatedZeroed backing size align = Miri.Interpreter.NativeAllocBytes.zeroed backing.storage backing.host size align

def Miri.Input.EvalNativeConstruction.isolatedDrop {U : Type} (backing : IsolatedBacking U) (buffer : Interpreter.NativeAllocBytes.Buffer) : Interpreter.NativeMachine.M Memory.MiriMemoryKind U Unit

Equations

• Miri.Input.EvalNativeConstruction.isolatedDrop backing buffer = Miri.Interpreter.NativeAllocBytes.release backing.storage backing.host buffer

def Miri.Input.EvalNativeConstruction.isolatedLifecycleBacking {U : Type} (backing : IsolatedBacking U) : Interpreter.NativeAllocationLifecycle.Backing (Interpreter.NativeMachine.State Memory.MiriMemoryKind U)

The lifecycle selects the actual source allocator before ID reservation.

Equations

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

def Miri.Input.EvalNativeConstruction.globalLifecycleBacking {U : Type} (host : Interpreter.NativeAllocBytes.GlobalHost (Interpreter.NativeMachine.State Memory.MiriMemoryKind U)) : Interpreter.NativeAllocationLifecycle.Backing (Interpreter.NativeMachine.State Memory.MiriMemoryKind U)

Equations

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

def Miri.Input.EvalNativeConstruction.ownedBacking {U : Type} (backing : Interpreter.NativeAllocationLifecycle.Backing (Interpreter.NativeMachine.State Memory.MiriMemoryKind U)) (expose : Memory.AllocId → Bool → Interpreter.NativeMachine.M Memory.MiriMemoryKind U Unit) : Backing U

Canonical native address consumes Allocation-owned backing. Interpreter byte writes are flushed into that same storage before native exposure; no allocation or second address registry is created during FFI preparation.

Equations

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

structure Miri.Input.EvalNativeConstruction.Process (U C : Type) : Type

• tracingEnabled : Interpreter.NativeMachine.State Memory.MiriMemoryKind U → Bool
• warningEmitted : Interpreter.NativeMachine.State Memory.MiriMemoryKind U → Bool
• setWarningEmitted : Interpreter.NativeMachine.State Memory.MiriMemoryKind U → Bool → Interpreter.NativeMachine.State Memory.MiriMemoryKind U
• diagnosticSharedMemory : C → Bool → Interpreter.NativeMachine.M Memory.MiriMemoryKind U Unit

def Miri.Input.EvalNativeConstruction.effects {U C N Code : Type} (hostBits : Nat) (compiler : Compiler U C) (backing : Backing U) (process : Process U C) (lookupSymbol : C → N → String → Interpreter.NativeMachine.M Memory.MiriMemoryKind U (Option (Interpreter.Native.SymbolInfo Code))) (executor : Interpreter.NativeExecutor.Hooks Memory.MiriMemoryKind U C Code) : EvalNativeMachine.Effects U C N Code

hostBits is the actual configured host usize width. Lookup operates on the actual World-loaded handle selected by EvalNativeMachine, retaining the source vector index even when library path strings repeat.

Equations

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