proposition: Lemma test_iop__extcall: extcall_properties test_iop_sem test_iop_sig.
proof: Proof. constructor; intros. - destruct H as [_ [_ ?]]. destruct vargs; try destruct v; try contradiction; destruct vargs; try contradiction. 1: destruct (Int.eq Int.one (Int.modu i (Int.repr 2))); subst; easy. destruct (Ptrofs.eq Ptrofs.one (Ptrofs.modu i (Ptrofs.repr 2))). 1: contradiction. destruct (valid_b_o_So_dec m1 b i); subst; easy. - trivial. - destruct H as [? _]. subst m1. trivial. - destruct H as [? _]. subst m1. trivial. - destruct H as [? _]. subst m1. trivial. - destruct H as [? [? ?]]; subst m2 t. exists vres, m1'. split. 2: split3; [apply Val.lessdef_refl | trivial | apply Mem.unchanged_on_refl]. split3; trivial. do 2 (try destruct vargs; try destruct v); try contradiction; inversion H1; inversion H4; inversion H6; auto. clear -H0 H3. destruct (Ptrofs.eq Ptrofs.one (Ptrofs.modu i (Ptrofs.repr 2))); auto. destruct (valid_b_o_So_dec m1 b i); destruct (valid_b_o_So_dec m1' b i); [trivial| | contradiction..]. clear H3; destruct n. destruct H0 as [_ [? _ _] _]. unfold valid_b_o_So in *. unfold Mem.range_perm in *. intros. specialize (v ofs H). assert (inject_id b = Some (b, 0)) by now unfold inject_id. specialize (mi_perm _ _ _ ofs Cur Nonempty H0). replace (ofs + 0) with ofs in mi_perm by lia. apply (mi_perm v). - intros. exists f, vres, m1'. destruct H0 as [? [? ?]]. subst. split. 2: { split. - destruct vres; auto. do 2 (destruct vargs; try destruct v; try contradiction). + destruct (Int.eq Int.one (Int.modu i0 (Int.repr 2))); [inversion H4 | easy]. + destruct (Ptrofs.eq Ptrofs.one (Ptrofs.modu i0 (Ptrofs.repr 2))); try contradiction. destruct (valid_b_o_So_dec m2 b0 i0); [inversion H4 | easy]. - split; [trivial|]. split; [apply Mem.unchanged_on_refl|]. split; [apply Mem.unchanged_on_refl|]. split; [apply inject_incr_refl | congruence]. } split3; trivial. do 2 (destruct vargs; try destruct v; try contradiction). + inversion H2. inversion H5. inversion H7. auto. + inversion H2. inversion H5. inversion H7. subst. clear H7 H2. destruct (Ptrofs.eq Ptrofs.one (Ptrofs.modu i (Ptrofs.repr 2))) eqn:parity1; [contradiction|]. destruct (valid_b_o_So_dec m2 b i); [|contradiction]. assert (OF: Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr delta)) = Ptrofs.unsigned i + delta). { eapply Mem.address_inject; eauto. apply v. lia. } assert (AL: (2 | delta)). { change 2 with (align_chunk Mint16unsigned). clear - H10 v H1. eauto using Mem.mi_align, Mem.mi_inj, Mem.range_perm_max. } destruct (Ptrofs.eq Ptrofs.one (Ptrofs.modu (Ptrofs.add i (Ptrofs.repr delta)) (Ptrofs.repr 2))) eqn:parity2. * assert (0 <= Ptrofs.unsigned i + delta < Ptrofs.modulus). { destruct H1 as [_ _ _ _ rep _]. specialize (rep _ _ _ i H10) as [_ rep]. left. unfold valid_b_o_So in v. unfold Mem.range_perm in v. specialize (v (Ptrofs.unsigned i)). apply Mem.perm_cur_max in v. auto. lia. apply lt_ptr_mod in rep. assumption. } clear - parity1 parity2 AL H0. rewrite <- Bool.not_false_iff_true in parity2. unfold not in *. destruct parity2. unfold Ptrofs.modu in *. rewrite Ptrofs.unsigned_repr_eq in *. rewrite (Z.mod_small 2 _) in * by easy. unfold Ptrofs.add; repeat rewrite Ptrofs.unsigned_repr_eq. rewrite Z.add_mod_idemp_r, (Z.mod_small (Ptrofs.unsigned i + delta) _) by easy. rewrite <- parity1. do 2 f_equal. rewrite <- Z.add_mod_idemp_r, (Znumtheory.Zdivide_mod delta 2) by easy. now replace (Ptrofs.unsigned i + 0) with (Ptrofs.unsigned i) by lia. * destruct (valid_b_o_So_dec m1' b2 (Ptrofs.add i (Ptrofs.repr delta))); auto. destruct n. assert (inj := H1). destruct H1 as [[? _ _] _ _ _ rep _]. unfold valid_b_o_So in *. rewrite OF. replace (Ptrofs.unsigned i + delta + 2) with ((Ptrofs.unsigned i + 2) + delta) by lia. eapply Mem.range_perm_inject; eauto. - destruct H as [_ [? _]]. subst t. simpl; lia. - generalize H. destruct H as [_ [? _]]. subst t1; inversion H0; subst t2. intro H; exists vres1, m1; apply H. - destruct H as [? [? ?]]. destruct H0 as [? [? ?]]. subst m1 m2 t1 t2. split; [constructor|]. intros _. split; trivial. do 2 (try destruct vargs; try destruct v; try contradiction). + destruct (Int.eq Int.one (Int.modu i (Int.repr 2))); subst; [trivial | contradiction]. + destruct (Ptrofs.eq Ptrofs.one (Ptrofs.modu i (Ptrofs.repr 2))); [contradiction|]. destruct (valid_b_o_So_dec m b i); [|contradiction]. subst; trivial. 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