Source-point persistent address choices. Cached, dead/type-id and external address paths do not consume managed reuse/slack draws. Pool-prefix mutations and inverse-map removal remain visible if the following tape is exhausted.

@[reducible, inline]

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

Equations

• Miri.Interpreter.ExecutionAddressChoices.State = Miri.Interpreter.PointerMachine.State

@[reducible, inline]

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

Equations

• Miri.Interpreter.ExecutionAddressChoices.M = Miri.Interpreter.PointerMachine.M

def Miri.Interpreter.ExecutionAddressChoices.addrFromAllocId {K U : Type} (access : ExecutionChoices.Access (State K U)) (h : PointerMachine.Hooks K U) (id : Memory.AllocId) (kind : Option Memory.AllocAddresses.AddressMemoryKind) : M K U UInt64

AddressRandomChoices is only a transport for the existing source algorithm; unused fields are never sampled. Every used field comes from a fresh tape event.

Equations

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

def Miri.Interpreter.ExecutionAddressChoices.freeAllocId {K U : Type} (access : ExecutionChoices.Access (State K U)) (h : PointerMachine.Hooks K U) (id : Memory.AllocId) (size : ABI.Size) (align : ABI.Align) (kind : Memory.AllocAddresses.AddressMemoryKind) : M K U Unit

Source free_alloc_id removes inverse/exposure mappings before the reuse Bernoulli draw, then release-clock and add_addr, including error partial state.

Equations

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