fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Factor karatsuba through IdfunWithAlt, add test	Jason Gross	2017-06-11
\| \| \| \| \| \| \| \| \| \| \|	Currently the refinement is commented out. Also, we drop the proof of equality early (and probably won't use it in the first place); there's no way we can carry around such a proof in reflective-land, so we'll need to add an arithmetical-equality semi-decider to reflective-land that can prove the relevant equalities (or we'll need to leave them over as side-conditions). I expeect this may make things significantly easier on @jadephilipoom.
*	Fix broken implicits	Jason Gross	2017-06-08
\| \| \| \|	Closes #190
*	start saturated-arithmetic API for use in Montgomery (see discussion in #157)	jadep	2017-06-08
\|
*	first stage of synthesis for karatsuba with alt-bounds hack, contains ↵	jadep	2017-06-07
\| \| \| \|	several admitted lemmas
*	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).
*	Make Karatsuba depend on Arithmetic/Core to make calling it less of a pain	jadep	2017-06-02
\|
*	pulled in a CPS version of Karatsuba from another branch	jadep	2017-06-02
\|
*	Strip trailing whitespace	Jason Gross	2017-06-02
\| \| \| \| \| \| \|	With ```bash bash ./etc/coq-scripts/formatting/strip-trailing-whitespace.sh ```
*	Only use bool in freeze	Jason Gross	2017-05-21
\| \| \| \|	This closes #186
*	fix last wide mul in curve25519-51	Andres Erbsen	2017-05-20
\|
*	src/Specific/x25519_c64.c.sh: use exact donna skeleton	Andres Erbsen	2017-05-20
\|
*	make display	Jason Gross	2017-05-20
\|
*	make display (freeze, fully notationified)	Jason Gross	2017-05-20
\| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change -------------------------------------------- 0m00.00s \| Total \| 0m00.00s \|\| +0m00.00s --------------------------------------------
*	make display	Jason Gross	2017-05-20
\| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change -------------------------------------------- 0m00.00s \| Total \| 0m00.00s \|\| +0m00.00s --------------------------------------------
*	make display	Jason Gross	2017-05-20
\| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change -------------------------------------------- 0m00.00s \| Total \| 0m00.00s \|\| +0m00.00s --------------------------------------------
*	make display (freeze, ladderstep with adc)	Jason Gross	2017-05-17
\|
*	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.
*	make display (with adc, bool)	Jason Gross	2017-05-17
\|
*	make display	Jason Gross	2017-05-17
\|
*	Add reflective machinery for adc, zselect	Jason Gross	2017-05-17
\|
*	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
\|