Finish some proofs and remove unnecessary Admitted

7 files changed, 76 insertions, 33 deletions

diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index d45587c..ac358fe 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -99,8 +99,9 @@ let compile_c_file sourcename ifile ofile =
       in
       match translation csyntax with
       | Vericert.Errors.OK v ->
-        v
+        if !Vericert.Cohpred.cohpred_counter > 0 then Printf.fprintf stderr "OK\n"; v
       | Vericert.Errors.Error msg ->
+        if !Vericert.Cohpred.cohpred_counter > 0 then Printf.fprintf stderr "OK\n";
         let loc = file_loc sourcename in
         fatal_error loc "%a"  print_error msg in
     let oc = open_out ofile in
diff --git a/lib/cohpred b/lib/cohpred
-Subproject ebcf34c3c6041cdf0c96bbf116c3622ea8df4dc
+Subproject 763f5342e01b3f749b1302e8eb124b9067746f5
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v
index b774b48..ca2d8a2 100644
--- a/src/hls/GiblePargenproof.v
+++ b/src/hls/GiblePargenproof.v
@@ -941,12 +941,54 @@ have been evaluable.
       exists ts', step_cf_instr tge ts cf t ts'
              /\ match_states s' ts'.
   Proof.
-
 (*|
 Proof Sketch:  Trivial because of structural equality.
 |*)
-
-  Admitted.
+    inversion 1; subst; clear H; inversion 1; subst; clear H.
+    - exploit find_function_translated; eauto; simplify.
+      econstructor; split.
+      + constructor; eauto using sig_transl_function.
+      + replace (rs' ## args) with (rs ## args).
+        now (repeat (constructor; auto)).
+        erewrite map_ext; auto.
+    - exploit find_function_translated; eauto; simplify.
+      econstructor; split.
+      + constructor; eauto using sig_transl_function.
+        unfold transl_function in TRANSL0. destruct_match; try discriminate.
+        inv TRANSL0. eauto.
+      + replace (rs' ## args) with (rs ## args).
+        now (repeat (constructor; auto)).
+        erewrite map_ext; auto.
+    - econstructor; split.
+      + econstructor; eauto using sig_transl_function.
+        eapply Events.eval_builtin_args_preserved; eauto.
+        eapply eval_builtin_args_eq; eauto.
+        auto.
+      + constructor; auto.
+        unfold regmap_setres; intros. destruct_match; auto.
+        subst. destruct (peq x0 x); subst.
+        * now rewrite ! PMap.gss.
+        * now rewrite ! PMap.gso by auto.
+    - econstructor; split.
+      + econstructor; eauto. eapply Op.eval_condition_lessdef; eauto.
+        replace (rs' ## args) with (rs ## args).
+        apply regs_lessdef_regs.
+        unfold regs_lessdef; auto.
+        erewrite map_ext; auto.
+        apply Mem.extends_refl.
+      + constructor; auto.
+    - econstructor; split.
+      + econstructor; eauto. now rewrite <- REG.
+      + constructor; auto.
+    - econstructor; split.
+      + econstructor; eauto. unfold transl_function in TRANSL0.
+        destruct_match; try discriminate. inv TRANSL0. eauto.
+      + replace (regmap_optget or Vundef rs') with (regmap_optget or Vundef rs).
+        constructor; auto. unfold regmap_optget. destruct_match; auto.
+    - econstructor; split.
+      + econstructor; eauto.
+      + constructor; auto.
+  Qed.
 
   Lemma match_states_stepBB :
     forall s f sp pc rs pr m sf' f' trs tps tm rs' pr' m' trs' tpr' tm',
diff --git a/src/hls/GiblePargenproofCommon.v b/src/hls/GiblePargenproofCommon.v
index 0a09c23..345836f 100644
--- a/src/hls/GiblePargenproofCommon.v
+++ b/src/hls/GiblePargenproofCommon.v
@@ -309,38 +309,38 @@ Lemma prune_predicated_mutexcl :
     predicated_mutexcl y.
 Proof.
   unfold prune_predicated; intros.
-  Admitted.
-#[local] Hint Resolve prune_predicated_mutexcl : mte.
+  Abort.
+(*#[local] Hint Resolve prune_predicated_mutexcl : mte.*)
 
 Lemma app_predicated_mutexcl :
   forall A p (x: predicated A) y,
     predicated_mutexcl x ->
     predicated_mutexcl y ->
     predicated_mutexcl (app_predicated p x y).
-Proof. Admitted.
-#[local] Hint Resolve app_predicated_mutexcl : mte.
+Proof. Abort.
+(*#[local] Hint Resolve app_predicated_mutexcl : mte.*)
 
 Lemma seq_app_predicated_mutexcl :
   forall A B (f: predicated (A -> B)) y,
     predicated_mutexcl f ->
     predicated_mutexcl y ->
     predicated_mutexcl (seq_app f y).
-Proof. Admitted.
-#[local] Hint Resolve seq_app_predicated_mutexcl : mte.
+Proof. Abort.
+(* #[local] Hint Resolve seq_app_predicated_mutexcl : mte. *)
 
 Lemma all_predicated_mutexcl:
   forall f l,
     all_mutexcl f ->
     predicated_mutexcl (merge (list_translation l f)).
-Proof. Admitted.
-#[local] Hint Resolve all_predicated_mutexcl : mte.
+Proof. Abort.
+(* #[local] Hint Resolve all_predicated_mutexcl : mte. *)
 
 Lemma flap2_predicated_mutexcl :
   forall A B C (f: predicated (A -> B -> C)) x y,
     predicated_mutexcl f ->
     predicated_mutexcl (flap2 f x y).
-Proof. Admitted.
-#[local] Hint Resolve flap2_predicated_mutexcl : mte.
+Proof. Abort.
+(* #[local] Hint Resolve flap2_predicated_mutexcl : mte. *)
 
 Lemma all_mutexcl_set :
   forall f n r,
@@ -370,11 +370,11 @@ Lemma all_mutexcl_maintained :
 Proof.
   destruct i; cbn -[seq_app]; intros; unfold Option.bind in *; repeat destr; inv H0.
   - trivial.
-  - apply prune_predicated_mutexcl in Heqo1; auto with mte.
-  - apply prune_predicated_mutexcl in Heqo0; auto with mte.
-  - apply prune_predicated_mutexcl in Heqo0; auto with mte.
-    apply app_predicated_mutexcl; auto with mte.
-  - unfold all_mutexcl; intros; rewrite forest_pred_reg; auto.
-  - unfold all_mutexcl; intros. unfold "<-e". unfold "#r". cbn.
-    fold (get_forest x f). auto.
-Qed.
+  (* - apply prune_predicated_mutexcl in Heqo1; auto with mte. *)
+  (* - apply prune_predicated_mutexcl in Heqo0; auto with mte. *)
+  (* - apply prune_predicated_mutexcl in Heqo0; auto with mte. *)
+  (*   apply app_predicated_mutexcl; auto with mte. *)
+  (* - unfold all_mutexcl; intros; rewrite forest_pred_reg; auto. *)
+  (* - unfold all_mutexcl; intros. unfold "<-e". unfold "#r". cbn. *)
+  (*   fold (get_forest x f). auto. *)
+Abort.
diff --git a/src/hls/GiblePargenproofEquiv.v b/src/hls/GiblePargenproofEquiv.v
index 91688a0..ee1c11c 100644
--- a/src/hls/GiblePargenproofEquiv.v
+++ b/src/hls/GiblePargenproofEquiv.v
@@ -1114,7 +1114,7 @@ Section SEM_PRED_EXEC.
 End SEM_PRED_EXEC.
 
 Module HashExprNorm(HS: Hashable).
-  Module H := HashTree(HS).
+  Module H := hls.HashTree.HashTree(HS).
 
   Definition norm_tree: Type := PTree.t pred_op * H.hash_tree.
 
diff --git a/src/hls/GiblePargenproofEvaluable.v b/src/hls/GiblePargenproofEvaluable.v
index 84e7200..3bb9c66 100644
--- a/src/hls/GiblePargenproofEvaluable.v
+++ b/src/hls/GiblePargenproofEvaluable.v
@@ -284,7 +284,7 @@ Proof.
   unfold predicated_prod in *. exploit all_evaluable_map_and.
   2: { eauto. }
   intros. 2: { eauto. }
-Admitted. (* Requires simple lemma to prove, but this lemma is not needed. *)
+Abort. (* Requires simple lemma to prove, but this lemma is not needed. *)
 
 Lemma cons_pred_expr_evaluable :
   forall G (ctx: @ctx G) ps a b,
@@ -294,8 +294,8 @@ Lemma cons_pred_expr_evaluable :
 Proof.
   unfold cons_pred_expr; intros.
   apply all_evaluable_predicated_map.
-  now apply all_evaluable_predicated_prod.
-Qed.
+  (*now apply all_evaluable_predicated_prod.*)
+Abort.
 
 Lemma fold_right_all_evaluable :
   forall G (ctx: @ctx G) ps n,
@@ -303,10 +303,10 @@ Lemma fold_right_all_evaluable :
     all_evaluable ctx ps (NE.fold_right cons_pred_expr (NE.singleton (T, Enil)) n).
 Proof.
   induction n; cbn in *; intros.
-  - unfold cons_pred_expr. eapply all_evaluable_predicated_map. eapply all_evaluable_predicated_prod.
-    inv H. auto. unfold all_evaluable; intros. inv H0. exists true. constructor.
-  - inv H. specialize (IHn H3). now eapply cons_pred_expr_evaluable.
-Qed.
+  - unfold cons_pred_expr. eapply all_evaluable_predicated_map. (*eapply all_evaluable_predicated_prod.
+    inv H. auto. unfold all_evaluable; intros. inv H0. exists true. constructor.*) admit.
+  - inv H. specialize (IHn H3). (*now eapply cons_pred_expr_evaluable.*)
+Abort.
 
 Lemma merge_all_evaluable :
   forall G (ctx: @ctx G) ps,
diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v
index 99dfd77..86e992a 100644
--- a/src/hls/Predicate.v
+++ b/src/hls/Predicate.v
@@ -7,7 +7,7 @@ Require Import Coq.Logic.Decidable.
 
 Require Import vericert.common.Vericertlib.
 Require Import vericert.hls.Sat.
-Require Import HashTree.
+Require Import vericert.hls.HashTree.
 
 Declare Scope pred_op.
 
@@ -603,7 +603,7 @@ Lemma stseytin_and_correct2 :
     sat_lit cur c <-> sat_lit p1 c /\ sat_lit p2 c.
 Proof.
   intros. split. intros. inv H1. unfold stseytin_and in *.
-  inv H0; try contradiction. Admitted.
+  inv H0; try contradiction. Abort.
 
 Lemma stseytin_or_correct :
   forall cur p1 p2 fm c,
@@ -625,7 +625,7 @@ Lemma stseytin_or_correct2 :
     stseytin_or cur p1 p2 = fm ->
     sat_formula fm c ->
     sat_lit cur c <-> sat_lit p1 c \/ sat_lit p2 c.
-Proof. Admitted.
+Proof. Abort.
 
 Lemma xtseytin_correct :
   forall p next l n fm c,