Core local-allocation lifecycle transitions from rustc's interpreter memory.rs. Allocation IDs, Miri machine state, pointer lookup, native allocation bytes, memory-copy access checks, and machine deallocation hooks are explicit inputs. State changes performed before a source error are retained.

inductive Miri.Memory.MemoryKind (MachineKind : Type) : Type

• stack {MachineKind : Type} : MemoryKind MachineKind
• callerLocation {MachineKind : Type} : MemoryKind MachineKind
• machine {MachineKind : Type} (kind : MachineKind) : MemoryKind MachineKind

@[instance_reducible]

instance Miri.Memory.instDecidableEqMemoryKind {MachineKind✝ : Type} [DecidableEq MachineKind✝] : DecidableEq (MemoryKind MachineKind✝)

Equations

• Miri.Memory.instDecidableEqMemoryKind = Miri.Memory.instDecidableEqMemoryKind.decEq

def Miri.Memory.instDecidableEqMemoryKind.decEq {MachineKind✝ : Type} [DecidableEq MachineKind✝] (x✝ x✝¹ : MemoryKind MachineKind✝) : Decidable (x✝ = x✝¹)

Equations

• Miri.Memory.instDecidableEqMemoryKind.decEq Miri.Memory.MemoryKind.stack Miri.Memory.MemoryKind.stack = isTrue ⋯
• Miri.Memory.instDecidableEqMemoryKind.decEq Miri.Memory.MemoryKind.stack Miri.Memory.MemoryKind.callerLocation = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryKind.decEq Miri.Memory.MemoryKind.stack (Miri.Memory.MemoryKind.machine kind) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryKind.decEq Miri.Memory.MemoryKind.callerLocation Miri.Memory.MemoryKind.stack = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryKind.decEq Miri.Memory.MemoryKind.callerLocation Miri.Memory.MemoryKind.callerLocation = isTrue ⋯
• Miri.Memory.instDecidableEqMemoryKind.decEq Miri.Memory.MemoryKind.callerLocation (Miri.Memory.MemoryKind.machine kind) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryKind.decEq (Miri.Memory.MemoryKind.machine kind) Miri.Memory.MemoryKind.stack = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryKind.decEq (Miri.Memory.MemoryKind.machine kind) Miri.Memory.MemoryKind.callerLocation = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryKind.decEq (Miri.Memory.MemoryKind.machine a) (Miri.Memory.MemoryKind.machine b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Miri.Memory.instReprMemoryKind.repr {MachineKind✝ : Type} [Repr MachineKind✝] : MemoryKind MachineKind✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprMemoryKind {MachineKind✝ : Type} [Repr MachineKind✝] : Repr (MemoryKind MachineKind✝)

Equations

• Miri.Memory.instReprMemoryKind = { reprPrec := Miri.Memory.instReprMemoryKind.repr }

inductive Miri.Memory.GlobalAllocationKind : Type

• function : GlobalAllocationKind
• vtable : GlobalAllocationKind
• typeId : GlobalAllocationKind
• static : GlobalAllocationKind
• memory : GlobalAllocationKind

@[instance_reducible]

instance Miri.Memory.instDecidableEqGlobalAllocationKind : DecidableEq GlobalAllocationKind

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprGlobalAllocationKind : Repr GlobalAllocationKind

Equations

• Miri.Memory.instReprGlobalAllocationKind = { reprPrec := Miri.Memory.instReprGlobalAllocationKind.repr }

def Miri.Memory.instReprGlobalAllocationKind.repr : GlobalAllocationKind → Nat → Std.Format

Equations

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

inductive Miri.Memory.GlobalAllocationPayload : Type

The source-level shape of a compiler global. Memory contents use CTFE provenance until adjustGlobalAllocation converts them for the selected machine. A static stores its identity and source predicates; its initializer is evaluated only when the source get_global_alloc path is taken.

• memory (allocation : Allocation) : GlobalAllocationPayload
• function : GlobalAllocationPayload
• vtable : GlobalAllocationPayload
• typeId : GlobalAllocationPayload
• static (definition : Nat) (isStatic threadLocal foreignItem : Bool) : GlobalAllocationPayload

structure Miri.Memory.LocalAllocation (Prov Extra MachineKind : Type) : Type

• kind : MemoryKind MachineKind
• allocation : Allocation Prov Extra

structure Miri.Memory.DeadAllocation : Type

• allocId : AllocId
• size : ABI.Size
• align : ABI.Align

@[instance_reducible]

instance Miri.Memory.instDecidableEqDeadAllocation : DecidableEq DeadAllocation

Equations

• Miri.Memory.instDecidableEqDeadAllocation = Miri.Memory.instDecidableEqDeadAllocation.decEq

def Miri.Memory.instDecidableEqDeadAllocation.decEq (x✝ x✝¹ : DeadAllocation) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprDeadAllocation : Repr DeadAllocation

Equations

• Miri.Memory.instReprDeadAllocation = { reprPrec := Miri.Memory.instReprDeadAllocation.repr }

def Miri.Memory.instReprDeadAllocation.repr : DeadAllocation → Nat → Std.Format

Equations

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

structure Miri.Memory.GlobalAllocation : Type

Global allocation metadata is indexed by the runtime rustc AllocId. Exporter graph IDs are canonical graph indices, so imported IDs are kept in a separate explicit map rather than treated as runtime IDs.

• allocId : AllocId
• kind : GlobalAllocationKind
• size : ABI.Size
• align : ABI.Align
• mutability : Mutability
• payload : Option GlobalAllocationPayload

inductive Miri.Memory.AllocationIdError : Type

• exhausted : AllocationIdError
• alreadyIssued (allocId : AllocId) : AllocationIdError

def Miri.Memory.instDecidableEqAllocationIdError.decEq (x✝ x✝¹ : AllocationIdError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.instDecidableEqAllocationIdError.decEq Miri.Memory.AllocationIdError.exhausted Miri.Memory.AllocationIdError.exhausted = isTrue ⋯
• Miri.Memory.instDecidableEqAllocationIdError.decEq Miri.Memory.AllocationIdError.exhausted (Miri.Memory.AllocationIdError.alreadyIssued allocId) = isFalse ⋯
• Miri.Memory.instDecidableEqAllocationIdError.decEq (Miri.Memory.AllocationIdError.alreadyIssued allocId) Miri.Memory.AllocationIdError.exhausted = isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instDecidableEqAllocationIdError : DecidableEq AllocationIdError

Equations

• Miri.Memory.instDecidableEqAllocationIdError = Miri.Memory.instDecidableEqAllocationIdError.decEq

@[instance_reducible]

instance Miri.Memory.instReprAllocationIdError : Repr AllocationIdError

Equations

• Miri.Memory.instReprAllocationIdError = { reprPrec := Miri.Memory.instReprAllocationIdError.repr }

def Miri.Memory.instReprAllocationIdError.repr : AllocationIdError → Nat → Std.Format

Equations

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

inductive Miri.Memory.MemoryMetadataError : Type

• duplicateExportId (exportId : Nat) : MemoryMetadataError
• duplicateRuntimeId (allocId : AllocId) : MemoryMetadataError
• globalIdAlreadyPresent (allocId : AllocId) : MemoryMetadataError
• missingExportId (exportId : Nat) : MemoryMetadataError

@[instance_reducible]

instance Miri.Memory.instDecidableEqMemoryMetadataError : DecidableEq MemoryMetadataError

Equations

• Miri.Memory.instDecidableEqMemoryMetadataError = Miri.Memory.instDecidableEqMemoryMetadataError.decEq

def Miri.Memory.instDecidableEqMemoryMetadataError.decEq (x✝ x✝¹ : MemoryMetadataError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.instDecidableEqMemoryMetadataError.decEq (Miri.Memory.MemoryMetadataError.duplicateExportId exportId) (Miri.Memory.MemoryMetadataError.duplicateRuntimeId allocId) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryMetadataError.decEq (Miri.Memory.MemoryMetadataError.duplicateExportId exportId) (Miri.Memory.MemoryMetadataError.globalIdAlreadyPresent allocId) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryMetadataError.decEq (Miri.Memory.MemoryMetadataError.duplicateExportId exportId) (Miri.Memory.MemoryMetadataError.missingExportId exportId_1) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryMetadataError.decEq (Miri.Memory.MemoryMetadataError.duplicateRuntimeId allocId) (Miri.Memory.MemoryMetadataError.duplicateExportId exportId) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryMetadataError.decEq (Miri.Memory.MemoryMetadataError.duplicateRuntimeId allocId) (Miri.Memory.MemoryMetadataError.globalIdAlreadyPresent allocId_1) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryMetadataError.decEq (Miri.Memory.MemoryMetadataError.duplicateRuntimeId allocId) (Miri.Memory.MemoryMetadataError.missingExportId exportId) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryMetadataError.decEq (Miri.Memory.MemoryMetadataError.globalIdAlreadyPresent allocId) (Miri.Memory.MemoryMetadataError.duplicateExportId exportId) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryMetadataError.decEq (Miri.Memory.MemoryMetadataError.globalIdAlreadyPresent allocId) (Miri.Memory.MemoryMetadataError.duplicateRuntimeId allocId_1) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryMetadataError.decEq (Miri.Memory.MemoryMetadataError.globalIdAlreadyPresent allocId) (Miri.Memory.MemoryMetadataError.missingExportId exportId) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryMetadataError.decEq (Miri.Memory.MemoryMetadataError.missingExportId exportId) (Miri.Memory.MemoryMetadataError.duplicateExportId exportId_1) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryMetadataError.decEq (Miri.Memory.MemoryMetadataError.missingExportId exportId) (Miri.Memory.MemoryMetadataError.duplicateRuntimeId allocId) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryMetadataError.decEq (Miri.Memory.MemoryMetadataError.missingExportId exportId) (Miri.Memory.MemoryMetadataError.globalIdAlreadyPresent allocId) = isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instReprMemoryMetadataError : Repr MemoryMetadataError

Equations

• Miri.Memory.instReprMemoryMetadataError = { reprPrec := Miri.Memory.instReprMemoryMetadataError.repr }

def Miri.Memory.instReprMemoryMetadataError.repr : MemoryMetadataError → Nat → Std.Format

Equations

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

inductive Miri.Memory.GlobalAccessError : Type

• notFound (allocId : AllocId) : GlobalAccessError
• dereferenceFunctionPointer (allocId : AllocId) : GlobalAccessError
• dereferenceVTablePointer (allocId : AllocId) : GlobalAccessError
• dereferenceTypeIdPointer (allocId : AllocId) : GlobalAccessError
• staticNotAStatic (allocId : AllocId) (definition : Nat) : GlobalAccessError
• threadLocalStatic (allocId : AllocId) (definition : Nat) : GlobalAccessError
• unsupportedExternStatic (allocId : AllocId) (definition : Nat) : GlobalAccessError
• payloadUnavailable (allocId : AllocId) : GlobalAccessError
• payloadKindMismatch (allocId : AllocId) (kind payloadKind : GlobalAllocationKind) : GlobalAccessError
• hookFailure (hook message : String) : GlobalAccessError

def Miri.Memory.instDecidableEqGlobalAccessError.decEq (x✝ x✝¹ : GlobalAccessError) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.instDecidableEqGlobalAccessError : DecidableEq GlobalAccessError

Equations

• Miri.Memory.instDecidableEqGlobalAccessError = Miri.Memory.instDecidableEqGlobalAccessError.decEq

@[instance_reducible]

instance Miri.Memory.instReprGlobalAccessError : Repr GlobalAccessError

Equations

• Miri.Memory.instReprGlobalAccessError = { reprPrec := Miri.Memory.instReprGlobalAccessError.repr }

def Miri.Memory.instReprGlobalAccessError.repr : GlobalAccessError → Nat → Std.Format

Equations

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

inductive Miri.Memory.MemoryAccessError : Type

• globalAccess (reason : GlobalAccessError) : MemoryAccessError
• allocationLookup (reason : AllocationLookupError) : MemoryAccessError
• readOnlyAllocation (allocId : AllocId) : MemoryAccessError
• missingGlobalMachineKind (allocId : AllocId) : MemoryAccessError

@[instance_reducible]

instance Miri.Memory.instDecidableEqMemoryAccessError : DecidableEq MemoryAccessError

Equations

• Miri.Memory.instDecidableEqMemoryAccessError = Miri.Memory.instDecidableEqMemoryAccessError.decEq

def Miri.Memory.instDecidableEqMemoryAccessError.decEq (x✝ x✝¹ : MemoryAccessError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.instDecidableEqMemoryAccessError.decEq (Miri.Memory.MemoryAccessError.globalAccess a) (Miri.Memory.MemoryAccessError.globalAccess b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Memory.instDecidableEqMemoryAccessError.decEq (Miri.Memory.MemoryAccessError.globalAccess reason) (Miri.Memory.MemoryAccessError.allocationLookup reason_1) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryAccessError.decEq (Miri.Memory.MemoryAccessError.globalAccess reason) (Miri.Memory.MemoryAccessError.readOnlyAllocation allocId) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryAccessError.decEq (Miri.Memory.MemoryAccessError.globalAccess reason) (Miri.Memory.MemoryAccessError.missingGlobalMachineKind allocId) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryAccessError.decEq (Miri.Memory.MemoryAccessError.allocationLookup reason) (Miri.Memory.MemoryAccessError.globalAccess reason_1) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryAccessError.decEq (Miri.Memory.MemoryAccessError.allocationLookup reason) (Miri.Memory.MemoryAccessError.readOnlyAllocation allocId) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryAccessError.decEq (Miri.Memory.MemoryAccessError.allocationLookup reason) (Miri.Memory.MemoryAccessError.missingGlobalMachineKind allocId) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryAccessError.decEq (Miri.Memory.MemoryAccessError.readOnlyAllocation allocId) (Miri.Memory.MemoryAccessError.globalAccess reason) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryAccessError.decEq (Miri.Memory.MemoryAccessError.readOnlyAllocation allocId) (Miri.Memory.MemoryAccessError.allocationLookup reason) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryAccessError.decEq (Miri.Memory.MemoryAccessError.readOnlyAllocation allocId) (Miri.Memory.MemoryAccessError.missingGlobalMachineKind allocId_1) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryAccessError.decEq (Miri.Memory.MemoryAccessError.missingGlobalMachineKind allocId) (Miri.Memory.MemoryAccessError.globalAccess reason) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryAccessError.decEq (Miri.Memory.MemoryAccessError.missingGlobalMachineKind allocId) (Miri.Memory.MemoryAccessError.allocationLookup reason) = isFalse ⋯
• Miri.Memory.instDecidableEqMemoryAccessError.decEq (Miri.Memory.MemoryAccessError.missingGlobalMachineKind allocId) (Miri.Memory.MemoryAccessError.readOnlyAllocation allocId_1) = isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instReprMemoryAccessError : Repr MemoryAccessError

Equations

• Miri.Memory.instReprMemoryAccessError = { reprPrec := Miri.Memory.instReprMemoryAccessError.repr }

def Miri.Memory.instReprMemoryAccessError.repr : MemoryAccessError → Nat → Std.Format

Equations

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

inductive Miri.Memory.LiveAllocationInfoError : Type

• lookup (reason : AllocationLookupError) : LiveAllocationInfoError
• useAfterFree (allocId : AllocId) (message : CheckInAllocMsg) : LiveAllocationInfoError

def Miri.Memory.instDecidableEqLiveAllocationInfoError.decEq (x✝ x✝¹ : LiveAllocationInfoError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.instDecidableEqLiveAllocationInfoError.decEq (Miri.Memory.LiveAllocationInfoError.lookup reason) (Miri.Memory.LiveAllocationInfoError.useAfterFree allocId message) = isFalse ⋯
• Miri.Memory.instDecidableEqLiveAllocationInfoError.decEq (Miri.Memory.LiveAllocationInfoError.useAfterFree allocId message) (Miri.Memory.LiveAllocationInfoError.lookup reason) = isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instDecidableEqLiveAllocationInfoError : DecidableEq LiveAllocationInfoError

Equations

• Miri.Memory.instDecidableEqLiveAllocationInfoError = Miri.Memory.instDecidableEqLiveAllocationInfoError.decEq

@[instance_reducible]

instance Miri.Memory.instReprLiveAllocationInfoError : Repr LiveAllocationInfoError

Equations

• Miri.Memory.instReprLiveAllocationInfoError = { reprPrec := Miri.Memory.instReprLiveAllocationInfoError.repr }

def Miri.Memory.instReprLiveAllocationInfoError.repr : LiveAllocationInfoError → Nat → Std.Format

Equations

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

structure Miri.Memory.MemoryState (Prov Extra MachineKind : Type) : Type

• nextAllocId : UInt64

  Mirrors rustc's AllocMap::next_id, which starts at one and increments monotonically for every reserved local or imported-global allocation.

• idSupplyExhausted : Bool
• issuedIdTable : Miri.Memory.KeyedArray UInt64 Miri.Memory.AllocId fun (id : Miri.Memory.AllocId) => id.value
• live : Array (AllocId × LocalAllocation Prov Extra MachineKind)
• dead : Array DeadAllocation
• globalTable : Miri.Memory.KeyedArray UInt64 Miri.Memory.GlobalAllocation fun (global : Miri.Memory.GlobalAllocation) => global.allocId.value
• importedGlobalTable : Miri.Memory.KeyedArray Nat (Nat × Miri.Memory.AllocId) Prod.fst
• importedGlobalRuntimeTable : Miri.Memory.KeyedArray UInt64 (UInt64 × Nat) Prod.fst
• extraFnPtrTable : Miri.Memory.KeyedArray UInt64 Miri.Memory.AllocId fun (id : Miri.Memory.AllocId) => id.value
• vaListTable : Miri.Memory.KeyedArray UInt64 Miri.Memory.AllocId fun (id : Miri.Memory.AllocId) => id.value
• byteGlobalKeys : Array (Array UInt8 × Fin 32 × AllocId)

  TCX global byte dedup keys, sharing this allocation supply. Imported compiler identities are seeded only from exact salt-query evidence.

• byteGlobalKeysReady : Bool
• sourceAllocIdWorldActive : Bool

  Optional exact post-export TCX source-number world. Runtime IDs remain dense; this crosswalk retains raw rustc identities for diagnostics.

• sourceAllocIdNext : UInt64
• sourceAllocIdExhausted : Bool
• sourceAllocIdByRuntimeTable : Miri.Memory.KeyedArray UInt64 (Miri.Memory.AllocId × UInt64) fun (pair : Miri.Memory.AllocId × UInt64) => pair.fst.value
• runtimeBySourceAllocIdTable : Miri.Memory.KeyedArray UInt64 (UInt64 × Miri.Memory.AllocId) Prod.fst
• opaqueSourceGlobalIds : Array UInt64
• sourceByteImageFamilyComplete : Bool

inductive Miri.Memory.MemoryLifecycleError : Type

• allocation (error : AllocError) : MemoryLifecycleError
• allocationIdError (error : AllocationIdError) : MemoryLifecycleError
• metadataError (error : MemoryMetadataError) : MemoryLifecycleError
• hookFailure (hook message : String) : MemoryLifecycleError
• allocationTooLarge (size maximum : ABI.Size) : MemoryLifecycleError
• allocationNotLocal (allocId : AllocId) : MemoryLifecycleError
• dynamicallyAllocatingGlobal : MemoryLifecycleError
• danglingPointer (address : UInt64) : MemoryLifecycleError
• nonzeroAllocationOffset (operation : String) (allocId : AllocId) (offset : ABI.Size) : MemoryLifecycleError
• globalAllocationDeallocation (allocId : AllocId) (kind : GlobalAllocationKind) : MemoryLifecycleError
• useAfterFree (allocId : AllocId) : MemoryLifecycleError
• immutableAllocation (allocId : AllocId) : MemoryLifecycleError
• memoryKindMismatch (allocId : AllocId) : MemoryLifecycleError
• layoutMismatch (allocId : AllocId) (actualSize requestedSize : ABI.Size) (actualAlign requestedAlign : ABI.Align) : MemoryLifecycleError
• duplicateDeadAllocation (allocId : AllocId) : MemoryLifecycleError

def Miri.Memory.instDecidableEqMemoryLifecycleError.decEq (x✝ x✝¹ : MemoryLifecycleError) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.instDecidableEqMemoryLifecycleError : DecidableEq MemoryLifecycleError

Equations

• Miri.Memory.instDecidableEqMemoryLifecycleError = Miri.Memory.instDecidableEqMemoryLifecycleError.decEq

def Miri.Memory.instReprMemoryLifecycleError.repr : MemoryLifecycleError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprMemoryLifecycleError : Repr MemoryLifecycleError

Equations

• Miri.Memory.instReprMemoryLifecycleError = { reprPrec := Miri.Memory.instReprMemoryLifecycleError.repr }

@[instance_reducible]

instance Miri.Memory.instToStringGlobalAllocationKind : ToString GlobalAllocationKind

Equations

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

@[instance_reducible]

instance Miri.Memory.instToStringAllocationIdError : ToString AllocationIdError

Equations

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

@[instance_reducible]

instance Miri.Memory.instToStringMemoryMetadataError : ToString MemoryMetadataError

Equations

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

def Miri.Memory.MemoryState.issuedIds {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) : Array AllocId

Equations

• state.issuedIds = (Miri.Memory.MemoryState.issuedIdTable✝ state).toArray

def Miri.Memory.MemoryState.globals {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) : Array GlobalAllocation

Equations

• state.globals = (Miri.Memory.MemoryState.globalTable✝ state).toArray

def Miri.Memory.MemoryState.importedGlobalIds {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) : Array (Nat × AllocId)

Equations

• state.importedGlobalIds = (Miri.Memory.MemoryState.importedGlobalTable✝ state).toArray

def Miri.Memory.MemoryState.extraFnPtrIds {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) : Array AllocId

Equations

• state.extraFnPtrIds = (Miri.Memory.MemoryState.extraFnPtrTable✝ state).toArray

def Miri.Memory.MemoryState.vaListIds {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) : Array AllocId

Equations

• state.vaListIds = (Miri.Memory.MemoryState.vaListTable✝ state).toArray

def Miri.Memory.MemoryState.sourceAllocIdByRuntime {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) : Array (AllocId × UInt64)

Equations

• state.sourceAllocIdByRuntime = (Miri.Memory.MemoryState.sourceAllocIdByRuntimeTable✝ state).toArray

def Miri.Memory.MemoryState.runtimeBySourceAllocId {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) : Array (UInt64 × AllocId)

Equations

• state.runtimeBySourceAllocId = (Miri.Memory.MemoryState.runtimeBySourceAllocIdTable✝ state).toArray

def Miri.Memory.MemoryState.pushGlobal {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (entry : GlobalAllocation) : MemoryState Prov Extra MachineKind

Equations

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

def Miri.Memory.MemoryState.hasIssuedId {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (id : AllocId) : Bool

Equations

• state.hasIssuedId id = (Miri.Memory.MemoryState.issuedIdTable✝ state).contains id.value

def Miri.Memory.MemoryState.hasGlobalId {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (id : AllocId) : Bool

Equations

• state.hasGlobalId id = (Miri.Memory.MemoryState.globalTable✝ state).contains id.value

def Miri.Memory.MemoryState.hasImportedRuntimeId {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (id : AllocId) : Bool

Equations

• state.hasImportedRuntimeId id = (Miri.Memory.MemoryState.importedGlobalRuntimeTable✝ state).contains id.value

def Miri.Memory.MemoryState.importedGraphIdForRuntime? {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (id : AllocId) : Option Nat

Equations

• state.importedGraphIdForRuntime? id = Option.map Prod.snd ((Miri.Memory.MemoryState.importedGlobalRuntimeTable✝ state).find? id.value)

def Miri.Memory.MemoryState.hasExtraFunctionId {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (id : AllocId) : Bool

Equations

• state.hasExtraFunctionId id = (Miri.Memory.MemoryState.extraFnPtrTable✝ state).contains id.value

def Miri.Memory.MemoryState.hasVaListId {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (id : AllocId) : Bool

Equations

• state.hasVaListId id = (Miri.Memory.MemoryState.vaListTable✝ state).contains id.value

def Miri.Memory.MemoryState.mapGlobals {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (f : GlobalAllocation → GlobalAllocation) : MemoryState Prov Extra MachineKind

Equations

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

def Miri.Memory.MemoryState.setGlobalPayload {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (id : AllocId) (payload : GlobalAllocationPayload) : MemoryState Prov Extra MachineKind

Replace payloads on every ordered row sharing a runtime allocation ID, matching mapGlobals semantics while using the certified ID index.

Equations

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

def Miri.Memory.MemoryState.setGlobalEntries {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (entries : Array GlobalAllocation) : MemoryState Prov Extra MachineKind

Array-based metadata import for callers constructing a standalone memory state. It preserves duplicate rows and source order while rebuilding the certified lookup index.

Equations

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

def Miri.Memory.MemoryState.setIssuedIds {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (ids : Array AllocId) : MemoryState Prov Extra MachineKind

Equations

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

def Miri.Memory.MemoryState.setImportedGlobalIds {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (entries : Array (Nat × AllocId)) : MemoryState Prov Extra MachineKind

Equations

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

def Miri.Memory.MemoryState.setExtraFunctionIds {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (ids : Array AllocId) : MemoryState Prov Extra MachineKind

Equations

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

def Miri.Memory.MemoryState.setVaListIds {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (ids : Array AllocId) : MemoryState Prov Extra MachineKind

Equations

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

def Miri.Memory.MemoryState.setSourceAllocIdCrosswalks {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (byRuntime : Array (AllocId × UInt64)) (bySource : Array (UInt64 × AllocId)) : MemoryState Prov Extra MachineKind

Equations

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

def Miri.Memory.MemoryState.empty {Prov Extra MachineKind : Type} : MemoryState Prov Extra MachineKind

Equations

• Miri.Memory.MemoryState.empty = { }

def Miri.Memory.MemoryState.reserveAllocId {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) : MemoryState Prov Extra MachineKind × Except AllocationIdError AllocId

AllocMap::reserve uses an AtomicU64 starting at one and fetch_add. The returned ID is consumed before later machine hooks run. A zero value reifies the source's NonZero::new(...).unwrap() exhaustion panic; the state is marked exhausted so a caller cannot continue after that source-fatal path.

Equations

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

def Miri.Memory.MemoryState.sourceAllocIdForRuntime? {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (id : AllocId) : Option UInt64

Equations

• state.sourceAllocIdForRuntime? id = Option.map Prod.snd ((Miri.Memory.MemoryState.sourceAllocIdByRuntimeTable✝ state).find? id.value)

def Miri.Memory.MemoryState.runtimeForSourceAllocId? {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (sourceId : UInt64) : Option AllocId

Equations

• state.runtimeForSourceAllocId? sourceId = Option.map Prod.snd ((Miri.Memory.MemoryState.runtimeBySourceAllocIdTable✝ state).find? sourceId)

def Miri.Memory.MemoryState.findGlobal? {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (id : AllocId) : Option GlobalAllocation

Equations

• state.findGlobal? id = (Miri.Memory.MemoryState.globalTable✝ state).find? id.value

def Miri.Memory.MemoryState.globalsForId {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (id : AllocId) : Array GlobalAllocation

Equations

• state.globalsForId id = (Miri.Memory.MemoryState.globalTable✝ state).valuesFor id.value

def Miri.Memory.MemoryState.runtimeIdForExport? {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (exportId : Nat) : Option AllocId

Equations

• state.runtimeIdForExport? exportId = Option.map Prod.snd ((Miri.Memory.MemoryState.importedGlobalTable✝ state).find? exportId)

def Miri.Memory.MemoryState.hasFunctionPointer {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (id : AllocId) : Bool

Equations

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

def Miri.Memory.MemoryState.isAllocLive {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (id : AllocId) : Bool

Equations

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

def Miri.Memory.MemoryState.registerExtraFunction {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (id : AllocId) : MemoryState Prov Extra MachineKind

Equations

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

def Miri.Memory.MemoryState.registerVaList {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (id : AllocId) : MemoryState Prov Extra MachineKind

Equations

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

def Miri.Memory.MemoryState.getAllocInfo {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (id : AllocId) : Except AllocationLookupError AllocationInfo

Source get_alloc_info precedence: local bytes, function values, va-lists, compiler globals, then dead-allocation metadata. Missing metadata is an explicit lookup error instead of an unchecked map expectation.

Equations

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

def Miri.Memory.MemoryState.getLiveAllocSizeAndAlign {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (id : AllocId) (message : CheckInAllocMsg) : Except LiveAllocationInfoError (ABI.Size × ABI.Align)

Source get_live_alloc_size_and_align, with both absent metadata and a dead allocation distinguished explicitly.

Equations

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

def Miri.Memory.MemoryState.setLiveAllocation {MachineKind Prov Extra : Type} [DecidableEq MachineKind] (state : MemoryState Prov Extra MachineKind) (id : AllocId) (allocation : Allocation Prov Extra) : Except AllocationLookupError (MemoryState Prov Extra MachineKind)

Equations

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

theorem Miri.Memory.MemoryState.setLiveAllocation_of_find {MachineKind Prov Extra : Type} [DecidableEq MachineKind] (state : MemoryState Prov Extra MachineKind) (id : AllocId) (entry : LocalAllocation Prov Extra MachineKind) (allocation : Allocation Prov Extra) (present : Array.find? (fun (row : AllocId × LocalAllocation Prov Extra MachineKind) => row.fst == id) state.live = some (id, entry)) : state.setLiveAllocation id allocation = Except.ok { nextAllocId := state.nextAllocId, idSupplyExhausted := state.idSupplyExhausted, issuedIdTable := Miri.Memory.MemoryState.issuedIdTable✝ state, live := (Array.filter (fun (row : AllocId × LocalAllocation Prov Extra MachineKind) => row.fst != id) state.live).push (id, { kind := entry.kind, allocation := allocation }), dead := state.dead, globalTable := Miri.Memory.MemoryState.globalTable✝ state, importedGlobalTable := Miri.Memory.MemoryState.importedGlobalTable✝ state, importedGlobalRuntimeTable := Miri.Memory.MemoryState.importedGlobalRuntimeTable✝ state, extraFnPtrTable := Miri.Memory.MemoryState.extraFnPtrTable✝ state, vaListTable := Miri.Memory.MemoryState.vaListTable✝ state, byteGlobalKeys := state.byteGlobalKeys, byteGlobalKeysReady := state.byteGlobalKeysReady, sourceAllocIdWorldActive := state.sourceAllocIdWorldActive, sourceAllocIdNext := state.sourceAllocIdNext, sourceAllocIdExhausted := state.sourceAllocIdExhausted, sourceAllocIdByRuntimeTable := Miri.Memory.MemoryState.sourceAllocIdByRuntimeTable✝ state, runtimeBySourceAllocIdTable := Miri.Memory.MemoryState.runtimeBySourceAllocIdTable✝ state, opaqueSourceGlobalIds := state.opaqueSourceGlobalIds, sourceByteImageFamilyComplete := state.sourceByteImageFamilyComplete }

Exact live write-back from a raw current lookup. This exposes the update without requiring clients to unfold private memory-map helpers.

def Miri.Memory.MemoryState.removeUnreachable {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (reachable : Array AllocId) : MemoryState Prov Extra MachineKind

The upstream provenance collector prunes only dead-allocation metadata in this part of Memory; live-map and address-map collection have separate owners.

Equations

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

theorem Miri.Memory.MemoryState.reserve_of_highWater {Prov Extra MachineKind : Type} (state : MemoryState Prov Extra MachineKind) (available : state.idSupplyExhausted = false) (nonzero : state.nextAllocId ≠ 0) (sourceAvailable : state.sourceAllocIdWorldActive = true → state.sourceAllocIdExhausted = false) (sourceNonzero : state.sourceAllocIdWorldActive = true → state.sourceAllocIdNext ≠ 0) (issued : ∀ (id : AllocId), id ∈ state.issuedIds → id.value.toNat < state.nextAllocId.toNat) (live : ∀ (row : AllocId × LocalAllocation Prov Extra MachineKind), row ∈ state.live → row.fst.value.toNat < state.nextAllocId.toNat) (global : ∀ (row : GlobalAllocation), row ∈ state.globals → row.allocId.value.toNat < state.nextAllocId.toNat) (dead : ∀ (row : DeadAllocation), row ∈ state.dead → row.allocId.value.toNat < state.nextAllocId.toNat) : ∃ (after : MemoryState Prov Extra MachineKind), state.reserveAllocId = (after, Except.ok { value := state.nextAllocId, nonzero := nonzero })

Raw high-water data and nonzero supplies suffice for the actual allocator reservation. No future allocation/byte/choice operation succeeds by assumption.

structure Miri.Memory.MachineHookResult (HookState α : Type) : Type

• state : HookState
• outcome : Except String α

inductive Miri.Memory.AdjustedGlobalAllocation (Prov Extra : Type) : Type

• borrowed {Prov Extra : Type} (allocation : Allocation Prov Extra) : AdjustedGlobalAllocation Prov Extra
• owned {Prov Extra : Type} (allocation : Allocation Prov Extra) : AdjustedGlobalAllocation Prov Extra

structure Miri.Memory.MemoryStateHookResult (Prov Extra MachineKind HookState α : Type) : Type

A callback receives the current memory and returns its complete successor, including on failure. This is an ordered state transition, never a map merge between two independently changed memory snapshots.

• memory : MemoryState Prov Extra MachineKind
• state : HookState
• outcome : Except String α

@[reducible, inline]

abbrev Miri.Memory.GlobalMemoryHookResult (Prov Extra MachineKind HookState α : Type) : Type

Compatibility name retained for the global-allocation source interface.

Equations

• Miri.Memory.GlobalMemoryHookResult = Miri.Memory.MemoryStateHookResult

structure Miri.Memory.GlobalAllocationHooks (Prov Extra MachineKind HookState : Type) : Type

• synchronizeMemory : MemoryState Prov Extra MachineKind → HookState → HookState

  Install the authoritative memory into any embedded machine view before entering callbacks and after lifecycle-owned cache insertion. Hook states without an embedded memory leave their independent state unchanged.

• evaluateStaticInitializer : MemoryState Prov Extra MachineKind → HookState → Nat → GlobalMemoryHookResult Prov Extra MachineKind HookState Allocation
• beforeAccessGlobal : MemoryState Prov Extra MachineKind → HookState → AllocId → Allocation → Option Nat → Bool → GlobalMemoryHookResult Prov Extra MachineKind HookState Unit
• adjustGlobalAllocation : MemoryState Prov Extra MachineKind → HookState → AllocId → Allocation → GlobalMemoryHookResult Prov Extra MachineKind HookState (AdjustedGlobalAllocation Prov Extra)

structure Miri.Memory.GlobalAllocationResult (Prov Extra MachineKind HookState : Type) : Type

• memory : MemoryState Prov Extra MachineKind
• hooks : HookState
• outcome : Except GlobalAccessError (AdjustedGlobalAllocation Prov Extra)

structure Miri.Memory.MemoryAccessResult (Prov Extra MachineKind HookState α : Type) : Type

• memory : MemoryState Prov Extra MachineKind
• hooks : HookState
• outcome : Except MemoryAccessError α

structure Miri.Memory.PointerResolutionResult (Prov Extra MachineKind HookState ProvExtra : Type) : Type

• memory : MemoryState Prov Extra MachineKind
• state : HookState
• outcome : Except UInt64 (AllocId × ABI.Size × ProvExtra)

structure Miri.Memory.MemoryLifecycleResult (Prov Extra MachineKind HookState α : Type) : Type

• memory : MemoryState Prov Extra MachineKind
• hooks : HookState
• outcome : Except MemoryLifecycleError α

structure Miri.Memory.MemoryDeallocationResult (Prov Extra MachineKind HookState : Type) : Type

The source Memory::deallocate_ptr moves the removed allocation into a local owner. Preserve that exact owner in the result so machine adapters can run its drop effects on every post-removal return without inferring ownership from a map difference.

• memory : MemoryState Prov Extra MachineKind
• hooks : HookState
• detached : Option (AllocId × LocalAllocation Prov Extra MachineKind)
• outcome : Except MemoryLifecycleError Unit

structure Miri.Memory.MemoryReallocationResult (Prov Extra MachineKind HookState : Type) : Type

Reallocation is allocate-copy-deallocate. When the final deallocation removes its source before returning an error, preserve that exact owner for adapters that must perform allocation-specific drop effects.

• memory : MemoryState Prov Extra MachineKind
• hooks : HookState
• detached : Option (AllocId × LocalAllocation Prov Extra MachineKind)
• outcome : Except MemoryLifecycleError (Pointer Prov)

structure Miri.Memory.MemoryCopyResult (Prov Extra MachineKind HookState : Type) : Type

• memory : MemoryState Prov Extra MachineKind
• hooks : HookState
• outcome : Except String Unit

@[instance_reducible]

instance Miri.Memory.instToStringMemoryLifecycleError : ToString MemoryLifecycleError

Equations

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

MemoryLifecycleHooks names the machine-dependent portions of rustc's Machine trait. Every stateful hook returns its updated hook state even when it fails, so callers can preserve source ordering and side effects. The copy hook is required for reallocation and must implement the source mem_copy checks and byte/provenance/initialization transfer; there is no default copy.

structure Miri.Memory.MemoryLifecycleHooks (Prov Extra MachineKind HookState ProvExtra : Type) : Type

• synchronizeMemory : MemoryState Prov Extra MachineKind → HookState → HookState

  Keep machine states that embed memory aligned with the explicit authoritative successor at each allocation lifecycle boundary.

• initLocalAllocation : MemoryState Prov Extra MachineKind → HookState → AllocId → MemoryKind MachineKind → ABI.Size → ABI.Align → MemoryStateHookResult Prov Extra MachineKind HookState Extra
• adjustRootPointer : MemoryState Prov Extra MachineKind → HookState → AllocId → MemoryKind MachineKind → MemoryStateHookResult Prov Extra MachineKind HookState (Pointer Prov)
• resolvePointer : MemoryState Prov Extra MachineKind → HookState → Pointer (Option Prov) → Int → PointerResolutionResult Prov Extra MachineKind HookState ProvExtra
• beforeDeallocation : MemoryState Prov Extra MachineKind → HookState → Allocation Prov Extra → Pointer (Option Prov) → AllocId → ProvExtra → ABI.Size → ABI.Align → MemoryKind MachineKind → MemoryStateHookResult Prov Extra MachineKind HookState Unit
• copyMemory : HookState → MemoryState Prov Extra MachineKind → Pointer (Option Prov) → Pointer (Option Prov) → ABI.Size → Bool → Bool → MemoryCopyResult Prov Extra MachineKind HookState

Hooks around the allocation-storage part of rustc's mem_copy_repeatedly. Pointer access and machine callbacks vary between interpreter machines, so they are explicit inputs. Read/write callbacks return the memory as well as hook state so mutations to Allocation.extra remain visible if a later stage fails.

structure Miri.Memory.MemoryCopyHooks (Prov Extra MachineKind HookState ProvExtra : Type) : Type

• synchronizeMemory : MemoryState Prov Extra MachineKind → HookState → HookState

  Install the authoritative successor in machine states that also contain a memory view before the next callback and in every returned prefix.

• pointerAccess : MemoryState Prov Extra MachineKind → HookState → Pointer (Option Prov) → ABI.Size → MemoryStateHookResult Prov Extra MachineKind HookState (Option (AllocId × ABI.Size × ProvExtra))
• tryGetAllocId : MemoryState Prov Extra MachineKind → HookState → Pointer (Option Prov) → UInt64 → Option AllocId
• beforeAllocationAccess : MemoryState Prov Extra MachineKind → HookState → AllocId → MemoryStateHookResult Prov Extra MachineKind HookState Unit
• beforeMemoryRead : HookState → MemoryState Prov Extra MachineKind → Allocation Prov Extra → Pointer (Option Prov) → AllocId → ProvExtra → AllocRange → MemoryCopyResult Prov Extra MachineKind HookState
• beforeMemoryWrite : HookState → MemoryState Prov Extra MachineKind → Allocation Prov Extra → Pointer (Option Prov) → AllocId → ProvExtra → AllocRange → MemoryCopyResult Prov Extra MachineKind HookState

structure Miri.Memory.MemoryDeallocationHooks (Prov Extra MachineKind HookState ProvExtra : Type) : Type

The deallocation source event uses only resolution and the ordered before-deallocation effect. Allocation/root/copy callbacks are not inputs.

• synchronizeMemory : MemoryState Prov Extra MachineKind → HookState → HookState
• resolvePointer : MemoryState Prov Extra MachineKind → HookState → Pointer (Option Prov) → Int → PointerResolutionResult Prov Extra MachineKind HookState ProvExtra
• beforeDeallocation : MemoryState Prov Extra MachineKind → HookState → Allocation Prov Extra → Pointer (Option Prov) → AllocId → ProvExtra → ABI.Size → ABI.Align → MemoryKind MachineKind → MemoryStateHookResult Prov Extra MachineKind HookState Unit

def Miri.Memory.MemoryLifecycleHooks.deallocation {Prov Extra MachineKind HookState ProvExtra : Type} (hooks : MemoryLifecycleHooks Prov Extra MachineKind HookState ProvExtra) : MemoryDeallocationHooks Prov Extra MachineKind HookState ProvExtra

Equations

• hooks.deallocation = { synchronizeMemory := hooks.synchronizeMemory, resolvePointer := hooks.resolvePointer, beforeDeallocation := hooks.beforeDeallocation }

def Miri.Memory.MemoryLifecycle.registerImportedGlobal {MachineKind Prov Extra HookState : Type} [DecidableEq MachineKind] (memory : MemoryState Prov Extra MachineKind) (hooksState : HookState) (exportId : Nat) (kind : GlobalAllocationKind) (size : ABI.Size) (align : ABI.Align) (mutability : Mutability := Mutability.Not) (payload : Option GlobalAllocationPayload := none) : MemoryLifecycleResult Prov Extra MachineKind HookState AllocId

Register an imported global by separating its canonical exporter graph ID from the fresh runtime AllocId assigned by rustc's monotonic supply. This keeps imported IDs disjoint from later local allocations and makes every export-ID lookup explicit.

Equations

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

def Miri.Memory.MemoryLifecycle.getGlobalAlloc {Prov Extra MachineKind HookState : Type} (memory : MemoryState Prov Extra MachineKind) (hooksState : HookState) (id : AllocId) (isWrite : Bool) (hooks : GlobalAllocationHooks Prov Extra MachineKind HookState) : GlobalAllocationResult Prov Extra MachineKind HookState

Source get_global_alloc: classify the compiler global, resolve a lazy static initializer when needed, run before_access_global, then let the machine convert provenance/bytes/extras. A borrowed conversion remains marked borrowed so immutable access does not populate the local map.

Equations

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

def Miri.Memory.MemoryLifecycle.getAllocRaw {MachineKind Prov Extra HookState : Type} [DecidableEq MachineKind] (memory : MemoryState Prov Extra MachineKind) (hooksState : HookState) (id : AllocId) (globalKind : Option MachineKind) (hooks : GlobalAllocationHooks Prov Extra MachineKind HookState) : MemoryAccessResult Prov Extra MachineKind HookState (Allocation Prov Extra)

Source get_alloc_raw: return a local allocation directly. On a global miss, cache only a machine-owned conversion; a borrowed conversion is returned without inserting that allocation. All nested callback memory transitions are retained before the outer cache insertion or any failure is returned.

Equations

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

def Miri.Memory.MemoryLifecycle.getAllocRawMut {MachineKind Prov Extra HookState : Type} [DecidableEq MachineKind] (memory : MemoryState Prov Extra MachineKind) (hooksState : HookState) (id : AllocId) (globalKind : Option MachineKind) (hooks : GlobalAllocationHooks Prov Extra MachineKind HookState) : MemoryAccessResult Prov Extra MachineKind HookState (Allocation Prov Extra)

Source get_alloc_raw_mut: missing globals are adjusted with is_write, then materialized as MemoryKind::Machine(GLOBAL_KIND) before the mutability check. Thus an immutable-global error retains the newly cached allocation.

Equations

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

def Miri.Memory.MemoryLifecycle.copyResolvedRanges {MachineKind Prov Extra HookState : Type} [DecidableEq MachineKind] (memory : MemoryState Prov Extra MachineKind) (hooksState : HookState) (sourceId : AllocId) (sourceOffset : ABI.Size) (destId : AllocId) (destOffset size : ABI.Size) (repeatCount : UInt64) (pointerSize : ABI.Size) (nonoverlapping : Bool) : MemoryLifecycleResult Prov Extra MachineKind HookState Unit

Perform the allocation-storage part of mem_copy_repeatedly after its caller has resolved pointers and run source/destination access hooks. This uses Allocation's snapshot-based byte, initialization, and provenance copy. The source allocation value is captured before the destination update, which also gives same-allocation copies the source's overlap-safe byte semantics.

The caller remains responsible for the source's pointer-access checks, the zero-size source/read-hook ordering, before_alloc_access, memory read/write hooks, and global-allocation lookup. Missing local allocations are explicit errors; this helper never treats a global or unresolved allocation as an empty local block. Any destination mutation already made by Allocation before its error is written back into the memory state.

Equations

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

def Miri.Memory.MemoryLifecycle.memCopyRepeatedly {MachineKind Prov Extra HookState ProvExtra : Type} [DecidableEq MachineKind] (memory : MemoryState Prov Extra MachineKind) (hooksState : HookState) (sourcePointer destPointer : Pointer (Option Prov)) (size : ABI.Size) (repeatCount : UInt64) (nonoverlapping : Bool) (pointerSize : ABI.Size) (hooks : MemoryCopyHooks Prov Extra MachineKind HookState ProvExtra) : MemoryLifecycleResult Prov Extra MachineKind HookState Unit

Source-ordered bridge for Memory::mem_copy_repeatedly. pointerAccess performs the machine's pointer checks and returns none for a zero-sized access. The source lookup probe is deliberately after both pointer checks and before the source read hook; it still runs for zero-sized copies. A zero-sized source returns after that probe, while a zero-sized destination returns after the source read hook. The allocation read/write hooks run in source order, including for repeatCount = 0 when the source range is nonempty.

Once both local allocations are resolved, Allocation.copyRepeatedly handles the checked destination size, snapshot, initialization/provenance transfer, overlap assertions, and destination mutations. This method does not synthesize global allocations: callers must use their global-allocation path or receive an explicit allocationNotLocal error.

Equations

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

def Miri.Memory.MemoryLifecycle.insertAllocation {MachineKind Prov Extra HookState : Type} [DecidableEq MachineKind] (memory : MemoryState Prov Extra MachineKind) (hooksState : HookState) (synchronizeMemory : MemoryState Prov Extra MachineKind → HookState → HookState) (allocation : Allocation Prov) (kind : MemoryKind MachineKind) (maximumObjectSize : ABI.Size) (globalKind : Option (MemoryKind MachineKind)) (initExtra : MemoryState Prov Extra MachineKind → HookState → AllocId → MemoryKind MachineKind → ABI.Size → ABI.Align → MemoryStateHookResult Prov Extra MachineKind HookState Extra) (adjustRoot : MemoryState Prov Extra MachineKind → HookState → AllocId → MemoryKind MachineKind → MemoryStateHookResult Prov Extra MachineKind HookState (Pointer Prov)) : MemoryLifecycleResult Prov Extra MachineKind HookState (Pointer Prov)

Source Memory::insert_allocation: enforce the object-size bound, reserve an ID, initialize machine extras, insert into the live map, then adjust the root pointer.

Equations

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

def Miri.Memory.MemoryLifecycle.allocatePtr {MachineKind Prov Extra HookState : Type} [DecidableEq MachineKind] (memory : MemoryState Prov Extra MachineKind) (hooksState : HookState) (synchronizeMemory : MemoryState Prov Extra MachineKind → HookState → HookState) (size : ABI.Size) (align : ABI.Align) (kind : MemoryKind MachineKind) (init : AllocInit) (maximumObjectSize : ABI.Size) (globalKind : Option (MemoryKind MachineKind)) (zeroedStorage : ABI.Size → ABI.Align → Option (Array UInt8)) (initExtra : MemoryState Prov Extra MachineKind → HookState → AllocId → MemoryKind MachineKind → ABI.Size → ABI.Align → MemoryStateHookResult Prov Extra MachineKind HookState Extra) (adjustRoot : MemoryState Prov Extra MachineKind → HookState → AllocId → MemoryKind MachineKind → MemoryStateHookResult Prov Extra MachineKind HookState (Pointer Prov)) : MemoryLifecycleResult Prov Extra MachineKind HookState (Pointer Prov)

Source Memory::allocate_ptr: create zeroed backing storage with the requested initialization mask, then reserve the allocation ID and enter the insert_allocation transition. The host allocator is a legal-result callback (none means allocation exhaustion).

Equations

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

def Miri.Memory.MemoryLifecycle.deallocatePtrWith {MachineKind Prov Extra HookState ProvExtra : Type} [DecidableEq MachineKind] (memory : MemoryState Prov Extra MachineKind) (hooksState : HookState) (pointer : Pointer (Option Prov)) (oldSizeAndAlign : Option (ABI.Size × ABI.Align)) (kind : MemoryKind MachineKind) (hooks : MemoryDeallocationHooks Prov Extra MachineKind HookState ProvExtra) : MemoryDeallocationResult Prov Extra MachineKind HookState

Source Memory::deallocate_ptr. The local allocation is removed before mutability, kind, and layout validation. A failure in those checks or in a machine hook therefore retains the source's already-removed live-map state. The Miri machine's address-reuse release occurs inside its deallocation hook, after borrow/race/synchronization checks, before dead-layout caching.

Equations

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

def Miri.Memory.MemoryLifecycle.deallocatePtr {MachineKind Prov Extra HookState ProvExtra : Type} [DecidableEq MachineKind] (memory : MemoryState Prov Extra MachineKind) (hooksState : HookState) (pointer : Pointer (Option Prov)) (oldSizeAndAlign : Option (ABI.Size × ABI.Align)) (kind : MemoryKind MachineKind) (hooks : MemoryLifecycleHooks Prov Extra MachineKind HookState ProvExtra) : MemoryDeallocationResult Prov Extra MachineKind HookState

Compatibility projection for source users that already own the complete allocation lifecycle. Deallocation itself consumes only its two actual hooks.

Equations

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

def Miri.Memory.MemoryLifecycle.reallocatePtr {MachineKind Prov Extra HookState ProvExtra : Type} [DecidableEq MachineKind] (memory : MemoryState Prov Extra MachineKind) (hooksState : HookState) (pointer : Pointer (Option Prov)) (oldSizeAndAlign : Option (ABI.Size × ABI.Align)) (newSize : ABI.Size) (newAlign : ABI.Align) (kind : MemoryKind MachineKind) (initGrowth : AllocInit) (maximumObjectSize : ABI.Size) (globalKind : Option (MemoryKind MachineKind)) (zeroedStorage : ABI.Size → ABI.Align → Option (Array UInt8)) (hooks : MemoryLifecycleHooks Prov Extra MachineKind HookState ProvExtra) : MemoryReallocationResult Prov Extra MachineKind HookState

Source Memory::reallocate_ptr is allocate, copy, deallocate. The source's mem_copy operation is a required callback because its access, initialization, provenance, and overlapping-copy semantics are separately ported by the memory-access layer. Any failure keeps mutations from earlier steps, including a newly allocated block.

Equations

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