proposition: Lemma Is_from_extcall: extcall_properties Is_from_sem Is_from_sig.
proof: Proof. constructor; intros. - destruct H as [_ [_ ?]]. do 4 (destruct vargs; try destruct v; try contradiction). destruct H as [_ [_ [_ [_ [_ [_ [_ ?]]]]]]]. destruct H as [[_ [_ ?]] | [_ ?]]; subst; apply I. - apply H0. - destruct H as [? _]. subst m1. trivial. - destruct H as [? _]. subst m1. trivial. - destruct H as [? _]. subst m1. trivial. - exists vres, m1'. destruct H as [? [? ?]]; subst m2 t. split. 2: split3; [apply Val.lessdef_refl | trivial | apply Mem.unchanged_on_refl]. split3; trivial. do 4 (destruct vargs; try destruct v; try contradiction). inversion H1; inversion H4; inversion H6; inversion H11; inversion H13; inversion H18; inversion H20; subst. clear H4 H11 H18 H20 H13 H6 H1. destruct H3 as [n [? [? [? [? ?]]]]]. exists n. do 4 (split; trivial). clear -H0 H4. destruct H4 as [? [? ?]]. split3; [|eapply Mem.valid_pointer_extends; eauto | tauto]. destruct H as [? [? ?]]. do 2 (split; trivial). intros. specialize (H4 i2 H5). eapply Mem.valid_pointer_extends; eauto. - intros. exists f, vres, m1'. destruct H0 as [? [? ?]]. split. 2: { split. 2: repeat (split; [now subst|]); congruence. clear -H4. do 4 (destruct vargs; try destruct v; try contradiction). destruct H4 as [_ [_ [_ [_ [_ [_ [_ H]]]]]]]. destruct vres; auto. now destruct H. } split3; trivial. do 4 (destruct vargs; try destruct v; try contradiction). inversion H2; inversion H7; inversion H9; inversion H17; inversion H19; inversion H27; inversion H29; subst. clear H2 H7 H9 H17 H19 H27 H29. destruct H4 as [n [? [? [? [? [? [? ?]]]]]]]. exists n. rewrite H3 in H12; rewrite H22 in H12; inversion H12. subst; clear H12. assert (Hf: 0 <= Ptrofs.unsigned i + n < Ptrofs.modulus) by (rewrite H4; apply Ptrofs.unsigned_range). assert (Ha: Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr delta)) + n < Ptrofs.modulus). { destruct H1 as [_ _ _ _ rep _]. destruct (rep b0 b3 delta (Ptrofs.add i (Ptrofs.repr n)) H22) as [Hx Hy]. { right. apply Mem.perm_cur_max, Mem.valid_pointer_nonempty_perm. destruct H5 as [_ [_ H5]]. assert (Hm: 0 <= n - 1 < n) by lia; rewrite <- (H5 _ Hm). f_equal; unfold Ptrofs.add; repeat rewrite Ptrofs.unsigned_repr_eq. rewrite Z.add_mod_idemp_r, Z.mod_small by easy. lia. } clear -Hx Hy Hf H0. apply lt_ptr_mod in Hy. unfold Ptrofs.add in *. repeat rewrite Ptrofs.unsigned_repr_eq in *. rewrite Z.add_mod_idemp_r, Z.mod_small in * by easy. rewrite Z.mod_small; [lia|]. destruct i. unfold Ptrofs.unsigned in *; simpl in *. lia. } split3; [| |split3; [| |split3]]; trivial. + destruct H1 as [_ _ _ _ rep _]. destruct (rep _ _ delta (Ptrofs.add i (Ptrofs.repr n)) H22) as [Hd' Hd]. { right. apply Mem.perm_cur_max, Mem.valid_pointer_nonempty_perm. destruct H5 as [_ [_ H5]]. assert (0 <= n - 1 < n) by lia. rewrite <- (H5 _ H1). f_equal. unfold Ptrofs.add; repeat rewrite Ptrofs.unsigned_repr_eq. rewrite Z.add_mod_idemp_r, Z.mod_small by easy. lia. } unfold Ptrofs.add. rewrite <- H4. destruct (Ptrofs.unsigned_range i) as [? _]. repeat rewrite Ptrofs.unsigned_repr_eq. repeat rewrite Z.add_mod_idemp_r by easy. unfold Ptrofs.add in Hd. repeat rewrite Ptrofs.unsigned_repr_eq in Hd. rewrite Z.add_mod_idemp_r, Z.mod_small in Hd by easy. apply lt_ptr_mod in Hd. repeat rewrite Z.mod_small; [lia | trivial | lia]. + split3; [easy | lia|]. intros. destruct H5 as [_ [_ H5]]. rewrite <- (Mem.valid_pointer_inject _ _ _ _ _ _ _ H22 H1 (H5 i2 H3)). f_equal. unfold Ptrofs.add; repeat rewrite Ptrofs.unsigned_repr_eq. destruct H1 as [_ _ _ _ rep _]. destruct (rep _ _ delta i H22) as [_ Hd]. { left. apply Mem.perm_cur_max, Mem.valid_pointer_nonempty_perm. assert (0 <= 0 < n) by lia; rewrite <- (H5 0 H1); f_equal; lia. } apply lt_ptr_mod in Hd. rewrite Z.add_mod_idemp_r, Z.mod_small by easy. lia. + rewrite <- (Mem.valid_pointer_inject _ _ _ _ _ _ _ H32 H1 H6). f_equal. unfold Ptrofs.add. repeat rewrite Ptrofs.unsigned_repr_eq. destruct H1 as [_ _ _ _ rep _]. destruct (rep _ _ delta1 i1 H32) as [_ Hd]. { left; now apply Mem.perm_cur_max, Mem.valid_pointer_nonempty_perm. } apply lt_ptr_mod in Hd. rewrite Z.add_mod_idemp_r, Z.mod_small by easy. lia. + destruct H7. * destruct H3 as [? [? ?]]; subst b1 vres. destruct H1 as [_ _ _ _ rep _]. destruct (rep b0 b3 delta i H22) as [_ Hp]. { left; apply Mem.perm_cur_max, Mem.valid_pointer_nonempty_perm. destruct H5 as [_ [_ H5]]; assert (0 <= 0 < n) by lia. specialize (H5 0 H1). now replace (Ptrofs.unsigned i + 0) with (Ptrofs.unsigned i) in H5 by lia. } destruct (rep b0 b3 delta i1 H22) as [_ Hq]. { left; apply Mem.perm_cur_max, Mem.valid_pointer_nonempty_perm; destruct H5 as [_ [_ ?]]; assert (0 <= 0 < n) by lia. specialize (H1 0 H3); now rewrite H6. } destruct (rep b0 b3 delta i0 H22) as [_ Hr]. { destruct H5 as [_ [_ H5]]. rewrite <- H4. assert (Hm: 0 <= n - 1 < n) by lia. right. apply Mem.perm_cur_max, Mem.valid_pointer_nonempty_perm. rewrite <- (H5 _ Hm); f_equal; lia. } rewrite H22 in H32; inversion H32. left. split3; trivial. subst delta1. clear -H7 Hp Hq Hr. unfold Ptrofs.add; repeat rewrite Ptrofs.unsigned_repr_eq. apply lt_ptr_mod in Hp; apply lt_ptr_mod in Hq; apply lt_ptr_mod in Hr. repeat rewrite Z.add_mod_idemp_r, Z.mod_small by easy. lia. * destruct H3. right. split; trivial. rename m2 into m; rename m1' into m'. destruct H1 as [_ _ _ lap rep _]. destruct H3. -- destruct (eq_block b3 b7); [|now left]. subst b3. right. split; trivial. unfold Ptrofs.add; repeat rewrite Ptrofs.unsigned_repr_eq. repeat rewrite Z.add_mod_idemp_r by easy. destruct H5 as [_ [_ H5]]. assert (0 <= 0 < n) by lia. pose proof (H5 _ H3). apply Mem.valid_pointer_nonempty_perm, Mem.perm_cur_max in H6. apply Mem.valid_pointer_nonempty_perm, Mem.perm_cur_max in H8. replace (Ptrofs.unsigned i + 0) with (Ptrofs.unsigned i) in H8 by lia. destruct (rep _ _ delta1 i1 H32) as [_ Hp]; [left; easy|]. destruct (rep _ _ delta i H22) as [_ Hq]; [left; easy|]. destruct (rep _ _ delta i0 H22) as [_ Hr]. { rewrite <- H4. assert (Hm: 0 <= n - 1 < n) by lia. specialize (H5 _ Hm). replace (Ptrofs.unsigned i + (n - 1)) with (Ptrofs.unsigned i + n - 1) in H5 by lia. apply Mem.valid_pointer_nonempty_perm, Mem.perm_cur_max in H5. now right. } replace Ptrofs.max_unsigned with (Z.pred Ptrofs.modulus) in * by (unfold Ptrofs.max_unsigned; lia). rewrite <- Z.lt_le_pred in *. repeat rewrite Z.mod_small by easy. destruct (lap _ _ _ _ _ _ _ _ H1 H22 H32 H8 H6); [contradiction|]. clear rep Hp Hq Hr. replace (Ptrofs.unsigned i) with ((Ptrofs.unsigned i - delta) + delta) in H5 by lia. assert ((Ptrofs.unsigned i1 + delta1 < Ptrofs.unsigned i + delta) \/ (Ptrofs.unsigned i1 + delta1 >= Ptrofs.unsigned i0 + delta) \/ ((Ptrofs.unsigned i1 + delta1 >= Ptrofs.unsigned i + delta) /\ Ptrofs.unsigned i1 + delta1 < Ptrofs.unsigned i0 + delta)) by lia. destruct H10; [auto | destruct H10; [auto|]]. exfalso. destruct H10. rewrite <- H4 in H11. assert (0 <= Ptrofs.unsigned i1 + delta1 - Ptrofs.unsigned i - delta < n) by lia. specialize (H5 (Ptrofs.unsigned i1 + delta1 - Ptrofs.unsigned i - delta) H12). apply Mem.valid_pointer_nonempty_perm, Mem.perm_cur_max in H5. destruct (lap b0 b7 delta b1 b7 delta1 _ (Ptrofs.unsigned i1) H1 H22 H32 H5 H6); [auto | apply H13; lia]. -- destruct H1. subst b0 vres. right. rewrite H22 in H32; inversion H32. clear H32. split; trivial. unfold Ptrofs.add; repeat rewrite Ptrofs.unsigned_repr_eq. repeat rewrite Z.add_mod_idemp_r by easy. subst delta1. destruct (rep b1 b3 delta i H22) as [_ Hp]. { left; apply Mem.perm_cur_max, Mem.valid_pointer_nonempty_perm. destruct H5 as [_ [_ H5]]; assert (H1: 0 <= 0 < n) by lia. specialize (H5 0 H1). now replace (Ptrofs.unsigned i + 0) with (Ptrofs.unsigned i) in H5 by lia. } destruct (rep b1 b3 delta i1 H22) as [_ Hq]. 1: now left; apply Mem.perm_cur_max, Mem.valid_pointer_nonempty_perm. destruct (rep b1 b3 delta i0 H22) as [_ Hr]. { destruct H5 as [_ [_ H5]]. rewrite <- H4. assert (Hm: 0 <= n - 1 < n) by lia. right. apply Mem.perm_cur_max, Mem.valid_pointer_nonempty_perm. rewrite <- (H5 _ Hm); f_equal; lia. } clear - H3 Hp Hq Hr. apply lt_ptr_mod in Hp; apply lt_ptr_mod in Hq; apply lt_ptr_mod in Hr. repeat rewrite Z.mod_small by easy. destruct H3; [left | right]; lia. - intros. destruct H as [_ [? _]]. subst t. simpl. lia. - intros. generalize H. destruct H as [_ [? _]]. subst t1. inversion H0. subst t2. clear H0. intro H. exists vres1, m1. apply H. - intros. destruct H as [? [? ?]]. destruct H0 as [? [? ?]]. subst m1 m2 t1 t2. split; [constructor|]. intros _. split; trivial. do 4 (destruct vargs; try destruct v; try contradiction). destruct H2 as [_ [_ [_ [_ [_ [_ [_ ?]]]]]]]. destruct H4 as [_ [_ [_ [_ [_ [_ [_ ?]]]]]]]. intuition; congruence. Qed.
imports: compcert.common.Events compcert.common.Memory compcert.common.Values compcert.common.AST compcert.lib.Integers Coq.ZArith.BinInt Coq.Lists.List Coq.micromega.Lia