proposition: Lemma lmc_vertex_rep_eq: forall sh g v new_v, vertex_rep sh (lgraph_mark_copied g v new_v) v = data_at sh (if Archi.ptr64 then tulong else tuint) (Z2val 0) (offset_val (- WORD_SIZE) (vertex_address g v)) * data_at sh int_or_ptr_type (vertex_address g new_v) (vertex_address g v) * data_at sh (tarray int_or_ptr_type (Zlength (make_fields_vals g v) - 1)) (tl (make_fields_vals g v)) (offset_val WORD_SIZE (vertex_address g v)).
proof: Proof. intros. unfold vertex_rep. rewrite lmc_vertex_address. unfold vertex_at. rewrite sepcon_assoc. f_equal. - f_equal. unfold make_header. simpl vlabel at 1. unfold update_copied_old_vlabel, graph_gen.update_vlabel. rewrite if_true by reflexivity. simpl. unfold Z2val. reflexivity. - rewrite lmc_make_fields_vals_eq, data_at_tarray_value_split_1. + simpl hd. f_equal. simpl tl. replace (Zlength (vertex_address g new_v :: tl (make_fields_vals g v)) - 1) with (Zlength (make_fields_vals g v) - 1). 1: reflexivity. transitivity (Zlength (tl (make_fields_vals g v))). 2: rewrite Zlength_cons; rep_lia. assert (0 < Zlength (make_fields_vals g v)) by (rewrite fields_eq_length; apply (proj1 (raw_fields_range (vlabel g v)))). remember (make_fields_vals g v). destruct l. 1: rewrite Zlength_nil in H; lia. rewrite Zlength_cons. simpl. lia. + rewrite Zlength_cons. rep_lia. Qed.
imports: VST.veric.compcert_rmaps VST.msl.shares VST.msl.wand_frame VST.concurrency.conclib CertiGraph.lib.List_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.ramification_lemmas CertiGraph.graph.graph_model CertiGraph.CertiGC.GCGraph CertiGraph.CertiGC.env_graph_gc CertiGraph.msl_ext.iter_sepcon Coq.Lists.List