This was accomplished by changing the way enter_block works, removing
the overly-complicated argument passing through simulated ID
instructions and replacing it with memreq propagation in registers.
A lot of support code and code/proof cleanup was also added.