fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	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.
*	Remove coqprime-8.4	Jason Gross	2017-04-02
\| \| \| \| \| \| \|	We're using tactics in terms in some places, and so have no hope of compiling with Coq 8.4. We no longer pretend to support it. We can probably also remove some other compatibility things, if we want.