From e11d6d06e6eda3cd5940765dbbea420416725832 Mon Sep 17 00:00:00 2001 From: Samuel Gruetter Date: Fri, 2 Feb 2018 11:21:21 -0500 Subject: add bedrock bit vectors library (bbv) as a submodule replacing the Bedrock directory --- .gitmodules | 3 + Bedrock/Nomega.v | 73 ---- Bedrock/Word.v | 1239 ------------------------------------------------------ Makefile | 2 +- _CoqProject | 9 +- bbv | 1 + 6 files changed, 11 insertions(+), 1316 deletions(-) delete mode 100644 Bedrock/Nomega.v delete mode 100644 Bedrock/Word.v create mode 160000 bbv diff --git a/.gitmodules b/.gitmodules index eb73fc298..5993f4d31 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,6 @@ [submodule "etc/coq-scripts"] path = etc/coq-scripts url = https://github.com/JasonGross/coq-scripts.git +[submodule "bbv"] + path = bbv + url = git@github.mit.edu:plv/bbv.git diff --git a/Bedrock/Nomega.v b/Bedrock/Nomega.v deleted file mode 100644 index 9c550b512..000000000 --- a/Bedrock/Nomega.v +++ /dev/null @@ -1,73 +0,0 @@ -(* Make [omega] work for [N] *) - -Require Import Coq.Arith.Arith Coq.omega.Omega Coq.NArith.NArith. - -Global Set Asymmetric Patterns. - -Local Open Scope N_scope. - -Hint Rewrite Nplus_0_r nat_of_Nsucc nat_of_Nplus nat_of_Nminus - N_of_nat_of_N nat_of_N_of_nat - nat_of_P_o_P_of_succ_nat_eq_succ nat_of_P_succ_morphism : N. - -Theorem nat_of_N_eq : forall n m, - nat_of_N n = nat_of_N m - -> n = m. - intros ? ? H; apply (f_equal N_of_nat) in H; - autorewrite with N in *; assumption. -Qed. - -Theorem Nneq_in : forall n m, - nat_of_N n <> nat_of_N m - -> n <> m. - congruence. -Qed. - -Theorem Nneq_out : forall n m, - n <> m - -> nat_of_N n <> nat_of_N m. - intuition. - match goal with H0 : _ |- _ => apply nat_of_N_eq in H0; tauto end. -Qed. - -Theorem Nlt_out : forall n m, n < m - -> (nat_of_N n < nat_of_N m)%nat. - unfold Nlt; intros ?? H. - rewrite nat_of_Ncompare in H. - apply nat_compare_Lt_lt; assumption. -Qed. - -Theorem Nlt_in : forall n m, (nat_of_N n < nat_of_N m)%nat - -> n < m. - unfold Nlt; intros. - rewrite nat_of_Ncompare. - apply (proj1 (nat_compare_lt _ _)); assumption. -Qed. - -Theorem Nge_out : forall n m, n >= m - -> (nat_of_N n >= nat_of_N m)%nat. - unfold Nge; intros ?? H. - rewrite nat_of_Ncompare in H. - apply nat_compare_ge; assumption. -Qed. - -Theorem Nge_in : forall n m, (nat_of_N n >= nat_of_N m)%nat - -> n >= m. - unfold Nge; intros. - rewrite nat_of_Ncompare. - apply nat_compare_ge; assumption. -Qed. - -Ltac nsimp H := simpl in H; repeat progress (autorewrite with N in H; simpl in H). - -Ltac pre_nomega := - try (apply nat_of_N_eq || apply Nneq_in || apply Nlt_in || apply Nge_in); simpl; - repeat (progress autorewrite with N; simpl); - repeat match goal with - | [ H : _ <> _ |- _ ] => apply Nneq_out in H; nsimp H - | [ H : _ = _ -> False |- _ ] => apply Nneq_out in H; nsimp H - | [ H : _ |- _ ] => (apply (f_equal nat_of_N) in H - || apply Nlt_out in H || apply Nge_out in H); nsimp H - end. - -Ltac nomega := pre_nomega; omega || (unfold nat_of_P in *; simpl in *; omega). diff --git a/Bedrock/Word.v b/Bedrock/Word.v deleted file mode 100644 index ecdecee3c..000000000 --- a/Bedrock/Word.v +++ /dev/null @@ -1,1239 +0,0 @@ -(** Fixed precision machine words *) - -Require Import Coq.Arith.Arith Coq.Arith.Div2 Coq.NArith.NArith Coq.Bool.Bool Coq.omega.Omega. -Require Import Bedrock.Nomega. - -Set Implicit Arguments. - - -(** * Basic definitions and conversion to and from [nat] *) - -Inductive word : nat -> Set := -| WO : word O -| WS : bool -> forall n, word n -> word (S n). - -Fixpoint wordToNat sz (w : word sz) : nat := - match w with - | WO => O - | WS false _ w' => (wordToNat w') * 2 - | WS true _ w' => S (wordToNat w' * 2) - end. - -Fixpoint wordToNat' sz (w : word sz) : nat := - match w with - | WO => O - | WS false _ w' => 2 * wordToNat w' - | WS true _ w' => S (2 * wordToNat w') - end. - -Theorem wordToNat_wordToNat' : forall sz (w : word sz), - wordToNat w = wordToNat' w. -Proof. - induction w. auto. simpl. rewrite mult_comm. reflexivity. -Qed. - -Fixpoint mod2 (n : nat) : bool := - match n with - | 0 => false - | 1 => true - | S (S n') => mod2 n' - end. - -Fixpoint natToWord (sz n : nat) : word sz := - match sz with - | O => WO - | S sz' => WS (mod2 n) (natToWord sz' (div2 n)) - end. - -Fixpoint wordToN sz (w : word sz) : N := - match w with - | WO => 0 - | WS false _ w' => N.double (wordToN w') - | WS true _ w' => N.succ_double (wordToN w') - end%N. - -Definition Nmod2 (n : N) : bool := - match n with - | N0 => false - | Npos (xO _) => false - | _ => true - end. - -Definition wzero sz := natToWord sz 0. - -Fixpoint wzero' (sz : nat) : word sz := - match sz with - | O => WO - | S sz' => WS false (wzero' sz') - end. - -Fixpoint posToWord (sz : nat) (p : positive) {struct p} : word sz := - match sz with - | O => WO - | S sz' => - match p with - | xI p' => WS true (posToWord sz' p') - | xO p' => WS false (posToWord sz' p') - | xH => WS true (wzero' sz') - end - end. - -Definition NToWord (sz : nat) (n : N) : word sz := - match n with - | N0 => wzero' sz - | Npos p => posToWord sz p - end. - -Fixpoint Npow2 (n : nat) : N := - match n with - | O => 1 - | S n' => 2 * Npow2 n' - end%N. - - -Ltac rethink := - match goal with - | [ H : ?f ?n = _ |- ?f ?m = _ ] => replace m with n; simpl; auto - end. - -Theorem mod2_S_double : forall n, mod2 (S (2 * n)) = true. - induction n; simpl; intuition; rethink. -Qed. - -Theorem mod2_double : forall n, mod2 (2 * n) = false. - induction n; simpl; intuition; rewrite <- plus_n_Sm; rethink. -Qed. - -Local Hint Resolve mod2_S_double mod2_double. - -Theorem div2_double : forall n, div2 (2 * n) = n. - induction n; simpl; intuition; rewrite <- plus_n_Sm; f_equal; rethink. -Qed. - -Theorem div2_S_double : forall n, div2 (S (2 * n)) = n. - induction n; simpl; intuition; f_equal; rethink. -Qed. - -Hint Rewrite div2_double div2_S_double : div2. - -Theorem natToWord_wordToNat : forall sz w, natToWord sz (wordToNat w) = w. - induction w as [|b]; rewrite wordToNat_wordToNat'; intuition; f_equal; unfold natToWord, wordToNat'; fold natToWord; fold wordToNat'; - destruct b; f_equal; autorewrite with div2; intuition. -Qed. - -Fixpoint pow2 (n : nat) : nat := - match n with - | O => 1 - | S n' => 2 * pow2 n' - end. - -Theorem roundTrip_0 : forall sz, wordToNat (natToWord sz 0) = 0. - induction sz; simpl; intuition. -Qed. - -Hint Rewrite roundTrip_0 : wordToNat. - -Local Hint Extern 1 (@eq nat _ _) => omega. - -Theorem untimes2 : forall n, n + (n + 0) = 2 * n. - auto. -Qed. - -Section strong. - Variable P : nat -> Prop. - - Hypothesis PH : forall n, (forall m, m < n -> P m) -> P n. - - Lemma strong' : forall n m, m <= n -> P m. - induction n; simpl; intuition; apply PH; intuition. - elimtype False; omega. - Qed. - - Theorem strong : forall n, P n. - intros; eapply strong'; eauto. - Qed. -End strong. - -Theorem div2_odd : forall n, - mod2 n = true - -> n = S (2 * div2 n). - induction n as [n] using strong; simpl; intuition. - - destruct n as [|n]; simpl in *; intuition. - discriminate. - destruct n as [|n]; simpl in *; intuition. - do 2 f_equal. - replace (div2 n + S (div2 n + 0)) with (S (div2 n + (div2 n + 0))); auto. -Qed. - -Theorem div2_even : forall n, - mod2 n = false - -> n = 2 * div2 n. - induction n as [n] using strong; simpl; intuition. - - destruct n as [|n]; simpl in *; intuition. - destruct n as [|n]; simpl in *; intuition. - discriminate. - f_equal. - replace (div2 n + S (div2 n + 0)) with (S (div2 n + (div2 n + 0))); auto. -Qed. - -Lemma wordToNat_natToWord' : forall sz w, exists k, wordToNat (natToWord sz w) + k * pow2 sz = w. - induction sz as [|sz IHsz]; simpl; intro w; intuition; repeat rewrite untimes2. - - exists w; intuition. - - case_eq (mod2 w); intro Hmw. - - specialize (IHsz (div2 w)); firstorder. - rewrite wordToNat_wordToNat' in *. - let x' := match goal with H : _ + ?x * _ = _ |- _ => x end in - rename x' into x. (* force non-auto-generated name *) - exists x; intuition. - rewrite mult_assoc. - rewrite (mult_comm x 2). - rewrite mult_comm. simpl mult at 1. - rewrite (plus_Sn_m (2 * wordToNat' (natToWord sz (div2 w)))). - rewrite <- mult_assoc. - rewrite <- mult_plus_distr_l. - rewrite H; clear H. - symmetry; apply div2_odd; auto. - - specialize (IHsz (div2 w)); firstorder. - let x' := match goal with H : _ + ?x * _ = _ |- _ => x end in - rename x' into x. (* force non-auto-generated name *) - exists x; intuition. - rewrite mult_assoc. - rewrite (mult_comm x 2). - rewrite <- mult_assoc. - rewrite mult_comm. - rewrite <- mult_plus_distr_l. - match goal with H : _ |- _ => rewrite H; clear H end. - symmetry; apply div2_even; auto. -Qed. - -Theorem wordToNat_natToWord : forall sz w, exists k, wordToNat (natToWord sz w) = w - k * pow2 sz /\ k * pow2 sz <= w. - intros sz w; destruct (wordToNat_natToWord' sz w) as [k]; exists k; intuition. -Qed. - -Definition wone sz := natToWord sz 1. - -Fixpoint wones (sz : nat) : word sz := - match sz with - | O => WO - | S sz' => WS true (wones sz') - end. - - -(** Comparisons *) - -Fixpoint wmsb sz (w : word sz) (a : bool) : bool := - match w with - | WO => a - | WS b _ x => wmsb x b - end. - -Definition whd sz (w : word (S sz)) : bool := - match w in word sz' return match sz' with - | O => unit - | S _ => bool - end with - | WO => tt - | WS b _ _ => b - end. - -Definition wtl sz (w : word (S sz)) : word sz := - match w in word sz' return match sz' with - | O => unit - | S sz'' => word sz'' - end with - | WO => tt - | WS _ _ w' => w' - end. - -Theorem WS_neq : forall b1 b2 sz (w1 w2 : word sz), - (b1 <> b2 \/ w1 <> w2) - -> WS b1 w1 <> WS b2 w2. - intros b1 b2 sz w1 w2 ? H0; intuition. - apply (f_equal (@whd _)) in H0; tauto. - apply (f_equal (@wtl _)) in H0; tauto. -Qed. - - -(** Shattering **) - -Lemma shatter_word : forall n (a : word n), - match n return word n -> Prop with - | O => fun a => a = WO - | S _ => fun a => a = WS (whd a) (wtl a) - end a. - destruct a; eauto. -Qed. - -Lemma shatter_word_S : forall n (a : word (S n)), - exists b, exists c, a = WS b c. -Proof. - intros n a; repeat eexists; apply (shatter_word a). -Qed. -Lemma shatter_word_0 : forall a : word 0, - a = WO. -Proof. - intros a; apply (shatter_word a). -Qed. - -Hint Resolve shatter_word_0. - -Require Import Coq.Logic.Eqdep_dec. - -Definition weq : forall sz (x y : word sz), {x = y} + {x <> y}. - refine (fix weq sz (x : word sz) : forall y : word sz, {x = y} + {x <> y} := - match x in word sz return forall y : word sz, {x = y} + {x <> y} with - | WO => fun _ => left _ _ - | WS b _ x' => fun y => if bool_dec b (whd y) - then if weq _ x' (wtl y) then left _ _ else right _ _ - else right _ _ - end); clear weq. - - abstract (symmetry; apply shatter_word_0). - - abstract (subst; symmetry; apply (shatter_word (n:=S _) _)). - - let y' := y in (* kludge around warning of mechanically generated names not playing well with [abstract] *) - abstract (rewrite (shatter_word y'); simpl; intro H; injection H; intros; - eauto using inj_pair2_eq_dec, eq_nat_dec). - - let y' := y in (* kludge around warning of mechanically generated names not playing well with [abstract] *) - abstract (rewrite (shatter_word y'); simpl; intro H; injection H; auto). -Defined. - -Fixpoint weqb sz (x : word sz) : word sz -> bool := - match x in word sz return word sz -> bool with - | WO => fun _ => true - | WS b _ x' => fun y => - if eqb b (whd y) - then if @weqb _ x' (wtl y) then true else false - else false - end. - -Theorem weqb_true_iff : forall sz x y, - @weqb sz x y = true <-> x = y. -Proof. - induction x as [|b ? x IHx]; simpl; intros y. - { split; auto. } - { rewrite (shatter_word y) in *. simpl in *. - case_eq (eqb b (whd y)); intros H. - case_eq (weqb x (wtl y)); intros H0. - split; auto; intros. rewrite eqb_true_iff in H. f_equal; eauto. eapply IHx; eauto. - split; intros H1; try congruence. inversion H1; clear H1; subst. - eapply inj_pair2_eq_dec in H4. eapply IHx in H4. congruence. - eapply Peano_dec.eq_nat_dec. - split; intros; try congruence. - inversion H0. apply eqb_false_iff in H. congruence. } -Qed. - -(** * Combining and splitting *) - -Fixpoint combine (sz1 : nat) (w : word sz1) : forall sz2, word sz2 -> word (sz1 + sz2) := - match w in word sz1 return forall sz2, word sz2 -> word (sz1 + sz2) with - | WO => fun _ w' => w' - | WS b _ w' => fun _ w'' => WS b (combine w' w'') - end. - -Fixpoint split1 (sz1 sz2 : nat) : word (sz1 + sz2) -> word sz1 := - match sz1 with - | O => fun _ => WO - | S sz1' => fun w => WS (whd w) (split1 sz1' sz2 (wtl w)) - end. - -Fixpoint split2 (sz1 sz2 : nat) : word (sz1 + sz2) -> word sz2 := - match sz1 with - | O => fun w => w - | S sz1' => fun w => split2 sz1' sz2 (wtl w) - end. - -Ltac shatterer := simpl; intuition; - match goal with - | [ w : _ |- _ ] => rewrite (shatter_word w); simpl - end; f_equal; auto. - -Theorem combine_split : forall sz1 sz2 (w : word (sz1 + sz2)), - combine (split1 sz1 sz2 w) (split2 sz1 sz2 w) = w. - induction sz1; shatterer. -Qed. - -Theorem split1_combine : forall sz1 sz2 (w : word sz1) (z : word sz2), - split1 sz1 sz2 (combine w z) = w. - induction sz1; shatterer. -Qed. - -Theorem split2_combine : forall sz1 sz2 (w : word sz1) (z : word sz2), - split2 sz1 sz2 (combine w z) = z. - induction sz1; shatterer. -Qed. - -Require Import Coq.Logic.Eqdep_dec. - - -Theorem combine_assoc : forall n1 (w1 : word n1) n2 n3 (w2 : word n2) (w3 : word n3) Heq, - combine (combine w1 w2) w3 - = match Heq in _ = N return word N with - | refl_equal => combine w1 (combine w2 w3) - end. - induction w1 as [|?? w1 IHw1]; simpl; intros n2 n3 w2 w3 Heq; intuition. - - rewrite (UIP_dec eq_nat_dec Heq (refl_equal _)); reflexivity. - - rewrite (IHw1 _ _ _ _ (plus_assoc _ _ _)); clear IHw1. - repeat match goal with - | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf - end. - generalize dependent (combine w1 (combine w2 w3)). - rewrite plus_assoc; intros w Heq0 e. - rewrite (UIP_dec eq_nat_dec e (refl_equal _)). - rewrite (UIP_dec eq_nat_dec Heq0 (refl_equal _)). - reflexivity. -Qed. - -Theorem split2_iter : forall n1 n2 n3 Heq w, - split2 n2 n3 (split2 n1 (n2 + n3) w) - = split2 (n1 + n2) n3 (match Heq in _ = N return word N with - | refl_equal => w - end). - induction n1 as [|n1 IHn1]; simpl; intros n2 n3 Heq w; intuition. - - rewrite (UIP_dec eq_nat_dec Heq (refl_equal _)); reflexivity. - - rewrite (IHn1 _ _ (plus_assoc _ _ _)). - f_equal. - repeat match goal with - | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf - end. - generalize dependent w. - simpl. - fold plus. - generalize (n1 + (n2 + n3)); clear. - intros n w Heq e. - generalize Heq e. - subst. - intros Heq0 e. - rewrite (UIP_dec eq_nat_dec e (refl_equal _)). - rewrite (UIP_dec eq_nat_dec Heq0 (refl_equal _)). - reflexivity. -Qed. - -Theorem combine_end : forall n1 n2 n3 Heq w, - combine (split1 n2 n3 (split2 n1 (n2 + n3) w)) - (split2 (n1 + n2) n3 (match Heq in _ = N return word N with - | refl_equal => w - end)) - = split2 n1 (n2 + n3) w. - induction n1 as [|n1 IHn1]; simpl; intros n2 n3 Heq w. - - rewrite (UIP_dec eq_nat_dec Heq (refl_equal _)). - apply combine_split. - - rewrite (shatter_word w) in *. - simpl. - eapply trans_eq; [ | apply IHn1 with (Heq := plus_assoc _ _ _) ]; clear IHn1. - repeat f_equal. - repeat match goal with - | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf - end. - simpl. - generalize dependent w. - rewrite plus_assoc. - intros w e Heq0. - rewrite (UIP_dec eq_nat_dec e (refl_equal _)). - rewrite (UIP_dec eq_nat_dec Heq0 (refl_equal _)). - reflexivity. -Qed. - - -(** * Extension operators *) - -Definition sext (sz : nat) (w : word sz) (sz' : nat) : word (sz + sz') := - if wmsb w false then - combine w (wones sz') - else - combine w (wzero sz'). - -Definition zext (sz : nat) (w : word sz) (sz' : nat) : word (sz + sz') := - combine w (wzero sz'). - - -(** * Arithmetic *) - -Definition wneg sz (x : word sz) : word sz := - NToWord sz (Npow2 sz - wordToN x). - -Definition wordBin (f : N -> N -> N) sz (x y : word sz) : word sz := - NToWord sz (f (wordToN x) (wordToN y)). - -Definition wplus := wordBin Nplus. -Definition wmult := wordBin Nmult. -Definition wmult' sz (x y : word sz) : word sz := - split2 sz sz (NToWord (sz + sz) (Nmult (wordToN x) (wordToN y))). -Definition wminus sz (x y : word sz) : word sz := wplus x (wneg y). - -Definition wnegN sz (x : word sz) : word sz := - natToWord sz (pow2 sz - wordToNat x). - -Definition wordBinN (f : nat -> nat -> nat) sz (x y : word sz) : word sz := - natToWord sz (f (wordToNat x) (wordToNat y)). - -Definition wplusN := wordBinN plus. - -Definition wmultN := wordBinN mult. -Definition wmultN' sz (x y : word sz) : word sz := - split2 sz sz (natToWord (sz + sz) (mult (wordToNat x) (wordToNat y))). - -Definition wminusN sz (x y : word sz) : word sz := wplusN x (wnegN y). - -(** * Notations *) - -Delimit Scope word_scope with word. -Bind Scope word_scope with word. - -Notation "w ~ 1" := (WS true w) - (at level 7, left associativity, format "w '~' '1'") : word_scope. -Notation "w ~ 0" := (WS false w) - (at level 7, left associativity, format "w '~' '0'") : word_scope. - -Notation "^~" := wneg. -Notation "l ^+ r" := (@wplus _ l%word r%word) (at level 50, left associativity). -Notation "l ^* r" := (@wmult _ l%word r%word) (at level 40, left associativity). -Notation "l ^- r" := (@wminus _ l%word r%word) (at level 50, left associativity). - -Theorem wordToN_nat : forall sz (w : word sz), wordToN w = N_of_nat (wordToNat w). - induction w as [|b ? w IHw]; intuition. - destruct b; unfold wordToN, wordToNat; fold wordToN; fold wordToNat. - - rewrite N_of_S. - rewrite N_of_mult. - rewrite <- IHw. - rewrite Nmult_comm. - rewrite N.succ_double_spec. - rewrite N.add_1_r. - reflexivity. - - rewrite N_of_mult. - rewrite <- IHw. - rewrite Nmult_comm. - reflexivity. -Qed. - -Theorem mod2_S : forall n k, - 2 * k = S n - -> mod2 n = true. - induction n as [n] using strong; intros. - destruct n; simpl in *. - elimtype False; omega. - destruct n; simpl in *; auto. - destruct k as [|k]; simpl in *. - discriminate. - apply H with k; auto. -Qed. - -Theorem wzero'_def : forall sz, wzero' sz = wzero sz. - unfold wzero; induction sz; simpl; intuition. - congruence. -Qed. - -Theorem posToWord_nat : forall p sz, posToWord sz p = natToWord sz (nat_of_P p). - induction p as [ p IHp | p IHp | ]; destruct sz; simpl; intuition; f_equal; try rewrite wzero'_def in *. - - rewrite ZL6. - destruct (ZL4 p) as [x Heq]; rewrite Heq; simpl. - replace (x + S x) with (S (2 * x)) by omega. - symmetry; apply mod2_S_double. - - rewrite IHp. - rewrite ZL6. - destruct (nat_of_P p); simpl; intuition. - replace (n + S n) with (S (2 * n)) by omega. - rewrite div2_S_double; auto. - - unfold nat_of_P; simpl. - rewrite ZL6. - replace (nat_of_P p + nat_of_P p) with (2 * nat_of_P p) by omega. - symmetry; apply mod2_double. - - rewrite IHp. - unfold nat_of_P; simpl. - rewrite ZL6. - replace (nat_of_P p + nat_of_P p) with (2 * nat_of_P p) by omega. - rewrite div2_double. - auto. - auto. -Qed. - -Theorem NToWord_nat : forall sz n, NToWord sz n = natToWord sz (nat_of_N n). - destruct n; simpl; intuition; try rewrite wzero'_def in *. - auto. - apply posToWord_nat. -Qed. - -Theorem wplus_alt : forall sz (x y : word sz), wplus x y = wplusN x y. - unfold wplusN, wplus, wordBinN, wordBin; intros. - - repeat rewrite wordToN_nat; repeat rewrite NToWord_nat. - rewrite nat_of_Nplus. - repeat rewrite nat_of_N_of_nat. - reflexivity. -Qed. - -Theorem wmult_alt : forall sz (x y : word sz), wmult x y = wmultN x y. - unfold wmultN, wmult, wordBinN, wordBin; intros. - - repeat rewrite wordToN_nat; repeat rewrite NToWord_nat. - rewrite nat_of_Nmult. - repeat rewrite nat_of_N_of_nat. - reflexivity. -Qed. - -Theorem Npow2_nat : forall n, nat_of_N (Npow2 n) = pow2 n. - induction n as [|n IHn]; simpl; intuition. - rewrite <- IHn; clear IHn. - case_eq (Npow2 n); intuition. - rewrite untimes2. - match goal with - | [ |- context[Npos ?p~0] ] - => replace (Npos p~0) with (Ndouble (Npos p)) by reflexivity - end. - apply nat_of_Ndouble. -Qed. - -Theorem wneg_alt : forall sz (x : word sz), wneg x = wnegN x. - unfold wnegN, wneg; intros. - repeat rewrite wordToN_nat; repeat rewrite NToWord_nat. - rewrite nat_of_Nminus. - do 2 f_equal. - apply Npow2_nat. - apply nat_of_N_of_nat. -Qed. - -Theorem wminus_Alt : forall sz (x y : word sz), wminus x y = wminusN x y. - intros; unfold wminusN, wminus; rewrite wneg_alt; apply wplus_alt. -Qed. - -Theorem wplus_unit : forall sz (x : word sz), natToWord sz 0 ^+ x = x. - intros; rewrite wplus_alt; unfold wplusN, wordBinN; intros. - rewrite roundTrip_0; apply natToWord_wordToNat. -Qed. - -Theorem wplus_comm : forall sz (x y : word sz), x ^+ y = y ^+ x. - intros; repeat rewrite wplus_alt; unfold wplusN, wordBinN; f_equal; auto. -Qed. - -Theorem drop_mod2 : forall n k, - 2 * k <= n - -> mod2 (n - 2 * k) = mod2 n. - induction n as [n] using strong; intros. - - do 2 (destruct n; simpl in *; repeat rewrite untimes2 in *; intuition). - - destruct k; simpl in *; intuition. - - destruct k; simpl; intuition. - rewrite <- plus_n_Sm. - repeat rewrite untimes2 in *. - simpl; auto. - apply H; omega. -Qed. - -Theorem div2_minus_2 : forall n k, - 2 * k <= n - -> div2 (n - 2 * k) = div2 n - k. - induction n as [n] using strong; intros. - - do 2 (destruct n; simpl in *; intuition; repeat rewrite untimes2 in *). - destruct k; simpl in *; intuition. - - destruct k; simpl in *; intuition. - rewrite <- plus_n_Sm. - apply H; omega. -Qed. - -Theorem div2_bound : forall k n, - 2 * k <= n - -> k <= div2 n. - intros ? n H; case_eq (mod2 n); intro Heq. - - rewrite (div2_odd _ Heq) in H. - omega. - - rewrite (div2_even _ Heq) in H. - omega. -Qed. - -Theorem drop_sub : forall sz n k, - k * pow2 sz <= n - -> natToWord sz (n - k * pow2 sz) = natToWord sz n. - induction sz as [|sz IHsz]; simpl; intros n k *; intuition; repeat rewrite untimes2 in *; f_equal. - - rewrite mult_assoc. - rewrite (mult_comm k). - rewrite <- mult_assoc. - apply drop_mod2. - rewrite mult_assoc. - rewrite (mult_comm 2). - rewrite <- mult_assoc. - auto. - - rewrite <- (IHsz (div2 n) k). - rewrite mult_assoc. - rewrite (mult_comm k). - rewrite <- mult_assoc. - rewrite div2_minus_2. - reflexivity. - rewrite mult_assoc. - rewrite (mult_comm 2). - rewrite <- mult_assoc. - auto. - - apply div2_bound. - rewrite mult_assoc. - rewrite (mult_comm 2). - rewrite <- mult_assoc. - auto. -Qed. - -Local Hint Extern 1 (_ <= _) => omega. - -Theorem wplus_assoc : forall sz (x y z : word sz), x ^+ (y ^+ z) = x ^+ y ^+ z. - intros sz x y z *; repeat rewrite wplus_alt; unfold wplusN, wordBinN; intros. - - repeat match goal with - | [ |- context[wordToNat (natToWord ?sz ?w)] ] => - let Heq := fresh "Heq" in - destruct (wordToNat_natToWord sz w) as [? [Heq ?]]; rewrite Heq - end. - - match goal with - | [ |- context[wordToNat ?x + wordToNat ?y - ?x1 * pow2 ?sz + wordToNat ?z] ] - => replace (wordToNat x + wordToNat y - x1 * pow2 sz + wordToNat z) - with (wordToNat x + wordToNat y + wordToNat z - x1 * pow2 sz) by auto - end. - match goal with - | [ |- context[wordToNat ?x + (wordToNat ?y + wordToNat ?z - ?x0 * pow2 ?sz)] ] - => replace (wordToNat x + (wordToNat y + wordToNat z - x0 * pow2 sz)) - with (wordToNat x + wordToNat y + wordToNat z - x0 * pow2 sz) by auto - end. - repeat rewrite drop_sub; auto. -Qed. - -Theorem roundTrip_1 : forall sz, wordToNat (natToWord (S sz) 1) = 1. - induction sz; simpl in *; intuition. -Qed. - -Theorem mod2_WS : forall sz (x : word sz) b, mod2 (wordToNat (WS b x)) = b. - intros sz x b. rewrite wordToNat_wordToNat'. - destruct b; simpl. - - rewrite untimes2. - case_eq (2 * wordToNat x); intuition. - eapply mod2_S; eauto. - rewrite <- (mod2_double (wordToNat x)); f_equal; omega. -Qed. - -Theorem div2_WS : forall sz (x : word sz) b, div2 (wordToNat (WS b x)) = wordToNat x. - destruct b; rewrite wordToNat_wordToNat'; unfold wordToNat'; fold wordToNat'. - apply div2_S_double. - apply div2_double. -Qed. - -Theorem wmult_unit : forall sz (x : word sz), natToWord sz 1 ^* x = x. - intros sz x; rewrite wmult_alt; unfold wmultN, wordBinN; intros. - destruct sz; simpl. - rewrite (shatter_word x); reflexivity. - rewrite roundTrip_0; simpl. - rewrite plus_0_r. - rewrite (shatter_word x). - f_equal. - - apply mod2_WS. - - rewrite div2_WS. - apply natToWord_wordToNat. -Qed. - -Theorem wmult_comm : forall sz (x y : word sz), x ^* y = y ^* x. - intros; repeat rewrite wmult_alt; unfold wmultN, wordBinN; auto with arith. -Qed. - -Theorem wmult_assoc : forall sz (x y z : word sz), x ^* (y ^* z) = x ^* y ^* z. - intros sz x y z; repeat rewrite wmult_alt; unfold wmultN, wordBinN; intros. - - repeat match goal with - | [ |- context[wordToNat (natToWord ?sz ?w)] ] => - let Heq := fresh "Heq" in - destruct (wordToNat_natToWord sz w) as [? [Heq ?]]; rewrite Heq - end. - - rewrite mult_minus_distr_l. - rewrite mult_minus_distr_r. - match goal with - | [ |- natToWord _ (_ - _ * (?x0' * _)) = natToWord _ (_ - ?x1' * _ * _) ] - => rename x0' into x0, x1' into x1 (* force the names to not be autogenerated *) - end. - rewrite (mult_assoc (wordToNat x) x0). - rewrite <- (mult_assoc x1). - rewrite (mult_comm (pow2 sz)). - rewrite (mult_assoc x1). - repeat rewrite drop_sub; auto with arith. - rewrite (mult_comm x1). - rewrite <- (mult_assoc (wordToNat x)). - rewrite (mult_comm (wordToNat y)). - rewrite mult_assoc. - rewrite (mult_comm (wordToNat x)). - repeat rewrite <- mult_assoc. - auto with arith. - repeat rewrite <- mult_assoc. - auto with arith. -Qed. - -Theorem wmult_plus_distr : forall sz (x y z : word sz), (x ^+ y) ^* z = (x ^* z) ^+ (y ^* z). - intros sz x y z; repeat rewrite wmult_alt; repeat rewrite wplus_alt; unfold wmultN, wplusN, wordBinN; intros. - - repeat match goal with - | [ |- context[wordToNat (natToWord ?sz ?w)] ] => - let Heq := fresh "Heq" in - destruct (wordToNat_natToWord sz w) as [? [Heq ?]]; rewrite Heq - end. - - rewrite mult_minus_distr_r. - match goal with - | [ |- natToWord _ (_ - ?x0' * _ * _) = natToWord _ (_ - ?x1' * _ + (_ - ?x2' * _)) ] - => rename x0' into x0, x1' into x1, x2' into x2 (* force the names to not be autogenerated *) - end. - rewrite <- (mult_assoc x0). - rewrite (mult_comm (pow2 sz)). - rewrite (mult_assoc x0). - - replace (wordToNat x * wordToNat z - x1 * pow2 sz + - (wordToNat y * wordToNat z - x2 * pow2 sz)) - with (wordToNat x * wordToNat z + wordToNat y * wordToNat z - x1 * pow2 sz - x2 * pow2 sz). - repeat rewrite drop_sub; auto with arith. - rewrite (mult_comm x0). - rewrite (mult_comm (wordToNat x + wordToNat y)). - rewrite <- (mult_assoc (wordToNat z)). - auto with arith. - generalize dependent (pow2 sz); intros. - repeat match goal with - | [ |- context[natToWord ?sz (?f ?x ?y)] ] => generalize dependent (f x y); intros - | [ H : context[natToWord ?sz (?f ?x ?y)] |- _ ] => generalize dependent (f x y); intros - | [ H : wordToNat (natToWord _ _) = _ |- _ ] => clear H - end. - omega. -Qed. - -Theorem wminus_def : forall sz (x y : word sz), x ^- y = x ^+ ^~ y. - reflexivity. -Qed. - -Theorem wordToNat_bound : forall sz (w : word sz), wordToNat w < pow2 sz. - induction w as [|b]; simpl; intuition. - destruct b; simpl; omega. -Qed. - -Theorem natToWord_pow2 : forall sz, natToWord sz (pow2 sz) = natToWord sz 0. - induction sz as [|sz]; simpl; intuition. - - generalize (div2_double (pow2 sz)); simpl; intro Hr; rewrite Hr; clear Hr. - f_equal. - generalize (mod2_double (pow2 sz)); auto. - auto. -Qed. - -Theorem wminus_inv : forall sz (x : word sz), x ^+ ^~ x = wzero sz. - intros sz x; rewrite wneg_alt; rewrite wplus_alt; unfold wnegN, wplusN, wzero, wordBinN; intros. - - repeat match goal with - | [ |- context[wordToNat (natToWord ?sz ?w)] ] => - let Heq := fresh "Heq" in - destruct (wordToNat_natToWord sz w) as [? [Heq ?]]; rewrite Heq - end. - - match goal with - | [ |- context[wordToNat ?x + (pow2 ?sz - wordToNat ?x - ?x0 * pow2 ?sz)] ] - => replace (wordToNat x + (pow2 sz - wordToNat x - x0 * pow2 sz)) - with (pow2 sz - x0 * pow2 sz) - end. - rewrite drop_sub; auto with arith. - apply natToWord_pow2. - generalize (wordToNat_bound x). - match goal with Heq : wordToNat (natToWord _ _) = _ |- _ => clear Heq end. - omega. -Qed. - -Definition wring (sz : nat) : ring_theory (wzero sz) (wone sz) (@wplus sz) (@wmult sz) (@wminus sz) (@wneg sz) (@eq _) := - mk_rt _ _ _ _ _ _ _ - (@wplus_unit _) (@wplus_comm _) (@wplus_assoc _) - (@wmult_unit _) (@wmult_comm _) (@wmult_assoc _) - (@wmult_plus_distr _) (@wminus_def _) (@wminus_inv _). - -Lemma wring_eq_ext (sz : nat) : ring_eq_ext (@wplus sz) (@wmult sz) (@wneg sz) (@eq _). -Proof. - constructor; repeat intro; subst; reflexivity. -Qed. - -Theorem weqb_sound : forall sz (x y : word sz), weqb x y = true -> x = y. -Proof. - eapply weqb_true_iff. -Qed. - -Arguments weqb_sound : clear implicits. - -Ltac isWcst w := - match eval hnf in w with - | WO => constr:(true) - | WS ?b ?w' => - match eval hnf in b with - | true => isWcst w' - | false => isWcst w' - | _ => constr:(false) - end - | _ => constr:(false) - end. - -Ltac wcst w := - let b := isWcst w in - match b with - | true => w - | _ => constr:(NotConstant) - end. - -(* Here's how you can add a ring for a specific bit-width. - There doesn't seem to be a polymorphic method, so this code really does need to be copied. *) - -(* -Definition wring8 := wring 8. -Add Ring wring8 : wring8 (decidable (weqb_sound 8), constants [wcst]). -*) - - -(** * Bitwise operators *) - -Fixpoint wnot sz (w : word sz) : word sz := - match w with - | WO => WO - | WS b _ w' => WS (negb b) (wnot w') - end. - -Fixpoint bitwp (f : bool -> bool -> bool) sz (w1 : word sz) : word sz -> word sz := - match w1 with - | WO => fun _ => WO - | WS b _ w1' => fun w2 => WS (f b (whd w2)) (bitwp f w1' (wtl w2)) - end. - -Definition wor := bitwp orb. -Definition wand := bitwp andb. -Definition wxor := bitwp xorb. - -Notation "l ^| r" := (@wor _ l%word r%word) (at level 50, left associativity). -Notation "l ^& r" := (@wand _ l%word r%word) (at level 40, left associativity). - -Theorem wor_unit : forall sz (x : word sz), wzero sz ^| x = x. - unfold wzero, wor; induction x; simpl; intuition congruence. -Qed. - -Theorem wor_comm : forall sz (x y : word sz), x ^| y = y ^| x. - unfold wor; induction x; intro y; rewrite (shatter_word y); simpl; intuition; f_equal; auto with bool. -Qed. - -Theorem wor_assoc : forall sz (x y z : word sz), x ^| (y ^| z) = x ^| y ^| z. - unfold wor; induction x; intro y; rewrite (shatter_word y); simpl; intuition; f_equal; auto with bool. -Qed. - -Theorem wand_unit : forall sz (x : word sz), wones sz ^& x = x. - unfold wand; induction x; simpl; intuition congruence. -Qed. - -Theorem wand_kill : forall sz (x : word sz), wzero sz ^& x = wzero sz. - unfold wzero, wand; induction x; simpl; intuition congruence. -Qed. - -Theorem wand_comm : forall sz (x y : word sz), x ^& y = y ^& x. - unfold wand; induction x; intro y; rewrite (shatter_word y); simpl; intuition; f_equal; auto with bool. -Qed. - -Theorem wand_assoc : forall sz (x y z : word sz), x ^& (y ^& z) = x ^& y ^& z. - unfold wand; induction x; intro y; rewrite (shatter_word y); simpl; intuition; f_equal; auto with bool. -Qed. - -Theorem wand_or_distr : forall sz (x y z : word sz), (x ^| y) ^& z = (x ^& z) ^| (y ^& z). - unfold wand, wor; induction x as [|b]; intro y; rewrite (shatter_word y); intro z; rewrite (shatter_word z); simpl; intuition; f_equal; auto with bool. - destruct (whd y); destruct (whd z); destruct b; reflexivity. -Qed. - -Definition wbring (sz : nat) : semi_ring_theory (wzero sz) (wones sz) (@wor sz) (@wand sz) (@eq _) := - mk_srt _ _ _ _ _ - (@wor_unit _) (@wor_comm _) (@wor_assoc _) - (@wand_unit _) (@wand_kill _) (@wand_comm _) (@wand_assoc _) - (@wand_or_distr _). - - -(** * Inequality proofs *) - -Ltac word_simpl := unfold sext, zext, wzero in *; simpl in *. - -Ltac word_eq := ring. - -Ltac word_eq1 := match goal with - | _ => ring - | [ H : _ = _ |- _ ] => ring [H] - end. - -Theorem word_neq : forall sz (w1 w2 : word sz), - w1 ^- w2 <> wzero sz - -> w1 <> w2. - intros; intro; subst. - unfold wminus in H. - rewrite wminus_inv in H. - tauto. -Qed. - -Ltac word_neq := apply word_neq; let H := fresh "H" in intro H; simpl in H; ring_simplify in H; try discriminate. - -Ltac word_contra := match goal with - | [ H : _ <> _ |- False ] => apply H; ring - end. - -Ltac word_contra1 := match goal with - | [ H : _ <> _ |- False ] => apply H; - match goal with - | _ => ring - | [ H' : _ = _ |- _ ] => ring [H'] - end - end. - -Open Scope word_scope. - -(** * Signed Logic **) -Definition wordToZ sz (w : word sz) : Z := - if wmsb w true then - (** Negative **) - match wordToN (wneg w) with - | N0 => 0%Z - | Npos x => Zneg x - end - else - (** Positive **) - match wordToN w with - | N0 => 0%Z - | Npos x => Zpos x - end. -Definition ZToWord sz (v : Z) : word sz := - if (v w2" := (@wlt _ w2%word w1%word) : word_scope. -Notation "w1 >= w2" := (~(@wlt _ w1%word w2%word)) : word_scope. -Notation "w1 < w2" := (@wlt _ w1%word w2%word) : word_scope. -Notation "w1 <= w2" := (~(@wlt _ w2%word w1%word)) : word_scope. - -Notation "w1 '>s' w2" := (@wslt _ w2%word w1%word) (at level 70) : word_scope. -Notation "w1 '>s=' w2" := (~(@wslt _ w1%word w2%word)) (at level 70) : word_scope. -Notation "w1 ' rewrite H; clear H end. - match goal with - | [ |- context[?n - ?x * pow2 (S ?sz) + (?m - ?x0 * pow2 (S ?sz))] ] - => replace (n - x * pow2 (S sz) + (m - x0 * pow2 (S sz))) with (n + m - x * pow2 (S sz) - x0 * pow2 (S sz)) - by omega - end. - repeat rewrite drop_sub; auto; omega. -Qed. - -Lemma natToWord_S : forall sz n, natToWord sz (S n) = natToWord _ 1 ^+ natToWord _ n. - intros sz n; change (S n) with (1 + n); apply natToWord_plus. -Qed. - -Theorem natToWord_inj : forall sz n m, natToWord sz n = natToWord sz m - -> (n < pow2 sz)%nat - -> (m < pow2 sz)%nat - -> n = m. - intros sz n m H H0 H1. - apply (f_equal (@wordToNat _)) in H. - destruct (wordToNat_natToWord sz n) as [x H2]. - destruct (wordToNat_natToWord sz m) as [x0 H3]. - intuition. - match goal with - | [ H : wordToNat ?x = wordToNat ?y, H' : wordToNat ?x = ?a, H'' : wordToNat ?y = ?b |- _ ] - => let H0 := fresh in assert (H0 : a = b) by congruence; clear H H' H''; rename H0 into H - end. - assert (x = 0). - destruct x; auto. - simpl in *. - generalize dependent (x * pow2 sz). - intros. - omega. - assert (x0 = 0). - destruct x0; auto. - simpl in *. - generalize dependent (x0 * pow2 sz). - intros. - omega. - subst; simpl in *; omega. -Qed. - -Lemma wordToNat_natToWord_idempotent : forall sz n, - (N.of_nat n < Npow2 sz)%N - -> wordToNat (natToWord sz n) = n. - intros sz n H. - destruct (wordToNat_natToWord sz n) as [x]; intuition. - destruct x as [|x]. - simpl in *; omega. - simpl in *. - apply Nlt_out in H. - autorewrite with N in *. - rewrite Npow2_nat in *. - generalize dependent (x * pow2 sz). - intros; omega. -Qed. - -Lemma wplus_cancel : forall sz (a b c : word sz), - a ^+ c = b ^+ c - -> a = b. - intros sz a b c H. - apply (f_equal (fun x => x ^+ ^~ c)) in H. - repeat rewrite <- wplus_assoc in H. - rewrite wminus_inv in H. - repeat rewrite (wplus_comm _ (wzero sz)) in H. - repeat rewrite wplus_unit in H. - assumption. -Qed. diff --git a/Makefile b/Makefile index b8f390a26..d482fd330 100644 --- a/Makefile +++ b/Makefile @@ -53,7 +53,7 @@ endif update-_CoqProject:: $(SHOW)'ECHO > _CoqProject' - $(HIDE)(echo '-R $(SRC_DIR) $(MOD_NAME)'; echo '-R Bedrock Bedrock'; (git ls-files 'src/*.v' 'Bedrock/*.v' | $(SORT_COQPROJECT))) > _CoqProject + $(HIDE)(echo '-R $(SRC_DIR) $(MOD_NAME)'; echo '-R bbv bbv'; (git ls-files --recurse-submodules 'src/*.v' 'bbv/*.v' | $(SORT_COQPROJECT))) > _CoqProject $(VOFILES): | coqprime diff --git a/_CoqProject b/_CoqProject index 96ffb03f9..5fd534bca 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,7 +1,10 @@ -R src Crypto --R Bedrock Bedrock -Bedrock/Nomega.v -Bedrock/Word.v +-R bbv bbv +bbv/DepEq.v +bbv/DepEqNat.v +bbv/NatLib.v +bbv/Nomega.v +bbv/Word.v src/Demo.v src/Algebra/Field.v src/Algebra/Field_test.v diff --git a/bbv b/bbv new file mode 160000 index 000000000..8bd42f213 --- /dev/null +++ b/bbv @@ -0,0 +1 @@ +Subproject commit 8bd42f21304d7a22c1b1225fe81236ad106a5309 -- cgit v1.2.3