More macro/fundef re-use

Collapse the expansion of Hyp_pool_ex1 in a proof

Make pfn/va/pa use more consistent (esp APs)

VIP: Verify page_add_to_list_pool; page_add_to_list

VIP: Verify page_add_to_list_pool_ex1

VIP: Add provenance arg to freeArea_cell_wf function

VIP: Add provenance arg to Hyp_pool* predicates

VIP: Verify __hyp_attach_page; node_to_page

VIP: Verify __hyp_extract_page

VIP: Verify __hyp_put_page

Use helper function for calculating virt addr

Use tabs consistently in page_alloc.c

Use helper function

VIP: Remove (void*) cast from __hyp_va

VIP: Remove i2p casts due to hyp_page_to_virt