Merge conflicts solved and cleaning in Asmgenproof after expansion

1 files changed, 18 insertions, 146 deletions

diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v
index 82c1917d..6abad4ed 100644
--- a/riscV/Asmgenproof.v
+++ b/riscV/Asmgenproof.v
@@ -161,165 +161,37 @@ Proof.
 Qed.
 Hint Resolve addptrofs_label: labels.
 
-Remark transl_cond_float_nolabel:
-  forall c r1 r2 r3 insn normal,
-  transl_cond_float c r1 r2 r3 = (insn, normal) -> nolabel insn.
-Proof.
-  unfold transl_cond_float; intros. destruct c; inv H; exact I.
-Qed.
-
-Remark transl_cond_single_nolabel:
-  forall c r1 r2 r3 insn normal,
-  transl_cond_single c r1 r2 r3 = (insn, normal) -> nolabel insn.
-Proof.
-  unfold transl_cond_single; intros. destruct c; inv H; exact I.
-   Qed.
-
 Remark transl_cbranch_label:
   forall cond args lbl k c,
   transl_cbranch cond args lbl k = OK c -> tail_nolabel k c.
 Proof.
   intros. unfold transl_cbranch in H; destruct cond; TailNoLabel.
-- destruct c0; simpl; TailNoLabel.
-- destruct c0; simpl; TailNoLabel.
-- destruct (Int.eq n Int.zero).
-  destruct c0; simpl; TailNoLabel.
-  apply tail_nolabel_trans with (transl_cbranch_int32s c0 x X31 lbl :: k).
-  auto with labels. destruct c0; simpl; TailNoLabel.
-- destruct (Int.eq n Int.zero).
-  destruct c0; simpl; TailNoLabel.
-  apply tail_nolabel_trans with (transl_cbranch_int32u c0 x X31 lbl :: k).
-  auto with labels. destruct c0; simpl; TailNoLabel.
-- destruct c0; simpl; TailNoLabel.
-- destruct c0; simpl; TailNoLabel.
-- destruct (Int64.eq n Int64.zero).
-  destruct c0; simpl; TailNoLabel.
-  apply tail_nolabel_trans with (transl_cbranch_int64s c0 x X31 lbl :: k).
-  auto with labels. destruct c0; simpl; TailNoLabel.
-- destruct (Int64.eq n Int64.zero).
-  destruct c0; simpl; TailNoLabel.
-  apply tail_nolabel_trans with (transl_cbranch_int64u c0 x X31 lbl :: k).
-  auto with labels. destruct c0; simpl; TailNoLabel.
-- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
-     destruct normal; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
+  all:  destruct optR0 as [[]|]; TailNoLabel.
 Qed.
 
-Remark transl_cond_op_label:
-  forall cond args r k c,
-  transl_cond_op cond r args k = OK c -> tail_nolabel k c.
-Proof.
-  intros. unfold transl_cond_op in H; destruct cond; TailNoLabel.
-- destruct c0; simpl; TailNoLabel.
-- destruct c0; simpl; TailNoLabel. 
-- unfold transl_condimm_int32s.
-  destruct (Int.eq n Int.zero).
-+ destruct c0; simpl; TailNoLabel.
-+ destruct c0; simpl.
-* eapply tail_nolabel_trans; [apply opimm32_label; intros; exact I | TailNoLabel].
-* eapply tail_nolabel_trans; [apply opimm32_label; intros; exact I | TailNoLabel].
-* apply opimm32_label; intros; exact I.
-* destruct (Int.eq n (Int.repr Int.max_signed)). apply loadimm32_label. apply opimm32_label; intros; exact I.
-* eapply tail_nolabel_trans. apply loadimm32_label. TailNoLabel.
-* eapply tail_nolabel_trans. apply loadimm32_label. TailNoLabel.
-- unfold transl_condimm_int32u.
-  destruct (Int.eq n Int.zero).
-+ destruct c0; simpl; TailNoLabel.
-+ destruct c0; simpl; 
-  try (eapply tail_nolabel_trans; [apply loadimm32_label | TailNoLabel]).
-  apply opimm32_label; intros; exact I.
-- destruct c0; simpl; TailNoLabel.
-     - destruct c0; simpl; TailNoLabel.
-- unfold transl_condimm_int64s.
-  destruct (Int64.eq n Int64.zero).
-+ destruct c0; simpl; TailNoLabel.
-+ destruct c0; simpl.
-* eapply tail_nolabel_trans; [apply opimm64_label; intros; exact I | TailNoLabel].
-* eapply tail_nolabel_trans; [apply opimm64_label; intros; exact I | TailNoLabel].
-* apply opimm64_label; intros; exact I.
-* destruct (Int64.eq n (Int64.repr Int64.max_signed)). apply loadimm32_label. apply opimm64_label; intros; exact I.
-* eapply tail_nolabel_trans. apply loadimm64_label. TailNoLabel.
-* eapply tail_nolabel_trans. apply loadimm64_label. TailNoLabel.
-- unfold transl_condimm_int64u.
-  destruct (Int64.eq n Int64.zero).
-+ destruct c0; simpl; TailNoLabel.
-+ destruct c0; simpl; 
-  try (eapply tail_nolabel_trans; [apply loadimm64_label | TailNoLabel]).
-     apply opimm64_label; intros; exact I.
-- destruct (transl_cond_float c0 r x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_float c0 r x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_single c0 r x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_single c0 r x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-   Qed.
-
 Remark transl_op_label:
   forall op args r k c,
   transl_op op args r k = OK c -> tail_nolabel k c.
 Proof.
 Opaque Int.eq.
   unfold transl_op; intros; destruct op; TailNoLabel.
-- destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
-- destruct (Float.eq_dec n Float.zero); TailNoLabel.
-- destruct (Float32.eq_dec n Float32.zero); TailNoLabel.
-- destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).
-+ eapply tail_nolabel_trans; [|apply addptrofs_label]. TailNoLabel.
-+ TailNoLabel. 
-- apply opimm32_label; intros; exact I.
-- apply opimm32_label; intros; exact I.
-- apply opimm32_label; intros; exact I.
-- apply opimm32_label; intros; exact I.
-- destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel.
-- apply opimm64_label; intros; exact I.
-- apply opimm64_label; intros; exact I.
-- apply opimm64_label; intros; exact I.
-- apply opimm64_label; intros; exact I.
-- destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel.
-- eapply transl_cond_op_label; eauto.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
+  { destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel. }
+  { destruct (Float.eq_dec n Float.zero); TailNoLabel. }
+  { destruct (Float32.eq_dec n Float32.zero); TailNoLabel. }
+  { destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).
+    + eapply tail_nolabel_trans; [|apply addptrofs_label]. TailNoLabel.
+    + TailNoLabel. }
+  { apply opimm32_label; intros; exact I. }
+  { apply opimm32_label; intros; exact I. }
+  { apply opimm32_label; intros; exact I. }
+  { apply opimm32_label; intros; exact I. }
+  { destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel. }
+  { apply opimm64_label; intros; exact I. }
+  { apply opimm64_label; intros; exact I. }
+  { apply opimm64_label; intros; exact I. }
+  { apply opimm64_label; intros; exact I. }
+  { destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel. }
+  all: destruct optR0 as [[]|]; simpl; TailNoLabel.
 Qed.
 
 Remark indexed_memory_access_label: