proposition: Lemma ti_token_rep_add: forall h p sp i (Hs: 0 <= i < MAX_SPACES), space_start (Znth i (spaces h)) = nullval -> space_start sp <> nullval -> malloc_token Ews (tarray int_or_ptr_type (total_space sp)) (space_start sp) * ti_token_rep h p |-- ti_token_rep (add_new_space h sp i Hs) p.
proof: Proof. intros. unfold ti_token_rep. simpl. cancel. 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 H1. rewrite <- (sublist_rejoin 0 i) by lia. rewrite !iter_sepcon_app_sepcon. cancel. rewrite (sublist_next i) by lia. simpl. cancel. subst l. unfold space_token_rep at 1. rewrite H. rewrite if_true by reflexivity. unfold space_token_rep. rewrite if_false by assumption. cancel. 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