Improvements in Asmgenproof

* Deleting the (duplicated) length_agree lemma (there was an equivalent lemma named list_length_z_nat for this purpose)
* Lemmas about labels :
  * label_in_header_list
  * no_label_in_basic_inst
  * label_pos_body
  * label_pos_preserved_gen and label_pos_preserved

1 files changed, 111 insertions, 32 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 7d1f1d05..db6548fe 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -22,7 +22,7 @@ Require Machblockgenproof Asmblockgenproof.
 Require Import Asmgen.
 Require Import Axioms.
 Require Import IterList.
-
+Require Import Ring.
 
 Module Asmblock_PRESERVATION.
 
@@ -314,18 +314,18 @@ Proof.
   unfold list_length_z; simpl; rewrite list_length_add_acc; reflexivity.
 Qed.
 
-Lemma length_agree A (l : list A):
-  list_length_z l = Z.of_nat (length l).
-Proof.
-  induction l as [| ? l IH]; intros.
-  - unfold list_length_z; reflexivity.
-  - simpl; rewrite list_length_z_cons, Zpos_P_of_succ_nat; omega.
-Qed.
+(*Lemma length_agree A (l : list A):*)
+  (*list_length_z l = Z.of_nat (length l).*)
+(*Proof.*)
+  (*induction l as [| ? l IH]; intros.*)
+  (*- unfold list_length_z; reflexivity.*)
+  (*- simpl; rewrite list_length_z_cons, Zpos_P_of_succ_nat; omega.*)
+(*Qed.*)
 
 Lemma bblock_size_aux bb: size bb = list_length_z (header bb) + list_length_z (body bb) + Z.of_nat (length_opt (exit bb)).
 Proof.
   unfold size.
-  repeat (rewrite length_agree). repeat (rewrite Nat2Z.inj_add). reflexivity.
+  repeat (rewrite list_length_z_nat). repeat (rewrite Nat2Z.inj_add). reflexivity.
 Qed.
 
 Lemma header_size_lt_block_size bb:
@@ -334,14 +334,14 @@ Proof.
   rewrite bblock_size_aux.
   generalize (bblock_non_empty bb); intros NEMPTY; destruct NEMPTY as [HDR|EXIT].
   - destruct (body bb); try contradiction; rewrite list_length_z_cons;
-    repeat rewrite length_agree; omega.
-  - destruct (exit bb); try contradiction; simpl; repeat rewrite length_agree; omega.
+    repeat rewrite list_length_z_nat; omega.
+  - destruct (exit bb); try contradiction; simpl; repeat rewrite list_length_z_nat; omega.
 Qed.
 
 Lemma body_size_le_block_size bb:
   list_length_z (body bb) <= size bb.
 Proof.
-  rewrite bblock_size_aux; repeat rewrite length_agree; omega.
+  rewrite bblock_size_aux; repeat rewrite list_length_z_nat; omega.
 Qed.
 
 
@@ -516,7 +516,7 @@ Proof.
   unfold size.
   rewrite equal_header_size, equal_exit_size.
   erewrite equal_body_size; eauto.
-  rewrite length_agree.
+  rewrite list_length_z_nat.
   repeat (rewrite app_length).
   rewrite plus_assoc. auto.
 Qed.
@@ -537,12 +537,12 @@ Proof.
     destruct (zeq pos 0).
     + inv FINDBB.
       exploit bblock_size_preserved; eauto; intros SIZE; rewrite SIZE.
-      repeat (rewrite length_agree). rewrite app_length, Nat2Z.inj_add.
+      repeat (rewrite list_length_z_nat). rewrite app_length, Nat2Z.inj_add.
       omega.
     + generalize (IHbbs tbbs' (pos - size bb) bb' FINDBB UNFOLD). intros IH.
       exploit bblock_size_preserved; eauto; intros SIZE.
-      repeat (rewrite length_agree); rewrite app_length.
-      rewrite Nat2Z.inj_add; repeat (rewrite <- length_agree).
+      repeat (rewrite list_length_z_nat); rewrite app_length.
+      rewrite Nat2Z.inj_add; repeat (rewrite <- list_length_z_nat).
       omega.
 Qed.
 
@@ -776,7 +776,7 @@ Proof.
 
   assert (n >= list_length_z (header bb) + list_length_z (body bb)). { omega. }
   rewrite Nat2Z.inj_add.
-  repeat (rewrite <- length_agree). assumption.
+  repeat (rewrite <- list_length_z_nat). assumption.
 Qed.
 
 Lemma exec_arith_instr_dont_move_PC ai rs rs': forall
@@ -893,12 +893,12 @@ Proof.
               unfold size in SIZE. rewrite <- EXIT in SIZE. simpl in SIZE.
               destruct SIZE as (LOWER & UPPER).
               repeat (rewrite Nat2Z.inj_add in UPPER).
-              repeat (rewrite <- length_agree in UPPER). repeat (rewrite Nat2Z.inj_add in NGE).
-              repeat (rewrite <- length_agree in NGE). simpl in UPPER.
+              repeat (rewrite <- list_length_z_nat in UPPER). repeat (rewrite Nat2Z.inj_add in NGE).
+              repeat (rewrite <- list_length_z_nat in NGE). simpl in UPPER.
               assert (n = list_length_z (header bb) + list_length_z (body bb)). { omega. }
               assert (n = size bb - 1). {
                 unfold size. rewrite <- EXIT. simpl.
-                repeat (rewrite Nat2Z.inj_add). repeat (rewrite <- length_agree). simpl. omega.
+                repeat (rewrite Nat2Z.inj_add). repeat (rewrite <- list_length_z_nat). simpl. omega.
               }
               symmetry in EXIT.
               eexists; split.
@@ -1297,8 +1297,8 @@ Proof.
   assert (tc' = tc) by congruence; subst.
     exploit (find_instr_bblock (list_length_z (header bb) + Z.of_nat n)); eauto.
     { unfold size; split.
-      - rewrite length_agree; omega.
-      - repeat (rewrite length_agree). repeat (rewrite Nat2Z.inj_add). omega. }
+      - rewrite list_length_z_nat; omega.
+      - repeat (rewrite list_length_z_nat). repeat (rewrite Nat2Z.inj_add). omega. }
     intros (i & NTH & FIND_INSTR).
     exists i; intros.
     inv NTH.
@@ -1308,7 +1308,7 @@ Proof.
       rewrite Z.add_assoc in FIND_INSTR;
       intuition.
     - (* absurd *) rewrite bblock_size_aux in H0;
-      rewrite H in H0; simpl in H0; repeat rewrite length_agree in H0; omega.
+      rewrite H in H0; simpl in H0; repeat rewrite list_length_z_nat in H0; omega.
 Qed.
 
 (** "is_tail" auxiliary lemma about is_tail to move in IterList ou Coqlib (déplacer aussi Machblockgenproof.is_tail_app_inv) ? *)
@@ -1406,7 +1406,11 @@ Proof.
   assert (BOUNDBB: Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned)
   by (eapply size_of_blocks_bounds; eauto).
   exploit exec_basic_simulation; eauto.
-  { admit. (* TODO *) }
+  { assert (list_length_z (header bb) >= 0) by eapply list_length_z_pos.
+    assert (list_length_z (header bb) < size bb) by eapply header_size_lt_block_size.
+    destruct BOUNDBB.
+    (*assert (size bb < Ptrofs.max_unsigned) by omega.*)
+    admit. (* TODO *) }
   intros (rs_next' & m_next' & EXEC_INSTR & MI_NEXT).
   (* Code from the star' lemma bellow. We need this to exploit exec_step_internal. *)
   exploit exec_basic_dont_move_PC; eauto. intros AGPC.
@@ -1422,8 +1426,8 @@ Proof.
   (* Execute internal step. *)
   exploit (Asm.exec_step_internal tge b); eauto.
     { (* unfold Ptrofs.add. repeat (rewrite Ptrofs.unsigned_repr);
-      try rewrite length_agree; try split; try omega.
-      simpl; rewrite <- length_agree; assumption. *)
+      try rewrite list_length_z_nat; try split; try omega.
+      simpl; rewrite <- list_length_z_nat; assumption. *)
       admit. (* TODO *) }
 
   (* This is our STEP hypothesis. *)
@@ -1508,16 +1512,91 @@ Proof.
   exploit list_nth_z_range; eauto. omega.
 Qed.
 
-Lemma basic_block_header_length: forall bb,
-  (length (header bb) <= 1)%nat.
+Lemma label_in_header_list lbl a:
+  is_label lbl a = true -> list_length_z (header a) <= 1 -> header a = lbl :: nil.
 Proof.
-Admitted.
-
-Lemma label_pos_preserved f lbl z tf: forall
+  intros.
+  eapply is_label_correct_true in H.
+  destruct (header a).
+  - eapply in_nil in H. contradiction.
+  - rewrite list_length_z_cons in H0.
+    assert (list_length_z l0 >= 0) by eapply list_length_z_pos.
+    assert (list_length_z l0 = 0) by omega.
+    rewrite list_length_z_nat in H2.
+    assert (Datatypes.length l0 = 0%nat) by omega.
+    eapply length_zero_iff_nil in H3. subst.
+    unfold In in H. destruct H.
+    + subst; eauto.
+    + destruct H.
+Qed.
+
+Lemma no_label_in_basic_inst: forall a lbl x,
+  basic_to_instruction a = OK x -> Asm.is_label lbl x = false.
+Proof.
+  intros.
+  destruct a; simpl in *;
+  repeat destruct i; simpl in *;
+  try (try destruct_reg_inv; monadInv H; simpl in *; reflexivity).
+Qed.
+
+Lemma label_pos_body bdy: forall c1 c2 z ex lbl
+  (HUNF : unfold_body bdy = OK c2),
+  Asm.label_pos lbl (z + Z.of_nat ((Datatypes.length bdy) + length_opt ex)) c1 = Asm.label_pos lbl (z) ((c2 ++ unfold_exit ex) ++ c1).
+Proof.
+  induction bdy.
+  - intros. inversion HUNF. simpl in *.
+    destruct ex eqn:EQEX.
+    + simpl in *. unfold Asm.is_label. destruct c; simpl; try congruence.
+      destruct i; simpl; try congruence.
+    + simpl in *. ring_simplify (z + 0). auto.
+  - intros. inversion HUNF; clear HUNF. monadInv H0. simpl in *.
+    erewrite no_label_in_basic_inst; eauto. rewrite <- IHbdy; eauto.
+    erewrite Zpos_P_of_succ_nat.
+    apply f_equal2; auto. omega.
+Qed.
+
+Lemma label_pos_preserved_gen bbs: forall lbl c z
+  (HUNF: unfold bbs = OK c),
+  label_pos lbl z bbs = Asm.label_pos lbl z c.
+Proof.
+  induction bbs.
+  - intros. simpl in *. inversion HUNF. simpl. reflexivity.
+  - intros. simpl in *. monadInv HUNF. unfold unfold_bblock in EQ.
+    destruct (zle _ _); try congruence. monadInv EQ.
+    destruct (is_label _ _) eqn:EQLBL.
+    + erewrite label_in_header_list; eauto.
+      simpl in *. destruct (peq lbl lbl); try congruence.
+    + erewrite IHbbs; eauto.
+      assert (Asm.label_pos lbl (z + size a) x0 = Asm.label_pos lbl (z + list_length_z (header a)) ((x1 ++ unfold_exit (exit a)) ++ x0)).
+      { unfold size.
+        rewrite <- plus_assoc. rewrite Nat2Z.inj_add.
+        rewrite list_length_z_nat.
+        replace (z + (Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a)))) with (z + Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a))) by omega.
+        eapply (label_pos_body (body a) x0 x1 (z + Z.of_nat (Datatypes.length (header a))) (exit a) lbl). auto. }
+      unfold is_label in *.
+      destruct (header a).
+      * replace (z + list_length_z (@nil label)) with (z) in H; eauto.
+        unfold list_length_z. simpl. omega.
+      * assert (l1 = nil).
+        { destruct l1; try congruence. rewrite !list_length_z_cons in l.
+          assert (list_length_z l2 >= 0) by eapply list_length_z_pos.
+          assert (list_length_z l2 + 1 + 1 >= 2) by omega.
+          assert (2 <= 1) by omega. contradiction H2. omega. }
+        subst. simpl in *. destruct (in_dec _ _) as [HIN|HNIN]; try congruence.
+        simpl in *.
+        destruct (peq _ _); try intuition congruence.
+Qed.
+
+Lemma label_pos_preserved b f lbl z tf: forall
+  (FIND: Genv.find_funct_ptr ge b = Some (Internal f))
   (FINDF: transf_function f = OK tf),
   label_pos lbl z (fn_blocks f) = Asm.label_pos lbl z (Asm.fn_code tf).
 Proof.
-Admitted.
+  intros.
+  eapply label_pos_preserved_gen.
+  unfold transf_function in FINDF. monadInv FINDF.
+  destruct zlt; try congruence. inversion EQ0. eauto.
+Qed.
 
 Lemma goto_label_preserved bb rs1 m1 rs1' m1' rs2 m2 lbl f tf v: forall
   (FINDF: transf_function f = OK tf)