diff options
Diffstat (limited to 'src/Assembly')
| -rw-r--r-- | src/Assembly/Pseudize.v | 17 | ||||
| -rw-r--r-- | src/Assembly/Pseudo.v | 12 | ||||
| -rw-r--r-- | src/Assembly/QhasmEvalCommon.v | 51 | ||||
| -rw-r--r-- | src/Assembly/QhasmUtil.v | 13 | ||||
| -rw-r--r-- | src/Assembly/State.v | 32 | ||||
| -rw-r--r-- | src/Assembly/Vectorize.v | 6 | ||||
| -rw-r--r-- | src/Assembly/Wordize.v | 20 |
7 files changed, 80 insertions, 71 deletions
diff --git a/src/Assembly/Pseudize.v b/src/Assembly/Pseudize.v index c167dd6a1..ea14dc52e 100644 --- a/src/Assembly/Pseudize.v +++ b/src/Assembly/Pseudize.v @@ -1,7 +1,8 @@ Require Export Bedrock.Word Bedrock.Nomega. -Require Import NArith NPeano List Sumbool Compare_dec Omega. -Require Import QhasmCommon QhasmEvalCommon QhasmUtil Pseudo State. -Require Export Wordize Vectorize. +Require Import Coq.NArith.NArith Coq.Numbers.Natural.Peano.NPeano Coq.Lists.List Coq.Bool.Sumbool Coq.Arith.Compare_dec Coq.omega.Omega. +Require Import Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmEvalCommon Crypto.Assembly.QhasmUtil Crypto.Assembly.Pseudo Crypto.Assembly.State. +Require Export Crypto.Assembly.Wordize Crypto.Assembly.Vectorize. +Require Export Crypto.Util.FixCoqMistakes. Import Pseudo ListNotations StateCommon EvalUtil ListState. @@ -34,8 +35,8 @@ Section Conversion. replace (k mod n) with k by ( assert (n <> 0) as NZ by omega; pose proof (Nat.div_mod k n NZ); - replace (k mod n) with (k - n * (k / n)) by intuition; - rewrite (Nat.div_small k n); intuition). + replace (k mod n) with (k - n * (k / n)) by intuition auto with zarith; + rewrite (Nat.div_small k n); intuition auto with zarith). autounfold; simpl. destruct (nth_error x k); simpl; try inversion H0; intuition. @@ -48,8 +49,8 @@ Section Conversion. intros; autounfold; simpl. unfold indexize; destruct (le_dec n 0), (le_dec len 0); - try replace n with 0 in * by intuition; - try replace len with 0 in * by intuition; + try replace n with 0 in * by intuition auto with zarith; + try replace len with 0 in * by intuition auto with zarith; autounfold; simpl in *; rewrite H; autounfold; simpl; rewrite NToWord_wordToN; intuition. @@ -247,7 +248,7 @@ Section Conversion. simpl; intuition. Qed. - Definition pseudeq {w s} (n m: nat) (f: list (word w) -> list (word w)) : Type := + Definition pseudeq {w s} (n m: nat) (f: list (word w) -> list (word w)) : Type := {p: @Pseudo w s n m | forall x: (list (word w)), List.length x = n -> exists m' c', pseudoEval p (x, TripleM.empty N, None) = Some (f x, m', c')}. diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v index e3f1e63ff..b8aae4521 100644 --- a/src/Assembly/Pseudo.v +++ b/src/Assembly/Pseudo.v @@ -1,6 +1,7 @@ -Require Import QhasmCommon QhasmUtil State. -Require Import Language QhasmEvalCommon. -Require Import List Compare_dec Omega. +Require Import Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmUtil Crypto.Assembly.State. +Require Import Crypto.Assembly.Language Crypto.Assembly.QhasmEvalCommon. +Require Import Coq.Lists.List Coq.Arith.Compare_dec Coq.omega.Omega. +Require Export Crypto.Util.FixCoqMistakes. Module Pseudo <: Language. Import EvalUtil ListState. @@ -96,7 +97,7 @@ Module Pseudo <: Language. else pseudoEval r st )) | PFunExp n p e => - (fix funexpseudo (e': nat) (st': ListState w) := + (fix funexpseudo (e': nat) (st': ListState w) := match e' with | O => Some st' | S e'' => @@ -116,7 +117,7 @@ Module Pseudo <: Language. Definition indexize {n: nat} (x: nat): Index n. intros; destruct (le_dec n 0). - - exists 0; abstract intuition. + - exists 0; abstract intuition auto with zarith. - exists (x mod n)%nat; abstract ( pose proof (Nat.mod_bound_pos x n); omega). Defined. @@ -179,4 +180,3 @@ Module Pseudo <: Language. Close Scope pseudo_notations. End Pseudo. - diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v index 4c64d8681..9760dc869 100644 --- a/src/Assembly/QhasmEvalCommon.v +++ b/src/Assembly/QhasmEvalCommon.v @@ -1,7 +1,8 @@ -Require Import QhasmCommon QhasmUtil State. -Require Import ZArith Sumbool. +Require Import Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmUtil Crypto.Assembly.State. +Require Import Coq.ZArith.ZArith Coq.Bool.Sumbool. Require Import Bedrock.Word. -Require Import Logic.Eqdep_dec ProofIrrelevance. +Require Import Coq.Logic.Eqdep_dec Coq.Logic.ProofIrrelevance. +Require Export Crypto.Util.FixCoqMistakes. Module EvalUtil. Definition evalTest {n} (o: TestOp) (a b: word n): bool := @@ -78,13 +79,13 @@ Module EvalUtil. Proof. induction a; unfold getWidth; simpl; intuition. Qed. Lemma width_eq {n} (a b: Width n): a = b. - Proof. + Proof. assert (Some a = Some b) as H by ( replace (Some a) with (getWidth n) by (rewrite getWidth_eq; intuition); replace (Some b) with (getWidth n) by (rewrite getWidth_eq; intuition); intuition). inversion H; intuition. - Qed. + Qed. (* Mapping Conversions *) @@ -102,29 +103,29 @@ Module EvalUtil. Definition mapping_dec {n} (a b: Mapping n): {a = b} + {a <> b}. refine (match (a, b) as p' return (a, b) = p' -> _ with - | (regM v, regM v') => fun _ => + | (regM v, regM v') => fun _ => if (Nat.eq_dec (regName v) (regName v')) then left _ else right _ - | (stackM v, stackM v') => fun _ => + | (stackM v, stackM v') => fun _ => if (Nat.eq_dec (stackName v) (stackName v')) then left _ else right _ - | (constM v, constM v') => fun _ => + | (constM v, constM v') => fun _ => if (Nat.eq_dec (constValueN v) (constValueN v')) then left _ else right _ - | (memM _ v i, memM _ v' i') => fun _ => - if (Nat.eq_dec (memName v) (memName v')) + | (memM _ v i, memM _ v' i') => fun _ => + if (Nat.eq_dec (memName v) (memName v')) then if (Nat.eq_dec (memLength v) (memLength v')) then if (Nat.eq_dec (proj1_sig i) (proj1_sig i')) then left _ else right _ else right _ else right _ | _ => fun _ => right _ - end (eq_refl (a, b))); + end (eq_refl (a, b))); try destruct v, v'; subst; unfold regName, stackName, constValueN, memName, memLength in *; repeat progress (try apply f_equal; subst; match goal with @@ -158,10 +159,10 @@ Module EvalUtil. | [ H: proj1_sig ?a <> proj1_sig ?b |- _ ] => let l0 := fresh in let l1 := fresh in destruct a, b; simpl in H; subst - | [ H: existT ?a ?b _ = existT ?a ?b _ |- _ ] => + | [ H: existT ?a ?b _ = existT ?a ?b _ |- _ ] => apply (inj_pair2_eq_dec _ Nat.eq_dec) in H; subst; intuition - | [ H: exist _ _ _ = exist _ _ _ |- _ ] => + | [ H: exist _ _ _ = exist _ _ _ |- _ ] => inversion H; subst; intuition (* Single specialized wordToNat proof *) @@ -176,12 +177,12 @@ Module EvalUtil. Definition dec_lt (a b: nat): {(a < b)%nat} + {(a >= b)%nat}. assert ({(a <? b)%nat = true} + {(a <? b)%nat <> true}) - by abstract (destruct (a <? b)%nat; intuition); + by abstract (destruct (a <? b)%nat; intuition auto with bool); destruct H. - left; abstract (apply Nat.ltb_lt; intuition). - - right; abstract (rewrite Nat.ltb_lt in *; intuition). + - right; abstract (rewrite Nat.ltb_lt in *; intuition auto with zarith). Defined. Fixpoint stackNames {n} (lst: list (Mapping n)): list nat := @@ -216,12 +217,12 @@ Module QhasmEval. omap (getReg r state) (fun v => if (Nat.eq_dec O (wordToNat v)) then Some true - else Some false) + else Some false) | CReg n o a b => omap (getReg a state) (fun va => omap (getReg b state) (fun vb => Some (evalTest o va vb))) - | CConst n o a c => + | CConst n o a c => omap (getReg a state) (fun va => Some (evalTest o va (constValueW c))) end. @@ -245,35 +246,35 @@ Module QhasmEval. let (v', co) := (evalIntOp o va vb) in Some (setCarryOpt co (setReg a v' state)))) - | IOpMem _ _ o r m i => + | IOpMem _ _ o r m i => omap (getReg r state) (fun va => omap (getMem m i state) (fun vb => let (v', co) := (evalIntOp o va vb) in Some (setCarryOpt co (setReg r v' state)))) - | DOp _ o a b (Some x) => + | DOp _ o a b (Some x) => omap (getReg a state) (fun va => omap (getReg b state) (fun vb => let (low, high) := (evalDualOp o va vb) in Some (setReg x high (setReg a low state)))) - | DOp _ o a b None => + | DOp _ o a b None => omap (getReg a state) (fun va => omap (getReg b state) (fun vb => let (low, high) := (evalDualOp o va vb) in Some (setReg a low state))) - | ROp _ o r i => + | ROp _ o r i => omap (getReg r state) (fun v => let v' := (evalRotOp o v i) in Some (setReg r v' state)) - | COp _ o a b => + | COp _ o a b => omap (getReg a state) (fun va => omap (getReg b state) (fun vb => match (getCarry state) with | None => None - | Some c0 => + | Some c0 => let (v', c') := (evalCarryOp o va vb c0) in Some (setCarry c' (setReg a v' state)) end)) @@ -281,7 +282,7 @@ Module QhasmEval. Definition evalAssignment (a: Assignment) (state: State): option State := match a with - | ARegMem _ _ r m i => + | ARegMem _ _ r m i => omap (getMem m i state) (fun v => Some (setReg r v state)) | AMemReg _ _ m i r => omap (getReg r state) (fun v => Some (setMem m i v state)) @@ -289,7 +290,7 @@ Module QhasmEval. omap (getReg b state) (fun v => Some (setStack a v state)) | ARegStack _ a b => omap (getStack b state) (fun v => Some (setReg a v state)) - | ARegReg _ a b => + | ARegReg _ a b => omap (getReg b state) (fun v => Some (setReg a v state)) | AConstInt _ r c => Some (setReg r (constValueW c) state) diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v index acf2b5c31..1ab894e94 100644 --- a/src/Assembly/QhasmUtil.v +++ b/src/Assembly/QhasmUtil.v @@ -1,6 +1,7 @@ -Require Import ZArith NArith NPeano. -Require Import QhasmCommon. +Require Import Coq.ZArith.ZArith Coq.NArith.NArith Coq.Numbers.Natural.Peano.NPeano. +Require Import Crypto.Assembly.QhasmCommon. Require Export Bedrock.Word. +Require Export Crypto.Util.FixCoqMistakes. Delimit Scope nword_scope with w. Local Open Scope nword_scope. @@ -14,12 +15,12 @@ Section Util. Definition high {k n: nat} (p: (k <= n)%nat) (w: word n): word k. refine (split1 k (n - k) (convS w _)). - abstract (replace n with (k + (n - k)) by omega; intuition). + abstract (replace n with (k + (n - k)) by omega; intuition auto with arith). Defined. Definition low {k n: nat} (p: (k <= n)%nat) (w: word n): word k. refine (split2 (n - k) k (convS w _)). - abstract (replace n with (k + (n - k)) by omega; intuition). + abstract (replace n with (k + (n - k)) by omega; intuition auto with zarith). Defined. Definition extend {k n: nat} (p: (k <= n)%nat) (w: word k): word n. @@ -61,7 +62,7 @@ Section Util. refine match (le_dec m n) with | left p => (extend _ (low p x), extend _ (@high (n - m) n _ x)) | right p => (extend _ x, _) - end; try abstract intuition. + end; try abstract intuition auto with zarith. replace (n - m) with O by abstract omega; exact WO. Defined. @@ -75,4 +76,4 @@ Section Util. Notation "A <- X ; B" := (omap X (fun A => B)) (at level 70, right associativity). End Util. -Close Scope nword_scope.
\ No newline at end of file +Close Scope nword_scope. diff --git a/src/Assembly/State.v b/src/Assembly/State.v index 8602c7f96..3467a5cad 100644 --- a/src/Assembly/State.v +++ b/src/Assembly/State.v @@ -1,12 +1,14 @@ -Require Export String List Logic. +Require Export Coq.Strings.String Coq.Lists.List Coq.Init.Logic. Require Export Bedrock.Word. -Require Import ZArith NArith NPeano Ndec. -Require Import Compare_dec Omega. -Require Import OrderedType Coq.Structures.OrderedTypeEx. -Require Import FMapPositive FMapFullAVL JMeq. +Require Import Coq.ZArith.ZArith Coq.NArith.NArith Coq.Numbers.Natural.Peano.NPeano Coq.NArith.Ndec. +Require Import Coq.Arith.Compare_dec Coq.omega.Omega. +Require Import Coq.Structures.OrderedType Coq.Structures.OrderedTypeEx. +Require Import Coq.FSets.FMapPositive Coq.FSets.FMapFullAVL Coq.Logic.JMeq. -Require Import QhasmUtil QhasmCommon. +Require Import Crypto.Assembly.QhasmUtil Crypto.Assembly.QhasmCommon. + +Require Export Crypto.Util.FixCoqMistakes. (* We want to use pairs and triples as map keys: *) @@ -50,16 +52,16 @@ Module Pair_as_OT <: UsualOrderedType. destruct (Nat_as_OT.compare x0 y0); unfold Nat_as_OT.lt, Nat_as_OT.eq in *. - - apply LT; abstract (unfold lt; simpl; destruct (Nat.eq_dec x0 y0); intuition). + - apply LT; abstract (unfold lt; simpl; destruct (Nat.eq_dec x0 y0); intuition auto with zarith). - destruct (Nat_as_OT.compare x1 y1); unfold Nat_as_OT.lt, Nat_as_OT.eq in *. + apply LT; abstract (unfold lt; simpl; destruct (Nat.eq_dec x0 y0); intuition). - + apply EQ; abstract (unfold lt; simpl; subst; intuition). - + apply GT; abstract (unfold lt; simpl; destruct (Nat.eq_dec y0 x0); intuition). + + apply EQ; abstract (unfold lt; simpl; subst; intuition auto with relations). + + apply GT; abstract (unfold lt; simpl; destruct (Nat.eq_dec y0 x0); intuition auto with zarith). - - apply GT; abstract (unfold lt; simpl; destruct (Nat.eq_dec y0 x0); intuition). + - apply GT; abstract (unfold lt; simpl; destruct (Nat.eq_dec y0 x0); intuition auto with zarith). Defined. Definition eq_dec (a b: t): {a = b} + {a <> b}. @@ -69,14 +71,14 @@ Module Pair_as_OT <: UsualOrderedType. - right; abstract ( unfold lt in *; simpl in *; destruct (Nat.eq_dec a0 b0); intuition; - inversion H; intuition). + inversion H; intuition auto with zarith). - left; abstract (inversion e; intuition). - right; abstract ( unfold lt in *; simpl in *; destruct (Nat.eq_dec b0 a0); intuition; - inversion H; intuition). + inversion H; intuition auto with zarith). Defined. End Pair_as_OT. @@ -132,7 +134,7 @@ Module Triple_as_OT <: UsualOrderedType. unfold Nat_as_OT.lt, Nat_as_OT.eq, lt, eq in *; destruct (Nat.eq_dec (get0 x) (get0 y)); destruct (Nat.eq_dec (get1 x) (get1 y)); - simpl; intuition). + simpl; intuition auto with zarith). Ltac compare_eq x y := abstract ( @@ -163,14 +165,14 @@ Module Triple_as_OT <: UsualOrderedType. - right; abstract ( unfold lt, get0, get1, get2 in *; simpl in *; destruct (Nat.eq_dec a0 b0), (Nat.eq_dec a1 b1); - intuition; inversion H; intuition). + intuition; inversion H; intuition auto with zarith). - left; abstract (inversion e; intuition). - right; abstract ( unfold lt, get0, get1, get2 in *; simpl in *; destruct (Nat.eq_dec b0 a0), (Nat.eq_dec b1 a1); - intuition; inversion H; intuition). + intuition; inversion H; intuition auto with zarith). Defined. End Triple_as_OT. diff --git a/src/Assembly/Vectorize.v b/src/Assembly/Vectorize.v index d2fca3ce6..4eed28aad 100644 --- a/src/Assembly/Vectorize.v +++ b/src/Assembly/Vectorize.v @@ -1,6 +1,8 @@ Require Export Bedrock.Word Bedrock.Nomega. -Require Import NPeano NArith PArith Ndigits Compare_dec Arith. -Require Import ProofIrrelevance Ring List Omega. +Require Import Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith Coq.PArith.PArith Coq.NArith.Ndigits Coq.Arith.Compare_dec Coq.Arith.Arith. +Require Import Coq.Logic.ProofIrrelevance Coq.setoid_ring.Ring Coq.Lists.List Coq.omega.Omega. + +Require Export Crypto.Util.FixCoqMistakes. Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y. diff --git a/src/Assembly/Wordize.v b/src/Assembly/Wordize.v index bac25db71..5e27a93b7 100644 --- a/src/Assembly/Wordize.v +++ b/src/Assembly/Wordize.v @@ -1,9 +1,11 @@ Require Export Bedrock.Word Bedrock.Nomega. -Require Import NArith PArith Ndigits Nnat NPow NPeano Ndec. -Require Import Compare_dec Omega. -Require Import FunctionalExtensionality ProofIrrelevance. -Require Import QhasmUtil QhasmEvalCommon. +Require Import Coq.NArith.NArith Coq.PArith.PArith Coq.NArith.Ndigits Coq.NArith.Nnat Coq.Numbers.Natural.Abstract.NPow Coq.Numbers.Natural.Peano.NPeano Coq.NArith.Ndec. +Require Import Coq.Arith.Compare_dec Coq.omega.Omega. +Require Import Coq.Logic.FunctionalExtensionality Coq.Logic.ProofIrrelevance. +Require Import Crypto.Assembly.QhasmUtil Crypto.Assembly.QhasmEvalCommon. + +Require Export Crypto.Util.FixCoqMistakes. Hint Rewrite wordToN_nat Nat2N.inj_add N2Nat.inj_add Nat2N.inj_mul N2Nat.inj_mul Npow2_nat : N. @@ -18,7 +20,7 @@ Section WordizeUtil. intros; unfold break in *; destruct (le_dec m n); inversion H; subst; clear H; simpl. Admitted. - + Lemma mask_wand : forall (n: nat) (x: word n) m b, (& (mask (N.to_nat m) x) < b)%N -> (& (x ^& (@NToWord n (N.ones m))) < b)%N. @@ -33,7 +35,7 @@ Section WordizeUtil. Qed. Lemma word_param_eq: forall n m, word n = word m -> n = m. - Proof. (* TODO: How do we prove this *) Admitted. + Proof. (* TODO: How do we prove this *) Admitted. Lemma word_conv_eq: forall {n m} (y: word m) p, &y = &(@convS (word m) (word n) y p). @@ -153,7 +155,7 @@ Section WordizeUtil. - intros; simpl; replace (a + 0) with a; nomega. - intros. - replace (a + S b) with (S a + b) by intuition. + replace (a + S b) with (S a + b) by intuition auto with zarith. rewrite (IHb (S a)); simpl; clear IHb. induction (Npow2 a), (Npow2 b); simpl; intuition. rewrite Pos.mul_xO_r; intuition. @@ -180,7 +182,7 @@ Section Wordization. rewrite wordToN_NToWord; intuition. apply (N.lt_le_trans _ (b + &y)%N _). - - apply N.add_lt_le_mono; try assumption; intuition. + - apply N.add_lt_le_mono; try assumption; intuition auto with relations. - replace (Npow2 n) with (b + Npow2 n - b)%N by nomega. replace (b + Npow2 n - b)%N with (b + (Npow2 n - b))%N by ( @@ -402,7 +404,7 @@ Ltac wordize_ast := | [ |- _ = _ ] => reflexivity end. -Ltac lt_crush := try abstract (clear; vm_compute; intuition). +Ltac lt_crush := try abstract (clear; vm_compute; intuition auto with zarith). (** Bounding Tactics **) |