fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Separate out a24 constant as a Z	Jason Gross	2017-10-18
\|
*	Saner checking for freeze and ladderstep	Jason Gross	2017-10-18
\|
*	Move more of carry_sig, zero_sig, one_sig, etc to gallina	Jason Gross	2017-10-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ------------------------------------------------------------------------------------------- 8m28.18s \| Total \| 8m28.73s \|\| -0m00.55s ------------------------------------------------------------------------------------------- 0m06.23s \| Specific/X25519/C64/Synthesis \| 0m09.93s \|\| -0m03.69s 3m28.42s \| Specific/X25519/C64/ladderstep \| 3m26.20s \|\| +0m02.22s 0m02.19s \| Specific/Framework/ArithmeticSynthesis/Defaults \| 0m00.71s \|\| +0m01.48s 2m03.48s \| Specific/NISTP256/AMD64/femul \| 2m04.36s \|\| -0m00.87s 0m24.97s \| Specific/X25519/C64/femul \| 0m24.56s \|\| +0m00.41s 0m24.38s \| Specific/NISTP256/AMD64/fesub \| 0m23.90s \|\| +0m00.48s 0m21.75s \| Specific/NISTP256/AMD64/feadd \| 0m21.87s \|\| -0m00.12s 0m20.38s \| Specific/X25519/C64/freeze \| 0m20.04s \|\| +0m00.33s 0m19.57s \| Specific/X25519/C64/fesquare \| 0m19.83s \|\| -0m00.25s 0m17.47s \| Specific/NISTP256/AMD64/feopp \| 0m17.87s \|\| -0m00.40s 0m15.16s \| Specific/NISTP256/AMD64/fenz \| 0m15.40s \|\| -0m00.24s 0m08.25s \| Specific/NISTP256/AMD64/Synthesis \| 0m08.38s \|\| -0m00.13s 0m04.01s \| Specific/Framework/ArithmeticSynthesis/Montgomery \| 0m03.90s \|\| +0m00.10s 0m01.06s \| Specific/Framework/ArithmeticSynthesis/Base \| 0m01.06s \|\| +0m00.00s 0m01.01s \| Specific/Framework/SynthesisFramework \| 0m00.95s \|\| +0m00.06s 0m00.90s \| Specific/Framework/ArithmeticSynthesis/HelperTactics \| 0m00.90s \|\| +0m00.00s 0m00.86s \| Specific/Framework/ArithmeticSynthesis/Freeze \| 0m00.75s \|\| +0m00.10s 0m00.82s \| Specific/Framework/MontgomeryReificationTypesPackage \| 0m00.78s \|\| +0m00.03s 0m00.81s \| Specific/Framework/ArithmeticSynthesis/Karatsuba \| 0m00.75s \|\| +0m00.06s 0m00.79s \| Specific/Framework/ArithmeticSynthesis/MontgomeryPackage \| 0m00.72s \|\| +0m00.07s 0m00.77s \| Specific/Framework/ReificationTypesPackage \| 0m00.76s \|\| +0m00.01s 0m00.75s \| Specific/Framework/ArithmeticSynthesis/LadderstepPackage \| 0m00.75s \|\| +0m00.00s 0m00.75s \| Specific/Framework/ArithmeticSynthesis/FreezePackage \| 0m00.74s \|\| +0m00.01s 0m00.72s \| Specific/Framework/ArithmeticSynthesis/KaratsubaPackage \| 0m00.72s \|\| +0m00.00s 0m00.69s \| Specific/Framework/ArithmeticSynthesis/BasePackage \| 0m00.73s \|\| -0m00.04s 0m00.68s \| Specific/Framework/ArithmeticSynthesis/DefaultsPackage \| 0m00.76s \|\| -0m00.07s 0m00.67s \| Specific/Framework/ArithmeticSynthesis/SquareFromMul \| 0m00.78s \|\| -0m00.10s 0m00.32s \| Specific/Framework/CurveParameters \| 0m00.31s \|\| +0m00.01s 0m00.32s \| Specific/Framework/CurveParametersPackage \| 0m00.33s \|\| -0m00.01s
*	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

|

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

After | File Name | Before || Change ------------------------------------------------------------------------------------------- 8m28.18s | Total | 8m28.73s || -0m00.55s ------------------------------------------------------------------------------------------- 0m06.23s | Specific/X25519/C64/Synthesis | 0m09.93s || -0m03.69s 3m28.42s | Specific/X25519/C64/ladderstep | 3m26.20s || +0m02.22s 0m02.19s | Specific/Framework/ArithmeticSynthesis/Defaults | 0m00.71s || +0m01.48s 2m03.48s | Specific/NISTP256/AMD64/femul | 2m04.36s || -0m00.87s 0m24.97s | Specific/X25519/C64/femul | 0m24.56s || +0m00.41s 0m24.38s | Specific/NISTP256/AMD64/fesub | 0m23.90s || +0m00.48s 0m21.75s | Specific/NISTP256/AMD64/feadd | 0m21.87s || -0m00.12s 0m20.38s | Specific/X25519/C64/freeze | 0m20.04s || +0m00.33s 0m19.57s | Specific/X25519/C64/fesquare | 0m19.83s || -0m00.25s 0m17.47s | Specific/NISTP256/AMD64/feopp | 0m17.87s || -0m00.40s 0m15.16s | Specific/NISTP256/AMD64/fenz | 0m15.40s || -0m00.24s 0m08.25s | Specific/NISTP256/AMD64/Synthesis | 0m08.38s || -0m00.13s 0m04.01s | Specific/Framework/ArithmeticSynthesis/Montgomery | 0m03.90s || +0m00.10s 0m01.06s | Specific/Framework/ArithmeticSynthesis/Base | 0m01.06s || +0m00.00s 0m01.01s | Specific/Framework/SynthesisFramework | 0m00.95s || +0m00.06s 0m00.90s | Specific/Framework/ArithmeticSynthesis/HelperTactics | 0m00.90s || +0m00.00s 0m00.86s | Specific/Framework/ArithmeticSynthesis/Freeze | 0m00.75s || +0m00.10s 0m00.82s | Specific/Framework/MontgomeryReificationTypesPackage | 0m00.78s || +0m00.03s 0m00.81s | Specific/Framework/ArithmeticSynthesis/Karatsuba | 0m00.75s || +0m00.06s 0m00.79s | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage | 0m00.72s || +0m00.07s 0m00.77s | Specific/Framework/ReificationTypesPackage | 0m00.76s || +0m00.01s 0m00.75s | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | 0m00.75s || +0m00.00s 0m00.75s | Specific/Framework/ArithmeticSynthesis/FreezePackage | 0m00.74s || +0m00.01s 0m00.72s | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage | 0m00.72s || +0m00.00s 0m00.69s | Specific/Framework/ArithmeticSynthesis/BasePackage | 0m00.73s || -0m00.04s 0m00.68s | Specific/Framework/ArithmeticSynthesis/DefaultsPackage | 0m00.76s || -0m00.07s 0m00.67s | Specific/Framework/ArithmeticSynthesis/SquareFromMul | 0m00.78s || -0m00.10s 0m00.32s | Specific/Framework/CurveParameters | 0m00.31s || +0m00.01s 0m00.32s | Specific/Framework/CurveParametersPackage | 0m00.33s || -0m00.01s

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