Checks that memory accesses are well-typed in the sense of the \ghost qualifier. That is, only ghost code can declare ghost memory, and ghost code can modify only ghost memory. Registered as a transformation category (that doesn't transform anything but will complain if there are bad accesses).