proposition: Lemma generation_rep_field_compatible: forall g gen, graph_has_gen g gen -> generation_rep g gen |-- !! (field_compatible (tarray int_or_ptr_type (graph_gen_size g gen)) [] (gen_start g gen)).
proof: Proof. intros. pose proof H. apply graph_has_gen_start_isptr in H. remember (gen_start g gen). destruct v; try contradiction. unfold field_compatible. entailer. unfold size_compatible. rewrite sizeof_tarray_int_or_ptr by apply pvs_ge_zero. sep_apply (generation_rep_ptrofs g gen b i Heqv). entailer. rewrite Heqv. sep_apply (generation_rep_align_compatible g gen H0). entailer!!. 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