Import exact TCX byte/salt identity evidence. Probes that miss the imported compiler image do not create runtime globals; subsequent reservation stays lazy. Completeness is checked against every qualifying immutable imported allocation, not inferred from a catalog that merely happens to contain some literals.

structure Miri.Input.CompilerGlobalBytes.Prepared : Type

• strType : MIR.TyId
• keys : Array (Array UInt8 × Fin 32 × Memory.AllocId)

def Miri.Input.CompilerGlobalBytes.prepare {P E K : Type} (program : LoweredProgram) (runtime : RuntimeMetadata) (memory : Memory.MemoryState P E K) (sourceEquality : Option (RuntimeMetadata.JsonReflexivity runtime.source.raw) := none) : Except String Prepared

Attach immediately after graph import, before source runtime reservations. The exported graph must be the same complete identity universe that was probed. Compiler pool identity/serialization remains an explicit exporter trust boundary.

Equations

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

def Miri.Input.CompilerGlobalBytes.attachProfiled {K U : Type} (profile : Lean.Options) (program : LoweredProgram) (runtime : RuntimeMetadata) (sourceEquality : Option (RuntimeMetadata.JsonReflexivity runtime.source.raw) := none) : Interpreter.MachineHooks.M K U Prepared

Equations

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

def Miri.Input.CompilerGlobalBytes.attach {K U : Type} (program : LoweredProgram) (runtime : RuntimeMetadata) (sourceEquality : Option (RuntimeMetadata.JsonReflexivity runtime.source.raw) := none) : Interpreter.MachineHooks.M K U Prepared

Equations

• Miri.Input.CompilerGlobalBytes.attach program runtime sourceEquality = Miri.Input.CompilerGlobalBytes.attachProfiled ∅ program runtime sourceEquality

theorem Miri.Input.CompilerGlobalBytes.attach_profile_identity {K U : Type} (program : LoweredProgram) (runtime : RuntimeMetadata) (sourceEquality : Option (RuntimeMetadata.JsonReflexivity runtime.source.raw)) : attach program runtime sourceEquality = attachProfiled ∅ program runtime sourceEquality

def Miri.Input.CompilerGlobalBytes.strLayout {K U : Type} (runtime : RuntimeMetadata) (prepared : Prepared) : Interpreter.MachineHooks.M K U Interpreter.LocalLayout

Equations

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