Exact body-keyed compiler results for the source stack preamble. Failed normalization/evaluation is retained until the corresponding runtime event.

structure Miri.Input.CompilerLifecycle.Entry : Type

• preamble : Except String MIR.SpanRef
• callee : Except String Interpreter.CallInstance
• checks : Except String (Array (Except Interpreter.StepError Interpreter.CompilerConstantEvidence))

structure Miri.Input.CompilerLifecycle.Prepared : Type

• program : LoweredProgram
• entries : Array Entry

def Miri.Input.CompilerLifecycle.prepare (program : LoweredProgram) : Prepared

Equations

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

def Miri.Input.CompilerLifecycle.preambleSpan {K User : Type} (p : Prepared) (body : Interpreter.LoadedBody) : Interpreter.MachineHooks.M K User MIR.SpanRef

Equations

• Miri.Input.CompilerLifecycle.preambleSpan p body = Miri.Input.CompilerLifecycle.lift✝ do let __do_lift ← Miri.Input.CompilerLifecycle.entry✝ p body __do_lift.preamble

def Miri.Input.CompilerLifecycle.requiredConstants {K User : Type} (p : Prepared) (body : Interpreter.LoadedBody) : Interpreter.MachineHooks.M K User Unit

Equations

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

def Miri.Input.CompilerLifecycle.hooks {K User C : Type} (p : Prepared) (base : Interpreter.CallMachine.Lifecycle K User C) : Interpreter.CallMachine.Lifecycle K User C

Equations

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

theorem Miri.Input.CompilerLifecycle.preamble_known {K U : Type} (p : Prepared) (body : Interpreter.LoadedBody) (actual : LoweredBody) (span : MIR.SpanRef) (fnInstance : Interpreter.CallInstance) (row : p.program.bundle.bodies[body.identity.index]? = some actual) (contents : actual.body = body.body) (evidence : p.entries[body.identity.index]? = some { preamble := Except.ok span, callee := Except.ok fnInstance, checks := Except.ok #[] }) : preambleSpan p body = pure span

theorem Miri.Input.CompilerLifecycle.required_empty {K U : Type} (p : Prepared) (body : Interpreter.LoadedBody) (actual : LoweredBody) (span : MIR.SpanRef) (fnInstance : Interpreter.CallInstance) (row : p.program.bundle.bodies[body.identity.index]? = some actual) (contents : actual.body = body.body) (evidence : p.entries[body.identity.index]? = some { preamble := Except.ok span, callee := Except.ok fnInstance, checks := Except.ok #[] }) (frames : Array (Interpreter.Frame Memory.Provenance Interpreter.LocalLayout Interpreter.MachineHooks.FrameExtra)) (frame : Interpreter.Frame Memory.Provenance Interpreter.LocalLayout Interpreter.MachineHooks.FrameExtra) (machine : Interpreter.MachineHooks.MachineState K U) (identity : frame.bodyIdentity = body.identity) (function : frame.functionInstance = fnInstance) : requiredConstants p body { stack := { frames := frames.push frame }, machine := machine } = EStateM.Result.ok () { stack := { frames := frames.push frame }, machine := machine }