proposition: Lemma body_mark: semax_body Vprog Gprog f_mark mark_spec.
proof: Proof. start_function. remember (vgamma g x) as dlr eqn:?H. destruct dlr as [[d l] r]. rename H0 into H_GAMMA_g; symmetry in H_GAMMA_g. rename H into H_weak_valid. forward_if (PROP (pointer_val_val x <> nullval) LOCAL (temp _x (pointer_val_val x)) SEP (dag sh x g)). - apply denote_tc_test_eq_split. 2: entailer!. apply dag_local_facts; auto. - forward. Exists g. entailer!. destruct x. 1: simpl in H; inversion H. apply (mark_null_refl g). - forward. entailer!. - Intros. assert (vvalid g x) as gx_vvalid. { destruct H_weak_valid; [| auto]. unfold is_null_SGBA in H0; simpl in H0; subst x. exfalso. apply H. auto. } assert (isptr (pointer_val_val x) /\ exists b i, x = ValidPointer b i). { destruct x. 2: exfalso; apply H; reflexivity. split; simpl; auto. exists b, i. reflexivity. } destruct H0 as [? [b [i ?]]]. clear H0 H_weak_valid. pose proof (@root_unfold _ (sSGG_VST sh) g x d l r gx_vvalid). simpl in H0. simpl reachable_dag_vertices_at. erewrite H0 by eauto. Intros. change (vertex_at x (d, l, r)) with (@data_at CompSpecs sh node_type (Vint (Int.repr (if d then 1 else 0)), (pointer_val_val l, pointer_val_val r)) (pointer_val_val x)). forward. eapply semax_pre with (PROP () LOCAL (temp _root_mark (Vint (Int.repr (if d then 1 else 0))); temp _x (pointer_val_val x)) SEP (dag sh x g)). 1: { pose proof (@root_unfold _ (sSGG_VST sh) g x d l r gx_vvalid). simpl in H2. simpl reachable_dag_vertices_at. erewrite H2 by eauto; simpl vertex_at; entailer!. } forward_if (PROP (d = false) LOCAL (temp _x (pointer_val_val x)) SEP (dag sh x g)). + forward. Exists g. entailer!. eapply (mark_vgamma_true_refl g); eauto. now destruct d. + forward. entailer!. now destruct d. + pose proof (@root_unfold _ (sSGG_VST sh) g x d l r gx_vvalid). simpl in H2. simpl reachable_dag_vertices_at. erewrite H2 by eauto. Intros. subst d. change (vertex_at x (false, l, r)) with (@data_at CompSpecs sh node_type (Vint (Int.repr 0), (pointer_val_val l, pointer_val_val r)) (pointer_val_val x)). forward. 1: entailer!; destruct l; simpl; auto. forward. 1: entailer!; destruct r; simpl; auto. forward. pose proof Graph_vgen_true_mark1 g x _ _ H_GAMMA_g gx_vvalid. apply semax_pre with (PROP () LOCAL (temp _r (pointer_val_val r); temp _l (pointer_val_val l); temp _x (pointer_val_val x)) SEP (dag sh x (Graph_vgen g x true))). 1: { pose proof (@root_update_unfold _ (sSGG_VST sh) g). simpl in H4. simpl reachable_dag_vertices_at. erewrite H4 by eauto; simpl vertex_at; entailer!. } forget (Graph_vgen g x true) as g1. assert (weak_valid g1 l) by (eapply left_weak_valid; eauto). localize [dag sh l g1]. forward_call (sh, g1, l). Intros g2. unlocalize [dag sh x g2] using g2 assuming H5. 1: { subst. pose proof (@dag_ramify_left _ (sSGG_VST sh) g g1 (ValidPointer b i) l r gx_vvalid H_GAMMA_g H3). simpl reachable_dag_vertices_at in *. eapply H1. } assert (weak_valid g2 r) by (eapply right_weak_valid; eauto). localize [dag sh r g2]. forward_call (sh, g2, r). Intros g3. unlocalize [dag sh x g3] using g3 assuming H7. 1: { subst. pose proof (@dag_ramify_right _ (sSGG_VST sh) g _ _ _ _ _ gx_vvalid H_GAMMA_g H3 H5). simpl reachable_dag_vertices_at in *; eapply H1. } Exists g3. entailer!. apply (mark1_mark_left_mark_right g g1 g2 g3 (ValidPointer b i) l r); auto. Qed.
imports: CertiGraph.lib.Coqlib VST.floyd.proofauto CertiGraph.mark.env_mark_bin CertiGraph.graph.graph_model CertiGraph.graph.weak_mark_lemmas CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.reachable_computable CertiGraph.msl_application.Graph CertiGraph.msl_application.GraphBin CertiGraph.msl_application.Graph_Mark CertiGraph.msl_application.DagBin_Mark CertiGraph.floyd_ext.share CertiGraph.mark.spatial_graph_bin_mark VST.msl.wand_frame VST.floyd.reassoc_seq VST.floyd.field_at_wand