proposition: Lemma vertex_rep_memory_block: forall sh g v, vertex_rep sh g v |-- memory_block sh (WORD_SIZE * vertex_size g v) (offset_val (- WORD_SIZE) (vertex_address g v)).
proof: Proof. intros. sep_apply (vertex_rep_isptr sh g v). Intros. destruct v as [gen num]. unfold vertex_rep, vertex_at. simpl in H. rewrite vertex_head_address_eq. unfold vertex_address, vertex_offset. simpl. remember (gen_start g gen). destruct v; try contradiction. remember (previous_vertices_size g gen num). assert (0 <= z) by (rewrite Heqz; apply pvs_ge_zero). unfold vertex_size. entailer. rewrite <- fields_eq_length. destruct H1 as [_ [_ [? _]]]. simpl in H1. destruct H3 as [_ [_ [? _]]]. simpl in H3. rewrite <- H4 in H3. remember (previous_vertices_size g gen num). remember (Zlength (make_fields_vals g (gen, num))). rewrite (Z.add_comm z0). rewrite Z.mul_add_distr_l with (m := 1). rewrite Z.mul_1_r. simpl offset_val. remember (Ptrofs.add i (Ptrofs.repr (WORD_SIZE * z))). rewrite <- (Ptrofs.repr_unsigned i0). remember (Ptrofs.unsigned i0) as ofs. assert (Ptrofs.add i (Ptrofs.repr (WORD_SIZE * (z + 1))) = Ptrofs.repr (ofs + WORD_SIZE)). { unfold WORD_SIZE in *. rewrite Z.mul_add_distr_l, Z.mul_1_r. rewrite <- ptrofs_add_repr, <- Ptrofs.add_assoc. rewrite Ptrofs.add_unsigned. rewrite <- Heqi0. rewrite <- Heqofs. f_equal. } assert (Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr (WORD_SIZE * (z + 1)))) = ofs + WORD_SIZE). { rewrite H6, Ptrofs.unsigned_repr_eq. apply Z.mod_small. destruct (Ptrofs.unsigned_range i0). rewrite <- Heqofs in *. unfold WORD_SIZE. lia. } rewrite H6. assert (0 <= z0) by (subst z0; apply Zlength_nonneg). 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 H9 in H3. clear H9. rewrite <- Heqz0 in *. rewrite memory_block_split; [|unfold WORD_SIZE in *; rep_lia..]. sep_apply (data_at_memory_block sh (if Archi.ptr64 then tulong else tuint) (Z2val (make_header g (gen, num))) (Vptr b (Ptrofs.repr ofs))). simpl sizeof. unfold WORD_SIZE. apply cancel_left. fold WORD_SIZE. sep_apply (data_at_memory_block sh (tarray int_or_ptr_type z0) (make_fields_vals g (gen, num)) (Vptr b (Ptrofs.repr (ofs + WORD_SIZE)))). unfold WORD_SIZE. simpl sizeof. rewrite Z.max_r; 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