diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-10-26 20:24:12 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-10-26 20:24:12 +0100 |
commit | e51e42283ac9f1f0a80c989ebca7d52eb35f08d3 (patch) | |
tree | e4e9615be7869348d6c3b1cbbc00bc92cfb7675c /src/hls | |
parent | b1ca2f1a6159a313e259a697826380962d7cfa48 (diff) | |
download | vericert-e51e42283ac9f1f0a80c989ebca7d52eb35f08d3.tar.gz vericert-e51e42283ac9f1f0a80c989ebca7d52eb35f08d3.zip |
Work more on equivalence of SAT
Diffstat (limited to 'src/hls')
-rw-r--r-- | src/hls/Abstr.v | 154 | ||||
-rw-r--r-- | src/hls/Predicate.v | 15 | ||||
-rw-r--r-- | src/hls/PrintVerilog.ml | 2 |
3 files changed, 137 insertions, 34 deletions
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index ec8fd36..fd7c910 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -16,6 +16,8 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) +Require Import Coq.Logic.Decidable. + Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Globalenvs. @@ -281,10 +283,33 @@ Fixpoint of_list {A} (l: list A): option (non_empty A) := | nil => None end. +Fixpoint replace {A} (f: A -> A -> bool) (a b: A) (l: non_empty A) := + match l with + | a' ::| l' => if f a a' then b ::| replace f a b l' else a' ::| replace f a b l' + | singleton a' => if f a a' then singleton b else singleton a' + end. + Inductive In {A: Type} (x: A) : non_empty A -> Prop := | In_cons : forall a b, x = a \/ In x b -> In x (a ::| b) | In_single : In x (singleton x). +Lemma in_dec: + forall A (a: A) (l: non_empty A), + (forall a b: A, {a = b} + {a <> b}) -> + {In a l} + {~ In a l}. +Proof. + induction l; intros. + { specialize (X a a0). inv X. + left. constructor. + right. unfold not. intros. apply H. inv H0. auto. } + { pose proof X as X2. + specialize (X a a0). inv X. + left. constructor; tauto. + apply IHl in X2. inv X2. + left. constructor; tauto. + right. unfold not in *; intros. apply H0. inv H1. now inv H3. } +Qed. + End NonEmpty. Module NE := NonEmpty. @@ -513,8 +538,7 @@ Proof. - intros. simplify. repeat (destruct_match; crush). subst. apply IHe1 in H. unfold not in *. intros. apply H. inv H0. auto. - intros. simplify. repeat (destruct_match; crush); subst. - unfold not in *; intros. inv H0. rewrite beq_expression_refl in H. - discriminate. + unfold not in *; intros. inv H0. rewrite beq_expression_refl in H. discriminate. unfold not in *; intros. inv H. rewrite beq_expression_list_refl in Heqb. discriminate. - simplify. repeat (destruct_match; crush); subst; unfold not in *; intros. @@ -537,6 +561,21 @@ Proof. apply beq_expression_correct2 in Heqb. auto. Defined. +Definition pred_expr_item_eq (pe1 pe2: pred_op * expression) : bool := + @equiv_dec _ SATSetoid _ (fst pe1) (fst pe2) && beq_expression (snd pe1) (snd pe2). + +Lemma pred_expr_dec: forall (pe1 pe2: pred_op * expression), + {pred_expr_item_eq pe1 pe2 = true} + {pred_expr_item_eq pe1 pe2 = false}. +Proof. + intros; destruct (pred_expr_item_eq pe1 pe2) eqn:?; unfold not; [tauto | now right]. +Qed. + +Lemma pred_expr_dec2: forall (pe1 pe2: pred_op * expression), + {pred_expr_item_eq pe1 pe2 = true} + {~ pred_expr_item_eq pe1 pe2 = true}. +Proof. + intros; destruct (pred_expr_item_eq pe1 pe2) eqn:?; unfold not; [tauto | now right]. +Qed. + Module HashExpr <: Hashable. Definition t := expression. Definition eq_dec := expression_dec. @@ -676,7 +715,7 @@ Proof. assert (P m true). rewrite <- H. fold f'. apply Maps.PTree_Properties.fold_rec. unfold P; intros. rewrite <- H1 in H4. auto. - red; intros. rewrite Maps.PTree.gempty in H2. discriminate. + red; intros. now rewrite Maps.PTree.gempty in H2. unfold P; intros. unfold f' in H4. boolInv. rewrite Maps.PTree.gsspec in H5. destruct (peq i k). subst. inv H5. auto. @@ -910,13 +949,20 @@ Section CORRECT. Proof. Admitted. - Lemma exists_norm_expr3 : +(* Lemma exists_norm_expr3 : forall e x pe expr m t h h', t ! e = None -> norm_expression m x h = (t, h') -> ~ NE.In (pe, expr) x. Proof. - Admitted. + Admitted.*) + + Lemma norm_expr_constant : + forall x m h t h' e p, + norm_expression m x h = (t, h') -> + h ! e = Some p -> + h' ! e = Some p. + Proof. Admitted. Lemma norm_expr_In : forall A B sem ctx x pe expr v, @@ -926,6 +972,23 @@ Section CORRECT. sem ctx expr v. Proof. Admitted. + Lemma norm_expr_Extract : + forall A B sem ctx x pe expr v, + @sem_pred_expr A B sem ctx x v -> + NE.In (pe, expr) x -> + eval_predf (ctx_ps ctx) pe = false -> + @sem_pred_expr A B sem ctx (NE.replace pred_expr_item_eq (pe, expr) (⟂, expr) x) v. + Proof. + induction x. + { simplify. destruct_match; auto. destruct a. + unfold pred_expr_item_eq in Heqb. simplify. + destruct (equiv_dec pe p) eqn:?; try easy. + rewrite e0 in H1. + inv H. crush. + } + { simplify. + } + Section SEM_PRED. Context (B: Type). @@ -933,6 +996,10 @@ Section CORRECT. Context (osem: @ctx tfd -> expression -> B -> Prop). Context (SEMSIM: forall e v v', isem ictx e v -> osem octx e v' -> v = v'). + Ltac simplify' l := intros; unfold_constants; cbn -[l] in *; + repeat (nicify_hypotheses; nicify_goals; kill_bools; substpp); + cbn -[l] in *. + Lemma check_correct_sem_value: forall x x' v v', beq_pred_expr x x' = true -> @@ -941,39 +1008,60 @@ Section CORRECT. v = v'. Proof. induction x. - - intros. + - intros * BEQ SEM1 SEM2. unfold beq_pred_expr in *. intros. repeat (destruct_match; try discriminate; []); subst. - inv H0. - pose Heqp as X. + rename Heqp into HNORM1. + rename Heqp0 into HNORM2. + inv SEM1. rename H0 into HEVAL. rename H2 into ISEM. + pose HNORM1 as X. eapply exists_norm_expr in X; [|constructor]. - Opaque norm_expression. simplify. Transparent norm_expression. - destruct (t0 ! x) eqn:?. - { eapply forall_ptree_true in H0; eauto. unfold tree_equiv_check_el in *. rewrite Heqo in H0. - apply equiv_check_dec in H0. - eapply exists_norm_expr2 in Heqo. - 3: { eauto. } - 2: { admit. } - eapply norm_expr_In in Heqo; eauto. - inv HSIM; simplify. setoid_rewrite H0 in H3. eassumption. + simplify' norm_expression. + rename H0 into HT1. + rename H1 into HH1. + rename H into HFORALL1. + rename H2 into HFORALL2. + destruct (t0 ! x) eqn:DSTR. + { eapply forall_ptree_true in HT1; eauto. unfold tree_equiv_check_el in *. rewrite DSTR in HT1. + apply equiv_check_dec in HT1. + eapply exists_norm_expr2 in DSTR; try solve [eapply norm_expr_constant; eassumption | eassumption]. + eapply norm_expr_In in DSTR; try eassumption. eauto. + inv HSIM; simplify. now setoid_rewrite <- HT1. } { + eapply forall_ptree_true in HT1; [|eassumption]. + unfold tree_equiv_check_el in *. rewrite DSTR in HT1. apply equiv_check_dec in HT1. + now setoid_rewrite HT1 in HEVAL. + } + - intros. unfold beq_pred_expr in H. intros. repeat (destruct_match; try discriminate; []); subst. + destruct a. + inv H0. + { pose Heqp as X. eapply exists_norm_expr in X; [|constructor; tauto]. simplify' norm_expression. + eapply forall_ptree_true in H0; [|eassumption]. + destruct (t0 ! x0) eqn:DSTR. + { + unfold tree_equiv_check_el in H0. rewrite DSTR in H0. apply equiv_check_dec in H0. + eapply exists_norm_expr2 in DSTR; try solve [eapply norm_expr_constant; eassumption | eassumption]. + eapply norm_expr_In in DSTR; try eassumption; eauto. + rewrite <- H0. inv HSIM; eauto. + } + { + unfold tree_equiv_check_el in *. rewrite DSTR in H0. apply equiv_check_dec in H0. + now rewrite H0 in H7. + } + } + { (* This is the inductive argument, which says that if the element is in the list, then + taking it out will result in two equivalent lists, otherwise just taking the current element + results in equivalent lists. *) + simplify' norm_expression. eapply exists_norm_expr in Heqp; [|constructor]; eauto. + simplify' norm_expression. + eapply forall_ptree_true in H0; [|eassumption]. + unfold tree_equiv_check_el in H0. + destruct (t0 ! x0) eqn:DSTR. + { + apply equiv_check_dec in H0. + eapply exists_norm_expr2 in DSTR; try solve [eapply norm_expr_constant; eassumption | eassumption]. + } } - eapply exists_norm_expr in Heqp. - unfold sat_pred_simple in *. - repeat destruct_match; try discriminate; []; subst. - assert (X: unsat (Por (Pand p (Pnot p0)) (Pand p0 (Pnot p)))) by eauto. - pose proof (sat_equiv2 _ _ X). - destruct x, x'; simplify. - repeat destruct_match; try discriminate; []. inv Heqp0. inv H0. inv H1. - inv Heqp - - apply sat_predicate_Pvar_inj in H2; subst. - - assert (e0 = e1) by (eapply hash_present_eq; eauto); subst. - eauto using sem_value_det. - - admit. - - admit. - - admit. Admitted. End SEM_PRED. diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v index 0ab7e77..ec558c6 100644 --- a/src/hls/Predicate.v +++ b/src/hls/Predicate.v @@ -399,6 +399,21 @@ Proof. apply equiv_check_dec in H. crush. Qed. +Lemma equiv_check_decidable2 : + forall p1 p2, {p1 == p2} + {p1 =/= p2}. +Proof. + intros. destruct (equiv_check p1 p2) eqn:?. + unfold decidable. + left. apply equiv_check_dec; auto. + unfold decidable, not; right; intros. + simpl. unfold complement. intros. + apply not_true_iff_false in Heqb. apply Heqb. + apply equiv_check_dec. eauto. +Qed. + #[global] Instance DecidableSATSetoid : DecidableSetoid SATSetoid := { setoid_decidable := equiv_check_decidable }. + +#[global] +Instance SATSetoidEqDec : EqDec SATSetoid := equiv_check_decidable2. diff --git a/src/hls/PrintVerilog.ml b/src/hls/PrintVerilog.ml index a5fa554..fbb26c5 100644 --- a/src/hls/PrintVerilog.ml +++ b/src/hls/PrintVerilog.ml @@ -82,7 +82,7 @@ let register a = | Some s -> s | None -> sprintf "reg_%d" (P.to_int a) -(*let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l))*) +(*let literal l = s printf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l))*) let literal l = let l' = camlint_of_coqint l in |