slight refactoring, in order to avoid a duplication of the proof.

1 files changed, 36 insertions, 40 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 6b5b0913..530166c2 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -1141,54 +1141,51 @@ Lemma exec_body_simulation_plus_alt li: forall b ofs f bb rs m s2 rs' m'
   exists s2', plus Asm.step tge s2 E0 s2'
              /\ match_internal (size bb - (Z.of_nat (length_opt (exit bb)))) (State rs' m') s2'.
 Proof.
-  induction li as [|a [|b]]; simpl.
-  - (* len(body bb) == 0 *)
-    congruence.
-  - (* len(body bb) == 1 *)
-    (* Contruct the MI hypothesis. *)
-    intros. rewrite <- BLI in *. simpl in *.
-    exploit internal_functions_unfold; eauto.
-    intros (tc & FINDtf & TRANStf & _). 
-    assert (BDYLENPOS: (0 < length (body bb))%nat). { rewrite <- BLI; simpl; omega. }
-    exploit find_basic_instructions; eauto.
-    rewrite <- BLI; intros FINDBI.
-    destruct FINDBI as (i_next & (bi_next' & (NTHBI & TRANSBI & FIND_INSTR))).
-    inversion NTHBI; subst bi_next'.
-    destruct (exec_basic _ _ _ _ _) eqn:EXEC_BASIC; next_stuck_cong.
-    inversion BODY. subst.
-    destruct s as (rs1 & m1); simpl in *.
-    destruct s2 as (rs2 & m2); simpl in *.
-    exploit exec_basic_simulation; eauto.
-    intros (rs_next' & m_next' & EXEC_INSTR & MI_NEXT).
+  induction li as [|a li]; simpl; try congruence.
+  intros; rewrite <- BLI in *. simpl in *.
+  assert (BDYLENPOS: (0 < length (body bb))%nat). { rewrite <- BLI; simpl; omega. }
+  exploit internal_functions_unfold; eauto.
+  intros (tc & FINDtf & TRANStf & _). 
+  exploit find_basic_instructions; eauto.
+  rewrite <- BLI; intros FINDBI.
+  destruct FINDBI as (i_next & (bi_next' & (NTHBI & TRANSBI & FIND_INSTR))).
+  inversion NTHBI; subst bi_next'.
+  destruct (exec_basic _ _ _ _ _) eqn:EXEC_BASIC; next_stuck_cong.
+  destruct s as (rs1 & m1); simpl in *.
+  destruct s2 as (rs2 & m2); simpl in *.
+  exploit exec_basic_simulation; eauto.
+  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'].
-    subst A. subst B. subst C. subst D. subst E.
-    rewrite ATPC in AGPC. symmetry in AGPC, ATPC_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'].
+  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.
+  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).
-    
-    (* Execute internal step. *)
-    exploit (Asm.exec_step_internal tge b (Ptrofs.add ofs (Ptrofs.repr ((list_length_z (header bb)))))
+  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).
+
+  (* 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);
       try rewrite length_agree; try split; try omega.
       simpl; rewrite <- length_agree; assumption. }
 
-    (* This is our STEP hypothesis. *)
-    intros STEP_NEXT.
-    
+  (* This is our STEP hypothesis. *)
+  intros STEP_NEXT.
+  destruct li as [|a' li]; simpl in *.
+  - (* case of a single instruction: this our base case in the induction *)
     (* XXX New code --> no need to use the star' lemma this way. *)
+    inversion BODY; subst.
     eexists; split.
     + apply plus_one. eauto.
     + assert (BDYLEN: list_length_z (body bb) = 1).
@@ -1197,8 +1194,7 @@ Proof.
       { rewrite bblock_size_aux. omega. }
       rewrite BDYLEN in LEN1. rewrite LEN1. apply MI_NEXT.
   - (* len(body bb) >= 1 *)
-    (* Comment factoriser le code pour éviter de répéter les étapes du ca précédent ? Utiliser une ltac serait trop lourd ? *)
-
+    (* TODO: apply the induction hypothesis IHli *)
 Admitted.
 
 Lemma exec_body_simulation_plus b ofs f bb rs m s2 rs' m': forall