Core atomic intrinsic dispatch plus the Miri VClock/weak-memory pipeline. Physical reads/writes must invoke the full interpreter memory/TB/sync hooks; the restricted Unit-extra AtomicScalarMemory component is not promoted to a complete atomic execution. Every finite permitted choice remains explicit.

inductive Miri.Interpreter.IntrinsicAtomicRmw : Type

• mir (op : MIR.BinOp) (negate : Bool) : IntrinsicAtomicRmw
• min : IntrinsicAtomicRmw
• max : IntrinsicAtomicRmw
• swap : IntrinsicAtomicRmw

def Miri.Interpreter.instDecidableEqIntrinsicAtomicRmw.decEq (x✝ x✝¹ : IntrinsicAtomicRmw) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqIntrinsicAtomicRmw.decEq (Miri.Interpreter.IntrinsicAtomicRmw.mir op negate) Miri.Interpreter.IntrinsicAtomicRmw.min = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntrinsicAtomicRmw.decEq (Miri.Interpreter.IntrinsicAtomicRmw.mir op negate) Miri.Interpreter.IntrinsicAtomicRmw.max = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntrinsicAtomicRmw.decEq (Miri.Interpreter.IntrinsicAtomicRmw.mir op negate) Miri.Interpreter.IntrinsicAtomicRmw.swap = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntrinsicAtomicRmw.decEq Miri.Interpreter.IntrinsicAtomicRmw.min (Miri.Interpreter.IntrinsicAtomicRmw.mir op negate) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntrinsicAtomicRmw.decEq Miri.Interpreter.IntrinsicAtomicRmw.min Miri.Interpreter.IntrinsicAtomicRmw.min = isTrue ⋯
• Miri.Interpreter.instDecidableEqIntrinsicAtomicRmw.decEq Miri.Interpreter.IntrinsicAtomicRmw.max (Miri.Interpreter.IntrinsicAtomicRmw.mir op negate) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntrinsicAtomicRmw.decEq Miri.Interpreter.IntrinsicAtomicRmw.max Miri.Interpreter.IntrinsicAtomicRmw.max = isTrue ⋯
• Miri.Interpreter.instDecidableEqIntrinsicAtomicRmw.decEq Miri.Interpreter.IntrinsicAtomicRmw.swap (Miri.Interpreter.IntrinsicAtomicRmw.mir op negate) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntrinsicAtomicRmw.decEq Miri.Interpreter.IntrinsicAtomicRmw.swap Miri.Interpreter.IntrinsicAtomicRmw.swap = isTrue ⋯

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqIntrinsicAtomicRmw : DecidableEq IntrinsicAtomicRmw

Equations

• Miri.Interpreter.instDecidableEqIntrinsicAtomicRmw = Miri.Interpreter.instDecidableEqIntrinsicAtomicRmw.decEq

@[instance_reducible]

instance Miri.Interpreter.instReprIntrinsicAtomicRmw : Repr IntrinsicAtomicRmw

Equations

• Miri.Interpreter.instReprIntrinsicAtomicRmw = { reprPrec := Miri.Interpreter.instReprIntrinsicAtomicRmw.repr }

def Miri.Interpreter.instReprIntrinsicAtomicRmw.repr : IntrinsicAtomicRmw → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.WeakCasPolicy : Type

• neverFail : WeakCasPolicy
• alwaysFail : WeakCasPolicy
• mayFail : WeakCasPolicy

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqWeakCasPolicy : DecidableEq WeakCasPolicy

Equations

• Miri.Interpreter.instDecidableEqWeakCasPolicy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instReprWeakCasPolicy : Repr WeakCasPolicy

Equations

• Miri.Interpreter.instReprWeakCasPolicy = { reprPrec := Miri.Interpreter.instReprWeakCasPolicy.repr }

def Miri.Interpreter.instReprWeakCasPolicy.repr : WeakCasPolicy → Nat → Std.Format

Equations

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

structure Miri.Interpreter.AtomicLocation : Type

• allocation : Memory.AllocId
• range : Memory.AllocRange

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqAtomicLocation : DecidableEq AtomicLocation

Equations

• Miri.Interpreter.instDecidableEqAtomicLocation = Miri.Interpreter.instDecidableEqAtomicLocation.decEq

def Miri.Interpreter.instDecidableEqAtomicLocation.decEq (x✝ x✝¹ : AtomicLocation) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.Interpreter.instReprAtomicLocation.repr : AtomicLocation → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprAtomicLocation : Repr AtomicLocation

Equations

• Miri.Interpreter.instReprAtomicLocation = { reprPrec := Miri.Interpreter.instReprAtomicLocation.repr }

structure Miri.Interpreter.AtomicAccessHooks (P S C V : Type) : Type

• target : ABI.TargetDataLayout
• getGlobal : S → Option Concurrency.GlobalState
• setGlobal : S → Concurrency.GlobalState → S
• threads : S → Concurrency.ThreadManager
• getAtomic : S → Memory.AllocId → Except StepError (Concurrency.AtomicState (Memory.Scalar P))
• setAtomic : Memory.AllocId → Concurrency.AtomicState (Memory.Scalar P) → RvalueM S Unit
• placeLayout : V → ABI.TyAndLayout MIR.TyId
• placePointer : V → Except StepError (Memory.Pointer (Option P))
• physicalRead : C → V → RvalueM S (RvalueImmTy P)
• physicalWrite : C → Immediate P → V → RvalueM S Unit
• ghostRead : C → V → RvalueM S (Option (Memory.Scalar P))
• checkPointerAlign : C → Memory.Pointer (Option P) → ABI.Align → RvalueM S Unit
• resolveAllocation : C → Memory.Pointer (Option P) → RvalueM S (Memory.AllocId × ABI.Size)
• mutability : C → Memory.AllocId → RvalueM S Memory.Mutability
• scalarOps : ScalarOpsHooks P S C
• loadChoiceRank : C → Nat → RvalueM S Nat
• weakPolicy : WeakCasPolicy
• weakSuccessChoice : C → RvalueM S Bool
• diagnostic : C → Concurrency.WeakMemoryDiagnostic → RvalueM S Unit
• classifyDispatchError : Concurrency.AtomicDispatchError → StepError
• classifyGlobalError : Concurrency.GlobalStateError → StepError

structure Miri.Interpreter.IntrinsicAtomicHooks (P S C V : Type) extends Miri.Interpreter.AtomicAccessHooks P S C V : Type

• target : ABI.TargetDataLayout
• getGlobal : S → Option Concurrency.GlobalState
• setGlobal : S → Concurrency.GlobalState → S
• threads : S → Concurrency.ThreadManager
• getAtomic : S → Memory.AllocId → Except StepError (Concurrency.AtomicState (Memory.Scalar P))
• setAtomic : Memory.AllocId → Concurrency.AtomicState (Memory.Scalar P) → RvalueM S Unit
• placeLayout : V → ABI.TyAndLayout MIR.TyId
• placePointer : V → Except StepError (Memory.Pointer (Option P))
• physicalRead : C → V → RvalueM S (RvalueImmTy P)
• physicalWrite : C → Immediate P → V → RvalueM S Unit
• ghostRead : C → V → RvalueM S (Option (Memory.Scalar P))
• checkPointerAlign : C → Memory.Pointer (Option P) → ABI.Align → RvalueM S Unit
• resolveAllocation : C → Memory.Pointer (Option P) → RvalueM S (Memory.AllocId × ABI.Size)
• mutability : C → Memory.AllocId → RvalueM S Memory.Mutability
• scalarOps : ScalarOpsHooks P S C
• loadChoiceRank : C → Nat → RvalueM S Nat
• weakPolicy : WeakCasPolicy
• weakSuccessChoice : C → RvalueM S Bool
• diagnostic : C → Concurrency.WeakMemoryDiagnostic → RvalueM S Unit
• classifyDispatchError : Concurrency.AtomicDispatchError → StepError
• classifyGlobalError : Concurrency.GlobalStateError → StepError
• orderingConst : C → Nat → RvalueM S Concurrency.AtomicOrdering
• volatileConst : C → Nat → RvalueM S Unit
• derefPointer : C → OpTy P → RvalueM S V
• readImmediate : C → OpTy P → RvalueM S (RvalueImmTy P)
• writeImmediate : C → Immediate P → V → RvalueM S Unit
• returnToBlock : C → Option MIR.BasicBlockId → RvalueM S Unit

@[instance_reducible]

instance Miri.Interpreter.instCoeIntrinsicAtomicHooksAtomicAccessHooks {P S C V : Type} : Coe (IntrinsicAtomicHooks P S C V) (AtomicAccessHooks P S C V)

Equations

• Miri.Interpreter.instCoeIntrinsicAtomicHooksAtomicAccessHooks = { coe := Miri.Interpreter.IntrinsicAtomicHooks.toAtomicAccessHooks }

def Miri.Interpreter.IntrinsicAtomic.allowDataRaces {P S C V A : Type} (h : AtomicAccessHooks P S C V) (action : RvalueM S A) : RvalueM S A

Exact source flag window, including restoration after physical-hook error. Global lenses must view the same global state used by the memory access hooks.

Equations

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

def Miri.Interpreter.IntrinsicAtomic.access {P S C V : Type} (h : AtomicAccessHooks P S C V) (choice : C) (place : V) (kind : Concurrency.AtomicAccessKind) : RvalueM S AtomicLocation

Source atomic_access_check staging: size-derived alignment, pointer alignment, allocation identity and read-only rules. Actual byte hooks follow.

Equations

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

def Miri.Interpreter.IntrinsicAtomic.dispatch {P S C V A : Type} (h : AtomicAccessHooks P S C V) (location : AtomicLocation) (operation : Concurrency.AtomicState (Memory.Scalar P) → Concurrency.ThreadManager → Concurrency.AtomicTransition (Memory.Scalar P) A) : RvalueM S A

Commit post-byte/per-clock mutations even when a later byte or clock fails. The state lens must preserve unrelated memory, provenance and borrow metadata.

Equations

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

def Miri.Interpreter.IntrinsicAtomic.load {P S C V : Type} (h : AtomicAccessHooks P S C V) (choice : C) (place : V) (ordering : Concurrency.AtomicOrdering) : RvalueM S (Memory.Scalar P)

Equations

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

def Miri.Interpreter.IntrinsicAtomic.store {P S C V : Type} (h : AtomicAccessHooks P S C V) (choice : C) (place : V) (value : RvalueImmTy P) (ordering : Concurrency.AtomicOrdering) : RvalueM S Unit

Equations

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

def Miri.Interpreter.IntrinsicAtomic.rmwValue {P S C V : Type} [Memory.PointerProvenance P] (h : AtomicAccessHooks P S C V) (choice : C) (op : IntrinsicAtomicRmw) (left right : RvalueImmTy P) : RvalueM S (RvalueImmTy P)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.IntrinsicAtomic.rmwValue h choice Miri.Interpreter.IntrinsicAtomicRmw.swap left right = pure right

def Miri.Interpreter.IntrinsicAtomic.rmw {P S C V : Type} [Memory.PointerProvenance P] (h : AtomicAccessHooks P S C V) (choice : C) (place : V) (op : IntrinsicAtomicRmw) (operand : RvalueImmTy P) (ordering : Concurrency.AtomicOrdering) : RvalueM S (Memory.Scalar P)

Equations

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

def Miri.Interpreter.IntrinsicAtomic.compareExchange {P S C V : Type} [Memory.PointerProvenance P] (h : AtomicAccessHooks P S C V) (choice : C) (place : V) (expected newValue : RvalueImmTy P) (weak : Bool) (success failure : Concurrency.AtomicOrdering) : RvalueM S (Memory.Scalar P × Bool)

Equations

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

def Miri.Interpreter.IntrinsicAtomic.fence {P S C V : Type} (h : AtomicAccessHooks P S C V) (ordering : Concurrency.AtomicOrdering) (singlethread : Bool) : RvalueM S Unit

Equations

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

def Miri.Interpreter.IntrinsicAtomic.pointerBinary {P S C : Type} [Memory.PointerProvenance P] (target : ABI.TargetDataLayout) (ops : ScalarOpsHooks P S C) (isRaw : C → MIR.TyId → RvalueM S Bool) (usizeLayout : C → RvalueM S (ABI.TyAndLayout MIR.TyId)) (choice : C) (op : MIR.BinOp) (left right : RvalueImmTy P) : RvalueM S (RvalueImmTy P)

Actual Miri operator.rs pointer operations used by atomic pointers. Relative CTFE provenance cannot be substituted for machine addresses. The arithmetic branch keeps the source's usize temporary layout while retaining LHS provenance.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.IntrinsicAtomic.pointerBinary target ops isRaw usizeLayout choice op left right = Miri.Interpreter.IntrinsicAtomic.invalid✝ "unsupported Miri pointer binary operation"

def Miri.Interpreter.IntrinsicAtomic.eval {P S C V : Type} [Memory.PointerProvenance P] (h : IntrinsicAtomicHooks P S C V) (choice : C) (name : String) (args : Array (OpTy P)) (dest : V) (ret : Option MIR.BasicBlockId) : RvalueM S Bool

Ordering generic indexes and volatile-constant evaluation match pinned core atomic.rs. Unknown atomic names preserve the source not-handled result.

Equations

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