proposition: Lemma heap_struct_rep_eq: forall sh l p, heap_struct_rep sh l p = @data_at CompSpecs sh (tarray space_type MAX_SPACES) l p.
proof: Proof. intros. unfold heap_struct_rep. apply pred_ext; rewrite data_at_isptr; Intros. - unfold_data_at (@data_at CompSpecs _ heap_type _ _). entailer!. clear H0. rewrite field_at_data_at. unfold field_address. rewrite if_true by assumption. simpl. entailer!!. - unfold_data_at (@data_at CompSpecs _ heap_type _ _). entailer!. clear H0 H1. rewrite field_at_data_at. unfold field_address. rewrite if_true. + simpl. rewrite isptr_offset_val_zero by assumption. entailer!. + unfold field_compatible in *. simpl in *. intuition. * destruct p; try contradiction. clear -H2. unfold align_compatible in *. unfold heap_type. evar (c: composite). apply (align_compatible_rec_Tstruct cenv_cs _heap noattr c _). 1,2: subst c; reflexivity. simpl co_members. intros. simpl in H. if_tac in H; inversion H. subst. clear H. inversion H0. subst z0. rewrite Z.add_0_r. apply H2. * red. simpl. left; 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