Start of the postpasschedproof, redefining verify schedule lemmas

1 files changed, 91 insertions, 41 deletions

diff --git a/aarch64/PostpassScheduling.v b/aarch64/PostpassScheduling.v
index a9473789..fa7e2776 100644
--- a/aarch64/PostpassScheduling.v
+++ b/aarch64/PostpassScheduling.v
@@ -18,6 +18,7 @@
 Require Import Coqlib Errors AST Integers.
 Require Import Asmblock Axioms Memory Globalenvs.
 Require Import Asmblockdeps Asmblockgenproof0 Asmblockprops.
+Require Import IterList.
 (*Require Peephole.*)
 
 Local Open Scope error_monad_scope.
@@ -28,6 +29,10 @@ Axiom schedule: bblock -> (list basic) * option control.
 
 Extract Constant schedule => "PostpassSchedulingOracle.schedule".
 
+Section verify_schedule.
+
+Variable lk: aarch64_linker.
+
 (*
 (** * Concat all bundles into one big basic block *)
 
@@ -216,22 +221,22 @@ Definition verify_schedule (bb bb' : bblock) : res unit :=
   | false => Error (msg "PostpassScheduling.verify_schedule")
   end.
 
-(*Definition verify_size bb lbb := if (Z.eqb (size bb) (size_blocks lbb)) then OK tt else Error (msg "PostpassScheduling:verify_size: wrong size").*)
+Definition verify_size bb bb' := if (Z.eqb (size bb) (size bb')) then OK tt else Error (msg "PostpassScheduling:verify_size: wrong size").
 
-(*Lemma verify_size_size:*)
-  (*forall bb lbb, verify_size bb lbb = OK tt -> size bb = size_blocks lbb.*)
-(*Proof.*)
-  (*intros. unfold verify_size in H. destruct (size bb =? size_blocks lbb) eqn:SIZE; try discriminate.*)
-  (*apply Z.eqb_eq. assumption.*)
-(*Qed.*)
+Lemma verify_size_size:
+  forall bb bb', verify_size bb bb' = OK tt -> size bb = size bb'.
+Proof.
+  intros. unfold verify_size in H. destruct (size bb =? size bb') eqn:SIZE; try discriminate.
+  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 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:*)
@@ -354,14 +359,22 @@ Definition do_schedule (bb: bblock) : res bblock :=
   (*end.*)
 
 Definition verified_schedule (bb : bblock) : res bblock :=
-  let bb'  := no_header bb in
+  let nhbb  := no_header bb in
   (* TODO remove? let bb'' := Peephole.optimize_bblock bb' in *)
-  do lb <- do_schedule bb';
+  do nhbb' <- do_schedule nhbb;
   (*do tbb <- concat_all lbb;*)
-  (*do sizecheck <- verify_size bb lbb;*)
-  do schedcheck <- verify_schedule bb' lb; (* TODO Keep this one *)
-  (*do parcheck <- verify_par res;*)
-  OK (stick_header (header bb) lb).
+  let bb' := stick_header (header bb) nhbb' in
+  do sizecheck <- verify_size bb bb';
+  do schedcheck <- verify_schedule bb bb'; (* TODO Keep this one *)
+  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.*)
@@ -393,21 +406,38 @@ Definition verified_schedule (bb : bblock) : res bblock :=
 (*Qed.*)
 
 
-(*Definition verified_schedule (bb : bblock) : res (list bblock) :=*)
-  (*verified_schedule_nob bb.*)
+(* 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 lbb, verified_schedule bb = OK lbb -> size bb = size_blocks lbb.*)
-(*Proof.*)
-  (*intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.*)
-  (*all: try (apply verified_schedule_nob_size; auto; fail).*)
-  (*inv H. simpl. omega.*)
-(*Qed.*)
+Lemma verified_schedule_size:
+  forall bb bb', verified_schedule bb = OK bb' -> size bb = size bb'.
+Proof.
+  intros. unfold verified_schedule in H.
+  monadInv H.
+  unfold do_schedule in EQ.
+  destruct schedule in EQ.
+  destruct (size (no_header bb) =? 1) eqn:TRIVB.
+  - inv EQ. unfold size. simpl. reflexivity.
+  - unfold schedule_to_bblock in EQ.
+  destruct o in EQ.
+  + inv EQ. unfold verify_size in EQ1. unfold size in *. simpl in *.
+    rewrite Z.eqb_neq in TRIVB.
+    destruct (Z.of_nat (Datatypes.length (header bb) + Datatypes.length (body bb) + length_opt (exit bb)) =?
+    Z.of_nat (Datatypes.length (header bb) + Datatypes.length l + 1)) eqn:ESIZE; try discriminate.
+    rewrite Z.eqb_eq in ESIZE; repeat rewrite Nat2Z.inj_add in *;
+    rewrite ESIZE. reflexivity.
+  + unfold make_bblock_from_basics in EQ. destruct l in EQ; try discriminate.
+    inv EQ. unfold verify_size in EQ1; unfold size in *; simpl in *.
+    destruct (Z.of_nat (Datatypes.length (header bb) + Datatypes.length (body bb) + length_opt (exit bb)) =?
+    Z.of_nat (Datatypes.length (header bb) + Datatypes.S (Datatypes.length l) + 0)) eqn:ESIZE; try discriminate.
+    rewrite Z.eqb_eq in ESIZE. repeat rewrite Nat2Z.inj_add in *.
+    rewrite ESIZE. reflexivity.
+Qed.
 
 (*Lemma verified_schedule_no_header_in_middle:*)
   (*forall lbb bb,*)
@@ -447,18 +477,37 @@ Definition verified_schedule (bb : bblock) : res bblock :=
   (*destruct (bblock_simub _ _); auto; try discriminate.*)
 (*Qed.*)
 
-(*Theorem verified_schedule_correct:*)
-  (*forall ge f bb lbb,*)
-  (*verified_schedule bb = OK lbb ->*)
-  (*exists tbb,*)
-     (*is_concat tbb lbb*)
-  (*/\ bblock_simu ge f bb tbb.*)
-(*Proof.*)
-  (*intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.*)
-  (*all: try (eapply verified_schedule_nob_correct; eauto; fail).*)
-  (*inv H. eexists. split; simpl; auto. constructor; auto. simpl; auto. constructor; auto.*)
-(*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.
+  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)) ->*)
@@ -468,6 +517,7 @@ Definition verified_schedule (bb : bblock) : res bblock :=
   (*intros. unfold verified_schedule in H0. rewrite H in H0. inv H0. reflexivity.*)
 (*Qed.*)
 
+End verify_schedule.
 
 Fixpoint transf_blocks (lbb : list bblock) : res (list bblock) :=
   match lbb with