fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Fix changed qualified tactic name	Jason Gross	2017-01-17
\|
*	Add ladderstep_other_assoc	Jason Gross	2017-01-07
\|
*	Add more generic ladderstep	Jason Gross	2017-01-07
\|
*	implement X25519	Andres Erbsen	2016-11-06
\|
*	move B_order_l and prime_q	Andres Erbsen	2016-11-06
\|
*	put EdDSA encoding sign bit at the MSB	Andres Erbsen	2016-11-04
\|
*	Filled in point/scalar encoding definitions.	jadep	2016-10-10
\|
*	Ed25519: add basepoint and prove most EdDSA preconditions	Andres Erbsen	2016-10-10
\|
*	Spec.Ed25519: prove that Curve25519 is an elliptic curve	Andres Erbsen	2016-10-10
\|
*	Spec.Ed25519: fix exponent field modulus	Andres Erbsen	2016-10-10
\|
*	Moved PointEncoding out of Spec	jadep	2016-10-06
\|
*	Fixed a lingering inappropriate use of Logic.eq	jadep	2016-10-06
\|
*	fix 8.4 build	jadep	2016-10-03
\|
*	A couple hotfixes; recent commits somehow broke things	jadep	2016-10-03
\|
*	Wrote proofs necessary to fill in all point-encoding related context ↵	jadep	2016-10-03
\| \| \| \|	variables in EdDSARepChange.v
*	Ed25519: use Global Instance	Andres Erbsen	2016-10-03
\|
*	Spec: add ed25519	Andres Erbsen	2016-10-03
\|
*	MxDH: do not depend on implicit import of list notations	Andres Erbsen	2016-09-26
\|
*	add Montgomery x-coordinate Diffie-Hellman and Curve25519	Andres Erbsen	2016-09-26
\|
*	alternative signing derivation	Andres Erbsen	2016-09-22
\| \| \| \|	cleanup
*	Derive EdDSA.verify from equational specification	Andres Erbsen	2016-09-16
\| \| \| \|	Experiments/SpecEd25519 will come back soon
*	ModularArithmetic: conversions between [F] and [nat]	Andres Erbsen	2016-09-16
\|
*	Fully qualify [Require]s	Jason Gross	2016-09-08
\| \| \| \|	This way they won't become ambiguous if we add new files
*	remove eq_dec from Monoid	Andres Erbsen	2016-08-23
\|
*	[cbv beta] in the beginning of Obligation Tactic for 8.5	Andres Erbsen	2016-08-08
\|
*	[F] has its own module now	Andres Erbsen	2016-08-05
\| \| \| \| \| \|	[ZToField] -> [F.of_Z] [FieldToZ] -> [F.to_Z] [Zmod.lem] -> [F.lem]
*	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
*	compute on [F q]!	Andres Erbsen	2016-07-20
\|
*	remove field_algebra	Andres Erbsen	2016-07-11
\|
*	added proofs about addition chain exponentiation for later use in ↵	jadep	2016-07-10
\| \| \| \|	ModularBaseSystem [pow], which we need for sqrt and inversion.
*	Define the spec of Weierstrass curves (#6)	Jason Gross	2016-07-03
\| \| \| \| \|	Define the spec of Weierstrass curves This is the start of work on P256.
*	scalarmult support; EdDSA.sign produces valid signatures	Andres Erbsen	2016-06-27
\|
*	EdDSA: prove things about spec	Andres Erbsen	2016-06-25
\|
*	EdDSA.Notations: indentation	Andres Erbsen	2016-06-22
\|
*	Fix broken notations (hopefully)	Jason Gross	2016-06-22
\|
*	Handle renaming of NPeano.pow to Nat.pow (#3)	Jason Gross	2016-06-22
\| \| \| \|	We leave ambiguous which [pow] and [modulo] we refer to, so that this builds in both 8.4 and 8.5
*	EdDSA.v: resolve ambiguity based on ed25519.py	Andres Erbsen	2016-06-21
\|
*	Whitespace change	Jason Gross	2016-06-21
\|
*	use Local Obligation Tactic (8.5-compat)	Andres Erbsen	2016-06-21
\|
*	remove trailing whitespace from src/	Andres Erbsen	2016-06-20
\|
*	Remove anything incompatible with new algebraic hierarcy	Andres Erbsen	2016-06-20
\| \| \| \| \| \|	- PointEncoding (these will hopefully come back soon) - EdDSAProofs (not a priority to bring back, but not hard either) - Ed25519 spec bits and pieces which were not finished anyway
*	Merge branch 'field-experiment'	Andres Erbsen	2016-06-20
\|\ \| \| \| \| \| \|	includes broken files to be removed in next commit
\| *	port EdDSA spec	Andres Erbsen	2016-06-20
\| \|
\| *	move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems	Andres Erbsen	2016-06-17
\| \|
\| *	port edwards curve spec	Andres Erbsen	2016-06-16
\| \|
* \|	Minor 8.5 changes	Jason Gross	2016-06-10
\| \|
* \|	More changes for 8.5	Jason Gross	2016-06-10
\| \| \| \| \| \| \| \|	[Local Coercion :=] changed meanings. Use [Let] and [Local Coercion] for consistent behavior
\| *	before changing SRep from N to F l	Andres Erbsen	2016-05-27
\|/
*	Changed name of Encoding to CanonicalEncoding, and changed notation to match.	jadep	2016-04-29
\|
*	Moved sign_bit definition to Spec.	jadep	2016-04-29
\|