Split proof up into more files

1 files changed, 395 insertions, 0 deletions

diff --git a/src/hls/GiblePargenproofEvaluable.v b/src/hls/GiblePargenproofEvaluable.v
new file mode 100644
index 0000000..9013cd5
--- /dev/null
+++ b/src/hls/GiblePargenproofEvaluable.v
@@ -0,0 +1,395 @@
+Require Import compcert.backend.Registers.
+Require Import compcert.common.AST.
+Require Import compcert.common.Errors.
+Require Import compcert.common.Linking.
+Require Import compcert.common.Globalenvs.
+Require Import compcert.common.Memory.
+Require Import compcert.common.Values.
+Require Import compcert.lib.Maps.
+
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.GibleSeq.
+Require Import vericert.hls.GiblePar.
+Require Import vericert.hls.Gible.
+Require Import vericert.hls.GiblePargenproofEquiv.
+Require Import vericert.hls.GiblePargen.
+Require Import vericert.hls.Predicate.
+Require Import vericert.hls.Abstr.
+Require Import vericert.common.Monad.
+
+#[local] Open Scope positive.
+#[local] Open Scope forest.
+#[local] Open Scope pred_op.
+
+#[local] Opaque simplify.
+#[local] Opaque deep_simplify.
+
+
+Definition evaluable {A B C} (sem: ctx -> B -> C -> Prop) (ctx: @ctx A) p := exists b, sem ctx p b.
+
+Definition p_evaluable {A} := @evaluable A _ _ sem_pexpr.
+
+Definition evaluable_expr {A} := @evaluable A _ _ sem_pred.
+
+Definition all_evaluable {A B} (ctx: @ctx A) f_p (l: predicated B) :=
+  forall p y, NE.In (p, y) l -> p_evaluable ctx (from_pred_op f_p p).
+
+Definition all_evaluable2 {A B C} (ctx: @ctx A) (sem: Abstr.ctx -> B -> C -> Prop) (l: predicated B) :=
+  forall p y, NE.In (p, y) l -> evaluable sem ctx y.
+
+Definition pred_forest_evaluable {A} (ctx: @ctx A) (ps: PTree.t pred_pexpr) :=
+  forall i p, ps ! i = Some p -> p_evaluable ctx p.
+
+Definition forest_evaluable {A} (ctx: @ctx A) (f: forest) :=
+  pred_forest_evaluable ctx f.(forest_preds).
+
+Lemma all_evaluable_cons :
+  forall A B pr ctx b a,
+    all_evaluable ctx pr (NE.cons a b) ->
+    @all_evaluable A B ctx pr b.
+Proof.
+  unfold all_evaluable; intros.
+  enough (NE.In (p, y) (NE.cons a b)); eauto.
+  constructor; tauto.
+Qed.
+
+Lemma all_evaluable2_cons :
+  forall A B C sem ctx b a,
+    all_evaluable2 ctx sem (NE.cons a b) ->
+    @all_evaluable2 A B C ctx sem b.
+Proof.
+  unfold all_evaluable2; intros.
+  enough (NE.In (p, y) (NE.cons a b)); eauto.
+  constructor; tauto.
+Qed.
+
+Lemma all_evaluable_cons2 :
+  forall A B pr ctx b a p,
+    @all_evaluable A B ctx pr (NE.cons (p, a) b) ->
+    p_evaluable ctx (from_pred_op pr p).
+Proof.
+  unfold all_evaluable; intros.
+  eapply H. constructor; eauto.
+Qed.
+
+Lemma all_evaluable2_cons2 :
+  forall A B C sem ctx b a p,
+    @all_evaluable2 A B C ctx sem (NE.cons (p, a) b) ->
+    evaluable sem ctx a.
+Proof.
+  unfold all_evaluable; intros.
+  eapply H. constructor; eauto.
+Qed.
+
+Lemma all_evaluable_cons3 :
+  forall A B pr ctx b p a,
+    all_evaluable ctx pr b ->
+    p_evaluable ctx (from_pred_op pr p) ->
+    @all_evaluable A B ctx pr (NE.cons (p, a) b).
+Proof.
+  unfold all_evaluable; intros. inv H1. inv H3. inv H1. auto.
+  eauto.
+Qed.
+
+Lemma all_evaluable_singleton :
+  forall A B pr ctx b p,
+    @all_evaluable A B ctx pr (NE.singleton (p, b)) ->
+    p_evaluable ctx (from_pred_op pr p).
+Proof.
+  unfold all_evaluable; intros. eapply H. constructor.
+Qed.
+
+Lemma get_forest_p_evaluable :
+  forall A (ctx: @ctx A) f r,
+    forest_evaluable ctx f ->
+    p_evaluable ctx (f #p r).
+Proof.
+  intros. unfold "#p", get_forest_p'.
+  destruct_match. unfold forest_evaluable in *.
+  unfold pred_forest_evaluable in *. eauto.
+  unfold p_evaluable, evaluable. eexists.
+  constructor. constructor.
+Qed.
+
+Lemma set_forest_p_evaluable :
+  forall A (ctx: @ctx A) f r p,
+    forest_evaluable ctx f ->
+    p_evaluable ctx p ->
+    forest_evaluable ctx (f #p r <- p).
+Proof.
+  unfold forest_evaluable, pred_forest_evaluable; intros.
+  destruct (peq i r); subst.
+  - rewrite forest_pred_gss2 in H1. now inv H1.
+  - rewrite forest_pred_gso2 in H1 by auto; eauto.
+Qed.
+
+  Lemma evaluable_singleton :
+    forall A B ctx fp r,
+      @all_evaluable A B ctx fp (NE.singleton (T, r)).
+  Proof.
+    unfold all_evaluable, evaluable; intros.
+    inv H. simpl. exists true. constructor.
+  Qed.
+
+Lemma evaluable_negate :
+  forall G (ctx: @ctx G) p,
+    p_evaluable ctx p ->
+    p_evaluable ctx (¬ p).
+Proof.
+  unfold p_evaluable, evaluable in *; intros.
+  inv H. eapply sem_pexpr_negate in H0. econstructor; eauto.
+Qed.
+
+Lemma predicated_evaluable :
+  forall G (ctx: @ctx G) ps (p: pred_op),
+    pred_forest_evaluable ctx ps ->
+    p_evaluable ctx (from_pred_op ps p).
+Proof.
+  unfold pred_forest_evaluable; intros. induction p; intros; cbn.
+  - repeat destruct_match; subst; unfold get_forest_p'.
+    destruct_match. eapply H; eauto. econstructor. constructor. constructor.
+    eapply evaluable_negate.
+    destruct_match. eapply H; eauto. econstructor. constructor. constructor.
+  - repeat econstructor.
+  - repeat econstructor.
+  - inv IHp1. inv IHp2. econstructor. apply sem_pexpr_Pand; eauto.
+  - inv IHp1. inv IHp2. econstructor. apply sem_pexpr_Por; eauto.
+Qed.
+
+Lemma predicated_evaluable_all :
+  forall A G (ctx: @ctx G) ps (p: predicated A),
+    pred_forest_evaluable ctx ps ->
+    all_evaluable ctx ps p.
+Proof.
+  unfold all_evaluable; intros.
+  eapply predicated_evaluable. eauto.
+Qed.
+
+Lemma predicated_evaluable_all_list :
+  forall A G (ctx: @ctx G) ps (p: list (predicated A)),
+    pred_forest_evaluable ctx ps ->
+    Forall (all_evaluable ctx ps) p.
+Proof.
+  induction p.
+  - intros. constructor.
+  - intros. constructor; eauto. apply predicated_evaluable_all; auto.
+Qed.
+
+#[local] Hint Resolve evaluable_singleton : core.
+#[local] Hint Resolve predicated_evaluable : core.
+#[local] Hint Resolve predicated_evaluable_all : core.
+#[local] Hint Resolve predicated_evaluable_all_list : core.
+
+Lemma evaluable_and_true :
+  forall G (ctx: @ctx G) ps p,
+    p_evaluable ctx (from_pred_op ps p) ->
+    p_evaluable ctx (from_pred_op ps (p ∧ T)).
+Proof.
+  intros. unfold evaluable in *. inv H. exists (x && true). cbn.
+  apply sem_pexpr_Pand; auto. constructor.
+Qed.
+
+Lemma all_evaluable_predicated_map :
+  forall A B G (ctx: @ctx G) ps (f: A -> B) p,
+    all_evaluable ctx ps p ->
+    all_evaluable ctx ps (predicated_map f p).
+Proof.
+  induction p.
+  - unfold all_evaluable; intros.
+    exploit NEin_map; eauto; intros. inv H1. inv H2.
+    eapply H; eauto.
+  - intros. cbn.
+    eapply all_evaluable_cons3. eapply IHp. eapply all_evaluable_cons; eauto.
+    cbn. destruct a. cbn in *. eapply all_evaluable_cons2; eauto.
+Qed.
+
+Lemma all_evaluable_predicated_map2 :
+  forall A B G (ctx: @ctx G) ps (f: A -> B) p,
+    all_evaluable ctx ps (predicated_map f p) ->
+    all_evaluable ctx ps p.
+Proof.
+  induction p.
+  - unfold all_evaluable in *; intros.
+    eapply H. eapply NEin_map2; eauto.
+  - intros. cbn. destruct a.
+    cbn in H. pose proof H. eapply all_evaluable_cons in H; eauto.
+    eapply all_evaluable_cons2 in H0; eauto.
+    unfold all_evaluable. specialize (IHp H).
+    unfold all_evaluable in IHp.
+    intros. inv H1. inv H3. inv H1; eauto.
+    specialize (IHp _ _ H1). eauto.
+Qed.
+
+Lemma all_evaluable_map_and :
+  forall A B G (ctx: @ctx G) ps (a: NE.non_empty ((pred_op * A) * (pred_op * B))),
+    (forall p1 x p2 y,
+       NE.In ((p1, x), (p2, y)) a ->
+            p_evaluable ctx (from_pred_op ps p1)
+            /\ p_evaluable ctx (from_pred_op ps p2)) ->
+    all_evaluable ctx ps (NE.map (fun x => match x with ((a, b), (c, d)) => (Pand a c, (b, d)) end) a).
+Proof.
+  induction a.
+  - intros. cbn. repeat destruct_match. inv Heqp.
+    unfold all_evaluable; intros. inv H0.
+    unfold evaluable.
+    exploit H. constructor.
+    intros [Ha Hb]. inv Ha. inv Hb.
+    exists (x && x0). apply sem_pexpr_Pand; auto.
+  - intros. unfold all_evaluable; cbn; intros. inv H0. inv H2.
+    + repeat destruct_match. inv Heqp0. inv H0.
+      specialize (H p2 a1 p3 b ltac:(constructor; eauto)).
+      inv H. inv H0. inv H1. exists (x && x0).
+      apply sem_pexpr_Pand; eauto.
+    + eapply IHa; intros. eapply H. econstructor. right. eauto.
+      eauto.
+Qed.
+
+Lemma all_evaluable_map_add :
+  forall A B G (ctx: @ctx G) ps (a: pred_op * A) (b: predicated B) p1 x p2 y,
+    p_evaluable ctx (from_pred_op ps (fst a)) ->
+    all_evaluable ctx ps b ->
+    NE.In (p1, x, (p2, y)) (NE.map (fun x : pred_op * B => (a, x)) b) ->
+    p_evaluable ctx (from_pred_op ps p1) /\ p_evaluable ctx (from_pred_op ps p2).
+Proof.
+  induction b; intros.
+  - cbn in *. inv H1. unfold all_evaluable in *. specialize (H0 _ _ ltac:(constructor)).
+    auto.
+  - cbn in *. inv H1. inv H3.
+    + inv H1. unfold all_evaluable in H0. specialize (H0 _ _ ltac:(constructor; eauto)); auto.
+    + eapply all_evaluable_cons in H0. specialize (IHb _ _ _ _ H H0 H1). auto.
+Qed.
+
+Lemma all_evaluable_non_empty_prod :
+  forall A B G (ctx: @ctx G) ps p1 x p2 y (a: predicated A) (b: predicated B),
+    all_evaluable ctx ps a ->
+    all_evaluable ctx ps b ->
+    NE.In ((p1, x), (p2, y)) (NE.non_empty_prod a b) ->
+    p_evaluable ctx (from_pred_op ps p1)
+    /\ p_evaluable ctx (from_pred_op ps p2).
+Proof.
+  induction a; intros.
+  - cbn in *. eapply all_evaluable_map_add; eauto. destruct a; cbn in *. eapply H; constructor.
+  - cbn in *. eapply NE.NEin_NEapp5 in H1. inv H1. eapply all_evaluable_map_add; eauto.
+    destruct a; cbn in *. eapply all_evaluable_cons2; eauto.
+    eapply all_evaluable_cons in H. eauto.
+Qed.
+
+Lemma all_evaluable_predicated_prod :
+  forall A B G (ctx: @ctx G) ps (a: predicated A) (b: predicated B),
+    all_evaluable ctx ps a ->
+    all_evaluable ctx ps b ->
+    all_evaluable ctx ps (predicated_prod a b).
+Proof.
+  intros. unfold all_evaluable; intros.
+  unfold predicated_prod in *. exploit all_evaluable_map_and.
+  2: { eauto. }
+  intros. 2: { eauto. }
+Admitted. (* Requires simple lemma to prove, but this lemma is not needed. *)
+
+Lemma cons_pred_expr_evaluable :
+  forall G (ctx: @ctx G) ps a b,
+    all_evaluable ctx ps a ->
+    all_evaluable ctx ps b ->
+    all_evaluable ctx ps (cons_pred_expr a b).
+Proof.
+  unfold cons_pred_expr; intros.
+  apply all_evaluable_predicated_map.
+  now apply all_evaluable_predicated_prod.
+Qed.
+
+Lemma fold_right_all_evaluable :
+  forall G (ctx: @ctx G) ps n,
+    Forall (all_evaluable ctx ps) (NE.to_list n) ->
+    all_evaluable ctx ps (NE.fold_right cons_pred_expr (NE.singleton (T, Enil)) n).
+Proof.
+  induction n; cbn in *; intros.
+  - unfold cons_pred_expr. eapply all_evaluable_predicated_map. eapply all_evaluable_predicated_prod.
+    inv H. auto. unfold all_evaluable; intros. inv H0. exists true. constructor.
+  - inv H. specialize (IHn H3). now eapply cons_pred_expr_evaluable.
+Qed.
+
+Lemma merge_all_evaluable :
+  forall G (ctx: @ctx G) ps,
+    pred_forest_evaluable ctx ps ->
+    forall f args,
+      all_evaluable ctx ps (merge (list_translation args f)).
+Proof.
+  intros. eapply predicated_evaluable_all. eauto.
+Qed.
+
+  Lemma forest_evaluable_regset :
+    forall A f (ctx: @ctx A) n x,
+      forest_evaluable ctx f ->
+      forest_evaluable ctx f #r x <- n.
+  Proof.
+    unfold forest_evaluable, pred_forest_evaluable; intros.
+    eapply H. eauto.
+  Qed.
+
+  Lemma evaluable_impl :
+    forall A (ctx: @ctx A) a b,
+      p_evaluable ctx a ->
+      p_evaluable ctx b ->
+      p_evaluable ctx (a → b).
+  Proof.
+    unfold evaluable.
+    inversion_clear 1 as [b1 SEM1].
+    inversion_clear 1 as [b2 SEM2].
+    unfold Pimplies.
+    econstructor. apply sem_pexpr_Por;
+    eauto using sem_pexpr_negate.
+  Qed.
+
+  Lemma parts_evaluable :
+    forall A (ctx: @ctx A) b p0,
+      evaluable sem_pred ctx p0 ->
+      evaluable sem_pexpr ctx (Plit (b, p0)).
+  Proof.
+    intros. unfold evaluable in *. inv H.
+    destruct b. do 2 econstructor. eauto.
+    exists (negb x). constructor. rewrite negb_involutive. auto.
+  Qed.
+
+  Lemma p_evaluable_Pand :
+    forall A (ctx: @ctx A) a b,
+      p_evaluable ctx a ->
+      p_evaluable ctx b ->
+      p_evaluable ctx (a ∧ b).
+  Proof.
+    intros. inv H. inv H0.
+    econstructor. apply sem_pexpr_Pand; eauto.
+  Qed.
+
+  Lemma from_predicated_evaluable :
+    forall A (ctx: @ctx A) f b a,
+      pred_forest_evaluable ctx f ->
+      all_evaluable2 ctx sem_pred a ->
+      p_evaluable ctx (from_predicated b f a).
+  Proof.
+    induction a.
+    cbn. destruct_match; intros.
+    eapply evaluable_impl.
+    eauto using predicated_evaluable.
+    unfold all_evaluable2 in H0. unfold p_evaluable.
+    eapply parts_evaluable. eapply H0. econstructor.
+
+    intros. cbn. destruct_match.
+    eapply p_evaluable_Pand.
+    eapply all_evaluable2_cons2 in H0.
+    eapply evaluable_impl.
+    eauto using predicated_evaluable.
+    unfold all_evaluable2 in H0. unfold p_evaluable.
+    eapply parts_evaluable. eapply H0.
+    eapply all_evaluable2_cons in H0. eauto.
+  Qed.
+
+  Lemma p_evaluable_imp :
+    forall A (ctx: @ctx A) a b,
+      sem_pexpr ctx a false ->
+      p_evaluable ctx (a → b).
+  Proof.
+    intros. unfold "→".
+    unfold p_evaluable, evaluable. exists true.
+    constructor. replace true with (negb false) by trivial. left.
+    now apply sem_pexpr_negate.
+  Qed.