Actual raw-memory binding for source OS-string helpers. UTF-16 reads use one aligned integer access per element; writes acquire the full destination once, as source get_ptr_alloc_mut does, preserving source race/borrow events.

@[reducible, inline]

abbrev Miri.Interpreter.OsStringMachine.State (K U : Type) : Type

Equations

• Miri.Interpreter.OsStringMachine.State = Miri.Interpreter.PointerMachine.State

@[reducible, inline]

abbrev Miri.Interpreter.OsStringMachine.M (K U A : Type) : Type

Equations

• Miri.Interpreter.OsStringMachine.M = Miri.Interpreter.PointerMachine.M

structure Miri.Interpreter.OsStringMachine.Hooks (K U : Type) : Type

• access : PlaceMachine.AccessConfig K (PointerMachine.User U)
• pointer : PointerMachine.Hooks K U
• symbolicAlignment : Bool
• enforceAlignment : Bool

def Miri.Interpreter.OsStringMachine.readWideString {K U : Type} [DecidableEq K] (h : Hooks K U) (budget : Nat) (pointer : Memory.Pointer (Option Memory.Provenance)) : M K U (Array UInt16)

Equations

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

def Miri.Interpreter.OsStringMachine.writeWideString {K U : Type} [DecidableEq K] (h : Hooks K U) (units : Array UInt16) (pointer : Memory.Pointer (Option Memory.Provenance)) (capacity : UInt64) : M K U (Bool × UInt64)

Equations

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

def Miri.Interpreter.OsStringMachine.bind {K U D MD B I Os Kind : Type} [DecidableEq K] (h : Hooks K U) (budget : Nat) (memory : MemoryShims.Hooks Memory.Provenance (State K U) D MD B I) (base : OsStrings.Hooks Memory.Provenance (State K U) Os Kind) : OsStrings.Hooks Memory.Provenance (State K U) Os Kind

Retain exact actual host encoding and runtime array-layout/allocator leaves. Missing compiler-created runtime array types are never replaced by byte views.

Equations

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

def Miri.Interpreter.OsStringMachine.bindMiri {S Os Kind D MD B I : Type} (strings : OsStrings.Hooks Memory.Provenance S Os Kind) (base : MiriShims.Hooks Memory.Provenance S D MD B I Os) : MiriShims.Hooks Memory.Provenance S D MD B I Os

miri_host_to_target_path reads a plain host OsStr, then performs only the HostToTarget conversion on output; reading a target path here would convert twice.

Equations

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