Merge branch 'aarch64_block_bodystar' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into aarch64_block_bodystar

1 files changed, 14 insertions, 10 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 96cbf232..8ac9684d 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -1163,24 +1163,28 @@ Proof.
 Qed.
 
 Lemma exec_body_simulation_plus_alt li: forall b ofs f bb rs m s2 rs' m'
-  (BLI: li = body bb)
+  (BLI: is_tail li (body bb))
   (ATPC: rs 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)
-  (NEMPTY_BODY: body bb <> nil)
-  (MATCHI: match_internal (list_length_z (header bb)) (State rs m) s2)
-  (BODY: exec_body lk ge (body bb) rs m = Next rs' m'),
+  (NEMPTY_BODY: li <> nil)
+  (MATCHI: match_internal ((list_length_z (header bb)) + (list_length_z (body bb)) - (list_length_z li)) (State rs m) s2)
+  (BODY: exec_body lk ge li rs m = Next 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 li]; simpl; try congruence.
-  intros; rewrite <- BLI in *. simpl in *.
-  assert (BDYLENPOS: (0 < length (body bb))%nat). { rewrite <- BLI; simpl; omega. }
+  intros.
+  assert (BDYLENPOS: ((length li) < length (body bb))%nat). { admit. (* TODO *) }
   exploit internal_functions_unfold; eauto.
   intros (tc & FINDtf & TRANStf & _). 
   exploit find_basic_instructions; eauto.
-  rewrite <- BLI; intros FINDBI.
+  intros FINDBI.
   destruct FINDBI as (i_next & (bi_next' & (NTHBI & TRANSBI & FIND_INSTR))).
+
+(* TODO: hum not -- very tedious here ? *)
+
+(*
   inversion NTHBI; subst bi_next'.
   destruct (exec_basic _ _ _ _ _) eqn:EXEC_BASIC; next_stuck_cong.
   destruct s as (rs1 & m1); simpl in *.
@@ -1215,7 +1219,7 @@ Proof.
   (* 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 *)
+  - (* case of a single instruction in li: this our base case in the induction *)
     (* XXX New code --> no need to use the star' lemma this way. *)
     inversion BODY; subst.
     eexists; split.
@@ -1225,8 +1229,8 @@ Proof.
       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.
-  - (* len(body bb) >= 1 *)
-    (* TODO: apply the induction hypothesis IHli *)
+  - (* TODO: apply the induction hypothesis IHli *)
+*)
 Admitted.
 
 Lemma exec_body_simulation_plus b ofs f bb rs m s2 rs' m': forall