Canonical state reassociation. Source machine validation/alignment/ghost fields and the alloc-address symbolic-alignment map each have exactly one owner. This changes record nesting only: no frame, memory, clock or cache is created. Error results are transported with their actual partially updated state.

@[reducible, inline]

abbrev Miri.Interpreter.ExecutionStateTransport.Outer (U : Type) : Type

Equations

• Miri.Interpreter.ExecutionStateTransport.Outer U = Miri.Interpreter.ThreadStacks.Storage (Miri.Interpreter.ValidityMachine.UserState U)

@[reducible, inline]

abbrev Miri.Interpreter.ExecutionStateTransport.Inner (U : Type) : Type

Equations

• Miri.Interpreter.ExecutionStateTransport.Inner U = Miri.Interpreter.ValidityMachine.UserState (Miri.Interpreter.ThreadStacks.Storage U)

def Miri.Interpreter.ExecutionStateTransport.toInner {U : Type} (u : Outer U) : Inner U

Equations

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

def Miri.Interpreter.ExecutionStateTransport.toOuter {U : Type} (u : Inner U) : Outer U

Equations

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

@[simp]

theorem Miri.Interpreter.ExecutionStateTransport.outer_roundtrip {U : Type} (u : Outer U) : toOuter (toInner u) = u

@[simp]

theorem Miri.Interpreter.ExecutionStateTransport.inner_roundtrip {U : Type} (u : Inner U) : toInner (toOuter u) = u

def Miri.Interpreter.ExecutionStateTransport.inward {K U : Type} (s : MachineHooks.State K (Outer U)) : MachineHooks.State K (Inner U)

Equations

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

def Miri.Interpreter.ExecutionStateTransport.outward {K U : Type} (s : MachineHooks.State K (Inner U)) : MachineHooks.State K (Outer U)

Equations

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

@[simp]

theorem Miri.Interpreter.ExecutionStateTransport.outward_inward {K U : Type} (s : MachineHooks.State K (Outer U)) : outward (inward s) = s

@[simp]

theorem Miri.Interpreter.ExecutionStateTransport.inward_outward {K U : Type} (s : MachineHooks.State K (Inner U)) : inward (outward s) = s

def Miri.Interpreter.ExecutionStateTransport.action {K U A : Type} (a : MachineHooks.M K (Inner U) A) : MachineHooks.M K (Outer U) A

Run an existing validity/pointer/atomic operation on the same actual state.

Equations

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

def Miri.Interpreter.ExecutionStateTransport.reverseAction {K U A : Type} (a : MachineHooks.M K (Outer U) A) : MachineHooks.M K (Inner U) A

Outer scheduler/registry/compiler operations can be used by inner drivers.

Equations

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

def Miri.Interpreter.ExecutionStateTransport.scalar {P K U C : Type} (h : ScalarOpsHooks P (MachineHooks.State K (Inner U)) C) : ScalarOpsHooks P (MachineHooks.State K (Outer U)) C

Equations

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

def Miri.Interpreter.ExecutionStateTransport.atomic {P K U C V : Type} (h : IntrinsicAtomicHooks P (MachineHooks.State K (Inner U)) C V) : IntrinsicAtomicHooks P (MachineHooks.State K (Outer U)) C V

Equations

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

def Miri.Interpreter.ExecutionStateTransport.atomicMachine {K U C Payload : Type} [DecidableEq K] (base : IntrinsicAtomicHooks Memory.Provenance (MachineHooks.State K (Inner U)) C (RuntimePlace Memory.Provenance)) (access : PlaceMachine.AccessConfig K (Inner U)) (allocation : PlaceMachine.AllocationConfig K (Inner U)) (compiler : PlaceMachine.CompilerHooks K (Inner U) C) (pointers : PointerMachine.Hooks K (ValidityMachine.Control (ThreadStacks.Storage U))) (extras : MemoryExtras.Hooks K (Inner U) Payload) : IntrinsicAtomicHooks Memory.Provenance (MachineHooks.State K (Outer U)) C (RuntimePlace Memory.Provenance)

Assemble the actual canonical physical atomic pipeline, then transport its complete dictionary. This is not a second atomic implementation.

Equations

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

def Miri.Interpreter.ExecutionStateTransport.pointerAllocation {K U : Type} (h : PointerMachine.Hooks K (ValidityMachine.Control (ThreadStacks.Storage U))) (p : Memory.Pointer Memory.Provenance) (size : Int64) : MachineHooks.M K (Outer U) (Option (Memory.AllocId × ABI.Size))

The pointer dictionary's source effects run against the canonical address, provenance and symbolic-alignment state carried by the reassociation.

Equations

• Miri.Interpreter.ExecutionStateTransport.pointerAllocation h p size = Miri.Interpreter.ExecutionStateTransport.action (Miri.Interpreter.PointerMachine.ptrGetAlloc h p size)

def Miri.Interpreter.ExecutionStateTransport.exposeProvenance {K U : Type} [DecidableEq K] (h : PointerMachine.Hooks K (ValidityMachine.Control (ThreadStacks.Storage U))) (p : Memory.Provenance) : MachineHooks.M K (Outer U) Unit

Equations

• Miri.Interpreter.ExecutionStateTransport.exposeProvenance h p = Miri.Interpreter.ExecutionStateTransport.action (Miri.Interpreter.PointerMachine.exposeProvenance h p)

def Miri.Interpreter.ExecutionStateTransport.withGhostValidation {K U A : Type} (a : MachineHooks.M K (Outer U) A) : MachineHooks.M K (Outer U) A

The scope encloses the entire transported action. Restoration uses the post-action Control, retaining failures, registry updates and cached unions.

Equations

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

def Miri.Interpreter.ExecutionStateTransport.enforceValidity {K U : Type} : MachineHooks.M K (Outer U) Bool

Equations

• Miri.Interpreter.ExecutionStateTransport.enforceValidity = Miri.Interpreter.ExecutionStateTransport.action Miri.Interpreter.ValidityMachine.enforceValidity

def Miri.Interpreter.ExecutionStateTransport.enforceValidityRecursively {K U : Type} : MachineHooks.M K (Outer U) Bool

Equations

• Miri.Interpreter.ExecutionStateTransport.enforceValidityRecursively = Miri.Interpreter.ExecutionStateTransport.action Miri.Interpreter.ValidityMachine.enforceValidityRecursively

def Miri.Interpreter.ExecutionStateTransport.readImmediate {K U : Type} [DecidableEq K] (access : PlaceMachine.AccessConfig K (Inner U)) (value : OpTy Memory.Provenance) : MachineHooks.M K (Outer U) (RvalueImmTy Memory.Provenance)

Equations

• Miri.Interpreter.ExecutionStateTransport.readImmediate access value = Miri.Interpreter.ExecutionStateTransport.action (Miri.Interpreter.ValidityMachine.readImmediate access value)

def Miri.Interpreter.ExecutionStateTransport.step {K U C O X Host : Type} [DecidableEq K] (h : ExecutionMachine.Config K (Inner U) C O X Host) (limits : ExecutionMachine.Limits) (c : C) (s : MachineHooks.State K (Outer U)) : StepResult (MachineHooks.State K (Outer U)) Bool

Whole MIR execution uses the existing full source assembly with all its physical/validation dictionaries instantiated at Inner U. Outer state keeps its scheduler-facing ThreadStacks representation between steps.

Equations

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