proposition: Lemma isolate_frame: forall sh frames z, 0 <= z < Zlength (map rp_val (frames2rootpairs frames)) -> frames_rep sh frames |-- data_at sh int_or_ptr_type (Znth z (map rp_val (frames2rootpairs frames))) (frame_root_address frames z) * ALL v:val, data_at sh int_or_ptr_type v (frame_root_address frames z) -* frames_rep sh (update_frames frames (upd_Znth z (map rp_val (frames2rootpairs frames)) v)).
proof: Proof. intros. unfold frames_rep. revert z H. unfold frames2rootpairs. induction frames as [ | [a r s] rest ]; simpl; intros. - list_solve. - autorewrite with sublist in H. simpl in H. if_tac. + clear IHrest. Intros. unfold roots_rep, frames2rootpairs. simpl iter_sepcon. rewrite iter_sepcon_app_sepcon. change (iter_sepcon (concat _) _) with (roots_rep sh (frames2rootpairs rest)). unfold frame2rootpairs. rewrite iter_sepcon_frame2rootpairs' by auto with field_compatible. simpl fr_roots. simpl fr_root. rewrite !Znth_map by list_solve. rewrite Znth_app1 by list_solve. erewrite (data_at_tarray_split _ _ z) by (try reflexivity; list_solve). erewrite (data_at_tarray_split _ (Zlength s - z) 1). 3: instantiate (1 := (sublist z (Zlength s) s)). all: try reflexivity. all: try list_solve. rewrite !sublist_sublist by lia. rewrite (sublist_one (0+z) (1+z)) by list_solve. erewrite data_at_singleton_array_eq by reflexivity. rewrite !Z.sub_add. rewrite Z.add_0_l. change (sizeof int_or_ptr_type) with WORD_SIZE. rewrite <- (Z.mul_comm WORD_SIZE). autorewrite with sublist. cancel. apply allp_right; intro v. rewrite !map_app. rewrite !upd_Znth_app1 by list_solve. autorewrite with sublist. rewrite prop_true_andp by auto. rewrite (sublist_same 0 (Zlength (concat _))) by list_solve. change (concat (map _ rest)) with(frames2rootpairs rest). rewrite update_frames_same. apply -> wand_sepcon_adjoint. rewrite iter_sepcon_app_sepcon. rewrite iter_sepcon_frame2rootpairs' by list_simplify. autorewrite with sublist. change (iter_sepcon _ _) with (roots_rep sh (frames2rootpairs rest)). cancel. erewrite (data_at_tarray_split _ (Zlength s) z). 4: reflexivity. all: try reflexivity. all: try list_solve. rewrite sublist_upd_Znth_l by list_solve. cancel. erewrite (data_at_tarray_split _ (Zlength s - z) 1). 4: instantiate (1 := sublist z (Zlength s) (upd_Znth z s v)). all: try reflexivity. all: try list_solve. autorewrite with sublist. rewrite (sublist_one (0+z) (1+z)) by list_solve. erewrite data_at_singleton_array_eq by reflexivity. rewrite Z.add_0_l. rewrite upd_Znth_same by lia. rewrite sublist_upd_Znth_r by lia. cancel. + Intros. unfold roots_rep, frames2rootpairs. simpl iter_sepcon. rewrite iter_sepcon_app_sepcon. change (iter_sepcon (concat _) _) with (roots_rep sh (frames2rootpairs rest)). unfold frame2rootpairs. rewrite iter_sepcon_frame2rootpairs' by auto with field_compatible. simpl fr_roots. simpl fr_root. rewrite !map_app. rewrite Znth_app2 by list_solve. change (concat (map _ rest)) with (frames2rootpairs rest) in *. sep_apply (IHrest (z-Zlength s)); clear IHrest; try list_solve. autorewrite with sublist. cancel. do 2 sep_apply allp_sepcon1. apply allp_right; intro v. apply allp_left with (x:=v). repeat sep_apply log_normalize.sepcon_wand_wand_sepcon. apply wand_derives; auto. rewrite !upd_Znth_app2 by list_solve. autorewrite with sublist. rewrite prop_true_andp by auto. rewrite frames_p_update_frames. rewrite iter_sepcon_app_sepcon. rewrite iter_sepcon_frame2rootpairs' by auto. cancel. apply derives_refl. 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