fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	compute on [F q]!	Andres Erbsen	2016-07-20
\|
*	experiments wd25519: simplify proof for a	Andres Erbsen	2016-07-20
\|
*	Move mul_rep_extended (do we actually care about this?)	Jason Gross	2016-07-20
\|
*	Don't use auto with *	Jason Gross	2016-07-20
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It's fragile and slow. Now we're 45 seconds faster. After \| File Name \| Before \|\| Change ------------------------------------------------------------------------------- 1m03.42s \| Total \| 1m49.00s \|\| -0m45.57s ------------------------------------------------------------------------------- 0m20.01s \| ModularArithmetic/ModularBaseSystemProofs \| 1m05.69s \|\| -0m45.67s 0m32.14s \| Specific/GF25519 \| 0m31.92s \|\| +0m00.21s 0m07.05s \| Specific/GF1305 \| 0m07.07s \|\| -0m00.02s 0m02.84s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.90s \|\| -0m00.06s 0m00.69s \| Experiments/SpecificCurve25519 \| 0m00.69s \|\| +0m00.00s 0m00.69s \| ModularArithmetic/ModularBaseSystemInterface \| 0m00.73s \|\| -0m00.04s
*	Absolutize some imports	Jason Gross	2016-07-20
\|
*	Remove dependency of ext_base on pseudomersenne	Jason Gross	2016-07-20
\|
*	Add Z.lt_le_incl to zarith	Jason Gross	2016-07-20
\|
*	Add another lemma about +, <= to arith	Jason Gross	2016-07-20
\|
*	Use a proof that doesn't require as many assumptions in extended_base_length	Jason Gross	2016-07-20
\|
*	Work around bad design in Coq	Jason Gross	2016-07-19
\| \| \| \| \|	This is https://coq.inria.fr/bugs/show_bug.cgi?id=4949, [intuition] should not use [auto with *] by default
*	Add a distr_length database	Jason Gross	2016-07-19
\|
*	Remove stuff from PseudoMersenneBaseParamProofs.v	Jason Gross	2016-07-19
\|
*	{base} -> base	Jason Gross	2016-07-19
\|
*	Move two_k_nonzero to PseudoMersenneBaseParamProofs.v	Jason Gross	2016-07-19
\| \| \| \|	It has nothing to do with ext_base
*	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.