A checked, source-shaped port of Miri's allocation AddressGenerator. The source RNG's 0..16 sample is represented by Fin 16, rather than by a fixed seed or a chosen pseudo-random stream.

structure Miri.Memory.AllocAddresses.AddressRange : Type

• start : UInt64
• stop : UInt64

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instDecidableEqAddressRange : DecidableEq AddressRange

Equations

• Miri.Memory.AllocAddresses.instDecidableEqAddressRange = Miri.Memory.AllocAddresses.instDecidableEqAddressRange.decEq

def Miri.Memory.AllocAddresses.instDecidableEqAddressRange.decEq (x✝ x✝¹ : AddressRange) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instReprAddressRange : Repr AddressRange

Equations

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

def Miri.Memory.AllocAddresses.instReprAddressRange.repr : AddressRange → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instInhabitedAddressRange : Inhabited AddressRange

Equations

• Miri.Memory.AllocAddresses.instInhabitedAddressRange = { default := Miri.Memory.AllocAddresses.instInhabitedAddressRange.default }

structure Miri.Memory.AllocAddresses.AddressGenerator : Type

• nextBaseAddr : UInt64
• endAddr : UInt64

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instDecidableEqAddressGenerator : DecidableEq AddressGenerator

Equations

• Miri.Memory.AllocAddresses.instDecidableEqAddressGenerator = Miri.Memory.AllocAddresses.instDecidableEqAddressGenerator.decEq

def Miri.Memory.AllocAddresses.instDecidableEqAddressGenerator.decEq (x✝ x✝¹ : AddressGenerator) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.Memory.AllocAddresses.instReprAddressGenerator.repr : AddressGenerator → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instReprAddressGenerator : Repr AddressGenerator

Equations

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

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instInhabitedAddressGenerator : Inhabited AddressGenerator

Equations

• Miri.Memory.AllocAddresses.instInhabitedAddressGenerator = { default := Miri.Memory.AllocAddresses.instInhabitedAddressGenerator.default }

inductive Miri.Memory.AllocAddresses.AddressGeneratorError : Type

• invalidAlignment (error : ABI.AlignError) : AddressGeneratorError
• zeroAlignment : AddressGeneratorError
• slackAdditionOverflow (address slack : UInt64) : AddressGeneratorError
• alignmentRoundingOverflow (address align : UInt64) : AddressGeneratorError
• allocationEndOverflow (address length : UInt64) : AddressGeneratorError
• addressSpaceFull (next endAddr : UInt64) : AddressGeneratorError

def Miri.Memory.AllocAddresses.instDecidableEqAddressGeneratorError.decEq (x✝ x✝¹ : AddressGeneratorError) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instDecidableEqAddressGeneratorError : DecidableEq AddressGeneratorError

Equations

• Miri.Memory.AllocAddresses.instDecidableEqAddressGeneratorError = Miri.Memory.AllocAddresses.instDecidableEqAddressGeneratorError.decEq

def Miri.Memory.AllocAddresses.instReprAddressGeneratorError.repr : AddressGeneratorError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instReprAddressGeneratorError : Repr AddressGeneratorError

Equations

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

@[instance_reducible]

instance Miri.Memory.AllocAddresses.instToStringAddressGeneratorError : ToString AddressGeneratorError

Equations

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

structure Miri.Memory.AllocAddresses.AddressGenerationResult : Type

• state : AddressGenerator
• outcome : Except AddressGeneratorError UInt64

def Miri.Memory.AllocAddresses.AddressGenerator.new (start stop : UInt64) : AddressGenerator

Equations

• Miri.Memory.AllocAddresses.AddressGenerator.new start stop = { nextBaseAddr := start, endAddr := stop }

def Miri.Memory.AllocAddresses.AddressGenerator.getRemaining (generator : AddressGenerator) : AddressRange

Equations

• generator.getRemaining = { start := generator.nextBaseAddr, stop := generator.endAddr }

def Miri.Memory.AllocAddresses.AddressGenerator.legalSlack (slack : Fin 16) : Prop

The source sample is from the half-open range 0..16.

Equations

• Miri.Memory.AllocAddresses.AddressGenerator.legalSlack slack = (↑slack < 16)

theorem Miri.Memory.AllocAddresses.AddressGenerator.slack_is_legal (slack : Fin 16) : legalSlack slack

def Miri.Memory.AllocAddresses.AddressGenerator.alignAddr (address alignment : UInt64) : Except AddressGeneratorError UInt64

Source align_addr, with the strict_add overflow made explicit. This preserves the source's evaluation order: it adds the whole alignment before subtracting the remainder.

Equations

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

def Miri.Memory.AllocAddresses.AddressGenerator.generate (generator : AddressGenerator) (size : ABI.Size) (align : ABI.Align) (slack : Fin 16) : AddressGenerationResult

Execute one source generation step using a legal source random choice. The state includes the source mutation made before its final address-space check, including the updated next address on an exhaustion error.

Equations

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