Actual lifecycle closure on EvalWorld. Full-state root addressing and operation-local deallocation views preserve the real active stack. There is one address/tape map; inverse removal, reuse choices and release clocks are performed by ExecutionAddressChoices at their source event cuts.

@[reducible, inline]

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

Equations

• Miri.Input.EvalAllocationMachine.User = Miri.Input.EvalBackendMachine.User

@[reducible, inline]

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

Equations

• Miri.Input.EvalAllocationMachine.State = Miri.Input.EvalBackendMachine.State

def Miri.Input.EvalAllocationMachine.tape {Os R P H D O Aff B Host : Type} : Interpreter.ExecutionChoices.Access (State Os R P H D O Aff B Host)

Equations

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

def Miri.Input.EvalAllocationMachine.allocation {Os R P H D O Aff B Host : Type} (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (Interpreter.ThreadStacks.Storage (EvalWorld.World Os R P H D O Aff B Host)))) (extras : Interpreter.MemoryExtras.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) P) (base : Interpreter.PlaceMachine.AllocationConfig Memory.MiriMemoryKind (User Os R P H D O Aff B Host)) : Interpreter.PlaceMachine.AllocationConfig Memory.MiriMemoryKind (User Os R P H D O Aff B Host)

Tree/race initialization is already PlaceMachine.initStackExtra. This replaces its tail with source extras creation, using the actual backend flags, and replaces root addressing with fresh source-point draws on the full state.

Equations

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

def Miri.Input.EvalAllocationMachine.deallocateWith {Os R P H D O Aff B Host : Type} (spans : Interpreter.AllocationDriver.SpanHooks) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (Interpreter.ThreadStacks.Storage (EvalWorld.World Os R P H D O Aff B Host)))) (extras : Interpreter.MemoryExtras.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) P) (diagnostic : Memory.AllocId → Interpreter.PlaceMachine.MachineM Memory.MiriMemoryKind (User Os R P H D O Aff B Host) Unit) (nativeDrop : Option (Memory.Allocation Memory.Provenance TreeBorrows.BorrowTree → Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D O Aff B Host) Unit)) (ptr : Memory.Pointer (Option Memory.Provenance)) (old : Option (ABI.Size × ABI.Align)) (kind : Memory.MemoryKind Memory.MiriMemoryKind) : Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D O Aff B Host) Unit

Capture the actual active view at this deallocation, not at Config creation. The source lifecycle callback executes only machine operations, so its active stack remains this view. Every partial machine/tape effect is returned.

Equations

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

def Miri.Input.EvalAllocationMachine.deallocate {Os R P H D O Aff B Host : Type} (spans : Interpreter.AllocationDriver.SpanHooks) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (Interpreter.ThreadStacks.Storage (EvalWorld.World Os R P H D O Aff B Host)))) (extras : Interpreter.MemoryExtras.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) P) (base : Interpreter.AllocationMachine.DeallocationHooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) P) (ptr : Memory.Pointer (Option Memory.Provenance)) (old : Option (ABI.Size × ABI.Align)) (kind : Memory.MemoryKind Memory.MiriMemoryKind) : Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D O Aff B Host) Unit

Compatibility input projects only the genuine diagnostic/native effects; span, pointer, clock, tree, address and error semantics are source-owned.

Equations

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