fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Remove all the .v files in SpecificGen	Jason Gross	2017-04-02
\| \| \| \|	This gets most of the way to 10 in #14.
*	Switch to fully uncurried form for reflection	Jason Gross	2017-03-01
\| \| \| \| \| \| \| \| \| \| \|	This will eventually make a number of proofs easier. Unfortunately, the correctness lemmas for AddCoordinates and LadderStep no longer work (because of different arities), and there's a proof in Experiments/Ed25519 that I've admitted. The correctness lemmas will be easy to re-add when we have a more general version that handle arbitrary type shapes.
*	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
\|
*	Copy over better prefreeze	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.
*	Fix some sqrt things	Jason Gross	2016-11-14
\|
*	Fix a missing unfold	Jason Gross	2016-11-14
\|
*	Update bounds things with prefreeze	Jason Gross	2016-11-14
\|
*	for i in *.json; do ./copy_bounds.sh $i; done	Jason Gross	2016-11-14
\|
*	Add SpecificGen/GF*	Jason Gross	2016-11-13
	For bounds analysis