Rust supervisor protocol and Capstone result interpretation. External decode, ptrace, IPC, host signal, and page-protection effects are explicit operations; there is no assumption that an arbitrary native execution is safe.

@[reducible, inline]

abbrev Miri.Interpreter.Native.Trace.Pid : Type

Equations

• Miri.Interpreter.Native.Trace.Pid = Int32

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

• stop : Signal
• usr1 : Signal
• segv : Signal
• cont : Signal
• other (number : Int32) : Signal

@[instance_reducible]

instance Miri.Interpreter.Native.Trace.instDecidableEqSignal : DecidableEq Signal

Equations

• Miri.Interpreter.Native.Trace.instDecidableEqSignal = Miri.Interpreter.Native.Trace.instDecidableEqSignal.decEq

def Miri.Interpreter.Native.Trace.instDecidableEqSignal.decEq (x✝ x✝¹ : Signal) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.Native.Trace.instDecidableEqSignal.decEq Miri.Interpreter.Native.Trace.Signal.stop Miri.Interpreter.Native.Trace.Signal.stop = isTrue ⋯
• Miri.Interpreter.Native.Trace.instDecidableEqSignal.decEq Miri.Interpreter.Native.Trace.Signal.stop (Miri.Interpreter.Native.Trace.Signal.other number) = isFalse ⋯
• Miri.Interpreter.Native.Trace.instDecidableEqSignal.decEq Miri.Interpreter.Native.Trace.Signal.usr1 Miri.Interpreter.Native.Trace.Signal.usr1 = isTrue ⋯
• Miri.Interpreter.Native.Trace.instDecidableEqSignal.decEq Miri.Interpreter.Native.Trace.Signal.usr1 (Miri.Interpreter.Native.Trace.Signal.other number) = isFalse ⋯
• Miri.Interpreter.Native.Trace.instDecidableEqSignal.decEq Miri.Interpreter.Native.Trace.Signal.segv Miri.Interpreter.Native.Trace.Signal.segv = isTrue ⋯
• Miri.Interpreter.Native.Trace.instDecidableEqSignal.decEq Miri.Interpreter.Native.Trace.Signal.segv (Miri.Interpreter.Native.Trace.Signal.other number) = isFalse ⋯
• Miri.Interpreter.Native.Trace.instDecidableEqSignal.decEq Miri.Interpreter.Native.Trace.Signal.cont Miri.Interpreter.Native.Trace.Signal.cont = isTrue ⋯
• Miri.Interpreter.Native.Trace.instDecidableEqSignal.decEq Miri.Interpreter.Native.Trace.Signal.cont (Miri.Interpreter.Native.Trace.Signal.other number) = isFalse ⋯
• Miri.Interpreter.Native.Trace.instDecidableEqSignal.decEq (Miri.Interpreter.Native.Trace.Signal.other number) Miri.Interpreter.Native.Trace.Signal.stop = isFalse ⋯
• Miri.Interpreter.Native.Trace.instDecidableEqSignal.decEq (Miri.Interpreter.Native.Trace.Signal.other number) Miri.Interpreter.Native.Trace.Signal.usr1 = isFalse ⋯
• Miri.Interpreter.Native.Trace.instDecidableEqSignal.decEq (Miri.Interpreter.Native.Trace.Signal.other number) Miri.Interpreter.Native.Trace.Signal.segv = isFalse ⋯
• Miri.Interpreter.Native.Trace.instDecidableEqSignal.decEq (Miri.Interpreter.Native.Trace.Signal.other number) Miri.Interpreter.Native.Trace.Signal.cont = isFalse ⋯

def Miri.Interpreter.Native.Trace.instReprSignal.repr : Signal → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.Native.Trace.instReprSignal : Repr Signal

Equations

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

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

• exited (pid : Pid) (code : Int32) : WaitStatus
• signaled (pid : Pid) (signal : Signal) : WaitStatus
• syscall (pid : Pid) : WaitStatus
• stopped (pid : Pid) (signal : Signal) : WaitStatus
• ptraceEvent (pid : Pid) (signal : Signal) : WaitStatus
• other : WaitStatus

def Miri.Interpreter.Native.Trace.instReprWaitStatus.repr : WaitStatus → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.Native.Trace.instReprWaitStatus : Repr WaitStatus

Equations

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

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

• start (info : StartFfiInfo) : ExecEvent
• endFfi : ExecEvent
• status (pid : Pid) (signal : Signal) : ExecEvent
• syscall (pid : Pid) : ExecEvent
• died (code : Option Int32) : ExecEvent

@[instance_reducible]

instance Miri.Interpreter.Native.Trace.instReprExecEvent : Repr ExecEvent

Equations

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

def Miri.Interpreter.Native.Trace.instReprExecEvent.repr : ExecEvent → Nat → Std.Format

Equations

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

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

• attached : Bool
• overrideRetcode : Option Int32
• lastCode : Option Int32

@[instance_reducible]

instance Miri.Interpreter.Native.Trace.instReprListener : Repr Listener

Equations

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

def Miri.Interpreter.Native.Trace.instReprListener.repr : Listener → Nat → Std.Format

Equations

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

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

• listener : Listener
• currentPid : Pid
• pages : Array Nat
• stack : Option Nat
• events : Array AccessEvent

def Miri.Interpreter.Native.Trace.instReprSupervisor.repr : Supervisor → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.Native.Trace.instReprSupervisor : Repr Supervisor

Equations

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

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

• image : Array UInt8

  Full backend register image, not just IP/SP; restoration preserves all regs.

• ip : Nat
• sp : Nat

def Miri.Interpreter.Native.Trace.instReprRegisters.repr : Registers → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.Native.Trace.instReprRegisters : Repr Registers

Equations

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

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

• isMemory : Bool
• size : UInt8
• access : Option (Bool × Bool)

@[instance_reducible]

instance Miri.Interpreter.Native.Trace.instReprOperand : Repr Operand

Equations

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

def Miri.Interpreter.Native.Trace.instReprOperand.repr : Operand → Nat → Std.Format

Equations

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

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

• hostBits : Nat
• wordSize : Nat
• pageSize : Nat
• wait : C → Option Pid → Bool → RvalueM S (Except Unit WaitStatus)

  Failure models waitid error; none is WNOHANG/StillAlive.

• pollRequest : C → RvalueM S (Option TraceRequest)
• confirm : C → RvalueM S Unit
• continueProcess : C → Pid → Option Signal → RvalueM S Bool
• syscall : C → Pid → RvalueM S Bool
• kill : C → Pid → Signal → RvalueM S Unit
• yieldHost : C → RvalueM S Unit
• sendEvents : C → Array AccessEvent → RvalueM S Unit
• signalAddress : C → Pid → RvalueM S Nat
• registers : C → Pid → RvalueM S Registers
• setRegisters : C → Pid → Registers → RvalueM S Unit
• writeWord : C → Pid → Nat → Nat → RvalueM S Unit
• readWord : C → Pid → Nat → RvalueM S (Option (Array UInt8))

  ptrace read errors are source-defaulted to zero, represented by none.

• decodeOne : C → Array UInt8 → Nat → RvalueM S (Array Operand)
• singleStep : C → Pid → RvalueM S Unit
• memprOff : Nat
• memprOn : Nat
• pageAddrGlobal : Nat
• pageCountGlobal : Nat
• unexpectedSignal : C → Signal → RvalueM S Unit
• segfaultDiagnostic : C → Nat → Array Nat → Registers → RvalueM S Unit

def Miri.Interpreter.Native.Trace.poll {S C : Type} (h : Hooks S C) (choice : C) (listener : Listener) : RvalueM S (Listener × Option ExecEvent)

One listener polling iteration. None requests the source host yield/retry; no bounded polling result is interpreted as process completion.

Equations

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

def Miri.Interpreter.Native.Trace.appendDecoded (addr : Nat) (operands : Array Operand) (initial : Array AccessEvent) : Except (StepError × Array AccessEvent) (Array AccessEvent)

Capstone memory operands retain read-before-write, uncertain RW writes, and source partial event append before detecting a second memory operand.

Equations

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

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

• ready (pid : Pid) : WaitResult
• pending : WaitResult
• died (code : Option Int32) : WaitResult

def Miri.Interpreter.Native.Trace.instReprWaitResult.repr : WaitResult → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.Native.Trace.instReprWaitResult : Repr WaitResult

Equations

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

def Miri.Interpreter.Native.Trace.waitSignalStep {S C : Type} (h : Hooks S C) (choice : C) (pid : Option Pid) (signal : Signal) : RvalueM S WaitResult

One iteration of source wait_for_signal, retaining unknown-status continue and signal forwarding. Caller retains pending state until the requested signal.

Equations

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

def Miri.Interpreter.Native.Trace.waitSignal {S C : Type} (h : Hooks S C) (choice : C) (pid : Option Pid) (signal : Signal) : Nat → RvalueM S WaitResult

Bounded operational prefix of a possibly diverging wait. Exhaustion returns pending; it never authorizes the caller to advance the supervisor protocol.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.Native.Trace.waitSignal h choice pid signal 0 = pure Miri.Interpreter.Native.Trace.WaitResult.pending

def Miri.Interpreter.Native.Trace.instructionBytes {S C : Type} (h : Hooks S C) (choice : C) (pid : Pid) (ip : Nat) : RvalueM S (Array UInt8)

Source instruction-byte collection reads ceil(15/wordSize) complete words, with individual ptrace failures zero-filled before the Capstone call.

Equations

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

def Miri.Interpreter.Native.Trace.clearCallbackStack {S C : Type} (h : Hooks S C) (choice : C) (pid : Pid) (stack : Nat) : RvalueM S Unit

Equations

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

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

• saved : Registers
• callback : Registers
• pageAddress : Nat
• pageCount : Nat
• bytes : Array UInt8
• events : Array AccessEvent

@[instance_reducible]

instance Miri.Interpreter.Native.Trace.instReprFaultPreparation : Repr FaultPreparation

Equations

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

def Miri.Interpreter.Native.Trace.instReprFaultPreparation.repr : FaultPreparation → Nat → Std.Format

Equations

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

def Miri.Interpreter.Native.Trace.prepareFault {S C : Type} (h : Hooks S C) (choice : C) (pid : Pid) (pages : Array Nat) (stack : Nat) (events : Array AccessEvent) : RvalueM S (Option FaultPreparation)

Pure Rust-side preparation before mempr_off. Native faults outside the owned pages kill the child; they never become a successful unknown memory access.

Equations

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