Direct source validity compiler leaves. Physical Box projection uses the canonical projection driver; CTFE allocation lookup executes the canonical pointer/global algorithm and exact compiler static predicates. No baseline visitor dictionary or successful missing-query defaults are needed.
def
Miri.Input.CompilerValidityLeaves.make
{K U C : Type}
(p : CompilerProviders.Prepared)
(image : AllocationImage.Imported)
(arrays : RuntimeArrayQueries.Access (Interpreter.ValidityMachine.State K U))
(projection :
Interpreter.PlaceProjectionHooks Memory.Provenance (Interpreter.ValidityMachine.State K U) C
Interpreter.MachineHooks.FrameExtra)
(pointers : Interpreter.PointerMachine.Hooks K (Interpreter.ValidityMachine.Control U))
:
Equations
- One or more equations did not get rendered due to their size.