proposition: Lemma iter_sepcon_vertex_rep_ptrofs: forall g gen b i sh num, Vptr b i = gen_start g gen -> iter_sepcon (map (fun x : nat => (gen, x)) (nat_inc_list num)) (vertex_rep sh g) |-- !! (WORD_SIZE * previous_vertices_size g gen num + Ptrofs.unsigned i < Ptrofs.modulus).
proof: Proof. intros. induction num. 1: entailer. rewrite nat_inc_list_S, map_app, iter_sepcon_app_sepcon. assert_PROP (WORD_SIZE * previous_vertices_size g gen num + Ptrofs.unsigned i < Ptrofs.modulus) by (unfold generation_rep in IHnum; sep_apply IHnum; entailer!!). clear IHnum. simpl iter_sepcon. entailer. unfold vertex_rep at 2. unfold vertex_at. rewrite vertex_head_address_eq. unfold vertex_address, vertex_offset. simpl. rewrite <- H. inv_int i. entailer. destruct H1 as [_ [_ [? _]]]. simpl in H1. destruct H4 as [_ [_ [? _]]]. simpl in H4. rewrite <- H5 in H4. clear H3 H6 H5. rewrite ptrofs_add_repr in *. apply prop_right. pose proof (pvs_ge_zero g gen num). rewrite Ptrofs.unsigned_repr_eq in H1. unfold WORD_SIZE in *. rewrite Z.mod_small in H1 by rep_lia. rewrite pvs_S. unfold vertex_size. rewrite <- fields_eq_length. rewrite Z.mul_add_distr_l, Z.mul_1_r, Z.add_assoc in H4. rewrite Ptrofs.unsigned_repr_eq in H4. rewrite Z.mod_small in H4 by rep_lia. assert ((@Zlength (@reptype CompSpecs int_or_ptr_type) (make_fields_vals g (gen, num))) = (@Zlength val (make_fields_vals g (gen, num)))) by reflexivity. rewrite H5 in *. 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