proposition: Lemma heap_rest_rep_cut: forall (h: heap) i s (H1: 0 <= i < Zlength (spaces h)) (H2: has_space (Znth i (spaces h)) s), space_start (Znth i (spaces h)) <> nullval -> heap_rest_rep h = data_at_ (space_sh (Znth i (spaces h))) (tarray int_or_ptr_type s) (offset_val (WORD_SIZE * used_space (Znth i (spaces h))) (space_start (Znth i (spaces h)))) * heap_rest_rep (cut_heap h i s H1 H2).
proof: Proof. intros. unfold heap_rest_rep. pose proof (split3_full_length_list 0 i _ _ H1 (Zminus_0_l_reverse (Zlength (spaces h)))). replace (i - 0) with i in H0 by lia. simpl in *. remember (firstn (Z.to_nat i) (spaces h)) as l1. remember (skipn (Z.to_nat (i + 1)) (spaces h)) as l2. assert (Zlength l1 = i). { rewrite Zlength_length by lia. subst l1. apply firstn_length_le. rewrite Zlength_correct in H1. rep_lia. } rewrite H0 at 5. rewrite (upd_Znth_char _ _ _ _ _ H3). rewrite H0 at 1. rewrite !iter_sepcon_app_sepcon. simpl. remember (data_at_ (space_sh (Znth i (spaces h))) (tarray int_or_ptr_type s) (offset_val (WORD_SIZE * used_space (Znth i (spaces h))) (space_start (Znth i (spaces h))))) as P. rewrite (sepcon_comm P), sepcon_assoc. f_equal. rewrite (sepcon_comm _ P), <- sepcon_assoc. f_equal. unfold space_rest_rep. simpl. do 2 rewrite if_false by assumption. red in H2. subst P. remember (Znth i (spaces h)) as sp. rewrite (data_at__tarray_value _ _ _ _ H2). rewrite offset_offset_val. replace (total_space sp - used_space sp - s) with (total_space sp - (used_space sp + s)) by lia. replace (WORD_SIZE * used_space sp + WORD_SIZE * s) with (WORD_SIZE * (used_space sp + s))%Z by rep_lia. reflexivity. 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