1partition_alloc - ALLOC hyp:$1, $2 GT(0):$$.r:$$.e NE(0) 2partition_alloc - BPS charlength($$.r)=infinity 3partition_alloc - BPS bytesize($$.r)=$1 4partition_alloc - NPD.SRC env : $$.r : $$.e NE(0) 5partition_alloc - UNINIT.HEAP 1 : *($$.r) : 1 6partition_alloc - UnsafeAllocSizeAccepter $2 7partition_free - FREE hyp $2 8