fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add some rewrites and admitted lemmas	Jason Gross	2016-10-27
\|
*	Add beginnings of various interpretations of expression trees	Jason Gross	2016-10-27
\|
*	Add {push,pull}_Zof_N hint db to ZUtil	Jason Gross	2016-10-27
\|
*	Merge pull request #84 from mit-plv/rsloan-phoas	Jason Gross	2016-10-27
\|\ \| \| \| \|	Patching master with most of my Conversion refactors
* \|	prove admit about F.to_nat x mod m	Andres Erbsen	2016-10-27
\| \|
* \|	proved last admit (Proper_feEnc) in Experiments/Ed25519	jadep	2016-10-27
\| \|
* \|	proved an admit (eq_enc_S_iff) in Ed25519.v	jadep	2016-10-27
\| \|
* \|	Add Inline import	Jason Gross	2016-10-27
\| \| \| \| \| \| \| \|	N.B. The proof of Wf for InlineConst is currently admitted
* \|	Add {un,}curry_wire_digits	Jason Gross	2016-10-27
\| \|
* \|	CompleteEdwardsCurve.ExtendedCoordinates: remove admitted lift_homomorphism ↵	Andres Erbsen	2016-10-27
\| \| \| \| \| \| \| \|	lemma that did not turn out to be necessary
* \|	Add {un,}curry_{bin,un}op_fe25519	Jason Gross	2016-10-27
\| \|
* \|	Add length_fe25519	Jason Gross	2016-10-27
\| \| \| \| \| \| \| \|	It'll be needed for generic reification and uncurrying
* \|	Fix implicit status of curry	Jason Gross	2016-10-27
\| \|
* \|	Add curry and uncurry to tuple	Jason Gross	2016-10-27
\| \|
* \|	Add syntax and reification for the ops in GF25519	Jason Gross	2016-10-27
\| \| \| \| \| \| \| \|	That is, for add, sub, mul, opp, freeze, ge_modulus, pack, and unpack.
* \|	Fix a missing import in previous commit	Jason Gross	2016-10-27
\| \|
* \|	Factor out cmov{l,ne} and neg	Jason Gross	2016-10-27
\| \| \| \| \| \| \| \|	This way we will have a faster build of reification things
* \|	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
\| \| \| \| \| \| \| \|	Not sure if it's needed, but it was pretty easy to write...
* \|	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 ↵	jadep	2016-10-27
\| \| \| \| \| \| \| \|	properly account for the case when which [n] and [pred n] are BOTH out of bounds in my statement of initial bounds)
* \|	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
\| \| \| \| \| \| \| \|	Prep for WfRelReflective
* \|	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
\| \| \| \| \| \| \| \|	This allows side conditions to be solved more quickly
* \|	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
\| \|