Select disabled race tracking or canonical vector clocks from the shared EvalWorld; reject inconsistent clock storage.

@[reducible, inline]

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

Equations

• Miri.Input.EvalBackendMachine.User Os R P H D O Aff B Host = Miri.Interpreter.ExecutionStateTransport.Inner (Miri.Input.EvalWorld.World Os R P H D O Aff B Host)

@[reducible, inline]

abbrev Miri.Input.EvalBackendMachine.Machine (Os R P 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.EvalBackendMachine.State (Os R P H D O Aff B Host : Type) : Type

Equations

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

def Miri.Input.EvalBackendMachine.handler {Os R P H D O Aff B Host : Type} (m : Machine Os R P H D O Aff B Host) : Except Interpreter.StepError (Interpreter.RaceMode.Handler B)

Equations

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

def Miri.Input.EvalBackendMachine.access {Os R P H D O Aff B Host : Type} (base : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (User Os R P H D O Aff B Host)) : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (User Os R P H D O Aff B Host)

Preserve source diagnostic staging and validate canonical clock storage before continuing to race/synchronization memory hooks.

Equations

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

def Miri.Input.EvalBackendMachine.dispatcher {Os R P H D O Aff B Host C V : Type} : Interpreter.IntrinsicBackend.Dispatcher (State Os R P H D O Aff B Host) C V

Equations

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