fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Fix side-condition from previous commit	Jason Gross	2016-07-19
\|
*	Add another lemma to distr_length	Jason Gross	2016-07-19
\|
*	Use update_nth in add_to_nth (#26)	Jason Gross	2016-07-19
\| \| \| \| \| \|	It leads to a slightly more transparent and clearer definition. If I got everything right, nothing should depend on the judgmental definition of [add_to_nth] anymore.
*	ext_base: now defined in terms of ext_limb_widths	Jason Gross	2016-07-18
\|
*	Add a lemma about base_from_limb_widths and app	Jason Gross	2016-07-18
\|
*	Add a lemma about sum_firstn	Jason Gross	2016-07-18
\|
*	Add a ListUtil lemma	Jason Gross	2016-07-18
\|
*	Move more proofs earlier	Jason Gross	2016-07-18
\|
*	Make Pow2BaseProofs independent of the def of add_to_nth	Jason Gross	2016-07-18
\|
*	Silence a warning	Jason Gross	2016-07-18
\| \| \| \| \| \| \| \| \|	File "./src/Experiments/GenericFieldPow.v", line 130, characters 4-471: Warning: Casts are ignored in patterns [cast-in-pattern,automation] @andres-erbsen Did you intend for the cast at https://github.com/mit-plv/fiat-crypto/commit/6823b63275333ebb11c7f84068894f76cdb06068#diff-078114b2627a38e74938989c7ca2f6d1R131 to have semantic meaning for some reason, performance or otherwise?
*	Express carry_simple in terms of carry_gen	Jason Gross	2016-07-18
\| \| \| \| \| \|	Also make much of the remaining code outside of Pow2BaseProofs independent of the precise definition of carry_simple. (We use [Local Opaque] to enforce this modularity.
*	Fix for Coq 8.4 (missing lemmas)	Jason Gross	2016-07-18
\|
*	Fix for Coq 8.4 (omega used to be weaker)	Jason Gross	2016-07-18
\|
*	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]
*	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
\|
*	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
\| \|
\| *	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
\| \|
\| *	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.
\| \| *	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
\| \| \|