Pinned shims/os_str.rs. Host OsStr encodings remain explicit operational leaves; they are not replaced with Lean UTF-8 strings. Allocation size follows the source encoded-byte length even for UTF-16 output. Path conversion itself is implemented on exact code units, preserving invalid non-Unicode paths.

@[reducible, inline]

abbrev Miri.Interpreter.OsStrings.M (σ α : Type) : Type

Equations

• Miri.Interpreter.OsStrings.M = EStateM Miri.Interpreter.StepError

inductive Miri.Interpreter.OsStrings.Direction : Type

• hostToTarget : Direction
• targetToHost : Direction

@[instance_reducible]

instance Miri.Interpreter.OsStrings.instDecidableEqDirection : DecidableEq Direction

Equations

• Miri.Interpreter.OsStrings.instDecidableEqDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.OsStrings.instReprDirection : Repr Direction

Equations

• Miri.Interpreter.OsStrings.instReprDirection = { reprPrec := Miri.Interpreter.OsStrings.instReprDirection.repr }

def Miri.Interpreter.OsStrings.instReprDirection.repr : Direction → Nat → Std.Format

Equations

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

def Miri.Interpreter.OsStrings.windowsToUnix {A : Type u_1} [BEq A] (ascii : UInt8 → A) (path : List A) : List A

Generic code units implement the same source routine for u8 and u16.

Equations

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

def Miri.Interpreter.OsStrings.unixToWindows {A : Type u_1} [BEq A] (ascii : UInt8 → A) (path : List A) : List A

Equations

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

structure Miri.Interpreter.OsStrings.Hooks (P S Os Kind : Type) : Type

• hostWindows : Bool
• hostUnix : Bool
• targetWindows : Bool
• fromUnixBytes : ByteArray → Os

  OsStr::from_bytes / OsString::from_vec on the actual Unix host.

• fromUtf8 : ByteArray → Except StepError Os

  std::str::from_utf8 then OsStr::new, retaining invalid-UTF8 unsupported.

• fromWide : Array UInt16 → Except StepError Os

  Windows from_wide is lossless; other hosts use strict String::from_utf16.

• toWide : Os → Except StepError (Array UInt16)

  Windows encode_wide; other hosts require valid UTF8 then encode_utf16.

• encodedBytes : Os → ByteArray
• encodedLength : Os → Nat
• readCString : Memory.Pointer (Option P) → M S ByteArray
• readWideString : Memory.Pointer (Option P) → M S (Array UInt16)
• writeCString : ByteArray → Memory.Pointer (Option P) → UInt64 → M S (Bool × UInt64)
• writeWideString : Array UInt16 → Memory.Pointer (Option P) → UInt64 → M S (Bool × UInt64)
• arrayLayout : Bool → UInt64 → M S LocalLayout

  Actual Ty::new_array(u8/u16,count) and layout_of, including runtime type interning; a matching byte layout cannot substitute a fabricated type ID.

• allocate : LocalLayout → Kind → M S (Memory.Pointer (Option P))

def Miri.Interpreter.OsStrings.bytesToOsStr {P S Os Kind : Type} (h : Hooks P S Os Kind) (bytes : ByteArray) : Except StepError Os

Equations

• Miri.Interpreter.OsStrings.bytesToOsStr h bytes = if h.hostUnix = true then Except.ok (h.fromUnixBytes bytes) else h.fromUtf8 bytes

def Miri.Interpreter.OsStrings.unixIntoString (bytes : ByteArray) : Option String

Unix OsString::into_string: consume the exact encoded bytes and return the string only when they form valid UTF-8. This is distinct from lossy display conversion and is the operation used by Miri's localtime_r for guest TZ.

Equations

• Miri.Interpreter.OsStrings.unixIntoString bytes = String.fromUTF8? bytes

def Miri.Interpreter.OsStrings.unixIntoStringOf {Os : Type} (encodedBytes : Os → ByteArray) (value : Os) : Option String

Equations

• Miri.Interpreter.OsStrings.unixIntoStringOf encodedBytes value = Miri.Interpreter.OsStrings.unixIntoString (encodedBytes value)

def Miri.Interpreter.OsStrings.readOsString {P S Os Kind : Type} (h : Hooks P S Os Kind) (pointer : Memory.Pointer (Option P)) : M S Os

Equations

• Miri.Interpreter.OsStrings.readOsString h pointer = do let __do_lift ← h.readCString pointer Miri.Interpreter.OsStrings.lift✝ (Miri.Interpreter.OsStrings.bytesToOsStr h __do_lift)

def Miri.Interpreter.OsStrings.readOsWideString {P S Os Kind : Type} (h : Hooks P S Os Kind) (pointer : Memory.Pointer (Option P)) : M S Os

Equations

• Miri.Interpreter.OsStrings.readOsWideString h pointer = do let __do_lift ← h.readWideString pointer Miri.Interpreter.OsStrings.lift✝ (h.fromWide __do_lift)

def Miri.Interpreter.OsStrings.writeOsString {P S Os Kind : Type} (h : Hooks P S Os Kind) (value : Os) (pointer : Memory.Pointer (Option P)) (capacity : UInt64) : M S (Bool × UInt64)

Equations

• Miri.Interpreter.OsStrings.writeOsString h value pointer capacity = h.writeCString (h.encodedBytes value) pointer capacity

def Miri.Interpreter.OsStrings.writeOsWideString {P S Os Kind : Type} (h : Hooks P S Os Kind) (value : Os) (pointer : Memory.Pointer (Option P)) (capacity : UInt64) (truncate : Bool := false) : M S (Bool × UInt64)

Return the original failed/full length result even after successfully writing the truncated prefix, exactly as the source helper does.

Equations

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

def Miri.Interpreter.OsStrings.allocOsString {P S Os Kind : Type} (h : Hooks P S Os Kind) (value : Os) (kind : Kind) (wide : Bool := false) : M S (Memory.Pointer (Option P))

Source uses encoded OsStr length for both arrays, before conversion to UTF-16. Its unwrap/assert failure occurs after the actual allocation effects.

Equations

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

def Miri.Interpreter.OsStrings.convertPath {P S Os Kind : Type} (h : Hooks P S Os Kind) (value : Os) (direction : Direction) : Except StepError Os

Equations

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

def Miri.Interpreter.OsStrings.readPath {P S Os Kind : Type} (h : Hooks P S Os Kind) (pointer : Memory.Pointer (Option P)) (wide : Bool := false) : M S Os

Equations

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

def Miri.Interpreter.OsStrings.writePath {P S Os Kind : Type} (h : Hooks P S Os Kind) (path : Os) (pointer : Memory.Pointer (Option P)) (capacity : UInt64) (wide truncate : Bool := false) : M S (Bool × UInt64)

Equations

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

def Miri.Interpreter.OsStrings.allocPath {P S Os Kind : Type} (h : Hooks P S Os Kind) (path : Os) (kind : Kind) (wide : Bool := false) : M S (Memory.Pointer (Option P))

Equations

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