proposition: Lemma heap_rest_rep_reset: forall (g: LGraph) h gen, graph_heap_compatible g h -> graph_has_gen g gen -> heap_rest_rep h * generation_rep g gen |-- heap_rest_rep (reset_nth_heap gen h).
proof: Proof. intros. unfold heap_rest_rep. simpl. assert (gen < length (spaces h))%nat by (red in H0; destruct H as [_ [_ ?]]; lia). destruct (reset_nth_space_Permutation _ _ H1) as [l [? ?]]. rewrite (iter_sepcon_permutation _ H3). rewrite (iter_sepcon_permutation _ H2). simpl. cancel. destruct (gt_gs_compatible _ _ H _ H0) as [? [? ?]]. fold (nth_space h gen). unfold space_rest_rep. unfold reset_space at 1. assert (isptr (space_start (nth_space h gen))) by (rewrite <- H4; apply start_isptr). assert (space_start (nth_space h gen) <> nullval). { destruct (space_start (nth_space h gen)); try contradiction. intro; inversion H8. } simpl space_start. rewrite !if_false by assumption. sep_apply (generation_rep_data_at_ g gen H0). unfold graph_gen_size. rewrite H6. unfold gen_start. rewrite if_true by assumption. rewrite H4. unfold nth_sh. rewrite H5. simpl. remember (nth_space h gen). replace (WORD_SIZE * 0)%Z with 0 by lia. rewrite isptr_offset_val_zero by assumption. replace (total_space s - 0) with (total_space s) by lia. rewrite <- data_at__tarray_value by apply space_order. 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