proposition: Lemma graph_and_heap_rest_valid_ptr: forall (g: LGraph) (h: heap) gen, graph_has_gen g gen -> ti_size_spec h -> graph_heap_compatible g h -> graph_rep g * heap_rest_rep h |-- valid_pointer (space_start (nth_space h gen)).
proof: Proof. intros. sep_apply (graph_and_heap_rest_data_at_ _ _ _ H H1). unfold generation_data_at_. destruct (gt_gs_compatible _ _ H1 _ H) as [? [? ?]]. sep_apply (data_at__memory_block_cancel (nth_sh g gen) (tarray int_or_ptr_type (gen_size h gen)) (gen_start g gen)). simpl sizeof. rewrite Z.max_r by (unfold gen_size; apply (proj1 (total_space_range (nth_space h gen)))). unfold gen_start. if_tac. 2: contradiction. rewrite H2. fold WORD_SIZE. sep_apply (memory_block_valid_ptr (nth_sh g gen) (WORD_SIZE * gen_size h gen) (space_start (nth_space h gen))); unfold WORD_SIZE; [|pose proof (ti_size_gt_0 g h gen H1 H5 H0); lia | entailer!!]. unfold nth_sh. apply readable_nonidentity, writable_readable, generation_share_writable. 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