proposition: Lemma vertex_rep_valid_int_or_ptr: forall sh g v, vertex_rep sh g v |-- !! (valid_int_or_ptr (vertex_address g v)).
proof: Proof. intros. sep_apply (vertex_rep_isptr sh g v). Intros. unfold vertex_rep, vertex_at, vertex_address. remember (gen_start g (vgeneration v)) as vv. destruct vv; try contradiction. inv_int i. entailer!. destruct H3 as [_ [_ [_ [? _]]]]. clear -H3. hnf in H3. inv H3. 1: simpl in H; inversion H. assert (0 <= 0 < Zlength (make_fields_vals g v)). { split; [lia|]. rewrite fields_eq_length. destruct (raw_fields_head_cons (vlabel g v)) as [r [l [? _]]]. rewrite H. rewrite Zlength_cons. pose proof (Zlength_nonneg l). lia. } apply H4 in H. rewrite Z.mul_0_r, Z.add_0_r in H. clear H4. inv H. inv H0. simpl in H1. fold WORD_SIZE in *. split. - simpl; rewrite !ptrofs_add_repr in *. apply (even_divided_odd_false WORD_SIZE); easy. - rewrite !ptrofs_add_repr in *. apply (four_divided_tenth_pl_false WORD_SIZE); [apply four_div_WORD_SIZE | easy]. 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