fact: Definition valid_pq (pq : val) (h: heap): mpred := EX arr : val, EX junk: list heap_item, (!! heap_ordered (heap_items h)) && (!! (Zlength ((heap_items h) ++ junk) = heap_capacity h)) && (!! (2 * (heap_capacity h - 1) <= Int.max_unsigned)) && (data_at Tsh t_pq (Vint (Int.repr (heap_capacity h)), (Vint (Int.repr (heap_size h)), arr)) pq * harray ((heap_items h) ++ junk) arr).
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel RelationClasses