Fixing the propagation of the new BOUNDED hyp

1 files changed, 20 insertions, 8 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 35d30d06..a055bb42 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -1087,6 +1087,7 @@ Proof.
       try (inversion MATCHI; subst; rewrite <- AG; try congruence);
       try (exploit next_inst_preserved; eauto);
       try (destruct_reg_size).
+    + 
 
       all:admit.
     all:admit.
@@ -1135,6 +1136,15 @@ Proof.
 
     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.
@@ -1148,10 +1158,6 @@ Proof.
     simpl in FIND_INSTR; rewrite Z.add_0_r in FIND_INSTR.
     rewrite list_length_z_cons in FIND_INSTR.
 
-    destruct BOUNDED as [(? & LT_MAX) LT_END_OF_BODY].
-    assert (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.
     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 |}
@@ -1325,7 +1331,17 @@ Proof.
 
   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'].
@@ -1337,10 +1353,6 @@ Proof.
   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).
   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.