Fix proof of predicates completely

2 files changed, 24 insertions, 7 deletions

diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v
index c1c5fdb..b2fdd63 100644
--- a/src/hls/GiblePargen.v
+++ b/src/hls/GiblePargen.v
@@ -279,6 +279,7 @@ Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest
       do _ <- assert_ (check_mutexcl predicated);
       do _ <- assert_ (predicated_not_in_forest p f);
       do _ <- assert_ (is_initial_pred_and_notin f p pred);
+      do _ <- assert_ (match sat_pred_simple (¬ from_predicated_inv predicated) with None => true | Some _ => false end);
       Some (pred, f #p p <- new_pred)
   | RBexit p c =>
       let new_p := simplify (negate (dfltp p) ∧ pred) in
diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v
index b3f7154..29667f1 100644
--- a/src/hls/GiblePargenproofBackward.v
+++ b/src/hls/GiblePargenproofBackward.v
@@ -417,14 +417,22 @@ Proof.
   assert (HPRED': sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps i))
     by now inv H0.
   inversion_clear HPRED' as [? ? ? HPRED].
-  destruct ti as [is_trs is_tps is_tm]. do 2 destr. inv H4. inv H1.
+  destruct ti as [is_trs is_tps is_tm]. do 3 destr. inv H4. inv H1.
   pose proof H as YH. specialize (YH src). rewrite forest_pred_gss in YH.
   inv YH; try inv H3.
   + inv H1. inv H6. replace false with (negb true) in H4 by auto.
     replace false with (negb true) in H8 by auto.
     eapply sem_pexpr_negate2 in H4. eapply sem_pexpr_negate2 in H8.
     destruct i.
-    exploit from_predicated_sem_pred_expr2. admit. admit. eauto. admit. intros.
+    exploit from_predicated_sem_pred_expr2.
+      3: eauto.
+      { eauto. }
+      { unfold assert_ in Heqo. clear Heqo2. destr. now eapply check_mutexcl_correct. } 
+      { unfold assert_ in Heqo2. repeat destr. unfold sat_pred_simple in Heqo3.
+        destruct (sat_pred_tseytin (¬ from_predicated_inv (seq_app (pred_ret (PEsetpred c)) (merge (list_translation args f))))); [destruct s; discriminate|]. rewrite <- negb_involutive. symmetry.
+        rewrite <- negb_involutive. rewrite <- eval_predf_negate. f_equal. eauto.
+      }
+      intros.
     exploit sem_pred_expr_seq_app_val2. eapply HPRED. eauto. simplify.
     inv H3. inv H15. clear H13.
     exploit sem_merge_list; eauto; intros. instantiate (1:=args) in H3.
@@ -461,7 +469,15 @@ Proof.
     * case_eq (eval_predf (is_ps i) (dfltp p)); intros.
       -- eapply sem_pexpr_eval in H3; eauto.
          destruct i.
-         exploit from_predicated_sem_pred_expr2. admit. admit. eauto. admit. intros.
+         exploit from_predicated_sem_pred_expr2.
+           3: eauto.
+           { eauto. }
+           { unfold assert_ in Heqo. clear Heqo2. destr. now apply check_mutexcl_correct. }
+           { unfold assert_ in Heqo2. repeat destr. unfold sat_pred_simple in Heqo3.
+        destruct (sat_pred_tseytin (¬ from_predicated_inv (seq_app (pred_ret (PEsetpred c)) (merge (list_translation args f))))); [destruct s; discriminate|]. rewrite <- negb_involutive. symmetry.
+        rewrite <- negb_involutive. rewrite <- eval_predf_negate. f_equal. eauto.
+      }
+           intros.
          exploit sem_pred_expr_seq_app_val2. eapply HPRED. eauto. simplify.
          inv H7. inv H15. clear H13.
          exploit sem_merge_list; eauto; intros. instantiate (1:=args) in H7.
@@ -481,7 +497,7 @@ Proof.
       -- econstructor. apply exec_RB_falsy.
          destruct p. constructor. inv H2. erewrite <- eval_predf_pr_equiv; eauto.
          easy.
-Admitted.
+Qed.
 
 Lemma evaluable_pred_expr_exists_RBexit :
   forall sp i ti p cf,
@@ -1358,10 +1374,10 @@ Proof.
     repeat destr; cbn in *; inversion_clear 1; subst; cbn in *; auto.
   inversion_clear H; destruct o; auto.
   - destruct (peq p0 x); subst.
-    + inv H0. eapply gather_predicates_fold in H1. rewrite H1 in Heqo3. discriminate.
+    + inv H0. eapply gather_predicates_fold in H1. rewrite H1 in Heqo4. discriminate.
     + rewrite PTree.gso by auto; auto.
   - destruct (peq p0 x); subst.
-    { rewrite H1 in Heqo3. inversion Heqo3. }
+    { rewrite H1 in Heqo4. inversion Heqo4. }
     rewrite PTree.gso by auto; auto.
 Qed.
 
@@ -1649,7 +1665,7 @@ Proof.
           rewrite mask_pred_map_not_in_pred; auto.
       * inv HSEM_MID. specialize (H2 x). rewrite forest_pred_gso in H2 by auto.
         destruct (preds ! x) eqn:HDESTR.
-        -- destruct u2. now rewrite mask_pred_map_in_pred.
+        -- destruct u3. now rewrite mask_pred_map_in_pred.
         -- rewrite mask_pred_map_not_in_pred; auto.
     + unfold Option.bind2, Option.bind, Option.ret in *; repeat destr.
       generalize dependent Heqo; repeat destr; intros Heqo; inv Heqo.