fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Move FancyMachine from Experiments to Specific	Jason Gross	2016-09-08
\| \| \| \| \| \| \| \| \| \|	Quoting Andres: > I am leaning towards putting this in Specifc instead of Experiments -- it > seems like complete result on its own, these files are unlikely to be reused > for something else, and I don't think we are expecting to need to remove it > any time soon. Currently, `Specific` code does not quantify over anything (no > context variables), but this seems secondary. We could make versions of this > with the curve constants plugged in, though.
*	make 8.4 happier	jadep	2016-09-06
\|
*	Finished sqrt in GF25519	jadep	2016-09-06
\|
*	Pushed [freeze] through to GF25519 in preparation for defining [sqrt], ↵	jadep	2016-09-06
\| \| \| \|	cleaning up freeze-related organization and definitions along the way
*	updated GF25519 to match new exponentiation chain code	jadep	2016-08-31
\|
*	Added square roots to GF1305, started reworking freeze_opt in preparation ↵	jadep	2016-08-31
\| \| \| \|	for instantiating it in GF25519 (needed for equality comparison in sqrt_5mod8)
*	Replaced placeholdeer [opp] operation in ModularBaseSystem with a real ↵	jadep	2016-08-24
\| \| \| \|	implementation, and pushed that up through Specific.
*	Added optimized [inv] operation to Specific, and removed dependencies on ↵	jadep	2016-08-24
\| \| \| \|	ModularBaseSystemField.v
*	Shifted around some of the proofs in ModularBaseSystemField.v and propagated ↵	jadep	2016-08-23
\| \| \| \|	field proof through GF1305.v as a proof of concept; working towards deleting that ModularBaseSystemField.v
*	Speed up src/Specific/GF25519.v (#54)	Jason Gross	2016-08-18
\| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ----------------------------------------------------------------- 0m13.37s \| Total \| 0m40.29s \|\| -0m26.91s ----------------------------------------------------------------- 0m10.09s \| Specific/GF25519 \| 0m37.00s \|\| -0m26.91s 0m03.29s \| Experiments/SpecificCurve25519 \| 0m03.30s \|\| -0m00.00s
*	Updated GF files to reflect change in [repeat]	jadep	2016-08-16
\|
*	Added specific versions of [pack] and [unpack] to GF1305.v	jadep	2016-08-16
\|
*	Merge of conversion development branch with master	jadep	2016-08-16
\|\
\| *	Added specific versions of [pack] and [unpack] to GF25519	jadep	2016-08-16
\|/
*	Tweaked structure of GF [carry_mul] so that carry chain is specified in ↵	jadep	2016-08-09
\| \| \| \|	Specific.
*	Refactor ModularArithmetic into Zmod, expand Decidable	Andres Erbsen	2016-08-04
\| \| \| \| \| \| \| \| \| \| \| \|	ModularArithmetic now uses Algebra lemmas in various places instead of custom manual proofs. Similarly, Util.Decidable is used to state and prove the relevant decidability results. Backwards-incompatible changes: F_some_lemma -> Zmod.some_lemma Arguments ZToField _%Z _%Z : clear implicits. inv_spec says inv x * x = 1, not x * inv x = 1
*	Removed lingering print statement.	jadep	2016-07-21
\|
*	re-introduced extra field isomorphism layer for 8.4 compatibility and better ↵	jadep	2016-07-21
\| \| \| \|	organization of reasoning.
*	restructured ModularBaseSystem pipeline to put tuple conversion before ↵	jadep	2016-07-20
\| \| \| \|	ModularBaseSystem is fully defined, rather than after ModularBaseSystemOpt
*	Fixed unsimplified multiplication definitions in Specific by separating out ↵	jadep	2016-07-18
\| \| \| \|	the zsimplify step; after inserting clauses, we can't rewrite under the binders, but we can do the rewrite and insertions in different definitions.
*	more changes to Specific for 8.4 compatibility	jadep	2016-07-15
\|
*	re-cleaned operations in Specific and updated GF25519 to match GF1305	jadep	2016-07-12
\|
*	cleaned Specific operations so they produce code without proof terms, and ↵	jadep	2016-07-12
\| \| \| \|	proved that GF1305 is a field
*	pushing through a tweak to the arguments of [sub], and defining a field over ↵	jadep	2016-07-12
\| \| \| \|	ModularBaseSystemInterface using some placeholder operations.
*	ported Specific files to use ModularBaseSystemInterface	jadep	2016-07-11
\|
*	defined some group operations, stated group lemma for tuple-based [add] (in ↵	jadep	2016-07-08
\| \| \| \|	terms of isomorphism to ModularArithmetic.F), proved lemma about tuple-based [mul] based on the goals generated by the group constructor
*	stuck trying to figure out dependently typed continuation passing style	Andres Erbsen	2016-07-06
\|
*	Aggregate all level specifications not in Spec/*	Jason Gross	2016-06-22
\| \| \| \| \|	This prevents notation conflicts (see comment in Notations.v for more explanation).
*	remove obsolete rep mechanism	Andres Erbsen	2016-06-20
\|
*	GF25519: quiet	Andres Erbsen	2016-06-20
\|
*	Merge branch 'field-experiment'	Andres Erbsen	2016-06-20
\|\ \| \| \| \| \| \|	includes broken files to be removed in next commit
* \|	Canonicalization is now automated in GF25519 and added to GF1305.	jadep	2016-06-17
\| \|
* \|	Specific version of freeze for GF25519 (automation still needs a little work)	jadep	2016-06-17
\| \|
* \|	PseudoMersenneBaseRep.mul now carries by default (made possible by strictly ↵	jadep	2016-06-15
\| \| \| \| \| \| \| \|	base-length digit vectors)
* \|	Another fix for an anomaly in 8.4pl2	Jason Gross	2016-06-11
\| \|
* \|	Work around bug #4811 (slow f_equal)	Jason Gross	2016-06-11
\| \| \| \| \| \| \| \| \| \|	This is https://coq.inria.fr/bugs/show_bug.cgi?id=4811, [f_equal] loops(?) in 8.5pl1 (fixed already in 8.5.dev)
\| *	ed25519: refactor some Proper	Andres Erbsen	2016-06-06
\| \|
\| *	rewrite in Let_In binder by tactic	Andres Erbsen	2016-06-04
\| \|
\| *	Let_In rewriting	Andres Erbsen	2016-06-03
\| \|
\| *	leibniz equal version of topdown rewriting of sigma types: nicer	Andres Erbsen	2016-06-01
\| \|
\| *	leibniz equal version of topdown rewriting of sigma types	Andres Erbsen	2016-06-01
\| \|
\| *	E impl: proper morphisms are hard to dow without setoids	Andres Erbsen	2016-05-30
\| \|
\| *	ERep add	Andres Erbsen	2016-05-29
\| \|
\| *	--amend	Andres Erbsen	2016-05-28
\| \|
\| *	verify derivation, EdDSA layer: allow arbitrary equivalence relation for ↵	Andres Erbsen	2016-05-28
\| \| \| \| \| \| \| \|	ERep and SRep
\| *	verify derivation, EdDSA layer: remove unused context variables	Andres Erbsen	2016-05-28
\| \|
\| *	verify derivation: EdDSA layer	Andres Erbsen	2016-05-28
\| \|
\| *	right after scalars to F l	Andres Erbsen	2016-05-27
\| \|
\| *	before changing SRep from N to F l	Andres Erbsen	2016-05-27
\|/
*	ed25519: indentation fix	Andres Erbsen	2016-05-24
\|