proposition: Lemma generation_rep_align_compatible: forall g gen, graph_has_gen g gen -> generation_rep g gen |-- !! (align_compatible (tarray int_or_ptr_type (graph_gen_size g gen)) (gen_start g gen)).
proof: Proof. intros. apply graph_has_gen_start_isptr in H. remember (gen_start g gen). destruct v; try contradiction. sep_apply (generation_rep_ptrofs g gen b i Heqv). Intros. unfold generation_rep, graph_gen_size in *. remember (number_of_vertices (nth_gen g gen)) as num. clear Heqnum. remember (nth_sh g gen) as sh. clear Heqsh. induction num. - unfold previous_vertices_size. simpl fold_left. apply prop_right. constructor. intros. lia. - unfold generation_rep. rewrite nat_inc_list_S, map_app, iter_sepcon_app_sepcon. simpl iter_sepcon. entailer. unfold vertex_rep at 2. unfold vertex_at. rename H0 into HS. rewrite vertex_head_address_eq. entailer!. clear H1 H2 H3 H4. destruct H0 as [_ [_ [_ [? _]]]]. rewrite <- Heqv in H0. inv_int i. hnf in H0. rewrite ptrofs_add_repr in H0. inv H0. simpl in H1. inv H1. simpl in H3. simpl in HS. pose proof (svs_gt_one g (gen, num)). pose proof (pvs_ge_zero g gen num). rewrite pvs_S in HS. rewrite Ptrofs.unsigned_repr_eq in H3. unfold WORD_SIZE in *. rewrite Z.mod_small in H3 by rep_lia. rewrite Z.add_comm in H3. apply Z.divide_add_cancel_r in H3. 2: apply Z.divide_factor_l. constructor. intros. rewrite Ptrofs.unsigned_repr_eq. rewrite Z.mod_small by lia. simpl sizeof. apply align_compatible_rec_by_value with Mptr. 1: reflexivity. simpl. apply Z.divide_add_r; [assumption | apply Z.divide_factor_l]. 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