proposition: Lemma body_find: semax_body Vprog Gprog f_find find_spec.
proof: Proof. start_function. remember (vgamma g x) as rpa eqn:?H. destruct rpa as [r pa]. symmetry in H0. Opaque pointer_val_val. forward. Transparent pointer_val_val. localize [data_at sh node_type (vgamma2cdata (vgamma g x)) (pointer_val_val x)]. rewrite H0. simpl vgamma2cdata. forward. 1: entailer!; destruct pa; simpl; auto. unlocalize [whole_graph sh g]. 1: rewrite H0; simpl; apply (@vertices_at_ramif_1_stable _ _ _ _ SGBA_VST _ _ (SGA_VST sh) g (vvalid g) x (r, pa)); auto. forward_while (EX p: pointer_val, EX ppa: pointer_val, PROP (reachable g x p /\ vgamma g p = (vlabel g p, ppa)) LOCAL (temp _p (pointer_val_val ppa); temp _tmp (pointer_val_val p); temp _x (pointer_val_val x)) SEP (vertices_at sh (vvalid g) g)). - Exists x pa. entailer!. split; [apply reachable_refl | f_equal; simpl in H0; inversion H0]; auto. - entailer!. destruct H1. apply reachable_foot_valid in H1. pose proof (valid_parent _ _ _ _ H1 H5). apply denote_tc_test_eq_split; apply graph_local_facts; auto. - destruct H1. Opaque pointer_val_val. forward. Transparent pointer_val_val. remember (vgamma g ppa) as rpa eqn:?H. destruct rpa as [mr mgpa]. symmetry in H3. assert (H_VALID_PPA: vvalid g ppa) by (apply (valid_parent _ p (vlabel g p)); [apply reachable_foot_valid in H1 |]; auto). localize [data_at sh node_type (vgamma2cdata (vgamma g ppa)) (pointer_val_val ppa)]. rewrite H3. simpl vgamma2cdata. forward. 1: entailer!; destruct mgpa; simpl; auto. unlocalize [whole_graph sh g]. 1: rewrite H3; simpl; apply (@vertices_at_ramif_1_stable _ _ _ _ SGBA_VST _ _ (SGA_VST sh) g (vvalid g) ppa (mr, mgpa)); auto. Exists (ppa, mgpa). simpl fst. simpl snd. assert (mr = vlabel g ppa) by (simpl in H3; inversion H3; auto). rewrite <- H4. entailer !. apply reachable_edge with p; auto. apply (vgamma_not_edge g p (vlabel g p)); auto. apply reachable_foot_valid in H1; auto. intro. subst. apply HRE; trivial. - destruct H1. rename HRE into Htemp. assert (HRE: p = ppa). { destruct p; destruct ppa; inversion Htemp; trivial. } subst ppa. assert (uf_root g x p) by (split; intros; auto; apply (parent_loop g p (vlabel g p) y); auto). forward_while (EX g': UFGraph, EX tmp: pointer_val, EX xv: pointer_val, PROP (uf_equiv g g' /\ uf_root g' xv p) LOCAL (temp _p (pointer_val_val p); temp _tmp (pointer_val_val tmp); temp _x (pointer_val_val xv)) SEP (whole_graph sh g')). + Exists g p x. entailer!. apply (uf_equiv_refl _ (liGraph g)). + entailer!. apply denote_tc_test_eq_split; apply graph_local_facts. * destruct H4 as [_ [? _]]. apply reachable_head_valid in H4; assumption. * destruct H4 as [[? _] _]. rewrite <- H4. apply reachable_foot_valid in H1; assumption. + destruct H4 as [? ?]. rename HRE into Htemp'. assert (HRE: xv <> p). { intro; subst; apply Htemp'; trivial. } remember (vgamma g' xv) as rpa eqn:?H. destruct rpa as [xr xpa]. symmetry in H6. assert (H_VALID_XV: vvalid g' xv) by (destruct H5 as [? _]; apply reachable_head_valid in H5; auto). localize [data_at sh node_type (vgamma2cdata (vgamma g' xv)) (pointer_val_val xv)]. rewrite H6. simpl vgamma2cdata. forward. 1: entailer!; destruct xpa; simpl; auto. unlocalize [whole_graph sh g']. 1: rewrite H6; apply (@vertices_at_ramif_1_stable _ _ _ _ SGBA_VST _ _ (SGA_VST sh) g' (vvalid g') xv (xr, xpa)); auto. assert (weak_valid g' p) by (right; destruct H4; rewrite <- H4; apply reachable_foot_valid in H1; auto). assert (vvalid g' xv) by (destruct H5; apply reachable_head_valid in H5; auto). assert (~ reachable g' p xv) by (intro; destruct H5 as [_ ?]; specialize (H5 _ H9); auto). assert (vertices_at sh (vvalid (Graph_gen_redirect_parent g' xv p H7 H8 H9)) (Graph_gen_redirect_parent g' xv p H7 H8 H9) = vertices_at sh (vvalid g') (Graph_gen_redirect_parent g' xv p H7 H8 H9)). { apply vertices_at_Same_set. unfold Ensembles.Same_set, Ensembles.Included, Ensembles.In. simpl. intuition. } assert (H_P_NOT_NULL: p <> null) by (apply reachable_foot_valid in H1; intro; subst p; apply (valid_not_null g null H1); simpl; auto). localize [data_at sh node_type (Vint (Int.repr (Z.of_nat xr)), pointer_val_val xpa) (pointer_val_val xv)]. forward. unlocalize [whole_graph sh (Graph_gen_redirect_parent g' xv p H7 H8 H9)]. 1: rewrite H10; apply (@graph_gen_redirect_parent_ramify _ (sSGG_VST sh)); auto. Opaque pointer_val_val. forward. Transparent pointer_val_val. Exists (((Graph_gen_redirect_parent g' xv p H7 H8 H9), xpa), xpa). simpl fst. simpl snd. rewrite H10. entailer !. split. * apply (graph_gen_redirect_parent_equiv' g g' xv p); auto. * apply (uf_root_gen_dst_preserve g' (liGraph g')); auto. -- apply (vgamma_not_reachable _ _ xr); auto. pose proof (uf_root_not_eq_root_vgamma g' _ _ _ _ H6 H5 HRE). auto. -- apply (vgamma_uf_root g' xv xr xpa p); auto. + destruct H4. forward. Exists g' p. entailer!. rewrite <- (uf_equiv_root_the_same g g' x p); auto. Qed.
imports: CertiGraph.unionfind.env_unionfind_iter CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.reachable_computable CertiGraph.msl_application.Graph CertiGraph.msl_application.UnionFindGraph CertiGraph.msl_application.GList CertiGraph.msl_application.GList_UnionFind CertiGraph.floyd_ext.share CertiGraph.unionfind.spatial_graph_uf_iter