fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Remove outdated C128 files	Jason Gross	2017-11-12
\|
*	add back incorrectly deleted files	jadep	2017-11-12
\|
*	update remake-curves.sh and Makefile	jadep	2017-11-12
\|
*	Add a dummy karatsuba parameter	Jason Gross	2017-11-07
\| \| \| \| \| \|	Currently unused, but adding it here in preparation for removing reification (which will allow easy support of karatsuba separate from goldilocks).
*	find . -name "py_interpreter.sh" \| xargs chmod +x	Jason Gross	2017-11-03
\|
*	Add generated py_interpreter.sh files	Jason Gross	2017-11-02
\|
*	Add tight and loose bounds, no carry in add, sub	Jason Gross	2017-10-22
\| \| \| \| \| \| \| \|	Following Andres' suggestions to allow making ladderstep from other synthesis things. It went though mostly without a hitch, though there were a number of boilerplate changes needed.
*	Saner checking for freeze and ladderstep	Jason Gross	2017-10-18
\|
*	Explicitly specify base	Jason Gross	2017-10-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This allows it to be something other than log2(m)/sz. After \| File Name \| Before \|\| Change ------------------------------------------------------------------------------------------- 8m20.82s \| Total \| 8m37.82s \|\| -0m17.00s ------------------------------------------------------------------------------------------- 1m59.42s \| Specific/NISTP256/AMD64/femul \| 2m19.09s \|\| -0m19.67s 3m28.66s \| Specific/X25519/C64/ladderstep \| 3m28.02s \|\| +0m00.63s 0m24.97s \| Specific/X25519/C64/femul \| 0m24.60s \|\| +0m00.36s 0m24.08s \| Specific/NISTP256/AMD64/fesub \| 0m23.48s \|\| +0m00.59s 0m22.00s \| Specific/NISTP256/AMD64/feadd \| 0m21.34s \|\| +0m00.66s 0m20.34s \| Specific/X25519/C64/freeze \| 0m19.76s \|\| +0m00.57s 0m19.85s \| Specific/X25519/C64/fesquare \| 0m19.93s \|\| -0m00.07s 0m18.04s \| Specific/NISTP256/AMD64/feopp \| 0m17.69s \|\| +0m00.34s 0m15.10s \| Specific/NISTP256/AMD64/fenz \| 0m15.37s \|\| -0m00.26s 0m08.31s \| Specific/NISTP256/AMD64/Synthesis \| 0m08.24s \|\| +0m00.07s 0m05.96s \| Specific/X25519/C64/Synthesis \| 0m06.25s \|\| -0m00.29s 0m02.10s \| Specific/Framework/ArithmeticSynthesis/Defaults \| 0m02.14s \|\| -0m00.04s 0m01.00s \| Specific/Framework/SynthesisFramework \| 0m01.03s \|\| -0m00.03s 0m00.97s \| Specific/Framework/ArithmeticSynthesis/Base \| 0m01.02s \|\| -0m00.05s 0m00.89s \| Specific/Framework/ArithmeticSynthesis/Freeze \| 0m00.84s \|\| +0m00.05s 0m00.80s \| Specific/Framework/ArithmeticSynthesis/Karatsuba \| 0m00.81s \|\| -0m00.01s 0m00.79s \| Specific/Framework/ArithmeticSynthesis/MontgomeryPackage \| 0m00.80s \|\| -0m00.01s 0m00.76s \| Specific/Framework/MontgomeryReificationTypesPackage \| 0m00.75s \|\| +0m00.01s 0m00.74s \| Specific/Framework/ReificationTypesPackage \| 0m00.77s \|\| -0m00.03s 0m00.74s \| Specific/Framework/ArithmeticSynthesis/BasePackage \| 0m00.74s \|\| +0m00.00s 0m00.73s \| Specific/Framework/ArithmeticSynthesis/SquareFromMul \| 0m00.70s \|\| +0m00.03s 0m00.72s \| Specific/Framework/ArithmeticSynthesis/DefaultsPackage \| 0m00.68s \|\| +0m00.03s 0m00.70s \| Specific/Framework/ArithmeticSynthesis/LadderstepPackage \| 0m00.72s \|\| -0m00.02s 0m00.70s \| Specific/Framework/ArithmeticSynthesis/FreezePackage \| 0m00.77s \|\| -0m00.07s 0m00.69s \| Specific/Framework/ArithmeticSynthesis/KaratsubaPackage \| 0m00.70s \|\| -0m00.01s 0m00.42s \| Specific/X25519/C64/CurveParameters \| 0m00.38s \|\| +0m00.03s 0m00.36s \| Specific/Framework/CurveParameters \| 0m00.32s \|\| +0m00.03s 0m00.33s \| Specific/Framework/RawCurveParameters \| 0m00.29s \|\| +0m00.04s 0m00.33s \| Specific/Framework/CurveParametersPackage \| 0m00.30s \|\| +0m00.03s 0m00.32s \| Specific/NISTP256/AMD64/CurveParameters \| 0m00.30s \|\| +0m00.02s
*	Turn CurveParameters into a record	Jason Gross	2017-10-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is a first step towards removing module functors from the code generation After \| File Name \| Before \|\| Change --------------------------------------------------------------------------------------------- 13m12.84s \| Total \| 13m13.24s \|\| -0m00.39s --------------------------------------------------------------------------------------------- 2m09.48s \| Specific/X25519/C64/ladderstep \| 2m03.07s \|\| +0m06.40s 1m08.48s \| Specific/X2448/Karatsuba/C64/femul \| 1m12.93s \|\| -0m04.45s 1m33.58s \| Specific/NISTP256/AMD64/femul \| 1m30.93s \|\| +0m02.64s 1m06.71s \| Specific/X2555/C128/ladderstep \| 1m09.55s \|\| -0m02.84s 0m35.01s \| Specific/X25519/C32/fesquare \| 0m36.58s \|\| -0m01.57s 1m02.68s \| Specific/X25519/C32/femul \| 1m02.39s \|\| +0m00.28s 0m44.51s \| Specific/X2448/Karatsuba/C64/Synthesis \| 0m44.29s \|\| +0m00.21s 0m31.30s \| Specific/X25519/C32/Synthesis \| 0m31.17s \|\| +0m00.12s 0m26.73s \| Specific/X25519/C32/freeze \| 0m27.38s \|\| -0m00.64s 0m22.81s \| Specific/NISTP256/AMD128/femul \| 0m23.28s \|\| -0m00.47s 0m20.30s \| Specific/NISTP256/AMD64/fesub \| 0m20.02s \|\| +0m00.28s 0m17.76s \| Specific/NISTP256/AMD64/feadd \| 0m17.70s \|\| +0m00.06s 0m17.04s \| Specific/X25519/C64/femul \| 0m17.51s \|\| -0m00.47s 0m15.18s \| Specific/X25519/C64/freeze \| 0m14.93s \|\| +0m00.25s 0m15.14s \| Specific/NISTP256/AMD64/feopp \| 0m15.32s \|\| -0m00.17s 0m14.72s \| Specific/NISTP256/AMD64/fenz \| 0m14.68s \|\| +0m00.04s 0m14.50s \| Specific/X25519/C64/fesquare \| 0m14.54s \|\| -0m00.03s 0m14.26s \| Specific/NISTP256/AMD128/feadd \| 0m14.48s \|\| -0m00.22s 0m14.21s \| Specific/NISTP256/AMD128/fesub \| 0m14.43s \|\| -0m00.21s 0m14.10s \| Specific/NISTP256/AMD128/fenz \| 0m14.07s \|\| +0m00.02s 0m11.67s \| Specific/NISTP256/AMD128/feopp \| 0m11.67s \|\| +0m00.00s 0m10.12s \| Specific/X25519/C64/Synthesis \| 0m10.42s \|\| -0m00.30s 0m08.53s \| Specific/NISTP256/AMD64/Synthesis \| 0m08.44s \|\| +0m00.08s 0m06.44s \| Specific/X2555/C128/Synthesis \| 0m06.30s \|\| +0m00.14s 0m03.65s \| Specific/NISTP256/AMD128/Synthesis \| 0m03.60s \|\| +0m00.04s 0m01.00s \| Specific/X25519/C32/CurveParameters \| 0m01.07s \|\| -0m00.07s 0m00.98s \| Specific/Framework/SynthesisFramework \| 0m01.00s \|\| -0m00.02s 0m00.80s \| Specific/Framework/ArithmeticSynthesis/Freeze \| 0m00.73s \|\| +0m00.07s 0m00.79s \| Specific/Framework/ArithmeticSynthesis/Defaults \| 0m00.74s \|\| +0m00.05s 0m00.78s \| Specific/Framework/ArithmeticSynthesis/Karatsuba \| 0m00.79s \|\| -0m00.01s 0m00.75s \| Specific/Framework/ArithmeticSynthesis/MontgomeryPackage \| 0m00.71s \|\| +0m00.04s 0m00.74s \| Specific/Framework/ArithmeticSynthesis/Base \| 0m00.77s \|\| -0m00.03s 0m00.73s \| Specific/Framework/ArithmeticSynthesis/FreezePackage \| 0m00.69s \|\| +0m00.04s 0m00.73s \| Specific/Framework/MontgomeryReificationTypesPackage \| 0m00.70s \|\| +0m00.03s 0m00.72s \| Specific/Framework/ReificationTypesPackage \| 0m00.75s \|\| -0m00.03s 0m00.70s \| Specific/Framework/ArithmeticSynthesis/KaratsubaPackage \| 0m00.70s \|\| +0m00.00s 0m00.69s \| Specific/Framework/ArithmeticSynthesis/DefaultsPackage \| 0m00.70s \|\| -0m00.01s 0m00.68s \| Specific/Framework/ArithmeticSynthesis/SquareFromMul \| 0m00.72s \|\| -0m00.03s 0m00.66s \| Specific/Framework/ArithmeticSynthesis/LadderstepPackage \| 0m00.69s \|\| -0m00.02s 0m00.65s \| Specific/Framework/ArithmeticSynthesis/BasePackage \| 0m00.66s \|\| -0m00.01s 0m00.43s \| Specific/X25519/C64/CurveParameters \| 0m00.39s \|\| +0m00.03s 0m00.34s \| Specific/Framework/CurveParameters \| 0m00.29s \|\| +0m00.05s 0m00.32s \| Specific/X2555/C128/CurveParameters \| 0m00.30s \|\| +0m00.02s 0m00.30s \| Specific/NISTP256/AMD128/CurveParameters \| 0m00.28s \|\| +0m00.01s 0m00.30s \| Specific/X2448/Karatsuba/C64/CurveParameters \| 0m00.31s \|\| -0m00.01s 0m00.30s \| Specific/Framework/CurveParametersPackage \| 0m00.29s \|\| +0m00.01s 0m00.29s \| Specific/NISTP256/AMD64/CurveParameters \| 0m00.29s \|\| +0m00.00s 0m00.26s \| Specific/Framework/RawCurveParameters \| N/A \|\| +0m00.26s
*	Support p256 / montgomery in json format	Jason Gross	2017-10-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Extra time comes from adding AMD128 to NISTP256, mostly. After \| File Name \| Before \|\| Change --------------------------------------------------------------------------------------------- 13m25.13s \| Total \| 13m30.82s \|\| -0m05.69s --------------------------------------------------------------------------------------------- N/A \| Specific/IntegrationTestMontgomeryP256_128 \| 0m25.42s \|\| -0m25.42s 0m22.75s \| Specific/NISTP256/AMD128/femul \| N/A \|\| +0m22.75s 1m31.64s \| Specific/NISTP256/AMD64/femul \| 1m52.42s \|\| -0m20.78s 0m14.46s \| Specific/NISTP256/AMD128/fesub \| N/A \|\| +0m14.46s 0m14.25s \| Specific/NISTP256/AMD128/feadd \| N/A \|\| +0m14.25s 0m14.12s \| Specific/NISTP256/AMD128/fenz \| N/A \|\| +0m14.11s N/A \| Specific/NISTP256/AMD64/MontgomeryP256 \| 0m13.00s \|\| -0m13.00s N/A \| Specific/IntegrationTestMontgomeryP256_128_Sub \| 0m12.40s \|\| -0m12.40s N/A \| Specific/IntegrationTestMontgomeryP256_128_Add \| 0m11.99s \|\| -0m11.99s 0m11.74s \| Specific/NISTP256/AMD128/feopp \| N/A \|\| +0m11.74s N/A \| Specific/IntegrationTestMontgomeryP256_128_Opp \| 0m11.22s \|\| -0m11.22s N/A \| Specific/IntegrationTestMontgomeryP256_128_Nonzero \| 0m09.27s \|\| -0m09.26s N/A \| Specific/MontgomeryP256_128 \| 0m09.26s \|\| -0m09.25s 0m08.42s \| Specific/NISTP256/AMD64/Synthesis \| N/A \|\| +0m08.41s 0m14.67s \| Specific/NISTP256/AMD64/fenz \| 0m09.98s \|\| +0m04.68s 0m04.12s \| Specific/Framework/ArithmeticSynthesis/Montgomery \| N/A \|\| +0m04.12s 0m03.58s \| Specific/NISTP256/AMD128/Synthesis \| N/A \|\| +0m03.58s 1m10.78s \| Specific/X2555/C128/ladderstep \| 1m08.36s \|\| +0m02.42s 1m02.10s \| Specific/X25519/C32/femul \| 1m00.59s \|\| +0m01.50s 0m43.59s \| Specific/X2448/Karatsuba/C64/Synthesis \| 0m44.86s \|\| -0m01.26s 0m34.97s \| Specific/X25519/C32/fesquare \| 0m35.98s \|\| -0m01.00s 0m20.10s \| Specific/NISTP256/AMD64/fesub \| 0m18.37s \|\| +0m01.73s 0m17.61s \| Specific/NISTP256/AMD64/feadd \| 0m15.94s \|\| +0m01.67s 2m09.77s \| Specific/X25519/C64/ladderstep \| 2m09.79s \|\| -0m00.01s 1m11.70s \| Specific/X2448/Karatsuba/C64/femul \| 1m11.60s \|\| +0m00.10s 0m32.14s \| Specific/X25519/C32/Synthesis \| 0m31.70s \|\| +0m00.44s 0m27.94s \| Specific/X25519/C32/freeze \| 0m28.06s \|\| -0m00.11s 0m17.62s \| Specific/X25519/C64/femul \| 0m17.41s \|\| +0m00.21s 0m15.21s \| Specific/X25519/C64/freeze \| 0m14.74s \|\| +0m00.47s 0m14.86s \| Specific/NISTP256/AMD64/feopp \| 0m14.96s \|\| -0m00.10s 0m14.58s \| Specific/X25519/C64/fesquare \| 0m14.06s \|\| +0m00.51s 0m10.10s \| Specific/X25519/C64/Synthesis \| 0m09.78s \|\| +0m00.32s 0m06.22s \| Specific/X2555/C128/Synthesis \| 0m06.17s \|\| +0m00.04s 0m01.01s \| Specific/X25519/C32/CurveParameters \| 0m01.05s \|\| -0m00.04s 0m00.99s \| Specific/Framework/SynthesisFramework \| 0m01.08s \|\| -0m00.09s 0m00.79s \| Specific/Framework/MontgomeryReificationTypes \| N/A \|\| +0m00.79s 0m00.78s \| Specific/Framework/ArithmeticSynthesis/SquareFromMul \| 0m00.70s \|\| +0m00.08s 0m00.78s \| Specific/Framework/ArithmeticSynthesis/Karatsuba \| 0m00.75s \|\| +0m00.03s 0m00.76s \| Specific/Framework/ArithmeticSynthesis/MontgomeryPackage \| N/A \|\| +0m00.76s 0m00.75s \| Specific/Framework/IntegrationTestTemporaryMiscCommon \| 0m00.80s \|\| -0m00.05s 0m00.75s \| Specific/Framework/MontgomeryReificationTypesPackage \| N/A \|\| +0m00.75s 0m00.73s \| Specific/Framework/ArithmeticSynthesis/Defaults \| 0m00.75s \|\| -0m00.02s 0m00.72s \| Specific/Framework/ReificationTypesPackage \| 0m00.70s \|\| +0m00.02s 0m00.72s \| Specific/Framework/ArithmeticSynthesis/Base \| 0m00.73s \|\| -0m00.01s 0m00.72s \| Specific/Framework/ArithmeticSynthesis/BasePackage \| 0m00.69s \|\| +0m00.03s 0m00.72s \| Specific/Framework/ArithmeticSynthesis/LadderstepPackage \| 0m00.76s \|\| -0m00.04s 0m00.70s \| Specific/Framework/ArithmeticSynthesis/Freeze \| 0m00.75s \|\| -0m00.05s 0m00.70s \| Specific/Framework/ArithmeticSynthesis/KaratsubaPackage \| 0m00.77s \|\| -0m00.07s 0m00.69s \| Specific/Framework/ArithmeticSynthesis/DefaultsPackage \| 0m00.71s \|\| -0m00.02s 0m00.67s \| Specific/Framework/ArithmeticSynthesis/FreezePackage \| 0m00.74s \|\| -0m00.06s 0m00.43s \| Specific/X25519/C64/CurveParameters \| 0m00.43s \|\| +0m00.00s 0m00.38s \| Specific/Framework/IntegrationTestDisplayCommon \| 0m00.40s \|\| -0m00.02s 0m00.38s \| Specific/Framework/IntegrationTestDisplayCommonTactics \| 0m00.37s \|\| +0m00.01s 0m00.34s \| Specific/Framework/CurveParameters \| 0m00.32s \|\| +0m00.02s 0m00.33s \| Specific/X2555/C128/CurveParameters \| 0m00.33s \|\| +0m00.00s 0m00.32s \| Specific/NISTP256/AMD128/CurveParameters \| N/A \|\| +0m00.32s 0m00.32s \| Specific/X2448/Karatsuba/C64/CurveParameters \| 0m00.33s \|\| -0m00.01s 0m00.31s \| Specific/Framework/CurveParametersPackage \| 0m00.33s \|\| -0m00.02s 0m00.30s \| Specific/NISTP256/AMD64/CurveParameters \| N/A \|\| +0m00.30s
*	Reorganize the curve-specific synthesis framework	Jason Gross	2017-10-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This brings in most of the changes that I made when figuring out how to integrate montgomery into the framework. The code is a bit slower because the we drop `Print Assumptions` at the bottom of each synthesis problem, to record that things are closed under the global context. If we remove this, we get back the time that we lost with this commit. After \| File Name \| Before \|\| Change --------------------------------------------------------------------------------------------- 13m10.63s \| Total \| 11m51.91s \|\| +1m18.71s --------------------------------------------------------------------------------------------- 1m15.83s \| Specific/X2555/C128/ladderstep \| 1m02.57s \|\| +0m13.25s 1m03.07s \| Specific/X25519/C32/femul \| 0m54.99s \|\| +0m08.07s 0m36.49s \| Specific/X25519/C32/fesquare \| 0m27.77s \|\| +0m08.72s 1m08.99s \| Specific/X2448/Karatsuba/C64/femul \| 1m01.88s \|\| +0m07.10s 0m26.82s \| Specific/X25519/C32/freeze \| 0m19.81s \|\| +0m07.01s 2m06.29s \| Specific/X25519/C64/ladderstep \| 2m00.03s \|\| +0m06.26s 0m17.48s \| Specific/X25519/C64/femul \| 0m10.81s \|\| +0m06.67s 0m14.78s \| Specific/X25519/C64/freeze \| 0m08.19s \|\| +0m06.58s 0m14.12s \| Specific/X25519/C64/fesquare \| 0m07.45s \|\| +0m06.66s 1m48.54s \| Specific/NISTP256/AMD64/femul \| 1m51.58s \|\| -0m03.04s 0m44.50s \| Specific/X2448/Karatsuba/C64/Synthesis \| 0m43.81s \|\| +0m00.68s 0m31.40s \| Specific/X25519/C32/Synthesis \| 0m31.02s \|\| +0m00.37s 0m25.72s \| Specific/IntegrationTestMontgomeryP256_128 \| 0m25.34s \|\| +0m00.37s 0m18.36s \| Specific/NISTP256/AMD64/fesub \| 0m18.79s \|\| -0m00.42s 0m16.45s \| Specific/NISTP256/AMD64/feadd \| 0m16.40s \|\| +0m00.05s 0m15.15s \| Specific/NISTP256/AMD64/feopp \| 0m14.79s \|\| +0m00.36s 0m12.27s \| Specific/IntegrationTestMontgomeryP256_128_Sub \| 0m11.90s \|\| +0m00.36s 0m12.06s \| Specific/IntegrationTestMontgomeryP256_128_Add \| 0m11.89s \|\| +0m00.16s 0m10.93s \| Specific/IntegrationTestMontgomeryP256_128_Opp \| 0m11.39s \|\| -0m00.46s 0m10.12s \| Specific/X25519/C64/Synthesis \| 0m09.86s \|\| +0m00.25s 0m09.86s \| Specific/NISTP256/AMD64/fenz \| 0m09.54s \|\| +0m00.32s 0m09.40s \| Specific/IntegrationTestMontgomeryP256_128_Nonzero \| 0m09.16s \|\| +0m00.24s 0m06.08s \| Specific/X2555/C128/Synthesis \| 0m05.72s \|\| +0m00.36s 0m01.06s \| Specific/Framework/SynthesisFramework \| 0m00.98s \|\| +0m00.08s 0m01.05s \| Specific/X25519/C32/CurveParameters \| 0m01.01s \|\| +0m00.04s 0m00.88s \| Specific/Framework/ReificationTypes \| 0m00.84s \|\| +0m00.04s N/A \| Specific/Framework/ArithmeticSynthesisFramework \| 0m00.82s \|\| -0m00.82s 0m00.81s \| Specific/Framework/ArithmeticSynthesis/Karatsuba \| N/A \|\| +0m00.81s 0m00.79s \| Specific/Framework/ArithmeticSynthesis/SquareFromMul \| N/A \|\| +0m00.79s 0m00.79s \| Specific/Framework/ArithmeticSynthesis/Base \| N/A \|\| +0m00.79s 0m00.79s \| Specific/Framework/ArithmeticSynthesis/Freeze \| N/A \|\| +0m00.79s 0m00.78s \| Specific/Framework/ArithmeticSynthesis/BasePackage \| N/A \|\| +0m00.78s 0m00.76s \| Specific/Framework/IntegrationTestTemporaryMiscCommon \| 0m00.78s \|\| -0m00.02s 0m00.74s \| Specific/Framework/ArithmeticSynthesis/HelperTactics \| N/A \|\| +0m00.74s 0m00.74s \| Specific/Framework/ArithmeticSynthesis/KaratsubaPackage \| N/A \|\| +0m00.74s 0m00.73s \| Specific/Framework/ArithmeticSynthesis/FreezePackage \| N/A \|\| +0m00.73s 0m00.72s \| Specific/Framework/ReificationTypesPackage \| N/A \|\| +0m00.72s 0m00.70s \| Specific/Framework/ArithmeticSynthesis/Defaults \| N/A \|\| +0m00.70s 0m00.69s \| Specific/Framework/ArithmeticSynthesis/LadderstepPackage \| N/A \|\| +0m00.69s 0m00.69s \| Specific/Framework/ArithmeticSynthesis/DefaultsPackage \| N/A \|\| +0m00.69s 0m00.68s \| Specific/Framework/ArithmeticSynthesis/Ladderstep \| N/A \|\| +0m00.68s N/A \| Specific/Framework/LadderstepSynthesisFramework \| 0m00.68s \|\| -0m00.68s 0m00.42s \| Specific/Framework/IntegrationTestDisplayCommon \| 0m00.39s \|\| +0m00.02s 0m00.40s \| Specific/X25519/C64/CurveParameters \| 0m00.44s \|\| -0m00.03s 0m00.34s \| Specific/Framework/IntegrationTestDisplayCommonTactics \| 0m00.35s \|\| -0m00.00s 0m00.33s \| Specific/X2555/C128/CurveParameters \| 0m00.31s \|\| +0m00.02s 0m00.33s \| Specific/Framework/CurveParameters \| 0m00.31s \|\| +0m00.02s 0m00.33s \| Specific/Framework/CurveParametersPackage \| N/A \|\| +0m00.33s 0m00.31s \| Specific/X2448/Karatsuba/C64/CurveParameters \| 0m00.32s \|\| -0m00.01s 0m00.07s \| Specific/Framework/Packages \| N/A \|\| +0m00.07s
*	Fold Karatsuba into json format and synthesis	Jason Gross	2017-10-18
\| \| \| \| \|	The json format now takes an additional, optional "goldilocks" boolean / boolean-string key determining if we're doing karatsuba.
*	Build curve-specific files from json	Jason Gross	2017-10-18
	The X25519 curves are now generated from `.json` files. This code only works in >= 8.7, because it makes use of the recently-merged-from-fiat `transparent_abstract` tactic to allow defining things in tactics without massive slowdown. The structure is as follows: 0. The module types and tactic definitions that set up the infrastructure live in `src/Specific/Framework/` 1. There are `.json` files in `src/Specific/CurveParameters/` that specify curve characteristics. A simple example is `x2555_130.json`, which is: ```json { "modulus" : "2^255-5", "base" : "130", "a24" : "121665 (* XXX TODO(andreser) FIXME? Is this right for this curve? )", "sz" : "3", "bitwidth" : "128", "carry_chain1" : "default", "carry_chain2" : ["0", "1"], "coef_div_modulus" : "2", "operations" : ["ladderstep"] } ``` A more complicated example is `x25519_c64.json`: ```json { "modulus" : "2^255-19", "base" : "51", "a24" : "121665", "sz" : "5", "bitwidth" : "64", "carry_chain1" : "default", "carry_chain2" : ["0", "1"], "coef_div_modulus" : "2", "operations" : ["femul", "fesquare", "freeze", "ladderstep"], "extra_files" : ["X25519_C64/scalarmult.c"], "compiler" : "gcc -march=native -mtune=native -std=gnu11 -O3 -flto -fomit-frame-pointer -fwrapv -Wno-attributes", "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 )); " } ``` 3. The `src/Specific/CurveParameters/remake_curves.sh` script holds a list of curves to be made, what directories they should end up living in, and it invokes `src/Specific/Framework/make_curve.py` to transform these files into outputs. The Python script fills in a few defaults (such as computing `s` and `c` from the modulus, if you don't pass them explicitly), and does a lot of processing on the C code that is pasted verbatim from donna to get it to be in the right format for Coq. This Python script creates the files: - `CurveParameters.v` (the Coq-ified version of the json file, which instantiates an appropriate module type); - `Synthesis.v`, which instantiates a `MakeSynthesisTactics` with the curve parameter modules, invokes a tactic from the applied module functor to synthesize all of the relevant non-reflective bits (basically, what used to live in @jadephilipoom 's `ArithmeticSynthesisTest.v`), and then instantiates another module functor `PackageSynthesis` which defines notations via tactics in terms to access the names of the various fields defined by the synthesis tactic; - any other files you ask it for, such as `compiler.sh`, `femul.v`, `femulDisplay.v`. All of the `*Display.v` files are simple, and all the the operation synthesis files have a single `Definition` (with the appropriate type), and solve the definition by invoking a single tactic defined in `PackageSynthesis`, e.g., `synthesize_mul` or `synthesize_ladderstep`.

|

| | | | | |

Currently unused, but adding it here in preparation for removing reification (which will allow easy support of karatsuba separate from goldilocks).

|

| | | | | | | |

Following Andres' suggestions to allow making ladderstep from other synthesis things. It went though mostly without a hitch, though there were a number of boilerplate changes needed.

|

| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |

This allows it to be something other than log2(m)/sz. After | File Name | Before || Change ------------------------------------------------------------------------------------------- 8m20.82s | Total | 8m37.82s || -0m17.00s ------------------------------------------------------------------------------------------- 1m59.42s | Specific/NISTP256/AMD64/femul | 2m19.09s || -0m19.67s 3m28.66s | Specific/X25519/C64/ladderstep | 3m28.02s || +0m00.63s 0m24.97s | Specific/X25519/C64/femul | 0m24.60s || +0m00.36s 0m24.08s | Specific/NISTP256/AMD64/fesub | 0m23.48s || +0m00.59s 0m22.00s | Specific/NISTP256/AMD64/feadd | 0m21.34s || +0m00.66s 0m20.34s | Specific/X25519/C64/freeze | 0m19.76s || +0m00.57s 0m19.85s | Specific/X25519/C64/fesquare | 0m19.93s || -0m00.07s 0m18.04s | Specific/NISTP256/AMD64/feopp | 0m17.69s || +0m00.34s 0m15.10s | Specific/NISTP256/AMD64/fenz | 0m15.37s || -0m00.26s 0m08.31s | Specific/NISTP256/AMD64/Synthesis | 0m08.24s || +0m00.07s 0m05.96s | Specific/X25519/C64/Synthesis | 0m06.25s || -0m00.29s 0m02.10s | Specific/Framework/ArithmeticSynthesis/Defaults | 0m02.14s || -0m00.04s 0m01.00s | Specific/Framework/SynthesisFramework | 0m01.03s || -0m00.03s 0m00.97s | Specific/Framework/ArithmeticSynthesis/Base | 0m01.02s || -0m00.05s 0m00.89s | Specific/Framework/ArithmeticSynthesis/Freeze | 0m00.84s || +0m00.05s 0m00.80s | Specific/Framework/ArithmeticSynthesis/Karatsuba | 0m00.81s || -0m00.01s 0m00.79s | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage | 0m00.80s || -0m00.01s 0m00.76s | Specific/Framework/MontgomeryReificationTypesPackage | 0m00.75s || +0m00.01s 0m00.74s | Specific/Framework/ReificationTypesPackage | 0m00.77s || -0m00.03s 0m00.74s | Specific/Framework/ArithmeticSynthesis/BasePackage | 0m00.74s || +0m00.00s 0m00.73s | Specific/Framework/ArithmeticSynthesis/SquareFromMul | 0m00.70s || +0m00.03s 0m00.72s | Specific/Framework/ArithmeticSynthesis/DefaultsPackage | 0m00.68s || +0m00.03s 0m00.70s | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | 0m00.72s || -0m00.02s 0m00.70s | Specific/Framework/ArithmeticSynthesis/FreezePackage | 0m00.77s || -0m00.07s 0m00.69s | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage | 0m00.70s || -0m00.01s 0m00.42s | Specific/X25519/C64/CurveParameters | 0m00.38s || +0m00.03s 0m00.36s | Specific/Framework/CurveParameters | 0m00.32s || +0m00.03s 0m00.33s | Specific/Framework/RawCurveParameters | 0m00.29s || +0m00.04s 0m00.33s | Specific/Framework/CurveParametersPackage | 0m00.30s || +0m00.03s 0m00.32s | Specific/NISTP256/AMD64/CurveParameters | 0m00.30s || +0m00.02s

| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |

This is a first step towards removing module functors from the code generation After | File Name | Before || Change --------------------------------------------------------------------------------------------- 13m12.84s | Total | 13m13.24s || -0m00.39s --------------------------------------------------------------------------------------------- 2m09.48s | Specific/X25519/C64/ladderstep | 2m03.07s || +0m06.40s 1m08.48s | Specific/X2448/Karatsuba/C64/femul | 1m12.93s || -0m04.45s 1m33.58s | Specific/NISTP256/AMD64/femul | 1m30.93s || +0m02.64s 1m06.71s | Specific/X2555/C128/ladderstep | 1m09.55s || -0m02.84s 0m35.01s | Specific/X25519/C32/fesquare | 0m36.58s || -0m01.57s 1m02.68s | Specific/X25519/C32/femul | 1m02.39s || +0m00.28s 0m44.51s | Specific/X2448/Karatsuba/C64/Synthesis | 0m44.29s || +0m00.21s 0m31.30s | Specific/X25519/C32/Synthesis | 0m31.17s || +0m00.12s 0m26.73s | Specific/X25519/C32/freeze | 0m27.38s || -0m00.64s 0m22.81s | Specific/NISTP256/AMD128/femul | 0m23.28s || -0m00.47s 0m20.30s | Specific/NISTP256/AMD64/fesub | 0m20.02s || +0m00.28s 0m17.76s | Specific/NISTP256/AMD64/feadd | 0m17.70s || +0m00.06s 0m17.04s | Specific/X25519/C64/femul | 0m17.51s || -0m00.47s 0m15.18s | Specific/X25519/C64/freeze | 0m14.93s || +0m00.25s 0m15.14s | Specific/NISTP256/AMD64/feopp | 0m15.32s || -0m00.17s 0m14.72s | Specific/NISTP256/AMD64/fenz | 0m14.68s || +0m00.04s 0m14.50s | Specific/X25519/C64/fesquare | 0m14.54s || -0m00.03s 0m14.26s | Specific/NISTP256/AMD128/feadd | 0m14.48s || -0m00.22s 0m14.21s | Specific/NISTP256/AMD128/fesub | 0m14.43s || -0m00.21s 0m14.10s | Specific/NISTP256/AMD128/fenz | 0m14.07s || +0m00.02s 0m11.67s | Specific/NISTP256/AMD128/feopp | 0m11.67s || +0m00.00s 0m10.12s | Specific/X25519/C64/Synthesis | 0m10.42s || -0m00.30s 0m08.53s | Specific/NISTP256/AMD64/Synthesis | 0m08.44s || +0m00.08s 0m06.44s | Specific/X2555/C128/Synthesis | 0m06.30s || +0m00.14s 0m03.65s | Specific/NISTP256/AMD128/Synthesis | 0m03.60s || +0m00.04s 0m01.00s | Specific/X25519/C32/CurveParameters | 0m01.07s || -0m00.07s 0m00.98s | Specific/Framework/SynthesisFramework | 0m01.00s || -0m00.02s 0m00.80s | Specific/Framework/ArithmeticSynthesis/Freeze | 0m00.73s || +0m00.07s 0m00.79s | Specific/Framework/ArithmeticSynthesis/Defaults | 0m00.74s || +0m00.05s 0m00.78s | Specific/Framework/ArithmeticSynthesis/Karatsuba | 0m00.79s || -0m00.01s 0m00.75s | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage | 0m00.71s || +0m00.04s 0m00.74s | Specific/Framework/ArithmeticSynthesis/Base | 0m00.77s || -0m00.03s 0m00.73s | Specific/Framework/ArithmeticSynthesis/FreezePackage | 0m00.69s || +0m00.04s 0m00.73s | Specific/Framework/MontgomeryReificationTypesPackage | 0m00.70s || +0m00.03s 0m00.72s | Specific/Framework/ReificationTypesPackage | 0m00.75s || -0m00.03s 0m00.70s | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage | 0m00.70s || +0m00.00s 0m00.69s | Specific/Framework/ArithmeticSynthesis/DefaultsPackage | 0m00.70s || -0m00.01s 0m00.68s | Specific/Framework/ArithmeticSynthesis/SquareFromMul | 0m00.72s || -0m00.03s 0m00.66s | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | 0m00.69s || -0m00.02s 0m00.65s | Specific/Framework/ArithmeticSynthesis/BasePackage | 0m00.66s || -0m00.01s 0m00.43s | Specific/X25519/C64/CurveParameters | 0m00.39s || +0m00.03s 0m00.34s | Specific/Framework/CurveParameters | 0m00.29s || +0m00.05s 0m00.32s | Specific/X2555/C128/CurveParameters | 0m00.30s || +0m00.02s 0m00.30s | Specific/NISTP256/AMD128/CurveParameters | 0m00.28s || +0m00.01s 0m00.30s | Specific/X2448/Karatsuba/C64/CurveParameters | 0m00.31s || -0m00.01s 0m00.30s | Specific/Framework/CurveParametersPackage | 0m00.29s || +0m00.01s 0m00.29s | Specific/NISTP256/AMD64/CurveParameters | 0m00.29s || +0m00.00s 0m00.26s | Specific/Framework/RawCurveParameters | N/A || +0m00.26s

| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |

Extra time comes from adding AMD128 to NISTP256, mostly. After | File Name | Before || Change --------------------------------------------------------------------------------------------- 13m25.13s | Total | 13m30.82s || -0m05.69s --------------------------------------------------------------------------------------------- N/A | Specific/IntegrationTestMontgomeryP256_128 | 0m25.42s || -0m25.42s 0m22.75s | Specific/NISTP256/AMD128/femul | N/A || +0m22.75s 1m31.64s | Specific/NISTP256/AMD64/femul | 1m52.42s || -0m20.78s 0m14.46s | Specific/NISTP256/AMD128/fesub | N/A || +0m14.46s 0m14.25s | Specific/NISTP256/AMD128/feadd | N/A || +0m14.25s 0m14.12s | Specific/NISTP256/AMD128/fenz | N/A || +0m14.11s N/A | Specific/NISTP256/AMD64/MontgomeryP256 | 0m13.00s || -0m13.00s N/A | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m12.40s || -0m12.40s N/A | Specific/IntegrationTestMontgomeryP256_128_Add | 0m11.99s || -0m11.99s 0m11.74s | Specific/NISTP256/AMD128/feopp | N/A || +0m11.74s N/A | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m11.22s || -0m11.22s N/A | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.27s || -0m09.26s N/A | Specific/MontgomeryP256_128 | 0m09.26s || -0m09.25s 0m08.42s | Specific/NISTP256/AMD64/Synthesis | N/A || +0m08.41s 0m14.67s | Specific/NISTP256/AMD64/fenz | 0m09.98s || +0m04.68s 0m04.12s | Specific/Framework/ArithmeticSynthesis/Montgomery | N/A || +0m04.12s 0m03.58s | Specific/NISTP256/AMD128/Synthesis | N/A || +0m03.58s 1m10.78s | Specific/X2555/C128/ladderstep | 1m08.36s || +0m02.42s 1m02.10s | Specific/X25519/C32/femul | 1m00.59s || +0m01.50s 0m43.59s | Specific/X2448/Karatsuba/C64/Synthesis | 0m44.86s || -0m01.26s 0m34.97s | Specific/X25519/C32/fesquare | 0m35.98s || -0m01.00s 0m20.10s | Specific/NISTP256/AMD64/fesub | 0m18.37s || +0m01.73s 0m17.61s | Specific/NISTP256/AMD64/feadd | 0m15.94s || +0m01.67s 2m09.77s | Specific/X25519/C64/ladderstep | 2m09.79s || -0m00.01s 1m11.70s | Specific/X2448/Karatsuba/C64/femul | 1m11.60s || +0m00.10s 0m32.14s | Specific/X25519/C32/Synthesis | 0m31.70s || +0m00.44s 0m27.94s | Specific/X25519/C32/freeze | 0m28.06s || -0m00.11s 0m17.62s | Specific/X25519/C64/femul | 0m17.41s || +0m00.21s 0m15.21s | Specific/X25519/C64/freeze | 0m14.74s || +0m00.47s 0m14.86s | Specific/NISTP256/AMD64/feopp | 0m14.96s || -0m00.10s 0m14.58s | Specific/X25519/C64/fesquare | 0m14.06s || +0m00.51s 0m10.10s | Specific/X25519/C64/Synthesis | 0m09.78s || +0m00.32s 0m06.22s | Specific/X2555/C128/Synthesis | 0m06.17s || +0m00.04s 0m01.01s | Specific/X25519/C32/CurveParameters | 0m01.05s || -0m00.04s 0m00.99s | Specific/Framework/SynthesisFramework | 0m01.08s || -0m00.09s 0m00.79s | Specific/Framework/MontgomeryReificationTypes | N/A || +0m00.79s 0m00.78s | Specific/Framework/ArithmeticSynthesis/SquareFromMul | 0m00.70s || +0m00.08s 0m00.78s | Specific/Framework/ArithmeticSynthesis/Karatsuba | 0m00.75s || +0m00.03s 0m00.76s | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage | N/A || +0m00.76s 0m00.75s | Specific/Framework/IntegrationTestTemporaryMiscCommon | 0m00.80s || -0m00.05s 0m00.75s | Specific/Framework/MontgomeryReificationTypesPackage | N/A || +0m00.75s 0m00.73s | Specific/Framework/ArithmeticSynthesis/Defaults | 0m00.75s || -0m00.02s 0m00.72s | Specific/Framework/ReificationTypesPackage | 0m00.70s || +0m00.02s 0m00.72s | Specific/Framework/ArithmeticSynthesis/Base | 0m00.73s || -0m00.01s 0m00.72s | Specific/Framework/ArithmeticSynthesis/BasePackage | 0m00.69s || +0m00.03s 0m00.72s | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | 0m00.76s || -0m00.04s 0m00.70s | Specific/Framework/ArithmeticSynthesis/Freeze | 0m00.75s || -0m00.05s 0m00.70s | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage | 0m00.77s || -0m00.07s 0m00.69s | Specific/Framework/ArithmeticSynthesis/DefaultsPackage | 0m00.71s || -0m00.02s 0m00.67s | Specific/Framework/ArithmeticSynthesis/FreezePackage | 0m00.74s || -0m00.06s 0m00.43s | Specific/X25519/C64/CurveParameters | 0m00.43s || +0m00.00s 0m00.38s | Specific/Framework/IntegrationTestDisplayCommon | 0m00.40s || -0m00.02s 0m00.38s | Specific/Framework/IntegrationTestDisplayCommonTactics | 0m00.37s || +0m00.01s 0m00.34s | Specific/Framework/CurveParameters | 0m00.32s || +0m00.02s 0m00.33s | Specific/X2555/C128/CurveParameters | 0m00.33s || +0m00.00s 0m00.32s | Specific/NISTP256/AMD128/CurveParameters | N/A || +0m00.32s 0m00.32s | Specific/X2448/Karatsuba/C64/CurveParameters | 0m00.33s || -0m00.01s 0m00.31s | Specific/Framework/CurveParametersPackage | 0m00.33s || -0m00.02s 0m00.30s | Specific/NISTP256/AMD64/CurveParameters | N/A || +0m00.30s

| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |

This brings in most of the changes that I made when figuring out how to integrate montgomery into the framework. The code is a bit slower because the we drop `Print Assumptions` at the bottom of each synthesis problem, to record that things are closed under the global context. If we remove this, we get back the time that we lost with this commit. After | File Name | Before || Change --------------------------------------------------------------------------------------------- 13m10.63s | Total | 11m51.91s || +1m18.71s --------------------------------------------------------------------------------------------- 1m15.83s | Specific/X2555/C128/ladderstep | 1m02.57s || +0m13.25s 1m03.07s | Specific/X25519/C32/femul | 0m54.99s || +0m08.07s 0m36.49s | Specific/X25519/C32/fesquare | 0m27.77s || +0m08.72s 1m08.99s | Specific/X2448/Karatsuba/C64/femul | 1m01.88s || +0m07.10s 0m26.82s | Specific/X25519/C32/freeze | 0m19.81s || +0m07.01s 2m06.29s | Specific/X25519/C64/ladderstep | 2m00.03s || +0m06.26s 0m17.48s | Specific/X25519/C64/femul | 0m10.81s || +0m06.67s 0m14.78s | Specific/X25519/C64/freeze | 0m08.19s || +0m06.58s 0m14.12s | Specific/X25519/C64/fesquare | 0m07.45s || +0m06.66s 1m48.54s | Specific/NISTP256/AMD64/femul | 1m51.58s || -0m03.04s 0m44.50s | Specific/X2448/Karatsuba/C64/Synthesis | 0m43.81s || +0m00.68s 0m31.40s | Specific/X25519/C32/Synthesis | 0m31.02s || +0m00.37s 0m25.72s | Specific/IntegrationTestMontgomeryP256_128 | 0m25.34s || +0m00.37s 0m18.36s | Specific/NISTP256/AMD64/fesub | 0m18.79s || -0m00.42s 0m16.45s | Specific/NISTP256/AMD64/feadd | 0m16.40s || +0m00.05s 0m15.15s | Specific/NISTP256/AMD64/feopp | 0m14.79s || +0m00.36s 0m12.27s | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m11.90s || +0m00.36s 0m12.06s | Specific/IntegrationTestMontgomeryP256_128_Add | 0m11.89s || +0m00.16s 0m10.93s | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m11.39s || -0m00.46s 0m10.12s | Specific/X25519/C64/Synthesis | 0m09.86s || +0m00.25s 0m09.86s | Specific/NISTP256/AMD64/fenz | 0m09.54s || +0m00.32s 0m09.40s | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.16s || +0m00.24s 0m06.08s | Specific/X2555/C128/Synthesis | 0m05.72s || +0m00.36s 0m01.06s | Specific/Framework/SynthesisFramework | 0m00.98s || +0m00.08s 0m01.05s | Specific/X25519/C32/CurveParameters | 0m01.01s || +0m00.04s 0m00.88s | Specific/Framework/ReificationTypes | 0m00.84s || +0m00.04s N/A | Specific/Framework/ArithmeticSynthesisFramework | 0m00.82s || -0m00.82s 0m00.81s | Specific/Framework/ArithmeticSynthesis/Karatsuba | N/A || +0m00.81s 0m00.79s | Specific/Framework/ArithmeticSynthesis/SquareFromMul | N/A || +0m00.79s 0m00.79s | Specific/Framework/ArithmeticSynthesis/Base | N/A || +0m00.79s 0m00.79s | Specific/Framework/ArithmeticSynthesis/Freeze | N/A || +0m00.79s 0m00.78s | Specific/Framework/ArithmeticSynthesis/BasePackage | N/A || +0m00.78s 0m00.76s | Specific/Framework/IntegrationTestTemporaryMiscCommon | 0m00.78s || -0m00.02s 0m00.74s | Specific/Framework/ArithmeticSynthesis/HelperTactics | N/A || +0m00.74s 0m00.74s | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage | N/A || +0m00.74s 0m00.73s | Specific/Framework/ArithmeticSynthesis/FreezePackage | N/A || +0m00.73s 0m00.72s | Specific/Framework/ReificationTypesPackage | N/A || +0m00.72s 0m00.70s | Specific/Framework/ArithmeticSynthesis/Defaults | N/A || +0m00.70s 0m00.69s | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | N/A || +0m00.69s 0m00.69s | Specific/Framework/ArithmeticSynthesis/DefaultsPackage | N/A || +0m00.69s 0m00.68s | Specific/Framework/ArithmeticSynthesis/Ladderstep | N/A || +0m00.68s N/A | Specific/Framework/LadderstepSynthesisFramework | 0m00.68s || -0m00.68s 0m00.42s | Specific/Framework/IntegrationTestDisplayCommon | 0m00.39s || +0m00.02s 0m00.40s | Specific/X25519/C64/CurveParameters | 0m00.44s || -0m00.03s 0m00.34s | Specific/Framework/IntegrationTestDisplayCommonTactics | 0m00.35s || -0m00.00s 0m00.33s | Specific/X2555/C128/CurveParameters | 0m00.31s || +0m00.02s 0m00.33s | Specific/Framework/CurveParameters | 0m00.31s || +0m00.02s 0m00.33s | Specific/Framework/CurveParametersPackage | N/A || +0m00.33s 0m00.31s | Specific/X2448/Karatsuba/C64/CurveParameters | 0m00.32s || -0m00.01s 0m00.07s | Specific/Framework/Packages | N/A || +0m00.07s

| | | | |

The json format now takes an additional, optional "goldilocks" boolean / boolean-string key determining if we're doing karatsuba.

The X25519 curves are now generated from `.json` files. This code only works in >= 8.7, because it makes use of the recently-merged-from-fiat `transparent_abstract` tactic to allow defining things in tactics without massive slowdown. The structure is as follows: 0. The module types and tactic definitions that set up the infrastructure live in `src/Specific/Framework/` 1. There are `.json` files in `src/Specific/CurveParameters/` that specify curve characteristics. A simple example is `x2555_130.json`, which is: ```json { "modulus" : "2^255-5", "base" : "130", "a24" : "121665 (* XXX TODO(andreser) FIXME? Is this right for this curve? *)", "sz" : "3", "bitwidth" : "128", "carry_chain1" : "default", "carry_chain2" : ["0", "1"], "coef_div_modulus" : "2", "operations" : ["ladderstep"] } ``` A more complicated example is `x25519_c64.json`: ```json { "modulus" : "2^255-19", "base" : "51", "a24" : "121665", "sz" : "5", "bitwidth" : "64", "carry_chain1" : "default", "carry_chain2" : ["0", "1"], "coef_div_modulus" : "2", "operations" : ["femul", "fesquare", "freeze", "ladderstep"], "extra_files" : ["X25519_C64/scalarmult.c"], "compiler" : "gcc -march=native -mtune=native -std=gnu11 -O3 -flto -fomit-frame-pointer -fwrapv -Wno-attributes", "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 )); " } ``` 3. The `src/Specific/CurveParameters/remake_curves.sh` script holds a list of curves to be made, what directories they should end up living in, and it invokes `src/Specific/Framework/make_curve.py` to transform these files into outputs. The Python script fills in a few defaults (such as computing `s` and `c` from the modulus, if you don't pass them explicitly), and does a lot of processing on the C code that is pasted verbatim from donna to get it to be in the right format for Coq. This Python script creates the files: - `CurveParameters.v` (the Coq-ified version of the json file, which instantiates an appropriate module type); - `Synthesis.v`, which instantiates a `MakeSynthesisTactics` with the curve parameter modules, invokes a tactic from the applied module functor to synthesize all of the relevant non-reflective bits (basically, what used to live in @jadephilipoom 's `ArithmeticSynthesisTest.v`), and then instantiates another module functor `PackageSynthesis` which defines notations via tactics in terms to access the names of the various fields defined by the synthesis tactic; - any other files you ask it for, such as `compiler.sh`, `femul.v`, `femulDisplay.v`. All of the `*Display.v` files are simple, and all the the operation synthesis files have a single `Definition` (with the appropriate type), and solve the definition by invoking a single tactic defined in `PackageSynthesis`, e.g., `synthesize_mul` or `synthesize_ladderstep`.