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. - apply denote_tc_test_eq_split. 2: entailer!. apply graph_local_facts; auto. - forward. Exists g. entailer!. destruct x. 1: simpl in H; inversion H. apply (mark_null_refl g). - 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. localize [data_at 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. unlocalize [graph sh x g]. 1: apply (@root_stable_ramify _ (sSGG_VST sh) g x _ H_GAMMA_g); auto. forward_if. + forward. Exists g. entailer!. eapply (mark_vgamma_true_refl g); eauto. clear - H0; destruct d; [auto | inversion H0]. + assert (d = false) by (destruct d; congruence). subst d. localize [data_at 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. unlocalize [graph sh x (Graph_vgen g x true)]. 1: apply (@root_update_ramify _ (sSGG_VST sh) g x _ (false, l, r) (true, l, r)); auto; eapply Graph_vgen_vgamma; eauto. pose proof Graph_vgen_true_mark1 g x _ _ H_GAMMA_g gx_vvalid. forget (Graph_vgen g x true) as g1. assert (weak_valid g1 l) by (eapply left_weak_valid; eauto). localize [graph sh l g1]. forward_call (sh, g1, l). Intros g2. unlocalize [graph sh x g2] using g2 assuming H4. 1: subst; eapply (@graph_ramify_left _ (sSGG_VST sh) g); eauto. assert (weak_valid g2 r) by (eapply right_weak_valid; eauto). localize [graph sh r g2]. forward_call (sh, g2, r). Intros g3. unlocalize [graph sh x g3] using g3 assuming H6. 1: subst; eapply (@graph_ramify_right _ (sSGG_VST sh) g); eauto. Exists g3. entailer!. apply (mark1_mark_left_mark_right g g1 g2 g3 (ValidPointer b i) l r); auto. Qed.
imports: Demo.env_mark_bin CertiGraph.graph.graph_model CertiGraph.graph.weak_mark_lemmas CertiGraph.msl_application.Graph CertiGraph.msl_application.Graph_Mark CertiGraph.msl_application.GraphBin CertiGraph.msl_application.GraphBin_Mark CertiGraph.floyd_ext.share Demo.spatial_graph_bin_mark