Build the startup environment's memory bundle from the same fixed source execution configuration. Deallocation is a machine action composed at each call site, so span and address-release hooks see the actual active stack.

@[reducible, inline]

abbrev Miri.Input.EvalStartupMemoryConstruction.W (Os R Payload H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalStartupMemoryConstruction.W = Miri.Input.EvalEntryMachine.W

@[reducible, inline]

abbrev Miri.Input.EvalStartupMemoryConstruction.InnerControl (Os R P H D O Aff B Host : Type) : Type

Equations

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

def Miri.Input.EvalStartupMemoryConstruction.environmentMemory {Os R P H D O Aff B Host C ClockHost : Type} [DecidableEq Memory.MiriMemoryKind] (prepared : EvalPreparation.Prepared) (execution : EvalExecutable.Core Os R P H D O Aff B Host C ClockHost) (leaves : EvalConfigurationCore.Leaves Os R P H D O Aff B Host C ClockHost) (spans : Interpreter.AllocationDriver.SpanHooks) (choice : C) (alignment : Interpreter.ValidityMachine.AlignmentCheck) (stringScanBudget : Nat) : EvalHostRuntimeConstruction.EnvironmentMemory (InnerControl Os R P H D O Aff B Host) C P

Equations

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