Resumable source supervisor and child-side FFI protocol. A finite prefix ending in a wait is pending execution, never a completed successful call.

inductive Miri.Interpreter.Native.Trace.Phase : Type

• initialStop : Phase
• listen : Phase
• startStop : Phase
• faultOff (pid : Pid) (prep : FaultPreparation) : Phase
• faultStep (pid : Pid) (prep : FaultPreparation) : Phase
• faultOn (pid : Pid) (saved : Registers) : Phase
• died (code : Option Int32) : Phase

def Miri.Interpreter.Native.Trace.instReprPhase.repr : Phase → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.Native.Trace.instReprPhase : Repr Phase

Equations

• Miri.Interpreter.Native.Trace.instReprPhase = { reprPrec := Miri.Interpreter.Native.Trace.instReprPhase.repr }

structure Miri.Interpreter.Native.Trace.Runtime : Type

• supervisor : Supervisor
• phase : Phase

def Miri.Interpreter.Native.Trace.instReprRuntime.repr : Runtime → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.Native.Trace.instReprRuntime : Repr Runtime

Equations

• Miri.Interpreter.Native.Trace.instReprRuntime = { reprPrec := Miri.Interpreter.Native.Trace.instReprRuntime.repr }

def Miri.Interpreter.Native.Trace.advance {S C : Type} (h : Hooks S C) (choice : C) (runtime : Runtime) : RvalueM S Runtime

One supervisor transition, preserving source ptrace/signal ordering across explicit pending waits. In particular protection is restored before resumption.

Equations

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

structure Miri.Interpreter.Native.Trace.ChildHooks (S C : Type) : Type

• hostBits : Nat
• pageSize : Nat
• lock : C → RvalueM S Unit
• unlock : C → RvalueM S Unit
• enabled : S → Bool
• pages : C → RvalueM S (Array (Nat × Nat))

  Actual isolated allocator pages, in source enumeration order.

• allocateStack : C → Nat → RvalueM S Nat
• freeStack : C → Nat → RvalueM S Unit
• send : C → TraceRequest → RvalueM S Unit
• receiveConfirmation : C → RvalueM S Unit
• raise : C → Signal → RvalueM S Unit
• protect : C → Nat → Nat → Bool → RvalueM S Unit
• receiveEvents : C → Nat → RvalueM S (Except Bool (Array AccessEvent))

  Source timeout is 5 seconds; timeout panics, IPC disconnect returns none.

• setInterchange : C → Nat → RvalueM S Unit
• currentContextAddress : C → RvalueM S Nat

def Miri.Interpreter.Native.Trace.doFfiLocked {S C A : Type} (h : ChildHooks S C) (choice : C) (action : RvalueM S A) : RvalueM S (A × Option (Array AccessEvent))

Caller must hold the shared supervisor mutex. Protected execution errors abort the external process in Rust; they do not manufacture cleanup/success.

Equations

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

def Miri.Interpreter.Native.Trace.doFfi {S C A : Type} (h : ChildHooks S C) (choice : C) (action : RvalueM S A) : RvalueM S (A × Option (Array AccessEvent))

Source lock is acquired even with tracing disabled. A normal interpreter error unlocks via the Rust mutex guard; a backend process abort has no successor.

Equations

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

def Miri.Interpreter.Native.Trace.rawCall {S C A : Type} (h : ChildHooks S C) (choice : C) (action : RvalueM S A) : RvalueM S (A × Option (Array AccessEvent))

Native InterpCx interchange is set outside the supervisor lock and cleared only after its normal return. Callback aborts cannot return fabricated bytes.

Equations

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

def Miri.Interpreter.Native.Trace.registerRetcode {S C : Type} (h : ChildHooks S C) (choice : C) (code : Int32) : RvalueM S Unit

Equations

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