proposition: Lemma field_compatible0_Tarray_offset: forall {cs: compspecs} t n i n' i' p p', field_compatible0 (Tarray t n' noattr) (ArraySubsc i' :: nil) p -> 0 <= n <= n' -> 0 <= i <= n -> n-i <= n'-i' -> i <= i' -> p' = offset_val (sizeof t * (i'-i)) p -> field_compatible0 (Tarray t n noattr) (ArraySubsc i :: nil) p'.
proof: Proof. intros until 1. intros ?H ?H Hni Hii Hp. subst p'. assert (SP := sizeof_pos t). assert (SS: sizeof t * n <= sizeof t * n'). apply Zmult_le_compat_l. lia. lia. assert (SS': (sizeof t * n + sizeof t * (n'-n) = sizeof t * n')%Z). rewrite <- Z.mul_add_distr_l. f_equal. lia. hnf in H|-*. intuition auto with field_compatible. * destruct p; try contradiction. clear - SP SS SS' H H4 H0 H5 H3 H8 Hni Hii. red in H3|-*. unfold expr.sizeof in *. simpl in H3,H8|-*. rewrite Z.max_r in H3|-* by lia. rename i0 into j. pose proof (Ptrofs.unsigned_range j). fold (sizeof t) in *. assert (0 <= sizeof t * (i'-i) <= sizeof t * n'). split. apply Z.mul_nonneg_nonneg; lia. apply Zmult_le_compat_l. lia. lia. assert (sizeof t * (i'-i+n) <= sizeof t * n'). apply Zmult_le_compat_l. lia. lia. unfold Ptrofs.add. rewrite (Ptrofs.unsigned_repr (_ * _)) by (change Ptrofs.max_unsigned with (Ptrofs.modulus -1); lia). rewrite Ptrofs.unsigned_repr_eq. rewrite Zmod_small by lia. pose proof Z.mul_add_distr_l (sizeof t) (i' - i) n. lia. * destruct p; try contradiction. simpl in H3, H6 |- *. unfold expr.sizeof in *. simpl in H3, H6 |- *. rewrite Z.max_r in H3 by lia. constructor; intros. unfold Ptrofs.add. rewrite !Ptrofs.unsigned_repr_eq. assert (Ptrofs.modulus <> 0) by computable. rewrite Z.add_mod by auto. rewrite Z.mod_mod by auto. rewrite <- Z.add_mod by auto. inv_int i0. fold (sizeof t) in *. pose_size_mult cs t (0 :: i' - i :: i' - i + i1 :: n' :: nil). rewrite Zmod_small by lia. rewrite <- Z.add_assoc, <- H14. eapply align_compatible_rec_Tarray_inv; [eassumption |]. 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