eval.rs::eval_entry final reporting/leak policy. Host diagnostics remain explicit effects; reachability and thread-leak decisions are actual machine operations, not caller-provided booleans.

@[reducible, inline]

abbrev Miri.Interpreter.EntryResult.Leaks : Type

Equations

• Miri.Interpreter.EntryResult.Leaks = Array (Miri.Memory.AllocId × Miri.Memory.LocalAllocation Miri.Memory.Provenance Miri.TreeBorrows.BorrowTree Miri.Memory.MiriMemoryKind)

structure Miri.Interpreter.EntryResult.Hooks (U : Type) : Type

• reportResult : StepError → MachineHooks.M Memory.MiriMemoryKind U (Option (Int32 × Bool))
• staticRoots : U → Array Memory.AllocId
• reportThreadLeak : MachineHooks.M Memory.MiriMemoryKind U Unit
• reportLeaks : Leaks → MachineHooks.M Memory.MiriMemoryKind U Unit
• ignoreLeaksNote : MachineHooks.M Memory.MiriMemoryKind U Unit
• failureCode : Int32

def Miri.Interpreter.EntryResult.finishProfiled {U : Type} (profile : Lean.Options) (h : Hooks U) (ignoreLeaks : Bool) (outcome : StepError) : MachineHooks.M Memory.MiriMemoryKind U Int32

Equations

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

def Miri.Interpreter.EntryResult.finish {U : Type} (h : Hooks U) (ignoreLeaks : Bool) (outcome : StepError) : MachineHooks.M Memory.MiriMemoryKind U Int32

Equations

• Miri.Interpreter.EntryResult.finish h ignoreLeaks outcome = Miri.Interpreter.EntryResult.finishProfiled ∅ h ignoreLeaks outcome

theorem Miri.Interpreter.EntryResult.finishProfiled_eq_finish {U : Type} (profile : Lean.Options) (h : Hooks U) (ignoreLeaks : Bool) (outcome : StepError) : finishProfiled profile h ignoreLeaks outcome = finish h ignoreLeaks outcome