Work towards proving evaluability

3 files changed, 169 insertions, 38 deletions

diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v
index 8e8c9b5..4b95cf2 100644
--- a/src/hls/GiblePargen.v
+++ b/src/hls/GiblePargen.v
@@ -289,11 +289,11 @@ Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest
       Some (new_p, f <-e pruned)
   end.
 
-Definition remember_expr (f : forest) (lst: list pred_expr) (i : instr): list pred_expr :=
+Definition remember_expr (f : forest) (lst: list (resource * pred_expr)) (i : instr): list (resource * pred_expr) :=
   match i with
   | RBnop => lst
-  | RBop p op rl r => (f #r (Reg r)) :: lst
-  | RBload  p chunk addr rl r => (f #r (Reg r)) :: lst
+  | RBop p op rl r => (Reg r, f #r (Reg r)) :: lst
+  | RBload  p chunk addr rl r => (Reg r, f #r (Reg r)) :: lst
   | RBstore p chunk addr rl r => lst
   | RBsetpred p' c args p => lst
   | RBexit p c => lst
@@ -309,6 +309,11 @@ Definition remember_expr_m (f : forest) (lst: list pred_expr) (i : instr): list
   | RBexit p c => lst
   end.
 
+(*|
+Not actually needed, because there is a better way to show that a predicate is
+evaluable.
+|*)
+
 Definition remember_expr_p (f : forest) (lst: list pred_op) (i : instr): list pred_op :=
   match i with
   | RBnop => lst
@@ -319,11 +324,11 @@ Definition remember_expr_p (f : forest) (lst: list pred_op) (i : instr): list pr
   | RBexit p c => lst
   end.
 
-Definition update' (s: pred_op * forest * list pred_expr * list pred_expr) (i: instr): option (pred_op * forest * list pred_expr * list pred_expr) :=
+Definition update_top (s: pred_op * forest * list (resource * pred_expr) * list pred_expr) (i: instr): option (pred_op * forest * list (resource * pred_expr) * list pred_expr) :=
   let '(p, f, l, lm) := s in
   Option.bind2 (fun p' f' => Option.ret (p', f', remember_expr f l i, remember_expr_m f lm i)) (update (p, f) i).
 
-Definition update'' (s: pred_op * forest * list pred_expr * list pred_expr * list pred_op) (i: instr): option (pred_op * forest * list pred_expr * list pred_expr * list pred_op) :=
+Definition update'' (s: pred_op * forest * list (resource * pred_expr) * list pred_expr * list pred_op) (i: instr): option (pred_op * forest * list (resource * pred_expr) * list pred_expr * list pred_op) :=
   let '(p, f, l, lm, lp) := s in
   Option.bind2 (fun p' f' => Option.ret (p', f', remember_expr f l i, remember_expr_m f lm i, remember_expr_p f lp i)) (update (p, f) i).
 
@@ -347,11 +352,11 @@ Definition gather_predicates (preds : PTree.t unit) (i : instr): option (PTree.t
   | _ => Some preds
   end.
 
-Definition abstract_sequence' (b : list instr) : option (forest * list pred_expr * list pred_expr) :=
+Definition abstract_sequence_top (b : list instr) : option (forest * list (resource * pred_expr) * list pred_expr) :=
   Option.bind (fun x => Option.bind (fun _ => Some x)
     (mfold_left gather_predicates b (Some (PTree.empty _))))
       (Option.map (fun x => let '(_, y, z, zm) := x in (y, z, zm))
-        (mfold_left update' b (Some (Ptrue, empty, nil, nil)))).
+        (mfold_left update_top b (Some (Ptrue, empty, nil, nil)))).
 
 (*Compute match update (T, mk_forest (PTree.empty _) (PTree.empty _) (NE.singleton (T, EEbase)))
   (RBop None Op.Odiv (1::2::nil) 3) with
@@ -404,10 +409,23 @@ Definition empty_trees (bb: SeqBB.t) (bbt: ParBB.t) : bool :=
   | _ => true
   end.
 
+Definition check_evaluability1 a b :=
+  forallb (fun be =>
+    existsb (fun ae =>
+      resource_eq (fst ae) (fst be) 
+      && HN.beq_pred_expr (snd ae) (snd be)
+    ) a
+  ) b.
+
+Definition check_evaluability2 a b :=
+  forallb (fun be => existsb (fun ae => HN.beq_pred_expr ae be) a) b.
+
 Definition schedule_oracle (bb: SeqBB.t) (bbt: ParBB.t) : bool :=
-  match abstract_sequence bb, abstract_sequence (concat (concat bbt)) with
-  | Some bb', Some bbt' =>
+  match abstract_sequence_top bb, abstract_sequence_top (concat (concat bbt)) with
+  | Some (bb', reg_expr, m_expr), Some (bbt', reg_expr_t, m_expr_t) =>
       check bb' bbt' && empty_trees bb bbt
+      && check_evaluability1 reg_expr reg_expr_t
+      && check_evaluability2 m_expr m_expr_t
   | _, _ => false
   end.
 
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v
index a27edd5..d956fcb 100644
--- a/src/hls/GiblePargenproof.v
+++ b/src/hls/GiblePargenproof.v
@@ -48,6 +48,91 @@ Module Import OptionExtra := MonadExtra(Option).
 
 Ltac destr := destruct_match; try discriminate; [].
 
+Lemma equiv_update_top:
+  forall i p f l lm p' f' l' lm',
+    update_top (p, f, l, lm) i = Some (p', f', l', lm') ->
+    update (p, f) i = Some (p', f').
+Proof.
+  intros. unfold update_top, Option.bind2, Option.ret in *. repeat destr.
+  inv Heqp1. now inv H.
+Qed.
+
+Lemma remember_expr_eq :
+  forall l i f,
+    remember_expr f (map snd l) i = map snd (GiblePargen.remember_expr f l i).
+Proof.
+  induction l; destruct i; auto.
+Qed.
+
+Lemma equiv_update'_top:
+  forall i p f l lm p' f' l' lm',
+    update_top (p, f, l, lm) i = Some (p', f', l', lm') ->
+    update' (p, f, map snd l, lm) i = Some (p', f', map snd l', lm').
+Proof.
+  intros. unfold update', update_top, Option.bind2, Option.ret in *. repeat destr.
+  inv Heqp1. inv H. repeat f_equal. apply remember_expr_eq.
+Qed.
+
+Lemma equiv_fold_update'_top:
+  forall i p f l lm p' f' l' lm',
+    mfold_left update_top i (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
+    mfold_left update' i (Some (p, f, map snd l, lm)) = Some (p', f', map snd l', lm').
+Proof.
+  induction i; cbn -[update_top update'] in *; intros.
+  - inv H; auto.
+  - exploit OptionExtra.mfold_left_Some; eauto;
+      intros [[[[p_mid f_mid] l_mid] lm_mid] HB].
+    exploit equiv_update'_top; try eassumption.
+    intros. rewrite H0. eapply IHi. rewrite HB in H. eauto.
+Qed.
+
+Lemma equiv_fold_update_top:
+  forall i p f l lm p' f' l' lm',
+    mfold_left update_top i (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
+    mfold_left update i (Some (p, f)) = Some (p', f').
+Proof.
+  induction i; cbn -[update_top update] in *; intros.
+  - inv H; auto.
+  - exploit OptionExtra.mfold_left_Some; eauto;
+      intros [[[[p_mid f_mid] l_mid] lm_mid] HB].
+    exploit equiv_update_top; try eassumption.
+    intros. rewrite H0. eapply IHi. rewrite HB in H. eauto.
+Qed.
+
+Lemma spec_abstract_sequence_top :
+  mfold_left
+  fun (s : pred_op * forest * list pred_expr * list pred_expr) (i : instr) =>
+    let
+    '(p, f, l, lm) := s in
+     Option.bind2 (fun (p' : pred_op) (f' : forest) => Option.ret (p', f', , remember_expr_m f lm i))
+       (update (p, f) i)
+         : pred_op * forest * list pred_expr * list pred_expr -> instr -> option (pred_op * forest * list pred_expr * list pred_expr).
+
+Lemma top_implies_abstract_sequence :
+  forall y f l1 l2,
+    abstract_sequence_top y = Some (f, l1, l2) ->
+    abstract_sequence y = Some f.
+Proof.
+  unfold abstract_sequence, abstract_sequence_top; intros.
+  unfold Option.bind in *. repeat destr.
+  inv H.
+  unfold Option.map in *|-. repeat destr. subst. inv Heqo.
+  erewrite equiv_fold_update_top by eauto. auto.
+Qed.
+
+Lemma top_implies_abstract_sequence' :
+  forall y f l1 l2,
+    abstract_sequence_top y = Some (f, l1, l2) ->
+    abstract_sequence' y = Some (f, map snd l1, l2).
+Proof.
+  unfold abstract_sequence', abstract_sequence_top; intros.
+  unfold Option.bind in *|-. repeat destr.
+  inv H.
+  unfold Option.map in *|-. repeat destr. subst. inv Heqo.
+  exploit equiv_fold_update'_top; eauto; intros.
+  setoid_rewrite H. cbn. setoid_rewrite Heqm. auto.
+Qed.
+
 Definition state_lessdef := GiblePargenproofEquiv.match_states.
 
 Definition match_prog (prog : GibleSeq.program) (tprog : GiblePar.program) :=
@@ -415,6 +500,31 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
     eapply IHx; eauto.
   Qed.
 
+  Lemma abstract_sequence_evaluable :
+    forall sp x i i' cf f l0 l,
+      SeqBB.step ge sp (Iexec i) x (Iterm i' cf) ->
+      abstract_sequence_top x = Some (f, l0, l) ->
+      evaluable_pred_list (mk_ctx i sp ge) f.(forest_preds) (map snd l0).
+  Proof.
+    induction x; cbn; intros.
+    - inv H0. inv H.
+    - exploit top_implies_abstract_sequence; eauto; intros. inv H. inv H7; eauto.
+      + unfold abstract_sequence_top, Option.bind, Option.map in *.
+        repeat destr; subst. inv H0. inv Heqo.
+        unfold evaluable_pred_list; intros.
+        unfold evaluable_pred_expr.
+        exploit OptionExtra.mfold_left_Some. eapply Heqm1.
+        intros [[[[p_mid f_mid] l_mid] lm_mid] HB]. inv HB.
+
+  Lemma abstract_sequence_evaluable_m :
+    forall sp x i i' cf f l0 l,
+      SeqBB.step ge sp (Iexec i) x (Iterm i' cf) ->
+      abstract_sequence_top x = Some (f, l0, l) ->
+      evaluable_pred_list_m (mk_ctx i sp ge) f.(forest_preds) l.
+  Proof. Admitted.
+
+(* abstract_sequence_top x = Some (f, l0, l) -> *)
+
   Lemma schedule_oracle_correct :
     forall x y sp i i' ti cf,
       schedule_oracle x y = true ->
@@ -424,12 +534,15 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
              /\ state_lessdef i' ti'.
   Proof.
     unfold schedule_oracle; intros. repeat (destruct_match; try discriminate). simplify.
+    exploit top_implies_abstract_sequence; [eapply Heqo|]; intros.
+    exploit top_implies_abstract_sequence'; eauto; intros.
     exploit abstr_sequence_correct; eauto; simplify.
     exploit local_abstr_check_correct2; eauto.
     { constructor. eapply ge_preserved_refl. reflexivity. }
 (*    { inv H. inv H8. exists pr'. intros x0. specialize (H x0). auto. } *)
     simplify.
-    exploit abstr_seq_reverse_correct; eauto. admit. admit. admit. admit. reflexivity. simplify.
+    exploit abstr_seq_reverse_correct; eauto.
+    admit. reflexivity. simplify.
     exploit seqbb_step_parbb_step; eauto; intros.
     econstructor; split; eauto.
     etransitivity; eauto.
diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v
index 815f005..af9f3b4 100644
--- a/src/hls/GiblePargenproofBackward.v
+++ b/src/hls/GiblePargenproofBackward.v
@@ -66,6 +66,26 @@ the translation goes from GiblePar to Abstr, whereas the correctness proof is
 needed from Abstr to GiblePar to get the proper direction of the proof.
 |*)
 
+Definition remember_expr (f : forest) (lst: list pred_expr) (i : instr): list pred_expr :=
+  match i with
+  | RBnop => lst
+  | RBop p op rl r => (f #r (Reg r)) :: lst
+  | RBload  p chunk addr rl r => (f #r (Reg r)) :: lst
+  | RBstore p chunk addr rl r => lst
+  | RBsetpred p' c args p => lst
+  | RBexit p c => lst
+  end.
+
+Definition update' (s: pred_op * forest * list pred_expr * list pred_expr) (i: instr): option (pred_op * forest * list pred_expr * list pred_expr) :=
+  let '(p, f, l, lm) := s in
+  Option.bind2 (fun p' f' => Option.ret (p', f', remember_expr f l i, remember_expr_m f lm i)) (update (p, f) i).
+
+Definition abstract_sequence' (b : list instr) : option (forest * list pred_expr * list pred_expr) :=
+  Option.bind (fun x => Option.bind (fun _ => Some x)
+    (mfold_left gather_predicates b (Some (PTree.empty _))))
+      (Option.map (fun x => let '(_, y, z, zm) := x in (y, z, zm))
+        (mfold_left update' b (Some (Ptrue, empty, nil, nil)))).
+
 Section CORRECTNESS.
 
 Context (prog: GibleSeq.program) (tprog : GiblePar.program).
@@ -86,15 +106,6 @@ Proof.
     eapply IHi; eauto.
 Qed.
 
-Lemma equiv_update1':
-  forall i p f l lm p' f' l' lm' lp lp',
-    update'' (p, f, l, lm, lp) i = Some (p', f', l', lm', lp') ->
-    update' (p, f, l, lm) i = Some (p', f', l', lm').
-Proof.
-  intros. unfold update', update'', Option.bind2, Option.ret in *. repeat destr.
-  inv Heqp1. now inv H.
-Qed.
-
 Lemma equiv_update1:
   forall i p f l lm p' f' l' lm',
     update' (p, f, l, lm) i = Some (p', f', l', lm') ->
@@ -113,24 +124,13 @@ Proof.
   inv Heqp1. now inv H.
 Qed.
 
-Lemma equiv_update':
-  forall i p f l lm p' f' l' lm' lp lp',
-    mfold_left update'' i (Some (p, f, l, lm, lp)) = Some (p', f', l', lm', lp') ->
-    mfold_left update' i (Some (p, f, l, lm)) = Some (p', f', l', lm').
-Proof.
-  induction i; cbn -[update'' update'] in *; intros.
-  - inv H; auto.
-  - exploit OptionExtra.mfold_left_Some; eauto;
-      intros [[[[[p_mid f_mid] l_mid] lm_mid] lp_mid] HB].
-    exploit equiv_update1'; try eassumption.
-    intros. rewrite H0. eapply IHi. rewrite HB in H. eauto.
-Qed.
 
-Lemma equiv_update'':
-  forall i p f l lm p' f' l' lm' lp lp',
-    mfold_left update'' i (Some (p, f, l, lm, lp)) = Some (p', f', l', lm', lp') ->
-    mfold_left update i (Some (p, f)) = Some (p', f').
-Proof. eauto using equiv_update', equiv_update. Qed.
+
+(* Lemma equiv_update'': *)
+(*   forall i p f l lm p' f' l' lm' lp lp', *)
+(*     mfold_left update'' i (Some (p, f, l, lm, lp)) = Some (p', f', l', lm', lp') -> *)
+(*     mfold_left update i (Some (p, f)) = Some (p', f'). *)
+(* Proof. eauto using equiv_update', equiv_update. Qed. *)
 
 Definition i_state (s: istate): instr_state :=
   match s with
@@ -1818,11 +1818,10 @@ Proof.
 Qed.
 
 Lemma abstr_seq_reverse_correct:
-  forall sp x i i' ti cf x' l lm ps',
+  forall sp x i i' ti cf x' l lm,
     abstract_sequence' x = Some (x', l, lm) ->
     evaluable_pred_list (mk_ctx i sp ge) x'.(forest_preds) l ->
     evaluable_pred_list_m (mk_ctx i sp ge) x'.(forest_preds) lm ->
-    sem_predset {| ctx_is := i; ctx_sp := sp; ctx_ge := ge |} x' ps' ->
     sem (mk_ctx i sp ge) x' (i', (Some cf)) ->
     state_lessdef i ti ->
    exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf)
@@ -1830,6 +1829,7 @@ Lemma abstr_seq_reverse_correct:
 Proof.
   intros. unfold abstract_sequence' in H.
   unfold Option.map, Option.bind in H. repeat destr. inv H. inv Heqo.
+  pose proof H2 as X. inv X.
   eapply abstr_seq_reverse_correct_fold;
     try eassumption; try reflexivity; auto using sem_empty, all_preds_in_empty.
   inversion 1.