fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
\| \| *	Add more distr_length proofs in BaseSystemProofs	Jason Gross	2016-07-18
\| \| \|
\| \| *	Add more natsimplify le_dec lemmas	Jason Gross	2016-07-18
\| \| \|
\| \| *	Add more NatUtil lemmas	Jason Gross	2016-07-18
\| \| \|
\| \| *	Add natsimplify lemmas about eq_nat_dec	Jason Gross	2016-07-18
\| \| \|
\| \| *	Fix some typos in the previous commit	Jason Gross	2016-07-18
\| \| \|
\| \| *	Add some lemmas about nth_default in bounds	Jason Gross	2016-07-18
\| \| \|
\| \| *	Remove a nested proof	Jason Gross	2016-07-18
\| \|/ \| \| \| \| \| \| \| \|	Fix for Warning: Nested proofs are deprecated and will stop working in a future Coq version [deprecated-nested-proofs,deprecated]
* \|	changed base notation	jadep	2016-07-18
\| \|
\| *	Move some definitions to Pow2Base (#24)	Jason Gross	2016-07-18
\|/ \| \| \| \| \| \| \| \|	* Move some definitions to Pow2Base These definitions don't depend on PseudoMersenneBaseParams, only on limb_widths, and we'll want them for BarrettReduction / P256. * Fix for Coq 8.4
*	ported IterAssocOp to use monoid rather than a billion context variables ↵	jadep	2016-07-18
\| \| \| \|	that add up to a monoid
*	rewrote Testbit and factored out some necessary lemmas about 'uniform' bases ↵	jadep	2016-07-18
\| \| \| \|	(bases that are repeats of the same power of 2) into Pow2Base
*	Added lemmas to ZUtil and NatUtil (for Testbit)	jadep	2016-07-18
\|
*	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.
*	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-07-15
\|\
* \|	proved an admit in field homomorphisms that turned out to be unprovable; I ↵	jadep	2016-07-15
\| \| \| \| \| \| \| \|	added another precondition and pushed it through everywhere but one place in ExtendedCoordinates, where I was stuck.
* \|	more changes to Specific for 8.4 compatibility	jadep	2016-07-15
\| \|
\| *	Experiments/SpecificCurve25519.v: curve25519 addition using small Z-s	Andres Erbsen	2016-07-13
\| \|
\| *	tuple: applying functions to tuples of arbitrary length	Andres Erbsen	2016-07-12
\|/
*	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
*	removing experimental file accidentally included in last commit	jadep	2016-07-12
\|
*	pushing through a tweak to the arguments of [sub], and defining a field over ↵	jadep	2016-07-12
\| \| \| \|	ModularBaseSystemInterface using some placeholder operations.
*	prove that if something is isomorphic to a field, it is a field	jadep	2016-07-11
\|
*	Merge pull request #21 from JasonGross/base-log-cap-notations	jadephilipoom	2016-07-11
\|\ \| \| \| \|	Make [base] and [log_cap] notations
* \|	An attempt at fixing 8.5pl2	Jason Gross	2016-07-11
\| \| \| \| \| \|	See #23
\| *	Make [base] and [log_cap] notations	Jason Gross	2016-07-11
\|/ \| \| \| \| \| \| \|	Also use [ZUtil.Z.pow2_mod]. This lets us remove the dependency of ModularBaseSystem on ModularArithmetic.PseudoMersenneBaseParamProofs. This is a small part of reorganizing and factoring ModularBaseSystem for use with Barrett reduction.
*	Merge of fixedlength and master	jadep	2016-07-11
\|\
* \|	ported Specific files to use ModularBaseSystemInterface	jadep	2016-07-11
\| \|
\| *	Merge pull request #22 from mit-plv/wrap-nsatz	Andres Erbsen	2016-07-11
\| \|\ \| \| \| \| \| \|	stop using raw nsatz, field_algebra, common_denominator
\| \| *	s/conservative_common_denominator/common_denominator/g	Andres Erbsen	2016-07-11
\| \| \|
\| \| *	rename [common_denominator] to [field_simplify_if_div]	Andres Erbsen	2016-07-11
\| \| \|
\| \| *	remove field_algebra	Andres Erbsen	2016-07-11
\| \| \|
\| \| *	port CompleteEdwardsCurveTheorems (builds again)	Andres Erbsen	2016-07-11
\| \| \|
\| \| *	pose proof fails where specialize works (typeclass resolution / unification?)	Andres Erbsen	2016-07-11
\| \| \|
\| \| *	wrap nsatz in Algebra	Andres Erbsen	2016-07-11
\| \|/
\| *	[congruence] is more powerful in 8.5 than in 8.4	Andres Erbsen	2016-07-11
\| \|
\| *	Add 8.5pl2 to travis	Jason Gross	2016-07-11
\| \|
\| *	merge	jadep	2016-07-10
\| \|\
\| * \|	added proofs about addition chain exponentiation for later use in ↵	jadep	2016-07-10
\| \| \| \| \| \| \| \| \| \| \| \|	ModularBaseSystem [pow], which we need for sqrt and inversion.
\| \| *	Update .gitignore	Jason Gross	2016-07-10
\| \| \|
\| \| *	Fix ListUtil for Coq 8.4	Jason Gross	2016-07-10
\| \| \|
\| \| *	Update ListUtil	Jason Gross	2016-07-08
\| \| \|
\| \| *	Fix NatUtil for 8.4	Jason Gross	2016-07-08
\| \| \|
\| \| *	Add useful tactics and util lemmas	Jason Gross	2016-07-08
\| \| \|
* \| \|	proved correctness of [add] operation in ModularBaseSystemInterface	jadep	2016-07-08
\| \| \|
* \| \|	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
* \| \|	added a few length proofs to ModularBaseSystemProofs to help with tuple ↵	jadep	2016-07-08
\| \| \| \| \| \| \| \| \| \| \| \|	conversion
\| \| *	Add a NatUtil lemma and db	Jason Gross	2016-07-08
\| \| \|
\| \| *	Add a ListUtil lemma	Jason Gross	2016-07-08
\| \| \|
\| \| *	Add a ListUtil lemma	Jason Gross	2016-07-08
\| \| \|