From c8a696682fcbdc720d67eb8d93f2c0c5b5c03548 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Mon, 20 Jul 2020 15:38:44 +0200 Subject: Define substitution conformly to SMT-LIB --- src/SMT_terms.v | 49 +----------- src/array/Array_checker.v | 22 +++--- src/bva/BVList.v | 194 +++++----------------------------------------- src/bva/Bva_checker.v | 20 ++--- src/spl/Operators.v | 6 +- 5 files changed, 47 insertions(+), 244 deletions(-) diff --git a/src/SMT_terms.v b/src/SMT_terms.v index a85804c..bbb122a 100644 --- a/src/SMT_terms.v +++ b/src/SMT_terms.v @@ -783,7 +783,6 @@ Module Atom. | BO_BVor (_: N) | BO_BVxor (_: N) | BO_BVadd (_: N) - | BO_BVsubst (_: N) | BO_BVmult (_: N) | BO_BVult (_: N) | BO_BVslt (_: N) @@ -852,7 +851,6 @@ Module Atom. | BO_BVor s1, BO_BVor s2 | BO_BVxor s1, BO_BVxor s2 | BO_BVadd s1, BO_BVadd s2 - | BO_BVsubst s1, BO_BVsubst s2 | BO_BVmult s1, BO_BVmult s2 => N.eqb s1 s2 | BO_BVult s1, BO_BVult s2 => N.eqb s1 s2 | BO_BVslt s1, BO_BVslt s2 => N.eqb s1 s2 @@ -952,8 +950,8 @@ Module Atom. Lemma reflect_bop_eqb : forall o1 o2, reflect (o1 = o2) (bop_eqb o1 o2). Proof. - intros [ | | | | | | | A1|s1|s1 |s1 | s1 | s1 | s1 | s1 | s1 | s1 | s1 | s1 | I1 E1 | I1 E1 ] - [ | | | | | | | A2|s2|s2| s2 | s2 | s2 | s2 | s2 | s2 | s2 | s2 | s2 |I2 E2 | I2 E2 ]; + intros [ | | | | | | | A1|s1|s1 |s1 | s1 | s1 | s1 | s1 | s1 | s1 | s1 | I1 E1 | I1 E1 ] + [ | | | | | | | A2|s2|s2| s2 | s2 | s2 | s2 | s2 | s2 | s2 | s2 |I2 E2 | I2 E2 ]; simpl;try (constructor;trivial;discriminate). - preflect (Typ.reflect_eqb A1 A2). constructor;subst;trivial. @@ -971,8 +969,6 @@ Module Atom. constructor;subst;trivial. - preflect (N.eqb_spec s1 s2). constructor;subst;trivial. - - preflect (N.eqb_spec s1 s2). - constructor;subst;trivial. - intros. preflect (N.eqb_spec s1 s2). preflect (N.eqb_spec n n0). @@ -1116,7 +1112,6 @@ Qed. | BO_BVor s => ((Typ.TBV s,Typ.TBV s), Typ.TBV s) | BO_BVxor s => ((Typ.TBV s,Typ.TBV s), Typ.TBV s) | BO_BVadd s => ((Typ.TBV s,Typ.TBV s), Typ.TBV s) - | BO_BVsubst s => ((Typ.TBV s,Typ.TBV s), Typ.TBV s) | BO_BVmult s => ((Typ.TBV s,Typ.TBV s), Typ.TBV s) | BO_BVult s => ((Typ.TBV s,Typ.TBV s), Typ.Tbool) | BO_BVconcat s1 s2 => ((Typ.TBV s1,Typ.TBV s2), (Typ.TBV (s1 + s2))) @@ -1364,12 +1359,6 @@ Qed. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. (*additional case for BO_BVadd*) - (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). - left. exists (Typ.TBV n). now rewrite N.eqb_refl; easy. - right. intros. rewrite andb_false_r. easy. - right. intros. rewrite andb_false_r. easy. - right. intros. rewrite andb_false_r. easy. - (*additional case for BO_BVsubst*) (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). left. exists (Typ.TBV n). now rewrite N.eqb_refl; easy. right. intros. rewrite andb_false_r. easy. @@ -1544,8 +1533,6 @@ Qed. apply_binop (Typ.TBV s) (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_xor s) | BO_BVadd s => apply_binop (Typ.TBV s) (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_add s) - | BO_BVsubst s => - apply_binop (Typ.TBV s) (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_subt s) | BO_BVmult s => apply_binop (Typ.TBV s) (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_mult s) | BO_BVult s => @@ -1788,7 +1775,7 @@ Qed. rewrite Hb. intros. exists (@BITVECTOR_LIST.bv_sextn n n0 y); auto. rewrite Typ.cast_refl; auto. (* Binary operators *) - destruct op as [ | | | | | | | A |s1|s2| s3 | s4 | s5 | s6 | s7 | s8 | s9 | s10 | n m | ti te | ti te]; + destruct op as [ | | | | | | | A |s1|s2| s3 | s4 | s6 | s7 | s8 | s9 | s10 | n m | ti te | ti te]; [ intros [ ti' te' | i | | | |s ] | intros [ ti' te' | i | | | |s ] | intros [ ti' te' | i | | | |s ] | @@ -1806,7 +1793,6 @@ Qed. intros [ ti' te' | i | | | |s ] | intros [ ti' te' | i | | | |s ] | intros [ ti' te' | i | | | |s ] | - intros [ ti' te' | i | | | |s ] | intros [ ti' te' | i | | | |s ] | | ]; simpl; try discriminate; unfold is_true; @@ -1895,20 +1881,6 @@ Qed. rewrite Hb, Hc. intros y1 Hy1 y2 Hy2. rewrite Typ.cast_refl. exists (BITVECTOR_LIST.bv_add y1 y2); auto. - (*BO_BVsubt*) - simpl in s. - intros. rewrite !andb_true_iff in H. destruct H as ((Ha, Hb), Hc). - apply Typ.eqb_spec in Hb. - apply Typ.eqb_spec in Hc. - rewrite N.eqb_eq in Ha. - revert Hb Hc. rewrite Ha in *. intros. - - destruct (check_aux_interp_hatom h1) as [x1 Hx1]. - rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl. - revert x1 Hx1 x2 Hx2. - rewrite Hb, Hc. intros y1 Hy1 y2 Hy2. - rewrite Typ.cast_refl. - exists (BITVECTOR_LIST.bv_subt y1 y2); auto. (*BO_BVmult*) simpl in s. intros. rewrite !andb_true_iff in H. destruct H as ((Ha, Hb), Hc). @@ -2151,15 +2123,6 @@ Qed. specialize (H (Typ.TBV n)). simpl in H. apply andb_false_iff in H. destruct H. specialize (@Typ.cast_diff (get_type h1) (Typ.TBV n)). intros. - rewrite andb_false_iff in H. destruct H as [ H | H ]. - rewrite N.eqb_refl in H. now contradict H. - apply Typ.cast_diff in H. now rewrite H. - apply Typ.cast_diff in H. rewrite H. - case (Typ.cast (get_type h1) (Typ.TBV n)); auto. - (*BVsubt*) - specialize (H (Typ.TBV n)). simpl in H. - apply andb_false_iff in H. destruct H. - specialize (@Typ.cast_diff (get_type h1) (Typ.TBV n)). intros. rewrite andb_false_iff in H. destruct H as [ H | H ]. rewrite N.eqb_refl in H. now contradict H. apply Typ.cast_diff in H. now rewrite H. @@ -2448,7 +2411,7 @@ Qed. simpl; [ | exists true; auto]. intro k. exists (BITVECTOR_LIST.bv_sextn i0 (k interp_t x)) ; auto. (* Binary operators *) - intros [ | | | | | | |A | | | | | | | | | | | | ti te| ti te] h1 h2; simpl; rewrite andb_true_iff; intros [H1 H2]; destruct (IH h1 H1) as [x Hx]; destruct (IH h2 H2) as [y Hy]; rewrite Hx, Hy; simpl. + intros [ | | | | | | |A | | | | | | | | | | | ti te| ti te] h1 h2; simpl; rewrite andb_true_iff; intros [H1 H2]; destruct (IH h1 H1) as [x Hx]; destruct (IH h2 H2) as [y Hy]; rewrite Hx, Hy; simpl. case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ); simpl; try (exists true; auto); intro k2; exists (k1 interp_t x + k2 interp_t y)%Z; auto. case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ); simpl; try (exists true; auto); intro k2; exists (k1 interp_t x - k2 interp_t y)%Z; auto. case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ); simpl; try (exists true; auto); intro k2; exists (k1 interp_t x * k2 interp_t y)%Z; auto. @@ -2478,10 +2441,6 @@ Qed. intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) (Typ.TBV n)) as [k2| ]; simpl; try (exists true; reflexivity); exists (BITVECTOR_LIST.bv_add (k1 interp_t x) (k2 interp_t y)); auto. - (*BO_BVsubst*) - case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) (Typ.TBV n)); simpl; try (exists true; auto); - intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) (Typ.TBV n)) as [k2| ]; - simpl; try (exists true; reflexivity); exists (BITVECTOR_LIST.bv_subt (k1 interp_t x) (k2 interp_t y)); auto. (*BO_BVmult*) case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) (Typ.TBV n)); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) (Typ.TBV n)) as [k2| ]; diff --git a/src/array/Array_checker.v b/src/array/Array_checker.v index 0540855..da0f6f2 100644 --- a/src/array/Array_checker.v +++ b/src/array/Array_checker.v @@ -206,9 +206,9 @@ Section certif. case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true). intros a Heq2. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). - intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] a1 a2 Heq3; try (intros; now apply C.interp_true). + intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] a1 a2 Heq3; try (intros; now apply C.interp_true). case_eq (t_atom .[ a1]); try (intros; now apply C.interp_true). - intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] b1 b2 Heq4; try (intros; now apply C.interp_true). + intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] b1 b2 Heq4; try (intros; now apply C.interp_true). case_eq (t_atom .[ b1]); try (intros; now apply C.interp_true). intros [ ] c1 c2 c3 Heq5. (* roweq *) @@ -415,13 +415,13 @@ Section certif. case_eq (t_form .[ Lit.blit j]); try (intros; now apply C.interp_true). intros b Heq4. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). - intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] a1 a2 Heq5; try (intros; now apply C.interp_true). + intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] a1 a2 Heq5; try (intros; now apply C.interp_true). case_eq (t_atom .[ b]); try (intros; now apply C.interp_true). - intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] b1 b2 Heq6; try (intros; now apply C.interp_true). + intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] b1 b2 Heq6; try (intros; now apply C.interp_true). case_eq (t_atom .[ b1]); try (intros; now apply C.interp_true). - intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] c1 c2 Heq7; try (intros; now apply C.interp_true). + intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] c1 c2 Heq7; try (intros; now apply C.interp_true). case_eq (t_atom .[ b2]); try (intros; now apply C.interp_true). - intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] d1 d2 Heq8; try (intros; now apply C.interp_true). + intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] d1 d2 Heq8; try (intros; now apply C.interp_true). case_eq (Typ.eqb t t1 && Typ.eqb t t3 && Typ.eqb t0 t2 && Typ.eqb t0 t4); try (intros; now apply C.interp_true). intros Heq9. @@ -906,18 +906,18 @@ Section certif. case_eq (t_form .[ Lit.blit (a .[1])]); try (intros; now apply C.interp_true). intros c Heq6. case_eq (t_atom .[ b]); try (intros; now apply C.interp_true). - intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] b1 b2 Heq7; try (intros; now apply C.interp_true). + intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] b1 b2 Heq7; try (intros; now apply C.interp_true). case_eq t; try (intros; now apply C.interp_true). intros t0 t1 Heq8. case_eq (t_atom .[ c]); try (intros; now apply C.interp_true). - intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] c1 c2 Heq9; try (intros; now apply C.interp_true). + intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] c1 c2 Heq9; try (intros; now apply C.interp_true). case_eq (Typ.eqb t1 t2); [ intros Heq10 | intros Heq10; now apply C.interp_true]. case_eq (t_atom .[ c1]); try (intros; now apply C.interp_true). - intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] d1 d2 Heq11; try (intros; now apply C.interp_true). + intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] d1 d2 Heq11; try (intros; now apply C.interp_true). case_eq (t_atom .[ c2]); try (intros; now apply C.interp_true). - intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] e1 e2 Heq12; try (intros; now apply C.interp_true). + intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] e1 e2 Heq12; try (intros; now apply C.interp_true). case_eq (t_atom .[ d2]); try (intros; rewrite !andb_false_r; simpl; now apply C.interp_true). - intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] f1 f2 Heq14; + intros [ | | | | | | | |N|N|N|N|N|N|N|N| | | | ] f1 f2 Heq14; try (intros; rewrite !andb_false_r; simpl; now apply C.interp_true). case_eq (Typ.eqb t0 t3 && Typ.eqb t0 t5 && Typ.eqb t1 t4 && Typ.eqb t1 t6); [ intros Heq13'| intro; now apply C.interp_true]. diff --git a/src/bva/BVList.v b/src/bva/BVList.v index c542d48..2381b1b 100644 --- a/src/bva/BVList.v +++ b/src/bva/BVList.v @@ -53,28 +53,29 @@ Module Type BITVECTOR. (*equality*) Parameter bv_eq : forall n, bitvector n -> bitvector n -> bool. + (*unary operations*) + Parameter bv_not : forall n, bitvector n -> bitvector n. + Parameter bv_neg : forall n, bitvector n -> bitvector n. + Parameter bv_extr : forall (i n0 n1 : N), bitvector n1 -> bitvector n0. + (*binary operations*) Parameter bv_concat : forall n m, bitvector n -> bitvector m -> bitvector (n + m). Parameter bv_and : forall n, bitvector n -> bitvector n -> bitvector n. Parameter bv_or : forall n, bitvector n -> bitvector n -> bitvector n. Parameter bv_xor : forall n, bitvector n -> bitvector n -> bitvector n. Parameter bv_add : forall n, bitvector n -> bitvector n -> bitvector n. - Parameter bv_subt : forall n, bitvector n -> bitvector n -> bitvector n. Parameter bv_mult : forall n, bitvector n -> bitvector n -> bitvector n. Parameter bv_ult : forall n, bitvector n -> bitvector n -> bool. Parameter bv_slt : forall n, bitvector n -> bitvector n -> bool. + Notation bv_subt bv1 bv2 := (bv_add bv1 (bv_neg bv2)). + Parameter bv_ultP : forall n, bitvector n -> bitvector n -> Prop. Parameter bv_sltP : forall n, bitvector n -> bitvector n -> Prop. Parameter bv_shl : forall n, bitvector n -> bitvector n -> bitvector n. Parameter bv_shr : forall n, bitvector n -> bitvector n -> bitvector n. - (*unary operations*) - Parameter bv_not : forall n, bitvector n -> bitvector n. - Parameter bv_neg : forall n, bitvector n -> bitvector n. - Parameter bv_extr : forall (i n0 n1 : N), bitvector n1 -> bitvector n0. - (* Parameter bv_extr : forall (n i j : N) {H0: n >= j} {H1: j >= i}, bitvector n -> bitvector (j - i). *) Parameter bv_zextn : forall (n i: N), bitvector n -> bitvector (i + n). @@ -122,6 +123,11 @@ Parameter zeros : N -> bitvector. (*equality*) Parameter bv_eq : bitvector -> bitvector -> bool. +(*unary operations*) +Parameter bv_not : bitvector -> bitvector. +Parameter bv_neg : bitvector -> bitvector. +Parameter bv_extr : forall (i n0 n1: N), bitvector -> bitvector. + (*binary operations*) Parameter bv_concat : bitvector -> bitvector -> bitvector. Parameter bv_and : bitvector -> bitvector -> bitvector. @@ -129,7 +135,6 @@ Parameter bv_or : bitvector -> bitvector -> bitvector. Parameter bv_xor : bitvector -> bitvector -> bitvector. Parameter bv_add : bitvector -> bitvector -> bitvector. Parameter bv_mult : bitvector -> bitvector -> bitvector. -Parameter bv_subt : bitvector -> bitvector -> bitvector. Parameter bv_ult : bitvector -> bitvector -> bool. Parameter bv_slt : bitvector -> bitvector -> bool. @@ -139,11 +144,6 @@ Parameter bv_sltP : bitvector -> bitvector -> Prop. Parameter bv_shl : bitvector -> bitvector -> bitvector. Parameter bv_shr : bitvector -> bitvector -> bitvector. -(*unary operations*) -Parameter bv_not : bitvector -> bitvector. -Parameter bv_neg : bitvector -> bitvector. -Parameter bv_extr : forall (i n0 n1: N), bitvector -> bitvector. - (*Parameter bv_extr : forall (n i j: N) {H0: n >= j} {H1: j >= i}, bitvector -> bitvector.*) Parameter bv_zextn : forall (n i: N), bitvector -> bitvector. @@ -160,7 +160,6 @@ Axiom bv_and_size : forall n a b, size a = n -> size b = n -> size (bv_and a Axiom bv_or_size : forall n a b, size a = n -> size b = n -> size (bv_or a b) = n. Axiom bv_xor_size : forall n a b, size a = n -> size b = n -> size (bv_xor a b) = n. Axiom bv_add_size : forall n a b, size a = n -> size b = n -> size (bv_add a b) = n. -Axiom bv_subt_size : forall n a b, size a = n -> size b = n -> size (bv_subt a b) = n. Axiom bv_mult_size : forall n a b, size a = n -> size b = n -> size (bv_mult a b) = n. Axiom bv_not_size : forall n a, size a = n -> size (bv_not a) = n. Axiom bv_neg_size : forall n a, size a = n -> size (bv_neg a) = n. @@ -238,6 +237,12 @@ Module RAW2BITVECTOR (M:RAWBITVECTOR) <: BITVECTOR. Definition bv_eq n (bv1 bv2:bitvector n) := M.bv_eq bv1 bv2. + Definition bv_not n (bv1: bitvector n) : bitvector n := + @MkBitvector n (M.bv_not bv1) (M.bv_not_size (wf bv1)). + + Definition bv_neg n (bv1: bitvector n) : bitvector n := + @MkBitvector n (M.bv_neg bv1) (M.bv_neg_size (wf bv1)). + Definition bv_ultP n (bv1 bv2:bitvector n) := M.bv_ultP bv1 bv2. Definition bv_sltP n (bv1 bv2:bitvector n) := M.bv_sltP bv1 bv2. @@ -251,8 +256,7 @@ Module RAW2BITVECTOR (M:RAWBITVECTOR) <: BITVECTOR. Definition bv_add n (bv1 bv2:bitvector n) : bitvector n := @MkBitvector n (M.bv_add bv1 bv2) (M.bv_add_size (wf bv1) (wf bv2)). - Definition bv_subt n (bv1 bv2:bitvector n) : bitvector n := - @MkBitvector n (M.bv_subt bv1 bv2) (M.bv_subt_size (wf bv1) (wf bv2)). + Notation bv_subt bv1 bv2 := (bv_add bv1 (bv_neg bv2)). Definition bv_mult n (bv1 bv2:bitvector n) : bitvector n := @MkBitvector n (M.bv_mult bv1 bv2) (M.bv_mult_size (wf bv1) (wf bv2)). @@ -264,12 +268,6 @@ Module RAW2BITVECTOR (M:RAWBITVECTOR) <: BITVECTOR. Definition bv_slt n (bv1 bv2:bitvector n) : bool := M.bv_slt bv1 bv2. - Definition bv_not n (bv1: bitvector n) : bitvector n := - @MkBitvector n (M.bv_not bv1) (M.bv_not_size (wf bv1)). - - Definition bv_neg n (bv1: bitvector n) : bitvector n := - @MkBitvector n (M.bv_neg bv1) (M.bv_neg_size (wf bv1)). - Definition bv_concat n m (bv1:bitvector n) (bv2: bitvector m) : bitvector (n + m) := @MkBitvector (n + m) (M.bv_concat bv1 bv2) (M.bv_concat_size (wf bv1) (wf bv2)). @@ -575,42 +573,6 @@ Definition twos_complement b := Definition bv_neg (a: bitvector) : bitvector := (twos_complement a). -Definition subst_list' a b := add_list a (twos_complement b). - -Definition bv_subt' (a b : bitvector) : bitvector := - match (@size a) =? (@size b) with - | true => (subst_list' (@bits a) (@bits b)) - | _ => nil - end. - -Definition subst_borrow b1 b2 b := - match b1, b2, b with - | true, true, true => (true, true) - | true, true, false => (false, false) - | true, false, true => (false, false) - | false, true, true => (false, true) - | false, false, true => (true, true) - | false, true, false => (true, true) - | true, false, false => (true, false) - | false, false, false => (false, false) - end. - -Fixpoint subst_list_borrow bs1 bs2 b {struct bs1} := - match bs1, bs2 with - | nil, _ => nil - | _ , nil => nil - | b1 :: bs1, b2 :: bs2 => - let (r, b) := subst_borrow b1 b2 b in r :: (subst_list_borrow bs1 bs2 b) - end. - -Definition subst_list (a b: list bool) := subst_list_borrow a b false. - -Definition bv_subt (a b : bitvector) : bitvector := - match (@size a) =? (@size b) with - | true => subst_list (@bits a) (@bits b) - | _ => nil - end. - (*less than*) Fixpoint ult_list_big_endian (x y: list bool) := @@ -1735,33 +1697,6 @@ Qed. (* bitwise SUBST properties *) -Lemma subst_list_empty_empty_l: forall a, (subst_list [] a) = []. -Proof. intro a. unfold subst_list; auto. Qed. - -Lemma subst_list_empty_empty_r: forall a, (subst_list a []) = []. -Proof. intro a. - induction a as [ | a xs IHxs]. - - auto. - - unfold subst_list; auto. -Qed. - -Lemma subst_list'_empty_empty_r: forall a, (subst_list' a []) = []. -Proof. intro a. - induction a as [ | a xs IHxs]. - - auto. - - unfold subst_list' in *. unfold twos_complement. simpl. reflexivity. -Qed. - -Lemma subst_list_borrow_length: forall (a b: list bool) c, length a = length b -> length a = length (subst_list_borrow a b c). -Proof. induction a as [ | a' xs IHxs]. - simpl. auto. - intros [ | b ys]. - - simpl. intros. exact H. - - intros. simpl in *. - case_eq (subst_borrow a' b c); intros r c0 Heq. simpl. apply f_equal. - specialize (@IHxs ys). apply IHxs. inversion H; reflexivity. -Qed. - Lemma length_twos_complement: forall (a: list bool), length a = length (twos_complement a). Proof. intro a. induction a as [ | a' xs IHxs]. @@ -1771,30 +1706,6 @@ Proof. intro a. rewrite length_mk_list_false. rewrite <- not_list_length. reflexivity. Qed. -Lemma subst_list_length: forall (a b: list bool), length a = length b -> length a = length (subst_list a b). -Proof. intros a b H. unfold subst_list. apply (@subst_list_borrow_length a b false). exact H. Qed. - -Lemma subst_list'_length: forall (a b: list bool), length a = length b -> length a = length (subst_list' a b). -Proof. intros a b H. unfold subst_list'. - rewrite <- (@length_add_list_eq a (twos_complement b)). - - reflexivity. - - rewrite <- (@length_twos_complement b). exact H. -Qed. - -Lemma subst_list_borrow_empty_neutral: forall (a: list bool), (subst_list_borrow a (mk_list_false (length a)) false) = a. -Proof. intro a. induction a as [ | a' xs IHxs]. - - simpl. reflexivity. - - simpl. - cut(subst_borrow a' false false = (a', false)). - + intro H. rewrite H. rewrite IHxs. reflexivity. - + unfold subst_borrow. case a'; auto. -Qed. - -Lemma subst_list_empty_neutral: forall (a: list bool), (subst_list a (mk_list_false (length a))) = a. -Proof. intros a. unfold subst_list. - apply (@subst_list_borrow_empty_neutral a). -Qed. - Lemma twos_complement_cons_false: forall a, false :: twos_complement a = twos_complement (false :: a). Proof. intro a. induction a as [ | a xs IHxs]; unfold twos_complement; simpl; reflexivity. @@ -1808,12 +1719,6 @@ Proof. intro n. apply f_equal. exact IHn. Qed. -Lemma subst_list'_empty_neutral: forall (a: list bool), (subst_list' a (mk_list_false (length a))) = a. -Proof. intros a. unfold subst_list'. - rewrite (@twos_complement_false_false (length a)). - rewrite add_list_empty_neutral_r. reflexivity. -Qed. - (* some list ult and slt properties *) Lemma ult_list_big_endian_trans : forall x y z, @@ -2117,36 +2022,6 @@ Proof. intros. now apply rev_neq in H1. Qed. -(* bitvector SUBT properties *) - -Lemma bv_subt_size: forall n a b, size a = n -> size b = n -> size (bv_subt a b) = n. -Proof. intros n a b H0 H1. - unfold bv_subt, size, bits in *. rewrite H0, H1. rewrite N.eqb_compare. - rewrite N.compare_refl. rewrite <- subst_list_length. exact H0. - now rewrite <- Nat2N.inj_iff, H0. -Qed. - -Lemma bv_subt_empty_neutral_r: forall a, (bv_subt a (mk_list_false (length (bits a)))) = a. -Proof. intro a. unfold bv_subt, size, bits. - rewrite N.eqb_compare. rewrite length_mk_list_false. - rewrite N.compare_refl. - rewrite subst_list_empty_neutral. reflexivity. -Qed. - -Lemma bv_subt'_size: forall n a b, (size a) = n -> (size b) = n -> size (bv_subt' a b) = n. -Proof. intros n a b H0 H1. unfold bv_subt', size, bits in *. - rewrite H0, H1. rewrite N.eqb_compare. rewrite N.compare_refl. - rewrite <- subst_list'_length. exact H0. - now rewrite <- Nat2N.inj_iff, H0. -Qed. - -Lemma bv_subt'_empty_neutral_r: forall a, (bv_subt' a (mk_list_false (length (bits a)))) = a. -Proof. intro a. unfold bv_subt', size, bits. - rewrite N.eqb_compare. rewrite length_mk_list_false. - rewrite N.compare_refl. - rewrite subst_list'_empty_neutral. reflexivity. -Qed. - (* bitwise ADD-NEG properties *) Lemma add_neg_list_carry_false: forall a b c, add_list_ingr a (add_list_ingr b c true) false = add_list_ingr a (add_list_ingr b c false) true. @@ -2220,37 +2095,6 @@ Proof. intro a. unfold bv_add, bv_not, size, bits. rewrite not_list_length. rewrite Nat2N.id, not_list_length. reflexivity. Qed. - -(* bitwise ADD-SUBST properties *) - -Lemma add_subst_list_carry_opp: forall n a b, (length a) = n -> (length b) = n -> (add_list_ingr (subst_list' a b) b false) = a. -Proof. intros n a b H0 H1. - unfold subst_list', twos_complement, add_list. - rewrite add_neg_list_carry_false. rewrite not_list_length at 1. - rewrite add_list_carry_empty_neutral_r. - specialize (@add_list_carry_assoc a (map negb b) b true false false true). - intro H2. rewrite H2; try auto. rewrite add_neg_list_carry_neg_f_r. - rewrite H1. rewrite <- H0. rewrite add_list_carry_unit_t; reflexivity. -Qed. - -Lemma add_subst_opp: forall n a b, (length a) = n -> (length b) = n -> (add_list (subst_list' a b) b) = a. -Proof. intros n a b H0 H1. unfold add_list, size, bits. - apply (@add_subst_list_carry_opp n a b); easy. -Qed. - -(* bitvector ADD-SUBT properties *) - -Lemma bv_add_subst_opp: forall n a b, (size a) = n -> (size b) = n -> (bv_add (bv_subt' a b) b) = a. -Proof. intros n a b H0 H1. unfold bv_add, bv_subt', add_list, size, bits in *. - rewrite H0, H1. - rewrite N.eqb_compare. rewrite N.eqb_compare. rewrite N.compare_refl. - rewrite <- (@subst_list'_length a b). rewrite H0. - rewrite N.compare_refl. rewrite (@add_subst_list_carry_opp (nat_of_N n) a b); auto; - inversion H0; rewrite Nat2N.id; auto. - symmetry. now rewrite <- Nat2N.inj_iff, H0. - now rewrite <- Nat2N.inj_iff, H0. -Qed. - (* bitvector MULT properties *) Lemma prop_mult_bool_step_k_h_len: forall a b c k, diff --git a/src/bva/Bva_checker.v b/src/bva/Bva_checker.v index 20cc2cf..24cf620 100644 --- a/src/bva/Bva_checker.v +++ b/src/bva/Bva_checker.v @@ -1186,7 +1186,7 @@ Proof. intros f Heq2. case_eq (t_atom .[ f]); try (intros; now apply C.interp_true). - intros [ | | | | | | |[ A B | A| | | |n]|N|N|N|N|N|N|N|N|N| | | | ]; + intros [ | | | | | | |[ A B | A| | | |n]|N|N|N|N|N|N|N|N| | | | ]; try (intros; now apply C.interp_true). intros a b Heq3. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). intros c Heq4. @@ -3215,7 +3215,7 @@ Proof. case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true). intros a bsres Heq8. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). - intros [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; + intros [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). (* BVand *) - case_eq ((a1 == a1') && (a2 == a2') || (a1 == a2') && (a2 == a1')); @@ -4513,7 +4513,7 @@ Lemma valid_check_bbEq pos1 pos2 lres : C.valid rho (check_bbEq pos1 pos2 lres). case_eq (t_form .[ Lit.blit a]); try (intros; now apply C.interp_true). intros a3 Heq10. case_eq (t_atom .[ a3]); try (intros; now apply C.interp_true). - intros [ | | | | | | | [ A B | A | | | |n]|N|N|N|N|N|N|N|N|N| | | | ]; + intros [ | | | | | | | [ A B | A | | | |n]|N|N|N|N|N|N|N|N| | | | ]; try (intros; now apply C.interp_true). intros a1' a2' Heq9. @@ -5168,7 +5168,7 @@ Proof. case_eq (t_form .[ Lit.blit a]); try (intros; now apply C.interp_true). intros a3 Heq10. case_eq (t_atom .[ a3]); try (intros; now apply C.interp_true). - intros [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N|N| | | | ]; + intros [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N| | | | ]; try (intros; now apply C.interp_true). intros a1' a2' Heq9. @@ -5394,7 +5394,7 @@ Proof. case_eq (t_form .[ Lit.blit a]); try (intros; now apply C.interp_true). intros a3 Heq10. case_eq (t_atom .[ a3]); try (intros; now apply C.interp_true). - intros [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; + intros [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). case_eq ((a1 == a1') && (a2 == a2')); simpl; intros Heq15; try (now apply C.interp_true). @@ -5805,7 +5805,7 @@ Proof. case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true). intros a bsres Heq8. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). - intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; + intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). (* BVadd *) @@ -6603,7 +6603,7 @@ Proof. case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true). intros a bsres Heq8. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). - intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). + intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). (* BVmult *) - case_eq ((a1 == a1') && (a2 == a2') (* || (a1 == a2') && (a2 == a1')*) ); simpl; intros Heq10; try (now apply C.interp_true). @@ -6911,7 +6911,7 @@ Proof. case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true). intros a bsres Heq8. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). - intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). + intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). (* BVconcat *) - case_eq ((a1 == a1') && (a2 == a2')); simpl; intros Heq10; try (now apply C.interp_true). case_eq ( @@ -8055,7 +8055,7 @@ Proof. case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true). intros a bsres Heq8. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). - intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). + intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). case_eq (t_atom .[ a2]); try (intros; now apply C.interp_true). intros c Heqa2. case_eq c; try (intros; now apply C.interp_true). intros bv2 n0 Heqc. (* BVshl *) @@ -8385,7 +8385,7 @@ Proof. case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true). intros a bsres Heq8. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). - intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). + intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). case_eq (t_atom .[ a2]); try (intros; now apply C.interp_true). intros c Heqa2. case_eq c; try (intros; now apply C.interp_true). intros bv2 n0 Heqc. (* BVshr *) diff --git a/src/spl/Operators.v b/src/spl/Operators.v index f0aba15..d9fd40a 100644 --- a/src/spl/Operators.v +++ b/src/spl/Operators.v @@ -169,10 +169,10 @@ Section Operators. PArray.forallb_spec, check_diseqs_complete_spec, length_mapi; split; intros [H1 H2]; split. clear H2; intros i Hi; generalize (H1 _ Hi); rewrite get_mapi; auto; case_eq (Lit.is_pos (diseq .[ i])); try discriminate; intro Heq1; case_eq (get_form (Lit.blit (diseq .[ i]))); - try discriminate; intros a Heq2; case_eq (get_atom a); try discriminate; intros [ | | | | | | | B | | | | | | | | | | | | | ]; try discriminate; intros h1 h2 Heq3; case_eq (Typ.eqb A B); try discriminate; change (Typ.eqb A B = true) with (is_true (Typ.eqb A B)); rewrite Typ.eqb_spec; intro; subst B; case_eq (h1 == h2); try discriminate; rewrite eqb_false_spec; intro H2; case_eq (check_in h1 dist); try discriminate; case_eq (check_in h2 dist); try discriminate; rewrite !check_in_spec; intros H3 H4 _; split; try discriminate; exists a; split; auto; exists h1, h2; repeat split; auto; rewrite <- In2_In; auto. + try discriminate; intros a Heq2; case_eq (get_atom a); try discriminate; intros [ | | | | | | | B | | | | | | | | | | | | ]; try discriminate; intros h1 h2 Heq3; case_eq (Typ.eqb A B); try discriminate; change (Typ.eqb A B = true) with (is_true (Typ.eqb A B)); rewrite Typ.eqb_spec; intro; subst B; case_eq (h1 == h2); try discriminate; rewrite eqb_false_spec; intro H2; case_eq (check_in h1 dist); try discriminate; case_eq (check_in h2 dist); try discriminate; rewrite !check_in_spec; intros H3 H4 _; split; try discriminate; exists a; split; auto; exists h1, h2; repeat split; auto; rewrite <- In2_In; auto. clear H1; intros x y Hxy; destruct (H2 _ _ Hxy) as [i [H1 H4]]; clear H2; rewrite get_mapi in H4; auto; exists i; split; auto; generalize H4; - case_eq (Lit.is_pos (diseq .[ i])); intro Heq; try (intros [H|H]; discriminate); case_eq (get_form (Lit.blit (diseq .[ i]))); [intros a| | |intros a1 a2|intros a1|intros a1|intros a1|intros a1 a2|intros a1 a2| intros a1 a2 a3|intros a ls]; intro Heq2; try (intros [H|H]; discriminate); case_eq (get_atom a); [intros a1|intros a1 a2|intros [ | | | | | | | B | | | | | | | | | | | | | ] h1 h2|intros a1 a2|intros a1 a2 | intros a1 a2]; intro Heq3; try (intros [H|H]; discriminate); try (case_eq (Typ.eqb A B); try (intros _ [H|H]; discriminate); change (Typ.eqb A B = true) with (is_true (Typ.eqb A B)); rewrite Typ.eqb_spec; intro; subst B; case_eq (h1 == h2); try (intros _ [H|H]; discriminate); rewrite eqb_false_spec; intro H10; case (check_in h1 dist); try (intros [H|H]; discriminate); case (check_in h2 dist); try (intros [H|H]; discriminate); simpl; intro H3; split; try discriminate; exists a; split; auto; destruct H3 as [H3|H3]; inversion H3; subst; auto). + case_eq (Lit.is_pos (diseq .[ i])); intro Heq; try (intros [H|H]; discriminate); case_eq (get_form (Lit.blit (diseq .[ i]))); [intros a| | |intros a1 a2|intros a1|intros a1|intros a1|intros a1 a2|intros a1 a2| intros a1 a2 a3|intros a ls]; intro Heq2; try (intros [H|H]; discriminate); case_eq (get_atom a); [intros a1|intros a1 a2|intros [ | | | | | | | B | | | | | | | | | | | | ] h1 h2|intros a1 a2|intros a1 a2 | intros a1 a2]; intro Heq3; try (intros [H|H]; discriminate); try (case_eq (Typ.eqb A B); try (intros _ [H|H]; discriminate); change (Typ.eqb A B = true) with (is_true (Typ.eqb A B)); rewrite Typ.eqb_spec; intro; subst B; case_eq (h1 == h2); try (intros _ [H|H]; discriminate); rewrite eqb_false_spec; intro H10; case (check_in h1 dist); try (intros [H|H]; discriminate); case (check_in h2 dist); try (intros [H|H]; discriminate); simpl; intro H3; split; try discriminate; exists a; split; auto; destruct H3 as [H3|H3]; inversion H3; subst; auto). intros. destruct H0; now contradict H0. clear H2; intros i Hi; rewrite get_mapi; auto; destruct (H1 _ Hi) as [H2 [a [H3 [h1 [h2 [H4 [H5 H6]]]]]]]; clear H1; replace (Lit.is_pos (diseq .[ i])) with false by (case_eq (Lit.is_pos (diseq .[ i])); auto); rewrite H3, H4, Typ.eqb_refl; simpl; replace (h1 == h2) with false by (case_eq (h1 == h2); auto; rewrite eqb_spec; intro H; elim H5; auto); simpl; rewrite <- In2_In, <- !check_in_spec in H6; auto; destruct H6 as [H6 H7]; rewrite H6, H7; auto. @@ -247,7 +247,7 @@ intros. destruct H0; now contradict H0. get_atom hb = Atom.Abop (Atom.BO_eq ty) y x). Proof. intros f1 f2; unfold check_distinct_two_args; split. - case (get_form f1); try discriminate; intro ha; case (get_form f2); try discriminate; intro hb; case_eq (get_atom ha); try discriminate; intros [A] [ |x [ |y [ |l]]] Heq1; try discriminate; case_eq (get_atom hb); try discriminate; intros [ | | | | | | |B | | | | | | | | | | | | | ] x' y' Heq2; try discriminate; rewrite !andb_true_iff, orb_true_iff, !andb_true_iff; change (Typ.eqb A B = true) with (is_true (Typ.eqb A B)); rewrite Typ.eqb_spec, !Int63Properties.eqb_spec; intros [H1 [[H2 H3]|[H2 H3]]]; subst B x' y'; exists ha, hb, A, x, y; auto. + case (get_form f1); try discriminate; intro ha; case (get_form f2); try discriminate; intro hb; case_eq (get_atom ha); try discriminate; intros [A] [ |x [ |y [ |l]]] Heq1; try discriminate; case_eq (get_atom hb); try discriminate; intros [ | | | | | | |B | | | | | | | | | | | | ] x' y' Heq2; try discriminate; rewrite !andb_true_iff, orb_true_iff, !andb_true_iff; change (Typ.eqb A B = true) with (is_true (Typ.eqb A B)); rewrite Typ.eqb_spec, !Int63Properties.eqb_spec; intros [H1 [[H2 H3]|[H2 H3]]]; subst B x' y'; exists ha, hb, A, x, y; auto. intros [ha [hb [A [x [y [H1 [H2 [H3 [H4|H4]]]]]]]]]; rewrite H1, H2, H3, H4, Typ.eqb_refl, !eqb_refl; auto; rewrite orb_true_r; auto. Qed. -- cgit