proposition: Lemma iter_sepcon_frame2rootpairs': forall (sh: share) (r: val) (s: list val), field_compatible0 (tarray int_or_ptr_type (Zlength s)) [] r -> iter_sepcon (frame2rootpairs' r 0 s) (fun av => data_at sh int_or_ptr_type (rp_val av) (rp_adr av)) = data_at sh (tarray int_or_ptr_type (Zlength s)) s r.
proof: Proof. intros. replace r with (offset_val (0*WORD_SIZE) r) at 2 by (apply isptr_offset_val_zero; auto with field_compatible). set (n := Zlength s) in *. unfold n. replace 0 with (n - Zlength s) by lia. assert (Zlength s <= n) by lia. clearbody n. induction s; simpl. change (Zlength nil) with 0. rewrite data_at_zero_array_eq; try reflexivity. auto with field_compatible. change (a::s) with ([a]++s). rewrite split2_data_at_Tarray_app with (mid:=1) by list_solve. f_equal. symmetry. apply data_at_singleton_array_eq; auto. replace (Z.succ _) with (n - Zlength s) by list_solve. rewrite IHs by list_solve. replace (Zlength _ - _) with (Zlength s) by list_solve. f_equal. replace (Zlength (_ ++ _)) with (1 + Zlength s) by list_solve. unfold field_address0. rewrite if_true. simpl. rewrite offset_offset_val. f_equal. change WORD_SIZE with 8. lia. eapply (field_compatible0_Tarray_offset int_or_ptr_type (1+Zlength s) 1). apply arr_field_compatible0. apply H. instantiate (1:= n - Zlength s). 1,2,3,4,5: list_solve. f_equal. simpl. change WORD_SIZE with 8. lia. 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