diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-20 00:13:43 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-20 00:13:43 -0400 |
| commit | a2f81a1a2a82be7c445748cfca375bd5f74688d2 (patch) | |
| tree | 7c22ab68b1db58556c941db2a03544d0ed107b43 /src/Assembly/GF25519.v | |
| parent | 6b0876b5625cc9982bde1f4f24851c99a245d480 (diff) | |
Use carry versions of operations
Diffstat (limited to 'src/Assembly/GF25519.v')
| -rw-r--r-- | src/Assembly/GF25519.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v index 80d9044c4..50a886305 100644 --- a/src/Assembly/GF25519.v +++ b/src/Assembly/GF25519.v @@ -42,7 +42,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 @@ -95,7 +95,7 @@ Module GF25519. Definition inputBounds := feBound ++ feBound. Definition ge25519_sub_expr := - Eval cbv beta delta [fe25519 add mul sub Let_In] in sub. + Eval cbv beta delta [fe25519 carry_add mul carry_sub Let_In] in carry_sub. Definition ge25519_sub' (P Q: @interp_type Z FE) : { r: @HL.expr Z (@interp_type Z) FE @@ -148,7 +148,7 @@ Module GF25519. Definition inputBounds := feBound ++ feBound. Definition ge25519_mul_expr := - Eval cbv beta delta [fe25519 add mul sub Let_In] in mul. + Eval cbv beta delta [fe25519 carry_add mul carry_sub Let_In] in mul. Definition ge25519_mul' (P Q: @interp_type Z FE) : { r: @HL.expr Z (@interp_type Z) FE @@ -201,7 +201,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 @@ -255,4 +255,4 @@ 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. |