Initialization, callback construction, and mprotect helper boundaries from native_lib/{mod.rs,trace/child.rs,trace/parent.rs,trace/stub.rs}.

structure Miri.Interpreter.Native.LibraryHooks (S C Handle : Type) : Type

• enabledBuild : Bool
• hostTriple : String
• targetTriple : String
• load : C → String → RvalueM S Handle
• allocateInterchange : C → Nat → RvalueM S Unit

def Miri.Interpreter.Native.initializeLibraries {S C Handle : Type} (h : LibraryHooks S C Handle) (choice : C) (paths : Array String) : RvalueM S (Array (Handle × Library))

Source Machine::new checks host/target once per configured library, before loading that library. Empty configuration does not spuriously reject a cross compile, while the supported build still allocates its interchange cell.

Equations

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

inductive Miri.Interpreter.Native.ForkResult : Type

• parent (child : Trace.Pid) : ForkResult
• child : ForkResult

def Miri.Interpreter.Native.instReprForkResult.repr : ForkResult → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.Native.instReprForkResult : Repr ForkResult

Equations

• Miri.Interpreter.Native.instReprForkResult = { reprPrec := Miri.Interpreter.Native.instReprForkResult.repr }

inductive Miri.Interpreter.Native.InitOutcome : Type

• initialized : InitOutcome
• unavailable : InitOutcome
• supervisorExited (code : Int32) : InitOutcome

@[instance_reducible]

instance Miri.Interpreter.Native.instReprInitOutcome : Repr InitOutcome

Equations

• Miri.Interpreter.Native.instReprInitOutcome = { reprPrec := Miri.Interpreter.Native.instReprInitOutcome.repr }

def Miri.Interpreter.Native.instReprInitOutcome.repr : InitOutcome → Nat → Std.Format

Equations

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

structure Miri.Interpreter.Native.InitHooks (S C : Type) : Type

• supported : Bool
• ptraceScope : C → RvalueM S (Option String)
• lock : C → RvalueM S Unit
• unlock : C → RvalueM S Unit
• initialized : S → Bool
• createChannels : C → RvalueM S Unit
• sysconfPageSize : C → RvalueM S Nat
• storePageSize : C → Nat → RvalueM S Unit
• fork : C → RvalueM S ForkResult
• seize : C → Trace.Pid → Bool → Bool → Bool → RvalueM S Bool

  PTRACE_O_TRACESYSGOOD | TRACECLONE | TRACEFORK; false means seize failed.

• killChild : C → Trace.Pid → RvalueM S Unit
• runSupervisor : C → Trace.Pid → RvalueM S (Option Int32)

  Actual supervisor operational execution. Returning means its source ExecEnd, not proof of completion/safety of the arbitrary native program.

• forgetGuard : C → RvalueM S Unit

  Parent intentionally leaks the mutex guard before its supervisor loop.

• parentDeathSignal : C → Trace.Signal → RvalueM S Bool
• raise : C → Trace.Signal → RvalueM S Unit
• installSupervisor : C → RvalueM S Unit

def Miri.Interpreter.Native.initSupervisor {S C : Type} (h : InitHooks S C) (choice : C) : RvalueM S InitOutcome

Ptrace-scope fast rejection precedes the initialized/lock check exactly as source. Parent exit is explicit, not an initialized interpreter continuation.

Equations

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

structure Miri.Interpreter.Native.ClosureHooks (P S C V Code Closure : Type) : Type

• native : Hooks P S C V Code
• build : C → Option (Array FfiType × FfiType) → Bool → RvalueM S Closure

  Backend leaks descriptor data+closure until process exit, as source.

• activeInterchange : S → Bool

def Miri.Interpreter.Native.buildClosure {P S C V Code Closure : Type} (h : ClosureHooks P S C V Code Closure) (choice : C) (fuel : Nat) (inputs : Array MIR.TyId) (output : MIR.TyId) : RvalueM S Closure

Unsupported signature conversion builds the source aborting closure with an empty descriptor; it does not reject creation of the function pointer.

Equations

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

def Miri.Interpreter.Native.callback {P S C V Code Closure A : Type} (h : ClosureHooks P S C V Code Closure) (unsupportedSignature : Bool) : RvalueM S A

Source callback always diagnoses and exits: successful native→Rust callbacks are not implemented in pinned Miri either. The returned error has no value.

Equations

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

structure Miri.Interpreter.Native.ProtectionHooks (S C : Type) : Type

• hostBits : Nat
• pageAddress : S → Nat
• pageSize : S → Nat
• pageCount : S → Nat
• mprotect : C → Nat → Nat → Bool → RvalueM S Bool
• raiseStop : C → RvalueM S Bool

inductive Miri.Interpreter.Native.ProtectionOutcome : Type

• stopped : ProtectionOutcome
• exit (code : Int32) : ProtectionOutcome

def Miri.Interpreter.Native.instReprProtectionOutcome.repr : ProtectionOutcome → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.Native.instReprProtectionOutcome : Repr ProtectionOutcome

Equations

• Miri.Interpreter.Native.instReprProtectionOutcome = { reprPrec := Miri.Interpreter.Native.instReprProtectionOutcome.repr }

def Miri.Interpreter.Native.protectionHelper {S C : Type} (h : ProtectionHooks S C) (choice : C) (off : Bool) : RvalueM S ProtectionOutcome

Source off helper uses saturating multiplication, on helper wrapping multiplication. Neither error unwinds through the synthetic callback stack.

Equations

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