proposition: Lemma generation_rep_memory_block: forall g gen, graph_has_gen g gen -> generation_rep g gen |-- memory_block (nth_sh g gen) (WORD_SIZE * 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. unfold generation_rep, graph_gen_size. remember (number_of_vertices (nth_gen g gen)) as num. clear Heqnum. remember (nth_sh g gen) as sh. clear Heqsh. induction num. - simpl. rewrite memory_block_zero_Vptr. auto. - sep_apply (iter_sepcon_vertex_rep_ptrofs g gen b i sh (S num) Heqv). Intros. rename H0 into HS. simpl in HS. unfold generation_rep. rewrite nat_inc_list_S, map_app, iter_sepcon_app_sepcon. simpl. unfold generation_rep in IHnum. sep_apply IHnum. rewrite pvs_S, Z.add_comm. rewrite <- (Ptrofs.repr_unsigned i) at 2. remember (previous_vertices_size g gen num) as zp. assert (0 <= zp) by (rewrite Heqzp; apply pvs_ge_zero). pose proof (svs_gt_one g (gen, num)) as HS1. pose proof (Ptrofs.unsigned_range i) as HS2. rewrite pvs_S in HS. rewrite Z.add_comm, Z.mul_add_distr_l, memory_block_split; [| unfold WORD_SIZE in *; rep_lia..]. rewrite (Ptrofs.repr_unsigned i). apply cancel_left. sep_apply (vertex_rep_memory_block sh g (gen, num)). rewrite vertex_head_address_eq, <- Heqzp, <- Heqv. simpl offset_val. rewrite <- ptrofs_add_repr, Ptrofs.repr_unsigned. auto. 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