From baeaefa7e1c24e38b3ed41bd894db45057d0eb2b Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Mon, 4 Feb 2019 16:20:18 +0100
Subject: Proof of label_pos related things in PostpassSchedulingproof

---
 mppa_k1c/PostpassSchedulingproof.v | 119 ++++++++++++++++++++++++++++++++-----
 1 file changed, 104 insertions(+), 15 deletions(-)

(limited to 'mppa_k1c')

diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index ad423fb0..08f6f1be 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -123,7 +123,8 @@ Axiom verified_schedule_single_inst: forall bb, size bb = 1 -> verified_schedule
 Axiom verified_schedule_header:
   forall bb tbb lbb,
   verified_schedule bb = OK (tbb :: lbb) ->
-  header bb = header tbb.
+     header bb = header tbb
+  /\ Forall (fun b => header b = nil) lbb.
 
 Remark builtin_body_nil:
   forall bb ef args res, exit bb = Some (PExpand (Pbuiltin ef args res)) -> body bb = nil.
@@ -566,28 +567,116 @@ Proof.
   destruct lbb; simpl in *; discriminate.
 Qed.
 
+Lemma header_nil_label_pos_none:
+  forall lbb l p,
+  Forall (fun b => header b = nil) lbb -> label_pos l p lbb = None.
+Proof.
+  induction lbb.
+  - intros. simpl. auto.
+  - intros. inv H. simpl. unfold is_label. rewrite H2. destruct (in_dec l nil). { inv i. }
+    auto.
+Qed.
+
 Lemma verified_schedule_label:
   forall bb tbb lbb l,
   verified_schedule bb = OK (tbb :: lbb) ->
-  is_label l bb = is_label l tbb.
+     is_label l bb = is_label l tbb
+  /\ label_pos l 0 lbb = None.
 Proof.
-Admitted.
+  intros. exploit verified_schedule_header; eauto.
+  intros (HdrEq & HdrNil).
+  split.
+  - unfold is_label. rewrite HdrEq. reflexivity.
+  - apply header_nil_label_pos_none. assumption.
+Qed.
 
-Lemma label_pos_head_app:
-  forall c bb lbb l tc,
-  verified_schedule bb = OK lbb ->
-  label_pos l 0 c = label_pos l 0 tc ->
-  label_pos l 0 (bb :: c) = label_pos l 0 (lbb ++ tc).
+Lemma label_pos_app_none:
+  forall c c' l p p',
+  label_pos l p c = None ->
+  label_pos l (p' + size_blocks c) c' = label_pos l p' (c ++ c').
 Proof.
   induction c.
-  - intros. simpl in H0. destruct lbb.
-    + apply verified_schedule_not_empty in H. contradiction.
-    + rewrite (head_tail lbb). simpl tl.
-      simpl. erewrite verified_schedule_label; eauto.
-      destruct (is_label l b) eqn:ISLBL; simpl; auto.
-      (* TODO - finish *)
-Admitted.
+  - intros. simpl in *. rewrite Z.add_0_r. reflexivity.
+  - intros. simpl in *. destruct (is_label _ _) eqn:ISLABEL.
+    + discriminate.
+    + eapply IHc in H. rewrite Z.add_assoc. eauto.
+Qed.
+
+Remark label_pos_pvar_none_add:
+  forall tc l p p' k,
+  label_pos l (p+k) tc = None -> label_pos l (p'+k) tc = None.
+Proof.
+  induction tc.
+  - intros. simpl. auto.
+  - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
+    + discriminate.
+    + pose (IHtc l p p' (k + size a)). repeat (rewrite Z.add_assoc in e). auto.
+Qed.
+
+Lemma label_pos_pvar_none:
+  forall tc l p p',
+  label_pos l p tc = None -> label_pos l p' tc = None.
+Proof.
+  intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1.
+  eapply label_pos_pvar_none_add; eauto.
+Qed.
+
+Remark label_pos_pvar_some_add_add:
+  forall tc l p p' k k',
+  label_pos l (p+k') tc = Some (p+k) -> label_pos l (p'+k') tc = Some (p'+k).
+Proof.
+  induction tc.
+  - intros. simpl in H. discriminate.
+  - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
+    + inv H. assert (k = k') by omega. subst. reflexivity.
+    + pose (IHtc l p p' k (k' + size a)). repeat (rewrite Z.add_assoc in e). auto.
+Qed.
+
+Lemma label_pos_pvar_some_add:
+  forall tc l p p' k,
+  label_pos l p tc = Some (p+k) -> label_pos l p' tc = Some (p'+k).
+Proof.
+  intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1.
+  eapply label_pos_pvar_some_add_add; eauto.
+Qed.
+
+Remark label_pos_pvar_add:
+  forall c tc l p p' k,
+  label_pos l (p+k) c = label_pos l p tc ->
+  label_pos l (p'+k) c = label_pos l p' tc.
+Proof.
+  induction c.
+  - intros. simpl in *.
+    exploit label_pos_pvar_none; eauto.
+  - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
+    + exploit label_pos_pvar_some_add; eauto.
+    + pose (IHc tc l p p' (k+size a)). repeat (rewrite Z.add_assoc in e). auto.
+Qed.
 
+Lemma label_pos_pvar:
+  forall c tc l p p',
+  label_pos l p c = label_pos l p tc ->
+  label_pos l p' c = label_pos l p' tc.
+Proof.
+  intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1.
+  eapply label_pos_pvar_add; eauto.
+Qed.
+
+Lemma label_pos_head_app:
+  forall c bb lbb l tc p,
+  verified_schedule bb = OK lbb ->
+  label_pos l p c = label_pos l p tc ->
+  label_pos l p (bb :: c) = label_pos l p (lbb ++ tc).
+Proof.
+  intros. simpl. destruct lbb as [|tbb lbb].
+  - apply verified_schedule_not_empty in H. contradiction.
+  - simpl. exploit verified_schedule_label; eauto. intros (ISLBL & LBLPOS).
+    rewrite ISLBL.
+    destruct (is_label l tbb) eqn:ISLBL'; simpl; auto.
+    eapply label_pos_pvar in H0. erewrite H0.
+    erewrite verified_schedule_size; eauto. simpl size_blocks. rewrite Z.add_assoc.
+    erewrite label_pos_app_none; eauto.
+Qed.
 
 Lemma label_pos_preserved:
   forall c tc l,
-- 
cgit