fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	minor updates needed to make it compile with bbv	Samuel Gruetter	2018-02-05
\| \| \| \|	removing lemma wordToNat_wzero is ok because it's already in bbv
*	Add eq_ZToWord	Jason Gross	2017-06-17
\|
*	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).
*	Use Z.max 0, not an if statement	Jason Gross	2017-04-08
\| \| \| \|	Leads to fewer match branches
*	Add wordToZ_ZToWord_mod_full	Jason Gross	2017-04-08
\|
*	Add wordToZ_ZToWord_mod	Jason Gross	2017-04-08
\|
*	Add ZToWord_wordToZ_ZToWord_small	Jason Gross	2017-04-08
\|
*	Add wordToZ{_gen,}_range	Jason Gross	2017-03-30
\|
*	Add log and non-log versions of FixedWordSizes lem	Jason Gross	2017-02-23
\|
*	Move things from WordUtil to ZUtil, add word lemma	Jason Gross	2017-02-06
\|
*	Split off non-unfolding version of fixed_size_op_to_word	Jason Gross	2017-02-03
\| \| \| \|	Called syntactic_fixed_size_op_to_word
*	Add valid_update lemmas about FixedWordSizes	Jason Gross	2017-02-03
\|
*	Don't unfold wordToZ_gen in fixed_Size_op_to_word	Jason Gross	2017-02-03
\| \| \| \|	It was messing up some proofs that relied on that being folded.
*	Fix a missing argument	Jason Gross	2017-02-03
\|
*	Fix a typo	Jason Gross	2017-02-03
\|
*	Handle more kinds of ops in fixed_size_op_to_word	Jason Gross	2017-02-03
\|
*	Add fixed_size_op_to_word tactic	Jason Gross	2017-02-03
\|
*	Add wordToZ_ZToWord_wordToZ	Jason Gross	2017-02-01
\|
*	Add ZToWord_wordToZ_ZToWord	Jason Gross	2017-02-01
\|
*	Add wordToZ_ZToWord, ZToWord_wordToZ	Jason Gross	2017-02-01
\|
*	Add transparent equality proofs for fixed wordT	Jason Gross	2017-01-21
	Such a pain to make proofs compute