Types as Contracts

Given that they ban ptrtoint, the "intended" model is that allocas can be allocated in "imaginary space" and have an address that is not a number. I'm still not sure how to square "imaginary space" with DCE of arbitrarily-complex expressions including memory accesses, but it seems like something that "could" be done.