Simplifications in Peephole and size proof.

1 files changed, 13 insertions, 51 deletions

diff --git a/aarch64/PostpassScheduling.v b/aarch64/PostpassScheduling.v
index 19bed77b..b8c16131 100644
--- a/aarch64/PostpassScheduling.v
+++ b/aarch64/PostpassScheduling.v
@@ -68,66 +68,28 @@ 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.
 
+Definition do_peephole (bb: bblock) : bblock :=
+  let res := Peephole.optimize_bblock bb in
+  if (size res =? size bb) then res else bb.
+
 Definition verified_schedule (bb : bblock) : res bblock :=
   let nhbb  := no_header bb in
-  let nhbb' := Peephole.optimize_bblock nhbb in
-  do nhbb'' <- do_schedule nhbb';
-  let bb' := stick_header (header bb) nhbb'' in
+  let phbb := do_peephole nhbb in
+  do schbb <- do_schedule phbb;
+  let bb' := stick_header (header bb) schbb in
   do sizecheck <- verify_size bb bb';
   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.
-  (*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.*)
+  intros. unfold verified_schedule in H.
+  monadInv H.
+  unfold verify_size in EQ1.
+  destruct (size _ =? size _) eqn:ESIZE_H in EQ1; try discriminate.
+  rewrite Z.eqb_eq in ESIZE_H; rewrite ESIZE_H; reflexivity.
+Qed.
 
 Theorem verified_schedule_correct:
   forall ge f bb bb',