Prove find_instr_bblock_tail

1 files changed, 89 insertions, 2 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 7ef345b2..6e54d399 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -468,13 +468,100 @@ Proof.
   intros n H; destruct (zeq _ _); (try eapply IHl); omega.
 Qed.
 
+Lemma equal_header_size bb:
+  length (header bb) = length (unfold_label (header bb)).
+Proof.
+  induction (header bb); auto.
+  simpl. rewrite IHl. auto.
+Qed.
+
+Lemma equal_body_size:
+  forall bb tb,
+  unfold_body (body bb) = OK tb ->
+  length (body bb) = length tb.
+Proof.
+  intros bb. induction (body bb).
+  - simpl. intros ? H. inversion H. auto.
+  - intros tb H. simpl in H. apply bind_inversion in H. destruct H as (? & BI & TAIL).
+    apply bind_inversion in TAIL. destruct TAIL as (tb' & BODY' & CONS). inv CONS.
+    simpl. specialize (IHl tb' BODY'). rewrite IHl. reflexivity.
+Qed.
+
+Lemma equal_exit_size bb:
+  length_opt (exit bb) = length (unfold_exit (exit bb)).
+Proof.
+  destruct (exit bb); trivial.
+Qed.
+
+Lemma bblock_size_preserved bb tb:
+  unfold_bblock bb = OK tb ->
+  size bb = list_length_z tb.
+Proof.
+  unfold unfold_bblock. intros UNFOLD_BBLOCK.
+  destruct (zle (list_length_z (header bb)) 1). 2: { inversion UNFOLD_BBLOCK. }
+  apply bind_inversion in UNFOLD_BBLOCK. destruct UNFOLD_BBLOCK as (? & UNFOLD_BODY & CONS).
+  inversion CONS.
+  unfold size.
+  rewrite equal_header_size, equal_exit_size.
+  erewrite equal_body_size; eauto.
+  rewrite length_agree.
+  repeat (rewrite app_length).
+  rewrite plus_assoc. auto.
+Qed.
+
+Lemma unfold_bblock_not_nil bb:
+  unfold_bblock bb = OK nil -> False.
+Proof.
+  intros.
+  exploit bblock_size_preserved; eauto. unfold list_length_z; simpl. intros SIZE.
+  generalize (bblock_size_pos bb). intros SIZE'. omega.
+Qed.
+
+(* same proof as list_nth_z_range (Coqlib) *)
+Lemma find_instr_range:
+  forall c n i,
+  Asm.find_instr n c = Some i -> 0 <= n < list_length_z c.
+Proof.
+  induction c; simpl; intros.
+  discriminate.
+  rewrite list_length_z_cons. destruct (zeq n 0).
+  generalize (list_length_z_pos c); omega.
+  exploit IHc; eauto. omega.
+Qed.
+
+Lemma find_instr_tail:
+  forall tbb pos c i,
+  Asm.find_instr pos c = Some i ->
+  Asm.find_instr (pos + list_length_z tbb) (tbb ++ c) = Some i.
+Proof.
+  induction tbb as [| ? ? IHtbb].
+  - intros. unfold list_length_z; simpl. rewrite Z.add_0_r. assumption.
+  - intros. rewrite list_length_z_cons. simpl.
+    destruct (zeq (pos + (list_length_z tbb + 1)) 0).
+    + exploit find_instr_range; eauto. intros POS_RANGE.
+      generalize (list_length_z_pos tbb). omega.
+    + replace (pos + (list_length_z tbb + 1) - 1) with (pos + list_length_z tbb) by omega.
+      eapply IHtbb; eauto.
+Qed.
+
 Lemma find_instr_bblock_tail:
-  forall pos c i bb tbb,
+  forall tbb bb pos c i,
   Asm.find_instr pos c = Some i ->
   unfold_bblock bb = OK tbb ->
   Asm.find_instr (pos + size bb ) (tbb ++ c) = Some i.
 Proof.
-Admitted.
+  induction tbb.
+   - intros. exploit unfold_bblock_not_nil; eauto. intros. contradiction.
+   - intros. simpl.
+     destruct (zeq (pos + size bb) 0).
+     + (* absurd *)
+       exploit find_instr_range; eauto. intros POS_RANGE.
+       generalize (bblock_size_pos bb). intros SIZE. omega.
+     + erewrite bblock_size_preserved; eauto.
+       rewrite list_length_z_cons.
+       replace (pos + (list_length_z tbb + 1) - 1) with (pos + list_length_z tbb) by omega.
+       apply find_instr_tail; auto.
+Qed.
 
 Lemma list_nth_z_find_label:
   forall (ll : list label) il n l,