Add SMTCoq solver as dependency

6 files changed, 216 insertions, 47 deletions

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.