Imported/dynamic symbolic vtables share canonical type/predicate identities and the same actual allocation/address engine. Compiler query leaves stay typed.

structure Miri.Input.CompilerVTableMachine.Prepared : Type

• calls : CompilerCallPipeline.Prepared
• queries : CompilerVTableQueries.Prepared

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

Equations

• Miri.Input.CompilerVTableMachine.prepare calls = do let __do_lift ← Miri.Input.CompilerVTableQueries.prepare calls.symbols.facts pure { calls := calls, queries := __do_lift }

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

def Miri.Input.CompilerVTableMachine.vtableHooks {K User Other C : Type} (p : Prepared) (image : AllocationImage.Imported) (h : Interpreter.VTableMachine.Hooks K User Other) (base : Interpreter.VTableHooks Memory.Provenance (Interpreter.MachineHooks.State K User) C Interpreter.CallInstance (ABI.FnAbi MIR.TyId)) : Interpreter.VTableHooks Memory.Provenance (Interpreter.MachineHooks.State K User) C Interpreter.CallInstance (ABI.FnAbi MIR.TyId)

Runtime symbolic maps must wrap the imported queries: reversing this order would lose freshly reserved function/vtable identities after successful casts.

Equations

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

def Miri.Input.CompilerVTableMachine.virtualHooks {K User Other C : Type} (p : Prepared) (image : AllocationImage.Imported) (h : Interpreter.VTableMachine.Hooks K User Other) (base : Interpreter.VirtualCalls.Hooks Memory.Provenance (Interpreter.MachineHooks.State K User) C Interpreter.MachineHooks.FrameExtra) : Interpreter.VirtualCalls.Hooks Memory.Provenance (Interpreter.MachineHooks.State K User) C Interpreter.MachineHooks.FrameExtra

Equations

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

def Miri.Input.CompilerVTableMachine.virtualLeaves {K User Other C : Type} (p : Prepared) (image : AllocationImage.Imported) (h : Interpreter.VTableMachine.Hooks K User Other) (base : Interpreter.ExecutionCallLeaves.Virtual K User C) : Interpreter.ExecutionCallLeaves.Virtual K User C

Production compiler/vtable leaves require no runtime-operation scaffold.

Equations

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

def Miri.Input.CompilerVTableMachine.callHooks {K User Other C Extern : Type} (p : Prepared) (image : AllocationImage.Imported) (h : Interpreter.VTableMachine.Hooks K User Other) (virtual : Interpreter.VirtualCalls.Hooks Memory.Provenance (Interpreter.MachineHooks.State K User) C Interpreter.MachineHooks.FrameExtra) (budget : Nat) (base : Interpreter.CallHooks Memory.Provenance (Interpreter.MachineHooks.State K User) C Interpreter.MachineHooks.FrameExtra Other Extern (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId)) : Interpreter.CallHooks Memory.Provenance (Interpreter.MachineHooks.State K User) C Interpreter.MachineHooks.FrameExtra Other Extern (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId)

Close virtual receiver/type selection, dynamic drop, caller location and actual function-pointer resolution on the canonical call state.

Equations

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

def Miri.Input.CompilerVTableMachine.castHooks {K User Other C D : Type} (p : Prepared) (image : AllocationImage.Imported) (h : Interpreter.VTableMachine.Hooks K User Other) (vtableBase : Interpreter.VTableHooks Memory.Provenance (Interpreter.MachineHooks.State K User) C Interpreter.CallInstance (ABI.FnAbi MIR.TyId)) (base : Interpreter.CastHooks Memory.Provenance (Interpreter.MachineHooks.State K User) C D) : Interpreter.CastHooks Memory.Provenance (Interpreter.MachineHooks.State K User) C D

Unsize/upcast casts create and inspect actual symbolic vtables and actual function pointers; compiler layout/type queries remain the source provider.

Equations

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

def Miri.Input.CompilerVTableMachine.validityHooks {K User Other C Pad : Type} (p : Prepared) (image : AllocationImage.Imported) (h : Interpreter.VTableMachine.Hooks K User Other) (vtableBase : Interpreter.VTableHooks Memory.Provenance (Interpreter.MachineHooks.State K User) C Interpreter.CallInstance (ABI.FnAbi MIR.TyId)) (base : Interpreter.ValidityVisitor.Hooks Memory.Provenance (Interpreter.MachineHooks.State K User) C Interpreter.MachineHooks.FrameExtra (Interpreter.FnVal Other) (ABI.FnAbi MIR.TyId) Pad) : Interpreter.ValidityVisitor.Hooks Memory.Provenance (Interpreter.MachineHooks.State K User) C Interpreter.MachineHooks.FrameExtra (Interpreter.FnVal Other) (ABI.FnAbi MIR.TyId) Pad

Validity preserves FnVal.Other for source get_ptr_fn checks while compiler virtual method entries retain full Instance identities.

Equations

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