diff options
38 files changed, 936 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 832d595de..96ffb03f9 100644 --- a/_CoqProject +++ b/_CoqProject @@ -3263,6 +3263,20 @@ src/Specific/solinas32_2e255m19_10limbs/fesub.v src/Specific/solinas32_2e255m19_10limbs/fesubDisplay.v src/Specific/solinas32_2e255m19_10limbs/freeze.v src/Specific/solinas32_2e255m19_10limbs/freezeDisplay.v +src/Specific/solinas32_2e255m19_10limbs_donna/CurveParameters.v +src/Specific/solinas32_2e255m19_10limbs_donna/Synthesis.v +src/Specific/solinas32_2e255m19_10limbs_donna/feadd.v +src/Specific/solinas32_2e255m19_10limbs_donna/feaddDisplay.v +src/Specific/solinas32_2e255m19_10limbs_donna/fecarry.v +src/Specific/solinas32_2e255m19_10limbs_donna/fecarryDisplay.v +src/Specific/solinas32_2e255m19_10limbs_donna/femul.v +src/Specific/solinas32_2e255m19_10limbs_donna/femulDisplay.v +src/Specific/solinas32_2e255m19_10limbs_donna/fesquare.v +src/Specific/solinas32_2e255m19_10limbs_donna/fesquareDisplay.v +src/Specific/solinas32_2e255m19_10limbs_donna/fesub.v +src/Specific/solinas32_2e255m19_10limbs_donna/fesubDisplay.v +src/Specific/solinas32_2e255m19_10limbs_donna/freeze.v +src/Specific/solinas32_2e255m19_10limbs_donna/freezeDisplay.v src/Specific/solinas32_2e255m19_11limbs/CurveParameters.v src/Specific/solinas32_2e255m19_11limbs/Synthesis.v src/Specific/solinas32_2e255m19_11limbs/feadd.v @@ -5293,6 +5307,20 @@ src/Specific/solinas64_2e255m19_5limbs/fesub.v src/Specific/solinas64_2e255m19_5limbs/fesubDisplay.v src/Specific/solinas64_2e255m19_5limbs/freeze.v src/Specific/solinas64_2e255m19_5limbs/freezeDisplay.v +src/Specific/solinas64_2e255m19_5limbs_donna/CurveParameters.v +src/Specific/solinas64_2e255m19_5limbs_donna/Synthesis.v +src/Specific/solinas64_2e255m19_5limbs_donna/feadd.v +src/Specific/solinas64_2e255m19_5limbs_donna/feaddDisplay.v +src/Specific/solinas64_2e255m19_5limbs_donna/fecarry.v +src/Specific/solinas64_2e255m19_5limbs_donna/fecarryDisplay.v +src/Specific/solinas64_2e255m19_5limbs_donna/femul.v +src/Specific/solinas64_2e255m19_5limbs_donna/femulDisplay.v +src/Specific/solinas64_2e255m19_5limbs_donna/fesquare.v +src/Specific/solinas64_2e255m19_5limbs_donna/fesquareDisplay.v +src/Specific/solinas64_2e255m19_5limbs_donna/fesub.v +src/Specific/solinas64_2e255m19_5limbs_donna/fesubDisplay.v +src/Specific/solinas64_2e255m19_5limbs_donna/freeze.v +src/Specific/solinas64_2e255m19_5limbs_donna/freezeDisplay.v src/Specific/solinas64_2e255m19_6limbs/CurveParameters.v src/Specific/solinas64_2e255m19_6limbs/Synthesis.v src/Specific/solinas64_2e255m19_6limbs/feadd.v diff --git a/src/Specific/CurveParameters/remake_curves.sh b/src/Specific/CurveParameters/remake_curves.sh index bb51658cf..1a5c578b7 100755 --- a/src/Specific/CurveParameters/remake_curves.sh +++ b/src/Specific/CurveParameters/remake_curves.sh @@ -11,6 +11,8 @@ ${MAKE} "$@" x25519_c32.json ../X25519/C32/ ${MAKE} "$@" x2448_c64_karatsuba.json ../X2448/Karatsuba/C64/ ${MAKE} "$@" nistp256_amd128.json ../NISTP256/AMD128/ ${MAKE} "$@" nistp256_amd64.json ../NISTP256/AMD64/ +${MAKE} "$@" solinas32_2e255m19_10limbs_donna.json ../solinas32_2e255m19_10limbs_donna/ +${MAKE} "$@" solinas64_2e255m19_5limbs_donna.json ../solinas64_2e255m19_5limbs_donna/ ${MAKE} "$@" montgomery32_2e127m1_4limbs.json ../montgomery32_2e127m1_4limbs/ ${MAKE} "$@" montgomery64_2e127m1_2limbs.json ../montgomery64_2e127m1_2limbs/ ${MAKE} "$@" solinas32_2e127m1_5limbs.json ../solinas32_2e127m1_5limbs/ diff --git a/src/Specific/CurveParameters/solinas32_2e255m19_10limbs_donna.json b/src/Specific/CurveParameters/solinas32_2e255m19_10limbs_donna.json new file mode 100644 index 000000000..9e80be3db --- /dev/null +++ b/src/Specific/CurveParameters/solinas32_2e255m19_10limbs_donna.json @@ -0,0 +1,237 @@ +{ + "base": "25.5", + "bitwidth": 32, + "carry_chains": "default", + "coef_div_modulus": "2", + "compiler": "clang -fbracket-depth=999999 -march=native -mtune=native -std=gnu11 -O3 -flto -fuse-ld=lld -fomit-frame-pointer -fwrapv -Wno-attributes -fno-strict-aliasing -Da24_hex='0x3039' -Da24_val='12345' -Da_minus_two_over_four_array='{0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x30,0x39}' -Dbitwidth='32' -Dlimb_weight_gaps_array='{26,25,26,25,26,25,26,25,26,25}' -Dmodulus_array='{0x7f,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xed}' -Dmodulus_bytes_val='32' -Dmodulus_limbs='10' -Dq_mpz='(1_mpz<<255) - 19'", + "compilerxx": "clang++ -fbracket-depth=999999 -march=native -mtune=native -std=gnu++11 -O3 -flto -fuse-ld=lld -fomit-frame-pointer -fwrapv -Wno-attributes -fno-strict-aliasing -Da24_hex='0x3039' -Da24_val='12345' -Da_minus_two_over_four_array='{0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x30,0x39}' -Dbitwidth='32' -Dlimb_weight_gaps_array='{26,25,26,25,26,25,26,25,26,25}' -Dmodulus_array='{0x7f,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xed}' -Dmodulus_bytes_val='32' -Dmodulus_limbs='10' -Dq_mpz='(1_mpz<<255) - 19'", + "modulus": "2^255 - 19", + "operations": [ + "femul", + "feadd", + "fesub", + "fesquare", + "fecarry", + "freeze" + ], + "sz": "10", + "mul_header" : "(* Micro-optimized form from curve25519-donna by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)", + "mul_code" + : + " + output[0] = ((limb) ((s32) in2[0])) * ((s32) in[0]); + output[1] = ((limb) ((s32) in2[0])) * ((s32) in[1]) + + ((limb) ((s32) in2[1])) * ((s32) in[0]); + output[2] = 2 * ((limb) ((s32) in2[1])) * ((s32) in[1]) + + ((limb) ((s32) in2[0])) * ((s32) in[2]) + + ((limb) ((s32) in2[2])) * ((s32) in[0]); + output[3] = ((limb) ((s32) in2[1])) * ((s32) in[2]) + + ((limb) ((s32) in2[2])) * ((s32) in[1]) + + ((limb) ((s32) in2[0])) * ((s32) in[3]) + + ((limb) ((s32) in2[3])) * ((s32) in[0]); + output[4] = ((limb) ((s32) in2[2])) * ((s32) in[2]) + + 2 * (((limb) ((s32) in2[1])) * ((s32) in[3]) + + ((limb) ((s32) in2[3])) * ((s32) in[1])) + + ((limb) ((s32) in2[0])) * ((s32) in[4]) + + ((limb) ((s32) in2[4])) * ((s32) in[0]); + output[5] = ((limb) ((s32) in2[2])) * ((s32) in[3]) + + ((limb) ((s32) in2[3])) * ((s32) in[2]) + + ((limb) ((s32) in2[1])) * ((s32) in[4]) + + ((limb) ((s32) in2[4])) * ((s32) in[1]) + + ((limb) ((s32) in2[0])) * ((s32) in[5]) + + ((limb) ((s32) in2[5])) * ((s32) in[0]); + output[6] = 2 * (((limb) ((s32) in2[3])) * ((s32) in[3]) + + ((limb) ((s32) in2[1])) * ((s32) in[5]) + + ((limb) ((s32) in2[5])) * ((s32) in[1])) + + ((limb) ((s32) in2[2])) * ((s32) in[4]) + + ((limb) ((s32) in2[4])) * ((s32) in[2]) + + ((limb) ((s32) in2[0])) * ((s32) in[6]) + + ((limb) ((s32) in2[6])) * ((s32) in[0]); + output[7] = ((limb) ((s32) in2[3])) * ((s32) in[4]) + + ((limb) ((s32) in2[4])) * ((s32) in[3]) + + ((limb) ((s32) in2[2])) * ((s32) in[5]) + + ((limb) ((s32) in2[5])) * ((s32) in[2]) + + ((limb) ((s32) in2[1])) * ((s32) in[6]) + + ((limb) ((s32) in2[6])) * ((s32) in[1]) + + ((limb) ((s32) in2[0])) * ((s32) in[7]) + + ((limb) ((s32) in2[7])) * ((s32) in[0]); + output[8] = ((limb) ((s32) in2[4])) * ((s32) in[4]) + + 2 * (((limb) ((s32) in2[3])) * ((s32) in[5]) + + ((limb) ((s32) in2[5])) * ((s32) in[3]) + + ((limb) ((s32) in2[1])) * ((s32) in[7]) + + ((limb) ((s32) in2[7])) * ((s32) in[1])) + + ((limb) ((s32) in2[2])) * ((s32) in[6]) + + ((limb) ((s32) in2[6])) * ((s32) in[2]) + + ((limb) ((s32) in2[0])) * ((s32) in[8]) + + ((limb) ((s32) in2[8])) * ((s32) in[0]); + output[9] = ((limb) ((s32) in2[4])) * ((s32) in[5]) + + ((limb) ((s32) in2[5])) * ((s32) in[4]) + + ((limb) ((s32) in2[3])) * ((s32) in[6]) + + ((limb) ((s32) in2[6])) * ((s32) in[3]) + + ((limb) ((s32) in2[2])) * ((s32) in[7]) + + ((limb) ((s32) in2[7])) * ((s32) in[2]) + + ((limb) ((s32) in2[1])) * ((s32) in[8]) + + ((limb) ((s32) in2[8])) * ((s32) in[1]) + + ((limb) ((s32) in2[0])) * ((s32) in[9]) + + ((limb) ((s32) in2[9])) * ((s32) in[0]); + output[10] = 2 * (((limb) ((s32) in2[5])) * ((s32) in[5]) + + ((limb) ((s32) in2[3])) * ((s32) in[7]) + + ((limb) ((s32) in2[7])) * ((s32) in[3]) + + ((limb) ((s32) in2[1])) * ((s32) in[9]) + + ((limb) ((s32) in2[9])) * ((s32) in[1])) + + ((limb) ((s32) in2[4])) * ((s32) in[6]) + + ((limb) ((s32) in2[6])) * ((s32) in[4]) + + ((limb) ((s32) in2[2])) * ((s32) in[8]) + + ((limb) ((s32) in2[8])) * ((s32) in[2]); + output[11] = ((limb) ((s32) in2[5])) * ((s32) in[6]) + + ((limb) ((s32) in2[6])) * ((s32) in[5]) + + ((limb) ((s32) in2[4])) * ((s32) in[7]) + + ((limb) ((s32) in2[7])) * ((s32) in[4]) + + ((limb) ((s32) in2[3])) * ((s32) in[8]) + + ((limb) ((s32) in2[8])) * ((s32) in[3]) + + ((limb) ((s32) in2[2])) * ((s32) in[9]) + + ((limb) ((s32) in2[9])) * ((s32) in[2]); + output[12] = ((limb) ((s32) in2[6])) * ((s32) in[6]) + + 2 * (((limb) ((s32) in2[5])) * ((s32) in[7]) + + ((limb) ((s32) in2[7])) * ((s32) in[5]) + + ((limb) ((s32) in2[3])) * ((s32) in[9]) + + ((limb) ((s32) in2[9])) * ((s32) in[3])) + + ((limb) ((s32) in2[4])) * ((s32) in[8]) + + ((limb) ((s32) in2[8])) * ((s32) in[4]); + output[13] = ((limb) ((s32) in2[6])) * ((s32) in[7]) + + ((limb) ((s32) in2[7])) * ((s32) in[6]) + + ((limb) ((s32) in2[5])) * ((s32) in[8]) + + ((limb) ((s32) in2[8])) * ((s32) in[5]) + + ((limb) ((s32) in2[4])) * ((s32) in[9]) + + ((limb) ((s32) in2[9])) * ((s32) in[4]); + output[14] = 2 * (((limb) ((s32) in2[7])) * ((s32) in[7]) + + ((limb) ((s32) in2[5])) * ((s32) in[9]) + + ((limb) ((s32) in2[9])) * ((s32) in[5])) + + ((limb) ((s32) in2[6])) * ((s32) in[8]) + + ((limb) ((s32) in2[8])) * ((s32) in[6]); + output[15] = ((limb) ((s32) in2[7])) * ((s32) in[8]) + + ((limb) ((s32) in2[8])) * ((s32) in[7]) + + ((limb) ((s32) in2[6])) * ((s32) in[9]) + + ((limb) ((s32) in2[9])) * ((s32) in[6]); + output[16] = ((limb) ((s32) in2[8])) * ((s32) in[8]) + + 2 * (((limb) ((s32) in2[7])) * ((s32) in[9]) + + ((limb) ((s32) in2[9])) * ((s32) in[7])); + output[17] = ((limb) ((s32) in2[8])) * ((s32) in[9]) + + ((limb) ((s32) in2[9])) * ((s32) in[8]); + output[18] = 2 * ((limb) ((s32) in2[9])) * ((s32) in[9]); + output[8] += output[18] << 4; + output[8] += output[18] << 1; + output[8] += output[18]; + output[7] += output[17] << 4; + output[7] += output[17] << 1; + output[7] += output[17]; + output[6] += output[16] << 4; + output[6] += output[16] << 1; + output[6] += output[16]; + output[5] += output[15] << 4; + output[5] += output[15] << 1; + output[5] += output[15]; + output[4] += output[14] << 4; + output[4] += output[14] << 1; + output[4] += output[14]; + output[3] += output[13] << 4; + output[3] += output[13] << 1; + output[3] += output[13]; + output[2] += output[12] << 4; + output[2] += output[12] << 1; + output[2] += output[12]; + output[1] += output[11] << 4; + output[1] += output[11] << 1; + output[1] += output[11]; + output[0] += output[10] << 4; + output[0] += output[10] << 1; + output[0] += output[10]; +", + "square_header" : "(* Micro-optimized form from curve25519-donna by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)", + "square_code" + : + " + output[0] = ((limb) ((s32) in[0])) * ((s32) in[0]); + output[1] = 2 * ((limb) ((s32) in[0])) * ((s32) in[1]); + output[2] = 2 * (((limb) ((s32) in[1])) * ((s32) in[1]) + + ((limb) ((s32) in[0])) * ((s32) in[2])); + output[3] = 2 * (((limb) ((s32) in[1])) * ((s32) in[2]) + + ((limb) ((s32) in[0])) * ((s32) in[3])); + output[4] = ((limb) ((s32) in[2])) * ((s32) in[2]) + + 4 * ((limb) ((s32) in[1])) * ((s32) in[3]) + + 2 * ((limb) ((s32) in[0])) * ((s32) in[4]); + output[5] = 2 * (((limb) ((s32) in[2])) * ((s32) in[3]) + + ((limb) ((s32) in[1])) * ((s32) in[4]) + + ((limb) ((s32) in[0])) * ((s32) in[5])); + output[6] = 2 * (((limb) ((s32) in[3])) * ((s32) in[3]) + + ((limb) ((s32) in[2])) * ((s32) in[4]) + + ((limb) ((s32) in[0])) * ((s32) in[6]) + + 2 * ((limb) ((s32) in[1])) * ((s32) in[5])); + output[7] = 2 * (((limb) ((s32) in[3])) * ((s32) in[4]) + + ((limb) ((s32) in[2])) * ((s32) in[5]) + + ((limb) ((s32) in[1])) * ((s32) in[6]) + + ((limb) ((s32) in[0])) * ((s32) in[7])); + output[8] = ((limb) ((s32) in[4])) * ((s32) in[4]) + + 2 * (((limb) ((s32) in[2])) * ((s32) in[6]) + + ((limb) ((s32) in[0])) * ((s32) in[8]) + + 2 * (((limb) ((s32) in[1])) * ((s32) in[7]) + + ((limb) ((s32) in[3])) * ((s32) in[5]))); + output[9] = 2 * (((limb) ((s32) in[4])) * ((s32) in[5]) + + ((limb) ((s32) in[3])) * ((s32) in[6]) + + ((limb) ((s32) in[2])) * ((s32) in[7]) + + ((limb) ((s32) in[1])) * ((s32) in[8]) + + ((limb) ((s32) in[0])) * ((s32) in[9])); + output[10] = 2 * (((limb) ((s32) in[5])) * ((s32) in[5]) + + ((limb) ((s32) in[4])) * ((s32) in[6]) + + ((limb) ((s32) in[2])) * ((s32) in[8]) + + 2 * (((limb) ((s32) in[3])) * ((s32) in[7]) + + ((limb) ((s32) in[1])) * ((s32) in[9]))); + output[11] = 2 * (((limb) ((s32) in[5])) * ((s32) in[6]) + + ((limb) ((s32) in[4])) * ((s32) in[7]) + + ((limb) ((s32) in[3])) * ((s32) in[8]) + + ((limb) ((s32) in[2])) * ((s32) in[9])); + output[12] = ((limb) ((s32) in[6])) * ((s32) in[6]) + + 2 * (((limb) ((s32) in[4])) * ((s32) in[8]) + + 2 * (((limb) ((s32) in[5])) * ((s32) in[7]) + + ((limb) ((s32) in[3])) * ((s32) in[9]))); + output[13] = 2 * (((limb) ((s32) in[6])) * ((s32) in[7]) + + ((limb) ((s32) in[5])) * ((s32) in[8]) + + ((limb) ((s32) in[4])) * ((s32) in[9])); + output[14] = 2 * (((limb) ((s32) in[7])) * ((s32) in[7]) + + ((limb) ((s32) in[6])) * ((s32) in[8]) + + 2 * ((limb) ((s32) in[5])) * ((s32) in[9])); + output[15] = 2 * (((limb) ((s32) in[7])) * ((s32) in[8]) + + ((limb) ((s32) in[6])) * ((s32) in[9])); + output[16] = ((limb) ((s32) in[8])) * ((s32) in[8]) + + 4 * ((limb) ((s32) in[7])) * ((s32) in[9]); + output[17] = 2 * ((limb) ((s32) in[8])) * ((s32) in[9]); + output[18] = 2 * ((limb) ((s32) in[9])) * ((s32) in[9]); + output[8] += output[18] << 4; + output[8] += output[18] << 1; + output[8] += output[18]; + output[7] += output[17] << 4; + output[7] += output[17] << 1; + output[7] += output[17]; + output[6] += output[16] << 4; + output[6] += output[16] << 1; + output[6] += output[16]; + output[5] += output[15] << 4; + output[5] += output[15] << 1; + output[5] += output[15]; + output[4] += output[14] << 4; + output[4] += output[14] << 1; + output[4] += output[14]; + output[3] += output[13] << 4; + output[3] += output[13] << 1; + output[3] += output[13]; + output[2] += output[12] << 4; + output[2] += output[12] << 1; + output[2] += output[12]; + output[1] += output[11] << 4; + output[1] += output[11] << 1; + output[1] += output[11]; + output[0] += output[10] << 4; + output[0] += output[10] << 1; + output[0] += output[10]; +" +} diff --git a/src/Specific/CurveParameters/solinas64_2e255m19_5limbs_donna.json b/src/Specific/CurveParameters/solinas64_2e255m19_5limbs_donna.json new file mode 100644 index 000000000..68a2032c2 --- /dev/null +++ b/src/Specific/CurveParameters/solinas64_2e255m19_5limbs_donna.json @@ -0,0 +1,80 @@ +{ + "base": "51", + "bitwidth": 64, + "carry_chains": "default", + "coef_div_modulus": "2", + "compiler": "clang -fbracket-depth=999999 -march=native -mtune=native -std=gnu11 -O3 -flto -fuse-ld=lld -fomit-frame-pointer -fwrapv -Wno-attributes -fno-strict-aliasing -Da24_hex='0x3039' -Da24_val='12345' -Da_minus_two_over_four_array='{0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x30,0x39}' -Dbitwidth='64' -Dlimb_weight_gaps_array='{51,51,51,51,51}' -Dmodulus_array='{0x7f,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xed}' -Dmodulus_bytes_val='32' -Dmodulus_limbs='5' -Dq_mpz='(1_mpz<<255) - 19'", + "compilerxx": "clang++ -fbracket-depth=999999 -march=native -mtune=native -std=gnu++11 -O3 -flto -fuse-ld=lld -fomit-frame-pointer -fwrapv -Wno-attributes -fno-strict-aliasing -Da24_hex='0x3039' -Da24_val='12345' -Da_minus_two_over_four_array='{0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x30,0x39}' -Dbitwidth='64' -Dlimb_weight_gaps_array='{51,51,51,51,51}' -Dmodulus_array='{0x7f,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xed}' -Dmodulus_bytes_val='32' -Dmodulus_limbs='5' -Dq_mpz='(1_mpz<<255) - 19'", + "modulus": "2^255 - 19", + "operations": [ + "femul", + "feadd", + "fesub", + "fesquare", + "fecarry", + "freeze" + ], + "sz": "5", + "mul_header" : "(* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)", + "mul_code" + : + " + uint128_t t[5]; + limb r0,r1,r2,r3,r4,s0,s1,s2,s3,s4,c; + + r0 = in[0]; + r1 = in[1]; + r2 = in[2]; + r3 = in[3]; + r4 = in[4]; + + s0 = in2[0]; + s1 = in2[1]; + s2 = in2[2]; + s3 = in2[3]; + s4 = in2[4]; + + t[0] = ((uint128_t) r0) * s0; + t[1] = ((uint128_t) r0) * s1 + ((uint128_t) r1) * s0; + t[2] = ((uint128_t) r0) * s2 + ((uint128_t) r2) * s0 + ((uint128_t) r1) * s1; + t[3] = ((uint128_t) r0) * s3 + ((uint128_t) r3) * s0 + ((uint128_t) r1) * s2 + ((uint128_t) r2) * s1; + t[4] = ((uint128_t) r0) * s4 + ((uint128_t) r4) * s0 + ((uint128_t) r3) * s1 + ((uint128_t) r1) * s3 + ((uint128_t) r2) * s2; + + r4 *= 19; + r1 *= 19; + r2 *= 19; + r3 *= 19; + + t[0] += ((uint128_t) r4) * s1 + ((uint128_t) r1) * s4 + ((uint128_t) r2) * s3 + ((uint128_t) r3) * s2; + t[1] += ((uint128_t) r4) * s2 + ((uint128_t) r2) * s4 + ((uint128_t) r3) * s3; + t[2] += ((uint128_t) r4) * s3 + ((uint128_t) r3) * s4; + t[3] += ((uint128_t) r4) * s4; +", + "square_header" : "(* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)", + "square_code" + : + " + uint128_t t[5]; + limb r0,r1,r2,r3,r4,c; + limb d0,d1,d2,d4,d419; + + r0 = in[0]; + r1 = in[1]; + r2 = in[2]; + r3 = in[3]; + r4 = in[4]; + + do { + d0 = r0 * 2; + d1 = r1 * 2; + d2 = r2 * 2 * 19; + d419 = r4 * 19; + d4 = d419 * 2; + + t[0] = ((uint128_t) r0) * r0 + ((uint128_t) d4) * r1 + (((uint128_t) d2) * (r3 )); + t[1] = ((uint128_t) d0) * r1 + ((uint128_t) d4) * r2 + (((uint128_t) r3) * (r3 * 19)); + t[2] = ((uint128_t) d0) * r2 + ((uint128_t) r1) * r1 + (((uint128_t) d4) * (r3 )); + t[3] = ((uint128_t) d0) * r3 + ((uint128_t) d1) * r2 + (((uint128_t) r4) * (d419 )); + t[4] = ((uint128_t) d0) * r4 + ((uint128_t) d1) * r3 + (((uint128_t) r2) * (r2 )); +" +} diff --git a/src/Specific/solinas32_2e255m19_10limbs_donna/CurveParameters.v b/src/Specific/solinas32_2e255m19_10limbs_donna/CurveParameters.v new file mode 100644 index 000000000..1be3437a3 --- /dev/null +++ b/src/Specific/solinas32_2e255m19_10limbs_donna/CurveParameters.v @@ -0,0 +1,257 @@ +Require Import Crypto.Specific.Framework.RawCurveParameters. +Require Import Crypto.Util.LetIn. + +(*** +Modulus : 2^255 - 19 +Base: 25.5 +***) + +Definition curve : CurveParameters := + {| + sz := 10%nat; + base := 25 + 1/2; + bitwidth := 32; + s := 2^255; + c := [(1, 19)]; + carry_chains := Some [seq 0 (pred 10); [0; 1]]%nat; + + a24 := None; + coef_div_modulus := Some 2%nat; + + goldilocks := None; + karatsuba := None; + montgomery := false; + freeze := Some true; + ladderstep := false; + + mul_code := Some (fun a b => + (* Micro-optimized form from curve25519-donna by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *) + let '(in9, in8, in7, in6, in5, in4, in3, in2, in1, in0) := a in + let '(in29, in28, in27, in26, in25, in24, in23, in22, in21, in20) := b in + dlet output0 := in20 * in0 in + dlet output1 := in20 * in1 + + in21 * in0 in + dlet output2 := 2 * in21 * in1 + + in20 * in2 + + in22 * in0 in + dlet output3 := in21 * in2 + + in22 * in1 + + in20 * in3 + + in23 * in0 in + dlet output4 := in22 * in2 + + 2 * (in21 * in3 + + in23 * in1) + + in20 * in4 + + in24 * in0 in + dlet output5 := in22 * in3 + + in23 * in2 + + in21 * in4 + + in24 * in1 + + in20 * in5 + + in25 * in0 in + dlet output6 := 2 * (in23 * in3 + + in21 * in5 + + in25 * in1) + + in22 * in4 + + in24 * in2 + + in20 * in6 + + in26 * in0 in + dlet output7 := in23 * in4 + + in24 * in3 + + in22 * in5 + + in25 * in2 + + in21 * in6 + + in26 * in1 + + in20 * in7 + + in27 * in0 in + dlet output8 := in24 * in4 + + 2 * (in23 * in5 + + in25 * in3 + + in21 * in7 + + in27 * in1) + + in22 * in6 + + in26 * in2 + + in20 * in8 + + in28 * in0 in + dlet output9 := in24 * in5 + + in25 * in4 + + in23 * in6 + + in26 * in3 + + in22 * in7 + + in27 * in2 + + in21 * in8 + + in28 * in1 + + in20 * in9 + + in29 * in0 in + dlet output10 := 2 * (in25 * in5 + + in23 * in7 + + in27 * in3 + + in21 * in9 + + in29 * in1) + + in24 * in6 + + in26 * in4 + + in22 * in8 + + in28 * in2 in + dlet output11 := in25 * in6 + + in26 * in5 + + in24 * in7 + + in27 * in4 + + in23 * in8 + + in28 * in3 + + in22 * in9 + + in29 * in2 in + dlet output12 := in26 * in6 + + 2 * (in25 * in7 + + in27 * in5 + + in23 * in9 + + in29 * in3) + + in24 * in8 + + in28 * in4 in + dlet output13 := in26 * in7 + + in27 * in6 + + in25 * in8 + + in28 * in5 + + in24 * in9 + + in29 * in4 in + dlet output14 := 2 * (in27 * in7 + + in25 * in9 + + in29 * in5) + + in26 * in8 + + in28 * in6 in + dlet output15 := in27 * in8 + + in28 * in7 + + in26 * in9 + + in29 * in6 in + dlet output16 := in28 * in8 + + 2 * (in27 * in9 + + in29 * in7) in + dlet output17 := in28 * in9 + + in29 * in8 in + dlet output18 := 2 * in29 * in9 in + dlet output8 := output8 + output18 << 4 in + dlet output8 := output8 + output18 << 1 in + dlet output8 := output8 + output18 in + dlet output7 := output7 + output17 << 4 in + dlet output7 := output7 + output17 << 1 in + dlet output7 := output7 + output17 in + dlet output6 := output6 + output16 << 4 in + dlet output6 := output6 + output16 << 1 in + dlet output6 := output6 + output16 in + dlet output5 := output5 + output15 << 4 in + dlet output5 := output5 + output15 << 1 in + dlet output5 := output5 + output15 in + dlet output4 := output4 + output14 << 4 in + dlet output4 := output4 + output14 << 1 in + dlet output4 := output4 + output14 in + dlet output3 := output3 + output13 << 4 in + dlet output3 := output3 + output13 << 1 in + dlet output3 := output3 + output13 in + dlet output2 := output2 + output12 << 4 in + dlet output2 := output2 + output12 << 1 in + dlet output2 := output2 + output12 in + dlet output1 := output1 + output11 << 4 in + dlet output1 := output1 + output11 << 1 in + dlet output1 := output1 + output11 in + dlet output0 := output0 + output10 << 4 in + dlet output0 := output0 + output10 << 1 in + dlet output0 := output0 + output10 in + (output9, output8, output7, output6, output5, output4, output3, output2, output1, output0) + ); + + square_code := Some (fun a => + (* Micro-optimized form from curve25519-donna by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *) + let '(in9, in8, in7, in6, in5, in4, in3, in2, in1, in0) := a in + dlet output0 := in0 * in0 in + dlet output1 := 2 * in0 * in1 in + dlet output2 := 2 * (in1 * in1 + + in0 * in2) in + dlet output3 := 2 * (in1 * in2 + + in0 * in3) in + dlet output4 := in2 * in2 + + 4 * in1 * in3 + + 2 * in0 * in4 in + dlet output5 := 2 * (in2 * in3 + + in1 * in4 + + in0 * in5) in + dlet output6 := 2 * (in3 * in3 + + in2 * in4 + + in0 * in6 + + 2 * in1 * in5) in + dlet output7 := 2 * (in3 * in4 + + in2 * in5 + + in1 * in6 + + in0 * in7) in + dlet output8 := in4 * in4 + + 2 * (in2 * in6 + + in0 * in8 + + 2 * (in1 * in7 + + in3 * in5)) in + dlet output9 := 2 * (in4 * in5 + + in3 * in6 + + in2 * in7 + + in1 * in8 + + in0 * in9) in + dlet output10 := 2 * (in5 * in5 + + in4 * in6 + + in2 * in8 + + 2 * (in3 * in7 + + in1 * in9)) in + dlet output11 := 2 * (in5 * in6 + + in4 * in7 + + in3 * in8 + + in2 * in9) in + dlet output12 := in6 * in6 + + 2 * (in4 * in8 + + 2 * (in5 * in7 + + in3 * in9)) in + dlet output13 := 2 * (in6 * in7 + + in5 * in8 + + in4 * in9) in + dlet output14 := 2 * (in7 * in7 + + in6 * in8 + + 2 * in5 * in9) in + dlet output15 := 2 * (in7 * in8 + + in6 * in9) in + dlet output16 := in8 * in8 + + 4 * in7 * in9 in + dlet output17 := 2 * in8 * in9 in + dlet output18 := 2 * in9 * in9 in + dlet output8 := output8 + output18 << 4 in + dlet output8 := output8 + output18 << 1 in + dlet output8 := output8 + output18 in + dlet output7 := output7 + output17 << 4 in + dlet output7 := output7 + output17 << 1 in + dlet output7 := output7 + output17 in + dlet output6 := output6 + output16 << 4 in + dlet output6 := output6 + output16 << 1 in + dlet output6 := output6 + output16 in + dlet output5 := output5 + output15 << 4 in + dlet output5 := output5 + output15 << 1 in + dlet output5 := output5 + output15 in + dlet output4 := output4 + output14 << 4 in + dlet output4 := output4 + output14 << 1 in + dlet output4 := output4 + output14 in + dlet output3 := output3 + output13 << 4 in + dlet output3 := output3 + output13 << 1 in + dlet output3 := output3 + output13 in + dlet output2 := output2 + output12 << 4 in + dlet output2 := output2 + output12 << 1 in + dlet output2 := output2 + output12 in + dlet output1 := output1 + output11 << 4 in + dlet output1 := output1 + output11 << 1 in + dlet output1 := output1 + output11 in + dlet output0 := output0 + output10 << 4 in + dlet output0 := output0 + output10 << 1 in + dlet output0 := output0 + output10 in + (output9, output8, output7, output6, output5, output4, output3, output2, output1, output0) + ); + + upper_bound_of_exponent_loose := None; + upper_bound_of_exponent_tight := None; + allowable_bit_widths := None; + freeze_extra_allowable_bit_widths := None; + modinv_fuel := None + |}. + +Ltac extra_prove_mul_eq _ := idtac. +Ltac extra_prove_square_eq _ := idtac. diff --git a/src/Specific/solinas32_2e255m19_10limbs_donna/Synthesis.v b/src/Specific/solinas32_2e255m19_10limbs_donna/Synthesis.v new file mode 100644 index 000000000..c27bd5b77 --- /dev/null +++ b/src/Specific/solinas32_2e255m19_10limbs_donna/Synthesis.v @@ -0,0 +1,9 @@ +Require Import Crypto.Specific.Framework.SynthesisFramework. +Require Import Crypto.Specific.solinas32_2e255m19_10limbs_donna.CurveParameters. + +Module P <: PrePackage. + Definition package : Tag.Context. + Proof. make_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq. Defined. +End P. + +Module Export S := PackageSynthesis P. diff --git a/src/Specific/solinas32_2e255m19_10limbs_donna/compiler.sh b/src/Specific/solinas32_2e255m19_10limbs_donna/compiler.sh new file mode 100755 index 000000000..94ceeba0c --- /dev/null +++ b/src/Specific/solinas32_2e255m19_10limbs_donna/compiler.sh @@ -0,0 +1,4 @@ +#!/bin/sh +set -eu + +clang -fbracket-depth=999999 -march=native -mtune=native -std=gnu11 -O3 -flto -fuse-ld=lld -fomit-frame-pointer -fwrapv -Wno-attributes -fno-strict-aliasing -Da24_hex='0x3039' -Da24_val='12345' -Da_minus_two_over_four_array='{0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x30,0x39}' -Dbitwidth='32' -Dlimb_weight_gaps_array='{26,25,26,25,26,25,26,25,26,25}' -Dmodulus_array='{0x7f,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xed}' -Dmodulus_bytes_val='32' -Dmodulus_limbs='10' -Dq_mpz='(1_mpz<<255) - 19' "$@" diff --git a/src/Specific/solinas32_2e255m19_10limbs_donna/compilerxx.sh b/src/Specific/solinas32_2e255m19_10limbs_donna/compilerxx.sh new file mode 100755 index 000000000..129e195ba --- /dev/null +++ b/src/Specific/solinas32_2e255m19_10limbs_donna/compilerxx.sh @@ -0,0 +1,4 @@ +#!/bin/sh +set -eu + +clang++ -fbracket-depth=999999 -march=native -mtune=native -std=gnu++11 -O3 -flto -fuse-ld=lld -fomit-frame-pointer -fwrapv -Wno-attributes -fno-strict-aliasing -Da24_hex='0x3039' -Da24_val='12345' -Da_minus_two_over_four_array='{0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x30,0x39}' -Dbitwidth='32' -Dlimb_weight_gaps_array='{26,25,26,25,26,25,26,25,26,25}' -Dmodulus_array='{0x7f,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xed}' -Dmodulus_bytes_val='32' -Dmodulus_limbs='10' -Dq_mpz='(1_mpz<<255) - 19' "$@" diff --git a/src/Specific/solinas32_2e255m19_10limbs_donna/feadd.v b/src/Specific/solinas32_2e255m19_10limbs_donna/feadd.v new file mode 100644 index 000000000..7d4318c78 --- /dev/null +++ b/src/Specific/solinas32_2e255m19_10limbs_donna/feadd.v @@ -0,0 +1,14 @@ +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Specific.solinas32_2e255m19_10limbs_donna.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition add : + { add : feBW_tight -> feBW_tight -> feBW_loose + | forall a b, phiBW_loose (add a b) = F.add (phiBW_tight a) (phiBW_tight b) }. +Proof. + Set Ltac Profiling. + Time synthesize_add (). + Show Ltac Profile. +Time Defined. + +Print Assumptions add. diff --git a/src/Specific/solinas32_2e255m19_10limbs_donna/feaddDisplay.v b/src/Specific/solinas32_2e255m19_10limbs_donna/feaddDisplay.v new file mode 100644 index 000000000..233b9f92b --- /dev/null +++ b/src/Specific/solinas32_2e255m19_10limbs_donna/feaddDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.solinas32_2e255m19_10limbs_donna.feadd. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. + +Check display add. diff --git a/src/Specific/solinas32_2e255m19_10limbs_donna/fecarry.v b/src/Specific/solinas32_2e255m19_10limbs_donna/fecarry.v new file mode 100644 index 000000000..534d538d0 --- /dev/null +++ b/src/Specific/solinas32_2e255m19_10limbs_donna/fecarry.v @@ -0,0 +1,14 @@ +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Specific.solinas32_2e255m19_10limbs_donna.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition carry : + { carry : feBW_loose -> feBW_tight + | forall a, phiBW_tight (carry a) = (phiBW_loose a) }. +Proof. + Set Ltac Profiling. + Time synthesize_carry (). + Show Ltac Profile. +Time Defined. + +Print Assumptions carry. diff --git a/src/Specific/solinas32_2e255m19_10limbs_donna/fecarryDisplay.v b/src/Specific/solinas32_2e255m19_10limbs_donna/fecarryDisplay.v new file mode 100644 index 000000000..cda477ab7 --- /dev/null +++ b/src/Specific/solinas32_2e255m19_10limbs_donna/fecarryDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.solinas32_2e255m19_10limbs_donna.fecarry. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. + +Check display carry. diff --git a/src/Specific/solinas32_2e255m19_10limbs_donna/femul.v b/src/Specific/solinas32_2e255m19_10limbs_donna/femul.v new file mode 100644 index 000000000..918b0e5a9 --- /dev/null +++ b/src/Specific/solinas32_2e255m19_10limbs_donna/femul.v @@ -0,0 +1,14 @@ +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Specific.solinas32_2e255m19_10limbs_donna.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition mul : + { mul : feBW_loose -> feBW_loose -> feBW_tight + | forall a b, phiBW_tight (mul a b) = F.mul (phiBW_loose a) (phiBW_loose b) }. +Proof. + Set Ltac Profiling. + Time synthesize_mul (). + Show Ltac Profile. +Time Defined. + +Print Assumptions mul. diff --git a/src/Specific/solinas32_2e255m19_10limbs_donna/femulDisplay.v b/src/Specific/solinas32_2e255m19_10limbs_donna/femulDisplay.v new file mode 100644 index 000000000..c0973e1e2 --- /dev/null +++ b/src/Specific/solinas32_2e255m19_10limbs_donna/femulDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.solinas32_2e255m19_10limbs_donna.femul. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. + +Check display mul. diff --git a/src/Specific/solinas32_2e255m19_10limbs_donna/fesquare.v b/src/Specific/solinas32_2e255m19_10limbs_donna/fesquare.v new file mode 100644 index 000000000..68939088c --- /dev/null +++ b/src/Specific/solinas32_2e255m19_10limbs_donna/fesquare.v @@ -0,0 +1,14 @@ +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Specific.solinas32_2e255m19_10limbs_donna.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition square : + { square : feBW_loose -> feBW_tight + | forall a, phiBW_tight (square a) = F.mul (phiBW_loose a) (phiBW_loose a) }. +Proof. + Set Ltac Profiling. + Time synthesize_square (). + Show Ltac Profile. +Time Defined. + +Print Assumptions square. diff --git a/src/Specific/solinas32_2e255m19_10limbs_donna/fesquareDisplay.v b/src/Specific/solinas32_2e255m19_10limbs_donna/fesquareDisplay.v new file mode 100644 index 000000000..651779f2b --- /dev/null +++ b/src/Specific/solinas32_2e255m19_10limbs_donna/fesquareDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.solinas32_2e255m19_10limbs_donna.fesquare. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. + +Check display square. diff --git a/src/Specific/solinas32_2e255m19_10limbs_donna/fesub.v b/src/Specific/solinas32_2e255m19_10limbs_donna/fesub.v new file mode 100644 index 000000000..3c5d12e55 --- /dev/null +++ b/src/Specific/solinas32_2e255m19_10limbs_donna/fesub.v @@ -0,0 +1,14 @@ +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Specific.solinas32_2e255m19_10limbs_donna.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition sub : + { sub : feBW_tight -> feBW_tight -> feBW_loose + | forall a b, phiBW_loose (sub a b) = F.sub (phiBW_tight a) (phiBW_tight b) }. +Proof. + Set Ltac Profiling. + Time synthesize_sub (). + Show Ltac Profile. +Time Defined. + +Print Assumptions sub. diff --git a/src/Specific/solinas32_2e255m19_10limbs_donna/fesubDisplay.v b/src/Specific/solinas32_2e255m19_10limbs_donna/fesubDisplay.v new file mode 100644 index 000000000..a4ec24ade --- /dev/null +++ b/src/Specific/solinas32_2e255m19_10limbs_donna/fesubDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.solinas32_2e255m19_10limbs_donna.fesub. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. + +Check display sub. diff --git a/src/Specific/solinas32_2e255m19_10limbs_donna/freeze.v b/src/Specific/solinas32_2e255m19_10limbs_donna/freeze.v new file mode 100644 index 000000000..c57bd2f06 --- /dev/null +++ b/src/Specific/solinas32_2e255m19_10limbs_donna/freeze.v @@ -0,0 +1,14 @@ +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Specific.solinas32_2e255m19_10limbs_donna.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition freeze : + { freeze : feBW_tight -> feBW_limbwidths + | forall a, phiBW_limbwidths (freeze a) = phiBW_tight a }. +Proof. + Set Ltac Profiling. + Time synthesize_freeze (). + Show Ltac Profile. +Time Defined. + +Print Assumptions freeze. diff --git a/src/Specific/solinas32_2e255m19_10limbs_donna/freezeDisplay.v b/src/Specific/solinas32_2e255m19_10limbs_donna/freezeDisplay.v new file mode 100644 index 000000000..3992875a2 --- /dev/null +++ b/src/Specific/solinas32_2e255m19_10limbs_donna/freezeDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.solinas32_2e255m19_10limbs_donna.freeze. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. + +Check display freeze. diff --git a/src/Specific/solinas32_2e255m19_10limbs_donna/py_interpreter.sh b/src/Specific/solinas32_2e255m19_10limbs_donna/py_interpreter.sh new file mode 100755 index 000000000..c5b125c07 --- /dev/null +++ b/src/Specific/solinas32_2e255m19_10limbs_donna/py_interpreter.sh @@ -0,0 +1,4 @@ +#!/bin/sh +set -eu + +/usr/bin/env python3 "$@" -Dq='2**255 - 19' -Dmodulus_bytes='25.5' -Da24='121665' diff --git a/src/Specific/solinas64_2e255m19_5limbs_donna/CurveParameters.v b/src/Specific/solinas64_2e255m19_5limbs_donna/CurveParameters.v new file mode 100644 index 000000000..e128a8a09 --- /dev/null +++ b/src/Specific/solinas64_2e255m19_5limbs_donna/CurveParameters.v @@ -0,0 +1,74 @@ +Require Import Crypto.Specific.Framework.RawCurveParameters. +Require Import Crypto.Util.LetIn. + +(*** +Modulus : 2^255 - 19 +Base: 51 +***) + +Definition curve : CurveParameters := + {| + sz := 5%nat; + base := 51; + bitwidth := 64; + s := 2^255; + c := [(1, 19)]; + carry_chains := Some [seq 0 (pred 5); [0; 1]]%nat; + + a24 := None; + coef_div_modulus := Some 2%nat; + + goldilocks := None; + karatsuba := None; + montgomery := false; + freeze := Some true; + ladderstep := false; + + mul_code := Some (fun a b => + (* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *) + let '(r4, r3, r2, r1, r0) := a in + let '(s4, s3, s2, s1, s0) := b in + dlet t0 := r0 * s0 in + dlet t1 := r0 * s1 + r1 * s0 in + dlet t2 := r0 * s2 + r2 * s0 + r1 * s1 in + dlet t3 := r0 * s3 + r3 * s0 + r1 * s2 + r2 * s1 in + dlet t4 := r0 * s4 + r4 * s0 + r3 * s1 + r1 * s3 + r2 * s2 in + + dlet r4 := r4 * 19 in + dlet r1 := r1 * 19 in + dlet r2 := r2 * 19 in + dlet r3 := r3 * 19 in + + dlet t0 := t0 + r4 * s1 + r1 * s4 + r2 * s3 + r3 * s2 in + dlet t1 := t1 + r4 * s2 + r2 * s4 + r3 * s3 in + dlet t2 := t2 + r4 * s3 + r3 * s4 in + dlet t3 := t3 + r4 * s4 in + (t4, t3, t2, t1, t0) + ); + + square_code := Some (fun a => + (* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *) + let '(r4, r3, r2, r1, r0) := a in + dlet d0 := r0 * 2 in + dlet d1 := r1 * 2 in + dlet d2 := r2 * 2 * 19 in + dlet d419 := r4 * 19 in + dlet d4 := d419 * 2 in + + dlet t0 := r0 * r0 + d4 * r1 + (d2 * (r3 )) in + dlet t1 := d0 * r1 + d4 * r2 + (r3 * (r3 * 19)) in + dlet t2 := d0 * r2 + r1 * r1 + (d4 * (r3 )) in + dlet t3 := d0 * r3 + d1 * r2 + (r4 * (d419 )) in + dlet t4 := d0 * r4 + d1 * r3 + (r2 * (r2 )) in + (t4, t3, t2, t1, t0) + ); + + upper_bound_of_exponent_loose := None; + upper_bound_of_exponent_tight := None; + allowable_bit_widths := None; + freeze_extra_allowable_bit_widths := None; + modinv_fuel := None + |}. + +Ltac extra_prove_mul_eq _ := idtac. +Ltac extra_prove_square_eq _ := idtac. diff --git a/src/Specific/solinas64_2e255m19_5limbs_donna/Synthesis.v b/src/Specific/solinas64_2e255m19_5limbs_donna/Synthesis.v new file mode 100644 index 000000000..51b1a64a7 --- /dev/null +++ b/src/Specific/solinas64_2e255m19_5limbs_donna/Synthesis.v @@ -0,0 +1,9 @@ +Require Import Crypto.Specific.Framework.SynthesisFramework. +Require Import Crypto.Specific.solinas64_2e255m19_5limbs_donna.CurveParameters. + +Module P <: PrePackage. + Definition package : Tag.Context. + Proof. make_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq. Defined. +End P. + +Module Export S := PackageSynthesis P. diff --git a/src/Specific/solinas64_2e255m19_5limbs_donna/compiler.sh b/src/Specific/solinas64_2e255m19_5limbs_donna/compiler.sh new file mode 100755 index 000000000..a16722d20 --- /dev/null +++ b/src/Specific/solinas64_2e255m19_5limbs_donna/compiler.sh @@ -0,0 +1,4 @@ +#!/bin/sh +set -eu + +clang -fbracket-depth=999999 -march=native -mtune=native -std=gnu11 -O3 -flto -fuse-ld=lld -fomit-frame-pointer -fwrapv -Wno-attributes -fno-strict-aliasing -Da24_hex='0x3039' -Da24_val='12345' -Da_minus_two_over_four_array='{0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x30,0x39}' -Dbitwidth='64' -Dlimb_weight_gaps_array='{51,51,51,51,51}' -Dmodulus_array='{0x7f,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xed}' -Dmodulus_bytes_val='32' -Dmodulus_limbs='5' -Dq_mpz='(1_mpz<<255) - 19' "$@" diff --git a/src/Specific/solinas64_2e255m19_5limbs_donna/compilerxx.sh b/src/Specific/solinas64_2e255m19_5limbs_donna/compilerxx.sh new file mode 100755 index 000000000..a3b9b5579 --- /dev/null +++ b/src/Specific/solinas64_2e255m19_5limbs_donna/compilerxx.sh @@ -0,0 +1,4 @@ +#!/bin/sh +set -eu + +clang++ -fbracket-depth=999999 -march=native -mtune=native -std=gnu++11 -O3 -flto -fuse-ld=lld -fomit-frame-pointer -fwrapv -Wno-attributes -fno-strict-aliasing -Da24_hex='0x3039' -Da24_val='12345' -Da_minus_two_over_four_array='{0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x30,0x39}' -Dbitwidth='64' -Dlimb_weight_gaps_array='{51,51,51,51,51}' -Dmodulus_array='{0x7f,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xed}' -Dmodulus_bytes_val='32' -Dmodulus_limbs='5' -Dq_mpz='(1_mpz<<255) - 19' "$@" diff --git a/src/Specific/solinas64_2e255m19_5limbs_donna/feadd.v b/src/Specific/solinas64_2e255m19_5limbs_donna/feadd.v new file mode 100644 index 000000000..98e5735f3 --- /dev/null +++ b/src/Specific/solinas64_2e255m19_5limbs_donna/feadd.v @@ -0,0 +1,14 @@ +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Specific.solinas64_2e255m19_5limbs_donna.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition add : + { add : feBW_tight -> feBW_tight -> feBW_loose + | forall a b, phiBW_loose (add a b) = F.add (phiBW_tight a) (phiBW_tight b) }. +Proof. + Set Ltac Profiling. + Time synthesize_add (). + Show Ltac Profile. +Time Defined. + +Print Assumptions add. diff --git a/src/Specific/solinas64_2e255m19_5limbs_donna/feaddDisplay.v b/src/Specific/solinas64_2e255m19_5limbs_donna/feaddDisplay.v new file mode 100644 index 000000000..059ef987e --- /dev/null +++ b/src/Specific/solinas64_2e255m19_5limbs_donna/feaddDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.solinas64_2e255m19_5limbs_donna.feadd. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. + +Check display add. diff --git a/src/Specific/solinas64_2e255m19_5limbs_donna/fecarry.v b/src/Specific/solinas64_2e255m19_5limbs_donna/fecarry.v new file mode 100644 index 000000000..4b58a2ab5 --- /dev/null +++ b/src/Specific/solinas64_2e255m19_5limbs_donna/fecarry.v @@ -0,0 +1,14 @@ +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Specific.solinas64_2e255m19_5limbs_donna.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition carry : + { carry : feBW_loose -> feBW_tight + | forall a, phiBW_tight (carry a) = (phiBW_loose a) }. +Proof. + Set Ltac Profiling. + Time synthesize_carry (). + Show Ltac Profile. +Time Defined. + +Print Assumptions carry. diff --git a/src/Specific/solinas64_2e255m19_5limbs_donna/fecarryDisplay.v b/src/Specific/solinas64_2e255m19_5limbs_donna/fecarryDisplay.v new file mode 100644 index 000000000..18687ce79 --- /dev/null +++ b/src/Specific/solinas64_2e255m19_5limbs_donna/fecarryDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.solinas64_2e255m19_5limbs_donna.fecarry. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. + +Check display carry. diff --git a/src/Specific/solinas64_2e255m19_5limbs_donna/femul.v b/src/Specific/solinas64_2e255m19_5limbs_donna/femul.v new file mode 100644 index 000000000..279480168 --- /dev/null +++ b/src/Specific/solinas64_2e255m19_5limbs_donna/femul.v @@ -0,0 +1,14 @@ +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Specific.solinas64_2e255m19_5limbs_donna.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition mul : + { mul : feBW_loose -> feBW_loose -> feBW_tight + | forall a b, phiBW_tight (mul a b) = F.mul (phiBW_loose a) (phiBW_loose b) }. +Proof. + Set Ltac Profiling. + Time synthesize_mul (). + Show Ltac Profile. +Time Defined. + +Print Assumptions mul. diff --git a/src/Specific/solinas64_2e255m19_5limbs_donna/femulDisplay.v b/src/Specific/solinas64_2e255m19_5limbs_donna/femulDisplay.v new file mode 100644 index 000000000..6e350b13c --- /dev/null +++ b/src/Specific/solinas64_2e255m19_5limbs_donna/femulDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.solinas64_2e255m19_5limbs_donna.femul. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. + +Check display mul. diff --git a/src/Specific/solinas64_2e255m19_5limbs_donna/fesquare.v b/src/Specific/solinas64_2e255m19_5limbs_donna/fesquare.v new file mode 100644 index 000000000..d6f25e43a --- /dev/null +++ b/src/Specific/solinas64_2e255m19_5limbs_donna/fesquare.v @@ -0,0 +1,14 @@ +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Specific.solinas64_2e255m19_5limbs_donna.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition square : + { square : feBW_loose -> feBW_tight + | forall a, phiBW_tight (square a) = F.mul (phiBW_loose a) (phiBW_loose a) }. +Proof. + Set Ltac Profiling. + Time synthesize_square (). + Show Ltac Profile. +Time Defined. + +Print Assumptions square. diff --git a/src/Specific/solinas64_2e255m19_5limbs_donna/fesquareDisplay.v b/src/Specific/solinas64_2e255m19_5limbs_donna/fesquareDisplay.v new file mode 100644 index 000000000..9cb7597d9 --- /dev/null +++ b/src/Specific/solinas64_2e255m19_5limbs_donna/fesquareDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.solinas64_2e255m19_5limbs_donna.fesquare. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. + +Check display square. diff --git a/src/Specific/solinas64_2e255m19_5limbs_donna/fesub.v b/src/Specific/solinas64_2e255m19_5limbs_donna/fesub.v new file mode 100644 index 000000000..ba562d051 --- /dev/null +++ b/src/Specific/solinas64_2e255m19_5limbs_donna/fesub.v @@ -0,0 +1,14 @@ +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Specific.solinas64_2e255m19_5limbs_donna.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition sub : + { sub : feBW_tight -> feBW_tight -> feBW_loose + | forall a b, phiBW_loose (sub a b) = F.sub (phiBW_tight a) (phiBW_tight b) }. +Proof. + Set Ltac Profiling. + Time synthesize_sub (). + Show Ltac Profile. +Time Defined. + +Print Assumptions sub. diff --git a/src/Specific/solinas64_2e255m19_5limbs_donna/fesubDisplay.v b/src/Specific/solinas64_2e255m19_5limbs_donna/fesubDisplay.v new file mode 100644 index 000000000..caeb9f1ff --- /dev/null +++ b/src/Specific/solinas64_2e255m19_5limbs_donna/fesubDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.solinas64_2e255m19_5limbs_donna.fesub. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. + +Check display sub. diff --git a/src/Specific/solinas64_2e255m19_5limbs_donna/freeze.v b/src/Specific/solinas64_2e255m19_5limbs_donna/freeze.v new file mode 100644 index 000000000..f479b3551 --- /dev/null +++ b/src/Specific/solinas64_2e255m19_5limbs_donna/freeze.v @@ -0,0 +1,14 @@ +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Specific.solinas64_2e255m19_5limbs_donna.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition freeze : + { freeze : feBW_tight -> feBW_limbwidths + | forall a, phiBW_limbwidths (freeze a) = phiBW_tight a }. +Proof. + Set Ltac Profiling. + Time synthesize_freeze (). + Show Ltac Profile. +Time Defined. + +Print Assumptions freeze. diff --git a/src/Specific/solinas64_2e255m19_5limbs_donna/freezeDisplay.v b/src/Specific/solinas64_2e255m19_5limbs_donna/freezeDisplay.v new file mode 100644 index 000000000..386ccca71 --- /dev/null +++ b/src/Specific/solinas64_2e255m19_5limbs_donna/freezeDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.solinas64_2e255m19_5limbs_donna.freeze. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. + +Check display freeze. diff --git a/src/Specific/solinas64_2e255m19_5limbs_donna/py_interpreter.sh b/src/Specific/solinas64_2e255m19_5limbs_donna/py_interpreter.sh new file mode 100755 index 000000000..b561a9733 --- /dev/null +++ b/src/Specific/solinas64_2e255m19_5limbs_donna/py_interpreter.sh @@ -0,0 +1,4 @@ +#!/bin/sh +set -eu + +/usr/bin/env python3 "$@" -Dq='2**255 - 19' -Dmodulus_bytes='51' -Da24='121665' |