proposition: Lemma heap_rep_ramif_stable: forall sh h p gen1 gen2, gen1 <> gen2 -> Z.of_nat gen1 < MAX_SPACES -> Z.of_nat gen2 < MAX_SPACES -> heap_rep sh h p |-- (space_struct_rep sh p h gen1 * space_struct_rep sh p h gen2) * ((space_struct_rep sh p h gen1 * space_struct_rep sh p h gen2) -* heap_rep sh h p).
proof: Proof. intros. unfold heap_rep. set (Q := heap_rest_rep _). remember (map space_tri (spaces h)). assert (0 <= Z.of_nat gen1 < MAX_SPACES) by rep_lia. assert (0 <= Z.of_nat gen2 < MAX_SPACES) by rep_lia. assert (Z.of_nat gen1 <> Z.of_nat gen2) by lia. assert (Zlength l = MAX_SPACES) by (subst; rewrite Zlength_map; apply spaces_size). destruct (heap_struct_rep_split sh l p _ _ H2 H3 H4 H5) as [B ?]. rewrite H6, !Nat2Z.id. assert (forall i, 0 <= Z.of_nat i < MAX_SPACES -> data_at sh space_type (Znth (Z.of_nat i) l) (space_address p i) = space_struct_rep sh p h i). { intros. unfold space_struct_rep. subst l. rewrite Zlength_map in H5. rewrite nth_space_Znth, Znth_map by rep_lia. reflexivity. } rewrite !H7 by rep_lia. rewrite (sepcon_assoc _ B Q). cancel. apply wand_frame_intro. 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