fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	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
\|
*	Allow 'bool' in output	Jason Gross	2017-05-17
\|
*	Add notations for adc	Jason Gross	2017-05-17
\| \| \| \|	This closes #173
*	make display	Jason Gross	2017-05-17
\|
*	Zselect notation	Jason Gross	2017-05-17
\|
*	Add reflective machinery for adc, zselect	Jason Gross	2017-05-17
\|
*	Ltac scope interprets some notations as errors, so we make anf a definition	Jason Gross	2017-05-17
\|
*	Fix a typo in prev commit, add convenience notation	Jason Gross	2017-05-17
\|
*	Allow specifying pipeline options at call-time	Jason Gross	2017-05-17
\| \| \| \| \|	For now, the only option is anormal-form. This will be needed for freeze, because the adc optimization doesn't work when not in anf.
*	Update adc lemmas to version freeze actually uses	Jason Gross	2017-05-17
\|
*	Add more context proper lemmas	Jason Gross	2017-05-16
\|
*	Flip argument order on interp for easier Proper lemmas	Jason Gross	2017-05-16
\|
*	Add context_equiv and prove some Proper lemmas	Jason Gross	2017-05-16
\|
*	Revert "Add dec_eq_positive"	Jason Gross	2017-05-16
\| \| \| \| \| \|	This reverts commit 3a494ebb0d6ba4fa7952be40203ca4b573e37904. It already existed.
*	Add dec_eq_positive	Jason Gross	2017-05-16
\|
*	Flip order of extendb, lookup arguments	Jason Gross	2017-05-16
\| \| \| \|	This allows better Proper lemmas
*	Remove useless argument	Jason Gross	2017-05-16
\|
*	Add Interp_compile	Jason Gross	2017-05-16
\|
*	Slightly better type for Interp_InterpToPHOAS	Jason Gross	2017-05-16
\|
*	Add Named.ExprInversion	Jason Gross	2017-05-15
\|
*	Add Wf_from_unit	Jason Gross	2017-05-15
\| \| \| \| \|	This one is much easier to compute with, and it means we can get rid of a lot of pesky Named.wff proofs.
*	Add more pointed prop lemmas	Jason Gross	2017-05-15
\|
*	Add src/Compilers/Z/Named/DeadCodeEliminationInterp.v	Jason Gross	2017-05-15
\|
*	Add DeadCodeEliminationInterp	Jason Gross	2017-05-15
\|
*	Add a stronger lemma to registerassigninterp	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
\|
*	Add reserved java notation	Jason Gross	2017-05-14
\|
*	Add a reserved C notation	Jason Gross	2017-05-14
\|
*	update c.sh for new return notation	Andres Erbsen	2017-05-14
\|
*	Merge branch 'with-return' of https://github.com/JasonGross/fiat-crypto into ↵	Andres Erbsen	2017-05-14
\|\ \| \| \| \| \| \|	return-notation
* \|	Add GetNames	Jason Gross	2017-05-14
\| \|
* \|	Add Named.default_names_for	Jason Gross	2017-05-14
\| \|
\| *	make display (for return statement)	Jason Gross	2017-05-14
\| \|
\| *	Stick 'return' at the end of printed functions	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....
*	Add Named.CountLets	Jason Gross	2017-05-14
\|
*	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
\|
*	Add Z/Named/DeadCodeElimination.v	Jason Gross	2017-05-14
\|
*	Split off EliminateDeadCode	Jason Gross	2017-05-14
\|
*	make display without 0x0 * _	Jason Gross	2017-05-14
\|
*	Do more arithmetic simplifying	Jason Gross	2017-05-14
\| \| \| \|	Needed to remove some multiplication by 0
*	specialize squaring earlier	Andres Erbsen	2017-05-14
\|
*	preserve common subexpressions in donna-derived code	Andres Erbsen	2017-05-14
\|