fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Flip argument order on interp for easier Proper lemmas	Jason Gross	2017-05-16
\|
*	Add DeadCodeEliminationInterp	Jason Gross	2017-05-15
\|
*	use ladderstep from donna (2% faster?)	Andres Erbsen	2017-05-15
\|
*	disable ANormal form, we now support expression output!	Andres Erbsen	2017-05-14
\|
*	update c.sh for new return notation	Andres Erbsen	2017-05-14
\|
*	make display (for return statement)	Jason Gross	2017-05-14
\|
*	make display again (really not sure what's up)	Jason Gross	2017-05-14
\|
*	make display	Jason Gross	2017-05-14
\| \| \| \|	Not quite sure what changed....
*	force carry intermediates to be bound early	Andres Erbsen	2017-05-14
\|
*	make display (ladderstep with specialize square)	Jason Gross	2017-05-14
\|
*	Use specialized square in ladderstep	Jason Gross	2017-05-14
\|
*	Make proj1_sig square_sig take only one argument	Jason Gross	2017-05-14
\|
*	make display without 0x0 * _	Jason Gross	2017-05-14
\|
*	specialize squaring earlier	Andres Erbsen	2017-05-14
\|
*	preserve common subexpressions in donna-derived code	Andres Erbsen	2017-05-14
\|
*	applied micro-optimizations from donna with [transitivity] and [ring] (as ↵	jadep	2017-05-14
\| \| \| \|	per #176)
*	remove lingering [About]	jadephilipoom	2017-05-14
\|
*	make freeze use the correct versions of add_get_carry and zselect	jadep	2017-05-14
\|
*	CSE without inlining arithmetic expressions	Jason Gross	2017-05-14
\| \| \| \| \| \| \| \| \| \|	This takes care of most of #158. The remaining bits are reworking the Wf and interpretation lemmas to actually work. (The former needs a only bit of rethinking and rephrasing to handle the fact that sometimes we change the stored symbolic expression from a complicated one to a fresh variable, while the latter needs major surgery, which Adam tells me is easy, and this is a note that when I come back to it, I should look at the email thread with Adam about CSE from last summer.)
*	Support destructuring dlet and slet	Jason Gross	2017-05-13
\| \| \| \| \|	The current way to support it is a kludge around the fact that `x binder` only works for recursive notations
*	plug in tuple-select rather than using context variables	jadep	2017-05-01
\|
*	move hints and context outside section (this is what happens when you ↵	jadep	2017-05-01
\| \| \| \|	'organize' code last-minute and don't check that it still works)
*	first synthesis of freeze code	jadep	2017-05-01
\|
*	use IntegrationTestSquare in C code	Andres Erbsen	2017-04-22
\|
*	make display	Jason Gross	2017-04-20
\|
*	Update ladderstep display logs	Jason Gross	2017-04-17
\|
*	Inline a24_sig in ladderstep	Jason Gross	2017-04-17
\| \| \| \| \|	Update the pipeline to be powerful enough to take advantage of this change by doing more simplification.
*	Construct a24_sig	Jason Gross	2017-04-17
\|
*	Add a few more constants to ladderstep 130 display	Jason Gross	2017-04-15
\|
*	Also unfold lift3_sig	Jason Gross	2017-04-15
\|
*	Update display of ladderstep130	Jason Gross	2017-04-14
\|
*	Use 128/256 in ladderstep 130	Jason Gross	2017-04-14
\|
*	Split off a-normal form from flattening	Jason Gross	2017-04-14
\| \| \| \|	Now we can flatten let binders without putting operations in a-normal form
*	Add support for cse-modulo-normalization	Jason Gross	2017-04-14
\|
*	Add hand-cse'd version of square	Jason Gross	2017-04-14
\| \| \| \|	cc @andres-erbsen
*	Add display of square	Jason Gross	2017-04-14
\|
*	Update ladderstep display	Jason Gross	2017-04-14
\|
*	Handle new ladderstep and square in dsiplay	Jason Gross	2017-04-14
\|
*	Add test for square	Jason Gross	2017-04-14
\|
*	Clean up ladderstep goal with help from Andres	Jason Gross	2017-04-14
\| \| \| \| \| \| \|	It's now much simpler. Because it's much simpler, the goal that the glue code is given has more [Tuple.map], and fewer of them unfolded, so I've updated the glue code to handle more nested [Tuple.map] in front of [wordToZ].
*	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
*	Update display logs	Jason Gross	2017-04-13
\|
*	Update display to not line-wrap	Jason Gross	2017-04-13
\| \| \| \|	Add some notations to prevent massive indentation
*	Update ladderstep display	Jason Gross	2017-04-13
\|
*	Rewrite the ladderstep goal	Jason Gross	2017-04-13
\| \| \| \| \| \| \|	It's now more amenable to use in the montgomery loop, and the display will only have one copy of the code. Unfortunately, it's much more ad-hoc and kludgy now.
*	Add eexists_sig_etransitivity_for_rewrite_fun_R	Jason Gross	2017-04-13
\|
*	Add lift4_sig_sig	Jason Gross	2017-04-13
\|
*	Add eexists_sig_etransitivity_R	Jason Gross	2017-04-13
\|
*	Split off Compilers.Named.Context	Jason Gross	2017-04-10
\|
*	Update display logs	Jason Gross	2017-04-07
\|