proposition: Lemma body_exch: semax_body Vprog Gprog f_exch exch_spec.
proof: Proof. start_function. rename H1 into Hl1. rename H2 into Hl2. unfold linked_heap_array, heap_array. Intros. forward. { rewrite Znth_map; trivial. } forward. { rewrite Znth_map; trivial. } forward. { repeat rewrite Znth_map; trivial. } forward. { repeat rewrite Znth_map; trivial. } forward. { repeat rewrite Znth_map; trivial. } forward. forward. { repeat rewrite Znth_map; trivial. entailer!. case (eq_dec j k); intro. + subst k. rewrite upd_Znth_same. trivial. rewrite Zlength_map; auto. + rewrite upd_Znth_diff; auto. 2,3: rewrite Zlength_map; auto. remember (@Znth (val * (val * val)) (Vundef, (Vundef, Vundef)) k (map heap_item_rep arr_contents)). assert (In p (map heap_item_rep arr_contents)). { subst p. apply Znth_In. now rewrite Zlength_map. } apply list_in_map_inv in H5. destruct H5 as [x [? ?]]. destruct x. destruct p0. unfold heap_item_rep in H5. simpl in H5. now rewrite H5. } forward. forward. repeat rewrite upd_Znth_same, upd_Znth_overwrite. 3,4: rewrite Zlength_upd_Znth. 2,3,4,5: rewrite Zlength_map; lia. repeat rewrite Znth_map. 2,3: lia. replace (let (x, _) := heap_item_rep (Znth k arr_contents) in x) with (fst (heap_item_rep (Znth k arr_contents))) by trivial. simpl fst. simpl snd. unfold lookup_array. assert (Hl3: forall idx, 0 <= idx < Zlength arr_contents -> 0 <= fst (fst (Znth idx arr_contents)) <= Int.max_unsigned). { intros. destruct H1. specialize (H3 _ H2). cbn in H3. destruct H3. unfold heap_item_key in H3. lia. } forward. { entailer!. destruct H1. destruct (H9 k H0). apply H9. lia. } forward. forward. forward. repeat rewrite upd_Znth_overwrite. repeat rewrite upd_Znth_same. 2,3,4,5,6: repeat rewrite Zlength_upd_Znth; rewrite Zlength_map; rep_lia. simpl snd. unfold heap_item_rep. forward. { entailer!. destruct H1. destruct (H9 j H). apply H9. lia. } Exists (Zexchange lookup_contents (heap_item_key (Znth j arr_contents)) (heap_item_key (Znth k arr_contents))). autorewrite with sublist in *. unfold linked_heap_array, heap_array, lookup_array. repeat rewrite Zlength_Zexchange. entailer!; repeat rewrite Zlength_upd_Znth in *; rewrite Zlength_map in *. { split. apply lookup_oob_eq_Zexchange; auto. apply linked_correctly_Zexchange; auto. } { apply sepcon_derives; apply data_at_ext_derives; auto. * case (Z.eq_dec k j); intro. - subst k. rewrite upd_Znth_overwrite. 2: rewrite Zlength_map; rep_lia. simpl snd. change (Vint (Int.repr (fst (fst (Znth j arr_contents)))), (Vint (snd (fst (Znth j arr_contents))), Vint (snd (Znth j arr_contents)))) with (heap_item_rep (Znth j arr_contents)). rewrite upd_Znth_map, upd_Znth_same_Znth, Zexchange_eq. trivial. lia. - rewrite Znth_upd_Znth_diff; auto. clear H2 H5 H7 H8 H3 H6 H4. change (let (_, z) := let (_, y) := @Znth (val * (val * val)) (Vundef, (Vundef, Vundef)) k (@map heap_item (@reptype CompSpecs t_item) heap_item_rep arr_contents) in y in z) with (snd (snd ((Znth k (map heap_item_rep arr_contents))))). rewrite Znth_map; auto. change (Vint (Int.repr (fst (fst (Znth k arr_contents)))), (Vint (snd (fst (Znth k arr_contents))), Vint (snd (Znth k arr_contents)))) with (heap_item_rep (Znth k arr_contents)). rewrite upd_Znth_map; auto. change (Vint (Int.repr (fst (fst (Znth j arr_contents)))), (Vint (snd (fst (Znth j arr_contents))), Vint (snd (Znth j arr_contents)))) with (heap_item_rep (Znth j arr_contents)). rewrite upd_Znth_map; auto. f_equal. rewrite upd_Znth_Zexchange; auto. * change (Vint (Int.repr j)) with ((fun z : Z => Vint (Int.repr z)) j). rewrite upd_Znth_map. change (Vint (Int.repr k)) with ((fun z : Z => Vint (Int.repr z)) k). rewrite upd_Znth_map. f_equal. change (fst (fst ?c)) with (heap_item_key c). destruct H1 as [Hx H1]. destruct (H1 _ H). destruct (H1 _ H0). rewrite Zexchange_symm; auto. rewrite <- upd_Znth_Zexchange; auto. rewrite H10, H12. trivial. } Time Qed. Lemma body_sink: semax_body Vprog Gprog f_sink sink_spec. Proof. start_function. rename H4 into Hl. assert (Hc : k = Zlength arr_contents \/ 0 <= k < Zlength arr_contents) by lia. destruct Hc as [Hc | Hc]. * forward_loop ( PROP () LOCAL (temp _k (Vint (Int.repr k)); temp _first_available (Vint (Int.repr first_available))) SEP (linked_heap_array arr_contents arr lookup_contents lookup) ). entailer!. forward_if False. exfalso. lia. forward. Exists arr_contents lookup_contents. entailer!. eapply weak_heapOrdered_oob. 2: apply H3. rewrite Zlength_correct, Nat2Z.id. apply le_refl. * assert (Hx : k < Zlength arr_contents) by lia. specialize (H2 Hx). clear H1 Hx. rename H2 into H1. rename H3 into H2. forward_loop (EX k' : Z, EX arr_contents' : list heap_item, EX lookup_contents' : list Z, PROP (0 <= k' < Zlength arr_contents; sink arr_contents (Z.to_nat k) = sink arr_contents' (Z.to_nat k'); lookup_oob_eq arr_contents' lookup_contents lookup_contents') LOCAL (temp _k (Vint (Int.repr k')); temp _arr arr; temp _lookup lookup; temp _first_available (Vint (Int.repr first_available))) SEP (linked_heap_array arr_contents' arr lookup_contents' lookup)). Exists k arr_contents lookup_contents. entailer!. Intros k' arr_contents' lookup_contents'. assert (Zlength arr_contents = Zlength arr_contents'). { unfold sink in H4. generalize (sink_permutation _ cmp_rel cmp_dec arr_contents (Z.to_nat k)); intro. generalize (sink_permutation _ cmp_rel cmp_dec arr_contents' (Z.to_nat k')); intro. apply Permutation_Zlength in H6. apply Permutation_Zlength in H7. congruence. } forward_if (Zleft_child k' < first_available). { forward. entailer!. rewrite Zleft_child_unfold; lia. } { forward. Exists arr_contents' lookup_contents'. entailer!. unfold sink at 2 in H4. rewrite <- Zleft_child_unfold in H7; try lia. unfold Zleft_child in H7. rewrite H6 in H7. rewrite Zlength_correct in H7. erewrite sink_done in H4. 2: apply Znth_nth_error; lia. rewrite <- H4. { split. * apply sink_hO. apply cmp_po. apply cmp_linear. apply H2. * apply sink_permutation. } intros. assert (left_child (Z.to_nat k') < length arr_contents')%nat by (apply nth_error_Some; congruence). lia. intros. assert (right_child (Z.to_nat k') < length arr_contents')%nat by (apply nth_error_Some; congruence). unfold right_child in H8. lia. } forward. rewrite mul_repr, add_repr. rewrite <- Zleft_child_unfold. 2: lia. forward_if (EX b : bool, PROP (if b then Zright_child k' < first_available /\ cmp_rel (Znth (Zright_child k') arr_contents') (Znth (Zleft_child k') arr_contents') else Zright_child k' >= first_available \/ ~cmp_rel (Znth (Zright_child k') arr_contents') (Znth (Zleft_child k') arr_contents') ) LOCAL (temp _t'1 (Val.of_bool b); temp _k (Vint (Int.repr k')); temp _j (Vint (Int.repr (Zleft_child k'))); temp _arr arr; temp _lookup lookup; temp _first_available (Vint (Int.repr first_available))) SEP (linked_heap_array arr_contents' arr lookup_contents' lookup)). { forward_call (Zright_child k', Zleft_child k', arr, arr_contents', lookup, lookup_contents'). { entailer!. simpl. repeat f_equal. rewrite Zright_child_unfold, Zleft_child_unfold; lia. } { rewrite Int.unsigned_repr in H8. rewrite Zright_child_unfold, Zleft_child_unfold in *; lia. rewrite Zleft_child_unfold in *; rep_lia. } forward. Exists (cmp (Znth (Zright_child k') arr_contents') (Znth (Zleft_child k') arr_contents')). unfold cmp_rel. rewrite Zright_child_unfold, Zleft_child_unfold in *. rewrite Int.unsigned_repr in H8. 2,3,4,5: rep_lia. case cmp; entailer!. } { forward. Exists false. rewrite Zright_child_unfold, Zleft_child_unfold in *. rewrite Int.unsigned_repr in H8. entailer!. 1,2,3,4: rep_lia. } Intro b. set (j' := if b then Zright_child k' else Zleft_child k'). forward_if (PROP (if b then Zright_child k' < first_available /\ cmp_rel (Znth (Zright_child k') arr_contents') (Znth (Zleft_child k') arr_contents') else Zright_child k' >= first_available \/ ~cmp_rel (Znth (Zright_child k') arr_contents') (Znth (Zleft_child k') arr_contents') ) LOCAL (temp _t'1 (Val.of_bool b); temp _k (Vint (Int.repr k')); temp _j (Vint (Int.repr j')); temp _arr arr; temp _lookup lookup; temp _first_available (Vint (Int.repr first_available))) SEP (linked_heap_array arr_contents' arr lookup_contents' lookup)); [ destruct b; try discriminate H8.. | ]. { forward. subst j'. rewrite Zright_child_unfold, Zleft_child_unfold in *; try lia. entailer!!. apply H9. } { forward. entailer!!. } Intros. forward_call (k', j', arr, arr_contents', lookup, lookup_contents'). { subst j'. rewrite Zright_child_unfold, Zleft_child_unfold in *; try lia. destruct b; lia. } forward_if (~cmp_rel (Znth k' arr_contents') (Znth j' arr_contents')); try (destruct (cmp _ _) eqn:?H in H9; try discriminate H9). { forward. Exists arr_contents' lookup_contents'. entailer!. unfold sink at 2 in H4. erewrite sink_done in H4; intros. rewrite <- H4. split. apply sink_hO. apply cmp_po. apply cmp_linear. apply H2. apply sink_permutation. apply Znth_nth_error. lia. * rewrite <- (Nat2Z.id (left_child _)) in H0. change (Z.of_nat _) with (Zleft_child k') in H0. rewrite Znth_nth_error in H0. 2: rewrite Zright_child_unfold, Zleft_child_unfold in *; lia. inversion H0. subst b0. clear H0. destruct b; subst j'; auto. transitivity (Znth (Zright_child k') arr_contents'); tauto. * assert (0 <= Zright_child k' < Zlength arr_contents'). { split. unfold Zright_child. lia. apply Z2Nat.inj_lt. unfold Zright_child. lia. lia. rewrite ZtoNat_Zlength. eapply nth_error_Some. unfold Zright_child. rewrite Nat2Z.id. congruence. } rewrite <- (Nat2Z.id (right_child _)) in H0. change (Z.of_nat _) with (Zright_child k') in H0. rewrite Znth_nth_error in H0; try lia. inversion H0. subst b0. clear H0. destruct b; subst j'; auto. destruct H8. lia. transitivity (Znth (Zleft_child k') arr_contents'). trivial. destruct (cmp_linear (Znth (Zleft_child k') arr_contents') (Znth (Zright_child k') arr_contents')); auto. contradiction. } { forward. entailer!. unfold cmp_rel in H0. subst j'. congruence. } forward_call (k', j', arr, arr_contents', lookup, lookup_contents'). { subst j'. rewrite Zright_child_unfold, Zleft_child_unfold in *; try lia. split3. - destruct b; lia. - lia. - destruct H5. apply Permutation_Zlength in H5. lia. } Intros lookup_contents''. forward. Exists j' (Zexchange arr_contents' k' j') lookup_contents''. entailer!. split. subst j'. rewrite Zright_child_unfold, Zleft_child_unfold in *; try lia. destruct b; lia. split. + unfold sink at 2. unfold Zexchange. erewrite sink_step. apply H4. apply Znth_nth_error; lia. unfold left_child. replace (1 + Z.to_nat k' + Z.to_nat k')%nat with (Z.to_nat (2 * k' + 1)) by lia. apply Znth_nth_error. split. lia. rewrite <- Zleft_child_unfold; try lia. rewrite <- Zleft_child_unfold; try lia. case_eq (nth_error arr_contents' (right_child (Z.to_nat k'))); intros. - assert (h = Znth (Zright_child k') arr_contents'). { rewrite <- (nat_of_Z_eq (right_child _)) in H0. rewrite Znth_nth_error in H0. inversion H0. trivial. assert ((Z.to_nat (Z.of_nat (right_child (Z.to_nat k')))) < length arr_contents')%nat by (apply nth_error_Some; congruence). rewrite Zlength_correct. lia. } subst h. assert (Zright_child k' < Zlength arr_contents'). { assert (right_child (Z.to_nat k') < length arr_contents')%nat by (apply nth_error_Some; congruence). unfold Zright_child. rewrite Zlength_correct. lia. } clear H0. subst j'. destruct b. ** right. split. unfold Zright_child. lia. tauto. ** left. split. unfold Zleft_child. lia. destruct H8. lia. tauto. - subst j'. destruct b. ** rewrite H6 in H8. apply nth_error_None in H0. destruct H8. unfold Zright_child in H8. rewrite Zlength_correct in H8. lia. ** split. unfold Zleft_child. lia. tauto. + transitivity lookup_contents'; trivial. eapply lookup_oob_eq_shuffle. 2: apply H5. apply Permutation_map, Zexchange_Permutation. Time Qed. Lemma body_swim: semax_body Vprog Gprog f_swim swim_spec. Proof. start_function. rename H1 into Hz1. rename H2 into Hz2. forward_loop (EX k' : Z, EX arr_contents' : list heap_item, EX lookup_contents' : list Z, PROP (0 <= k' < Zlength arr_contents; swim arr_contents (Z.to_nat k) = swim arr_contents' (Z.to_nat k'); lookup_oob_eq arr_contents' lookup_contents lookup_contents') LOCAL (temp _k (Vint (Int.repr k')); temp _arr arr; temp _lookup lookup) SEP (linked_heap_array arr_contents' arr lookup_contents' lookup)). Exists k arr_contents lookup_contents. entailer!. Intros k' arr_contents' lookup_contents'. assert (Zlength arr_contents = Zlength arr_contents'). { unfold swim in H2. generalize (swim_permutation _ cmp_rel cmp_dec arr_contents (Z.to_nat k)); intro. generalize (swim_permutation _ cmp_rel cmp_dec arr_contents' (Z.to_nat k')); intro. apply Permutation_Zlength in H4. apply Permutation_Zlength in H5. congruence. } generalize (parent_le (Z.to_nat k')); intro Hq. assert (Hx: k' = 0 \/ k' > 0) by lia. forward_if (EX b : bool, PROP (if b then k' > 0 /\ cmp_rel (Znth k' arr_contents') (Znth (Zparent k') arr_contents') else k' = 0 \/ ~cmp_rel (Znth k' arr_contents') (Znth (Zparent k') arr_contents') ) LOCAL (temp _t'1 (Val.of_bool b); temp _k (Vint (Int.repr k')); temp _arr arr; temp _lookup lookup) SEP (linked_heap_array arr_contents' arr lookup_contents' lookup)). { destruct Hx as [Hx | Hx]. subst k'. inversion H5. forward_call (k', Zparent k', arr, arr_contents', lookup, lookup_contents'). { entailer!. rewrite Zparent_repr by lia. rewrite divu_repr by lia. reflexivity. } { assert (parent (Z.to_nat k') <= (Z.to_nat k'))%nat by apply parent_le. unfold Zparent. lia. } forward. unfold cmp_rel. case (cmp (Znth k' arr_contents') (Znth (Zparent k') arr_contents')). Exists true. entailer!. Exists false. entailer!. } { forward. Exists false. entailer!. } Intro b. forward_if (PROP (k' > 0 /\ cmp_rel (Znth k' arr_contents') (Znth (Zparent k') arr_contents')) LOCAL (temp _k (Vint (Int.repr k')); temp _lookup lookup; temp _arr arr) SEP (linked_heap_array arr_contents' arr lookup_contents' lookup)); [ destruct b; try discriminate H5 .. | ]. { forward. entailer!. tauto. } { forward. Exists arr_contents' lookup_contents'. entailer!. split. { assert (heap_ordered (swim arr_contents (Z.to_nat k))). { apply swim_hO; auto. apply cmp_po. apply cmp_linear. } unfold swim at 2 in H2. destruct H6. * subst k'. simpl in H2. rewrite swim_0 in H2. rewrite <- H2. trivial. * erewrite swim_done in H2; eauto. rewrite <- H2. trivial. apply Znth_nth_error; lia. unfold Zparent. rewrite <- Znth_nth_error; try lia. rewrite Nat2Z.id. trivial. } { unfold swim in H2. generalize (swim_permutation _ cmp_rel cmp_dec arr_contents (Z.to_nat k)); intro. generalize (swim_permutation _ cmp_rel cmp_dec arr_contents' (Z.to_nat k')); intro. rewrite H2 in H7. etransitivity. apply H7. symmetry. trivial. } } forward_call (k', Zparent k', arr, arr_contents', lookup, lookup_contents'). { entailer!. rewrite Zparent_repr by lia. rewrite divu_repr by lia. reflexivity. } { split3; [unfold Zparent | | destruct H3; apply Permutation_Zlength in H3]; lia. } Intros lookup_contents''. forward. Exists (Zparent k') (Zexchange arr_contents' k' (Zparent k')) lookup_contents''. entailer!. split. unfold Zparent. lia. split. 2: split. * unfold swim, Zparent, Zexchange in *. rewrite Nat2Z.id. erewrite swim_step. congruence. rewrite H4, Zlength_correct in H1. 4: apply H6. 2: apply Znth_nth_error. 3: rewrite <- Znth_nth_error. 3: rewrite Nat2Z.id; trivial. 1,2,3: lia. * transitivity lookup_contents'; trivial. eapply lookup_oob_eq_shuffle. 2: apply H3. apply Permutation_map, Zexchange_Permutation. * rewrite Zparent_repr by lia. rewrite divu_repr by lia. reflexivity. Time Qed. Lemma body_less: semax_body Vprog Gprog f_less less_spec. Proof. start_function. unfold linked_heap_array, heap_array. Intros. forward. rewrite Znth_map; trivial. forward. do 2 (rewrite Znth_map; trivial). forward. repeat rewrite Znth_map in * by trivial. unfold linked_heap_array, heap_array. simpl. entailer!!. unfold cmp. destruct (negb _); reflexivity. Qed.
imports: RelationClasses VST.floyd.proofauto CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel CertiGraph.binheap.binary_heap_pro CertiGraph.binheap.binary_heap_malloc_spec CertiGraph.binheap.env_binary_heap_pro CertiGraph.binheap.spec_binary_heap_pro