helpers.rs::eval_path and eval_context.rs::eval_global for exact named libc globals used by pthread synchronization. Query identity is the full source path; static and const allocations are materialized through the canonical allocation image and root-pointer operations.

structure Miri.Input.CompilerNamedGlobals.Value : Type

• definition : MIR.DefId
• ty : MIR.TyId
• allocation : AllocationId
• isStatic : Bool

structure Miri.Input.CompilerNamedGlobals.Entry : Type

• name : String
• result : Except String Value
• payload : Lean.Json

structure Miri.Input.CompilerNamedGlobals.Prepared : Type

• program : LoweredProgram
• runtime : RuntimeMetadata
• entries : Array Entry

def Miri.Input.CompilerNamedGlobals.prepare (runtime : RuntimeMetadata) (program : LoweredProgram) (sourceEquality : Option (RuntimeMetadata.JsonReflexivity runtime.source.raw) := none) : Except String Prepared

Retain every exact path query, including unavailable rows. Failed queries are raised only when the corresponding source path is demanded.

Equations

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

def Miri.Input.CompilerNamedGlobals.global {K U Other : Type} (prepared : Prepared) (memory : CompilerLinkSections.Memory K U Other) (name : String) : Interpreter.MachineHooks.M K U (Interpreter.MPlaceTy Memory.Provenance)

Execute the source global-root-pointer query using the imported compiler allocation and ordinary extern/static pointer hooks. No name or byte-content lookup substitutes for the exact compiler row.

Equations

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