proposition: Lemma body_build_heap: semax_body Vprog Gprog f_build_heap build_heap_spec.
proof: Proof. start_function. assert_PROP (2 * (size - 1) <= Int.max_unsigned). { apply prop_right. rep_lia. } assert (Zlength arr_contents <= Int.max_unsigned) by rep_lia. forward. rewrite sub_repr. rewrite <- Zparent_repr. 2: lia. forward_loop (EX s : Z, EX arr_contents' : list heap_item, PROP (0 <= s < Zlength arr_contents; weak_heap_ordered_top_down_bounded arr_contents' s s; Permutation arr_contents arr_contents') LOCAL (temp _arr arr; temp _size__1 (Vint (Int.repr size)); temp _start (Vint (Int.repr s))) SEP (harray arr_contents' arr)). { Exists (Zparent size) arr_contents. entailer!. split. rewrite Zparent_unfold. 2: lia. split. apply Z_div_pos; lia. eapply Z.le_lt_trans. 2: apply Z.div_lt. apply Z.div_le_mono. 1,2,3,4: lia. red. generalize (weak_heapOrdered_bounded_half _ cmp_rel arr_contents); intro. unfold Zparent. rewrite ZtoNat_Zlength, Nat2Z.id. trivial. } Intros s arr_contents'. generalize (Permutation_Zlength _ _ _ H5); intro. forward_call (s, arr, arr_contents', size, s). Intros arr_contents''. forward_if (s > 0). { forward. subst s. Exists arr_contents''. entailer!. split. 2: eapply Permutation_trans; eauto. apply heapOrdered_bounded_root_heapOrdered. apply H7. } { forward. entailer!. } forward. Exists (s - 1) arr_contents''. entailer!. split. 2: eapply Permutation_trans; eauto. red in H7. apply hObU_whObU_pred. replace (1 + Z.to_nat (s-1))%nat with (Z.to_nat s) by rep_lia. trivial. Qed.
imports: RelationClasses Sorting VST.floyd.proofauto CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel CertiGraph.binheap.binary_heap CertiGraph.binheap.env_binary_heap