Production validity construction at the actual stored Control layer. No base visitor or independent ghost/union-cache setters enter this interface.
def
Miri.Input.EvalValidityMachine.hooks
{K U C O : Type}
[DecidableEq K]
(prepared : CompilerFactAdapters.Prepared)
(runtime : CompilerRuntimeQueries.Prepared)
(leaves : Interpreter.ExecutionValidity.Leaves (Interpreter.ValidityMachine.State K U) C)
(access : Interpreter.ValidityMachine.Access K U)
(allocation : Interpreter.PlaceMachine.AllocationConfig K (Interpreter.ValidityMachine.UserState U))
(compiler : Interpreter.ValidityMachine.Compiler K U C)
(projection :
Interpreter.PlaceProjectionHooks Memory.Provenance (Interpreter.ValidityMachine.State K U) C
Interpreter.MachineHooks.FrameExtra)
(vtable :
Interpreter.VTableHooks Memory.Provenance (Interpreter.ValidityMachine.State K U) C (Interpreter.FnVal O)
(ABI.FnAbi MIR.TyId))
(discriminant :
Interpreter.DiscriminantHooks Memory.Provenance (Interpreter.ValidityMachine.State K U) C
(Interpreter.RuntimePlace Memory.Provenance))
(pointers : Interpreter.PointerMachine.Hooks K (Interpreter.ValidityMachine.Control U))
(retag : Interpreter.TypedRetag.Hooks K (Interpreter.ValidityMachine.UserState U))
(retagBudget : Nat)
:
All portable memory/provenance/padding operations are canonical. The final provider wrapper installs exact compiler paths, source box projection, and choice-time typed retag preparation over the same state.
Equations
- One or more equations did not get rendered due to their size.