From 7b68243df6cc0529e7d666e3c7f2c7f09c6af1a7 Mon Sep 17 00:00:00 2001
From: Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr>
Date: Wed, 5 Aug 2020 14:54:06 +0200
Subject: Proof for size_of_blocks_max_pos

---
 aarch64/Asmgenproof.v | 68 +++++++++++++++++++++++++++++++++++++--------------
 1 file changed, 50 insertions(+), 18 deletions(-)

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 16977d67..2ee33568 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -221,24 +221,6 @@ Proof.
     rewrite H; omega.
 Qed.
 
-Lemma size_of_blocks_max_pos pos f tf bi:
-  find_bblock pos (fn_blocks f) = Some bi ->
-  transf_function f = OK tf ->
-  pos + size bi <= max_pos tf.
-Admitted.
-
-Lemma size_of_blocks_bounds fb pos f bi:
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  find_bblock pos (fn_blocks f) = Some bi ->
-  pos + size bi <= Ptrofs.max_unsigned.
-Proof.
-  intros; exploit internal_functions_translated; eauto.
-  intros (tf & _ & TRANSf).
-  assert (pos + size bi <= max_pos tf). { eapply size_of_blocks_max_pos; eauto. }
-  assert (max_pos tf <= Ptrofs.max_unsigned). { eapply functions_bound_max_pos; eauto. }
-  omega.
-Qed.
-
 Lemma one_le_max_unsigned:
   1 <= Ptrofs.max_unsigned.
 Proof.
@@ -517,6 +499,44 @@ Proof.
   rewrite plus_assoc. auto.
 Qed.
 
+Lemma size_of_blocks_max_pos_aux:
+  forall bbs tbbs pos bb,
+  find_bblock pos bbs = Some bb ->
+  unfold bbs = OK tbbs ->
+  pos + size bb <= list_length_z tbbs.
+Proof.
+  induction bbs as [| bb ? IHbbs].
+  - intros tbbs ? ? FINDBB; inversion FINDBB.
+  - simpl; intros tbbs pos bb' FINDBB UNFOLD.
+    apply bind_inversion in UNFOLD; destruct UNFOLD as (tbb & UNFOLD_BBLOCK & H).
+    apply bind_inversion in H; destruct H as (tbbs' & UNFOLD & CONS).
+    inv CONS.
+    destruct (zlt pos 0). { discriminate FINDBB. }
+    destruct (zeq pos 0).
+    + inv FINDBB.
+      exploit bblock_size_preserved; eauto; intros SIZE; rewrite SIZE.
+      repeat (rewrite length_agree). rewrite app_length, Nat2Z.inj_add.
+      omega.
+    + generalize (IHbbs tbbs' (pos - size bb) bb' FINDBB UNFOLD). intros IH.
+      exploit bblock_size_preserved; eauto; intros SIZE.
+      repeat (rewrite length_agree); rewrite app_length.
+      rewrite Nat2Z.inj_add; repeat (rewrite <- length_agree).
+      omega.
+Qed.
+
+Lemma size_of_blocks_max_pos pos f tf bi:
+  find_bblock pos (fn_blocks f) = Some bi ->
+  transf_function f = OK tf ->
+  pos + size bi <= max_pos tf.
+Proof.
+  unfold transf_function, max_pos.
+  intros FINDBB UNFOLD.
+  apply bind_inversion in UNFOLD. destruct UNFOLD as (? & UNFOLD & H).
+  destruct (zlt Ptrofs.max_unsigned (list_length_z x)). { discriminate H. }
+  inv H. simpl.
+  eapply size_of_blocks_max_pos_aux; eauto.
+Qed.
+
 Lemma unfold_bblock_not_nil bb:
   unfold_bblock bb = OK nil -> False.
 Proof.
@@ -552,6 +572,18 @@ Proof.
       eapply IHtbb; eauto.
 Qed.
 
+Lemma size_of_blocks_bounds fb pos f bi:
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
+      find_bblock pos (fn_blocks f) = Some bi ->
+      pos + size bi <= Ptrofs.max_unsigned.
+Proof.
+  intros; exploit internal_functions_translated; eauto.
+  intros (tf & _ & TRANSf).
+  assert (pos + size bi <= max_pos tf). { eapply size_of_blocks_max_pos; eauto. }
+  assert (max_pos tf <= Ptrofs.max_unsigned). { eapply functions_bound_max_pos; eauto. }
+  omega.
+Qed.
+
 Lemma find_instr_bblock_tail:
   forall tbb bb pos c i,
   Asm.find_instr pos c = Some i ->
-- 
cgit