exec_body_simulation_plus_gen proof OK

1 files changed, 35 insertions, 11 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 87392139..df83e6a7 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -1371,6 +1371,24 @@ Proof.
   eexists; eexists; intuition eauto.
 Qed.
 
+Lemma header_body_tail_bound: forall (a: basic) (li: list basic) bb ofs
+  (BOUNDBB : Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned)
+  (BDYLENPOS : 0 <= list_length_z (body bb) - list_length_z (a :: li) <
+              list_length_z (body bb)),
+0 <= list_length_z (header bb) + list_length_z (body bb) - list_length_z (a :: li) <=
+Ptrofs.max_unsigned.
+Proof.
+  intros.
+  assert (HBBPOS: list_length_z (header bb) >= 0) by eapply list_length_z_pos.
+  assert (HBBSIZE: list_length_z (header bb) < size bb) by eapply header_size_lt_block_size.
+  assert (OFSBOUND: 0 <= Ptrofs.unsigned ofs <= Ptrofs.max_unsigned) by eapply Ptrofs.unsigned_range_2.
+  assert (BBSIZE: size bb <= Ptrofs.max_unsigned) by omega.
+  unfold size in BBSIZE.
+  rewrite !Nat2Z.inj_add in BBSIZE.
+  rewrite <- !list_length_z_nat in BBSIZE.
+  omega.
+Qed.
+
 (* A more general version of the exec_body_simulation_plus lemma below.
    This generalization is necessary for the induction proof inside the body.
 *)
@@ -1403,14 +1421,10 @@ Proof.
   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)
+  assert (BOUNDBBMAX: Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned)
   by (eapply size_of_blocks_bounds; eauto).
+  exploit header_body_tail_bound; eauto. intros BDYTAIL.
   exploit exec_basic_simulation; eauto.
-  { 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.
@@ -1425,10 +1439,20 @@ Proof.
   simpl in FIND_INSTR.
   (* Execute internal step. *)
   exploit (Asm.exec_step_internal tge b); eauto.
-    { (* unfold Ptrofs.add. repeat (rewrite Ptrofs.unsigned_repr);
-      try rewrite list_length_z_nat; try split; try omega.
-      simpl; rewrite <- list_length_z_nat; assumption. *)
-      admit. (* TODO *) }
+  {
+    rewrite Ptrofs.add_unsigned.
+    repeat (rewrite Ptrofs.unsigned_repr); try omega.
+    2: {
+      assert (BOUNDOFS: 0 <= Ptrofs.unsigned ofs <= Ptrofs.max_unsigned) by eapply Ptrofs.unsigned_range_2.
+      assert (list_length_z (body bb) <= size bb) by eapply body_size_le_block_size.
+      assert (list_length_z (header bb) <= 1). { eapply size_header; eauto. }
+      omega. }
+    try rewrite list_length_z_nat; try split;
+    simpl; rewrite <- !list_length_z_nat;
+    replace (Ptrofs.unsigned ofs + (list_length_z (header bb) + list_length_z (body bb) -
+      list_length_z (a :: li))) with (Ptrofs.unsigned ofs + list_length_z (header bb) +
+      (list_length_z (body bb) - list_length_z (a :: li))) by omega;
+    try assumption; try omega. }
 
   (* This is our STEP hypothesis. *)
   intros STEP_NEXT.
@@ -1459,7 +1483,7 @@ Proof.
    + intros (s2' & LAST_STEPS & LAST_MATCHS).
      eexists. split; eauto.
      eapply plus_left'; eauto.
-Admitted.
+Qed.
 
 Lemma exec_body_simulation_plus b ofs f bb rs m s2 rs' m': forall
   (ATPC: rs PC = Vptr b ofs)