Source construction for the Unix environment foreign-item arm. The compiler ABI recipe and genuine environment/host operations are explicit; frame relevance, symbol clashes, ABI compatibility, target policy and guest memory writes are bound to the canonical compiler and execution state.

@[reducible, inline]

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

Equations

• Miri.Input.EvalUnixConstruction.User = Miri.Input.EvalCoreMachine.User

@[reducible, inline]

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

Equations

• Miri.Input.EvalUnixConstruction.State = Miri.Input.EvalCoreMachine.State

@[reducible, inline]

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

Equations

• Miri.Input.EvalUnixConstruction.M Os R P H D O Aff B Host A = Miri.Interpreter.MachineHooks.M Miri.Memory.MiriMemoryKind (Miri.Input.EvalUnixConstruction.User Os R P H D O Aff B Host) A

@[reducible, inline]

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

Equations

• Miri.Input.EvalUnixConstruction.Stored = Miri.Input.EvalCoreMachine.Stored

@[reducible, inline]

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

Equations

• Miri.Input.EvalUnixConstruction.InnerControl Os R P H D O Aff B Host = Miri.Interpreter.ValidityMachine.Control (Miri.Input.EvalUnixConstruction.Stored Os R P H D O Aff B Host)

inductive Miri.Input.EvalUnixConstruction.RejectOpWith : Type

• abort : RejectOpWith
• noWarning : RejectOpWith
• warning : RejectOpWith
• warningWithoutBacktrace : RejectOpWith

@[instance_reducible]

instance Miri.Input.EvalUnixConstruction.instDecidableEqRejectOpWith : DecidableEq RejectOpWith

Equations

• Miri.Input.EvalUnixConstruction.instDecidableEqRejectOpWith x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Input.EvalUnixConstruction.instReprRejectOpWith : Repr RejectOpWith

Equations

• Miri.Input.EvalUnixConstruction.instReprRejectOpWith = { reprPrec := Miri.Input.EvalUnixConstruction.instReprRejectOpWith.repr }

def Miri.Input.EvalUnixConstruction.instReprRejectOpWith.repr : RejectOpWith → Nat → Std.Format

Equations

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

inductive Miri.Input.EvalUnixConstruction.IsolatedOp : Type

Exact source MiriConfig.isolated_op setting. communicate is checked against this value, and shim policy actions are derived below.

• allow : IsolatedOp
• reject (mode : RejectOpWith) : IsolatedOp

@[instance_reducible]

instance Miri.Input.EvalUnixConstruction.instDecidableEqIsolatedOp : DecidableEq IsolatedOp

Equations

• Miri.Input.EvalUnixConstruction.instDecidableEqIsolatedOp = Miri.Input.EvalUnixConstruction.instDecidableEqIsolatedOp.decEq

def Miri.Input.EvalUnixConstruction.instDecidableEqIsolatedOp.decEq (x✝ x✝¹ : IsolatedOp) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.EvalUnixConstruction.instDecidableEqIsolatedOp.decEq Miri.Input.EvalUnixConstruction.IsolatedOp.allow Miri.Input.EvalUnixConstruction.IsolatedOp.allow = isTrue ⋯
• Miri.Input.EvalUnixConstruction.instDecidableEqIsolatedOp.decEq Miri.Input.EvalUnixConstruction.IsolatedOp.allow (Miri.Input.EvalUnixConstruction.IsolatedOp.reject mode) = isFalse ⋯
• Miri.Input.EvalUnixConstruction.instDecidableEqIsolatedOp.decEq (Miri.Input.EvalUnixConstruction.IsolatedOp.reject mode) Miri.Input.EvalUnixConstruction.IsolatedOp.allow = isFalse ⋯

def Miri.Input.EvalUnixConstruction.instReprIsolatedOp.repr : IsolatedOp → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Input.EvalUnixConstruction.instReprIsolatedOp : Repr IsolatedOp

Equations

• Miri.Input.EvalUnixConstruction.instReprIsolatedOp = { reprPrec := Miri.Input.EvalUnixConstruction.instReprIsolatedOp.repr }

structure Miri.Input.EvalUnixConstruction.HostConfigEffects (S Os E : Type) : Type

Genuine host filesystem/error-display effects plus exact Miri host configuration values. It contains no target memory, ABI, libc constant, EnvVars, errno-slot, or policy callback.

• communicate : Bool
• isolatedOp : IsolatedOp
• hostPid : EStateM Interpreter.StepError S UInt32
• currentDirectory : EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError E) Os)
• setCurrentDirectory : Os → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError E) Unit)
• pageSize : UInt64
• numCpus : UInt32
• miriVersion : String
• homeDirectory : EStateM Interpreter.StepError S (Option Os)
• hostErrorDisplay : Interpreter.IoError.HostError E → EStateM Interpreter.StepError S Os
• unknownErrorDisplay : Memory.Scalar Memory.Provenance → EStateM Interpreter.StepError S Os

structure Miri.Input.EvalUnixConstruction.IoHostEffects (S E : Type) : Type

Native error conversions that cannot be computed from the target compiler facts. Unix errno/libc lookups and conversion of host errors remain explicit; the IoError machine, compiler constants, errno memory and scalar access are constructed here.

• hostErrno : String → EStateM Interpreter.StepError S Int32
• hostFromRaw : Int32 → EStateM Interpreter.StepError S (Interpreter.IoError.HostError E)
• hostFromKind : Interpreter.IoError.ErrorKind → EStateM Interpreter.StepError S (Interpreter.IoError.HostError E)

def Miri.Input.EvalUnixConstruction.environmentVariablesFromSource {Os R P H D O Aff B Host C Payload : Type} [DecidableEq Memory.MiriMemoryKind] (host : EvalHostRuntimeConstruction.OsHostEffects Os) (hostEffects : EvalHostRuntimeConstruction.EnvironmentHostEffects (InnerControl Os R P H D O Aff B Host)) (family : Interpreter.ForeignItems.Family) (memory : EvalHostRuntimeConstruction.EnvironmentMemory (InnerControl Os R P H D O Aff B Host) C Payload) : Interpreter.EnvVars.Hooks (Option Memory.Provenance) Os (State Os R P H D O Aff B Host)

Source EnvVars backed by the same EvalWorld environment root and real runtime memory/allocation geometry as startup. The only environment-specific effects are the actual host OsStr conversions and the two host error outcomes; all target strings, arrays, reads, writes, allocation kinds and roots come from EnvironmentMemory.

Equations

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

def Miri.Input.EvalUnixConstruction.environmentFromRuntime {Os R P H D O Aff B Host E C Payload : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (userRelevantCrates : Array Nat) (compatibilityBudget : Nat) (host : EvalHostRuntimeConstruction.OsHostEffects Os) (hostEffects : EvalHostRuntimeConstruction.EnvironmentHostEffects (InnerControl Os R P H D O Aff B Host)) (hostConfig : HostConfigEffects (State Os R P H D O Aff B Host) Os E) (ioHost : IoHostEffects (State Os R P H D O Aff B Host) E) (memory : EvalHostRuntimeConstruction.EnvironmentMemory (InnerControl Os R P H D O Aff B Host) C Payload) : Except Interpreter.StepError (Interpreter.UnixEnvironmentDispatch.Hooks (State Os R P H D O Aff B Host) Os E Interpreter.EnvVars.Kind)

Compose Unix environment dispatch from the real runtime memory bundle. source remains only for process/host/isolation policy and host-error display; its environment, OS-string memory, scalar/pointer access, compiler constants, typed projections, errno allocation, and errno-place state are all replaced by the canonical providers.

Equations

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