proposition: Lemma heap_struct_rep_add: forall (heap_p: val) (h: heap) sh sp i (Hs: 0 <= i < MAX_SPACES), data_at sh space_type (space_tri sp) (space_address heap_p (Z.to_nat i)) * (@data_at CompSpecs sh (tarray space_type (@Zlength (@reptype CompSpecs space_type) (@sublist (@reptype CompSpecs space_type) (i + 1) MAX_SPACES (map space_tri (spaces h))))) (@sublist (@reptype CompSpecs space_type) (i + 1) MAX_SPACES (map space_tri (spaces h))) (offset_val (@sizeof CompSpecs space_type) (offset_val (SPACE_STRUCT_SIZE * i) heap_p)) * @data_at CompSpecs sh (tarray space_type i) (@sublist (@reptype CompSpecs space_type) 0 i (map space_tri (spaces h))) heap_p) = (heap_struct_rep sh (map space_tri (spaces (add_new_space h sp i Hs))) heap_p).
proof: Proof. intros. assert (Zlength (map space_tri (spaces h)) = MAX_SPACES) by (rewrite Zlength_map, spaces_size; reflexivity). assert (Zlength (map space_tri (spaces (add_new_space h sp i Hs))) = MAX_SPACES) by (rewrite Zlength_map, spaces_size; reflexivity). rewrite hsr_single_explicit with (i := i) by assumption. simpl. rewrite <- !upd_Znth_map, upd_Znth_same by lia. rewrite sublist_upd_Znth_r; [| lia | pose proof Hs; rep_lia]. rewrite sublist_upd_Znth_l by 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