Source memory.rs fn_ptr/get_fn_alloc/get_ptr_fn and machine.rs salt/root provenance. Function identities are full instances, never numeric addresses.

structure Miri.Interpreter.FunctionPointers.FunctionEntry : Type

• callee : CallInstance
• salt : Fin 32
• allocation : Memory.AllocId

structure Miri.Interpreter.FunctionPointers.Registry (Other : Type) : Type

• functions : Array FunctionEntry
• extras : Array (Memory.AllocId × Other)

def Miri.Interpreter.FunctionPointers.Registry.empty {Other : Type} : Registry Other

Empty means no functions have yet been reserved. Imported global functions must be seeded explicitly when attaching an already populated compiler image.

Equations

• Miri.Interpreter.FunctionPointers.Registry.empty = { functions := #[], extras := #[] }

def Miri.Interpreter.FunctionPointers.Registry.mergePersistent {Other : Type} (fresh live : Registry Other) : Except String (Registry Other)

Merge TCX-wide GlobalAlloc::Function(instance,salt) reservations into a fresh EvalWorld registry. Imported image entries are seeded by startup and must agree with any identity retained from an earlier Miri world. Per-world FnVal::Other entries deliberately stay in the fresh registry: source Miri allocates those with reserve_alloc_id rather than the TCX dedup cache.

Equations

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

structure Miri.Interpreter.FunctionPointers.Hooks (K User Other : Type) : Type

• registry : User → Registry Other
• putRegistry : User → Registry Other → User
• crossCrateInlineAlways : Bool
• inlineNever : CallInstance → MachineHooks.M K User Bool
• chooseSalt : MachineHooks.M K User (Fin 32)
• ptrGetAlloc : Memory.Pointer Memory.Provenance → MachineHooks.M K User (Option (Memory.AllocId × ABI.Size))
• adjustRootPointer : Memory.AllocId → Memory.BorTag → MachineHooks.M K User (Memory.Pointer Memory.Provenance)
• importedFunction : Memory.AllocId → MachineHooks.M K User (Option CallInstance)

def Miri.Interpreter.FunctionPointers.globalSalt {K User Other : Type} (h : Hooks K User Other) (callee : CallInstance) : MachineHooks.M K User (Fin 32)

Both generic-argument inspection and inline-attribute query precede the uniqueness decision. The threshold Always short-circuits the compiler query.

Equations

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

def Miri.Interpreter.FunctionPointers.rootPointer {K User Other : Type} (h : Hooks K User Other) (id : Memory.AllocId) : MachineHooks.M K User (Memory.Pointer Memory.Provenance)

Function globals cannot be TLS/extern statics. Borrow root tags are created before address assignment, and retained if the latter fails.

Equations

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

def Miri.Interpreter.FunctionPointers.functionPointer {K User Other : Type} (h : Hooks K User Other) (value : FnVal Other) : MachineHooks.M K User (Memory.Pointer Memory.Provenance)

Equations

• Miri.Interpreter.FunctionPointers.functionPointer h value = do let __do_lift ← Miri.Interpreter.FunctionPointers.reserve✝ h value Miri.Interpreter.FunctionPointers.rootPointer h __do_lift

def Miri.Interpreter.FunctionPointers.allocation {K User Other : Type} (h : Hooks K User Other) (pointer : Memory.Pointer (Option Memory.Provenance)) : MachineHooks.M K User (Memory.AllocId × ABI.Size)

Source ptr_get_alloc_id(ptr,0): missing provenance is dangling even when an integer happens to equal a function address. Wildcards use actual exposed lookup.

Equations

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

def Miri.Interpreter.FunctionPointers.globalFunction {K User Other : Type} (h : Hooks K User Other) (id : Memory.AllocId) : MachineHooks.M K User (Option CallInstance)

Equations

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

def Miri.Interpreter.FunctionPointers.getFnAlloc {K User Other : Type} (h : Hooks K User Other) (id : Memory.AllocId) : MachineHooks.M K User (Option (FnVal Other))

Equations

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

def Miri.Interpreter.FunctionPointers.getPtrFn {K User Other : Type} (h : Hooks K User Other) (pointer : Memory.Pointer (Option Memory.Provenance)) : MachineHooks.M K User (FnVal Other)

Equations

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

def Miri.Interpreter.FunctionPointers.pointerMachine {K User Other : Type} (pointer : PointerMachine.Hooks K User) (choices : Memory.AllocId → Memory.AllocAddresses.AddressRandomChoices) (base : Hooks K (PointerMachine.User User) Other) : Hooks K (PointerMachine.User User) Other

Close actual absolute-address resolution and adjustment with PointerMachine. Random address choices remain explicit source outcomes, not a fixed seed.

Equations

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

structure Miri.Interpreter.FunctionPointers.AddressLens (User Payload : Type) : Type

A lawful embedding of existing address state into a larger concrete machine user record (for example ThreadStacks.Storage). No second frame stack is made.

• get : User → PointerMachine.User Payload
• put : User → PointerMachine.User Payload → User
• getPut (user : User) (value : PointerMachine.User Payload) : self.get (self.put user value) = value
• putGet (user : User) : self.put user (self.get user) = user
• putPut (user : User) (first second : PointerMachine.User Payload) : self.put (self.put user first) second = self.put user second

def Miri.Interpreter.FunctionPointers.pointerMachineVia {User Payload K Other : Type} (lens : AddressLens User Payload) (pointer : PointerMachine.Hooks K Payload) (choices : Memory.AllocId → Memory.AllocAddresses.AddressRandomChoices) (base : Hooks K User Other) : Hooks K User Other

Same actual address engine under a lawful user-record embedding. All memory, borrow/race/thread/stack mutations survive both result branches.

Equations

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

def Miri.Interpreter.FunctionPointers.callHooks {K User Other C Extern FnABI ArgABI : Type} (h : Hooks K User Other) (base : CallHooks Memory.Provenance (MachineHooks.State K User) C MachineHooks.FrameExtra Other Extern FnABI ArgABI) : CallHooks Memory.Provenance (MachineHooks.State K User) C MachineHooks.FrameExtra Other Extern FnABI ArgABI

Equations

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

def Miri.Interpreter.FunctionPointers.vtableHooks {K User Other C FnABI : Type} (h : Hooks K User Other) (base : VTableHooks Memory.Provenance (MachineHooks.State K User) C CallInstance FnABI) : VTableHooks Memory.Provenance (MachineHooks.State K User) C CallInstance FnABI

Reuse actual allocation resolution for vtable/type-validity consumers. The existing FullInstance-only VTable dictionary cannot represent machine extra functions: retain that representation gap explicitly rather than classify UB.

Equations

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

def Miri.Interpreter.FunctionPointers.unwindHooks {K User Other C : Type} (h : Hooks K User Other) (base : Unwind.Hooks K User C Other) : Unwind.Hooks K User C Other

Equations

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

def Miri.Interpreter.FunctionPointers.backtraceHooks {K User Other D MD B I E Loc : Type} (h : Hooks K User Other) (base : Backtrace.Hooks Memory.Provenance (MachineHooks.State K User) D MD B I E Loc) : Backtrace.Hooks Memory.Provenance (MachineHooks.State K User) D MD B I E Loc

Equations

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

def Miri.Interpreter.FunctionPointers.castHooks {K User Other C D : Type} (h : Hooks K User Other) (base : CastHooks Memory.Provenance (MachineHooks.State K User) C D) : CastHooks Memory.Provenance (MachineHooks.State K User) C D

Equations

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