diff options
| author |  Robert Sloan <varomodt@google.com> | 2016-10-21 14:08:14 -0700 |
|---|---|---|
| committer | Robert Sloan <varomodt@google.com> | 2016-10-21 14:08:14 -0700 |
| commit | eed4e2ee6d6a60268c6729920613962ff3fc5285 (patch) | |
| tree | 4a4669505728b365149bb455904e0c211fc7833e /src/Assembly/GF25519.v | |
| parent | 4225439aa82294a6d2a56fc4f622dc318e69529f (diff) | |
| parent | 37e2b17fa4daf7e85466a02e0be2ffb603f446cb (diff) | |
merge rsloan-phoas refactors into master
Diffstat (limited to 'src/Assembly/GF25519.v')
| -rw-r--r-- | src/Assembly/GF25519.v | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v index a21b54cf0..605bcfd2e 100644 --- a/src/Assembly/GF25519.v +++ b/src/Assembly/GF25519.v @@ -45,7 +45,7 @@ Module GF25519. Definition inputBounds := feBound ++ feBound. Definition ge25519_add_expr := - Eval cbv beta delta [fe25519 add mul sub Let_In] in add. + Eval cbv beta delta [fe25519 carry_add mul carry_sub Let_In] in carry_add. Definition ge25519_add' (P Q: @interp_type Z FE) : { r: @HL.expr Z (@interp_type Z) FE | HL.interp (t := FE) r = ge25519_add_expr P Q }. @@ -88,7 +88,7 @@ Module GF25519. Definition inputBounds := feBound. Definition ge25519_opp_expr := - Eval cbv beta delta [fe25519 add mul sub opp Let_In] in opp. + Eval cbv beta delta [fe25519 carry_add mul carry_sub carry_opp Let_In] in carry_opp. Definition ge25519_opp' (P: @interp_type Z FE) : { r: @HL.expr Z (@interp_type Z) FE @@ -140,13 +140,13 @@ Module GF25519. 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 + let z := LL.interp' (fun x => NToWord bits (Z.to_N x)) (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 + let z := LL.interp' (fun x => NToWord bits (Z.to_N x)) (op' x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) in z. Definition radd : ExprBinOp := Add.wordProg. @@ -155,7 +155,4 @@ Module GF25519. End GF25519. Extraction "GF25519Add" GF25519.Add. -Extraction "GF25519Sub" GF25519.Sub. -Extraction "GF25519Mul" GF25519.Mul. Extraction "GF25519Opp" GF25519.Opp. - |