diff options
Diffstat (limited to 'src/Assembly')
| -rw-r--r-- | src/Assembly/Pipeline.v | 15 | ||||
| -rw-r--r-- | src/Assembly/Pseudo.v | 48 | ||||
| -rw-r--r-- | src/Assembly/QhasmUtil.v | 23 | ||||
| -rw-r--r-- | src/Assembly/Vectorize.v | 5 |
4 files changed, 50 insertions, 41 deletions
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v index 8e58e7345..87102cca8 100644 --- a/src/Assembly/Pipeline.v +++ b/src/Assembly/Pipeline.v @@ -1,8 +1,9 @@ Require Import Bedrock.Word. -Require Import QhasmCommon QhasmEvalCommon. -Require Import Pseudo Qhasm AlmostQhasm Conversion Language. -Require Import PseudoConversion AlmostConversion StringConversion. -Require Import Wordize Vectorize Pseudize. +Require Import Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmEvalCommon. +Require Import Crypto.Assembly.Pseudo Crypto.Assembly.Qhasm Crypto.Assembly.AlmostQhasm Crypto.Assembly.Conversion Crypto.Assembly.Language. +Require Import Crypto.Assembly.PseudoConversion Crypto.Assembly.AlmostConversion Crypto.Assembly.StringConversion. +Require Import Crypto.Assembly.Wordize Crypto.Assembly.Vectorize Crypto.Assembly.Pseudize. +Require Import Crypto.Util.Notations. Module Pipeline. Export AlmostQhasm Qhasm QhasmString. @@ -24,8 +25,8 @@ End Pipeline. Module PipelineExamples. Import Pipeline ListNotations StateCommon EvalUtil ListState. - Local Notation "v [[ i ]]" := (nth i v (wzero _)) (at level 40). - Local Notation "$$ v" := (natToWord _ v) (at level 40). + Local Notation "v [[ i ]]" := (nth i v (wzero _)). + Local Notation "$$ v" := (natToWord _ v). (* Definition add_example: @pseudeq 32 W32 1 1 (fun v => @@ -53,7 +54,7 @@ Module PipelineExamples. plet b := v[[0]] in (* NOTE: we want the lets in this format to unify with - pseudo_mult_dual *) + pseudo_mult_dual *) plet c := multHigh a b in plet d := a ^* b in diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v index b8aae4521..ca4700a7f 100644 --- a/src/Assembly/Pseudo.v +++ b/src/Assembly/Pseudo.v @@ -1,6 +1,7 @@ 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 Import Crypto.Util.Notations. Require Export Crypto.Util.FixCoqMistakes. Module Pseudo <: Language. @@ -31,8 +32,8 @@ Module Pseudo <: Language. }. Definition Params := Params'. - Definition State (p: Params): Type := ListState (width p). - Definition Program (p: Params): Type := + Definition State (p: Params) : Type := ListState (width p). + Definition Program (p: Params) : Type := @Pseudo (width p) (spec p) (inputs p) (outputs p). Definition Unary32: Params := mkParams 32 W32 1 1. @@ -40,7 +41,7 @@ Module Pseudo <: Language. (* Evaluation *) - Fixpoint pseudoEval {n m w s} (prog: @Pseudo w s n m) (st: ListState w): option (ListState w) := + Fixpoint pseudoEval {n m w s} (prog: @Pseudo w s n m) (st: ListState w) : option (ListState w) := match prog with | PVar n _ i => omap (getVar i st) (fun x => Some (setList [x] st)) | PMem n m v i => omap (getMem v i st) (fun x => Some (setList [x] st)) @@ -114,7 +115,7 @@ Module Pseudo <: Language. Delimit Scope pseudo_notations with p. Local Open Scope pseudo_notations. - Definition indexize {n: nat} (x: nat): Index n. + Definition indexize {n: nat} (x: nat) : Index n. intros; destruct (le_dec n 0). - exists 0; abstract intuition auto with zarith. @@ -123,60 +124,65 @@ Module Pseudo <: Language. Defined. Notation "% A" := (PVar _ (Some false) (indexize A)) - (at level 20, right associativity) : pseudo_notations. + : pseudo_notations. Notation "$ A" := (PVar _ (Some true) (indexize A)) - (at level 20, right associativity) : pseudo_notations. + : pseudo_notations. Notation "A :[ B ]:" := (PMem _ _ (indexize A) (indexize B)) - (at level 20, right associativity) : pseudo_notations. + : pseudo_notations. Notation "# A" := (PConst _ (natToWord _ A)) - (at level 20, right associativity) : pseudo_notations. + : pseudo_notations. Notation "A :+: B" := (PBin _ IAdd (PComb _ _ _ A B)) - (at level 60, right associativity) : pseudo_notations. + : pseudo_notations. Notation "A :+c: B" := (PCarry _ AddWithCarry (PComb _ _ _ A B)) - (at level 60, right associativity) : pseudo_notations. + : pseudo_notations. Notation "A :-: B" := (PBin _ ISub (PComb _ _ _ A B)) - (at level 60, right associativity) : pseudo_notations. + : pseudo_notations. Notation "A :&: B" := (PBin _ IAnd (PComb _ _ _ A B)) - (at level 45, right associativity) : pseudo_notations. + : pseudo_notations. Notation "A :^: B" := (PBin _ IXor (PComb _ _ _ A B)) - (at level 45, right associativity) : pseudo_notations. + : pseudo_notations. Notation "A :>>: B" := (PShift _ Shr (indexize B) A) - (at level 60, right associativity) : pseudo_notations. + : pseudo_notations. Notation "A :<<: B" := (PShift _ Shl (indexize B) A) - (at level 60, right associativity) : pseudo_notations. + : pseudo_notations. Notation "A :*: B" := (PDual _ Mult (PComb _ _ _ A B)) - (at level 55, right associativity) : pseudo_notations. + : pseudo_notations. + (* TODO(rsloan, from jgross): This notation is not okay. It breaks + [constr:(nat)] and [((1):nat)]. Please remove all frowny faces + from notations, and then move [Reserved Notation] line to + Fiat.Crypto.Util.Notations. *) + Reserved Notation "O :( A , B ): :?: L ::: R" (at level 70, right associativity). Notation "O :( A , B ): :?: L ::: R" := (PIf _ _ O (indexize A) (indexize B) L R) - (at level 70, right associativity) : pseudo_notations. + : pseudo_notations. Notation "F :**: e" := (PFunExp _ F e) - (at level 70, right associativity) : pseudo_notations. + : pseudo_notations. Notation "E :->: F" := (PLet _ _ _ E F) - (at level 70, right associativity) : pseudo_notations. + : pseudo_notations. Notation "A :|: B" := (PComb _ _ _ A B) - (at level 65, left associativity) : pseudo_notations. + : pseudo_notations. Notation "n ::: A :():" := (PCall _ _ n A) - (at level 65, left associativity) : pseudo_notations. + : pseudo_notations. Close Scope pseudo_notations. End Pseudo. diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v index 1ab894e94..53e9cf573 100644 --- a/src/Assembly/QhasmUtil.v +++ b/src/Assembly/QhasmUtil.v @@ -1,40 +1,41 @@ Require Import Coq.ZArith.ZArith Coq.NArith.NArith Coq.Numbers.Natural.Peano.NPeano. Require Import Crypto.Assembly.QhasmCommon. +Require Import Crypto.Util.Notations. Require Export Bedrock.Word. Require Export Crypto.Util.FixCoqMistakes. Delimit Scope nword_scope with w. Local Open Scope nword_scope. -Notation "& x" := (wordToN x) (at level 30) : nword_scope. -Notation "** x" := (NToWord _ x) (at level 30) : nword_scope. +Notation "& x" := (wordToN x) : nword_scope. +Notation "** x" := (NToWord _ x) : nword_scope. Section Util. - Definition convS {A B: Set} (x: A) (H: A = B): B := + Definition convS {A B: Set} (x: A) (H: A = B) : B := eq_rect A (fun B0 : Set => B0) x B H. - Definition high {k n: nat} (p: (k <= n)%nat) (w: word n): word k. + 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 auto with arith). Defined. - Definition low {k n: nat} (p: (k <= n)%nat) (w: word n): word k. + 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 auto with zarith). Defined. - Definition extend {k n: nat} (p: (k <= n)%nat) (w: word k): word n. + Definition extend {k n: nat} (p: (k <= n)%nat) (w: word k) : word n. refine (convS (zext w (n - k)) _). abstract (replace (k + (n - k)) with n by omega; intuition). Defined. - Definition shiftr {n} (w: word n) (k: nat): word n := + Definition shiftr {n} (w: word n) (k: nat) : word n := match (le_dec k n) with | left p => extend p (high p w) | right _ => wzero n end. - Definition mask {n} (k: nat) (w: word n): word n := + Definition mask {n} (k: nat) (w: word n) : word n := match (le_dec k n) with | left p => extend p (low p w) | right _ => w @@ -58,7 +59,7 @@ Section Util. end). Defined. - Definition break {n} (m: nat) (x: word n): word m * word (n - m). + Definition break {n} (m: nat) (x: word n) : word m * word (n - m). refine match (le_dec m n) with | left p => (extend _ (low p x), extend _ (@high (n - m) n _ x)) | right p => (extend _ x, _) @@ -67,13 +68,13 @@ Section Util. replace (n - m) with O by abstract omega; exact WO. Defined. - Definition addWithCarry {n} (x y: word n) (c: bool): word n := + Definition addWithCarry {n} (x y: word n) (c: bool) : word n := x ^+ y ^+ (natToWord _ (if c then 1 else 0)). Definition omap {A B} (x: option A) (f: A -> option B) := match x with | Some y => f y | _ => None end. - Notation "A <- X ; B" := (omap X (fun A => B)) (at level 70, right associativity). + Notation "A <- X ; B" := (omap X (fun A => B)). End Util. Close Scope nword_scope. diff --git a/src/Assembly/Vectorize.v b/src/Assembly/Vectorize.v index 4eed28aad..08e9ee356 100644 --- a/src/Assembly/Vectorize.v +++ b/src/Assembly/Vectorize.v @@ -1,20 +1,21 @@ Require Export Bedrock.Word Bedrock.Nomega. 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 Import Crypto.Util.Notations. 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. -Notation "'plet' x := y 'in' z" := (Let_In y (fun x => z)) (at level 60). +Notation "'plet' x := y 'in' z" := (Let_In y (fun x => z)). Section Vector. Import ListNotations. Definition vec T n := {x: list T | length x = n}. - Definition vget {n T} (x: vec T n) (i: {v: nat | (v < n)%nat}): T. + Definition vget {n T} (x: vec T n) (i: {v: nat | (v < n)%nat}) : T. refine ( match (proj1_sig x) as x' return (proj1_sig x) = x' -> _ with | [] => fun _ => _ |