fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	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
\|
*	Revert change to [nsatz] (it was making Coq run out of memory)	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
\|
*	Various fixes in alternative nsatz	Jason Gross	2016-10-27
\|
*	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
\|
*	Add tactics to implement better fraction removal	Jason Gross	2016-10-26
\| \| \| \|	From https://github.com/coq/ceps/blob/master/text/007-nsatz-inequalities.md
*	Add lemmas about algebra	Jason Gross	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
\| \| \| \| \|	We don't have working word code yet, because the reification code currently does spurious word->N->Z->N->word conversions everywhere. So we use Z instead.
*	prove SRepMul admit	Andres Erbsen	2016-10-25
\|
*	Proved homomorphism between curve groups (Twisted Edwards Curve ↵	jadep	2016-10-24
\| \| \| \|	representation with coordinates in F and Extended representation with coordinates in GF25519)
*	Freeze before packing to get canonical encodings	jadep	2016-10-24
\|
*	ed25519: prove some admits	Andres Erbsen	2016-10-24
\|