A checked value port of Miri's size/alignment/thread keyed address reuse pool. RNG outputs are explicit legal-choice arguments; no seed or PRNG stream is introduced.

def Miri.Memory.AllocAddresses.maxReusePoolSize : Nat

Equations

• Miri.Memory.AllocAddresses.maxReusePoolSize = 64

inductive Miri.Memory.AllocAddresses.AddressMemoryKind : Type

Only this distinction from rustc MemoryKind affects reuse-pool behavior: stack allocations are never remembered or reused. All other kinds follow the same pool policy.

• stack : AddressMemoryKind
• other : AddressMemoryKind

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instDecidableEqAddressMemoryKind : DecidableEq AddressMemoryKind

Equations

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

def Miri.Memory.AllocAddresses.instReprAddressMemoryKind.repr : AddressMemoryKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instReprAddressMemoryKind : Repr AddressMemoryKind

Equations

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

@[reducible, inline]

abbrev Miri.Memory.AllocAddresses.AddressThreadId : Type

The source thread index is an ordered u32.

Equations

• Miri.Memory.AllocAddresses.AddressThreadId = UInt32

structure Miri.Memory.AllocAddresses.AddressReuseConfig : Type

• addressReuseRate : Float
• addressReuseCrossThreadRate : Float

def Miri.Memory.AllocAddresses.instDecidableEqAddressReuseConfig.decEq (x✝ x✝¹ : AddressReuseConfig) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instDecidableEqAddressReuseConfig : DecidableEq AddressReuseConfig

Equations

• Miri.Memory.AllocAddresses.instDecidableEqAddressReuseConfig = Miri.Memory.AllocAddresses.instDecidableEqAddressReuseConfig.decEq

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instReprAddressReuseConfig : Repr AddressReuseConfig

Equations

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

def Miri.Memory.AllocAddresses.instReprAddressReuseConfig.repr : AddressReuseConfig → Nat → Std.Format

Equations

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

structure Miri.Memory.AllocAddresses.ReusableAddress : Type

• address : UInt64
• size : ABI.Size
• thread : AddressThreadId
• clock : Concurrency.VClock

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instReprReusableAddress : Repr ReusableAddress

Equations

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

def Miri.Memory.AllocAddresses.instReprReusableAddress.repr : ReusableAddress → Nat → Std.Format

Equations

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

structure Miri.Memory.AllocAddresses.ReusePool : Type

• addressReuseRate : Float
• addressReuseCrossThreadRate : Float
• pool : Array (Array ReusableAddress)

  The outer index is the alignment's log2, like source subpool.

def Miri.Memory.AllocAddresses.instReprReusePool.repr : ReusePool → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instReprReusePool : Repr ReusePool

Equations

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

inductive Miri.Memory.AllocAddresses.ReusePoolError : Type

• invalidRate (rate : Float) : ReusePoolError
• illegalBernoulliChoice (rate : Float) (choice : Bool) : ReusePoolError
• invalidAlignment (error : ABI.AlignError) : ReusePoolError
• invalidRangeChoice (choice begin stop : Nat) : ReusePoolError
• malformedPoolIndex (index length : Nat) : ReusePoolError
• malformedChoiceIndex (index length : Nat) : ReusePoolError
• reusedAddressMisaligned (address alignment : UInt64) : ReusePoolError

def Miri.Memory.AllocAddresses.instReprReusePoolError.repr : ReusePoolError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instReprReusePoolError : Repr ReusePoolError

Equations

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

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instToStringReusePoolError : ToString ReusePoolError

Equations

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

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

• state : ReusePool
• outcome : Except ReusePoolError α

structure Miri.Memory.AllocAddresses.ReusedAddress : Type

• address : UInt64
• clockToAcquire : Option Concurrency.VClock

  A cross-thread address carries the donor clock for an acquire hook.

def Miri.Memory.AllocAddresses.instReprReusedAddress.repr : ReusedAddress → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instReprReusedAddress : Repr ReusedAddress

Equations

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

def Miri.Memory.AllocAddresses.ReusePool.bernoulliChoiceAllowed (rate : Float) (choice : Bool) : Bool

The support of a source rng.random_bool(rate) result. For interior rates both results are possible; endpoints permit only the corresponding result.

Equations

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

def Miri.Memory.AllocAddresses.ReusePool.new (config : AddressReuseConfig) : Except ReusePoolError ReusePool

Equations

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

def Miri.Memory.AllocAddresses.ReusePool.addressSpaceShortage (pool : ReusePool) : ReusePool

Equations

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

def Miri.Memory.AllocAddresses.ReusePool.addAddr (pool : ReusePool) (choice : Bool) (address : UInt64) (size : ABI.Size) (align : ABI.Align) (kind : AddressMemoryKind) (thread : AddressThreadId) (makeClock : Unit → Concurrency.VClock) : ReusePoolResult Unit

Add an address using the explicit outcome of the source Bernoulli draw. Stack addresses short-circuit before consuming that choice.

Equations

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

def Miri.Memory.AllocAddresses.ReusePool.prepareTakeAddr (pool : ReusePool) (reuseChoice crossThreadChoice : Bool) (size : ABI.Size) (align : ABI.Align) (kind : AddressMemoryKind) (thread : AddressThreadId) : ReusePoolResult (Option (Nat × Nat))

Source prefix before the pool-index random draw. Exposes the exact half-open candidate range while retaining ensure_subpool mutations, so an effectful choice input may be requested at the actual source event.

Equations

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

def Miri.Memory.AllocAddresses.ReusePool.takeAddr (pool : ReusePool) (reuseChoice crossThreadChoice : Bool) (selection : Nat) (size : ABI.Size) (align : ABI.Align) (kind : AddressMemoryKind) (thread : AddressThreadId) : ReusePoolResult (Option ReusedAddress)

Try taking a reusable address. reuseChoice and crossThreadChoice are the two source Bernoulli outcomes; selection is the absolute usize index sampled from the source's eligible half-open [begin, stop) range. A missing candidate returns none while keeping the source's possibly extended empty subpool.

Equations

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

def Miri.Memory.AllocAddresses.ReusePool.WellFormed (pool : ReusePool) : Prop

The sorted-and-bounded pool invariant maintained by public mutations.

Equations

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

theorem Miri.Memory.AllocAddresses.ReusePool.emptyPool_wellFormed (reuseRate crossThreadRate : Float) : { addressReuseRate := reuseRate, addressReuseCrossThreadRate := crossThreadRate }.WellFormed