From 5321f82fb46a87ca372b10ba5729509871cc935a Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 19 Jul 2022 08:53:57 +0200
Subject: Work on implementing abstract predicates

---
 benchmarks/polybench-syn/common.mk |   8 +-
 src/common/Monad.v                 |  11 +-
 src/common/Vericertlib.v           |  40 +----
 src/hls/Abstr.v                    | 202 +++++++++++-----------
 src/hls/Gible.v                    |   2 +
 src/hls/GiblePargen.v              | 200 ++++++++++++++--------
 src/hls/GiblePargenproof.v         |  20 +--
 src/hls/HTLPargen.v                |   1 +
 src/hls/HTLgen.v                   |   1 +
 src/hls/HashTree.v                 |  26 +++
 src/hls/PipelineOp.v               |   4 +-
 src/hls/Predicate.v                | 333 +++++++++++++++++++++----------------
 src/hls/PrintAbstr.ml              |  30 +++-
 src/hls/PrintGible.ml              |  34 ++--
 src/hls/RTLParFU.v                 |   2 +
 test/Makefile                      |   2 +-
 16 files changed, 528 insertions(+), 388 deletions(-)

diff --git a/benchmarks/polybench-syn/common.mk b/benchmarks/polybench-syn/common.mk
index e155e4a..877dd68 100644
--- a/benchmarks/polybench-syn/common.mk
+++ b/benchmarks/polybench-syn/common.mk
@@ -1,5 +1,5 @@
 VERICERT ?= vericert
-VERICERT_OPTS ?= -DSYNTHESIS -fschedule -fif-conv
+VERICERT_OPTS ?= -DSYNTHESIS -fschedule -fif-conv -dgblseq -dgblpar
 
 IVERILOG ?= iverilog
 IVERILOG_OPTS ?=
@@ -9,17 +9,17 @@ VERILATOR_OPTS ?= -Wno-fatal -Wno-lint -Wno-style -Wno-WIDTH --top main --exe $(
 
 TARGETS ?=
 
-%.v: %.c
+%.sv: %.c
 	@echo -e "\033[0;35mMAKE\033[0m" $<
 	$(VERICERT) $(VERICERT_OPTS) $< -o $@
 
-%.iver: %.v
+%.iver: %.sv
 	$(IVERILOG) -o $@ $(IVERILOG_OPTS) $<
 
 %.gcc: %.c
 	$(CC) $(CFLAGS) $< -o $@
 
-%.verilator: %.v
+%.verilator: %.sv
 	$(VERILATOR) $(VERILATOR_OPTS) --Mdir $@ --cc $<
 	@echo -e $(MAKE) -C $@ -f Vmain.mk
 	@$(MAKE) -C $@ -f Vmain.mk &>/dev/null
diff --git a/src/common/Monad.v b/src/common/Monad.v
index fcbe527..ece047c 100644
--- a/src/common/Monad.v
+++ b/src/common/Monad.v
@@ -18,6 +18,8 @@
 
 From Coq Require Import Lists.List.
 
+Declare Scope monad_scope.
+
 Module Type Monad.
 
   Parameter mon : Type -> Type.
@@ -36,17 +38,18 @@ End Monad.
 Module MonadExtra(M : Monad).
   Import M.
 
-  Module MonadNotation.
+  Module Import MonadNotation.
 
     Notation "'do' X <- A ; B" :=
       (bind A (fun X => B))
-        (at level 200, X name, A at level 100, B at level 200).
+        (at level 200, X name, A at level 100, B at level 200) : monad_scope.
     Notation "'do' ( X , Y ) <- A ; B" :=
       (bind2 A (fun X Y => B))
-        (at level 200, X name, Y name, A at level 100, B at level 200).
+        (at level 200, X name, Y name, A at level 100, B at level 200) : monad_scope.
 
   End MonadNotation.
-  Import MonadNotation.
+
+  #[local] Open Scope monad_scope.
 
   Fixpoint traverselist {A B: Type} (f: A -> mon B) (l: list A) {struct l}: mon (list B) :=
     match l with
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v
index 5540f34..24abece 100644
--- a/src/common/Vericertlib.v
+++ b/src/common/Vericertlib.v
@@ -31,6 +31,7 @@ Require Import compcert.lib.Integers.
 Require Import compcert.lib.Maps.
 
 Require Import vericert.common.Show.
+Require Export vericert.common.Optionmonad.
 
 (* Depend on CompCert for the basic library, as they declare and prove some
    useful theorems. *)
@@ -198,45 +199,6 @@ Ltac crush := simplify; try discriminate; try congruence; try lia; liapp;
 
 Definition compose (A B C : Type) (f : B -> C) (g : A -> B) (x : A) : C := f (g x). *)
 
-Module Option.
-
-Definition default {T : Type} (x : T) (u : option T) : T :=
-  match u with
-  | Some y => y
-  | _ => x
-  end.
-
-Definition map {S : Type} {T : Type} (f : S -> T) (u : option S) : option T :=
-  match u with
-  | Some y => Some (f y)
-  | _ => None
-  end.
-
-Definition liftA2 {T : Type} (f : T -> T -> T) (a : option T) (b : option T) : option T :=
-  match a with
-  | Some x => map (f x) b
-  | _ => None
-  end.
-
-Definition bind {A B : Type} (f : option A) (g : A -> option B) : option B :=
-  match f with
-  | Some a => g a
-  | _ => None
-  end.
-
-Definition join {A : Type} (a : option (option A)) : option A :=
-  match a with
-  | None => None
-  | Some a' => a'
-  end.
-
-Module Notation.
-Notation "'do' X <- A ; B" := (bind A (fun X => B))
-   (at level 200, X name, A at level 100, B at level 200).
-End Notation.
-
-End Option.
-
 Parameter debug_print : string -> unit.
 
 Definition debug_show {A B : Type} `{Show A} (a : A) (b : B) : B :=
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v
index 9902dc9..bfe49f3 100644
--- a/src/hls/Abstr.v
+++ b/src/hls/Abstr.v
@@ -91,6 +91,8 @@ Module R_indexed.
   Definition eq := resource_eq.
 End R_indexed.
 
+Compute xO xH.
+
 (*|
 We can then create expressions that mimic the expressions defined in RTLBlock
 and RTLPar, which use expressions instead of registers as their inputs and
@@ -116,17 +118,12 @@ Inductive expression : Type :=
 | Eexit : cf_instr -> expression
 with expression_list : Type :=
 | Enil : expression_list
-| Econs : expression -> expression_list -> expression_list
-.
+| Econs : expression -> expression_list -> expression_list.
 
 Definition apred : Type := expression.
-
-Inductive apred_op : Type :=
-| APlit: (bool * apred) -> apred_op
-| APtrue: apred_op
-| APfalse: apred_op
-| APand: apred_op -> apred_op -> apred_op
-| APor: apred_op -> apred_op -> apred_op.
+Definition apred_op := @Predicate.pred_op apred.
+Definition pred_op := @Predicate.pred_op positive.
+Definition predicate := positive.
 
 (* Declare Scope apred_op. *)
 
@@ -222,6 +219,16 @@ Proof.
     right. unfold not in *; intros. apply H0. inv H1. now inv H3. }
 Qed.
 
+Fixpoint filter {A: Type} (f: A -> bool) (l: non_empty A) : option (non_empty A) :=
+  match l with
+  | singleton a =>
+      if f a then Some (singleton a) else None
+  | a ::| b =>
+      if f a then
+        match filter f b with Some x => Some (a ::| x) | None => Some (singleton a) end
+      else filter f b
+  end.
+
 End NonEmpty.
 
 Module NE := NonEmpty.
@@ -233,6 +240,7 @@ Definition apredicated A := NE.non_empty (apred_op * A).
 Definition predicated A := NE.non_empty (pred_op * A).
 
 Definition apred_expr := apredicated expression.
+Definition pred_expr := predicated expression.
 
 (*|
 Using ``IMap`` we can create a map from resources to any other type, as
@@ -245,7 +253,7 @@ Definition forest : Type := Rtree.t apred_expr.
 
 Definition get_forest v (f: forest) :=
   match Rtree.get v f with
-  | None => NE.singleton (APtrue, (Ebase v))
+  | None => NE.singleton (Ptrue, (Ebase v))
   | Some v' => v'
   end.
 
@@ -345,19 +353,19 @@ with sem_val_list : ctx -> expression_list -> list val -> Prop :=
 .
 
 Inductive eval_apred (c: ctx): apred_op -> bool -> Prop :=
-| eval_APtrue : eval_apred c APtrue true
-| eval_APfalse : eval_apred c APfalse false
+| eval_APtrue : eval_apred c Ptrue true
+| eval_APfalse : eval_apred c Pfalse false
 | eval_APlit : forall p (b: bool) bres,
     sem_pred c p (if b then bres else negb bres) ->
-    eval_apred c (APlit (b, p)) bres
+    eval_apred c (Plit (b, p)) bres
 | eval_APand : forall p1 p2 b1 b2,
   eval_apred c p1 b1 ->
   eval_apred c p2 b2 ->
-  eval_apred c (APand p1 p2) (b1 && b2)
+  eval_apred c (Pand p1 p2) (b1 && b2)
 | eval_APor1 : forall p1 p2 b1 b2,
   eval_apred c p1 b1 ->
   eval_apred c p2 b2 ->
-  eval_apred c (APor p1 p2) (b1 || b2).
+  eval_apred c (Por p1 p2) (b1 || b2).
 
 Inductive sem_pred_expr {B: Type} (sem: ctx -> expression -> B -> Prop):
   ctx -> apred_expr -> B -> Prop :=
@@ -527,22 +535,22 @@ Import HT.
 Fixpoint hash_predicate (max: predicate) (ap: apred_op) (h: hash_tree)
   : pred_op * hash_tree :=
   match ap with
-  | APtrue => (Ptrue, h)
-  | APfalse => (Pfalse, h)
-  | APlit (b, ap') =>
+  | Ptrue => (Ptrue, h)
+  | Pfalse => (Pfalse, h)
+  | Plit (b, ap') =>
       let (p', h') := hash_value max ap' h in
       (Plit (b, p'), h')
-  | APand p1 p2 =>
+  | Pand p1 p2 =>
       let (p1', h') := hash_predicate max p1 h in
       let (p2', h'') := hash_predicate max p2 h' in
       (Pand p1' p2', h'')
-  | APor p1 p2 =>
+  | Por p1 p2 =>
       let (p1', h') := hash_predicate max p1 h in
       let (p2', h'') := hash_predicate max p2 h' in
       (Por p1' p2', h'')
   end.
 
-Fixpoint norm_expression (max: predicate) (pe: apred_expr) (h: hash_tree)
+Fixpoint anorm_expression (max: predicate) (pe: apred_expr) (h: hash_tree)
   : (PTree.t pred_op) * hash_tree :=
   match pe with
   | NE.singleton (p, e) =>
@@ -551,7 +559,7 @@ Fixpoint norm_expression (max: predicate) (pe: apred_expr) (h: hash_tree)
     (PTree.set hashed_e hashed_p (PTree.empty _), h'')
   | (p, e) ::| pr =>
     let (hashed_e, h') := hash_value max e h in
-    let (norm_pr, h'') := norm_expression max pr h' in
+    let (norm_pr, h'') := anorm_expression max pr h' in
     let (hashed_p, h''') := hash_predicate max p h'' in
     match norm_pr ! hashed_e with
     | Some pr_op =>
@@ -561,7 +569,24 @@ Fixpoint norm_expression (max: predicate) (pe: apred_expr) (h: hash_tree)
     end
   end.
 
-Definition mk_pred_stmnt' e p_e := ¬ p_e ∨ Plit (true, e).
+Fixpoint norm_expression (max: predicate) (pe: pred_expr) (h: hash_tree)
+  : (PTree.t pred_op) * hash_tree :=
+  match pe with
+  | NE.singleton (p, e) =>
+    let (hashed_e, h') := hash_value max e h in
+    (PTree.set hashed_e p (PTree.empty _), h')
+  | (p, e) ::| pr =>
+    let (hashed_e, h') := hash_value max e h in
+    let (norm_pr, h'') := norm_expression max pr h' in
+    match norm_pr ! hashed_e with
+    | Some pr_op =>
+      (PTree.set hashed_e (pr_op ∨ p) norm_pr, h'')
+    | None =>
+      (PTree.set hashed_e p norm_pr, h'')
+    end
+  end.
+
+Definition mk_pred_stmnt' (e: predicate) p_e := ¬ p_e ∨ Plit (true, e).
 
 Definition mk_pred_stmnt t := PTree.fold (fun x a b => mk_pred_stmnt' a b ∧ x) t T.
 
@@ -571,6 +596,10 @@ Definition encode_expression max pe h :=
   let (tree, h) := norm_expression max pe h in
   (mk_pred_stmnt tree, h).
 
+Definition aencode_expression max pe h :=
+  let (tree, h) := anorm_expression max pe h in
+  (mk_pred_stmnt tree, h).
+
 (*Fixpoint encode_expression_ne (max: predicate) (pe: pred_expr_ne) (h: hash_tree)
   : (PTree.t pred_op) * hash_tree :=
   match pe with
@@ -583,11 +612,11 @@ Definition encode_expression max pe h :=
     (Pand (Por (Pnot p) (Pvar p')) p'', h'')
   end.*)
 
-(* Fixpoint max_pred_expr (pe: pred_expr) : positive := *)
-(*   match pe with *)
-(*   | NE.singleton (p, e) => max_predicate p *)
-(*   | (p, e) ::| pe' => Pos.max (max_predicate p) (max_pred_expr pe') *)
-(*   end. *)
+Fixpoint max_pred_expr (pe: pred_expr) : positive :=
+  match pe with
+  | NE.singleton (p, e) => max_predicate p
+  | (p, e) ::| pe' => Pos.max (max_predicate p) (max_pred_expr pe')
+  end.
 
 Definition empty : forest := Rtree.empty _.
 
@@ -634,29 +663,9 @@ Inductive similar {A B} : @ctx A -> @ctx B -> Prop :=
     similar (mk_ctx ist sp ge) (mk_ctx ist' sp tge).
 
 Definition beq_pred_expr_once (pe1 pe2: apred_expr) : bool :=
-  match pe1, pe2 with
-  (* PEsingleton None e1, PEsingleton None e2 => beq_expression e1 e2
-  | PEsingleton (Some p1) e1, PEsingleton (Some p2) e2 =>
-    if beq_expression e1 e2
-    then match sat_pred_simple bound (Por (Pand p1 (Pnot p2)) (Pand p2 (Pnot p1))) with
-         | Some None => true
-         | _ => false
-         end
-    else false
-  | PEsingleton (Some p) e1, PEsingleton None e2
-  | PEsingleton None e1, PEsingleton (Some p) e2 =>
-    if beq_expression e1 e2
-    then match sat_pred_simple bound (Pnot p) with
-         | Some None => true
-         | _ => false
-         end
-    else false*)
-  | pe1, pe2 =>
-    (* let max := Pos.max (max_pred_expr pe1) (max_pred_expr pe2) in *)
-    let (p1, h) := encode_expression 1%positive pe1 (PTree.empty _) in
-    let (p2, h') := encode_expression 1%positive pe2 h in
-    equiv_check p1 p2
-  end.
+  let (p1, h) := aencode_expression 1%positive pe1 (PTree.empty _) in
+  let (p2, h') := aencode_expression 1%positive pe2 h in
+  equiv_check p1 p2.
 
 Definition tree_equiv_check_el (np2: PTree.t pred_op) (n: positive) (p: pred_op): bool :=
   match np2 ! n with
@@ -725,43 +734,39 @@ Module Type AbstrPredSet.
 
 End AbstrPredSet.
 
-Section ABSTR_PRED.
-
-  Context (h: hash_tree).
-  Context (m: predicate).
-
-  Definition sat_aequiv ap1 ap2 :=
-    exists p1 p2,
-      sat_equiv p1 p2
-      /\ hash_predicate m ap1 h = (p1, h)
-      /\ hash_predicate m ap2 h = (p2, h).
-
-  Lemma aequiv_symm : forall a b, sat_aequiv a b -> sat_aequiv b a.
-  Proof.
-    unfold sat_aequiv; simplify; do 2 eexists; simplify; [symmetry | |]; eauto.
-  Qed.
-
-  Lemma aequiv_trans :
-    forall a b c,
-      sat_aequiv a b ->
-      sat_aequiv b c ->
-      sat_aequiv a c.
-  Proof.
-    unfold sat_aequiv; intros * H H0; simplify; do 2 eexists; simplify;
-      [| eassumption | eassumption]; rewrite H0 in H3; inv H3.
-    transitivity x2; auto.
-  Qed.
+Definition sat_aequiv ap1 ap2 :=
+  exists h p1 p2,
+    sat_equiv p1 p2
+    /\ hash_predicate 1 ap1 h = (p1, h)
+    /\ hash_predicate 1 ap2 h = (p2, h).
 
-  Instance PER_aequiv : PER sat_aequiv :=
-    { PER_Symmetric := aequiv_symm;
-      PER_Transitive := aequiv_trans;
-    }.
-
-End ABSTR_PRED.
+Lemma aequiv_symm : forall a b, sat_aequiv a b -> sat_aequiv b a.
+Proof.
+  unfold sat_aequiv; simplify; do 3 eexists; simplify; [symmetry | |]; eauto.
+Qed.
 
+Lemma existsh :
+  forall ap1,
+  exists h p1,
+    hash_predicate 1 ap1 h = (p1, h).
+Proof. Admitted.
 
+Lemma aequiv_refl : forall a, sat_aequiv a a.
+Proof.
+  unfold sat_aequiv; intros.
+  pose proof (existsh a); simplify.
+  do 3 eexists; simplify; eauto. reflexivity.
+Qed.
 
-Definition hash_predicate
+Lemma aequiv_trans :
+  forall a b c,
+    sat_aequiv a b ->
+    sat_aequiv b c ->
+    sat_aequiv a c.
+Proof.
+  unfold sat_aequiv; intros.
+  simplify.
+Abort.
 
 Lemma norm_expr_mutexcl :
   forall m pe h t h' e e' p p',
@@ -773,7 +778,7 @@ Lemma norm_expr_mutexcl :
     p ⇒ ¬ p'.
 Proof. Abort.
 
-Lemma norm_expression_sem_pred :
+(*Lemma norm_expression_sem_pred :
   forall A B sem ctx pe v,
     sem_pred_expr sem ctx pe v ->
     forall pt et et' max,
@@ -827,12 +832,11 @@ Lemma norm_expression_sem_pred2 :
       predicated_mutexcl pe ->
       norm_expression (max_pred_expr pe) pe et = (pt, et') ->
       sem_pred_expr sem ctx pe v.
-Proof. Admitted.
+Proof. Admitted.*)
 
-Definition beq_pred_expr (pe1 pe2: pred_expr) : bool :=
-  let max := Pos.max (max_pred_expr pe1) (max_pred_expr pe2) in
-  let (np1, h) := norm_expression max pe1 (PTree.empty _) in
-  let (np2, h') := norm_expression max pe2 h in
+Definition beq_pred_expr (pe1 pe2: apred_expr) : bool :=
+  let (np1, h) := anorm_expression 1 pe1 (PTree.empty _) in
+  let (np2, h') := anorm_expression 1 pe2 h in
   forall_ptree (tree_equiv_check_el np2) np1
   && forall_ptree (tree_equiv_check_None_el np1) np2.
 
@@ -1102,7 +1106,7 @@ Section CORRECT.
   Proof.
     Abort.*)
 
-  Lemma norm_expr_implies :
+(*  Lemma norm_expr_implies :
     forall x m h t h' e expr p,
       norm_expression m x h = (t, h') ->
       h' ! e = Some expr ->
@@ -1140,7 +1144,7 @@ Section CORRECT.
           pose proof H0; rewrite e0 in H2;
             apply sem_pred_expr_cons_false; auto; inv H; crush.
       - inv H; constructor; auto; now apply sem_pred_expr_cons_false.
-  Qed.
+  Qed.*)
 
   Section SEM_PRED.
 
@@ -1153,7 +1157,7 @@ Section CORRECT.
                         repeat (nicify_hypotheses; nicify_goals; kill_bools; substpp);
                         cbn -[l] in *.
 
-    Lemma check_correct_sem_value:
+(*    Lemma check_correct_sem_value:
       forall x x' v v' t t' h h',
         beq_pred_expr x x' = true ->
         predicated_mutexcl x -> predicated_mutexcl x' ->
@@ -1270,7 +1274,7 @@ Section CORRECT.
             eapply exists_norm_expr2 in DSTR; try solve [eapply norm_expr_constant; eassumption | eassumption].
           }
         }
-    Admitted.*) Abort.
+    Admitted.*) Abort.*)
 
   End SEM_PRED.
 
@@ -1281,7 +1285,7 @@ Section CORRECT.
     Context (osem: @ctx tfd -> expression -> B -> Prop).
     Context (SEMCORR: forall e v, isem ictx e v -> osem octx e v).
 
-    Lemma sem_pred_tree_corr:
+(*    Lemma sem_pred_tree_corr:
       forall x x' v t t' h h',
              beq_pred_expr x x' = true ->
              predicated_mutexcl x -> predicated_mutexcl x' ->
@@ -1289,7 +1293,7 @@ Section CORRECT.
              norm_expression (Pos.max (max_pred_expr x) (max_pred_expr x')) x' h = (t', h') ->
              sem_pred_tree isem ictx h t v ->
              sem_pred_tree osem octx h' t' v.
-    Proof using SEMCORR. Admitted.
+    Proof using SEMCORR. Admitted.*)
 
   End SEM_PRED_CORR.
 
@@ -1325,7 +1329,7 @@ Admitted.
 End CORRECT.
 
 Lemma get_empty:
-  forall r, empty#r = NE.singleton (T, Ebase r).
+  forall r, empty#r = NE.singleton (Ptrue, Ebase r).
 Proof.
   intros; unfold get_forest;
   destruct_match; auto; [ ];
@@ -1420,7 +1424,7 @@ End BOOLEAN_EQUALITY.
 Lemma map1:
   forall w dst dst',
     dst <> dst' ->
-    (empty # dst <- w) # dst' = NE.singleton (T, Ebase dst').
+    (empty # dst <- w) # dst' = NE.singleton (Ptrue, Ebase dst').
 Proof. intros; unfold get_forest; rewrite Rtree.gso; auto; apply get_empty. Qed.
 
 Lemma genmap1:
@@ -1430,7 +1434,7 @@ Lemma genmap1:
 Proof. intros; unfold get_forest; rewrite Rtree.gso; auto. Qed.
 
 Lemma map2:
-  forall (v : pred_expr) x rs,
+  forall (v : apred_expr) x rs,
     (rs # x <- v) # x = v.
 Proof. intros; unfold get_forest; rewrite Rtree.gss; trivial. Qed.
 
diff --git a/src/hls/Gible.v b/src/hls/Gible.v
index fdc9a9d..0603269 100644
--- a/src/hls/Gible.v
+++ b/src/hls/Gible.v
@@ -43,6 +43,8 @@ Require Import Predicate.
 Require Import Vericertlib.
 
 Definition node := positive.
+Definition predicate := positive.
+Definition pred_op := @pred_op predicate.
 
 (*|
 .. index::
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v
index 01ee2cd..dae1efc 100644
--- a/src/hls/GiblePargen.v
+++ b/src/hls/GiblePargen.v
@@ -27,6 +27,7 @@ Require Import compcert.lib.Maps.
 Require compcert.verilog.Op.
 
 Require Import vericert.common.Vericertlib.
+Require Import vericert.common.Monad.
 Require Import vericert.hls.GibleSeq.
 Require Import vericert.hls.GiblePar.
 Require Import vericert.hls.Gible.
@@ -39,6 +40,11 @@ Import NE.NonEmptyNotation.
 #[local] Open Scope forest.
 #[local] Open Scope pred_op.
 
+Module OptionExtra := MonadExtra(Option).
+Import OptionExtra.
+Import OptionExtra.MonadNotation.
+#[local] Open Scope monad_scope.
+
 (*|
 ====================
 Gible Par Generation
@@ -53,7 +59,7 @@ to correctly translate the predicates.
 |*)
 
 Fixpoint list_translation (l : list reg) (f : forest) {struct l}
-  : list pred_expr :=
+  : list apred_expr :=
   match l with
   | nil => nil
   | i :: l => (f # (Reg i)) :: (list_translation l f)
@@ -65,58 +71,58 @@ Fixpoint replicate {A} (n: nat) (l: A) :=
   | S n => l :: replicate n l
   end.
 
-Definition merge''' x y :=
+Definition merge''' {A: Type} (x y: option (@Predicate.pred_op A)) :=
   match x, y with
   | Some p1, Some p2 => Some (Pand p1 p2)
   | Some p, None | None, Some p => Some p
   | None, None => None
   end.
 
-Definition merge'' x :=
+Definition merge'' {A: Type} x :=
   match x with
-  | ((a, e), (b, el)) => (merge''' a b, Econs e el)
+  | ((a, e), (b, el)) => (@merge''' A a b, Econs e el)
   end.
 
-Definition map_pred_op {A B} (pf: option pred_op * (A -> B))
-           (pa: option pred_op * A): option pred_op * B :=
+Definition map_pred_op {A B P: Type} (pf: option (@Predicate.pred_op P) * (A -> B))
+           (pa: option (@Predicate.pred_op P) * A): option (@Predicate.pred_op P) * B :=
   match pa, pf with
   | (p, a), (p', f) => (merge''' p p', f a)
   end.
 
-Definition predicated_prod {A B: Type} (p1: predicated A) (p2: predicated B) :=
+Definition predicated_prod {A B: Type} (p1: apredicated A) (p2: apredicated B) :=
   NE.map (fun x => match x with ((a, b), (c, d)) => (Pand a c, (b, d)) end)
          (NE.non_empty_prod p1 p2).
 
-Definition predicated_map {A B: Type} (f: A -> B) (p: predicated A)
-  : predicated B := NE.map (fun x => (fst x, f (snd x))) p.
+Definition predicated_map {A B: Type} (f: A -> B) (p: apredicated A)
+  : apredicated B := NE.map (fun x => (fst x, f (snd x))) p.
 
 (*map (fun x => (fst x, Econs (snd x) Enil)) pel*)
-Definition merge' (pel: pred_expr) (tpel: predicated expression_list) :=
+Definition merge' (pel: apred_expr) (tpel: apredicated expression_list) :=
   predicated_map (uncurry Econs) (predicated_prod pel tpel).
 
-Fixpoint merge (pel: list pred_expr): predicated expression_list :=
+Fixpoint merge (pel: list apred_expr): apredicated expression_list :=
   match pel with
   | nil => NE.singleton (T, Enil)
   | a :: b => merge' a (merge b)
   end.
 
-Definition map_predicated {A B} (pf: predicated (A -> B)) (pa: predicated A)
-  : predicated B :=
+Definition map_predicated {A B} (pf: apredicated (A -> B)) (pa: apredicated A)
+  : apredicated B :=
   predicated_map (fun x => (fst x) (snd x)) (predicated_prod pf pa).
 
-Definition predicated_apply1 {A B} (pf: predicated (A -> B)) (pa: A)
-  : predicated B :=
+Definition predicated_apply1 {A B} (pf: apredicated (A -> B)) (pa: A)
+  : apredicated B :=
   NE.map (fun x => (fst x, (snd x) pa)) pf.
 
-Definition predicated_apply2 {A B C} (pf: predicated (A -> B -> C)) (pa: A)
-           (pb: B): predicated C :=
+Definition predicated_apply2 {A B C} (pf: apredicated (A -> B -> C)) (pa: A)
+           (pb: B): apredicated C :=
   NE.map (fun x => (fst x, (snd x) pa pb)) pf.
 
-Definition predicated_apply3 {A B C D} (pf: predicated (A -> B -> C -> D))
-           (pa: A) (pb: B) (pc: C): predicated D :=
+Definition predicated_apply3 {A B C D} (pf: apredicated (A -> B -> C -> D))
+           (pa: A) (pb: B) (pc: C): apredicated D :=
   NE.map (fun x => (fst x, (snd x) pa pb pc)) pf.
 
-Definition predicated_from_opt {A: Type} (p: option pred_op) (a: A) :=
+Definition predicated_from_opt {A: Type} (p: option apred_op) (a: A) :=
   match p with
   | Some p' => NE.singleton (p', a)
   | None => NE.singleton (T, a)
@@ -137,18 +143,19 @@ Fixpoint NEapp {A} (l m: NE.non_empty A) :=
   | a ::| b => a ::| NEapp b m
   end.
 
-Definition app_predicated' {A: Type} (a b: predicated A) :=
+Definition app_predicated' {A: Type} (a b: apredicated A) :=
   let negation := ¬ (NEfold_left (fun a b => a ∨ (fst b)) b ⟂) in
   NEapp (NE.map (fun x => (negation ∧ fst x, snd x)) a) b.
 
-Definition app_predicated {A: Type} (p: option pred_op) (a b: predicated A) :=
-  match p with
-  | Some p' => NEapp (NE.map (fun x => (¬ p' ∧ fst x, snd x)) a)
-                     (NE.map (fun x => (p' ∧ fst x, snd x)) b)
-  | None => b
-  end.
+Definition app_predicated {A: Type} (p': apred_op) (a b: apredicated A) :=
+  NEapp (NE.map (fun x => (¬ p' ∧ fst x, snd x)) a)
+        (NE.map (fun x => (p' ∧ fst x, snd x)) b).
 
-Definition pred_ret {A: Type} (a: A) : predicated A :=
+Definition prune_predicated {A: Type} (a: apredicated A) :=
+  NE.filter (fun x => match deep_simplify expression_dec (fst x) with ⟂ => false | _ => true end)
+            (NE.map (fun x => (deep_simplify expression_dec (fst x), snd x)) a).
+
+Definition pred_ret {A: Type} (a: A) : apredicated A :=
   NE.singleton (T, a).
 
 (*|
@@ -167,53 +174,105 @@ This is done by multiplying the predicates together, and assigning the negation
 of the expression to the other predicates.
 |*)
 
-Definition upd_pred_forest (p: option pred_op) (f: forest) :=
-  match p with
-  | Some p' =>
-      PTree.map (fun i e =>
-                   NE.map (fun (x: pred_op * expression) =>
-                             let (pred, expr) := x in
-                             (Pand p' pred, expr)
-                          ) e) f
-  | None => f
+Definition upd_pred_forest (p: apred_op) (f: forest) :=
+  PTree.map (fun i e =>
+               NE.map (fun (x: apred_op * expression) =>
+                         let (pred, expr) := x in
+                         (Pand p pred, expr)) e) f.
+
+Fixpoint apredicated_to_apred_op (b: bool) (a: apredicated expression): apred_op :=
+  match a with
+  | NE.singleton (p, e) => Pimplies p (Plit (b, e))
+  | (p, e) ::| r =>
+      Pand (Pimplies p (Plit (true, e))) (apredicated_to_apred_op b r)
+  end.
+
+(* Fixpoint get_pred' (f: forest) (ap: pred_op): option apred_op := *)
+(*   match ap with *)
+(*   | Ptrue => Some Ptrue *)
+(*   | Pfalse => Some Pfalse *)
+(*   | Plit (a, b) => *)
+(*       match f # (Pred b) with *)
+(*       | NE.singleton (Ptrue, p) => Some (Plit (a, p)) *)
+(*       | _ => None *)
+(*       end *)
+(*   | Pand a b => match (get_pred' f a), (get_pred' f b) with *)
+(*                | Some a', Some b' => Some (Pand a' b') *)
+(*                | _, _ => None *)
+(*                end *)
+(*   | Por a b => match (get_pred' f a), (get_pred' f b) with *)
+(*               | Some a', Some b' => Some (Por a' b') *)
+(*               | _, _ => None *)
+(*               end *)
+(*   end. *)
+
+(* Definition get_pred (f: forest) (ap: option pred_op): option apred_op := *)
+(*   get_pred' f (Option.default T ap). *)
+
+Fixpoint get_pred' (f: forest) (ap: pred_op): apred_op :=
+  match ap with
+  | Ptrue => Ptrue
+  | Pfalse => Pfalse
+  | Plit (a, b) =>
+      apredicated_to_apred_op a (f # (Pred b))
+  | Pand a b => Pand (get_pred' f a) (get_pred' f b)
+  | Por a b => Por (get_pred' f a) (get_pred' f b)
   end.
 
-Definition update (fop : option pred_op * forest) (i : instr): (option pred_op * forest) :=
-  let (pred, f) := fop in
+Definition get_pred (f: forest) (ap: option pred_op): apred_op :=
+  get_pred' f (Option.default Ptrue ap).
+
+#[local] Open Scope monad_scope.
+
+Definition simpl_combine {A: Type} (a b: option (@Predicate.pred_op A)) :=
+  Option.map simplify (combine_pred a b).
+
+Definition update (fop : option (apred_op * forest)) (i : instr): option (apred_op * forest) :=
+  do (pred, f) <- fop;
   match i with
   | RBnop => fop
   | RBop p op rl r =>
-      (pred, f # (Reg r) <-
-             (app_predicated (combine_pred p pred)
+      do pruned <-
+           prune_predicated
+             (app_predicated (get_pred f p ∧ pred)
                              (f # (Reg r))
-                             (map_predicated (pred_ret (Eop op)) (merge (list_translation rl f)))))
+                             (map_predicated (pred_ret (Eop op)) (merge (list_translation rl f))));
+      Some (pred, f # (Reg r) <- pruned)
   | RBload p chunk addr rl r =>
-    (pred, f # (Reg r) <-
-      (app_predicated (combine_pred p pred)
-         (f # (Reg r))
-         (map_predicated
-            (map_predicated (pred_ret (Eload chunk addr))
-                            (merge (list_translation rl f)))
-            (f # Mem))))
+      do pruned <-
+           prune_predicated
+             (app_predicated (get_pred f p ∧ pred)
+                             (f # (Reg r))
+                             (map_predicated
+                                (map_predicated (pred_ret (Eload chunk addr))
+                                                (merge (list_translation rl f)))
+                                (f # Mem)));
+      Some (pred, f # (Reg r) <- pruned)
   | RBstore p chunk addr rl r =>
-    (pred, f # Mem <-
-      (app_predicated (combine_pred p pred)
-         (f # Mem)
-         (map_predicated
-            (map_predicated
-               (predicated_apply2 (map_predicated (pred_ret Estore)
-                                                  (f # (Reg r))) chunk addr)
-               (merge (list_translation rl f))) (f # Mem))))
+      do pruned <-
+           prune_predicated
+             (app_predicated (get_pred f p ∧ pred)
+                             (f # Mem)
+                             (map_predicated
+                                (map_predicated
+                                   (predicated_apply2 (map_predicated (pred_ret Estore)
+                                                                      (f # (Reg r))) chunk addr)
+                                   (merge (list_translation rl f))) (f # Mem)));
+      Some (pred, f # Mem <- pruned)
   | RBsetpred p' c args p =>
-    (pred, f # (Pred p) <-
-    (app_predicated (combine_pred p' pred)
-       (f # (Pred p))
-       (map_predicated (pred_ret (Esetpred c))
-                       (merge (list_translation args f)))))
+      do pruned <-
+           prune_predicated
+             (app_predicated (get_pred f p' ∧ pred)
+                                    (f # (Pred p))
+                                    (map_predicated (pred_ret (Esetpred c))
+                                                    (merge (list_translation args f))));
+      Some (pred, f # (Pred p) <- pruned)
   | RBexit p c =>
-      (combine_pred (Some (negate (Option.default T p))) pred,
-        f # Exit <-
-          (app_predicated (combine_pred p pred) (f # Exit) (pred_ret (Eexit c))))
+      let new_p := simplify (get_pred' f (negate (Option.default T p)) ∧ pred) in
+      do pruned <-
+           prune_predicated
+             (app_predicated (get_pred f p ∧ pred) (f # Exit) (pred_ret (Eexit c)));
+      Some (new_p, f # Exit <- pruned)
   end.
 
 (*|
@@ -224,8 +283,8 @@ code than in the RTLBlock code.
 Get a sequence from the basic block.
 |*)
 
-Definition abstract_sequence (b : list instr) : forest :=
-  snd (fold_left update b (None, empty)).
+Definition abstract_sequence (b : list instr) : option forest :=
+  Option.map snd (fold_left update b (Some (Ptrue, empty))).
 
 (*|
 Check equivalence of control flow instructions.  As none of the basic blocks
@@ -252,8 +311,11 @@ Definition empty_trees (bb: SeqBB.t) (bbt: ParBB.t) : bool :=
   end.
 
 Definition schedule_oracle (bb: SeqBB.t) (bbt: ParBB.t) : bool :=
-  (check (abstract_sequence bb) (abstract_sequence (concat (concat bbt))))
-  && empty_trees bb bbt.
+  match abstract_sequence bb, abstract_sequence (concat (concat bbt)) with
+  | Some bb', Some bbt' =>
+      check bb' bbt' && empty_trees bb bbt
+  | _, _ => false
+  end.
 
 Definition check_scheduled_trees := beq2 schedule_oracle.
 
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v
index 955902c..84a128a 100644
--- a/src/hls/GiblePargenproof.v
+++ b/src/hls/GiblePargenproof.v
@@ -106,7 +106,7 @@ Proof. induction l; crush. Qed.
 Lemma check_dest_l_dec i r : {check_dest_l i r = true} + {check_dest_l i r = false}.
 Proof. destruct (check_dest_l i r); tauto. Qed.
 
-Lemma check_dest_update :
+(*Lemma check_dest_update :
   forall f i r,
   check_dest i r = false ->
   (snd (update f i)) # (Reg r) = (snd f) # (Reg r).
@@ -1162,13 +1162,13 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
       sem (mk_ctx i sp ge) (snd (update (p, f) a)) (i'', None).
   Proof. Admitted.
 
-  Lemma sem_update_instr_term :
+(*  Lemma sem_update_instr_term :
     forall f i' i'' a sp i cf p p',
       sem (mk_ctx i sp ge) f (i', None) ->
       step_instr ge sp (Iexec i') (RBexit p cf) (Iterm i'' cf) ->
       sem (mk_ctx i sp ge) (snd (update (p', f) a)) (i'', Some cf)
            /\ falsy (is_ps i'') (fst (update (p', f) a)).
-  Proof. Admitted.
+  Proof. Admitted.*)
 
   Lemma step_instr_lessdef :
     forall sp a i i' ti,
@@ -1184,7 +1184,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
       exists ti', step_instr ge sp (Iexec ti) a (Iterm ti' cf) /\ state_lessdef i' ti'.
   Proof. Admitted.
 
-  Lemma app_predicated_semregset :
+(*  Lemma app_predicated_semregset :
     forall A ctx o f res r y,
       @sem_regset A ctx f res ->
       falsy (ctx_ps ctx) o ->
@@ -1212,7 +1212,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
   Proof.
     inversion 1; subst; crush.
     constructor.
-  Admitted.
+  Admitted.*)
 
   Lemma combined_falsy :
     forall i o1 o,
@@ -1224,7 +1224,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
     constructor. auto.
   Qed.
 
-  Lemma falsy_update :
+  (*Lemma falsy_update :
     forall f a ps,
       falsy ps (fst f) ->
       falsy ps (fst (update f a)).
@@ -1306,7 +1306,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
   Proof.
     unfold abstract_sequence. intros; eapply abstr_fold_correct; eauto.
     simplify. eapply sem_empty.
-  Qed.
+  Qed.*)
 
   Lemma abstr_check_correct :
     forall sp i i' a b cf ti,
@@ -1333,7 +1333,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
       exists ti', ParBB.step tge sp (Iexec ti) y (Iterm ti' cf)
              /\ state_lessdef i' ti'.
   Proof.
-    unfold schedule_oracle; intros. simplify.
+    (*unfold schedule_oracle; intros. simplify.
     exploit abstr_sequence_correct; eauto; simplify.
     exploit abstr_check_correct; eauto. apply state_lessdef_refl. simplify.
     exploit abstr_seq_reverse_correct; eauto. apply state_lessdef_refl. simplify.
@@ -1341,7 +1341,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
     econstructor; split; eauto.
     etransitivity; eauto.
     etransitivity; eauto.
-  Qed.
+  Qed.*) Admitted.
 
   Lemma step_cf_correct :
     forall cf ts s s' t,
@@ -1422,4 +1422,4 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
     exact transl_step_correct.
   Qed.
 
-End CORRECTNESS.
+End CORRECTNESS.*)
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index d9a2b48..b602ab6 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -102,6 +102,7 @@ Export HTLMonad.
 Module HTLMonadExtra := Monad.MonadExtra(HTLMonad).
 Import HTLMonadExtra.
 Export MonadNotation.
+#[local] Open Scope monad_scope.
 
 Fixpoint pred_expr (preg: reg) (p: pred_op) :=
   match p with
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v
index c793b1b..bff68a2 100644
--- a/src/hls/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -99,6 +99,7 @@ Export HTLMonad.
 Module HTLMonadExtra := Monad.MonadExtra(HTLMonad).
 Import HTLMonadExtra.
 Export MonadNotation.
+#[local] Open Scope monad_scope.
 
 Definition state_goto (st : reg) (n : node) : stmnt :=
   Vnonblock (Vvar st) (Vlit (posToValue n)).
diff --git a/src/hls/HashTree.v b/src/hls/HashTree.v
index 9f9ec81..80a7825 100644
--- a/src/hls/HashTree.v
+++ b/src/hls/HashTree.v
@@ -21,6 +21,8 @@ Require Import Coq.Structures.Equalities.
 Require Import compcert.lib.Maps.
 
 Require Import vericert.common.Vericertlib.
+Require Import vericert.common.Monad.
+Require Import vericert.common.Statemonad.
 
 #[local] Open Scope positive.
 
@@ -432,4 +434,28 @@ Module HashTree(H: Hashable).
         by (apply max_not_present; lia). crush.
   Qed.
 
+  Module HashState <: State.
+    Definition st := hash_tree.
+    Definition st_prop (h1 h2: hash_tree): Prop :=
+      forall x y, h1 ! x = Some y -> h2 ! x = Some y.
+
+    Lemma st_refl :
+      forall s, st_prop s s.
+    Proof. unfold st_prop; auto. Qed.
+
+    Lemma st_trans :
+      forall s1 s2 s3,
+        st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3.
+    Proof.
+      unfold st_prop; intros; eauto.
+    Qed.
+
+    #[export] Instance HashStatePreorder : PreOrder st_prop :=
+      { PreOrder_Reflexive := st_refl;
+        PreOrder_Transitive := st_trans;
+      }.
+  End HashState.
+
+  Module HashMonad := Statemonad(HashState).
+
 End HashTree.
diff --git a/src/hls/PipelineOp.v b/src/hls/PipelineOp.v
index 63d7d5a..90ccea0 100644
--- a/src/hls/PipelineOp.v
+++ b/src/hls/PipelineOp.v
@@ -31,8 +31,10 @@ Require Import vericert.common.Vericertlib.
 Require Import vericert.hls.Gible.
 Require Import vericert.hls.GiblePar.
 Require Import vericert.hls.FunctionalUnits.
+Require Import vericert.common.Monad.
 
-Import Option.Notation.
+Module OptionExtra := MonadExtra(Option).
+Import OptionExtra.MonadNotation.
 
 Local Open Scope positive.
 
diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v
index b9333d9..8dbd0f6 100644
--- a/src/hls/Predicate.v
+++ b/src/hls/Predicate.v
@@ -7,22 +7,142 @@ Require Import Coq.Logic.Decidable.
 
 Require Import vericert.common.Vericertlib.
 Require Import vericert.hls.Sat.
-
-Definition predicate : Type := positive.
-
-Inductive pred_op : Type :=
-| Plit: (bool * predicate) -> pred_op
-| Ptrue: pred_op
-| Pfalse: pred_op
-| Pand: pred_op -> pred_op -> pred_op
-| Por: pred_op -> pred_op -> pred_op.
+Require Import HashTree.
 
 Declare Scope pred_op.
 
+Section PRED_DEFINITION.
+
+  Context {A: Type}.
+
+  Definition predicate := A.
+
+  Inductive pred_op : Type :=
+  | Plit: (bool * predicate) -> pred_op
+  | Ptrue: pred_op
+  | Pfalse: pred_op
+  | Pand: pred_op -> pred_op -> pred_op
+  | Por: pred_op -> pred_op -> pred_op.
+
+  Fixpoint negate (p: pred_op) :=
+    match p with
+    | Plit (b, pr) => Plit (negb b, pr)
+    | Ptrue => Pfalse
+    | Pfalse => Ptrue
+    | Pand A B => Por (negate A) (negate B)
+    | Por A B => Pand (negate A) (negate B)
+    end.
+
+  Definition Pimplies (p: pred_op) p' := Por (negate p) p'.
+
+  Fixpoint predicate_use (p: pred_op) : list predicate :=
+    match p with
+    | Plit (b, p) => p :: nil
+    | Ptrue => nil
+    | Pfalse => nil
+    | Pand a b => predicate_use a ++ predicate_use b
+    | Por a b => predicate_use a ++ predicate_use b
+    end.
+
+  Definition combine_pred (p1 p2: option pred_op): option pred_op :=
+    match p1, p2 with
+    | Some p1, Some p2 => Some (Pand p1 p2)
+    | Some p, _ | _, Some p => Some p
+    | None, None => None
+    end.
+
+  Definition simplify' (p: pred_op) :=
+    match p with
+    (* | (Plit (b1, a)) ∧ (Plit (b2, b)) as p' => *)
+    (*     if Pos.eqb a b then *)
+    (*       if negb (xorb b1 b2) then Plit (b1, a) else ⟂ *)
+    (*     else p' *)
+    (* | (Plit (b1, a)) ∨ (Plit (b2, b)) as p' => *)
+    (*     if Pos.eqb a b then *)
+    (*       if negb (xorb b1 b2) then Plit (b1, a) else T *)
+    (*     else p' *)
+    | Pand A Ptrue => A
+    | Pand Ptrue A => A
+    | Pand _ Pfalse => Pfalse
+    | Pand Pfalse _ => Pfalse
+    | Por _ Ptrue => Ptrue
+    | Por Ptrue _ => Ptrue
+    | Por A Pfalse => A
+    | Por Pfalse A => A
+    | A => A
+    end.
+
+  Fixpoint simplify (p: pred_op) :=
+    match p with
+    | Pand A B =>
+        let A' := simplify A in
+        let B' := simplify B in
+        simplify' (Pand A' B')
+    | Por A B =>
+        let A' := simplify A in
+        let B' := simplify B in
+        simplify' (Por A' B')
+    | Ptrue => Ptrue
+    | Pfalse => Pfalse
+    | Plit a => Plit a
+    end.
+
+  Section DEEP_SIMPLIFY.
+
+    Context (eqd: forall a b: A, {a = b} + {a <> b}).
+
+    Definition deep_simplify' (p: pred_op) :=
+      match p with
+      | Pand A Ptrue => A
+      | Pand Ptrue A => A
+      | Pand _ Pfalse => Pfalse
+      | Pand Pfalse _ => Pfalse
+      | Por _ Ptrue => Ptrue
+      | Por Ptrue _ => Ptrue
+      | Por A Pfalse => A
+      | Por Pfalse A => A
+
+      | Pand (Plit (b1, a)) (Plit (b2, b)) =>
+          if eqd a b then
+            if bool_eqdec b1 b2 then
+              Plit (b1, a)
+            else Pfalse
+          else Pand (Plit (b1, a)) (Plit (b2, b))
+      | Por (Plit (b1, a)) (Plit (b2, b)) =>
+          if eqd a b then
+            if bool_eqdec b1 b2 then
+              Plit (b1, a)
+            else Ptrue
+          else Por (Plit (b1, a)) (Plit (b2, b))
+
+      | A => A
+      end.
+
+    Fixpoint deep_simplify (p: pred_op) :=
+      match p with
+      | Pand A B =>
+          let A' := deep_simplify A in
+          let B' := deep_simplify B in
+          deep_simplify' (Pand A' B')
+      | Por A B =>
+          let A' := deep_simplify A in
+          let B' := deep_simplify B in
+          deep_simplify' (Por A' B')
+      | Ptrue => Ptrue
+      | Pfalse => Pfalse
+      | Plit a => Plit a
+      end.
+
+  End DEEP_SIMPLIFY.
+
+End PRED_DEFINITION.
+
 Notation "A ∧ B" := (Pand A B) (at level 20) : pred_op.
 Notation "A ∨ B" := (Por A B) (at level 25) : pred_op.
 Notation "⟂" := (Pfalse) : pred_op.
 Notation "'T'" := (Ptrue) : pred_op.
+Notation "¬ A" := (negate A) (at level 15) : pred_op.
+Notation "A → B" := (Pimplies A B) (at level 30) : pred_op.
 
 #[local] Open Scope pred_op.
 
@@ -47,18 +167,18 @@ Lemma equiv_refl : forall a, sat_equiv a a.
 Proof. crush. Qed.
 
 #[global]
-Instance Equivalence_SAT : Equivalence sat_equiv :=
+ Instance Equivalence_SAT : Equivalence sat_equiv :=
   { Equivalence_Reflexive := equiv_refl ;
     Equivalence_Symmetric := equiv_symm ;
     Equivalence_Transitive := equiv_trans ;
   }.
 
 #[global]
-Instance SATSetoid : Setoid pred_op :=
+ Instance SATSetoid : Setoid pred_op :=
   { equiv := sat_equiv; }.
 
 #[global]
-Instance PandProper : Proper (equiv ==> equiv ==> equiv) Pand.
+ Instance PandProper : Proper (equiv ==> equiv ==> equiv) Pand.
 Proof.
   unfold Proper. simplify. unfold "==>".
   intros.
@@ -68,7 +188,7 @@ Proof.
 Qed.
 
 #[global]
-Instance PorProper : Proper (equiv ==> equiv ==> equiv) Por.
+ Instance PorProper : Proper (equiv ==> equiv ==> equiv) Por.
 Proof.
   unfold Proper, "==>". simplify.
   intros.
@@ -78,7 +198,7 @@ Proof.
 Qed.
 
 #[global]
-Instance sat_predicate_Proper : Proper (equiv ==> eq ==> eq) sat_predicate.
+ Instance sat_predicate_Proper : Proper (equiv ==> eq ==> eq) sat_predicate.
 Proof.
   unfold Proper, "==>". simplify.
   intros.
@@ -86,19 +206,8 @@ Proof.
   apply H.
 Qed.
 
-Fixpoint negate (p: pred_op) :=
-  match p with
-  | Plit (b, pr) => Plit (negb b, pr)
-  | T => ⟂
-  | ⟂ => T
-  | A ∧ B => negate A ∨ negate B
-  | A ∨ B => negate A ∧ negate B
-  end.
-
-Notation "¬ A" := (negate A) (at level 15) : pred_op.
-
 Lemma negate_correct :
-  forall h a, sat_predicate (negate h) a = negb (sat_predicate h a).
+  forall (h: @pred_op positive) a, sat_predicate (negate h) a = negb (sat_predicate h a).
 Proof.
   induction h; crush.
   - repeat destruct_match; subst; crush; symmetry; apply negb_involutive.
@@ -150,8 +259,8 @@ Proof.
   intros. specialize (H c); simplify.
   rewrite negate_correct in *.
   destruct (sat_predicate b c) eqn:X;
-  destruct (sat_predicate a c) eqn:X2;
-  crush.
+    destruct (sat_predicate a c) eqn:X2;
+    crush.
 Qed.
 
 Lemma sat_predicate_and :
@@ -183,8 +292,8 @@ Proof.
   specialize (H c); simplify.
   rewrite negate_correct in *.
   destruct (sat_predicate b c) eqn:X;
-  destruct (sat_predicate a c) eqn:X2;
-  crush.
+    destruct (sat_predicate a c) eqn:X2;
+    crush.
 Qed.
 
 Lemma sat_equiv4 :
@@ -197,52 +306,16 @@ Proof.
   rewrite andb_negb_r. auto.
 Qed.
 
-Definition simplify' (p: pred_op) :=
-  match p with
-  | (Plit (b1, a)) ∧ (Plit (b2, b)) as p' =>
-      if Pos.eqb a b then
-        if negb (xorb b1 b2) then Plit (b1, a) else ⟂
-      else p'
-  | (Plit (b1, a)) ∨ (Plit (b2, b)) as p' =>
-      if Pos.eqb a b then
-        if negb (xorb b1 b2) then Plit (b1, a) else T
-      else p'
-  | A ∧ T => A
-  | T ∧ A => A
-  | _ ∧ ⟂ => ⟂
-  | ⟂ ∧ _ => ⟂
-  | _ ∨ T => T
-  | T ∨ _ => T
-  | A ∨ ⟂ => A
-  | ⟂ ∨ A => A
-  | A => A
-  end.
-
 Lemma pred_op_dec :
-  forall p1 p2: pred_op,
-  { p1 = p2 } + { p1 <> p2 }.
+  forall p1 p2: @pred_op positive,
+    { p1 = p2 } + { p1 <> p2 }.
 Proof. pose proof Pos.eq_dec. repeat decide equality. Qed.
 
-Fixpoint simplify (p: pred_op) :=
-  match p with
-  | A ∧ B =>
-    let A' := simplify A in
-    let B' := simplify B in
-    simplify' (A' ∧ B')
-  | A ∨ B =>
-    let A' := simplify A in
-    let B' := simplify B in
-    simplify' (A' ∨ B')
-  | T => T
-  | ⟂ => ⟂
-  | Plit a => Plit a
-  end.
-
 Lemma simplify'_correct :
   forall h a,
     sat_predicate (simplify' h) a = sat_predicate h a.
 Proof.
-  (*destruct h; crush; repeat destruct_match; crush;
+(*destruct h; crush; repeat destruct_match; crush;
   solve [rewrite andb_true_r; auto | rewrite orb_false_r; auto].
 Qed.*) Admitted.
 
@@ -271,15 +344,15 @@ Fixpoint mult {A: Type} (a b: list (list A)) : list (list A) :=
 
 Lemma satFormula_concat:
   forall a b agn,
-  satFormula a agn ->
-  satFormula b agn ->
-  satFormula (a ++ b) agn.
+    satFormula a agn ->
+    satFormula b agn ->
+    satFormula (a ++ b) agn.
 Proof. induction a; crush. Qed.
 
 Lemma satFormula_concat2:
   forall a b agn,
-  satFormula (a ++ b) agn ->
-  satFormula a agn /\ satFormula b agn.
+    satFormula (a ++ b) agn ->
+    satFormula a agn /\ satFormula b agn.
 Proof.
   induction a; simplify;
     try apply IHa in H1; crush.
@@ -287,14 +360,14 @@ Qed.
 
 Lemma satClause_concat:
   forall a a1 a0,
-  satClause a a1 ->
-  satClause (a0 ++ a) a1.
+    satClause a a1 ->
+    satClause (a0 ++ a) a1.
 Proof. induction a0; crush. Qed.
 
 Lemma satClause_concat2:
   forall a a1 a0,
-  satClause a0 a1 ->
-  satClause (a0 ++ a) a1.
+    satClause a0 a1 ->
+    satClause (a0 ++ a) a1.
 Proof.
   induction a0; crush.
   inv H; crush.
@@ -302,8 +375,8 @@ Qed.
 
 Lemma satClause_concat3:
   forall a b c,
-  satClause (a ++ b) c ->
-  satClause a c \/ satClause b c.
+    satClause (a ++ b) c ->
+    satClause a c \/ satClause b c.
 Proof.
   induction a; crush.
   inv H; crush.
@@ -313,8 +386,8 @@ Qed.
 
 Lemma satFormula_mult':
   forall p2 a a0,
-  satFormula p2 a0 \/ satClause a a0 ->
-  satFormula (map (fun x : list lit => a ++ x) p2) a0.
+    satFormula p2 a0 \/ satClause a a0 ->
+    satFormula (map (fun x : list lit => a ++ x) p2) a0.
 Proof.
   induction p2; crush.
   - inv H. inv H0. apply satClause_concat. auto.
@@ -325,8 +398,8 @@ Qed.
 
 Lemma satFormula_mult2':
   forall p2 a a0,
-  satFormula (map (fun x : list lit => a ++ x) p2) a0 ->
-  satClause a a0 \/ satFormula p2 a0.
+    satFormula (map (fun x : list lit => a ++ x) p2) a0 ->
+    satClause a a0 \/ satFormula p2 a0.
 Proof.
   induction p2; crush.
   apply IHp2 in H1. inv H1; crush.
@@ -336,8 +409,8 @@ Qed.
 
 Lemma satFormula_mult:
   forall p1 p2 a,
-  satFormula p1 a \/ satFormula p2 a ->
-  satFormula (mult p1 p2) a.
+    satFormula p1 a \/ satFormula p2 a ->
+    satFormula (mult p1 p2) a.
 Proof.
   induction p1; crush.
   apply satFormula_concat; crush.
@@ -345,13 +418,13 @@ Proof.
   apply IHp1. auto.
   apply IHp1. auto.
   apply satFormula_mult';
-  inv H; crush.
+    inv H; crush.
 Qed.
 
 Lemma satFormula_mult2:
   forall p1 p2 a,
-  satFormula (mult p1 p2) a ->
-  satFormula p1 a \/ satFormula p2 a.
+    satFormula (mult p1 p2) a ->
+    satFormula p1 a \/ satFormula p2 a.
 Proof.
   induction p1; crush.
   apply satFormula_concat2 in H; crush.
@@ -364,19 +437,19 @@ Fixpoint trans_pred (p: pred_op) :
   {fm: formula | forall a,
       sat_predicate p a = true <-> satFormula fm a}.
   refine
-  (match p with
+    (match p with
      | Plit (b, p') => exist _ (((b, Pos.to_nat p') :: nil) :: nil) _
      | Ptrue => exist _ nil _
      | Pfalse => exist _ (nil::nil) _
      | Pand p1 p2 =>
-      match trans_pred p1, trans_pred p2 with
-      | exist _ p1' _, exist _ p2' _ => exist _ (p1' ++ p2') _
-      end
+         match trans_pred p1, trans_pred p2 with
+         | exist _ p1' _, exist _ p2' _ => exist _ (p1' ++ p2') _
+         end
      | Por p1 p2 =>
-      match trans_pred p1, trans_pred p2 with
-      | exist _ p1' _, exist _ p2' _ => exist _ (mult p1' p2') _
-      end
-   end); split; intros; simpl in *; auto; try solve [crush].
+         match trans_pred p1, trans_pred p2 with
+         | exist _ p1' _, exist _ p2' _ => exist _ (mult p1' p2') _
+         end
+     end); split; intros; simpl in *; auto; try solve [crush].
   - destruct b; auto. apply negb_true_iff in H. auto.
   - destruct b. inv H. inv H0; auto. apply negb_true_iff. inv H. inv H0; eauto. contradiction.
   - apply satFormula_concat.
@@ -492,8 +565,8 @@ Proof.
     assert
       (satFormula
          (((true, n1) :: bar l0 :: bar l1 :: nil)
-             :: (bar (true, n1) :: l0 :: nil)
-             :: (bar (true, n1) :: l1 :: nil) :: nil) c).
+            :: (bar (true, n1) :: l0 :: nil)
+            :: (bar (true, n1) :: l1 :: nil) :: nil) c).
     eapply stseytin_and_correct. unfold stseytin_and. eauto.
     unfold satLit. simpl. admit.
     inv H; try contradiction. inv H1; try contradiction. eauto.
@@ -508,15 +581,6 @@ Fixpoint max_predicate (p: pred_op) : positive :=
   | Por a b => Pos.max (max_predicate a) (max_predicate b)
   end.
 
-Fixpoint predicate_use (p: pred_op) : list positive :=
-  match p with
-  | Plit (b, p) => p :: nil
-  | Ptrue => nil
-  | Pfalse => nil
-  | Pand a b => predicate_use a ++ predicate_use b
-  | Por a b => predicate_use a ++ predicate_use b
-  end.
-
 Definition tseytin (p: pred_op) :
   {fm: formula | forall a,
       sat_predicate p a = true <-> satFormula fm a}.
@@ -529,21 +593,21 @@ Definition tseytin (p: pred_op) :
   intros. eapply xtseytin_correct; eauto. Defined.
 
 Definition tseytin_simple (p: pred_op) : formula :=
-    let m := Pos.to_nat (max_predicate p + 1) in
-    let '(m, n, fm) := xtseytin m p in
-    (n::nil) :: fm.
+  let m := Pos.to_nat (max_predicate p + 1) in
+  let '(m, n, fm) := xtseytin m p in
+  (n::nil) :: fm.
 
 Definition sat_pred_tseytin (p: pred_op) :
   ({al : alist | sat_predicate p (interp_alist al) = true}
    + {forall a : asgn, sat_predicate p a = false}).
   refine
-  ( match tseytin p with
-    | exist _ fm _ =>
-      match satSolve fm with
-      | inleft (exist _ a _) => inleft (exist _ a _)
-      | inright _ => inright _
-      end
-    end ).
+    ( match tseytin p with
+      | exist _ fm _ =>
+          match satSolve fm with
+          | inleft (exist _ a _) => inleft (exist _ a _)
+          | inright _ => inright _
+          end
+      end ).
   - apply i in s0. auto.
   - intros. specialize (n a). specialize (i a).
     destruct (sat_predicate p a). exfalso.
@@ -560,13 +624,13 @@ Definition sat_pred (p: pred_op) :
   ({al : alist | sat_predicate p (interp_alist al) = true}
    + {forall a : asgn, sat_predicate p a = false}).
   refine
-  ( match trans_pred p with
-    | exist _ fm _ =>
-      match satSolve fm with
-      | inleft (exist _ a _) => inleft (exist _ a _)
-      | inright _ => inright _
-      end
-    end ).
+    ( match trans_pred p with
+      | exist _ fm _ =>
+          match satSolve fm with
+          | inleft (exist _ a _) => inleft (exist _ a _)
+          | inright _ => inright _
+          end
+      end ).
   - apply i in s0. auto.
   - intros. specialize (n a). specialize (i a).
     destruct (sat_predicate p a). exfalso.
@@ -651,15 +715,11 @@ Proof.
 Qed.
 
 #[global]
-Instance DecidableSATSetoid : DecidableSetoid SATSetoid :=
+ Instance DecidableSATSetoid : DecidableSetoid SATSetoid :=
   { setoid_decidable := equiv_check_decidable }.
 
 #[global]
-Instance SATSetoidEqDec : EqDec SATSetoid := equiv_check_decidable2.
-
-Definition Pimplies p p' := ¬ p ∨ p'.
-
-Notation "A → B" := (Pimplies A B) (at level 30) : pred_op.
+ Instance SATSetoidEqDec : EqDec SATSetoid := equiv_check_decidable2.
 
 Definition implies p p' :=
   forall c, sat_predicate p c = true -> sat_predicate p' c = true.
@@ -674,7 +734,7 @@ Proof.
 Qed.
 
 #[global]
-Instance PimpliesProper : Proper (equiv ==> equiv ==> equiv) Pimplies.
+ Instance PimpliesProper : Proper (equiv ==> equiv ==> equiv) Pimplies.
 Proof.
   unfold Proper, "==>". simplify. unfold "→".
   intros.
@@ -684,20 +744,13 @@ Proof.
 Qed.
 
 #[global]
-Instance simplifyProper : Proper (equiv ==> equiv) simplify.
+ Instance simplifyProper : Proper (equiv ==> equiv) simplify.
 Proof.
   unfold Proper, "==>". simplify. unfold "→".
   intros. unfold sat_equiv; intros.
   rewrite ! simplify_correct; auto.
 Qed.
 
-Definition combine_pred (p1 p2: option pred_op): option pred_op :=
-  match p1, p2 with
-  | Some p1, Some p2 => Some (Pand p1 p2)
-  | Some p, _ | _, Some p => Some p
-  | None, None => None
-  end.
-
 Lemma predicate_lt :
   forall p p0,
     In p0 (predicate_use p) -> p0 <= max_predicate p.
diff --git a/src/hls/PrintAbstr.ml b/src/hls/PrintAbstr.ml
index c63fa02..c4a772e 100644
--- a/src/hls/PrintAbstr.ml
+++ b/src/hls/PrintAbstr.ml
@@ -1,18 +1,20 @@
-(**open Camlcoq
+open Camlcoq
 open Datatypes
 open Maps
 open AST
 open Abstr
 open PrintAST
 open Printf
+open Abstr
 
 let rec expr_to_list = function
   | Enil -> []
   | Econs (e, el) -> e :: expr_to_list el
 
 let res pp = function
-  | Reg r -> fprintf pp "r%d" (P.to_int r)
+  | Reg r -> fprintf pp "x%d" (P.to_int r)
   | Pred r -> fprintf pp "p%d" (P.to_int r)
+  | Exit -> fprintf pp "EXIT"
   | Mem -> fprintf pp "M"
 
 let rec print_expression pp = function
@@ -29,11 +31,29 @@ let rec print_expression pp = function
       print_expression e
   | Esetpred (c, el) ->
     fprintf pp "(%a)" (PrintOp.print_condition print_expression) (c, expr_to_list el)
+  | Eexit cf ->
+    fprintf pp "[%a]" PrintGible.print_bblock_exit cf
+
+let rec rev_index = function
+  | BinNums.Coq_xH -> Mem
+  | BinNums.Coq_xO BinNums.Coq_xH -> Exit
+  | BinNums.Coq_xI (BinNums.Coq_xI r) -> Pred r
+  | BinNums.Coq_xO (BinNums.Coq_xO r) -> Reg r
+
+let print_pred_expr = PrintGible.print_pred_op_gen print_expression
 
 let rec print_predicated pp = function
   | NE.Coq_singleton (p, e) ->
-    fprintf pp "%a %a" PrintRTLBlockInstr.print_pred_option p print_expression e
+    fprintf pp "%a %a" print_pred_expr p print_expression e
   | NE.Coq_cons ((p, e), pr) ->
-    fprintf pp "%a %a\n%a" PrintRTLBlockInstr.print_pred_option p print_expression e
+    fprintf pp "%a %a\n%a" print_pred_expr p print_expression e
       print_predicated pr
-*)
+
+let print_forest pp f =
+  fprintf pp "########################################\n";
+  List.iter
+    (function (i, y) -> fprintf pp "-- %a --\n%a\n"
+                          res (rev_index i)
+                          print_predicated y)
+    (PTree.elements f);
+  flush stdout
diff --git a/src/hls/PrintGible.ml b/src/hls/PrintGible.ml
index 16d91af..a0dbaea 100644
--- a/src/hls/PrintGible.ml
+++ b/src/hls/PrintGible.ml
@@ -22,46 +22,48 @@ let ros pp = function
   | Coq_inl r -> reg pp r
   | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
 
-let rec print_pred_op pp = function
-  | Plit p -> if fst p then pred pp (snd p) else fprintf pp "~%a" pred (snd p)
-  | Pand (p1, p2) -> fprintf pp "(%a ∧ %a)" print_pred_op p1 print_pred_op p2
-  | Por (p1, p2) -> fprintf pp "(%a ∨ %a)" print_pred_op p1 print_pred_op p2
+let rec print_pred_op_gen f pp = function
+  | Plit p -> if fst p then f pp (snd p) else fprintf pp "~%a" f (snd p)
+  | Pand (p1, p2) -> fprintf pp "(%a ∧ %a)" (print_pred_op_gen f) p1 (print_pred_op_gen f) p2
+  | Por (p1, p2) -> fprintf pp "(%a ∨ %a)" (print_pred_op_gen f) p1 (print_pred_op_gen f) p2
   | Ptrue -> fprintf pp "T"
   | Pfalse -> fprintf pp "⟂"
 
-let print_pred_option pp = function
-  | Some x -> fprintf pp "(%a)" print_pred_op x
+let print_pred_option_gen f pp = function
+  | Some x -> fprintf pp "(%a)" (print_pred_op_gen f) x
   | None -> ()
 
+let print_pred_option = print_pred_option_gen pred
+
 let print_bblock_exit pp i =
   match i with
   | RBcall(_, fn, args, res, _) ->
-      fprintf pp "%a = %a(%a)\n"
+      fprintf pp "%a = %a(%a)"
         reg res ros fn regs args;
   | RBtailcall(_, fn, args) ->
-      fprintf pp "tailcall %a(%a)\n"
+      fprintf pp "tailcall %a(%a)"
         ros fn regs args
   | RBbuiltin(ef, args, res, _) ->
-      fprintf pp "%a = %s(%a)\n"
+      fprintf pp "%a = %s(%a)"
         (print_builtin_res reg) res
         (name_of_external ef)
         (print_builtin_args reg) args
   | RBcond(cond, args, s1, s2) ->
-      fprintf pp "if (%a) goto %d else goto %d\n"
+      fprintf pp "if (%a) goto %d else goto %d"
         (PrintOp.print_condition reg) (cond, args)
         (P.to_int s1) (P.to_int s2)
   | RBjumptable(arg, tbl) ->
       let tbl = Array.of_list tbl in
-      fprintf pp "jumptable (%a)\n" reg arg;
+      fprintf pp "jumptable (%a)" reg arg;
       for i = 0 to Array.length tbl - 1 do
-        fprintf pp "\tcase %d: goto %d\n" i (P.to_int tbl.(i))
+        fprintf pp "\tcase %d: goto %d" i (P.to_int tbl.(i))
       done
   | RBreturn None ->
-      fprintf pp "return\n"
+      fprintf pp "return"
   | RBreturn (Some arg) ->
-      fprintf pp "return %a\n" reg arg
+      fprintf pp "return %a" reg arg
   | RBgoto n ->
-     fprintf pp "goto %d\n" (P.to_int n)
+     fprintf pp "goto %d" (P.to_int n)
 
 let print_bblock_body pp i =
   fprintf pp "\t\t";
@@ -86,4 +88,4 @@ let print_bblock_body pp i =
       pred p
       (PrintOp.print_condition reg) (c, args)
   | RBexit (p, cf) ->
-    fprintf pp "%a %a" print_pred_option p print_bblock_exit cf
+    fprintf pp "%a %a\n" print_pred_option p print_bblock_exit cf
diff --git a/src/hls/RTLParFU.v b/src/hls/RTLParFU.v
index f0ceafd..fe48ac5 100644
--- a/src/hls/RTLParFU.v
+++ b/src/hls/RTLParFU.v
@@ -33,6 +33,8 @@ Require Import Predicate.
 Require Import Vericertlib.
 
 Definition node := positive.
+Definition predicate := positive.
+Definition pred_op := @pred_op predicate.
 
 Inductive instr : Type :=
 | FUnop : instr
diff --git a/test/Makefile b/test/Makefile
index 58a3c12..f037cea 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -1,6 +1,6 @@
 CC ?= gcc
 VERICERT ?= vericert
-VERICERT_OPTS ?= -fschedule -fif-conv
+VERICERT_OPTS ?= -O0 -finline -fschedule -fif-conv -drtl -dgblseq -dgblpar
 IVERILOG ?= iverilog
 IVERILOG_OPTS ?=
 
-- 
cgit