Add SMTCoq solver as dependency

14 files changed, 233 insertions, 71 deletions

diff --git a/Makefile b/Makefile
index 3d8dfff..a600d53 100644
--- a/Makefile
+++ b/Makefile
@@ -15,22 +15,8 @@ COQINCLUDES := -R src vericert \
                $(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d)) \
                -R lib/CompCert/flocq Flocq \
                -R lib/CompCert/MenhirLib MenhirLib \
-               -R src TVSMT \
-               -R lib/cohpred/smtcoq/src SMTCoq \
-               -I lib/smtcoq/src \
-               -I lib/smtcoq/src/bva \
-               -I lib/smtcoq/src/classes \
-               -I lib/smtcoq/src/array \
-               -I lib/smtcoq/src/cnf \
-               -I lib/smtcoq/src/euf \
-               -I lib/smtcoq/src/lfsc \
-               -I lib/smtcoq/src/lia \
-               -I lib/smtcoq/src/smtlib2 \
-               -I lib/smtcoq/src/trace \
-               -I lib/smtcoq/src/verit \
-               -I lib/smtcoq/src/zchaff \
-               -I lib/smtcoq/src/PArray \
-               -I lib/smtcoq/src/../3rdparty/alt-ergo
+               -R lib/cohpred/theory cohpred_theory \
+               -R lib/cohpred/smtcoq/src SMTCoq
 
 
 COQEXEC := $(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source
diff --git a/dune b/dune
index 3ad2811..aa082a3 100644
--- a/dune
+++ b/dune
@@ -1,11 +1,8 @@
-(dirs :standard \ "./lib/CompCert/x86_32" "./lib/CompCert/cfrontend" "./lib/CompCert/powerpc" "./lib/CompCert/riscV"
-      "./lib/CompCert/arm" "./lib/CompCert/aarch64" "./lib/CompCert/extraction"
-      "./lib/CompCert/x86" "./lib/CompCert/x86_64")
-
 (include_subdirs unqualified)
 
 (library
  (public_name vericert)
  (modules_without_implementation c debugTypes dwarfTypes)
- (libraries menhirLib str unix ocamlgraph)
+ (modules (:standard \ driver gCC deLexer))
+ (libraries menhirLib str unix ocamlgraph coq-smtcoq)
  (flags (:standard -warn-error -A -w -8-9-16-20-26-27-32..36-39-41-44..45-50-60-67)))
diff --git a/lib/CompCert b/lib/CompCert
-Subproject ab617cf8e6e60e8de3eb8de220f71dd05c18209
+Subproject 504b0c12ad945e394375dcfb52cc503d9574708
diff --git a/lib/cohpred b/lib/cohpred
-Subproject 66a63543cd9d7612b4f51bd8c27433232f18ded
+Subproject ebcf34c3c6041cdf0c96bbf116c3622ea8df4dc
diff --git a/src/Compiler.v b/src/Compiler.v
index 5ff291e..2fb909e 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -55,6 +55,7 @@ Require Import compcert.common.Errors.
 Require Import compcert.common.Linking.
 Require Import compcert.common.Smallstep.
 Require Import compcert.lib.Coqlib.
+Require Import compcert.lib.Maps.
 
 Require vericert.hls.Verilog.
 Require vericert.hls.Veriloggen.
@@ -279,7 +280,7 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
    @@ print (print_GibleSeq 0)
    @@ total_if HLSOpts.optim_if_conversion CondElim.transf_program
    @@ print (print_GibleSeq 1)
-   @@ total_if HLSOpts.optim_if_conversion (fold_left (fun a b => IfConversion.transf_program b a) (Maps.PTree.empty _ :: Maps.PTree.empty _ :: nil))
+   @@ total_if HLSOpts.optim_if_conversion (fold_left (fun a b => IfConversion.transf_program b a) (PTree.empty _ :: PTree.empty _ :: nil))
    @@ print (print_GibleSeq 2)
   @@@ DeadBlocks.transf_program
    @@ print (print_GibleSeq 3)
diff --git a/src/bourdoncle/BourdoncleAux.ml b/src/bourdoncle/BourdoncleAux.ml
index 1ea4de6..932bb18 100644
--- a/src/bourdoncle/BourdoncleAux.ml
+++ b/src/bourdoncle/BourdoncleAux.ml
@@ -20,7 +20,7 @@ let positive_of_int n = P.of_int (n+1)
 
 (* Functions copied from SliceToString to avoid mutual inclusion *)
 let nodeToString (p : P.t) : string =
-  Int.to_string (P.to_int p)
+  string_of_int (P.to_int p)
 let rec cleanListToString' (aToString: 'a -> string) (l : 'a list) =
   match l with
   | [] -> ""
diff --git a/src/dune b/src/dune
new file mode 100644
index 0000000..fdcb9fd
--- /dev/null
+++ b/src/dune
@@ -0,0 +1 @@
+(dirs (:standard \ pipelining))
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index 20fc48c..b65bc41 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -55,9 +55,13 @@ From compcert Require
     Parser
     Initializers.
 
+From cohpred_theory Require
+    Smtpredicate.
+
 (* Standard lib *)
 Require Import ExtrOcamlBasic.
 Require Import ExtrOcamlString.
+Require Import ExtrOCamlInt63.
 
 (* Coqlib *)
 Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)".
@@ -172,7 +176,7 @@ Extract Constant Cabs.char_code => "int64".
 Load extractionMachdep.
 
 (* Avoid name clashes *)
-Extraction Blacklist List String Int.
+Extraction Blacklist List String Int Uint63.
 
 (* Cutting the dependency to R. *)
 Extract Inlined Constant Defs.F2R => "fun _ -> assert false".
@@ -185,6 +189,8 @@ Extract Constant GibleSeqgen.partition => "Partition.partition".
 Extract Constant GiblePargen.schedule => "Schedule.schedule_fn".
 Extract Constant Abstr.print_forest => "(PrintAbstr.print_forest stdout)".
 
+Extract Constant Smtpredicate.pred_verit_unsat => "Cohpred.smt_certificate".
+
 (* Loop normalization *)
 Extract Constant IfConversion.build_bourdoncle => "BourdoncleAux.build_bourdoncle".
 (*Extract Constant IfConversion.get_if_conv_t => "(fun _ -> [Maps.PTree.empty; Maps.PTree.empty; Maps.PTree.empty])".*)
@@ -202,6 +208,8 @@ Separate Extraction
          Verilog.stmnt_to_list
          Bourdoncle.bourdoncle
 
+   Smtpredicate.check_smt_total
+
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
    Ctypes.merge_attributes Ctypes.remove_attributes 
diff --git a/src/hls/DeadBlocksproof.v b/src/hls/DeadBlocksproof.v
index 8ac6d0d..1783213 100644
--- a/src/hls/DeadBlocksproof.v
+++ b/src/hls/DeadBlocksproof.v
@@ -3,30 +3,32 @@ both that the transformation ensures that generated functions are
 satisfying the predicate [wf_dfs_function] and that the transformation
 preserves the semantics. *)
 
-Require Recdef.
-Require Import FSets.
-Require Import Coqlib.
-Require Import Ordered.
-Require Import Errors.
-Require Import Maps.
-Require Import AST.
-Require Import Integers.
-Require Import Values.
-Require Import Globalenvs.
-Require Import Op.
-Require Import Registers.
-Require Import Smallstep.
-Require Import DeadBlocks.
-Require Import Kildall.
-Require Import Conventions.
-Require Import Integers.
-Require Import Floats.
-Require Import Utils.
-Require Import Events.
-Require Import Gible.
-Require Import GibleSeq.
-Require Import Relation_Operators.
-Require Import Vericertlib.
+From Coq Require funind.Recdef.
+From Coq Require Import FSets.FSets.
+From Coq Require Import Program.Utils.
+From Coq Require Import Relation_Operators.
+
+From compcert Require Import Errors.
+From compcert Require Import Maps.
+From compcert Require Import AST.
+From compcert Require Import Integers.
+From compcert Require Import Values.
+From compcert Require Import Globalenvs.
+From compcert Require Import Op.
+From compcert Require Import Registers.
+From compcert Require Import Smallstep.
+From compcert Require Import Kildall.
+From compcert Require Import Conventions.
+From compcert Require Import Integers.
+From compcert Require Import Floats.
+From compcert Require Import Events.
+From compcert Require Import Ordered.
+From compcert Require Import Coqlib.
+
+From vericert Require Import DeadBlocks.
+From vericert Require Import Gible.
+From vericert Require Import GibleSeq.
+From vericert Require Import Vericertlib.
 
 Unset Allow StrictProp.
 
diff --git a/src/hls/Gible.v b/src/hls/Gible.v
index cb080c5..b8feb37 100644
--- a/src/hls/Gible.v
+++ b/src/hls/Gible.v
@@ -39,8 +39,8 @@ Require Import compcert.common.Smallstep.
 Require Import compcert.lib.Maps.
 Require Import compcert.verilog.Op.
 
-Require Import Predicate.
-Require Import Vericertlib.
+Require Import vericert.hls.Predicate.
+Require Import vericert.common.Vericertlib.
 
 Definition node := positive.
 Definition predicate := positive.
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v
index 736f461..25531a8 100644
--- a/src/hls/GiblePargen.v
+++ b/src/hls/GiblePargen.v
@@ -26,8 +26,11 @@ Require Import compcert.common.Values.
 Require Import compcert.lib.Floats.
 Require Import compcert.lib.Integers.
 Require Import compcert.lib.Maps.
+Require compcert.common.Errors.
 Require compcert.verilog.Op.
 
+Module Err := compcert.common.Errors.
+
 Require Import vericert.common.Vericertlib.
 Require Import vericert.common.Monad.
 Require Import vericert.hls.GibleSeq.
@@ -464,19 +467,19 @@ Top-level Functions
 Parameter schedule : GibleSeq.function -> GiblePar.function.
 
 Definition transl_function (f: GibleSeq.function)
-  : Errors.res GiblePar.function :=
+  : Err.res GiblePar.function :=
   let tfcode := fn_code (schedule f) in
   if check_scheduled_trees f.(GibleSeq.fn_code) tfcode then
-    Errors.OK (mkfunction f.(GibleSeq.fn_sig)
+    Err.OK (mkfunction f.(GibleSeq.fn_sig)
                           f.(GibleSeq.fn_params)
                           f.(GibleSeq.fn_stacksize)
                           tfcode
                           f.(GibleSeq.fn_entrypoint))
   else
-    Errors.Error
-      (Errors.msg "GiblePargen: Could not prove the blocks equivalent.").
+    Err.Error
+      (Err.msg "GiblePargen: Could not prove the blocks equivalent.").
 
 Definition transl_fundef := transf_partial_fundef transl_function.
 
-Definition transl_program (p : GibleSeq.program) : Errors.res GiblePar.program :=
+Definition transl_program (p : GibleSeq.program) : Err.res GiblePar.program :=
   transform_partial_program transl_fundef p.
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v
index 5d36ae9..b774b48 100644
--- a/src/hls/GiblePargenproof.v
+++ b/src/hls/GiblePargenproof.v
@@ -127,7 +127,7 @@ Qed.
 Definition state_lessdef := GiblePargenproofEquiv.match_states.
 
 Definition match_prog (prog : GibleSeq.program) (tprog : GiblePar.program) :=
-  match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog.
+  match_program (fun cu f tf => transl_fundef f = OK tf) eq prog tprog.
 
 (* TODO: Fix the `bb` and add matches for them. *)
 Inductive match_stackframes: GibleSeq.stackframe -> GiblePar.stackframe -> Prop :=
@@ -177,7 +177,7 @@ Section CORRECTNESS.
     forall (b: Values.block) (f: GibleSeq.fundef),
       Genv.find_funct_ptr ge b = Some f ->
       exists tf,
-        Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Errors.OK tf.
+        Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf.
   Proof using TRANSL.
     intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto.
     intros (cu & tf & P & Q & R); exists tf; auto.
@@ -187,7 +187,7 @@ Section CORRECTNESS.
     forall (v: Values.val) (f: GibleSeq.fundef),
       Genv.find_funct ge v = Some f ->
       exists tf,
-        Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf.
+        Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf.
   Proof using TRANSL.
     intros. exploit (Genv.find_funct_match TRANSL); eauto.
     intros (cu & tf & P & Q & R); exists tf; auto.
diff --git a/src/hls/GiblePargenproofEquiv.v b/src/hls/GiblePargenproofEquiv.v
index 9e58981..1f3ad1c 100644
--- a/src/hls/GiblePargenproofEquiv.v
+++ b/src/hls/GiblePargenproofEquiv.v
@@ -41,6 +41,9 @@ Require vericert.common.NonEmpty.
 Module NE := NonEmpty.
 Import NE.NonEmptyNotation.
 
+Module OE := MonadExtra(Option).
+Import OE.MonadNotation.
+
 #[local] Open Scope non_empty_scope.
 #[local] Open Scope positive.
 #[local] Open Scope pred_op.
@@ -482,12 +485,50 @@ Proof.
   apply X.
 Defined.
 
-Definition beq_pred_pexpr (pe1 pe2: pred_pexpr): bool :=
+Require cohpred_theory.Predicate.
+Require cohpred_theory.Smtpredicate.
+Module TV := cohpred_theory.Predicate.
+Module STV := cohpred_theory.Smtpredicate.
+
+Module TVL := TV.ThreeValued(PHashExpr).
+
+Fixpoint transf_pred_op {A} (p: @Predicate.pred_op A): @TV.pred A :=
+  match p with
+  | Ptrue => TV.Ptrue
+  | Pfalse => TV.Pfalse
+  | Plit (b, p) =>
+    if b then TV.Pbase p else TV.Pnot (TV.Pbase p)
+  | Pand p1 p2 =>
+    TV.Pand (transf_pred_op p1) (transf_pred_op p2)
+  | Por p1 p2 =>
+    TV.Por (transf_pred_op p1) (transf_pred_op p2)
+  end.
+
+(*|
+This following equivalence checker takes two pred_pexpr, hashes them, and then
+proves them equivalent.  However, it's not quite clear whether this actually
+proves that, given that ``pe1`` results in a value, then ``pe2`` will also
+result in a value.  The issue is that even though this proves that both hashed
+predicates will result in the same value, how do we then show that the initial
+predicates will also be correct and equivalent.
+|*)
+
+Definition beq_pred_pexpr' (pe1 pe2: pred_pexpr): bool :=
   if pred_pexpr_eqb pe1 pe2 then true else
   let (np1, h) := hash_predicate 1 pe1 (PTree.empty _) in
   let (np2, h') := hash_predicate 1 pe2 h in
   equiv_check np1 np2.
 
+(*|
+Given two predicated expressions, prove that they are equivalent.
+|*)
+
+Definition beq_pred_pexpr (pe1 pe2: pred_pexpr): bool :=
+  if pred_pexpr_eqb pe1 pe2 then true else
+  let (np1, h) := TVL.hash_predicate (transf_pred_op pe1) (Maps.PTree.empty _) in
+  let (np2, h') := TVL.hash_predicate (transf_pred_op pe2) h in
+  STV.check_smt_total (TV.equiv np1 np2).
+
 Lemma inj_asgn_eg : forall a b, (a =? b)%positive = (a =? a)%positive -> a = b.
 Proof.
   intros. destruct (peq a b); subst.
@@ -815,7 +856,7 @@ Section CORRECT.
         apply sem_pred_expr_cons_false; auto.
         now apply sem_pexpr_corr.
   Qed.
-  
+
   Lemma sem_pred_expr_corr :
     forall A B (sem: forall G, @Abstr.ctx G -> A -> B -> Prop) a p r,
       (forall x y, sem _ ictx x y -> sem _ octx x y) ->
@@ -870,7 +911,7 @@ Section SEM_PRED_EXEC.
       + apply IHp2 in H. solve [constructor; auto].
       + apply IHp1 in H2. apply IHp2 in H4. solve [constructor; auto].
   Qed.
-  
+
   Lemma sem_pexpr_negate2 :
     forall p b,
       sem_pexpr ctx (¬ p) (negb b) ->
@@ -1127,7 +1168,7 @@ Module HashExprNorm(HS: Hashable).
     | Some p' => equiv_check p p'
     | None => equiv_check p ⟂
     end.
-  
+
   Definition tree_equiv_check_None_el (np2: PTree.t pred_op) (n: positive) (p: pred_op): bool :=
     match np2 ! n with
     | Some p' => true
@@ -1230,7 +1271,7 @@ Module HashExprNorm(HS: Hashable).
       + rewrite PTree.gso in H2 by auto. now rewrite PTree.gempty in H2.
     - assert (H.wf_hash_table h1) by eauto using H.wf_hash_table_distr.
       destruct_match; inv H0.
-      + destruct (peq h0 x); subst; eauto. 
+      + destruct (peq h0 x); subst; eauto.
         rewrite PTree.gso in H1 by auto. eauto.
       + destruct (peq h0 x); subst; eauto.
         * pose proof Heqp0 as X.
@@ -1660,15 +1701,138 @@ Proof.
     specialize (H1 h br).
 Abort.
 
+Local Open Scope monad_scope.
+Fixpoint sem_valueF (e: expression) : option val :=
+  match e with
+  | Ebase (Reg r) => Some ((ctx_rs ctx) !! r)
+  | Eop op args =>
+    do lv <- sem_val_listF args;
+    Op.eval_operation (ctx_ge ctx) (ctx_sp ctx) op lv (ctx_mem ctx)
+  | Eload chunk addr args mexp =>
+    do m' <- sem_memF mexp;
+    do lv <- sem_val_listF args;
+    do a <- Op.eval_addressing (ctx_ge ctx) (ctx_sp ctx) addr lv;
+    Mem.loadv chunk m' a
+  | _ => None
+  end
+with sem_memF (e: expression) : option mem :=
+  match e with
+  | Ebase Mem => Some (ctx_mem ctx)
+  | Estore vexp chunk addr args mexp =>
+    do m' <- sem_memF mexp;
+    do v <- sem_valueF vexp;
+    do lv <- sem_val_listF args;
+    do a <- Op.eval_addressing (ctx_ge ctx) (ctx_sp ctx) addr lv;
+    Mem.storev chunk m' a v
+  | _ => None
+  end
+with sem_val_listF (e: expression_list) : option (list val) :=
+  match e with
+  | Enil => Some nil
+  | Econs e l =>
+    do v <- sem_valueF e;
+    do lv <- sem_val_listF l;
+    Some (v :: lv)
+  end.
+
+Definition sem_predF (e: pred_expression): option bool :=
+  match e with
+  | PEbase p => Some ((ctx_ps ctx) !! p)
+  | PEsetpred c args =>
+    do lv <- sem_val_listF args;
+    Op.eval_condition c lv (ctx_mem ctx)
+  end.
+Local Close Scope monad_scope.
+
+Definition sem_pexprF := TVL.eval_predicate sem_predF.
+
+Lemma sem_valueF_correct :
+  forall e v m,
+    (sem_valueF e = Some v -> sem_value ctx e v)
+    /\ (sem_memF e = Some m -> sem_mem ctx e m).
+Proof.
+  induction e using expression_ind2 with
+    (P0 := fun p => forall l, sem_val_listF p = Some l -> sem_val_list ctx p l); intros.
+  - split; intros; destruct r; try discriminate; cbn in *; inv H; constructor.
+  - split; intros.
+    + cbn in *; unfold Option.bind in *; destruct_match; try discriminate.
+      econstructor; eauto.
+    + cbn in *. discriminate.
+  - split; intros; cbn in *; try discriminate; unfold Option.bind in *;
+      repeat (destruct_match; try discriminate; []).
+    econstructor; eauto. eapply IHe0; auto.
+  - split; intros; cbn in *; try discriminate; unfold Option.bind in *;
+      repeat (destruct_match; try discriminate; []).
+    econstructor; eauto. eapply IHe3; eauto. eapply IHe1; eauto.
+  - cbn in *. inv H. constructor.
+  - cbn in *; unfold Option.bind in *;
+      repeat (destruct_match; try discriminate; []). inv H. constructor; eauto.
+      eapply IHe; auto. apply (ctx_mem ctx).
+Qed.
+
+Lemma sem_val_listF_correct :
+  forall l vl,
+    sem_val_listF l = Some vl ->
+    sem_val_list ctx l vl.
+Proof.
+  induction l.
+  - intros. cbn in *. inv H. constructor.
+  - cbn; intros. unfold Option.bind in *;
+      repeat (destruct_match; try discriminate; []). inv H. constructor; eauto.
+    eapply sem_valueF_correct; eauto. apply (ctx_mem ctx).
+Qed.
+
+Lemma sem_valueF_correct2 :
+  forall e v m,
+    (sem_value ctx e v -> sem_valueF e = Some v)
+    /\ (sem_mem ctx e m -> sem_memF e = Some m).
+Proof.
+  induction e using expression_ind2 with
+    (P0 := fun p => forall l, sem_val_list ctx p l -> sem_val_listF p = Some l); intros.
+  - split; inversion 1; cbn; auto.
+  - split; inversion 1; subst; clear H. cbn; unfold Option.bind.
+    erewrite IHe; eauto.
+  - split; inversion 1; subst; clear H. cbn; unfold Option.bind.
+    specialize (IHe0 v m'). inv IHe0.
+    erewrite H0; eauto. erewrite IHe; eauto. rewrite H8; auto.
+  - split; inversion 1; subst; clear H. cbn; unfold Option.bind.
+    specialize (IHe3 v0 m'); inv IHe3.
+    specialize (IHe1 v0 m'); inv IHe1.
+    erewrite H0; eauto.
+    erewrite H1; eauto.
+    erewrite IHe2; eauto.
+    rewrite H10; auto.
+  - inv H. auto.
+  - inv H. cbn; unfold Option.bind.
+    specialize (IHe v (ctx_mem ctx)). inv IHe.
+    erewrite H; eauto.
+    erewrite IHe0; eauto.
+Qed.
+
+Lemma sem_val_listF_correct2 :
+  forall l vl,
+    sem_val_list ctx l vl ->
+    sem_val_listF l = Some vl.
+Proof.
+  induction l.
+  - inversion 1; subst; auto.
+  - inversion 1; subst; clear H.
+    specialize (sem_valueF_correct2 e v (ctx_mem ctx)); inversion 1; clear H.
+    cbn; unfold Option.bind. erewrite H0; eauto. erewrite IHl; eauto.
+Qed.
+
+(* Definition eval_pexpr_atom {G} (ctx: @Abstr.ctx G)  (p: pred_expression) := *)
+
 Lemma sem_pexpr_beq_correct :
-  forall p1 p2 b,
+  forall p1 p2,
     beq_pred_pexpr p1 p2 = true ->
-    sem_pexpr ctx p1 b ->
-    sem_pexpr ctx p2 b.
+    sem_pexprF (transf_pred_op p1) = sem_pexprF (transf_pred_op p2).
 Proof.
-  unfold beq_pred_pexpr.
-  induction p1; intros; destruct_match; crush.
-  Admitted.
+  unfold beq_pred_pexpr; intros.
+  destruct_match; subst; auto.
+  repeat destruct_match.
+  pose proof STV.valid_check_smt_total.
+  unfold sem_pexprF.
 
 (*|
 This should only require a proof of sem_pexpr_beq_correct, the rest is
diff --git a/src/hls/RTLParFU.v b/src/hls/RTLParFU.v
index b677be7..b28c0ee 100644
--- a/src/hls/RTLParFU.v
+++ b/src/hls/RTLParFU.v
@@ -29,8 +29,8 @@ Require Import compcert.lib.Maps.
 Require Import compcert.verilog.Op.
 
 Require Import vericert.hls.FunctionalUnits.
-Require Import Predicate.
-Require Import Vericertlib.
+Require Import vericert.hls.Predicate.
+Require Import vericert.common.Vericertlib.
 
 Definition node := positive.
 Definition predicate := positive.