fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Fix display log	Jason Gross	2017-10-06
\|
*	Factor out some bits of ladderstep preglue	Jason Gross	2017-10-05
\| \| \| \| \|	This requires some changes to nonzero, which now needs to unfold proj1_sig itself.
*	Add missing tactic in comment in ladderstep	Jason Gross	2017-09-27
\|
*	Add src/Specific/X25519/C32/compiler.sh, update ↵	Jason Gross	2017-09-27
\| \| \| \|	src/Specific/X25519/C64/scalarmult.c
*	Add curve25519-donna-c64 to etc/third_party	Jason Gross	2017-09-27
\|
*	Add missing file	Jason Gross	2017-09-21
\|
*	Add femul,fesqure for C32	Jason Gross	2017-09-21
\| \| \| \| \|	32-bit ladderstep takes way too long (at least on Coq 8.6), so we don't add it yet
*	Add extract_Expr	Jason Gross	2017-09-21
\|
*	Split off tactics in IntegrationTestDisplayCommon	Jason Gross	2017-09-21
\|
*	make bench	Jason Gross	2017-09-12
\|
*	Fix more commented out alternatives	Jason Gross	2017-09-05
\|
*	Fix commented out alternate version in ladderstep	Jason Gross	2017-09-05
\|
*	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
*	More fine-grained tactics imports	Jason Gross	2017-07-08
\|
*	prove an admit in ArithmeticSynthesisTest	Andres Erbsen	2017-07-06
\|
*	make bench	Andres Erbsen	2017-07-06
\|
*	make bench	Jason Gross	2017-07-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	``` make -j test make -j -k bench touch capture.sh make -k bench sudo etc/turboboost.sh off sudo etc/hyperthreading.sh off touch capture.sh make -k bench sudo etc/turboboost.sh on sudo etc/hyperthreading.sh on ```
*	benchmark NISTZ256 with and without adx	Andres Erbsen	2017-07-05
\|
*	make bench	Andres Erbsen	2017-07-05
\|
*	make bench	Andres Erbsen	2017-07-04
\|
*	use att style assembly with icc, test it	Andres Erbsen	2017-07-04
\|
*	test p256 mixed addition	Andres Erbsen	2017-07-04
\| \| \| \| \|	passed after fixing some stupid typos in glue code -- no conceptual issues.
*	work around GCC issues 81294 and 81300	Andres Erbsen	2017-07-03
\|
*	fix mulx argument order using sed, test feadd, femul (fails due to #234)	Andres Erbsen	2017-07-03
\|
*	Fix display target	Jason Gross	2017-07-03
\|
*	X25519 test (passed on first try)	Andres Erbsen	2017-07-02
\|
*	automate P256 integration	Andres Erbsen	2017-07-02
\|
*	Merge branch 'use-cmovznz' of https://github.com/JasonGross/fiat-crypto	Andres Erbsen	2017-07-02
\|\
* \|	make display	Andres Erbsen	2017-07-01
\| \|
* \|	changes to log files after running make c	jadep	2017-07-01
\| \|
* \|	add missing import	jadep	2017-06-30
\| \|
* \|	Fix misnamed references in Specific/ (broke after saturated arithetic reorg)	jadep	2017-06-30
\| \|
* \|	Reorganization of saturated arithmetic	jadep	2017-06-29
\| \|
\| *	make display	Jason Gross	2017-06-29
\| \|
* \|	make display	Jason Gross	2017-06-29
\| \|
* \|	Fix unfolding to not unfold sub_with_get_borrow in P256	Jason Gross	2017-06-29
\|/
*	Use -std=gnu11 for older versions of gcc	Jason Gross	2017-06-28
\|
*	match C code in Jacobian addition	Andres Erbsen	2017-06-27
\|
*	p256 compilation and benchmarks with manual kludges	Andres Erbsen	2017-06-27
\|
*	More proof fixing	Jason Gross	2017-06-26
\|
*	Remove an admit	Jason Gross	2017-06-26
\| \| \| \|	This proof should possibly be factored out and go elsewhere.....
*	make display	Jason Gross	2017-06-26
\|
*	Add nonzero synthesis	Jason Gross	2017-06-26
\|
*	make display on p256	Andres Erbsen	2017-06-25
\|
*	make display	Jason Gross	2017-06-25
\|
*	make display	Jason Gross	2017-06-24
\|
*	Fix some things not being unfolded	Jason Gross	2017-06-24
\|
*	make display	Jason Gross	2017-06-24
\|
*	Clean up some montgomery wbw instantiation, make display	Jason Gross	2017-06-24
\|
*	Remove admits	Jason Gross	2017-06-24
\|