Canonical Place ↔ Miri machine access. Vector-clock and Tree Borrows rules are actual operations; address/global/weak-memory/synchronization policies are required leaves. Typed failures survive the legacy string memory-hook boundary.

@[reducible, inline]

abbrev Miri.Interpreter.PlaceMachine.Machine (K User : Type) : Type

Equations

• Miri.Interpreter.PlaceMachine.Machine K User = Miri.Interpreter.MachineHooks.MachineState K User

@[reducible, inline]

abbrev Miri.Interpreter.PlaceMachine.State (K User : Type) : Type

Equations

• Miri.Interpreter.PlaceMachine.State K User = Miri.Interpreter.MachineHooks.State K User

@[reducible, inline]

abbrev Miri.Interpreter.PlaceMachine.M (K User A : Type) : Type

Equations

• Miri.Interpreter.PlaceMachine.M K User A = Miri.Interpreter.MachineHooks.M K User A

@[reducible, inline]

abbrev Miri.Interpreter.PlaceMachine.MachineM (K User A : Type) : Type

Equations

• Miri.Interpreter.PlaceMachine.MachineM K User A = EStateM Miri.Interpreter.StepError (Miri.Interpreter.PlaceMachine.Machine K User) A

structure Miri.Interpreter.PlaceMachine.AccessState (K User : Type) : Type

• machine : Machine K User
• pendingError : Option StepError

structure Miri.Interpreter.PlaceMachine.AccessConfig (K User : Type) : Type

Policies outside ordinary non-atomic VClock/Tree-Borrows access. Diagnostic runs before races; weakMemoryWrite after successful race write; syncAccess after successful Tree Borrows. Hooks may change User/external indices, not live bytes; the allocation-access layer owns byte/extra commits. Disabled policies must be chosen explicitly by the machine configuration.

• runtime : ABI.RuntimeTargetDataLayout
• ghostMode : Bool
• globalKind : Option K
• globalHooks : Memory.GlobalAllocationHooks Memory.Provenance TreeBorrows.BorrowTree K (AccessState K User)
• dynamicLayout : DynamicLayoutResolver Memory.Provenance TreeBorrows.BorrowTree K (AccessState K User)
• resolvePointer : Memory.MemoryState Memory.Provenance TreeBorrows.BorrowTree K → Memory.Pointer (Option Memory.Provenance) → Int → MachineM K User (Except UInt64 (Memory.ResolvedPointer Memory.ProvenanceExtra))
• beforeAllocationAccess : Memory.AllocId → MachineM K User Unit
• diagnostic : Bool → Memory.AllocId → Memory.AllocRange → MachineM K User Unit
• weakMemoryWrite : Memory.AllocId → Memory.AllocRange → MachineM K User Unit
• syncAccess : Bool → Memory.AllocId → Memory.AllocRange → MachineM K User Unit
• retainTouched : Machine K User → Option (Memory.AllocationAccessRef Memory.Provenance TreeBorrows.BorrowTree) → Machine K User
• memoryError : MemoryOperandError → StepError

def Miri.Interpreter.PlaceMachine.memoryAccess {K User : Type} (config : AccessConfig K User) (write : Bool) (state : AccessState K User) (tree : TreeBorrows.BorrowTree) (allocId : Memory.AllocId) (provenance : Memory.ProvenanceExtra) (range : Memory.AllocRange) : Memory.AllocationExtraHookResult (AccessState K User) TreeBorrows.BorrowTree

Source before_memory_read/write order, retaining the tree after access UB and prior clock/weak-memory effects on every failure.

Equations

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

def Miri.Interpreter.PlaceMachine.accessHooks {K User : Type} (config : AccessConfig K User) : Memory.AllocationAccessHooks Memory.Provenance TreeBorrows.BorrowTree K (AccessState K User) Memory.ProvenanceExtra

Equations

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

def Miri.Interpreter.PlaceMachine.readImmediate {K User : Type} [DecidableEq K] (config : AccessConfig K User) (operand : OpTy Memory.Provenance) : M K User (RvalueImmTy Memory.Provenance)

Equations

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

def Miri.Interpreter.PlaceMachine.readRaw {K User : Type} [DecidableEq K] (config : AccessConfig K User) (operand : OpTy Memory.Provenance) : M K User (ImmediateOrPlace Memory.Provenance)

Equations

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

def Miri.Interpreter.PlaceMachine.writeMemory {K User : Type} [DecidableEq K] (config : AccessConfig K User) (willValidate : MemoryOperandLayout → Bool) (value : Immediate Memory.Provenance) (place : MPlaceTy Memory.Provenance) : M K User Unit

Equations

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

theorem Miri.Interpreter.PlaceMachine.writeMemory_zero_uninit {K User : Type} [DecidableEq K] (config : AccessConfig K User) (later : MemoryOperandLayout → Bool) (place : MPlaceTy Memory.Provenance) (pointer : Memory.Pointer (Option Memory.Provenance)) (ty : Option Nat) (pointerSize : ABI.Size) (unitLayout : localMemoryLayout place.layout = { size := ABI.Size.ZERO, align := ABI.Align.ONE, backendRepr := ABI.BackendRepr.Memory, canonicalType := ty }) (placeMemory : place.mplace = { ptr := pointer, metadata := MemPlaceMeta.none, misaligned := none }) (pointerMetadata : config.runtime.pointerSizeIn config.runtime.defaultAddressSpace = Except.ok pointerSize) (retain : ∀ (machine : Machine K User), config.retainTouched machine none = machine) (state : State K User) : writeMemory config later Immediate.uninit place state = EStateM.Result.ok () state

The canonical zero-sized unit write preserves the entire machine and stack. No allocation lookup, pointer resolution or permission transition is assumed. The layout and pointer-size premises concern compiler/target data only.

def Miri.Interpreter.PlaceMachine.initStackExtra {K User : Type} (allocationTail : Memory.AllocId → ABI.Size → ABI.Align → MachineM K User Unit) (id : Memory.AllocId) (size : ABI.Size) (align : ABI.Align) : MachineM K User TreeBorrows.BorrowTree

Source stack init_allocation: root borrow tree before allocation race state. Stack allocation time comes from the active thread; historical local clocks are transferred by afterLocalMovedToMemory later. Span-only diagnostic and weak-memory construction leaves remain explicit.

Equations

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

structure Miri.Interpreter.PlaceMachine.AllocationConfig (K User : Type) : Type

• maximumObjectSize : ABI.Size
• zeroedStorage : ABI.Size → ABI.Align → Option (Array UInt8)
• nativeStorage : Option (ABI.Size → ABI.Align → Memory.AllocInit → M K User (Except Memory.AllocError (Memory.Allocation Memory.Provenance)))
• nativeDrop : Option (Memory.Allocation Memory.Provenance → M K User Unit)
• diagnostic : Memory.AllocId → ABI.Size → ABI.Align → MachineM K User Unit
• allocationTail : Memory.AllocId → ABI.Size → ABI.Align → MachineM K User Unit
• adjustRootAddress : Memory.AllocId → Memory.BorTag → M K User (Memory.Pointer Memory.Provenance)

  Actual address-map allocation with the existing root tag. This must not replace the tag or derive an absolute address from allocation identity.

def Miri.Interpreter.PlaceMachine.allocateStackRaw {K User : Type} [DecidableEq K] (config : AllocationConfig K User) (size : ABI.Size) (align : ABI.Align) : M K User (Memory.Pointer (Option Memory.Provenance))

Actual uninitialized stack allocation, with root/tree/clock effects retained when a later root-address adjustment fails.

Equations

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

def Miri.Interpreter.PlaceMachine.allocateStack {K User : Type} [DecidableEq K] (config : AllocationConfig K User) (layout : LocalLayout) : M K User (MPlaceTy Memory.Provenance)

Typed stack allocation retains the source sized-layout check. Raw temporary buffers use allocateStackRaw directly and require no fabricated compiler type.

Equations

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

structure Miri.Interpreter.PlaceMachine.CompilerHooks (K User C : Type) : Type

• debugAssertions : Bool
• layout : C → MIR.LocalId → M K User LocalLayout
• validationInProgress : M K User Bool
• projection : C → M K User (ProjectionCx Memory.Provenance)
• deref : C → RuntimePlace Memory.Provenance → Bool → M K User (RuntimePlace Memory.Provenance)
• checkPlaceType : C → MIR.Place → RuntimePlace Memory.Provenance → M K User Unit
• memoryOffset : C → MemPlace Memory.Provenance → ABI.Size → OffsetMode → MemPlaceMeta Memory.Provenance → M K User (MemPlace Memory.Provenance)
• debugAbiCheck : Immediate Memory.Provenance → LocalLayout → M K User Unit
• localSpan : MIR.Body → MIR.LocalId → M K User MIR.SpanRef
• enforceValidity : C → LocalLayout → M K User Bool
• validate : C → RuntimePlace Memory.Provenance → M K User Unit
• willValidateMemory : MemoryOperandLayout → Bool

def Miri.Interpreter.PlaceMachine.layoutLocal {K User C : Type} (compiler : CompilerHooks K User C) (choice : C) (id : MIR.LocalId) : M K User LocalLayout

Equations

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

def Miri.Interpreter.PlaceMachine.localToOpCore {K User : Type} (layoutOf : MIR.LocalId → M K User LocalLayout) (validationInProgress : M K User Bool) (id : MIR.LocalId) : M K User (OpTy Memory.Provenance)

Source local read, with layout/cache resolution provided separately from unrelated compiler/place operations. The actual read event remains mandatory.

Equations

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

def Miri.Interpreter.PlaceMachine.localToOp {K User C : Type} (compiler : CompilerHooks K User C) (choice : C) (id : MIR.LocalId) : M K User (OpTy Memory.Provenance)

Equations

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

def Miri.Interpreter.PlaceMachine.placeHooks {K User C : Type} [DecidableEq K] (access : AccessConfig K User) (allocation : AllocationConfig K User) (compiler : CompilerHooks K User C) : PlaceHooks Memory.Provenance (State K User) C MachineHooks.FrameExtra

Equations

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

structure Miri.Interpreter.PlaceMachine.RetagQueries (K User : Type) : Type

Compiler/type/layout preparation remains fallible; the write-uninit stage is supplied by the actual typed memory writer below, including races and TB.

• preparePointerRetag : RvalueImmTy Memory.Provenance → MIR.TyId → TreeBorrows.RetagPolicy.RetagMode → M K User TreeBorrows.RetagPipeline.Request
• reconstructImmediate : RvalueImmTy Memory.Provenance → Option Memory.Provenance → M K User (RvalueImmTy Memory.Provenance)
• preparePlaceProtection : MPlaceTy Memory.Provenance → M K User TreeBorrows.RetagPipeline.Request
• ensureTreeExtra : Memory.AllocId → M K User Unit

def Miri.Interpreter.PlaceMachine.retagHooks {K User : Type} [DecidableEq K] (access : AccessConfig K User) (queries : RetagQueries K User) : MachineHooks.Hooks K User

Equations

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

def Miri.Interpreter.PlaceMachine.bindRvalue {K User C : Type} [DecidableEq K] (base : RvalueHooks Memory.Provenance (State K User) C (RuntimePlace Memory.Provenance)) (access : AccessConfig K User) (allocation : AllocationConfig K User) (compiler : CompilerHooks K User C) (queries : RetagQueries K User) (copy : PlaceCopyHooks Memory.Provenance (State K User) C) (evaluatePlace : C → MIR.Place → Bool → M K User (RuntimePlace Memory.Provenance)) : RvalueHooks Memory.Provenance (State K User) C (RuntimePlace Memory.Provenance)

Bind canonical typed places and actual retag/race hooks to the existing rvalue interpreter. The supplied evaluator is normally PlaceDynamic.evalPlace; operand evaluation/projection, casts and compiler facts stay required in base. No unconditional retag is inserted on raw-pointer or integer copies: the source rvalue dispatcher chooses Default/TwoPhase/Raw/None and its retag trigger.

Equations

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

theorem Miri.Interpreter.PlaceMachine.memoryAccess_fresh_write {K User : Type} (config : AccessConfig K User) (machine : Machine K User) (id : Memory.AllocId) (tag : Memory.BorTag) (size : ABI.Size) (noClocks : machine.dataRace = none) (diagnostic : config.diagnostic true id (Memory.allocRange ABI.Size.ZERO size) machine = EStateM.Result.ok () machine) (weak : config.weakMemoryWrite id (Memory.allocRange ABI.Size.ZERO size) machine = EStateM.Result.ok () machine) (sync : config.syncAccess true id (Memory.allocRange ABI.Size.ZERO size) machine = EStateM.Result.ok () machine) : memoryAccess config true { machine := machine } (TreeBorrows.BorrowTree.new tag size) id (Memory.ProvenanceExtra.concrete tag) (Memory.allocRange ABI.Size.ZERO size) = { state := { machine := machine }, extra := TreeBorrows.BorrowTree.new tag size, outcome := Except.ok () }

Internal stage composition for the fresh allocation's first whole write. The caller discharges diagnostic/weak/sync edges from the current raw machine.

theorem Miri.Interpreter.PlaceMachine.resolvePointer_ok {K User : Type} (config : AccessConfig K User) (memory : Memory.MemoryState Memory.Provenance TreeBorrows.BorrowTree K) (machine : Machine K User) (pointer : Memory.Pointer (Option Memory.Provenance)) (amount : Int) (result : Except UInt64 (Memory.ResolvedPointer Memory.ProvenanceExtra)) (resolved : config.resolvePointer memory pointer amount machine = EStateM.Result.ok result machine) : (accessHooks config).resolvePointer memory { machine := machine } pointer amount = { state := { machine := machine }, outcome := Except.ok result }

An internal exact resolver equation lifted through the production bridge.

theorem Miri.Interpreter.PlaceMachine.writeMemory_of_result {K User : Type} [DecidableEq K] (config : AccessConfig K User) (later : MemoryOperandLayout → Bool) (value : Immediate Memory.Provenance) (place : MPlaceTy Memory.Provenance) (state : State K User) (memory : Memory.MemoryState Memory.Provenance TreeBorrows.BorrowTree K) (touched : Option (Memory.AllocationAccessRef Memory.Provenance TreeBorrows.BorrowTree)) (retain : config.retainTouched = fun (machine : Machine K User) (x : Option (Memory.AllocationAccessRef Memory.Provenance TreeBorrows.BorrowTree)) => machine) (operand : writeImmediateToMplaceNoValidate state.machine.memory { machine := state.machine } value { mplace := place.mplace, layout := localMemoryLayout place.layout } config.runtime config.ghostMode config.globalKind config.globalHooks (accessHooks config) config.dynamicLayout later = { memory := memory, hooks := { machine := state.machine }, touched := touched, outcome := Except.ok () }) : writeMemory config later value place state = EStateM.Result.ok () { stack := state.stack, machine := have __src := state.machine; { memory := memory, borrowTracker := __src.borrowTracker, dataRace := __src.dataRace, threads := __src.threads, raceAllocations := __src.raceAllocations, allocationSpans := __src.allocationSpans, user := __src.user } }

Commit a successful actual operand mutation through the production memory writer; every stack/user field outside memory is retained exactly.