Merge remote-tracking branch 'origin/aarch64_block_bodystar' into aarch64_block_bodystar

1 files changed, 114 insertions, 222 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index c89a4320..7d1f1d05 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -21,6 +21,7 @@ Require Import Op Locations Machblock Conventions PseudoAsmblock Asmblock.
 Require Machblockgenproof Asmblockgenproof.
 Require Import Asmgen.
 Require Import Axioms.
+Require Import IterList.
 
 
 Module Asmblock_PRESERVATION.
@@ -1276,100 +1277,6 @@ Proof.
     try (find_rwrt_ag).
 Qed.
 
-Lemma exec_body_simulation_star': forall
-  b ofs f bb tc bis end_of_body rs_start m_start s_start rs_end m_end
-  (ATPC: rs_start PC = Vptr b ofs)
-  (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
-  (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb)
-  (MATCHI: match_internal (end_of_body - list_length_z bis) (State rs_start m_start) s_start)
-  (BOUNDED: 0 <= Ptrofs.unsigned ofs + end_of_body <= Ptrofs.max_unsigned
-            /\ list_length_z bis <= end_of_body)
-  (UNFOLD: unfold (fn_blocks f) = OK tc)
-  (FINDBI: forall n : nat, (n < length bis)%nat ->
-          exists (i : Asm.instruction) (bi : basic),
-             list_nth_z bis (Z.of_nat n) = Some bi
-          /\ basic_to_instruction bi = OK i
-          /\ Asm.find_instr (Ptrofs.unsigned ofs + end_of_body - (list_length_z bis) + Z.of_nat n) tc = Some i)
-  (BODY: exec_body lk ge bis rs_start m_start = Next rs_end m_end),
-  exists s_end, star Asm.step tge s_start E0 s_end
-             /\ match_internal end_of_body (State rs_end m_end) s_end.
-Proof.
-  induction bis as [| bi_next bis IH].
-  - intros; eexists; split.
-    + apply star_refl.
-    + inv BODY;
-      unfold list_length_z in MATCHI; simpl in MATCHI; rewrite Z.sub_0_r in MATCHI;
-      assumption.
-  - intros.
-    exploit internal_functions_unfold; eauto.
-    intros (x & FINDtf & TRANStf & _).
-    assert (x = tc) by congruence; subst x.
-
-    assert (FINDBI' := FINDBI).
-    specialize (FINDBI' 0%nat).
-    destruct FINDBI' as (i_next & (bi_next' & (NTHBI & TRANSBI & FIND_INSTR))); try (simpl; omega).
-    inversion NTHBI; subst bi_next'.
-    simpl in BODY; destruct exec_basic as [s_next|] eqn:BASIC; try discriminate.
-
-    destruct s_next as (rs_next & m_next); simpl in BODY.
-    destruct s_start as (rs_start' & m_start').
-
-    destruct BOUNDED as [(LT_MIN & LT_MAX) LT_END_OF_BODY].
-    assert (LT_END_OF_BODY_BIS: list_length_z bis < end_of_body)
-      by (rewrite list_length_z_cons in LT_END_OF_BODY; omega).
-    generalize (Ptrofs.unsigned_range_2 ofs); intros LT_OFS_MAXU.
-
-    assert (list_length_z (bi_next :: bis) >= 0) by eapply list_length_z_pos.
-    assert (BOUNDED_BIS: 0 <= end_of_body - list_length_z (bi_next :: bis) <= Ptrofs.max_unsigned) by omega.
-
-    exploit exec_basic_simulation; eauto.
-    intros (rs_next' & m_next' & EXEC_INSTR & MI_NEXT).
-    exploit exec_basic_dont_move_PC; eauto; intros AGPC.
-    inversion MI_NEXT as [? ? ? ? ? M_NEXT_AGREE RS_NEXT_AGREE ATPC_NEXT OFS_NEXT RS RS']; subst.
-    rewrite ATPC in AGPC; symmetry in AGPC, ATPC_NEXT.
-
-    inversion MATCHI as [? ? ? ? ? M_AGREE RS_AGREE ATPC' OFS RS RS']; subst.
-    symmetry in ATPC'. rewrite list_length_z_cons in ATPC'.
-    rewrite ATPC in ATPC'.
-    unfold Val.offset_ptr in ATPC'.
-    simpl in FIND_INSTR; rewrite Z.add_0_r in FIND_INSTR.
-    rewrite list_length_z_cons in FIND_INSTR.
-
-    exploit (Asm.exec_step_internal tge b
-             (Ptrofs.add ofs (Ptrofs.repr (end_of_body - (list_length_z bis + 1))))
-             {| Asm.fn_sig := fn_sig f; Asm.fn_code := tc |}
-             i_next rs_start' m_start'); eauto.
-    { unfold Ptrofs.add; repeat (rewrite Ptrofs.unsigned_repr);
-      try (split; try omega; rewrite length_agree; omega).
-      rewrite Z.add_sub_assoc; assumption. }
-    intros STEP_NEXT.
-
-    rewrite list_length_z_cons in MI_NEXT.
-    (* XXX use better tactics *)
-    replace (end_of_body - (list_length_z bis + 1) + 1)
-       with (end_of_body - list_length_z bis) in MI_NEXT by omega.
-    assert (0 <= Ptrofs.unsigned ofs + end_of_body <= Ptrofs.max_unsigned
-            /\ list_length_z bis <= end_of_body). { split; omega. }
-    exploit IH; eauto.
-    { (* XXX *)
-      intros n NLT.
-      assert (NLT': (n + 1 < length (bi_next :: bis))%nat). { simpl; omega. }
-      specialize (FINDBI (n + 1)%nat NLT').
-      rewrite list_length_z_cons in FINDBI; simpl in FINDBI.
-      destruct zeq as [e|]. { rewrite Nat2Z.inj_add in e; simpl in e; omega. }
-      rewrite Nat2Z.inj_add in FINDBI; simpl in FINDBI.
-      replace (Ptrofs.unsigned ofs + end_of_body - (list_length_z bis + 1) + (Z.of_nat n + 1))
-         with (Ptrofs.unsigned ofs + end_of_body - list_length_z bis + Z.of_nat n) in FINDBI by omega.
-      replace (Z.pred (Z.of_nat n + 1)) with (Z.of_nat n) in FINDBI by omega.
-      assumption. }
-    intros IH'.
-    destruct IH' as (? & STEP_REST & MATCH_REST).
-
-    eexists; split.
-    + eapply star_step; eauto.
-    + auto.
-Qed.
-
 Lemma find_basic_instructions b ofs f bb tc: forall
   (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
   (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb)
@@ -1404,7 +1311,70 @@ Proof.
       rewrite H in H0; simpl in H0; repeat rewrite length_agree in H0; omega.
 Qed.
 
-Lemma exec_body_simulation_plus_alt li: forall b ofs f bb rs m s2 rs' m'
+(** "is_tail" auxiliary lemma about is_tail to move in IterList ou Coqlib (déplacer aussi Machblockgenproof.is_tail_app_inv) ? *)
+
+Lemma is_tail_app_right A (l2 l1: list A): is_tail l1 (l2++l1).
+Proof.
+  intros; eapply Machblockgenproof.is_tail_app_inv; econstructor.
+Qed.
+
+Lemma is_tail_app_def A (l1 l2: list A):
+  is_tail l1 l2 -> exists l3, l2 = l3 ++ l1.
+Proof.
+  induction 1 as [|x l1 l2]; simpl.
+  - exists nil; simpl; auto.
+  - destruct IHis_tail as (l3 & EQ); rewrite EQ.
+    exists (x::l3); simpl; auto.
+Qed.
+
+Lemma is_tail_bound A (l1 l2: list A):
+  is_tail l1 l2 -> (length l1 <= length l2)%nat.
+Proof.
+  intros H; destruct (is_tail_app_def _ _ _ H) as (l3 & EQ).
+  subst; rewrite app_length.
+  omega.
+Qed.
+
+Lemma is_tail_list_nth_z A (l1 l2: list A):
+  is_tail l1 l2 -> list_nth_z l2 ((list_length_z l2) - (list_length_z l1)) = list_nth_z l1 0.
+Proof.
+  induction 1; simpl.
+  - replace (list_length_z c - list_length_z c) with 0; omega || auto.
+  - assert (X: list_length_z (i :: c2) > list_length_z c1).
+    { rewrite !list_length_z_nat, <- Nat2Z.inj_gt.
+      exploit is_tail_bound; simpl; eauto.
+      omega. }
+    destruct (zeq (list_length_z (i :: c2) - list_length_z c1) 0) as [Y|Y]; try omega.
+    replace (Z.pred (list_length_z (i :: c2) - list_length_z c1)) with (list_length_z c2 - list_length_z c1); auto.
+    rewrite list_length_z_cons.
+    omega.
+Qed.
+
+(* TODO: remplacer find_basic_instructions directement par ce lemme ? *)
+Lemma find_basic_instructions_alt b ofs f bb tc n: forall
+  (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
+  (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb)
+  (UNFOLD: unfold (fn_blocks f) = OK tc)
+  (BOUND: 0 <= n < list_length_z (body bb)),
+  exists (i : Asm.instruction) (bi : basic),
+     list_nth_z (body bb) n = Some bi
+  /\ basic_to_instruction bi = OK i
+  /\ Asm.find_instr (Ptrofs.unsigned ofs
+                     + (list_length_z (header bb))
+                     + n) tc
+                     = Some i.
+Proof.
+  intros; assert ((Z.to_nat n) < length (body bb))%nat.
+  { rewrite Nat2Z.inj_lt, <- list_length_z_nat, Z2Nat.id; try omega. }
+  exploit find_basic_instructions; eauto.
+  rewrite Z2Nat.id; try omega. intros (i & bi & X).
+  eexists; eexists; intuition eauto.
+Qed.
+
+(* A more general version of the exec_body_simulation_plus lemma below.
+   This generalization is necessary for the induction proof inside the body.
+*)
+Lemma exec_body_simulation_plus_gen li: forall b ofs f bb rs m s2 rs' m'
   (BLI: is_tail li (body bb))
   (ATPC: rs PC = Vptr b ofs)
   (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
@@ -1417,38 +1387,27 @@ Lemma exec_body_simulation_plus_alt li: forall b ofs f bb rs m s2 rs' m'
 Proof.
   induction li as [|a li]; simpl; try congruence.
   intros.
-  (*assert (BDYLENPOS: ((length li) < length (body bb))%nat). { *)
-  assert (BDYLENPOS: (0 < length (body bb))%nat). { 
-    (*apply is_tail_cons_left in BLI as BLI'.*)
-    (*apply is_tail_incl in BLI as INCLBLI.*)
-    (*apply NoDup_incl_length in INCLBLI as INCLBLILEN.*)
-    (* TODO -> The above statement requires a NoDup hyp... *)
-    (*econstructor.*)
-    (*assert (TAILLEN: ((length li) < (length (a :: li)))%nat). {*)
-      (*econstructor.*)
-    admit. }
+  assert (BDYLENPOS: 0 <= (list_length_z (body bb) - list_length_z (a::li)) < list_length_z (body bb)). {
+    assert (Z.of_nat O < list_length_z (a::li) <= list_length_z (body bb)); try omega.
+    rewrite !list_length_z_nat; split.
+    - rewrite <- Nat2Z.inj_lt. simpl. omega.
+    - rewrite <- Nat2Z.inj_le; eapply is_tail_bound; eauto.
+  }
   exploit internal_functions_unfold; eauto.
   intros (tc & FINDtf & TRANStf & _). 
-  exploit find_basic_instructions; eauto.
-  intros FINDBI.
-  destruct FINDBI as (i_next & (bi_next' & (NTHBI & TRANSBI & FIND_INSTR))).
-  assert (NEMPTY_BODY': body bb <> nil). {
-    eapply is_tail_in in BLI as BLIIN.
-    unfold not. intros.
-    rewrite H in BLIIN.
-    eapply in_nil in BLIIN; eauto. }
-
-(* Il nous faut une hypothese type BDY: body bb = bi :: bis *)
-(* TODO: hum not -- very tedious here ? *)
-
-  (*
-  inversion NTHBI; subst bi_next'.
+  exploit find_basic_instructions_alt; eauto.
+  intros (tbi & (bi & (NTHBI & TRANSBI & FIND_INSTR))).
+  exploit is_tail_list_nth_z; eauto.
+  rewrite NTHBI; simpl.
+  intros X; inversion X; subst; clear X NTHBI.
   destruct (exec_basic _ _ _ _ _) eqn:EXEC_BASIC; next_stuck_cong.
   destruct s as (rs1 & m1); simpl in *.
   destruct s2 as (rs2 & m2); simpl in *.
+  assert (BOUNDBB: Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned)
+  by (eapply size_of_blocks_bounds; eauto).
   exploit exec_basic_simulation; eauto.
+  { 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.
   inversion MI_NEXT as [A B C D E M_NEXT_AGREE RS_NEXT_AGREE ATPC_NEXT PC_OFS_NEXT RS RS'].
@@ -1458,20 +1417,14 @@ Proof.
   inv MATCHI. symmetry in AGPC0.
   rewrite ATPC in AGPC0.
   unfold Val.offset_ptr in AGPC0.
-  simpl in FIND_INSTR; rewrite Z.add_0_r in FIND_INSTR.
-
-  assert (Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned)
-  by (eapply size_of_blocks_bounds; eauto).
-  generalize (header_size_lt_block_size bb). rewrite length_agree; intros HEADER_LT.
-  generalize (Ptrofs.unsigned_range_2 ofs). intros (A & B).
 
+  simpl in FIND_INSTR.
   (* Execute internal step. *)
-  exploit (Asm.exec_step_internal tge b (Ptrofs.add ofs (Ptrofs.repr ((list_length_z (header bb)))))
-             {| Asm.fn_sig := fn_sig f; Asm.fn_code := tc |}
-             i_next rs2 m2); eauto.
-    { unfold Ptrofs.add. repeat (rewrite Ptrofs.unsigned_repr);
+  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. }
+      simpl; rewrite <- length_agree; assumption. *)
+      admit. (* TODO *) }
 
   (* This is our STEP hypothesis. *)
   intros STEP_NEXT.
@@ -1481,13 +1434,27 @@ Proof.
     inversion BODY; subst.
     eexists; split.
     + apply plus_one. eauto.
-    + assert (BDYLEN: list_length_z (body bb) = 1).
-      { rewrite <- BLI. apply list_length_z_cons. }
-      assert (LEN1: size bb - Z.of_nat (length_opt (exit bb)) = list_length_z (header bb) + list_length_z (body bb)).
-      { rewrite bblock_size_aux. omega. }
-      rewrite BDYLEN in LEN1. rewrite LEN1. apply MI_NEXT.
+    + constructor; auto.
+      rewrite ATPC_NEXT.
+      apply f_equal.
+      apply f_equal.
+      rewrite bblock_size_aux, list_length_z_cons; simpl.
+      omega.
   - (* TODO: apply the induction hypothesis IHli *)
-*)
+   exploit (IHli b ofs f bb rs1 m_next' (State rs_next' m_next')); congruence || eauto.
+   + exploit is_tail_app_def; eauto.
+     intros (l3 & EQ); rewrite EQ.
+     exploit (is_tail_app_right _ (l3 ++ a::nil)).
+     rewrite <- app_assoc; simpl; eauto.
+   + constructor; auto.
+     rewrite ATPC_NEXT.
+     apply f_equal.
+     apply f_equal.
+     rewrite! list_length_z_cons; simpl.
+     omega.
+   + intros (s2' & LAST_STEPS & LAST_MATCHS).
+     eexists. split; eauto.
+     eapply plus_left'; eauto.
 Admitted.
 
 Lemma exec_body_simulation_plus b ofs f bb rs m s2 rs' m': forall
@@ -1501,89 +1468,10 @@ Lemma exec_body_simulation_plus b ofs f bb rs m s2 rs' m': forall
              /\ match_internal (size bb - (Z.of_nat (length_opt (exit bb)))) (State rs' m') s2'.
 Proof.
   intros.
-  exploit internal_functions_unfold; eauto.
-  intros (tc & FINDtf & TRANStf & _).
-
-  (* Prove an Asm.step given that body bb is not empty *)
-
-  destruct (body bb) as [| bi bis] eqn:BDY; try contradiction.
-  assert (H: (0 < length (body bb))%nat). { rewrite BDY; simpl; omega. }
-  exploit find_basic_instructions; eauto. clear H. rewrite BDY; intros FINDBI.
-  destruct FINDBI as (i_next & (bi_next' & (NTHBI & TRANSBI & FIND_INSTR))).
-  inversion NTHBI; subst bi_next'.
-  simpl in BODY. destruct exec_basic as [s_next|] eqn:BASIC; try discriminate.
-
-  destruct s_next as (rs_next & m_next); simpl in BODY.
-  destruct s2 as (rs_start' & m_start').
-
-  assert (list_length_z (header bb) >= 0) by eapply list_length_z_pos.
-  assert (LT_OFS_BB_MAXU: Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned)
-    by (eapply size_of_blocks_bounds; eauto).
-  generalize (header_size_lt_block_size bb). rewrite length_agree; intros HEADER_LT.
-  generalize (Ptrofs.unsigned_range_2 ofs). intros (LT_MIN & LT_MAX).
-  assert (list_length_z (header bb) <= Ptrofs.max_unsigned).
-  { rewrite length_agree; omega. }
-  assert (BOUNDED: 0 <= list_length_z (header bb) <= Ptrofs.max_unsigned) by omega.
-  exploit exec_basic_simulation; eauto.
-
-  intros (rs_next' & m_next' & EXEC_INSTR & MI_NEXT).
-  exploit exec_basic_dont_move_PC; eauto. intros AGPC.
-  inversion MI_NEXT as [A B C D E M_NEXT_AGREE RS_NEXT_AGREE ATPC_NEXT PC_OFS_NEXT RS RS'].
-  subst A. subst B. subst C. subst D. subst E.
-  rewrite ATPC in AGPC. symmetry in AGPC, ATPC_NEXT.
-
-  inv MATCHI. symmetry in AGPC0.
-  rewrite ATPC in AGPC0.
-  unfold Val.offset_ptr in AGPC0.
-  simpl in FIND_INSTR; rewrite Z.add_0_r in FIND_INSTR.
-
-  exploit (Asm.exec_step_internal tge b (Ptrofs.add ofs (Ptrofs.repr ((list_length_z (header bb)))))
-           {| Asm.fn_sig := fn_sig f; Asm.fn_code := tc |}
-           i_next rs_start' m_start'); eauto.
-  { unfold Ptrofs.add. repeat (rewrite Ptrofs.unsigned_repr);
-    try rewrite length_agree; try split; try omega.
-    simpl; rewrite <- length_agree; assumption. }
-  intros STEP_NEXT.
-
-  (* Now, use exec_body_simulation_star' to go the rest of the way 0+ steps *)
-  rewrite AGPC in ATPC_NEXT.
-  unfold Val.offset_ptr in ATPC_NEXT.
-  unfold Ptrofs.add in ATPC_NEXT.
-  rewrite Ptrofs.unsigned_repr in ATPC_NEXT. 2: { rewrite length_agree; split; omega. }
-
-  (* give omega more facts to work with *)
-  assert (list_length_z (header bb) + list_length_z (body bb) <= size bb). {
-    rewrite bblock_size_aux. omega. }
-  generalize (body_size_le_block_size bb). rewrite length_agree. intros.
-  assert (0 <= Ptrofs.unsigned ofs + (list_length_z (header bb) + list_length_z (body bb))
-            <= Ptrofs.max_unsigned
-            /\ list_length_z bis <= list_length_z (header bb) + list_length_z (body bb)).
-  { split; try omega. split; try omega.
-    - rewrite length_agree in H0; repeat (rewrite length_agree); omega.
-    - rewrite BDY. rewrite list_length_z_cons; repeat rewrite length_agree; omega. }
-
-  exploit (exec_body_simulation_star' b ofs
-           f bb tc bis (list_length_z (header bb) + list_length_z (body bb))); eauto.
-  - rewrite BDY. unfold list_length_z. simpl.
-    repeat (rewrite list_length_add_acc). repeat (rewrite Z.add_0_r).
-    rewrite Z.add_assoc. rewrite Z.add_sub_swap. rewrite Z.add_simpl_r.
-    apply MI_NEXT.
-  - rewrite Z.add_assoc.
-    intros n NBOUNDS.
-    rewrite BDY.
-    assert (NBOUNDS': (n + 1 < length (body bb))%nat). { rewrite BDY; simpl; omega. }
-    exploit find_basic_instructions; eauto. rewrite BDY; intros FINDBI.
-    simpl in FINDBI. destruct zeq as [e|]. { rewrite Nat2Z.inj_add in e; simpl in e; omega. }
-    rewrite Nat2Z.inj_add in FINDBI; simpl in FINDBI.
-    replace (Z.pred (Z.of_nat n + 1)) with (Z.of_nat n) in FINDBI by omega.
-    rewrite list_length_z_cons, Z.add_assoc, Z.add_sub_swap, Z.add_simpl_r.
-    replace (Ptrofs.unsigned ofs + list_length_z (header bb) + (Z.of_nat n + 1))
-       with (Ptrofs.unsigned ofs + list_length_z (header bb) + 1 + Z.of_nat n) in FINDBI by omega.
-    assumption.
-  - intros (s_end & STAR_STEP & MI_STAR).
-    eexists s_end; split.
-    + eapply plus_left; eauto.
-    + rewrite bblock_size_aux, Z.add_simpl_r. assumption.
+  exploit exec_body_simulation_plus_gen; eauto.
+  - constructor.
+  - replace (list_length_z (header bb) + list_length_z (body bb) - list_length_z (body bb)) with (list_length_z (header bb)); auto.
+    omega.
 Qed.
 
 Lemma exec_body_simulation_star b ofs f bb rs m s2 rs' m': forall
@@ -1894,9 +1782,13 @@ Proof.
       rewrite H in EXIT. (* exit bb is a cfi *)
       inv EXIT.
       rewrite H in MATCHI. simpl in MATCHI.
-      exploit exec_cfi_simulation; eauto; intros.
+      exploit internal_functions_translated; eauto.
+      rewrite FINDtf.
+      intros (tf & FINDtf' & TRANSf). inversion FINDtf'; subst; clear FINDtf'.
+      exploit exec_cfi_simulation; eauto.
       (* extract exec_cfi_simulation's conclusion as separate hypotheses *)
-      destruct H3. destruct H3. destruct H3. rewrite H5.
+      (* TODO: ligne ci-dessous à remplacer avec un intro (rs2' & m2' & ...) *)
+      intro H3; destruct H3; destruct H3; destruct H3. rewrite H5.
       inversion MATCHI.
       apply plus_one.
       eapply Asm.exec_step_internal; eauto.