Physical source synchronization arenas. References index source host objects; callback tokens come exclusively from the shared ThreadMachine supply. The arena contains no interpreter functions and has no independent token generator.

@[reducible, inline]

abbrev Miri.Interpreter.TypedSyncMachine.User (U : Type) : Type

Equations

• Miri.Interpreter.TypedSyncMachine.User = Miri.Interpreter.ExecutionStateTransport.Inner

@[reducible, inline]

abbrev Miri.Interpreter.TypedSyncMachine.State (K U : Type) : Type

Equations

• Miri.Interpreter.TypedSyncMachine.State K U = Miri.Interpreter.MachineHooks.State K (Miri.Interpreter.TypedSyncMachine.User U)

@[reducible, inline]

abbrev Miri.Interpreter.TypedSyncMachine.M (K U A : Type) : Type

Equations

• Miri.Interpreter.TypedSyncMachine.M K U A = Miri.Interpreter.MachineHooks.M K (Miri.Interpreter.TypedSyncMachine.User U) A

structure Miri.Interpreter.TypedSyncMachine.Views (U : Type) : Type

• storage : U → Concurrency.TypedSyncRuntime.Storage
• putStorage : U → Concurrency.TypedSyncRuntime.Storage → U
• nextCallback : U → Nat
• putNextCallback : U → Nat → U

def Miri.Interpreter.TypedSyncMachine.newObject {U K : Type} (v : Views U) (object : Concurrency.TypedSyncRuntime.Object) : M K U Concurrency.TypedSyncRuntime.Ref

Equations

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

def Miri.Interpreter.TypedSyncMachine.getObject {U K : Type} (v : Views U) (ref : Concurrency.TypedSyncRuntime.Ref) : M K U Concurrency.TypedSyncRuntime.Object

Equations

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

def Miri.Interpreter.TypedSyncMachine.putObject {U K : Type} (v : Views U) (ref : Concurrency.TypedSyncRuntime.Ref) (value : Concurrency.TypedSyncRuntime.Object) : M K U Unit

Equations

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

def Miri.Interpreter.TypedSyncMachine.owns {U K : Type} (v : Views U) (token : Nat) : M K U Bool

Equations

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

def Miri.Interpreter.TypedSyncMachine.register {U K : Type} (v : Views U) (capture : Concurrency.TypedSyncRuntime.Capture) : M K U Nat

Equations

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

def Miri.Interpreter.TypedSyncMachine.take {U K : Type} (v : Views U) (token : Nat) : M K U Concurrency.TypedSyncRuntime.Capture

Equations

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

def Miri.Interpreter.TypedSyncMachine.bind {U K : Type} (v : Views U) (base : Concurrency.TypedSyncRuntime.Hooks (State K U)) : Concurrency.TypedSyncRuntime.Hooks (State K U)

Source physical state and ownership are closed here. Remaining fields in base are the concrete scalar/error writes and source configuration; they are not an object store, callback evaluator, or synthetic clock.

Equations

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

structure Miri.Interpreter.TypedSyncMachine.Effects (S : Type) : Type

Actual compiler/OS writes and immutable source configuration. No callback or object-store fields are requested from the production caller.

• handler : Concurrency.SyncClockHandler
• usizeBits : Nat
• communicate : Bool
• writeScalar : Int32 → Concurrency.TypedSyncRuntime.Dest → EStateM StepError S Unit
• writeInt : Int → Concurrency.TypedSyncRuntime.Dest → EStateM StepError S Unit
• errnoNegOne : String → Concurrency.TypedSyncRuntime.Dest → EStateM StepError S Unit
• windowsTrue : EStateM StepError S Int32
• windowsFalse : EStateM StepError S Int32
• windowsTimeoutError : EStateM StepError S Unit

def Miri.Interpreter.TypedSyncMachine.typed {U K : Type} (v : Views U) (e : Effects (State K U)) : Concurrency.TypedSyncRuntime.Hooks (State K U)

Equations

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

def Miri.Interpreter.TypedSyncMachine.runtime {U K : Type} (v : Views U) (e : Effects (State K U)) : Concurrency.SyncRuntime.Hooks (State K U) Concurrency.TypedSyncRuntime.Ref Int32 Concurrency.TypedSyncRuntime.Dest

Production SyncRuntime dictionary: its backend variant contains no Registry S, dummy getter, or no-op setter. All source callbacks use the typed interpreter.

Equations

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

def Miri.Interpreter.TypedSyncMachine.initOnce {U K : Type} (v : Views U) (e : Effects (State K U)) : Concurrency.InitOnce.Hooks (State K U) Concurrency.TypedSyncRuntime.Ref Int32 Concurrency.TypedSyncRuntime.Dest

Equations

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