proposition: Lemma body_find: semax_body Vprog Gprog f_find find_spec.
proof: Proof. start_function. rewrite whole_graph_unfold. Intros n. forward. assert (H_BOUND: 0 <= i < Zlength (nat_inc_list n)) by (rewrite Zlength_correct, nat_inc_list_length, H0; assumption). forward. - apply prop_right. rewrite H0. auto. - rewrite <- (map_id (nat_inc_list n)) at 1. rewrite Znth_nat_inc_list. 2: rewrite H0; auto. simpl id. forward_if (EX g': UFGraph, EX rt: Z, PROP (uf_equiv g g' /\ uf_root g' i rt) LOCAL (temp _p (Vint (Int.repr rt)); temp _subsets (pointer_val_val subsets); temp _i (Vint (Int.repr i))) SEP (whole_graph sh g' subsets)). + rewrite whole_graph_fold; [|intuition..]. destruct (vgamma (lg_gg g) i) eqn: ?. forward_call (sh, g, subsets, z). * unfold vgamma, UnionFindGraph.vgamma in Heqp. inversion Heqp. clear Heqp. destruct (Z_lt_dec (dst (lg_gg g) i) 0). 1: exfalso; apply H2; auto. destruct ((proj2 (@only_one_edge _ _ _ _ _ _ (liGraph g) _ i H)) (eq_refl i)) as [_ ?]. destruct (valid_graph g _ H3) as [_ [? | ?]]; auto. hnf in H6. exfalso. apply n1. auto. * Intros vret. destruct vret as [g' root]. simpl fst in *. simpl snd in *. rewrite whole_graph_unfold. Intros n'. forward. Opaque Znth. forward. Transparent Znth. -- apply prop_right. rewrite H5. destruct H3. rewrite <- H3. auto. -- assert (n' = n). { destruct H3, (lt_eq_lt_dec n n'); [destruct s|]; auto; exfalso. - specialize (H3 (Z.of_nat n)). specialize (H0 (Z.of_nat n)). specialize (H5 (Z.of_nat n)). rewrite <- H0 in H3. rewrite <- H3 in H5. lia. - specialize (H3 (Z.of_nat n')). specialize (H0 (Z.of_nat n')). specialize (H5 (Z.of_nat n')). rewrite <- H0 in H3. rewrite <- H3 in H5. lia. } subst n'. assert (z <> i) by (unfold vgamma, UnionFindGraph.vgamma in Heqp; inversion Heqp; intro; apply H2; rewrite H9 in H7; rewrite H9; subst i; auto). assert (weak_valid g' root) by (right; destruct H4; apply reachable_foot_valid in H4; auto). assert (vvalid g' i) by (destruct H3 as [? _]; rewrite <- H3; apply H). assert (~ reachable g' root i) by (apply (uf_equiv_not_reachable g g' i n0 z root); auto). apply (exp_right (Graph_gen_redirect_parent g' i root H8 H9 H10)). apply (exp_right root). rewrite Znth_nat_inc_list. 2: rewrite H0; auto. Opaque vgamma2cdata. Opaque vgamma. entailer !; [split|]. Transparent vgamma. Transparent vgamma2cdata. ++ apply (graph_gen_redirect_parent_equiv g g' i n0 z); auto. ++ apply (uf_root_gen_dst_same g' (liGraph g') i i root); auto. ** rewrite <- (uf_equiv_root_the_same g g' i root); auto. apply (uf_root_edge _ (liGraph g) _ z); [| apply (vgamma_not_dst g i n0 z) | rewrite (uf_equiv_root_the_same g g')]; auto. ** apply reachable_refl; auto. ++ rewrite whole_graph_unfold. apply (exp_right n). entailer. unfold vgamma2cdata at 2. unfold vgamma at 2. unfold UnionFindGraph.vgamma. cut ((upd_Znth i (map (fun x : Z => vgamma2cdata (vgamma (lg_gg g') x)) (nat_inc_list n)) (Vint (Int.repr root), Vint (Int.repr (Z.of_nat (vlabel (lg_gg g') i))))) = (map (fun x : Z => vgamma2cdata (vgamma (lg_gg (Graph_gen_redirect_parent g' i root H8 H9 H10)) x)) (nat_inc_list n))); intros. ** rewrite <- H15. apply derives_refl. ** rewrite <- H0 in H. destruct H4. apply reachable_foot_valid in H4. rewrite <- H5 in H4. clear -H H4. rewrite <- upd_Znth_Graph_redirect_parent; auto. + unfold vgamma2cdata at 1. unfold vgamma at 1. unfold UnionFindGraph.vgamma. forward. rewrite whole_graph_fold; [|intuition..]. apply (exp_right g). simpl projT2. simpl id. apply (exp_right i). entailer !. split; [|split]. 1: apply (uf_equiv_refl _ (liGraph g)). 2: rewrite <- H2; reflexivity. destruct (Z_lt_dec (dst (lg_gg g) i) 0). * split. 1: apply reachable_refl; auto. intros. destruct H4 as [[? ?] ?]. destruct H4 as [[? ?] [? ?]]. simpl in H4. subst z. destruct l0. -- simpl in H5. auto. -- simpl in H6. destruct H6. assert (strong_evalid g z) by (destruct l0; [|destruct H6]; auto). destruct H8 as [? [? ?]]. symmetry in H4. destruct (@only_one_edge _ _ _ _ _ _ (liGraph g) _ z H) as [? _]. specialize (H11 (conj H4 H8)). simpl in H11. subst z. rewrite <- H0 in H10. destruct H10. assert (dst g i < 0) by apply l. exfalso; lia. * destruct (vvalid_src_evalid _ (liGraph g) i H) as [_ ?]. destruct (valid_graph g _ H4) as [_ [? | ?]]. 1: simpl in H5; exfalso; auto. simpl id in *. rewrite <- H0 in H5. rewrite <- H0 in H. apply repr_inj_unsigned in H2. -- exfalso. rewrite H0 in H. assert (reachable g i i) by (apply reachable_refl; auto). pose proof (dst_not_reachable _ (liGraph g) _ _ _ H H2 H6). auto. -- split. 1: lia. rewrite Z.lt_eq_cases. left. apply Z.lt_trans with (Int.max_signed / 8). 2: reflexivity. destruct H5. apply Z.lt_le_trans with (Z.of_nat n); auto. -- split. 1: lia. rewrite Z.lt_eq_cases. left. apply Z.lt_trans with (Int.max_signed / 8). 2: compute; auto. destruct H. apply Z.lt_le_trans with (Z.of_nat n); auto. + Intros g' rt. forward. apply (exp_right g'). apply (exp_right rt). entailer !. Qed.
imports: CertiGraph.lib.List_ext CertiGraph.sample_mark.env_unionfind_arr CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.reachable_computable CertiGraph.graph.UnionFind CertiGraph.msl_application.UnionFindGraph CertiGraph.msl_application.ArrayGraph CertiGraph.floyd_ext.share CertiGraph.sample_mark.spatial_array_graph Coq.Lists.List