fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Fix for Coq 8.5 (more unfolding)	Jason Gross	2016-11-15
\|
*	Fix sqrt handling in specificgen	Jason Gross	2016-11-14
\|
*	Handle both kinds of sqrt	Jason Gross	2016-11-14
\|
*	More generic sqrt in SpecificGen	Jason Gross	2016-11-14
\|
*	More generic sqrt	Jason Gross	2016-11-14
\|
*	Copy over better prefreeze	Jason Gross	2016-11-14
\|
*	Fix postfreezeW_correct_and_bounded	Jason Gross	2016-11-14
\|
*	Update SpecificGen to be faster	Jason Gross	2016-11-14
\|
*	Speed up some GF25519 tactics	Jason Gross	2016-11-14
\|
*	Support for 128-bit words	Jason Gross	2016-11-14
\| \| \| \| \|	I haven't found a good way to genericize the proofs of relatedness things, mostly because Modules and functors are annoying.
*	Add word-size-independent interpretations	Jason Gross	2016-11-14
\|
*	Update sqrtm1 for 3mod4	Jason Gross	2016-11-14
\|
*	Fix some sqrt things	Jason Gross	2016-11-14
\|
*	Fix a missing unfold	Jason Gross	2016-11-14
\|
*	Fix a missing unfold	Jason Gross	2016-11-14
\|
*	Update bounds things with prefreeze	Jason Gross	2016-11-14
\|
*	Fix changes in naming in SpecificGen	Jason Gross	2016-11-14
\|
*	extraction: inline field operations into group operations	Andres Erbsen	2016-11-14
\|
*	for i in *.json; do ./copy_bounds.sh $i; done	Jason Gross	2016-11-14
\|
*	Add mulW_noinline	Jason Gross	2016-11-14
\|
*	Proper_sqrt	Andres Erbsen	2016-11-13
\|
*	Proper_sqrt_3mod4 Proper_sqrt_5mod8	Andres Erbsen	2016-11-13
\|
*	Don't copy bounds files if no argument is passed	Jason Gross	2016-11-13
\|
*	Add SpecificGen/GF*	Jason Gross	2016-11-13
\| \| \| \|	For bounds analysis
*	Work around bug #5198 (broken tc resolution)	Jason Gross	2016-11-12
\| \| \| \| \|	This is https://coq.inria.fr/bugs/show_bug.cgi?id=5198, Inlining lets breaks typechecking of [Definition]s
*	More 8.4pl2 fixes	Jason Gross	2016-11-12
\| \| \| \|	Also, I meant 8.4pl2 in the previous commit, not 8.2
*	Fix for Coq 8.2	Jason Gross	2016-11-12
\|
*	Fix for Coq 8.4pl2	Jason Gross	2016-11-12
\|
*	Remove extra admitted lemmas in 8.4	Jason Gross	2016-11-12
\|
*	Fixes for 8.4 (instantiate)	Jason Gross	2016-11-12
\|
*	GF25519: add ErepAdd	Andres Erbsen	2016-11-11
\|
*	GF25519: add optimized addition chain	Andres Erbsen	2016-11-11
\|
*	use @implicits in rewrite (8.4)	Andres Erbsen	2016-11-11
\|
*	Proved postfreezeW_correct_and_bounded	jadep	2016-11-11
\|
*	Remove dead code in rebuild-reified.py	Jason Gross	2016-11-11
\|
*	Begin filling in @JasonGross's stubs	jadep	2016-11-11
\|
*	Define word version of conditional subtraction	jadep	2016-11-11
\|
*	separate freeze into two parts	jadep	2016-11-11
\|
*	Fix reification of neg	Jason Gross	2016-11-11
\| \| \| \|	Note that we don't actually use reified neg anywhwere. If we did, the previous commit wouldn't've built...
*	Make [neg] a unary operation in reflection	Jason Gross	2016-11-11
\| \| \| \| \| \|	It now takes a meta-level [Z] argument which is the bit width. I haven't modified any of the extraction directives, so I don't know if extraction still works nicely.
*	Remove more conditional subtract	Jason Gross	2016-11-11
\|
*	Remove extra conditional subtract things	Jason Gross	2016-11-11
\|
*	Remove special code for reified conditional sub	Jason Gross	2016-11-11
\|
*	8.4-compatible universe handling	Jason Gross	2016-11-11
\|
*	Remove 8.6 only syntax	Jason Gross	2016-11-11
\|
*	Automatically generate code for field operations with different primes	jadep	2016-11-11
\|
*	Freeze stubs	Jason Gross	2016-11-11
\|
*	Lemmas about winit, wlast	Rob Sloan	2016-11-11
\|
*	prove last HList admit	Andres Erbsen	2016-11-11
\|
*	prove admits in Util.Tuple	Andres Erbsen	2016-11-11
\|