fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	benchmark NISTZ256 with and without adx	Andres Erbsen	2017-07-05
\|
*	fix .h dependencies in makefile (closes #235)	Andres Erbsen	2017-07-05
\|
*	benchmarking: correct for differences in CPU and TSC frequency	Andres Erbsen	2017-07-05
\|
*	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.
*	fix mulx argument order using sed, test feadd, femul (fails due to #234)	Andres Erbsen	2017-07-03
\|
*	X25519 test (passed on first try)	Andres Erbsen	2017-07-02
\|
*	automate P256 integration	Andres Erbsen	2017-07-02
\|
*	make bench: include all benchmarks	Andres Erbsen	2017-07-01
\|
*	benchmark OpenSSL p256 C code	Andres Erbsen	2017-07-01
\|
*	benchmark OpenSSL curve25519	Andres Erbsen	2017-07-01
\|
*	Add proper dependencies on .h file in Makefile	Jason Gross	2017-06-29
\|
*	Make the same display on windows and linux	Jason Gross	2017-06-28
\| \| \| \|	Do this by removing windows line endings via sed
*	p256 compilation and benchmarks with manual kludges	Andres Erbsen	2017-06-27
\|
*	Drop the two slowest files from the lite target	Jason Gross	2017-06-26
\|
*	add openssl nistz256 for benchmarking	Andres Erbsen	2017-06-23
\|
*	Makefile: c: h	Andres Erbsen	2017-06-20
\|
*	don't key benchmarks on cpu frequency	Andres Erbsen	2017-06-18
\|
*	measurements.txt depends on scripts that generate it	Andres Erbsen	2017-06-18
\|
*	"make bench", currently just X25519-C64 (closes #185)	Andres Erbsen	2017-06-18
\|
*	compile X25519 C code from Makefile	Andres Erbsen	2017-06-18
\|
*	Don't make curves proofs on travis (hopefully fast enough build)	Jason Gross	2017-06-17
\|
*	Fix notation-overriden warning issues	Jason Gross	2017-06-15
\| \| \| \|	This change is necessary because we've added -compat 8.6.
*	Add -compat 8.6 to _CoqProject	Jason Gross	2017-06-15
\| \| \| \| \| \|	This allows fiat-crypto to continue working with trunk, after the merge of https://github.com/coq/coq/pull/220. We will remove this when we migrate to requiring 8.6.1 or 8.7 (neither of which is released yet).
*	Add a printlite target to display lite files	Jason Gross	2017-06-14
\|
*	Error if Makefile.vo_closure doesn't exist and we need it	Jason Gross	2017-06-14
\|
*	Handle multiple lite-unmade-vofiles	Jason Gross	2017-06-12
\|
*	Fix lite target (typo in makefile fn call)	Jason Gross	2017-06-12
\|
*	Better support for coq_makefile2 with fewer warnings	Jason Gross	2017-06-12
\|
*	Don't print directory when entering coqprime folder	Jason Gross	2017-06-11
\|
*	Remove Karatsuba from the lite target	Jason Gross	2017-06-09
\| \| \| \|	It was pretty slow.
*	Compatibility with coq_makefile2	Jason Gross	2017-06-01
\| \| \| \|	Work harder to overwrite OTHERFLAGS if there's nothing there
*	Add only-heavy target	Jason Gross	2017-05-18
\|
*	specialize squaring earlier	Andres Erbsen	2017-05-14
\|
*	s/appcontext/context/	Jason Gross	2017-05-11
\| \| \| \|	They mean the same thing since 8.5, and appcontext is deprecated.
*	Track .dir-locals.el rather than generating it	Jason Gross	2017-04-24
\| \| \| \| \|	Since we're only using one version of coqprime, we no longer need to generate .dir-locals.el
*	X25519: wrap synthesized code in donna-c64, run SUPERCOP benchmarks	Andres Erbsen	2017-04-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	21% slower than donna 36% slower than assembly with saturated limbs. cycles impl compiler 593072 crypto_scalarmult/curve25519/amd64-64 gcc_-m64_-march=core-avx2_-O3_-fomit-frame-pointer 636660 crypto_scalarmult/curve25519/amd64-51 gcc_-funroll-loops_-fno-schedule-insns_-O2_-fomit-frame-pointer 660220 crypto_scalarmult/curve25519/donna_c64 gcc_-m64_-march=native_-mtune=native_-O3_-fomit-frame-pointer 804684 crypto_scalarmult/curve25519/fiat_c64 clang_-march=native_-O3_-fomit-frame-pointer_-fwrapv_-Qunused-arguments 815716 crypto_scalarmult/curve25519/fiat_c64 gcc_-m64_-march=core-avx2_-O3_-fomit-frame-pointer Setup: Broadwell i7-5600U 2.60GHz in an X1C3. no HT, no TB, wall power. Journalctl did not record any thermal throttling, idk if trustworthy. Cc: @achlipala @JasonGross @jadephilipoom
*	Makefile fixes	Jason Gross	2017-04-09
\| \| \| \| \| \| \|	Fix the lite target to remove all transitive (reverse) dependencies. Don't run `coqtop` to get the version unless we're actually going to use it to build things
*	Fix printreversedeps	Jason Gross	2017-04-09
\|
*	Add printreversedeps	Jason Gross	2017-04-09
\|
*	Display un-interped C code	Jason Gross	2017-04-07
\|
*	Add Display files and targets	Jason Gross	2017-04-07
\|
*	Ladderstep isn't that heavy	Jason Gross	2017-04-07
\|
*	Add IntegrationTestLadderstep.v	Jason Gross	2017-04-07
\|
*	Don't duplicate entries when updating _CoqProject	Jason Gross	2017-04-07
\| \| \| \|	This can happen if you're in the middle of resolving a merge conflict (git ls-files will list some files twice).
*	Clean up coq_makefile invocation	Jason Gross	2017-04-06
\| \| \| \| \|	We don't need that part of the `sed` command anymore, now that we no longer support 8.4.
*	Add note to makefile	Jason Gross	2017-04-03
\|
*	Add printdeps target to print recursive dependencies of a file	Jason Gross	2017-04-03
\|
*	Remove old reflective pipeline, making way the new	Jason Gross	2017-04-03
\|
*	Remove everything after the individual reified ops	Jason Gross	2017-04-03
\| \| \| \| \|	This includes extraction and associated targets. I've left the .hs files lying around, currently unused.