Finish sem_update_instr finally

4 files changed, 352 insertions, 3 deletions

diff --git a/src/hls/Gible.v b/src/hls/Gible.v
index 0603269..cc35640 100644
--- a/src/hls/Gible.v
+++ b/src/hls/Gible.v
@@ -158,6 +158,20 @@ Definition predset := PMap.t bool.
 Definition eval_predf (pr: predset) (p: pred_op) :=
   sat_predicate p (fun x => pr !! (Pos.of_nat x)).
 
+Lemma sat_pred_agree0 :
+  forall a b p,
+    (forall x, x <> 0%nat -> a x = b x) ->
+    sat_predicate p a = sat_predicate p b.
+Proof.
+  induction p; auto; intros.
+  - destruct p. cbn. assert (Pos.to_nat p <> 0%nat) by lia.
+    apply H in H0. now rewrite H0.
+  - specialize (IHp1 H). specialize (IHp2 H).
+    cbn. rewrite IHp1. rewrite IHp2. auto.
+  - specialize (IHp1 H). specialize (IHp2 H).
+    cbn. rewrite IHp1. rewrite IHp2. auto.
+Qed.
+
 #[global]
  Instance eval_predf_Proper : Proper (eq ==> equiv ==> eq) eval_predf.
 Proof.
@@ -190,6 +204,26 @@ Proof.
     erewrite IHp1; try eassumption; erewrite IHp2; eauto.
 Qed.
 
+Lemma eval_predf_not_PredIn :
+  forall ps p b op,
+    ~ PredIn p op ->
+    eval_predf (ps # p <- b) op = eval_predf ps op.
+Proof.
+  induction op; auto.
+  - intros. destruct p0. cbn. rewrite Pos2Nat.id.
+    destruct (peq p p0); subst.
+      { exfalso; apply H; constructor. }
+    rewrite Regmap.gso; auto.
+  - intros. cbn. unfold eval_predf in *. rewrite IHop1.
+    rewrite IHop2. auto.
+    unfold not; intros; apply H; constructor; tauto.
+    unfold not; intros; apply H; constructor; tauto.
+  - intros. cbn. unfold eval_predf in *. rewrite IHop1.
+    rewrite IHop2. auto.
+    unfold not; intros; apply H; constructor; tauto.
+    unfold not; intros; apply H; constructor; tauto.
+Qed.
+
 Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
   match rl, vl with
   | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs)
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v
index 4d36180..dcfad5d 100644
--- a/src/hls/GiblePargen.v
+++ b/src/hls/GiblePargen.v
@@ -183,6 +183,23 @@ Definition is_initial_pred_and_notin (f: forest) (p: positive) (p_next: pred_op)
   | _ => false
   end.
 
+Definition predicated_not_in {A} (p: Gible.predicate) (l: predicated A): bool :=
+  NE.fold_right (fun (a: pred_op * A) (b: bool) =>
+    b && negb (predin peq p (fst a))
+  ) true l.
+
+Definition predicated_not_in_pred_expr (p: Gible.predicate) (tree: RTree.t pred_expr) :=
+  PTree.fold (fun b _ a =>
+    b && predicated_not_in p a
+  ) tree true.
+
+Definition predicated_not_in_pred_eexpr (p: Gible.predicate) (l: pred_eexpr) :=
+  predicated_not_in p l.
+
+Definition predicated_not_in_forest (p: Gible.predicate) (f: forest) :=
+  predicated_not_in_pred_expr p f.(forest_regs)
+  && predicated_not_in p f.(forest_exit).
+
 Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest) :=
   let (pred, f) := fop in
   match i with
@@ -220,7 +237,9 @@ Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest
         (from_pred_op f.(forest_preds) (dfltp p' ∧ pred)
            → from_predicated true f.(forest_preds) (seq_app (pred_ret (PEsetpred c))
                                                   (merge (list_translation args f))))
+        ∧ (from_pred_op f.(forest_preds) (¬ (dfltp p') ∨ ¬ pred) → (f #p p))
       in
+      do _ <- assert_ (predicated_not_in_forest p f);
       do _ <- assert_ (is_initial_pred_and_notin f p pred);
       Some (pred, f #p p <- new_pred)
   | RBexit p c =>
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v
index 0eab247..7667ac2 100644
--- a/src/hls/GiblePargenproof.v
+++ b/src/hls/GiblePargenproof.v
@@ -793,6 +793,14 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
     eapply sem_pred_expr_map_Pand; eauto.
   Qed.
 
+  Lemma sem_pred_expr_app_predicated_false :
+    forall A B C sem ctx f_p y x v p ps,
+      sem_pred_expr f_p sem ctx y v ->
+      (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) ->
+      eval_predf ps p = false ->
+      @sem_pred_expr A B C f_p sem ctx (app_predicated p y x) v.
+  Admitted.
+
   Lemma sem_pred_expr_prune_predicated :
     forall A B C sem ctx f_p y x v,
       sem_pred_expr f_p sem ctx x v ->
@@ -1770,6 +1778,242 @@ all be evaluable.
     + auto.
   Qed.
 
+  Definition predicated_not_inP {A} (p: Gible.predicate) (l: predicated A) :=
+    forall op e, NE.In (op, e) l -> ~ PredIn p op.
+
+  Lemma predicated_not_inP_cons :
+    forall A p (a: (pred_op * A)) l,
+      predicated_not_inP p (NE.cons a l) ->
+      predicated_not_inP p l.
+  Proof.
+    unfold predicated_not_inP; intros. eapply H. econstructor. right; eauto.
+  Qed.
+
+  Lemma sem_pexpr_not_in :
+    forall G (ctx: @ctx G) p0 ps p e b,
+      ~ PredIn p p0 ->
+      sem_pexpr ctx (from_pred_op ps p0) b ->
+      sem_pexpr ctx (from_pred_op (PTree.set p e ps) p0) b.
+  Proof.
+    induction p0; auto; intros.
+    - cbn. destruct p. unfold get_forest_p'.
+      assert (p0 <> p) by
+        (unfold not; intros; apply H; subst; constructor).
+      rewrite PTree.gso; auto.
+    - cbn in *.
+      assert (X: ~ PredIn p p0_1 /\ ~ PredIn p p0_2) by
+        (split; unfold not; intros; apply H; constructor; tauto).
+      inversion_clear X as [X1 X2].
+      inv H0. inv H4.
+      specialize (IHp0_1 _ p e _ X1 H0). constructor. tauto.
+      specialize (IHp0_2 _ p e _ X2 H0). constructor. tauto.
+      constructor; auto.
+    - cbn in *.
+      assert (X: ~ PredIn p p0_1 /\ ~ PredIn p p0_2) by
+        (split; unfold not; intros; apply H; constructor; tauto).
+      inversion_clear X as [X1 X2].
+      inv H0. inv H4.
+      specialize (IHp0_1 _ p e _ X1 H0). constructor. tauto.
+      specialize (IHp0_2 _ p e _ X2 H0). constructor. tauto.
+      constructor; auto.
+  Qed.
+
+  Lemma sem_pred_not_in :
+    forall A B G (ctx: @ctx G) (s: @Abstr.ctx G -> A -> B -> Prop) l v p e ps,
+      sem_pred_expr ps s ctx l v ->
+      predicated_not_inP p l ->
+      sem_pred_expr (PTree.set p e ps) s ctx l v.
+  Proof.
+    induction l.
+    - intros. unfold predicated_not_inP in H0.
+      destruct a. constructor. apply sem_pexpr_not_in.
+      eapply H0. econstructor. inv H. auto. inv H. auto.
+    - intros. inv H. constructor. unfold predicated_not_inP in H0.
+      eapply sem_pexpr_not_in. eapply H0. constructor. left. eauto.
+      auto. auto.
+      apply sem_pred_expr_cons_false. apply sem_pexpr_not_in. eapply H0.
+      constructor. tauto. auto. auto.
+      eapply IHl. eauto. eapply predicated_not_inP_cons; eauto.
+  Qed.
+
+  Lemma pred_not_in_forestP :
+    forall pred f,
+      predicated_not_in_forest pred f = true ->
+      forall x, predicated_not_inP pred (f #r x).
+  Proof. Admitted.
+
+  Lemma pred_not_in_forest_exitP :
+    forall pred f,
+      predicated_not_in_forest pred f = true ->
+      predicated_not_inP pred (forest_exit f).
+  Proof. Admitted.
+
+  Lemma from_predicated_sem_pred_expr :
+    forall A (ctx: @ctx A) preds pe b,
+      sem_pred_expr preds sem_pred ctx pe b ->
+      sem_pexpr ctx (from_predicated true preds pe) b.
+  Proof. Admitted.
+
+  Lemma sem_update_Isetpred:
+    forall A (ctx: @ctx A) f pr p0 c args b rs m,
+      valid_mem (ctx_mem ctx) m ->
+      sem ctx f (mk_instr_state rs pr m, None) ->
+      Op.eval_condition c rs ## args m = Some b ->
+      truthy pr p0 ->
+      sem_pexpr ctx
+      (from_predicated true (forest_preds f) (seq_app (pred_ret (PEsetpred c)) (merge (list_translation args f)))) b.
+  Proof.
+    intros. eapply from_predicated_sem_pred_expr.
+    pose proof (sem_merge_list _ ctx f rs pr m args H0).
+    apply sem_pred_expr_ident2 in H3; simplify.
+    eapply sem_pred_expr_seq_app_val; [eauto| |].
+    constructor. constructor. constructor.
+    econstructor; eauto.
+    erewrite storev_eval_condition; eauto.
+  Qed.
+
+  Lemma sem_update_Isetpred_top:
+    forall A f p p' f' rs m pr args p0 state c pred b,
+      Op.eval_condition c rs ## args m = Some b ->
+      truthy pr p0 ->
+      valid_mem (is_mem (ctx_is state)) m ->
+      sem state f ((mk_instr_state rs pr m), None) ->
+      update (p, f) (RBsetpred p0 c args pred) = Some (p', f') ->
+      eval_predf pr p = true ->
+      @sem A state f' (mk_instr_state rs (pr # pred <- b) m, None).
+  Proof.
+    intros * EVAL_OP TRUTHY VALID SEM UPD EVAL_PRED.
+    pose proof SEM as SEM2.
+    inversion UPD as [PRUNE]. unfold Option.bind in PRUNE. destr. destr.
+    inversion_clear PRUNE.
+    rename Heqo into PRUNE.
+    inversion_clear SEM as [? ? ? ? ? ? REG PRED MEM EXIT].
+    cbn [is_ps] in *. constructor.
+    + constructor. intros. apply sem_pred_not_in. rewrite forest_pred_reg.
+      inv REG. auto. rewrite forest_pred_reg. apply pred_not_in_forestP.
+      unfold assert_ in *. repeat (destruct_match; try discriminate); auto.
+    + constructor; intros. destruct (peq x pred); subst.
+      * rewrite Regmap.gss.
+        rewrite forest_pred_gss.
+        cbn [update] in *. unfold Option.bind in *. destr. destr. inv UPD.
+        replace b with (b && true) by eauto with bool.
+        apply sem_pexpr_Pand.
+        destruct b. constructor. right.
+        eapply sem_update_Isetpred; eauto.
+        constructor. constructor. replace false with (negb true) by auto.
+        apply sem_pexpr_negate. inv TRUTHY. constructor.
+        cbn. eapply sem_pexpr_eval. inv PRED. eauto. auto.
+        replace false with (negb true) by auto.
+        apply sem_pexpr_negate.
+        eapply sem_pexpr_eval. inv PRED. eauto. auto.
+        eapply sem_update_Isetpred; eauto.
+        constructor. constructor. constructor.
+        replace true with (negb false) by auto. apply sem_pexpr_negate.
+        eapply sem_pexpr_eval. inv PRED. eauto. inv TRUTHY. auto. cbn -[eval_predf].
+        rewrite eval_predf_negate. rewrite H; auto.
+        replace true with (negb false) by auto. apply sem_pexpr_negate.
+        eapply sem_pexpr_eval. inv PRED. eauto. rewrite eval_predf_negate.
+        rewrite EVAL_PRED. auto.
+      * rewrite Regmap.gso by auto. inv PRED. specialize (H x).
+        rewrite forest_pred_gso by auto; auto.
+    + rewrite forest_pred_reg. apply sem_pred_not_in. auto. apply pred_not_in_forestP.
+      unfold assert_ in *. now repeat (destruct_match; try discriminate).
+    + cbn -[from_predicated from_pred_op seq_app]. apply sem_pred_not_in; auto.
+      apply pred_not_in_forest_exitP.
+      unfold assert_ in *. now repeat (destruct_match; try discriminate).
+  Qed.
+
+  Lemma sem_pexpr_impl :
+    forall A (state: @ctx A) a b res,
+      sem_pexpr state b res ->
+      sem_pexpr state a true ->
+      sem_pexpr state (a → b) res.
+  Proof.
+    intros. destruct res.
+    constructor; tauto.
+    constructor; auto. replace false with (negb true) by auto.
+    now apply sem_pexpr_negate.
+  Qed.
+
+  Lemma sem_update_falsy:
+    forall A state f f' rs ps m p a p',
+      instr_falsy ps a ->
+      update (p, f) a = Some (p', f') ->
+      sem state f (mk_instr_state rs ps m, None) ->
+      @sem A state f' (mk_instr_state rs ps m, None).
+  Proof.
+    inversion 1; cbn [update] in *; intros.
+    - unfold Option.bind in *. destr. inv H2.
+      constructor.
+      * constructor. intros. destruct (peq x res); subst.
+        rewrite forest_reg_gss. cbn.
+        eapply sem_pred_expr_prune_predicated; eauto.
+        eapply sem_pred_expr_app_predicated_false. inv H3. inv H8. auto.
+        inv H3. inv H9. eauto. rewrite eval_predf_Pand. cbn -[eval_predf].
+        rewrite H0. auto. 
+        rewrite forest_reg_gso. inv H3. inv H8. auto.
+        unfold not; intros; apply n0. now inv H1.
+      * constructor; intros. rewrite forest_reg_pred. inv H3. inv H9. auto.
+      * rewrite forest_reg_gso. inv H3. auto. unfold not; intros. inversion H1.
+      * inv H3. auto.
+    - unfold Option.bind in *. destr. inv H2.
+      constructor.
+      * constructor. intros. destruct (peq x dst); subst.
+        rewrite forest_reg_gss. cbn.
+        eapply sem_pred_expr_prune_predicated; eauto.
+        eapply sem_pred_expr_app_predicated_false. inv H3. inv H8. auto.
+        inv H3. inv H9. eauto. rewrite eval_predf_Pand. cbn -[eval_predf].
+        rewrite H0. auto. 
+        rewrite forest_reg_gso. inv H3. inv H8. auto.
+        unfold not; intros; apply n0. now inv H1.
+      * constructor; intros. rewrite forest_reg_pred. inv H3. inv H9. auto.
+      * rewrite forest_reg_gso. inv H3. auto. unfold not; intros. inversion H1.
+      * inv H3. auto.
+    - unfold Option.bind in *. destr. inv H2.
+      constructor.
+      * constructor. intros. rewrite forest_reg_gso by discriminate. inv H3. inv H8. auto.
+      * constructor; intros. rewrite forest_reg_pred. inv H3. inv H9. auto.
+      * rewrite forest_reg_gss. cbn. eapply sem_pred_expr_prune_predicated; eauto.
+        eapply sem_pred_expr_app_predicated_false. inv H3. auto. inv H3. inv H9. eauto.
+        rewrite eval_predf_Pand. cbn -[eval_predf]. rewrite H0. auto.
+      * inv H3. auto.
+    - unfold Option.bind in *. destr. destr. inv H2.
+      constructor.
+      * constructor; intros. rewrite forest_pred_reg. apply sem_pred_not_in.
+        inv H3. inv H8. auto. apply pred_not_in_forestP. unfold assert_ in Heqo. now destr.
+      * constructor. intros. destruct (peq x pred); subst.
+        rewrite forest_pred_gss. replace (ps !! pred) with (true && ps !! pred) by auto.
+        assert (sem_pexpr state0 (¬ (from_pred_op (forest_preds f) p0 ∧ from_pred_op (forest_preds f) p')) true).
+        { replace true with (negb false) by auto. apply sem_pexpr_negate.
+          constructor. left. eapply sem_pexpr_eval. inv H3. inv H9. eauto.
+          auto.
+        }
+        apply sem_pexpr_Pand. constructor; tauto.
+        apply sem_pexpr_impl. inv H3. inv H10. eauto.
+        { constructor. left. eapply sem_pexpr_eval. inv H3. inv H10. eauto.
+          rewrite eval_predf_negate. rewrite H0. auto.
+        }
+        rewrite forest_pred_gso by auto. inv H3. inv H9. auto.
+      * rewrite forest_pred_reg. apply sem_pred_not_in. inv H3. auto.
+        apply pred_not_in_forestP. unfold assert_ in Heqo. now destr.
+      * apply sem_pred_not_in. inv H3; auto. cbn.
+        apply pred_not_in_forest_exitP. unfold assert_ in Heqo. now destr.
+    - unfold Option.bind in *. destr. inv H2. inv H3. constructor.
+      * constructor. inv H8. auto.
+      * constructor. intros. inv H9. eauto.
+      * auto.
+      * cbn. eapply sem_pred_expr_prune_predicated; [|eauto].
+        eapply sem_pred_expr_app_predicated_false; auto.
+        inv H9. eauto.
+        rewrite eval_predf_Pand. cbn -[eval_predf]. rewrite H0. auto.
+  Qed.
+
+  Definition setpred_wf (i: instr): bool :=
+    match i with
+    | RBsetpred (Some op) _ _ p => negb (predin peq p op)
+    | _ => true
+    end.
+
   Lemma sem_update_instr :
     forall f i' i'' a sp p i p' f',
       step_instr ge sp (Iexec i') a (Iexec i'') ->
@@ -1784,9 +2028,9 @@ all be evaluable.
     - eauto using sem_update_Iop_top.
     - eauto using sem_update_Iload_top.
     - eauto using sem_update_Istore_top.
-    - admit.
-    - admit.
-  Admitted.
+    - eauto using sem_update_Isetpred_top.
+    - destruct i''. eauto using sem_update_falsy.
+  Qed.
 
   Lemma Pand_true_left :
     forall ps a b,
diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v
index 58b960c..105c2da 100644
--- a/src/hls/Predicate.v
+++ b/src/hls/Predicate.v
@@ -87,6 +87,15 @@ Section PRED_DEFINITION.
     | Plit a => Plit a
     end.
 
+  Inductive PredIn (a: predicate): pred_op -> Prop :=
+  | PredIn_Plit: forall b, PredIn a (Plit (b, a))
+  | PredIn_Pand: forall p1 p2,
+    PredIn a p1 \/ PredIn a p2 ->
+    PredIn a (Pand p1 p2)
+  | PredIn_Por: forall p1 p2,
+    PredIn a p1 \/ PredIn a p2 ->
+    PredIn a (Por p1 p2).
+
   Section DEEP_SIMPLIFY.
 
     Context (eqd: forall a b: A, {a = b} + {a <> b}).
@@ -140,6 +149,18 @@ Section PRED_DEFINITION.
       | Plit (_, a') => eqd a a'
       end.
 
+    Lemma predin_PredIn:
+      forall a p, PredIn a p <-> predin a p = true.
+    Proof.
+      induction p; split; try solve [inversion 1 | discriminate].
+      - cbn. destruct p. inversion 1; subst. destruct eqd; auto.
+      - intros. cbn in *. destruct p. destruct eqd. subst. constructor. discriminate.
+      - inversion 1. apply orb_true_intro. tauto.
+      - intros. cbn in *. constructor. apply orb_prop in H. tauto.
+      - inversion 1. apply orb_true_intro. tauto.
+      - intros. cbn in *. apply orb_prop in H. constructor. tauto.
+    Qed.
+
   End DEEP_SIMPLIFY.
 
 End PRED_DEFINITION.
@@ -812,3 +833,34 @@ Proof.
   - eapply Pos.max_le_iff.
     eapply in_app_or in H. inv H; eauto.
 Qed.
+
+Lemma PredIn_decidable:
+  forall A (a: A) p (eqd: forall a b: A, { a = b } + { a <> b }),
+    { PredIn a p } + { ~ PredIn a p }.
+Proof.
+  intros. destruct (predin eqd a p) eqn:?.
+  - apply predin_PredIn in Heqb. tauto.
+  - right. unfold not; intros. apply not_true_iff_false in Heqb.
+    apply Heqb. now apply predin_PredIn.
+Qed.
+
+Lemma sat_predicate_pred_not_in :
+  forall p a a' op,
+    (forall x, x <> (Pos.to_nat p) -> a x = a' x) ->
+    ~ PredIn p op ->
+    sat_predicate op a = sat_predicate op a'.
+Proof.
+  induction op; intros H; auto.
+  - destruct p0. intros. destruct (peq p p0); subst.
+    + exfalso. apply H0. constructor.
+    + cbn. assert (Pos.to_nat p0 <> Pos.to_nat p). unfold not; intros; apply n.
+      now apply Pos2Nat.inj. apply H in H1. rewrite H1. auto.
+  - intros. assert (~ PredIn p op1 /\ ~ PredIn p op2).
+    split; unfold not; intros; apply H0; constructor; tauto.
+    inv H1. specialize (IHop1 H H2). specialize (IHop2 H H3).
+    cbn. rewrite IHop1. rewrite IHop2. auto.
+  - intros. assert (~ PredIn p op1 /\ ~ PredIn p op2).
+    split; unfold not; intros; apply H0; constructor; tauto.
+    inv H1. specialize (IHop1 H H2). specialize (IHop2 H H3).
+    cbn. rewrite IHop1. rewrite IHop2. auto.
+Qed.