Work on scheduling proof

4 files changed, 154 insertions, 25 deletions

diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v
index e97e907..f201914 100644
--- a/src/hls/Abstr.v
+++ b/src/hls/Abstr.v
@@ -219,6 +219,10 @@ Lemma get_empty:
   forall r, empty#r r = NE.singleton (Ptrue, Ebase r).
 Proof. unfold "#r"; intros. rewrite RTree.gempty. trivial. Qed.
 
+Lemma get_empty_p:
+  forall p, empty#p p = Plit (true, PEbase p).
+Proof. unfold "#p", get_forest_p'; intros. rewrite PTree.gempty. trivial. Qed.
+
 Lemma forest_reg_gso:
   forall (f : forest) w dst dst',
     dst <> dst' ->
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v
index 11da966..08806aa 100644
--- a/src/hls/GiblePargen.v
+++ b/src/hls/GiblePargen.v
@@ -40,6 +40,8 @@ Require Import vericert.hls.GiblePargenproofEquiv.
 
 Import NE.NonEmptyNotation.
 
+Import ListNotations.
+
 #[local] Open Scope positive.
 #[local] Open Scope forest.
 #[local] Open Scope pred_op.
@@ -309,6 +311,11 @@ Get a sequence from the basic block.
 Definition abstract_sequence (b : list instr) : option forest :=
   Option.map snd (mfold_left update b (Some (Ptrue, empty))).
 
+Compute Option.bind (fun x => RTree.get (Reg 3) (forest_regs x))
+  (abstract_sequence
+    [RBop None Op.Odiv [1;2] 3;
+     RBop None (Op.Ointconst (Int.repr 10)) nil 3]).
+
 (*|
 Check equivalence of control flow instructions.  As none of the basic blocks
 should have been moved, none of the labels should be different, meaning the
diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v
index 02d776d..7b68475 100644
--- a/src/hls/GiblePargenproofBackward.v
+++ b/src/hls/GiblePargenproofBackward.v
@@ -92,25 +92,122 @@ Definition abstract_sequence' (b : list instr) : option (forest * list pred_expr
   Option.map (fun x => let '(_, y, z) := x in (y, z))
     (mfold_left update' b (Some (Ptrue, empty, nil))).
 
-Lemma abstr_seq_reverse_correct :
-  forall sp x i i' ti cf x' l p p' l' f,
-    mfold_left update' x (Some (p, f, l)) = Some (p', x', l') ->
-    (forall p, In p l -> exists r, sem_pred_expr x'.(forest_preds) sem_value (mk_ctx i sp ge) p r) ->
-    sem (mk_ctx i sp ge) x' (i', (Some cf)) ->
+Definition i_state (s: istate): instr_state :=
+  match s with
+  | Iexec t => t
+  | Iterm t _ => t
+  end.
+
+Definition cf_state (s: istate): option cf_instr :=
+  match s with
+  | Iexec _ => None
+  | Iterm _ cf => Some cf
+  end.
+
+Definition evaluable_pred_expr {G} (ctx: @Abstr.ctx G) pr p :=
+  exists r,
+      sem_pred_expr pr sem_value ctx p r.
+
+Definition evaluable_pred_list {G} ctx pr l :=
+  forall p,
+    In p l ->
+    @evaluable_pred_expr G ctx pr p.
+
+Lemma evaluable_pred_expr_exists :
+  forall sp pr f i0 exit_p exit_p' f' cf i ti p op args dst,
+    update (exit_p, f) (RBop p op args dst) = Some (exit_p', f') ->
+    sem (mk_ctx i0 sp ge) f (i, cf) ->
+    evaluable_pred_expr (mk_ctx i0 sp ge) pr (f' #r (Reg dst)) ->
     state_lessdef i ti ->
-   exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf)
-           /\ state_lessdef i' ti'.
+    exists ti', step_instr ge sp (Iexec ti) (RBop p op args dst) (Iexec ti').
+Proof.
+  intros. cbn in H. unfold Option.bind in H. destr. inv H.
+  destruct ti. econstructor. econstructor.
+  unfold evaluable_pred_expr in H1. Admitted.
+
+Lemma remember_expr_in :
+  forall x l f a,
+    In x l -> In x (remember_expr f l a).
+Proof.
+  unfold remember_expr; destruct a; eauto using in_cons.
+Qed.
+
+Lemma in_mfold_left_abstr :
+  forall instrs p f l p' f' l' x,
+    mfold_left update' instrs (Some (p, f, l)) = Some (p', f', l') ->
+    In x l -> In x l'.
+Proof.
+  induction instrs; intros.
+  - cbn in *; now inv H.
+  - cbn -[update] in *.
+    pose proof H as Y.
+    apply OptionExtra.mfold_left_Some in Y. inv Y.
+    rewrite H1 in H. destruct x0 as ((p_int & f_int) & l_int).
+    exploit IHinstrs; eauto.
+    unfold Option.bind2, Option.ret in H1; repeat destr. inv H1.
+    auto using remember_expr_in.
+Qed.
+
+Lemma abstr_seq_reverse_correct_fold :
+  forall sp instrs i0 i i' ti cf f' l p p' l' f,
+    sem (mk_ctx i0 sp ge) f (i, None) ->
+    mfold_left update' instrs (Some (p, f, l)) = Some (p', f', l') ->
+    evaluable_pred_list (mk_ctx i0 sp ge) f'.(forest_preds) l' ->
+    sem (mk_ctx i0 sp ge) f' (i', Some cf) ->
+    state_lessdef i ti ->
+    exists ti',
+      SeqBB.step ge sp (Iexec ti) instrs (Iterm ti' cf)
+      /\ state_lessdef i' ti'.
+Proof.
+  induction instrs; intros * Y3 Y Y0 Y1 Y2.
+  - cbn in *. inv Y.
+    assert (similar {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |}
+                    {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |})
+      by auto using similar_refl.
+    now eapply sem_det in H; [| eapply Y1 | eapply Y3 ].
+  - cbn -[update] in Y.
+    pose proof Y as YX.
+    apply OptionExtra.mfold_left_Some in YX. inv YX.
+    rewrite H in Y.
+    destruct x as ((p_mid & f_mid) & l_mid).
+    unfold Option.bind2, Option.ret in H. repeat destr.
+    inv H.
+
+    (* Assume we are in RBop for now*)
+    assert (exists pred op args dst, a = RBop pred op args dst)
+      by admit; destruct H as (pred & op & args & dst & EQ); subst a.
+
+    exploit evaluable_pred_expr_exists; eauto.
+    unfold evaluable_pred_list in Y0.
+    instantiate (1 := forest_preds f').
+    apply Y0 in YI. auto.
+    (* provable using evaluability in list *) intros [t step].
+
+    assert (exists ti_mid, sem {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |}
+                             f_mid (ti_mid, None)) by admit.
+
+    destruct H as (ti_mid & Hsem2).
+    exploit IHinstrs. 2: { eapply Y. }  eauto. auto. eauto. reflexivity.
+    intros (ti_mid' & Hseq & Hstate).
+    assert (state_lessdef ti_mid t) by admit.
+    exists ti_mid'; split; auto.
+    econstructor; eauto.
+Admitted.
+
+Lemma sem_empty :
+  forall G (ctx: @Abstr.ctx G),
+    sem ctx empty (ctx_is ctx, None).
 Proof.
-  induction x; [admit|]; intros.
-  cbn -[update] in H.
-  pose proof H as Y.
-  apply OptionExtra.mfold_left_Some in Y. inv Y.
-  rewrite H3 in H.
-  destruct x0 as ((p_mid & f_mid) & l_mid).
-  exploit IHx; eauto. admit.
-  intros (ti_mid & Hseq & Hstate).
-
-Lemma abstr_seq_reverse_correct :
+  intros. destruct ctx. cbn. destruct ctx_is.
+  constructor.
+  constructor. cbn. intros. rewrite get_empty.
+  constructor. cbn. constructor. constructor. constructor. intros.
+  rewrite get_empty_p. constructor. constructor.
+  rewrite get_empty. constructor. cbn. constructor.
+  constructor. constructor. cbn. constructor. constructor.
+Qed.
+
+Lemma abstr_seq_reverse_correct:
   forall sp x i i' ti cf x' l,
     abstract_sequence' x = Some (x', l) ->
     (forall p, In p l -> exists r, sem_pred_expr x'.(forest_preds) sem_value (mk_ctx i sp ge) p r) ->
@@ -122,15 +219,13 @@ Proof.
 (*  intros. exploit sem_exists_execution; eauto; simplify.
   eauto using sem_equiv_execution.
 Qed. *)
-  induction x; [admit|].
-  intros. unfold abstract_sequence' in H. cbn -[update] in H.
+  intros. unfold abstract_sequence' in H.
   unfold Option.map in H. repeat destr. inv H.
-  pose proof Heqm as Y.
-  apply OptionExtra.mfold_left_Some in Y. inv Y.
-  rewrite H in Heqm. exploit IHx.
-  unfold abstract_sequence', Option.map.
-  destruct x0 as ((p' & f') & l').
-  unfold Option.bind2, Option.ret in H. repeat destr.
+  eapply  abstr_seq_reverse_correct_fold.
+  2: {  eauto. }
+  all: eauto.
+  apply sem_empty.
+Qed.
 
 (*|
 Proof Sketch:
diff --git a/src/hls/GiblePargenproofEquiv.v b/src/hls/GiblePargenproofEquiv.v
index da2b2c1..5f589a7 100644
--- a/src/hls/GiblePargenproofEquiv.v
+++ b/src/hls/GiblePargenproofEquiv.v
@@ -735,6 +735,29 @@ Section CORRECT.
     - apply negb_inj. apply sem_pred_det with (e:=p0); auto.
   Qed.
 
+  Lemma sem_pred_expr_det :
+    forall A B p b1 b2 f (s: forall G, @Abstr.ctx G -> A -> B -> Prop),
+      (forall p b1 b2, s _ ictx p b1 -> s _ octx p b2 -> b1 = b2) ->
+      sem_pred_expr f (s _) ictx p b1 -> sem_pred_expr f (s _) octx p b2 -> b1 = b2.
+  Proof.
+    induction p; crush.
+    - inv H0. inv H1. eauto.
+    - inv H0; inv H1; eauto; exploit sem_pexpr_det; eauto; discriminate.
+  Qed.
+
+  Lemma sem_det :
+    forall p i cf i' cf',
+      sem ictx p (i, cf) ->
+      sem octx p (i', cf') ->
+      cf = cf' /\ match_states i i'.
+  Proof.
+    repeat inversion 1; subst; split.
+    - eauto using sem_pred_expr_det, sem_exit_det.
+    - inv H11; inv H12; inv H2; inv H3;
+      constructor; intros;
+      eauto using sem_pexpr_det, sem_pred_expr_det, sem_value_det, sem_mem_det.
+  Qed.
+
   Lemma sem_pexpr_corr :
     forall p b, sem_pexpr ictx p b -> sem_pexpr octx p b.
   Proof.