Add work on abstract predicates

6 files changed, 377 insertions, 96 deletions

diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index 29c6e4c..aba2fe7 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -187,7 +187,7 @@ Extract Constant GiblePargen.schedule => "Schedule.schedule_fn".
 
 (* Loop normalization *)
 Extract Constant IfConversion.build_bourdoncle => "BourdoncleAux.build_bourdoncle".
-Extract Constant IfConversion.get_if_conv_t => "(fun _ -> [Maps.PTree.empty])".
+Extract Constant IfConversion.get_if_conv_t => "(fun _ -> [Maps.PTree.empty; Maps.PTree.empty; Maps.PTree.empty])".
 
 (* Needed in Coq 8.4 to avoid problems with Function definitions. *)
 Set Extraction AccessOpaque.
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v
index 3001123..9902dc9 100644
--- a/src/hls/Abstr.v
+++ b/src/hls/Abstr.v
@@ -1,6 +1,6 @@
 (*
  * Vericert: Verified high-level synthesis.
- * Copyright (C) 2021 Yann Herklotz <yann@yannherklotz.com>
+ * Copyright (C) 2021-2022 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
  * it under the terms of the GNU General Public License as published by
@@ -17,6 +17,7 @@
  *)
 
 Require Import Coq.Logic.Decidable.
+Require Import Coq.Structures.Equalities.
 
 Require Import compcert.backend.Registers.
 Require Import compcert.common.AST.
@@ -118,6 +119,24 @@ with expression_list : Type :=
 | 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.
+
+(* Declare Scope apred_op. *)
+
+(* Notation "A ∧ B" := (Pand A B) (at level 20) : apred_op. *)
+(* Notation "A ∨ B" := (Por A B) (at level 25) : apred_op. *)
+(* Notation "⟂" := (Pfalse) : apred_op. *)
+(* Notation "'T'" := (Ptrue) : apred_op. *)
+
+(* #[local] Open Scope apred_op. *)
+
 (*Inductive pred_expr : Type :=
 | PEsingleton : option pred_op -> expression -> pred_expr
 | PEcons : option pred_op -> expression -> pred_expr -> pred_expr.*)
@@ -210,9 +229,10 @@ Import NE.NonEmptyNotation.
 
 #[local] Open Scope non_empty_scope.
 
+Definition apredicated A := NE.non_empty (apred_op * A).
 Definition predicated A := NE.non_empty (pred_op * A).
 
-Definition pred_expr := predicated expression.
+Definition apred_expr := apredicated expression.
 
 (*|
 Using ``IMap`` we can create a map from resources to any other type, as
@@ -221,11 +241,11 @@ resources can be uniquely identified as positive numbers.
 
 Module Rtree := ITree(R_indexed).
 
-Definition forest : Type := Rtree.t pred_expr.
+Definition forest : Type := Rtree.t apred_expr.
 
 Definition get_forest v (f: forest) :=
   match Rtree.get v f with
-  | None => NE.singleton (T, (Ebase v))
+  | None => NE.singleton (APtrue, (Ebase v))
   | Some v' => v'
   end.
 
@@ -324,28 +344,43 @@ with sem_val_list : ctx -> expression_list -> list val -> Prop :=
     sem_val_list ctx (Econs e l) (v :: lv)
 .
 
+Inductive eval_apred (c: ctx): apred_op -> bool -> Prop :=
+| eval_APtrue : eval_apred c APtrue true
+| eval_APfalse : eval_apred c APfalse 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_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_APor1 : forall p1 p2 b1 b2,
+  eval_apred c p1 b1 ->
+  eval_apred c p2 b2 ->
+  eval_apred c (APor p1 p2) (b1 || b2).
+
 Inductive sem_pred_expr {B: Type} (sem: ctx -> expression -> B -> Prop):
-  ctx -> pred_expr -> B -> Prop :=
+  ctx -> apred_expr -> B -> Prop :=
 | sem_pred_expr_cons_true :
   forall ctx e pr p' v,
-    eval_predf (ctx_ps ctx) pr = true ->
+    eval_apred ctx pr true ->
     sem ctx e v ->
     sem_pred_expr sem ctx ((pr, e) ::| p') v
 | sem_pred_expr_cons_false :
   forall ctx e pr p' v,
-    eval_predf (ctx_ps ctx) pr = false ->
+    eval_apred ctx pr false ->
     sem_pred_expr sem ctx p' v ->
     sem_pred_expr sem ctx ((pr, e) ::| p') v
 | sem_pred_expr_single :
   forall ctx e pr v,
-    eval_predf (ctx_ps ctx) pr = true ->
+    eval_apred ctx pr true ->
     sem ctx e v ->
     sem_pred_expr sem ctx (NE.singleton (pr, e)) v
 .
 
-Definition collapse_pe (p: pred_expr) : option expression :=
+Definition collapse_pe (p: apred_expr) : option expression :=
   match p with
-  | NE.singleton (T, p) => Some p
+  | NE.singleton (APtrue, p) => Some p
   | _ => None
   end.
 
@@ -361,13 +396,13 @@ Inductive sem_regset : ctx -> forest -> regset -> Prop :=
     (forall x, sem_pred_expr sem_value ctx (f # (Reg x)) (rs' !! x)) ->
     sem_regset ctx f rs'.
 
-Inductive sem : ctx -> forest -> instr_state * cf_instr -> Prop :=
+Inductive sem : ctx -> forest -> instr_state * option cf_instr -> Prop :=
 | Sem:
     forall ctx rs' m' f pr' cf,
     sem_regset ctx f rs' ->
     sem_predset ctx f pr' ->
     sem_pred_expr sem_mem ctx (f # Mem) m' ->
-    sem_pred_expr sem_exit ctx (f # Exit) (Some cf) ->
+    sem_pred_expr sem_exit ctx (f # Exit) cf ->
     sem ctx f (mk_instr_state rs' pr' m', cf).
 
 End SEMANTICS.
@@ -480,35 +515,49 @@ Proof.
   intros; destruct (pred_expr_item_eq pe1 pe2) eqn:?; unfold not; [tauto | now right].
 Qed.
 
-Module HashExpr <: Hashable.
+Module HashExpr' <: MiniDecidableType.
   Definition t := expression.
   Definition eq_dec := expression_dec.
-End HashExpr.
+End HashExpr'.
 
+Module HashExpr := Make_UDT(HashExpr').
 Module HT := HashTree(HashExpr).
 Import HT.
 
-Definition combine_option {A} (a b: option A) : option A :=
-  match a, b with
-  | Some a', _ => Some a'
-  | _, Some b' => Some b'
-  | _, _ => None
+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') =>
+      let (p', h') := hash_value max ap' h in
+      (Plit (b, p'), h')
+  | APand 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 =>
+      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: pred_expr) (h: hash_tree)
+Fixpoint norm_expression (max: predicate) (pe: apred_expr) (h: hash_tree)
   : (PTree.t pred_op) * hash_tree :=
   match pe with
   | NE.singleton (p, e) =>
-    let (p', h') := hash_value max e h in
-    (PTree.set p' p (PTree.empty _), h')
+    let (hashed_e, h') := hash_value max e h in
+    let (hashed_p, h'') := hash_predicate max p h' in
+    (PTree.set hashed_e hashed_p (PTree.empty _), h'')
   | (p, e) ::| pr =>
-    let (p', h') := hash_value max e h in
-    let (p'', h'') := norm_expression max pr h' in
-    match p'' ! p' with
+    let (hashed_e, h') := hash_value max e h in
+    let (norm_pr, h'') := norm_expression max pr h' in
+    let (hashed_p, h''') := hash_predicate max p h'' in
+    match norm_pr ! hashed_e with
     | Some pr_op =>
-      (PTree.set p' (pr_op ∨ p) p'', h'')
+      (PTree.set hashed_e (pr_op ∨ hashed_p) norm_pr, h''')
     | None =>
-      (PTree.set p' p p'', h'')
+      (PTree.set hashed_e hashed_p norm_pr, h''')
     end
   end.
 
@@ -534,11 +583,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 _.
 
@@ -584,7 +633,7 @@ Inductive similar {A B} : @ctx A -> @ctx B -> Prop :=
     match_states ist ist' ->
     similar (mk_ctx ist sp ge) (mk_ctx ist' sp tge).
 
-Definition beq_pred_expr_once (pe1 pe2: pred_expr) : bool :=
+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 =>
@@ -603,9 +652,9 @@ Definition beq_pred_expr_once (pe1 pe2: pred_expr) : bool :=
          end
     else false*)
   | pe1, pe2 =>
-    let max := Pos.max (max_pred_expr pe1) (max_pred_expr pe2) in
-    let (p1, h) := encode_expression max pe1 (PTree.empty _) in
-    let (p2, h') := encode_expression max pe2 h in
+    (* 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.
 
@@ -631,10 +680,8 @@ Variant sem_pred_tree {A B: Type} (sem: ctx -> expression -> B -> Prop):
       et ! e = Some expr ->
       sem_pred_tree sem ctx et pt v.
 
-Variant predicated_mutexcl {A: Type} : predicated A -> Prop :=
-| predicated_mutexcl_intros : forall pe,
-    (forall x y, NE.In x pe -> NE.In y pe -> x <> y -> fst x ⇒ ¬ fst y) ->
-    predicated_mutexcl pe.
+Definition predicated_mutexcl {A: Type} (pe: predicated A): Prop :=
+  forall x y, NE.In x pe -> NE.In y pe -> x <> y -> fst x ⇒ ¬ fst y.
 
 Lemma hash_value_in :
   forall max e et h h0,
@@ -657,15 +704,65 @@ Lemma norm_expr_constant :
 Proof. Admitted.
 
 Lemma predicated_cons :
-  forall A (a:pred_op * A) x,
+  forall A (a: pred_op * A) x,
     predicated_mutexcl (a ::| x) ->
     predicated_mutexcl x.
 Proof.
-  intros.
-  inv H. constructor; intros.
-  apply H0; auto; constructor; tauto.
+  unfold predicated_mutexcl; intros.
+  apply H; auto; constructor; tauto.
 Qed.
 
+Module Type AbstrPredSet.
+
+  Parameter apred_list : list apred_op.
+
+  Parameter h : hash_tree.
+
+  Axiom h_valid :
+    forall a,
+      In a apred_list ->
+      exists p, hash_predicate 1 a h = (p, h).
+
+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.
+
+  Instance PER_aequiv : PER sat_aequiv :=
+    { PER_Symmetric := aequiv_symm;
+      PER_Transitive := aequiv_trans;
+    }.
+
+End ABSTR_PRED.
+
+
+
+Definition hash_predicate
+
 Lemma norm_expr_mutexcl :
   forall m pe h t h' e e' p p',
     norm_expression m pe h = (t, h') ->
diff --git a/src/hls/Gible.v b/src/hls/Gible.v
index cacca85..fdc9a9d 100644
--- a/src/hls/Gible.v
+++ b/src/hls/Gible.v
@@ -251,6 +251,9 @@ Variant truthy (ps: predset): option pred_op -> Prop :=
   | truthy_None: truthy ps None
   | truthy_Some: forall p, eval_predf ps p = true -> truthy ps (Some p).
 
+Variant falsy (ps: predset): option pred_op -> Prop :=
+  | falsy_Some: forall p, eval_predf ps p = false -> falsy ps (Some p).
+
 Variant instr_falsy (ps: predset): instr -> Prop :=
   | RBop_falsy :
     forall p op args res,
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v
index da0567b..01ee2cd 100644
--- a/src/hls/GiblePargen.v
+++ b/src/hls/GiblePargen.v
@@ -211,7 +211,7 @@ Definition update (fop : option pred_op * forest) (i : instr): (option pred_op *
        (map_predicated (pred_ret (Esetpred c))
                        (merge (list_translation args f)))))
   | RBexit p c =>
-      (combine_pred (Option.map negate p) pred,
+      (combine_pred (Some (negate (Option.default T p))) pred,
         f # Exit <-
           (app_predicated (combine_pred p pred) (f # Exit) (pred_ret (Eexit c))))
   end.
@@ -224,11 +224,8 @@ code than in the RTLBlock code.
 Get a sequence from the basic block.
 |*)
 
-Fixpoint abstract_sequence (f : option pred_op * forest) (b : list instr) : option pred_op * forest :=
-  match b with
-  | nil => f
-  | i :: l => abstract_sequence (update f i) l
-  end.
+Definition abstract_sequence (b : list instr) : forest :=
+  snd (fold_left update b (None, empty)).
 
 (*|
 Check equivalence of control flow instructions.  As none of the basic blocks
@@ -255,9 +252,8 @@ Definition empty_trees (bb: SeqBB.t) (bbt: ParBB.t) : bool :=
   end.
 
 Definition schedule_oracle (bb: SeqBB.t) (bbt: ParBB.t) : bool :=
-  (check (snd (abstract_sequence (None, empty) bb))
-         (snd (abstract_sequence (None, empty) (concat (concat bbt))))) &&
-  empty_trees bb bbt.
+  (check (abstract_sequence bb) (abstract_sequence (concat (concat bbt))))
+  && empty_trees bb bbt.
 
 Definition check_scheduled_trees := beq2 schedule_oracle.
 
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v
index eaf0c32..955902c 100644
--- a/src/hls/GiblePargenproof.v
+++ b/src/hls/GiblePargenproof.v
@@ -59,6 +59,28 @@ Inductive state_lessdef : instr_state -> instr_state -> Prop :=
       (forall x, ps1 !! x = ps2 !! x) ->
       state_lessdef (mk_instr_state rs1 ps1 m1) (mk_instr_state rs2 ps2 m1).
 
+Lemma state_lessdef_refl x : state_lessdef x x.
+Proof. destruct x; constructor; auto. Qed.
+
+Lemma state_lessdef_symm x y : state_lessdef x y -> state_lessdef y x.
+Proof. destruct x; destruct y; inversion 1; subst; simplify; constructor; auto. Qed.
+
+Lemma state_lessdef_trans :
+  forall a b c,
+    state_lessdef a b ->
+    state_lessdef b c ->
+    state_lessdef a c.
+Proof.
+  inversion 1; inversion 1; subst; simplify.
+  constructor; eauto; intros. rewrite H0. auto.
+Qed.
+
+#[global] Instance Equivalence_state_lessdef : Equivalence state_lessdef :=
+  { Equivalence_Reflexive := state_lessdef_refl;
+    Equivalence_Symmetric := state_lessdef_symm;
+    Equivalence_Transitive := state_lessdef_trans;
+  }.
+
 Definition check_dest i r' :=
   match i with
   | RBop p op rl r => (r =? r')%positive
@@ -160,8 +182,8 @@ Qed.
 
 Lemma abstr_comp :
   forall l i f x x0,
-  abstract_sequence f (l ++ i :: nil) = x ->
-  abstract_sequence f l = x0 ->
+  fold_left update (l ++ i :: nil) f = x ->
+  fold_left update l f = x0 ->
   x = update x0 i.
 Proof. induction l; intros; crush; eapply IHl; eauto. Qed.
 
@@ -1036,38 +1058,6 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
       constructor; eauto.
   Qed.
 
-  (* TODO: Fix these proofs, now the cf_instr is in the State. *)
-  Lemma step_cf_instr_correct:
-    forall t s s' cf,
-      GibleSeq.step_cf_instr ge s cf t s' ->
-      forall r,
-        match_states s r ->
-        exists r', step_cf_instr tge r cf t r' /\ match_states s' r'.
-  Proof using TRANSL.
-
-    (*induction 1; repeat semantics_simpl;
-    try solve [repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp)].
-    { do 3 (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp).
-      eapply eval_builtin_args_eq. eapply REG.
-      eapply Events.eval_builtin_args_preserved. eapply symbols_preserved.
-      eauto.
-      intros.
-      unfold regmap_setres. destruct res.
-      destruct (Pos.eq_dec x0 x); subst.
-      repeat rewrite Regmap.gss; auto.
-      repeat rewrite Regmap.gso; auto.
-      eapply REG. eapply REG.
-    }
-    { repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp).
-      unfold regmap_optget. destruct or. rewrite REG. constructor; eauto.
-      constructor; eauto.
-    }
-    { exploit IHstep_cf_instr; eauto. simplify.
-      repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp).
-      erewrite eval_predf_pr_equiv; eauto.
-    }
-  Qed.*) Admitted.
-
   #[local] Hint Resolve Events.external_call_symbols_preserved : core.
   #[local] Hint Resolve eval_builtin_args_eq : core.
   #[local] Hint Resolve symbols_preserved : core.
@@ -1146,6 +1136,195 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
     eapply IHx; eauto.
   Qed.
 
+  Lemma eval_predf_negate :
+    forall ps p,
+      eval_predf ps (negate p) = negb (eval_predf ps p).
+  Proof.
+    unfold eval_predf; intros. rewrite negate_correct. auto.
+  Qed.
+
+  Lemma is_truthy_negate :
+    forall ps p pred,
+      truthy ps p ->
+      falsy ps (combine_pred (Some (negate (Option.default T p))) pred).
+  Proof.
+    inversion 1; subst; simplify.
+    - destruct pred; constructor; auto.
+    - destruct pred; constructor.
+      rewrite eval_predf_Pand. rewrite eval_predf_negate. rewrite H0. auto.
+      rewrite eval_predf_negate. rewrite H0. auto.
+  Qed.
+
+  Lemma sem_update_instr :
+    forall f i' i'' a sp p i,
+      sem (mk_ctx i sp ge) f (i', None) ->
+      step_instr ge sp (Iexec i') a (Iexec i'') ->
+      sem (mk_ctx i sp ge) (snd (update (p, f) a)) (i'', None).
+  Proof. Admitted.
+
+  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.
+
+  Lemma step_instr_lessdef :
+    forall sp a i i' ti,
+      step_instr ge sp (Iexec i) a (Iexec i') ->
+      state_lessdef i ti ->
+      exists ti', step_instr ge sp (Iexec ti) a (Iexec ti') /\ state_lessdef i' ti'.
+  Proof. Admitted.
+
+  Lemma step_instr_lessdef_term :
+    forall sp a i i' ti cf,
+      step_instr ge sp (Iexec i) a (Iterm i' cf) ->
+      state_lessdef i ti ->
+      exists ti', step_instr ge sp (Iexec ti) a (Iterm ti' cf) /\ state_lessdef i' ti'.
+  Proof. Admitted.
+
+  Lemma app_predicated_semregset :
+    forall A ctx o f res r y,
+      @sem_regset A ctx f res ->
+      falsy (ctx_ps ctx) o ->
+      @sem_regset A ctx f # r <- (app_predicated o f#r y) res.
+  Proof.
+    inversion 1; subst; crush.
+    constructor; intros.
+    destruct (resource_eq r (Reg x)); subst.
+    + rewrite map2; eauto. unfold app_predicated. inv H1. admit.
+    + rewrite genmap1; auto.
+  Admitted.
+
+  Lemma app_predicated_sempredset :
+    forall A ctx o f rs r y ps,
+      @sem_predset A ctx f rs ->
+      falsy ps o ->
+      @sem_predset A ctx f # r <- (app_predicated o f#r y) rs.
+  Proof. Admitted.
+
+  Lemma app_predicated_sem :
+    forall A ctx o f i cf r y,
+      @sem A ctx f (i, cf) ->
+      falsy (is_ps i) o ->
+      @sem A ctx f # r <- (app_predicated o f#r y) (i, cf).
+  Proof.
+    inversion 1; subst; crush.
+    constructor.
+  Admitted.
+
+  Lemma combined_falsy :
+    forall i o1 o,
+      falsy i o1 ->
+      falsy i (combine_pred o o1).
+  Proof.
+    inversion 1; subst; crush. destruct o; simplify.
+    constructor. rewrite eval_predf_Pand. rewrite H0. crush.
+    constructor. auto.
+  Qed.
+
+  Lemma falsy_update :
+    forall f a ps,
+      falsy ps (fst f) ->
+      falsy ps (fst (update f a)).
+  Proof.
+    destruct f; destruct a; inversion 1; subst; crush.
+    rewrite <- H1. constructor. unfold Option.default. destruct o0.
+    rewrite eval_predf_Pand. rewrite H0. crush. crush.
+  Qed.
+
+  Lemma abstr_fold_falsy :
+    forall x i0 sp cf i f,
+    sem (mk_ctx i0 sp ge) (snd f) (i, cf) ->
+    falsy (is_ps i) (fst f) ->
+    sem (mk_ctx i0 sp ge) (snd (fold_left update x f)) (i, cf).
+  Proof.
+    induction x; crush.
+    eapply IHx.
+    destruct a; destruct f; crush;
+      try solve [eapply app_predicated_sem; eauto; apply combined_falsy; auto].
+    now apply falsy_update.
+  Qed.
+
+  Lemma state_lessdef_sem :
+    forall i sp f i' ti cf,
+      sem (mk_ctx i sp ge) f (i', cf) ->
+      state_lessdef i ti ->
+      exists ti', sem (mk_ctx ti sp ge) f (ti', cf) /\ state_lessdef i' ti'.
+  Proof. Admitted.
+
+  Lemma abstr_fold_correct :
+    forall sp x i i' i'' cf f,
+      SeqBB.step ge sp (Iexec i') x (Iterm i'' cf) ->
+      sem (mk_ctx i sp ge) (snd f) (i', None) ->
+      forall ti,
+        state_lessdef i ti ->
+        exists ti', sem (mk_ctx ti sp ge) (snd (fold_left update x f)) (ti', Some cf)
+               /\ state_lessdef i'' ti'.
+  Proof.
+    induction x; simplify; inv H.
+    - destruct f; exploit IHx; eauto; eapply sem_update_instr; eauto.
+    - destruct f. inversion H5; subst.
+      exploit state_lessdef_sem; eauto; intros. inv H. inv H2.
+      exploit step_instr_lessdef_term; eauto; intros. inv H2. inv H4.
+      exploit sem_update_instr_term; eauto; intros. inv H4.
+      eexists; split. eapply abstr_fold_falsy; eauto.
+      auto.
+  Qed.
+
+  Lemma sem_regset_empty :
+    forall A ctx, @sem_regset A ctx empty (ctx_rs ctx).
+  Proof.
+    intros; constructor; intros.
+    constructor; auto. constructor.
+  Qed.
+
+  Lemma sem_predset_empty :
+    forall A ctx, @sem_predset A ctx empty (ctx_ps ctx).
+  Proof.
+    intros; constructor; intros.
+    constructor; auto. constructor.
+  Qed.
+
+  Lemma sem_empty :
+    forall A ctx, @sem A ctx empty (ctx_is ctx, None).
+  Proof.
+    intros. destruct ctx. destruct ctx_is.
+    constructor; try solve [constructor; constructor; crush].
+    eapply sem_regset_empty.
+    eapply sem_predset_empty.
+  Qed.
+
+  Lemma abstr_sequence_correct :
+    forall sp x i i'' cf,
+      SeqBB.step ge sp (Iexec i) x (Iterm i'' cf) ->
+      forall ti,
+        state_lessdef i ti ->
+        exists ti', sem (mk_ctx ti sp ge) (abstract_sequence x) (ti', Some cf)
+               /\ state_lessdef i'' ti'.
+  Proof.
+    unfold abstract_sequence. intros; eapply abstr_fold_correct; eauto.
+    simplify. eapply sem_empty.
+  Qed.
+
+  Lemma abstr_check_correct :
+    forall sp i i' a b cf ti,
+      check a b = true ->
+      sem (mk_ctx i sp ge) a (i', cf) ->
+      state_lessdef i ti ->
+      exists ti', sem (mk_ctx ti sp ge) b (ti', cf)
+             /\ state_lessdef i' ti'.
+  Proof. Admitted.
+
+  Lemma abstr_seq_reverse_correct :
+    forall sp x i i' ti cf,
+    sem (mk_ctx i sp ge) (abstract_sequence x) (i', (Some cf)) ->
+    state_lessdef i ti ->
+    exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf)
+           /\ state_lessdef i' ti'.
+  Proof. Admitted.
+
   Lemma schedule_oracle_correct :
     forall x y sp i i' ti cf,
       schedule_oracle x y = true ->
@@ -1153,7 +1332,16 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
       state_lessdef i ti ->
       exists ti', ParBB.step tge sp (Iexec ti) y (Iterm ti' cf)
              /\ state_lessdef i' ti'.
-  Proof. Admitted.
+  Proof.
+    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.
+    exploit seqbb_step_parbb_step; eauto; intros.
+    econstructor; split; eauto.
+    etransitivity; eauto.
+    etransitivity; eauto.
+  Qed.
 
   Lemma step_cf_correct :
     forall cf ts s s' t,
diff --git a/src/hls/HashTree.v b/src/hls/HashTree.v
index f3c57a8..9f9ec81 100644
--- a/src/hls/HashTree.v
+++ b/src/hls/HashTree.v
@@ -1,6 +1,6 @@
 (*
  * Vericert: Verified high-level synthesis.
- * Copyright (C) 2021 Yann Herklotz <yann@yannherklotz.com>
+ * Copyright (C) 2021-2022 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
  * it under the terms of the GNU General Public License as published by
@@ -16,6 +16,8 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
+Require Import Coq.Structures.Equalities.
+
 Require Import compcert.lib.Maps.
 
 Require Import vericert.common.Vericertlib.
@@ -136,12 +138,7 @@ Proof.
   eapply IHl. eauto.
 Qed.
 
-Module Type Hashable.
-
-  Parameter t: Type.
-  Parameter eq_dec: forall (t1 t2: t), {t1 = t2} + {t1 <> t2}.
-
-End Hashable.
+Module Type Hashable := UsualDecidableType.
 
 Module HashTree(H: Hashable).