proposition: Lemma graph_thread_v_in_range: forall g h v, graph_heap_compatible g h -> graph_has_v g v -> v_in_range (vertex_address g v) (gen_start g (vgeneration v)) (WORD_SIZE * gen_size h (vgeneration v)).
proof: Proof. intros. red. unfold vertex_address. exists (WORD_SIZE * vertex_offset g v). split. 2: reflexivity. unfold gen_size. destruct H0. remember (vgeneration v). split. - unfold vertex_offset. unfold WORD_SIZE. pose proof (pvs_ge_zero g (vgeneration v) (vindex v)). rep_lia. - unfold WORD_SIZE. apply Zmult_lt_compat_l. 1: rep_lia. apply Z.lt_le_trans with (used_space (nth_space h n)). 2: apply (proj2 (space_order (nth_space h n))). destruct (gt_gs_compatible _ _ H _ H0) as [? [? ?]]. rewrite <- H4, Heqn. apply vo_lt_gs. subst n. assumption. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics Coq.micromega.Lia compcert.lib.Integers compcert.common.Values VST.veric.base VST.veric.Clight_lemmas VST.veric.val_lemmas VST.veric.shares VST.msl.seplog VST.msl.shares VST.zlist.sublist VST.floyd.coqlib3 VST.floyd.functional_base VST.floyd.data_at_rec_lemmas VST.zlist.list_solver CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen