Source stack.rs storage_live_dyn's query-free type fast path and place.rs allocate_dyn. This uses the original local type, not its normalized layout. Compiler inference subtypes absent from the input remain explicit obligations.

def Miri.Input.CompilerStorage.veryTriviallySized (runtime : RuntimeMetadata) (ty : MIR.TyId) : Except Interpreter.StepError Bool

Every recursive step follows a canonical type edge. The type-table length bounds an acyclic path; exhaustion diagnoses malformed cyclic input, rather than limiting MIR execution or returning an invented sizedness result.

Equations

• Miri.Input.CompilerStorage.veryTriviallySized runtime ty = Miri.Input.CompilerStorage.trivial✝ runtime (runtime.source.types.size + 1) ty

def Miri.Input.CompilerStorage.hooks {K U C : Type} [DecidableEq K] (p : CompilerProviders.Prepared) (allocation : Interpreter.PlaceMachine.AllocationConfig K U) (dynamic : Interpreter.DynamicLayoutHooks Memory.Provenance (Interpreter.MachineHooks.State K U) C) (dynamicBudget : Nat) (choice : C) (deallocateStack : Memory.Pointer (Option Memory.Provenance) → Interpreter.MachineHooks.M K U Unit) : Interpreter.MachineHooks.StorageHooks K U

Actual source storage dictionary. The only allocation input is the real stack allocator, and dynamic size/alignment queries execute before reserving an allocation ID. Deallocation is the actual allocation-lifecycle operation.

Equations

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