diff options
Diffstat (limited to 'src/Assembly/GF25519.v')
| -rw-r--r-- | src/Assembly/GF25519.v | 173 |
1 files changed, 38 insertions, 135 deletions
diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v index 80d9044c4..a21b54cf0 100644 --- a/src/Assembly/GF25519.v +++ b/src/Assembly/GF25519.v @@ -9,6 +9,9 @@ Module GF25519. Definition bits: nat := 64. Definition width: Width bits := W64. + Instance ZE : Evaluable Z := @ZEvaluable bits. + Existing Instance ZE. + Fixpoint makeBoundList {n} k (b: @BoundedWord n) := match k with | O => nil @@ -17,9 +20,9 @@ Module GF25519. Section DefaultBounds. Import ListNotations. - Local Notation rr exp := (range N 0%N (2^exp + 2^exp/10)%N). + Local Notation rr exp := (2^exp + 2^exp/10)%Z. - Definition feBound: list (Range N) := + Definition feBound: list Z := [rr 26; rr 27; rr 26; rr 27; rr 26; rr 27; rr 26; rr 27; rr 26; rr 27]. End DefaultBounds. @@ -45,8 +48,7 @@ Module GF25519. Eval cbv beta delta [fe25519 add mul sub Let_In] in add. Definition ge25519_add' (P Q: @interp_type Z FE) : - { r: @HL.expr Z (@interp_type Z) FE - | HL.interp (E := ZEvaluable) (t := FE) r = ge25519_add_expr P Q }. + { r: @HL.expr Z (@interp_type Z) FE | HL.interp (t := FE) r = ge25519_add_expr P Q }. Proof. vm_compute in P, Q; repeat match goal with @@ -63,8 +65,7 @@ Module GF25519. let R := HL.rhs_of_goal in let X := HL.reify (@interp_type Z) R in - transitivity (HL.interp (E := ZEvaluable) (t := ResultType) X); - [reflexivity|]. + transitivity (HL.interp (t := ResultType) X); [reflexivity|]. cbv iota beta delta [ interp_type interp_binop HL.interp @@ -75,124 +76,10 @@ Module GF25519. Definition ge25519_add (P Q: @interp_type Z ResultType) := proj1_sig (ge25519_add' P Q). - Definition hlProg'': NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) := + Definition hlProg: NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) := liftFE (fun p => (liftFE (fun q => ge25519_add p q))). - - Definition hlProg': NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType). - refine (liftN (HLConversions.mapVar _ _) hlProg''); intro t; - [ refine LL.uninterp_arg | refine LL.interp_arg ]. - Defined. - - Definition hlProg: NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType) := - Eval vm_compute in hlProg'. End AddExpr. - Module SubExpr <: Expression. - Definition bits: nat := bits. - Definition inputs: nat := 20. - Definition width: Width bits := width. - Definition ResultType := FE. - Definition inputBounds := feBound ++ feBound. - - Definition ge25519_sub_expr := - Eval cbv beta delta [fe25519 add mul sub Let_In] in sub. - - Definition ge25519_sub' (P Q: @interp_type Z FE) : - { r: @HL.expr Z (@interp_type Z) FE - | HL.interp (E := ZEvaluable) (t := FE) r = ge25519_sub_expr P Q }. - Proof. - vm_compute in P, Q; repeat - match goal with - | [x:?T |- _] => - lazymatch T with - | Z => fail - | prod _ _ => destruct x - | _ => clear x - end - end. - - eexists. - cbv beta delta [ge25519_sub_expr]. - - let R := HL.rhs_of_goal in - let X := HL.reify (@interp_type Z) R in - transitivity (HL.interp (E := ZEvaluable) (t := ResultType) X); - [reflexivity|]. - - cbv iota beta delta [ - interp_type interp_binop HL.interp - Z.land ZEvaluable eadd esub emul eshiftr eand]. - reflexivity. - Defined. - - Definition ge25519_sub (P Q: @interp_type Z ResultType) := - proj1_sig (ge25519_sub' P Q). - - Definition hlProg'': NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) := - liftFE (fun p => (liftFE (fun q => ge25519_sub p q))). - - Definition hlProg': NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType). - refine (liftN (HLConversions.mapVar _ _) hlProg''); intro t; - [ refine LL.uninterp_arg | refine LL.interp_arg ]. - Defined. - - Definition hlProg: NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType) := - Eval vm_compute in hlProg'. - End SubExpr. - - Module MulExpr <: Expression. - Definition bits: nat := bits. - Definition inputs: nat := 20. - Definition width: Width bits := width. - Definition ResultType := FE. - Definition inputBounds := feBound ++ feBound. - - Definition ge25519_mul_expr := - Eval cbv beta delta [fe25519 add mul sub Let_In] in mul. - - Definition ge25519_mul' (P Q: @interp_type Z FE) : - { r: @HL.expr Z (@interp_type Z) FE - | HL.interp (E := ZEvaluable) (t := FE) r = ge25519_mul_expr P Q }. - Proof. - vm_compute in P, Q; repeat - match goal with - | [x:?T |- _] => - lazymatch T with - | Z => fail - | prod _ _ => destruct x - | _ => clear x - end - end. - - eexists. - cbv beta delta [ge25519_mul_expr]. - - let R := HL.rhs_of_goal in - let X := HL.reify (@interp_type Z) R in - transitivity (HL.interp (E := ZEvaluable) (t := ResultType) X); - [reflexivity|]. - - cbv iota beta delta [ - interp_type interp_binop HL.interp - Z.land ZEvaluable eadd esub emul eshiftr eand]. - reflexivity. - Defined. - - Definition ge25519_mul (P Q: @interp_type Z ResultType) := - proj1_sig (ge25519_mul' P Q). - - Definition hlProg'': NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) := - liftFE (fun p => (liftFE (fun q => ge25519_mul p q))). - - Definition hlProg': NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType). - refine (liftN (HLConversions.mapVar _ _) hlProg''); intro t; - [ refine LL.uninterp_arg | refine LL.interp_arg ]. - Defined. - - Definition hlProg: NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType) := - Eval vm_compute in hlProg'. - End MulExpr. - Module OppExpr <: Expression. Definition bits: nat := bits. Definition inputs: nat := 10. @@ -205,7 +92,7 @@ Module GF25519. Definition ge25519_opp' (P: @interp_type Z FE) : { r: @HL.expr Z (@interp_type Z) FE - | HL.interp (E := ZEvaluable) (t := FE) r = ge25519_opp_expr P }. + | HL.interp (E := @ZEvaluable bits) (t := FE) r = ge25519_opp_expr P }. Proof. vm_compute in P; repeat match goal with @@ -222,7 +109,7 @@ Module GF25519. let R := HL.rhs_of_goal in let X := HL.reify (@interp_type Z) R in - transitivity (HL.interp (E := ZEvaluable) (t := ResultType) X); + transitivity (HL.interp (E := @ZEvaluable bits) (t := ResultType) X); [reflexivity|]. cbv iota beta delta [ @@ -234,25 +121,41 @@ Module GF25519. Definition ge25519_opp (P: @interp_type Z ResultType) := proj1_sig (ge25519_opp' P). - Definition hlProg'': NAry 10 Z (@HL.expr Z (@interp_type Z) ResultType) := + Definition hlProg: NAry 10 Z (@HL.expr Z (@interp_type Z) ResultType) := liftFE (fun p => ge25519_opp p). - - Definition hlProg': NAry 10 Z (@HL.expr Z (@LL.arg Z Z) ResultType). - refine (liftN (HLConversions.mapVar _ _) hlProg''); intro t; - [ refine LL.uninterp_arg | refine LL.interp_arg ]. - Defined. - - Definition hlProg: NAry 10 Z (@HL.expr Z (@LL.arg Z Z) ResultType) := - Eval vm_compute in hlProg'. End OppExpr. Module Add := Pipeline AddExpr. - Module Sub := Pipeline SubExpr. - Module Mul := Pipeline MulExpr. Module Opp := Pipeline OppExpr. + + Section Operations. + Definition wfe: Type := @interp_type (word bits) FE. + + Definition ExprBinOp : Type := NAry 20 Z (@CompileLL.WExpr bits FE). + Definition ExprUnOp : Type := NAry 10 Z (@CompileLL.WExpr bits FE). + + Existing Instance WordEvaluable. + + Definition interp_bexpr (op: ExprBinOp) (x y: tuple (word bits) 10): tuple (word bits) 10 := + let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) := x in + let '(y0, y1, y2, y3, y4, y5, y6, y7, y8, y9) := y in + let op' := NArgMap (fun v => Z.of_N (@wordToN bits v)) op in + let z := LL.interp (op' x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in + z. + + Definition interp_uexpr (op: ExprUnOp) (x: tuple (word bits) 10): tuple (word bits) 10 := + let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) := x in + let op' := NArgMap (fun v => Z.of_N (@wordToN bits v)) op in + let z := LL.interp (op' x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) in + z. + + Definition radd : ExprBinOp := Add.wordProg. + Definition ropp : ExprUnOp := Opp.wordProg. + End Operations. End GF25519. Extraction "GF25519Add" GF25519.Add. Extraction "GF25519Sub" GF25519.Sub. Extraction "GF25519Mul" GF25519.Mul. -Extraction "GF25519Opp" GF25519.Opp.
\ No newline at end of file +Extraction "GF25519Opp" GF25519.Opp. + |