Main part of postpasssch proof now completed

1 files changed, 9 insertions, 414 deletions

diff --git a/aarch64/PostpassScheduling.v b/aarch64/PostpassScheduling.v
index fa7e2776..74c2438e 100644
--- a/aarch64/PostpassScheduling.v
+++ b/aarch64/PostpassScheduling.v
@@ -17,9 +17,8 @@
 
 Require Import Coqlib Errors AST Integers.
 Require Import Asmblock Axioms Memory Globalenvs.
-Require Import Asmblockdeps Asmblockgenproof0 Asmblockprops.
+Require Import Asmblockdeps Asmblockprops.
 Require Import IterList.
-(*Require Peephole.*)
 
 Local Open Scope error_monad_scope.
 
@@ -33,188 +32,6 @@ Section verify_schedule.
 
 Variable lk: aarch64_linker.
 
-(*
-(** * Concat all bundles into one big basic block *)
-
-(* Lemmas necessary for defining concat_all *)
-Lemma app_nonil {A: Type} (l l': list A) : l <> nil -> l ++ l' <> nil.
-Proof.
-  intros. destruct l; simpl.
-  - contradiction.
-  - discriminate.
-Qed.
-
-Lemma app_nonil2 {A: Type} : forall (l l': list A), l' <> nil -> l ++ l' <> nil.
-Proof.
-  destruct l.
-  - intros. simpl; auto.
-  - intros. rewrite <- app_comm_cons. discriminate.
-Qed.
-
-Definition check_size bb :=
-  if zlt Ptrofs.max_unsigned (size bb)
-    then Error (msg "PostpassSchedulingproof.check_size")
-  else OK tt.
-
-Program Definition concat2 (bb bb': bblock) : res bblock :=
-  do ch <- check_size bb;
-  do ch' <- check_size bb';
-  match (exit bb) with
-  | None => 
-      match (header bb') with
-      | nil => 
-          match (exit bb') with 
-          | Some (PExpand (Pbuiltin _ _ _)) => Error (msg "PostpassSchedulingproof.concat2: builtin not alone")
-          | _ => OK {| header := header bb; body := body bb ++ body bb'; exit := exit bb' |}
-          end
-      | _ => Error (msg "PostpassSchedulingproof.concat2")
-      end
-  | _ => Error (msg "PostpassSchedulingproof.concat2")
-  end.
-Next Obligation.
-  apply wf_bblock_refl. constructor.
-  - destruct bb' as [hd' bdy' ex' WF']. destruct bb as [hd bdy ex WF]. simpl in *.
-    apply wf_bblock_refl in WF'. apply wf_bblock_refl in WF.
-    inversion_clear WF'. inversion_clear WF. clear H1 H3.
-    inversion H2; inversion H0.
-    + left. apply app_nonil. auto.
-    + right. auto.
-    + left. apply app_nonil2. auto.
-    + right. auto.
-  - unfold builtin_alone. intros. rewrite H0 in H.
-    assert (Some (PExpand (Pbuiltin ef args res)) <> Some (PExpand (Pbuiltin ef args res))).
-    apply (H ef args res). contradict H1. auto.
-Defined.
-
-Lemma concat2_zlt_size:
-  forall a b bb,
-  concat2 a b = OK bb ->
-     size a <= Ptrofs.max_unsigned
-  /\ size b <= Ptrofs.max_unsigned.
-Proof.
-  intros. monadInv H.
-  split.
-  - unfold check_size in EQ. destruct (zlt Ptrofs.max_unsigned (size a)); monadInv EQ. omega.
-  - unfold check_size in EQ1. destruct (zlt Ptrofs.max_unsigned (size b)); monadInv EQ1. omega.
-Qed.
-
-Lemma concat2_noexit:
-  forall a b bb,
-  concat2 a b = OK bb ->
-  exit a = None.
-Proof.
-  intros. destruct a as [hd bdy ex WF]; simpl in *.
-  destruct ex as [e|]; simpl in *; auto.
-  unfold concat2 in H. simpl in H. monadInv H.
-Qed.
-
-Lemma concat2_decomp:
-  forall a b bb,
-  concat2 a b = OK bb ->
-     body bb = body a ++ body b
-  /\ exit bb = exit b.
-Proof.
-  intros. exploit concat2_noexit; eauto. intros.
-  destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bd ex WF]; simpl in *.
-  subst exa.
-  unfold concat2 in H; simpl in H.
-  destruct hdb.
-  - destruct exb.
-    + destruct c.
-      * destruct i; monadInv H; split; auto.
-      * monadInv H. split; auto.
-    + monadInv H. split; auto.
-  - monadInv H.
-Qed.
-
-Lemma concat2_size:
-  forall a b bb, concat2 a b = OK bb -> size bb = size a + size b.
-Proof.
-  intros. unfold concat2 in H.
-  destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bdy ex WF]; simpl in *.
-  destruct exa; monadInv H. destruct hdb; try (monadInv EQ2). destruct exb; try (monadInv EQ2).
-  - destruct c.
-    + destruct i; monadInv EQ2;
-      unfold size; simpl; rewrite app_length; rewrite Nat.add_0_r; rewrite <- Nat2Z.inj_add; rewrite Nat.add_assoc; reflexivity.
-    + monadInv EQ2. unfold size; simpl. rewrite app_length. rewrite Nat.add_0_r. rewrite <- Nat2Z.inj_add. rewrite Nat.add_assoc. reflexivity.
-  - unfold size; simpl. rewrite app_length. repeat (rewrite Nat.add_0_r). rewrite <- Nat2Z.inj_add. reflexivity.
-Qed.
-
-Lemma concat2_header:
-  forall bb bb' tbb,
-  concat2 bb bb' = OK tbb -> header bb = header tbb.
-Proof.
-  intros. destruct bb as [hd bdy ex COR]; destruct bb' as [hd' bdy' ex' COR']; destruct tbb as [thd tbdy tex tCOR]; simpl in *.
-  unfold concat2 in H. simpl in H. monadInv H.
-  destruct ex; try discriminate. destruct hd'; try discriminate. destruct ex'.
-  - destruct c.
-    + destruct i; try discriminate; congruence.
-    + congruence.
-  - congruence.
-Qed.
-
-Lemma concat2_no_header_in_middle:
-  forall bb bb' tbb,
-  concat2 bb bb' = OK tbb ->
-  header bb' = nil.
-Proof.
-  intros. destruct bb as [hd bdy ex COR]; destruct bb' as [hd' bdy' ex' COR']; destruct tbb as [thd tbdy tex tCOR]; simpl in *.
-  unfold concat2 in H. simpl in H. monadInv H.
-  destruct ex; try discriminate. destruct hd'; try discriminate. reflexivity.
-Qed.
-
-
-
-Fixpoint concat_all (lbb: list bblock) : res bblock :=
-  match lbb with
-  | nil => Error (msg "PostpassSchedulingproof.concatenate: empty list")
-  | bb::nil => OK bb
-  | bb::lbb =>
-      do bb' <- concat_all lbb;
-      concat2 bb bb'
-  end.
-
-Lemma concat_all_size :
-  forall lbb a bb bb',
-  concat_all (a :: lbb) = OK bb ->
-  concat_all lbb = OK bb' ->
-  size bb = size a + size bb'.
-Proof.
-  intros. unfold concat_all in H. fold concat_all in H.
-  destruct lbb; try discriminate.
-  monadInv H. rewrite H0 in EQ. inv EQ.
-  apply concat2_size. assumption.
-Qed.
-
-Lemma concat_all_header:
-  forall lbb bb tbb,
-  concat_all (bb::lbb) = OK tbb -> header bb = header tbb.
-Proof.
-  destruct lbb.
-  - intros. simpl in H. congruence.
-  - intros. simpl in H. destruct lbb.
-    + inv H. eapply concat2_header; eassumption.
-    + monadInv H. eapply concat2_header; eassumption.
-Qed.
-
-Lemma concat_all_no_header_in_middle:
-  forall lbb tbb,
-  concat_all lbb = OK tbb ->
-  Forall (fun b => header b = nil) (tail lbb).
-Proof.
-  induction lbb; intros; try constructor.
-  simpl. simpl in H. destruct lbb.
-  - constructor.
-  - monadInv H. simpl tl in IHlbb. constructor.
-    + apply concat2_no_header_in_middle in EQ0. apply concat_all_header in EQ. congruence.
-    + apply IHlbb in EQ. assumption.
-Qed.
-
-Inductive is_concat : bblock -> list bblock -> Prop :=
-  | mk_is_concat: forall tbb lbb, concat_all lbb = OK tbb -> is_concat tbb lbb.
-*)
-(** * Remainder of the verified scheduler *)
-
 Definition verify_schedule (bb bb' : bblock) : res unit :=
   match bblock_simub bb bb' with
   | true => OK tt
@@ -230,105 +47,6 @@ Proof.
   apply Z.eqb_eq. assumption.
 Qed.
 
-(* Lemma verify_schedule_no_header:
-  forall bb bb',
-  verify_schedule (no_header bb) bb' = verify_schedule bb bb'.
-Proof.
-  intros. unfold verify_schedule. unfold bblock_simub. unfold pure_bblock_simu_test, bblock_simu_test. rewrite trans_block_noheader_inv.
-  reflexivity.
-Qed. *)
-
-
-(*Lemma stick_header_verify_schedule:*)
-  (*forall hd bb' hbb' bb,*)
-  (*stick_header hd bb' = hbb' ->*)
-  (*verify_schedule bb bb' = verify_schedule bb hbb'.*)
-(*Proof.*)
-  (*intros. unfold verify_schedule. unfold bblock_simub, pure_bblock_simu_test, bblock_simu_test.*)
-  (*rewrite <- H. rewrite trans_block_header_inv. reflexivity.*)
-(*Qed.*)
-
-(*Lemma check_size_stick_header:*)
-  (*forall bb hd,*)
-  (*check_size bb = check_size (stick_header hd bb).*)
-(*Proof.*)
-  (*intros. unfold check_size. rewrite stick_header_size. reflexivity.*)
-(*Qed.*)
-
-(*Lemma stick_header_concat2:*)
-  (*forall bb bb' hd tbb,*)
-  (*concat2 bb bb' = OK tbb ->*)
-  (*concat2 (stick_header hd bb) bb' = OK (stick_header hd tbb).*)
-(*Proof.*)
-  (*intros. monadInv H. erewrite check_size_stick_header in EQ.*)
-  (*unfold concat2. rewrite EQ. rewrite EQ1. simpl.*)
-  (*destruct bb as [hdr bdy ex COR]; destruct bb' as [hdr' bdy' ex' COR']; simpl in *.*)
-  (*destruct ex; try discriminate. destruct hdr'; try discriminate. destruct ex'.*)
-  (*- destruct c.*)
-    (*+ destruct i; try discriminate; inv EQ2; unfold stick_header; simpl; reflexivity.*)
-    (*+ inv EQ2. unfold stick_header; simpl. reflexivity.*)
-  (*- inv EQ2. unfold stick_header; simpl. reflexivity.*)
-(*Qed.*)
-
-(*Lemma stick_header_concat_all:*)
-  (*forall bb c tbb hd,*)
-  (*concat_all (bb :: c) = OK tbb ->*)
-  (*concat_all (stick_header hd bb :: c) = OK (stick_header hd tbb).*)
-(*Proof.*)
-  (*intros. simpl in *. destruct c; try congruence.*)
-  (*monadInv H. rewrite EQ. simpl.*)
-  (*apply stick_header_concat2. assumption.*)
-(*Qed.*)
-
-(*Lemma stick_header_code_no_header:*)
-  (*forall bb c,*)
-  (*stick_header_code (header bb) (no_header bb :: c) = OK (bb :: c).*)
-(*Proof.*)
-  (*intros. unfold stick_header_code. simpl. rewrite stick_header_no_header. reflexivity.*)
-(*Qed.*)
-
-(*Lemma hd_tl_size:*)
-  (*forall lbb bb, hd_error lbb = Some bb -> size_blocks lbb = size bb + size_blocks (tl lbb).*)
-(*Proof.*)
-  (*destruct lbb.*)
-  (*- intros. simpl in H. discriminate.*)
-  (*- intros. simpl in H. inv H. simpl. reflexivity.*)
-(*Qed.*)
-
-(*Lemma stick_header_code_size:*)
-  (*forall h lbb lbb', stick_header_code h lbb = OK lbb' -> size_blocks lbb = size_blocks lbb'.*)
-(*Proof.*)
-  (*intros. unfold stick_header_code in H. destruct (hd_error lbb) eqn:HD; try discriminate.*)
-  (*inv H. simpl. rewrite stick_header_size. erewrite hd_tl_size; eauto.*)
-(*Qed.*)
-
-(*Lemma stick_header_code_no_header_in_middle:*)
-  (*forall c h lbb,*)
-  (*stick_header_code h c = OK lbb ->*)
-  (*Forall (fun b => header b = nil) (tl c) ->*)
-  (*Forall (fun b => header b = nil) (tl lbb).*)
-(*Proof.*)
-  (*destruct c; intros.*)
-  (*- unfold stick_header_code in H. simpl in H. discriminate.*)
-  (*- unfold stick_header_code in H. simpl in H. inv H. simpl in H0.*)
-    (*simpl. assumption.*)
-(*Qed.*)
-
-(*Lemma stick_header_code_concat_all:*)
-  (*forall hd lbb hlbb tbb,*)
-  (*stick_header_code hd lbb = OK hlbb ->*)
-  (*concat_all lbb = OK tbb ->*)
-  (*exists htbb,*)
-     (*concat_all hlbb = OK htbb*)
-  (*/\ stick_header hd tbb = htbb.*)
-(*Proof.*)
-  (*intros. exists (stick_header hd tbb). split; auto.*)
-  (*destruct lbb.*)
-  (*- unfold stick_header_code in H. simpl in H. discriminate.*)
-  (*- unfold stick_header_code in H. simpl in H. inv H.*)
-    (*apply stick_header_concat_all. assumption.*)
-(*Qed.*)
-
 Program Definition make_bblock_from_basics lb :=
   match lb with
   | nil => Error (msg "PostpassScheduling.make_bblock_from_basics")
@@ -341,79 +59,22 @@ Program Definition schedule_to_bblock (lb: list basic) (oc: option control) : re
   | Some c => OK {| header := nil; body := lb; exit := Some c |}
   end.
 Next Obligation.
-  unfold Is_true, AB.non_empty_bblockb.
-  unfold AB.non_empty_exit. rewrite orb_true_r. reflexivity.
+  unfold Is_true, non_empty_bblockb.
+  unfold non_empty_exit. rewrite orb_true_r. reflexivity.
 Qed.
 
 Definition do_schedule (bb: bblock) : res bblock :=
   if (Z.eqb (size bb) 1) then OK (bb) 
-  else match (schedule bb) with (lb, oc) => schedule_to_bblock lb oc end. (* TODO Something here *)
-
-(* TODO to remove ? *)
-(*Definition verify_par_bblock (bb: bblock) : res unit :=*)
-  (*if (bblock_para_check bb) then OK tt else Error (msg "PostpassScheduling.verify_par_bblock").*)
-(*Fixpoint verify_par (lbb: list bblock) :=*)
-  (*match lbb with*)
-  (*| nil => OK tt*)
-  (*| bb :: lbb => do res <- verify_par_bblock bb; verify_par lbb*)
-  (*end.*)
+  else match (schedule bb) with (lb, oc) => schedule_to_bblock lb oc end.
 
 Definition verified_schedule (bb : bblock) : res bblock :=
   let nhbb  := no_header bb in
-  (* TODO remove? let bb'' := Peephole.optimize_bblock bb' in *)
   do nhbb' <- do_schedule nhbb;
-  (*do tbb <- concat_all lbb;*)
   let bb' := stick_header (header bb) nhbb' in
   do sizecheck <- verify_size bb bb';
-  do schedcheck <- verify_schedule bb bb'; (* TODO Keep this one *)
+  do schedcheck <- verify_schedule bb bb';
   OK (bb').
 
-(* Definition verified_schedule_nob (bb : bblock) : res (list bblock) :=
-  let nhbb  := no_header bb in
-  do bb' <- do_schedule nhbb;
-  do sizecheck <- verify_size nhbb bb';
-  do schedcheck <- verify_schedule nhbb bb';
-  do res <- stick_header_code (header bb) bb';
-  OK res. *)
-
-(*Lemma verified_schedule_nob_size:*)
-  (*forall bb lbb, verified_schedule_nob bb = OK lbb -> size bb = size_blocks lbb.*)
-(*Proof.*)
-  (*intros. monadInv H. erewrite <- stick_header_code_size; eauto.*)
-  (*apply verify_size_size.*)
-  (*destruct x1; try discriminate. assumption.*)
-(*Qed.*)
-
-(*Lemma verified_schedule_nob_no_header_in_middle:*)
-  (*forall lbb bb,*)
-  (*verified_schedule_nob bb = OK lbb ->*)
-     (*Forall (fun b => header b = nil) (tail lbb).*)
-(*Proof.*)
-  (*intros. monadInv H. eapply stick_header_code_no_header_in_middle; eauto.*)
-  (*eapply concat_all_no_header_in_middle. eassumption.*)
-(*Qed.*)
-
-(*Lemma verified_schedule_nob_header:*)
-  (*forall bb tbb lbb,*)
-  (*verified_schedule_nob bb = OK (tbb :: lbb) ->*)
-     (*header bb = header tbb*)
-  (*/\ Forall (fun b => header b = nil) lbb.*)
-(*Proof.*)
-  (*intros. split.*)
-  (*- monadInv H. unfold stick_header_code in EQ3. destruct (hd_error _); try discriminate. inv EQ3.*)
-    (*simpl. reflexivity.*)
-  (*- apply verified_schedule_nob_no_header_in_middle in H. assumption.*)
-(*Qed.*)
-
-
-(* Definition verified_schedule (bb : bblock) : res (list bblock) :=
-  verified_schedule_nob bb. *)
-(* TODO Remove? 
-  match exit bb with
-  | Some (PExpand (Pbuiltin ef args res)) => OK (bb::nil) (* Special case for ensuring the lemma verified_schedule_builtin_idem *)
-  | _ => verified_schedule_nob bb
-  end.*)
-
 Lemma verified_schedule_size:
   forall bb bb', verified_schedule bb = OK bb' -> size bb = size bb'.
 Proof.
@@ -439,83 +100,17 @@ Proof.
     rewrite ESIZE. reflexivity.
 Qed.
 
-(*Lemma verified_schedule_no_header_in_middle:*)
-  (*forall lbb bb,*)
-  (*verified_schedule bb = OK lbb ->*)
-     (*Forall (fun b => header b = nil) (tail lbb).*)
-(*Proof.*)
-  (*intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.*)
-  (*all: try (eapply verified_schedule_nob_no_header_in_middle; eauto; fail).*)
-  (*inv H. simpl. auto.*)
-(*Qed.*)
-
-(*Lemma verified_schedule_header:*)
-  (*forall bb tbb lbb,*)
-  (*verified_schedule bb = OK (tbb :: lbb) ->*)
-     (*header bb = header tbb*)
-  (*/\ Forall (fun b => header b = nil) lbb.*)
-(*Proof.*)
-  (*intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.*)
-  (*all: try (eapply verified_schedule_nob_header; eauto; fail).*)
-  (*inv H. split; simpl; auto.*)
-(*Qed.*)
-
-
-(*Lemma verified_schedule_nob_correct:*)
-  (*forall ge f bb lbb,*)
-  (*verified_schedule_nob bb = OK lbb ->*)
-  (*exists tbb,*)
-     (*is_concat tbb lbb*)
-  (*/\ bblock_simu ge f bb tbb.*)
-(*Proof.*)
-  (*intros. monadInv H.*)
-  (*exploit stick_header_code_concat_all; eauto.*)
-  (*intros (tbb & CONC & STH).*)
-  (*exists tbb. split; auto. constructor; auto.*)
-  (*rewrite verify_schedule_no_header in EQ2. erewrite stick_header_verify_schedule in EQ2; eauto.*)
-  (*eapply bblock_simub_correct; eauto. unfold verify_schedule in EQ2.*)
-  (*destruct (bblock_simub _ _); auto; try discriminate.*)
-(*Qed.*)
-
 Theorem verified_schedule_correct:
   forall ge f bb bb',
   verified_schedule bb = OK bb' ->
   bblock_simu lk ge f bb bb'.
 Proof.
-(*  intros.
-  assert (size bb = size bb'). { apply verified_schedule_size. auto. }
-  unfold verified_schedule in H. monadInv H.
+  intros.
+  monadInv H.
   eapply bblock_simub_correct.
-  unfold do_schedule in EQ.
   unfold verify_schedule in EQ0.
-  
-  destruct (bblock_simub _ _) in *; try discriminate.
-  destruct schedule.
-  simpl. unfold bblock_simub.
-  
-    eapply bblock_simub_correct.
-  destruct (bblock_simub); try discriminate.
-  
-  destruct schedule.
-   unfold bblock_simu, exec_bblock. destruct (exit bb). destruct c. destruct i.
-   
-   - intros rs m rs' m' t (rs1 & m1 & EBDY & EXT).
-   
-     eexists; eexists; split.
-     simpl. unfold exec_body.
-   
-  all: try (eapply verified_schedule_nob_correct; eauto; fail).
-  inv H. eexists; eexists; split; simpl; auto. constructor; auto. simpl; auto. constructor; auto.
-Qed. *)
-Admitted.
-(*Lemma verified_schedule_builtin_idem:*)
-  (*forall bb ef args res lbb,*)
-  (*exit bb = Some (PExpand (Pbuiltin ef args res)) ->*)
-  (*verified_schedule bb = OK lbb ->*)
-  (*lbb = bb :: nil.*)
-(*Proof.*)
-  (*intros. unfold verified_schedule in H0. rewrite H in H0. inv H0. reflexivity.*)
-(*Qed.*)
+  destruct (bblock_simub _ _) in *; try discriminate; auto.
+Qed.
 
 End verify_schedule.