Source TCX allocate_bytes_dedup and InterpCx allocate_str_dedup. Global allocation identity and CTFE bytes are retained lazily; normal memory access still performs the actual global conversion and Tree Borrows hooks.

def Miri.Interpreter.GlobalByteMachine.reserve {K U : Type} (bytes : Array UInt8) (salt : Fin 32) : MachineHooks.M K U Memory.AllocId

Reserve only after the exact imported salt-key catalog has been attached. A missing catalog cannot be replaced with an initially empty dedup table.

Equations

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

def Miri.Interpreter.GlobalByteMachine.bytes {K U O : Type} (functions : FunctionPointers.Hooks K U O) (value : Array UInt8) : MachineHooks.M K U (Memory.Pointer Memory.Provenance)

Non-function globals always take the source random salt branch. The root borrow tag/address is adjusted on every mention, including dedup hits.

Equations

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

def Miri.Interpreter.GlobalByteMachine.string {K U O : Type} [DecidableEq K] (functions : FunctionPointers.Hooks K (ValidityMachine.UserState U) O) (access : ValidityMachine.Access K U) (strLayout : ValidityMachine.M K U LocalLayout) (value : String) : ValidityMachine.M K U (MPlaceTy Memory.Provenance)

Allocation/root effects precede length construction and the str layout query, exactly as place.rs:1156–1175. Only the resulting physical place caches alignment; no fabricated type or integer-address pointer is constructed.

Equations

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