proposition: Lemma heap_rest_rep_add: forall h sp i (Hs: 0 <= i < MAX_SPACES), space_start (Znth i (spaces h)) = nullval -> heap_rest_rep h * space_rest_rep sp = heap_rest_rep (add_new_space h sp i Hs).
proof: Proof. intros. unfold heap_rest_rep. simpl. remember (spaces h). rewrite <- (sublist_same 0 (Zlength l) l) at 1 by lia. assert (Zlength l = MAX_SPACES) by (subst; rewrite spaces_size; reflexivity). rewrite upd_Znth_unfold. 2: now rewrite H0. rewrite <- (sublist_rejoin 0 i) by lia. rewrite !iter_sepcon_app_sepcon. rewrite sepcon_assoc. f_equal. rewrite (sublist_next i) by lia. simpl. rewrite sepcon_emp, sepcon_comm. f_equal. subst l. unfold space_rest_rep at 1. rewrite if_true by assumption. rewrite emp_sepcon. 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