diff options
Diffstat (limited to 'src/SMT_terms.v')
| -rw-r--r-- | src/SMT_terms.v | 1666 |
1 files changed, 1503 insertions, 163 deletions
diff --git a/src/SMT_terms.v b/src/SMT_terms.v index 65c0d8f..c411c99 100644 --- a/src/SMT_terms.v +++ b/src/SMT_terms.v @@ -1,22 +1,20 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2016 *) +(* Copyright (C) 2011 - 2019 *) (* *) -(* Michaël Armand *) -(* Benjamin Grégoire *) -(* Chantal Keller *) -(* *) -(* Inria - École Polytechnique - Université Paris-Sud *) +(* See file "AUTHORS" for the list of authors *) (* *) (* This file is distributed under the terms of the CeCILL-C licence *) (* *) (**************************************************************************) -Require Import Bool List Int63 PArray. -Require Import Misc State. - +Require Import Bool Int63 PArray BinPos SMT_classes_instances. +Require Import Misc State BVList. (* FArray Equalities DecidableTypeEx. *) +Require FArray. +Require List . +Local Open Scope list_scope. Local Open Scope array_scope. Local Open Scope int63_scope. @@ -40,7 +38,16 @@ Module Form. | Fimp (_:fargs) | Fxor (_:_lit) (_:_lit) | Fiff (_:_lit) (_:_lit) - | Fite (_:_lit) (_:_lit) (_:_lit). + | Fite (_:_lit) (_:_lit) (_:_lit) + (* Bit-blasting predicate (theory of bit vectors): + bbT a [l1;...;ln] means [l1;...;ln] is the bitwise representation of a + (in little endian) + WARNING: this is a slight infringement of stratification + *) + | FbbT (_:atom) (_:list _lit) + (* TODO: replace [list _lit] with [fargs] *) + . + Definition is_Ftrue h := match h with Ftrue => true | _ => false end. @@ -49,13 +56,15 @@ Module Form. match h with Ffalse => true | _ => false end. Lemma is_Ftrue_correct : forall h, is_Ftrue h -> h = Ftrue. - Proof. destruct h;trivial;discriminate. Qed. + Proof. destruct h; trivial;discriminate. Qed. Lemma is_Ffalse_correct : forall h, is_Ffalse h -> h = Ffalse. Proof. destruct h;trivial;discriminate. Qed. + Section Interp. Variable interp_atom : atom -> bool. + Variable interp_bvatom : atom -> forall s, BITVECTOR_LIST.bitvector s. Section Interp_form. @@ -79,6 +88,10 @@ Module Form. | Fite a b c => if Lit.interp interp_var a then Lit.interp interp_var b else Lit.interp interp_var c + | FbbT a ls => + let ils := List.map (Lit.interp interp_var) ls in + let n := N.of_nat (List.length ils) in + BITVECTOR_LIST.bv_eq (interp_bvatom a n) (BITVECTOR_LIST.of_bits ils) end. End Interp_form. @@ -88,7 +101,7 @@ Module Form. Variable t_form : PArray.array form. Definition t_interp : PArray.array bool := - PArray.foldi_left (fun i t_b hf => + PArray.foldi_left (fun i t_b hf => t_b.[i <- interp_aux (PArray.get t_b) hf]) (PArray.make (PArray.length t_form) true) t_form. @@ -98,8 +111,9 @@ Module Form. | Fnot2 _ l => Lit.blit l < i | Fand args | For args | Fimp args => PArray.forallb (fun l => Lit.blit l < i) args - | Fxor a b | Fiff a b => (Lit.blit a < i) && (Lit.blit b < i) + | Fxor a b | Fiff a b => (Lit.blit a < i) && (Lit.blit b < i) | Fite a b c => (Lit.blit a < i) && (Lit.blit b < i) && (Lit.blit c < i) + | FbbT _ ls => List.forallb (fun l => Lit.blit l < i) ls end. Lemma lt_form_interp_form_aux : @@ -112,16 +126,19 @@ Module Form. try (apply afold_left_eq;unfold is_true in H0; rewrite PArray.forallb_spec in H0;intros; auto using Lit.interp_eq_compat). - f_equal;auto using Lit.interp_eq_compat. - apply afold_right_eq;unfold is_true in H0; - rewrite PArray.forallb_spec in H0;intros; - auto using Lit.interp_eq_compat. - unfold is_true in H0;rewrite !andb_true_iff in H0;decompose [and] H0; - rewrite !(Lit.interp_eq_compat f1 f2);auto. - unfold is_true in H0;rewrite !andb_true_iff in H0;decompose [and] H0; - rewrite !(Lit.interp_eq_compat f1 f2);auto. - unfold is_true in H0;rewrite !andb_true_iff in H0;decompose [and] H0; - rewrite !(Lit.interp_eq_compat f1 f2);auto. + - f_equal;auto using Lit.interp_eq_compat. + - apply afold_right_eq;unfold is_true in H0; + rewrite PArray.forallb_spec in H0;intros; + auto using Lit.interp_eq_compat. + - unfold is_true in H0;rewrite !andb_true_iff in H0;decompose [and] H0; + rewrite !(Lit.interp_eq_compat f1 f2);auto. + - unfold is_true in H0;rewrite !andb_true_iff in H0;decompose [and] H0; + rewrite !(Lit.interp_eq_compat f1 f2);auto. + - unfold is_true in H0;rewrite !andb_true_iff in H0;decompose [and] H0; + rewrite !(Lit.interp_eq_compat f1 f2);auto. + - replace (List.map (Lit.interp f2) l) with (List.map (Lit.interp f1) l); auto. + unfold is_true in H0. rewrite List.forallb_forall in H0. + apply List_map_ext_in. intros x Hx. apply Lit.interp_eq_compat; auto. Qed. Definition wf := PArray.forallbi lt_form t_form. @@ -227,98 +244,160 @@ Module Form. End Form. -(* TODO Move this *) -Record typ_eqb : Type := Typ_eqb { - te_carrier : Type; - te_eqb : te_carrier -> te_carrier -> bool; - te_reflect : forall x y, reflect (x = y) (te_eqb x y) -}. - -Section Typ_eqb_param. - - Variable A : Type. - Variable r : { eq : A -> A -> bool & forall x y, reflect (x = y) (eq x y) }. - - Definition typ_eqb_of_typ_eqb_param : typ_eqb := - Typ_eqb A (projT1 r) (projT2 r). - -End Typ_eqb_param. - -(* Common used types into which we interpret *) - -(* Unit *) -Section Unit_typ_eqb. +Require OrderedTypeEx. - Let carrier : Type := unit. - - Let eqb : carrier -> carrier -> bool := - fun _ _ => true. - - Lemma unit_reflect : - forall x y, reflect (x = y) (eqb x y). - Proof. - unfold eqb; intros x y; case x; case y; simpl; - constructor; reflexivity. - Qed. - - Definition unit_typ_eqb := - Typ_eqb carrier eqb unit_reflect. - -End Unit_typ_eqb. -(* End TODO *) Module Typ. + Import FArray. + Notation index := int (only parsing). Inductive type := + | TFArray : type -> type -> type | Tindex : index -> type | TZ : type | Tbool : type - | Tpositive : type. + | Tpositive : type + | TBV : N -> type. Definition ftype := (list type * type)%type. Section Interp. - Variable t_i : PArray.array typ_eqb. + Import OrderedTypeEx. + + Variable t_i : PArray.array typ_compdec. - Definition interp t := + Fixpoint interp_compdec_aux (t:type) : {ty: Type & CompDec ty} := match t with - | Tindex i => (t_i.[i]).(te_carrier) - | TZ => Z - | Tbool => bool - | Tpositive => positive + | TFArray ti te => + existT (fun ty : Type => CompDec ty) + (@farray (type_compdec (projT2 (interp_compdec_aux ti))) + (type_compdec (projT2 (interp_compdec_aux te))) + (@ord_of_compdec _ (projT2 (interp_compdec_aux ti))) + (@inh_of_compdec _ (projT2 (interp_compdec_aux te)))) + (FArray_compdec + (type_compdec (projT2 (interp_compdec_aux ti))) + (type_compdec (projT2 (interp_compdec_aux te)))) + | Tindex i => + existT (fun ty : Type => CompDec ty) + (te_carrier (t_i .[ i])) (te_compdec (t_i .[ i])) + | TZ => existT (fun ty : Type => CompDec ty) Z Z_compdec + | Tbool => existT (fun ty : Type => CompDec ty) bool bool_compdec + | Tpositive => existT (fun ty : Type => CompDec ty) positive Positive_compdec + | TBV n => existT (fun ty : Type => CompDec ty) (BITVECTOR_LIST.bitvector n) (BV_compdec n) end. + Definition interp_compdec (t:type) : CompDec (projT1 (interp_compdec_aux t)) := + projT2 (interp_compdec_aux t). + + Definition interp (t:type) : Type := type_compdec (interp_compdec t). + + Definition interp_ftype (t:ftype) := - List.fold_right (fun dom codom =>interp dom -> codom) + List.fold_right (fun dom codom => interp dom -> codom) (interp (snd t)) (fst t). + + Definition dec_interp (t:type) : DecType (interp t). + destruct (interp_compdec t). + subst ty. + apply Decidable. + Defined. + + Instance comp_interp (t:type) : Comparable (interp t). + destruct (interp_compdec t). + subst ty. + apply Comp. + Defined. + + Instance ord_interp (t:type) : OrdType (interp t). + destruct (interp_compdec t). + subst ty. + apply Ordered. + Defined. + + + Definition inh_interp (t:type) : Inhabited (interp t). + unfold interp. + destruct (interp_compdec t). + apply Inh. + Defined. + + Definition inhabitant_interp (t:type) : interp t := default_value. + + + Hint Resolve + dec_interp comp_interp ord_interp + inh_interp interp_compdec : typeclass_instances. + + (* Boolean equality over interpretation of a btype *) Section Interp_Equality. + Definition i_eqb (t:type) : interp t -> interp t -> bool := - match t with - | Tindex i => (t_i.[i]).(te_eqb) - | TZ => Z.eqb - | Tbool => Bool.eqb - | Tpositive => Peqb - end. + eqb_of_compdec (interp_compdec t). + + + Lemma eqb_compdec_spec {t} (c : CompDec t) : forall x y, + eqb_of_compdec c x y = true <-> x = y. + intros. + destruct c. + destruct Eqb. + simpl. + auto. + Qed. + + Lemma eqb_compdec_spec_false {t} (c : CompDec t) : forall x y, + eqb_of_compdec c x y = false <-> x <> y. + intros. + destruct c. + destruct Eqb. + simpl. + split. intros. + unfold not. intros. + apply eqb_spec in H0. + rewrite H in H0. now contradict H0. + intros. unfold not in H. + rewrite <- not_true_iff_false. + unfold not. intros. + apply eqb_spec in H0. + apply H in H0. now contradict H0. + Qed. Lemma i_eqb_spec : forall t x y, i_eqb t x y <-> x = y. Proof. - destruct t;simpl;intros. - symmetry;apply reflect_iff;apply te_reflect. - apply Z.eqb_eq. - apply Bool.eqb_true_iff. - apply Peqb_eq. + intros. + unfold i_eqb. + apply eqb_compdec_spec. + Qed. + + Lemma i_eqb_spec_false : forall t x y, i_eqb t x y = false <-> x <> y. + Proof. + intros. + unfold i_eqb. + apply eqb_compdec_spec_false. Qed. + Lemma reflect_eqb_compdec {t} (c : CompDec t) : forall x y, + reflect (x = y) (eqb_of_compdec c x y). + intros. + destruct c. + destruct Eqb. + simpl in *. + apply iff_reflect. + symmetry; auto. + Qed. + + Lemma reflect_i_eqb : forall t x y, reflect (x = y) (i_eqb t x y). Proof. - intros;apply iff_reflect;symmetry;apply i_eqb_spec. + intros. + unfold i_eqb. + apply reflect_eqb_compdec. Qed. Lemma i_eqb_sym : forall t x y, i_eqb t x y = i_eqb t y x. @@ -328,6 +407,67 @@ Module Typ. rewrite is_true_iff in *; now rewrite i_eqb_spec in *. Qed. + + (* Lemma i_eqb_compdec_tbv (c: CompDec): forall x y, TBV x y = BITVECTOR_LIST_FIXED.bv_eq x y. *) + (* Proof. *) + + Definition i_eqb_eqb (t:type) : interp t -> interp t -> bool := + match t with + | Tindex i => eqb_of_compdec (t_i.[i]).(te_compdec) + | TZ => Z.eqb (* Zeq_bool *) + | Tbool => Bool.eqb + | Tpositive => Peqb + | TBV n => (@BITVECTOR_LIST.bv_eq n) + | TFArray ti te => i_eqb (TFArray ti te) + end. + + + Lemma eqb_compdec_refl {t} (c : CompDec t) : forall x, + eqb_of_compdec c x x = true. + intros. + destruct c. + destruct Eqb. + simpl. + apply eqb_spec. auto. + Qed. + + Lemma i_eqb_refl : forall t x, i_eqb t x x. + Proof. + intros. + unfold i_eqb. + apply eqb_compdec_refl. + Qed. + + + Lemma eqb_compdec_trans {t} (c : CompDec t) : forall x y z, + eqb_of_compdec c x y = true -> + eqb_of_compdec c y z = true -> + eqb_of_compdec c x z = true . + intros. + destruct c. + destruct Eqb. + simpl in *. + apply eqb_spec. + apply eqb_spec in H. + apply eqb_spec in H0. + subst; auto. + Qed. + + Lemma i_eqb_trans : forall t x y z, i_eqb t x y -> i_eqb t y z -> i_eqb t x z. + Proof. + intros. + unfold i_eqb. + apply (eqb_compdec_trans _ x y z); auto. + Qed. + + + Lemma i_eqb_t : forall t x y, i_eqb t x y = i_eqb_eqb t x y. + Proof. + intros. + unfold i_eqb_eqb. + destruct t; simpl; auto; unfold i_eqb; simpl. + Qed. + End Interp_Equality. End Interp. @@ -355,34 +495,94 @@ Module Typ. Notation idcast := (Cast (fun P x => x)). (* La fonction cast calcule cast_result *) - Definition cast (A B: type) : cast_result A B := + Fixpoint positive_cast (n m : positive) {struct n} : + option (forall P, P n -> P m) := + match n, m return option (forall P, P n -> P m) with + | xH, xH => Some (fun P x => x) + | xO p, xO q => + match positive_cast p q with + | Some k => Some (fun P => k (fun y => P (xO y))) + | None => None + end + | xI p, xI q => + match positive_cast p q with + | Some k => Some (fun P => k (fun y => P (xI y))) + | None => None + end + | _, _ => None + end. + + Definition N_cast (n m : N) : option (forall P, P n -> P m) := + match n, m return option (forall P, P n -> P m) with + | N0, N0 => Some (fun P x => x) + | Npos p, Npos q => + match positive_cast p q with + | Some k => Some (fun P => k (fun y => P (Npos y))) + | None => None + end + | _, _ => None + end. + + + (* TODO *) + + Fixpoint cast (A B: type) : cast_result A B := match A as C, B as D return cast_result C D with | Tindex i, Tindex j => - match cast i j with + match Int63Op.cast i j with | Some k => Cast (fun P => k (fun y => P (Tindex y))) | None => NoCast end | TZ, TZ => idcast | Tbool, Tbool => idcast | Tpositive, Tpositive => idcast + | TBV n, TBV m => + match N_cast n m with + | Some k => Cast (fun P => k (fun y => P (TBV y))) + | None => NoCast + end + | TFArray k1 e1, TFArray k2 e2 => + match cast k1 k2, cast e1 e2 with + | Cast kk, Cast ke => + let ka P := + let Pb d := P (TFArray d e1) in + let Pc d := P (TFArray k2 d) in + fun x => ke Pc (kk Pb x) + in Cast ka + | _, _ => NoCast + end | _, _ => NoCast end. - Lemma cast_refl: - forall A, cast A A = Cast (fun P (H : P A) => H). + Lemma positive_cast_refl: + forall p, positive_cast p p = Some (fun P (H : P p) => H). + Proof. induction p as [p IHp|p IHp| ]; simpl; try rewrite IHp; auto. Qed. + + Lemma N_cast_refl: + forall n, N_cast n n = Some (fun P (H : P n) => H). + Proof. intros [ |p]; simpl; try rewrite positive_cast_refl; auto. Qed. + + Fixpoint cast_refl A: + cast A A = Cast (fun P (H : P A) => H). Proof. - intros A0;destruct A0;simpl;trivial. - rewrite cast_refl;trivial. + destruct A;simpl;trivial. + do 2 rewrite cast_refl. easy. + rewrite Int63Properties.cast_refl;trivial. + rewrite N_cast_refl;trivial. Qed. + (* Remark : I use this definition because eqb will not be used only in the interpretation *) - Definition eqb (A B: type) : bool := + Fixpoint eqb (A B: type) : bool := match A, B with | Tindex i, Tindex j => i == j | TZ, TZ => true | Tbool, Tbool => true | Tpositive, Tpositive => true - | _, _ => false + | TBV n, TBV m => N.eqb n m + | TFArray k1 e1, TFArray k2 e2 => + eqb k1 k2 && eqb e1 e2 + | _,_ => false end. @@ -398,10 +598,43 @@ Module Typ. Lemma not_is_true_eq_false : forall b:bool, ~ b <-> b = false. Proof. exact not_true_iff_false. Qed. - Lemma cast_diff: forall A B, eqb A B = false -> cast A B = NoCast. + Lemma positive_cast_diff: forall p q, p <> q -> positive_cast p q = None. + Proof. + induction p as [p IHp|p IHp| ]; intros [q|q| ]; auto; intro Heq. + - simpl. rewrite IHp; auto. + intro H. apply Heq. rewrite H. reflexivity. + - simpl. rewrite IHp; auto. + intro H. apply Heq. rewrite H. reflexivity. + - elim Heq. reflexivity. + Qed. + + Lemma N_cast_diff: forall n m, n <> m -> N_cast n m = None. Proof. - intros A0 B0;destruct A0; destruct B0;simpl;trivial;try discriminate. - intros Heq;rewrite (cast_diff _ _ Heq);trivial. + intros [ |n] [ |m]; auto; intro Heq. + - elim Heq; reflexivity. + - simpl. rewrite positive_cast_diff; auto. + intro H. apply Heq. rewrite H. reflexivity. + Qed. + + Fixpoint cast_diff A B: eqb A B = false -> cast A B = NoCast. + Proof. + destruct A; destruct B;simpl;trivial;try discriminate. + intros. + rewrite andb_false_iff in H. + destruct H; apply cast_diff in H; rewrite H; auto. + case (cast A1 B1); auto. + intros H. rewrite (Int63Properties.cast_diff _ _ H);trivial. + rewrite N.eqb_neq. intro Heq. now rewrite N_cast_diff. + Qed. + + Lemma cast_eqb A B k: cast A B = Cast k -> eqb A B = true. + Proof. + intros. + apply not_false_iff_true. + unfold not. + intro. + apply cast_diff in H0. + rewrite H in H0. inversion H0. Qed. Lemma neq_cast : forall A B, @@ -410,22 +643,65 @@ Module Typ. intros C D;case_eq (eqb C D);trivial;apply cast_diff. Qed. - Lemma reflect_eqb : forall x y, reflect (x = y) (eqb x y). + Fixpoint reflect_eqb x y: reflect (x = y) (eqb x y). Proof. - intros x y;destruct x;destruct y;simpl;try constructor;trivial;try discriminate. - apply iff_reflect;rewrite eqb_spec;split;intros H;[inversion H | subst];trivial. + destruct x;destruct y;simpl;try constructor;trivial;try discriminate. + apply iff_reflect. + split. + intro H. inversion H. subst. + rewrite andb_true_iff. + split; + [specialize (reflect_eqb y1 y1) | specialize (reflect_eqb y2 y2)]; + apply reflect_iff in reflect_eqb; apply reflect_eqb; auto. + intros. + rewrite andb_true_iff in H; destruct H. + apply (reflect_iff _ _ (reflect_eqb x1 y1)) in H. + apply (reflect_iff _ _ (reflect_eqb x2 y2)) in H0. + subst; auto. + apply iff_reflect;rewrite Int63Properties.eqb_spec;split;intros H;[inversion H | subst]; trivial. + apply iff_reflect. rewrite N.eqb_eq. split;intros H;[inversion H | subst]; trivial. Qed. Lemma eqb_spec : forall x y, eqb x y <-> x = y. Proof. - intros;symmetry;apply reflect_iff;apply reflect_eqb. + intros. + symmetry. + apply reflect_iff. + apply reflect_eqb. Qed. Lemma eqb_refl : forall x, eqb x x. Proof. intros; rewrite eqb_spec; auto. Qed. + + Lemma cast_eq A B k: cast A B = Cast k -> A = B. + Proof. + intros. apply eqb_spec. apply (cast_eqb _ _ k). auto. + Qed. + + Lemma nocast_refl A B: cast A B = NoCast -> cast B A = NoCast. + Proof. + intros. + apply cast_diff. + rewrite neq_cast in H. + case_eq (eqb A B). intro. + rewrite H0 in H. + apply eqb_spec in H0. + rewrite H0 in H. + rewrite cast_refl in H. + now contradict H. + intro. + apply not_true_iff_false. + unfold not. + intro. + apply eqb_spec in H1. + rewrite H1 in H0. rewrite eqb_refl in H0. now contradict H0. + Qed. + + End Cast. + End Typ. Arguments Typ.Cast {_} {_} _. @@ -471,20 +747,28 @@ Proof. Qed. (* End move *) + Module Atom. Notation func := int (only parsing). - - Inductive cop : Type := + + Inductive cop : Type := | CO_xH - | CO_Z0. + | CO_Z0 + | CO_BV (_: list bool) (_ :N). Inductive unop : Type := | UO_xO | UO_xI - | UO_Zpos + | UO_Zpos | UO_Zneg - | UO_Zopp. + | UO_Zopp + | UO_BVbitOf (_: N) (_: nat) + | UO_BVnot (_: N) + | UO_BVneg (_: N) + | UO_BVextr (i: N) (n0: N) (n1: N) (* TODO n1 first arg *) + | UO_BVzextn (n: N) (i: N) + | UO_BVsextn (n: N) (i: N). Inductive binop : Type := | BO_Zplus @@ -494,17 +778,35 @@ Module Atom. | BO_Zle | BO_Zge | BO_Zgt - | BO_eq (_ : Typ.type). + | BO_eq (_ : Typ.type) + | BO_BVand (_: N) + | BO_BVor (_: N) + | BO_BVxor (_: N) + | BO_BVadd (_: N) + | BO_BVsubst (_: N) + | BO_BVmult (_: N) + | BO_BVult (_: N) + | BO_BVslt (_: N) + | BO_BVconcat (_: N) (_: N) + | BO_BVshl (_: N) + | BO_BVshr (_: N) + | BO_select (_ : Typ.type) (_ : Typ.type) + | BO_diffarray (_ : Typ.type) (_ : Typ.type) + . Inductive nop : Type := | NO_distinct (_ : Typ.type). + Inductive terop : Type := + | TO_store (_ : Typ.type) (_ : Typ.type). + Notation hatom := int (only parsing). - + Inductive atom : Type := | Acop (_: cop) | Auop (_ : unop) (_:hatom) | Abop (_ : binop) (_:hatom) (_:hatom) + | Atop (_ : terop) (_:hatom) (_:hatom) (_:hatom) | Anop (_ : nop) (_: list hatom) | Aapp (_:func) (_: list hatom). @@ -514,18 +816,25 @@ Module Atom. (** Equality *) Definition cop_eqb o o' := match o, o' with - | CO_xH, CO_xH + | CO_xH, CO_xH | CO_Z0, CO_Z0 => true + | CO_BV bv s, CO_BV bv' s' => N.eqb s s' && RAWBITVECTOR_LIST.beq_list bv bv' | _,_ => false end. Definition uop_eqb o o' := match o, o' with - | UO_xO, UO_xO + | UO_xO, UO_xO | UO_xI, UO_xI - | UO_Zpos, UO_Zpos + | UO_Zpos, UO_Zpos | UO_Zneg, UO_Zneg | UO_Zopp, UO_Zopp => true + | UO_BVbitOf s1 n, UO_BVbitOf s2 m => Nat_eqb n m && N.eqb s1 s2 + | UO_BVnot s1, UO_BVnot s2 => N.eqb s1 s2 + | UO_BVneg s1, UO_BVneg s2 => N.eqb s1 s2 + | UO_BVextr i0 n00 n01, UO_BVextr i1 n10 n11 => N.eqb i0 i1 && N.eqb n00 n10 && N.eqb n01 n11 + | UO_BVzextn s1 i1, UO_BVzextn s2 i2 => N.eqb s1 s2 && N.eqb i1 i2 + | UO_BVsextn s1 i1, UO_BVsextn s2 i2 => N.eqb s1 s2 && N.eqb i1 i2 | _,_ => false end. @@ -539,9 +848,27 @@ Module Atom. | BO_Zge, BO_Zge | BO_Zgt, BO_Zgt => true | BO_eq t, BO_eq t' => Typ.eqb t t' + | BO_BVand s1, BO_BVand s2 => N.eqb s1 s2 + | 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 + | BO_BVconcat s1 s2, BO_BVconcat s3 s4 => N.eqb s1 s3 && N.eqb s2 s4 + | BO_BVshl s1, BO_BVshl s2 => N.eqb s1 s2 + | BO_BVshr s1, BO_BVshr s2 => N.eqb s1 s2 + | BO_select ti te, BO_select ti' te' + | BO_diffarray ti te, BO_diffarray ti' te' => Typ.eqb ti ti' && Typ.eqb te te' | _,_ => false end. + Definition top_eqb o o' := + match o, o' with + | TO_store ti te, TO_store ti' te' => Typ.eqb ti ti' && Typ.eqb te te' + end. + Definition nop_eqb o o' := match o, o' with | NO_distinct t, NO_distinct t' => Typ.eqb t t' @@ -553,6 +880,8 @@ Module Atom. | Auop o t, Auop o' t' => uop_eqb o o' && (t == t') | Abop o t1 t2, Abop o' t1' t2' => bop_eqb o o' && (t1 == t1') && (t2 == t2') | Anop o t, Anop o' t' => nop_eqb o o' && list_beq Int63Native.eqb t t' + | Atop o t1 t2 t3, Atop o' t1' t2' t3' => + top_eqb o o' && (t1 == t1') && (t2 == t2') && (t3 == t3') | Aapp a la, Aapp b lb => (a == b) && list_beq Int63Native.eqb la lb | _, _ => false end. @@ -565,19 +894,109 @@ Module Atom. Lemma reflect_cop_eqb : forall o1 o2, reflect (o1 = o2) (cop_eqb o1 o2). Proof. - destruct o1;destruct o2;simpl;constructor;trivial;discriminate. + destruct o1; destruct o2; simpl; try (constructor; trivial; discriminate). + apply iff_reflect. split. intro. + inversion H. rewrite andb_true_iff. split. + rewrite N.eqb_refl; auto. apply RAWBITVECTOR_LIST.List_eq_refl; auto. + intros. rewrite andb_true_iff in H. destruct H as (Ha, Hb). + apply N.eqb_eq in Ha. rewrite RAWBITVECTOR_LIST.List_eq in Hb. + now rewrite Ha, Hb. Qed. Lemma reflect_uop_eqb : forall o1 o2, reflect (o1 = o2) (uop_eqb o1 o2). Proof. - destruct o1;destruct o2;simpl;constructor;trivial;discriminate. + intros [ | | | | | s1 n1 | s1 | s1 | s1 | s1 | s1 ] [ | | | | |s2 n2 | s2 | s2 | s2 | s2 | s2 ];simpl; try constructor;trivial; try discriminate. + - apply iff_reflect. case_eq (Nat_eqb n1 n2). + + case_eq ((s1 =? s2)%N). + * rewrite N.eqb_eq, beq_nat_true_iff. + intros -> ->. split; reflexivity. + * rewrite N.eqb_neq, beq_nat_true_iff. + intros H1 ->; split; try discriminate. + intro H. inversion H. elim H1. auto. + + split; auto. + * rewrite beq_nat_false_iff in H. intros. contradict H0. + intro H'. apply H. inversion H'. reflexivity. + * intros. contradict H0. easy. + - apply iff_reflect. rewrite N.eqb_eq. split; intro H. + + now inversion H. + + now rewrite H. + - apply iff_reflect. rewrite N.eqb_eq. split; intro H. + + now inversion H. + + now rewrite H. + - intros. apply iff_reflect. split. intro H. + inversion H. + rewrite !andb_true_iff; split. + split; now rewrite N.eqb_eq. + now rewrite N.eqb_eq. + intros. rewrite !andb_true_iff in H. + destruct H as ((Ha, Hb), Hc). + rewrite N.eqb_eq in Ha, Hb, Hc. + subst. + reflexivity. + - intros. apply iff_reflect. split; intros. + + rewrite !andb_true_iff. inversion H. + split; try split; try now rewrite N.eqb_eq. + + rewrite !andb_true_iff in H. + destruct H as (Ha, Hb). + rewrite N.eqb_eq in Ha, Hb. + now subst. + - intros. apply iff_reflect. split; intros. + + rewrite !andb_true_iff. inversion H. + split; try split; try now rewrite N.eqb_eq. + + rewrite !andb_true_iff in H. + destruct H as (Ha, Hb). + rewrite N.eqb_eq in Ha, Hb. + now subst. Qed. - + + Lemma reflect_bop_eqb : forall o1 o2, reflect (o1 = o2) (bop_eqb o1 o2). Proof. - destruct o1;destruct o2;simpl;try (constructor;trivial;discriminate). - preflect (Typ.reflect_eqb t t0). - constructor;subst;trivial. + 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 ]; + simpl;try (constructor;trivial;discriminate). + - preflect (Typ.reflect_eqb A1 A2). + constructor;subst;trivial. + - preflect (N.eqb_spec s1 s2). + constructor;subst;trivial. + - preflect (N.eqb_spec s1 s2). + constructor;subst;trivial. + - preflect (N.eqb_spec s1 s2). + constructor;subst;trivial. + - preflect (N.eqb_spec s1 s2). + constructor;subst;trivial. + - preflect (N.eqb_spec s1 s2). + constructor;subst;trivial. + - preflect (N.eqb_spec s1 s2). + 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). + constructor;subst;trivial. + + - preflect (N.eqb_spec s1 s2). + constructor;subst;trivial. + - preflect (N.eqb_spec s1 s2). + constructor;subst;trivial. + + - preflect (Typ.reflect_eqb I1 I2). + preflect (Typ.reflect_eqb E1 E2). + constructor;subst;trivial. + - preflect (Typ.reflect_eqb I1 I2). + preflect (Typ.reflect_eqb E1 E2). + constructor;subst;trivial. +Qed. + + Lemma reflect_top_eqb : forall o1 o2, reflect (o1 = o2) (top_eqb o1 o2). + Proof. + intros [ I1 E1 ] [ I2 E2 ]. simpl. + preflect (Typ.reflect_eqb I1 I2). + preflect (Typ.reflect_eqb E1 E2). + constructor;subst;trivial. Qed. Lemma reflect_nop_eqb : forall o1 o2, reflect (o1 = o2) (nop_eqb o1 o2). @@ -594,32 +1013,40 @@ Module Atom. preflect (reflect_uop_eqb u u0); preflect (Int63Properties.reflect_eqb i i0); constructor;subst;trivial. (* Binary operators *) - preflect (reflect_bop_eqb b b0); + preflect (reflect_bop_eqb b b0); preflect (Int63Properties.reflect_eqb i i1); preflect (Int63Properties.reflect_eqb i0 i2); constructor;subst;trivial. + (* Ternary operators *) + preflect (reflect_top_eqb t t0). + preflect (Int63Properties.reflect_eqb i i2). + preflect (Int63Properties.reflect_eqb i0 i3). + preflect (Int63Properties.reflect_eqb i1 i4). + constructor;subst;trivial. (* N-ary operators *) - preflect (reflect_nop_eqb n n0); preflect (reflect_list_beq _ _ Int63Properties.reflect_eqb l l0); constructor; subst; reflexivity. + preflect (reflect_nop_eqb n n0); + preflect (reflect_list_beq _ _ Int63Properties.reflect_eqb l l0); + constructor; subst; reflexivity. (* Application *) preflect (Int63Properties.reflect_eqb i i0); preflect (reflect_list_beq _ _ Int63Properties.reflect_eqb l l0); constructor;subst;trivial. Qed. - + Lemma eqb_spec : forall t1 t2, eqb t1 t2 <-> t1 = t2. Proof. - intros;symmetry;apply reflect_iff;apply reflect_eqb. + intros;symmetry; apply reflect_iff; apply reflect_eqb. Qed. - + (** Typing and interpretation *) - + Record val (t:Type) (I:t -> Type) := Val { v_type : t; v_val : I v_type }. Section Typing_Interp. - Variable t_i : PArray.array typ_eqb. + Variable t_i : PArray.array typ_compdec. Local Notation interp_t := (Typ.interp t_i). Local Notation interp_ft := (Typ.interp_ftype t_i). @@ -646,38 +1073,63 @@ Module Atom. simpl in H1; rewrite Typ.cast_refl in H1; auto. Qed. - (* Interprétation d'une fonction*) + (* Interpretation of a function*) Variable t_func : PArray.array tval. (** Type checking of atom assuming an type for hatom *) Section Typ_Aux. Variable get_type : hatom -> Typ.type. - Definition typ_cop o := + Definition typ_cop o := match o with - | CO_xH => Typ.Tpositive + | CO_xH => Typ.Tpositive | CO_Z0 => Typ.TZ + | CO_BV _ s => Typ.TBV s end. Definition typ_uop o := match o with - | UO_xO => (Typ.Tpositive,Typ.Tpositive) - | UO_xI => (Typ.Tpositive,Typ.Tpositive) + | UO_xO => (Typ.Tpositive,Typ.Tpositive) + | UO_xI => (Typ.Tpositive,Typ.Tpositive) | UO_Zpos => (Typ.Tpositive, Typ.TZ) | UO_Zneg => (Typ.Tpositive, Typ.TZ) | UO_Zopp => (Typ.TZ, Typ.TZ) + | UO_BVbitOf s _ => (Typ.TBV s, Typ.Tbool) + | UO_BVnot s => (Typ.TBV s, Typ.TBV s) + | UO_BVneg s => (Typ.TBV s, Typ.TBV s) + | UO_BVextr i n0 n1 => (Typ.TBV n1, Typ.TBV n0) + | UO_BVzextn s i => (Typ.TBV s, Typ.TBV (i + s)) + | UO_BVsextn s i => (Typ.TBV s, Typ.TBV (i + s)) end. - Definition typ_bop o := + Definition typ_bop o := match o with - | BO_Zplus => ((Typ.TZ,Typ.TZ), Typ.TZ) - | BO_Zminus => ((Typ.TZ,Typ.TZ), Typ.TZ) - | BO_Zmult => ((Typ.TZ,Typ.TZ), Typ.TZ) - | BO_Zlt => ((Typ.TZ,Typ.TZ), Typ.Tbool) - | BO_Zle => ((Typ.TZ,Typ.TZ), Typ.Tbool) - | BO_Zge => ((Typ.TZ,Typ.TZ), Typ.Tbool) + | BO_Zplus => ((Typ.TZ,Typ.TZ), Typ.TZ) + | BO_Zminus => ((Typ.TZ,Typ.TZ), Typ.TZ) + | BO_Zmult => ((Typ.TZ,Typ.TZ), Typ.TZ) + | BO_Zlt => ((Typ.TZ,Typ.TZ), Typ.Tbool) + | BO_Zle => ((Typ.TZ,Typ.TZ), Typ.Tbool) + | BO_Zge => ((Typ.TZ,Typ.TZ), Typ.Tbool) | BO_Zgt => ((Typ.TZ,Typ.TZ), Typ.Tbool) | BO_eq t => ((t,t),Typ.Tbool) + | BO_BVand s => ((Typ.TBV s,Typ.TBV s), (Typ.TBV s)) + | 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))) + | BO_BVslt s => ((Typ.TBV s,Typ.TBV s), Typ.Tbool) + | BO_BVshl s => ((Typ.TBV s,Typ.TBV s), Typ.TBV s) + | BO_BVshr s => ((Typ.TBV s,Typ.TBV s), Typ.TBV s) + | BO_select ti te => ((Typ.TFArray ti te, ti), te) + | BO_diffarray ti te => ((Typ.TFArray ti te, Typ.TFArray ti te), ti) + end. + + Definition typ_top o := + match o with + | TO_store ti te => ((Typ.TFArray ti te, ti, te), Typ.TFArray ti te) end. Definition typ_nop o := @@ -692,16 +1144,21 @@ Module Atom. | _, _ => false end. - Definition check_aux (a:atom) (t:Typ.type) : bool := + Definition check_aux (a:atom) (t:Typ.type) : bool := match a with - | Acop o => Typ.eqb (typ_cop o) t + | Acop o => Typ.eqb (typ_cop o) t | Auop o a => let (ta,t') := typ_uop o in Typ.eqb t' t && Typ.eqb (get_type a) ta | Abop o a1 a2 => let (ta,t') := typ_bop o in let (ta1,ta2) := ta in - Typ.eqb t' t && Typ.eqb (get_type a1) ta1 && Typ.eqb (get_type a2) ta2 + Typ.eqb t' t && Typ.eqb (get_type a1) ta1 && Typ.eqb (get_type a2) ta2 + | Atop o a1 a2 a3 => + let (ta, t') := typ_top o in + let '(ta1, ta2, ta3) := ta in + Typ.eqb t' t && Typ.eqb (get_type a1) ta1 && + Typ.eqb (get_type a2) ta2 && Typ.eqb (get_type a3) ta3 | Anop o a => let (ta,t') := typ_nop o in (Typ.eqb t' t) && (List.forallb (fun t1 => Typ.eqb (get_type t1) ta) a) @@ -715,7 +1172,7 @@ Module Atom. Lemma unicity : forall a t1 t2, check_aux a t1 -> check_aux a t2 -> t1 = t2. Proof. - destruct a;simpl. + destruct a;simpl. (* Constants *) intros t1 t2;rewrite !Typ.eqb_spec;intros;subst;trivial. (* Unary operators *) @@ -729,8 +1186,20 @@ Module Atom. intros [[H1 _] _] [[H2 _] _]; change (is_true (Typ.eqb (snd (typ_bop b)) t1)) in H1. change (is_true (Typ.eqb (snd (typ_bop b)) t2)) in H2. rewrite Typ.eqb_spec in H1, H2;subst;trivial. + (* Ternary operators *) + unfold is_true. intros. + destruct typ_top. destruct p. destruct p. + rewrite !andb_true_iff in H, H0. + destruct H as (((Ha, Hb), Hc), Hd). + destruct H0 as (((H0a, H0b), H0c), H0d). + apply Typ.eqb_spec in Ha. + apply Typ.eqb_spec in H0a. now subst. (* N-ary operators *) - intros t1 t2; destruct (typ_nop n) as [ta t']; unfold is_true; rewrite !andb_true_iff; change (is_true (Typ.eqb t' t1) /\ is_true (List.forallb (fun t3 : int => Typ.eqb (get_type t3) ta) l) -> is_true (Typ.eqb t' t2) /\ is_true (List.forallb (fun t3 : int => Typ.eqb (get_type t3) ta) l) -> t1 = t2); rewrite !Typ.eqb_spec; intros [H1 _] [H2 _]; subst; auto. + intros t1 t2; destruct (typ_nop n) as [ta t']; + unfold is_true; rewrite !andb_true_iff; + change (is_true (Typ.eqb t' t1) /\ is_true + (List.forallb (fun t3 : int => Typ.eqb (get_type t3) ta) l) -> is_true (Typ.eqb t' t2) /\ is_true (List.forallb + (fun t3 : int => Typ.eqb (get_type t3) ta) l) -> t1 = t2); rewrite !Typ.eqb_spec; intros [H1 _] [H2 _]; subst; auto. (* Application *) intros t1 t2;destruct (v_type Typ.ftype interp_ft (t_func.[ i])). unfold is_true;rewrite !andb_true_iff;intros [_ H1] [_ H2]. @@ -759,21 +1228,222 @@ Module Atom. Lemma check_aux_dec : forall a, {exists T, check_aux a T} + {forall T, check_aux a T = false}. Proof. - intros [op|op h|op h1 h2|op ha|f args]; simpl. + intros [op|op h|op h1 h2|op ha i i0|f args | i e ]; simpl. (* Constants *) left; destruct op; simpl. exists Typ.Tpositive; auto. exists Typ.TZ; auto. + exists (Typ.TBV n); now rewrite N.eqb_refl. (* Unary operators *) - destruct op; simpl; try (case (Typ.eqb (get_type h) Typ.Tpositive); [left; exists Typ.Tpositive|right; intro; rewrite andb_false_r]; reflexivity); try (case (Typ.eqb (get_type h) Typ.Tpositive); [left; exists Typ.TZ|right; intro; rewrite andb_false_r]; reflexivity); case (Typ.eqb (get_type h) Typ.TZ); [left; exists Typ.TZ|right; intro; rewrite andb_false_r]; reflexivity. + destruct op; simpl; + (case (Typ.eqb (get_type h) Typ.Tpositive)). + left; exists Typ.Tpositive; easy. + right; intros; rewrite andb_false_r; easy. + left; exists Typ.Tpositive; easy. + right; intros; rewrite andb_false_r; easy. + + left; exists Typ.TZ; easy. + right; intros; rewrite andb_false_r; easy. + left; exists Typ.TZ; easy. + right; intros; rewrite andb_false_r; easy. + + + (case (Typ.eqb (get_type h) Typ.TZ)). + left. exists Typ.TZ. easy. + right. intros. rewrite andb_false_r. easy. + + (case (Typ.eqb (get_type h) Typ.TZ)). + left. exists Typ.TZ. easy. + right. intros. rewrite andb_false_r. easy. + + (case (Typ.eqb (get_type h) (Typ.TBV n))). + left. exists Typ.Tbool. easy. + right. intros. rewrite andb_false_r. easy. + + (case (Typ.eqb (get_type h) (Typ.TBV n))). + left. exists Typ.Tbool. easy. + right. intros. rewrite andb_false_r. easy. + + (case (Typ.eqb (get_type h) (Typ.TBV n))). + left. exists (Typ.TBV n). now rewrite N.eqb_refl; easy. + right. intros. rewrite andb_false_r. easy. + + (case (Typ.eqb (get_type h) (Typ.TBV n))). + left. exists (Typ.TBV n). now rewrite N.eqb_refl; easy. + right. intros. rewrite andb_false_r. easy. + + (case (Typ.eqb (get_type h) (Typ.TBV n))). + left. exists (Typ.TBV n). now rewrite N.eqb_refl; easy. + right. intros. rewrite andb_false_r. easy. + + (case (Typ.eqb (get_type h) (Typ.TBV n))). + left. exists (Typ.TBV n). now rewrite N.eqb_refl; easy. + right. intros. rewrite andb_false_r. easy. + + (case (Typ.eqb (get_type h) (Typ.TBV n1))). + left. exists (Typ.TBV n0). now rewrite N.eqb_refl; easy. + right. intros. rewrite andb_false_r. easy. + + (case (Typ.eqb (get_type h) (Typ.TBV n1))). + left. exists (Typ.TBV n0). now rewrite N.eqb_refl; easy. + right. intros. rewrite andb_false_r. easy. + + (case (Typ.eqb (get_type h) (Typ.TBV n))). + left. exists (Typ.TBV (i + n)). now rewrite N.eqb_refl; easy. + right. intros. rewrite andb_false_r. easy. + + (case (Typ.eqb (get_type h) (Typ.TBV n))). + left. exists (Typ.TBV (i + n)). now rewrite N.eqb_refl; easy. + right. intros. rewrite andb_false_r. easy. + + (case (Typ.eqb (get_type h) (Typ.TBV n))). + left. exists (Typ.TBV (i + n)). now rewrite N.eqb_refl; easy. + right. intros. rewrite andb_false_r. easy. + + (case (Typ.eqb (get_type h) (Typ.TBV n))). + left. exists (Typ.TBV (i + n)). now rewrite N.eqb_refl; easy. + right. intros. rewrite andb_false_r. easy. + (* Binary operators *) - destruct op; simpl; try (case (Typ.eqb (get_type h1) Typ.TZ); [case (Typ.eqb (get_type h2) Typ.TZ); [left; exists Typ.TZ|right; intro; rewrite andb_false_r]|right; intro; rewrite andb_false_r]; reflexivity); try (case (Typ.eqb (get_type h1) Typ.TZ); [case (Typ.eqb (get_type h2) Typ.TZ); [left; exists Typ.Tbool|right; intro; rewrite andb_false_r]|right; intro; rewrite andb_false_r]; reflexivity); case (Typ.eqb (get_type h1) t); [case (Typ.eqb (get_type h2) t); [left; exists Typ.Tbool|right; intro; rewrite andb_false_r]|right; intro; rewrite andb_false_r]; reflexivity. + destruct op; simpl. + (case (Typ.eqb (get_type h1) Typ.TZ)); (case (Typ.eqb (get_type h2) Typ.TZ)). + left. exists Typ.TZ. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + (case (Typ.eqb (get_type h1) Typ.TZ)); (case (Typ.eqb (get_type h2) Typ.TZ)). + left. exists Typ.TZ. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _ )). + left. exists Typ.TZ. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). + left. exists Typ.Tbool. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). + left. exists Typ.Tbool. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). + left. exists Typ.Tbool. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). + left. exists Typ.Tbool. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). + left. exists Typ.Tbool. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + (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_BVor*) + (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_BVxor*) + (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_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. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + (*additional case for BO_BVmult*) + (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_BVult*) + (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). + left. exists (Typ.Tbool). 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_BVslt*) + (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). + left. exists (Typ.Tbool). 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_BVconcat*) + (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). + left. exists (Typ.TBV (n + n0)). 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_BVshl*) + (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_BVshr*) + (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. + + + (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). + left. exists t0. rewrite Typ.eqb_refl. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + + + (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). + left. exists t. rewrite Typ.eqb_refl. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + + (* Ternary operators *) + revert i i0; destruct op; simpl. intros h1 h2. + (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)); + (case (Typ.eqb (get_type ha) _)). + left. exists (Typ.TFArray t t0). rewrite !Typ.eqb_refl. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. + right. intros. rewrite andb_false_r. easy. (* N-ary operators *) - destruct op as [ty]; simpl; case (List.forallb (fun t1 : int => Typ.eqb (get_type t1) ty) ha). + destruct f as [ty]; simpl; case (List.forallb (fun t1 : int => Typ.eqb (get_type t1) ty) args). left; exists Typ.Tbool; auto. right; intro T; rewrite andb_false_r; auto. (* Application *) - case (v_type Typ.ftype interp_ft (t_func .[ f])); intros; apply check_args_dec. + case (v_type Typ.ftype interp_ft (t_func .[ i])); intros; apply check_args_dec. Qed. End Typ_Aux. @@ -799,6 +1469,16 @@ Module Atom. | _, _ => bvtrue end. + Definition apply_terop (t1 t2 t3 r : Typ.type) + (op : interp_t t1 -> interp_t t2 -> interp_t t3 -> interp_t r) (tv1 tv2 tv3: bval) := + let (t1', v1) := tv1 in + let (t2', v2) := tv2 in + let (t3', v3) := tv3 in + match Typ.cast t1' t1, Typ.cast t2' t2, Typ.cast t3' t3 with + | Typ.Cast k1, Typ.Cast k2, Typ.Cast k3 => Bval r (op (k1 _ v1) (k2 _ v2) (k3 _ v3)) + | _, _, _ => bvtrue + end. + Fixpoint apply_func targs tr (f:interp_ft (targs,tr)) (lv:list bval) : bval := match targs as targs0 return interp_ft (targs0,tr) -> bval with @@ -824,19 +1504,30 @@ Module Atom. match o with | CO_xH => Bval Typ.Tpositive xH | CO_Z0 => Bval Typ.TZ Z0 + | CO_BV bv s => Bval (Typ.TBV s) (BITVECTOR_LIST._of_bits bv s) end. - Definition interp_uop o := + Definition interp_uop o := match o with | UO_xO => apply_unop Typ.Tpositive Typ.Tpositive xO | UO_xI => apply_unop Typ.Tpositive Typ.Tpositive xI | UO_Zpos => apply_unop Typ.Tpositive Typ.TZ Zpos | UO_Zneg => apply_unop Typ.Tpositive Typ.TZ Zneg | UO_Zopp => apply_unop Typ.TZ Typ.TZ Zopp + | UO_BVbitOf s n => apply_unop (Typ.TBV s) Typ.Tbool (BITVECTOR_LIST.bitOf n) + | UO_BVnot s => apply_unop (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_not s) + | UO_BVneg s => apply_unop (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_neg s) + | UO_BVextr i n0 n1 => + apply_unop (Typ.TBV n1) (Typ.TBV n0) (@BITVECTOR_LIST.bv_extr i n0 n1) + | UO_BVzextn s i => + apply_unop (Typ.TBV s) (Typ.TBV (i + s)) (@BITVECTOR_LIST.bv_zextn s i) + | UO_BVsextn s i => + apply_unop (Typ.TBV s) (Typ.TBV (i + s)) (@BITVECTOR_LIST.bv_sextn s i) end. + Definition interp_bop o := - match o with + match o with | BO_Zplus => apply_binop Typ.TZ Typ.TZ Typ.TZ Zplus | BO_Zminus => apply_binop Typ.TZ Typ.TZ Typ.TZ Zminus | BO_Zmult => apply_binop Typ.TZ Typ.TZ Typ.TZ Zmult @@ -845,6 +1536,37 @@ Module Atom. | BO_Zge => apply_binop Typ.TZ Typ.TZ Typ.Tbool Zge_bool | BO_Zgt => apply_binop Typ.TZ Typ.TZ Typ.Tbool Zgt_bool | BO_eq t => apply_binop t t Typ.Tbool (Typ.i_eqb t_i t) + | BO_BVand s => + apply_binop (Typ.TBV s) (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_and s) + | BO_BVor s => + apply_binop (Typ.TBV s) (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_or s) + | BO_BVxor s => + 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 => + apply_binop (Typ.TBV s) (Typ.TBV s) Typ.Tbool (@BITVECTOR_LIST.bv_ult s) + | BO_BVslt s => + apply_binop (Typ.TBV s) (Typ.TBV s) Typ.Tbool (@BITVECTOR_LIST.bv_slt s) + | BO_BVconcat s1 s2 => + apply_binop (Typ.TBV s1) (Typ.TBV s2) (Typ.TBV (s1 + s2)) (@BITVECTOR_LIST.bv_concat s1 s2) + | BO_BVshl s => + apply_binop (Typ.TBV s) (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_shl s) + | BO_BVshr s => + apply_binop (Typ.TBV s) (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_shr s) + | BO_select ti te => apply_binop (Typ.TFArray ti te) ti te FArray.select + | BO_diffarray ti te => + apply_binop (Typ.TFArray ti te) (Typ.TFArray ti te) ti FArray.diff + end. + + Definition interp_top o := + match o with + | TO_store ti te => + apply_terop (Typ.TFArray ti te) ti te (Typ.TFArray ti te) FArray.store end. Fixpoint compute_interp ty acc l := @@ -884,8 +1606,8 @@ Module Atom. Lemma compute_interp_spec : forall ty l acc, match compute_interp ty acc l with - | Some l' => forall i j, In2 i j l' <-> (In2 i j acc \/ (In j acc /\ exists a, In a l /\ interp_hatom a = Bval ty i) \/ (exists a b, In2 b a l /\ interp_hatom a = Bval ty i /\ interp_hatom b = Bval ty j)) - | None => exists a, In a l /\ let (ta,_) := interp_hatom a in ta <> ty + | Some l' => forall i j, In2 i j l' <-> (In2 i j acc \/ (List.In j acc /\ exists a, List.In a l /\ interp_hatom a = Bval ty i) \/ (exists a b, In2 b a l /\ interp_hatom a = Bval ty i /\ interp_hatom b = Bval ty j)) + | None => exists a, List.In a l /\ let (ta,_) := interp_hatom a in ta <> ty end. Proof. intro ty; induction l as [ |a q IHq]; simpl. @@ -932,7 +1654,7 @@ Module Atom. Lemma compute_interp_spec_rev : forall ty l, match compute_interp ty nil l with | Some l' => forall i j, In2 j i (rev l') <-> (exists a b, In2 b a l /\ interp_hatom a = Bval ty i /\ interp_hatom b = Bval ty j) - | None => exists a, In a l /\ let (ta,_) := interp_hatom a in ta <> ty + | None => exists a, List.In a l /\ let (ta,_) := interp_hatom a in ta <> ty end. Proof. intros ty l; generalize (compute_interp_spec ty l nil); case (compute_interp ty nil l); auto; intros l' H i j; rewrite In2_rev, (H i j); split; auto; intros [H1|[[H1 _]|H1]]; auto; inversion H1. @@ -943,6 +1665,7 @@ Module Atom. | Acop o => interp_cop o | Auop o a => interp_uop o (interp_hatom a) | Abop o a1 a2 => interp_bop o (interp_hatom a1) (interp_hatom a2) + | Atop o a1 a2 a3 => interp_top o (interp_hatom a1) (interp_hatom a2) (interp_hatom a3) | Anop (NO_distinct t) a => match compute_interp t nil a with | Some l => Bval Typ.Tbool (distinct (Typ.i_eqb t_i t) (rev l)) @@ -961,6 +1684,14 @@ Module Atom. | _ => true end. + Definition interp_bv (v:bval) (s:N) : BITVECTOR_LIST.bitvector s := + let (t,v) := v in + match Typ.cast t (Typ.TBV s) with + | Typ.Cast k => k _ v + | _ => BITVECTOR_LIST.zeros s + end. + + (* If an atom is well-typed, it has an interpretation *) @@ -987,20 +1718,114 @@ Module Atom. check_aux get_type a t -> exists v, interp_aux a = (Bval t v). Proof. - intros [op|op h|op h1 h2|op ha|f l]; simpl. + intros [op|op h|op h1 h2|op h1 h2 h3|op ha|f l]; simpl. (* Constants *) - destruct op; intros [i| | | ]; simpl; try discriminate; intros _. + destruct op as [ | |l n]; intros [ | i | | | |size]; simpl; try discriminate. exists 1%positive; auto. exists 0%Z; auto. + intros H. exists (BITVECTOR_LIST._of_bits l size). unfold is_true in H. rewrite N.eqb_eq in H. now rewrite H. (* Unary operators *) - destruct op; intros [i| | | ]; simpl; try discriminate; rewrite Typ.eqb_spec; intro H1; destruct (check_aux_interp_hatom h) as [x Hx]; rewrite Hx; simpl; generalize x Hx; rewrite H1; intros y Hy; rewrite Typ.cast_refl. + destruct op as [ | | | | |n n0|n|n|n n0 n1|n n0|n n0]; intros [ | ind| | | |size]; + simpl; try discriminate; try rewrite Typ.eqb_spec; + intros H1a; destruct (check_aux_interp_hatom h) + as [x Hx]; rewrite Hx; simpl; generalize x Hx; + try rewrite H1a; intros y Hy; try rewrite Typ.cast_refl. exists (y~0)%positive; auto. exists (y~1)%positive; auto. exists (Zpos y); auto. exists (Zneg y); auto. exists (- y)%Z; auto. - (* Binary operators *) - destruct op as [ | | | | | | |A]; intros [i| | | ]; simpl; try discriminate; unfold is_true; rewrite andb_true_iff; try (change (Typ.eqb (get_type h1) Typ.TZ = true /\ Typ.eqb (get_type h2) Typ.TZ = true) with (is_true (Typ.eqb (get_type h1) Typ.TZ) /\ is_true (Typ.eqb (get_type h2) Typ.TZ)); rewrite !Typ.eqb_spec; intros [H1 H2]; destruct (check_aux_interp_hatom h1) as [x1 Hx1]; rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl; generalize x1 Hx1 x2 Hx2; rewrite H1, H2; intros y1 Hy1 y2 Hy2; rewrite !Typ.cast_refl). + (* bitOf *) + exists (BITVECTOR_LIST.bitOf n0 y); auto. + (* bv_not *) + intros. + apply andb_true_iff in H1a. destruct H1a as (Ha, Hb). + rewrite N.eqb_eq in Ha. + revert x y Hx Hy Hb. + rewrite <- Ha in *. intros. + apply Typ.eqb_spec in Hb. + revert x y Hx Hy. + rewrite Hb. intros. + exists (@BITVECTOR_LIST.bv_not n y); auto. rewrite Typ.cast_refl; auto. + (* bv_neg *) + intros. + apply andb_true_iff in H1a. destruct H1a as (Ha, Hb). + rewrite N.eqb_eq in Ha. + revert x y Hx Hy Hb. + rewrite <- Ha in *. intros. + apply Typ.eqb_spec in Hb. + revert x y Hx Hy. + rewrite Hb. intros. + exists (@BITVECTOR_LIST.bv_neg n y); auto. rewrite Typ.cast_refl; auto. + (* bv_extr *) + intros. + apply andb_true_iff in H1a. destruct H1a as (Ha, Hb). + rewrite N.eqb_eq in Ha. + revert x y Hx Hy Hb. + rewrite <- Ha in *. intros. + apply Typ.eqb_spec in Hb. + revert x y Hx Hy. + rewrite Hb. intros. + exists (@BITVECTOR_LIST.bv_extr n n0 n1 y); auto. rewrite Typ.cast_refl; auto. + (* bv_zextn *) + intros. + apply andb_true_iff in H1a. destruct H1a as (Ha, Hb). + rewrite N.eqb_eq in Ha. + revert x y Hx Hy Hb. + rewrite <- Ha in *. intros. + apply Typ.eqb_spec in Hb. + revert x y Hx Hy. + rewrite Hb. intros. + exists (@BITVECTOR_LIST.bv_zextn n n0 y); auto. rewrite Typ.cast_refl; auto. + (* bv_sextn *) + intros. + apply andb_true_iff in H1a. destruct H1a as (Ha, Hb). + rewrite N.eqb_eq in Ha. + revert x y Hx Hy Hb. + rewrite <- Ha in *. intros. + apply Typ.eqb_spec in Hb. + revert x y Hx Hy. + 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]; + [ 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 ] | + 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 ] | + 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 ] | + 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; + try (rewrite andb_true_iff ;change (Typ.eqb (get_type h1) Typ.TZ = true /\ Typ.eqb (get_type h2) Typ.TZ = true) with + (is_true (Typ.eqb (get_type h1) Typ.TZ) /\ is_true (Typ.eqb (get_type h2) Typ.TZ)); + rewrite !Typ.eqb_spec; intros [H1 H2]; + destruct (check_aux_interp_hatom h1) as [x1 Hx1]; + rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; + rewrite Hx2; simpl; generalize x1 Hx1 x2 Hx2; + rewrite H1, H2; intros y1 Hy1 y2 Hy2; rewrite !Typ.cast_refl); + + try (change (Typ.eqb (get_type h1) Typ.TBV = true /\ Typ.eqb (get_type h2) Typ.TBV = true) with + (is_true (Typ.eqb (get_type h1) Typ.TBV) /\ is_true (Typ.eqb (get_type h2) Typ.TBV)); + rewrite !Typ.eqb_spec; intros [H1 H2]; + destruct (check_aux_interp_hatom h1) as [x1 Hx1]; + rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; + rewrite Hx2; simpl; generalize x1 Hx1 x2 Hx2; rewrite H1, H2; + intros y1 Hy1 y2 Hy2; rewrite !Typ.cast_refl). + exists (y1 + y2)%Z; auto. exists (y1 - y2)%Z; auto. exists (y1 * y2)%Z; auto. @@ -1008,14 +1833,218 @@ Module Atom. exists (y1 <=? y2)%Z; auto. exists (y1 >=? y2)%Z; auto. exists (y1 >? y2)%Z; auto. - change (Typ.eqb (get_type h1) A = true /\ Typ.eqb (get_type h2) A = true) with (is_true (Typ.eqb (get_type h1) A) /\ is_true (Typ.eqb (get_type h2) A)); rewrite !Typ.eqb_spec; intros [H1 H2]; destruct (check_aux_interp_hatom h1) as [x1 Hx1]; rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl; generalize x1 Hx1 x2 Hx2; rewrite H1, H2; intros y1 Hy1 y2 Hy2; rewrite !Typ.cast_refl; exists (Typ.i_eqb t_i A y1 y2); auto. + rewrite andb_true_iff ; change (Typ.eqb (get_type h1) A = true /\ Typ.eqb (get_type h2) A = true) with + (is_true (Typ.eqb (get_type h1) A) /\ is_true (Typ.eqb (get_type h2) A)); + rewrite !Typ.eqb_spec; intros [H1 H2]; destruct (check_aux_interp_hatom h1) as [x1 Hx1]; + rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl; + generalize x1 Hx1 x2 Hx2; rewrite H1, H2; intros y1 Hy1 y2 Hy2; rewrite !Typ.cast_refl; + exists (Typ.i_eqb t_i A y1 y2); auto. + (*BO_BVand*) + 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_and y1 y2); auto. + (*BO_BVor*) + 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_or y1 y2); auto. + (*BO_BVxor*) + 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_xor y1 y2); auto. + (*BO_BVadd*) + 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_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). + 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_mult y1 y2); auto. + (*BO_BVult*) + intros. rewrite !andb_true_iff in H. destruct H as (Hb, Hc). + apply Typ.eqb_spec in Hb. + apply Typ.eqb_spec in Hc. + + 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_ult y1 y2); auto. + (*BO_BVslt*) + intros. rewrite !andb_true_iff in H. destruct H as (Hb, Hc). + apply Typ.eqb_spec in Hb. + apply Typ.eqb_spec in Hc. + + 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_slt y1 y2); auto. + (*BO_BVconcat*) + intros. rewrite !andb_true_iff in H. destruct H as ((Ha, Hb), Hc). + apply N.eqb_eq in Ha. + apply Typ.eqb_spec in Hb. + apply Typ.eqb_spec in Hc. + + 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. + rewrite <- Ha. + exists (BITVECTOR_LIST.bv_concat y1 y2); auto. + (*BO_BVshl*) + 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_shl y1 y2); auto. + (*BO_BVshr*) + 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_shr y1 y2); auto. + + (* BO_select *) + intros t' H. + rewrite !andb_true_iff in H. + destruct H as ((H1, H2), H3). + destruct (check_aux_interp_hatom h1) as [x1 Hx1]. + rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl. + apply Typ.eqb_spec in H1. + apply Typ.eqb_spec in H2. + apply Typ.eqb_spec in H3. + revert x1 Hx1 x2 Hx2. + rewrite H2, H3, H1. + rewrite !Typ.cast_refl. + intros. + exists (FArray.select x1 x2); auto. + + (* BO_diffarray *) + intros t' H. + rewrite !andb_true_iff in H. + destruct H as ((H1, H2), H3). + destruct (check_aux_interp_hatom h1) as [x1 Hx1]. + rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl. + apply Typ.eqb_spec in H1. + apply Typ.eqb_spec in H2. + apply Typ.eqb_spec in H3. + revert x1 Hx1 x2 Hx2. + rewrite H2, H3, H1. + rewrite !Typ.cast_refl. + intros. + exists (FArray.diff x1 x2); auto. + + (* Ternary operatores *) + destruct op as [ti te]; intros [ ti' te' | | | | | ]; + simpl; try discriminate; unfold is_true. + intros H. + rewrite !andb_true_iff in H. + destruct H as ((((H1, H2), H3), H4), H5). + apply Typ.eqb_spec in H1. + apply Typ.eqb_spec in H2. + apply Typ.eqb_spec in H3. + apply Typ.eqb_spec in H4. + apply Typ.eqb_spec in H5. + destruct (check_aux_interp_hatom h1) as [x1 Hx1]. rewrite Hx1; + destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; + destruct (check_aux_interp_hatom h3) as [x3 Hx3]; rewrite Hx3; simpl. + revert x1 Hx1 x2 Hx2 x3 Hx3. + rewrite H3, H4, H5, H1, H2. + intros. + rewrite !Typ.cast_refl. + intros. + exists (FArray.store x1 x2 x3); auto. + (* N-ary operators *) - destruct op as [A]; simpl; intros [ | | | ]; try discriminate; simpl; intros _; case (compute_interp A nil ha). + destruct op as [A]; simpl; intros [ | | | | | ]; try discriminate; simpl; intros _; case (compute_interp A nil ha). intro l; exists (distinct (Typ.i_eqb t_i A) (rev l)); auto. exists true; auto. (* Application *) intro t; apply check_args_interp_aux. - Qed. +Qed. (* If an atom is not well-typed, its interpretation is bvtrue *) @@ -1039,15 +2068,201 @@ Module Atom. (forall T, check_aux get_type a T = false) -> interp_aux a = bvtrue. Proof. - intros [op|op h|op h1 h2|op ha|f l]; simpl. + intros [op | op h | op h1 h2 | op h1 h2 h3 | op ha | f l]; simpl. (* Constants *) destruct op; simpl; intro H. discriminate (H Typ.Tpositive). discriminate (H Typ.TZ). + specialize (H (Typ.TBV n)). simpl in H. rewrite N.eqb_refl in H. now contradict H. (* Unary operators *) - destruct op; simpl; intro H; destruct (check_aux_interp_hatom h) as [v Hv]; rewrite Hv; simpl; rewrite Typ.neq_cast; try (pose (H2 := H Typ.Tpositive); simpl in H2; rewrite H2; auto); pose (H2 := H Typ.TZ); simpl in H2; rewrite H2; auto. + destruct op; simpl; intro H; destruct (check_aux_interp_hatom h) as [v Hv]; + rewrite Hv; simpl; rewrite Typ.neq_cast; + try (pose (H2 := H Typ.Tpositive); simpl in H2; rewrite H2; auto); + try (pose (H2 := H Typ.TZ); simpl in H2; rewrite H2; auto); + try (pose (H2 := H Typ.Tbool); simpl in H2; rewrite H2; auto); + try (pose (H2 := H Typ.TBV); simpl in H2; rewrite H2; auto). + (* bv_not *) + specialize (H (Typ.TBV n)). simpl in H. rewrite andb_false_iff in H. + destruct H as [ H | H]. + rewrite N.eqb_refl in H. now contradict H. + now rewrite H. + (* bv_neg *) + specialize (H (Typ.TBV n)). simpl in H. rewrite andb_false_iff in H. + destruct H as [ H | H]. + rewrite N.eqb_refl in H. now contradict H. + now rewrite H. + (* bv_extr *) + specialize (H (Typ.TBV n0)). simpl in H. rewrite andb_false_iff in H. + destruct H as [ H | H]. + rewrite N.eqb_refl in H. now contradict H. + now rewrite H. + (* bv_zextn *) + specialize (H (Typ.TBV (i + n))). simpl in H. rewrite andb_false_iff in H. + destruct H as [ H | H]. + rewrite N.eqb_refl in H. now contradict H. + now rewrite H. + (* bv_sextn *) + specialize (H (Typ.TBV (i + n))). simpl in H. rewrite andb_false_iff in H. + destruct H as [ H | H]. + rewrite N.eqb_refl in H. now contradict H. + now rewrite H. (* Binary operators *) - destruct op; simpl; intro H; destruct (check_aux_interp_hatom h1) as [v1 Hv1]; destruct (check_aux_interp_hatom h2) as [v2 Hv2]; rewrite Hv1, Hv2; simpl; try (pose (H2 := H Typ.TZ); simpl in H2; rewrite andb_false_iff in H2; destruct H2 as [H2|H2]; [rewrite (Typ.neq_cast (get_type h1)), H2|rewrite (Typ.neq_cast (get_type h2)), H2; case (Typ.cast (get_type h1) Typ.TZ)]; auto); try (pose (H2 := H Typ.Tbool); simpl in H2; rewrite andb_false_iff in H2; destruct H2 as [H2|H2]; [rewrite (Typ.neq_cast (get_type h1)), H2|rewrite (Typ.neq_cast (get_type h2)), H2; case (Typ.cast (get_type h1) Typ.TZ)]; auto); case (Typ.cast (get_type h1) t); auto. + destruct op; simpl; intro H; destruct (check_aux_interp_hatom h1) as [v1 Hv1]; + destruct (check_aux_interp_hatom h2) as [v2 Hv2]; rewrite Hv1, Hv2; simpl; + try (pose (H2 := H Typ.TZ); simpl in H2; rewrite andb_false_iff in H2; + destruct H2 as [H2|H2]; [rewrite (Typ.neq_cast (get_type h1)), + H2|rewrite (Typ.neq_cast (get_type h2)), H2; case (Typ.cast (get_type h1) Typ.TZ)]; auto); + try (pose (H2 := H Typ.Tbool); simpl in H2; rewrite andb_false_iff in H2; destruct H2 as [H2|H2]; + [rewrite (Typ.neq_cast (get_type h1)), H2|rewrite (Typ.neq_cast (get_type h2)), H2; case (Typ.cast (get_type h1) Typ.TZ)]; auto); + try (pose (H2 := H Typ.TBV); simpl in H2; rewrite !andb_false_iff in H2; destruct H2 as [[H2|H2]|H2]; + [rewrite N.eqb_refl in H2; discriminate | rewrite (Typ.neq_cast (get_type h1)), H2|rewrite (Typ.neq_cast (get_type h2)), H2; + case (Typ.cast (get_type h1) Typ.TBV); case (Typ.cast (get_type h1) Typ.TBV)]; auto). + intros. simpl in H. + case_eq (Typ.cast (get_type h1) t). easy. easy. + case_eq (Typ.cast (get_type h1) t). easy. easy. + (*BVand*) + 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. + (*BVor*) + 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. + (*BVxor*) + 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. + (*BVadd*) + 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. + apply Typ.cast_diff in H. rewrite H. + case (Typ.cast (get_type h1) (Typ.TBV n)); auto. + (*BVmult*) + 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. + (*BVult*) + specialize (H Typ.Tbool). simpl in H. + apply andb_false_iff in H. destruct H. + specialize (@Typ.cast_diff (get_type h1) (Typ.TBV n)). intros. + specialize (H0 H). now rewrite H0. + + case_eq (Typ.cast (get_type h1) (Typ.TBV n)). intros. + specialize (@Typ.cast_diff (get_type h2) (Typ.TBV n)). intros. + specialize (H1 H). easy. + easy. + + case_eq (Typ.cast (get_type h1) (Typ.TBV n)). intros. + specialize (@Typ.cast_diff (get_type h2) (Typ.TBV n)). intros. + specialize (H1 H2). easy. + easy. + + (*BVslt*) + specialize (H Typ.Tbool). simpl in H. + apply andb_false_iff in H. destruct H. + specialize (@Typ.cast_diff (get_type h1) (Typ.TBV n)). intros. + specialize (H0 H). now rewrite H0. + + case_eq (Typ.cast (get_type h1) (Typ.TBV n)). intros. + specialize (@Typ.cast_diff (get_type h2) (Typ.TBV n)). intros. + specialize (H1 H). easy. + easy. + + case_eq (Typ.cast (get_type h1) (Typ.TBV n)). intros. + specialize (@Typ.cast_diff (get_type h2) (Typ.TBV n)). intros. + specialize (H1 H2). easy. + easy. + (*BVconcat*) + specialize (H (Typ.TBV (n+n0))). 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. + (*BVshl*) + 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. + (*BVshr*) + 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. + + (* BO_select *) + specialize (H t0). simpl in H. + rewrite !andb_false_iff in H. destruct H. destruct H. + rewrite Typ.eqb_refl in H. now contradict H. + rewrite (Typ.cast_diff _ _ H); auto. + rewrite (Typ.cast_diff _ _ H); auto. + case (Typ.cast (get_type h1) (Typ.TFArray t t0)); auto. + + (* BO_diffarray *) + specialize (H t). simpl in H. + rewrite !andb_false_iff in H. destruct H. destruct H. + rewrite Typ.eqb_refl in H. now contradict H. + rewrite (Typ.cast_diff _ _ H); auto. + rewrite (Typ.cast_diff _ _ H); auto. + case (Typ.cast (get_type h1) (Typ.TFArray t t0)); auto. + + (* Ternary operators *) + destruct op; simpl; intro H; + destruct (check_aux_interp_hatom h1) as [v1 Hv1]; + destruct (check_aux_interp_hatom h2) as [v2 Hv2]; + destruct (check_aux_interp_hatom h3) as [v3 Hv3]; + rewrite Hv1, Hv2, Hv3; simpl. + specialize (H (Typ.TFArray t t0)). simpl in H. + rewrite !andb_false_iff in H. + destruct H as [[ [ [ H | H] | H] | H] | H]; + try (rewrite (Typ.cast_diff _ _ H); auto); + try (case (Typ.cast (get_type h1) (Typ.TFArray t t0)); auto); + try (rewrite !Typ.eqb_refl in H; now contradict H). + intros. case (Typ.cast (get_type h2) t); auto. + (* N-ary operators *) destruct op as [A]; simpl; intro H; generalize (H Typ.Tbool); simpl; clear H; assert (H: forall l1, List.forallb (fun t1 : int => Typ.eqb (get_type t1) A) ha = false -> match compute_interp A l1 ha with | Some l => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l)) | None => bvtrue end = bvtrue). induction ha as [ |h ha Iha]; simpl. @@ -1058,7 +2273,7 @@ Module Atom. apply H. (* Application *) apply check_args_interp_aux_contr. - Qed. +Qed. End Interp_Aux. @@ -1075,6 +2290,7 @@ Module Atom. | Acop _ => true | Auop _ h => h < i | Abop _ h1 h2 => (h1 < i) && (h2 < i) + | Atop _ h1 h2 h3 => (h1 < i) && (h2 < i) && (h3 < i) | Anop _ ha => List.forallb (fun h => h < i) ha | Aapp f args => List.forallb (fun h => h < i) args end. @@ -1089,6 +2305,8 @@ Module Atom. rewrite Hf;trivial. (* Binary operators *) unfold is_true in H;rewrite andb_true_iff in H;destruct H;rewrite !Hf;trivial. + (* Ternary operators *) + unfold is_true in H;rewrite !andb_true_iff in H;do 2 destruct H;rewrite !Hf;trivial. (* N-ary operators *) destruct n as [A]; replace (compute_interp f1 A nil l) with (compute_interp f2 A nil l); trivial; assert (H1: forall acc, compute_interp f2 A acc l = compute_interp f1 A acc l); auto; induction l as [ |k l IHl]; simpl; auto; intro acc; simpl in H; unfold is_true in H; rewrite andb_true_iff in H; destruct H as [H1 H2]; rewrite (Hf _ H1); destruct (f2 k) as [ta va]; destruct (Typ.cast ta A) as [ka| ]; auto. (* Application *) @@ -1205,18 +2423,32 @@ Module Atom. intros h Hh a IH; generalize (wf_t_i h Hh). case (t_atom.[h]); simpl. (* Constants *) - intros [ | ] _; simpl. + intros [ | | ] _; simpl. exists 1%positive; auto. exists 0%Z; auto. + exists (BITVECTOR_LIST._of_bits l n); auto. (* Unary operators *) - intros [ | | | | ] i H; simpl; destruct (IH i H) as [x Hx]; rewrite Hx; simpl. + + intros [ | | | | | | | | i0 n0 n1| n i0| n i0] i H; + simpl; destruct (IH i H) as [x Hx]; rewrite Hx; simpl. + case (Typ.cast (v_type Typ.type interp_t (a .[ i])) Typ.Tpositive); simpl; try (exists true; auto); intro k; exists ((k interp_t x)~0)%positive; auto. case (Typ.cast (v_type Typ.type interp_t (a .[ i])) Typ.Tpositive); simpl; try (exists true; auto); intro k; exists ((k interp_t x)~1)%positive; auto. case (Typ.cast (v_type Typ.type interp_t (a .[ i])) Typ.Tpositive); simpl; try (exists true; auto); intro k; exists (Zpos (k interp_t x)); auto. case (Typ.cast (v_type Typ.type interp_t (a .[ i])) Typ.Tpositive); simpl; try (exists true; auto); intro k; exists (Zneg (k interp_t x)); auto. case (Typ.cast (v_type Typ.type interp_t (a .[ i])) Typ.TZ); simpl; try (exists true; auto); intro k; exists (- k interp_t x)%Z; auto. - (* Binary operators *) - intros [ | | | | | | |A] 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 .[ i])) (Typ.TBV n)); simpl; [ | exists true; auto]. intro k; exists (BITVECTOR_LIST.bitOf n0 (k interp_t x)) ; auto. + case (Typ.cast (v_type Typ.type interp_t (a .[ i])) (Typ.TBV n)); simpl; [ | exists true; auto]. intro k; exists (BITVECTOR_LIST.bv_not (k interp_t x)) ; auto. + case (Typ.cast (v_type Typ.type interp_t (a .[ i])) (Typ.TBV n)); simpl; [ | exists true; auto]. intro k; exists (BITVECTOR_LIST.bv_neg (k interp_t x)) ; auto. + case (Typ.cast (v_type Typ.type interp_t (a .[ i])) (Typ.TBV n1)); + simpl; [ | exists true; auto]. intro k; exists (BITVECTOR_LIST.bv_extr i0 n0 (k interp_t x)) ; auto. + case (Typ.cast (v_type Typ.type interp_t (a .[ i])) (Typ.TBV n)); + simpl; [ | exists true; auto]. intro k. exists (BITVECTOR_LIST.bv_zextn i0 (k interp_t x)) ; auto. + case (Typ.cast (v_type Typ.type interp_t (a .[ i])) (Typ.TBV n)); + 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. 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. @@ -1225,13 +2457,95 @@ Module Atom. 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) as [k2| ]; simpl; try (exists true; reflexivity); exists (k1 interp_t x >=? k2 interp_t y); 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) as [k2| ]; simpl; try (exists true; reflexivity); exists (k1 interp_t x >? k2 interp_t y); auto. case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) A); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) A) as [k2| ]; simpl; try (exists true; reflexivity); exists (Typ.i_eqb t_i A (k1 interp_t x) (k2 interp_t y)); auto. + + (*BO_BVand*) + 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_and (k1 interp_t x) (k2 interp_t y)); + auto. + (*BO_BVor*) + 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_or (k1 interp_t x) (k2 interp_t y)); + auto. + (*BO_BVxor*) + 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_xor (k1 interp_t x) (k2 interp_t y)); + auto. + (*BO_BVadd*) + 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_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| ]; + simpl; try (exists true; reflexivity); exists (BITVECTOR_LIST.bv_mult (k1 interp_t x) (k2 interp_t y)); + auto. + (*BO_BVult*) + 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_ult (k1 interp_t x) (k2 interp_t y)); + auto. + (*BO_BVslt*) + 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_slt (k1 interp_t x) (k2 interp_t y)); + auto. + (*BO_BVconcat*) + 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 (n0))) as [k2| ]; + simpl; try (exists true; reflexivity); exists (BITVECTOR_LIST.bv_concat (k1 interp_t x) (k2 interp_t y)); + auto. + (*BO_BVshl*) + 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_shl (k1 interp_t x) (k2 interp_t y)); + auto. + (*BO_BVshr*) + 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_shr (k1 interp_t x) (k2 interp_t y)); + auto. + (* BO_select *) + case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) (Typ.TFArray ti te) ); + simpl; try (exists true; auto); intro k1; + case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) ti) as [k2| ]; + simpl; try (exists true; reflexivity). + exists (FArray.select (k1 interp_t x) (k2 interp_t y)); auto. + + (* BO_diffarray *) + case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) (Typ.TFArray ti te) ); + simpl; try (exists true; auto); intro k1; + case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) (Typ.TFArray ti te)) as [k2| ]; + simpl; try (exists true; reflexivity). + exists (FArray.diff (k1 interp_t x) (k2 interp_t y)); auto. + + (* Ternary operators *) + intros [ti te] h1 h2 h3; simpl; rewrite !andb_true_iff; intros [[H1 H2] H3]; + destruct (IH h1 H1) as [x Hx]; + destruct (IH h2 H2) as [y Hy]; + destruct (IH h3 H3) as [z Hz]; rewrite Hx, Hy, Hz; simpl. + case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) (Typ.TFArray ti te) ); + simpl; try (exists true; auto); intro k1; + case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) ti ); + simpl; try (exists true; auto); intro k2; + case (Typ.cast (v_type Typ.type interp_t (a .[ h3])) te) as [k3| ]; + simpl; try (exists true; reflexivity). + exists (FArray.store (k1 interp_t x) (k2 interp_t y) (k3 interp_t z)); auto. + (* N-ary operators *) intros [A] l; assert (forall acc, List.forallb (fun h0 : int => h0 < h) l = true -> exists v, match compute_interp (get a) A acc l with | Some l0 => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l0)) | None => bvtrue end = Bval (v_type Typ.type interp_t match compute_interp (get a) A acc l with | Some l0 => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l0)) | None => bvtrue end) v); auto; induction l as [ |i l IHl]; simpl. intros acc _; exists (distinct (Typ.i_eqb t_i A) (rev acc)); auto. intro acc; rewrite andb_true_iff; intros [H1 H2]; destruct (IH _ H1) as [va Hva]; rewrite Hva; simpl; case (Typ.cast (v_type Typ.type interp_t (a .[ i])) A); simpl; try (exists true; auto); intro k; destruct (IHl (k interp_t va :: acc) H2) as [vb Hvb]; exists vb; auto. (* Application *) intros i l H; apply (check_aux_interp_aux_lt_aux a h IH l H (t_func.[i])). - Qed. +Qed. Lemma check_aux_interp_hatom_lt : forall h, h < length t_atom -> exists v, t_interp.[h] = Bval (get_type h) v. @@ -1302,6 +2616,11 @@ Module Atom. let interp := interp_hatom t_atom in fun a => interp_bool (interp a). + Definition interp_form_hatom_bv t_atom : + hatom -> forall s, BITVECTOR_LIST.bitvector s := + let interp := interp_hatom t_atom in + fun a s => interp_bv (interp a) s. + End Typing_Interp. Definition check_atom t_atom := @@ -1319,3 +2638,24 @@ Module Atom. End Atom. Arguments Atom.Val {_} {_} _ _. + +(* These definitions are not used. This is just a hack, Coq refuses to + construct PArrays from OCaml if these are not here for some silly reason *) +(* +Section PredefinedArrays. + Variable t_i : PArray.array typ_compdec. + + Definition mkarray_typ_compdec := @PArray.make typ_compdec. + Definition arrayset_typ_compdec := @PArray.set typ_compdec. + + Definition mkarray_func := @PArray.make (Atom.tval t_i). + Definition arrayset_func := @PArray.set (Atom.tval t_i). + + Definition mkarray_form := @PArray.make Form.form. + Definition arrayset_form := @PArray.set Form.form. + + Definition mkarray_atom := @PArray.make Atom.atom. + Definition arrayset_atom := @PArray.set Atom.atom. + +End PredefinedArrays. +*) |