A checked port of the non-host-specific state transitions in Miri's alloc_addresses/mod.rs. Allocation metadata, liveness, host addresses, borrow-tracker exposure, and cross-thread clock acquisition remain explicit caller hooks.

inductive Miri.Memory.AllocAddresses.ProvenanceMode : Type

• default : ProvenanceMode
• permissive : ProvenanceMode
• strict : ProvenanceMode

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instDecidableEqProvenanceMode : DecidableEq ProvenanceMode

Equations

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

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instReprProvenanceMode : Repr ProvenanceMode

Equations

• Miri.Memory.AllocAddresses.instReprProvenanceMode = { reprPrec := Miri.Memory.AllocAddresses.instReprProvenanceMode.repr }

def Miri.Memory.AllocAddresses.instReprProvenanceMode.repr : ProvenanceMode → Nat → Std.Format

Equations

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

inductive Miri.Memory.AllocAddresses.AddressSpaceMode : Type

• managed : AddressSpaceMode
• nativeLib : AddressSpaceMode

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instDecidableEqAddressSpaceMode : DecidableEq AddressSpaceMode

Equations

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

def Miri.Memory.AllocAddresses.instReprAddressSpaceMode.repr : AddressSpaceMode → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instReprAddressSpaceMode : Repr AddressSpaceMode

Equations

• Miri.Memory.AllocAddresses.instReprAddressSpaceMode = { reprPrec := Miri.Memory.AllocAddresses.instReprAddressSpaceMode.repr }

def Miri.Memory.AllocAddresses.AddressSpaceMode.fromFlags (nativeLibEnabled : Bool) : AddressSpaceMode

Equations

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

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instToStringAddressSpaceMode : ToString AddressSpaceMode

Equations

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

inductive Miri.Memory.AllocAddresses.AllocationAddressKind : Type

• liveData : AllocationAddressKind
• typeId : AllocationAddressKind
• dead : AllocationAddressKind

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instDecidableEqAllocationAddressKind : DecidableEq AllocationAddressKind

Equations

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

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instReprAllocationAddressKind : Repr AllocationAddressKind

Equations

• Miri.Memory.AllocAddresses.instReprAllocationAddressKind = { reprPrec := Miri.Memory.AllocAddresses.instReprAllocationAddressKind.repr }

def Miri.Memory.AllocAddresses.instReprAllocationAddressKind.repr : AllocationAddressKind → Nat → Std.Format

Equations

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

structure Miri.Memory.AllocAddresses.AllocationAddressInfo : Type

• kind : AllocationAddressKind
• live : Bool
• size : ABI.Size
• align : ABI.Align
• memoryKind : Option AddressMemoryKind
• thread : AddressThreadId

def Miri.Memory.AllocAddresses.instReprAllocationAddressInfo.repr : AllocationAddressInfo → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instReprAllocationAddressInfo : Repr AllocationAddressInfo

Equations

• Miri.Memory.AllocAddresses.instReprAllocationAddressInfo = { reprPrec := Miri.Memory.AllocAddresses.instReprAllocationAddressInfo.repr }

structure Miri.Memory.AllocAddresses.AddressRandomChoices : Type

• reuse : Bool

  Outcome of the source address-reuse Bernoulli draw.

• crossThread : Bool

  Outcome of the cross-thread Bernoulli draw, consumed only after reuse.

• poolIndex : Nat

  Absolute pool index in the source begin..end random range.

• slack : Fin 16

  Slack outcome in the source 0..16 range for a fresh address.

structure Miri.Memory.AllocAddresses.AddressExternalHooks : Type

• externalAddress : Option UInt64

  Native libraries supply physical addresses; absence remains an explicit capability requirement.

structure Miri.Memory.AllocAddresses.BaseAddressEntry : Type

• allocId : AllocId
• address : UInt64

def Miri.Memory.AllocAddresses.instReprBaseAddressEntry.repr : BaseAddressEntry → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instReprBaseAddressEntry : Repr BaseAddressEntry

Equations

• Miri.Memory.AllocAddresses.instReprBaseAddressEntry = { reprPrec := Miri.Memory.AllocAddresses.instReprBaseAddressEntry.repr }

structure Miri.Memory.AllocAddresses.InverseAddressEntry : Type

• address : UInt64
• allocId : AllocId

def Miri.Memory.AllocAddresses.instReprInverseAddressEntry.repr : InverseAddressEntry → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instReprInverseAddressEntry : Repr InverseAddressEntry

Equations

• Miri.Memory.AllocAddresses.instReprInverseAddressEntry = { reprPrec := Miri.Memory.AllocAddresses.instReprInverseAddressEntry.repr }

structure Miri.Memory.AllocAddresses.AddressGenerationState : Type

• generator : AddressGenerator
• reusePool : ReusePool

def Miri.Memory.AllocAddresses.instReprAddressGenerationState.repr : AddressGenerationState → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instReprAddressGenerationState : Repr AddressGenerationState

Equations

• Miri.Memory.AllocAddresses.instReprAddressGenerationState = { reprPrec := Miri.Memory.AllocAddresses.instReprAddressGenerationState.repr }

structure Miri.Memory.AllocAddresses.GlobalAddressState : Type

• intToPtrMap : Array InverseAddressEntry
• baseAddr : Array BaseAddressEntry
• exposed : Array AllocId
• provenanceMode : ProvenanceMode
• addressMode : AddressSpaceMode
• generation : Option AddressGenerationState
• preparedNativeBytes : Array (AllocId × PreparedGlobalBytes)

  Source native prepared_alloc_bytes, surviving global-memory snapshots.

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instReprGlobalAddressState : Repr GlobalAddressState

Equations

• Miri.Memory.AllocAddresses.instReprGlobalAddressState = { reprPrec := Miri.Memory.AllocAddresses.instReprGlobalAddressState.repr }

def Miri.Memory.AllocAddresses.instReprGlobalAddressState.repr : GlobalAddressState → Nat → Std.Format

Equations

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

inductive Miri.Memory.AllocAddresses.AddressStateError : Type

• reusePool (error : ReusePoolError) : AddressStateError
• addressGenerator (error : AddressGeneratorError) : AddressStateError
• pointerArithmetic (error : PointerError) : AddressStateError
• missingBaseAddress (allocId : AllocId) : AddressStateError
• baseAddressAlreadyCached (allocId : AllocId) (address : UInt64) : AddressStateError
• missingInverseEntry (address : UInt64) : AddressStateError
• inverseEntryMismatch (address : UInt64) (expected actual : AllocId) : AddressStateError
• duplicateAddress (address : UInt64) (existingAllocId newAllocId : AllocId) : AddressStateError
• missingAddressGeneration : AddressStateError
• unexpectedAddressGeneration : AddressStateError
• missingAllocationInfo (allocId : AllocId) : AddressStateError
• missingMemoryKind (allocId : AllocId) : AddressStateError
• deadAllocation (allocId : AllocId) : AddressStateError
• strictAddressLookup : AddressStateError
• strictIntegerToPointerCast : AddressStateError
• missingAllocationSize (allocId : AllocId) : AddressStateError
• missingLivenessStatus (allocId : AllocId) : AddressStateError
• deadAllocationInAddressIndex (allocId : AllocId) : AddressStateError
• externalAddressHookRequired (mode : AddressSpaceMode) : AddressStateError
• borrowTrackerHookRequired (allocId : AllocId) (tag : BorTag) : AddressStateError
• borrowTrackerFailure (allocId : AllocId) (tag : BorTag) (message : String) : AddressStateError
• acquireClockFailure (address : UInt64) (clock : Concurrency.VClock) (message : String) : AddressStateError
• malformedInverseIndex (index length : Nat) : AddressStateError

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instReprAddressStateError : Repr AddressStateError

Equations

• Miri.Memory.AllocAddresses.instReprAddressStateError = { reprPrec := Miri.Memory.AllocAddresses.instReprAddressStateError.repr }

def Miri.Memory.AllocAddresses.instReprAddressStateError.repr : AddressStateError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instToStringAddressStateError : ToString AddressStateError

Equations

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

structure Miri.Memory.AllocAddresses.AddressStateResult (α : Type) : Type

• state : GlobalAddressState
• outcome : Except AddressStateError α

inductive Miri.Memory.AllocAddresses.AddressAssignment : Type

A selected cross-thread reuse is not reported as immediately usable until its synchronization hook has completed.

• ready (address : UInt64) : AddressAssignment
• acquireRequired (allocId : AllocId) (address : UInt64) (clock : Concurrency.VClock) : AddressAssignment

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instReprAddressAssignment : Repr AddressAssignment

Equations

• Miri.Memory.AllocAddresses.instReprAddressAssignment = { reprPrec := Miri.Memory.AllocAddresses.instReprAddressAssignment.repr }

def Miri.Memory.AllocAddresses.instReprAddressAssignment.repr : AddressAssignment → Nat → Std.Format

Equations

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

structure Miri.Memory.AllocAddresses.AddressLookupHooks : Type

• sizeOf : AllocId → Option ABI.Size
• isLive : AllocId → Option Bool

def Miri.Memory.AllocAddresses.GlobalAddressState.new (provenanceMode : ProvenanceMode) (mode : AddressSpaceMode) (start stop : UInt64) (config : AddressReuseConfig) : Except AddressStateError GlobalAddressState

Equations

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

def Miri.Memory.AllocAddresses.GlobalAddressState.cacheAddress (state : GlobalAddressState) (id : AllocId) (address : UInt64) : AddressStateResult Unit

Cache first in baseAddr, then add the nonzero address to the sorted inverse vector. A duplicate inverse address reports the source unwrap_err failure after retaining the earlier base-map insertion.

Equations

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

def Miri.Memory.AllocAddresses.GlobalAddressState.addrFromAllocId (state : GlobalAddressState) (id : AllocId) (info? : Option AllocationAddressInfo) (choices : AddressRandomChoices) (hooks : AddressExternalHooks := { }) : AddressStateResult AddressAssignment

The cached fast path precedes allocation-info and random-choice requirements. Managed choices remain explicit; native addresses require external hooks.

Equations

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

def Miri.Memory.AllocAddresses.GlobalAddressState.completeAcquire (pending : AddressStateResult AddressAssignment) (clockResult : Except String Unit) : AddressStateResult AddressAssignment

Complete a cross-thread reuse after the caller has acquired the returned clock. The address is cached only after successful acquisition, matching the source's ? before interp_ok.

Equations

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

def Miri.Memory.AllocAddresses.GlobalAddressState.allocIdFromAddr (state : GlobalAddressState) (address : UInt64) (size : Int64) (hooks : AddressLookupHooks) : Except AddressStateError (Option AllocId)

Source alloc_id_from_addr, with allocation-size and liveness lookups as explicit caller hooks. Negative accesses search from addr.saturating_sub(1). Only addresses in exposed allocations produce wildcard provenance.

Equations

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

def Miri.Memory.AllocAddresses.GlobalAddressState.exposeProvenance (state : GlobalAddressState) (provenance : Provenance) (allocationLive? : Option Bool) (borrowTrackerEnabled : Bool) (tagHook? : Option (Except String Unit)) : AddressStateResult Unit

Source expose_provenance. If borrow tracking is enabled, insertion into the exposed set precedes the explicit tracker hook result.

Equations

• One or more equations did not get rendered due to their size.
• state.exposeProvenance Miri.Memory.Provenance.wildcard allocationLive? borrowTrackerEnabled tagHook? = (pure { state := state, outcome := Except.ok () }).run

def Miri.Memory.AllocAddresses.GlobalAddressState.ptrFromAddrCast (state : GlobalAddressState) (address : UInt64) (firstAtSourceLocation : Bool) : AddressStateResult (Pointer (Option Provenance) × Bool)

Source ptr_from_addr_cast: default mode retains wildcard provenance and reports the source warning as metadata; strict mode returns the explicit stop.

Equations

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

def Miri.Memory.AllocAddresses.GlobalAddressState.exposedAllocations (state : GlobalAddressState) : Array AllocId

Equations

• state.exposedAllocations = state.exposed

def Miri.Memory.AllocAddresses.GlobalAddressState.removeUnreachableAllocs (state : GlobalAddressState) (liveIds : Array AllocId) : GlobalAddressState

The source GC hook only removes entries from the cached id-to-base map. The inverse map and exposed set are already cleared by free.

Equations

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

def Miri.Memory.AllocAddresses.GlobalAddressState.ptrGetAlloc (state : GlobalAddressState) (pointer : Pointer Provenance) (accessSize : Int64) (hooks : AddressLookupHooks) (cx : PointerArithmetic) : Except AddressStateError (Option (AllocId × ABI.Size))

Source ptr_get_alloc. This returns a concrete allocation directly or resolves wildcard provenance through the exposed inverse map; validity and allocation bounds are checked by later memory hooks.

Equations

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

def Miri.Memory.AllocAddresses.GlobalAddressState.freeAllocId (state : GlobalAddressState) (id : AllocId) (size : ABI.Size) (align : ABI.Align) (kind : AddressMemoryKind) (thread : AddressThreadId) (reuseChoice : Bool) (clock : Unit → Concurrency.VClock) : AddressStateResult Unit

Source free_alloc_id: remove inverse/exposed membership while retaining the base cache, then offer the freed range to the reuse pool.

Equations

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

theorem Miri.Memory.AllocAddresses.GlobalAddressState.allocation_base_zero (state : GlobalAddressState) (address : UInt64) (id : AllocId) (hooks : AddressLookupHooks) (position : Nat) (mode : state.provenanceMode ≠ ProvenanceMode.strict) (search : Miri.Memory.AllocAddresses.GlobalAddressState.findInverseIndex✝ state.intToPtrMap address = (position, true)) (row : state.intToPtrMap[position]? = some { address := address, allocId := id }) (exposed : state.exposed.contains id = true) (live : hooks.isLive id = some true) : state.allocIdFromAddr address 0 hooks = Except.ok (some id)

Proof interface to the existing inverse-search consumer, exact base case.

theorem Miri.Memory.AllocAddresses.GlobalAddressState.allocation_interior_zero (state : GlobalAddressState) (address base : UInt64) (id : AllocId) (hooks : AddressLookupHooks) (size : ABI.Size) (position : Nat) (mode : state.provenanceMode ≠ ProvenanceMode.strict) (search : Miri.Memory.AllocAddresses.GlobalAddressState.findInverseIndex✝ state.intToPtrMap address = (position + 1, false)) (row : state.intToPtrMap[position]? = some { address := base, allocId := id }) (known : hooks.sizeOf id = some size) (inside : address - base < size.bytes) (exposed : state.exposed.contains id = true) (live : hooks.isLive id = some true) : state.allocIdFromAddr address 0 hooks = Except.ok (some id)

Proof interface to the existing inverse-search consumer, interior case.

theorem Miri.Memory.AllocAddresses.GlobalAddressState.pointer_from_selection (state : GlobalAddressState) (pointer : Pointer Provenance) (count : Int64) (hooks : AddressLookupHooks) (arithmetic : PointerArithmetic) (id : AllocId) (base relative : UInt64) (selected : (match pointer.provenance with | Provenance.concrete id tag => Except.ok (some id) | Provenance.wildcard => state.allocIdFromAddr pointer.offset.bytes count hooks) = Except.ok (some id)) (cached : Array.find? (fun (row : BaseAddressEntry) => row.allocId == id) state.baseAddr = some { allocId := id, address := base }) (truncated : arithmetic.truncateToTargetUsize (pointer.offset.bytes - base) = Except.ok relative) : state.ptrGetAlloc pointer count hooks arithmetic = Except.ok (some (id, ABI.Size.ofBytes relative))

The selected allocation and a current base cache complete ptr_get_alloc.