proposition: Lemma graph_and_heap_rest_v_in_range_iff: forall g h gen v, graph_heap_compatible g h -> graph_has_gen g gen -> graph_has_v g v -> graph_rep g * heap_rest_rep h |-- !! (v_in_range (vertex_address g v) (gen_start g gen) (WORD_SIZE * gen_size h gen) <-> vgeneration v = gen).
proof: Proof. intros. unfold iff. rewrite and_comm. apply prop_and_right. - intros. rewrite <- H2. apply graph_thread_v_in_range; assumption. - rewrite prop_impl, <- imp_andp_adjoint; Intros. destruct (Nat.eq_dec (vgeneration v) gen). 1: apply prop_right; assumption. sep_apply (graph_heap_rest_iter_sepcon _ _ H). pose proof (graph_thread_v_in_range _ _ _ H H1). destruct H1. assert (NoDup [vgeneration v; gen]) by (constructor; [|constructor; [|constructor]]; intro HS; simpl in HS; destruct HS; auto). assert (incl [vgeneration v; gen] (nat_inc_list (length (g_gen (glabel g))))) by (apply incl_cons; [|apply incl_cons]; [rewrite nat_inc_list_In_iff; assumption..| apply incl_nil]). sep_apply (iter_sepcon_incl_true (generation_data_at_ g h) H5 H6); simpl. rewrite sepcon_emp. unfold generation_data_at_. remember (nth_sh g (vgeneration v)) as sh1. remember (nth_sh g gen) as sh2. sep_apply (v_in_range_data_at_ _ _ _ sh1 H3). Intros m1. sep_apply (v_in_range_data_at_ _ _ _ sh2 H2). Intros m2. remember (vertex_address g v) as p. rewrite <- sepcon_assoc, (sepcon_comm (memory_block sh2 m2 p)), (sepcon_assoc TT). sep_apply (readable_writable_memory_block_FF sh2 sh1 m2 m1 p); auto. + apply writable_readable. subst. apply generation_share_writable. + subst. apply generation_share_writable. + entailer!. 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