proposition: Lemma heap_struct_rep_split_lt: forall sh l heap_p i1 i2, i1 < MAX_SPACES -> i2 < MAX_SPACES -> 0 <= i1 < i2 -> Zlength l = MAX_SPACES -> exists B, heap_struct_rep sh l heap_p = @data_at CompSpecs sh space_type (Znth i1 l) (space_address heap_p (Z.to_nat i1)) * @data_at CompSpecs sh space_type (Znth i2 l) (space_address heap_p (Z.to_nat i2)) * B.
proof: Proof. intros. exists (@data_at CompSpecs sh (tarray space_type (@Zlength (@reptype CompSpecs space_type) (@sublist (@reptype CompSpecs space_type) (i2 + 1) MAX_SPACES l))) (@sublist (@reptype CompSpecs space_type) (i2 + 1) MAX_SPACES l) (offset_val (SPACE_STRUCT_SIZE * (i2 + 1)) heap_p) * @data_at CompSpecs sh (tarray space_type i1) (@sublist (@reptype CompSpecs space_type) 0 i1 l) heap_p * @data_at CompSpecs sh (tarray space_type (i2 - i1 - 1)) (@sublist (@reptype CompSpecs space_type) (i1 + 1) i2 l) (offset_val (SPACE_STRUCT_SIZE * (i1 + 1)) heap_p)). rewrite heap_struct_rep_eq. rewrite (data_at_tarray_space sh MAX_SPACES i1) by rep_lia. rewrite (sublist_next i1 MAX_SPACES l) by rep_lia. replace (MAX_SPACES - i1) with (Zlength (sublist (i1 + 1) MAX_SPACES l) + 1) by (rewrite Zlength_sublist; rep_lia). rewrite data_at_tarray_split_1 by reflexivity. unfold space_address. rewrite Z2Nat.id by lia. rewrite sepcon_comm, !sepcon_assoc. f_equal. rewrite offset_offset_val. rewrite Z2Nat.id by lia. replace (SPACE_STRUCT_SIZE * i1 + sizeof space_type) with (SPACE_STRUCT_SIZE * (i1 + 1))%Z by (simpl sizeof; unfold SPACE_STRUCT_SIZE; rep_lia). assert (Zlength (sublist (i1 + 1) MAX_SPACES l) = (MAX_SPACES-1) - i1) by (rewrite Zlength_sublist; rep_lia). rewrite H3. rewrite (data_at_tarray_space sh ((MAX_SPACES-1) - i1) (i2 - i1 - 1)). 3: rewrite H3; reflexivity. 2: rep_lia. rewrite !sublist_sublist by rep_lia. replace (0 + (i1 + 1)) with (i1 + 1) by lia. replace (i2 - i1 - 1 + (i1 + 1)) with i2 by lia. replace ((MAX_SPACES-1) - i1 - (i2 - i1 - 1)) with (MAX_SPACES - i2) by lia. replace ((MAX_SPACES-1) - i1 + (i1 + 1)) with MAX_SPACES by lia. rewrite offset_offset_val, <- Z.mul_add_distr_l. replace (i1 + 1 + (i2 - i1 - 1)) with i2 by lia. rewrite (sublist_next i2 MAX_SPACES l) by rep_lia. replace (MAX_SPACES - i2) with (Zlength (sublist (i2 + 1) MAX_SPACES l) + 1) by (rewrite Zlength_sublist; rep_lia). rewrite data_at_tarray_split_1 by reflexivity. rewrite sepcon_assoc, sepcon_comm, !sepcon_assoc. f_equal. rewrite <- !sepcon_assoc. rewrite offset_offset_val. simpl sizeof. do 4 f_equal. unfold SPACE_STRUCT_SIZE; rep_lia. 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