fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
...
* \|	PHOAS notation fixups	Jason Gross	2016-10-27
* \|	Make it easier to export only phoas notations	Jason Gross	2016-10-27
* \|	add wf, not only rel_wf, to MapInterpWf	Jason Gross	2016-10-27
* \|	Add WfRelReflective	Jason Gross	2016-10-27
* \|	Factor WfReflective through WfReflectiveGen	Jason Gross	2016-10-27
* \|	removed now irrelevant commented-out code	jadep	2016-10-27
* \|	convert feEnc correctness proof to bounded type	jadep	2016-10-27
* \|	finished feEnc correctness	jadep	2016-10-27
* \|	most of feEnc correctness proof	jadep	2016-10-27
* \|	Slightly loosen freeze preconditions (in particular, I had failed to properly...	jadep	2016-10-27
* \|	add extra convenience lemmas about boundedness of convert	jadep	2016-10-27
* \|	removed lingering TODO	jadep	2016-10-27
* \|	Implicits for reflect_wfT	Jason Gross	2016-10-27
* \|	Add WfReflectiveGen	Jason Gross	2016-10-27
* \|	Move interp_flat_type_gen_rel_pointwise2 to Syntax	Jason Gross	2016-10-27
* \|	Add Wf proofs about MapInterp	Jason Gross	2016-10-27
* \|	Add arguments to mapf_interp_flat_type_gen	Jason Gross	2016-10-27
* \|	Add implicits to interp_flat_type_gen_rel_pointwise2	Jason Gross	2016-10-27
* \|	Change the argument implicits on rel_wff	Jason Gross	2016-10-27
\| *	Merge branch 'master' into rsloan-phoas	Jason Gross	2016-10-27
\| \|\ \| \|/ \|/\|
* \|	Revert change to [nsatz] (it was making Coq run out of memory)	Jason Gross	2016-10-27
\| *	Merge branch 'master' into rsloan-phoas	Jason Gross	2016-10-27
\| \|\
* \| \|	Simplify proof of proj1_fe25519_encode	Jason Gross	2016-10-27
* \| \|	Add lemmas about GF25519BoundedCommon.{encode,decode}	Jason Gross	2016-10-27
\| \|/ \|/\|
\| *	Fixes for Coq 8.4	Jason Gross	2016-10-27
\| *	Strip function extensionality, enable printing of sub, mul, opp, freeze	Jason Gross	2016-10-27
* \|	Various fixes in alternative nsatz	Jason Gross	2016-10-27
\| *	Tactics to manually remove Z.to/of_N and such	Robert Sloan	2016-10-26
* \|	Handle folded [not] in nsatz_strip_fractions	Jason Gross	2016-10-26
* \|	Split inequalities before specializing	Jason Gross	2016-10-26
* \|	Fix nsatz: don't clear inequalities	Jason Gross	2016-10-26
* \|	Fix a missing case in generalize_inv	Jason Gross	2016-10-26
* \|	Fix typos	Jason Gross	2016-10-26
* \|	Add tactics to implement better fraction removal	Jason Gross	2016-10-26
* \|	Add lemmas about algebra	Jason Gross	2016-10-26
\| *	Refactors to remove intermediate conversions	Robert Sloan	2016-10-26
* \|	Fix for Coq 8.4 (f_equiv changed behavior)	Jason Gross	2016-10-26
* \|	Initial work on filling ed25519 with bounded things	Jason Gross	2016-10-25
* \|	Switch to bounded Z	Jason Gross	2016-10-25
\| *	Refactors to remove intermediate conversions in HLConversions	Robert Sloan	2016-10-25
* \|	prove SRepMul admit	Andres Erbsen	2016-10-25
* \|	Proved homomorphism between curve groups (Twisted Edwards Curve representatio...	jadep	2016-10-24
* \|	Freeze before packing to get canonical encodings	jadep	2016-10-24
* \|	ed25519: prove some admits	Andres Erbsen	2016-10-24
* \|	Fix for Coq 8.4	Jason Gross	2016-10-24
* \|	Add more relations about fieldwise	Jason Gross	2016-10-24
* \|	Adjust bound on final word in wire_digits to 31	Jason Gross	2016-10-24
* \|	Fix bounds on wire_digits	Jason Gross	2016-10-24
\| *	Merge branch 'rsloan-phoas' of github.com:mit-plv/fiat-crypto into rsloan-phoas	Robert Sloan	2016-10-24
\| \|\
\| * \|	Use HL conversions for all data types + Pipeline.v refactors	Robert Sloan	2016-10-24