Actual compiler inlining attributes and imported GlobalAlloc::Function identity bridge. Exported compiler function reservations use CTFE_ALLOC_SALT=0.

structure Miri.Input.CompilerFunctionPointers.Prepared : Type

• calls : CompilerCallPipeline.Prepared
• inlineAttributes : Array (Interpreter.CallInstance × Bool)

@[reducible, inline]

abbrev Miri.Input.CompilerFunctionPointers.InlineIndex : Type

Equations

• Miri.Input.CompilerFunctionPointers.InlineIndex = Std.HashMap Nat (Array (Miri.Interpreter.CallInstance × Bool))

structure Miri.Input.CompilerFunctionPointers.InlineLookup (prepared : Prepared) : Type

• rows : Array (Miri.Interpreter.CallInstance × Bool)
• index : Miri.Input.CompilerFunctionPointers.InlineIndex
• exactRows : rows self = prepared.inlineAttributes

def Miri.Input.CompilerFunctionPointers.InlineLookup.prepare (prepared : Prepared) : InlineLookup prepared

Equations

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

def Miri.Input.CompilerFunctionPointers.inlineNeverUsing {prepared : Prepared} (lookup : InlineLookup prepared) (callee : Interpreter.CallInstance) : Option Bool

Equations

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

def Miri.Input.CompilerFunctionPointers.prepare (calls : CompilerCallPipeline.Prepared) : Except String Prepared

Equations

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

def Miri.Input.CompilerFunctionPointers.hooks {K User Other : Type} (p : Prepared) (image : AllocationImage.Imported) (base : Interpreter.FunctionPointers.Hooks K User Other) : Interpreter.FunctionPointers.Hooks K User Other

Equations

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

def Miri.Input.CompilerFunctionPointers.seedImportedProfiled {P E K Other : Type} (profile : Lean.Options) (p : Prepared) (image : AllocationImage.Imported) (memory : Memory.MemoryState P E K) (initial : Interpreter.FunctionPointers.Registry Other) : Except String (Interpreter.FunctionPointers.Registry Other)

Equations

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

def Miri.Input.CompilerFunctionPointers.seedImported {P E K Other : Type} (p : Prepared) (image : AllocationImage.Imported) (memory : Memory.MemoryState P E K) (initial : Interpreter.FunctionPointers.Registry Other) : Except String (Interpreter.FunctionPointers.Registry Other)

Equations

• Miri.Input.CompilerFunctionPointers.seedImported p image memory initial = Miri.Input.CompilerFunctionPointers.seedImportedProfiled ∅ p image memory initial

theorem Miri.Input.CompilerFunctionPointers.seedImported_profile_identity {P E K Other : Type} (p : Prepared) (image : AllocationImage.Imported) (memory : Memory.MemoryState P E K) (initial : Interpreter.FunctionPointers.Registry Other) : seedImported p image memory initial = seedImportedProfiled ∅ p image memory initial

def Miri.Input.CompilerFunctionPointers.attachProfiled {K User Other : Type} (profile : Lean.Options) (p : Prepared) (image : AllocationImage.Imported) (h : Interpreter.FunctionPointers.Hooks K User Other) : Interpreter.MachineHooks.M K User Unit

Attach the already imported compiler image before executing guest code. This installs source dedup identities, never allocation addresses or fake bytes.

Equations

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

def Miri.Input.CompilerFunctionPointers.attach {K User Other : Type} (p : Prepared) (image : AllocationImage.Imported) (h : Interpreter.FunctionPointers.Hooks K User Other) : Interpreter.MachineHooks.M K User Unit

Equations

• Miri.Input.CompilerFunctionPointers.attach p image h = Miri.Input.CompilerFunctionPointers.attachProfiled ∅ p image h

theorem Miri.Input.CompilerFunctionPointers.attach_profile_identity {K User Other : Type} (p : Prepared) (image : AllocationImage.Imported) (h : Interpreter.FunctionPointers.Hooks K User Other) : attach p image h = attachProfiled ∅ p image h

def Miri.Input.CompilerFunctionPointers.runtimeHooks {User Payload K Other : Type} (p : Prepared) (image : AllocationImage.Imported) (lens : Interpreter.FunctionPointers.AddressLens User Payload) (pointer : Interpreter.PointerMachine.Hooks K Payload) (choices : Memory.AllocId → Memory.AllocAddresses.AddressRandomChoices) (base : Interpreter.FunctionPointers.Hooks K User Other) : Interpreter.FunctionPointers.Hooks K User Other

Fully bind actual address operations and compiler function metadata under one lawful concrete user-state embedding. Choices are explicit semantic inputs.

Equations

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