Prepare work on evaluability of instructions

3 files changed, 133 insertions, 71 deletions

diff --git a/src/hls/Gible.v b/src/hls/Gible.v
index d04c78a..b7959be 100644
--- a/src/hls/Gible.v
+++ b/src/hls/Gible.v
@@ -265,18 +265,6 @@ Inductive eval_pred:
 | eval_pred_none:
   forall i i', eval_pred None i i' i'.
 
-Section RELABSTR.
-
-  Context {A B : Type} (ge : Genv.t A B).
-
-(*|
-.. index::
-   triple: semantics; RTLBlockInstr; instruction
-
-Step Instruction
-=============================
-|*)
-
 Definition truthyb (ps: predset) (p: option pred_op) :=
   match p with
   | None => true
@@ -313,6 +301,77 @@ Variant instr_falsy (ps: predset): instr -> Prop :=
       instr_falsy ps (RBexit (Some p) cf)
   .
 
+Inductive state_equiv : instr_state -> instr_state -> Prop :=
+| match_states_intro:
+  forall ps ps' rs rs' m m',
+    (forall x, rs !! x = rs' !! x) ->
+    (forall x, ps !! x = ps' !! x) ->
+    m = m' ->
+    state_equiv (mk_instr_state rs ps  m) (mk_instr_state rs' ps' m').
+
+Lemma state_equiv_refl x : state_equiv x x.
+Proof. destruct x; constructor; crush. Qed.
+
+Lemma state_equiv_commut x y : state_equiv x y -> state_equiv y x.
+Proof. inversion 1; constructor; crush. Qed.
+
+Lemma state_equiv_trans x y z :
+  state_equiv x y -> state_equiv y z -> state_equiv x z.
+Proof. repeat inversion 1; constructor; crush. Qed.
+
+#[global] Instance state_equiv_Equivalence : Equivalence state_equiv :=
+  { Equivalence_Reflexive := state_equiv_refl ;
+    Equivalence_Symmetric := state_equiv_commut ;
+    Equivalence_Transitive := state_equiv_trans ; }.
+
+Lemma match_states_list :
+  forall A (rs: Regmap.t A) rs',
+  (forall r, rs !! r = rs' !! r) ->
+  forall l, rs ## l = rs' ## l.
+Proof. induction l; crush. Qed.
+
+Lemma truthy_match_state :
+  forall ps ps' p,
+    (forall x, ps !! x = ps' !! x) ->
+    truthy ps p ->
+    truthy ps' p.
+Proof.
+  intros; destruct p; inv H0; constructor; auto.
+  erewrite eval_predf_pr_equiv; eauto.
+Qed.
+
+Lemma falsy_match_state :
+  forall ps ps' p,
+    (forall x, ps !! x = ps' !! x) ->
+    falsy ps p ->
+    falsy ps' p.
+Proof.
+  intros; destruct p; inv H0; constructor; auto.
+  erewrite eval_predf_pr_equiv; eauto.
+Qed.
+
+Lemma PTree_matches :
+  forall A (v: A) res rs rs',
+  (forall r, rs !! r = rs' !! r) ->
+  forall x, (Regmap.set res v rs) !! x = (Regmap.set res v rs') !! x.
+Proof.
+  intros; destruct (Pos.eq_dec x res); subst;
+  [ repeat rewrite Regmap.gss by auto
+  | repeat rewrite Regmap.gso by auto ]; auto.
+Qed.
+
+Section RELABSTR.
+
+  Context {A B : Type} (ge : Genv.t A B).
+
+(*|
+.. index::
+   triple: semantics; RTLBlockInstr; instruction
+
+Step Instruction
+=============================
+|*)
+
 Variant step_instr: val -> istate -> instr -> istate -> Prop :=
   | exec_RBnop:
     forall sp ist,
@@ -353,6 +412,34 @@ Variant step_instr: val -> istate -> instr -> istate -> Prop :=
       step_instr sp (Iexec st) i (Iexec st)
 .
 
+Lemma step_exists:
+  forall sp i instr i' ti,
+    step_instr sp (Iexec i) instr (Iexec i') ->
+    state_equiv i ti ->
+    exists ti',
+      step_instr sp (Iexec ti) instr (Iexec ti')
+      /\ state_equiv i' ti'.
+Proof.
+  inversion_clear 1; subst; intros.
+  - econstructor; split; eauto. constructor.
+  - destruct ti; cbn in *. inv H. econstructor. split.
+    econstructor. erewrite match_states_list; eauto.
+    eapply truthy_match_state; eauto. constructor; auto.
+    eapply PTree_matches; auto.
+  - inv H; cbn in *. eexists; split. econstructor.
+    erewrite match_states_list; eauto. eauto.
+    eapply truthy_match_state; eauto. constructor; auto.
+    eapply PTree_matches; auto.
+  - inv H; cbn in *. eexists; split. econstructor.
+    erewrite match_states_list; eauto. rewrite <- H6. eauto.
+    eapply truthy_match_state; eauto. constructor; auto.
+  - inv H. econstructor. split. econstructor. erewrite match_states_list; eauto.
+    eapply truthy_match_state; eauto. constructor; auto.
+    eapply PTree_matches; auto.
+  - inv H0; exists ti; split; auto;
+      repeat constructor; inv H; erewrite eval_predf_pr_equiv; eauto.
+Qed.
+
 End RELABSTR.
 
 (*|
diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v
index db0df19..b4442a8 100644
--- a/src/hls/GiblePargenproofBackward.v
+++ b/src/hls/GiblePargenproofBackward.v
@@ -31,6 +31,7 @@ Require Import vericert.hls.GiblePar.
 Require Import vericert.hls.Gible.
 Require Import vericert.hls.GiblePargenproofEquiv.
 Require Import vericert.hls.GiblePargenproofCommon.
+Require Import vericert.hls.GiblePargenproofForward.
 Require Import vericert.hls.GiblePargen.
 Require Import vericert.hls.Predicate.
 Require Import vericert.hls.Abstr.
@@ -130,9 +131,8 @@ Definition evaluable_pred_list {G} ctx pr l :=
 (*   unfold evaluable_pred_expr in H1. Admitted. *)
 
 Lemma evaluable_pred_expr_exists :
-  forall sp pr f i0 exit_p exit_p' f' i ti p op args dst,
-    (forall x, sem_pexpr (mk_ctx i0 sp ge) (get_forest_p' x f'.(forest_preds)) (pr !! x)) ->
-    eval_predf pr exit_p = true ->
+  forall sp f i0 exit_p exit_p' f' i ti p op args dst,
+    eval_predf (is_ps i) exit_p = true ->
     valid_mem (is_mem i0) (is_mem i) ->
     update (exit_p, f) (RBop p op args dst) = Some (exit_p', f') ->
     sem (mk_ctx i0 sp ge) f (i, None) ->
@@ -141,19 +141,22 @@ Lemma evaluable_pred_expr_exists :
     exists ti',
       step_instr ge sp (Iexec ti) (RBop p op args dst) (Iexec ti').
 Proof.
-  intros * HPRED HEVAL VALID_MEM **. cbn -[seq_app] in H. unfold Option.bind in H. destr. inv H.
-  destruct ti.
+  intros * HEVAL VALID_MEM **. cbn -[seq_app] in H. unfold Option.bind in H. destr. inv H.
+  assert (HPRED': sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps i))
+    by now inv H0.
+  inversion_clear HPRED' as [? ? ? HPRED].
+  destruct ti as [is_trs is_tps is_tm].
   unfold evaluable_pred_expr in H1. destruct H1 as (r & Heval).
   rewrite forest_reg_gss in Heval.
-  exploit sem_pred_expr_prune_predicated2; eauto; intros. cbn in HPRED.
-  pose proof (truthy_dec pr p) as YH. inversion_clear YH as [YH'|YH'].
-  - assert (eval_predf pr (dfltp p ∧ exit_p') = true).
+  exploit sem_pred_expr_prune_predicated2; eauto; intros.
+  pose proof (truthy_dec (is_ps i) p) as YH. inversion_clear YH as [YH'|YH'].
+  - assert (eval_predf (is_ps i) (dfltp p ∧ exit_p') = true).
     { pose proof (truthy_dflt _ _ YH'). rewrite eval_predf_Pand.
       rewrite H1. now rewrite HEVAL. }
     exploit sem_pred_expr_app_predicated2; eauto; intros.
     exploit sem_pred_expr_seq_app_val2; eauto; simplify.
     unfold pred_ret in *. inv H4. inv H12.
-    destruct i. exploit sem_merge_list; eauto; intros.
+    destruct i as [is_rs_1 is_ps_1 is_m_1]. exploit sem_merge_list; eauto; intros.
     instantiate (1 := args) in H4.
     eapply sem_pred_expr_ident2 in H4. simplify.
     exploit sem_pred_expr_ident_det. eapply H5. eapply H4.
@@ -164,18 +167,18 @@ Proof.
     + cbn in *. eapply eval_operation_valid_pointer. symmetry; eauto.
       unfold ctx_mem in H14. cbn in H14. erewrite <- match_states_list; eauto.
     + inv H0.
-      assert (sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f pr)
+      assert (sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps_1))
         by (now constructor).
       pose proof (sem_predset_det _ _ ltac:(reflexivity) _ _ _ H0 H17).
-      assert (truthy is_ps0 p).
+      assert (truthy is_ps_1 p).
       { eapply truthy_match_state; eassumption. }
       eapply truthy_match_state; eassumption.
   - inv YH'. cbn -[seq_app] in H.
-    assert (eval_predf pr (p0 ∧ exit_p') = false).
+    assert (eval_predf (is_ps i) (p0 ∧ exit_p') = false).
     { rewrite eval_predf_Pand. now rewrite H1. }
     eapply sem_pred_expr_app_predicated_false2 in H; eauto.
     eexists. eapply exec_RB_falsy. constructor. auto. cbn.
-    assert (sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f pr)
+    assert (sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps i))
         by (now constructor).
     inv H0. pose proof (sem_predset_det _ _ ltac:(reflexivity) _ _ _ H4 H8).
     inv H2.
@@ -302,6 +305,8 @@ Proof. Admitted.
 (* [[id:5e6486bb-fda2-4558-aed8-243a9698de85]] *)
 Lemma abstr_seq_reverse_correct_fold :
   forall sp instrs i0 i i' ti cf f' l p p' l' f,
+    valid_mem (is_mem i0) (is_mem i) ->
+    eval_predf (is_ps i) p = true ->
     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' ->
@@ -311,12 +316,12 @@ Lemma abstr_seq_reverse_correct_fold :
       SeqBB.step ge sp (Iexec ti) instrs (Iterm ti' cf)
       /\ state_lessdef i' ti'.
 Proof.
-  induction instrs; intros * Y3 Y Y0 Y1 Y2.
+  induction instrs; intros * YVALID YEVAL 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 |})
+    assert (X: similar {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |}
+                       {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |})
       by reflexivity.
-    now eapply sem_det in H; [| eapply Y1 | eapply Y3 ].
+    now eapply sem_det in X; [| exact Y1 | exact Y3 ].
   - cbn -[update] in Y.
     pose proof Y as YX.
     apply OptionExtra.mfold_left_Some in YX. inv YX.
@@ -330,18 +335,24 @@ Proof.
       by admit; destruct H as (pred & op & args & dst & EQ); subst a.
 
     exploit evaluable_pred_expr_exists; eauto.
+    
     (* I have the pred already from sem. *)
-    admit. admit. admit. intros [t step].
+    intros [ti_mid HSTEP].
     (* unfold evaluable_pred_list in Y0. *)
     (* instantiate (1 := forest_preds f'). *)
     (* eapply in_forest_evaluable; eauto. *)
     (* (* provable using evaluability in list *) intros [t step]. *)
 
-    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.
+    pose proof Y3 as YH.
+    pose proof HSTEP as YHSTEP.
+    pose proof Y2 as Y2SPLIT; inv Y2SPLIT.
+    eapply step_exists in YHSTEP.
+    2: { symmetry. econstructor; try eassumption; auto. }
+    inv YHSTEP. inv H1.
+    exploit sem_update_instr. auto. eauto. eauto. eauto. eauto. auto. intros.
+    exploit IHinstrs. 3: { eauto. } admit. admit. eauto. admit. eauto. symmetry.
+    instantiate (1:=ti_mid). admit. intros [ti' [YHH HLD]].
+    exists ti'; split; eauto. econstructor; eauto.
 Admitted.
 
 Lemma sem_empty :
diff --git a/src/hls/GiblePargenproofCommon.v b/src/hls/GiblePargenproofCommon.v
index 8d8e0a2..22b5978 100644
--- a/src/hls/GiblePargenproofCommon.v
+++ b/src/hls/GiblePargenproofCommon.v
@@ -221,44 +221,8 @@ Proof.
   unfold predicated_not_inP; intros. eapply H. econstructor. right; eauto.
 Qed.
 
-Lemma match_states_list :
-  forall A (rs: Regmap.t A) rs',
-  (forall r, rs !! r = rs' !! r) ->
-  forall l, rs ## l = rs' ## l.
-Proof. induction l; crush. Qed.
-
-Lemma PTree_matches :
-  forall A (v: A) res rs rs',
-  (forall r, rs !! r = rs' !! r) ->
-  forall x, (Regmap.set res v rs) !! x = (Regmap.set res v rs') !! x.
-Proof.
-  intros; destruct (Pos.eq_dec x res); subst;
-  [ repeat rewrite Regmap.gss by auto
-  | repeat rewrite Regmap.gso by auto ]; auto.
-Qed.
-
 Lemma truthy_dec:
   forall ps a, truthy ps a \/ falsy ps a.
 Proof.
   destruct a; try case_eq (eval_predf ps p); intuition (constructor; auto).
 Qed.
-
-Lemma truthy_match_state :
-  forall ps ps' p,
-    (forall x, ps !! x = ps' !! x) ->
-    truthy ps p ->
-    truthy ps' p.
-Proof.
-  intros; destruct p; inv H0; constructor; auto.
-  erewrite eval_predf_pr_equiv; eauto.
-Qed.
-
-Lemma falsy_match_state :
-  forall ps ps' p,
-    (forall x, ps !! x = ps' !! x) ->
-    falsy ps p ->
-    falsy ps' p.
-Proof.
-  intros; destruct p; inv H0; constructor; auto.
-  erewrite eval_predf_pr_equiv; eauto.
-Qed.