don't use bogus tags from x64_heap, prove COMPILER_RUN_INV_INR
update proof of COMPILER_RUN_INV_INL