Proof of label_pos related things in PostpassSchedulingproof

1 files changed, 104 insertions, 15 deletions

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,