implementing new-ref, wip
some work on bvi_to_bvp
more progress on bvi_To_bvp
some fixes to x64_heap
minor progress on x64
a bit of progress on bvi-to-bvp compiler proof
bit more progress on bvi-to-bvp proof
bvi-to-bvp proof cheat free!
Ref part of zBC_HEAP_THM proved