fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Generalize phis	Jason Gross	2017-10-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ----------------------------------------------------------------------- 3m56.20s \| Total \| 4m14.86s \|\| -0m18.66s ----------------------------------------------------------------------- 0m02.44s \| Specific/X25519/C32/ReificationTypes \| 0m19.48s \|\| -0m17.03s 2m00.12s \| Specific/X25519/C64/ladderstep \| 1m55.72s \|\| +0m04.40s 0m01.16s \| Specific/X25519/C64/ReificationTypes \| 0m05.17s \|\| -0m04.00s 0m26.27s \| Specific/X25519/C32/fesquare \| 0m27.76s \|\| -0m01.49s 0m52.60s \| Specific/X25519/C32/femul \| 0m52.46s \|\| +0m00.14s 0m10.35s \| Specific/X25519/C64/femul \| 0m10.28s \|\| +0m00.07s 0m08.30s \| Specific/IntegrationTestSub \| 0m08.69s \|\| -0m00.38s 0m07.97s \| Specific/IntegrationTestFreeze \| 0m08.00s \|\| -0m00.03s 0m06.99s \| Specific/X25519/C64/fesquare \| 0m07.31s \|\| -0m00.31s
*	Factor out parameter-specific code	Jason Gross	2017-10-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ------------------------------------------------------------------------------ 6m08.27s \| Total \| 6m25.95s \|\| -0m17.68s ------------------------------------------------------------------------------ N/A \| Specific/ArithmeticSynthesisTest32 \| 0m39.62s \|\| -0m39.61s 0m38.34s \| Specific/X25519/C32/ArithmeticSynthesisTest \| N/A \|\| +0m38.34s 0m20.46s \| Specific/X25519/C32/ReificationTypes \| N/A \|\| +0m20.46s 2m31.97s \| Specific/X25519/C64/ladderstep \| 2m51.10s \|\| -0m19.12s N/A \| Specific/ArithmeticSynthesisTest \| 0m09.54s \|\| -0m09.53s 0m09.50s \| Specific/X25519/C64/ArithmeticSynthesisTest \| N/A \|\| +0m09.50s 1m03.72s \| Specific/X25519/C32/femul \| 1m11.22s \|\| -0m07.50s 0m10.44s \| Specific/IntegrationTestFreeze \| 0m17.29s \|\| -0m06.84s 0m34.55s \| Specific/X25519/C32/fesquare \| 0m40.47s \|\| -0m05.92s 0m05.50s \| Specific/X25519/C64/ReificationTypes \| N/A \|\| +0m05.50s 0m12.47s \| Specific/X25519/C64/femul \| 0m13.98s \|\| -0m01.50s 0m08.93s \| Specific/X25519/C64/fesquare \| 0m10.67s \|\| -0m01.74s 0m11.14s \| Specific/IntegrationTestSub \| 0m12.06s \|\| -0m00.92s 0m00.50s \| Specific/X25519/C32/CurveParameters \| N/A \|\| +0m00.50s 0m00.38s \| Specific/CurveParameters \| N/A \|\| +0m00.38s 0m00.37s \| Specific/X25519/C64/CurveParameters \| N/A \|\| +0m00.37s
*	Factor out some of the preglue synthesis code	Jason Gross	2017-07-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This makes it a bit more uniform, and hopefully more automatable and packageable. Unfortunately, there's still no spec for this part of the pipeline, so the tactics simply aggregate common patterns. Alas, this also makes things a bit slower; I suspect that [Defined] is the place where things are slower. After \| File Name \| Before \|\| Change --------------------------------------------------------------------------------------- 13m51.14s \| Total \| 12m59.29s \|\| +0m51.84s --------------------------------------------------------------------------------------- 1m54.18s \| Specific/IntegrationTestKaratsubaMul \| 1m43.12s \|\| +0m11.06s 1m38.97s \| Specific/IntegrationTestLadderstep130 \| 1m30.26s \|\| +0m08.70s 2m19.75s \| Specific/NISTP256/AMD64/femul \| 2m14.08s \|\| +0m05.66s 0m39.90s \| Specific/IntegrationTestMontgomeryP256_128 \| 0m34.21s \|\| +0m05.68s 0m21.95s \| Specific/NISTP256/AMD64/fesub \| 0m19.23s \|\| +0m02.71s 0m21.37s \| Specific/NISTP256/AMD64/feadd \| 0m18.82s \|\| +0m02.55s 0m21.02s \| Specific/X25519/C64/femul \| 0m18.32s \|\| +0m02.69s 0m20.53s \| Specific/IntegrationTestFreeze \| 0m23.26s \|\| -0m02.73s 0m18.28s \| Specific/IntegrationTestMontgomeryP256_128_Sub \| 0m15.32s \|\| +0m02.96s 0m18.20s \| Specific/IntegrationTestMontgomeryP256_128_Add \| 0m15.52s \|\| +0m02.67s 0m16.35s \| Specific/IntegrationTestMontgomeryP256_128_Opp \| 0m13.52s \|\| +0m02.83s 0m13.92s \| Specific/IntegrationTestMontgomeryP256_128_Nonzero \| 0m11.84s \|\| +0m02.08s 0m18.23s \| Specific/NISTP256/AMD64/MontgomeryP256 \| 0m16.62s \|\| +0m01.60s 0m15.54s \| Specific/IntegrationTestSub \| 0m14.53s \|\| +0m01.00s 0m14.78s \| Specific/X25519/C64/fesquare \| 0m13.13s \|\| +0m01.64s 0m13.71s \| Specific/NISTP256/AMD64/fenz \| 0m12.69s \|\| +0m01.02s 3m14.34s \| Specific/X25519/C64/ladderstep \| 3m14.32s \|\| +0m00.02s 0m16.54s \| Specific/NISTP256/AMD64/feopp \| 0m16.48s \|\| +0m00.05s 0m12.21s \| Specific/MontgomeryP256_128 \| 0m12.70s \|\| -0m00.48s 0m00.73s \| Specific/IntegrationTestTemporaryMiscCommon \| 0m00.72s \|\| +0m00.01s 0m00.64s \| Specific/IntegrationTestDisplayCommon \| 0m00.60s \|\| +0m00.04s
*	Switch to using uint8_t rather than bool for adc	Jason Gross	2017-06-18
\| \| \| \|	This closes #206
*	Don't rely on autogenerated names	Jason Gross	2017-06-05
\| \| \| \| \| \|	This fixes all of the private-names warnings emitted by compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus the ones in coqprime, which I didn't touch).
*	Only use bool in freeze	Jason Gross	2017-05-21
\| \| \| \|	This closes #186
*	Add compiler optimization for add-with-carry	Jason Gross	2017-05-17
\| \| \| \| \| \| \| \| \| \| \|	This closes #171. It's unfortunately a bit fragile, and takes a really long time (about 60s) to prove correct, because Coq is bad at deep dependent pattern matching. We enable a-normal form for the freeze test, because the rewriter only works when the arguments to adc are var or const.
*	Add reflective machinery for adc, zselect	Jason Gross	2017-05-17