Asmgen proof completely proved with ldp/stp

1 files changed, 53 insertions, 29 deletions

diff --git a/aarch64/PostpassScheduling.v b/aarch64/PostpassScheduling.v
index 548976c9..19bed77b 100644
--- a/aarch64/PostpassScheduling.v
+++ b/aarch64/PostpassScheduling.v
@@ -77,45 +77,69 @@ Definition verified_schedule (bb : bblock) : res bblock :=
   do schedcheck <- verify_schedule bb bb';
   OK (bb').
 
+(*Lemma size_peephole_unchanged: forall bb,*)
+  (*size (Peephole.optimize_bblock (no_header bb)) = size (no_header bb).*)
+(*Proof.*)
+  (*intros.*)
+  (*unfold Peephole.optimize_bblock, size in *. simpl in *.*)
+  (*destruct non_empty_bblockb eqn:NEMPTY; auto.*)
+  (*apply inj_eq. rewrite Nat.add_cancel_r.*)
+  (*unfold Peephole.optimize_body.*)
+  (*remember (body bb) as l.*)
+  (*generalize dependent l.*)
+  (*induction l.*)
+  (*- simpl. reflexivity.*)
+  (*- intros.*)
+    (*simpl.*)
+  (*unfold Peephole.stp_rep, Peephole.ldp_rep.*)
+
 Lemma verified_schedule_size:
   forall bb bb', verified_schedule bb = OK bb' -> size bb = size bb'.
 Proof.
 Admitted.
-(* TODO
-  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.*)
+  (*intros. unfold verified_schedule in H.*)
+  (*monadInv H.*)
+  (*unfold do_schedule in EQ.*)
+  (*destruct schedule in EQ.*)
+  (*destruct Peephole.optimize_bblock eqn:PEEP.*)
+  (*destruct (size (_) =? 1) eqn:TRIVB in EQ.*)
+  (*[>destruct (size (Peephole.optimize_bblock (no_header bb)) =? 1) eqn:TRIVB.<]*)
+  (*-*)
+    (*inv EQ. *)
+    (*unfold Peephole.optimize_bblock in PEEP. simpl in *.*)
+
+    (*unfold size. *)
+    (*simpl in *.*)
+
+    (*simpl. unfold non_empty_bblockb, non_empty_exit, non_empty_body.*)
+    (*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.*)
 
 Theorem verified_schedule_correct:
   forall ge f bb bb',
   verified_schedule bb = OK bb' ->
   bblock_simu lk ge f bb bb'.
 Proof.
-Admitted.
-  (* TODO intros.*)
-  (*monadInv H.*)
-  (*eapply bblock_simub_correct.*)
-  (*unfold verify_schedule in EQ0.*)
-  (*destruct (bblock_simub _ _) in *; try discriminate; auto.*)
-(*Qed.*)
+  intros.
+  monadInv H.
+  eapply bblock_simub_correct.
+  unfold verify_schedule in EQ0.
+  destruct (bblock_simub _ _) in *; try discriminate; auto.
+Qed.
 
 End verify_schedule.