Single persistent storage composition for the canonical interpreter. No address/type/function/callback table is mirrored for compiler or GC adapters.

structure Miri.Input.EvalWorld.World (Os R Payload H D O Aff B Host : Type) : Type

• runtime : Interpreter.MachineGCRoots.Storage Os R Payload H D O Aff
• main : Option Interpreter.MainMachine.Data
• exit : Interpreter.WindowsExitMachine.Registry
• types : RuntimeArrayTypes.World
• functions : Interpreter.FunctionPointers.Registry O
• vtables : Interpreter.VTableMachine.Registry
• symbols : Interpreter.IntrinsicSymbolsMachine.Registry
• choices : Interpreter.ExecutionChoices.Tape
• trackedAllocations : Array Memory.AllocId

  The source machine's persistent tracked allocation set. This is shared by Miri tracking shims; it is not an allocation identity conversion table.

• backend : Interpreter.RaceMode.Selection B
• host : Host

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

• Miri.Input.EvalWorld.State Os R Payload H D O Aff B Host = Miri.Interpreter.MachineHooks.State Miri.Memory.MiriMemoryKind (Miri.Input.EvalWorld.User Os R Payload H D O Aff B Host)

def Miri.Input.EvalWorld.addresses {Os R Payload H D O Aff B Host : Type} : Interpreter.FunctionPointers.AddressLens (User Os R Payload H D O Aff B Host) (Interpreter.ValidityMachine.Control (World Os R Payload H D O Aff B Host))

Equations

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

def Miri.Input.EvalWorld.roots {Os R Payload H D O Aff B Host : Type} : Interpreter.MachineGCRoots.Views (User Os R Payload H D O Aff B Host) Os R Payload H D O

Equations

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

def Miri.Input.EvalWorld.collect {Os R Payload H D O Aff B Host : Type} : Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R Payload H D O Aff B Host) Unit

Every source provenance visitor reads the same runtime storage used by execution. In particular callback closures are not invented GC roots.

Equations

• Miri.Input.EvalWorld.collect = Miri.Interpreter.MachineGCRoots.run Miri.Input.EvalWorld.roots Miri.Input.EvalWorld.addresses

def Miri.Input.EvalWorld.ubFreedom {U C O X F A Aff P : Type} (main : Interpreter.MainMachine.Hooks U C O X F A Aff P) (base : Interpreter.RunLoopHooks (Interpreter.MainMachine.State U) C Interpreter.MainMachine.Callback) (scheduler : C → Interpreter.ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind U) (allowed : Interpreter.MainMachine.State U → C → Prop) (initial : Interpreter.MainMachine.State U → Prop) : Prop

Operational safety uses every permitted finite prefix, not an executable fuel bound or a single supplied tape. The relation stays conditional on the actual assembled operations and the semantic choice-support predicate.

Equations

• Miri.Input.EvalWorld.ubFreedom main base scheduler allowed initial = Miri.Interpreter.RunLoop.UBFreedomFrom (Miri.Interpreter.MainMachine.bindLoop main base scheduler) allowed initial