Initial compiler/image preparation for the canonical entry machine. The allocation import is deliberately not hidden in Except: failed registration retains the consumed allocation identities and successfully imported prefix.

structure Miri.Input.EvalPreparation.Prepared : Type

• compiler : CompilerProviders.Prepared
• image : AllocationImage.Imported
• types : RuntimeArrayTypes.World
• layouts : EvalEntryMachine.Layouts
• dummySpan : MIR.SpanRef

structure Miri.Input.EvalPreparation.Attempt : Type

• memory : Memory.MemoryState Memory.Provenance TreeBorrows.BorrowTree Memory.MiriMemoryKind
• outcome : Except String Prepared

def Miri.Input.EvalPreparation.prepareProfiled (profile : Lean.Options) (input : LoweredProgram) : Attempt

Compiler table preparation precedes allocation registration. All consumers share its final identity tables; graph definitions may not be appended only to an isolated image view. Primitive layouts and the persistent runtime type world are required evidence, never inferred from storage sizes.

Equations

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

def Miri.Input.EvalPreparation.prepare (input : LoweredProgram) : Attempt

Equations

• Miri.Input.EvalPreparation.prepare input = Miri.Input.EvalPreparation.prepareProfiled ∅ input

theorem Miri.Input.EvalPreparation.prepareProfiled_eq_prepare (profile : Lean.Options) (input : LoweredProgram) : prepareProfiled profile input = prepare input

Profiling only observes preparation boundaries and leaves every returned memory state and strict error unchanged.