Raw source residual bindings for the portable Miri-specific externs. This module derives host path conversion, output and isolation from source-level capabilities. Unsupported diagnostics and compiler identity evidence remain demand-local.

@[reducible, inline]

abbrev Miri.Input.EvalMiriHostEffectsConstruction.User (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalMiriHostEffectsConstruction.User Os R P H D O Aff B Host = Miri.Input.EvalCoreMachine.User Os R P H D O Aff B Host

@[reducible, inline]

abbrev Miri.Input.EvalMiriHostEffectsConstruction.State (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalMiriHostEffectsConstruction.State Os R P H D O Aff B Host = Miri.Input.EvalCoreMachine.State Os R P H D O Aff B Host

@[reducible, inline]

abbrev Miri.Input.EvalMiriHostEffectsConstruction.M (Os R P H D O Aff B Host A : Type) : Type

Equations

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

structure Miri.Input.EvalMiriHostEffectsConstruction.RawLeaves (Os R P H D O Aff B Host Error Meta Kind : Type) : Type

• strings : Interpreter.OsStrings.Hooks Memory.Provenance (State Os R P H D O Aff B Host) Os Kind
• hostFiles : EvalUnixIoConstruction.HostFileEffects (State Os R P H D O Aff B Host) H D O Error Meta
• writeRetryBudget : Nat

  Bound the source write_all retry loop so repeated Interrupted or adversarial short writes remain an explicit resource-exhaustion outcome.

• communicate : Bool
• sourceAllocIdNumber : Option (Memory.AllocId → M Os R P H D O Aff B Host UInt64)

  Exact rustc allocation-number identity mapping, when the source compiler retains it. Dense imported memory IDs are deliberately not accepted here.

• namePointer : Option (Memory.Pointer (Option Memory.Provenance) → UInt8 → ByteArray → M Os R P H D O Aff B Host Unit)
• printBorrowState : Option (UInt64 → Bool → M Os R P H D O Aff B Host Unit)

def Miri.Input.EvalMiriHostEffectsConstruction.writeAllHost {S E : Type} (write : ByteArray → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError E) Nat)) (budget : Nat) (bytes : ByteArray) : EStateM Interpreter.StepError S Unit

The source Write::write_all loop over a host writer. Host I/O errors are returned to this boundary and ignored by its caller; capability and interpreter errors remain thrown. A finite budget prevents endless Interrupted responses.

Equations

• Miri.Input.EvalMiriHostEffectsConstruction.writeAllHost write budget bytes = Miri.Input.EvalMiriHostEffectsConstruction.writeAllHost.loop write bytes budget 0

def Miri.Input.EvalMiriHostEffectsConstruction.writeAllHost.loop {S E : Type} (write : ByteArray → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError E) Nat)) (bytes : ByteArray) : Nat → Nat → EStateM Interpreter.StepError S Unit

Equations

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

def Miri.Input.EvalMiriHostEffectsConstruction.fromSource {Os R P H D O Aff B Host Error Meta Kind : Type} (leaves : RawLeaves Os R P H D O Aff B Host Error Meta Kind) : EvalPortableForeignConstruction.MiriEffects Os R P H D O Aff B Host Os

Bind actual source OS-string routines and host stdout/stderr effects to the Miri shim residual record. HostFileEffects.hostWrite errors are ignored because pinned foreign_items.rs ignores write_all errors; absent capabilities represented by StepError still propagate.

Equations

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

def Miri.Input.EvalMiriHostEffectsConstruction.fromCoreSource {Os R P H D O Aff B Host C Error Meta : Type} [DecidableEq Memory.MiriMemoryKind] (host : EvalHostRuntimeConstruction.OsHostEffects Os) (memory : EvalHostRuntimeConstruction.EnvironmentMemory (Interpreter.ValidityMachine.Control (EvalCoreMachine.Stored Os R P H D O Aff B Host)) C P) (hostFiles : EvalUnixIoConstruction.HostFileEffects (State Os R P H D O Aff B Host) H D O Error Meta) (communicate : Bool) (writeRetryBudget : Nat) (sourceAllocIdNumber : Option (Memory.AllocId → M Os R P H D O Aff B Host UInt64) := none) (namePointer : Option (Memory.Pointer (Option Memory.Provenance) → UInt8 → ByteArray → M Os R P H D O Aff B Host Unit) := none) (printBorrowState : Option (UInt64 → Bool → M Os R P H D O Aff B Host Unit) := none) : EvalPortableForeignConstruction.MiriEffects Os R P H D O Aff B Host Os

Source-context convenience constructor. OS encodings, target conversion, and target-memory C-string operations are generated from the same canonical environment memory and host OsStr implementation used by other shims.

Equations

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

def Miri.Input.EvalMiriHostEffectsConstruction.sourceAllocIdNumberFromImage {Os R P H D O Aff B Host : Type} (image : AllocationImage.Imported) : Memory.AllocId → M Os R P H D O Aff B Host UInt64

Recover rustc's allocation number only through the exact exporter-node to runtime-global crosswalk. Fresh runtime allocations and legacy exports have no witness and remain Unsupported; the runtime's own dense ID is never returned.

Equations

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

def Miri.Input.EvalMiriHostEffectsConstruction.sourceAllocIdFromImage {Os R P H D O Aff B Host : Type} (image : AllocationImage.Imported) : UInt64 → M Os R P H D O Aff B Host (Option Memory.AllocId)

Inverse source-number lookup for miri_print_borrow_state. Zero and a raw ID with no global return none. Opaque globals remain Unsupported: source memory and statics can be live data even before their payload is imported. Export-node witnesses and the runtime imported-global table must identify one unique allocation before it can be inspected.

Equations

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